diff --git a/FABRIC-2.md b/FABRIC-2.md index 78af291..add668e 100644 --- a/FABRIC-2.md +++ b/FABRIC-2.md @@ -232,7 +232,10 @@ and recorded. > tactics tried, and the explicit-quantifier form sidesteps that mechanism entirely. > > **Two genuine, non-tactical bugs found and deliberately left `oops`-flagged rather - > than fixed, each documented in place with a full explanation:** + > than fixed, each documented in place with a full explanation.** ***Both resolved the + > same day, 2026-08-13 — corrected here 2026-08-18, found stale during a docs-tree sweep; + > FABRIC-2.md had never been updated to match, even though both `.thy` files themselves + > record the fix in place.*** No live `oops` remains anywhere in `proof/` today. > - `StarForth_Stack_Words.thy`'s `roll_two_is_rot` — a three-way inconsistency between > `forth_roll_def`'s own index arithmetic (off-by-one against what the lemma expects), > the lemma's own expected ROT-equivalent output, and the real C `stack_word_roll` @@ -240,13 +243,30 @@ and recorded. > bottom-indexed convention ("1-indexed from bottom: n=1 moves bottom item to top") > matching neither. Not a proof-script issue — a genuine open question about what > `ROLL` is supposed to do, needing a decision before it can be closed either - > direction. + > direction. ~~Genuine open question.~~ **RESOLVED 2026-08-13**: `forth_roll_def` + > rewritten to match the real C's bottom-indexed convention exactly (traced from + > `stack_words.c:291-320`, its own comment is explicit: "1-indexed from bottom: n=1 + > moves bottom item to top") — a deliberately different operation from the + > standard/gforth "count from top" ROLL, not a bug in either the C or the original + > lemma's expectation, just two different definitions of ROLL that needed reconciling + > toward the real one. `roll_two_is_rot` now proves. > - `StarForth_Loop4_Pipeline.thy`'s `pm_record_hit_preserves_wf`/ > `pm_record_miss_preserves_wf` — `pm_wf` only requires `pm_last_accuracy_den > 0` > when `pm_prefetch_attempts > 0`; both operations increment `attempts` from 0 to 1 > without ever having required `den > 0` beforehand, so the postcondition needs > something the precondition never guaranteed. A genuine invariant-maintenance gap in - > `pm_wf`'s own definition, not fixed here. + > `pm_wf`'s own definition, not fixed here. **RESOLVED 2026-08-13**: both lemmas gained + > an explicit `pm_last_accuracy_den pm > 0` hypothesis, matching the precondition to + > what the postcondition actually needs — the invariant-maintenance gap this bullet + > describes, closed by stating it rather than by strengthening `pm_wf` itself. **A + > deeper, previously untracked issue surfaced by this fix, still open**: the model's + > `pm_last_accuracy_num`/`pm_last_accuracy_den` fraction pair does not correspond to the + > real C struct at all — `PipelineGlobalMetrics` (`include/vm.h`) has a single `double + > last_checked_accuracy` field, no num/den pair anywhere (confirmed against + > `src/vm_bootstrap.c:290-295`, `src/vm_time.c:412-413,627-628`). Flagged in the `.thy` + > file itself as its own separate future task ("a full field-level pass over + > `pipeline_metrics_state`"), not attempted as a side effect of this fix, and not + > tracked anywhere outside that one code comment until now. > > Toolchain: `/home/rajames/CLionProjects/Isabelle2011-1` now genuinely runs > Isabelle2025-2 (old 2011 install preserved as `Isabelle2011-1.old`). Gitea Actions CI @@ -311,6 +331,13 @@ and recorded. > structurally different DF usage — dispatch reassignment via a stored pointer, not a > plain value). Full suite: 54 theories, green. > + > **Theory count reconciled 2026-08-18** — this entry's own running count (53 here, then + > 54 two paragraphs up) reflects the suite's state at each point in this multi-session + > sweep, not a final figure; neither is current. **The actual, current count is 52** (`proof/` + > file count matches `proof/ROOT`'s registration exactly, verified directly, no orphans, no + > gaps) — matching `proof/COVERAGE.md`'s own count. `proof/FINDINGS.md` still says 53; + > that file was not corrected here (out of this pass's scope; flagged, not fixed). + > > **Continued, commit `6f59e4f`.** IS/DEFER@ (`StarForth_Defer_Words.thy`) now modelled > end to end too, sidestepping the FIND-family name-resolution gap (still itself > unmodelled everywhere in this suite) the same way `physics_freeze_words.c`'s diff --git a/docs/CLAUDE.md b/docs/CLAUDE.md index 7cd2711..67fef4b 100644 --- a/docs/CLAUDE.md +++ b/docs/CLAUDE.md @@ -42,15 +42,33 @@ is audience and stability, not quality. ## Makefile Targets +**Corrected 2026-08-18** — this section previously described a `docs/Makefile` with +`docs-formal`/`docs-working`/`docs-index`/`docs-audit`/`docs`/`docs-clean` targets. That file +does not exist and none of those targets exist anywhere in the tree. The real build lives one +level down, at `docs/formal/Makefile`, with a different target set entirely: + ``` -make docs-formal — build all three LaTeX volumes → PDFs in formal/build/ -make docs-working — render working/ markdown to HTML (optional, low priority) -make docs-index — generate docs/INDEX.md inventory of all doc files -make docs-audit — list files tagged OBSOLETE or SUPERSEDED in INDEX.md -make docs — run docs-formal + docs-index -make docs-clean — remove formal/build/ artifacts +# Run from docs/formal/ + +make — everything: all three volumes + books + standalone docs + doxygen +make vols — vol1 + vol2 + vol3 (the three-volume LaTeX set) +make vol1 — Volume I only +make vol2 — Volume II only +make vol3 — Volume III only +make books — dev-guide + user-guide + cookbook +make standalone — experiments + proofs + ssrn + patent (standalone LaTeX docs) +make doxygen — API reference PDF (requires the `doxygen` binary installed; + runs doxygen → fix-doxygen-unicode.py → doxygen/latex → PDF) +make clean — remove build artifacts ``` +`docs/working/` has no build step of its own (no HTML rendering target exists) — it's read +directly as markdown. `docs/INDEX.md` exists but is maintained manually, following this +file's own Phase 1 triage process below — there is no `docs-index`/`docs-audit` automation +that generates or checks it; treat `INDEX.md` as something a triage pass produces by hand, +and expect it to go stale between passes (confirmed stale as of this correction — check its +own date against `git log -1` before trusting it). + --- ## Phase 1: Triage (DO THIS FIRST)