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