codelib: words32/slot32 twins + verified u32 copy loop (#68 phase 2c) - #140
Merged
mfornet merged 7 commits intoJul 16, 2026
Merged
Conversation
…mutation Phase 2a of cajal-technologies#68. Adds CodeLib.RustStd.Region on top of the byte-level framing family in RustStd.Frame: - MemRegion (base : UInt32, len : Nat) with a decidable Disjoint predicate over .toNat intervals — the same shape the Frame lemmas consume, so omega/decide keep discharging it on concrete slots and symbolic array addresses alike. - Disjoint stores commute (write64/write64, write32/write32, mixed) — requested verbatim in cajal-technologies#68 and previously absent. Proved byte-pointwise via a new Mem.ext_bytes + write*_bytes_in, no bv_decide, axiom-clean. - Disjoint → Frame bridges (read*_write*_of_region) for all four widths. - MemRegion.slot64: the k-th u64 element slot, with no-wrap, codegen-shift and pairwise-disjointness lemmas. Consumer: SwapElements/Spec.lean's local address block (shl3, elemAddr_of_shl, elemAddr_toNat, elemAddr_disjoint) collapses to three one-line specialisations of the slot64 lemmas (elemAddr ptr k is defeq (slot64 ptr k).base). The registered SwapElementsSpec statement is unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phase 2b of cajal-technologies#68, on top of the MemRegion algebra. MemArray.lean — Mem.words64 base n : List UInt64, the list view of the u64 array [base, base+8n). Defined via List.range/map so length and indexing are simp-lemmas; plus words64_ext, words64_write64_outside (framing through MemRegion), words64_succ (snoc) and words64_write64_extend (the fill step as a view equation). This is the codelib home for the memory-as-list view merge_sort (cajal-technologies#106) carries privately as wordsAt. MemFillLoop.lean — fillWords_spec: the canonical fill loop writes v to each of the n u64 slots of [base, base+8n), proved for ALL n via the invariant/variant loop rule (wp_loop_cons), with the whole-region result stated as st'.mem.words64 base n.toNat = List.replicate n.toNat v. Every memory example under interpreter/Examples is a concrete native_decide check because symbolic framing lives downstream here in CodeLib; this is the first universally-quantified loop-over-memory theorem in the repo, and the shape merge_sort's proof needs. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
theebayuser
force-pushed
the
codelib/mem-words32
branch
from
July 14, 2026 23:30
8a53e4d to
9187214
Compare
…use fixes Follow-up to review of the words64 array view + fill-loop proof: - fillWords_spec now carries a frame condition: every byte outside `[base, base+8n)` is preserved (postcondition + loop invariant), so the theorem composes with facts about neighbouring memory (the merge_sort shape). - Extract `Mem.words64_slotAddr_toNat`, the shared no-wrap slot-address bridge, and use it in `words64_write64_outside` / `_extend` (was duplicated inline). - FillWords' `(const 3) shl` step reuses `MemRegion.shl3_eq_mul8` instead of a fresh `bv_decide`. - MemArray module docstring: drop the stale `words64_write64_set` reference (the lemma is `words64_write64_extend`) and correct the simp-lemma note (`getElem_words64` is intentionally not `@[simp]`). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phase 2c of cajal-technologies#68 — the 32-bit twins the [u32] memory proofs (merge_sort, cajal-technologies#106) need, plus their first consumer. - MemRegion.slot32 (+ shl2_eq_mul4, slot32_base_toNat, slot32_disjoint): the 4-byte element-slot twin of slot64. - Mem.words32: the List UInt32 view of [base, base+4n), in the same (List.range n).map shape as cajal-technologies#106's private `wordsAt`, with length/getElem/ext/write32_outside/succ and a general words32_write32_snoc (write the n-th slot ⇒ append its value to the length-n view). - copyWords_spec (MemCopyLoop.lean): the companion to cajal-technologies#139's fillWords_spec. The canonical load32/store32 copy loop over two disjoint u32 regions is proved, for all n, to leave `words32 dst n = words32 src n` with the source unchanged — what LLVM emits for a small opt-0 copy_from_slice, and the analogue of merge_sort's copy helpers. Invariant discharged via words32_write32_snoc (dst) + words32_write32_outside (src, MemRegion disjointness); axiom-clean. Refs cajal-technologies#68, cajal-technologies#106. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
theebayuser
force-pushed
the
codelib/mem-words32
branch
from
July 14, 2026 23:47
9187214 to
b70fe5e
Compare
…reuse Applies the same review pattern mfornet landed on the words64/fill-loop proof (e64576c) to the words32/copy-loop twin: - copyWords_spec now carries a frame condition: every byte outside `[dst, dst+4n)` is preserved (postcondition + loop invariant), so the theorem composes with facts about neighbouring memory (the merge_sort / copy_from_slice shape). Discharged per iteration via `Mem.write32_bytes_of_disjoint`. - Extract `Mem.words32_slotAddr_toNat` (the 4-byte twin of his `words64_slotAddr_toNat`) and use it in `words32_write32_outside` / `_snoc`, which duplicated the no-wrap slot-address bridge inline. - CopyWords' `(const 2) shl` step reuses `MemRegion.shl2_eq_mul4` instead of a fresh `bv_decide`. Full `lake build` green (codelib + programs, Lean v4.32.0); copyWords_spec is axiom-clean (standard axioms + one bv_decide reflection, no sorry). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…use, words64 snoc/extend symmetry - copyWords_spec: state disjointness as MemRegion.Disjoint (definitional restatement; unfolded to the Or once at the top of the proof) - copyWords_spec: use the Mem.words32_slotAddr_toNat bridge for hda instead of re-unfolding MemRegion.slot32; close haddr_d/haddr_s with UInt32.add_comm instead of two bv_decide SAT calls - MemArray: add the general Mem.words64_write64_snoc and re-derive words64_write64_extend from it, restoring 32/64 twin symmetry - docs: qualify the wordsAt references (PR cajal-technologies#106, not yet in-tree) and name the intended consumers of slot32_of_shl/slot32_disjoint Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
mfornet
approved these changes
Jul 16, 2026
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
2 participants
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.
Overview
Phase 2c of #68: the 32-bit twins of the
slot64/words64region+view algebra, plus a verified word-by-word copy loop — the pieces the[u32]memory proofs (merge_sort, #106) need. See the comment on #106 for how this maps onto theFraming.lean/wordsAtlemmas that PR is currently carrying privately.Stacked on #131 / #137 / #138 / #139 (review the last commit).
What's new
MemRegion.slot32(Region.lean) — thek-th 4-byte element slot, withshl2_eq_mul4,slot32_base_toNat(no-wrap), andslot32_disjoint. Exact 4-byte twin ofslot64.Mem.words32(MemArray.lean) — theList UInt32view of[base, base+4n), defined in the same(List.range n).map …shape as#106'swordsAt(so that file can become an import), withlength/getElem/ext/write32_outside/succand a generalwords32_write32_snoc("writing the n-th slot appends its value to the length-n view") that serves both copy and fill loops.copyWords_spec(MemCopyLoop.lean) — the companion to codelib: words64 array view + first ∀-quantified loop-over-memory proof (#68 phase 2b) #139'sfillWords_spec: the canonicalload32/store32copy loop over two disjointu32regions, proved for allnto leave the destination view equal to the (unchanged) source view:copy_from_sliceatopt-level = 0(a load/store loop, notmemory.copy), and the direct analogue ofmerge_sort's copy helpers. The loop invariant (words32 dst i = words32 src i, source region framed intact) is discharged withwords32_write32_snocon the destination andwords32_write32_outside(viaMemRegiondisjointness) on the source — notake/index gymnastics.Verification
lake buildgreen incodelib/; zero lint warnings.#print axioms copyWords_spec→ standard axioms + thebv_decidereflection axioms from the shift/address lemmas; nosorryAx.slot32/words32/words32_write32_snoc/words32_write32_outsideare all consumed bycopyWords_spec.Refs #68, #106.
Disclosure per CONTRIBUTING: AI tooling (Claude Code) was used to write and check these proofs; I own the change and am accountable for every line.
🤖 Generated with Claude Code