From fd820fc9ebc7485f2a57406824e2b55d0b639623 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Mon, 3 Aug 2026 10:57:42 -0400 Subject: [PATCH] =?UTF-8?q?FABRIC.md=20=C2=A73:=20declare=20the=20closed?= =?UTF-8?q?=20two-valued=20cell=20union?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review item REVIEW-A3. §23.1 dissolved the payload threshold by making large patrons heavy -- a 1024-byte block is 17 cells, one header and sixteen of payload. Those sixteen carry no identity, heat, TTL or code field, so they are a second cell shape, which §3's opening line ("One structure. No variants") forbade without saying so. An implementer reading §3 literally would have built the wrong structure. Declared: a cell is either a patron header or a continuation cell owned by exactly one patron. The union is closed, two-valued, and fixed at build time. This introduces no new principle -- it is the same discipline §18.3 applies to behaviours, and a two-valued union is the smallest instance of a closed enumeration. It is not a type field: the distinction is structural, tells the engine only whether a cell begins or continues a patron, and is exhausted by that. Continuation cells are never ranked, reaped or dispatched; they are floor space accounted for in their owner's mass. §13's "one datatype" bullet amended -- the datatype is a two-constructor sum rather than a bare record, costing one case split. §23.4 #3 (identity elision) expanded: it is downstream of the header/continuation encoding, since a scheme reusing the identity field as discriminator would couple the two decisions. Co-Authored-By: Claude Opus 5 --- FABRIC.md | 36 ++++++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/FABRIC.md b/FABRIC.md index e72b59f..5e6beec 100644 --- a/FABRIC.md +++ b/FABRIC.md @@ -100,6 +100,30 @@ One structure. No variants, no type field, no subclassing. Fixed-size cells. Links are indices, so the Stadium stays an array — no fragmentation, and tractable for Isabelle later. +#### A cell is one of exactly two things + +The wire table above describes a **patron header**. §23.1 establishes that a large patron is +not held by reference but simply occupies more cells — a 1024-byte block is 17 cells, one +header and sixteen of payload. Those sixteen carry no identity, no heat, no TTL and no code +field. + +That is a second cell shape, and this section's opening line — *"One structure. No variants"* +— forbade it without saying so. Declared properly: + +> **A cell is either a patron header or a continuation cell owned by exactly one patron. +> The union is closed, two-valued, and fixed at build time.** + +This introduces no new principle. It is the same discipline §18.3 applies to behaviours: a +closed enumeration fixed at build time is as tractable in HOL as a single record, and a +two-valued union is the smallest possible instance of one. §13's "one datatype" remains true +in substance — the datatype is now a two-constructor sum rather than a single record, which +costs a case split and nothing else. + +What it is **not** is a type field. The engine does not ask a header what kind of patron it +is; the two-valued distinction is structural, tells the engine only whether a cell begins a +patron or continues one, and is exhausted by that. A continuation cell is never ranked, +never reaped and never dispatched — it is floor space, accounted for in its owner's mass. + > **Amended by §19.2 and §23.1.** `mass` is an eighth wire, added when density was > defined — density is heat ÷ mass, so mass has to live in the entry. And the original > payload rule ("inline if small, by reference if large") was dissolved rather than @@ -382,8 +406,10 @@ and is where a verification effort usually dies. Unification deletes it outright What the design gives Isabelle/HOL, more or less for free: -- **One datatype.** The arena entry is a single record. Everything else is payload. You +- **One datatype.** The Stadium entry is a single record. Everything else is payload. You reason about `entry` once rather than about blocks, messages, VMs and events separately. + *(Amended by §3: a cell is a two-constructor sum — patron header or continuation cell — + not a bare record. That costs one case split and nothing else; the point stands.)* - **No pointers.** Fixed-size cells with index links means the arena models as a total function over a finite index set — no heap model, no separation logic, no aliasing, no null. This is the single biggest difference between a tractable proof effort and a @@ -1708,11 +1734,17 @@ Firmness of each figure: 2. **Cell size validation.** Build the header for real, count the bytes, and check that a typical message still fits in one cell with the behaviour tag and flags included. 3. **Is `identity` needed at all for every patron kind?** For a word it is a name; for a - block a content hash; for a message possibly nothing — its identity could be its index. + block a handle (§24.4); for a message possibly nothing — its identity could be its index. If identity can be elided for some kinds, 8 bytes of a 32-byte header is a large saving. This must not become a per-kind branch (§18.3), so it is only worth doing if it can be expressed uniformly. + **Larger than it first appeared.** §3 now declares cells a closed two-valued union — + header or continuation. Whatever distinguishes the two occupies header space and + interacts directly with any identity elision: a scheme that reuses the identity field as + the discriminator, for instance, would couple the two decisions. Settle the + header/continuation encoding first; identity elision is downstream of it. + --- ## 24. Mutation, identity, and mass stability