Conformance · the laws are the spec

210 laws.
Every one a property test.

The verdict is the contract. box-and-box isn’t defined by an implementation — it’s defined by these laws: associativity, the annihilation of a veto, the precedence of the bridge, the un-weakenability of the entrenched core. Each is checked against 2000 random cases on every run. Two hosts, in any language, must agree on all 143. Pass them, and you’re conformant — the way an implementation is POSIX because it passes the suite, not because it says so. Click any law to see its formal property and what it guarantees.

8
modal subsystems
210
property-tested laws
2000
trials per law
1
verdict, certified
  reproduce it yourself live output 
$ npm i -g box-and-box && node test/laws.mjs && node test/compose-laws.mjs

box-and-box law harness · 2000 trials/law
──────────────────────────────
Feasibility (L1–L14): 14/14 pass
Priority    (H1–H13): 13/13 pass
The bridge  (B1–B3):  3/3 pass
Permissions (D1–D9):  9/9 pass   · composition (DB1–DB3): 3/3
Time        (T1–T8):  8/8 pass   · composition (TB1–TB3): 3/3
Economy     (C1–C11): 11/11 pass · composition (CB1–CB6): 6/6
Knowledge   (E1–E8):  8/8 pass   · composition (EB1–EB3): 3/3
Coordination(S1–S8):  8/8 pass   · composition (SB1–SB3): 3/3
Self-amend  (R1–R8):  8/8 pass   · composition (RB1–RB3): 3/3
Evolution   (EV1–EV6):6/6 pass   · join: reflexive × axiological × resource
Compose/CC2 (CA·CP·CX):15/15 pass · & combine · |> pipeline · ⊗ cross · fail-closed
                      (100 suite + 1 anchor: a brick of bricks is a brick)
──────────────────────────────
✓ all 210 enforced laws hold.
· 3 declared-open gaps (CP5/CP6/CP7, the Value.pi carrier) print FALSIFIED by design.
Numerics
normative · the floor under every law

Two conformant runtimes must agree on every verdict — so they must agree on the arithmetic the verdicts are built from. box-and-box pins a single numeric domain: IEEE-754 binary64 (double); one canonical rounding util round(x, dp = 3) (and roundDelta = round(x, 6) for evolution deltas), defined as Math.round(x · 10^dp) / 10^dp — half-toward +∞ at the .5 boundary; one comparison tolerance EPS = 1e-9 via approxEq. Fields are EXACT (compared with ===: n, κ, phase, ledger balances) or TOLERANCE (compared with approxEq: β, utility, scores). Non-finite inputs pass through round unchanged — fail-closed, never NaN laundering. The full normative statement lives in the kernel README §Numerics and the exported box-and-box/numerics module; the laws below are stated over this domain.

The bridge
composition · 3 laws

feasible ▸ permitted ▸ best — the rule that composes the rest, and the annihilation that makes a veto absolute.

B1▸veto ⇒ score 0̲✓
propertyinfeasible(o) ⇒ gatedScore(o) = 0̲ (−∞)
guaranteesAn option that fails the feasibility floor scores the tropical annihilator — no amount of utility can lift it back into contention.
B2▸select ranks within feasible✓
propertyselect = argmax utility over the feasible set only
guaranteesThe chosen option is always feasible, and no feasible option out-scores it. Ranking happens strictly after the floor — never across it.
B3▸conservativity: one feasible ⇒ chosen✓
property|feasible| = 1 ⇒ that option chosen (even vs. utility 999)
guaranteesA lone feasible action wins regardless of how attractive the infeasible alternatives look. Feasibility is not a tiebreaker — it is a gate.
Feasibility
alethic · 14 laws

what can happen, the monoid of values, and the 0̲ that infeasibility collapses to.

L1▸combine associative✓
propertycombine(combine(a,b),c) = combine(a,combine(b,c))
guaranteesMerging values is grouping-independent — you can fold a stream of evidence in any order and reach the same state.
L2▸combine identity V0✓
propertycombine(a, V0) = a
guaranteesThe empty value is a true unit — merging in “nothing” changes nothing.
L3▸commutative families (n,κ,β,σ,deny)✓
propertycombine(a,b) = combine(b,a) on each field
guaranteesMerge order doesn't matter — the basis for conflict-free (CRDT) convergence across replicas.
L4▸β idempotent under min✓
propertycombine(a,a).β = a.β (β merges by min)
guaranteesConfidence merges conservatively (lowest wins) and re-merging a value with itself is stable.
L5▸σ idempotent under ∪✓
propertycombine(a,a).σ = a.σ (σ merges by ∪)
guaranteesThe capability set merges by union, so duplicates collapse and self-merge is a no-op.
L6▸κ idempotent under ∨✓
propertycombine(a,a).κ = a.κ (κ merges by ∨)
guaranteesThe cyclicity flag merges by OR and never flips spuriously on re-merge.
L7▸promote β-monotone✓
propertypromote(a, ev).β ≥ a.β
guaranteesEvidence can only raise confidence, never silently lower it.
L8▸reconcile antitone + idempotent✓
propertyreconcile(a,T).σ ⊆ a.σ, and reconcile is idempotent
guaranteesReconciliation only narrows the capability set and reaches a stable result in a single pass.
L9▸deliberate κ→false + idempotent✓
propertydeliberate(a).κ = false, and deliberate is idempotent
guaranteesDeliberation clears a detected cycle and is a fixpoint — running it again changes nothing.
L10▸chain refuses a backward phase✓
propertyphaseIdx(a) > phaseIdx(b) ⇒ chain(a,b) errors
guaranteesThe pipeline cannot run a phase backward — composition respects phase order.
L11▸chain associative where defined✓
propertychain assoc. on forward-ordered triples
guaranteesWhere the pipeline is legal, its composition is associative — sub-pipelines compose predictably.
L12▸promote distributes over combine on β✓
propertypromote(combine(a,b)).β = combine(promote a, promote b).β
guaranteesPromoting then merging gives the same confidence as merging then promoting — order of evidence vs. merge is irrelevant.
L13▸consume gate (β_min)✓
propertyconsume(a).ok ⟺ a.β ≥ β_min
guaranteesThe feasibility gate fires exactly at the confidence threshold — no margin, no slack.
L14▸deny_default idempotent under ∧✓
propertycombine(a,a).denyDefault = a.denyDefault (merges by ∧)
guaranteesDeny-by-default merges by AND — once any source denies, it stays denied, and self-merge is stable.
Permissions
deontic · 12 laws

obligation, prohibition, conflict, and contrary-to-duty repair — and how a permit composes into the verdict.

D1▸join commutative + associative✓
propertyjoin(a,b) = join(b,a), join associative
guaranteesPermission statuses combine order-free — the deontic lattice is a join-semilattice.
D2▸join identity OPTIONAL + idempotent✓
propertyjoin(a, OPTIONAL) = a, join(a,a) = a
guaranteesOPTIONAL (no constraint) is the unit, and joining a status with itself is a no-op.
D3▸O ⊔ F = CONFLICT✓
propertyjoin(OBLIGATORY, FORBIDDEN) = CONFLICT
guaranteesAn obligation and a prohibition on the same act surface as an explicit CONFLICT — never silently resolved.
D4▸join monotone (a ⊑ a⊔b)✓
propertyrank(a ⊔ b) ≥ rank(a) and ≥ rank(b)
guaranteesJoining never lowers deontic strength — constraints only accumulate upward.
D5▸CONFLICT absorbs✓
propertyjoin(CONFLICT, a) = CONFLICT
guaranteesConflict propagates through further joins until it is explicitly resolved.
D6▸resolve idempotent + clears conflict (distinct prio)✓
propertyresolve with distinct priorities clears CONFLICT; resolve idempotent
guaranteesPriority-based resolution terminates a conflict in one pass and re-running it is stable.
D7▸factual detachment (in force iff condition)✓
propertydetach(duty).inForce ⟺ condition holds
guaranteesA conditional duty is in force exactly when its triggering condition is true — no earlier, no later.
D8▸CTD partiality (repair iff violated)✓
propertyrepair present ⟺ primary duty violated
guaranteesA contrary-to-duty (reparative) obligation fires only on an actual violation — not pre-emptively.
D9▸comply: O⇒¬F (ought is permitted)✓
propertycomply(O,done)=ok; comply(F,done)≠ok; comply(O,¬done)≠ok
guaranteesWhat is obligatory is permitted; doing the forbidden, or omitting the obligatory, both fail compliance.
composition (DB1–DB3)
DB1▸forbidden excluded from decision✓
propertyforbidden option (utility 99) is never chosen; safe option wins
guaranteesPermissions sit above priority — utility 99 cannot beat a prohibition.
DB2▸obligation forces over higher score✓
propertyobligatory(utility 1) chosen over non-obligatory(utility 99)
guaranteesA duty overrides mere desirability — the kernel does the obligatory thing even when something flashier scores higher.
DB3▸alethic precedence ⇒ CTD escalation✓
propertyobligatory option infeasible ⇒ decision null + CTD escalation
guaranteesWhen you can't do your duty, the kernel escalates (contrary-to-duty) rather than faking compliance — feasibility still comes first.
Priority
axiological · 13 laws

how the feasible, permitted options are ranked — in a semiring, so preferences never resurrect a vetoed one.

H1▸⊕ commutative monoid✓
property⊕ commutative, associative, identity 0̲
guaranteesAlternatives combine order-free with a zero element — the “choose between” operator is well-behaved.
H2▸⊗ monoid✓
property⊗ associative, identity 1̲
guaranteesSequencing scores is associative with a unit — the “and then” operator composes cleanly.
H3▸left distributivity✓
propertya ⊗ (b ⊕ c) = (a ⊗ b) ⊕ (a ⊗ c)
guaranteesSequencing distributes over choice — a sound preference algebra, not ad-hoc arithmetic.
H4▸right distributivity✓
property(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)
guaranteesDistributivity holds on both sides — confirming a genuine semiring structure.
H5▸0̲ annihilates ⊗✓
property0̲ ⊗ a = 0̲
guaranteesTHE annihilation law — a vetoed option (0̲) times any utility stays 0̲. This is what makes a veto absolute in the score algebra.
H6▸⊕ idempotence (dioid only)✓
propertya ⊕ a = a under the tropical dioid
guaranteesBest-of-self is self on the tropical dioid. Deliberately fails under probability/log semirings (see “where the laws bend”) — picking the wrong semiring is a category error the suite catches.
H7▸⊗ monotone in order✓
propertya ≤ b ⇒ a ⊗ c ≤ b ⊗ c
guaranteesScaling by a common factor preserves ranking — sequencing never reorders preferences.
H8▸reinforce η-contraction✓
property|reinforce(u,t,e) − t| = (1−e)·|u − t|
guaranteesA learning update is a contraction toward the target — values converge, they don't oscillate.
H9▸rollout γ-contraction✓
property‖Bu − Bv‖ = γ·‖u − v‖
guaranteesThe Bellman backup is a γ-contraction — value iteration provably converges to a unique fixpoint.
H10▸dominate idempotent + Pareto✓
propertydominate idempotent; no Pareto-dominated survivor
guaranteesThe Pareto frontier is stable and clean — re-filtering changes nothing and no dominated option slips through.
H11▸anneal ε→0 idempotent✓
propertyanneal drives ε → 0, and is a fixpoint there
guaranteesExploration decays to zero — the schedule eventually commits to exploitation.
H12▸softmax shift-invariant✓
propertysoftmax(u, T) = softmax(u + c, T)
guaranteesScores are relative — adding a constant to every utility leaves the distribution unchanged.
H13▸T→0 collapses to argmax✓
propertysoftmax(u, 0⁺) → argmax
guaranteesZero temperature is exactly greedy selection — the continuous knob recovers the hard maximum at its limit.
Time
temporal · 11 laws

