Fix remaining decoder validation and CI review findings (supersedes #108)

.github/workflows/actions.lock

@@ -15,14 +15,13 @@ workflows:
     '.github/workflows/estate-rules.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/fork-governance-publish.yml':
-        - 'actions/checkout@v7.0.1'
         - 'actions/download-artifact@v8.0.2'
     '.github/workflows/fork-governance.yml':
         - 'actions/upload-artifact@v7.0.2'
     '.github/workflows/governance.yml': []
     '.github/workflows/hypatia-scan.yml': []
     '.github/workflows/instant-sync.yml':
-        - 'step-security/harden-runner@v2.22.3'
+        - 'step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43'
         - 'peter-evans/repository-dispatch@v4.0.1'
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
@@ -154,7 +153,7 @@ dependencies:
         commit: 'sha1-efb35369e0ad2afab669f228072c1b0d510eae64'
         owner_id: 2242
         repo_id: 204253808
-    'step-security/harden-runner@v2.22.3':
+    'step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43':
         ref: 'v2.22.3'
         commit: 'sha1-46b06cea07f9e64621fdf066ba77ac6915163d43'
         owner_id: 88700172

.github/workflows/fork-governance-publish.yml

@@ -3,9 +3,10 @@
 # Never check out the PR or execute anything downloaded from its run.
 #
 # Trust model: a fork PR controls the PR-side Fork governance workflow, so
-# its artifacts can lie. Lane pass/fail is therefore derived from GitHub's
-# own run metadata (job conclusions), the run must have actually called the
-# pinned reusable workflows named by the DEFAULT branch's
+# its artifacts can lie. Publication requires the PR head and base copies of
+# the scan workflow to match the default branch's trusted copy byte-for-byte.
+# Lane pass/fail is derived from GitHub's own run metadata (job conclusions),
+# and the run must have actually called the pinned reusable workflows named by the DEFAULT branch's
 # fork-governance.yml (referenced_workflows), and the artifact's lane
 # claims must agree or publication is refused. What remains
 # artifact-sourced is display shading only (K9/Hypatia verdict colors,
@@ -75,6 +76,23 @@ jobs:
           # workflow that fakes or swaps a lane does not satisfy this.
           gh api "repos/$GITHUB_REPOSITORY/contents/.github/workflows/fork-governance.yml" \
             --jq .content | base64 -d > "$RUNNER_TEMP/trusted-fork-governance.yml"
+          # A malicious PR can call the pinned reusables AND forge lookalike
+          # jobs/artifacts. Require the actual PR head and base workflow files
+          # to match the trusted default, not merely the list of reusables.
+          gh api "repos/$GITHUB_REPOSITORY/pulls/$pr" > "$RUNNER_TEMP/current-pr.json"
+          jq -e --arg sha "$sha" '.state == "open" and .head.sha == $sha' \
+            "$RUNNER_TEMP/current-pr.json" >/dev/null
+          head_repo=$(jq -r '.head.repo.full_name' "$RUNNER_TEMP/current-pr.json")
+          base_sha=$(jq -r '.base.sha' "$RUNNER_TEMP/current-pr.json")
+          gh api "repos/$head_repo/contents/.github/workflows/fork-governance.yml?ref=$sha" \
+            --jq .content | base64 -d > "$RUNNER_TEMP/head-fork-governance.yml"
+          gh api "repos/$GITHUB_REPOSITORY/contents/.github/workflows/fork-governance.yml?ref=$base_sha" \
+            --jq .content | base64 -d > "$RUNNER_TEMP/base-fork-governance.yml"
+          if ! cmp -s "$RUNNER_TEMP/trusted-fork-governance.yml" "$RUNNER_TEMP/head-fork-governance.yml" ||
+             ! cmp -s "$RUNNER_TEMP/trusted-fork-governance.yml" "$RUNNER_TEMP/base-fork-governance.yml"; then
+            echo "::error::PR scan workflow differs from the trusted default; refusing to publish."
+            exit 1
+          fi
           grep -oE 'uses: [^[:space:]#]+' "$RUNNER_TEMP/trusted-fork-governance.yml" \
             | awk '{print $2}' | grep '/\.github/workflows/' | sort -u \
             > "$RUNNER_TEMP/expected-reusables.txt"
@@ -116,7 +134,7 @@ jobs:
           name: fork-governance-result
           path: evidence
           github-token: ${{ github.token }}
-          run-id: ${{ steps.source.outputs.run }}
+          run-id: ${{ github.event.workflow_run.id }}
 
       - name: Validate lane result data
         if: steps.source.outputs.pr != ''
@@ -151,7 +169,7 @@ jobs:
           name: k9-grid
           path: k9-grid
           github-token: ${{ github.token }}
-          run-id: ${{ steps.source.outputs.run }}
+          run-id: ${{ github.event.workflow_run.id }}
 
       - name: Download the Hypatia grid from the verified run
         if: steps.source.outputs.pr != ''
@@ -161,18 +179,16 @@ jobs:
           name: verdict-grid
           path: verdict-grid
           github-token: ${{ github.token }}
-          run-id: ${{ steps.source.outputs.run }}
+          run-id: ${{ github.event.workflow_run.id }}
 
-      - name: Checkout the pinned trusted renderer
+      - name: Fetch the pinned trusted renderer
         if: steps.source.outputs.pr != ''
-        uses: actions/checkout@v7.0.1
-        with:
-          repository: metadatastician/standards
-          ref: 34cf03f988b8ca95b91b45d9b3351f7d3babfb65
-          path: canon
-          sparse-checkout: scripts/fork-governance-render.sh
-          sparse-checkout-cone-mode: false
-          persist-credentials: false
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          set -euo pipefail
+          gh api 'repos/metadatastician/standards/contents/scripts/fork-governance-render.sh?ref=34cf03f988b8ca95b91b45d9b3351f7d3babfb65' \
+            --jq .content | base64 -d > "$RUNNER_TEMP/trusted-renderer.sh"
 
       - name: Render and publish the verified run's summary
         if: steps.source.outputs.pr != ''
@@ -196,7 +212,7 @@ jobs:
                 --sha "$sha" --run "$(jq -r '.run' evidence/result.json)" --repo "$GITHUB_REPOSITORY")
           [ ! -s k9-grid/report.md ] || args+=(--k9-report k9-grid/report.md)
           [ ! -s verdict-grid/report.md ] || args+=(--hypatia-report verdict-grid/report.md)
