From 0faacb3e57599785c0150161dc957b89b9827cf5 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 18 Sep 2026 12:38:26 +0700 Subject: [PATCH] The spec records the second round: two containers, everything copies, five words in a header --- FIX.org | 27 ++++++++++ NEXT.md | 4 +- docs/BUILT.md | 10 ++++ docs/REVIEW-production-readiness.md | 4 +- spec-memory.md | 80 +++++++++++++++++++---------- 5 files changed, 93 insertions(+), 32 deletions(-) diff --git a/FIX.org b/FIX.org index 2d001f2..9bae6c5 100644 --- a/FIX.org +++ b/FIX.org @@ -256,3 +256,30 @@ NEXT.md are annotated at their live claims. Two of the day's fix lanes were cancelled with this (borrowed-flag, region element); the while-condition fix merged in the morning is deleted again by the repeal, and its pin with it. + +* The second round, 2026-09-18 — Pool, move-only, and the gen word + +Ordered by the author after the ownership repeal, on the same argument: the +Odin position, full stop. + +- Pool and (Handle T) are gone — types, checker arms, runtime section, + fixtures. Two containers are enough; a slab with generational handles is a + library over a Vec when a program wants one. +- The move-only concept is gone: everything copies as its header, copyable? + left the predicate list (four remain), and the struct/defdata/defunion + owning-field refusals are lifted. The region rule stands untouched — a + container of owning elements is still built against a region and released + by one free-all. +- The gen word left both container headers (read by nothing since it was + written). A Vec is ptr len cap allocator epoch; the epoch trap stays. +- Container globals keep both declaration rules, reworded: they start zeroed + (a global initialiser is a compile-time constant, and a container's only + constant is the empty one), and a defconst container is refused since a + constant is not an assignable place. sand.flan's experiment line would now + be refused with the reworded sentence. + +Everything verified together: dune test --force 232/0 with zero suite FAILs, +@x86 122 MATCH / 0 DIFFER, @sanitize clean, and the whole-repo check sweep +against the parent differs only where it should: the two negative fixtures +now accepted (vec-in-struct, the clause-less generics corpus), the two pool +fixtures deleted. diff --git a/NEXT.md b/NEXT.md index f033eb8..b032bcd 100644 --- a/NEXT.md +++ b/NEXT.md @@ -195,7 +195,7 @@ Worth stating because the notes elsewhere may still read the old way: an `Int`, a `Ptr`, an `Alloc` or a `Handle`, with aggregates leaving through an out-pointer, and `crossable` refuses an aggregate return from a `declare` outright. The refusal in `call_native` is unreachable and building sret behind it would have been *wrong* — that path is the C boundary, where - SysV returns a 16-byte slice in `rax:rdx` rather than by hidden pointer. `Vec`, `Map` and `Pool` all + SysV returns a 16-byte slice in `rax:rdx` rather than by hidden pointer. `Vec`, `Map` and `Pool` (since removed) all match; item 16's "unexercised" line was stale. - **The header check is not opt-in.** `vendor/raylib/raylib-5.5.h` is committed and `vendor/raylib/headers` names it directly. There is no `FLAN_RAYLIB_H`. @@ -321,7 +321,7 @@ the easy half. What is left is conditions, and the measurement moved them from ' doing first. Do that before item 1, not after. 3. **`Rt` with an aggregate return**, and with it most of the container runtime. `Vec`, `Map` and - `Pool` have not been exercised through this backend at all. + `Pool` (since removed) have not been exercised through this backend at all. 4. **`Fnval`'s indirection cell.** `FnAddr (Fnval n)` emits the symbol, which is right for a whole-program build and wrong the instant anything is redefined into it. There are no cells and no diff --git a/docs/BUILT.md b/docs/BUILT.md index 7521e67..410baff 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -2910,6 +2910,16 @@ is still right: a union has a C layout and still may not cross to C by value, be ## `(Handle T)` and the pool, which is what a stale reference answers with +**Removed 2026-09-18**, in the second round of the repeal: two containers are +enough, the corpus's only pools were its own fixtures, and a slab behind +generational handles is a library over a `Vec` when a program wants one — +which is where Odin keeps it. The `gen` word on `Vec` and `Map` went the same +day (maintained, read by nothing; the header is `ptr len cap allocator +epoch` now), and so did the move-only concept itself — everything copies, and +`copyable?` left the predicate list. spec-memory.md, "The repeal", carries +all three amendments. The section below is kept as the record of what was +built. + A handle is a reference to something that can die, which reports that it died rather than silently resolving to whatever reused its slot. `check.ml` refused `(Handle T)` by name as milestone 6; this is what it stood for, and the pool came with it because the pool is what makes the report possible. diff --git a/docs/REVIEW-production-readiness.md b/docs/REVIEW-production-readiness.md index e71c50d..e744b6d 100644 --- a/docs/REVIEW-production-readiness.md +++ b/docs/REVIEW-production-readiness.md @@ -144,8 +144,8 @@ The containers, strings/UTF-8, sequences, random, and printing layers are decent `flan_transfer_fail`, `flan_null_alloc_fail`, `flan_free_all_fail` → `rt_die`). Bounds and arithmetic already park via the break-loop hook; these should too. - **Unchecked `malloc` in `flan_argv`** (`flan_rt.c:162`) — the one in the file. -- **`v->gen` stale-slice word is maintained and never consulted** (`flan_rt.c:1347`) — - either implement the check or delete the field before someone trusts it. +- ~~**`v->gen` stale-slice word is maintained and never consulted**~~ — deleted + 2026-09-18 with the second round of the repeal; the header is five words now. - **`flan_slurp_into` conflates elements and bytes and skips `flan_vec_check`** (`flan_rt.c:2746`) — safe only because check.ml pins slurp to `(Vec u8)`; a latent trap. - **`flan run` swallows build flags as program arguments** (`bin/main.ml:634-651`) — diff --git a/spec-memory.md b/spec-memory.md index ad960e0..e3dfa8d 100644 --- a/spec-memory.md +++ b/spec-memory.md @@ -29,11 +29,10 @@ facility (see plan.org, "Managed classes"). or a literal in read-only memory. Copying a slice copies ptr+len, never the elements. A slice may be `const`-qualified; freeing through one is not possible because a slice has no allocator and no `cap`. -- `(Vec T)` and `(Map K V)` are **move-only**. Assignment hands over the one - header rather than copying it — there is no implicit shallow copy, so two - owners never arise from an assignment; `(clone x)` is the only spelling of a - second, independent one. Since the repeal, using the source binding again is - not a compile error: the header is still there, and a program that frees +- `(Vec T)` and `(Map K V)` **were move-only**; the second repeal removed the + concept. Assignment copies the header, the copies alias one buffer, and + `(clone x)` is the spelling of an independent one. Using a binding after + assigning it away is ordinary: the header is still there, and a program that frees through it twice or reads through it after a free misbehaves at run time, where the allocator and the dev build's generation word are the net. @@ -78,7 +77,10 @@ points at. allocator; `(clone x alloc)` names one. Value types (`[n T]`, structs of value types, primitives) need no `clone` — assignment already copies them. -A struct containing a `Vec` field is itself move-only. Ownership is structural, +A struct containing a `Vec` field was itself move-only until the second +repeal; since it, the field is admitted and the struct copies like any other +(see "The repeal"). The paragraphs below record the rule as designed. +Ownership is structural, not declared: a type is a value type iff all of its fields are **and it declares no `drop` hook** (see Allocators). A `drop` hook makes a type move-only for the same reason a `Vec` field does — exactly one owner, so the hook fires exactly @@ -106,12 +108,13 @@ region" for the rule that stands in its place and for what it costs. - A future lightweight provenance pass may reject the obvious mistakes (a borrow of a local escaping, use after an owner moves, and reallocation with a live borrow). It must not require Rust-style lifetime annotations or dictate - an ECS-shaped object model. Long-lived graph links use `(Handle a)`; temporary - graphs may use explicitly managed, stable region storage. -- Cross-referencing long-lived objects uses `(Handle a)` into a pool, never a - raw pointer or slice. A stale handle is detectable. + an ECS-shaped object model. +- Cross-referencing long-lived objects used `(Handle a)` into a `Pool` until + the second repeal (below) removed both: two containers proved enough, and a + program that wants generational indirection builds it over a `Vec`, as an + Odin program does. -## Globals of move-only type +## Container globals A global may be a `Vec` or a `Map`. Its intended lifetime is the process's — it is loaded once and never released — and before the repeal a flow rule enforced @@ -127,10 +130,9 @@ take their target as a borrow, so a global `(Vec u8)` is filled and grown where it stands. The aliasing contract is the one above and nothing more — a push that reallocates invalidates a slice taken before it, and that is the programmer's whether the owner is a local or a global. Globals get no borrow rule locals do -not have; the dev build's generation word lives on the `Vec`, so the stale-slice -trap works the same either way. +not have. -A move-only global **starts zeroed** — a zeroed `Vec` is an empty `Vec` — and is +A container global **starts zeroed** — a zeroed `Vec` is an empty `Vec` — and is loaded by whichever function loads it, with an ordinary assignment: ``` @@ -147,6 +149,9 @@ first block and leaks it; there is no `drop`, and freeing is a thing you write. ## The repeal — 2026-09-18 +(Extended the same day by a second round; see the amendments at the end of +this section.) + The first implementation carried a static flow analysis: a per-function dead set recording moved-out bindings, a borrow flag over the container-reading operations, an iteration diff for loops, and a borrowed-never-moved rule for @@ -162,17 +167,31 @@ believed. What the language promises after the repeal is Odin's contract, which is the model this memory design was built from in the first place: -- **The types** still decide what may be copied and what may own what: move-only - assignment hands over the header, `clone` is the only copy, and the - struct/union/pool ownership rules all stand. -- **The allocator** still decides what a free means: `can-free`, regions, +- **The allocator** decides what a free means: `can-free`, regions, `free-all`, and the region-only rules for containers of owning elements all stand. - **Which frees run, and when, is the program's.** `defer` is the tool, and a double free or use-after-free is a run-time misbehaviour, not a compile error. -- **The dev build detects.** The generation word on `Vec`, the region epoch - trap, and the block registry are the net, where a game is actually run. +- **The dev build detects.** The region epoch trap and the block registry are + the net, where a game is actually run. + +The same day, the rest of the concept followed, on the same argument carried +to its end: + +- **The move-only concept itself is gone.** Everything copies — a container as + its header, the copies aliasing one buffer. The `copyable?` predicate went + with it (four predicates remain), as did the struct, data-type and union + owning-field refusals: a struct may hold a `Vec`, and the two-headers-one- + buffer aliasing that buys is the program's, exactly as it is in Odin. +- **`Pool` and `(Handle a)` are gone.** Two containers are enough; a slab with + generational handles is a library a program writes over a `Vec` when it + wants one, which is where Odin keeps it too. +- **The `gen` word is gone from both headers.** It was bumped on every + reallocation and read by nothing — the stale-slice check it promised needs a + third word on every slice, not a word here. A `Vec` is now + `ptr len cap allocator epoch`; the epoch word stays because free-all + detection reads it on every operation. A future provenance pass (the "Open" section at the end of this document, and plan.org #3) remains the door back to static checking. It is additive: nothing @@ -235,13 +254,13 @@ instantiates it: > field-free storage. It does **not** support `=`, `<`, `+`, or `hash`. What makes that liveable is a `where` clause of compile-time type predicates, -written as a map at the head of the body. There are five — `ordered?`, `equal?`, -`hashable?`, `numeric?`, `copyable?` — they are not type classes because a +written as a map at the head of the body. There are four — `ordered?`, +`equal?`, `hashable?`, `numeric?` — they are not type classes because a predicate carries no implementations and merely gates a builtin the compiler -already has, and they entail one another in one direction, so one clause usually -does. A variable is move-only by default and `copyable?` is the opt-out, because -whether a variable moves is not decidable abstractly. plan.org's Types section -has the full account. +already has, and they entail one another in one direction, so one clause +usually does. (`copyable?` was the fifth until the second repeal removed the +move concept it opted out of.) plan.org's Types section has the full +account. ``` (defn sort! [s [$t]] () @@ -480,7 +499,8 @@ a reason that is not teardown — nothing records which member is live, so there is no fact a release could read — and a region answers the teardown question without touching that one. -A `Pool` is admitted with the others, and it is the one where the trade is not +A `Pool` was admitted with the others while it existed (the second repeal +removed the type), and it was the one where the trade is not identical, because `(release p h)` recycles a slot while the pool lives on. Whatever the dead element owned stays allocated until `free-all`. That is a region leak bounded by the region, which is what a region already is; it is not @@ -611,7 +631,11 @@ practice: a union is all-bytes-zero unless `uninit` says otherwise. Three things a union may not do, and each for a reason that does not expire: -- **No move-only member.** Nothing knows which member is live, so nothing can +- **No owning member** — until the second repeal, which admits one: nothing + records which member is live, and since nothing (the program included) can + free the right one through the union itself, the tag the program keeps + beside it is the way, C's way. The rest of this entry records the rule as + designed. Nothing knows which member is live, so nothing can tear one down. Unlike the struct and `defdata` refusals, this is not waiting on recursive teardown — there is no fact for teardown to read, and freeing the wrong member is a free of a pointer that was an `f64` a moment ago.