wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, affine i*n+k); unbuilt and untested

1 files changed, 1 insertions, 1 deletions

diff --git a/docs/SPEC.md b/docs/SPEC.md
index 7f37e33..06ee11c 100644
--- a/docs/SPEC.md
+++ b/docs/SPEC.md
@@ -667,7 +667,7 @@ int y = 7; asm { y @ 1 + y ! }    // y is 8
 
 4.15.2 the runtime, the core, the compiler, the language server, `run.zc` and `build.zc` are unbounded; std, icon and actor are checked except where a function reads headers on purpose.
 
-4.15.3 the compiler drops a check it can prove, and never changes when a check that can fail faults. a check is dropped for a constant index inside the array or the block; in a loop `for (...; i < b; i++)` whose body leaves `i`, `b` and the array alone (it assigns, increments or takes the address of none of them, and makes no closure), for `a[i]` when `b` is `len(a)`, or a constant no larger than a fixed array's length, or than the requested size of the block a pointer was set from (never a rounded block size). for a pointer the body must also call nothing, since a call might free or resize the block. when `b` is an `int` variable, the check of `a[i]` against `n` elements is hoisted: the loop entry works out once whether `0 <= i` and `b <= n`, and the check runs on each access only when that failed, so a fault still comes at the same access, after the same side effects.
+4.15.3 the compiler drops a check it can prove, and never changes when a check that can fail faults. a check is dropped for a constant index inside the array or the block; in a loop `for (...; i < b; i++)` whose body leaves `i`, `b` and the array alone (it assigns, increments or takes the address of none of them, and makes no closure), for `a[i]` when `b` is `len(a)`, or a constant no larger than a fixed array's length, or than the requested size of the block a pointer was set from (never a rounded block size). `b` may be `len(a)` written in the test itself, or the `len()` of another fixed array whose length is a known constant no larger than the one indexed. the length of `new(fixed T[?], n)` with a constant `n` is known like the size of a block. the loops may nest to any depth; every loop between the access and the one the size is known at must leave the array or pointer alone. an index `i * n + k` (sums and products of proved loop indices and constants, none negative) is dropped when its largest value is inside the array or block, as for `i < n`, `k < n` into exactly `n * n` elements; with a variable `n` the check stays. for a pointer the body must also call nothing, since a call might free or resize the block (any call: the block may be one another pointer aliases). when `b` is an `int` variable, the check of `a[i]` against `n` elements is hoisted: the loop entry works out once whether `0 <= i` and `b <= n`, and the check runs on each access only when that failed, so a fault still comes at the same access, after the same side effects.
 
 4.15.4 `zy --explain-checks [file] < source` compiles the unit, does not run it, and prints the checks the compiler kept, from the same analysis that drops the others, as json lines (format version 1). the first line is `{"version":1}`. each further line is one object for one kept check, in source order: `file` (the name given, default `<eval>`), `line`, `col` (from 1, of the `[`), `end_line`, `end_col` (just past the `]`), `fn` (the function; `<closure>` or `<eval>` outside a named one), `kind` (`index` for an array, `pointer` for a pointer), `loop_depth` (enclosing loops), `reason`, `fix` (prose), and optionally `edit` (`{"range":{"line":..,"col":..,"end_line":..,"end_col":..},"text":".."}`), present only for a purely mechanical fix. the reasons: `index-not-loop-variable` (the index is not the variable of an enclosing `for (i = ..; i < b; i++)`), `bound-not-invariant` (the body changes the index, the bound or the array, takes an address or makes a closure), `index-not-len-derived` (the bound is not `len()` of the array or a small enough constant), `size-unknown` (a pointer whose block size the compiler does not know), `pointer-may-be-freed` (the body calls something that might free or resize the block), `packed-elements` (sized-integer elements, always checked by the runtime) and `hoisted-to-loop-entry` (kept, but it runs only when the check at the loop entry failed). checks in included files, in unbounded code and in o3 code (which implies unbounded) are not listed. version 1 is stable: new kinds, reasons and fields may appear, and a consumer ignores a kind, a reason or a field it does not know.