Process correction: the sweep (proof/FINDINGS.md, proof/COVERAGE.md, the
low-risk repair pass, and the dictionary-insertion/TIB/DF gap-closure
continuation -- commits 346c793 through d59a913) was tracked only in
session memory instead of here, contrary to \S25.0's own rule that new
findings and decisions land in this document. Added retroactively under
item 5.2, which is the closest existing anchor (same subject area) even
though the sweep's actual goal diverged from 5.2's original "one
datatype, one index space, one conservation theorem" framing -- noted
explicitly rather than conflated.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adds de_df :: cell to dict_entry (StarForth_Base.thy) -- the DF cell
modelled as a plain value, closing gap (b) for every word that only
reads/writes it through its OWNING entry. Confirmed by grep this record
has exactly one construction site in the whole 52-theory suite
(dict_insert_entry), so the field addition's blast radius is contained
to StarForth_Defining_Words.thy alone -- full suite still verifies
unchanged elsewhere.
dict_write_df writes an existing entry's DF by word_id. forth_create_full/
forth_variable_full/forth_constant_full now compose the DF write in,
making CREATE/VARIABLE/CONSTANT the first three FULLY modelled words in
this file (guard through parse through insertion through the DF write --
nothing left unmodelled per word except the pin-shadow name-scan guard,
sidestepped the same way as everywhere else in this suite).
Their runtime companions (defining_runtime_create/_variable/_constant --
confirmed byte-identical C bodies) share one new definition,
forth_runtime_read_df, gated on ds_full matching vm_push's real internal
check. Required adding current_executing_word_id to vm_state (mirrors
vm->current_executing_entry, word-id-indexed like latest_id).
DEFER and : remain at their previous closure level: DEFER's DF write was
already implicitly closed (de_df=0 at creation matches its explicit
*df=0), but its own runtime is a fundamentally different DF usage
(dispatch reassignment via a stored pointer, gap c, not a plain value);
: has no vm_state field for vm->compiling_word tracking.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Extends the CONSTANT worked example from the previous commit to all five
name-parsing/entry-creating words. Each now has a forth_*_full definition
composing the real C order end to end, up to but not including the
data-field write (gap b, still open):
- forth_create_full: parse -> dict_insert_entry -> forth_align (reused
directly from StarForth_Dictionary_Words.thy's ALIGN model).
- forth_variable_full: parse -> forth_align -> forth_vm_allot_raw (new --
models the raw vm_allot() C helper VARIABLE calls directly, bounds-
checked against DICTIONARY_MEMORY_SIZE exactly like vm_align, distinct
from the FORTH word ALLOT's own VM_MEMORY_SIZE-bounded forth_allot) ->
dict_insert_entry.
- forth_colon_full: nested-':' guard (checked before the parse, matching
real C order) -> parse -> forth_colon_entry_half (mode-set + WORD_SMUDGED
insert). Added forth_parse_word_preserves_vm_mode/dictionary/
word_id_next to StarForth_Base.thy to support this composition cleanly.
- forth_defer_full: parse -> dict_insert_entry, the simplest of the five.
dict_insert_entry's callers (the four forth_*_entry_half definitions)
still take the parsed name as a caller parameter for standalone use.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
input_buffer/input_length/input_pos (include/vm.h:415-417) turned out to
be plain per-VM array/scalar fields, not host pointers -- unlike almost
every other input-adjacent gap in this suite. vm_parse_word (src/vm.c:
137-160) is a pure whitespace-delimited scan over them, now modelled as
forth_parse_word in StarForth_Base.thy (is_ws + dropWhile/takeWhile,
faithful to the C's skip-then-copy-with-truncation loop, including that
input_pos only advances past a truncated token by what was actually
copied, matching the C's `len < max_len - 1` bound exactly).
dict_insert_entry (added last session) now takes the entry's name as a
parameter instead of hardcoding the empty string. forth_constant_full
composes forth_parse_word with dict_insert_entry end-to-end as a worked
example: CONSTANT's real order (stack-underflow guard -> pop value ->
parse name -> vm_create_word) is modelled in full up to the data-field
write, which remains the one still-open gap. The other four entry-half
definitions (:/CREATE/VARIABLE/DEFER) take the parsed name as a caller
parameter for now rather than repeating the same composition four more
times in one pass.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Every prior file in the word-source sweep only ever read the abstract
dictionary table; none modelled insertion. dict_insert_entry now models
the word_id-assignment/dictionary-table/latest_id/word_id_next-counter
portion of vm_create_word (dictionary_management.c:379-470), reusing
word_id_next :: nat -- a field already declared in StarForth_Base.thy but
never previously written by any theory. Applied to :, CREATE, VARIABLE,
CONSTANT (StarForth_Defining_Words.thy) and DEFER (StarForth_Defer_Words.thy)
via forth_*_entry_half definitions, each named to keep visible what's
still not modelled: the TIB name-parse dependency, the DF (data-field)
write each word does afterward, and (for :) vm->compiling_word tracking,
none of which have a vm_state counterpart. Pin-shadow conflicts are
sidestepped via an explicit pinned_conflict :: bool parameter, the same
technique already used for the XT-pop gap elsewhere in this suite.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
DECAY-RATE@ (physics_freeze_words.c) pushed to the data stack with no
capacity check and no prior pop to make room, unlike its neighbors in
the same file -- the one live, unconditional missing-guard bug the
Isabelle sweep's ~15 candidate findings reduced to once checked against
vm_push()'s real internal bounds check (see proof/FINDINGS.md SS2).
Removed dictionary_manipulation_words.c's [ ] STATE and defining_words.c's
DEFER IS DEFER@ (plus the now-orphaned defining_runtime_defer helper) --
all confirmed permanently shadowed by later dictionary registrations
(defining_words.c and defer_words.c respectively), per FORTH's
newest-first lookup. No behavior change: the removed code was already
unreachable.
Verified: hosted `make` builds clean under -Wall -Werror; the hosted
self-test suite passes 965/965 implemented tests with no regressions.
Three-architecture QEMU acceptance boot, all clean to ok> with an
identical dict_hash=0x24b4279f0670aa3a across amd64/aarch64/riscv64 and
identical 1003/965/0/0 test totals -- logs attached.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Aggregates the sweep's cross-cutting architectural findings (file-scope
statics standing in for per-VM state, missing overflow guards, duplicate
word registration/shadowing) and gives an executive-summary coverage
index across all 34 src/word_source/*.c files, per Bob's original framing
for this initiative.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Completes the src/word_source/*.c sweep -- last of the 5 kernel-only
files.
Five INFER-*@ output accessors fully modelled: they read straight from
vm->last_inference_outputs, which is exactly the already-modelled
`last_inference :: inference_outputs_state option` field with matching
per-field names. Q.VARIANCE/INFER-DECAY-SLOPE/INFER-WINDOW-WIDTH get
guard/shape only, capturing a genuine finding: array_ptr sets vm->error
AND the caller still pushes a 0 placeholder regardless, unlike the
"error or push, never both" shape most guarded words in this sweep
follow. L8-UPDATE/L8-TABLE-FORCE get pop-shape only.
Second finding: L8-MODE/L8-UPDATE/L8-APPLY/L8-TABLE-FORCE manipulate
vm->ssm_l8_state (a legacy 16-mode struct) and, per L8-TABLE-FORCE's own
comment, a separate 128-config adaptive table the heartbeat's bandit
actually drives -- NEITHER is the `ssm_l8 :: ssm_l8_state` (4-mode
C0..C3) field this proof suite has modelled since early in the sweep.
Three L8 representations exist in the real system; none of this file's
words touch the one the model tracks. Flagged as an open question, not
guessed at.
WINDOW-DIVERSITY, INFER-RUN, L8-MODE, L8-APPLY, and the six BAYES-*
words deferred (unmodelled subsystems: rolling-window diversity
algorithm, the whole inference-engine run, legacy L8 state, hot-words
cache Bayesian posteriors).
Suite now 53 theories, green.
17 of 23 words fully modelled (Q.+/-/*//, Q.ABS/NEG, Q.FROM-INT/TO-INT,
Q.1/0/SCALE, Q.=/</>/0=, Q.MAX/MIN), reusing q48_add/q48_mul/q48_div/
q48_from_u64/q48_to_u64 already in StarForth_Q48_16.thy and cell_abs
(Q.ABS's raw sign-bit test is bit-for-bit cell_abs's `n <s 0`). Added
q48_sub there alongside, the one missing arithmetic primitive.
Q.LOG/EXP/SQRT/SIN/COS deferred (same transcendental-approximation class
already excluded from the sweep at q48_16_words.c). Q.PRINT deferred
(stdout only).
Finding: every word in this file pops/pushes via the VM_POP/VM_PUSH
macros, which resolve to completely unchecked vm_pop_fast/vm_push_fast
when STARFORTH_PERFORMANCE is defined -- a build-flag-gated stack-safety
hazard distinct from (and broader than) the individual missing-guard
instances found elsewhere in the sweep, since it silently disables every
guard in the entire file at once. Modelled assuming the safe path.
Suite now 52 theories, green.
StarForth_Lifecycle_Words_Hosted.thy: BIRTH/KILL/PAUSE/RESUME/USE are all
the SAME vm_state transition (pop u, pop caddr, log -- the C's own
"kernel build skips this file via Makefile glob" framing means this
covers only the hosted stand-ins; the real kernel capsule-birth-protocol
words live in src/starkernel/, out of this sweep's scope). First file in
the sweep where every registered word's full vm_state footprint is
captured with no deferred remainder -- name extraction is a pure memory
read, logging is pure I/O. Models the genuine partial-pop-before-error
case (C doesn't check vm->error between its two vm_pop calls).
StarForth_Defer_Words.thy: another duplicate-registration finding, same
class as defining_words.c vs dictionary_manipulation_words.c's [/]/STATE
-- word_registry.c registers this file's DEFER/IS/DEFER@ (Module 27)
AFTER defining_words.c's (Module 17), unconditionally in BOTH builds
(defer_words.c has no __STARKERNEL__ guard despite CLAUDE.md's "kernel-
only addition" framing; the hosted Makefile's SRC wildcard includes it
regardless). This makes StarForth_Defining_Words.thy's DEFER/IS/DEFER@
sentinels describe dead, shadowed code -- corrected in place with
cross-references. The live version hits the same three model gaps
anyway (dictionary-entry creation, data-field addressing, mutable
per-entry dispatch), so only IS's stack-underflow guard is new.
StarForth_Log_Words.thy: the five level-constant pushes, LOG-LEVEL!'s
guard+clamp, and all five LOG-*-STR words fully modelled (the STR words
share lifecycle_words_hosted.c's "pop2 + bounds-check, no vm_state write"
shape). LOG-LEVEL@, the (do-log-N) runtime words (raw threaded-code
pointer, same class as LIT), and the LOG-*" immediates (TIB + compile-
time dependencies) deferred. Finding: LOG-ERROR..DEBUG and LOG-LEVEL@
push with no overflow guard -- more instances of the pattern first found
at DECAY-RATE@.
Suite now 51 theories, green.
Stadium console fabric words (FABRIC.md items 4.3.3/4.3.5/4.3.7e/4.4q/
4.4v/4.4y). All four files gate their real hardware-touching bodies
behind __STARKERNEL__ (and, for keyboard, architecture too):
- StarForth_Framebuffer_Words.thy: PLOT/FB-WIDTH/FB-HEIGHT fully modelled
for the hosted-build fallback (deterministic, no hardware dependency);
kernel bodies (fb_put_pixel/fb_width/fb_height) deferred. Finding:
FB-WIDTH/FB-HEIGHT have no overflow guard before pushing -- second
instance of this class of bug after DECAY-RATE@.
- StarForth_Keyboard_Words.thy: all 6 words' non-kernel-or-wrong-arch
fallback modelled (fixed constant pushes / no-op); third and fourth
missing-overflow-guard instances. Real hardware polling
(i8042/virtio-input) deferred.
- StarForth_Scroll_Words.thy / StarForth_TTF_Words.thy: both files gate
registration itself behind __STARKERNEL__, so their words don't exist
at all in a hosted build -- no fallback to model, sentinel-only.
Suite now 48 theories, confirmed green via a full clean rebuild (HOL-
Library cold-built in 15m18s after an accidental heap clear, StarForth
itself 33s).
5 of 12 words fully modelled: ENTROPY@/ENTROPY! (XT-pop gap sidestepped
same as ACL words, but note this file's is_valid_dict_entry is a real
membership-check safety improvement over acl_words.c's null-only check),
RESET-ENTROPY (dictionary-wide bulk reset, same technique as
ACL-INIT-PRIMITIVES), ZUSE-AUTHENTICATE (single-field set), VERSION
(identity, no stack effect at all). TOP-WORDS/SEED/RANDOM/WAIT get
guard/shape only -- SEED and RANDOM both depend on g_prng_state, a
file-scope C static shared across the whole Tripod fleet (yet another
instance of the recurring file-scope-static-instead-of-per-VM pattern,
here meaning every VM draws from the same RNG stream). WORD-ENTROPY/(-/
INIT not modelled (pure printf / TIB dependency / real filesystem I/O
plus a custom text parser).
Finding: register_starforth_words registers its 10 words, bootstraps
the STARFORTH vocabulary, then re-registers 12 words (same 10 plus
ENTROPY@/ENTROPY!) into that vocabulary context -- noted as the second
file where registration order matters for which body actually runs,
judgment on intentionality deferred to the largely-unmodelled vocabulary
chain mechanics.
Suite now 44 theories, green.
StarForth_Physics_Diagnostic_Words.thy (physics_diagnostic_words.c):
3 of 4 words are pure-printf identity transitions; PHYSICS-BURN's guard
modelled, its arbitrary dynamically-selected func-pointer execution loop
is a new class of gap (not reducible to any prior one).
StarForth_Physics_Benchmark_Words.thy (physics_benchmark_words.c):
hot-words cache is a whole unmodelled subsystem. PHYSICS-RESET-STATS's
pipeline_metrics half (3 real vm_state fields) modelled; everything else
in the file deferred.
StarForth_Physics_Pipelining_Diagnostic_Words.thy
(physics_pipelining_diagnostic_words.c): root-cause finding --
`word_transition_metrics` has been a declared record type in
StarForth_Base.thy since early in the sweep but was never wired into
`dict_entry` as a field, so every word in this file touches state with
zero abstract representation. Three no-arg words modelled as identity
(with an explicit caveat that this reflects the model's blind spot, not
a no-op claim about the C); the three lookup words get only their
simplest empty-stack underflow case.
Suite now 43 theories, green.
6 of 9 words fully modelled (FREEZE-WORD, UNFREEZE-WORD, FROZEN?, HEAT!,
HEAT@, DECAY-RATE@), parameterised over an explicit word_id-resolution
input to sidestep the same raw-pointer name-lookup gap already flagged
for FIND -- these words are an even rawer variant (caddr is an
already-computed VM address cast straight to a host pointer, not a
parsed input-stream token). SHOW-HEAT/ALL-HEATS (stdout diagnostics) and
FREEZE-CRITICAL (21-name batch of the same FREEZE-WORD op) deferred.
Finding: DECAY-RATE@ is the only push-only word in this file (and one of
few in the whole sweep) with no data-stack-full guard before the raw
push -- a genuine overflow hazard, modelled faithfully.
4 of 6 words fully modelled (HEAT-PERCENTILES, LOOKUP-STRATEGY@/!,
SHOW-HEAT-OPTIMIZATION); REORG-BUCKETS deferred (bucket/lookup-table
structure has no vm_state counterpart); COMPARE-LOOKUPS partially --
guards and its net-zero effect on lookup_strategy modelled, the timed
FIND-loop benchmarking body deferred (same FIND gap already flagged
elsewhere).
Fills the gap the existing ACL_*.thy policy theories deliberately don't
cover: the six plain field-accessor getters (ACL-MODE@, ACL-PINNED?,
ACL-TTL@, ACL-ALLOW@, ACL-HEAT@, ACL-WORD-ID) and ACL-INIT-PRIMITIVES
(dictionary-wide bulk reset of unpinned entries). The mutating words
(ACL-PIN, ACL-MODE!, ACL-TTL!, ACL-ALLOW!, ACL-INHERIT) were already
modelled word-for-word in ACL_Pin_Monotone.thy / ACL_Inherit_Clears_Pin.thy
and are cross-referenced, not duplicated.
ACL-INIT-PRIMITIVES models cleanly despite the C using a raw ->link
linked-list walk: the abstract word_id-indexed dictionary expresses "for
every entry" directly, without needing the pointer-chasing gap already
flagged for TRAVERSE/FIND elsewhere.
4 of 19 words fully modelled ([, ], STATE, IMMEDIATE), 2 guard-only
partial (:, ;), rest deferred behind three named model gaps: dictionary-
entry creation (never modelled anywhere in this suite before now),
data-field addressing (same class as the existing >BODY gap), and
mutable per-entry dispatch (word_table is a fixed global, can't express
DEFER/IS).
Finding: defining_words.c's [/]/STATE are registered after (and thus
permanently shadow) dictionary_manipulation_words.c's versions of the
same names -- that file's prior "dead cross-VM-shared static" finding
only ever applied to the shadowed, unreachable code. The live versions
correctly use vm->state_addr, a real per-VM field, now added to
vm_state.
1 of 7 registered words modeled, partially: (FIND)'s two concretely-
decidable failure branches (invalid address; invalid length-derived
range). Its "found" branch, and VOCABULARY/DEFINITIONS/CONTEXT/CURRENT/
FORTH/ORDER entirely, are deferred.
Genuine finding: this is the 7th and by far most severe occurrence of
the file-scope-static-instead-of-per-VM-field bug pattern in this sweep.
The ENTIRE vocabulary subsystem (forth_vocab/context_vocab/current_vocab,
context_var_addr/current_var_addr, the first-character search index) is
file-scope C statics, not struct VM fields. In the Tripod multi-VM
fleet, one VM's VOCABULARY/DEFINITIONS/FORTH silently changes where
every other VM looks up and defines words -- a correctness hazard in
ordinary word resolution for the whole fleet, not just a diagnostic-flag
leak like the smaller prior instances. init_vocabulary_system's `static
int initialized` guard compounds this: only the first VM to touch any
vocabulary word seeds the vocabulary roots, from its own dictionary.
10 of 16 registered words modeled (COLD/WARM/BYE/WORDS/VLIST/PAGE/NOP/
QUIT/ABORT/EXECUTE guard-shape), plus the internal (ABORT") runtime
helper. Deferred: ( and \ (TIB dependency), SAVE-SYSTEM (real file I/O),
79-STANDARD (reads a non-per-VM global), ABORT" compile-time half (TIB +
codegen), SEE (TIB + raw threaded-code pointer walk).
Two findings. (1) system_running/forth_79_standard are file-scope C
statics doing per-VM-shaped work -- the 5th and 6th occurrence of this
bug pattern in the sweep (previously: control_words.c's cf_stack,
dictionary_manipulation_words.c's state_variable, string_words.c's
word_scratch_addr). (2) EXECUTE casts a popped FORTH cell straight to a
DictEntry host pointer and calls through it (entry->func(vm)), gated
only by a null check -- same hazard class as format_words.c's ?/DUMP but
far more consequential since EXECUTE is a core, ubiquitous primitive
rather than a diagnostic word. Flagged as the highest-severity finding
this sweep has produced.
editor_words.c: zero tractable words (first such file in this sweep) --
every word routes through the same deferred block-window cache as
block_words.c, and EDIT is an interactive stdin/stdout REPL loop, not a
single-step transition.
format_words.c: 17 of 19 registered words modeled (# and #S deferred,
multi-precision division out of scope). Two genuine C findings recorded:
(1) DECIMAL/HEX/OCTAL write only the FORTH-visible memory cell at
base_addr, never the separate vm->base host-mirror field that number
OUTPUT words actually read -- proved formally
(decimal_does_not_change_vm_base et al.), so HEX/OCTAL/DECIMAL silently
never affect printed output, only parsed input. (2) ? and DUMP cast the
popped cell directly to a host pointer and dereference it, bypassing
vm_addr_ok entirely -- an out-of-VM-bounds read, not modeled since it
isn't a vm->memory access at all.
Adds base_addr/hold_addr/hold_pos to vm_state (StarForth_Base.thy),
matching the scr_addr/here pattern from earlier files.
7 of 9 registered words modeled (EMIT/CR/?TERMINAL/TYPE/SPACE/SPACES/
(do-string)); KEY and ." deferred (real external input / TIB-adjacent
input-buffer dependency, same categories as earlier deferrals in this
sweep). Two genuine C findings recorded: ?TERMINAL is a permanent stub
always returning false, and TYPE's bounds check has a signed-integer-
overflow bypass (addr+count wraps negative for large addr/count,
defeating the VM_MEMORY_SIZE guard) with a machine-checked witness.
block_words.c is categorically different from every file covered so far in
this sweep: every other word_source file operates on pure per-VM internal
state already in vm_state (data_stack/return_stack/memory/dictionary).
block_words.c sits on top of a real disk-backed I/O subsystem
(block_subsystem.h) plus a per-VM in-memory cache of it
(vm->blk_vm_lbn/blk_vm_cbuf/blk_vm_dirty/blk_vm_next), none of which are
in vm_state.
Only SCR is self-contained (just needs vm->scr_addr, added to vm_state
the same way here/ecw_nesting were for earlier files). The other 11 words
are deferred for three reasons documented in the theory header: the
block-window cache subsystem (a modeling project on the scale of the
deferred TIB input subsystem, not a one-word extension), real disk I/O via
block_subsystem.h, and recursive vm_interpret()/printf() in LOAD/LIST/
THRU/-->.
Noted in passing: blk_vm_evict/blk_vm_flush_all's own comments document a
real raw-pointer-lifetime bug (stale C buffer pointers after block-
subsystem struct-copy eviction) that was already found and fixed by hand
in the C, before this suite ever looked at the file -- not an open issue,
just worth recording as prior art for exactly the class of bug this sweep
exists to catch.
30 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Closes the one word deferred from the previous pass for being a bigger
proof-engineering lift rather than a hard blocker. Adds bytes_eq (exact
n-byte match at two offsets) and search_from (bounded first-occurrence
search, tries offset 0..budget) as the missing helper, built the same way
bytes_compare was for COMPARE. Covers both C early-return special cases
(empty needle matches at start; needle longer than haystack never matches)
plus the general naive search's found/not-found outcomes.
10 of 25 words in string_words.c now modeled; the remaining 15 are the
TIB/input-subsystem, stdio, and raw-C-string/strtol clusters documented in
the file's header.
29 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Covers the 9 self-contained words in string_words.c that operate purely on
data_stack/memory with no dependency outside the existing model. Introduces
vm_addr_ok_m, a literal transcription of the real C vm_addr_ok bounds check
(src/vm.c:815-820) using VM_MEMORY_SIZE -- more precise than the sign-only
check earlier memory words used -- and resolve_span, a shared helper for
the auto-detect-counted-string pattern that recurs across six of this
file's words.
16 words deliberately not modeled, in three groups (full reasoning in the
theory header): (a) WORD/SPAN/TIB/>IN/SOURCE/QUERY/EXPECT depend on the
lazily-allocated TIB input subsystem (vm->tib_buf via vm_input_ensure),
which has no vm_state counterpart; QUERY/EXPECT also call fgets(stdin)
directly, real I/O with no HOL formalization; (b) CONVERT/NUMBER/ENCLOSE
depend on raw C-string scanning (strlen past a single vm_addr_ok-checked
byte -- a genuine unbounded-read hazard, noted not chased) or strtol(); (c)
S"/(s")/LITERAL/[LITERAL]/['] depend on the same compile-time/threaded-code
machinery already out of scope from control_words.c. SEARCH is deferred
despite being self-contained -- its nested substring search needs a bigger
proof-engineering lift than the single-pass helpers used here.
Third occurrence of the file-scope-static-instead-of-per-VM-field bug
pattern noted (WORD's word_scratch_addr), matching control_words.c's
cf_stack and dictionary_manipulation_words.c's state_variable -- not fixed,
flagged for aggregation when raised to Bob.
29 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Both blockers recorded at the previous resume point turned out to be
resolvable, not permanent:
- The "cell is unbounded int" blocker for D+/D-/DNEGATE/etc. was stale --
cell was already migrated to a 64-bit word type in commit fe6e705, before
this file was first touched. The note was never re-checked against
current StarForth_Base.thy before being carried forward. Same lesson the
control_words.c vm_ip finding taught one file earlier in this sweep:
re-verify carried-forward reasoning against the current file, don't just
trust a previous session's note.
- The missing vm->ecw_nesting field for 2>R/2R>/2R@ was a real, scoped gap
-- added ecw_nesting :: nat to vm_state in StarForth_Base.thy.
Adds S>D, D+, D-, DNEGATE, DABS, a d_compare helper, DMAX, DMIN, D<, D=,
D0=, D0<, D2*, D2/, 2>R, 2R>, 2R@. D2*/D2/ use push_bit/drop_bit/bit
(established idiom from StarForth_Q48_16.thy) for the 128-bit shifts; D2/
uses sint/div (floor division) rather than cell_sdiv (C99 truncating
division) since arithmetic right shift is floor division, not truncation,
for negative operands. DNEGATE's double-negation-is-identity property is
true but left unproved (needs the same carry/borrow-across-the-pair
algebra as D+/D-, not just simp) -- a nice-to-have, not core plumbing.
All 20 registered words in double_words.c are now covered. 28 theory
files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Covers the runtime half of control_words.c fully: (BRANCH), (0BRANCH),
(?DO), (DO), (LOOP), (+LOOP), (LEAVE), UNLOOP, I, J, EXIT. The "vm_ip as
raw pointer" gap flagged at every earlier resume point turns out not to
need a new model extension -- return_stack-held addresses dereference into
vm->memory exactly like @/! addresses from the data stack, so the existing
mem_read/unat machinery from StarForth_Memory_Words covers it directly.
The compile-time half (IF/ELSE/THEN, BEGIN/WHILE/REPEAT/AGAIN/UNTIL, the
compiling halves of ?DO/DO/LOOP/+LOOP/LEAVE, CASE/OF/ENDOF/ENDCASE) is left
unmodelled, not from a model gap but a genuine architectural finding:
Headline finding, not fixed: every compile-time control-flow word operates
on FILE-SCOPE C statics (cf_stack/cf_sp, cf_last_mode, leave_addrs/leave_sp,
endof_addrs/endof_sp, and their mark-stacks) -- none are struct VM fields,
none are keyed by VM instance. In the Tripod multi-VM fleet, two VMs
compiling control structures at overlapping times corrupt each other's
IF/DO/CASE nesting through this shared global state, and a VM whose
compilation aborts mid-structure leaves stale cf_sp/leave_sp/endof_sp state
for whichever VM compiles next. cf_epoch_sync's mode-transition reset
heuristic is itself keyed off a single global (cf_last_mode), not per-VM,
so it can neither reliably detect nor reliably avoid false resets across
VMs. Modelling these words against vm_state would require either inventing
a field the real implementation doesn't have (silently fixing the bug in
the proof) or modelling a bare global with no plumbing precedent in this
suite -- both out of scope, left as documented gaps.
28 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Covers the mode/flag half of dictionary_manipulation_words.c that's provable
against the existing vm_mode/dictionary/latest_id model. The raw-pointer
DictEntry navigation half (>BODY/>NAME/NAME>/>LINK/LINK>/CFA/LFA/NFA/PFA/
TRAVERSE/FIND/') is left unmodelled -- same class of gap as control_words.c's
deferred vm_ip/return-stack-as-raw-pointers issue, since the abstract
dict_entry record is word_id-indexed, not addressed, and has no counterpart
for struct-relative pointer arithmetic (name_len, link, body offset).
Genuine findings recorded in comments, not fixed:
- [, ], STATE, and INTERPRET all read/write a file-scope `static cell_t
state_variable` -- NOT vm->state_var, the real per-VM STATE field used
everywhere else in the interpreter. In the Tripod multi-VM fleet this
static is shared across every VM instance, not per-VM.
- dictionary_m_word_hidden's dead #else branch (unreachable since
WORD_HIDDEN is always defined) calls a function that doesn't exist
(dictionary_word_smudge vs. the real static dictionary_m_word_smudge).
27 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adds VM_MEMORY_SIZE and DICTIONARY_MEMORY_SIZE constants to StarForth_Base.thy
(previously only STACK_SIZE existed). SP@/SP! left unmodelled (oops-flagged
with explanation) -- the list-based data_stack model has no independent dsp
register distinct from list length, which is exactly what SP! manipulates.
Genuine findings recorded in comments, not fixed:
- LATEST has an identical body to HERE (both just push vm->here) rather than
consulting vm->latest -- doesn't return what its own doc comment claims.
- ALIGN (via vm_align/vm_allot) bounds-checks here against
DICTIONARY_MEMORY_SIZE (2MB), while ALLOT/,/C,/2, bound-check directly
against VM_MEMORY_SIZE (5MB) instead -- two different ceilings for the
same dictionary pointer.
Full suite (26 theory files) verifies with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Covers word_source/mixed_arithmetic_words.c. Two genuine findings recorded
in comments rather than fixed:
- register_mixed_arithmetic_words registers MOD and /MOD a second time,
after arithmetic_words.c's own registrations; vm_create_word links new
entries at the head of vm->latest and FIND scans from vm->latest forward,
so arithmetic_words.c's MOD//MOD are permanently shadowed, unreachable
dead code once bootstrap completes (verified against
dictionary_management.c and the module order in word_registry.c).
- M*, M/MOD, and the "avoids intermediate overflow" claim on */ and */MOD
are false on 64-bit builds: cell_t and "long long" are the same width
there, so the long-long intermediate does not actually widen the
product -- it wraps mod 2^64 like plain cell multiplication before the
32-bit-style split/reconstruction runs. M*/M/MOD are left undefined
here (oops-equivalent: documented as not modelled, since formalizing
"the wrong thing, faithfully" adds no proof value) rather than fixed.
MOD//MOD/*//*/MOD reuse cell_sdiv/cell_smod from the arithmetic-words
migration; M+/M- transcribe the C's hand-rolled signed carry/borrow
detection literally, proving only stack-level plumbing (not double-
precision correctness, which needs an interpretation function this
suite doesn't build).
All 24 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
cell_t is a 64-bit signed C long; the formal model previously used
unbounded HOL int, hiding wraparound and signed/unsigned distinctions
entirely. Switches cell to "64 word" throughout and fixes every proof
site that assumed int semantics:
- StarForth_Base.thy: cell_safe/cell_abs/cell_sdiv/cell_smod plus the
sint-bridging lemmas used across the suite
- StarForth_Loop1_Heat.thy, StarForth_Loop3_Decay.thy: heat tracking
converted to signed word comparisons (<s/\<le>s)
- StarForth_Stack_Words.thy: PICK/ROLL against real C ground truth
- StarForth_Arithmetic_Words.thy: ABS/MIN/MAX/div/mod rebuilt on signed
word semantics (cell_sdiv/cell_smod match C99 truncating division;
2/ uses signed_drop_bit to match "n >> 1"); documents a genuine
ABS(INT64_MIN) wraparound hazard mirroring the real C behavior
- StarForth_Memory_Words.thy: @/!/C@/C! address checks converted to
the signed order
All 23 theory files verify with zero errors, including
StarForth_Concurrent and StarForth_Correctness.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Covers the pure double-cell data-stack shuffle words from
src/word_source/double_words.c. Deliberately scoped to exclude:
- 2>R/2R>/2R@: branch on vm->ecw_nesting, a field vm_state doesn't track
at all -- needs a model extension first, not attempted here.
- S>D/D+/D-/DNEGATE/DABS/DMAX/DMIN/D</D=/D0=/D0</D2*/D2/: depend on
cell_t being a fixed-width (64-bit) wrapping integer (explicit
unsigned-long carry/borrow arithmetic, bitwise complement with
wraparound). StarForth_Base.thy's "cell = int" is unbounded, not
fixed-width, so this isn't expressible as currently modeled. Fixing it
means deciding whether cell becomes a 64-bit word type everywhere
(ripples into all 23 already-verified theories) -- a foundational
decision, flagged for later, not made as a side effect of this file.
24 theory files now verify with zero errors.
ROLL: forth_roll_def implemented a third, invented convention matching
neither the theory's own test lemma nor the real C stack_word_roll(). Traced
the actual C source (src/word_source/stack_words.c:287-320) and its passing
tests (stack_words_test.c roll_1/roll_2) to the real semantics -- ROLL is
1-indexed from the BOTTOM of the stack, not top-indexed as the old
definition assumed. Rewrote forth_roll_def to match, replaced the false
roll_one_nop/roll_two_is_rot with lemmas verified against the actual test
vectors.
PICK: forth_pick_def indexed into the pre-pop stack (still containing the
count n as its own head) instead of the post-pop stack, off by one position,
plus a bound check one too permissive. Fixed against src/word_source/
stack_words.c:265-282 and its pick_0/pick_1/pick_2 test vectors.
pm_wf: pm_record_hit_preserves_wf/pm_record_miss_preserves_wf were
oops-flagged as a genuine invariant gap. Fixed with the minimal added
hypothesis (pm_last_accuracy_den pm > 0), matching this session's established
discipline. Also documents a deeper finding: pm_last_accuracy_num/den don't
correspond to any field in the real PipelineGlobalMetrics C struct (which has
a single "double last_checked_accuracy", not a fraction) -- flagged for a
separate field-level audit, not attempted here.
All 23 theory files verify with zero errors.
Isabelle toolchain replaced (was genuinely 2011, 14+ years stale) and every
theory file fixed to actually compile -- most had apparently never been
checked under a working Isabelle at all. Fixed the vm_state self-reference
in StarForth_Base.thy properly (word_table is now a free-standing global
constant, not a circular record field), corrected the word_physics_transparent
axiom (was claiming full state equality from mere exec-equivalence, provably
too strong), and worked through 14 years of HOL-Library drift plus several
missing-hypothesis bugs across the physics-loop and ACL theories.
Two genuine (non-tactical) bugs found and left oops-flagged rather than
silently resolved: forth_roll's index arithmetic disagrees with both its own
test lemma and the real C ROLL implementation (three-way inconsistency), and
pm_wf isn't actually preserved by pm_record_hit/pm_record_miss. Both need a
decision, not a proof-script fix.
Full writeup in FABRIC-2.md item 5.2.
Isabelle2011-1 (genuinely 14+ years old) replaced with Isabelle2025-2 at the same path. Real build attempt: HOL-Library builds clean, StarForth session fails on one root-cause file (StarForth_Q48_16.thy) -- undefined fact, two non-closing proofs, one name collision against a new HOL-Library constant. Everything else is downstream unresolved-import fallout, not independent breakage. Not fixed yet.
ARTEMIS.md got the same well-scoped fix as TRIPOD.md (already committed separately). CONSOLE.md's entire architecture premise (Console as 4th Tripod VM) was superseded by FABRIC.md §17.5's later utility-not-patron ruling, and its keyboard-input-doesn't-exist claim is false -- i8042.c/virtio_input.c and the 4.4v keyboard bridge are live. HERMES.md's message-node cell count (8) contradicts the capsule's own 9 CONSTANT MSG-CELLS, and its locked block map is missing item 4.2's new blocks. Both reported, not fixed -- too large for a one-paragraph correction, left for Captain Bob's call on rewrite vs. superseded-header treatment.
capsules/init.4th births no VM but Hera (item 0.1). Artemis's disk device auto-attaches at boot (kernel_main.c M7.pre, real, unchanged); Artemis-as-VM-patron capsule birth does not.
Item 0.1 pruned capsules/init.4th to Hera-alone; TRIPOD.md was never updated to match. Corrected to reflect current on-demand-birth reality and distinguish Artemis-the-storage-device (auto-attaches at boot, kernel_main.c) from Artemis-the-VM-patron (not auto-spawned). Partial closure of FABRIC-2.md item 5.3 -- the doc's broader shrink-to-three-lines scope remains open.
Extends the existing lexicon (which already covered heat/decay/inference vocabulary but predated Stadium work entirely) with patron, mass, density, K, cell, code field, Stadium, warehouse, utility -- all cited to their FABRIC.md DECIDED sections. Adds a Kconfig-knob-to-concept table with verified wiring status, flagging STADIUM_CAPACITY_TICK as dead (matches this session's §12 Q5 finding). Bumped to v1.1.
Live console/framebuffer stack has zero dirty-region or heat/decay instrumentation (grepped framebuffer.c/vt100.c/console.c). True prerequisite is item 1.11 (dirty-event granularity), still unstarted, not 'the framebuffer work' generally, which has since shipped. Left open.
Traced every loop's actual firing cadence from source. Headline finding: the fleet-capacity loop (vm_physics_heartbeat_tick, the exact mechanism §22.4 cites as precedent) shares a global counter fed by every live VM, so with Tripod's real multi-VM topology it can fire faster in wall-clock terms than any single VM's own heat-inference loop -- the opposite of §22.4's required ordering. STADIUM_CAPACITY_TICK, the Kconfig symbol §22.4 specified as the fix, exists but is never read anywhere. Reported, not fixed; left open for Captain Bob's call.
Hermes v1's real message struct (init.4th blocks 4100/4105/4143) is 72 bytes with an out-of-line pointer+length payload, not the speculative 64-byte-cell/32-byte-inline-payload scheme from FABRIC.md §23.3. The design question is moot: the implementation went a different direction.
Verified via tools/kconfig/conf + kernel_amd64_defconfig: a .config edit to CONFIG_SK_PARITY_DEBUG genuinely flows through to the parity.c compile line's -D flag in both directions. Required installing bison/flex, which were missing.
Investigated 2026-08-13: not just the encoding field -- blk_get_meta()/
blk_set_meta() and the whole blk_meta_t on-disk layout have zero callers.
Captain Bob's ruling: flag and leave as-is, expected to be consumed once
Artemis's design (content-typed/owned/ACL'd blocks) is completed. No
code changed.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
No code change; closed as investigated and ruled not-a-bug (deliberate
future-milestone scaffolding) rather than left open as a loose TODO.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Investigated 2026-08-13: confirmed unreachable by repo-wide grep, but
each of the three stubs is a real doc-commented placeholder for a future
per-arch MMU milestone, not leftover cruft. Captain Bob's call: leave in
place, keep tracked as a TODO rather than delete or wire in a no-op call
site. No code changed.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Punch list §C item complete. Corrects this morning's "structurally
excluded" framing -- the Hera-is-root case was reachable via
S" Hera" KILL, fixed in db66406. Broken-parent-chain half remains
genuinely unreachable and is no longer tracked as open.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
