The repeal is written down where the rules were: spec, BUILT, NEXT, the ledger, FIX
This commit is contained in:
parent
2edd441ecf
commit
2b9f271cc3
22
FIX.org
22
FIX.org
@ -234,3 +234,25 @@ Left for the author, recorded where each lives:
|
||||
- sand.flan:167 still holds the refused defconst experiment; the diagnostic
|
||||
now prints in full and names the fix.
|
||||
- Tier 2 (install and shipping) deliberately not started.
|
||||
|
||||
* The repeal, 2026-09-18
|
||||
|
||||
The ownership flow analysis is removed: the per-function dead set, the borrow
|
||||
flag, the loop-iteration diff, and the borrowed-never-moved rule for globals.
|
||||
Use-after-move and double-free are no longer compile errors. What stands:
|
||||
move-only as a type property (assignment hands over the header, clone is the
|
||||
only copy), the struct/union/pool ownership rules, defconst-vs-defvar for
|
||||
move-only globals, defer, all allocator capabilities, and the dev build's
|
||||
generation checks — now the primary net, which is the Odin position the
|
||||
memory design came from.
|
||||
|
||||
Decided after the bug hunt put four of its ten lanes inside this machinery.
|
||||
An unsound checker is worse than none, because it is believed. The door back
|
||||
is spec-memory.md's provenance pass: removal widened acceptance without
|
||||
changing any accepted program's meaning, so a stricter pass can return
|
||||
additively. spec-memory.md "The repeal" is the amendment; BUILT.md and
|
||||
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.
|
||||
|
||||
13
NEXT.md
13
NEXT.md
@ -657,9 +657,9 @@ The prelude keeps a per-type layer for the numeric ones. That is the honest numb
|
||||
while `copyable?` is a predicate the compiler answers, because it already knows which types own heap storage.
|
||||
Same ergonomics, none of the trait machinery, consistent with the `where` decision above.
|
||||
|
||||
What this means in the body: a generic may not use a parameter twice unless it declares `copyable?`.
|
||||
`(defn twice [x $t] $t (+ x x))` is refused without it — correct at `i32`, wrong at `(Vec i32)`, and the
|
||||
checker cannot tell which until it substitutes.
|
||||
What this meant in the body — a generic may not use a parameter twice unless it declares `copyable?` — was
|
||||
repealed 2026-09-18 with the rest of the flow analysis; move-only-by-default still governs the structural
|
||||
rules (what a struct, union or pool may own at a `$t`).
|
||||
|
||||
1. **The runaway refusal.** `(defn grow [x $t] () (grow [x x]))` asks for a copy at `[2 t]`, then `[2 [2 t]]`,
|
||||
forever. Before the spike's cap it did not fail, it **hung** — and `Session.eval` runs the same code, so what
|
||||
@ -1728,10 +1728,9 @@ Two smaller findings, both written down beside the code that ran into them:
|
||||
macros from the forms fed back as `extra`. `format-f64` is `(clamp prec 0 9)` now. "A prelude macro may not call a
|
||||
macro" stands and names itself when violated.
|
||||
|
||||
- **A returned `Vec` is a move, and the dead set spans the function**, so an early `(return v)` on one branch kills
|
||||
the binding for the `v` at the foot of another. `replace-bytes` guards its empty-needle case with an `if` rather
|
||||
than a `when`/`return` for that reason. Probably correct as it stands — the analysis is not path-sensitive and
|
||||
making it so is a real piece of work — but it is a shape that reads as though it should compile.
|
||||
- ~~**A returned `Vec` is a move, and the dead set spans the function**~~ **Repealed 2026-09-18** with the rest of
|
||||
the flow analysis (spec-memory.md, "The repeal"): the early-`return` shape compiles now, and `replace-bytes` no
|
||||
longer needs its `if` workaround, though it keeps it harmlessly.
|
||||
|
||||
Already present and easy to miss: an **EDN parser**, at `vendor/edn/edn.flan`.
|
||||
|
||||
|
||||
@ -7,6 +7,8 @@ marked **DISPATCHED** have fix lanes; the rest are recorded here and wait.
|
||||
## Dispatched
|
||||
|
||||
### 1. `borrowed` grants the borrow flag to whole subtrees — moves inside container targets vanish
|
||||
**Repealed, not fixed (2026-09-18):** the flow analysis this hole lived in was removed wholesale
|
||||
(spec-memory.md, "The repeal"). The trigger programs now compile by design and misbehave at run time.
|
||||
`lib/check.ml:2062-2076`. The flag gates both `moved` (2003) and `global_borrow` (2033),
|
||||
and is set across the entire checking of the target: the index argument of `at`, the base
|
||||
of any `Field`. A move nested there is never recorded.
|
||||
@ -20,6 +22,8 @@ Fix direction: narrow the flag to the target's own read — restore `ctx.borrow`
|
||||
index of `at`; treat `Field` as simple only when its base chain bottoms out at a `Var`.
|
||||
|
||||
### 2. A `while` condition is move-checked outside `in_loop` — double free on iteration two
|
||||
**Fixed, then repealed (2026-09-18):** the fix merged (47cb46a) and was removed the same day with the
|
||||
whole flow analysis. The trigger compiles and aborts in the allocator at run time, by design.
|
||||
`lib/check.ml:1688-1691`. The condition is checked before `in_loop` is entered, but
|
||||
emit re-runs it every trip (`emit.ml:1838`). A condition that moves a local frees it
|
||||
once per iteration. Confirmed: glibc double-free abort, exit 134.
|
||||
@ -66,7 +70,9 @@ territory; fix or record, the lane's call.
|
||||
|
||||
## Recorded, not scheduled
|
||||
|
||||
- **Region guard never asks about elements** (`lib/check.ml:1272`, refusals 4092/4165):
|
||||
- **Region guard never asks about elements** — **repealed, not fixed (2026-09-18)**: with the flow
|
||||
analysis gone, `free` of an `at` result is no longer a checker question; the mixed-allocator
|
||||
construction is legal and its misuse is a run-time matter. (`lib/check.ml:1272`, refusals 4092/4165):
|
||||
a heap-backed inner Vec pushed into an arena-backed outer passes the guard; `at` then
|
||||
hands out an owning header, `free` accepts it, and the later read is a confirmed UAF
|
||||
(printed garbage). Breaks the premise stated in the clone note at check.ml:4152.
|
||||
|
||||
@ -2483,6 +2483,10 @@ different reason (below), but the adopt rule is what makes `Zero` of a Vec a usa
|
||||
|
||||
### Move-only is a dead set, and it is flow-sensitive at a join
|
||||
|
||||
**Repealed 2026-09-18.** The dead set, the borrow flag, and the loop rule this section describes were removed with
|
||||
the rest of the flow analysis — spec-memory.md, "The repeal", is the amendment. The section is kept as the record of
|
||||
what was built and why. Move-only as a *type* property (what may be copied, what may own what) stands.
|
||||
|
||||
Reading a move-only local is a move unless the site said it was a borrow. That is the conservative direction: passing
|
||||
one to a function, binding it, returning it and `free`ing it are all moves and all reach one place, and the handful of
|
||||
operations that only look at a container (`at`, `len`, `as-slice`, `push`, `reserve`, `clone`) say so. Only a
|
||||
@ -3597,9 +3601,8 @@ be wrong in a way worth being able to see: the prelude *was* reaching the expand
|
||||
over the file being compiled; the prelude reaches the checker through `Check.program`'s prepend. The call resolves
|
||||
to the macro's underlying `defn` and reports an arity error, which is why `format-f64` writes
|
||||
`(min 9 (max 0 prec))`.
|
||||
- **A returned `Vec` is a move and the dead set spans the function**, so an early `(return v)` on one branch kills
|
||||
the binding at the foot of another. `replace-bytes` guards its empty needle with an `if` rather than a
|
||||
`when`/`return` for that reason.
|
||||
- ~~**A returned `Vec` is a move and the dead set spans the function**~~ Repealed 2026-09-18; the shape compiles
|
||||
now and `replace-bytes`'s `if` guard is a harmless leftover.
|
||||
|
||||
### The refusal block is down from eight reasons to four
|
||||
|
||||
|
||||
@ -1,6 +1,9 @@
|
||||
# Spec 1 — Ownership, containers, and copies
|
||||
|
||||
Status: **frozen**. Closes plan.org open decisions #6 and #10, and resolves the
|
||||
Status: **frozen**, with one amendment: **the repeal of 2026-09-18** (see "The
|
||||
repeal", below), which removed the static flow analysis — use-after-move and
|
||||
double-free are no longer compile errors. Everything structural in this
|
||||
document still governs. Closes plan.org open decisions #6 and #10, and resolves the
|
||||
contradiction between "value structs copy on assignment" and owning containers.
|
||||
The Allocators section additionally settles the four things that had to be
|
||||
decided before `Vec` and `Map` are written: when storage is released, the `drop`
|
||||
@ -26,9 +29,13 @@ 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**. Binding, passing, or returning one
|
||||
transfers ownership; the source binding is dead afterwards and using it is a
|
||||
compile error. There is no shallow copy, so there is no double free.
|
||||
- `(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
|
||||
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.
|
||||
|
||||
## Maps — first implementation
|
||||
|
||||
@ -106,15 +113,14 @@ region" for the rule that stands in its place and for what it costs.
|
||||
|
||||
## Globals of move-only type
|
||||
|
||||
A global may be a `Vec` or a `Map`, and **reading one is always a borrow, never
|
||||
a move**. Nothing can take ownership of it, so nothing can `free` it; its
|
||||
lifetime is the process's and it is never released. That is one rule rather than
|
||||
a general ownership model for globals, and it is sound for the reason a general
|
||||
model would be needed and is not: the lifetime question has a constant answer.
|
||||
Passing a global to a function that owns its parameter, binding it to a local,
|
||||
returning it and freeing it are all refused at the read, which is exactly where
|
||||
a move would have been recorded for a local. `(clone g)` is the one of these
|
||||
that yields something another owner may have.
|
||||
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
|
||||
that: reading one was always a borrow, so nothing could take or free it. Since
|
||||
the repeal the intent is unchanged and the enforcement is manners: passing,
|
||||
binding, or freeing a global type-checks, and a program that frees one while
|
||||
other code still reads it has the ordinary use-after-free it would have with
|
||||
any other value. `(clone g)` remains the way to get something another owner
|
||||
may have.
|
||||
|
||||
Such a global is **mutable in place**: `push`, `put`, `reserve` and `set` all
|
||||
take their target as a borrow, so a global `(Vec u8)` is filled and grown where
|
||||
@ -139,6 +145,40 @@ outlive `main` — nothing re-runs between one entry and the next, so a re-enter
|
||||
`main` finds the global as it left it. Assigning a second time overwrites the
|
||||
first block and leaks it; there is no `drop`, and freeing is a thing you write.
|
||||
|
||||
## The repeal — 2026-09-18
|
||||
|
||||
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
|
||||
globals. It made use-after-move and double-free compile errors. It was removed,
|
||||
and removed rather than repaired, after one day's bug hunt found four
|
||||
structural holes in it (a move hidden in a borrowed target's subtree, the same
|
||||
hole through a global, a `while` condition outside the loop rule, and the
|
||||
region guard never asking about elements — docs/BUGS-2026-09-18.md). Each was
|
||||
fixable; the shape of the four together said the analysis would keep growing
|
||||
holes, and a checker that sometimes misses is worse than none, because it is
|
||||
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,
|
||||
`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.
|
||||
|
||||
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
|
||||
removed here changed what an accepted program means, so a stricter pass can
|
||||
return without changing the language, only its acceptances.
|
||||
|
||||
## Taking an address
|
||||
|
||||
`(addr x)` yields `(Ptr T)` for any assignable place `x` — a local, a global, a
|
||||
@ -334,10 +374,10 @@ There are exactly two release points, and neither of them is a scope.
|
||||
(a `Texture2D`, a socket, a file handle — see `drop` below). For a value that
|
||||
holds a resource and no storage, `free` runs `drop` and nothing else; it is
|
||||
still the release operation, and it is how a `Texture2D` in a local is
|
||||
released. `free` consumes its argument exactly as any other move does: the source
|
||||
binding is dead afterwards and using it is a compile error. That rule is
|
||||
already what makes a double free unrepresentable, so `free` needs no new
|
||||
analysis.
|
||||
released. Since the repeal, `free` consumes at run time only: nothing marks
|
||||
the binding dead, and a second `free` or a later read through it is a
|
||||
run-time misbehaviour the allocator or the dev build catches, not a compile
|
||||
error.
|
||||
2. **Region release** — `(free-all a)` on an allocator, which releases
|
||||
everything made from it at once, including storage reachable from bindings
|
||||
that are still in scope. The per-frame `(free-all context/temp)` at the top
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user