Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion .github/workflows/affinescript-verify.yml
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,11 @@ jobs:
- name: Checkout AffineScript compiler
if: steps.changed.outputs.any == 'true'
# advisory: compiler checkout is report-only until the port backlog
# is cleared and BLOCKING flips to true.
# is cleared and BLOCKING flips to true. "Verify changed .affine
# files" below checks steps.build.outputs.ok and the checkout dir,
# and on toolchain-unavailable emits an explicit ::warning:: +
# step-summary "SKIPPED — not a pass" instead of a silent green claim.
# hypatia: allow research_extensions/RE005 -- advisory-by-design, fails OPEN not closed; see comment above.
continue-on-error: true
uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/changelog-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ jobs:
if ! diff -q CHANGELOG.md CHANGELOG.md.new >/dev/null; then
echo "ERROR: CHANGELOG.md is out of date relative to commit history."
echo "Run git-cliff locally or switch to mode=commit-back."
diff -u CHANGELOG.md CHANGELOG.md.new | head -60 || true
diff -u CHANGELOG.md CHANGELOG.md.new | head -60
exit 1
fi
echo "CHANGELOG.md is up to date."
Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/ci-pipeline.yml
Original file line number Diff line number Diff line change
Expand Up @@ -524,6 +524,7 @@ jobs:
# Comments are stripped first: `_base.ncl` documents its own usage
# in a `#` comment containing a literal `import "../_base.ncl"`, and
# matching that would skip a file that typechecks perfectly well.
# hypatia: allow research_extensions/RE005 -- `|| true` absorbs grep's exit 1 on a file with no imports; an empty import list is the correct answer there, and the typecheck below still gates.
done < <(sed 's/#.*//' "$f" | grep -oE 'import[[:space:]]+"[^"]+"' | sed -E 's/.*"([^"]+)".*/\1/' || true)

if [ -n "$MISSING" ]; then
Expand Down Expand Up @@ -615,6 +616,7 @@ jobs:
sparse-checkout-cone-mode: false
# Not fatal here: the next step names precisely what was missing and
# then FAILS CLOSED. A fetch failure must never read as an exemption.
# hypatia: allow research_extensions/RE005 -- deliberate fail-closed: "Refuse Deno unless this repository is ledgered" below checks for the ledger file and exits 1 with an explicit ::error:: if missing, regardless of why.
continue-on-error: true

- name: Refuse Deno unless this repository is ledgered
Expand Down Expand Up @@ -1037,6 +1039,7 @@ jobs:
.machine_readable/pipeline-allow.txt
sparse-checkout-cone-mode: false
# Not fatal: the next step names what was missing and then FAILS CLOSED.
# hypatia: allow research_extensions/RE005 -- deliberate fail-closed: the Verdict step below treats an unreadable ledger exactly like an empty one, i.e. blocked.
continue-on-error: true

- name: Verdict — block unless this repository is ledgered
Expand Down
13 changes: 11 additions & 2 deletions .github/workflows/echidna-verify.yml
Original file line number Diff line number Diff line change
Expand Up @@ -124,14 +124,23 @@ jobs:
id: typecheck
if: steps.guard.outputs.present == 'true'
run: |
set -e
set -eo pipefail
echo "=== Agda proofs under lol/proofs ==="
find lol/proofs/theories -name '*.agda' -print
cd lol/proofs
failed=""
for f in $(find theories -name '*.agda'); do
echo "--- checking $f ---"
agda --safe "$f" 2>&1 | tee -a ../../agda-verify.log || true
if ! agda --safe "$f" 2>&1 | tee -a ../../agda-verify.log; then
failed="$failed$f"$'\n'
fi
done
if [ -n "$failed" ]; then
echo "::warning::agda --safe FAILED to type-check the following proof(s) (advisory until the evicted lol/proofs corpus's re-entry criteria are set; see issue #748):"
printf '%s' "$failed" | sed 's/^/ - /'
else
echo "All Agda proofs type-checked cleanly."
fi

