diff options
| author | 2026-10-14 20:03:35 +0330 | |
|---|---|---|
| committer | 2026-10-14 20:04:11 +0330 | |
| commit | 70400c5f382f23c1a72e8a948b41d8039e39e94d (patch) | |
| tree | d824cbe3aada9fb357954c700ebeac985cc59f84 /TODO.md | |
| parent | explain-checks: the record writer moves to src/lib/explain.zc, embedded and c... (diff) | |
detach doc comments on internal bounds helpers (genome size); todo: reuse capture_scan in the body scanner
Diffstat (limited to 'TODO.md')
| -rw-r--r-- | TODO.md | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -534,7 +534,7 @@ brief someone without re-reading the code. - fib is slightly slower under o3 than plain (0.86 against 0.78 ms), likely region entry and exit on every recursive call; related to direct o3-to-o3 calls. - a compiled o3 region that stores into its own code finishes the current activation on the old code; the change takes effect on the next entry. either document it or bail to the region interpreter when the hook drops the running region. - [ ] (in progress on work/exactsize) exact-size bounds checks: n is stored in p[-4] bits 32..62 and the check is 2 loads. -- [ ] (on work/checks) bounds checks out of loops and `--explain-checks`. done: a for loop's body is read ahead (`body_scan` in analyzer.zc) for the names it assigns, increments or takes the address of, closures, and anything that might free a block (calls, push/pop/resize/defer/asm/quote/new, stores to locals that can own); loop proofs now need a body that leaves the index, the bound and the array alone (before, a body that moved the index after a proved access was unchecked on the next iteration). `i < n` with an int n hoists the check to a flag computed at the loop entry (`hoist_guard`, `hoist_stub`): the check still runs, in place, when the flag says it can fail, so faults and side effects keep their order. a pointer set from `rt.new(n)` with a constant n is proved by `i < k` (k <= n) or hoisted, using the requested size (never the rounded block size), and only when the body cannot free or resize anything. `zy --explain-checks [file] < src` prints the kept checks as json lines from the same decisions (format v1 in docs/SPEC.md 4.15.4; consumers ignore unknown kinds, reasons and fields; `o3-candidate` is a possible future kind). later: hoisting for growable arrays with a variable bound, `while` loops, pointer sizes from `len()` once exact sizes land, mechanical `edit`s, tracking ownership precisely enough to hoist past calls that cannot free. +- [ ] (on work/checks) bounds checks out of loops and `--explain-checks`. done: a for loop's body is read ahead (`body_scan` in analyzer.zc) for the names it assigns, increments or takes the address of, closures, and anything that might free a block (calls, push/pop/resize/defer/asm/quote/new, stores to locals that can own); loop proofs now need a body that leaves the index, the bound and the array alone (before, a body that moved the index after a proved access was unchecked on the next iteration). `i < n` with an int n hoists the check to a flag computed at the loop entry (`hoist_guard`, `hoist_stub`): the check still runs, in place, when the flag says it can fail, so faults and side effects keep their order. a pointer set from `rt.new(n)` with a constant n is proved by `i < k` (k <= n) or hoisted, using the requested size (never the rounded block size), and only when the body cannot free or resize anything. `zy --explain-checks [file] < src` prints the kept checks as json lines from the same decisions (format v1 in docs/SPEC.md 4.15.4; consumers ignore unknown kinds, reasons and fields; `o3-candidate` is a possible future kind). later: hoisting for growable arrays with a variable bound, `while` loops, pointer sizes from `len()` once exact sizes land, mechanical `edit`s, tracking ownership precisely enough to hoist past calls that cannot free. cleanup: let the `bs_*` body scanner reuse capture_scan's token skipping instead of its own (about 0.5 to 1k genome words). the `--explain-checks` writer is `src/lib/explain.zc`, embedded and compiled only in that mode (a unit that defines its own `explain` namespace would clash with it). - [ ] (in progress on work/bench) `make bench`, `bench-check` and `bench-selftest`: baseline from ec49c6d, jit and llvm rows, interp rows only with `INTERP=1`. follow-up: fill the checks column from `--explain-checks` and re-save the baseline; the rule that fails when the check count rises is already in bench-check. - [ ] lsp and vscode bounds hints: diagnostics for kept checks with an all / loops / off setting, quick fixes, and a hot-checks command; the vscode extension supports all of it. later: `o3-candidate` hints for hot loops outside o3. - [ ] hoisting v2: use the u/m/d ownership tags to prove a loop can't free a pointer (v1 refuses to hoist when the loop body has any free, release or realloc, or any call that might free). |
