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>
S" Hera" KILL called vm_physics_retire(hera_id) before capsule_vm_kill()'s
own Hera guard ever ran. Hera's self-referential parent_vm_id makes
vm_physics_find_root_id() return her own id immediately, so
vm_physics_retire() treated her as an unreachable root and zeroed the
fleet's entire execution_heat_q48 sum -- silently, with only the
harmless-looking "cannot kill Hera" message as output. Guard the retire
call the same way capsule_vm_kill() already guards the actual kill.
Three-arch acceptance boot, all clean to ok>:
logs/20260813-083429/amd64, logs/20260813-083551/aarch64,
logs/20260813-083738/riscv64.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The touch()-fan-out truncation was wrongly blamed for monotonic
conservation drift. Corrected in place per this document's own rule for
bookkeeping errors (§25 discipline, same treatment as the four fixes
made during the 2026-08-12 closure audit) rather than left standing.
Full investigation and worked example live in FABRIC-2.md §B/§C.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Punch list §B item complete. Full read of capsule_vm_physics.c plus a
worked example show the touch()-fan-out truncation FABRIC.md §20.2
blamed cannot cause conservation drift -- vm_physics_transfer() moves
matched amounts on both sides of every call. Git history rules out a
since-fixed bug: the code predates §20.2's correction unchanged.
The one path that can genuinely drop heat is vm_physics_retire()'s
guarded no-valid-root case, structurally unreachable today (Hera can't
be killed, parent chains can't corrupt). Tracked as its own item in §C.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Punch list §B item complete. Documents the Hera-sole-owner ruling and
points to the vm_runtime.c fix (bcc72d0) and its three-arch acceptance
logs.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Only Hera writes the shared physical timer period now, gated by
vm_uuid_is_hera(vm->stadium_vm_id) in vm_tick_inference_engine(). Every
other VM's Loop #7 still adapts its own tick_target_ns as before, it just
no longer races to re-arm the one physical timer.
Includes 3-arch acceptance run (amd64/aarch64/riscv64, all booted clean
to ok>) and regenerated capsule/DoE artifacts.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
No document like this existed. Covers every core C-primitive FORTH word
(~470 registrations, 435 unique names after collapsing double-registered
ones) across all 36 src/word_source/*.c files plus
src/starkernel/capsule/mama_forth_words.c, organized into 34 category
sections matching the module order in register_forth79_words().
Each entry has word name, stack effect, and a one-sentence description
pulled from the doc comment above its implementation (or inferred where
none existed). Explicitly scoped to core primitives, not the ~330
FORTH-defined words inside .4th capsules -- those track individual
experiments/policies rather than the language itself and would need
their own document with a different update cadence.
Resolved, not just noted, the two real name collisions in the live
dictionary: [ ] STATE (dictionary_manipulation_words.c vs.
defining_words.c) and MOD /MOD */ */MOD (arithmetic_words.c vs.
mixed_arithmetic_words.c) -- checked actual registration order in
word_registry.c against the newest-first FIND search to determine which
implementation is actually reachable by name, rather than guessing.
Includes a "keeping this current" section documenting how to extend it
when words are added/removed/re-registered.
Also includes BLOCK_MAP.md/artemis.img/amd64.csv regenerated by builds
during this session, and a qemu boot log/DoE run that weren't from any
command in this session -- kept per repo convention, logs are audit
artifacts, not deleted.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
FABRIC.md did its job: §1-24's design argument is settled and every
implementation item through 4.5/4.4ac either landed or was explicitly
deferred with a reason. At 7,595 lines it was no longer a good place
to find what's actually still open, so it's now archival -- header
rewritten to say so, pointing to FABRIC-2.md.
Before closing it, read the entire document end to end (not sampled)
looking for anything unresolved: punch-list checkboxes, the nine
"### N.N Open" architectural subsections in §1-24, the §25.7
"reported, not scheduled" list, and any other "not yet"/"deferred"
language. Found and fixed four stale bookkeeping spots where later
work had actually resolved something but the note was never updated:
§19.6 #3 (resolved by item 2.1), §21.5 #4 (resolved by §20.5 #4), the
§25.7 stadium_owner[idx] bullet (resolved by item 4.2), and item 4.5's
own parent checkbox (all six sub-items 4.5a-4.5f were already [x]).
FABRIC-2.md carries forward everything genuinely still open: the
blocked/scoped punch-list items (1.11, 4.3, 4.4s, 4.6, 5.1-5.3, plus a
specific pending TRIPOD.md edit found within 5.3), two regressions
that were invisible with Tripod pruned to Hera-alone and are now live
since item 4.2 restored Hermes (the fleet heat leak in
vm_physics_touch(), and multi-VM heartbeat ownership), nine dead-code/
cruft reports, three open design questions (§12 Q5, §17.4, §23.4 #2),
and two documentation-debt items (the taxonomy/glossary Captain Bob
flagged 2026-08-04, and re-measuring ACL-RWT DoE overhead now that
real compiler optimization is enabled).
Also includes BLOCK_MAP.md/artemis.img/amd64.csv regenerated by builds
during this session, and a qemu boot log/DoE run that weren't from any
command in this session -- kept per repo convention, logs are audit
artifacts, not deleted.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Extends the amd64 headless screendump verification (99999 SCROLL-BACK
injected over the serial chardev socket, captured via QEMU's HMP
screendump over its monitor socket) to aarch64 (-device ramfb) and
riscv64 (-device ramfb) -- same script shape, no GUI or physical
typing needed on either. Both show the same deep-POST recovery
(Init: Mama birth..., HADES DoE rows 58-73, boot banner) and the same
pre-existing 4.4q live-cursor-draw glitch already confirmed on amd64,
present identically -- boot-mode scrollback is real and reachable on
every architecture, not just amd64.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Confirms 4.4ac's boot-mode scrollback ring actually works: injected
'99999 SCROLL-BACK' over the serial chardev socket (same mechanism the
old DOE_INJECT automation used to drive EXEC-DOE -- SCROLL-BACK is a
plain FORTH word, and sk_repl_step()'s input comes from console_getc()
polling the UART), then captured the framebuffer with QEMU's own HMP
screendump command over its monitor socket. No GTK session or physical
typing needed, correcting this item's own earlier assumption that it
would.
Result (logs/screendump-4.4ac/amd64-scrollback.png) shows PARITY:
MAMA_INIT, Init: Mama birth OK, ACL: CAPSULE-BIRTH pinned STRICT,
Starting heartbeat..., and HADES DoE rows from steps 58-73 all on
screen at once -- genuinely early POST content, not just the pre-TTF
tail. Also confirms a small pre-existing 4.4q limitation (live cursor
draw corrupting a scrolled-back view) is unaffected by this item, not
a new regression.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
vt100.c: font_8x16/bitmap-mode boot output previously had no scrollback
at all -- g_shadow/g_ring were only allocated in vt100_enable_ttf(), so
POST/self-test/heartbeat text was gone the instant it scrolled off,
recoverable only from the serial log. Gives boot mode its own ring/
shadow pair (bitmap cell geometry, 4096-line capacity), frozen as a
snapshot the moment vt100_enable_ttf() switches to the TTF-geometry
pair, per the two-independent-rings design scoped with Captain Bob.
scrollback_line_at()/scrollback_redraw()/vt100_scroll_back() now walk
all four segments (boot ring, boot shadow, TTF ring, TTF shadow) as one
continuous history, so PgUp from the REPL reaches back through POST.
Three-arch QEMU boot + logs clean (amd64/aarch64/riscv64, no faults, no
dictionary/parity regressions). Visual verification that PgUp actually
recalls POST text still needs an interactive GTK screendump -- noted as
open in FABRIC.md, same pattern as 4.4ab's screendump.
Also includes BLOCK_MAP.md/artemis.img regenerated by these builds, and
the acceptance-boot logs (plus stray logs from an earlier QEMU-instance
collision during testing -- kept per repo convention, logs are audit
artifacts, not deleted).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The qemu target used to poll the serial log for ok>/zuse)ok>, then
unconditionally kill the VM (optionally injecting EXEC-DOE first) — a
DoE-campaign automation shape that also fired during plain interactive
use, cutting the session out from under you the moment the prompt
appeared. All three arch branches (amd64/aarch64/riscv64) now just run
qemu-system-* in the foreground and block until it's closed manually;
serial logging to logs/ and DoE CSV extraction on exit are unchanged.
Also includes BLOCK_MAP.md/artemis.img/amd64.csv regenerated by the
qemu-esp test run, and that run's log/CSV artifacts.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Brings in the cursor indicator + HB-ON/HB-OFF runtime DoE toggle work.
Diverged from master's own three-arch verification commit (0d8fff3,
logs only, no code overlap) since that verification was made directly
on master rather than merged back to stadium-step-one first.
Cursor (Captain Bob: "the only thing we need is a cursor"):
vt100_draw_cursor() draws a solid block at the terminal's current
position, called from repl.c after the prompt prints and after every
keystroke/backspace. vt100_erase_cursor() cleans up the one gap a static
cursor has -- Enter/newline moves away from the cursor cell without a
character draw ever overwriting it, which left a stray block behind
until this fix.
HB-ON/HB-OFF (Captain Bob: run a program with or without instrumentation
without rebuilding):
Converted per-tick DoE logging from a build-time flag (HEARTBEAT_DOE_LOG)
to a runtime one. doe_log_tick_row() now self-gates on g_doe_log_enabled
(default 1, matching the old default) instead of being compiled out
entirely; the call site in vm_runtime.c is unconditional. Two new FORTH
words, HB-ON and HB-OFF, flip the flag live. Removed the now-dead
HEARTBEAT_DOE_LOG plumbing: the Kconfig symbol, and the -D forwarding in
both LOADER_CFLAGS and KERNEL_CFLAGS.
Verified: three-arch clean QEMU boot + logs; dictionary word count 466
(463 baseline + ALT+TAB + HB-ON + HB-OFF, exactly the three words added
across this session); amd64 screendump confirms the cursor renders
correctly after real interactive typing.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Confirms all three architectures boot clean on master after the
fast-forward merge from stadium-step-one (af20efa), identical to the
behavior verified on that branch: UEFI -> POST -> Mama birth -> Hermes
self-test -> heartbeat -> ok>, no DoE/ECW noise.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
full-screen vt100 terminal
4.4v -- keyboard-to-REPL bridge, real and tested:
Refactored KEY-EVENT's per-arch translation logic (keyboard_words.c) into
a shared C function, sk_key_event_poll(), so the REPL bridge reuses item
4.3.5f's already-converged Linux-keycode-namespace event stream instead
of building separate amd64/aarch64/riscv64 tables. repl.c's sk_kbd_getc()
decodes the standard US-QWERTY printable range plus Enter/Backspace/Shift
against that stream; sk_readline() polls it as a second source alongside
console_getc(). Verified via QEMU monitor sendkey injection, and by
Captain Bob typing directly into the live QEMU window over real emulated
PS/2 hardware mid-session (1 1 + . -> 2 ok, then a clean BYE shutdown).
4.4ab -- simplify to a full-screen terminal:
Captain Bob's call, reverting the 640x480 CANVAS box + independent REPL
strip (4.4o/4.4t/4.4x/4.4z) in favor of the simplest shape: the entire
framebuffer is one vt100 terminal, g_vt.cols/rows = fb_width()/fb_height()
divided by cell size, no origin offset, no box, no strip, no border
drawing. The REPL prompt is just the terminal's last scrolling line.
Scrollback, TTF rendering, and SGR color are all box-agnostic and keep
working unmodified.
4.4r -- reframed as a text/graphics mode toggle:
"Hide/show the scroll box" stopped meaning anything once the box was
removed; the underlying need survives as a whole-screen mode switch.
vt100_toggle_graphics() is a two-state machine (VISIBLE/HIDDEN) -- hidden
mode stops the terminal from touching the framebuffer while its logical
state keeps advancing, so direct framebuffer/TTF-TEXT drawing can use the
whole screen; showing again wipes and reuses scrollback_redraw() to
restore the terminal exactly. Reachable two ways, one transition function:
physically via Alt+TAB (4.4y revised from Ctrl+TAB) and programmatically
via the new ALT+TAB FORTH word.
Verified: three-arch clean QEMU boot + logs; amd64 screendump confirms
full-width text with no box/strip artifacts.
Punch list §25 items 4.4v/4.4r/4.4ab complete; 4.4y revised.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
draw_box_border() (vt100.c) strokes four 1px edges around the 640x480
CANVAS box, reusing the same border-gray constant the REPL strip's
border lines use (renamed VT100_STRIP_BORDER_GRAY -> VT100_BORDER_GRAY
since it's now shared -- one pinned color decision, 4.4w, not two).
Called from erase_display()'s box-scoped branch so the border survives
every box clear (the initial one and any later ESC[2J), not just the
first.
Verified: three-arch clean QEMU boot + logs, amd64 screendump showing a
full rectangle outline around the box, visually distinct from the strip
below it.
Punch list §25 item 4.4z complete.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Scope expanded from pure CANVAS-rectangle arithmetic (as originally
scoped) to also splitting the REPL prompt/input line out of the
scrollback box into an independent single-line strip, per Captain Bob's
explicit fold-in after the gap was reported (§25.0 rule 3) rather than
silently expanded.
vt100.c: VT100_BOX_ORIGIN_X/Y are no longer hardcoded per-arch literals --
both are now derived from fb_width()/fb_height() at vt100_enable_ttf()
time. New vt100_strip_draw() renders the bottom strip (gray border lines,
bright-white text) directly via the existing ttf_draw_glyph_cell()
rasterizer, independent of the box's own grid/cursor state. Border lines
are drawn after the glyph loop so an oversized cell can only be clipped
by them, never erase them.
console.c/console.h: console_fb_strip_draw() thin wrapper, matching the
existing console_fb_enable_ttf()/console_fb_scroll_*() pattern.
repl.c: builds a plain-text "[VMName] ok> <input>" mirror in
g_strip_prompt/strip_refresh(), refreshed on every keystroke (including
backspace) from sk_readline() -- already wired for item 4.4v, since
keyboard-typed characters will flow through the same console_getc() path
once that lands. Also widened sk_repl_step()/sk_repl_run()'s local input
buffer from a second, smaller 256-byte buffer to INPUT_BUFFER_SIZE
(1025), per 4.4w's decision.
Verified: three-arch clean QEMU boot + logs, amd64 screendump showing
the box and strip as two visually distinct regions with no visible
glyph/border clipping.
Punch list §25 item 4.4x complete.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
4.4w resolved: border gray = FB_ANSI_PALETTE[7] (0xAAAAAA); REPL input
line uses the full INPUT_BUFFER_SIZE=1025 buffer with left/right
horizontal scroll on a single line, not a smaller practical limit; the
15px/15px REPL-strip gaps and 8px box-to-strip gap from the second
mockup pass confirmed as-is. 4.4y resolved: toggle meta-key is Ctrl+TAB.
4.4u's own done-when (three open gaps resolved with Bob) is satisfied by
4.4w's resolution, so it's checked off too. Design-only, no code changes
in this commit -- 4.4x/4.4z pick up the drawing work these numbers
unblock.
Punch list §25 items 4.4u/4.4w/4.4y complete.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
vm_core.c: demote the per-word "ECW: w=... func=... 'NAME'" dispatch trace
from LOG_INFO to LOG_DEBUG. POST forces the logger to LOG_TEST for the
duration of the self-test run, and LOG_TEST includes LOG_INFO, so every
single word execution during POST was echoing this trace -- hundreds of
lines burying the actual module summaries and pass/fail tally. Still
available via --log-level=debug.
Combined with HEARTBEAT_DOE_LOG=0 (command-line Kconfig override, no
default change -- experiments/bare_metal/'s own DoE tooling still gets
HEARTBEAT_DOE_LOG=1 by default), all three architectures now boot clean:
UEFI -> POST summary -> Mama birth -> Hermes self-test -> heartbeat ->
ok>, with no [HADES][DOE] rows and no ECW flood. Verified by three-arch
QEMU boot; logs attached.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