- name: Postulate audit
if: steps.guard.outputs.present == 'true'
Expand Down
86 changes: 57 additions & 29 deletions .github/workflows/governance-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -550,12 +550,12 @@ jobs:
# failures because `find` crawled gitignored vendor directories.
# `git ls-files` works correctly on fresh PR checkouts because
# actions/checkout populates the index before running workflows.
RES_FILES=$(git ls-files '*.res' || true)
GO_FILES=$(git ls-files '*.go' || true)
RES_FILES=$(git ls-files '*.res')
GO_FILES=$(git ls-files '*.go')
PY_FILES=$(git ls-files '*.py' \
| grep -v venv | grep -v __pycache__ || true)
| grep -v venv | grep -v __pycache__ || [ $? -eq 1 ])
MAKE_FILES=$(git ls-files 'Makefile' 'Makefile.*' '*.mk' \
| grep -v '\.github/' || true)
| grep -v '\.github/' || [ $? -eq 1 ])
# Platform-required JVM shims carve-out 2026-06-02:
# Java is permitted only in Android source trees
# (android/**/src/**/*.java) because Android instantiates
Expand All @@ -574,12 +574,12 @@ jobs:
# only remaining Java carve-out is the minimal Android platform
# shim above. `.groovy` is detected so it is banned everywhere.
JAVA_FILES=$(git ls-files '*.java' '*.kt' '*.kts' '*.groovy' \
| grep -vE '(^|/)android/.*/src/.*\.java$' || true)
SWIFT_FILES=$(git ls-files '*.swift' || true)
DART_FILES=$(git ls-files '*.dart' 'pubspec.yaml' || true)
| grep -vE '(^|/)android/.*/src/.*\.java$' || [ $? -eq 1 ])
SWIFT_FILES=$(git ls-files '*.swift')
DART_FILES=$(git ls-files '*.dart' 'pubspec.yaml')
# V-lang detected by manifest (v.mod / vpkg.json); the .v extension
# collides with Verilog so we never key on it.
VMOD_FILES=$(git ls-files 'v.mod' 'vpkg.json' || true)
VMOD_FILES=$(git ls-files 'v.mod' 'vpkg.json')

