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

.github/workflows/lean.yml

@@ -0,0 +1,24 @@
+name: Lean Build
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-mathlib-cache: true
+
+      - name: Check no sorry
+        run: |
+          if grep -rn 'sorry' MidenLean/ --include='*.lean' | grep -v '\.lake' | grep -v 'Proofs/Generated/' | grep -v -- '--.*sorry'; then
+            echo "Found sorry in source files"
+            exit 1
+          fi

AGENTS.md

@@ -0,0 +1,98 @@
+# CLAUDE.md
+
+Formal verification of Miden Assembly (MASM) core library procedures in Lean 4. See [ARCHITECTURE.md](ARCHITECTURE.md) for design decisions and repository layout.
+
+## Build
+
+```bash
+lake build            # full build (includes Mathlib — slow first time)
+lake build MidenLean  # just the Lean library and proofs
+```
+
+Lean 4 v4.28.0 via elan. A clean build with zero `sorry` means all theorems are machine-checked.
+
+## Key conventions
+
+- **Lean 4 / Mathlib naming**: lowerCamelCase for defs and theorems, UpperCamelCase for types and namespaces.
+- **Dispatch architecture** (`Semantics.lean`): `execInstruction` dispatches each instruction to a dedicated handler (`execDrop`, `execDup`, `execSwap`, `execMovup`, etc.). `execWithEnv` executes `List Op` with a `ProcEnv` for procedure calls.
+- **Step lemmas** (`StepLemmas.lean`): parametric where possible (`stepDup`, `stepSwap`), with explicit range hypotheses for `movup`/`movdn`. Proved by `unfold execInstruction execFoo; rfl` or `simp`.
+- **Proof pattern**: destructure state, unfold procedure, rewrite to monadic `do`-form, step through with exact `rw [stepFoo]`, structural tactics (`miden_swap`, `miden_dup`, `miden_movup`, `miden_movdn`), and `miden_bind`. Use `miden_step` mainly for short residual steps, not as the default for long proofs. See `MidenLean/Proofs/U64/Min.lean`, `MidenLean/Proofs/U64/Max.lean`, and `MidenLean/Proofs/U64/Shr.lean`.
+- **Correctness theorems**: named `<procedure>_correct` in snake_case matching the MASM name (e.g., `u64_wrapping_sub_correct`).
+- **Theorem descriptions for README generation**: place a doc comment immediately above the main `*_correct` theorem with no intervening text other than whitespace. The first sentence should be a short high-level English summary of what the procedure proves, and it should be at least a few words long. The README table generator uses this doc comment directly, so avoid leaving only placeholder text. If you include extra lines like `Input stack:` or `Output stack:`, put the high-level summary first.
+- **Generated code** (`MidenLean/Generated/`): produced by the Rust translator. Do not edit by hand.
+- **Generated proof scaffolding** (`MidenLean/Proofs/Generated/`): produced by `masm-to-lean`. Do not edit by hand; copy the relevant scaffold into the manual proof file and complete it there.
+
+## Proof Workflow
+
+The expected workflow for a new or updated proof is:
+
+1. Regenerate the translated Lean code and proof scaffolding from the MASM source under `path-to/miden-vm/crates/lib/core/asm`.
+
+```bash
+timeout 180s cargo run --manifest-path masm-to-lean/Cargo.toml -- \
+  path/to/miden-vm/crates/lib/core/asm/math/u64.masm \
+  -o MidenLean/Generated \
+  --namespace Miden.Core \
+  --generate-proofs \
+  --proofs-output MidenLean/Proofs/Generated
+```
+
+2. Find the generated scaffold for the procedure you want to prove.
+
+- Translated procedure definitions live in `MidenLean/Generated/<Module>.lean`.
+- Generated proof scaffolds are split per procedure:
+  - `MidenLean/Proofs/Generated/<Module>/Common.lean`
+  - `MidenLean/Proofs/Generated/<Module>/<Proc>.lean`
+- The top-level `MidenLean/Proofs/Generated/<Module>.lean` file is only a lightweight index.
+
+3. Copy the generated scaffold into the manual proof file under `MidenLean/Proofs/...`.
+
+- Example: copy `MidenLean/Proofs/Generated/U64/Shr.lean` into `MidenLean/Proofs/U64/Shr.lean` and then edit the manual file.
+- Keep the generated file untouched so it can be regenerated freely.
+
+4. Complete the proof in the manual file.
+
+- For short straight-line procedures, keep the scaffold mostly flat and explicit.
+- For longer procedures with expensive ops like `pow2`, `u32DivMod`, `u32OverflowSub`, `div`, or `cswap`, split the proof into semantic chunks.
+- Prefer exact step rewrites and structural tactics over repeated `miden_step`.
+- Add helper lemmas only for real side conditions such as `isU32`, nonzero divisors, boolean normalization, or small arithmetic identities.
+- Remove helper lemmas that are no longer used.
+- Before finishing the file, replace the scaffold's placeholder theorem comment with a real high-level correctness description for the main `*_correct` theorem. Keep that doc comment directly attached to the theorem so `scripts/generate_verified_tables.py` can extract it.
+
+5. Validate with targeted Lean checks before broader builds.
+
+```bash
+timeout 180s lake env lean MidenLean/Proofs/U64/Shr.lean
+timeout 180s lake build MidenLean.Proofs.U64.Shr
+```
+
+Use the smallest relevant target first. Only run broader builds when the local proof checks.
+
+6. Regenerate the verified-procedures tables and update `README.md`.
+
+```bash
+python3 scripts/generate_verified_tables.py > /tmp/verified_tables.md
+```
+
+- The script builds each manual proof module componentwise, with strict per-module `timeout 180s lake build` checks.
+- It writes progress messages to stderr such as `starting proof ...` and `proof ... completed`.
+- Fix any emitted warnings before updating the README.
+- Replace the verified-procedures section in `README.md` with the generated markdown if it changed.
+
+## Scaffolding Expectations
+
+- Generated scaffolds are a starting point, not a finished proof.
+- `FlatAuto` and `FlatExplicit` scaffolds should contain useful setup and step structure for simpler procedures.
+- `Chunked` scaffolds are intentionally more skeletal. They should guide chunk boundaries and composition, but the final manual proof usually needs named intermediate values and local helper lemmas.
+- When looking for examples:
+  - use `Min` and `Max` as the reference shape for short proofs
+  - use `Shr` as the reference shape for chunked straight-line proofs
+
+## Development Workflow
+
+- Do not commit without explicit permission.
+- Do not use git worktrees or branches unless asked.
+- Always run Lean checks and `lake build` with strict timeouts. Default to 3-5 minutes. Otherwise you risk getting stuck or causing the entire system to run out of memory.
+- Prefer targeted proof checks such as `timeout 180s lake build MidenLean.Proofs.U64.Shr` over whole-project builds while iterating.
+- When writing new proofs, follow the existing pattern in the closest existing proof file.
+- After completing or updating manual proofs, rerun `scripts/generate_verified_tables.py` and keep the README proof tables in sync with the checked proofs.

