project-llzk · alexanderlhicks · Jun 11, 2026 · Jun 1, 2026 · Jun 2, 2026 · Jun 5, 2026
diff --git a/.github/workflows/certify.yml b/.github/workflows/certify.yml
@@ -32,16 +32,20 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: Cache .lake
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9
+        # GitHub rejects the old pinned cache SHA; use the maintained v4
+        # major until an audited v4 SHA is selected.
+        uses: actions/cache@v4
         with:
           path: |
             .lake
             ~/.elan
           key: lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}
 
       - name: lake update + build
+        env:
+          MATHLIB_NO_CACHE_ON_UPDATE: "1"
         run: |
-          lake update
+          lake update --no-cache
           lake build
 
       - name: Regenerate certs and compare to committed snapshot

diff --git a/.github/workflows/differential.yml b/.github/workflows/differential.yml
@@ -43,22 +43,23 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: Cache .lake
-        # actions/cache@v4.0.2
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9
+        # GitHub rejects the old pinned cache SHA; use the maintained v4
+        # major until an audited v4 SHA is selected.
+        uses: actions/cache@v4
         with:
           path: |
             .lake
             ~/.elan
           key: lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}
 
       - name: lake update + build
-        # `lake update` is a no-op against a SHA-pinned manifest, kept
-        # for the day we move to a branch pin. `lake build` builds the
-        # local LlzkLean lib + emit-certs exe; veir-opt builds lazily
-        # inside .lake/packages/VeIR/ on first `lake exec veir-opt`,
-        # which the differential script triggers.
+        # The manifest is SHA-pinned, but CI still needs Lake to hydrate
+        # dependencies. `--no-cache` avoids failing on the documented
+        # llzk-lean/mathlib toolchain split before the build starts.
+        env:
+          MATHLIB_NO_CACHE_ON_UPDATE: "1"
         run: |
-          lake update
+          lake update --no-cache
           lake build
 
       - name: Run differential harness

diff --git a/AGENTS.md b/AGENTS.md
@@ -0,0 +1,27 @@
+# llzk-lean Agent Entry
+
+Treat `docs/harness/CURRENT.md` as the active source of truth before doing
+dependency, differential, or certificate work in this repository.
+
+Required first checks:
+
+- Read `docs/harness/CURRENT.md`, `docs/harness/GATES.md`, and
+  `docs/harness/SOURCES.md`; read `docs/harness/PINS.md` before touching
+  Lake metadata or `.lake/packages/VeIR`.
+- Run `scripts/harness/doctor.sh --workspace-veir ../veir` from the repository
+  root when the companion checkout exists. If `../veir` is unavailable, run the
+  strict doctor without the workspace argument and report that the result is not
+  full acceptance evidence.
+- Run `scripts/harness/verify-pins.sh --workspace-veir ../veir` for any
+  dependency, review, or phase-close work.
+
+Policy:
+
+- Do not rely on `.lake/packages/VeIR` as hidden proof state.
+- Dirty dependency state is never acceptance evidence. Use `--mode exploratory`
+  only to investigate a mismatch, and report that mode explicitly.
+- Do not treat a missing `llzk-opt`, missing MLIR headers, or CI skip as
+  Strategy A or Strategy E coverage.
+- Keep phase evidence under the active phase directory
+  (`reviews/PHASE-01/evidence/` for the current pin phase) when changing
+  canonical harness docs, pins, or gates.
diff --git a/EmitCerts.lean b/EmitCerts.lean
@@ -92,7 +92,7 @@ def jsonHeader (certCount : Nat) : String :=
   s!"\{\n  \"schemaVersion\": \"0.2.0\",\n  \
 \"source\": \"VEIR Veir.Passes.Felt.Combine (stub catalog — {certCount} of 15 patterns)\",\n  \
 \"_note\": \"Hand-listed catalog. The full 15-pattern catalog will be derived reflectively from VEIR's Veir.Passes.Felt.Combine; today's source is LlzkLean.Cert.feltCombineCatalog.\",\n  \
-\"_aboutLlzkParityStatus\": \"Per-cert tag indicating how a VEIR rewrite relates to LLZK's runtime: 'aligned' = LLZK performs the same rewrite exactly; 'aligned-with-caveats' = LLZK performs it under additional conditions (e.g. modular reduction, field-name guard); 'veir-only' = LLZK has no matching fold or canonicalization pattern, the cert is a Lean-side soundness statement only. The C++ checker uses this to pick assertion polarity.\",\n  \
+\"_aboutLlzkParityStatus\": \"Per-cert tag indicating how a VEIR rewrite relates to LLZK's runtime: 'aligned' = LLZK performs the same rewrite exactly; 'aligned-with-caveats' = LLZK performs it under additional source-specific conditions; 'veir-only' = LLZK has no matching fold or canonicalization pattern, the cert is a Lean-side soundness statement only. The C++ checker uses this to pick assertion polarity.\",\n  \
 \"certs\": [\n    "
 
 def main : IO Unit := do