safety as an invariant over the whole trajectory; liveness as a horizon obligation.

T1▸G,F idempotent (GGφ≡Gφ)✓
propertyGGφ ≡ Gφ, FFφ ≡ Fφ
guaranteesThe LTL always/eventually operators are idempotent — “always always” is just “always.”
T2▸duality (¬Gφ≡F¬φ, ¬Fφ≡G¬φ)✓
property¬Gφ ≡ F¬φ, ¬Fφ ≡ G¬φ
guaranteesAlways and eventually are De Morgan duals — negation pushes cleanly through the temporal modalities.
T3▸∧,∨ commutative + idempotent✓
property∧, ∨ commutative and idempotent
guaranteesThe propositional layer under the temporal operators is a well-formed lattice.
T4▸progression faithful (monitor ≡ direct)✓
propertymonitor verdict = direct trace semantics
guaranteesThe incremental runtime monitor is sound — stepping a formula forward agrees with evaluating it over the whole trace.
T5▸safety finite-witness / liveness never-early✓
propertysafety emits a 'vio' witness at the breach step; liveness never commits false early
guaranteesSafety violations are caught at the exact step they occur; liveness is never failed prematurely (it may still be satisfiable later).
T6▸G/∧ and F/∨ distribute✓
propertyG(a ∧ b) ≡ Ga ∧ Gb, F(a ∨ b) ≡ Fa ∨ Fb
guaranteesThe standard LTL distribution identities hold — invariants and reachability decompose conjunctively/disjunctively.
T7▸until fixpoint (φUψ≡ψ∨(φ∧X(φUψ)))✓
propertyφUψ ≡ ψ ∨ (φ ∧ X(φUψ))
guaranteesUntil satisfies its defining fixpoint equation — the basis for unrolling it into a step-by-step monitor.
T8▸lasso GF/FG + G/F vs unrolling✓
propertyGF = some loop state; FG = every loop state; G/F = unrolled prefix
guaranteesOn lasso-shaped (ultimately periodic) traces, ω-regular monitoring matches the unrolled semantics — “infinitely often” and “eventually always” are decided on the loop.
composition (TB1–TB3)
TB1▸safety shield prunes a violating step✓
propertyresidual rejects a violating next step, accepts a holding one
guaranteesThe watchdog blocks the unsafe next action before it executes — safety is enforced at the step boundary.
TB2▸unmet liveness ⇒ escalation at horizon✓
propertymissed liveness at horizon ⇒ escalate (repair/replan)
guaranteesA deadline that comes and goes unmet triggers an escalate-and-replan, not a silent pass.
TB3▸safety violation ⇒ unsafe verdict✓
propertysupervise returns safe=false at the exact violatedAt index
guaranteesA trajectory breach is reported as unsafe and pinned to the step where it happened.
Economy
resource · 17 laws

a closed, double-entry budget; affine use; and pricing the kernel’s own deliberation.

C1▸conservation under transfer (Σ invariant)✓
propertytotal balance invariant under any transfer
guaranteesThe ledger is closed double-entry — a transfer moves value, it never creates or destroys it.
C2▸no overdraft; balances stay ≥ 0✓
propertyover-transfer ⇒ INFEASIBLE; all balances ≥ 0
guaranteesYou cannot spend what you don't have — the budget never goes negative.
C3▸independent transactions commute (CRDT)✓
propertydisjoint transfers commute
guaranteesNon-overlapping transactions can be applied in any order — the ledger converges like a CRDT.
C4▸linearity — spending depletes (not idempotent)✓
propertyspend twice removes two units
guaranteesConsumable resources are linear — each spend depletes, so re-running an action costs again (deliberately not idempotent).
C5▸reusability — using `!` does not deplete (idempotent)✓
propertyusing a reusable (`!`) skill twice leaves the balance unchanged
guaranteesThe “of-course” modality is copyable — a reusable capability can be invoked freely without drawing down a budget.
C6▸flow monotonicity — depletion only decreases✓
propertyavailable tokens only decrease over a run
guaranteesNo spontaneous refills — a consumable budget moves one direction until explicitly replenished.
C7▸capacity conservation (stability + plasticity)✓
propertytotal capacity invariant under allocate/forget
guaranteesAllocating and releasing capacity conserves the total — no capacity leaks between stability and plasticity.
C8▸no free reclaim — forgetting releases the knowledge✓
propertyforget releases capacity AND the associated knowledge
guaranteesReclaiming capacity isn't free — you give up the knowledge that occupied it. No having-it-both-ways.
C9▸irreversible sink is absorbing — sink monotone, allocation of unspent budget still feasible✓
propertykind[res]='irreversible' ⟹ sink(res) non-decreasing ∧ transfer(SINK → ·) = INFEASIBLE
guaranteesSome resources cannot be refunded. Tokens can; information leaked about a holdout cannot. This rung metered both on the same ledger until a spend was found to be reversible with Σ still conserved and no balance negative — so no existing law objected. The narrowing matters: moving previously-unspent budget out of the treasury is still permitted, because allocating the rest of a declared cap is budgeting, not un-leaking.
C10▸a declared cap bounds cumulative consumption of an irreversible resource✓
propertysink(res) ≤ cap[res], always
guaranteesThe bound is on what has been spent in total, not on what any account happens to hold. An account rich enough to afford the next query is still refused once the cumulative total would cross the cap — which is the only reading under which a privacy or holdout budget means anything.
C11▸the authority fields (kind, cap) are frozen — a declared cap cannot be rewritten✓
propertykind and cap are frozen at construction and on every clone; writing one throws
guaranteesC10 said “a declared, immutable cap” and the immutability was a comment: L.cap.hb = 100 walked past C10 and L.kind.hb = 'depletable' walked past C9. The two fields that decide what the rules are are now sealed, and the seal survives cloning. Balances are deliberately not sealed and that boundary is declared rather than enforced — a Ledger is a value, not a capability handle, and making balances unforgeable needs an opaque write-mediated object.
composition (CB1–CB6)
CB1▸exhaustion ⇒ infeasible (the alethic 0̲ gate)✓
propertyfeasible ⟺ balance ≥ cost
guaranteesRunning out of resource makes an action infeasible — the economy feeds directly into the alethic floor.
CB2▸cost composes additively along a pipeline (semiring)✓
propertythree staged spends = one lump spend of the sum
guaranteesA pipeline's cost is the sum of its stages' costs — budgeting composes predictably along |>.
CB3▸Type-II repair pricing (value ≥ cost ∧ affordable)✓
propertyrepair invoked ⟺ value ≥ cost ∧ affordable; charges cost
guaranteesThe kernel only pays to repair when the repair is worth its price and the budget can cover it — and it actually deducts the cost.
CB4▸irreversible exhaustion is not recoverable from the sink✓
propertyexhausted ∧ irreversible ⟹ no transfer out of SINK re-opens the CB1 gate
guaranteesCB1 closes the gate at exhaustion; this says the gate stays closed against the one move that used to re-open it. It does not say the gate can never re-open — allocating unspent treasury budget still does, and should. The distinction is between spending the rest of your budget and recovering what you already spent.
CB5▸the alethic gate agrees with the primitive✓
propertyfeasible(L, acct, cost) ⟺ charge(L, acct, cost) ≠ INFEASIBLE
guaranteesC10 was added to the spend primitive and not to the gate, so with a cap of 6, a sink at 5 and an account holding 10, feasible said GO on a spend transfer was already committed to refusing. C1, C2, C9 and C10 all still held — no law compared them. A decision layer answering yes over a primitive answering no is worse than either answer alone, because the caller has committed by the time it finds out. Both now consult one admissibility predicate, and this law is what keeps them pointed at it.
CB6▸a preflighted path never returns INFEASIBLE dressed as a ledger✓
propertyuse(·).L ≠ INFEASIBLE ∧ repair(·).L ≠ INFEASIBLE
guaranteesBoth use and repair ran their own affordability check and then called spend, so an irreversible resource at its cap produced {ok: true, L: INFEASIBLE} — a Symbol handed to a caller expecting a ledger. The general form is the lesson: a new invariant is not finished when the primitive that states it enforces it. Every other path deciding the same question has to be found and pointed at the same predicate.
Knowledge
epistemic · 11 laws

knowledge (S5) vs. belief (KD45); a known-unknown that must route to deliberation.

E1▸factivity T (Kφ → φ)✓
propertyKφ → φ
guaranteesKnowledge is factive (axiom T of S5) — if the kernel knows something, it is true. This is the line between knowing and merely believing.
E2▸distribution K (K(φ→ψ)∧Kφ → Kψ)✓
propertyK(φ→ψ) ∧ Kφ → Kψ
guaranteesKnowledge is closed under known implication — you know the consequences of what you know.
E3▸positive introspection (Kφ → KKφ)✓
propertyKφ → KKφ
guaranteesIf you know something, you know that you know it (axiom 4).
E4▸negative introspection (¬Kφ → K¬Kφ)✓
property¬Kφ → K¬Kφ
guaranteesIf you don't know something, you know that you don't (axiom 5) — the formal basis for routing a known-unknown to deliberation.
E5▸belief consistency D (¬(Bφ ∧ B¬φ))✓
property¬(Bφ ∧ B¬φ)
guaranteesBelief is consistent — the kernel never simultaneously believes a thing and its negation.
E6▸knowledge ⇒ belief (Kφ → Bφ)✓
propertyKφ → Bφ
guaranteesAnything known is also believed — knowledge is the stronger, factive layer above belief.
E7▸learning monotonicity (announce preserves K)✓
propertypublic announcement of a truth preserves prior K
guaranteesLearning a true fact never destroys existing knowledge — the epistemic state only grows.
E8▸common knowledge (Cφ → Eφ)✓
propertyCφ → Eφ
guaranteesCommon knowledge implies everyone-knows — the foundation for coordinated joint action.
composition (EB1–EB3)
EB1▸threshold gate monotone; K = belief@1✓
propertybelief gate monotone in threshold; knowledge = belief at threshold 1
guaranteesRaising the confidence bar can only restrict what counts as believed, and certain knowledge sits at the top of that scale.
EB2▸known-unknown ⇒ deliberate (κ)✓
propertyknowsItDoesntKnow ⇒ route = deliberate
guaranteesA recognized knowledge gap routes the decision into deliberation rather than acting on a guess.
EB3▸pooled knowledge dominates individual✓
propertyindividual knowledge ⊆ distributed knowledge
guaranteesPooling agents' knowledge never loses information — the group knows at least what any member does.
Coordination
strategic · 11 laws