ARCHITECTURE.md

@@ -14,45 +14,20 @@ The project has two components:
 ```
 ├── MidenLean.lean                  Root import file
 ├── MidenLean/
-│   ├── Felt.lean                   Goldilocks field (ZMod (2^64 - 2^32 + 1))
-│   ├── State.lean                  VM state: stack, memory, locals, advice
-│   ├── Instruction.lean            Inductive type for ~130 MASM instructions
-│   ├── Op.lean                     Control flow: ifElse, repeat, whileTrue
-│   ├── Semantics.lean              exec* handlers, execInstruction dispatch, execWithEnv, exec
-│   ├── Generated/
-│   │   ├── Word.lean               11 word procedures as List Op
-│   │   └── U64.lean                31 u64 procedures as List Op
+│   ├── Felt.lean                   Goldilocks field implementation
+│   ├── State.lean                  Miden VM state definition
+│   ├── Instruction.lean            Inductive type with ~130 MASM instructions
+│   ├── Op.lean                     Control flow and procedure call operations
+│   ├── Semantics.lean              Executable semantics for MASM instructions and procedures
+│   ├── Generated/                  Auto-generated MASM procedure definitions (do not edit)
 │   └── Proofs/
-│       ├── Helpers.lean            MidenState simp lemmas and Felt bounds lemmas
+│       ├── Helpers.lean            Reusable helper lemmas for state projections and boolean normalization
+│       ├── SimpAttrs.lean          `@[simp]` attributes for helper lemmas
 │       ├── StepLemmas.lean         Reusable single-instruction lemmas
-│       ├── Tactics.lean            miden_step / miden_steps tactic macros
-│       ├── Word.lean               word::eqz proof
-│       ├── WordTestz.lean          word::testz proof
-│       ├── U64.lean                u64::eqz, overflowing_add, wrapping_add proofs
-│       ├── U64Sub.lean             u64::wrapping_sub proof
-│       ├── U64OverflowingSub.lean  u64::overflowing_sub proof
-│       ├── U64WideningAdd.lean     u64::widening_add proof
-│       ├── U64WrappingMul.lean     u64::wrapping_mul proof
-│       ├── U64Eq.lean              u64::eq proof
-│       ├── U64Neq.lean             u64::neq proof
-│       ├── U64Lt.lean              u64::lt proof
-│       ├── U64Gt.lean              u64::gt proof
-│       ├── U64Lte.lean             u64::lte proof
-│       ├── U64Gte.lean             u64::gte proof
-│       ├── U64And.lean             u64::and proof
-│       ├── U64Or.lean              u64::or proof
-│       ├── U64Xor.lean             u64::xor proof
-│       ├── U64Clz.lean             u64::clz proof
-│       ├── U64Ctz.lean             u64::ctz proof
-│       ├── U64Clo.lean             u64::clo proof
-│       ├── U64Cto.lean             u64::cto proof
-│       └── U64U32Assert4.lean      u64::u32assert4 proof
-├── masm-to-lean/                   Rust translator
-│   └── src/
-│       ├── main.rs                 CLI entry point
-│       ├── translate.rs            AST → Lean code generation
-│       ├── instruction.rs          Instruction → Lean constructor mapping
-│       └── module.rs               Module/procedure → namespace/def
+│       ├── Tactics.lean            Reusable proof tactics
+│       ├── Generated/              Auto-generated proof scaffolding (do not edit)
+│       └── ...                     Per-module manual proofs for individual procedures
+├── masm-to-lean/                   Rust translator from MASM to Lean
 └── README.md                       Quick-start and proof inventory
 ```
 
@@ -119,7 +94,7 @@ Following Lean 4 / Mathlib style:
 | Category          | Convention     | Examples                                          |
 | ----------------- | -------------- | ------------------------------------------------- |
 | Types, structures | UpperCamelCase | `MidenState`, `Instruction`, `Op`                 |
-| Definitions       | lowerCamelCase | `execInstruction`, `execWithEnv`, `zeroMemory`        |
+| Definitions       | lowerCamelCase | `execInstruction`, `execWithEnv`, `zeroMemory`    |
 | Theorems          | lowerCamelCase | `stepDup`, `stepSwap`, `u64_eq_correct`           |
 | Namespaces        | UpperCamelCase | `MidenLean`, `MidenLean.StepLemmas`               |
 | Generated procs   | dot-separated  | `Miden.Core.Math.U64.eq`, `Miden.Core.Word.testz` |