feat: Updates to foundations, and audit gap resolutions, and improved ergonomics by dtumad · Pull Request #92 · succinctlabs/sp1-lean

dtumad · 2026-04-25T19:51:33Z

Updates to Dependencies

Updates lean major version 4.23 -> 4.29 and resolves build errors
Updates to most recent Lean_RV64D extraction (as of 4/24 currently, should pin something pre-merge). Uses the main upstream repo now instead of a succinctlabs fork. Memory proofs in particular had large changes from this, largely for the better.
Updates the extraction to use public sp1 release v6.1.0 and fix breaking changes (no is_trusted or related constraints, some numerical opcode re-ordering, JALR changes)

Audit Gaps

Load proofs were not in the SP1Chips.lean file and contained unsurfaced stop calls as a result. Added them there and fixed all the gaps. Should add lake exe mk_all check to CI to protect against this in another PR.
Utype proofs were missing sorry stubs and so also didn't surface. Added them and fixed all the gaps.
slti proof incorrectly had access to an is_sltu assumption, making the proof trivial. Removed this and resolved the gap.

Assumption Changes

Added a pma_check axiom mirroring existing pmp_check axiom. Needed for the RV64D extraction update.
Removed mprotect_disabled assumption, as it's not needed for this release.
Removed assumptions about Register.plat_clint_base and Register.plat_clint_size. Not needed after RV64D update.
AUIPC and LUI trusted intruction constraints now include op_b_0.val % 2 ^ 12 = 0 instead of op_b_0 >= 2^12 (i.e. the value is properly zero-extended).
Added assumption that Register.mseccfg has a zero bit in position 10, i.e. Zicfilp is not enabled in M-mode. Needed for the RV64D extraction update.

General Changes

