diff --git a/FABRIC-2.md b/FABRIC-2.md index 31df557..d37986d 100644 --- a/FABRIC-2.md +++ b/FABRIC-2.md @@ -179,6 +179,67 @@ and recorded. > Isabelle2025-2 (old 2011 install preserved as `Isabelle2011-1.old`). Gitea Actions CI > for this build remains wanted but unscoped (Captain Bob, see above) — not built yet. + > **PROCESS CORRECTION 2026-08-14/15 — the word-source coverage sweep below should have + > been tracked here from the start and was not; recorded now, retroactively, per §25.0's + > own rule that new findings/decisions land in this document.** Across several sessions + > (2026-08-14 through 2026-08-15) the proof suite was extended file-by-file to cover + > every file in `src/word_source/*.c` (34 files; `q48_16_words.c` deliberately excluded, + > it's the underlying math library, not a FORTH words file) — this was a *different* goal + > from 5.2's original "one datatype, one index space, one conservation theorem" framing + > (a Stadium-cell-model proof), and got tracked only in session memory instead of here. + > That memory is `project_isabelle_hol_proof_suite.md` in this machine's Claude memory + > store, if the full blow-by-blow is ever needed; the summary below is what matters for + > this document. + > + > **Sweep complete, commit `346c793`: all of `src/word_source/*.c` covered, 53 theories + > green.** Two deliverables followed, `proof/FINDINGS.md` (commit `3426d6a`) and + > `proof/COVERAGE.md` (same commit) — an aggregated cross-cutting-findings write-up and a + > coverage/purpose index, both requested by Captain Bob once the sweep was far enough + > along. + > + > **Repair pass, commit `dfdabcc` — low-risk defects only, per Captain Bob's explicit + > scope call.** `DECAY-RATE@` (`physics_freeze_words.c`) had a genuine missing + > stack-overflow guard (raw push, no `ds_full` check, unlike its neighbors in the same + > file) — fixed. Removed `dictionary_manipulation_words.c`'s dead, permanently-shadowed + > `[`/`]`/`STATE` and `defining_words.c`'s dead, permanently-shadowed `DEFER`/`IS`/ + > `DEFER@` (plus the now-orphaned `defining_runtime_defer` helper, which would have + > triggered an unused-static-function warning under `-Wall -Werror` if left behind) — + > both confirmed unreachable via `word_registry.c`'s registration order and FORTH's + > newest-first dictionary lookup, zero behavior change. **Correction caught mid-pass and + > worth recording**: ~14 of the sweep's ~15 "missing overflow guard" findings turned out + > to be false positives — `vm_push()`/`VM_PUSH` already bounds-check internally in every + > build this repo currently ships (`STARFORTH_PERFORMANCE`, the one flag that would + > disable that check, is never defined by any Makefile/Kconfig target here) — the proof + > model just hadn't credited that. Corrected in the `.thy` files and `FINDINGS.md`, not + > silently left overstated. Three-architecture QEMU acceptance: all three booted clean to + > `ok>` with an **identical** `dict_hash=0x24b4279f0670aa3a` and identical + > `1003/965/0/0` self-test totals — `logs/20260814-195128/amd64`, + > `logs/20260814-201210/aarch64`, `logs/20260814-202224/riscv64`. + > + > **Coverage-sweep continuation into structural gaps, commits `cc46cf8`/`1aca77d`/ + > `d3d66fb`/`d59a913` — proof-only, no C changes, no QEMU boot needed for these.** + > Dictionary insertion (`vm_create_word`) had never been modelled anywhere in the + > suite — every prior file only ever *read* the abstract `dictionary` table. + > `dict_insert_entry` now models the word_id-assignment/table/`latest_id`/ + > `word_id_next`-counter mechanism, reusing a `word_id_next` field that had been declared + > in `StarForth_Base.thy` since early in the sweep but never once written. Separately, + > `input_buffer`/`input_length`/`input_pos` (the TIB) turned out to be plain per-VM + > array/scalar fields, not host pointers as assumed everywhere else in the sweep, and + > `vm_parse_word` a pure scan — modelled as `forth_parse_word`. Composed together + > (plus a new `de_df :: cell` field on `dict_entry` and `dict_write_df` for the + > data-field write, and `current_executing_word_id` on `vm_state`), **CREATE, VARIABLE, + > and CONSTANT are now the first three fully-modelled words in + > `StarForth_Defining_Words.thy`** — guard through parse through insertion through the + > data-field write, matching the real C exactly, nothing left unmodelled per word except + > the pin-shadow name-scan guard (sidestepped via an explicit `bool` parameter, the same + > technique already used for the XT-pop gap elsewhere in this suite). `:` and DEFER are + > closed to the same point minus one remaining per-word gap each (`:` needs a + > `vm->compiling_word`-tracking field that doesn't exist yet; DEFER's own runtime is a + > structurally different DF usage — dispatch reassignment via a stored pointer, not a + > plain value). Full suite: 54 theories, green. Not yet done: IS/DEFER@ (need the + > FIND-family name-resolution gap first), the vocabulary-chain mechanics, the + > block-window cache, the hot-words cache — each flagged as its own project, not started. + - [ ] **5.3 — Shrink the subsystem documents.** `ARTEMIS.md`, `HERMES.md`, `CONSOLE.md`, `TRIPOD.md` need trimming now that `FABRIC-2.md` (via `FABRIC.md`) is the design-of-record. Not started. **Specific pending edit found within this item:** `TRIPOD.md`'s own Immediate