diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 3dd73c49..5fef6799 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -8,6 +8,15 @@ on: workflow_dispatch: jobs: + guards: + # Lightweight source-policy gates — run on a standard runner in parallel with the + # heavy build so a forbidden pattern blocks the PR in seconds without a Lean build. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: No skipKernelTC in source + run: scripts/check_no_skipkerneltc.sh + build: runs-on: [ diff --git a/AGENTS.md b/AGENTS.md index fe3d2d1d..2123de2d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -182,6 +182,13 @@ These are the keepers from sp1-lean's "faithful sub-circuit composition" discipl zero-imports header). - Heavy `toBitVec64` rw chains are whnf-expensive — `set_option maxHeartbeats 2000000 in` (carry lemmas need up to `16000000`). +- **Never `set_option (debug.)skipKernelTC`.** It bypasses the kernel's type-check re-run — the trust anchor + for an axiom-clean proof — so it is **CI-gated** (`scripts/check_no_skipkerneltc.sh`, run by the audit and a + standalone CI `guards` job; any hit in `SP1Clean/**/*.lean` fails the build). If a goal blocks on a kernel + deep-recursion / `2^64`-unfold error, the fix is to factor the expensive compute into an **abstract-`BitVec` + helper** proved once over variables (the `srl_toNat`/`sra_toNat` pattern), then apply it symbolically — never + silence the kernel. See `docs/agents/proof-patterns.md` §"Bit-shift chip soundness" (the `2^64` bullet) for + the worked fix. - `mul_eq_zero` won't fire on `ZMod p` (a `Nat.rec` Mul-instance quirk) — derive booleanness via `inv_mul_cancel₀` / a `bool_of_mul_pred`-style lemma instead. - `Word` is an `abbrev` for `Vector` — `w.toBitVec64` dot-notation fails; write `Word.toBitVec64 w`. diff --git a/SP1Clean/Model/SailMemory.lean b/SP1Clean/Model/SailMemory.lean index 2bcf6a01..68b09e3f 100644 --- a/SP1Clean/Model/SailMemory.lean +++ b/SP1Clean/Model/SailMemory.lean @@ -115,7 +115,7 @@ lemma run_within_mmio_readable_mmio (reg_val : BitVec 64) (offset : BitVec 64) (h_htif : s.regs.get Register.htif_tohost_base (hs _) = none) : (within_mmio_readable (physaddr.Physaddr (zero_extend (BitVec.addInt (reg_val + offset) 0))) width).run s = .ok false s := by - have h_base : BitVec.toNat plat_clint_base = 33554432 := by native_decide + have h_base : BitVec.toNat plat_clint_base = 33554432 := by rfl have h_bv : (reg_val + offset).toNat = (reg_val.toNat + offset.toNat) % 18446744073709551616 := BitVec.toNat_add reg_val offset simp [within_mmio_readable, get_config_rvfi, within_clint] @@ -130,7 +130,7 @@ lemma run_within_mmio_writable_mmio (reg_val : BitVec 64) (offset : BitVec 64) (h_htif : s.regs.get Register.htif_tohost_base (hs _) = none) : (within_mmio_writable (physaddr.Physaddr (zero_extend (BitVec.addInt (reg_val + offset) 0))) width).run s = .ok false s := by - have h_base : BitVec.toNat plat_clint_base = 33554432 := by native_decide + have h_base : BitVec.toNat plat_clint_base = 33554432 := by rfl have h_bv : (reg_val + offset).toNat = (reg_val.toNat + offset.toNat) % 18446744073709551616 := BitVec.toNat_add reg_val offset simp [within_mmio_writable, get_config_rvfi, within_clint] diff --git a/SP1Clean/Proofs/Chips/ShiftRightChip/Math.lean b/SP1Clean/Proofs/Chips/ShiftRightChip/Math.lean index 665f9410..e51a893a 100644 --- a/SP1Clean/Proofs/Chips/ShiftRightChip/Math.lean +++ b/SP1Clean/Proofs/Chips/ShiftRightChip/Math.lean @@ -9,42 +9,71 @@ functions (`RV64.srl`/`sra`/`srlw`/`sraw` from `RISCV/Instructions.lean`). Split (the chip-folder convention, mirroring `DivRemChip/Math.lean`): these are pure `Word`/`BitVec`/`ZMod p` lemmas with no circuit context. -Several carry `set_option debug.skipKernelTC true in` to isolate the documented `2^64` kernel -deep-recursion landmine (`BitVec.toNat_ushiftRight` at `BitVec 64` plants `2^64`; see `docs/agents/proof-patterns.md`). -The option only skips a kernel *re-check* — it adds **no** axiom (`#print axioms` still shows the standard -`[propext, Classical.choice, Quot.sound]`). Keep those `set_option`/`omit` lines verbatim. -/ +The `RV64.srl`/`sra` `.toNat` reductions plant a `2^64` that the kernel deep-recurses on when reduced +over a concrete `Word`-derived `BitVec 64` (`BitVec.toNat_ushiftRight`/`sshiftRight` via the +`@[expose]` shift bodies; see `docs/agents/proof-patterns.md`). Rather than suppress the kernel, +we isolate that unfold into abstract-`BitVec` bridges +(`srl_toNat`/`sra_toNat_{false,true}`, kernel-checked once over variables) and mask every `2^N` power +to a concrete literal — the `ShiftLeftChip` discipline. All lemmas are kernel-clean and axiom-clean +(`#print axioms` = `[propext, Classical.choice, Quot.sound]`). -/ namespace SP1Clean.ShiftRightChip variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)] local instance : NeZero p := ⟨by have := Fact.out (p := 2 ^ 17 < p); omega⟩ -set_option debug.skipKernelTC true in +/-! ### Abstract-`BitVec` RV64 shift bridges (kernel-clean isolation of the `2^64` landmine) + +`RV64.srl`/`RV64.sra` unfold (via `BitVec.ushiftRight`/`sshiftRight`'s `@[expose]` bodies) plants a +`2^64` the kernel deep-recurses on **when reduced over a concrete `Word`-derived `BitVec 64`**. We +isolate that unfold into these three lemmas over **abstract** `BitVec 64` arguments, where the `2^64` +body is kernel-checked once over variables (the discipline `ShiftLeftChip`'s `sll_rv64_eq` uses). The +`_div_to_bitvec` wrappers then only apply `BitVec.eq_of_toNat_eq` plus the clean `Word`-level +shift-count bridge — they never re-unfold a shift over a `Word` value, so they stay kernel-clean. -/ + +/-- `(RV64.srl c b).toNat` as a Nat division, over abstract `BitVec 64` (isolates the `2^64` unfold). -/ +lemma srl_toNat (c b : BitVec 64) : (RV64.srl c b).toNat = b.toNat / 2 ^ (c.toNat % 64) := by + have hsh : (BitVec.extractLsb 5 0 c).toNat = c.toNat % 64 := by + simp only [BitVec.extractLsb, BitVec.extractLsb'_toNat, Nat.shiftRight_zero] + simp only [RV64.srl] + rw [BitVec.ushiftRight_eq', BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, hsh] + +/-- `(RV64.sra c b).toNat` on a non-negative `b` (msb = 0): arithmetic = logical shift. -/ +lemma sra_toNat_false (c b : BitVec 64) (h_msb : b.msb = false) : + (RV64.sra c b).toNat = b.toNat / 2 ^ (c.toNat % 64) := by + have hsh : (BitVec.extractLsb 5 0 c).toNat = c.toNat % 64 := by + simp only [BitVec.extractLsb, BitVec.extractLsb'_toNat, Nat.shiftRight_zero] + simp only [RV64.sra] + rw [BitVec.sshiftRight_eq', BitVec.toNat_sshiftRight_of_msb_false h_msb, + Nat.shiftRight_eq_div_pow, hsh] + +/-- `(RV64.sra c b).toNat` on a negative `b` (msb = 1): the sign-filled complement form. -/ +lemma sra_toNat_true (c b : BitVec 64) (h_msb : b.msb = true) : + (RV64.sra c b).toNat = 2 ^ 64 - 1 - (2 ^ 64 - 1 - b.toNat) / 2 ^ (c.toNat % 64) := by + have hsh : (BitVec.extractLsb 5 0 c).toNat = c.toNat % 64 := by + simp only [BitVec.extractLsb, BitVec.extractLsb'_toNat, Nat.shiftRight_zero] + simp only [RV64.sra] + rw [BitVec.sshiftRight_eq', BitVec.toNat_sshiftRight_of_msb_true h_msb, + Nat.shiftRight_eq_div_pow, hsh] + omit [Fact (Nat.Prime p)] in -/-- **Goal-shape conversion for SRL, lifted to dodge the `2^64` kernel deep-recursion.** -`BitVec.toNat_ushiftRight` at `BitVec 64` plants `2^64` via `BitVec.ushiftRight`'s body, tripping -the kernel re-check. Lifting isolates the trigger to this lemma, and `debug.skipKernelTC` skips its -kernel re-check (`#print axioms` still shows the standard set — the option only removes the -re-verification layer for the known `2^64` shape). -Reduces the `RV64.srl` Spec equality to the Nat division form the `srl_close_su16_*` lemmas produce, with -the shift count already normalised to `rs2[0].val % 64`. -/ +/-- **Goal-shape conversion for SRL.** Reduces the `RV64.srl` Spec equality to the Nat division form the +`srl_close_su16_*` lemmas produce, with the shift count normalised to `rs2[0].val % 64`. The `2^64` +kernel landmine is isolated in `srl_toNat`; here only `BitVec.eq_of_toNat_eq` and the clean shift-count +bridge are used. -/ lemma srl_div_to_bitvec (W rs1 rs2 : Word (ZMod p)) (h_rs2U : Word.isU64 rs2) (hdiv : (Word.toBitVec64 W).toNat = (Word.toBitVec64 rs1).toNat / 2 ^ (rs2[0].val % 64)) : Word.toBitVec64 W = RV64.srl (Word.toBitVec64 rs2) (Word.toBitVec64 rs1) := by - have he : (BitVec.extractLsb 5 0 (Word.toBitVec64 rs2)).toNat = rs2[0].val % 64 := by - rw [show (BitVec.extractLsb 5 0 (Word.toBitVec64 rs2)).toNat - = (Word.toBitVec64 rs2).toNat % 2 ^ 6 from by - simp [BitVec.extractLsb, BitVec.extractLsb'_toNat, Nat.shiftRight_zero]] - rw [Word.toBitVec64_toNat h_rs2U, Word.toNat_def]; omega - rw [← BitVec.toNat_inj] - simp only [RV64.srl] - rw [BitVec.ushiftRight_eq'] - rw [BitVec.toNat_ushiftRight] - simp only [Nat.shiftRight_eq_div_pow] - rw [he]; exact hdiv + have hsh : (Word.toBitVec64 rs2).toNat % 64 = rs2[0].val % 64 := by + rw [Word.toBitVec64_toNat h_rs2U, Word.toNat_def, + show (2:ℕ)^16 = 65536 from by norm_num, show (2:ℕ)^32 = 4294967296 from by norm_num, + show (2:ℕ)^48 = 281474976710656 from by norm_num] + omega + apply BitVec.eq_of_toNat_eq + rw [srl_toNat, hsh] + exact hdiv -set_option debug.skipKernelTC true in omit [Fact (Nat.Prime p)] in /-- **SRA goal-shape conversion, MSB = 0 arm.** On a non-negative `rs1` (`toBitVec64 rs1`.msb = false), arithmetic shift = logical shift, so `RV64.sra` reduces to the same Nat division form as `RV64.srl`. -/ @@ -52,18 +81,15 @@ lemma sra_div_to_bitvec_false (W rs1 rs2 : Word (ZMod p)) (h_rs2U : Word.isU64 r (h_msb : (Word.toBitVec64 rs1).msb = false) (hdiv : (Word.toBitVec64 W).toNat = (Word.toBitVec64 rs1).toNat / 2 ^ (rs2[0].val % 64)) : Word.toBitVec64 W = RV64.sra (Word.toBitVec64 rs2) (Word.toBitVec64 rs1) := by - have he : (BitVec.extractLsb 5 0 (Word.toBitVec64 rs2)).toNat = rs2[0].val % 64 := by - rw [show (BitVec.extractLsb 5 0 (Word.toBitVec64 rs2)).toNat - = (Word.toBitVec64 rs2).toNat % 2 ^ 6 from by - simp [BitVec.extractLsb, BitVec.extractLsb'_toNat, Nat.shiftRight_zero]] - rw [Word.toBitVec64_toNat h_rs2U, Word.toNat_def]; omega - rw [← BitVec.toNat_inj] - simp only [RV64.sra] - rw [BitVec.sshiftRight_eq', BitVec.toNat_sshiftRight_of_msb_false h_msb] - simp only [Nat.shiftRight_eq_div_pow] - rw [he]; exact hdiv + have hsh : (Word.toBitVec64 rs2).toNat % 64 = rs2[0].val % 64 := by + rw [Word.toBitVec64_toNat h_rs2U, Word.toNat_def, + show (2:ℕ)^16 = 65536 from by norm_num, show (2:ℕ)^32 = 4294967296 from by norm_num, + show (2:ℕ)^48 = 281474976710656 from by norm_num] + omega + apply BitVec.eq_of_toNat_eq + rw [sra_toNat_false _ _ h_msb, hsh] + exact hdiv -set_option debug.skipKernelTC true in omit [Fact (Nat.Prime p)] in /-- **SRA goal-shape conversion, MSB = 1 arm.** On a negative `rs1`, arithmetic shift fills the high bits with the sign, giving the `2^64 - 1 - (2^64 - 1 - rs1) / 2^shamt` form (`toNat_sshiftRight_of_msb_true`). -/ @@ -72,32 +98,30 @@ lemma sra_div_to_bitvec_true (W rs1 rs2 : Word (ZMod p)) (h_rs2U : Word.isU64 rs (hsra : (Word.toBitVec64 W).toNat = 2 ^ 64 - 1 - (2 ^ 64 - 1 - (Word.toBitVec64 rs1).toNat) / 2 ^ (rs2[0].val % 64)) : Word.toBitVec64 W = RV64.sra (Word.toBitVec64 rs2) (Word.toBitVec64 rs1) := by - have he : (BitVec.extractLsb 5 0 (Word.toBitVec64 rs2)).toNat = rs2[0].val % 64 := by - rw [show (BitVec.extractLsb 5 0 (Word.toBitVec64 rs2)).toNat - = (Word.toBitVec64 rs2).toNat % 2 ^ 6 from by - simp [BitVec.extractLsb, BitVec.extractLsb'_toNat, Nat.shiftRight_zero]] - rw [Word.toBitVec64_toNat h_rs2U, Word.toNat_def]; omega - rw [← BitVec.toNat_inj] - simp only [RV64.sra] - rw [BitVec.sshiftRight_eq', BitVec.toNat_sshiftRight_of_msb_true h_msb] - simp only [Nat.shiftRight_eq_div_pow] - rw [he]; exact hsra + have hsh : (Word.toBitVec64 rs2).toNat % 64 = rs2[0].val % 64 := by + rw [Word.toBitVec64_toNat h_rs2U, Word.toNat_def, + show (2:ℕ)^16 = 65536 from by norm_num, show (2:ℕ)^32 = 4294967296 from by norm_num, + show (2:ℕ)^48 = 281474976710656 from by norm_num] + omega + apply BitVec.eq_of_toNat_eq + rw [sra_toNat_true _ _ h_msb, hsh] + exact hsra -set_option debug.skipKernelTC true in omit [Fact (Nat.Prime p)] [Fact (2 ^ 17 < p)] in /-- The MSB of `rs1`'s low 32 bits is the high bit of limb 1 (`rs1[1] ≥ 2^15`). The SRAW sign bit. -Lifted with `debug.skipKernelTC` to dodge the `2^64` kernel deep-recursion (same landmine as the -`*_div_to_bitvec` helpers — `Word.toBitVec64` plants `2^64` via `BitVec` reduction). -/ +Mirrors the kernel-clean `ShiftRightMath.toBitVec64_msb_eq_b3_ge` template: a `rw` chain (not +`simp only`) plus full concrete-literal masking of every `2^N` power (incl. `2^48`), so the kernel +never deep-recurses on a symbolic power. -/ lemma low32_msb_eq_b1 [NeZero p] {b : Word (ZMod p)} (h_isU64 : Word.isU64 b) : (BitVec.extractLsb' 0 32 (Word.toBitVec64 b)).msb = decide (b[1].val ≥ 32768) := by obtain ⟨b0_16, b1_16, _, _⟩ := Word.lt_cases_of_isU64 h_isU64 - rw [BitVec.msb_eq_decide] - simp only [BitVec.extractLsb'_toNat, Word.toBitVec64_toNat h_isU64, Word.toNat_def, - Nat.shiftRight_zero] + rw [BitVec.msb_eq_decide, BitVec.extractLsb'_toNat, Nat.shiftRight_zero, + Word.toBitVec64_toNat h_isU64, Word.toNat_def] have e16 : (2 : ℕ) ^ 16 = 65536 := by decide have e31 : (2 : ℕ) ^ (32 - 1) = 2147483648 := by decide have e32 : (2 : ℕ) ^ 32 = 4294967296 := by decide - rw [e16, e31, e32] at * + have e48 : (2 : ℕ) ^ 48 = 281474976710656 := by decide + rw [e16, e31, e32, e48] at * congr 1 apply propext constructor @@ -114,7 +138,6 @@ lemma hword_toNat {a b : ZMod p} (ha : a.val < 2 ^ 16) (hb : b.val < 2 ^ 16) : List.getElem_toArray, List.getElem_cons_zero, List.getElem_cons_succ] omega -set_option debug.skipKernelTC true in /-- **SRLW goal-shape conversion.** The committed result word `Wd` is the 64-bit sign-extension of the low-32 logical shift. Uses `toBitVec64_signExtend_word` (the W-variant keystone): `Wd[2] = Wd[3] = m*65535` sign-fill with `m` the output high bit (`srw_msb` on `a[1]`), and the low two limbs carry the 32-bit logical @@ -145,7 +168,6 @@ lemma srlw_div_to_bitvec (Wd rs1 rs2 : Word (ZMod p)) hlow, hshamt]; exact hdiv.symm rw [toBitVec64_signExtend_word Wd _ m hr0 hr1 hm hr2 hr3 hX]; rfl -set_option debug.skipKernelTC true in /-- **SRAW goal-shape conversion, MSB = 0 arm.** On a non-negative low-32 input, the arithmetic word-shift equals the logical one, so the result is `signExtend 64` of the same division form as SRLW. -/ lemma sraw_div_to_bitvec_false (Wd rs1 rs2 : Word (ZMod p)) @@ -174,7 +196,6 @@ lemma sraw_div_to_bitvec_false (Wd rs1 rs2 : Word (ZMod p)) rw [toBitVec64_signExtend_word Wd _ m hr0 hr1 hm hr2 hr3 hX] simp only [RV64.sraw, BitVec.extractLsb] -set_option debug.skipKernelTC true in /-- **SRAW goal-shape conversion, MSB = 1 arm.** On a negative low-32 input, the arithmetic word-shift fills with the sign, giving the `2^32 - 1 - (2^32 - 1 - rs1.low32) / 2^shamt` complement form (`toNat_sshiftRight_of_msb_true` at width 32), then `signExtend 64`. -/ diff --git a/docs/agents/proof-patterns.md b/docs/agents/proof-patterns.md index 6333b50d..0c7f512a 100644 --- a/docs/agents/proof-patterns.md +++ b/docs/agents/proof-patterns.md @@ -168,14 +168,22 @@ drops `section`/`end` markers and `/--` openers (strip/restore them). .prev_value` by `rs2 := adapter.op_c_memory.prev_value` (like `BranchChip`), and `Assumptions` bound `isU64` of *those reads* — otherwise the operand is disconnected from everything the circuit constrains and soundness is unprovable. (Contrast Add/Lt, which pass `op_b_val` *into* an operation gadget.) -- **Kernel `2^64` deep-recursion → lift the conversion + `skipKernelTC`.** `BitVec.toNat_ushiftRight` at - `BitVec 64` plants `2^64` (via `BitVec.ushiftRight`'s `@[expose]` body), tripping the kernel re-check even - under `lake build`'s `--tstack`. The split-into-bare-`rw` (sp1-lean PROOF_PATTERNS §3 #8) was **not** - enough here. Fix: lift the `toBitVec64 cols.a = RV64.srl rs2 rs1 ⟸ (toBitVec64 cols.a).toNat = rs1.toNat - / 2^(c0.val%64)` conversion into a `private` helper (`srl_div_to_bitvec`) so the trigger is isolated, and - put `set_option debug.skipKernelTC true in` on it (the doc-acknowledged **axiom-clean** escape — only - skips re-verifying the known `2^64` shape). Lemma name is `BitVec.extractLsb'_toNat` (not - `toNat_extractLsb'`); `extractLsb 5 0 = extractLsb' 0 6`, `.toNat = x.toNat % 2^6`. +- **Kernel `2^64` deep-recursion → abstract-`BitVec` bridge, NOT `skipKernelTC`.** `BitVec.toNat_ushiftRight` + at `BitVec 64` plants `2^64` (via `BitVec.ushiftRight`'s `@[expose]` body); reduced **over a concrete + `Word`-derived `BitVec 64`** it deep-recurses the kernel re-check even under `lake build`'s `--tstack`. The + split-into-bare-`rw` (sp1-lean PROOF_PATTERNS §3 #8) was **not** enough. The kernel-clean fix (mirrors + `ShiftLeftChip`'s `sll_rv64_eq`, no `skipKernelTC`): isolate the `RV64.srl`/`sra` `.toNat` unfold into a + helper over **abstract `BitVec 64` args** (`ShiftRightChip/Math.lean` `srl_toNat`/`sra_toNat_{false,true}` : + `(RV64.srl c b).toNat = b.toNat / 2^(c.toNat % 64)`), where the `2^64` body is kernel-checked once over + variables. The `_div_to_bitvec` wrapper then only does `apply BitVec.eq_of_toNat_eq; rw [srl_toNat, hsh]` + with `hsh : (toBitVec64 rs2).toNat % 64 = rs2[0].val % 64` proved the clean `ShiftLeft` way + (`Word.toBitVec64_toNat` + `Word.toNat_def` + `show (2:ℕ)^N = ` masks + `omega`) — so it never + re-unfolds a shift over a `Word` value. For a non-shift `BitVec 64` msb/extract (`low32_msb_eq_b1`), mirror + `toBitVec64_msb_eq_b3_ge`: a `rw` chain (not `simp only`) + mask **every** `2^N` (incl. `2^48`) to a literal. + (Was `set_option debug.skipKernelTC true in` — removed 2026-06-18; now CI-gated by + `scripts/check_no_skipkerneltc.sh` so it can't come back. The option is the last-resort escape, not + the recipe.) Lemma name is `BitVec.extractLsb'_toNat` (not `toNat_extractLsb'`); `extractLsb 5 0 = + extractLsb' 0 6`, `.toNat = x.toNat % 2^6`. - **`simp only [id_eq]` before `linear_combination`/`ring` over field elements.** Clean wraps field elements as `id (ZMod p)`, which blocks `ring`'s instance synthesis (`IsRightCancelAdd (id (ZMod p))`). `clear_value` does **not** fix it; `simp only [id_eq] at h ⊢` does (the `BranchChip` L510 pattern). @@ -211,11 +219,18 @@ drops `section`/`end` markers and `/--` openers (strip/restore them). case-split on `op_b[3].val ≥ 32768` (BitVec msb via `ShiftRightMath.toBitVec64_msb_eq_b3_ge`). The msb=0 arm reuses the SRL dispatch (`sra_div_to_bitvec_false` → `srl_close`); the msb=1 arm uses `sra_div_to_bitvec_true` → `sra_close_su16_*_case` with `sraFill = 65536 − v0123`. Both conversion - helpers carry `skipKernelTC` (the `2^64` trigger). SRLW/SRAW are the 32-bit (2-limb `HWord`) analogs, + helpers route through the abstract-`BitVec` bridges `sra_toNat_{false,true}` (kernel-clean, no + `skipKernelTC` — see the `2^64` bullet above). SRLW/SRAW are the 32-bit (2-limb `HWord`) analogs, `signExtend 64`-packaged via `toBitVec64_signExtend_word`. ## Landmines +- **Never `set_option (debug.)skipKernelTC` (CI-gated).** It bypasses the kernel type-check re-run, defeating + the axiom-clean trust anchor. `scripts/check_no_skipkerneltc.sh` fails the audit and CI on any hit in + `SP1Clean/**/*.lean`. When a goal blocks on a kernel deep-recursion / `2^64`-unfold error, factor the + expensive compute into an abstract-`BitVec` helper proved once over variables and apply it symbolically — + see the `2^64` bullet under "Bit-shift chip soundness" above for the worked `srl_toNat`/`sra_toNat` fix. + ### Gadget-level (arithmetic, `Native/Operations/` + `Proofs/Operations/`) - **`circuit_proof_start` must be the FIRST tactic** in soundness/completeness. Any diff --git a/docs/release-audit.md b/docs/release-audit.md index a3a52cb6..43304428 100644 --- a/docs/release-audit.md +++ b/docs/release-audit.md @@ -196,7 +196,9 @@ any new carrier fails CI for the audit script. `scripts/run_audit.sh` (checked in — the predecessor document's "re-create the harness as needed" gap is closed): pins → green `lake build SP1Clean` (3630 jobs; the only warnings are the four known -`sorry`s) → text inventory with gates → `scripts/gen_axiom_probe.py` (namespace-tracking declaration +`sorry`s) → text inventory with gates (sorry-set, no `axiom` declarations, and the no-`skipKernelTC` +guard `scripts/check_no_skipkerneltc.sh` — also a standalone CI `guards` job) → +`scripts/gen_axiom_probe.py` (namespace-tracking declaration scanner; self-checking — a wrong FQN fails elaboration) → `lake env lean scripts/axiom_probe.lean` → bucket + gate. Extraction currency: `SP1_DIR=../sp1 python3 update_extracted.py && git diff --exit-code SP1Clean/Extracted` (the witness vectors regenerate in the same run and re-verify on the diff --git a/scripts/check_no_skipkerneltc.sh b/scripts/check_no_skipkerneltc.sh new file mode 100755 index 00000000..852f4d2c --- /dev/null +++ b/scripts/check_no_skipkerneltc.sh @@ -0,0 +1,29 @@ +#!/usr/bin/env bash +# Gate: no `set_option (debug.)skipKernelTC` anywhere in the Lean source tree. +# +# `skipKernelTC` bypasses the kernel's type-check re-run — the trust anchor for an +# axiom-clean proof. It was a last-resort escape used while proving the bit-shift chips; +# the last site was removed 2026-06-18 and replaced by abstract-`BitVec` helper bridges +# (see `docs/agents/proof-patterns.md` §"Bit-shift chip soundness", the `2^64` bullet). +# This gate keeps it out for good. +# +# Scope is `SP1Clean/**/*.lean` only — `docs/` legitimately *mentions* the token +# ("…NOT `skipKernelTC`"), so scanning the source tree avoids those false positives. +# There are zero legitimate uses in source, so any case-insensitive hit fails the gate. +# +# Used by `scripts/run_audit.sh` (A2 gate) and `.github/workflows/lean_action_ci.yml` +# (the lightweight `guards` job). Exit 0 = clean, 1 = reintroduced. +# +# Usage: scripts/check_no_skipkerneltc.sh (from the repo root) + +set -uo pipefail +cd "$(dirname "$0")/.." + +if grep -rniE 'skipKernelTC' SP1Clean --include='*.lean'; then + echo "FAIL: skipKernelTC reintroduced in SP1Clean/ (see lines above)." >&2 + echo " Fix the kernel error by factoring the expensive compute into an abstract-BitVec" >&2 + echo " helper proved once over variables (the srl_toNat/sra_toNat pattern) — do NOT" >&2 + echo " bypass the kernel. See docs/agents/proof-patterns.md." >&2 + exit 1 +fi +exit 0 diff --git a/scripts/run_audit.sh b/scripts/run_audit.sh index df7b0361..e14699dc 100755 --- a/scripts/run_audit.sh +++ b/scripts/run_audit.sh @@ -41,6 +41,14 @@ if grep -rnE '^[[:space:]]*axiom[[:space:]]' SP1Clean --include='*.lean'; then else echo "PASS: no axiom declarations" fi + +echo +echo "== A2 skipKernelTC guard (gate: none in SP1Clean/) ==" +if scripts/check_no_skipkerneltc.sh; then + echo "PASS: no skipKernelTC usage" +else + echo "FAIL: skipKernelTC reintroduced (see above)"; fail=1 +fi echo "native_decide occurrences (disclosed, witness battery + Sail memory bridges):" grep -rn 'native_decide' SP1Clean --include='*.lean' | wc -l