aboutsummaryrefslogtreecommitdiff
path: root/docs
diff options
context:
space:
mode:
authorGravatar Moon Flower <moonflower@elhenney.local> 2026-10-14 09:02:46 +0330
committerGravatar Moon Flower <moonflower@elhenney.local> 2026-10-14 09:02:46 +0330
commitdb89626d1be6f0c700d11134cac07e57d09315ba (patch)
tree860c51f8468f165087db6c9aa1e15de512096660 /docs
parentbuild: generate everything into build/, keep src/ free of generated files (diff)
docs: record the two ownership gaps that block the bootstrap
`make genome` cannot complete: the second bootstrap stage runs the lifetime checker over the compiler's own source, which reports 8 errors, and mkgenome then reads the diagnostics as an image. the two limits are that an owned value held in a local has no move into another local — every accepted move originates at a call, so the free-then-replace rule only applies when the replacement comes from a call result — and that a local cannot be lent to a global, so redirecting the output stream at a scratch buffer needs a module-level variable. neither limit accepts an unsafe program; both refuse correct ones, so this is a completeness gap rather than a soundness failure. document the affected code, the diagnostics, what was tried and how each attempt failed, and a proposal. add src/tools/bootstrap-check.sh, which rebuilds both bootstrap stages and prints the compiler's diagnostics on its own source instead of the word dump.
Diffstat (limited to 'docs')
-rw-r--r--docs/BOOTSTRAP-OWNERSHIP.md155
-rw-r--r--docs/BORROW.md2
2 files changed, 157 insertions, 0 deletions
diff --git a/docs/BOOTSTRAP-OWNERSHIP.md b/docs/BOOTSTRAP-OWNERSHIP.md
new file mode 100644
index 0000000..509db2f
--- /dev/null
+++ b/docs/BOOTSTRAP-OWNERSHIP.md
@@ -0,0 +1,155 @@
+# the bootstrap does not compile: owned values cannot be moved between locals
+
+status: open, blocks `make`
+affects: `make genome`, the `fixpoint` check, the `genome.h is up to date` check
+see also: `docs/BORROW.md`
+
+## summary
+
+`make` bootstraps the compiler with `zc0` compiling `src/runtime/rt.zc`,
+`src/core/core.zc` and `src/compiler/compiler.zc` into a stage-0 image, stage-0
+becoming `build/zy0`, and `zy0` compiling the same three files again into the
+genome. the second compilation runs with lifetime checking enabled and rejects
+the compiler's own source. `bin/mkgenome` then reads the diagnostics as if they
+were an image:
+
+```
+mkgenome: input is not a genome for this map
+```
+
+the real output of `zy0` is a diagnostic list, not an image. nothing after the
+fixpoint can run, so a checkout with no prebuilt genome cannot be built.
+
+this is a completeness gap in the ownership rules, not a soundness failure. the
+checker is refusing correct programs; it is not accepting unsafe ones. the
+practical cost is that the compiler can no longer compile itself.
+
+## the affected code
+
+`methdef` in `src/compiler/compiler.zc` reassembles a typed generic method's
+token list. it saves the output stream state, redirects the stream at a scratch
+buffer, renders the return type into it, splits the result into tokens, builds a
+replacement buffer that interleaves the new tokens with the old ones, and hands
+the replacement back in place of the original.
+
+```zc
+word output = rt.outbuf, grow = rt.outgrow, buffer = rt.new(4096), return_tokens, joined;
+rt.outmode = 2; rt.outbuf = m*buffer; rt.outn = 0; rt.outcap = 4095; rt.outgrow = 0;
+tprint(rty); if (rtag) rt.put_s(".u"); buffer[rt.outn] = 0;
+rt.outmode = mode; rt.outbuf = output; rt.outn = length; rt.outcap = capacity; rt.outgrow = grow;
+return_tokens = tokens(buffer);
+...
+joined = rt.new((r[0] + return_tokens[0]) * 3 + 1);
+...
+word previous = m*r; r = d*joined; rt.free(return_tokens); rt.free(buffer); rt.free(previous);
+```
+
+three separate moves are needed here, and each one hits a different limit:
+
+1. lend the local scratch buffer to the output stream, then keep using it
+2. replace `r`, an owned local, with `joined`, another owned local
+3. store the local block into the global code-block list
+
+## what the checker reports
+
+```
+zc: line 5571: buffer: used after it was given away; owner buffer was transferred on line 5570 (declared on line 5569)
+zc: line 5573: buffer: used after it was given away; owner buffer was transferred on line 5570 (declared on line 5569)
+zc: line 5589: r: is an owned object and can't be copied into another variable
+zc: line 5589: r: still owns an object; overwriting it would leak it
+zc: line 5589: buffer: used after it was given away; owner buffer was transferred on line 5570 (declared on line 5569)
+zc: line 5590: joined: d object was never given away
+zc: line 10572: only a named owned object can be recast
+zc: line 10575: only a named owned object can be recast
+zc: 8 errors
+```
+
+the line numbers are into the concatenation, not into `compiler.zc`. subtract
+1401 lines: 5570 is `rt.outbuf = m*buffer;`, 5589 is the `previous` line, and
+10572 and 10575 are `rt.code_blocks = m*block;` in `syntax_resident`.
+
+## what was tried
+
+| change | result |
+|---|---|
+| `rt.outbuf = buffer;` — drop the `m*` | still reported as a transfer; any owned value assigned into a global transfers, and a second diagnostic appeared at the following line |
+| move the scratch buffer to a module global `rbuf`, assign it plainly, borrow it into `rt.outbuf` | accepted; removes five of the eight errors. this is the existing idiom, see `sgb` at `sig_attach` and `ltxt` in the literal pool |
+| `word previous = m*r; r = d*joined; rt.free(previous);` unchanged | `initial declarations still cannot copy an owned local`, per BORROW.md line 30 |
+| declare `previous` in the block's declaration list, then `previous = m*r;` | `r: is an owned object and can't be copied into another variable` |
+| `rt.free(r); r = joined;` — the documented free-then-replace idiom | `joined: is an owned object and can't be copied into another variable`, and `r` is then reported as given away at its next use |
+
+## is this a borrow checker issue
+
+yes, and it is worth separating two kinds of gap.
+
+**a move between two locals has no syntax.** the accepted moves in the
+compiler's own source all originate at a call:
+
+```zc
+word p = m*rt.new(capacity); // src/compiler/compiler.zc:644
+buf = m*inc_open(full); // src/compiler/compiler.zc:4632
+dgbuf = chk_resize(dgbuf, dgpos, cap) // src/compiler/compiler.zc:401
+rt.free(d*buf); // src/compiler/compiler.zc:4447
+```
+
+an owned value already held in a local can be disposed with `d*`, but it cannot
+be handed to another local, and it cannot replace one. the free-then-replace rule
+in BORROW.md line 30 covers `rt.free(buffer); buffer = replacement;` — but only
+when `replacement` arrives from a call. with a local on the right-hand side the
+same rule rejects the assignment and then reports the destination as given away.
+
+the replacement built here is a genuine local: it is written field by field and
+then has to become `r`. no current spelling expresses that. the shortest
+workaround is to route the swap through a call that takes both pointers and
+returns the survivor, so the move originates at a call result.
+
+**a local cannot be lent to a global.** the output stream is global state.
+redirecting it at a local scratch buffer is a borrow, not a transfer, but every
+spelling is a transfer:
+
+- `rt.outbuf = m*buffer;` transfers, so every later use of `buffer` is a use
+ after transfer
+- `rt.outbuf = buffer;` also transfers
+- the three working redirects in the compiler all assign a global or a pointer
+ derived from one — `rt.outbuf = dgbuf + dgpos + 5;`, `rt.outbuf = sgb;`,
+ `rt.outbuf = ift + at;`, `rt.outbuf = ltxt;`
+
+so the scratch buffer has to live at module scope. that is workable here, and it
+is what the module-global `rbuf` change adopts, but it costs something the
+local version did not: the buffer is shared state for the duration of the call,
+so any reentrancy through `methdef` would collide, and the checker cannot see
+that the borrow ends at the restore.
+
+## proposal
+
+in rough order of value:
+
+1. allow a move into an existing local when the source is an owned local and the
+ destination's previous owner is released in the same statement list, generalizing
+ the free-then-replace rule beyond call results. this alone resolves the
+ `methdef` reassembly.
+2. allow a global to hold a borrow of a local for a bounded region, so an output
+ stream can be pointed at a scratch buffer without a module-level variable. a
+ scoped-borrow rule on assignment into a global field would do it, and it removes
+ the reentrancy hazard that the module-global workaround introduces.
+3. give `rt.code_blocks = m*block;` a supported spelling. the error, `only a named
+ owned object can be recast`, does not describe what is wrong: `block` is named and
+ owned. it is used again at `here = block + 3;` two lines later, which is the real
+ constraint, and the diagnostic should say so and point at the later use.
+
+none of these accept a program that is currently accepted unsafely. each widens
+the set of programs the checker can describe. item 3 is also a message bug
+independent of the rule change: a wrong diagnostic on a correct-looking transfer.
+
+## reproducing
+
+`src/tools/bootstrap-check.sh` rebuilds the two bootstrap stages and prints the
+compiler's diagnostics on its own source instead of the word dump. it exits
+through `mkgenome` when the image is malformed, which is the same failure `make`
+reports.
+
+```
+bash src/tools/bootstrap-check.sh
+```
+
+a passing run prints `image ok: <n> bytes`. \ No newline at end of file
diff --git a/docs/BORROW.md b/docs/BORROW.md
index 818eea4..10beb84 100644
--- a/docs/BORROW.md
+++ b/docs/BORROW.md
@@ -41,6 +41,8 @@ the compiler functions, standard library, and language server currently run with
the analysis runs with the existing parser, ownership checker, and lifetime records; it does not have a separate source parser or a complete path-sensitive proof. snapshots conservatively join branches and loops. low-level and unknown boundaries can hide behavior, so a quiet diagnostic set is not a whole-program safety proof. zc is single-threaded; shared closure cells do not define concurrent mutation rules.
+two completeness limits block the compiler from compiling itself, and are written up in `docs/BOOTSTRAP-OWNERSHIP.md`. an owned value already held in a local has no move into another local; every accepted move originates at a call, so the free-then-replace rule above applies only when the replacement comes from a call result. and a local cannot be lent to a global, so an output stream has to be redirected at a module-level buffer rather than a scratch local. neither limit accepts an unsafe program; both refuse correct ones.
+
the maintained regressions cover these cases:
| case | behavior |