From 90ea3728590734419fdc00821a05e1010b3cebd8 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 15:30:17 +0000 Subject: [PATCH] docs(v4): heat.c's and the stacks' comments say what the code does (#181) - heat.c call_index(): the comment read as an unfinished thought ("hash-mod or just take low bits?", "ignore for now? Or clamp?"). It now states the rule the code follows: indexed by the target, a target past the table not counted, -1 telling the callers so; the table D-6's stand-in, which ENGINE step 4 Part A1 plans to remove. - stack.h points 1 and 2 said there was no overflow detection "and there never will be" and that a depth exceeded corrupted silently -- D-2, which D-16 revised. Now: guarded before every opcode, a mesh node 10 and 9, the host node 32 and 32 (D-17); C code that serves a node checks the depth itself. - stack.c named an 8-ring and depths 10 and 9 only, and said D-2's rule still held. - DATASHEET-F18.md section 13 item 4 (this gap) struck, resolved in place. Comments only: test_stack and test_heat unchanged at both widths (730,137 and 8,272 checks, 0 failures). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017RzZgrf7V7Zk2iczBXDRbm --- docs/v4.0.0/DATASHEET-F18.md | 6 ++++-- v4/include/v4/stack.h | 24 ++++++++++++++---------- v4/src/heat.c | 22 ++++++++-------------- v4/src/stack.c | 18 ++++++++++++------ 4 files changed, 38 insertions(+), 32 deletions(-) diff --git a/docs/v4.0.0/DATASHEET-F18.md b/docs/v4.0.0/DATASHEET-F18.md index 93f84779..f41e3cf2 100644 --- a/docs/v4.0.0/DATASHEET-F18.md +++ b/docs/v4.0.0/DATASHEET-F18.md @@ -339,9 +339,11 @@ These are reported, not hidden: built too (`MACHINE.md` §2.2): entries 0–5, the shared math, and nothing else. In the test host a node Hera births carries it. The products have no births yet, so they do not link it. A node that is born is still sent the host's assembled system through its port. -4. **`stack.h`'s opening comment** still says there is no overflow detection "and there never +4. ~~**`stack.h`'s opening comment** still says there is no overflow detection "and there never will be". D-16 revised that, and the header carries a revision note above it. The code - counts and guards (§4). The comment's first paragraph is out of date. + counts and guards (§4). The comment's first paragraph is out of date.~~ **Resolved + 2026-11-12 (#181):** `stack.h`'s points 1 and 2, and `stack.c`'s note, now say what the code + does -- counted, guarded before every opcode, the host node 32 and 32 (D-17). 5. **Branches in slots 4 and 5** are outside the spec but not trapped (§6). ## 14. What is not in the machine diff --git a/v4/include/v4/stack.h b/v4/include/v4/stack.h index fa7c400c..dea8fa4e 100644 --- a/v4/include/v4/stack.h +++ b/v4/include/v4/stack.h @@ -17,17 +17,21 @@ * * Two consequences that the ISA and the capsule code must both respect: * - * 1. There is no overflow or underflow detection, and there never will be. - * Pushing past the bottom silently overwrites the oldest entry. This is - * hardware behaviour, reproduced faithfully here rather than defended - * against: a golden model that trapped on overflow would diverge from - * the thing it is a model of, which is the whole point of the exercise. + * 1. A running programme cannot overflow or underflow a stack: before every + * opcode the executor checks that the stacks hold what it takes and have + * room for what it leaves, and faults instead (D-16, exec.h). The ring + * below still wraps -- that is what push and pop do when C code calls + * them at either end, and why C code that serves a node checks the depth + * first (manage.c, blocks.c) -- but no opcode reaches the wrap. * - * 2. Nesting is therefore shallow (10 and 9), and exceeding either depth - * corrupts silently rather than faulting. DECOMPOSITION.md section 3 - * calls this out as the constraint that "every CAP definition in section - * 4 and 5 must be re-checked against ... before it is accepted as a POST - * target; the hand traces so far assumed unbounded stacks." + * 2. Nesting is shallow: a mesh node's stacks are the F18's 10 and 9; the + * host node's are 32 and 32 (D-17: V4_DATA_RING and V4_RET_RING, set in + * v4/Makefile). One value or one call past either depth is a stack fault + * with its message, where under D-2 it corrupted silently. + * + * (Points 1 and 2 corrected 2026-11-12, #181: they said there was no overflow + * detection "and there never will be", and that exceeding a depth corrupted + * silently -- D-2's rule, which D-16 revised.) * * The T/S + 8-ring decomposition is the hardware shape, not an optimisation: * T and S are architectural registers (section 1.1 lists them), and the ring diff --git a/v4/src/heat.c b/v4/src/heat.c index a0f7d547..3ac9e937 100644 --- a/v4/src/heat.c +++ b/v4/src/heat.c @@ -24,21 +24,15 @@ void v4_heat_on_retire(v4_heat *h, unsigned op, v4_uheat_t *anticlock) static unsigned call_index(v4_cell target) { - /* Index by target address. The table is a fixed-size cache for the model. - * A real hardware table is deferred; here we hash-mod or just take low bits? - * Or simply if in range use it. The spec says "per-call-target heat table" - * indexed by target. For golden model, targets are small (node memory). */ + /* The per-call-target heat table is the golden model's stand-in until D-6 rules which + * heat structures exist in hardware (DECOMPOSITION.md D-6). It is indexed by the call's + * target address itself, V4_HEAT_MAX_CALL_TARGETS slots. A target at or past that has + * no slot: it is not counted, and (unsigned)-1 tells the callers so -- they then record + * nothing and read 0, rather than counting it in another target's slot. ENGINE.md step 4, + * Part A1, plans to remove the table with v4_heat_on_call (corrected 2026-11-12, #181: + * this comment read as an unfinished question). */ unsigned idx = (unsigned)(v4_ucell)target; - if (idx >= V4_HEAT_MAX_CALL_TARGETS) { - /* Out of range: ignore for now? Or clamp? D-6 deferred; but heat must - * be recorded for actual call targets exercised. Many tests will have - * targets < 4096. This is a conservative model choice: if target is - * outside the modeled table, we do not increment a modeled slot (and - * we could log, but not specified). The boundary philosophy says detect - * rather than corrupt: for the model, we just don't record in the fixed - * table -- acceptable until D-4/D-6 pin sizes. */ - return (unsigned)-1; /* invalid */ - } + if (idx >= V4_HEAT_MAX_CALL_TARGETS) return (unsigned)-1; return idx; } diff --git a/v4/src/stack.c b/v4/src/stack.c index a7b7b4b0..3e752c03 100644 --- a/v4/src/stack.c +++ b/v4/src/stack.c @@ -3,8 +3,11 @@ */ /* stack.c -- F18 circular hardware stacks. * - * The two decompositions (T/S + 8-ring, R + 8-ring) are exactly equivalent to - * flat circular buffers of depth 10 and 9 respectively. The argument, since + * The two decompositions (T/S + ring, R + ring) are exactly equivalent to flat + * circular buffers of depth V4_DATA_RING + 2 and V4_RET_RING + 1 -- 10 and 9 on + * a mesh node, as the F18, with an 8-cell ring; 32 and 32 on the host node + * (D-17). The argument below is written for a mesh node's 8, "mod 8" meaning + * mod the ring size (corrected 2026-11-12, #181: it named 8 only). The argument, since * the ISA is specified in terms of the decomposition and the differential * test in tests/test_stack.c is written against the flat form: * @@ -24,10 +27,13 @@ * Return stack, 9 deep, same argument with one register instead of two: the * stack reads R, ring[(head-1) mod 8], ..., ring[head mod 8]. * - * "No overflow or underflow; pushing past the bottom silently overwrites the - * oldest entry" (D-2) is not an extra rule here -- it is what a fixed-depth - * circular buffer with no bounds check does on its own, once the pointer is - * allowed to wrap. Nothing below tests head against anything. + * Nothing below tests head against anything: a push past the bottom overwrites + * the oldest entry, which is what a fixed-depth circular buffer does once the + * pointer wraps -- D-2's rule. D-16 revised it: each stack also counts what it + * holds (depth, kept here but never tested here), and the executor faults + * before an opcode would push onto a full stack or pop an empty one (exec.c). + * C code that pushes or pops for a node checks the depth itself (manage.c, + * blocks.c). (Corrected 2026-11-12, #181: this said D-2's rule still held.) */ #include "v4/stack.h"