The spec records the second round: two containers, everything copies, five words in a header
This commit is contained in:
parent
bb2471f7a1
commit
0faacb3e57
27
FIX.org
27
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.
|
||||
|
||||
4
NEXT.md
4
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
|
||||
|
||||
@ -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.
|
||||
|
||||
@ -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`) —
|
||||
|
||||
@ -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.
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user