feat: remove skipKernelTC overrides and gate against reintroduction

.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:
       [

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`.

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]

SP1Clean/Proofs/Chips/ShiftRightChip/Math.lean

@@ -9,61 +9,87 @@ 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`. -/
 lemma sra_div_to_bitvec_false (W rs1 rs2 : Word (ZMod p)) (h_rs2U : Word.isU64 rs2)
     (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`. -/

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 = <literal>` 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