fix(v4): #190 POST regenerates the same; #16 sanitizers and hosted-check nightly

Captain Bob, 2026-11-13: "Create the issues then fix them before the long
acceptance test runs"; #16: "Nightly".

#190 -- make -C v4 post79 did not reproduce POST:
- mkpost.py runs v3 with address randomisation off (setarch -R): its
  printed addresses (>IN, FIND) are the same each run, so POST79.md is.
- v4/Makefile post79 builds hosted v3 from this tree's source first and
  uses it, not the lfs/ copy, which can be older.
- post_cases.c and POST79.md regenerated: 539 cases -- LOAD.rest_of_line,
  which v3 gets through since it changed after 2026-10-07. Two runs the
  same. POST_FLOOR 538 -> 539 (#173).
- test_host_unit.c takes the table's count, not 538 typed in the test.

#16 -- scripts/nightly.sh v4-checks: make -C v4 sanitize hosted-check,
logged under logs/<TS>/v4-checks/, refused without qemu-user; nightly.yml
runs it after publishing, before the proofs, installing qemu-user if the
image lacks it.

Evidence (logs/20261113-014927/post79, -024314): before, regenerated with
nothing changed: 539 cases and addresses differing run to run; after: the
same twice, hosted POST 539/539; test, test-32 99 programs 0 failures;
v4-checks 79 programs under the sanitizers 0 failures, the hosted builds
alike. The first verification failed at test_host_unit.c:442 (kept); a
stray v4-checks run stopped at once is kept, labelled (-014453).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017RzZgrf7V7Zk2iczBXDRbm

.gitea/workflows/nightly.yml

@@ -1,8 +1,9 @@
 # Nightly snapshot of the kernel images: the acceptance protocol, the board images, Nexus, then
-# the proofs. Each stage is a step of scripts/nightly.sh (its header says what each does); any
+# v4 under the sanitizers with the hosted builds (#16), and the proofs. Each stage is a step of scripts/nightly.sh (its header says what each does); any
 # failure stops the run, and nothing is published unless every stage before it passed. The proofs
 # come last and run whatever happened before them: they check the theories, not the images, so a
-# failed proof does not hold back images that passed acceptance -- it turns the run red.
+# failed proof does not hold back images that passed acceptance -- it turns the run red. The v4
+# checks (#16; Captain Bob, 2026-11-13: "Nightly") are the same: the engine on the host, not the images.
 #
 #   org.starship:kernelImage:<LITHOS_VERSION>-SNAPSHOT, starshipos-snapshots
 #     classifier pc      StarshipOS.iso   amd64, UEFI -- the ISO the amd64 acceptance boot booted
@@ -80,6 +81,15 @@ jobs:
           name: kernel-images-${{ github.run_number }}
           path: build/nightly/
 
+      - name: v4 under the sanitizers, and the hosted builds alike
+        if: always()
+        run: |                    # hosted-check runs aarch64 and riscv64 under qemu-user (#16)
+          if ! command -v qemu-aarch64 >/dev/null || ! command -v qemu-riscv64 >/dev/null; then
+            S=$([ "$(id -u)" = 0 ] || echo sudo)
+            $S apt-get update -qq && $S env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq qemu-user
+          fi
+          scripts/nightly.sh v4-checks
+
       - name: Isabelle/HOL proofs
         if: always()
         run: scripts/nightly.sh proofs

docs/v4.0.0/POST79.md

@@ -3,7 +3,7 @@
 Written by `v4/tools/mkpost.py` from `v4/tools/post79_rules.py`; do not edit.
 Design: `NUCLEUS.md` section 6. The cases are `v4/system/post_cases.c`.
 
-POST runs 538 cases. 431 are v3's, with what the hosted v3 binary did as the
+POST runs 539 cases. 432 are v3's, with what the hosted v3 binary did as the
 expected result. This file lists every other case, and why.
 
 ## 1. Rewritten for FORTH-79 (59)
@@ -60,11 +60,11 @@ standard's and not v3's.
 | `CMOVE.basic` | `HERE S" Test" DUP >R HERE 10 + SWAP CMOVE CR` | stack `317`, printed `\n` | `65 PAD C! 66 PAD 1+ C! PAD PAD 10 + 2 CMOVE PAD 10 + C@ . PAD 11 + C@ . CR` | stack `empty`, prints `65 66 \n` | v3's address unit is a byte; a v4 address unit is a cell (D-1); and the v3 case leaves a value on the return stack |
 | `TYPE.basic_string` | `HERE S" Hello" DUP >R HERE SWAP CMOVE HERE R> TYPE CR` | stack `392`, printed `Hello\n` | `72 PAD C! 105 PAD 1+ C! PAD 2 TYPE CR` | stack `empty`, prints `Hi\n` | v3's address unit is a byte; a v4 address unit is a cell (D-1); and FORTH-79: >R R> R@ are for use inside a definition; v4 refuses them at the prompt |
 | `TYPE.numbers` | `HERE S" 12345" DUP >R HERE SWAP CMOVE HERE R> TYPE CR` | stack `398`, printed `12345\n` | `49 PAD C! 50 PAD 1+ C! PAD 2 TYPE CR` | stack `empty`, prints `12\n` | v3's address unit is a byte; a v4 address unit is a cell (D-1); and FORTH-79: >R R> R@ are for use inside a definition; v4 refuses them at the prompt |
-| `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `657828592 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
+| `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `7884064 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
 | `UPDATE.no_block` | `0 SCR ! UPDATE` | error | unchanged | stack `empty`, prints nothing | v3 raises an error FORTH-79 does not ask for |
-| `SCR.after_load` | `1 LOAD SCR @ . CR` | stack `empty`, printed `` | unchanged | stack `empty`, prints `1 \n` | v3 prints nothing after 1 LOAD; SCR is still 1 from the LIST before |
+| `SCR.after_load` | `1 LOAD SCR @ . CR` | stack `empty`, printed `1 \n` | unchanged | stack `empty`, prints `1 \n` | v3 prints nothing after 1 LOAD; SCR is still 1 from the LIST before |
-| `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `657827952 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
+| `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `7883424 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
-| `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `658154448 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
+| `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `8203888 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
 | `FIND.empty` | `FIND` | error | unchanged | stack `0`, prints nothing | FORTH-79: FIND leaves 0 when there is no word; v3 raises an error |
 | `VOCABULARY.cross_vocab_access` | `VOCABULARY V1 V1 DEFINITIONS : V1WORD 11 ; FORTH V1WORD . CR` | stack `empty`, printed `11 \n` | unchanged | an error | FORTH-79: a word defined in another vocabulary is not found from FORTH; v3 finds it |
 | `VOCABULARY.duplicate` | `VOCABULARY TESTVOC VOCABULARY TESTVOC` | error | unchanged | stack `empty`, prints nothing | v3 raises an error FORTH-79 does not ask for: defining a name again |

logs/20261113-014453/v4-checks/README.txt

@@ -0,0 +1,3 @@
+# Stopped, not a result: started by mistake on 2026-11-13 by a test of v4-checks's refusal
+# without qemu-user, which found qemu-user after all (/bin is /usr/bin here). Stopped by hand
+# at once; the stage was then tested with a PATH holding no qemu-*.

logs/20261113-014927/post79/README.txt

@@ -0,0 +1,7 @@
+# #190: make -C v4 post79
+before-*: the table regenerated with nothing changed, with the committed lfs/amd64/starforth and with v3 built from source: 539 cases, LOAD.rest_of_line added (v3 changed since 2026-10-07); POST79.md's v3 addresses different each run.
+after-run1/2.log: post79 after the fix (v3 built from source, run with setarch -R): post_cases.c and POST79.md the same both runs; 539 cases; hosted POST 539/539.
+failed-1-*.log: the first verification after the fix: test_host_unit.c:442 wanted 538 POST cases, typed in the test; POST ran 539 of 539. The test now takes the table's own count.
+after-test-test32.log: make -C v4 test test-32 after both fixes: 99 programs, 3724162 checks, 0 failures.
+logs/20261113-024314/v4-checks: scripts/nightly.sh v4-checks (#16), its first real run: 79 programs under the sanitizers, 0 failures; the hosted builds alike.
+logs/20261113-020030/v4-checks: the same stage on the first verification, which failed at test_host_unit.c:442 (see failed-1-*).

logs/20261113-014927/post79/before-addresses-vary.txt

@@ -0,0 +1,8 @@
+# #190, before the fix: POST79.md as mkpost.py wrote it from v3 built from source (<) against the committed one (>):
+# v3's printed addresses differ. Two runs of that same binary also differed from each other: >IN.initial printed 1076337952, then 241286432.
+< | `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `1076337952 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
+> | `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `657828592 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
+< | `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `1076337312 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
+< | `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `1076657776 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
+> | `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `657827952 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
+> | `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `658154448 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |

logs/20261113-020030/v4-checks/README.txt

@@ -0,0 +1,2 @@
+# The first real run of scripts/nightly.sh v4-checks (#16), on the first verification of #190: it
+# stopped at test_host_unit.c:442 (538 typed in the test; POST ran 539). Kept as evidence.

scripts/nightly.sh

@@ -19,6 +19,10 @@
 #       found, and one value (#172 -- it was one distinct value, which two of the three could make).
 #   scripts/nightly.sh test-32
 #       make -C v4 test-32: v4 with 32-bit cells, every test (the acceptance's last part).
+#   scripts/nightly.sh v4-checks
+#       make -C v4 sanitize hosted-check (#16; Captain Bob, 2026-11-13: in the nightly): every v4
+#       test under ASan and UBSan at both widths, and the three hosted builds booting alike --
+#       aarch64 and riscv64 under qemu-user (make init). Its log is logs/<TS>/v4-checks/.
 #   scripts/nightly.sh proofs
 #       isabelle build -c -D proof/, capped to fit the server (one thread, small heaps): the StarForth
 #       session checked afresh every run, whatever is
@@ -76,7 +80,7 @@ DOCS=build/nightly-docs
 LITHOS=$(sed -n 's/^LITHOS_VERSION *?= *//p' kernel/Makefile)
 VERSION=${NIGHTLY_VERSION:-$LITHOS-SNAPSHOT}
 usage() {
-    echo "Usage: scripts/nightly.sh accept <amd64|aarch64|riscv64|stick-high> | test-32 | proofs | images" >&2
+    echo "Usage: scripts/nightly.sh accept <amd64|aarch64|riscv64|stick-high> | test-32 | v4-checks | proofs | images" >&2
     echo "                          | publish <URL> | docs | publish-docs <URL> | gitea-release <tag>" >&2
     echo "                          | protocol [<stage>...] | protocol-report | dict-hash | post-count" >&2
     echo "  protocol stages: $PROTOCOL_STAGES" >&2
@@ -182,6 +186,14 @@ test-32)
     make --no-print-directory -C v4 test-32 2>&1 | tee "$OUT/test-32.txt"
     echo "=== nightly: test-32: $(grep -cE '[0-9]+ checks, 0 failures' "$OUT/test-32.txt") programs, 0 failures"
     ;;
+v4-checks)
+    command -v qemu-aarch64 >/dev/null && command -v qemu-riscv64 >/dev/null \
+        || { echo "nightly: v4-checks needs qemu-user (qemu-aarch64, qemu-riscv64): make init" >&2; exit 1; }
+    ts=$(date -u +%Y%m%d-%H%M%S)
+    mkdir -p "logs/$ts/v4-checks"
+    make --no-print-directory -C v4 sanitize hosted-check 2>&1 | tee "logs/$ts/v4-checks/v4-checks-$ts.log"
+    echo "=== nightly: v4-checks: $(grep -cE '[0-9]+ checks, 0 failures' "logs/$ts/v4-checks/v4-checks-$ts.log") programs under the sanitizers, 0 failures; the hosted builds alike"
+    ;;
 proofs)
     need "$OUT/.started"
     ts=$(date -u +%Y%m%d-%H%M%S)

