Problem: every time a proof writes to address A and reads from address B, it needs a lemma saying "if A ≠ B, the read returns the old value." Currently each proof writes its own memory disjointness lemmas from scratch instead of reusing generic ones (e.g itoa has ~10 such lemmas) and every new program re-derives them.
Solution: add region-based framing lemmas in codelib ( no interpreter changes)
Define a MemRegion type ( start address + length) and provide generic lemmas
- read_write_same: if addr is within the written region, read returns the new value
- read_write_disjoint: if the read region and write region don't overlap, read returns the old value
- write_write_commute: writes to disjoint regions commute
This helps with maintainability of proofs.
For spec readability (mentioned previously), add a MemArray type on top of MemRegion that wraps a base pointer + element size + count. Specs would use arr.get i instead of st.mem.read32(ptr + 4 * i), more readable.
Possible automating it: the verifier already reads the Wasm binary to generate Program.lean, it could also generate framing lemmas automatically by analyzing which memory ranges each function touches.
Reference: CompCert Memory Model (Leroy & Blazy, "Formal Verification of a C-like Memory Model," 2008; Leroy & Appel, "A Formally Verified Compiler Back-end," 2012).
Problem: every time a proof writes to address A and reads from address B, it needs a lemma saying "if A ≠ B, the read returns the old value." Currently each proof writes its own memory disjointness lemmas from scratch instead of reusing generic ones (e.g itoa has ~10 such lemmas) and every new program re-derives them.
Solution: add region-based framing lemmas in codelib ( no interpreter changes)
Define a MemRegion type ( start address + length) and provide generic lemmas
This helps with maintainability of proofs.
For spec readability (mentioned previously), add a MemArray type on top of MemRegion that wraps a base pointer + element size + count. Specs would use arr.get i instead of st.mem.read32(ptr + 4 * i), more readable.
Possible automating it: the verifier already reads the Wasm binary to generate Program.lean, it could also generate framing lemmas automatically by analyzing which memory ranges each function touches.
Reference: CompCert Memory Model (Leroy & Blazy, "Formal Verification of a C-like Memory Model," 2008; Leroy & Appel, "A Formally Verified Compiler Back-end," 2012).