Skip to content

Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory, stack depth enforcement#2

Open
tob-joe wants to merge 67 commits intomainfrom
semantics-comparison-tests
Open

Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory, stack depth enforcement#2
tob-joe wants to merge 67 commits intomainfrom
semantics-comparison-tests

Conversation

@tob-joe
Copy link
Contributor

@tob-joe tob-joe commented Mar 18, 2026 •
edited
Loading

Summary

Complete formal verification infrastructure for Miden VM core library procedures, building on the existing 23 proofs (u64 + word modules).

What's new in this PR

Semantic interpretation layer (Tiers 5-8)

  • toU64, toU128 interpretation functions with bridge lemmas
  • 29 semantic theorems proving u64 procedures compute the correct mathematical operations (comparison, arithmetic, bitwise, shifts, counting, divmod)

Proof quality (Tier 9)

  • Removed 98 maxHeartbeats annotations via O(1) equation lemma dispatch
  • Split slow proofs into symbolic sub-lemmas

Modeling improvements (Tier 10)

  • Emit/emitImm now record event IDs in state (72+ files updated)
  • Bounded stack model: min depth 16, max depth 2^16
  • Word type + accessors for word-addressed memory
  • Full word-addressed memory refactor (Nat -> Word matching Rust BTreeMap<u32, [Felt; 4]>)

Stack depth enforcement (Tier 11)

  • 11 instruction handlers check for stack overflow (return none when depth would exceed MAX_STACK_DEPTH)
  • Step lemmas carry overflow hypotheses
  • 30+ proof files carry hlen : rest.length + 30 <= MAX_STACK_DEPTH
  • 8 edge case tests for overflow/underflow boundary behavior

Build status

  • 1913 jobs, 0 errors, 0 warnings, 0 sorry
  • Vivisect: 18 Good, 0 Bad, 0 Broken, 0 Absurd
  • 55/55 acceptance criteria met across 13 galvanize iterations

Test plan

  • lake build MidenLean passes (1913 jobs, 0 errors)
  • Zero sorry outside Generated/
  • Tests/Semantics.lean: 100+ instruction tests + 8 stack depth edge cases
  • Tests/CrossValidation.lean: cross-validation against miden-vm reference vectors
  • CI workflow (lean.yml) passes on push

Generated with Claude Code

@tob-joe tob-joe force-pushed the semantics-comparison-tests branch from 854981d to e9489d2 Compare March 18, 2026 22:31
@tob-joe tob-joe changed the title Semantics tests, bug fixes, and semantic proof strengthening Semantic interpretation layer and non-trivial proof corollaries Mar 18, 2026
@tob-joe tob-joe changed the title Semantic interpretation layer and non-trivial proof corollaries Semantic proof layer, CI, and build fixes Mar 18, 2026
@tob-joe tob-joe changed the title Semantic proof layer, CI, and build fixes Semantic proof layer, proof infrastructure, CI, and build fixes Mar 19, 2026
tob-joe and others added 7 commits March 19, 2026 11:03
@tob-joe @claude
cross-product carry chain bridge lemma
0d3a3b6 
Prove cross_product_mod_2_64: the u32 carry chain
(prod_lo, cross1, cross2) correctly computes the low 64 bits
of the full product. This is the key infrastructure gap that
was blocking wrapping_mul, shl, shr, rotl, rotr semantics.

Proof technique: manual decomposition via Nat.div_add_mod at
each carry level, reducing to omega at each step. The lemma
holds for all Nat (no u32 bound hypotheses needed).

Used immediately to prove u64_wrapping_mul_semantic as a
one-line application.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
shl semantic + felt_lo32_hi32_toU64 bridge
4736928 
Add u64_shl_semantic: output = (toU64 lo hi * 2^shift) % 2^64.
Proof uses cross_product_mod_2_64 + felt_lo32_hi32_toU64 (new
bridge lemma showing lo32/hi32 split-and-rejoin is identity).

The same pattern works for shr, rotl, rotr (future ACs).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
counting defs + clz/ctz semantic theorems
116af71 
Add u64-level counting function definitions to Interp.lean:
- u64CountLeadingZeros, u64CountTrailingZeros
- u64CountLeadingOnes, u64CountTrailingOnes

Prove u64_clz_semantic and u64_ctz_semantic showing the
_correct output matches the u64-level definitions.

Clo/cto semantic theorems deferred (ZMod/Bool conversion
complexity with 0xFFFFFFFF sentinel value).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
store_word proof, fix OOM builds, doc update
42ec770 
- Prove word.store_word_u32s_le correct (AC-5): add
  stepMemStorewLe step lemma and equation lemma
- Fix WideningMul/Rotl/Rotr OOMs by splitting proofs
  via exec_append and extracting isU32 helpers
