Review fixes: kernel soundness, untrusted-input hardening, perf, CI

.github/workflows/bench-pr.yml

@@ -1,4 +1,13 @@
 # Creates a PR benchmark comment with a comparison to main
+#
+# SECURITY: this workflow builds and EXECUTES PR-branch code (which may come
+# from a fork). The job topology is load-bearing:
+#   - `benchmark` runs the untrusted code and must never hold credentials —
+#     no secrets, no token minting. Its only output is an uploaded artifact.
+#   - `comment` is the only privileged job (mints the GitHub App token). It
+#     runs on a fresh runner and executes no checked-out code, so untrusted
+#     build scripts can never observe the token.
+# Do not merge these jobs or move the token step into `benchmark`.
 name: Benchmark pull requests
 
 on:
@@ -30,9 +39,13 @@ jobs:
       - uses: actions/checkout@v6
       - name: Parse PR comment body
         id: bench-params
+        env:
+          # Passed via env (not inline interpolation) so comment text can
+          # never be evaluated as shell syntax.
+          COMMENT_BODY: ${{ github.event.comment.body }}
         run: |
           # Parse `issue_comment` body
-          printf '${{ github.event.comment.body }}' > comment.txt
+          printf '%s' "$COMMENT_BODY" > comment.txt
           BENCH_COMMAND=$(head -n 1 comment.txt | tr -d '\r')
           echo "$BENCH_COMMAND"
 
@@ -60,23 +73,25 @@ jobs:
         bench: ${{ fromJSON(needs.setup.outputs.benches) }}
     steps:
       - name: Set env vars
+        env:
+          ENV_VARS: ${{ needs.setup.outputs.env-vars }}
         run: |
           # Overrides default env vars with those specified in the `issue_comment` input if identically named
-          for var in ${{ needs.setup.outputs.env-vars }}
+          for var in $ENV_VARS
           do
             echo "$var" | tee -a $GITHUB_ENV
           done
       - uses: actions/checkout@v6
         # Get base branch of the PR
-      - uses: xt0rted/pull-request-comment-branch@v3
+      - uses: xt0rted/pull-request-comment-branch@e8b8daa837e8ea7331c0003c9c316a64c6d8b0b1 # v3
         id: comment-branch
       - name: Checkout base branch
         uses: actions/checkout@v6
         with:
           ref: ${{ steps.comment-branch.outputs.base_sha }}
           path : ${{ github.workspace }}/base
       - name: Run `lake build` on base branch
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           lake-package-directory: ${{ github.workspace }}/base
           test: false
@@ -94,7 +109,7 @@ jobs:
           path: ${{ github.workspace }}/pr
           ref: ${{ steps.comment-branch.outputs.head_sha }}
       - name: Run `lake build` on PR branch
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           lake-package-directory: ${{ github.workspace }}/pr
           test: false
@@ -109,43 +124,74 @@ jobs:
         run: |
           BENCH_REPORT=1 lake exe ${{ matrix.bench }}
         working-directory: ${{ github.workspace }}/pr
