docs(v4.0.0): step 6b -- POST is the kernel's: design, acceptance and plan
NUCLEUS.md 6.3 and section 7 as approved 2026-10-07: the kernel holds the cases as a table and feeds them to the node; a runner judges from outside; what the cases define stays, as in v3; a PARITY:V4_SYSTEM line after POST. The capsule harness and its two nucleus variables are withdrawn (6.3a keeps what they were). MESH.md step 6b has the acceptance. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 5.5
parent
9bfd5071d2
commit
b04ae55ec5
+22
-5
@@ -704,11 +704,28 @@ Each is tested, committed and pushed before the next.
|
||||
identities, a device joining at the end and known when it returns,
|
||||
release by asking, holes. Its acceptance is to be approved before it is
|
||||
built.
|
||||
**6b. POST is the kernel's.** Ruled 2026-10-07 (section 9): the kernel
|
||||
holds POST's cases and feeds them to Hera itself, with no POST words
|
||||
loaded into her dictionary. Today they are a capsule she loads
|
||||
(`NUCLEUS.md` section 6). Its design and acceptance are to be approved
|
||||
before it is built.
|
||||
**6b. POST is the kernel's.** Ruled 2026-10-07 (section 9); design
|
||||
approved 2026-10-07, `NUCLEUS.md` 6.3 and section 7. Acceptance, as
|
||||
approved:
|
||||
1. *Same verdict.* The three hosted programs and the three bare-metal
|
||||
boots print `PARITY:V4_POST tests=538 pass=538 fail=0`,
|
||||
`PARITY:V4_SYSTEM word_count=N dict_hash=0x...`, `PARITY:OK` and
|
||||
`POST: PASSED`, with the same hashes on all six.
|
||||
2. *Nothing of the harness is on the node.* At the prompt `T{` is an
|
||||
unknown word, and `(CATCH)` and `(EMIT-HOOK)` are gone from the
|
||||
nucleus.
|
||||
3. *What the cases define is there.* A word a case defines can be used
|
||||
at the prompt after boot, and survives `COLD`.
|
||||
4. *The judge can fail.* Given a case with a wrong expected stack, one
|
||||
with wrong expected output, one that must end in an error and does
|
||||
not, and one that ends in an error and must not, the runner reports
|
||||
each as a failure by name, and a boot with a failing case ends
|
||||
`PARITY:FAIL`, `POST: FAILED`.
|
||||
5. *A case's printing does not reach the console.* The boot log shows
|
||||
nothing that a passing case printed.
|
||||
6. *The suite.* `make -C v4 test` and `sanitize` pass at both widths;
|
||||
`mkcapsule --lint capsules/` is clean.
|
||||
|
||||
7. **A second unit; scaling while running; sleep, wake and kill by
|
||||
command.**
|
||||
8. **The hosted product is the five nodes**, on three ISAs: acceptance 1
|
||||
|
||||
+55
-17
@@ -156,31 +156,64 @@ departure is reported.
|
||||
|
||||
### 6.3 Form
|
||||
|
||||
`post79.4th` defines a small harness in FORTH and a tally. The harness
|
||||
needs two things from the nucleus that FORTH-79 does not provide. Both are
|
||||
variables an assembled word consults, and both have FORTH names:
|
||||
**Ruled 2026-10-07 (`MESH.md` step 6b): POST is the kernel's, as in v3.**
|
||||
The kernel holds the cases and feeds them to the node; nothing of POST's
|
||||
harness is loaded into the node's dictionary. What this section said
|
||||
before — a harness in FORTH in `post79.4th`, and two variables in the
|
||||
nucleus for it, `(CATCH)` and `(EMIT-HOOK)` — is withdrawn; 6.3a keeps it
|
||||
for the record.
|
||||
|
||||
| Variable | Consulted by | Effect while not zero |
|
||||
|---|---|---|
|
||||
| `(CATCH)` | the prompt loop (`quit.v4`) | A line that ends in an error does not say `ERROR`: `(CATCH)` is set to −1 and the line ends ` ok`. POST can then go on to its next case, and can check a case that must fail. |
|
||||
| `(EMIT-HOOK)` | `EMIT` (`core.v4`) | It holds the xt of a word ( c -- ) that is given each character instead of the console. POST uses it to compare what a case prints, and it keeps the messages of expected errors out of the boot log. |
|
||||
**v3, as built.** The cases are C tables compiled into the kernel
|
||||
(`v3/src/test_runner/modules/*.c`). For each, the kernel hands the line to
|
||||
the interpreter, reads the VM's error flag, and puts the VM's stack
|
||||
pointers, error and mode back (`test_common.c`, `run_single_test`). It
|
||||
runs once at boot on the first VM, against block RAM of POST's own, and
|
||||
the parity line is taken afterwards. Whatever the cases define stays in
|
||||
the dictionary.
|
||||
|
||||
The prompt loop sets `(EMIT-HOOK)` to 0 at the end of every line, so the
|
||||
console cannot be left silent. (This section first said one nucleus word
|
||||
would do; reading `quit.v4` and `core.v4` showed it takes these two.
|
||||
Amended 2026-10-05.)
|
||||
**v4.**
|
||||
|
||||
An error always ends the line it is on, so a case is several short lines
|
||||
and the harness words work across them.
|
||||
- *The cases* are a table in C, `v4/system/post_cases.c`, generated by
|
||||
`v4/tools/mkpost.py` (6.4) and linked into the hosted program and the
|
||||
kernel. Each is a name, its lines of FORTH, whether an error is
|
||||
expected, and what it must leave: the data stack, or only how many
|
||||
values for an address-dependent case (6.5), and the text it prints.
|
||||
- *The runner*, `v4/system/post.c`, is the kernel's and is shared by the
|
||||
hosted program, the bare-metal kernel and the tests. For each case it
|
||||
empties the node's data stack from outside; sends `DECIMAL FORTH
|
||||
DEFINITIONS`, the state every expected value was generated from (6.4);
|
||||
sends the case's lines one at a time, as the boot sends any line,
|
||||
keeping what the node prints and showing none of it; and judges. A case
|
||||
passes when it ended in an error exactly if one was expected and, if
|
||||
none was, its stack and its printed text are what the table has. An
|
||||
error ends the line it is on, so a case is several short lines; it has
|
||||
ended in an error if any of its lines did.
|
||||
- *What it prints.* For a failing case, `POST FAIL: name out<...>
|
||||
stack<...>`. Then `PARITY:V4_POST tests=N pass=N fail=N`.
|
||||
- *What is left.* What the cases define stays in the dictionary, as in
|
||||
v3 (ruled 2026-10-07, on being told that the capsule had ended with
|
||||
`FORGET` and left nothing). The system is sealed after POST, so `COLD`
|
||||
comes back to those words and `FORGET` will not go below them. Measured
|
||||
2026-10-07: they take about 1,290 cells of the 5,632 in the dictionary
|
||||
space.
|
||||
- *Gone:* `capsules/v4/post79.4th` and its blocks 7000 up; the harness
|
||||
words; `(CATCH)` and `(EMIT-HOOK)`, with what `EMIT` and the prompt
|
||||
loop did for them.
|
||||
|
||||
After the last case POST prints the number of cases, passes and failures,
|
||||
and names each failing case.
|
||||
### 6.3a As it was until step 6b
|
||||
|
||||
`post79.4th` defined a small harness in FORTH and a tally, and needed two
|
||||
variables from the nucleus: `(CATCH)`, so that a line ending in an error
|
||||
ended ` ok` and POST could go on; and `(EMIT-HOOK)`, the xt of a word given
|
||||
each character in place of the console, so that POST could compare what a
|
||||
case printed. Its last block was `T-REPORT` and `FORGET T#`: the harness
|
||||
and everything the cases had defined were forgotten.
|
||||
|
||||
### 6.4 Generating the expected values
|
||||
|
||||
`v4/tools/mkpost.py` reads the v3 test modules, keeps the cases for
|
||||
Required Word Set words, runs them in one session of the hosted v3 binary,
|
||||
and writes `capsules/v4/post79.4th`. It is a development tool
|
||||
and writes `v4/system/post_cases.c` (until step 6b, `capsules/v4/post79.4th`). It is a development tool
|
||||
(`make -C v4 post79`), run when the cases or the rules change; its output
|
||||
is committed and reviewed like any source. Every case starts from the same
|
||||
state on both machines: empty stack, `DECIMAL`, `FORTH DEFINITIONS`.
|
||||
@@ -221,13 +254,18 @@ The boot prints, in order:
|
||||
```
|
||||
PARITY:V4_NUCLEUS words=N image_hash=0x...
|
||||
PARITY:V4_CAPSULE name=v4:forth79.4th capsule_id=0x... capsule_hash=0x... dict_hash=0x...
|
||||
PARITY:V4_CAPSULE name=v4:post79.4th capsule_id=0x... capsule_hash=0x... dict_hash=0x...
|
||||
PARITY:V4_POST tests=N pass=N fail=N
|
||||
PARITY:V4_SYSTEM word_count=N dict_hash=0x...
|
||||
PARITY:OK
|
||||
POST: PASSED
|
||||
ok>
|
||||
```
|
||||
|
||||
`PARITY:V4_SYSTEM` (step 6b) is the parity of the system as it is sealed,
|
||||
after POST, as v3's `PARITY:M7.1a` is taken after POST: how many words
|
||||
FORTH holds and the dictionary hash. Until step 6b the POST capsule had a
|
||||
`PARITY:V4_CAPSULE` line of its own in that place.
|
||||
|
||||
On any failure it prints `PARITY:FAIL` and `POST: FAILED` in place of the
|
||||
last three lines and does not give a prompt.
|
||||
|
||||
|
||||
@@ -0,0 +1,138 @@
|
||||
# Step 6b: POST Is the Kernel's — Implementation Plan
|
||||
|
||||
> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking.
|
||||
|
||||
**Goal:** The kernel holds POST's cases and feeds them to Hera itself; nothing of POST's harness is in her dictionary.
|
||||
|
||||
**Architecture:** `mkpost.py` writes a C table of cases instead of a capsule. A runner, `v4/system/post.c`, sends each case's lines to the node through a callback its host supplies, keeps what the node prints, reads the node's data stack from outside, and judges. `boot.c` calls it where it loaded the POST capsule. The two nucleus variables the capsule harness needed go.
|
||||
|
||||
**Tech Stack:** C99, Python 3 (`v4/tools/mkpost.py`), the v4 nucleus dialect, `make -C v4`, `make -f kernel/Makefile`.
|
||||
|
||||
**Spec:** `docs/v4.0.0/NUCLEUS.md` 6.3 and section 7; acceptance in `docs/v4.0.0/MESH.md` step 6b.
|
||||
|
||||
## Global Constraints
|
||||
|
||||
- Branch `StarForth-v4.0.0`, main checkout. No new branch, no stash, no worktree. Commit and push after every task; end messages with `Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>`.
|
||||
- v4 follows the OS as designed: read how v3 does a thing before building it, and report a departure instead of building it.
|
||||
- No stubs or stand-ins. Do not fix anything in v3.
|
||||
- The cases are the same 538, with the same lines, as `capsules/v4/post79.4th` has today: the generator's choice of cases and its cutting of lines are not changed.
|
||||
- What the cases define stays in the dictionary; the system is sealed after POST.
|
||||
- Boot lines, in order: `PARITY:V4_NUCLEUS`, `PARITY:V4_CAPSULE name=v4:forth79.4th`, `PARITY:V4_POST tests=N pass=N fail=N`, `PARITY:V4_SYSTEM word_count=N dict_hash=0x%016llx`, `PARITY:OK`, `POST: PASSED`.
|
||||
- Before any QEMU run read `.claude/CLAUDE.md` "Running / Acceptance" and the memory note `acceptance-test-rules.md`. One QEMU at a time, `clean` before `qemu`, all three ISAs, logs kept. Never delete a log.
|
||||
|
||||
## Review Focus
|
||||
|
||||
1. **A case whose line never ends** (a loop, or a word waiting for the keyboard). Expected: the generator already leaves such cases out; the runner treats a line that does not come back as a failed case and POST as failed, and does not hang the boot silently. Test in Task 2.
|
||||
2. **A case that prints more than the runner keeps.** Expected: it fails by name; nothing is written past the buffer. Test in Task 2.
|
||||
3. **A case that leaves more on the stack than the table holds, or a full stack.** Expected: compared by depth first; a mismatch fails the case. Test in Task 2.
|
||||
4. **An error in the line that sets the state** (`DECIMAL FORTH DEFINITIONS`). Expected: the case fails by name. Test in Task 2.
|
||||
5. **The dictionary filling during POST**, now that nothing is forgotten. Expected: 538 of 538 with room to spare (measured about 1,290 of 5,632 cells); if a case fails for want of room, stop and report. Checked in Task 4.
|
||||
|
||||
---
|
||||
|
||||
### Task 1: The generator writes a table
|
||||
|
||||
**Files:** Modify `v4/tools/mkpost.py`, `v4/Makefile` (`post79` target's comment); Create `v4/include/v4/post.h`, `v4/system/post_cases.c` (generated); Regenerate `docs/v4.0.0/POST79.md`
|
||||
|
||||
**Interfaces — Produces** (`post.h`):
|
||||
```c
|
||||
#define V4_POST_STACK 0 /* the stack and the output are compared */
|
||||
#define V4_POST_DEPTH 1 /* only how many values are left; the output is not compared */
|
||||
#define V4_POST_DEPTH_OUTPUT 2 /* how many values, and the output */
|
||||
#define V4_POST_ERROR 3 /* it must end in an error; nothing else is compared */
|
||||
typedef struct {
|
||||
const char *name;
|
||||
const char *const *lines; /* line_count of them */
|
||||
unsigned line_count;
|
||||
int expect; /* V4_POST_* */
|
||||
const long long *stack; /* depth values, the deepest first */
|
||||
unsigned depth;
|
||||
const char *output; /* output_len characters */
|
||||
unsigned output_len;
|
||||
} v4_post_case;
|
||||
extern const v4_post_case v4_post_cases[];
|
||||
extern const unsigned v4_post_case_count;
|
||||
```
|
||||
|
||||
- [ ] **Step 1:** In `mkpost.py`, keep everything up to the choice and cutting of cases as it is. Replace the writing of blocks: for each case keep `lines` with the `T| ` prefix taken off, and the expectation as data (the mode, the stack list, the output string) where `expectation()` now returns harness lines. Write `v4/system/post_cases.c`: one `static const char *const` array of lines and one `static const long long` array of stack values per case, then the table. Escape every character of a line or an output that is not printable ASCII, and `"` and `\`, as octal. Remove `HARNESS` and the block writer; `OUTPUT` becomes the C file. `POST79.md`'s header line says the cases are in `v4/system/post_cases.c`.
|
||||
- [ ] **Step 2: Check the count before running it.** `grep -c '^T{ ' capsules/v4/post79.4th` is 538. Run `make -C v4 post79`; the report says 538 cases, and `grep -c '^ { "' v4/system/post_cases.c` is 538. If the number differs, stop: the generator's choice of cases changed.
|
||||
- [ ] **Step 3: Check the lines are the same.** A one-off script in the scratchpad: the `T| ` lines of the old capsule, in order with the prefix removed, equal the table's lines in order. Zero differences.
|
||||
- [ ] **Step 4:** `cc -std=c99 -Wall -Wextra -Wpedantic -Werror -Iv4/include -DV4_CELL_BITS=64 -c v4/system/post_cases.c -o /dev/null` compiles clean.
|
||||
- [ ] **Step 5: Commit** `feat(v4.0.0): POST's cases as a table the kernel holds` and push. (The capsule is still there and still what the boot runs.)
|
||||
|
||||
---
|
||||
|
||||
### Task 2: The runner
|
||||
|
||||
**Files:** Create `v4/system/post.c`, `v4/tests/test_host_post.c`; Modify `v4/include/v4/post.h`, `v4/Makefile` (tests named `test_host_post*.c` link `post.c`)
|
||||
|
||||
**Interfaces — Produces:**
|
||||
```c
|
||||
#define V4_POST_OUT 1024u /* the most of a case's printing that is kept */
|
||||
typedef struct {
|
||||
void *self;
|
||||
v4_node *n; /* the node POST is run on: its data stack is read and emptied */
|
||||
/* Send the node a line and run it to its end. What it prints is put at
|
||||
* `out`, at most `cap` characters, and *len is how many it printed in
|
||||
* all. Returns V4_TEXT_QUIT, V4_TEXT_COMPLETED or V4_TEXT_ERROR
|
||||
* (message.h), or a negative number if the line did not come back. */
|
||||
int (*line)(void *self, const char *text, unsigned text_len, char *out, unsigned cap, unsigned *len);
|
||||
void (*say)(void *self, const char *text, unsigned len); /* the console */
|
||||
} v4_post_host;
|
||||
typedef struct { unsigned tests, pass, fail; } v4_post_tally;
|
||||
/* Run the cases. Prints a line for each failing case and the PARITY:V4_POST
|
||||
* line. Returns 1 if none failed. */
|
||||
int v4_post_run(const v4_post_host *h, const v4_post_case *cases, unsigned count, v4_post_tally *tally);
|
||||
```
|
||||
|
||||
- [ ] **Step 1: Write the failing test** `test_host_post.c`: a host node with the nucleus assembled as `test_host_quit.c` assembles it, a kernel that serves its requests, and a `line` callback built on the same exchange of messages that test's `say` uses, returning the raw text and how the line ended. Cases written in the test, each with the verdict it must get:
|
||||
- `1 2 +` expecting stack `3`, no output: passes; `5 DUP . . CR` expecting empty stack and `5 5 \n`: passes;
|
||||
- `1 2 +` expecting `4`: fails; expecting two values: fails (Review Focus 3);
|
||||
- `65 EMIT` expecting output `B`: fails; expecting `A`: passes;
|
||||
- `NOSUCHWORD` expecting an error: passes; expecting stack empty: fails;
|
||||
- `1 2 +` expecting an error: fails;
|
||||
- a case of two lines, `: PQ 7 ;` then `PQ`, expecting `7`: passes, and afterwards `PQ` is still a word on the node;
|
||||
- a depth-only case `HERE` expecting depth 1: passes; depth 2: fails;
|
||||
- a case printing 2,000 characters: fails by name, and the byte after the runner's buffer is untouched (Review Focus 2);
|
||||
- a `line` callback that returns -1 for one case: that case fails, the rest are still judged, and the run returns 0 (Review Focus 1);
|
||||
- with `BASE` left at 16 and a non-empty stack before a case, the case still sees decimal and an empty stack;
|
||||
- a callback that makes the state line end in an error: the case fails by name (Review Focus 4).
|
||||
The tally and the `PARITY:V4_POST tests=N pass=N fail=N` line match the count; each failing case is named in a `POST FAIL: ` line; no passing case's output reaches `say`.
|
||||
- [ ] **Step 2: Run** `make -C v4 run-64-test_host_post.c`: fails to build, there is no `v4_post_run`.
|
||||
- [ ] **Step 3: Write `post.c`.** Nothing from the C library (the kernel links it). For each case: `v4_dstack_reset`; the state line, which must complete; each line in turn, the output appended to one buffer of `V4_POST_OUT`, an error on any line remembered; then the verdict:
|
||||
```c
|
||||
if (c->expect == V4_POST_ERROR) ok = errored && came_back;
|
||||
else if (errored || !came_back) ok = 0;
|
||||
else {
|
||||
ok = n->ds.depth == c->depth;
|
||||
if (ok && c->expect == V4_POST_STACK)
|
||||
for (k = c->depth; ok && k-- > 0; ) ok = v4_dstack_pop(&n->ds) == (v4_cell)c->stack[k];
|
||||
if (ok && c->expect != V4_POST_DEPTH)
|
||||
ok = total == c->output_len && total <= V4_POST_OUT && same(out, c->output, total);
|
||||
}
|
||||
```
|
||||
Read the stack before anything is popped when printing a failing case's `stack<...>`. `v4_dstack_reset` after every case.
|
||||
- [ ] **Step 4: Run** at 64 and 32 bits and under the sanitizers: 0 failures.
|
||||
- [ ] **Step 5: Commit** `feat(v4.0.0): the POST runner -- the kernel feeds a case and judges it from outside` and push.
|
||||
|
||||
---
|
||||
|
||||
### Task 3: The boot runs it, and the hooks go
|
||||
|
||||
**Files:** Modify `v4/system/boot.c` (the POST capsule out of `boot_capsules`; `post_watch` and its variables out; a line function that keeps output; the call of `v4_post_run`; the `PARITY:V4_SYSTEM` line), `v4/Makefile` (`SYSTEM_SRCS`), `kernel/Makefile:623-624` (`post.o`, `post_cases.o`), `v4/capsule/core.v4` (`EMIT`), `v4/capsule/quit.v4` (`(DONE)`, the two headers), `v4/tests/host_map.h`, `v4/tests/test_host_unit.c`; Delete `capsules/v4/post79.4th`
|
||||
|
||||
- [ ] **Step 1: Tests first.** In `test_host_unit.c`, Hera's POST becomes `v4_post_run` with a `line` callback built on the test's `tell`, and the check is the tally: 538, 538, 0. Add: after it, `T{` on Hera is an unknown word; `RS1` (defined by case `>R.basic`) is a word on Hera and still is after `COLD`. In `test_host_quit.c` add that `(CATCH)` and `(EMIT-HOOK)` are unknown words. Run and see them fail.
|
||||
- [ ] **Step 2: `boot.c`.** Split `v4_boot_line` so that its loop takes where the output goes; `v4_boot_line` passes the console and POST's callback passes a buffer. After the capsules: `v4_post_run`; on a failure `PARITY:FAIL`, `POST: FAILED`, return 0. Then `v4_image_seal`, then `PARITY:V4_SYSTEM word_count=` (the count of FORTH's words that `PARITY:V4_NUCLEUS` already uses) ` dict_hash=`, then `PARITY:OK`, `POST: PASSED`. `V4_POST_AT_BOOT=0` still leaves POST out.
|
||||
- [ ] **Step 3: The nucleus.** `EMIT` loses its first line and the `NONE:` label; `(DONE)` loses the store to `(EMIT-HOOK)` and the `(CATCH)` branch, so an error always ends `2 jump (FINISH)`; the two `header` lines, the two constants in `host_map.h` and their comments go.
|
||||
- [ ] **Step 4:** `git rm capsules/v4/post79.4th`; remove it from `host_open` in `test_host_unit.c`. `v4/build/mkcapsule --lint capsules/` is clean.
|
||||
- [ ] **Step 5: Run** `make -C v4 clean`, then `test`, `sanitize`, `hosted-check`. Update `hosted-check`'s greps in `v4/Makefile` if they name the POST capsule's line. All pass; the three hosted programs print the same `PARITY:V4_SYSTEM` line.
|
||||
- [ ] **Step 6: Acceptance 4 on the product.** With one case's expected stack changed by hand in a scratch copy of `post_cases.c` built into a scratch hosted binary (not committed), the boot names the case, prints `PARITY:FAIL` and `POST: FAILED`, and gives no prompt.
|
||||
- [ ] **Step 7: Commit** `feat(v4.0.0): POST is the kernel's -- the boot feeds the cases, and nothing of the harness is on the node` and push.
|
||||
|
||||
---
|
||||
|
||||
### Task 4: Bare metal, and the write-up
|
||||
|
||||
- [ ] **Step 1:** Three v4 boots with the typed session of step 6 and, added to it, `T{`, `RS1`, `COLD`, `RS1`, `HERE .`. Each log: POST 538 of 538, the `PARITY:V4_SYSTEM` line equal to hosted's, `T{` unknown, `RS1` printing `42 42` before and after `COLD`. If POST fails for want of dictionary room, stop and report (Review Focus 5).
|
||||
- [ ] **Step 2:** `MESH.md` step 6b as done; `NUCLEUS.md` section 8's list; `v4/README.md` "POST"; `POST79.md` as regenerated.
|
||||
- [ ] **Step 3: Commit** with the three logs, `feat(v4.0.0): POST is the kernel's -- bare metal, and written up`, and push.
|
||||
Reference in New Issue
Block a user