Formalize Ironwood zero knowledge in Lean

.github/workflows/book.yml

@@ -23,6 +23,7 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+      pull-requests: read # paths-filter lists changed files through the pull request API
     outputs:
       book: ${{ steps.filter.outputs.book }}
     steps:

.github/workflows/fixtures.yml

@@ -1,43 +1,17 @@
 name: Fixtures
 
-# Enforces that every checked-in verifier-fingerprint fixture family -- the honest
-# `Zcash/Snark/Fixtures/{SingleAction,MultiAction}/Honest/Fixture.lean` captures and the
-# random match-only `{SingleAction,MultiAction}/Random/` families with
-# their `proof-bytes.hex` siblings -- is byte-for-byte what the pinned public sources
-# regenerate, by running `scripts/regenerate-fingerprint-fixtures.sh`. The fixtures stay
-# checked in -- they are the formal artifact the Lean development proves about, imported
-# by the `FixtureCheck` target and required for a self-contained `lake build` -- and this
-# workflow closes the "trust that a human ran the capture correctly" gap by regenerating
-# them in CI and diffing. See zcash/ironwood#54.
+# Regenerate the existing honest/random one-Action and two-Action verifier
+# fixture families and their proof-byte siblings from Zakura's released exporters.
+# The four exact capture tests and release/package checksums are selected from
+# Zcash/Snark/ZeroKnowledge/Zakura/release.json by the regeneration tooling.
+# The separate prover captures use Common's pinned Rust-hosted exporter under
+# prover-fingerprint / unstable-prover-fingerprint. Lean CI independently
+# replays their complete selected executions; this is not universal Rust/Lean parity.
 #
-# Determinism: the captures use fixed ChaCha20 seeds and the exporter orders points by
-# a coordinate-key `BTreeSet` (not HashMap iteration order), and field/curve arithmetic
-# is platform-independent, so regeneration is bit-reproducible -- a diff means the
-# fixtures genuinely drifted from the pinned upstream, not run-to-run noise.
-#
-# Pins: single-sourced in `scripts/regenerate-fingerprint-fixtures.sh`, and there is exactly
-# one -- the `zcash/orchard` 0.15.5 release tag, which the script asserts is the tag rather
-# than a commit merely descended from it. No forks and no unreleased branches: the capture
-# tooling is upstream and released, the match-only exporter and `numInstanceColumns` shape
-# emission in `halo2_proofs` 0.3.5 (zcash/halo2#924) and the fabricate->replay random-capture
-# drivers in orchard 0.15.5 (zcash/orchard#541). Orchard's own published `Cargo.lock`
-# resolves `halo2_proofs` 0.3.5 from crates.io by checksum, which the script also asserts,
-# so no `[patch.crates-io]` override is involved and every cargo invocation runs `--locked`
-# against published crates. All four families -- honest pair included -- regenerate from
-# released sources alone.
-
-# Always triggers, so the `Fixtures CI` gate always reports (a workflow skipped by
-# `on.paths` would leave a required check pending). The heavy regeneration is instead
-# gated on a path filter computed inside the run, so it only builds Rust when the
-# fixtures or the pins (the regeneration script, or this workflow) actually change.
-# Two cheap guards run on every event regardless of the filter: the committed
-# capture-artifact set must equal the script's pinned regeneration list, and every
-# capture must carry the exporter header (`--check-set` below).
-#
-# The weekly schedule and manual dispatch bypass the filter and regenerate
-# unconditionally: pin rot — a moved or deleted upstream tag, a toolchain drift — then
-# surfaces on a clock, attributed to the pin, instead of failing the next unlucky PR
-# that happens to touch a filtered path.
+# This workflow always reports its required status. Local inventory/provenance
+# guards run on every event; actual regeneration runs when its inputs change or
+# on the schedule/manual triggers. The source and generated bytes are checked,
+# so existing captures must be refreshed before they can match a changed target.
 on:
   push:
     branches: [main]
@@ -58,6 +32,7 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+      pull-requests: read # paths-filter lists changed files through the pull request API
     outputs:
       # Scheduled and manually dispatched runs bypass the filter (the filter step is
       # skipped, and this expression then forces regeneration).
@@ -103,7 +78,16 @@ jobs:
               - 'Zcash/Snark/Fixtures/SingleAction/Random/proof-bytes.hex'
               - 'Zcash/Snark/Fixtures/MultiAction/Random/Fixture.lean'
               - 'Zcash/Snark/Fixtures/MultiAction/Random/proof-bytes.hex'
+              - 'Zcash/Snark/Fixtures/MANIFEST.tsv'
+              - 'Zcash/Snark/Fixtures/Prover/SingleAction.lean'
+              - 'Zcash/Snark/Fixtures/Prover/MultiAction.lean'
+              - 'Zcash/Snark/Fixtures/Prover/producer.json'
+              - 'Zcash/Snark/ZeroKnowledge/Zakura/release.json'
               - 'scripts/regenerate-fingerprint-fixtures.sh'
