codelib: region-disjointness algebra (MemRegion) + disjoint-write commutation (#68 phase 2a) - #138
Merged
Conversation
This was referenced Jul 11, 2026
…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>
theebayuser
force-pushed
the
codelib/mem-region
branch
from
July 14, 2026 23:30
d507945 to
c7b3329
Compare
mfornet
approved these changes
Jul 15, 2026
mfornet
added a commit
that referenced
this pull request
Jul 15, 2026
Post-merge review of #138 surfaced seven quality findings (no soundness issues); this addresses all of them: - Normalize all four Disjoint->Frame bridge lemmas to one convention (written region first) and fix the section docstring, which falsely claimed order-insensitivity and misdescribed the Frame lemmas' disjunction orientation. read32_write64_of_region's hypothesis flips accordingly (no consumers existed). - Use the Disjoint.symm helper in the bridges instead of inlining its body (h.elim Or.inr Or.inl) at each site. - Move the byte-level Mem foundations (ext_bytes, write64_bytes_in, write32_bytes_in) to Frame.lean's byte-footprint section next to their _of_disjoint siblings, so Frame-level lemmas can use them without an import cycle. - Factor the three verbatim-identical store-commutation case analyses into one generic skeleton, Mem.write_write_comm_of_footprints (Frame); each width pair is now a one-line instance, and a future width (write8/write16 already exist in Mem) costs only its two byte lemmas. - Derive slot64_of_shl from shl3_eq_mul8 instead of a second independent bv_decide, halving the SAT calls in the slot algebra. (shl3_eq_mul8 itself gained a consumer on main via #139's MemFillLoop, so it stays.) - Document Disjoint's ordered-interval semantics for zero-length regions. lake build green in codelib/ and programs/lean; SwapElementsSpec statement unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
mfornet
added a commit
that referenced
this pull request
Jul 15, 2026
#147) Post-merge review of #138 surfaced seven quality findings (no soundness issues); this addresses all of them: - Normalize all four Disjoint->Frame bridge lemmas to one convention (written region first) and fix the section docstring, which falsely claimed order-insensitivity and misdescribed the Frame lemmas' disjunction orientation. read32_write64_of_region's hypothesis flips accordingly (no consumers existed). - Use the Disjoint.symm helper in the bridges instead of inlining its body (h.elim Or.inr Or.inl) at each site. - Move the byte-level Mem foundations (ext_bytes, write64_bytes_in, write32_bytes_in) to Frame.lean's byte-footprint section next to their _of_disjoint siblings, so Frame-level lemmas can use them without an import cycle. - Factor the three verbatim-identical store-commutation case analyses into one generic skeleton, Mem.write_write_comm_of_footprints (Frame); each width pair is now a one-line instance, and a future width (write8/write16 already exist in Mem) costs only its two byte lemmas. - Derive slot64_of_shl from shl3_eq_mul8 instead of a second independent bv_decide, halving the SAT calls in the slot algebra. (shl3_eq_mul8 itself gained a consumer on main via #139's MemFillLoop, so it stays.) - Document Disjoint's ordered-interval semantics for zero-length regions. lake build green in codelib/ and programs/lean; SwapElementsSpec statement unchanged. Co-authored-by: Claude Fable 5 <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
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 2a of #68: a region-level memory algebra in
CodeLib.RustStd.Region, on top of the byte-level framing family from #131.Stacked on #131 and #137 (first two commits here are those PRs; review just the last commit).
What's new
MemRegion(base : UInt32,len : Nat) with a decidableDisjointpredicate over.toNatintervals — the same load-bearing shape theFramelemmas consume, soomega/decidekeep discharging side conditions on concrete frame slots and symbolic array addresses alike. Length isNat, notUInt32: regions are specification-level objects, and unbounded lengths keepDisjointhonest about integer intervals (a region of symbolic length8 * nis a first-class object).Mem.write64_write64_comm,write32_write32_comm, mixedwrite64_write32_comm) — requested verbatim in Memory for proof & spec maintainability #68 ("write_write_commute: writes to disjoint regions commute") and previously missing everywhere. Proved byte-pointwise via a newMem.ext_bytesextensionality lemma pluswrite*_bytes_in("inside its footprint, a store's byte depends only on address and value, not the underlying memory") — nobv_decide, no case blowup: three interval cases andomega.Disjoint→Framebridges (Mem.read64_write64_of_region, …, all four width combos): one-liners that let a proof carry a single region fact instead of re-shapingOrs at every call site.MemRegion.slot64— thek-th 8-byte slot of au64array — with the no-wrap (slot64_base_toNat), codegen-shift (slot64_of_shl,shl3_eq_mul8) and pairwise-disjointness (slot64_disjoint) lemmas that every array proof otherwise re-derives.Consumer (same PR, per the use-site rule)
Project.SwapElements.Spec's local address-arithmetic block (shl3,elemAddr_of_shl,elemAddr_toNat,elemAddr_disjoint) becomes three one-line specialisations of theslot64lemmas —elemAddr ptr kis definitionally(slot64 ptr k).base, so they connect byrfl-conversion. The registeredSwapElementsSpecstatement is byte-identical to #137; only proof plumbing moved.Reviewer note: the commute family's consumer-of-record is issue #68 itself (it is the item requested there); the first in-repo consumer arrives with the next PR in this series (
words64list-view + a ∀-quantified loop-over-memory example, where region framing at symbolic lengths does the work). Happy to split or drop pieces if you'd rather see the consumer land first.Verification
lake buildgreen incodelib/andprograms/lean/; zero lint warnings.#print axiomson the commute family:propext, Classical.choice, Quot.soundonly (the byte-pointwise proofs don't even need thebv_decidereflection axioms).swap_elements_correctunchanged in statement; still axiom-clean.Refs #68.
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