-          bash canon/scripts/fork-governance-render.sh "${args[@]}" >/dev/null
+          bash "$RUNNER_TEMP/trusted-renderer.sh" "${args[@]}" >/dev/null
           cat "$RUNNER_TEMP/fork-governance/body.md" >> "$GITHUB_STEP_SUMMARY"
           comment_id=$(gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/issues/$PR_NUMBER/comments" \
             | jq -r '[.[][] | select(.user.login == "github-actions[bot]"

.github/workflows/instant-sync.yml

@@ -23,7 +23,7 @@ jobs:
       # risking the dispatch; tighten to block+allowlist once a main run
       # shows the observed set.
       - name: Harden runner (egress audit)
-        uses: step-security/harden-runner@v2.22.3
+        uses: step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43 # v2.22.3
         with:
           egress-policy: audit
       - name: Trigger Propagation

.github/workflows/main-estate-audit.yml

@@ -29,59 +29,59 @@ jobs:
         with:
           fetch-depth: 0
           persist-credentials: false
-      
+
       - name: Required Files Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/required-files-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Code Hygiene Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/code-hygiene-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Manifest Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/manifest-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Idris2 ABI Purity Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/idris2-abi-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Zig UnifiedApiAdapter API Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/zig-unified-api-adapter-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Contractile Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/contractile-validation-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Recipes Set Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/recipes-set-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Affirmation Document Gate
         if: ${{ !cancelled() }}
         run: bash .github/affirmation-trusted/check.sh
-        
+
       - name: Academic Referencing Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/referencing-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Semantic Audit Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/semantic-audit-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: SPDX License Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/spdx-license-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Proof Runner Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/proof-runner-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: PRAT Testing Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/prat-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       # No "Panic Attack & Pons" step here (removed 2026-10-28): the
       # cicd-suite custom-tools-check composite prints "validation passed"
       # when neither tool is on PATH — which is always — so it certified
@@ -94,47 +94,47 @@ jobs:
       - name: WWW & Well-Known Compliance Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/www-compliance-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: BoJ Cartridge Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/boj-cartridge-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Formatting Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/formatting-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Accreditations & Badges Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/badges-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Metrics Extraction Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/metrics-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Linguist & Banned Languages Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/linguist-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Test & Benchmarks Dashboard Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/tests-benches-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Hosting & Site Status Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/hosting-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Git-Sea Analytics Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/gitsea-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Trust & Humans Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/trust-humans-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Are We UnAPI Gate (Secret Scanning)
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/secrets-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Reasonably Good Token Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/vaulted-tokens-check@bf7dd95cf49733019343ff485c2f45c6b261839c

.github/workflows/proofs.yml

@@ -27,6 +27,7 @@ on:
     paths:
       - 'verification/proofs/lean4/**'
       - 'verification/proofs/agda/**'
+      - 'tests/lib/strip-proof-comments.awk'
       - '.github/workflows/proofs.yml'
   pull_request:
   workflow_dispatch:
@@ -281,6 +282,14 @@ jobs:
               echo "::error::axiom-audit failed to run for $m (exit $audit_status)"
               exit 1
             fi
+            # jq -s silently skips empty files. Require exactly one report per
+            # module even when the tool exits 1 (a reported violation).
+            if ! jq -e -s 'length == 1 and (.[0] | type == "object" and (.audited | type == "number"))' \
+                 "$work/report-$m.json" >/dev/null 2>&1; then
+              cat "$work/report-$m.json" || true
+              echo "::error::axiom-audit produced no valid JSON report for $m (exit $audit_status)"
+              exit 1
+            fi
           done
           report="$work/report.json"
           # Lean 4.16 stores compiler IR (`_cstage*`, equation/match auxiliaries)

.github/workflows/quality.yml

@@ -75,7 +75,12 @@ jobs:
       - name: Gate falsifiability canaries (R10)
         run: bash scripts/test-gate-falsifiability.sh
       - name: Workflow and gate regression tests
-        run: bash tests/workflows/review_regressions_test.sh
+        run: |
+          bash tests/workflows/review_regressions_test.sh
+          bash tests/workflows/audit_report_test.sh
+          bash tests/workflows/publisher_trust_test.sh
+          bash tests/workflows/setup_test.sh
+          bash tests/workflows/validate_workflows_test.sh
   docs-present:
     runs-on: ubuntu-latest
     timeout-minutes: 15

.github/workflows/trope-check.yml

@@ -14,9 +14,11 @@ on:
     paths:
       - 'schemas/**'
       - 'src/idris2/**'
+      - 'src/rust/**'
       - 'src/interface/**'
       - 'abi.ipkg'
       - 'tests/conformance/**'
+      - 'tests/lib/strip-proof-comments.awk'
       - 'verification/proofs/idris2/**'
       - 'spec/**'
       - '.github/workflows/trope-check.yml'

build/setup.sh

@@ -134,11 +134,16 @@ detect_platform() {
             elif command -v choco >/dev/null 2>&1; then PKG_MGR="choco"
             fi
             ;;
-        FreeBSD*|DragonFly*)
+        FreeBSD*)
             OS="freebsd"
             DISTRO="freebsd"
             PKG_MGR="pkg"
             ;;
