Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory, stack depth enforcement#2
Open
Semantic theorems, proof quality, emit events, bounded stack, word-addressed memory, stack depth enforcement#2
Conversation
tob-joe
force-pushed
the
semantics-comparison-tests
branch
from
854981d to
e9489d2
Compare
tob-joe
changed the title
tob-joe
changed the title
tob-joe
changed the title
tob-joe
changed the title
- New Proofs/Interp.lean: toU64, toU128 interpretation functions and bridge lemmas (toU64_eq_iff, toU64_lt_iff, toU128_lt_iff) - Fix U64WideningMul.lean: remove redundant miden_bind after miden_dup/swap/movup (simp no-progress after Lean update) - Fix WordGt.lean: replace failing simp with congr + Bool.and_comm - Rewrite U64MinMax.lean: replace broken manual stepMovup calls with miden_movup tactics; fix theorem RHS argument order to match actual computation (gt/lt run on rearranged stack) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- u64_lt_semantic: proves result = decide(toU64 a < toU64 b) - u64_gt_semantic: proves result = decide(toU64 b < toU64 a) - u64_lte_semantic: proves result = decide(not(toU64 b < toU64 a)) - u64_gte_semantic: proves result = decide(not(toU64 a < toU64 b)) - u64_eq_semantic: proves result = decide(toU64 a = toU64 b) - Bridge lemmas in Interp.lean: - u32OverflowingSub_snd_eq_zero_iff: .2 == 0 iff a = b - u64_lt_condition_eq: borrow pattern = decide(toU64 < toU64) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Word proofs: reverse, eq, eqz, testz, test_eq, arrange, gt (full proof), lt/lte/gte (axiom-backed, to be proved) - StepLemmas: added step lemmas for dupw, cdrop, cswap, reversew with isU32 hypothesis support - Helpers: added Felt boolean lemmas, u32OverflowingSub borrow lemma, Felt.ofNat recovery, isU32 propagation - Tactics: miden_step auto-tactic with isU32 via assumption - CLAUDE.md: memory-limited lake build instructions - COMPARISON.md: updated with bug fixes and modeling notes Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…icates - Fix Miden.Core.Math.U64 -> Miden.Core.U64 in semantic corollaries - Restore Proofs/U64.lean and Proofs/Word.lean (deleted upstream but still imported by other upstream files) - Remove flat proof files superseded by upstream's U64/ and Word/ directory restructuring - Add Interp import to MidenLean.lean Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Runs `lake build MidenLean` and verifies no `sorry` in source files on push to main and on PRs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace manual elan install + cache setup with the standard leanprover/lean-action@v1 which handles elan, Mathlib cache, lake build, and .lake caching automatically. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Add step lemmas: stepDiv (field division), rename stepReverseW to stepReversew for naming consistency - Add tactics: miden_setup, miden_setup_env, miden_call for proof setup; add stepDupw/stepDiv/stepCdropIte/stepCswapIte to miden_step - Add equation lemmas: execInstruction_u32OverflowSub/WrappingSub/ WidenMul/WidenMadd, execU32WidenMul_concrete, execU32WidenMadd_concrete - Fix Shr.lean: hbnz -> hbz argument name, bridge beq/ne type mismatch - Fix Rotl.lean: replace manual execU32OverflowSub unfold with step lemma - Fix Rotr.lean: replace manual execU32WrappingSub unfold with step lemma - Fix Shl.lean: remove redundant dsimp after miden_setup_env - Exclude incomplete Divmod/Div/Mod from build (contain sorry) - Fix all lint warnings: unused simp args in U64, WideningAdd, Clz, Ctz, Clo, Cto, Helpers; unused variables in Interp; unused omega in Helpers Build: 0 errors, 0 warnings, 0 sorry in imported files. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Documents general Lean 4 proof guidance: goal inspection via MCP, no-sorry invariant, lint discipline, step lemma architecture, proof setup macros, chunked proof pattern, macro hygiene, and generated scaffolding isolation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Complete the 50-instruction u64.divmod correctness proof, verifying that advice-provided quotient and remainder satisfy the division identity a = b * q + r with r < b. Infrastructure: - Add step lemmas: stepEmitImm, stepAdvPush2, stepAssert, stepAssertWithError, stepAssertEq, stepAssertEqWithError - Add equation lemmas: execInstruction_advPush, execInstruction_emitImm - Add new step lemmas to miden_step tactic The proof steps through all 50 instructions including the exec "lt" sub-procedure call, discharging assertion obligations from the theorem hypotheses. Div.lean and Mod.lean (already complete) call u64_divmod_correct and are now re-imported into the build. Build: 0 errors, 0 warnings, 0 sorry. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The theorem had the advice tape in the wrong order (q_lo::q_hi::r_lo::r_hi) when the Miden VM handler actually pushes [q_hi, q_lo, r_hi, r_lo] onto the advice stack. Since advPush.2 reverses pairs, the correct hypothesis is q_hi::q_lo::r_hi::r_lo, producing standard LE layout on the operand stack. This required rewriting all cross-product hypotheses to match the actual MASM computation: - p1 = b_lo * q_lo (was b_lo * q_hi) - p2 = b_hi * q_lo + p1_hi (was b_hi * q_hi + cross0_hi) - p3 = b_lo * q_hi + p2_lo (was b_lo * q_lo + madd1_lo) - assert b_hi * q_hi == 0 (was b_hi * q_lo == 0) Output stack corrected to r_lo::r_hi::q_lo::q_hi (standard LE). Div.lean and Mod.lean updated to match the new signature. Verified against miden-vm source: u64.masm lines 367-511 and u64_div.rs handler. Build: 0 errors, 0 warnings, 0 sorry. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Semantics reference mapping: - Add inline comments to each handler section citing the miden-vm Rust source file and line range (processor/src/execution/operations/) - Document which instructions are native VM ops vs compiled from assembly (sub->neg+add, div->inv+mul, u32or, xor, etc.) - Add detailed advPush documentation with concrete reversal example explaining why vals.reverse is correct (N consecutive ADVPOP ops) Test gap investigation (AC-4): - The existing advPush test at line ~771 correctly tests reversal - The divmod bug was in the THEOREM HYPOTHESIS (wrong advice tape ordering), not in Semantics.lean -- no unit test could catch it - Root cause: theorem author assumed advPush doesn't reverse New tests (15+ additional): - advPush.1/2/4 reversal tests with distinct values - Two-stage advPush.2+advPush.2 simulating divmod's pattern - Order-sensitive regression tests: sub, u32OverflowSub, u32WidenMul, u32WidenMadd, movup, movdn - End-to-end divmod smoke tests on concrete inputs (10/3, 100/7) that execute the full 50-instruction procedure Build: 0 errors, 0 warnings, 0 sorry. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add tests for 43 previously untested instructions: - Assertions: assertWithError, assertzWithError, assertEqWithError, assertEqw - Stack: nop, dupw, swapw, movupw, movdnw, cdropw, pushList - Arithmetic: addImm, subImm, mulImm, divImm, eqImm, neqImm - U32: u32Assert2, u32AssertW, u32TestW, u32WrappingSub, u32WrappingMul, u32WrappingMadd, u32OverflowAdd3, u32WrappingAdd3, u32Mod, u32Gte, u32ShlImm, u32ShrImm, u32Rotl, u32RotlImm, u32Rotr, u32RotrImm - Memory: memLoadImm, memStoreImm, memStorewLe, memLoadwLe, memStorewBe, memLoadwBe, memStorewLeImm, memLoadwLeImm, memStorewBeImm, memLoadwBeImm - IO: emit, emitImm, exec (with ProcEnv) Every instruction constructor in Instruction.lean now has at least one #eval test verifying its happy-path behavior. Build: 0 errors, 0 warnings, 0 sorry. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add Tier 6 cross-validation tests that reproduce exact test vectors from miden-vm/crates/lib/core/tests/math/u64_mod.rs and run the same MASM procedures through our Lean execWithEnv model. Covered u64 procedures with miden-vm test vectors: - wrapping_add: a=0x200000005, b=0x100000003 -> [8,3] - lt/lte/gt/gte: 3 concrete cases each (0v0, 0v1, 1v0) - min/max: 3 cases each (0v0, 1v2, 3v2) - eq/neq/eqz: 2-3 cases each - divmod: 123/10 = q12 r3 (advice tape ordering validated) - clz/ctz/clo/cto: boundary cases (0 and all-ones) - shl: 1<<32 across limb boundary - shr: 0x100000001>>1 across limb boundary Added testU64ProcEnv with all u64 procedures for test execution. These tests would have caught the divmod advPush ordering bug: the concrete divmod test (123/10) validates the full advice-tape-to- output pipeline against the miden-vm expected result. Build: 0 errors, 0 warnings, 0 sorry. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add 6 semantic theorems proving u64 procedures compute the correct mathematical operations on interpreted 64-bit values: - u64_neq_semantic: output = decide(toU64 a != toU64 b) - u64_and/or/xor_toU64: output limbs encode toU64 a op toU64 b - u64_min/max_semantic: comparison uses toU64 a < toU64 b Bridge infrastructure in Interp.lean: - toU64_neq_iff, toU64_testBit decomposition - toU64_and/or/xor via Nat.eq_of_testBit_eq extensionality - felt_ofNat_val, isU32_lt, felt_ofNat_isU32 helpers Also hardened CLAUDE.md with mandatory systemd-run memory cap for all lake build commands (prior session OOM'd the machine). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…g_add Add 3 more semantic theorems: - u64_wrapping_sub_semantic: result = (toU64 a + 2^64 - toU64 b) % 2^64 - u64_overflowing_sub_semantic: borrow = decide(toU64 a < toU64 b), result = wrapping subtraction (same as wrapping_sub) - u64_widening_add_semantic: overflow * 2^64 + hi * 2^32 + lo = toU64 a + toU64 b (exact, no truncation) All proved by omega after unfolding u32OverflowingSub/toU64. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Fix Bad finding: unify u32CountLeadingOnes to use XOR (^^^) instead of arithmetic subtraction, matching u32CountTrailingOnes. Updated stepU32Clo and u64_clo_correct accordingly. Semantic theorems added: - u64_wrapping_sub_semantic: (toU64 a + 2^64 - toU64 b) % 2^64 - u64_overflowing_sub_semantic: borrow + wrapping result - u64_widening_add_semantic: exact sum via omega Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
18 unchecked ACs remain. All arithmetic/shift/rotation semantic theorems (7 ACs) are blocked on the same infrastructure gap: a bridge lemma proving that the u32 cross-product carry chain computes the low 64 bits of the u64-level operation. Omega cannot prove this (nonlinear floor-division terms). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Procedure-level tests (divmod smoke, cross-validation) moved from Tests/Semantics.lean to Tests/CrossValidation.lean to avoid OOM during parallel compilation. CrossValidation.lean is not imported by the main build; run with lake build MidenLean.Tests.CrossValidation. Also add galvanize spec and vivisect working artifacts from the current analysis session. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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>
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>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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>
- 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>
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>
All 19 procedure proofs complete, build passes within 10G, soundness docs added, modeling divergences deferred (AC-27-31) for next session. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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>
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
force-pushed
the
semantics-comparison-tests
branch
from
545db0c to
fdd3ae1
Compare
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>
- 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>
…emmas 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>
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>
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>
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>
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>
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>
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>
48/51 ACs complete. Remaining: AC-43 (bounded stack), AC-44 (word-addressed memory). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
tob-joe
changed the title
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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>
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
changed the title
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>
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
changed the title
Vivisect run 12 (full mode): 0 Broken, 0 Absurd, 1 Bad (intentional stack depth). 51/51 ACs complete. Memory model Bad finding resolved by word-addressed refactor. Spec text updated to reflect current state. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
AC-50: overflow/underflow guards in handlers AC-51: wellFormed hypotheses in step lemmas AC-52: update all proofs AC-53: stack depth edge case tests Checkpoint before starting implementation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
changed the title
…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>
COMPARISON.md went stale across three major changes (word-addressed memory, emit events, stack depth) without being caught. Add an ongoing AC to verify it after any semantic model change. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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,toU128interpretation functions with bridge lemmasProof quality (Tier 9)
maxHeartbeatsannotations via O(1) equation lemma dispatchModeling improvements (Tier 10)
Stack depth enforcement (Tier 11)
hlen : rest.length + 30 <= MAX_STACK_DEPTHBuild status
Test plan
lake build MidenLeanpasses (1913 jobs, 0 errors)Generated with Claude Code