which coalitions can actually ensure an outcome — ought-implies-can, made checkable.

S1▸unit: [C]⊤ and ¬[C]⊥✓
property[C]⊤ holds; [C]⊥ never holds
guaranteesAny coalition can ensure the trivially-true outcome, and none can force the impossible — the floor and ceiling of strategic ability.
S2▸coalition monotonicity (C ⊆ C′ ⇒ [C]φ → [C′]φ)✓
propertyC ⊆ C′ ⇒ [C]φ → [C′]φ
guaranteesA larger coalition can ensure anything a sub-coalition can — adding members never removes power.
S3▸outcome monotonicity (φ⊨ψ ⇒ [C]φ → [C]ψ)✓
propertyφ ⊨ ψ ⇒ [C]φ → [C]ψ
guaranteesIf a coalition can ensure a strong outcome, it can ensure any weaker one it entails.
S4▸superadditivity (disjoint C₁,C₂ cooperate)✓
property[C₁]φ₁ ∧ [C₂]φ₂ ⇒ [C₁∪C₂](φ₁ ∧ φ₂) for disjoint C₁,C₂
guaranteesDisjoint coalitions can pool their guarantees — cooperation achieves the conjunction of what each could ensure alone.
S5▸regularity (¬([C]φ ∧ [N∖C]¬φ))✓
property¬([C]φ ∧ [N∖C]¬φ)
guaranteesA coalition and its complement can't both force contradictory outcomes — the strategic game is consistent.
S6▸maintenance is a greatest fixpoint (□)✓
propertycanMaintain = greatest fixpoint (□)
guaranteesThe set of states from which a coalition can keep an invariant forever is exactly the greatest fixpoint — sound “can hold the line” reasoning.
S7▸reachability is a least fixpoint (◊)✓
propertycanReach = least fixpoint (◊)
guaranteesThe states from which a coalition can eventually force a goal are exactly the least fixpoint — sound “can get there” reasoning.
S8▸grand-coalition determinacy ([Σ]φ ↔ ∃ successor φ)✓
property[Σ]φ ⟺ ∃ successor satisfying φ
guaranteesThe grand coalition (everyone) can ensure exactly the outcomes some successor state realizes — full control collapses to plain reachability.
composition (SB1–SB3)
SB1▸single-agent collapse → temporal reachability✓
property1-agent canReach = BFS reachability
guaranteesWith a single agent, coalitional reachability reduces to ordinary graph reachability — the strategic layer generalizes the temporal one.
SB2▸ought-implies-can (¬ability ⇒ escalate)✓
propertyoblige ⇒ discharge if canEnsure, else escalate
guaranteesOught-implies-can is enforced — an obligation the coalition cannot ensure escalates instead of being falsely discharged.
SB3▸coordination needs ability ∧ common knowledge✓
propertyexecutable ⟺ canEnsure ∧ commonKnowledge
guaranteesA joint action is executable only when the coalition both has the power and shares the knowledge to coordinate it.
Self-amendment
reflexive · 11 laws

rules that change rules, with an entrenched core that no amendment can weaken.

R1▸success (enact adds, repeal removes)✓
propertyenact adds a rule; repeal removes it
guaranteesAmendments actually take effect — enacting installs the rule, repealing retracts it.
R2▸consistency (no surviving dominated conflict)✓
propertyarbitration leaves no dominated O/F conflict standing
guaranteesAfter arbitration the rule-set is conflict-free — a dominated obligation/prohibition pair can't survive.
R3▸minimal change (enact∘repeal = id)✓
propertyenact then repeal returns the exact original rule-set
guaranteesAmendment is surgical — adding then removing a rule leaves no residue.
R4▸entrenchment (no weakening the core)✓
propertyentrenched 'safe' rule cannot be repealed or weakened, only strengthened
guaranteesTHE entrenchment law — the ring-0 floor is un-writable from within. Self-amendment can tighten the core but never loosen it.
R5▸lex superior (priority wins)✓
propertyhigher-priority rule overrides lower
guaranteesLex superior — when rules clash, the one with higher authority prevails.
R6▸lex posterior (recency breaks ties)✓
propertyequal priority ⇒ more recent rule wins
guaranteesLex posterior — among equally authoritative rules, the latest enactment governs.
R7▸arbitration idempotent✓
propertyarbitration is idempotent
guaranteesResolving the rule-set once is enough — re-arbitrating produces the same result.
R8▸reflective stability (fixpoint)✓
propertystabilize reaches a fixpoint
guaranteesIterated self-amendment converges — the system that reasons about its own rules settles, it doesn't spin.
composition (RB1–RB3)
RB1▸cannot self-permit the forbidden✓
propertyan obligation out-prioritizing an entrenched prohibition is rejected
guaranteesYou can't legislate around the floor — no amendment can grant permission to do the entrenched-forbidden.
RB2▸revision propagates to govern✓
propertyenacting a prohibition flips the live verdict (A chosen → A vetoed)
guaranteesAmendments take effect on the very next decision — the governance verdict reflects the revised rule-set immediately.
RB3▸entrenched safety survives in supervise✓
propertyentrenched temporal floor can't be repealed and still enforces
guaranteesAn entrenched safety invariant resists repeal and keeps catching trajectory violations downstream in supervision.

Where the laws bend — by design

A governance algebra has to know the difference between regimes. So the harness also checks, on every run, that certain properties fail exactly where they should. These aren’t bugs — they’re the distinctions that make the kernel honest.

H6 · idempotence
holds under the tropical dioid; fails under probability and log semirings — expected, because those aren’t idempotent. Choosing the wrong semiring is a category error the laws catch.
factivity · T
knowledge (S5) is factive in 100% of cases; belief (KD45) believes a falsehood in ~30% — the whole point of separating “knows” from “believes.”
coalition power
the grand coalition can reach what a soloist can in 100% of games, and strictly more in 25% — ought-implies-can has teeth.
affine use
spend a depletable resource three times and tokens go 3 → 0; a reusable skill stays 1 → 1 — the “of course” modality, copyable where consumables are not.
Evolution
join · 6 laws

the measured, priced, certified self-revision bridge — a join across reflexive × axiological × resource: may this policy change, did it measurably improve, is it worth paying for.

EV1▸digest is key-order independent✓
propertydigest(canon(x)) is invariant under JSON key reordering
guaranteesThe content hash is canonical — reordering keys yields the same digest, so provenance is order-stable.
EV2▸chain verifies & detects tamper✓
propertyverify(chain) holds; mutating any record breaks verify
guaranteesThe hash-chain is tamper-evident — altering any past record invalidates the whole chain.
EV3▸refuse to weaken the entrenched floor✓
propertya change weakening an entrenched floor is rejected, even at large positive Δ
guaranteesNo improvement, however large, can buy a weakening of the safety floor.
EV4▸a regressing change is never accepted✓
propertyregresses(before, after) ⇒ decision ≠ accept
guaranteesA self-revision that measurably worsens the score vector cannot be accepted.
EV5▸priced accept ⇒ affordable ∧ worthwhile ∧ charged✓
propertyaccept ⇒ affordable ∧ worthwhile ∧ ledger charged
guaranteesAn accepted change was within budget, beat its predicted threshold, and paid the ledger.
EV6▸certificate soundness✓
propertypredicted / observed / verified / priced agree with the recorded decision
guaranteesThe evolution certificate is sound — every field matches the decision actually taken.
Composition (CC2)
compose · 13 laws

the lego layer — two brick operators, & (parallel coalition) and |> (sequential pipeline), over one shared floor 0̲. A brick of bricks is a brick.

CA1▸& associative✓
property(a & b) & c = a & (b & c)
guaranteesParallel composition regroups freely — carrier, quantities, and cost class all agree.
CA2▸& commutative✓
propertya & b = b & a (capability lattice)
guaranteesRunning capabilities together is order-independent on the commutative sub-carrier.
CA3▸& idempotent✓
propertya & a = a (value carrier)
guaranteesA coalition admits each member once — composing a capability with itself adds nothing.
CA4▸&none identity✓
propertya & none = none & a = a
guaranteesThe empty coalition is the identity for &.
CP1▸|> associative where feasible✓
property(a |> b) |> c = a |> (b |> c)
guaranteesSub-pipelines compose predictably — regrouping a feasible chain never changes the result.
CP2▸id identity✓
propertya |> id = id |> a = a
guaranteesThe pass-through brick is the identity for |>.
CP3▸|> non-commutative (backward ⇒ 0̲)✓
propertyforward a |> b survives; backward b |> a ⇒ 0̲
guaranteesOrder matters — a backward PULSE-phase hand-off is annihilated, so a pipeline can't run time backwards.
CP4▸infeasible hand-off ⇒ 0̲✓
propertyfeeds_into(a) ∩ accepts_from(b) = ∅ ⇒ a |> b = 0̲
guaranteesA type-mismatched hand-off floors the pipeline — outputs that don't fit the next input can't connect.
CX1▸0̲ absorbs both operators✓
propertya & 0̲ = 0̲ & a = a |> 0̲ = 0̲ |> a = 0̲
guaranteesThe floor is absorbing for both operators on either side — one floored part floors the whole.
CX2▸quantity semiring✓
propertyconfidence = ∏ · cost = Σ · latency = max
guaranteesComposite quantities follow the CC2 semiring — confidence multiplies, cost adds, latency takes the worst leg.
CX3▸conservative cost (uncertified ⇒ 0̲)✓
propertyan uncertified child ⇒ composite = 0̲
guaranteesAny child lacking a cost certificate poisons the whole assembly to the floor — you can't compose what you can't price.
CX4▸cost-class lattice (worst wins)✓
propertycertified composite costClass = join (worst) of children
guaranteesA certified composite is graded by its worst-case child — cost classes meet at the top of the lattice.
CX5▸closure (a brick of bricks is a brick)✓
propertycompose(brick, brick) is itself a brick
guaranteesComposition is closed — a composite re-composes like any leaf, so assemblies nest without limit.
CX6▸fail-closed (a malformed child ⇒ 0̲ or a valid brick, never an exception)✓
propertycompose(partial|garbage, b) never throws; result isZero or isBrick
guaranteesFail-closed is doctrine — a partial, malformed, or non-brick operand is normalized to the annihilating zero 0̲ or a valid brick, so the compose layer never propagates an exception or a default-allow.
CX7▸a malformed semantic value cannot normalize to LIVE — unknown floors to 0̲, not to V0✓
propertyunreadable(v) ⇒ isZero(Brick(value=v))
guaranteesThe contract half of this family has a semantic twin, and CX6 could not see it. A malformed value — a string, a number, an array, an error sentinel — floored to V0(), the benign identity value: feasible, acyclic, no conflict. So "I cannot interpret this value" became "the harmless value" and stayed LIVE. CX6 asks for "0̲ or a valid Brick, never an exception", and V0() is a valid Brick — so a fuzzer aimed at crashes was fully satisfied by the laundering. Directive 1 says FAIL-CLOSED and the code had read it as DO-NOT-THROW; not throwing is necessary and is not sufficient. A partial object is still fine — its fields are readable and the rest take documented defaults. The line is between "incomplete" and "not a Value at all".
AC-COMM▸&'s OWN floor is commutative (the anchor: a brick of bricks is a brick)✓
propertyisZero(a&b) === isZero(b&a)
guaranteesThis is the law CP7 is measured against, and it passes. The combine operator's own floor really is order-independent — which is what makes CP7's failure a defect in the downstream pipeline floor rather than in & itself. Listed here because the page counted the anchor in its total without ever showing it.