enforce "ReScript files" "use AffineScript instead" "$RES_FILES"
enforce "Go files" "use Rust/WASM instead" "$GO_FILES"
Expand All @@ -603,10 +603,10 @@ jobs:
# runtime impossible, not merely awkward. It blocked what the policy
# mandates. Bun artifacts are now accepted; npm and yarn are unchanged.
run: |
LOCK_FILES=$(git ls-files 'package-lock.json' '**/package-lock.json' 2>/dev/null || true)
YARN_FILES=$(find . -name "yarn.lock" -not -path "./.git/*" 2>/dev/null || true)
NPMRC_FILES=$(find . -name ".npmrc" -not -path "./.git/*" 2>/dev/null || true)
BUN_LOCK=$(find . \( -name "bun.lock" -o -name "bun.lockb" \) -not -path "./.git/*" 2>/dev/null || true)
LOCK_FILES=$(git ls-files 'package-lock.json' '**/package-lock.json' 2>/dev/null)
YARN_FILES=$(find . -name "yarn.lock" -not -path "./.git/*" 2>/dev/null)
NPMRC_FILES=$(find . -name ".npmrc" -not -path "./.git/*" 2>/dev/null)
BUN_LOCK=$(find . \( -name "bun.lock" -o -name "bun.lockb" \) -not -path "./.git/*" 2>/dev/null)
FAILED=""
if [ -n "$LOCK_FILES" ]; then
echo "❌ Tracked package-lock.json detected (standards#67 — npm-avoidant)."
Expand Down Expand Up @@ -764,17 +764,17 @@ jobs:
- name: Security checks
run: |
FAILED=false
WEAK_CRYPTO=$(grep -rE 'md5\(|sha1\(' --include="*.py" --include="*.rb" --include="*.js" --include="*.ts" --include="*.go" --include="*.rs" . 2>/dev/null | grep -v 'checksum\|cache\|test\|spec' | head -5 || true)
WEAK_CRYPTO=$(grep -rE 'md5\(|sha1\(' --include="*.py" --include="*.rb" --include="*.js" --include="*.ts" --include="*.go" --include="*.rs" . 2>/dev/null | grep -v 'checksum\|cache\|test\|spec' | head -5)
if [ -n "$WEAK_CRYPTO" ]; then
echo "⚠️ Weak crypto (MD5/SHA1) detected. Use SHA256+ for security:"
echo "$WEAK_CRYPTO"
fi
HTTP_URLS=$(grep -rE 'http://[^l][^o][^c]' --include="*.py" --include="*.js" --include="*.ts" --include="*.go" --include="*.rs" --include="*.yaml" --include="*.yml" . 2>/dev/null | grep -v 'localhost\|127.0.0.1\|example\|test\|spec' | head -5 || true)
HTTP_URLS=$(grep -rE 'http://[^l][^o][^c]' --include="*.py" --include="*.js" --include="*.ts" --include="*.go" --include="*.rs" --include="*.yaml" --include="*.yml" . 2>/dev/null | grep -v 'localhost\|127.0.0.1\|example\|test\|spec' | head -5)
if [ -n "$HTTP_URLS" ]; then
echo "⚠️ HTTP URLs found. Use HTTPS:"
echo "$HTTP_URLS"
fi
SECRETS=$(grep -rEi '(api_key|apikey|secret_key|password)\s*[=:]\s*["\x27][A-Za-z0-9+/=]{20,}' --include="*.py" --include="*.js" --include="*.ts" --include="*.go" --include="*.rs" --include="*.env" . 2>/dev/null | grep -v 'example\|sample\|test\|mock\|placeholder' | head -3 || true)
SECRETS=$(grep -rEi '(api_key|apikey|secret_key|password)\s*[=:]\s*["\x27][A-Za-z0-9+/=]{20,}' --include="*.py" --include="*.js" --include="*.ts" --include="*.go" --include="*.rs" --include="*.env" . 2>/dev/null | grep -v 'example\|sample\|test\|mock\|placeholder' | head -3)
if [ -n "$SECRETS" ]; then
echo "❌ Potential hardcoded secrets detected!"
FAILED=true
Expand Down Expand Up @@ -1001,26 +1001,50 @@ jobs:
# same merge commit but is always fetchable.
ref: ${{ github.sha }}
- name: Check file permissions
# advisory: informational only; repos can opt into blocking locally.
# No continue-on-error needed: the step below always exits 0 itself;
# it now surfaces its finding as an explicit ::warning:: instead of a
# silent printout.
run: |
find . -type f -perm /111 -name "*.sh" | head -20
continue-on-error: true
# advisory: informational only; repos can opt into blocking locally
FOUND=$(find . -type f -perm /111 -name "*.sh" | head -20)
if [ -n "$FOUND" ]; then
echo "::warning::Executable .sh files found (informational only):"
echo "$FOUND"
else
echo "No executable .sh files found."
fi
- name: Check TODO/FIXME
# advisory: informational only; repos can opt into blocking locally.
run: |
echo "=== TODOs ==="
grep -rn "TODO\|FIXME\|HACK\|XXX" --include="*.rs" --include="*.res" --include="*.py" --include="*.ex" . | head -20
continue-on-error: true
# advisory: informational only; repos can opt into blocking locally
FOUND=$(grep -rn "TODO\|FIXME\|HACK\|XXX" --include="*.rs" --include="*.res" --include="*.py" --include="*.ex" . | head -20)
if [ -n "$FOUND" ]; then
echo "::warning::TODO/FIXME/HACK/XXX markers found (informational only):"
echo "$FOUND"
else
echo "No TODO/FIXME/HACK/XXX markers found."
fi
- name: Check for large files
# advisory: informational only; repos can opt into blocking locally.
run: |
find . -type f -size +1M -not -path "./.git/*" | head -20
continue-on-error: true
# advisory: informational only; repos can opt into blocking locally
FOUND=$(find . -type f -size +1M -not -path "./.git/*" | head -20)
if [ -n "$FOUND" ]; then
echo "::warning::Files larger than 1M found (informational only):"
echo "$FOUND"
else
echo "No files larger than 1M found."
fi
- name: EditorConfig check
id: editorconfig_check
uses: editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393 # v3.0.0
# advisory: formatting hygiene is reported from the reusable estate
# bundle; repos opt into blocking formatter checks locally when ready.
# advisory-by-design, fails OPEN not closed: formatting hygiene is
# reported from the reusable estate bundle; the follow-up step below
# emits ::warning:: explicitly when this fails instead of silently
# swallowing it. Repos opt into blocking formatter checks locally.
# hypatia: allow research_extensions/RE005 -- advisory-by-design, fails OPEN; see comment above.
continue-on-error: true
- name: EditorConfig check - surface result
if: steps.editorconfig_check.outcome == 'failure'
run: echo "::warning::EditorConfig check found formatting issues (advisory only — see the 'EditorConfig check' step's own log above; repos opt into blocking locally when ready)."
# Sparse-check-out standards' scripts/ for the docs gate (a reusable
# workflow only auto-checks-out its own YAML, not sibling scripts).
- name: Check out standards for the docs gate
Expand Down Expand Up @@ -1190,7 +1214,7 @@ jobs:
fi
- name: Mixed content check
run: |
MIXED=$(grep -rE 'src="http://|href="http://' --include="*.html" --include="*.htm" . 2>/dev/null | grep -vE 'localhost|127\.0\.0\.1|example\.com|lol/|node_modules/|third-party/|vendor/' | head -5 || true)
MIXED=$(grep -rE 'src="http://|href="http://' --include="*.html" --include="*.htm" . 2>/dev/null | grep -vE 'localhost|127\.0\.0\.1|example\.com|lol/|node_modules/|third-party/|vendor/' | head -5)
if [ -n "$MIXED" ]; then
echo "::error::Mixed content (HTTP in HTML)"
echo "$MIXED"
Expand Down Expand Up @@ -1233,6 +1257,10 @@ jobs:
# very PR merges. An immutable pin removes the race entirely: the names
# at this SHA are fixed. The self-lint fallback in the next step still
# covers standards' own tree, where a rename lands before the bump.
# "Duplicate YAML keys in workflows" below refuses to run (::error:: +
# exit 1) when neither the fetched nor the self-hosted copy of the
# checker script is present, regardless of why the fetch failed.
# hypatia: allow research_extensions/RE005 -- deliberate fail-closed: see comment above.
continue-on-error: true

