[afflom]

Stacked on #264 (claude/issue-91-stage4-heap-lists at e307369f6); draft. H4-0, ahead of H4a, as the maintainer asked on #91.

What

RustPrims (compiler/src/RustPrims.lex.tex, language 1.2, on RustMemory, RustLists and the calculus's values; one structure and twelve definitions) states what the runtime's buffer, clone, and replace primitives are, for the semantics that reads a Vec/Rc as the value it holds. 21 theorems, all [propext] except the reflexivities (clone_reads and the four primitive laws), no definition observing an axiom.

• Erased meanings are the calculus primitives. erasedPush is prim append of the list and the one item, erasedLength is prim length; prim_append_nil, prim_append_cons, prim_length_nil, prim_length_cons state them on a list (reflexivity), and first_of_snoc/length_of_items are stated with them. erasedTruncate keeps a prefix.
• Buffer. A buffer reads as the list of its items in order (readBuf). bufNew is Vec::with_capacity (the slots of a capacity, none in use): new_reads. pushGrow is the push of RustMemory after a growth when full (push_reads, built from first_of_front, first_of_snoc, append_nothing, less_than_itself, put_into_blank); truncate_reads, first_of_take; length_reads, length_of_items. A valid buffer is append front back with length size front. The model grows by len + 1 slots (at least doubling a full buffer); the runtime's Vec doubles, and the capacity it reaches is the differential's, declared in SPEC §17.17.
• Clone (renamed from share_copy). cloneHandle is the clone of a list's buffer Rc: clone_reads, clone_holds, clone_blocks. share_copy of the shipped library table is Rc::from of a slice or text and is given no meaning here (H4b, with Str/Bytes). share_unique is aloneOn (alone_without_others, holder_blocks of #91 stage 4, H3b: the abstraction theorems of the list representation, kernel-checked (SP-27) #264); share_release is the release of #91 stage 4, H3b: the abstraction theorems of the list representation, kernel-checked (SP-27) #264.
• Replace. replaceHandle: replace_old_reads, replace_now_reads.
• clone_reads, clone_holds, alone_without_others, replace_old_reads, replace_now_reads restate definitions (an identity, projections) and are worded and checked as that and no more.

Proofs use the prior theorems (this module's and the imported ones: push_with_room, room_after_growth, holder_blocks, ...) as simplify rules.

Not in this PR, and why

The claim is the model's. That the declared semantics gives the primitives these readings is the opening of H4a's first function (length_list): per the maintainer's answer on #91, each list item is one machine call whose meaning is the existing TargetSyntax.Prim, with refines_ of the core shape, and the buffer/clone/replace constructors go where support code is authored (the RuntimeSyntax second module). That the runtime's Vec, Rc and mem::replace behave as the model is the evidence of the differential and of rustc.

SP-28 (build) and the measured figure

cargo test -p repo-conformance --test conformance -- conformance_sp_28, in its own part of bdd (preservation-prims, row bdd-preservation-prims), 4-core 15 GB container, pinned Lean 4.32.1, nothing else running: 120.9 s wall (module + seven planted modules), peak resident set of the pinned Lean 750,180 KiB (0.75 GB), sampled every three seconds, one lean at a time; lexlean verify of the module alone 24.4 s (debug binary). The figure first posted on #91 (62.6 s, 0.34 GB, 15.1 s) was for the 17-theorem version; the four primitive reflexivity lemmas and the prim append/prim length forms in first_of_snoc, length_of_items and push_reads account for the growth. Plants, each asserted by the theorems Lean refuses and the goal it leaves: a push that puts the item in front, a full buffer that is not grown (push_reads), a truncation that keeps one too many (truncate_reads), a clone that does not hold (clone_reads, clone_holds, clone_blocks), a replace that returns the new value, a length that counts one more (length_reads), a new buffer that is not empty (new_reads); plus the listing refusals.

Identity

New module in the compiler project. compiler/src is not in the embedded set the compiler-semantics ID hashes and compiler/expected covers only Main's closure, so no ID moves, no record regenerates, no relock is owed. Register 450, SP-28 in §31 (section §17.17) and the totals.

---

🤖 Generated with Claude Code

https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG

[afflom]

Maintainer review of 30389f7 (read-only; cargo fmt --check, validate-model 450, validate-spec-links 450, check-test-inventory with the preservation-prims part holding SP-28, all green; conformance_sp_28 reproduced green in 48.3 s, peak lean 336,492 KiB; the module canonical after a scratch relock; nothing under language/, crates/lexlean, RustSyntax, RustSemantics or the lock, so no identity move relative to the base). The R3 chain, the part, the six plants by exact refused set and goal, the pins and the SP-22 measurement are in order, and push_reads, truncate_reads and length_reads are real laws closed by prior theorems as rules. One round is needed, on the meanings themselves:

Round

1. shareCopy (RustPrims.lex.tex:95) is the identity on a Handle, and the register, §17.17 and the clause "a clone reads as the handle it clones" give share_copy the meaning of the Rc handle clone. But share_copy in the shipped library table (calculus/rust_library.rs:133-135, mapped at 247-249) is std::rc::Rc::from, "a shared immutable buffer holding a copy of a slice or a text"; the handle clone the list representation performs (buffer.clone(), std.rs.txt:27-28) is the clone construct. The row attributes a meaning to a primitive the module does not model. Either model Rc::from as share_copy (a fresh shared buffer reading as the copied items) and state the clone laws under the clone construct's name, or rename the definition and reword the register and §17.17 to the clone, dropping the share_copy name from them.
2. new_reads (:355) is stated on a record literal {slots := blank capacity fill, len := 0} and is true for any slots, so no allocator could be caught and no named model of buffer_new exists. Add bufNew capacity fill (Vec::with_capacity) and state new_reads about it; LAWS requires it.
3. The erased meanings are listAppend and lengthItems, while runItem evaluates Item.lengthList and appendList to the calculus's prim length and prim append (RustSemantics:486, 1171). A refines_ statement needs the bridge: define erasedPush/erasedLength with the calculus primitives, or add lengthItems xs = prim length xs and listAppend xs ys = prim append xs ys to the law set.

Nits (same push)

4. copy_reads, copy_holds, copy_blocks, alone_without_others, replace_old_reads, replace_now_reads are identity or projection restatements of #91 stage 4, H3b: the abstraction theorems of the list representation, kernel-checked (SP-27) #264's theorems; the register sells them as clone and replace laws. Either state replace over a store place and the clone over the handle set (others := cons copy others), or word the register as "by definition" for them.
5. pushGrow grows by len + 1 slots filled with the pushed item where the runtime grows by doubling; one sentence in §17.17.
6. The §31 row cites §17.16 while the prose sits in §17.17 (inherited from SP-26 and SP-27; fix all three rows in this push).

For H4a's first commit, so the refinement is over the declared semantics and not the model alone: per new Machine constructor, the lifting theorem (runMachine bufferLen [Value.list (readBuf buf)] = Value.nat buf.len, bufferPush likewise via pushGrow) proved from this module's laws, the two bridge lemmas of item 3, the std crate's length_list written as the oracle's walk (cells then run) rather than a call of the primitive, and the crate in a module outside Main's closure until the figure is on #91.

I re-verify the round by reading the diff.

---

Generated by Claude Code

[afflom]

Maintainer: the round at 6a1416a is accepted (read-only re-verification; cargo fmt --check, validate-model 450, validate-spec-links 450, check-test-inventory 780 with preservation-prims holding SP-28, all green; conformance_sp_28 reproduced green in 98 s, peak lean 721,624 KiB, so the author's 120.9 s / 750,180 KiB figure is of the right order and the growth from the 17-theorem version is real). cloneHandle is now stated against the clone construct of the list's Rc, with share_copy (Rc::from) declared H4b's and given no meaning here; bufNew models with_capacity and new_reads is about it with its plant; erasedPush and erasedLength are the calculus's prim append and prim length, which are what runItem evaluates appendList and lengthList to, with the four nil/cons lemmas as the stated bridge; growth declared; the §31 columns fixed. Twenty-one theorems, seven plants by refused set and goal.

Wording to ride H4a's first commit on this branch (no theorem, plant or gate changes): "(by definition)" after clone_reads, clone_holds, alone_without_others, replace_old_reads, replace_now_reads in the register statement itself (SPEC prose and VERIFICATION have it; the prose omits alone_without_others from its list); first_of_front is named as a piece of push_reads but is used only by length_reads, so move it; the case doc comments of rust_prims.rs, rust_lists.rs and rust_memory.rs cite §17.16; and the four prim_* laws require no function in LAWS, so require the tokens their prim append/prim length forms carry, or a content-free restatement would pass the listing.

#262 at 6af4ebd and #264 at e307369 carry only the asked wording and column changes and stay accepted. Lands after #254, #255, #259, #262 and #264 with its own regeneration.

---

Generated by Claude Code