diff --git a/LlzkLean/Cert.lean b/LlzkLean/Cert.lean
@@ -255,14 +255,13 @@ def Cert.mk' (patternId : String) (rootKind : String)
 -/
 def feltCombineCatalog : List Cert := [
   -- VEIR-side soundness claim with no current LLZK counterpart.
-  -- LLZK's `AddFeltOp::fold` (lib/Dialect/Felt/IR/Ops.cpp:141-149)
-  -- only folds when *both* operands are FeltConstAttrs with
-  -- matching, registered field names; LLZK registers no
-  -- canonicalization patterns for AddFeltOp. So this cert is a
-  -- VEIR-only soundness statement, not a contract on LLZK runtime
-  -- behavior. Strategy-E's checker should treat veir-only certs as
-  -- informational (label them in --verify-rewrites output, do not
-  -- assert LLZK ever exhibits the rewrite).
+  -- LLZK's `AddFeltOp::fold` only folds when *both* operands are
+  -- FeltConstAttrs with matching, registered field names; LLZK
+  -- registers no canonicalization patterns for AddFeltOp. So this
+  -- cert is a VEIR-only soundness statement, not a contract on LLZK
+  -- runtime behavior. Strategy-E's checker should treat veir-only
+  -- certs as informational (label them in --verify-rewrites output,
+  -- do not assert LLZK ever exhibits the rewrite).
   -- v0.2.0: `.const "felt.const" (some 0)` pins the literal value
   -- in the shape itself rather than via a separate constEquals
   -- condition. `commutative := true` flags felt.add as
@@ -276,26 +275,13 @@ def feltCombineCatalog : List Cert := [
     (conditions := [])
     (llzkParityStatus := .veirOnly)
     (description := "felt.add x (felt.const 0) → x. Sound over any ZMod p."),
-  -- LLZK does this fold (Ops.cpp:141-149) but with two caveats VEIR
-  -- doesn't share today:
-  --   (a) LLZK short-circuits unless both operands have a registered
-  --       field name (tryGetBinaryFoldData, Ops.cpp:57-79); VEIR's
-  --       fold has no field-name guard.
-  --   (b) LLZK applies modular reduction (field->reduce); VEIR's
-  --       implementation stores c1+c2 as an unreduced Int.
-  -- Both gaps are tracked in VEIR's FELT_PARITY_ASSESSMENT.
-  -- v0.2.0 expresses LLZK's actual fold conditions structurally:
-  --   - both operands' fieldName attrs must match (sameAttr) —
-  --     this is `lhsFieldName == rhsFieldName` in
-  --     llzk-lib/lib/Dialect/Felt/IR/Ops.cpp:66
-  --   - the shared fieldName must resolve in LLZK's Field
-  --     registry (attrInRegistry) — i.e. Field::tryGetField at
-  --     Ops.cpp:70-73 succeeds
-  -- With these conditions in place, this cert correctly describes
-  -- LLZK's fold *when the inputs are named-field*. (For unnamed
-  -- !felt.type operands LLZK still short-circuits to a no-op;
-  -- VEIR's fold fires unconditionally — that gap remains and
-  -- requires the Field-registry parity work on the VEIR side.)
+  -- LLZK does this fold when both operands share a registered field name.
+  -- Phase 7 aligns VEIR's registered-field fold result with LLZK's
+  -- `Field::reduce`; the side conditions below express LLZK's actual fold
+  -- preconditions structurally:
+  --   - both operands' fieldName attrs must match (sameAttr)
+  --   - the shared fieldName must resolve in LLZK's Field registry
+  --     (attrInRegistry)
   Cert.mk'
     (patternId := "constant_fold_add")
     (rootKind := "felt.add")
@@ -305,8 +291,8 @@ def feltCombineCatalog : List Cert := [
       .sameAttr "fieldName" ["lhs", "rhs"],
       .attrInRegistry "lhs" "fieldName" "field"
     ])