- name: Duplicate YAML keys in workflows
Expand Down Expand Up @@ -1442,7 +1470,7 @@ jobs:
# branches): 200 carry actions.lock, 163 do not, 5 have no workflows
# directory. The ledger makes that 163 an explicit, shrinking debt
# instead of a cliff.
total=$(grep -cve '^[[:space:]]*$' -e '^[[:space:]]*#' "$RUNNER_TEMP/lock-allow.txt" || true)
total=$(grep -cve '^[[:space:]]*$' -e '^[[:space:]]*#' "$RUNNER_TEMP/lock-allow.txt" || [ $? -eq 1 ])
: "${total:=0}"
# The ledger excuses missing-lock debt ONLY (gate exit 3: lockless,
# every ref pinned, grace window closed). Exit 1 is a LIVE
Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/hypatia-scan-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,12 @@ jobs:
# the filter itself would produce exactly the fake gate this estate
# keeps finding. Pinned to main because github.workflow_sha resolves to
# the CALLER's SHA, which would 404 here.
# advisory-by-design, not fail-closed: this checkout fails OPEN.
# "Filter SARIF through the baseline before upload" below falls back
# to uploading the SARIF UNFILTERED when the fetched filter script is
# unavailable — an unfiltered upload can only show more alerts, never
# hide real ones.
# hypatia: allow research_extensions/RE005 -- advisory-by-design, fails OPEN; see comment above.
continue-on-error: true
uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/readme-derive-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@ jobs:
elif ! diff -q <(norm "$RUNNER_TEMP/derived.md") <(norm "$DERIVED_PATH") >/dev/null; then
echo "::error::'$DERIVED_PATH' is STALE relative to '$CANONICAL'. Regenerate and commit it."
echo "----- diff (committed vs regenerated, normalised) -----"
diff <(norm "$DERIVED_PATH") <(norm "$RUNNER_TEMP/derived.md") || true
diff <(norm "$DERIVED_PATH") <(norm "$RUNNER_TEMP/derived.md") || [ $? -eq 1 ]
SHOW_CMD=1
else
echo "✓ $DERIVED_PATH is up to date with $CANONICAL"
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/scorecard-enforcer.yml
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ jobs:
- name: Check for pinned dependencies
run: |
# Check workflows for unpinned actions
unpinned=$(grep -r "uses:.*@v[0-9]" .github/workflows/*.yml 2>/dev/null | grep -v "#" | head -5 || true)
unpinned=$(grep -r "uses:.*@v[0-9]" .github/workflows/*.yml 2>/dev/null | grep -v "#" | head -5)
if [ -n "$unpinned" ]; then
echo "::warning::Found unpinned actions:"
echo "$unpinned"
Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/secret-scanner-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -628,15 +628,15 @@ jobs:
| grep -vE "$COMMENT" \
| grep -vE "$ENV_RHS" \
| grep -vE "$URL_RHS" \
| grep -vE "$PRAGMA" || true)"
| grep -vE "$PRAGMA" || [ $? -eq 1 ])"
[ -n "$hits" ] || continue

# ./src was the only path the previous version scanned. Hits there
# keep blocking exactly as before — no regression. Hits outside it
# are newly visible, so they warn until the cutoff rather than
# reddening repos that were never actually being scanned.
old_scope="$(printf '%s\n' "$hits" | grep -E '^\./src/' || true)"
new_scope="$(printf '%s\n' "$hits" | grep -vE '^\./src/' || true)"
old_scope="$(printf '%s\n' "$hits" | grep -E '^\./src/' || [ $? -eq 1 ])"
new_scope="$(printf '%s\n' "$hits" | grep -vE '^\./src/' || [ $? -eq 1 ])"

if [ -n "$old_scope" ]; then
printf '%s\n' "$old_scope"
Expand Down Expand Up @@ -776,7 +776,7 @@ jobs:

# Exemption 6: inline pragma on the immediately preceding line.
if [[ "$lineno" -gt 1 ]]; then
prev_line=$(sed -n "$((lineno - 1))p" "$filepath" 2>/dev/null || true)
prev_line=$(sed -n "$((lineno - 1))p" "$filepath" 2>/dev/null)
if echo "$prev_line" | grep -qE "$PRAGMA_RE"; then
echo " [skip] $filepath:$lineno — pragma on preceding line"
continue
Expand All @@ -789,7 +789,7 @@ jobs:

done < <(grep -rnE --include='*.sh' --include='*.bash' \
--exclude-dir='.git' --exclude-dir='node_modules' --exclude-dir='target' \
"$pattern" . 2>/dev/null || true)
"$pattern" . 2>/dev/null || [ $? -eq 1 ])
done

if [ $found -eq 1 ]; then
Expand Down
26 changes: 20 additions & 6 deletions .github/workflows/security-gate-pr-target.yml
Original file line number Diff line number Diff line change
Expand Up @@ -92,14 +92,28 @@ jobs:

echo "Checking out PR branch from fork: $FORK_REPO/$PR_BRANCH"

# Add the fork as a remote temporarily
git remote add pr-fork "https://github.com/$FORK_REPO.git" 2>/dev/null || true
# Add the fork as a remote. A fresh checkout should never already
# have this remote; if this fails we want to know, not guess.
git remote add pr-fork "https://github.com/$FORK_REPO.git"

# Fetch the PR branch
git fetch pr-fork -- "$PR_BRANCH" 2>/dev/null || true
# Fetch the PR branch. Do NOT swallow failure here: the scans below
# only inspect what is actually on disk, so a silently-tolerated
# fetch failure would let them run against the base repo's own
# tree while still reporting a fork PR as scanned and clean.
if ! git fetch pr-fork -- "$PR_BRANCH"; then
echo "::error::could not fetch PR branch '$PR_BRANCH' from $FORK_REPO — refusing to run the malicious-content/file-type scans against unverified content."
echo "pr_checked_out=false" >> "$GITHUB_OUTPUT"
exit 1
fi

# Checkout the PR branch
git checkout -f "pr-fork/$PR_BRANCH" 2>/dev/null || git checkout -f "$PR_BRANCH" 2>/dev/null || true
# Checkout the fetched PR branch. No fallback to a same-named
# branch in the base repo: that would silently scan the wrong
# (trusted, non-fork) tree while still reporting success.
if ! git checkout -f "pr-fork/$PR_BRANCH"; then
echo "::error::could not check out fetched branch 'pr-fork/$PR_BRANCH' — refusing to run the malicious-content/file-type scans against unverified content."
echo "pr_checked_out=false" >> "$GITHUB_OUTPUT"
exit 1
fi

echo "pr_checked_out=true" >> "$GITHUB_OUTPUT"

Expand Down
Loading