+              - 'scripts/regenerate-prover-fixtures.sh'
+              - 'scripts/regenerate_fingerprint_fixtures.py'
+              - 'scripts/prepare_zakura_release.py'
+              - 'scripts/check_zakura_release.py'
               - '.github/workflows/fixtures.yml'
 
   verify:
@@ -118,14 +102,17 @@ jobs:
         uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
         with:
           persist-credentials: false
-      # The script clones the pinned Orchard release, asserts the commit is the release
-      # tag and that its published lockfile resolves halo2_proofs 0.3.5 from crates.io by
-      # checksum, installs Orchard's pinned toolchain (`rustup show` against its
-      # `rust-toolchain.toml`), regenerates all four families plus the proof-byte
-      # siblings, and diffs every committed artifact byte-for-byte, exiting non-zero on
-      # any mismatch. Uncached: the job only runs when the path filter above fires.
-      - name: Regenerate every fixture family from the pinned Orchard release
+      # Authenticate the release sources and crates, use Common's toolchain/lockfile,
+      # execute its four existing capture drivers, and compare all six artifacts.
+      # CI never uses --update; any mismatch fails the check.
+      - name: Regenerate existing fixtures from the pinned Zakura release
+        env:
+          REGEN_WORK_DIR: ${{ runner.temp }}/zakura-fixtures
         run: ./scripts/regenerate-fingerprint-fixtures.sh
+      - name: Regenerate complete prover executions from the pinned Common exporter
+        env:
+          REGEN_WORK_DIR: ${{ runner.temp }}/zakura-prover-fixtures
+        run: ./scripts/regenerate-prover-fixtures.sh
 
   fixtures-ci:
     # The single stable check to mark as a required status check. It always runs, so it

.github/workflows/lean.yml

@@ -24,6 +24,7 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+      pull-requests: read # paths-filter lists changed files through the pull request API
     outputs:
       lean: ${{ steps.filter.outputs.lean }}
     steps:
@@ -54,6 +55,10 @@ jobs:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
         with:
           persist-credentials: false
+      - name: Check release provenance and fixture preparation failures
+        run: python3 -m unittest discover -s scripts -p 'test_zakura_*.py'
+      - name: Verify Zakura release sources and stored public artifacts
+        run: python3 scripts/check_zakura_release.py --cache-dir "${{ runner.temp }}/zakura-release-sources" --fetch
       # Content-pins the checked-in circuit VK fixtures (the `.json` CS/layout dumps
       # consumed by `CircuitCheck`). The Lean build does not recompute a hash — there
       # is no fast SHA-256 in the toolchain — so this OS `sha256sum -c` is the
@@ -247,6 +252,18 @@ jobs:
         with:
           path: .lake/packages
           key: lake-deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+      # Save completed compilation before the separate, potentially long execution check.
+      - name: Compare complete Rust and Lean prover executions
+        # The captures are independent. Wait for both, and propagate either failure.
+        run: |
+          lake env lean --run Zcash/Snark/Fixtures/Prover/Main.lean single &
+          single_replay_pid=$!
+          lake env lean --run Zcash/Snark/Fixtures/Prover/Main.lean multi &
+          multi_replay_pid=$!
+          prover_replay_status=0
+          wait "$single_replay_pid" || prover_replay_status=1
+          wait "$multi_replay_pid" || prover_replay_status=1
+          exit "$prover_replay_status"
 
   lean-ci:
     # The single stable check to mark as a required status check. It always

.github/workflows/zizmor.yml

@@ -21,6 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+      pull-requests: read # paths-filter lists changed files through the pull request API
     outputs:
       workflows: ${{ steps.filter.outputs.workflows }}
     steps:

.gitignore

@@ -4,3 +4,5 @@
 /.lake
 /.elan
 /scripts/generated/
+/Zcash/Snark/ZeroKnowledge/review/
+/scripts/__pycache__/

Zcash/Arithmetic/Domain.lean

@@ -6,9 +6,9 @@ import Zcash.Arithmetic.Field
 # Evaluation-domain scalars (pasta `Fp` constants and facts)
 
 halo2's domain data as pure functions: binary exponentiation (`powFast`), the size-`2^k`
-domain root of unity `omegaOf` (CompElliptic's certified Pasta `ROOT_OF_UNITY` squared
-down, `EvaluationDomain::new`), `Fp::DELTA`, and the domain facts (primitive-root, power
-injectivity, size nonvanishing) derived from the certificate's order fact.
+domain root of unity `omegaOf` (Pasta's `ROOT_OF_UNITY` squared down,
+`EvaluationDomain::new`), `Fp::DELTA`, and the domain facts (primitive-root, power
+injectivity, size nonvanishing). The root's order is checked by Lean's kernel.
 Moved out of `Zcash/Bridge` per the Clean-boundary architecture
 (`book/src/formal-verification/clean-boundary.md`): these are verifier-native arithmetic
 facts, not bridge plumbing.