-    (llzkParityStatus := .alignedWithCaveats)
-    (description := "felt.add (felt.const c1) (felt.const c2) → felt.const (c1+c2). Sound over any ZMod p. Caveat: LLZK applies modular reduction (field->reduce); VEIR's runtime fold stores c1+c2 unreduced. Otherwise aligned.")
+    (llzkParityStatus := .aligned)
+    (description := "felt.add (felt.const c1) (felt.const c2) → felt.const (c1+c2 reduced through the registered field). Sound over any ZMod p and aligned with LLZK's Field::reduce under the recorded registry side conditions.")
   -- TODO: derive the remaining 13 entries from
   --   Veir.Passes.Felt.Combine reflectively. Hand-listed here as
   --   stub-quality scaffolding — the real emitter walks the Lean

diff --git a/LlzkLean/CertValidate.lean b/LlzkLean/CertValidate.lean
@@ -39,6 +39,21 @@ import Veir.Passes.Felt.Proofs
 
 namespace LlzkLean.Cert
 
+section
+
+private partial def exprContainsConst (target : Lean.Name) : Lean.Expr → Bool
+  | .const n _ => n == target
+  | .app f a => exprContainsConst target f || exprContainsConst target a
+  | .lam _ t b _ => exprContainsConst target t || exprContainsConst target b
+  | .forallE _ t b _ => exprContainsConst target t || exprContainsConst target b
+  | .letE _ t v b _ =>
+      exprContainsConst target t || exprContainsConst target v || exprContainsConst target b
+  | .mdata _ b => exprContainsConst target b
+  | .proj _ _ b => exprContainsConst target b
+  | _ => false
+
+end
+
 open Lean Elab Command in
 /--
   Build-time assertion that the fully-qualified Lean name `nameStr`
@@ -77,7 +92,7 @@ elab "#assertCatalogCoverage" : command => do
   let mut veirPatternIds : List String := []
   for (n, info) in env.constants.toList do
     match n, info with