Contract declaration — missing ≠ universal

Added 2026-08-22. Until that day Brick() defaulted an absent contract field to '*' and typeMatch() waved through null on either side, so an assembly that declared no interface at all received the most permissive one in the algebra and every hand-off passed a check with nothing left to check — fail-open, in a runtime whose whole claim is that it refuses. Found by outside review.

These five were written against the unfixed code first, and four came back red. The fifth, CD2, was green from the start on purpose: an explicit '*' must keep composing, or "missing ≠ universal" collapses into "refuse everything" and the distinction carries nothing. The identity laws survive for the same reason — none() and idBrick() declare the wildcard rather than being handed it by an absence.

CD1▸an UNDECLARED feeds_into is not a wildcard✓
propertyisZero(undeclared |> narrow)
guaranteesAn interface nobody declared is unknown, and unknown refuses. The refusal names itself contract-undeclared, kept distinct from contract-mismatch: a mismatch is a fact about the parts, an absence is the lack of one, and an operator needs to be told which it hit.
CD2▸an EXPLICIT '*' IS a wildcard and still composes✓
property!isZero(star |> narrow)
guaranteesThe half of the distinction that has to keep working. An explicit '*' is a claim — made by a holder who can be held to it. This law is why the fix is "missing ≠ universal" rather than "refuse more".
CD3▸& does not launder undeclaredness into a declared interface✓
propertyundeclared(a.feeds_into) ⇒ undeclared((a&b).feeds_into)
guaranteesUndeclaredness is absorbing under the contract union. Without this the fix has a hole one operator wide: a coalition containing an undeclared part would inherit its partner's declared set and make the hand-off the undeclared part could not.
CD4▸identity is preserved DELIBERATELY, and its domain is stated✓
propertydeclared(a) ⇒ id|>a ≡ a ≡ a|>id  ∧  undeclared(a) ⇒ isZero(id|>a)
guaranteesBoth halves in one law. The fix narrows CP2's domain, and a narrowing left implicit is a law nobody can check — so the narrowing is itself stated. idBrick() declaring '*' is load-bearing, not incidental.
CD6▸& does not launder a DECLARED-but-incompatible member✓
propertyisZero(a|>c) ⇒ isZero((a&b)|>c)
guaranteesClosed by a RULING, not a patch. & used to union both contract ends while |> asked only for a non-empty intersection, so a coalition handed off on behalf of a member that could not have handed off itself — and identically on the input side. Three semantics were sound; Option U was ruled on outside review: outputs join, inputs meet, and a hand-off is a SUBSET test (OUT(a) ⊆ IN(b)), not an intersection. Meet-everywhere was rejected for hiding real outputs; routed hand-off was rejected as a default until a route witness exists to earn the permissiveness. This law was xfail for the few hours between opening it and the ruling landing.
CD7▸ANY is directional; an UNBOUND var is unknown and refuses; the identity is distinguished, not var-typed✓
propertyisZero(ANY |> narrow) ∧ isZero(VAR α |> narrow) ∧ id.identity = '|>'
guaranteesOne wildcard cannot mean two things. '*' was doing duty as both "any possible output" and "whatever came in, unchanged", and under intersection matching nothing ever forced the difference. The subset rule asks immediately: an ANY output is not safe into a narrow consumer, while a VAR α passthrough is. The identity is neither: it is a distinguished element of |>, branded rather than typed, and short-circuited before the contract check runs. This law previously required the opposite — it asserted !isZero(VAR α |> narrow), that a free variable on an ordinary brick must compose with a narrow consumer — and went green for as long as it existed. That is not polymorphism; it is universal compatibility wearing a Greek letter, and CD8 caught it laundering forbidden hand-offs in 11 of 64 endpoint pairs. A law can encode a defect as a requirement. Contract ends are now tagged undeclared | any | types | var, all four serialisable, so a contract can appear in a receipt, a hash or a replayed world instead of vanishing at the JSON boundary as raw undefined did.
CD8▸inserting the identity cannot change feasibility✓
propertyzero(a|>b) = zero((a|>id)|>b) = zero(a|>(id|>b))
guaranteesAn identity that changes what a pipeline may do is not an identity. Found on outside review 2026-08-22. CD4 proved id preserved the value and never asked whether it preserved feasibility — and it did not: x emitting U into d accepting T is correctly refused, while x |> id |> d composed. Measured at 11 of 64 endpoint pairs where a direct 0̲ became LIVE. The cause was α implemented as an endpoint matcher rather than a binding. The fix is not a stricter matcher — a var OUTPUT is genuinely unknown until bound, so making it directional would break the identity law instead of the soundness. Instead id became a distinguished element: a |> ID = a by construction, returning the operand itself, so it never reaches the check.
CD9▸& projects the same contract either way round✓
propertycontract(a & b) = contract(b & a)
guarantees& is this algebra's parallel operator and is proved commutative — but its projected interface was not. meetIn returned "the other operand" when it met a variable, so two differently named free variables gave (a&b) accepting β and (b&a) accepting α. No verdict differed at the time, because a var matched everything anyway — a latent bug held harmless by a second bug, which is exactly why nothing caught it. Both operators now treat an unbound var as absorbing, so the projection is order-independent by construction rather than by luck.
CD10▸a malformed contract end normalizes to UNDECLARED, never to a declared one✓
propertymalformed(t) ⇒ kind(norm(t)) = 'undeclared'
guaranteesnorm() used to filter: it took input it could not read, dropped the parts it did not understand, and returned the residue as a well-formed declaration. For an output endpoint that residue was usually the empty set — and under a subset rule ∅ ⊆ X holds for every X, so the least readable input in the algebra produced the most permissive endpoint in it. {kind:'types', values:[1,2,3]}, a bare 42, [null] and {} all composed into a narrow consumer. Only an explicitly supplied empty set still means "emits nothing", because that is a claim somebody made.
CD11▸normalization cannot widen admissibility✓
propertymalformed(t) ⇒ ∀c. isZero(brick(feeds_into=t) |> c)
guaranteesThe behavioural half of CD10, stated separately because CD10 could be satisfied by a normaliser that returned some other declared-but-narrow endpoint. What has to hold is the admissibility bound: whatever a malformed end becomes, it may not compose with a consumer a correct reading would have refused. This is the general principle behind all four of these laws — unknown or malformed evidence may never be canonicalised into a stronger claim than the input justified — and it is the same meta-error as the original missing → * that CD1–CD3 closed. The carrier changed; the mistake moved.
CD12▸identity privilege is UNFORGEABLE: no ordinary brick acquires it by declaring a field✓
propertyordinary(x) ⇒ (a |> x) ≠ a ∧ (x |> b) ≠ b
guaranteesA defect introduced BY the previous fix, not one that survived it. Making the identity a distinguished element was right; implementing the distinction as an ordinary identity:'|>' field on Brick() was not, because a field is data and data is written by whoever holds the pen. An uncertified brick with a contract matching nothing declared the privilege and both operators short-circuited past every floor they have — and it survived a JSON round-trip, the boundary this carrier exists to cross. The old code compared the NAME 'id' and a comment correctly called that forgeable, then replaced a forgeable name with a forgeable FIELD: the same thing wearing a schema. Serialisability and authenticity are different requirements. The identities are now singleton TERMS recognised by reference, serialised as a bare tag ({"kind":"pipe_identity"}) carrying nothing else, and decodeTerm() is the only door from data back to the privilege — a tag with a payload decodes to an ordinary brick.
VX1▸a present-but-invalid scalar floors the brick to 0̲; an ABSENT one still defaults✓
propertyinvalid(v[k]) ⇒ isZero(Brick(value=v))  ·  absent(k) ⇒ default
guaranteesThe answer to a question the previous round asked out loud: is partial-with-defaults itself a laundering route? Absence is fine; present-but-invalid was not. normValue() drew its line at "is this an object at all", so a brick could carry {beta:'high'} — present, explicitly asserted, not a number — stay LIVE, and hand beta = NaN downstream where the floor never fired because no beta_min had been required. A default is justified by ABSENCE and by nothing else. Spreading ...v over defaults did the opposite: the default was there to fill a hole and instead sat quietly beside a wrong answer.
VX2▸pi is a declared PHASE or null — never an uninterpretable string✓
propertyv.pi ∈ PHASES ∪ {null}
guarantees{pi:'not-a-phase'} stayed LIVE and could leave a composite carrying a phase phaseIdx has no index for — which is the input the |> phase floor reads. A carrier the floor cannot interpret is a floor that cannot fire.
VX3▸beta is finite and in [0,1]✓
property0 ≤ v.beta ≤ 1 ∧ finite(v.beta)
guaranteesPersistence is a [0,1] quantity under min. NaN, ±Infinity, -0.1, 1.1 and the string '0.5' all passed. Math.min(NaN, x) is NaN, so one bad operand poisons every composite it touches without any of them being refused.
VX4▸kappa and denyDefault are real booleans, not truthy stand-ins✓
propertytypeof v.kappa = 'boolean' ∧ typeof v.denyDefault = 'boolean'
guaranteeskappa:'false' is a non-empty string and therefore truthy — it asserts the opposite of what it appears to say, and κ is the cyclicity flag that routes to deliberation. denyDefault is the deny-by-default switch. Neither may be satisfied by coercion.
VX5▸normalization never manufactures NaN or Infinity in a LIVE brick✓
propertylive(b) ⇒ finite(b.value.n) ∧ finite(b.value.beta)
guaranteesThe OUTCOME form of VX1/VX3, stated separately because the original defect was not the bad input — it was NaN reaching a floor with no predicate that could test it. Whatever survives normalisation has to be arithmetically usable, and it has to stay so under composition.
CD13▸the identity does not bypass canonicalization✓
propertyisZero(Brick(x)) ⇒ isZero(x |> ID) ∧ isZero(ID |> x) ∧ isZero(x & &none)
guaranteesThird round on one boundary, and the previous fix created it. CD12 stopped ordinary data from BEING the identity and left open what the real identity does to an operand that was never canonicalised. ensure() accepted anything brick-shaped — a shape test, not a validity test — so a raw object with value.beta = 'high' passed through and the identity handed it straight back: Brick(raw) was 0̲ and raw |> ID was LIVE. Mutating a legitimate brick after construction did the same. The root cause was an identity law stated too strongly. a |> ID === a — return the very same object — is a JavaScript reference property, not the algebra's; the law is canon(a |> ID) ≡ canon(a), and insisting on the reference form is what created a privileged path around the normaliser. Operands are now canonicalised at ingress, and the zero test runs after that rather than before — a mutated brick's stale annihilated flag used to pass the check that ran first.
CD14▸identity terms are transitively immutable✓
property∀ o reachable from ID or &none · Object.isFrozen(o)
guaranteesFourth round on the identity boundary, and this one attacked the exemption the third round created. ensure() returns the units by reference and justified it — 'they are provably unchanged' — but nobody had done the proof. Object.freeze is shallow: it blocked replacing id.cost and permitted writing through it, permanently and process-wide. A caller could push onto &none.value.authority and collect the result under the other operator. The deep freeze also caught a bug in itself — the first draft used isFrozen as its visited marker, so it stopped at TYPES(), which is frozen with a live values array.
CD15▸a unit has algebraic meaning only under its own operator✓
propertycomposeAnd(ID, x) = composePipe(&none, x) = 0̲
guaranteesThe units were half distinguished-term and half privileged brick: recognised under their own operator, silently demoted to an ordinary brick under the other — carrying their Value, their holder and above all their free certificate into a composite. Deep-freezing alone removes today's payload and leaves the route open; the route is the defect. This is standard rather than a local invention: a duoidal category carries two monoidal structures with distinct units, related only by an explicitly declared structure map. Absent that map there is nothing to assume — missing ≠ universal, at the term level. The type carrier could never have enforced it: the &none output type is the empty set, and the empty set is a subset of everything, so the hand-off check passes vacuously.
CD16▸no unit contributes value, authority or cost under the other operator✓
propertycost(x ⊕ foreign-unit).certified ≠ true ∧ authority(x ⊕ foreign-unit) = ∅
guaranteesThe behavioural half, stated separately because CD15 could be satisfied by a runtime that returns 0̲ while still leaking the unit's privilege into the zero it returns. The units are the only terms in the algebra holding a costless certified certificate they never earned by analysis. That privilege may not reach a composite by the wrong door.
CD17▸a counterfeit unit refuses and names the transport fault✓
propertykind(x) ∈ {pipe_identity, and_identity} ∧ x ≠ singleton ⇒ 0̲
guaranteesdecodeTerm(encodeTerm(t)) === t holds, but nothing stopped a caller writing postMessage(idBrick()) instead of postMessage(encodeTerm(idBrick())). The copy that lands on the far side carries the canonical tag and not the reference. It must not compose as an ordinary brick — it arrives holding a free certificate — and it must not fail silently either: the defect is at the call site and the refusal says so. Measured across a real worker_threads realm boundary, not a same-realm clone.
QX1▸a malformed or absent q cannot become Q0 on an ordinary brick✓
propertymalformed(q) ∨ absent(q) ⇒ isZero(Brick(…))
guaranteesThe same meta-error for the third time, on a third carrier. missing contract → ANY (CD1–CD5); malformed Value → V0() (CX7, VX1–VX5); malformed q → Q0(), here. q:'nope', q:42, q:[] and a wholly absent q all became {confidence:1, cost:0, latency:0} — so unreadable measurement evidence read as perfect confidence, zero cost, zero latency, the most favourable point in the lattice, handed out for saying nothing.
QX2▸confidence is finite and in [0,1]✓
property0 ≤ q.confidence ≤ 1 ∧ finite
guaranteesconfidence:'high' composed to NaN; confidence:2 stayed LIVE. Confidence is the ⊗ component of the CC2 semiring — it multiplies down a pipeline, so one out-of-domain operand contaminates every composite downstream of it.
QX3▸cost is finite and ≥ 0✓
propertyq.cost ≥ 0 ∧ finite
guaranteesThe sharpest single symptom in this family: cost:'free' composed to the string 'free0', because + on a string concatenates. The runtime and the public page both describe cost as adding; nothing checked that the operands were numbers.
QX4▸latency is finite and ≥ 0✓
propertyq.latency ≥ 0 ∧ finite
guaranteeslatency:'fast' composed to NaN under max, and latency:-5 passed unchallenged. Found again independently by the mutation dimension of the metamorphic gate, which is how the ordering defect behind CD13 surfaced.
QX5▸only an identity TERM may carry Q0 without measurement evidence✓
propertyq ≡ Q0 ⇒ term ∈ {id, &none}
guaranteesA neutral element of the algebra is not the default interpretation of missing evidence. Q0 is the true identity of the CC2 semiring — 1 for a product, 0 for a sum, 0 for a max — and it is the correct measured quantity for id and &none, which cost nothing. It is wrong for an ordinary brick that merely arrived without measurements, because there every component is a maximal CLAIM rather than a neutral value. The identities keep it by supplying it explicitly and passing the same validation as everyone else — they are not exempt, they qualify.
QX6▸utility is a finite number✓
propertyfinite(utility) ∨ absent(utility)
guaranteestypeof NaN === 'number', so a NaN utility passed every check and silently poisoned any ranking it entered. An absent utility still defaults to 0 — the additive identity and the least favourable value, so defaulting it claims nothing — while an explicit null is an assertion, and utility is a number.
AD1▸the carrier is closed✓
propertyadmitted(a) ∧ admitted(b) ⇒ isZero(a ⊕ b) ∨ admitted(a ⊕ b)
guaranteesLIVE was doing duty for two different things — structurally valid (the constructor could read every field) and admitted (the shared floor lets it through). An uncertified brick is structurally perfect and unadmitted. Stated as closure it stops being a matter of taste: the anchor law is a brick of bricks is a brick, and u |> ID took a non-carrier element and returned a non-carrier element out of a composition. The algebra was not closed.
AD2▸the identity preserves an admitted element✓
propertyadmitted(a) ⇒ value(a ⊕ e) = value(a) ∧ contract(a ⊕ e) = contract(a) ∧ cost(a ⊕ e) = cost(a)
guaranteesThe identity law, restricted to the carrier. Identity laws quantify over the carrier — a ⊗ e = a says nothing about objects that are not elements — so restricting them costs no law and buys closure back. CD4b's genuine improvement survives intact: undeclared is not a floor condition, so an undeclared brick still passes through the identity unchanged and still refuses at its next real hand-off.
AD3▸the identity does not admit an unadmitted element✓
property¬admitted(x) ⇒ isZero(x ⊕ e), agreeing with isZero(x ⊕ anything)
guaranteesThe identity was the one operation in the algebra that applied no floor. u |> f was 0̲ and u |> ID returned u, LIVE, because the identity short-circuits before the floor — so the single route applying no floor was the element whose entire job is to change nothing. The property is agreement, not uncertified floors: whatever real composition decides about an operand, every identity route must decide the same.
AD4▸a declared floor requirement is enforced, not merely carried✓
propertyrequirement ∈ floor(a) ∪ floor(b) ⇒ enforced on a ⊕ b, and inherited by the composite
guaranteesfloor had been on every brick since the first draft: stored, unioned into every composite, threaded through the whole algebra — and never once read. floored() took a requirements argument that neither operator passed. A requirement propagated but not applied is worse than an absent one: in a receipt it reads exactly like a satisfied one.
AD5▸an unrecognised floor token refuses✓
propertytoken ∉ recognised ⇒ 0̲
guaranteesFail-closed means the unknown requirement is unmet, not unnoticed. A brick demanding floor: ['signed-by-treasury'] from a runtime that has never heard of it must not have the demand quietly dropped.
CERT1▸certified:true is not self-authenticating✓
property¬wellFormed(cert) ⇒ isZero(Brick(…))
guaranteesThe cost certificate is the fourth carrier, and the one that never got the treatment the other three did. The constructor stored it with no validation at all, so certificate at this layer meant an object asserting certified:true — {verdict:{certified:true,costClass:'poly'}} composed LIVE, allow, free. No issuer, no subject, no analyzer, no policy.
CERT2▸an admitted certificate binds its subject and may not out-permit its own verdict✓
propertywellFormed(c) ⇒ binds(subject, analyzer) ∧ strictness(c.policy) ≥ strictness(decisionOf(c.verdict))
guaranteesA presented certificate must at least bind what it certifies. Coherence is one-directional: a certificate may state a decision stricter than its verdict implies — a producer with its own policy layer may escalate a poly result — and may never state a more permissive one. certified must also be a real boolean: !! made the string 'false', the empty array and the empty object all read as certified.
CERT3▸composition never upgrades evidence✓
propertyauthenticated(a ⊕ b) ⇔ authenticated(a) ∧ authenticated(b)
guaranteesFolding two facts together cannot make either better attested than it arrived. A composite of one authenticated and one merely presented certificate is presented.
CERT4▸authentication is unforgeable by data and does not serialise✓
propertyisAttested is WeakSet membership; ¬isAttested(clone(c)) ∧ 'authenticated' ∉ verdict
guaranteesThe honest boundary this runtime can actually hold. box-and-box has no crypto and no dependency on the producer, so it cannot verify a signature and does not pretend to — it does what it already does for the identity terms, for the same reason: reference identity is the one property a caller cannot forge by writing data. Be precise about what this buys: attestation is unforgeable by data, not by code — anything that can import the module can attest. It is a defence against the boundary that matters for WORLD, receipts and replay: a certificate arriving as JSON, over postMessage, or out of a store can never be attested, because a WeakSet brand does not survive serialisation. The status is deliberately not a field — a privileged status stored as data is one any caller can write.
CERT5▸a certified verdict of unknown cost certifies nothing✓
propertycertified ∧ costClass = unknown ⇒ 0̲
guaranteesI certify that I do not know what this costs certifies nothing, and must not clear a floor whose whole subject is bounded cost. The floor tested certified === false and nothing tested the class, so the one combination that names its own ignorance was the one that passed. Every real class still composes, tower included — escalate is not annihilate.
CERT6▸composition never weakens resource policy✓
propertydecision(a ∘ b) ≥ max(decision a, decision b, decisionOf(result))
guaranteesThe composite decision was derived from costClass alone, so every stricter policy an operand carried was discarded on the way in: a certificate reading certified, poly, ANNIHILATE composed to certified, poly, ALLOW. That is policy laundering, and it contradicts the one-directional coherence rule the validator already enforces on a single certificate. Enforcing it per-leaf and dropping it per-composition made the rule true of every certificate and false of the algebra it was written to protect. Strictness now only accumulates, on allow < budget_check < escalate < annihilate.
CERT7▸an annihilate decision cannot enter the admitted carrier✓
propertypolicy.resourceDecision = annihilate ⇒ 0̲
guaranteesThe floor read the verdict and never the policy, so a certificate whose own instruction was do not admit this was admitted and composed LIVE. escalate and budget_check deliberately do not floor — they are live-with-an-obligation, and the composite carries them up at full strength rather than downgrading them. The brick itself stays structurally valid and unadmitted, the same shape as uncertified: policy is a floor condition, not a canonicalisation one.
CERT8▸an attested certificate is transitively immutable at attestation✓
propertyattest(c) ⇒ ∀ o reachable from c · Object.isFrozen(o)
guaranteesThe brand attached to a mutable object reference. Attest a certificate for hash-A, then set subject.hash = 'hash-B', and isAttested still said true — the certificate changed what it claimed to authenticate and the authentication survived. This is the attestation form of the shallow-frozen identity defect (CD14), one layer up. Freezing happens before branding, so there is no window in which an attested certificate is writable.
CERT9▸attestation binds a verifier to an exact subject, and the brick must be that subject✓
propertyverifyAndAttest(c, H) requires c.subject.hash = H; floor authenticated requires brick.artifact.hash = c.subject.hash
guaranteesWithout this the runtime established this certificate object was verified and never verified for this thing, so one attested certificate authenticated any number of unrelated bricks with different authority. 'Binds a subject' had been a statement made entirely inside the certificate. A brick now declares what it is (artifact), and absence is fail-closed: a brick that claims no identity cannot satisfy an authenticated floor.
CERT10▸a composite subject is a canonical composition identity, not a deduplicated leaf set✓
propertysubject(a |> b) = pipe(A,B) ≠ and(A,B) = subject(a & b)
guaranteessubject(a|>b) and subject(a&b) were both {parts:['A','B']}, and A|>A and A|>A|>A were both {parts:['A']}. A cost certificate whose subject cannot tell those apart is binding a bag of participants, not a composition — and those programs need not cost the same. What the identity may normalise is decided by which equations the suite actually proves: & flattens (CA1 associativity passes) but does not commute (CA2 is lattice-only; CP7 is the open counterexample) and does not dedupe (CA3 is lattice-only; cost and quantities accrue); |> does not flatten at all, because CP5/CP6 are declared-open.
CERT11▸a subject may never be empty✓
propertyvalid(subject) ⇔ isStr(kind) ∧ isStr(hash)
guarantees{kind:'weave-composite', parts:[]} was accepted and produced an admitted, authenticated brick — a certificate over the empty set — while the code four lines away said a certificate that names no subject certifies no subject. Two shapes for one obligation is how the empty one slipped through; there is now one.
CERT12▸attestation is a capability, not a free export✓
propertycreateAttestationAuthority() succeeds once per module instance; isAttested stays free
guaranteesThe previous round exported attest(cert) and said honestly that it was unforgeable by data but not by code. Once the same brand carries WORLD revisions and authority delegations, any module with package access may declare a fact authenticated is not a boundary at all. The authority is minted once, at bootstrap, and handed to whichever component actually verifies. The limit is stated rather than implied, and the noun matters: this is module-instance-order security, not realm — measured, two ESM instances in one realm mint two authorities with independent stores. Within one instance, code that runs before your bootstrap takes the authority instead. Reading is never a privilege, so isAttested remains a free export: asking whether a fact is authenticated must not require the power to make it so.
CERT13▸the canonical subject encoding is injective, and subject equality is the complete subject✓
propertyleaf ["leaf",kind,hash] · pipe ["pipe",L,R] · and ["and",T…]
guaranteesThe previous round replaced a deduplicated leaf set with a canonical term string and this page claimed a canonical term cannot collide. It could. Leaf hashes are arbitrary strings, so they shared a namespace with the grammar meant to distinguish them: subject(A |> B) and a leaf whose hash was pipe(A,B) were equal, and unAnd() parsed leaf strings as composite syntax so leaf("and(A,B)") & C collided with (A&B)&C. Untrusted input that looks like grammar being read as grammar — the same meta-error removed elsewhere, committed in the fix for the previous one. A canonical form built by concatenating untrusted strings is not canonical, it is a template. The term is now structured and serialised injectively, flattening reads a structured term from a private map rather than parsing a string, and leaf identity includes kind — {weave-ir, H} and {world-revision, H} both entered a term as bare H.
CERT14▸attestation alone does not authenticate a brick; attestation plus exact subject binding does✓
propertyauthenticatedFor(b) ⇔ isAttested(b.cost) ∧ sameSubject(b.artifact, b.cost.subject)
guaranteesisAttested(brick.cost) answers was this certificate object verified; it does not answer was it verified for this brick. The runtime asked the first and branded composites on it. Two things were conflated: the authentication property — an objective relation between an artifact and its evidence — and the authenticated floor, a contextual requirement that the relation exist. The floor decides whether authentication is required; it must not decide what authentication means. The property is now computed always, and the floor merely consults it.
CERT15▸an authenticated composite requires every operand authenticated for its own artifact✓
propertyauthenticated(a ∘ b) ⇔ authenticatedFor(a) ∧ authenticatedFor(b)
guaranteesThe laundering route. Two bricks each carrying an attested certificate bound to something else composed into an authenticated composite, and the operands' own identities disappeared from the result: X claiming X with a certificate for A, Y claiming Y with a certificate for B, produced a LIVE authenticated composite with subject pipe(A,B). Neither brick had to ask for an authenticated floor, because the branding step never consulted the binding.
CERT16▸a composite artifact is derived from operand artifacts, never from the certificate✓
propertyartifact(a ∘ b) = composeIdentity(op, a.artifact, b.artifact)
guaranteesIt was {...cost.subject} — the evidence manufacturing the identity of the thing it was supposedly evidence for, which makes any misbinding self-ratifying. The principle is the one this whole layer now rests on: evidence may authenticate an independently identified subject; evidence must never define the subject that makes the evidence appear valid. Both identities are computed by the same rule over different inputs, so they coincide exactly when each operand's certificate was bound to its own artifact, and diverge visibly when one was not. An operand declaring no artifact yields a composite with none, rather than borrowing one.
CERT17▸a canonical subject survives canonicalisation, JSON and structured clone✓
propertycomposite subject = {kind, hash, term} with hash = canonicalJSON(term), checked
guaranteesThe structured term first lived in a module-private WeakMap keyed on the subject object, so the meaning of a subject depended on whether that exact JS object had been minted by that module instance — and Brick() erased it when canonicalising an artifact into a fresh {kind, hash}. The certificate kept its term by reference and the artifact did not. A canonical identity is not canonical if reconstructing the same value erases information needed to extend that identity. The term is now durable data on the subject, and a term that disagrees with the hash it ships beside is refused — so a caller may hand one in and have it understood, and cannot lie about it.
CERT18▸exact binding is inductive at arbitrary depth, in every association✓
propertyartifact(compose*(A…N)) = subject(compose*(A…N)) for all depths and shapes
guaranteesCERT16 was true for two leaves and false at depth three: A & B bound correctly and (A & B) & C did not, because the two identities stopped being the same derivation once one side lost its structure. The law tested the base case and never the induction step, so it was green over a real closure failure. Depth and shape — left, right, balanced — are now swept rather than exemplified.
CERT19▸the authenticated carrier is closed at arbitrary depth✓
propertyauthenticatedFor(a) ∧ … ∧ authenticatedFor(n) ⇒ authenticatedFor(compose*(a…n))
guaranteesThe closure statement for authentication, matching AD1 for admission. One merely-presented leaf anywhere in the tree must break the brand for the whole tree — evidence is only as authenticated as its weakest participant.
CERT20▸presented evidence is bound evidence: binding is not part of authentication✓
propertypresentedFor(b) ⇔ artifact ∧ sameSubject(b.artifact, b.cost.subject); authenticatedFor(b) ⇔ presentedFor(b) ∧ isAttested(b.cost)
guaranteesBinding and authentication answer different questions — what is this evidence about and who established that it is genuine — and they were entangled, so binding was checked only when a brick asked for an authenticated floor. They are now layered: binding at the baseline, attestation on top. An absent artifact is not a contradiction — the brick has not said what it is, so it stays admitted and is neither presented-for nor authenticated-for; floor: ['bound'] turns the baseline rule into a positive requirement.
CERT21▸misbound evidence refuses at the baseline floor, attested or not✓
propertyartifact ∧ ¬sameSubject(artifact, cost.subject) ⇒ 0̲
guaranteesA certificate for A attached to an artifact X is not an unauthenticated certificate for X — it is the wrong certificate. It was admitted at the default floor, so the runtime held an object whose evidence explicitly named something else, and two of them composed into one. That is not a downgrade, it is an internally inconsistent admitted object. Evidence presented for a subject must first actually name that subject; authentication decides whether to trust the evidence, not whether it is about the thing carrying it. Misbinding is a floor condition rather than a canonicalisation one, so the brick is structurally valid and unadmitted — the same shape as uncertified.
CERT22▸subject equality is substitutive under composition✓
propertysameSubject(x,y) ⇒ composeIdentity(op,x,z) = composeIdentity(op,y,z), for every op and z
guaranteesterm was merely optional on every subject and equality compared kind+hash, so {kind,hash,term} and {kind,hash} were the same subject — and composing each with the same operand produced different identities, one LIVE and one 0̲. An equality relation under which x = y but compose(x,z) ≠ compose(y,z) is not the equality of the carrier; it is a coincidence of two selected fields. The repair is to remove the second representation rather than widen the comparison: subjects are a discriminated union on kind, a composite must carry its term, and anything else must not. Two subjects are equal only if replacing one with the other cannot change any future canonical identity.
CERT23▸a recursively canonical object enforces its invariants recursively✓
propertyisTerm(['leaf', k, h]) ⇒ k, h non-empty ∧ k ≠ 'weave-composite'
guaranteesEvery subject binds a hash — leaf or composite, no exceptions was enforced at the root and nowhere else: a leaf inside a term was checked with a bare typeof === 'string', so ['leaf','',''] was a well-formed node. A term containing it attested, was admitted, and cleared an authenticated floor while binding neither a namespace nor a digest at that position. An invariant enforced at the root of a tree is enforced on one node.
CERT24▸a runtime owns its attestation store✓
propertyisAttested(c, rtA) ⇏ isAttested(c, rtB)
guaranteesThe attestation brand began as one module-level WeakSet, documented for three rounds as module-instance-order security — an honest limitation, and not a scope. Once the same brand carries WORLD revisions, authority delegations, receipt admission and replay validity, it is the security root, and a security root whose extent is "whoever imported this file first" is not one. createComposeRuntime({verify}) mints a runtime that owns its store, so two tenants, worlds or verifiers in one process share no authentication state: a certificate attested by one is merely presented to the other. The module-level operators keep a default store, which is exactly the previous behaviour for anything that never asks for isolation. A verifier is mandatory — an authority that checks nothing relabels rather than authenticates.
CERT25▸the subject discriminator agrees with the term discriminator✓
propertykind = 'weave-composite' ⇒ term root ∈ {and, pipe}
guaranteesThe union was discriminated structurally — a composite must have a term — and not semantically: nothing asked what the term denoted. So a subject could declare kind:'weave-composite' while carrying a leaf term. It was a distinct subject at ingress and then evaporated at the identity layer: F ≠ A, yet F & C === A & C. A discriminator that the two halves of an object can disagree about is not discriminating.
CERT26▸every admitted composite subject is in the runtime's algebraic normal form✓
propertycanonicalTerm(t) ⇔ wellFormedTerm(t) ∧ root ≠ leaf ∧ t = normalize(t)
guaranteeswellFormedTerm proves a grammar. It does not prove the tree is the runtime's representative of its algebraic class — and the runtime itself only ever produces flat and, because CA1 is a passing law. So ['and',['and',A,B],C] was admitted beside ['and',A,B,C] with a different hash. Validity is not canonicality. Only proved equations are normalised: & flattens (CA1); & order and duplicates are untouched (CA2/CA3 are lattice-only, CP7 open); |> association is preserved exactly, because normalising it would assert an equation CP5/CP6 currently falsify. Noncanonical terms are refused, not repaired — a supplied term is an identity assertion, and a default may not overwrite a claim.
CERT27▸algebraically equivalent & assemblies have exactly one admissible representation✓
propertyleft-, right- and balanced-associated & trees over the same leaves mint one identity
guaranteesThe consequence that matters once these become WORLD revision ids, receipt identities and replay keys: two peers describing the same associative assembly must mint the same authoritative identity, or a revision id is a function of how somebody happened to parenthesise it. An identity is canonical only if every admissible representation of the same proved algebraic object produces the same identity. Verified over depths 3–6 in three associations, with |> deliberately staying distinct by association.
CERT28▸verification cannot change the claim being authenticated✓
propertysnapshot ▸ validate ▸ freeze ▸ compare ▸ verify(it) ▸ brand(it)
guaranteesThe certificate used to stay mutable while the injected verifier ran: validate, compare the subject to the caller's expectation, call verify, and only then freeze and brand. A verifier that writes to what it is checking moves the claim after the claim has been approved — verify(c){ c.subject.hash='B'; return true } made “verify this exact certificate for A” finish by authenticating B, which then cleared an authenticated floor and admitted. Freezing earlier is not enough on its own, because Object.freeze leaves an accessor an accessor; the certificate is therefore copied into inert data first, and validation, comparison, the verifier, the brand and the return value all see that one frozen snapshot. The structure verified must be the structure branded.
CERT29▸subject validation is total under the declared budget✓
property∀ admissible term, depth ≤ 4096 · nodes ≤ 100000 ⇒ a verdict, never an exception
guaranteesBecause |> association is preserved while CP5/CP6 are open, term depth is something a caller controls. Every walk over it recursed — wellFormedTerm, normalizeTerm, deepFreeze, and JSON.stringify in C++ — so past some engine-specific depth a hostile certificate produced a RangeError instead of 0̲. A limit the implementation discovers is not a limit the protocol declared. Every walk is now iterative and the ceiling is three stated numbers.
CERT30▸an over-budget subject refuses by name, never by exception✓
propertyover-budget ⇒ 0̲ with a named reason, and refusing costs less than accepting
guaranteesThe other half of CERT29: past the ceiling the answer must still be an answer. Depth and node count are separate exhaustions — a deep chain and a wide fan-out — and both refuse with a reason a caller can act on. A fan-out wider than the whole budget is refused in O(1) from the node itself: counting to a hundred thousand before declining to count to a hundred thousand is still doing the work.
CERT31▸a canonical hash is computed from what the term contains, never from what it volunteers✓
propertycanonTerm walks the structure; only leaf STRINGS reach JSON.stringify
guaranteescanonTerm was JSON.stringify, which asks a value how it would like to be serialised — it calls toJSON(). Array.isArray is true of an Array subclass, so a leaf could contain A and hash as X. Since sameSubject is kind+hash, a certificate about A attested against an expectation of X and the brick carrying it admitted. The doctrine the runtime states everywhere else — a supplied term is an identity assertion, checked against its bytes — was being enforced against bytes the asserter chose. Terms are now also copied, not adopted, so what a brick stores cannot tell a later reader a different story.
CERT32▸the canonical serialiser is byte-identical to the JSON.stringify that minted every existing hash✓
property∀ plain term t · canonTerm(t) === JSON.stringify(t)
guaranteesCERT31 replaced the serialiser so it could not be redirected by a hook and could not recurse. A canonical form that changes its bytes changes every hash ever minted, so the rewrite is admissible only if it is byte-for-byte the old one on plain data. Tested through the public surface over strings chosen to exercise JSON escaping — quotes, backslashes, control characters, a lone surrogate, astral pairs, and strings that look like the grammar itself.
TREE1▸a one-leaf composition tree returns a canonical Brick or 0̲, never the caller's input✓
propertycomposeTree(leaf) = ensure(leaf) through the shared floor
guaranteesThe leaf case was if (!node || node.op == null) return node — the caller's object, unexamined, out of a function that promises a composed brick. composeTree({id:'raw', cost:{nonsense:true}}) returned that object with no Value, no contract and no certificate; composeTree(42) returned 42. The correct identity operation on a single leaf is the one the algebra already defines, a |> ID, so the leaf takes exactly that path.
TREE2▸composeTree has no weaker ingress boundary than composeAnd/composePipe✓
propertyisZero(composeTree(x)) = isZero(x & none) = isZero(x |> ID)
guaranteesThe third public composition route canonicalised nothing whenever the tree had nothing to fold. A public route may not have a weaker ingress boundary because “nothing happened.” Nothing happening is not a reason to admit something that was never admissible — this is the identity-route defect the runtime has now closed four times (CD13's raw operand, CD4b's pass-through, ensure itself, and here). Scoped to ordinary operands: the units have their own rule about which operator they mean something under (CD15/CD16).
CD5▸an explicit null/undefined field is an ABSENCE, not a declaration✓
propertyisZero({feeds_into: null} |> narrow)
guaranteesCloses the second door into the same room. null is how a contract arrives from JSON when the field was never filled in — reading it as universal would reinstate the defect through the serialisation boundary.
CERT33▸the byte budget is canonical serialised UTF-8 bytes, not source string units✓
propertycanonBytes(s) === TextEncoder().encode(JSON.stringify(s)).length
guaranteesThe ceiling said 4 MiB and counted s.length. Those differ by six for a control character: 750,000 U+0000 is 750,000 source units and 4,500,055 canonical bytes, so a subject a third over the ceiling was admitted. A budget must name the quantity it bounds, and the quantity that matters is the one that gets stored, hashed and shipped. The length is computed without building the escaped string, because allocating 4 MiB to discover that 4 MiB is too much is the mistake the ceiling exists to prevent.
CERT34▸the hostile-data boundary is total: ingest yields a named 0̲ or a Brick, never an exception✓
property∀ hostile v · ingest(v) is a Brick, and 0̲ ⇒ it says why
guaranteesCERT28 made the certificate route snapshot-first, and the next question was whether that was a property of the route or of public ingress. It was the route: a throwing cost getter, a Proxy that traps getPrototypeOf, a term element with a throwing Symbol.toPrimitive each made an ordinary public call throw. The answer taken is that the boundary is declared and one function owns it — Brick/composeAnd/composePipe/composeTree are trusted construction over values you already own; ingest is the door for anything off a wire, and it snapshots to inert data first. An ingested brick is also deeply frozen, so the evidence a verdict was reached about cannot be rewritten afterwards.
CERT35▸refusing is not more expensive than accepting✓
property|refusal message| is bounded regardless of the size of what was refused
guaranteesFound by measuring the suite rather than reading it. malformedCert built its message with JSON.stringify(c.subject).slice(0, 200) — serialise the whole subject, keep 200 characters. Refusing a 100,100-leaf term therefore cost a full serialisation of the term: the check was O(1) and the sentence about the check was O(n). That is the same exhaustion the budget exists to refuse, reached through the one path everything hostile is guaranteed to take.
TREE3▸the fold's work is bounded: a shared child is priced per path, and an exponential DAG refuses by name✓
propertyfolds ≤ maxFoldNodes, and composeTree(x & x) === composeAnd(x, x)
guaranteesA depth ceiling is not a work ceiling. The previous round bounded this fold's depth and the handoff said it took the same ceiling as the term budget; depth is the only thing depth bounds. An AST is a graph, so a child reachable by two paths is folded twice, and 23 objects express 2²² folds — 112 seconds, refused by nothing. Sharing is not deduplicated, deliberately: & is idempotent on the capability lattice and is not idempotent on cost or quantities, so x & x is not x and memoising would change the arithmetic silently. A DAG is a tree that happens to share storage, and the budget prices it as the tree it denotes.
TREE4▸the operator is validated before the descent: an invalid root buys no subwork✓
propertyunknown op ⇒ refuses having read zero children
guaranteesThe operator used to be checked after both children had been folded, so an unknown operator at the root bought arbitrary valid subwork — 14 seconds in the witness — before the runtime discovered that the thing it was working for was never admissible. Witnessed by accessors on the child slots: if either is read, the law fails.
CERT36▸an inert snapshot has no semantic prototype: every field is own data✓
propertygetPrototypeOf(snapshot) === null ∧ every semantic field is an own property
guarantees{} inherits Object.prototype, which has an accessor named __proto__. JSON.parse treats that key as ordinary data and produces it as an own property — but copying it out with dst[k] = v runs the inherited setter and re-points the destination's prototype. So a certificate could arrive with no own subject at all, inherit a valid one, validate, attest — and then be rewritten through a prototype deepFreeze never walked, because getOwnPropertyNames does not see inherited properties. That is CERT8/CERT28 a third time, reached through inheritance rather than through mutability. Objects now get a null prototype and every field is installed with defineProperty, which never consults a setter — special-casing the name __proto__ would have fixed the witness and left the general defect in place. A field genuinely named __proto__ survives as ordinary own data, which is what a JSON document means by it.
CERT37▸descriptor-only ingress really is descriptor-only: no caller code runs during a snapshot✓
propertyarray indices come from the length descriptor; elements are read only via getOwnPropertyDescriptor
guaranteesThe per-key read was descriptor-based; index discovery was not. Array.from(src, …) iterates the source, so an accessor installed on an element ran once per snapshot. The outer catch kept the never-throw contract — which is why this was invisible — but a getter that performs a side effect and returns normally defeated the stronger property the boundary exists for. Never-throwing and never-executing are different guarantees, and only the second is what "inert" means.
CERT38▸the state WORLD requires is reachable by one call: ingested ∧ authenticated ∧ immutable✓
propertyingestAndVerify(raw) → a frozen brick whose exact certificate is branded in this runtime
guaranteesThe runtime ruled that WORLD accepts ingested-and-authenticated bricks only, and that state could not be constructed from outside. The brand is object identity in a WeakSet — deliberately, since that is what makes it unforgeable by data — so any copying boundary drops it, and ingest and verifyAndAttest are both copying boundaries: whichever runs second undoes the other. A rule whose required state has no construction path is not a rule. The sequence now happens inside the runtime, where the brand is applied after the last copy. It is deliberately not a field: an ingested: true boolean would be exactly the caller-asserted authority CERT1 removed, so the property is earned by which function produced the object and read as authenticatedFor(b) ∧ isFrozen(b).
CERT39▸the hostile boundary takes bytes, because reflection over an object is executable✓
propertyingestJSON(text) executes no caller code; adopt(obj) is named as the weaker route
guaranteesCERT37 promised that nothing caller-supplied runs during a snapshot. Object.getOwnPropertyNames and getOwnPropertyDescriptor are Proxy traps, so a valid brick behind a counting Proxy produced a live, authenticated, frozen result — the strongest state this runtime can hand to WORLD — while executing eight trap invocations of caller JavaScript. There is no portable way to inspect an arbitrary JavaScript object while guaranteeing its traps do not run: an API that has already received an object graph has crossed the line too late. So the guarantee moved rather than being patched. ingestJSON(text) parses bytes with a parser the runtime owns, which makes "no caller code executes" a fact about the input language instead of a hope about the input value; adopt(obj) keeps the object route under a name that no longer borrows the word "ingest". WORLD consumes only the first.
CERT40▸an own undefined is not absence: the boundary never erases present evidence✓
propertyown undefined ⇒ 0̲ by name, on every carrier
guaranteesThe copier skipped undefined because JSON has none and JSON.stringify drops such a key. Wrong in both directions: in an array, JSON.stringify emits null and keeps the slot, so the two carriers disagreed — and far worse, dropping it turned floor: [undefined] (present, invalid, refuses) into floor: [] (no requirement, admitted). The hostile boundary made the object less constrained than the input asked for. floor is the worst carrier for that to happen on, because an erased requirement is indistinguishable in a receipt from a satisfied one. Sixth carrier, same rule: absence may take a documented default; present-and-malformed may not be repaired into a stronger claim.
WIRE0▸the WORLD door is the same function however the caller got hold of it✓
propertyrt.f(x), const {f} = rt; f(x), and [x].map(rt.f) agree — for every ingress name
guaranteesingestJSONAndVerify was a method calling this.adoptAndVerify. Modules are strict, so a detached reference had this === undefined and threw a TypeError. Three things made that worse than an ordinary binding bug. It threw on the success path only — bad input still refused politely, so the failure appeared only once the caller got everything right. It broke the contract this runtime states most loudly, that the boundary never throws whatever it is handed (CERT34) — and the contract was true of the function while being false of the name. And of the ingress routes it was the only one written as a method, so the single door WORLD is specified to consume was the single door that broke under the idiom every consumer reaches for on a frozen namespace object.
WIRE1▸the byte budget bounds bytes, not source units✓
propertyutf8Len(text) > maxBytes ⇒ 0̲, for every UTF-8 width class
guaranteestext.length counts UTF-16 code units. Measured: 6,000,376 UTF-8 bytes went through a 4,194,304 ceiling live, authenticated and frozen, because U+0800 is one source unit and three bytes. This is CERT33's error — source units are not bytes — reappearing one boundary further out, in the function written to be the boundary. A budget must name the quantity it bounds; naming it is not enough, the check has to read it. The length is now counted without allocating the encoding, because a 4 MiB budget check must not build a 12 MiB buffer to decide it is over budget.
WIRE2▸a frame is not bytes until it is copied: no caller code participates in the bound✓
propertythe bound is read through %TypedArray%.prototype getters, never off the argument
guaranteesOutside review proposed ingestFrame(bytes: Uint8Array) as the narrower door. Measured before it was written, that reintroduces CERT39 one layer down: a Proxy over a Uint8Array passes instanceof and fires its traps, and a subclass whose byteLength getter lies both runs caller code and gets an oversized frame parsed. bytes.byteLength > MAX is exactly getOwnPropertyDescriptor(o, k) — a property read the caller animates. A typed array is still an object, so "the boundary takes bytes" is only true of an API that never asks the object anything. The bound is read through brand-checked intrinsics captured at module load, which a subclass cannot override and a Proxy has no internal slot to satisfy; a view onto a SharedArrayBuffer is refused because its contents can change between the check and the decode; and the bytes are copied before anything inspects them.
WIRE3▸duplicate member names refuse: a peer must be able to agree what was authenticated✓
propertya repeated object member ⇒ 0̲ by name, on every text route
guaranteesRFC 8259 §4 leaves duplicate names to the implementation — V8 keeps the last, other parsers keep the first, some refuse, some expose all. Measured: a brick declaring artifact twice, hash "B" then hash "A", came out live and authenticated carrying "A". Nothing about that is a fact two runtimes share, and a signature over it means nothing. RFC 7493 (I-JSON) forbids it, and RFC 8785 (JCS) builds on I-JSON precisely so that hashing has repeatable bytes — which is what RevisionRef will need. The check is a scan of the text, because by the time JSON.parse has returned the duplicate is gone and the survivor is whichever one the engine felt like keeping.
WIRE4▸a retained string is encodable: no lone surrogate reaches an identity✓
propertysurrogates and noncharacters ⇒ 0̲, in values and in member names, on every route
guaranteesJavaScript carries a lone surrogate happily; UTF-8 cannot represent one. TextEncoder silently replaces it with U+FFFD, so a hash this runtime authenticated is one it cannot transmit — the corruption happens on the way out of the process, not at some hypothetical foreign peer. Measured live and authenticated with U+D800 in the artifact hash. WIRE1 does not subsume this, and the ordering is the point: a strict UTF-8 decode rejects the raw form (bytes ED A0 80) and accepts "A\ud800", which is well-formed UTF-8 on the wire and only becomes a lone surrogate after JSON string-escape processing. Frame well-formedness and value well-formedness are two checks.
WIRE5▸the frame route yields the admissible state, and nothing weaker does✓
propertyingestFrameAndVerify ⇒ authenticated ∧ frozen; ingestFrame ⇒ frozen ∧ ¬authenticated
guaranteesThe composition WORLD consumes. CERT38 established that ingested-and-authenticated has to be reachable by one call, because two copying boundaries in series destroy the brand — whichever runs second undoes the other. WIRE1 moves that call to the frame. This law is the anchor: the door WORLD is pointed at actually produces what WORLD is specified to require, the non-verifying door is visibly weaker (frozen but not authenticated — the distinction WORLD reads), and a host that refuses the certificate refuses the brick by the host's own reason.
WIRE6▸owning a frame invokes no caller behaviour — the frame at return is the frame at call✓
propertythe copy performs no SpeciesConstructor, no constructor read, no property access on the source
guaranteesWIRE1/WIRE2 fixed the reads and left the copy as ArrayBuffer.prototype.slice — which is not an inert memmove. Its first steps run SpeciesConstructor(O, %ArrayBuffer%), reading O.constructor and then constructor[@@species] off an ordinary caller-supplied buffer, and the specification notes those steps may have side effects before the source data is copied. The captured pristine intrinsic called the caller's getter faithfully. Measured: a constructor getter that rewrites "hash":"A" to "hash":"B" in place produced artifact.hash B, authenticatedFor true — from a frame that held A when the call began. WIRE2 stayed green throughout, because it counted invocations of the getters it had replaced and never asked what the copy did. Capturing a function guarantees nothing if the function's own algorithm is specified to consult its operand. The copy is now %TypedArray%.prototype.set into a runtime-allocated buffer — internal slots and a memmove — and the element type is brand-checked through the intrinsic @@toStringTag, because set converts between element types.
WIRE7▸the boundary does not fetch its dependencies from the ambient realm at call time✓
propertyreplacing TextDecoder / Uint8Array / ArrayBuffer / JSON / Reflect.apply after import changes nothing
guaranteesOutside review replaced those globals after importing the module and measured frame ingress calling all of them — Reflect.apply 4×, TextDecoder 2×, Uint8Array 1×. Two threats were being conflated, and only one is WIRE's to answer. Hostile bytes in a trusted realm is WIRE's job: the frame must not be able to execute anything, and everything the boundary depends on is captured at module load. Hostile code sharing the realm is not, and no amount of capturing fixes it — ordinary ECMAScript primordials are mutable and reachable, which is exactly what SES/Hardened JavaScript lockdown() exists for. The declared contract: WIRE protects a trusted runtime against hostile input; it does not contain hostile code already executing in the same unhardened realm. If you need mutually hostile code in one process, give it a hardened realm, a worker, or a process — not a stricter parser. Capturing still earns its place inside that scope: it makes the boundary immune to accidental post-import patching, which is the failure that actually happens.

