iris-lean to prove merge-sort

.claude/CLAUDE.local.md

@@ -0,0 +1,78 @@
+\# personal rules (talos)
+
+
+
+\## behavior
+
+do not guess silently. state assumptions before acting.
+
+if anything is ambiguous, list interpretations and ask.
+
+if a simpler solution exists, say so before implementing.
+
+before any pattern decision, check if the codebase already does it.
+
+if found, use that. if not, stop and ask.
+
+
+
+\## code style
+
+minimum code to solve the problem. no extra features.
+
+no abstractions for one-time use.
+
+no decorative dividers. no emoji. no all-caps.
+
+comments: plain lowercase, a word or two.
+
+match existing style when editing existing code.
+
+no Co-Authored-By trailers in commits.
+
+
+
+\## scope
+
+only change what the task requires.
+
+do not refactor unrelated code.
+
+mention unrelated problems separately, do not fix them.
+
+touch as few files as possible.
+
+preserve existing structure.
+
+
+
+\## verification
+
+turn requests into success criteria before starting.
+
+run lake build to confirm. loop until it passes.
+
+
+
+\## reading code
+
+read surrounding code before editing.
+
+identify local conventions before introducing new patterns.
+
+
+
+\## lean 4 task patterns
+
+wp lemma: @\[simp, wp\_simp] theorem wp\_X\_cons, proof is by wp\_atomic.
+
+read execOne in Semantics.lean, mirror it in the wp body.
+
+new instruction: Instruction type + execOne + wp lemma + decoder + emitter.
+
+wp-only task: only touch Wp/Atomic.lean.
+
+do not touch Program.lean files.
+
+do not modify existing proofs.
+

.mcp.json

@@ -0,0 +1,15 @@
+{
+  "mcpServers": {
+    "lean-lsp-mcp": {
+      "type": "stdio",
+      "command": "C:\\Users\\User\\Miniconda\\Scripts\\lean-lsp-mcp.exe",
+      "args": [
+        "--lean-project-path",
+        "programs/lean"
+      ],
+      "env": {
+        "PYTHONUTF8": "1"
+      }
+    }
+  }
+}

codelib/CodeLib/RustStd/Frame.lean

@@ -159,4 +159,52 @@ theorem Mem.read32_write64_disjoint (m : Mem) (a : UInt32) (b : UInt32) (v : UIn
 @[simp] theorem Mem.write64_pages (m : Mem) (a : UInt32) (v : UInt64) :
     (m.write64 a v).pages = m.pages := rfl
 
+/-! ## Mixed-width read/write round-trips
+
+These lemmas extract the lower or upper 32-bit half from a `write64` or
+`read64` — the pattern that arises when func5 copies 8-byte descriptors
+through the shadow stack and then reads back the individual 32-bit fields. -/
+
+/-- Reading the lower 32 bits from a `write64` at the same address returns
+    the low 32-bit half of the stored value. -/
+theorem Mem.read32_write64_low (m : Mem) (a : UInt32) (v : UInt64) :
+    (m.write64 a v).read32 a = v.toUInt32 := by
+  simp only [Mem.read32, Mem.write64]
+  simp only [Nat.add_eq_left, OfNat.ofNat_ne_zero, Nat.succ_ne_self, ↓reduceIte,
+             Nat.reduceEqDiff]
+  bv_decide
+
+/-- The lower 32 bits of a `read64` equal the `read32` at the same address. -/
+theorem Mem.read64_lo_is_read32 (m : Mem) (a : UInt32) :
+    (m.read64 a).toUInt32 = m.read32 a := by
+  simp only [Mem.read64, Mem.read32]
+  bv_decide
+
+/-- Reading the upper 32 bits from a `write64` at the same base address
+    (offset +4) returns the high 32-bit half of the stored value.
+    Requires that the address does not overflow: `(a + 4).toNat = a.toNat + 4`. -/
+theorem Mem.read32_write64_high (m : Mem) (a : UInt32) (v : UInt64)
+    (hnat : (a + 4).toNat = a.toNat + 4) :
+    (m.write64 a v).read32 (a + 4) = (v >>> 32).toUInt32 := by
+  -- After hnat, read positions are a.toNat+4, a.toNat+4+1, a.toNat+4+2, a.toNat+4+3;
+  -- normalize the +1/+2/+3 offsets so they match the write64 footprint indices.
+  simp only [Mem.read32, Mem.write64, hnat,
+             show a.toNat + 4 + 1 = a.toNat + 5 from by omega,
+             show a.toNat + 4 + 2 = a.toNat + 6 from by omega,
+             show a.toNat + 4 + 3 = a.toNat + 7 from by omega]
+  simp only [Nat.add_eq_left, OfNat.ofNat_ne_zero, Nat.succ_ne_self, ↓reduceIte,
+             Nat.reduceEqDiff]
+  bv_decide
+
+/-- The upper 32 bits of a `read64` equal the `read32` at offset +4.
+    Requires that the address does not overflow: `(a + 4).toNat = a.toNat + 4`. -/
+theorem Mem.read64_hi_is_read32 (m : Mem) (a : UInt32)
+    (hnat : (a + 4).toNat = a.toNat + 4) :
+    ((m.read64 a) >>> 32).toUInt32 = m.read32 (a + 4) := by
+  simp only [Mem.read64, Mem.read32, hnat,
+             show a.toNat + 4 + 1 = a.toNat + 5 from by omega,
+             show a.toNat + 4 + 2 = a.toNat + 6 from by omega,
+             show a.toNat + 4 + 3 = a.toNat + 7 from by omega]
+  bv_decide
+
 end Wasm