admin/LithosAnanake
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix(v4.0.0): POST leaves nothing, as v3 really does; and what the review of step 6b found

Browse Source 
Captain Bob was told that v3 leaves the words POST's cases define in the
dictionary, and ruled that v4 should.  That was false: v3's run_test_suite
puts the dictionary back after each word's cases (test_common.c:333,
:365).  Shown that, he ruled that POST leaves nothing.  The boot now
seals the system, runs POST, and has the node do COLD, whose printing is
not shown; PARITY:V4_SYSTEM is the system as sealed.

A case the node does not come back from ends POST there, named, with how
many were not run: it would have stalled the boot for hours, where the
capsule had ended it.  The runner's test of it now uses a word that
really never ends.

hosted-check also requires that RS1 and T{ are unknown after boot, and
boots a program whose POST has failing cases (tests/post_cases_fail.c):
PARITY:FAIL, POST: FAILED, no prompt, none of a case's printing shown.

Comments and documents that still named the POST capsule or its two
hooks are brought up to date; NUCLEUS.md 6.3 says what v3 does, with the
lines, and how the wrong ruling came about.

make -C v4 test, sanitize and hosted-check pass; amd64, aarch64 and
riscv64 boot, POST 538 of 538, word_count=314, dict_hash
0x220ab283a504a3b3 on all six: logs/20261007-112638, -112901, -113220.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
rajames
2026-10-07 11:40:20 -04:00
co-authored by Claude Opus 5.5
parent eda6577a53
commit 18adf59091
17 changed files with 669 additions and 65 deletions
Download Patch File Download Diff File Expand all files Collapse all files
v4/Makefile
+20 -4
View File
@@ -27,7 +27,7 @@ CFLAGS ?= $(CSTD) $(WARN) $(OPT)
HERE := $(patsubst %/,%,$(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
SRCS := $(wildcard $(HERE)/src/*.c)
TESTS := $(wildcard $(HERE)/tests/*.c)
TESTS := $(wildcard $(HERE)/tests/test_*.c)
# Cell widths to build and verify. 32 is the F18/Zynq case, 64 the aarch64
# host case; see DECOMPOSITION.md D-5.
@@ -183,10 +183,11 @@ post79:
# PARITY:OK, POST: PASSED and the prompt: the same hashes on every ISA. It
# also checks that what the boot loaded is part of the system: after COLD
# the capsule's words and the kernel's are still there, and FORGET refuses
# them.
# them; that POST has left nothing of itself or of what its cases defined;
# and that a boot whose POST has a failing case fails.
.PHONY: hosted hosted-check
hosted: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/starforth4-$(i))
hosted-check: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/boot-$(i).txt)
hosted-check: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/boot-$(i).txt) $(BINDIR)/starforth4-postfail
@grep -q '^POST: PASSED$$' $(BINDIR)/boot-amd64.txt || { echo "hosted-check: no POST: PASSED"; exit 1; }
@cmp $(BINDIR)/boot-amd64.txt $(BINDIR)/boot-aarch64.txt
@cmp $(BINDIR)/boot-amd64.txt $(BINDIR)/boot-riscv64.txt
@@ -194,7 +195,22 @@ hosted-check: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/boot-$(i).txt)
@grep -q '^ok> 0 12 ok$$' $(BINDIR)/cold-amd64.txt || { echo "hosted-check: COLD lost the capsule's words"; cat $(BINDIR)/cold-amd64.txt; exit 1; }
@grep -q '^ok> Protected word$$' $(BINDIR)/cold-amd64.txt || { echo "hosted-check: a capsule word could be forgotten"; exit 1; }
@grep -q '^ok> Goodbye!$$' $(BINDIR)/cold-amd64.txt || { echo "hosted-check: COLD lost BYE"; exit 1; }
@echo "hosted-check: amd64, aarch64 and riscv64 boot identically"
@printf 'RS1\nT{\nWORDS\n' | $(BINDIR)/starforth4-amd64 > $(BINDIR)/after-post-amd64.txt
@grep -q "^ok> UNKNOWN WORD: 'RS1'$$" $(BINDIR)/after-post-amd64.txt || { echo "hosted-check: a word a POST case defined is still there"; exit 1; }
@grep -q "^ok> UNKNOWN WORD: 'T{'$$" $(BINDIR)/after-post-amd64.txt || { echo "hosted-check: POST's harness is on the node"; exit 1; }
@$(BINDIR)/starforth4-postfail < /dev/null > $(BINDIR)/postfail.txt; test $$? -ne 0 || { echo "hosted-check: a boot with a failing case did not fail"; exit 1; }
@grep -q '^POST FAIL: fail.wrong out<5 5 $$' $(BINDIR)/postfail.txt || { echo "hosted-check: the failing case was not named"; cat $(BINDIR)/postfail.txt; exit 1; }
@grep -q '^POST FAIL: fail.many out<QQQQ' $(BINDIR)/postfail.txt || { echo "hosted-check: the case that prints too much was not named"; exit 1; }
@grep -q '^PARITY:V4_POST tests=4 pass=2 fail=2$$' $(BINDIR)/postfail.txt || { echo "hosted-check: the tally is wrong"; cat $(BINDIR)/postfail.txt; exit 1; }
@grep -q '^POST: FAILED$$' $(BINDIR)/postfail.txt && grep -q '^PARITY:FAIL$$' $(BINDIR)/postfail.txt || { echo "hosted-check: no PARITY:FAIL, POST: FAILED"; exit 1; }
@! grep -q '^ok> \|^5 5 $$\|PARITY:OK\|PARITY:V4_SYSTEM' $(BINDIR)/postfail.txt || { echo "hosted-check: a failed boot gave a prompt, or showed a case's printing"; exit 1; }
@echo "hosted-check: amd64, aarch64 and riscv64 boot identically; a boot with a failing case fails"
# A hosted program whose POST has a case that fails (tests/post_cases_fail.c
# in the place of system/post_cases.c): hosted-check boots it and requires
# that the boot stops there. docs/v4.0.0/MESH.md step 6b, acceptance 4.
$(BINDIR)/starforth4-postfail: $(BINDIR)/starforth4-amd64 $(HERE)/tests/post_cases_fail.c
$(CC) $(SYSTEM_CFLAGS) -static $(BINDIR)/hosted-amd64.o $(BINDIR)/v4_image_64.c $(CAPSULE_DIR_C) $(ENGINE_SRCS) $(filter-out %/post_cases.c,$(SYSTEM_SRCS)) $(HERE)/tests/post_cases_fail.c $(BINDIR)/v3o-amd64/*.o -o $@
.PHONY: all test sanitize clean $(addprefix test-,$(WIDTHS))