v4/Makefile

@@ -218,13 +218,16 @@ $(foreach i,$(HOSTED_ISAS),$(eval $(call HOSTED_RULE,$(i))))
 # `make post` boots the amd64 system alone, which is the quick check after a
 # change to the vocabulary: nucleus, forth79.4th, POST, prompt.  `make
 # post79` writes POST's cases, system/post_cases.c, again from
-# v3's cases and tools/post79_rules.py (tools/mkpost.py); it needs the
+# v3's cases and tools/post79_rules.py (tools/mkpost.py), with the hosted v3
-# hosted v3 binary.
+# binary built first from this tree's source -- v3/Makefile, in its own build
+# directory; not the lfs/ copy, which can be older (#190).
+V3_HOSTED = $(shell $(MAKE) -s -C $(ROOT) -f v3/Makefile --eval 'v3bin: ; @echo $$(BINARY)' v3bin 2>/dev/null)
 .PHONY: post post79
 post: $(BINDIR)/starforth4-amd64
 	@$(BINDIR)/starforth4-amd64 < /dev/null
 post79:
-	python3 $(HERE)/tools/mkpost.py
+	$(MAKE) --no-print-directory -C $(ROOT) -f v3/Makefile $(V3_HOSTED)
+	python3 $(HERE)/tools/mkpost.py --v3 $(ROOT)/$(V3_HOSTED)
 
 # `make hosted` builds the three.  `make hosted-check` boots each with no
 # input and requires that all three print the same lines, ending in