- Add Rotl missing hhi hypothesis and carry isU32
- Update COMPARISON.md with divmod emitImm/advPush
  host interaction documentation

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
soundness docs for modeling divergences
06b521e 
Add "Soundness for proven theorems" sections to S-1
(unbounded stack), S-2 (element memory), and S-4
(emit no-op) in COMPARISON.md explaining why each
simplification is sound for the proven theorems.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
CI: exclude Proofs/Generated/ from sorry check
e09b16e 
Generated scaffolds contain sorry by design and are
not imported into the build.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
Fix post-rebase: remove old Proofs/U64.lean, update imports
ae5a1c8 
Remove MidenLean.Proofs.U64 and MidenLean.Proofs.Word (old
monolithic files) that conflict with upstream's per-module
Common.lean. Update all imports to use U64.Common.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe tob-joe force-pushed the semantics-comparison-tests branch from 545db0c to fdd3ae1 Compare March 19, 2026 15:10
tob-joe and others added 9 commits March 19, 2026 12:32
@tob-joe @claude
8 semantic theorems + bridge lemmas
a22979b 
Semantic theorems added:
- u64_eqz_semantic: eqz = decide(toU64 = 0)
- u64_wrapping_add_semantic: carry chain = (a+b)%2^64
- u64_widening_mul_semantic: 4-limb carry = toU64*toU64
  as toU128 via widening_mul_carry_chain bridge
- u64_divmod_semantic: operational hypotheses imply
  toU64 a = toU64 b * toU64 q + toU64 r, r < b
  (split into divmod_carry_chain + divmod_lt_bridge +
  divmod_eq_bridge sub-lemmas)
- u64_clo_semantic: XOR bridge to u64CountLeadingOnes
- u64_cto_semantic: XOR bridge to u64CountTrailingOnes

Bridge infrastructure (Interp.lean):
- widening_mul_carry_chain: 128-bit carry chain identity
- divmod_carry_chain: division verification identity
- shr_hi_only: shift>=32 reduces to hi/2^(shift-32)
- shr_lo_decomp: shift<32 decomposition identity
- felt_pow2_inv_mul: 2^32*(2^s)^(-1) = 2^(32-s) in field

Also fixed lint warnings in WideningMul, Rotl, Rotr.
43/49 ACs complete, build clean (0 warnings, 0 errors).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
shr/rotl/rotr semantic theorems
d42af81 
- u64_shr_semantic: proves output = toU64 lo hi / 2^shift
  via case split on shift >= 32 (shr_hi_only) vs < 32
  (shr_lo_decomp)
- u64_rotl_product/semantic: proves cross-product = toU64 * 2^eff
  via nlinarith + Nat.div_add_mod
- u64_rotr_product/semantic: same identity for right rotation
  with documented Felt overflow edge case for shift=0

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
equation lemmas eliminate maxHeartbeats from StepLemmas
f8a493b 
Add EquationLemmas.lean with O(1) dispatch lemmas for all ~100
instructions. Each reduces execInstruction s .foo = execFoo s via
rfl, avoiding the O(n) cost of unfolding the full pattern match.

StepLemmas.lean: all 45 set_option maxHeartbeats annotations removed.
Proofs now use simp only [execInstruction_foo] + unfold execFoo
instead of unfold execInstruction execFoo.

Helpers.lean: remove @[simp] from equation lemmas to prevent eager
rewriting that breaks downstream proofs.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
remove maxHeartbeats from all non-generated files
c01281f 
Remove all set_option maxHeartbeats annotations from non-generated
proof files (~98 annotations). Retain only Felt.lean:12 (native_decide
for primality requires extra heartbeats).

All U64 proofs build without maxHeartbeats. Some U128 proofs
(Gt, Max, WrappingMul, OverflowingMul) and Word.Eqz have
pre-existing build failures (undefined stepSwapw1/stepDupw1/
stepU32WrappingMadd, missing @[miden_dispatch] import, unknown
miden_loop tactic) that predate this change and were masked by
stale .olean caches.

Also adds missing SimpAttrs import to U128.OverflowingMul.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
events field added to MidenState
fc8254a 
Work-in-progress: adds events : List Felt to MidenState and updates
execEmit to record event IDs. Many proof files updated but some still
have incomplete evts parameter threading.

NOT YET COMPLETE - do not merge this commit standalone.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
more events field threading
1303a8a 
WIP: continued threading evts parameter through proof files.
Most U64 proofs pass (23/31). Remaining: OverflowingAdd,
WideningMul, Divmod, Div, Mod, Rotl, Rotr need manual
call-site fixes.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
events field - all U64 proofs pass
f76350d 
All 31 U64 proof modules now build with the events field.
Key changes: divmod/div/mod correctly track emitted event ID
(14153021663962350784) in output state. Word proofs partially
fixed (Gt iteration call site, StoreWordU32sLe congr).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
events field - Word proofs fixed
ba21884 
All U64 (31/31) and Word (10/11, excluding pre-existing
Word.Eqz miden_loop issue) proofs pass with events field.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
AC-45 complete -- events field in MidenState
0d66cea 
Adds events : List Felt field to MidenState. execEmit now records
the top stack element as event ID. emitImm records its argument.