-      - name: Get env for PR body
-        if: always()
-        run: |
-          SHORT_SHA_PR=$(git rev-parse --short HEAD)
-          REPO_URL=${{ github.server_url }}/${{ github.repository }}
-          echo "COMMIT_LINK=[\`$SHORT_SHA_PR\`]($REPO_URL/commit/${{ steps.comment-branch.outputs.head_sha }})" | tee -a $GITHUB_ENV
-          echo "WORKFLOW_LINK=[Workflow logs]($REPO_URL/actions/runs/${{ github.run_id }})" | tee -a $GITHUB_ENV
-        working-directory: ${{ github.workspace }}/pr
-      - name: Generate token to write PR comment
-        uses: actions/create-github-app-token@v3
-        if: always()
-        id: app-token
-        with:
-          app-id: ${{ secrets.TOKEN_APP_ID }}
-          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
       - name: Build benchmark comment body
         if: success()
         run: |
           {
-            echo '## Benchmark for `${{ matrix.bench }}` at ${{ env.COMMIT_LINK }}';
+            echo '## Benchmark for `${{ matrix.bench }}`';
             echo "";
             for file in .lake/benches/*/report.md; do
               [ -f "$file" ] && cat "$file" && echo ""
             done
-            echo "${{ env.WORKFLOW_LINK }}";
           } > ${{ github.workspace }}/comment-body.md
         working-directory: ${{ github.workspace }}/pr
-      - name: Comment on successful run
+      - name: Upload benchmark comment body
         if: success()
-        uses: peter-evans/create-or-update-comment@v5
+        uses: actions/upload-artifact@v4
+        with:
+          name: comment-body-${{ matrix.bench }}
+          path: ${{ github.workspace }}/comment-body.md
+
+  comment:
+    # Privileged job: mints the App token. Runs no checked-out code (see the
+    # header comment). `always()` so failures still produce a PR comment.
+    needs: [ setup, benchmark ]
+    if: always() && needs.setup.result == 'success'
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        bench: ${{ fromJSON(needs.setup.outputs.benches) }}
+    steps:
+      - uses: xt0rted/pull-request-comment-branch@e8b8daa837e8ea7331c0003c9c316a64c6d8b0b1 # v3
+        id: comment-branch
+      - name: Get env for PR body
+        run: |
+          REPO_URL=${{ github.server_url }}/${{ github.repository }}
+          HEAD_SHA=${{ steps.comment-branch.outputs.head_sha }}
+          SHORT_SHA_PR=$(printf '%s' "$HEAD_SHA" | cut -c1-7)
+          echo "COMMIT_LINK=[\`$SHORT_SHA_PR\`]($REPO_URL/commit/$HEAD_SHA)" | tee -a $GITHUB_ENV
+          echo "WORKFLOW_LINK=[Workflow logs]($REPO_URL/actions/runs/${{ github.run_id }})" | tee -a $GITHUB_ENV
+      - name: Download benchmark comment body
+        id: download
+        continue-on-error: true
+        uses: actions/download-artifact@v4
+        with:
+          name: comment-body-${{ matrix.bench }}
+      - name: Assemble comment body
+        if: steps.download.outcome == 'success'
+        run: |
+          {
+            echo '## Benchmark for `${{ matrix.bench }}` at ${{ env.COMMIT_LINK }}';
+            echo "";
+            cat comment-body.md;
+            echo "${{ env.WORKFLOW_LINK }}";
+          } > final-comment-body.md
+      - name: Generate token to write PR comment
+        uses: actions/create-github-app-token@v3
+        id: app-token
+        with:
+          app-id: ${{ secrets.TOKEN_APP_ID }}
+          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
+      - name: Comment on successful run
+        if: steps.download.outcome == 'success'
+        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v5
         with:
           token: ${{ steps.app-token.outputs.token }}
           issue-number: ${{ github.event.issue.number }}
-          body-path: 'comment-body.md'
+          body-path: 'final-comment-body.md'
       - name: Comment on failing run
-        if: failure()
-        uses: peter-evans/create-or-update-comment@v5
+        if: steps.download.outcome != 'success'
+        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v5
         with:
           token: ${{ steps.app-token.outputs.token }}
           issue-number: ${{ github.event.issue.number }}

.github/workflows/ci.yml

@@ -18,8 +18,8 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v6
-      - uses: actions-rust-lang/setup-rust-toolchain@v1
-      - uses: leanprover/lean-action@v1
+      - uses: actions-rust-lang/setup-rust-toolchain@46268bd060767258de96ed93c1251119784f2ab6 # v1
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           build-args: "--wfail -v"
       - name: Test Ix CLI
@@ -33,15 +33,17 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v6
-      - uses: actions-rust-lang/setup-rust-toolchain@v1
-      - uses: taiki-e/install-action@nextest
+      - uses: actions-rust-lang/setup-rust-toolchain@46268bd060767258de96ed93c1251119784f2ab6 # v1
+      - uses: taiki-e/install-action@0631aa6515c7d545823c67cfae7ef4fc7f490154 # v2
+        with:
+          tool: nextest
       # Install Lean for rust-bindgen step
-      - uses: leanprover/lean-action@v1
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           auto-config: false
           use-github-cache: false
       - name: Check Rustfmt code style
-        uses: actions-rust-lang/rustfmt@v1
+        uses: actions-rust-lang/rustfmt@4066006ec54a31931b9b1fddfd38f2fdf2d27143 # v1
       - name: Check clippy warnings
         run: cargo clippy --workspace --all-targets --all-features -- -D warnings
       - name: Check *everything* compiles
@@ -52,6 +54,6 @@ jobs:
         run: |
           echo "RUST_VERSION=$(awk -F '"' '/^channel/ {print $2}' rust-toolchain.toml)" | tee -a $GITHUB_ENV
       - name: Cargo-deny
-        uses: EmbarkStudios/cargo-deny-action@v2
+        uses: EmbarkStudios/cargo-deny-action@8f84122a46a358a27cb0625d85ad60ab436a1b87 # v2
         with:
           rust-version: ${{ env.RUST_VERSION }}

.github/workflows/compile.yml

@@ -18,7 +18,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v6
-      - uses: leanprover/lean-action@v1
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           auto-config: false
           build: true
@@ -56,7 +56,7 @@ jobs:
       - if: matrix.bench == 'FC'
         run: echo "COMPILE_DIR=${{env.COMPILE_DIR}}FC" | tee -a $GITHUB_ENV
       # Download elan and fetch mathlib cache
-      - uses: leanprover/lean-action@v1
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           lake-package-directory: ${{ env.COMPILE_DIR }}
           auto-config: false
@@ -102,7 +102,9 @@ jobs:
           [ "$sample" -gt 64 ] && sample=64
           echo "sample=$sample" | tee -a "$GITHUB_OUTPUT"
       # Deploy benchmark results to https://bencher.dev/console/projects/ix/plots
-      - uses: bencherdev/bencher@main
+      # Pinned by SHA (v0.6.6): this step's environment later holds
+      # BENCHER_API_TOKEN, so it must not track a moving branch.
+      - uses: bencherdev/bencher@50fb1e138651a46d2fb704fab1adab38c181552e # v0.6.6
       - name: Track benchmarks
         run: |
           # On a lean-toolchain bump (sample=0), omit file-size and constants

.github/workflows/ignored.yml

@@ -17,14 +17,14 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
-      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      - uses: actions-rust-lang/setup-rust-toolchain@46268bd060767258de96ed93c1251119784f2ab6 # v1
       # Only restore the cache, since `ci.yml` will save the test binary to the cache first
       - uses: actions/cache/restore@v5
         with:
           path: .lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-      - uses: leanprover/lean-action@v1
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           auto-config: false
           # `test-args` is currently broken, so we run `lake test` separately
@@ -39,14 +39,14 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v6
-      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      - uses: actions-rust-lang/setup-rust-toolchain@46268bd060767258de96ed93c1251119784f2ab6 # v1
       # Only restore the cache, since `ci.yml` will save the test binary to the cache first
       - uses: actions/cache/restore@v5
         with:
           path: .lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-      - uses: leanprover/lean-action@v1
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
         with:
           auto-config: false
           build: true

.github/workflows/nix.yml

@@ -20,7 +20,7 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v6
-      - uses: cachix/install-nix-action@v31
+      - uses: cachix/install-nix-action@b97f05dcb019ddea06450a50ef6203d2fdc19fee # v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
@@ -36,7 +36,7 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v6
-      - uses: cachix/install-nix-action@v31
+      - uses: cachix/install-nix-action@b97f05dcb019ddea06450a50ef6203d2fdc19fee # v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable
           github_access_token: ${{ secrets.GITHUB_TOKEN }}

Apps/ZKVoting/Verifier.lean

@@ -1,5 +1,10 @@
 import Ix.Claim
 
+/-- NOT IMPLEMENTED. A verifier stub that exits 0 unconditionally is worse
+    than none at all — anything scripted against it silently treats every
+    proof as valid — so it fails loudly until real verification (parse
+    commitments, deserialize the proof, check every vote is in the claim,
+    run the STARK verifier) lands. -/
 def main (_args : List String) : IO UInt32 := do
 --  TODO
 --  let mut votes := #[]
@@ -14,4 +19,5 @@ def main (_args : List String) : IO UInt32 := do
 --    -- TODO: print the resulting vote counts in the claim
 --    -- TODO: assert that every vote in `votes` is in the proof claim
 --    -- TODO: verify proof
-    return 0
+    IO.eprintln "error: ZKVoting verifier is not implemented; refusing to report success"
+    return 1

DebugIxVM.lean

@@ -0,0 +1,36 @@
+import Ix.IxVM
+import Tests.Ix.IxVM
+import Tests.Aiur.Common
+
+def buildIxVMEnv : IO AiurTestEnv := do
+  match AiurTestEnv.build IxVM.ixVM with
+  | .error e => throw <| IO.userError s!"Aiur setup failed: {e}"
+  | .ok env => pure env
+
+def mkCase (caseName : String) (leanEnv : Lean.Environment) : IO AiurTestCase := do
+  match caseName with
+  | "kernel_unit_tests" => pure <| AiurTestCase.exec `kernel_unit_tests
+  | "serde" => serdeNatAddComm leanEnv
+  | "Nat.add_comm" => kernelCheck ``Nat.add_comm leanEnv
+  | "Nat.sub_le_of_le_add" => kernelCheck ``Nat.sub_le_of_le_add leanEnv
+  | "String.Internal.append" => kernelCheck ``String.Internal.append leanEnv
+  | "extractMainModule" =>
+      kernelCheck (`_private.Init.Prelude |>.mkNum 0 |>.mkStr "Lean.extractMainModule._unsafe_rec") leanEnv
+  | other => throw <| IO.userError s!"unknown case: {other}"
+
+def runCase (env : AiurTestEnv) (tc : AiurTestCase) : IO UInt32 := do
+  IO.println s!"running {tc.label}"
+  let some funIdx := env.compiled.getFuncIdx tc.functionName
+    | throw <| IO.userError s!"missing function: {tc.functionName}"
+  let (execOutput, execIOBuffer, _queryCounts) :=
+    env.compiled.bytecode.execute funIdx tc.input tc.inputIOBuffer
+  IO.println s!"output ok: {execOutput == tc.expectedOutput}"
+  IO.println s!"io ok: {execIOBuffer == tc.expectedIOBuffer}"
+  pure <| if execOutput == tc.expectedOutput && execIOBuffer == tc.expectedIOBuffer then 0 else 1
+
+def main (args : List String) : IO UInt32 := do
+  let caseName := args.headD "kernel_unit_tests"
+  let leanEnv ← get_env!
+  let aiurEnv ← buildIxVMEnv
+  let tc ← mkCase caseName leanEnv
+  runCase aiurEnv tc

Ix/Aiur/Compiler/Check.lean

@@ -584,12 +584,14 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
   | .unit => pure (.unit .unit false)
   | .var x => do
     let ctx ← read
-    match (ctx.varTypes[x]?, x) with
-    | (some t, _) => pure (.var t false x)
-    | (none, Local.str localName) =>
-      let (typ, _) ← refLookup (Global.init localName)
-      pure (.var typ false x)
-    | (none, _) => throw $ .unboundLocal x
+    match ctx.varTypes[x]? with
+    | some t => pure (.var t false x)
+    -- No global-function fallback here: neither `SourceEval` nor `Lower`
+    -- implements one, so a program that typechecked via the fallback
+    -- would evaluate/compile to something else entirely (silent
+    -- miscompile). Unbound locals are errors; reference globals with
+    -- `.ref`.
+    | none => throw $ .unboundLocal x
   | .ref x => do
     let (typ, tArgs) ← refLookup x
     pure (.ref typ false x tArgs)