v4/system/POST_FLOOR

@@ -1,3 +1,3 @@
-538
+539
 # v4 POST: the fewest tests an accepted boot may report (#173). Raise it when POST grows;
 # never lower it without Captain Bob. scripts/nightly.sh post-count reads the first line.

v4/tests/test_host_unit.c

@@ -439,8 +439,11 @@ int main(void)
         uint64_t hash = v4_image_dict_hash(hera, &im);
         memcpy(before, hera->mem, sizeof before);
         host.self = 0; host.n = hera; host.line = post_line; host.say = post_say;
-        CHECK(v4_post_run(&host, v4_post_cases, v4_post_case_count, &tally) && tally.tests == 538 && tally.pass == 538 && tally.fail == 0
+        char want_line[64];       /* the table's own count, not a number typed here: it was 538, POST grew (#190) */
-              && strstr(post_said, "PARITY:V4_POST tests=538 pass=538 fail=0\n") != NULL && strstr(post_said, "POST FAIL") == NULL,
+        snprintf(want_line, sizeof want_line, "PARITY:V4_POST tests=%u pass=%u fail=0\n", v4_post_case_count, v4_post_case_count);
+        CHECK(v4_post_run(&host, v4_post_cases, v4_post_case_count, &tally) && tally.tests == v4_post_case_count
+              && tally.pass == v4_post_case_count && tally.fail == 0
+              && strstr(post_said, want_line) != NULL && strstr(post_said, "POST FAIL") == NULL,
               "and passes POST, which the kernel runs on her: %u of %u, %u failed; \"%s\"", tally.pass, tally.tests, tally.fail, post_said);
         CHECK(strcmp(tell(10, "RS1"), "42 42 \n") == 0, "while POST runs, what its cases define is on her: \"%s\"", printed);
         CHECK(strstr(tell(10, "COLD"), "Cold Start") != NULL, "the kernel puts her back to the system as it was sealed");

v4/tools/mkpost.py

@@ -29,7 +29,9 @@ and the same lines.)
 """
 import argparse
 import os
+import platform
 import re
+import shutil
 import subprocess
 import sys
 
@@ -252,7 +254,13 @@ def run_v3(v3, cases):
         script.extend(line[3:] for line in case["lines"])
         script.append('." [[E%d]]" BASE @ DECIMAL .S BASE ! ." [[S%d]]"' % (n, n))
     script.append("BYE")
-    done = subprocess.run([v3, "--log-none"], input=("\n".join(script) + "\n").encode("latin-1"),
+    # With the address space randomised, what v3 prints for an address (>IN, FIND) is different on
+    # every run, so the report (POST79.md) could never be written twice the same (#190): v3 is run
+    # with randomisation off (setarch -R), and its addresses are the same each time.
+    cmd = [v3, "--log-none"]
+    if shutil.which("setarch"):
+        cmd = ["setarch", platform.machine(), "-R"] + cmd
+    done = subprocess.run(cmd, input=("\n".join(script) + "\n").encode("latin-1"),
                           capture_output=True, timeout=600)
     text = ANSI.sub("", done.stdout.decode("latin-1"))        # a byte is a character
     results = []