Every ownership rule of docs/MEMORY.md and the phase that formalizes it. A rule is done when its typing rule is stated, used in the soundness proof, and every hole probe it is meant to reject is mapped to it in corpus/map.tsv.
Formal rules are Lean names in A1/ and A2/ (the same names, extended): typing rules are constructors of StmtT, RhsT, PushArg and the call check CallT; kill, exitScope and derive are the context operations they use. A1's calculus has owned Vec trees (a String is a Vec of bytes); A2 adds structs, enums, closures and trait objects, panics and the drop journal; threads are A3.
| MEMORY.md | Rule | Phase | Formal rule | Status |
|---|---|---|---|---|
| §1, §7.6 | Single owner, drop flags, auto-drop | A1 | an owner's slot is ⟨own, some tree⟩, a released or moved one ⟨own, none⟩ (the drop flag); HeapOK (one owner per allocation); Step.scopeSkip + DropSlot; exitScope | done |
| §2.1 | Moves — use after move | A1 | RhsT.moveOwn, PushArg.move, CallT (sink): the moved binding is dead (live := false) and every read needs a live entry; a moved argument is passed nowhere else in the call and reached from no other argument | done |
| §2.1b | Releasing what the compiler releases | A1 / B | StmtT.free releases only a live owner and kills it; inside unsafe is B | done for safe code |
| §2.2 | Second names | A1 | RhsT.moveOwn (an owner moves), RhsT.copyBor, RhsT.copyRoot, RhsT.borrow (a borrow is copied and depends on the root, derive) | done |
| §2.3 | Stack references must not escape | A1 / A2 | for borrows and views: exitScope ends them with their root, FnOK lets a result depend only on parameters; a closure's captures by handle are what it depends on (RhsT.pack: D), by name what it holds (capDeps), ended with their binding (exitScope, kill) | done |
| §2.4 | Exclusive access for inout arguments | A1 / A2 | CallT: an argument that moves or may change is not lent out (F), is passed once, and is reached from no other argument; paramOK, canDo (the inout bound); an inout argument of any owning type is its owner, never a borrow or a copy (paramOK_inout, h295), and a summary pair on one names a kind inside it (kindFits) | done |
| §2.5 | Iterator invalidation | A1 | a borrow of xs depends on xs: StmtT.push (kill .realloc), RhsT.pop (kill .drop), StmtT.assign and StmtT.free (kill .replace) end it | done |
| §2.6 | Loop-carried moves | A1 | StmtT.while: the body ends in the context it starts in | done |
| §2.7 | Escape through a callee | A1 / A2 / A3 | CallT against the callee's summary: what the result borrows (lends) and holds (rholds), what the callee stores into inout arguments (outHolds), its effect bound on each; FnOK checks the body against it; a closure handed to a callee is held by its result (heldOfArgs) and run as the callee may (NamesFree, mutNames); threads are A3 | done |
| §2.8 | Escape through a return | A1 / A2 | FnOK (the result depends only on what lends / rholds name), callRes at the call; a call through a package lends from the receiver too (recvRes) | done |
| §2.10 | Views end when their source may reallocate | A1 | RhsT.view, RhsT.sat; StmtT.push (Eff.realloc ends views, and element borrows when elements hold views); PushArg / held (a view in a container is still a view); outHolds (a callee storing a view into an argument) | done |
| §2.12 | A stored value belongs to its owner | A1 / A2 | PushArg.move, CallT (sink); aggregate literals (RhsT.pair, RhsT.inl, RhsT.inr) move or copy what they store, a field taken out (takel, taker, unpair) moves; a field replaced in place is the struct taken apart (StmtT.unpair, an owner or an inout struct it may replace) and assigned again (StmtT.assign), ending every borrow of the struct | done |
| §2.13 | A raw string in a value is a view | A1 / A2 | a string view is a slice entry (RhsT.view) depending on its owner; a view stored in an aggregate or a package makes that value depend on what it views (ViewsOK, held) | done |
| §2.11, §7.5 | Closures hold their captures | A2 | RhsT.pack (CapsOK: captures by handle are depended on, by name held, each read or changed within its bound); StmtT.callc (the call through a package: CallT on the code with the captures as inout arguments of their own, NamesFree — a binding a closure may change is changed by the call and reached from no argument but by a closure that changes it the same way — and no argument is such a binding); sigCtx / symNames (a closure a callee is handed may change the callee's inout parameters); ValOK.pkg / envDeps (the environment); A2/CAPTURES_DESIGN.md | done |
| §7.2, §7.3 | Panics and the drop journal | A2 | the panic steps unwind to StmtT.catchR (recover: StmtT.letrec, recStmt) through the journal, dropping what each scope owns (A2/Panic.lean); no_leak_end (A2/Leak.lean) | done |
| §7.7 | Reference-count cycles | B | Rc and its collector are the standard library's unsafe base | not started |
| §6.5 | Threads: Send, Sync, Arc, Mutex, Locked, RwLocked and % Frozen, Atomic, PFile, channels | A3 | — | not started |
| §3, §6.4 | unsafe boundary and the trusted base | B | — | not started |
Every change to the rules of docs/MEMORY.md is recorded here with its effect on the formal rules: whether it touches a rule that is proven (done above), and whether it extends the calculus (a new rule, or a rule made to reject more: every existing proof still holds) or breaks a proof (a rule made to accept more, which reopens its lemmas).
| Change | MEMORY.md | Touches a proven rule? | Effect |
|---|---|---|---|
What a returned value that may hold a closure lends (retclo) is read off its source expression at the ^, through the frame's closures, views and borrows (a bound closure, a join, a reassigned binding, a captured view), not only a literal capturing the parameter by name (h384–h388) | §2.11 | no: in the calculus a returned package's dependencies are its captures' (RhsT.pack, FnOK), whatever names them | none to the proof: the compiler's summary brought into line with A2's FnOK |
| A view of a call's temporary argument is used inside a call that consumes it; kept past it (bound, returned, assigned, stored, taken by a join, handed to a callee that keeps it) it is rejected once the caller owned the temporary — it was left owned by nothing and leaked (h378–h381) | §1 | no: the calculus names every argument (a temporary is a binding its statement makes, and its view borrows it) | extension: safe code is rejected more; the compiler brought into line with A1's named arguments |
A closure handed to a thread or fiber that captures a match's payload, or a binding read out of one, moves the option's owner with it (agora #140); UdpSocket is a shared handle with a drop, udp_close only stops it (h382, h383) | §6.5, §6.4 | no: threads are A3, library handles the trusted base (B) | none to the proof |
| A closure's env is in the panic journal: each function's closure bindings as one frame-table entry (value and owner slot), an argument's closure temporary and a struct literal argument's owned fields while the call runs (h375–h377) | §7.2 | no: A2's panic step drops what each slot owns, a package's environment with it | none to the proof: the compiler brought into line with A2's panic step |
An assignment's value is lent to whatever reads it (the arm of a ? / ?? statement it ends drops nothing); where a join that may select the target lends, the value is copied in (h371–h374) | §7.6 | no: in the calculus a conditional is a statement (ite) whose arms are assignments, and = x x moves the value over itself | none to the proof: the compiler brought into line with the calculus's reading of a join assigned to a binding |
A binding in a borrowed state is refused as an inout argument where the callee may replace that parameter (it used to be released under the binding's owner); a : ~ copy of a % Drop struct from a local owner takes the owner's drop flag, so a replacing call makes the copy the owner and the source moved; a ^ checks its expression's calls first (h367–h370, h295 folded in) | §2.4, §7.6 | no: the calculus has no borrowed binding as an inout argument (paramOK_inout) | none to the proof: the compiler brought into line with paramOK_inout, which never admitted the shape |
arc_get lends every Arc's payload, a trait object's and a cycle-capable one's too (it used to copy those), and the frozen view it lends is tracked for every Arc; a method called through a trait object is summarised as the union of its impls (what it changes and what it replaces, an inout receiver changing the box) before the summaries resolve (h364–h366) | §6.5, §7.7 | no: a call through an interface (callc) takes its parameter modes from the interface, which Implements holds every impl to; Arc is A3 | none to the proof for the dyn call: the compiler's summary had taken less than the impls do, and now takes their union, as Implements does. An ( Arc %Trait ) read is accepted where it was a compile error: the same frozen lend A3 must cover for every arc_get |
An owned binding with a drop flag is journaled with the flag, which the drain reads (it was read when the binding was recorded): a value moved into a literal, a sink parameter, a closure's capture or a dyn box is not released again by a later panic (h361–h363) | §7.2 | no: A2's panic step drops what each slot owns when the panic runs, and a moved owner's slot (⟨own, none⟩) owns nothing | none to the proof: the compiler brought into line with A2's panic step |
A crossing to another thread (thread_spawn, spawn*, chan_send, a pool's return, a Locked's value going in and out) checks at run time that it leaves no owner of a handle whose copies are one state behind, and panics otherwise; a trait object's box is checked through its vtable (h349–h355, h360) | §6.2, §6.5 | no: threads are A3 | closes the open hole recorded below (a library handle's copies on two threads) with a run-time check rather than a rule: A3 must take the crossing's precondition, every owner of such a block goes along, from the check, as a panic where it fails |
A % Sync marker on a Locked, a Channel or a Pool no longer vouches for its value, which faces Send where the container is reached from several threads; an RwLocked's value faces Sync (h357, h358) | §6.5 | no: threads are A3 | extension: safe code is rejected more |
| A binding read out of a library handle field, consumed or taken by a thread, takes its struct along: the struct is dead until given a fresh value (h348, h356) | §7.6 | no: library handles are the trusted base (B) | extension: safe code is rejected more |
An inout parameter given a binding whose value another owner keeps (a field read, a closure's capture) is given a copy; a closure's inout parameter is never an owner of its own (h345–h347) | §7.6 | no: the calculus has no borrowed binding as an inout argument (paramOK_inout) | none to the proof: the compiler gives such a parameter an owned copy, which the calculus types as a fresh owner passed inout |
The journal's elision knows the runtime's panicking entries (nurl_panic_index, a CPU tier's _missing gate, the crossing check), so a function whose only panic is one of them keeps its registrations (h359) | §7.2 | no | none to the proof: which calls may panic is the implementation's to know |
A trait object %Trait is Send only when its trait declares : Send, Sync only with : Send Sync; a : Send / : Sync supertrait is answered by the derivation at each impl (it used to demand an impl block of the marker, which never exists) (h344) | §6.5 | no: threads are A3 | extension for trait objects: safe code that moved or shared one is rejected more; a : Send / : Sync supertrait is accepted where the derivation holds, which only lets the object cross. A1 and A2 have no threads, so no lemma moves; A3 must take a trait object's thread facts from its trait's promise, since the object's type names no field |
A positive % Send / % Sync outside the standard library is unsafe % Send T { }; % NotSend, % NotSync, % Frozen and % Resource stay safe (they only add checks); the in / sync / nocapture claims and the standard library's own markers are in the trusted base, and --unsafe-report lists the program's | §3, §6.4, §6.5 | no: threads are A3 and the trusted base is B, neither started | extension: safe code is rejected more. A1 and A2 have no markers and no threads, so no lemma moves; A3 takes an unsafe % Send / unsafe % Sync as a hypothesis of the base, as B takes an unsafe body |
dist/heartbeat.nu's thread holds the node's liveness (an Atomic and a copy), not the table; PkMemberTable is % NotSend; mqtt_listen takes its client (sink); one open hole listed: a library handle's copies on two threads | §6.2, §6.5 | no: threads are A3 | standard library only (no rule changes) and a stated exception to the guarantee; A3 must model library handles' sharing copies (a copy is a second owner of one state), where the open hole sits |
A destructor that panics while a panic's journal drains is caught by the same recover; the first message is kept; the interrupted drain is ended by the frame that catches it | §7.2 | no: A2's drops run no program code (DropSlot) | none to the proof: runtime behaviour outside the calculus, stated in CLAIM.md (destructors as code are a planned refinement) |
Formal model: inout of every owning type (a struct, an enum, a closure, not only a Vec), a field replaced in place (an inout struct taken apart and assigned again), summary kinds on such a parameter inside it | §2.4, §2.12 | yes: paramOK, FnOK, StmtT.unpair (rules of A2, done) | extension of the calculus to programs it did not express before: paramOK and FnOK accept more parameter types, unpair more modes (canDo .replace for own), FnOK asks kindFits of summaries. Proof-breaking for the lemmas that took an inout parameter to be a Vec (AbsOK, allowed_canDo, callPostAux_lift, rr_sub, rhs_move, CtxWF.unpair, the unpair cases of preservation, progress and renaming): each re-proven, check.sh passes |