Add standard linters from ArkLib/Mathlib, fix all generated warnings, should add this check to CI.
Basic use of mathlib shake to add parallel compilation. Should probably also add this to CI.
Lots of refactors and updates to agent documentation. AI agents should run into pitfalls much less often now.
~40% speedup in DivRem and ShiftRight compile times, mostly by breaking obtain blocks apart, tweaking instance priorities, and extracting some shared helper lemmas.
Remove most of KoalaBear namespace and migrate lemmas to general fields (Full milestone 1 of EF grant needs constraint extraction updates as well).
Remove ``BoundedKoalaBear` and related abstractions completely

Move `mul_diff_one_neq` out of the `KoalaBear` namespace and restate it over any `[Field α]` — the proof goes through unchanged via aesop, and the lemma was only picked up as an aesop-forward rule so no callers reference it by name. Drop the 13 unused `KoalaBear.{ne_zero_*, val_*}` helpers (referenced only inside Field.lean); swap their internal uses in `inv_mul_*BB_eq_iff` for `by decide`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…sp1-lean into dtumad/milestone-3

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…sp1-lean into dtumad/milestone-3

Sail-v4 added two platform-level monadic reads inside control-flow instructions that the SP1 proofs cannot discharge from isInitialized alone: execute_JALR's new update_elp_state call (reads cur_privilege via currentlyEnabled Ext_Zicfilp), and jump_to's new alignment gate (reads misa via currentlyEnabled Ext_Zca). Mirror the pmp_check_machine pattern with three new axioms in SP1Foundations.Assumptions: - update_elp_state_of_isInitialized: SP1 doesn't enable Zicfilp, so update_elp_state reduces to pure (). - jump_to_of_mod4_eq_zero: 4-aligned targets skip the Zca check, making jump_to equivalent to writeReg nextPC target; pure RETIRE_SUCCESS. - jump_to_of_mask_mod4_eq_zero: specialisation for JALR's (rs1 + imm) & ~1 target shape. Plus SailState.isInitialized_insert so the axiom's side condition survives post-write state extensions, and mod4_eq_zero_of_0_1_are_0 (reverse of mul4_means_0_1_are_0) for chips that have bit-level alignment hypotheses instead of mod-4. Apply these to close the stop in JALR_correct. The same pattern is ready to unblock the 6 Branch stops and the Jal stop, pending local tactic plumbing (the ↑↑ vs #' BitVec.ofNat form mismatch). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…sp1-lean into dtumad/milestone-3

Suppress linter.unusedVariables in MemChecks.lean and BranchChip.lean (proofs there are stopped/sorried pending Sail v4 rewrite but keep their final parameter lists). Drop a no-op `repeat rw` in byte_decomp_128 that tripped unusedTactic/unreachableTactic, and mark BoundedKoalaBear.coe_of_le @[reducible] as required for class-valued defs in Lean 4.29. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…sp1-lean into dtumad/milestone-3

….com/succinctlabs/sp1-lean into dtumad/update-constraints-is-trusted

alexanderlhicks · 2026-04-29T16:19:28Z

  Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
  let _ ← execute_JAL imm rd

 set_option debug.skipKernelTC true in


how come this is needed (here and in other places)?

It is sort of hard to diagnose them, tends to have something to do with how sail generates many coercions between bitvec/nat/int. Often times these in theory discharge easily with reflexivity etc., but cause problems when the final proof compiles because we have large constants sitting around. #94 has started to fix some by just not having the koala bear prime in certain expressions, but still other things like Word.toBitVec64 still produce values like 2^48 in their terms, which the kernel can crash over when unifying.

The best MWE is probably something like:

example (b n : ℕ) : -- unifies properly ((b : ℤ) % n).toNat = b % n := by rfl example (b n : ℕ) : -- deep recursion ((b * 2^64 : ℤ) % n).toNat = (b * 2^64) % n := by rfl

I'd be fine scoping #94 to fix all of these as well, but it is really just hunting down and fixing overzealous unification with large constants, which can be difficult when aesop or simp do those things internally to their execution.

And also notably, the kernal is not shy about unfolding various things eagerly, so something like def Nat.twoPow (n : ℕ) : ℕ := 2 ^ n can't solve this.

alexanderlhicks · 2026-04-29T16:22:15Z


 -- Generated Lean code for chip LoadX0Chip
-@[irreducible] def constraints (Main : Vector (Fin KB) 50) : SP1ConstraintList :=
+@[irreducible] def constraints (Main : Vector (Fin KB) 48) : SP1ConstraintList :=


Is there a theorem for these constraints elsewhere? generally speaking it might be useful to make notes for each constraints file of where the corresponding correctness theorem is located.

No, I missed LoadX0 when doing the others. I will add that back and plan to gather all the chip_correct statements in a centralized file, making the current correctness statements into helper lemmas in each chip-specific file. I think that's probably the best way to make it easy to both make coverage clear to see and the proofs easy to look for.

alexanderlhicks · 2026-04-29T16:48:33Z

      let offset := (BitVec.signExtend 64 (sp1_imm_c Main)).toNat
-      reg_val + offset + 1 < 2^64) :
+      reg_val + offset + 1 < 2 ^ 64)
+    (h_below_clint :


Could you document assumptions like this? It shows up in several other places. Since this would be input dependent it's not immediately obvious this is realistic. Maybe it could be placed in SP1Foundations/Assumptions.lean if it stays as is?

This is actually strictly weaker than the already proven is_u48_sum found here, since SP1 has an even smaller memory region than we need for this. These should definitely be replaced with that, will work on the changes.

alexanderlhicks · 2026-04-29T17:04:51Z

-      let ram_size := (s.regs.get Register.plat_ram_size (hs _)).toNat
-      reg_val + offset + 2 ≤ ram_size)
+      reg_val + offset + 2 < 2 ^ 64)
    -- dt: This should eventually come from trusted instruction assumption


Any progress on this / reason this might be harder than expected? h_is_aligned shows up in other places.

See above comment on loadByte, this can come from the same place. Although it might be good to then add (s.regs.get Register.plat_ram_size (hs _)).toNat > 2^48, which would hopefully let us drop pma_check_machine axiom as constraints imply in memory if we assume that much ram size. Will also look at this.

alexanderlhicks · 2026-04-29T17:21:32Z

    (state_cstrs : (LoadByte.constraints Main).initialState s)
-    (h_is_lb : Main[46] = 1)
+    (h_is_lb : Main[45] = 1)
    (h_fits_in_mem :


Could this be derived from constraints? (also appears in other places iirc)

Constraints like these specifically are toggles because the same circuit handles multiple instructions. If this were zero you'd want it to behave like unsigned version so the theorem should fail then. There could I suppose be a combined lemma showing the circuit behavior as a whole. Across cases.

In a lot of the chips, there are specific predicates like is_sltu, is_divu, etc. that make this type of assumption look cleaner, but they are fundamentally the same sort of assumption

alexanderlhicks · 2026-04-29T17:32:11Z

Some general comments:
It would be good for the README.md to include
(i) The concrete list of instructions for which there are/aren't theorems, as far as I can tell there are none for FENCE, ECALL, EBREAK, which should be documented as these are due to SP1 implementation details.
(ii) A note on the TCB, including the spec, constraint extraction, axioms (and those of the RISC-V spec), non-trivial hypotheses, use of tactics that expand the tcb (native_decide is avoided I assume), assumptions about the lookups/permutation arguments (as outlined in SP1Foundations/Constraint.lean).
(iii) Pin or else make a note of when the proofs were last regenerated relative to a SP1 release or merge commit hash.

dtumad · 2026-06-08T00:11:44Z

Superceded by #97

dtumad and others added 30 commits February 17, 2026 18:23

Split off updates to mathlib and sail versions

d92865e

meta-programming fixes, grind fixes, dead constraints

ab63058

temp patch for leaky simp_all call

419ee1d

claude updates

f74d7a1

lay 4.29 foundation for merge

bf58f5c

merge divrem failure

4caa014

fix errors introduced with 1.29

55727ce

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

3183894

…sp1-lean into dtumad/milestone-3

close correct_subw: defer BitVec.ofNatLT_eq_ofNat until after PC rewrite

16b1294

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

temp store proof regression fixes

1fe9c53

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

28a17af

…sp1-lean into dtumad/milestone-3

more regression fixes

2b85251

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

9ff6975

…sp1-lean into dtumad/milestone-3

update riscv spec

b103467

more regression fixes

ebfc023

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

ed7c127

…sp1-lean into dtumad/milestone-3

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

d42e3b4

…sp1-lean into dtumad/milestone-3

isolate the build error in divrem regression

9fa7ebb

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

9992458

…sp1-lean into dtumad/milestone-3

regressions in sailM

134ea21

regressions in branch chip

79e145f

regressions in jal

79891c1

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

3715a70

…sp1-lean into dtumad/milestone-3

regressions in jal

65fa26e

Merge branch 'dtumad/milestone-3' of https://github.com/succinctlabs/…

f60d81a

…sp1-lean into dtumad/milestone-3

isolate memcheck regression

9d668ab

some mild performance wins

27a52d0

dtumad added 18 commits April 24, 2026 15:58

Updated extraction without is_trusted and some opcode changes

e686807

solve regressions from extraction

3322146

update claude tracking

a371da4

load regressions

f28d65f

Fix more of the regression from is_trusted

6de007b

resolve even more regressions from is_trusted change

1526474

resolving more regressions

af299c9

regressions in branch chip and start jalr fix

c9a458c

Merge branch 'dtumad/update-constraints-is-trusted' of https://github…

0d53931

….com/succinctlabs/sp1-lean into dtumad/update-constraints-is-trusted

Almost all regressions cleared

9ee7d76

regressions in branch chip

2aa8f41

update jal and jalr chip regressions / vulnerability disclosure fixes

f2f5ccd

remove dead maxHeartBeats after fixing all errors

4606ad4

remove some assumptions and axioms after all the updates

899d1c3

build errors from structural config pattern matches

b3995e8

clean build

944595b

Utype cases

f246510

close imm masking assumption with claude helper

c6d1be7

dtumad changed the title ~~feat: Updates to foundations, improved ergonomics, and audit gap resolutions~~ feat: Updates to foundations, and audit gap resolutions, and improved ergonomics Apr 25, 2026

dtumad added 2 commits April 25, 2026 15:14

lingering agent plan file

12bf78c

agent audit of changes

7c76907

dtumad requested a review from alexanderlhicks April 25, 2026 21:12

Removing unneeded linter exceptions

4a18c95

alexanderlhicks reviewed Apr 29, 2026

View reviewed changes

pin a specific RV64D extraction commit

baf1e9a

dtumad mentioned this pull request Apr 30, 2026

feat: Generalize constraints and proofs over general primes and fields #94

Closed

dtumad closed this Jun 8, 2026

Uh oh!

Conversation

dtumad commented Apr 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Updates to Dependencies

Audit Gaps

Assumption Changes

General Changes

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alexanderlhicks commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dtumad commented Jun 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

dtumad commented Apr 25, 2026 •

edited

Loading

alexanderlhicks commented Apr 29, 2026 •

edited

Loading