-    | .str parent baseName, .defnInfo _ =>
+    | .str parent baseName, .defnInfo defnInfo =>
       -- Filter to rewrite-pattern defs only. VEIR's pattern namespace
       -- also contains:
       --   - `matchAdd`, `matchSub`, ... — helper matchers (start with
@@ -87,12 +102,26 @@ elab "#assertCatalogCoverage" : command => do
       --   - `Combine.impl` — the pass body (compound name; filtered
       --     by the `Name.str parent baseName` pattern only matching
       --     single-segment names below the namespace).
+      --   - `projectToOperand`, `replaceWithNewOp`, and
+      --     `replaceWithBinOpOfConst` — shared rewrite tails used by the
+      --     verified patterns, not standalone rewrite patterns.
       -- A rewrite pattern's base name doesn't start with `match` or
-      -- `Combine` and isn't an internal `_*` name.
+      -- `Combine`, isn't an internal `_*` name, and isn't one of those
+      -- shared helper tails.
       let isHelper := baseName.startsWith "match"
       let isPass   := baseName == "Combine"
       let isInternal := baseName.startsWith "_"
-      if parent == nsPrefix && !isHelper && !isPass && !isInternal then
+      let isRewriteTailHelper :=
+        baseName == "projectToOperand" ||
+        baseName == "replaceWithNewOp" ||
+        baseName == "replaceWithBinOpOfConst"
+      -- Actual rewrite patterns take the active pattern rewriter plus an
+      -- operation pointer. This keeps ordinary helpers in `Veir.FeltPass`
+      -- from inflating the certificate coverage count.
+      let isPatternShaped :=
+        exprContainsConst ``Veir.PatternRewriter defnInfo.type &&
+        exprContainsConst ``Veir.OperationPtr defnInfo.type
+      if parent == nsPrefix && isPatternShaped && !isHelper && !isPass && !isInternal && !isRewriteTailHelper then
         veirPatternIds := baseName :: veirPatternIds
     | _, _ => pure ()
   let catalogIds := feltCombineCatalog.map (·.patternId)

diff --git a/README.md b/README.md
@@ -25,9 +25,10 @@ LLZK's Felt dialect:
   actual MLIR rewrites conform to the catalog at runtime, keeping Lean
   and Mathlib out of LLZK's runtime trusted base.
 
-The 15 verified Felt-dialect rewrites the catalog references live in
-VEIR on the [`llzkfelt_test1`](https://github.com/project-llzk/veir/tree/llzkfelt_test1)
-branch.
+The current proof basis is the clean VEIR commit
+[`d4cc1bf2d31beeca17eb2e8c9c7181d04af013a3`](docs/harness/PINS.md),
+selected from `project-llzk/veir` branch `felt-review-structural-close`
+and pinned through Lake metadata.
 
 ## Repository contents
 
@@ -49,6 +50,11 @@ documented under [`docs/`](docs/):
   A design + harness usage.
 - [`docs/strategy-e-certificates.md`](docs/strategy-e-certificates.md)
   — Strategy E cert format, lifecycle, and checker design.
+- [`docs/harness/PINS.md`](docs/harness/PINS.md) — current accepted
+  VEIR pin, update procedure, rollback procedure, and forbidden hidden
+  dependency state.
+- [`docs/harness/CURRENT.md`](docs/harness/CURRENT.md) — active
+  phase and acceptance rule for the harness.
 - [`docs/future-b-extraction.md`](docs/future-b-extraction.md) —
   Future: extract VEIR's verified rewriter to C++.
 - [`docs/future-c-drop-in.md`](docs/future-c-drop-in.md) — Future:

diff --git a/certs/felt-combine.cert.json b/certs/felt-combine.cert.json
@@ -2,9 +2,9 @@
   "schemaVersion": "0.2.0",
   "source": "VEIR Veir.Passes.Felt.Combine (stub catalog — 2 of 15 patterns)",
   "_note": "Hand-listed catalog. The full 15-pattern catalog will be derived reflectively from VEIR's Veir.Passes.Felt.Combine; today's source is LlzkLean.Cert.feltCombineCatalog.",
-  "_aboutLlzkParityStatus": "Per-cert tag indicating how a VEIR rewrite relates to LLZK's runtime: 'aligned' = LLZK performs the same rewrite exactly; 'aligned-with-caveats' = LLZK performs it under additional conditions (e.g. modular reduction, field-name guard); 'veir-only' = LLZK has no matching fold or canonicalization pattern, the cert is a Lean-side soundness statement only. The C++ checker uses this to pick assertion polarity.",
+  "_aboutLlzkParityStatus": "Per-cert tag indicating how a VEIR rewrite relates to LLZK's runtime: 'aligned' = LLZK performs the same rewrite exactly; 'aligned-with-caveats' = LLZK performs it under additional source-specific conditions; 'veir-only' = LLZK has no matching fold or canonicalization pattern, the cert is a Lean-side soundness statement only. The C++ checker uses this to pick assertion polarity.",
   "certs": [
     {"patternId":"right_identity_zero_add","rootKind":"felt.add","lhs":{"kind":"opResult","opKind":"felt.add","operands":[{"kind":"any"},{"kind":"const","opKind":"felt.const","value":0}],"commutative":true},"rhs":{"kind":"any"},"conditions":[],"theoremName":"Veir.Data.Felt.right_identity_zero_add","llzkParityStatus":"veir-only","description":"felt.add x (felt.const 0) → x. Sound over any ZMod p."},
-    {"patternId":"constant_fold_add","rootKind":"felt.add","lhs":{"kind":"opResult","opKind":"felt.add","operands":[{"kind":"const","opKind":"felt.const"},{"kind":"const","opKind":"felt.const"}],"commutative":true},"rhs":{"kind":"const","opKind":"felt.const"},"conditions":[{"kind":"sameAttr","attr":"fieldName","positions":["lhs","rhs"]},{"kind":"attrInRegistry","pos":"lhs","attr":"fieldName","registry":"field"}],"theoremName":"Veir.Data.Felt.constant_fold_add","llzkParityStatus":"aligned-with-caveats","description":"felt.add (felt.const c1) (felt.const c2) → felt.const (c1+c2). Sound over any ZMod p. Caveat: LLZK applies modular reduction (field->reduce); VEIR's runtime fold stores c1+c2 unreduced. Otherwise aligned."}
+    {"patternId":"constant_fold_add","rootKind":"felt.add","lhs":{"kind":"opResult","opKind":"felt.add","operands":[{"kind":"const","opKind":"felt.const"},{"kind":"const","opKind":"felt.const"}],"commutative":true},"rhs":{"kind":"const","opKind":"felt.const"},"conditions":[{"kind":"sameAttr","attr":"fieldName","positions":["lhs","rhs"]},{"kind":"attrInRegistry","pos":"lhs","attr":"fieldName","registry":"field"}],"theoremName":"Veir.Data.Felt.constant_fold_add","llzkParityStatus":"aligned","description":"felt.add (felt.const c1) (felt.const c2) → felt.const (c1+c2 reduced through the registered field). Sound over any ZMod p and aligned with LLZK's Field::reduce under the recorded registry side conditions."}
   ]
 }
diff --git a/checker/src/CertChecker.cpp b/checker/src/CertChecker.cpp
@@ -566,8 +566,9 @@ class DefaultMatcher : public Matcher {
     //   - ConstEquals: resolve `pos`, check it's a constant of expected value.
     //   - SameAttr: resolve each position, extract named attribute, compare.
     //   - AttrInRegistry: resolve `pos`, extract attr, check against
-    //     a hardcoded LLZK Field registry (initial: the six built-in
-    //     fields {bn128, bn254, babybear, goldilocks, mersenne31,
+    //     the accepted LLZK Field registry (Phase 2 source:
+    //     lib/Util/Field.cpp at llzk-lib db922857bc5a; built-ins
+    //     {bn128, bn254, grumpkin, babybear, goldilocks, mersenne31,
     //     koalabear}). Pluggable registries are a v0.3 feature.
     //   - ConstCompare: like ConstEquals, with CompareOp dispatch.
     //   - ResultTypeFromOperand: resolve `pos`, compare mlir::Type.

diff --git a/checker/src/CertChecker.h b/checker/src/CertChecker.h
@@ -88,8 +88,8 @@ enum class LlzkParityStatus {
   /// LLZK performs exactly this rewrite, same canonical output as the
   /// Lean spec. checkRewrite asserts LLZK's transformation matches.
   Aligned,
-  /// LLZK performs this rewrite under additional conditions the Lean
-  /// spec doesn't impose (e.g. field-name guard, modular reduction).
+  /// LLZK performs this rewrite under additional source-specific
+  /// conditions the Lean spec doesn't impose.
   /// checkRewrite asserts match-modulo-caveat; full alignment is a
   /// future-work item tracked per pattern.
   AlignedWithCaveats,
@@ -167,9 +167,8 @@ std::optional<CertCatalog> loadCertCatalog(const std::string &path,
 ///     AlignedWithCaveats cert — no caveat was needed).
 ///   - `matchedParity == AlignedWithCaveats` + `caveatTriggered == true`:
 ///     LHS + conditions matched but LLZK's replacement differs from
-///     the cert's RHS shape. The cert acknowledges this can happen
-///     (e.g., LLZK applies field->reduce; VEIR doesn't); the
-///     `caveatTriggered` flag surfaces the divergence in the pass
+///     the cert's RHS shape. The cert acknowledges this can happen;
+///     the `caveatTriggered` flag surfaces the divergence in the pass
 ///     diagnostics.
 ///
 /// `accepted == false` means no cert matched. `rejectReason` is a

diff --git a/checker/tests/test_loader.cpp b/checker/tests/test_loader.cpp
@@ -202,7 +202,7 @@ TEST(load_committed_snapshot) {
   // Spot-check cert[1]: constant_fold_add
   const Cert &c1 = catalog->certs[1];
   EXPECT(c1.patternId == "constant_fold_add", "cert[1] patternId");
-  EXPECT(c1.llzkParityStatus == LlzkParityStatus::AlignedWithCaveats,
+  EXPECT(c1.llzkParityStatus == LlzkParityStatus::Aligned,
          "cert[1] parity");
   EXPECT(c1.conditions.size() == 2, "cert[1] has 2 conditions");
   EXPECT(c1.conditions[0].kind == SideCondition::Kind::SameAttr,