+        DragonFly*)
+            OS="dragonfly"
+            DISTRO="dragonfly"
+            PKG_MGR="pkg"
+            ;;
         OpenBSD*)
             OS="openbsd"
             DISTRO="openbsd"
@@ -257,40 +262,30 @@ install_just_pinned() {
         }
     fi
 
-    if [ -w /usr/local/bin ]; then
-        _just_dest="/usr/local/bin"
-        _just_elevated="false"
-    elif [ "$(id -u 2>/dev/null || echo 1)" = "0" ] \
-        || command -v sudo >/dev/null 2>&1 || command -v doas >/dev/null 2>&1; then
-        _just_dest="/usr/local/bin"
-        _just_elevated="true"
+    _just_dest="/usr/local/bin"
+    if [ -d "$_just_dest" ] && [ -w "$_just_dest" ] &&
+        install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary"; then
+        : # Installed without elevation.
+    elif [ -d "$_just_dest" ] && { [ "$(id -u 2>/dev/null || echo 1)" = "0" ] ||
+        command -v sudo >/dev/null 2>&1 || command -v doas >/dev/null 2>&1; } &&
+        as_root install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary"; then
+        : # Installed with elevation.
     elif [ -n "${HOME:-}" ]; then
         _just_dest="$HOME/.local/bin"
-        _just_elevated="false"
-        mkdir -p "$_just_dest"
+        if ! mkdir -p "$_just_dest" || ! install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary"; then
+            fail "Could not install just into $_just_dest"
+            rm -rf "$_just_tmp"
+            return 1
+        fi
         warn "Installing just into $_just_dest; ensure it is on PATH for future shells"
     else
         fail "No writable install directory for just"
         rm -rf "$_just_tmp"
         return 1
     fi
-
-    if [ "$_just_elevated" = "true" ] && [ ! -w "$_just_dest" ]; then
-        as_root install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary" || {
-            fail "Could not install just into $_just_dest"
-            rm -rf "$_just_tmp"
-            return 1
-        }
-    else
-        install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary" || {
-            fail "Could not install just into $_just_dest"
-            rm -rf "$_just_tmp"
-            return 1
-        }
-    fi
-    PATH="$_just_dest:$PATH"
-    export PATH
     rm -rf "$_just_tmp"
+    PATH="$_just_dest${PATH:+:$PATH}"
+    export PATH
 }
 
 # Ensure just is on PATH, reusing an existing installation when available.
@@ -320,8 +315,9 @@ install_just() {
         scoop)      scoop install just ;;
         winget)     winget install --exact --id Casey.Just ;;
         choco)      choco install just -y ;;
-        rpm-ostree) as_root rpm-ostree install just ;;
-        guix)       guix install just ;;
+        # rpm-ostree layers packages for the next boot; Guix's profile may
+        # not be on this process's PATH. The pinned binary is usable now.
+        rpm-ostree|guix) install_just_pinned ;;
         pkg)        as_root pkg install -y just ;;
         pkg_add)    as_root pkg_add just ;;
         pkgin)      as_root pkgin -y install just ;;