Declared open — 3 laws that do not hold

These run on every build, print FALSIFIED in red, and are expected to. They are not skipped, not pending, not hidden. Three of them (CP5, CP6, CP7) trace to one root cause — the Value.pi carrier. CD6 is a separate defect in the contract algebra, added 2026-08-22, and it is the one blocked on a ruling rather than on a fix. The suite exits process.exit((total === 0 && xpass === 0) ? 0 : 1), so the build fails if one of them starts passing without being promoted into a real suite. A fixed defect quietly left in the exception list would be worse than the defect. The counterexamples below come from a live run; the trial index is wherever the generator happened to find one and differs run to run.

CP5▸the |> floor is ASSOCIATION-INVARIANT✗ FALSIFIED
propertyisZero((a|>b)|>c) === isZero(a|>(b|>c))
guaranteesHow you bracket a pipeline must not change whether it survives the floor. It does. Symptom 1 of the carrier defect.
π=[consolidate, learn, consolidate] → (a|>b)|>c = 0̲, a|>(b|>c) = live
CP6▸NO backward execution step survives |>, in either association✗ FALSIFIED
propertya pipeline containing a backward phase step must floor to 0̲
guaranteesA composition that runs a phase backwards should be refused regardless of bracketing. Same root cause as CP5.
π=[learn, retrieve, learn] has a backward step yet survives: (a|>b)|>c = 0̲, a|>(b|>c) = LIVE
CP7▸&-operand order does not change a downstream |> floor✗ FALSIFIED
propertyisZero((a&b)|>c) === isZero((b&a)|>c)
guaranteesThe one you can feel. & is commutative — AC-COMM above proves its own floor is — but the merge sets its phase by first-non-null, so (A&B) and (B&A) exit at different phases and chain differently. Reproduce it in your browser.
π=[route, retrieve, retrieve] → (a&b)|>c = 0̲, (b&a)|>c = LIVE (& is "commutative")