@@ -65,25 +65,30 @@ def rootOfUnityFp : Fp :=
 theorem rootOfUnityFp_eq_certified :
     rootOfUnityFp = CompElliptic.Fields.Pasta.pallasBase.rootOfUnity := rfl
 
+set_option maxRecDepth 8192 in
+/-- The deployed root literal has exact order `2^32`, by kernel-checked field arithmetic. -/
+theorem rootOfUnityFp_primitiveRoot : IsPrimitiveRoot rootOfUnityFp (2 ^ 32) := by
+  rw [IsPrimitiveRoot.iff_orderOf]
+  haveI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
+  apply orderOf_eq_prime_pow (p := 2) (n := 31)
+  · rw [← powFast_eq_pow]
+    decide +kernel
+  · rw [← powFast_eq_pow]
+    decide +kernel
+
 /-- The size-`2^k` domain's root of unity: the Pasta root (`ROOT_OF_UNITY = 5^((p−1)/2^32)`,
 pasta `Fp::GENERATOR = 5`) squared down `32 − k` times, exactly as `EvaluationDomain::new`
-does — so `omega = 5^((p−1)/2^k)`. Its order is a theorem of CompElliptic's certificate via
-`rootOfUnityFp_eq_certified`; agreement with the deployed key's omega is pinned by `VkMatch`
-against the captured VK. -/
+does — so `omega = 5^((p−1)/2^k)`. Its order follows from the kernel-checked root theorem;
+agreement with the deployed key's omega is pinned by `VkMatch` against the captured VK. -/
 def omegaOf (k : ℕ) : Fp :=
   powFast rootOfUnityFp (2 ^ (32 - k))
 
 /-- `omegaOf k` is a primitive size-`2^k` domain root for every supported exponent. -/
 theorem omegaOf_isPrimitiveRoot (k : ℕ) (hk : k ≤ 32) :
     IsPrimitiveRoot (omegaOf k) (2 ^ k) := by
-  have hroot :
-      IsPrimitiveRoot
-        CompElliptic.Fields.Pasta.pallasBase.rootOfUnity (2 ^ 32) :=
-    IsPrimitiveRoot.iff_orderOf.mpr
-      CompElliptic.Fields.Pasta.pallasBase.valid.rootOfUnity_order
   unfold omegaOf
-  rw [rootOfUnityFp_eq_certified, powFast_eq_pow]
-  apply IsPrimitiveRoot.pow (by positivity) hroot
+  rw [powFast_eq_pow]
+  apply IsPrimitiveRoot.pow (by positivity) rootOfUnityFp_primitiveRoot
   rw [← pow_add, Nat.sub_add_cancel hk]
 
 /-- Every point `omegaOf k ^ row` lies in the size-`2^k` evaluation domain. -/

Zcash/CensusCheck.lean

@@ -3,6 +3,11 @@ import Zcash.Snark.Fixtures.SingleAction.Honest.TrustBoundary
 import Zcash.Snark.Fixtures.SingleAction.Random.TrustBoundary
 import Zcash.Snark.Fixtures.MultiAction.Honest.TrustBoundary
 import Zcash.Snark.Fixtures.MultiAction.Random.TrustBoundary
+import Zcash.Snark.Fixtures.Prover.TrustBoundary
+import Zcash.Snark.ZeroKnowledge.TrustBoundary
+import Zcash.Snark.ZeroKnowledge.Vesta.TrustBoundary
+import Zcash.Snark.ZeroKnowledge.Action.TrustBoundary
+import Zcash.Snark.ZeroKnowledge.Zakura.TrustBoundary
 
 /-!
 # Endpoint-census completeness at the elaborated environment

Zcash/Circuits/Action/Circuit.lean

@@ -1388,10 +1388,12 @@ private def pointHint (key : String) :
     y := .hintGet key 2 (.const 0) 1
   }
 
-/-- One Nat-valued Action hint, read through the field-to-Nat bridge. -/
+/-- One scalar-valued Action hint, stored as low and high 128-bit limbs in row zero.
+Recombine their natural representatives before computing scalar windows. -/
 private def natHint (key : String) :
     Witgen.MOver Fp (AssignedCell Fp) (NExpr Fp) :=
-  pure (.val (.hintGet key 1 (.const 0) 0))
+  pure (.add (.val (.hintGet key 2 (.const 0) 0))
+    (.mul (.const (2 ^ 128)) (.val (.hintGet key 2 (.const 0) 1))))
 
 /-- A Merkle sibling hint at layer `i`. -/
 private def merkleSiblingHint (i : ℕ) : WitgenIR Fp 1 :=