Changes across 72+ files:
- State.lean: events field with default []
- Semantics.lean: execEmit reads top, emitImm records eventId
- EquationLemmas.lean: updated emitImm equation lemma
- StepLemmas.lean: all step lemmas take evts parameter
- Helpers.lean: equation lemma evts threading
- All U64/Word proof files: evts parameter threading
- Divmod/Div/Mod: output tracks emitted event ID

Build: EXIT 0, 0 errors, 0 warnings, 0 sorry.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe tob-joe changed the title Semantic interpretation layer, cross-validation, and CI Semantic theorems, proof optimizations, and emit event modeling Mar 19, 2026
tob-joe and others added 2 commits March 19, 2026 14:30
@tob-joe @claude
AC-43 bounded stack model
bc90018 
Add MIN_STACK_DEPTH (16), MAX_STACK_DEPTH (2^16), padStack function,
wellFormed predicate, and ofStackPadded constructor to MidenState.
These model the Rust VM's stack depth bounds without breaking
existing proofs (purely additive definitions).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
AC-49 Word type + accessors, split AC-44
72ddf55 
Add Word type (Felt x Felt x Felt x Felt), Word.zero/get/set/toList,
readWord/writeWord accessors on element-addressed memory, and
zeroWordMemory. These provide word-addressed capability without
breaking existing element-addressed proofs.

Split AC-44: AC-49 (achievable infrastructure) is done. The full
memory model refactor (Nat -> Felt to Nat -> Word) is deferred as
it requires rewriting all memory handlers and their proofs.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe tob-joe changed the title Semantic theorems, proof optimizations, and emit event modeling Semantic theorems, proof optimizations, emit events, and bounded stack Mar 19, 2026
tob-joe and others added 2 commits March 19, 2026 14:51
@tob-joe @claude
converged -- lint fix
60cdf13 
Iteration 11: removed dead tactic in StoreWordU32sLe.lean,
corrected assert semantics in spec. Vivisect: 0 Broken,
0 Absurd, 2 Bad (intentional). 50/51 ACs complete.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe @claude
AC-44 word-addressed memory model
ea6302c 
Refactor memory from Nat -> Felt (element-addressed) to
Nat -> Word (word-addressed) matching the Rust VM's
BTreeMap<u32, [Felt; 4]>. mem_load/mem_store access
element 0 of the word; mem_loadw/mem_storew access the
full word. Alignment checks removed from word ops.
27 files changed, 0 errors, 0 warnings, 0 sorry.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe tob-joe changed the title Semantic theorems, proof optimizations, emit events, and bounded stack Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory Mar 19, 2026
@tob-joe @claude
AC-50-53 per-instruction stack depth enforcement
c2a8582 
Add overflow guards to 11 instruction handlers that increase stack
depth (execPadw, execPush, execPushList, execDup, execDupw,
execU32Test, execU32TestW, execU32Split, execMemLoadImm, execLocLoad,
execAdvPush). Each returns none when s.stack.length + N >
MAX_STACK_DEPTH.

Update 5 step lemmas with hov overflow hypotheses. Update miden_step
tactic to discharge via simp [List.length_cons]; omega. Update 30+
proof files with hlen : rest.length + 30 <= MAX_STACK_DEPTH.

Add 8 edge case tests (push/dup/padw/advPush/u32Split on full stack,
drop on empty stack).

Fix pre-existing ha_align bug in Tactics.lean and stale -j 2 flag in
CLAUDE.md/guidelines.md (Lake 5.0.0 does not support -j).

Vivisect run 14: 18 Good, 0 Bad, 0 Broken, 0 Absurd. Build: 1913
jobs, 0 errors, 0 warnings, 0 sorry.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe tob-joe changed the title Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory, stack depth enforcement Mar 19, 2026
@tob-joe @claude
docs: update COMPARISON.md for word-addressed memory, emit events, st…
156637b 
…ack depth

S-1 rewritten: stack depth now enforced via overflow guards (11 handlers)
S-2 updated: memory model is now word-addressed (Nat -> Word), matching Rust
S-4 updated: emit/emitImm now record event IDs in state.events field
Test table: added stack depth edge case row (8 tests)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@tob-joe tob-joe force-pushed the semantics-comparison-tests branch 3 times, most recently from 5a1ebc4 to 156637b Compare March 23, 2026 08:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@tob-joe @fegge