From 5061bb1bd6aaa467ced3014b4797d591df534c21 Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Thu, 16 Jul 2026 20:41:44 -0400 Subject: [PATCH] docs(roadmap+adr) + formal: dev roadmap, ADRs 0020-0023, Lean authority model (proved) + TLA+ store MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Post-ratification deliverables (author-approved). - docs/spec/ROADMAP.md — phased development plan (Phase 0 scaffold → 1 prove the waist P1→P2→P0 → 2 ceremonies → 3 client libs → 4 BVP store), with the decided/held gate and per-phase exit criteria. - ADR 0020 — Authority = Effect × Assurance × Scope (product meet-lattice); rejects the linear verdict lattice. OB-12. - ADR 0021 — store append CAS now, Byzantine Vertical Paxos next (wedge/ reconfiguration; ref Abraham-Malkhi DCCL / Lamport-Malkhi-Zhou). OB-15. - ADR 0022 — signed-object grammar: one constructor, protected tuple, genesis STORE_ID_SELF. OB-13/OB-14. - ADR 0023 — the three-tier proof discipline (Lean+Aeneas / Tamarin-ProVerif / assumed crypto + conformance vectors). - formal/lean/Authority.lean — mathlib-free, COMPILES (exit 0), 25 theorems, 0 sorry: meet laws, attenuation (L4/PO-4), no-fail-open (OB-9/OB-12), order-independence (L1/PO-1). The Tier-3 algebra half, machine-checked. - formal/tla/CeremonyStore.tla — CAS append + anti-rollback state machine; invariants map to PO-2/2a/2c + OB-15/OB-16 (CAS-loser benign; checkpoint monotone; no rollback). - formal/README.md — how to check both, and why two tools. Nonbinding formal spikes per review-7; no wire structs frozen. Merge/implement of code remains gated on conformance vectors (Phase 1d). Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/adr/0020-authority-product-lattice.md | 254 +++++++++++++++ .../adr/0021-store-append-cas-now-bvp-next.md | 308 ++++++++++++++++++ docs/adr/0022-signed-object-grammar.md | 163 +++++++++ docs/adr/0023-three-tier-proof-discipline.md | 59 ++++ docs/spec/ROADMAP.md | 128 ++++++++ formal/README.md | 50 +++ formal/lean/Authority.lean | 126 +++++++ formal/tla/CeremonyStore.tla | 99 ++++++ 8 files changed, 1187 insertions(+) create mode 100644 docs/adr/0020-authority-product-lattice.md create mode 100644 docs/adr/0021-store-append-cas-now-bvp-next.md create mode 100644 docs/adr/0022-signed-object-grammar.md create mode 100644 docs/adr/0023-three-tier-proof-discipline.md create mode 100644 docs/spec/ROADMAP.md create mode 100644 formal/README.md create mode 100644 formal/lean/Authority.lean create mode 100644 formal/tla/CeremonyStore.tla diff --git a/docs/adr/0020-authority-product-lattice.md b/docs/adr/0020-authority-product-lattice.md new file mode 100644 index 0000000..315288b --- /dev/null +++ b/docs/adr/0020-authority-product-lattice.md @@ -0,0 +1,254 @@ +# ADR 0020 — Authority as a product meet-lattice (Effect × Assurance × Scope) + +- Status: Accepted (2026-07-16) +- Date: 2026-07-16 +- Context: The Ceremony Suite's narrow waist, P0 + ([`ceremony-contract.md`](../spec/ceremony-contract.md)), reached its + **v0.3.1 PROTOCOL FREEZE**. Review 7 (a protocol-freeze pass) filed + **OB-12 (severity B)**: the single most divergence-prone thing left in the + waist was the *type of an authority verdict*. Until this ADR it was carried + as a **linear chain of dispositions** — `deny ⊏ attest ⊏ ask ⊏ approve` — + one totally-ordered rung ladder. That shape had survived the split from the + v0.1.x monolith unexamined, and it is the carrier on which **all five laws** + (L1 meet-resolution, L2 tamper-boundedness, L3 fail-closed totality, L4 + attenuation, L5 ceremony gate) and the gate-acceptance checklist are stated. + Getting the carrier wrong quietly corrupts every law that quantifies over + it, so OB-12 was closed as a **type freeze**, not a wording tweak. +- Governed by / harmonizes with: **ADR 0002** (the `Caveats` meet-semilattice + and the unforgeable `ToolContext`; `meet`/`leq`/constructors, **no + `join`/`widen`**), **ADR 0012** (fence strength as a GLB over the report; + "narrow-only in both directions"), **ADR 0007** (step-up `Presence` as a + raise-only gesture axis), and the **#231** `passkey`→`attest` rename. This + ADR ratifies, at the ceremony-suite level, the decision text already frozen + in P0 §2.0/§2.4; the *proofs* that discharge it (PO-1, PO-3, PO-4) are the + held implementation phase. +- Scope: the **Authority** type — what `resolve` returns, what a `grant` + is, what a `ceiling` bounds. This is the *decision-semantics* carrier of the + P0 waist. It is distinct from, but built on the same algebra as, the + `Caveats` confinement lattice of ADR 0002 (see D7 and Notes). + +## Decision + +**Authority is a product meet-lattice of three independent axes**, with +componentwise attenuation. This is the frozen type (OB-12): + +``` +Authority = Effect × Assurance × Scope + Effect : deny ⊏ allow (deny = ⊥) + Assurance : none ⊏ presence ⊏ hardware (the old `attest` lives here) + Scope : once ⊏ session ⊏ durable (profile-declared closed order) + (e₁,a₁,s₁) ⊓ (e₂,a₂,s₂) = (e₁⊓e₂, a₁⊓a₂, s₁⊓s₂) + ⊥ = (deny, none, once) ⊤ = (allow, hardware, durable) +``` + +### D1 — Authority is the *product* of three lattices; meet is componentwise + +A verdict is not a rung; it is a **point** `(effect, assurance, scope)`. The +product of lattices is a lattice, so `⊓` is defined coordinatewise and the +meet identities (associative, commutative, idempotent) hold **automatically** +per axis and therefore on the product. Resolution `⨅ { authority(r) | r +matches q }` (L1) is exactly this product meet — hence order-independent, no +rule/file/load-order attack (**PO-1**). The three axes answer three +*orthogonal* questions and must never be forced onto one line: + +| Axis | Answers | Order | +|---|---|---| +| **Effect** | *what* is permitted | `deny ⊏ allow` | +| **Assurance** | *how strongly present* the human is | `none ⊏ presence ⊏ hardware` | +| **Scope** | *how long* the grant covers | `once ⊏ session ⊏ durable` (profile-declared) | + +### D2 — `deny` is the bottom of Effect; there is exactly one ⊥ + +`deny` is `Effect`'s ⊥, so `⊥ = (deny, none, once)` is the single denied +authority. There are **not** several semantically-equal "denied authorities" +to distinguish or accidentally order among — a fail-closed system whose bottom +is not canonical invites bugs where one deny out-ranks another. One ⊥, reached +by any axis meeting down through Effect, is the fail-closed floor L3 degrades +to. + +### D3 — `attest` is not a verb; assurance is its own axis + +The former `attest` disposition is **`Assurance = presence`** (or, with a +bound hardware/measurement attestation, `hardware`; P5 §4.1). Because it is a +coordinate and not a rung, it **composes with any Effect and any Scope**: +"allow, once, presence-required" and "allow, durable, hardware-required" and +"deny, none" are all expressible points. This is the formalization of ADR +0007's raise-only step-up `Presence` and the #231 `passkey`→`attest` rename: +the *strength of proof-of-presence* is independent of *what* was decided and +*for how long*. A grant with `Assurance > none` is **inert until a presence +proof discharges it** (P0 §3, the forward-only ratchet); un-discharged, it +degrades to `deny` (L3), and this degradation is ⊑-monotone. + +### D4 — `ask` is *not* an authority level; it is a control-flow result + +There is no `ask` rung. Resolution is a sum type: + +``` +Resolution = NeedsDecision (was `ask`: "no rule settled it — interact") + | Decided(Authority) +``` + +`NeedsDecision` has **no place in the lattice**; the gate never *grants* it. It +routes to a bound `DecisionSurface`; **headless (no surface) it degrades to +`deny`** (`⊥`-Effect, L3). The empty-meet default is load-bearing: the empty +product meet is `⊤ = (allow, hardware, durable)`, so *if an unmatched request +resolved to the empty meet it would fail OPEN*. L1 therefore makes the no-match +case an explicit `NeedsDecision` (piecewise, never a seed that would also +downgrade a legitimate `allow`). `resolve` is total (**PO-3**). + +### D5 — Scope is a profile-declared, *closed* order — not arbitrary strings + +A profile MUST publish its Scope set and its total order + meet (v1: +`once ⊏ session ⊏ durable`); an implementation **rejects a scope outside its +profile**. "Open vocabulary" means *a profile may extend the set*, never *any +string compares somehow*. This keeps the third axis a genuine lattice with a +decidable meet rather than an ungoverned free-text field that would break +`⊓`'s totality. + +### D6 — Attenuation is componentwise, under an explicit signed `ceiling` + +`PermissionRequest` carries an **explicit, signed `ceiling`** — the maximum +Authority the request may resolve to (P0 §2.1). L4 becomes: + +``` +effective = granted ⊓ required +granted ⊑ ceiling (componentwise: no axis exceeds the request ceiling) +authority(escalate) = ⊥ +``` + +`⊑` is the product order (`e₁⊑e₂ ∧ a₁⊑a₂ ∧ s₁⊑s₂`). The gate re-derives the +ceiling from policy at issue time and **re-checks each axis** before minting +(never trusts a surface-supplied ceiling); a grant exceeding it on *any* axis +is refused by the acceptance checklist (P0 §2.3, item 3). Authority composes by +meet and **never amplifies on any axis** (**PO-4**, `meet_never_amplifies` +lifted to the product). This is the ADR 0002/0012 "narrow-only, no `join`" +discipline, now three-dimensional and with a per-axis ceiling the old scalar +chain could not express. + +### D7 — The five laws lift componentwise; this is a carrier change, not a new law + +Freezing the product type touches **no law count**. L1 (meet-resolution) and L4 +(attenuation) are stated on the carrier and lift coordinatewise because a +product of lattices is a lattice; L2, L3, L5 are structurally unchanged. The +suite stays at **five laws**. This is the same algebra ADR 0002 established for +`Caveats` (a meet-semilattice with no widen), *generalized from one carrier to +a product of three* — the ceremony-suite `Authority` and the core `Caveats` +grant are siblings under one discipline, not two competing models. + +## Consequences + +**Positive** + +- **Orthogonality is expressible.** "Allow durably but require hardware + presence," "allow once with no presence," "deny" are distinct, composable + points. The old chain could not name most of these. +- **One meet, proven once.** Because the product's meet is the coordinatewise + meet of three trivially-correct small lattices, PO-1/PO-3/PO-4 reduce to + per-axis facts and lift for free — a much smaller proof surface for Lean + (Tier 3) than a bespoke order over fused dispositions. +- **`ask` can no longer be granted.** Lifting it to `NeedsDecision` removes an + entire class of confusion where a "please interact" sentinel could be + meet-ed, stored, or minted as if it were partial authority; headless + degradation to `deny` is now a typed, total function (L3). +- **Fail-open closed at the empty meet.** Making the no-match case explicit + (D4) removes the latent fail-open the empty product meet (`⊤`) would + otherwise create. +- **Per-axis ceiling.** Attenuation and the signed ceiling now bound *each + axis independently* (D6), so a policy can cap duration without capping effect + and vice versa — impossible on a single ≤. +- **Vocabulary hygiene (OB-9/OB-12).** One word, one job: `Effect`, + `Assurance`, `Scope` are authority axes; `NeedsDecision` and `escalate` are + control-flow / navigation, `authority(escalate) = ⊥`. No `ask` verdict, no + `attest` verb survives (P0 §2.4). + +**Negative / residual** + +- **Three axes to keep closed.** Each profile now owns publishing its Scope + order (D5); an implementation that forgets to reject an out-of-profile scope + reintroduces a non-lattice field. Guarded by conformance vectors, not by the + type alone. +- **Assurance is inert without discharge.** `Assurance > none` is a *promise* + until the presence proof + forward-only ratchet clears it (P0 §3); a caller + that treats a `presence`-tagged grant as already-active before discharge is a + bug the ratchet must catch, not the lattice. +- **Migration surface.** Any prose, schema, or test still speaking of `ask`/ + `attest` as verdicts must be rewritten; the DecisionMatrix and gate checklist + now quantify over three axis sets, not one ordered list. + +## Alternatives considered + +- **The linear verdict lattice `deny ⊏ attest ⊏ ask ⊏ approve`** (the prior + model). **REJECTED (OB-12)** on three independent grounds: + 1. **`ask` is not an authority level.** Placing it as a rung between `attest` + and `approve` implied it carried "more authority than attest, less than + approve" — meaningless. `ask` means *no rule decided; go interact*: a + control-flow outcome, not a grant. On the chain it could be meet-ed, + minted, or stored as partial authority, and the headless case had no + principled value. Lifting it to `NeedsDecision` (D4) is the fix. + 2. **`attest` conflated outcome with assurance.** One rung fused *what was + decided* (an allow) with *how strongly presence was proven* (a presence + proof). You could not express "deny with hardware presence," or trade + effect against assurance without also moving the other — because they + shared an axis. Factoring assurance into its own `none ⊏ presence ⊏ + hardware` order (D3) lets it compose with any Effect and Scope. + 3. **Scope had no home at all.** Duration (once/session/durable) was tracked + out-of-band, so a grant's lifetime could not attenuate under the same meet + or be bounded by the same ceiling. The product adds it as a first-class, + profile-declared axis (D5). + The chain also forced attenuation (L4) to be a single scalar ≤, unable to cap + one concern without the others, and gave the empty meet no safe default. The + product meet-lattice resolves all four defects with strictly *less* bespoke + algebra. +- **A four-axis product adding an explicit `Ask`/interaction axis.** REJECTED: + interaction is *control flow around* resolution, not a dimension *of* + authority. Modeling it as an axis re-imports exactly the category error of + putting `ask` in the lattice. It stays the `Resolution` sum type (D4). +- **Multiple distinct "denied" bottoms (per-reason deny).** REJECTED (D2): a + fail-closed system needs a single canonical ⊥. Deny *reasons* are audit + metadata on the record, never orderable authority values. +- **Free-text `Scope` strings with a runtime comparator.** REJECTED (D5): + "any string compares somehow" is not a lattice; the meet stops being total + and decidable. Scope is a closed, profile-declared order that an + implementation rejects outside of. + +## Notes + +- **Four independent reviewers converged** on `Effect × Assurance × Scope`. + OB-12 was closed as *4-way converged* (README review 7): four separate + adversarial passes, reasoning from different starting points (the `attest` + factorization, the `ask`-in-the-lattice smell, the missing duration concern, + and the empty-meet fail-open), each arrived at the same three-axis product. + That convergence is why this is frozen as a *type*, not left as an author's + call. +- **The five laws lift componentwise.** The frozen product carrier is a + *carrier* change, not a new law: L1 and L4 are stated over `Authority` and + lift coordinatewise (product of lattices is a lattice); L2/L3/L5 are + untouched. Count stays five. (This freeze rode alongside **OB-16**, which + corrected L2's *upward* direction to `TrustedStructure(m(R)) = + TrustedStructure(R)` — **equality**, not `⊆` — over the authority-generating + structure; that is a separate law correction, not part of this carrier + decision, but shipped in the same v0.3.1 cut.) +- **Roadmap: five → four.** With the algebra on a clean product carrier, the + next law-minimalism candidate is unifying **L1 + L4** into a single + "authority composes by meet" law (P0 §7). The count is decided by whether the + Lean formulation collapses them — *the algebra decides the count; ambition + doesn't.* Nothing here presumes that collapse; it is noted as a consequence + this freeze makes reachable. +- **Same discipline as the core lattice.** This `Authority` product is the + ceremony-suite sibling of the ADR 0002 `Caveats` meet-semilattice: `meet`, + `leq`, constructors — **no `join`/`widen`**. ADR 0012's "narrow-only in both + directions" and "GLB, never a stored parallel enum" carry over directly; the + only change is single-carrier → three-axis product. + +## References + +- P0 waist: [`docs/spec/ceremony-contract.md`](../spec/ceremony-contract.md) + §2.0 (frozen type), §2.4 (vocabulary), §3 (presence discharge / ratchet), + §4 (L1–L5), §7 (law minimalism). +- Suite index: [`docs/spec/README.md`](../spec/README.md) — OB-12 (type + freeze), OB-9 (empty-meet default), OB-16 (L2 upward = equality), PO-1/PO-3/ + PO-4. +- ADR 0002 (Caveats meet-semilattice + unforgeable context), ADR 0012 (fence + strength as GLB; narrow-only), ADR 0007 (step-up `Presence`, raise-only), + #231 (`passkey`→`attest` rename). P1 signed-object (the `ceiling`/`grant` + wire grammar), P5 rendering (`action.effect` binding, `hardware` attestation). \ No newline at end of file diff --git a/docs/adr/0021-store-append-cas-now-bvp-next.md b/docs/adr/0021-store-append-cas-now-bvp-next.md new file mode 100644 index 0000000..7fbd7ae --- /dev/null +++ b/docs/adr/0021-store-append-cas-now-bvp-next.md @@ -0,0 +1,308 @@ +# ADR 0021 — Store append: CAS now, Byzantine Vertical Paxos next + +- Status: **Accepted** — the steady-state append is **FROZEN** as + compare-and-swap on the expected head (v0.3.1 PROTOCOL FREEZE, 2026-07-16); + the Byzantine-Vertical-Paxos evolution is an **adopted roadmap**, **NOT + normative** until it lands its own ADR + a TLA+/Lean safety model. +- Date: 2026-07-16 +- Context: closes **OB-15** (Review 7, the v0.3.1 protocol freeze). Records the + chain-store append arbitration decision that P2 §1.1 states normatively, and + the sequenced evolution the README "Store roadmap" block adopts. Extends P2 + (Chain-Store Profile) §1.1/§4 and depends on P0 §2.0 (the `Effect × Assurance + × Scope` product lattice) and P1 §4·5 (the domain-separation tuple, which is + what makes `store_id`/`thread_id` a value the signature covers rather than + prose). Also touches P4 §2 (the quorum records) and P4 §3 (recovery), because + *replication* membership and *key-custody* membership are deliberately kept as + two separate thresholds. +- Origin: the adversarial review that flagged the **honest-race hole** — under + a naive "highest chain wins" or "different head at the same length ⇒ + equivocation" rule, two honest devices that each read a head, propose a + successor, and race to append would be indistinguishable from an attacker + forking the log. That is both a false-positive halt (a benign race trips + L2·H1's fork alarm) and a latent safety gap (no defined winner). The freeze + had to pick an arbitration rule *and* fix the definition of equivocation so + the two stop being confused. + +## Question + +How should the authority chain-store arbitrate **concurrent appends** — now, +for the single-writer steady state, and later, as a store is served by more +than one node — without any of: + +1. **re-opening the `P1 → P2 → P0` waist proof.** The provable MVP is that + triple; the append rule must be simple enough that the P2 trusted-state + machine (`untrusted_step_safe`, checkpoint monotonicity under `Extends`) + compiles and refines to Rust via Aeneas *today*; +2. **mislabeling honest races as attacks.** A CAS-loser is a device retrying, + not a Byzantine actor. Halting authority-minting on a benign race is a + self-inflicted denial of service, and "availability is a security property" + (P0 L2); +3. **committing prematurely to a consensus protocol** whose safety we have not + yet modeled. The chain-store is *deliberately not a blockchain* (P2 §1) — + no mining, tokens, leader election, or global total order — so whatever + replaces threshold-1 must be a **reconfigurable replication** protocol we + can prove, not a coin. + +## Decision + +### D1 — Freeze CAS-on-expected-head as the v0.3.1 steady-state append + +The append operation is **compare-and-swap on the thread's expected head** +(P2 §1.1, FROZEN): + +``` +Append(expected_head, next) commits next iff head(store_id, thread_id) == expected_head + otherwise the caller is a CAS-loser and RETRIES. +``` + +Single-writer / optimistic-concurrency; the **simplest** model that closes the +honest-race hole. `next` extends `expected_head` on the same `(store_id, +thread_id)` spine with `sequence` strictly greater (never a sibling) — the +forward-only ratchet's "extends" from P2 §1.1. This is the append rule the P2 +Lean trusted-state machine is written against; nothing here needs a quorum, a +leader, or a clock (validity keys on generation counters, P1 §2 — wall-clock is +provenance, never coordination). + +CAS is **not a lesser stand-in** for the eventual protocol — it is the +**threshold-1 steady-state case** of it (D3). Freezing it lets the waist be +proven now without foreclosing the evolution. + +### D2 — Refine equivocation: candidates and CAS-losers are NOT malicious + +This refinement is **load-bearing regardless of the append model** and survives +verbatim into the reconfigurable world: + +- a concurrent **candidate** record (an honest device proposing a successor to a + head it just read) is **NORMAL**; +- a **CAS-loser** (a candidate that lost the race to commit a parent) is + **BENIGN** — it retries; it is *never* evidence of misbehavior; +- **equivocation** is *two records both **committed** at the same `(store_id, + thread_id, sequence)` with different CIDs* — a genuine double-commit / fork, + not a race a writer lost. + +This aligns the append rule with P2 §4's anti-rollback layering: "fork = proof +of misbehavior" (§4 layer 3) applies **only at the certified frontier** — a +quorum-certified head, or one voter's conflicting certification votes. +Concurrent candidates and CAS-losers can never equivocate because neither is +committed at the certified layer. Confusing the two is exactly the DAG error P2 +§1 warns against (two heads at equal depth may be *legitimate* concurrent +descendants); the authority projection is a linear spine per causal thread, so +"one accepted successor at `n+1`" is a property of *commitment*, not of +*proposal*. + +### D3 — Adopt the roadmap: CAS → vertically-reconfigurable replication + +**Adopted sequencing (author's call):** prove the `P1 → P2 → P0` waist on CAS +first; **then** evolve P2 to separate a lean **steady-state** protocol from a +stronger **reconfiguration** mechanism. The separation is the core idea of +**Vertical Paxos** (Lamport-Malkhi-Zhou, PODC 2009) and its Byzantine +hardening, **Byzantine Vertical Paxos** (Abraham & Malkhi, IBM Zurich DCCL): an +auxiliary reconfiguration authority resolves *which configuration is active*, so +the ordinary read/write path can use **small quorums** while the expensive, +rare work is confined to reconfiguration. + +The reconfiguration primitive is **the wedge**: + +``` +1. FENCE the active configuration (stop it accepting new commands — "wedge") +2. CAPTURE a safe CLOSING STATE (preserve every acknowledged-but-partial + command decided in the old config) +3. CERTIFY the next configuration (quorum-sign the config transition) +4. RESUME under the new configuration +``` + +CAS is the degenerate wedge: a threshold-1 configuration whose "reconfiguration" +is trivial. Everything the freeze proves about the CAS steady state is the +`f = 0`/threshold-1 slice of the reconfigurable machine, so the evolution is +**additive**, not a rewrite — the same `AuthorityCheckpoint (store_id, +thread_id, sequence, head)` anchor, the same `Extends` order, the same D2 +definition of equivocation. + +### D4 — The two-node story (`f+1` steady / `2f+1` reconfiguration + a state-light witness) + +The target deployment shape mirrors P2/P3's solo-user **n = 2 device world** +(each enrolled device is the other's witness; the same k-of-n substrate as +revocation, reused): + +- **Steady state runs on `f+1` full nodes.** With `f = 1` that is the **two + enrolled devices** — both hold the full transcript and serve the ordinary + append/read path with a small quorum. This is what VP buys: the common case + does not pay majority-quorum cost. +- **Reconfiguration needs `2f+1` participants.** With `f = 1` that is three — + the two full nodes plus a **state-light witness** that participates *only* in + the wedge (fencing + certifying the next configuration) and does **not** carry + the full log. A phone, a cheap always-on box, or a cloud attestation node can + be the witness; it holds configuration/certification state, not history. +- **Safe failover.** If one full node is lost, the survivor plus the witness can + reconfigure to a new pair without losing any acknowledged command (D3 step 2) + and without a human racing to re-pin. This is the failover the frozen CAS + store cannot do — under CAS a lost sole writer is a manual recovery event. + +The exact fault-model quorum arithmetic (crash vs. Byzantine; whether the +Byzantine steady path is `f+1` with an honest reconfiguration authority or a +larger bound) is **pinned by the wedge ADR's TLA+ model, not asserted here** +(D7). The shape — *small steady quorum, larger quorum only at reconfiguration, +a witness that is heavy on trust and light on state* — is what is adopted. + +### D5 — Key custody is a SEPARATE threshold (Shamir), not the replication quorum + +**Do not conflate the replication configuration with the signing quorum.** They +answer different questions: + +- the **replication configuration** answers *which nodes order and commit + records* (the wedge quorum, D3/D4); +- **key custody** answers *who may sign authority* — the principal root and its + loosening entries (P4 §1–2). + +The signing key MAY be **Shamir-split** across a custody set that is +**independent** of the replication membership: a node can be in the active +configuration (it commits records) without holding a key share (it cannot mint +authority), and a Shamir share-holder can be offline and out of the +configuration entirely. Keeping the two thresholds orthogonal means a +compromise of the *replication* fabric cannot forge a signature, and a +reconfiguration cannot silently change *who can authorize* — that remains a +quorum-gated change to authority-generating structure under **P0 L2** (equality, +OB-16: sub-quorum actors can neither shrink **nor add** trusted structure). The +state-light witness (D4) is the clean example: it votes on configuration, holds +no key share, mints nothing. + +### D6 — The partition-authority ceiling becomes operation-sensitive on the §2.0 lattice + +Under the reconfigurable store, a node that can reach its steady-state quorum but +**not** a reconfiguration quorum (a partition) is not simply up-or-down. Its +authority **ceiling attenuates componentwise on the P0 §2.0 `Effect × Assurance +× Scope` lattice**: it may keep serving low-`Scope` operations within its fenced +configuration (e.g. `once`/`session`) while **`durable` scope and any structural +change** — anything that alters authority-generating structure — require a +certified reconfiguration and are therefore **denied** under partition +(fail-closed, L3). This is the honest, operation-sensitive version of "the store +is available": the ceiling degrades along the axes, `granted ⊑ ceiling` still +holds (L4), and the degradation is ⊑-monotone. CAS today is the flat case (a +sole writer's ceiling is its policy ceiling; a partition just stalls the +retry). + +### D7 — The wedge / closing-state is NOT normative until its own ADR + TLA+/Lean + +Explicitly out of the v0.3.1 freeze. Before any part of D3–D6 becomes normative +it must land: + +- **its own ADR** (the "wedge / closing-state" decision — expected next in the + ADR sequence), specifying the fault model, the exact quorum sizes, the + fencing mechanism, the closing-state capture, and the configuration-transition + record format; +- **a TLA+ model** of the wedge (fence → capture → certify → resume) proving + the safety invariant — **no acknowledged command is lost across a + reconfiguration, and no two configurations are simultaneously live** — under + crash and then Byzantine faults; +- **a Lean extension** of the P2 trusted-state machine showing the reconfigurable + transitions still satisfy `untrusted_step_safe` and checkpoint monotonicity + under `Extends` (the CAS proof is the threshold-1 instance it must subsume). + +Until those exist, implementations build to **D1 (CAS)** and **D2 (the refined +equivocation)** only. D2 is normative now *because it is append-model-independent*; +D3–D6 are the **adopted direction**, cited so implementers do not paint the CAS +store into a corner (e.g. by hard-coding "one writer forever" or by treating a +candidate as an attack). + +## Consequences + +- **The waist is provable today.** CAS is simple enough that the P2 Lean + trusted-state machine and its Aeneas refinement do not wait on a consensus + proof. The `P1 → P2 → P0` MVP proceeds on threshold-1. +- **Honest races never trip the fork alarm.** D2 makes L2·H1's + proof-of-misbehavior escalation fire only at the certified frontier, so a + two-device solo user racing two candidates gets a retry, not a `CHAIN HISTORY + REGRESSION` halt. This is also what P0 §3's attest transaction relies on + ("a fork is P2 proof-of-misbehavior, never a branch to silently adopt" — + checked per causal thread so concurrent threads never false-trip). +- **The evolution is additive.** Because CAS is the threshold-1 slice of the + reconfigurable machine and D2 is invariant across both, the BVP work extends + P2 rather than replacing it — same anchor, same `Extends`, same equivocation + definition. +- **Two full nodes get real failover — later.** The frozen store cannot fail + over a lost sole writer without human recovery; the adopted roadmap gives the + n=2 device world safe failover via a state-light witness, at the cost of the + wedge machinery, once D7's proofs land. +- **Custody stays decoupled from replication.** Shamir key-custody as a separate + threshold (D5) means neither growing the replication configuration nor losing + a replica changes *who can sign* — authority structure remains quorum-gated + under L2. +- **No blockchain.** The roadmap is reconfigurable *replication*, not consensus + by mining or a global order (P2 §1). The reference points are BVP / VP, not a + ledger coin. + +## Alternatives considered + +- **"Highest chain wins" / longest-log.** Rejected: this is the honest-race hole + itself — a truncated-or-forked-but-internally-valid log can be *longer*, and + two honest candidates at equal length are indistinguishable from a fork + (P2 §1, §3 finding #1). Length is not authority. +- **"Different head at the same `sequence` ⇒ equivocation."** Rejected: false on + a branching Conversation Graph and false for CAS races — it halts on benign + concurrency (D2). Equivocation is *committed* double-spend at the certified + layer, not divergent *proposals*. +- **Last-writer-wins (overwrite the head).** Rejected: silently drops an + acknowledged commit — the exact safety loss the closing-state capture (D3 + step 2) exists to prevent. Unacceptable for an authority transcript. +- **Jump straight to full BVP now.** Rejected: its safety is unproven in our + setting; adopting it before the TLA+/Lean model (D7) would block the waist + proof on a much larger obligation and violate law-minimalism ("the algebra + decides the count; ambition doesn't", P0 §7). CAS-first is the sequenced path. +- **Majority-quorum steady state (ordinary multi-Paxos / a BFT SMR in the hot + path).** Rejected as the *steady-state* rule: the whole point of the Vertical + Paxos separation is that the common path uses **small** quorums while a + separate reconfiguration authority does the expensive work rarely. Paying + majority cost on every append is the opposite of the n=2 solo-user ergonomics + P2/P3 target. +- **Leader election / a coordinator service.** Rejected as a permanent primitive: + it reintroduces the blockchain-shaped machinery P2 §1 explicitly excludes. The + reconfiguration authority in VP/BVP is a *rare-path* config master, not a + hot-path leader, and can itself be the state-light witness (D4). +- **One key threshold = the replication threshold.** Rejected (D5): conflating + custody with replication lets a fabric compromise forge signatures and lets a + reconfiguration silently move "who can authorize." Shamir custody stays a + separate threshold. + +## Tracking + +- **Steady-state append (D1) + refined equivocation (D2):** normative in P2 §1.1 + (v0.3.1 freeze). No further work — proven with the `P1 → P2 → P0` waist. +- **The wedge / closing-state ADR (D7):** the *next* decision in this sequence — + fault model, quorum sizes, fencing, closing-state capture, config-transition + record. **Blocks** any normativity for D3–D6. +- **TLA+ model (D7):** wedge safety (no acknowledged command lost across + reconfiguration; at most one live configuration) under crash then Byzantine + faults. To live beside the profiles (no `.tla` in the tree yet — this ADR is + the forcing function). +- **Lean extension (D7):** the reconfigurable P2 trusted-state machine subsuming + the CAS threshold-1 proof (`untrusted_step_safe`, checkpoint monotonicity). +- **Deployment (D4):** the n=2 + state-light-witness topology reuses the P3/P4 + enrollment + k-of-n substrate; the witness is a P4 role that votes on + configuration and holds no key share (D5). + +## References + +- **Byzantine Vertical Paxos — Ittai Abraham & Dahlia Malkhi (IBM Zurich DCCL).** + The Byzantine hardening of the VP separation; the reference for the + reconfigurable-replication target. +- **Vertical Paxos and Primary-Backup Replication — Leslie Lamport, Dahlia + Malkhi, Lidong Zhou, PODC 2009.** The origin of separating small-quorum + steady-state from a reconfiguration authority, and of the wedge/read-out on + reconfiguration. +- Adi Shamir, *How to Share a Secret*, CACM 1979 — the separate key-custody + threshold (D5). +- P2 (Chain-Store Profile) §1.1 (CAS + refined equivocation, FROZEN), §4 (the + external anti-rollback anchor; fork = proof-of-misbehavior at the certified + layer), §1 (linear authority spine; deliberately not a blockchain). +- P0 (Ceremony Contract) §2.0 (the `Effect × Assurance × Scope` product lattice + the partition ceiling attenuates on), L2/L4 (structural equality; attenuation), + §3 (the CAS attest transaction; per-thread fork check). +- P1 (Signed-Object) §2/§4·5 (`STORE_ID_SELF` genesis; the domain-separation + tuple that makes `(store_id, thread_id)` signature-covered). +- P4 (Identity Lifecycle) §2 (quorum records) and §3 (recovery) — the k-of-n + substrate the witness/reconfiguration quorum reuses. +- Schneier-Kelsey (1999); FssAgg (eprint 2008/185); RFC 6962 (CT Signed Tree + Heads / monotonicity); TUF — the canon for what a hash-chained log does and + does not buy (P2 §3). +- **OB-15** (Review 7, the v0.3.1 PROTOCOL FREEZE) — the finding this ADR + discharges; README "Store roadmap (adopted): CAS → Byzantine Vertical Paxos". diff --git a/docs/adr/0022-signed-object-grammar.md b/docs/adr/0022-signed-object-grammar.md new file mode 100644 index 0000000..9ddc934 --- /dev/null +++ b/docs/adr/0022-signed-object-grammar.md @@ -0,0 +1,163 @@ +# ADR 0022 — Signed-object grammar: one constructor, protected tuple + +- Status: **Accepted** — frozen in the v0.3.1 PROTOCOL FREEZE (2026-07-16, review 7); the *proof* that discharges it (PO-1c, a Lean canonicalization-injectivity contract, plus PO-8 allowlist-gating) is the still-held implementation phase. +- Date: 2026-07-16 +- Layer: **P1 (Signed-Object Profile)** — the foundation the other five profiles write in. This ADR records the grammar decision behind [`signed-object-profile.md` §2](../spec/signed-object-profile.md) and the genesis sentinel that P2 [`chain-store-profile.md` §1](../spec/chain-store-profile.md) consumes. +- Closes: **OB-13** (bare-cid signature gap → one constructor over a protected tuple) and **OB-14** (`store_id = CID(genesis)` is a non-computable fixed point → `STORE_ID_SELF` sentinel), both from the round-7 protocol-freeze review (README "Review 7 — the v0.3.1 PROTOCOL FREEZE"). + +## Context + +P1 makes objects **nameable, canonical, and verifiable** — it carries no authority semantics, but every authority-bearing profile above it (P0 requests/decisions, P2 store lines, P3 challenges, P4 identity records, P5 render transcripts) is a P1 signed object. So a gap in the signing grammar is a gap under the entire suite. + +Two earlier-draft formulations were found to be unsound by the freeze review: + +1. **The signature bound too little (OB-13).** A naive envelope signs only `cid = H(body)`: + + ``` + cid = H(body) + sig = Sign(signer, cid) ← the gap + ``` + + This authenticates the *body bytes* but leaves the **interpretation-bearing fields outside the signature**: `profile`, `codec`, and (depending on where the key id lives) `signer`. An attacker who cannot forge the signature can still, without breaking it: + - **re-tag the codec** — present the same `cid`/`sig` under a different declared `codec`, steering the verifier into a different (possibly attacker-favourable) decoder; + - **re-tag the profile** — replay a structurally-compatible body as a *different record type or profile version* (version-confusion / type-confusion), since the profile string that selects the schema was never signed; + - **swap the claimed signer** — if the key id sits beside the sig rather than under it. + + All three are the classic "the header selects the algorithm/interpretation but is not in the signed image" family — `alg:none`, JWS header injection, COSE critical-header confusion. The digest is honest about *bytes* and silent about *what those bytes mean*. + +2. **Genesis was a non-computable fixed point (OB-14).** P1 §4·5 makes *every* signed body begin with a domain-separation tuple that binds `store_id`. P2 defines `store_id = H(genesis record)`. The genesis record's body must therefore contain `store_id = H(genesis record)` — a value that depends on the very bytes being hashed. The first record of every store could not be canonically encoded at all. + +A third, related hazard motivates the grammar being *singular*: the earlier text said both "JSON for interchange, TOML at rest, DAG-CBOR for signing" **and** "verify over received bytes, never reserialize." Those contradict — a recipient handed JSON did not receive the signed DAG-CBOR bytes, and JSON → DAG-CBOR *is* a reserialization that need not reproduce the signed digest (RFC 8785 pitfall). + +## Question + +What is the **one normative constructor** for a signed object such that (a) nothing that changes an object's *interpretation* can change without breaking the signature, (b) there is no split identity between the envelope and the body it wraps, (c) verification is total and allowlist-gated before any attacker-influenced bytes are touched, (d) JSON/TOML remain usable as views without ever becoming a second authority-bearing serialization, and (e) the genesis record is canonically encodable despite `store_id` depending on its own hash? + +## Decision + +### D1 — One constructor; the signature covers a canonical *protected tuple*, not the bare CID + +There is exactly **one** signed-object grammar (no per-object choice). The signature covers a canonical **protected tuple** that pulls every interpretation-bearing field *inside* the signed image, domain-separated: + +```json +{ "profile": "agent-bridle/permission-request/v1", // protected + "codec": "dag-cbor", // protected + "cid": "cid:…", // = H(body); protected + "signer": "b3:…", // protected (fingerprint = H(pubkey)) + "body": "", // carried, not reconstructed + "sig": "…" } +``` +``` +protected = canon( "agent-bridle/signed-object/v1", // domain separation + profile, codec, cid, signer ) +sig = Sign(signer, protected) +``` + +Normative bindings (no implementer discretion): + +- **`sig` covers `protected`.** `profile`, `codec`, `cid`, and `signer` are all authenticated; changing any one breaks the signature. The bare-cid gap is closed by construction — a re-tagged codec, a re-tagged profile, or a swapped signer yields a different `protected` and therefore a verification failure. +- **The domain-separation constant `"agent-bridle/signed-object/v1"` is the first element of `protected`**, so a signature minted for this grammar cannot be cross-protocol-replayed as anything else, and the envelope grammar itself is versioned. +- **`signer` is the single canonical location for the key id.** The `by` field seen in inner-record examples (P0/P4) is the *same* value surfaced logically inside a body — never a second authority. `signer` is the pinned fingerprint `H(pubkey)` (P1 §1), self-certifying under L5. +- **`cid = H(body)` binds the body to the envelope**; the body bytes are **carried** (`base64url` of the canonical DAG-CBOR), never reconstructed by the recipient. This resolves the "sign DAG-CBOR / verify received bytes" contradiction: the canonical bytes travel intact, so the verifier can verify over exactly what was signed. +- Determinism (Ed25519, P1 §5) guarantees `protected` maps to one signature encoding, so re-signing does not fork a chain built over these objects (P2). + +### D2 — The body's domain tuple MUST equal the envelope (no split identity) + +Pulling the fields into `protected` is necessary but not sufficient: the *body* also carries its own domain-separation tuple (P1 §4·5), and it must not disagree with the envelope wrapping it. Otherwise an object could be honestly signed at the envelope while its inner tuple claims a different profile/version/signer. + +``` +body domain tuple = ("agent-bridle///", + store_id, thread_id_or_principal_id, generation, ) +``` + +Normative equality check (an implementation **rejects any mismatch**): + +- the body's domain-separation prefix MUST identify the **same** `profile` (and record-type/version) declared in the envelope; +- the body's declared `codec` MUST equal the envelope `codec`; +- the body's `signer`/`by` MUST equal the envelope `signer`. + +There is **one identity across the boundary**, asserted twice and required to match — the envelope cannot claim one signer while the body attributes itself to another, and the profile cannot be re-labelled between the two layers. + +### D3 — Verification order (allowlist before body; verify-over-received-bytes) + +Verification is **identical in all four client languages** (Rust/Python/Dart/TS) and total (fail-closed). The order is load-bearing, not stylistic: + +``` +1. allowlist codec + algorithms (P1 §4·4) — BEFORE touching body +2. recompute protected; verify sig over it under signer +3. verify cid == H(body) +4. decode body; check body domain tuple == (profile, codec, signer) (D2) +5. schema + critical fields; reject unknown authority-bearing fields +6. construct Sealed +``` + +Why the order matters: + +- **Step 1 precedes any hashing or decoding (PO-8).** Self-describing identifiers let the *object* declare its algorithm; a verifier that dispatched on the declared code alone would let an attacker pick a broken hash or `alg:none`. The declared `codec`/algorithm codes are checked against the locally-trusted Profile v1 table **before** the body is hashed or the sig verified. Agility lives in the profile, never on the wire. +- **Step 2 verifies over the recomputed `protected`, and step 3 verifies `cid == H(body)` over the *received* canonical bytes** — never a re-serialization of a parsed object. Typed deserialization drops unknown fields; reserializing cannot reproduce the signed digest. +- **Step 4 enforces D2.** Only after the sig and CID check does the body get decoded and its inner domain tuple compared to the envelope. +- **Step 5 fails closed on unknown authority-bearing fields** (silent-downgrade / version-confusion surface). Non-authority annotations may be preserved verbatim only when the profile marks them non-critical (COSE critical-header model). +- **Step 6 is the only way an object enters a kernel.** `Sealed` is the Rust heir of the content-addressable `Memo` read-time tamper check: objects are constructed *only* through this verification, immutable after. Nothing unverified crosses into P0's decision kernel. + +### D4 — JSON and TOML are views/containers, never independent authority-bearing serializations + +The **authority lives in `body` + `protected`.** Everything else is a rendering: + +- A **JSON** rendering is for humans and non-authority interchange. It is never itself verified as the signed image — a recipient who is handed JSON must obtain the carried canonical `body` bytes to verify; a JSON reconstruction is not the signed object. +- **TOML policy files (#220)** *wrap* the signed object; the TOML is a container around `body`/`protected`, not a parallel signed form. +- Because there is one signed byte-string and it is carried (D1), "many views, one signed image" is consistent: views may be lossy or reformatted freely, and none of them is authoritative. +- **Wall-clock is never a coordination primitive.** Validity keys on generation counters (the domain tuple's `generation`); RFC 3339 timestamps are provenance *data* inside the body, not authority. + +### D5 — Genesis `STORE_ID_SELF` sentinel breaks `store_id = CID(genesis)` + +The fixed point (OB-14) is broken by a reserved sentinel, not by exempting genesis from domain separation: + +- The **genesis body carries the reserved sentinel `store_id = 0x00` (`STORE_ID_SELF`)** in its domain tuple — a fixed, canonically-encodable value, so the genesis record can be encoded, hashed, and signed like any other object under D1. +- **The resulting `cid` of the genesis record *becomes* the store's `store_id`.** +- Every **subsequent** record binds that concrete `store_id` value in its own domain tuple (P1 §4·5), so no later record can be replayed into a different store. +- A **verifier resolves `STORE_ID_SELF` to "this record's own cid"** when checking the genesis record's domain tuple — the only record for which the sentinel is legal. `STORE_ID_SELF` appearing in any non-genesis record is rejected (fail-closed). + +This makes P2's `store_id` a normative, cryptographically-bound identifier (consumed by P2 §1's `AuthorityCheckpoint`) without circularity: genesis names itself via the sentinel; the store's identity is genesis's CID; everyone after commits to that identity. + +## Consequences + +- **The interpretation of an object is now authenticated, not just its bytes.** Codec-confusion, profile/version-confusion, and signer-swap are all detected at step 2 — they are no longer "valid signature, wrong meaning." +- **No split identity.** D2's equality check means an object cannot be honestly signed at the envelope while lying in its body about profile, codec, or signer. +- **One constructor for the whole suite.** P0/P2/P3/P4/P5 records are all this one shape; a single Lean canonicalization-injectivity contract (PO-1c) plus the allowlist-gating proof (PO-8) covers signing for every profile above P1. The kernel consumes `H` and `Sign` as **abstract injective / one-way contracts**, which is what lets Aeneas run without modelling crypto. +- **Views are free.** JSON/TOML can be reformatted, pretty-printed, or lossily projected without touching authority, because authority is the carried `body` + `protected`, never the view. +- **Genesis is canonically encodable**, so P2's per-record `store_id` binding (the anti-replay-across-stores property under P1 §4·5) has no exception carved out for the first record. +- **Cost:** the body bytes are carried (base64url) in addition to the CID, so a signed object is larger than a bare `{cid, sig}` reference. This is deliberate — "verify over received canonical bytes, never reserialize" requires the bytes to be present. Reference-only forms (e.g. `parents` links in P2) still carry just a CID, because they point at an object that is itself carried elsewhere. + +## Alternatives considered + +- **Bare-cid signature (`sig = Sign(signer, H(body))`).** Rejected (OB-13): leaves `profile`/`codec`/`signer` outside the signed image — the codec-retag / profile-confusion / signer-swap attacks above. +- **Detached signature over the JSON view.** Rejected (D4): JSON is not injective/canonical for signing; verifying a reconstructed JSON is exactly the reserialization the RFC 8785 pitfall warns against, and it makes a human-facing view authority-bearing. +- **Per-object choice of "sign the CID" vs "sign the tuple."** Rejected: two constructors is two attack surfaces and two proofs; the freeze mandates **one** normative constructor. +- **Omit the domain-separation constant from `protected`.** Rejected: without `"agent-bridle/signed-object/v1"` inside the signed image, a signature is cross-protocol-replayable and the envelope grammar is itself unversioned. +- **Exempt the genesis body from the domain tuple** (so it need not bind `store_id`). Rejected (OB-14): a per-record exception is a permanent special case in every verifier and a version-confusion foothold; the `STORE_ID_SELF` sentinel keeps genesis a *normal* signed object with a resolvable placeholder instead. +- **Randomized signatures (ECDSA random-nonce).** Rejected (P1 §5): a fresh signature on every re-sign changes the content hash and forks any P2 chain built over the object; Profile v1 pins deterministic Ed25519. + +## Proof obligations + +| PO | Statement | Tier | +|---|---|---| +| PO-1c | canonicalization is injective; verify-over-received-bytes is sound (one value ⇒ one byte-string; a parsed-then-reserialized object cannot reproduce the signed digest) | 3 (Lean contract) | +| PO-8 | algorithm/codec dispatch is allowlist-gated — no code outside the Profile v1 table is honoured (step 1 before any hashing) | 3 | +| WF-2 | the Memo discipline holds structurally on every wire object (content-CID unconditional; `signer`/`sig` at trust boundaries; `parents` for durability; Sealed at load) | vector | + +These are P1's obligations; the crypto primitives underneath (`H` collision-resistance, `Sign` unforgeability, deterministic-nonce) are **Tier 1** — assumed, cited to the literature, rotatable via the Profile-v1 allowlist. Positive + negative **conformance vectors** (shared JSON, kyln round-trip pattern) bind the four client languages to one observable verification behaviour — the teeth that keep implementations honest where proofs stop. They ship with the kernel (`suite.toml` `conformance_vectors`), the single implementation-phase item of the v0.3.1 exit gate. + +## Tracking + +- Grammar (D1–D4): `docs/spec/signed-object-profile.md` §2 / §4·4 / §4·5; closes **OB-13**. +- Genesis sentinel (D5): `docs/spec/signed-object-profile.md` §2 and `docs/spec/chain-store-profile.md` §1; closes **OB-14**; consumed by P2's `AuthorityCheckpoint.store_id`. +- Build/prove order: this is P1, the first profile proven — **P1 → P2 → P0 → P4 → P3** (README). + +## Relations + +- Suite index: [`README.md`](../spec/README.md) — Review 7 / v0.3.1 PROTOCOL FREEZE table (OB-13, OB-14). +- Owning profile: P1 [`signed-object-profile.md`](../spec/signed-object-profile.md). +- Consumers of `store_id`/`STORE_ID_SELF`: P2 [`chain-store-profile.md`](../spec/chain-store-profile.md) §1 (`AuthorityCheckpoint`, per-record store binding). +- Domain-tuple context binding (`store_id`, `thread_id`/`principal_id`, `generation`): P1 §4·5, discharging OB-6. +- `content-addressable` crate — `ContentId`, canonical DAG-CBOR, `MerkleNode`, the `Sealed` this grammar constructs; `Memo` read-time tamper check (WF-2). +- agent-mesh#66 — multihash wire format for `Fingerprint` (`signer`); #226/#227 — signed loosening entries as an existing P1 object. \ No newline at end of file diff --git a/docs/adr/0023-three-tier-proof-discipline.md b/docs/adr/0023-three-tier-proof-discipline.md new file mode 100644 index 0000000..51f7f23 --- /dev/null +++ b/docs/adr/0023-three-tier-proof-discipline.md @@ -0,0 +1,59 @@ +# ADR 0023 — The three-tier proof discipline + +- Status: **Accepted** (2026-07-16). Formalizes the verification architecture + the adversarial reviews demanded. +- Related: `docs/spec/README.md` ("The teeth"), `formal/`, ADRs 0020–0022. + +## Context + +Across review rounds 4–7, the recurring failure the reviewers punished was +*"prose becomes authority-bearing protocol"* — a claim proven at the wrong +level, e.g. an algebraic lattice argument used to justify a protocol's +freshness, or a hash-chain used to justify rollback resistance it does not +provide. A single "we'll prove it in Lean" is not credible, because different +claims need different tools. + +## Decision + +Correctness is enforced in **three tiers, each verified by a different kind of +tool, and the tiers are never conflated.** + +- **Tier 3 — kernel refinement (Lean + Aeneas).** The *authority algebra* and + the *trusted state machine*. A pure Rust kernel is extracted by Charon and + proven in Lean via Aeneas to **refine** a hand-written model. The algebra + lives in `formal/lean/Authority.lean` (meet laws, attenuation, no-fail-open, + order-independence — 25 theorems, 0 `sorry`); the store state machine lives + in `formal/tla/CeremonyStore.tla` (CAS append, checkpoint monotonicity, + no-rollback). CI gate: **no Rust kernel merges unless its refinement proof + passes.** +- **Tier 2 — protocol safety (Tamarin / ProVerif).** The *ceremonies* + (enrollment, introduction, discharge). A flawless lattice can sit behind a + leaky handshake, so MITM / replay / unknown-key-share get *symbolic* proof + under Dolev-Yao — **not** an algebraic argument. +- **Tier 1 — cryptographic primitives (assumed, cited).** Ed25519 + unforgeability, BLAKE3 collision resistance, deterministic nonces. The trust + base; rotatable via P1's algorithm allowlist. +- **Cross-cutting — conformance vectors.** Shared positive+negative JSON + vectors bind the four client languages to one observable behavior where + proofs stop. + +## Consequences + +- Each spec claim is tagged with the tier that discharges it (the PO ledger in + `docs/spec/README.md`). A claim with no tier is not a claim — it is prose. +- The pure kernel must stay pure (no serde/IO/crypto/UI) so Aeneas can run; + crypto enters as abstract injective/one-way contracts at the kernel edge + (ADR 0022). +- Tooling cost: three verifiers plus a vector harness. Accepted — it is the + price of not asking reviewers to intuit the protocol. + +## Alternatives considered + +- **One tool for everything (Lean only).** Rejected: Lean/Aeneas proves + functional correctness of pure code, not Dolev-Yao protocol safety; forcing + a handshake into a refinement proof would be exactly the tier-confusion the + reviews caught. +- **No formal track, tests only.** Rejected: the review series repeatedly + found soundness bugs (empty-meet fail-open, latent authority injection) that + survived passing tests; the whole point is that the adversary becomes a + proof checker. diff --git a/docs/spec/ROADMAP.md b/docs/spec/ROADMAP.md new file mode 100644 index 0000000..9899e41 --- /dev/null +++ b/docs/spec/ROADMAP.md @@ -0,0 +1,128 @@ +# Ceremony Suite — Development Roadmap & Project Plan + +**Status:** active, 2026-07-16. The spec is **ratified** (v0.3.1 protocol +freeze, PR #229 merged to `main`). This plan sequences the work from here to +a shipped, formally-verified, multi-language enforcement gate. + +**The governing rule:** *prove the narrow waist before building outward, and +never fossilize a wire format ahead of its conformance vectors.* Everything +below respects the dependency DAG `P1 → P2 → P0 → P4 → P3` (P5 on +{P0,P1,P4}) and the three proof tiers (Tier-3 Lean+Aeneas, Tier-2 +Tamarin/ProVerif, Tier-1 assumed crypto). + +## What is decided vs. held (the gate) + +- **Decided & frozen (v0.3.1):** the authority type (`Effect × Assurance × + Scope`), `ask`→`NeedsDecision`, the explicit ceiling, the signed-object + protected-tuple grammar, genesis `STORE_ID_SELF`, CAS append, the five + laws (L2 upward = equality). ADRs 0020–0023. +- **Safe to build now (nonbinding spikes):** the pure algebra/kernel and its + proofs; `Sealed` with adversarial property tests; a CAS-based P2 state + machine; DAG-CBOR/signature experiments; Lean/TLA+ models. +- **HELD until its conformance vectors exist:** frozen Rust structs, + serialized records, DB schemas, cross-language APIs, stored signatures. +- **Roadmap-only (post-waist):** Byzantine-Vertical-Paxos store evolution. + +--- + +## Phase 0 — Ratify & scaffold *(this cut)* + +| # | Deliverable | State | +|---|---|---| +| 0.1 | Merge the spec suite to `main` | ✅ PR #229 | +| 0.2 | ADRs 0020 (authority type) · 0021 (append CAS→BVP) · 0022 (signed grammar) · 0023 (proof discipline) | this cut | +| 0.3 | **Lean authority model** — `formal/lean/Authority.lean`, 25 theorems, 0 `sorry`, compiles | ✅ this cut | +| 0.4 | **TLA+ store model** — `formal/tla/CeremonyStore.tla` (CAS + anti-rollback invariants) | this cut | +| 0.5 | Aeneas/Charon toolchain green on gnuc (opam/OCaml leg) | pending (`../TOOLCHAIN.md`) | + +**Exit:** ADRs merged; both formal models under `formal/`; toolchain ready to +extract Rust→Lean. + +## Phase 1 — Prove the waist *(P1 → P2 → P0)* — the MVP + +The provable core. Each profile lands as: pure kernel → property tests → +formal proof → conformance vectors. + +- **1a P1 Signed-Object.** `ContentId`/canonical DAG-CBOR/`Sealed`; the + protected-tuple constructor + verify order (ADR 0022); algorithm allowlist; + genesis sentinel. Property tests (round-trip, tamper, unknown-field + fail-closed). *Gate:* PO-1c, PO-8 as Lean contracts + vectors. +- **1b P2 Chain-Store (CAS).** The append CAS + the anti-rollback trusted-state + machine. **TLA+/TLC model checked first** (`CeremonyStore.tla`), then the + pure Rust state machine refined to it. *Gate:* PO-2/2a/2c; TLC invariants + green. +- **1c P0 Authority kernel.** Pure `resolve` (piecewise, no fail-open) + + precedence + the gate-acceptance checklist. **Charon extracts the Rust + kernel; Aeneas proves it refines `Authority.lean`.** *Gate:* PO-1/3/4/5 + + the refinement bridge theorem; CI blocks any kernel that fails it. +- **1d Conformance vectors.** `tests/vectors/*.json` — positive **and + negative** — the cross-language behavioral contract. *This unblocks the + "held" wire freeze.* + +**Exit (the big one):** the Rust waist compiles, refines the Lean model, +passes the TLA+-checked store invariants, and the conformance vectors are +published. Only now do wire structs stop being nonbinding. + +## Phase 2 — Ceremonies *(P4 → P3 → P5)* + +- **2a P4 Identity Lifecycle.** Roles/delegation, records, quorum revocation + (exact policy predicate), break-glass/succession (conditional PO-R). Implements + P0's `AttestEvidence`/`ValidAssociationProof`. +- **2b P3 Enrollment.** SAS pairing, PoP introductions (recipient-issued + challenge, consume-last). **Tier-2: Tamarin/ProVerif** proofs of + freshness / no-MITM / no-unknown-key-share. +- **2c P5 Rendering.** Effect binding, gate-signed requests, surface + attestation (byte-compare canonical render; token = attention aid; **no raw + secrets**). Stated human-factors residual. + +**Exit:** the full ceremony flow works end-to-end against a reference harness; +protocol proofs green. + +## Phase 3 — Client libraries + +One Rust enforcement core; consumer-side libs elsewhere. **Never fork the gate.** + +- Rust (reference, `agent-bridle`) · Python (`agent-bridle-py` PyO3 — exists) · + Dart (flutter_rust_bridge → newt-mobile) · TypeScript (Claude Code / Codex — + pure-spec impl likely). All bound by the Phase-1d conformance vectors. +- First consumer: **newt-agent #1209** (the pinning ceremony). + +## Phase 4 — Store evolution: Byzantine Vertical Paxos *(post-waist)* + +Only after the waist is proven. Evolve P2 from CAS (threshold-1 steady state) +to **vertically-reconfigurable replication**: lean steady state + a stronger +**wedge**-based reconfiguration (fence config → safe closing state → certify +next config); 2-full-node deployments get failover via a state-light +reconfiguration participant (`f+1` steady / `2f+1` reconfig); the +partition-authority ceiling becomes operation-sensitive on the frozen lattice; +key custody is a separate Shamir threshold. + +- **4a** ADR + TLA+/Lean model of the wedge/closing-state correctness + (the exit gate before it is normative). +- **4b** Implementation as a P2 evolution / P6 profile. +- **Reference:** (Byzantine) Vertical Paxos — Abraham & Malkhi (IBM Zurich + DCCL); VP orig. Lamport-Malkhi-Zhou, PODC 2009. + +## Cross-cutting tracks + +- **Proof CI (Tier-3 gate).** No Rust kernel merges unless its Aeneas + refinement proof passes; mirrored in the pre-push hook (HOOK/PIPELINE + PARITY). TLA+/TLC and Tamarin runs wired into CI as they land. +- **Spec ↔ impl parity.** Every wire change updates the spec, the vectors, + and the ADR in one PR. +- **The `#231` rename** (`passkey`→`attest`→now `Assurance`) rides Phase 1. +- **L1+L4 unification** (five laws → four) — attempt during 1c if the Lean + formulation collapses them. + +## Milestone summary + +| Milestone | Gate | +|---|---| +| **M0** scaffold | ADRs + both formal models in `formal/` | +| **M1** waist proven | Rust waist refines Lean + passes TLA+ invariants + vectors published | +| **M2** ceremonies | end-to-end flow + Tier-2 protocol proofs | +| **M3** libraries | 4 languages agree on the conformance vectors | +| **M4** BVP store | wedge model proven, reconfiguration shipped | + +The prose is done arguing with itself. From M1 on, the adversary is a proof +checker and a conformance vector — exactly as intended. diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 0000000..d1085b4 --- /dev/null +++ b/formal/README.md @@ -0,0 +1,50 @@ +# formal/ — mechanized models of the Ceremony Suite + +Tier-3 (algebra + state machine) formal artifacts for `docs/spec/`. These are +the "solid and defensible" backbone: the spec's laws are not just prose, they +type-check / model-check. + +## `lean/Authority.lean` — the authority algebra (P0 §2.0, laws L1/L4) + +Mathlib-free Lean 4. The authority type `Effect × Assurance × Scope` is finite, +so axis laws are `decide`-checked and the product laws follow componentwise. + +```sh +lean formal/lean/Authority.lean # type-checks in seconds; exit 0 = proved +``` + +Proves (25 theorems, **0 `sorry`**): +- axis + product meet laws (commutative, associative, idempotent); +- **attenuation** `a ⊓ c ≤ a` and `≤ c` — authority never amplifies (L4 / PO-4); +- `attenuate_compose` — sequential ceilings collapse to one meet (order of + independent ceilings is irrelevant); +- **no fail-open** `resolve [] = NeedsDecision`, never ⊤/approve (OB-9/OB-12); +- **order-independence** `resolve (x::y::xs) = resolve (y::x::xs)` — the + generating step of any permutation (L1 / PO-1). + +The Aeneas track (Phase 1c) extracts the Rust `resolve` kernel with Charon and +proves it *refines* this model — so the implementation inherits these theorems. + +## `tla/CeremonyStore.tla` — the store state machine (P2, PO-2*) + +TLA+ model of the CAS append + the anti-rollback trusted-state machine: +concurrent candidates and CAS-losers are benign; the externally-protected +checkpoint is monotone; no rollback past it; equivocation is two *committed* +records at one `(store,thread,sequence)`. Check with TLC: + +```sh +# tlc CeremonyStore.tla (TLA+ Toolbox / tla2tools.jar; add a model with small bounds) +``` + +Maps invariants to PO-2 / PO-2a / PO-2c and OB-15 / OB-16. + +## Why two tools + +The **algebra** (a pure function over a lattice) is Lean+Aeneas territory — +it refines to Rust. The **protocol/state machine** (concurrency, an attacker +transition, temporal invariants) is TLA+ territory. Confusing the two is the +"prose becomes authority-bearing protocol" failure the reviews punished; the +proof tiers keep them apart (see `docs/spec/README.md` → "The teeth"). + +Enrollment ceremonies (P3) get **Tier-2** symbolic proofs (Tamarin/ProVerif) +in Phase 2 — a third tool for a third kind of claim. diff --git a/formal/lean/Authority.lean b/formal/lean/Authority.lean new file mode 100644 index 0000000..bdd72c4 --- /dev/null +++ b/formal/lean/Authority.lean @@ -0,0 +1,126 @@ +/- + Ceremony Suite — Authority algebra (mechanized core of P0 §2.0 + laws L1/L4) + + Mathlib-FREE on purpose: each axis is a tiny finite chain, so the axis meet + laws are `decide`-checked and the product laws follow componentwise. The + file type-checks in seconds with `lean Authority.lean` — no Mathlib build. + + Proved (Tier-3, the algebra half of the v0.3.1 freeze): + • each axis is a chain with a genuine meet (comm / assoc / idem); + • Authority = Effect × Assurance × Scope; meet is componentwise; + • attenuation: `a ⊓ c ≤ a` and `≤ c` (L4 / PO-4 — never amplifies); + • resolution is order-independent under adjacent transposition — the + generating step of any permutation (L1 / PO-1); + • no fail-open: `resolve [] = NeedsDecision`, never ⊤/approve (OB-9/OB-12). + + The append/rollback state machine (P2, PO-2*) is modeled separately in TLA+. +-/ +namespace Ceremony + +/-! ### Axes — finite chains; `deny/none/once` is ⊥ -/ +inductive Effect | deny | allow deriving DecidableEq, Repr +inductive Assurance | none | presence | hardware deriving DecidableEq, Repr +inductive Scope | once | session | durable deriving DecidableEq, Repr + +def Effect.rank : Effect → Nat | .deny => 0 | .allow => 1 +def Assurance.rank : Assurance → Nat | .none => 0 | .presence => 1 | .hardware => 2 +def Scope.rank : Scope → Nat | .once => 0 | .session => 1 | .durable => 2 + +def Effect.meet (a b : Effect) : Effect := if a.rank ≤ b.rank then a else b +def Assurance.meet (a b : Assurance) : Assurance := if a.rank ≤ b.rank then a else b +def Scope.meet (a b : Scope) : Scope := if a.rank ≤ b.rank then a else b + +/-- axis laws — concrete after `cases`, closed by `decide`. -/ +theorem Effect.meet_comm (a b : Effect) : a.meet b = b.meet a := by cases a <;> cases b <;> decide +theorem Effect.meet_assoc (a b c : Effect) : (a.meet b).meet c = a.meet (b.meet c) := by + cases a <;> cases b <;> cases c <;> decide +theorem Effect.meet_idem (a : Effect) : a.meet a = a := by cases a <;> decide +theorem Effect.absorbL (a b : Effect) : (a.meet b).meet a = a.meet b := by cases a <;> cases b <;> decide +theorem Effect.absorbR (a b : Effect) : (a.meet b).meet b = a.meet b := by cases a <;> cases b <;> decide + +theorem Assurance.meet_comm (a b : Assurance) : a.meet b = b.meet a := by cases a <;> cases b <;> decide +theorem Assurance.meet_assoc (a b c : Assurance) : (a.meet b).meet c = a.meet (b.meet c) := by + cases a <;> cases b <;> cases c <;> decide +theorem Assurance.meet_idem (a : Assurance) : a.meet a = a := by cases a <;> decide +theorem Assurance.absorbL (a b : Assurance) : (a.meet b).meet a = a.meet b := by cases a <;> cases b <;> decide +theorem Assurance.absorbR (a b : Assurance) : (a.meet b).meet b = a.meet b := by cases a <;> cases b <;> decide + +theorem Scope.meet_comm (a b : Scope) : a.meet b = b.meet a := by cases a <;> cases b <;> decide +theorem Scope.meet_assoc (a b c : Scope) : (a.meet b).meet c = a.meet (b.meet c) := by + cases a <;> cases b <;> cases c <;> decide +theorem Scope.meet_idem (a : Scope) : a.meet a = a := by cases a <;> decide +theorem Scope.absorbL (a b : Scope) : (a.meet b).meet a = a.meet b := by cases a <;> cases b <;> decide +theorem Scope.absorbR (a b : Scope) : (a.meet b).meet b = a.meet b := by cases a <;> cases b <;> decide + +/-! ### Authority = the product lattice -/ +structure Authority where + effect : Effect + assurance : Assurance + scope : Scope +deriving DecidableEq, Repr + +/-- ⊥ = (deny, none, once): the single denied authority. -/ +def Authority.bot : Authority := ⟨.deny, .none, .once⟩ + +def Authority.meet (a b : Authority) : Authority := + ⟨a.effect.meet b.effect, a.assurance.meet b.assurance, a.scope.meet b.scope⟩ +infixl:70 " ⊓ " => Authority.meet + +/-- the meet-induced order: `a ≤ b ↔ a ⊓ b = a`. -/ +def Authority.le (a b : Authority) : Prop := a ⊓ b = a +infix:50 " ≤ᴬ " => Authority.le + +/-! ### Product meet laws — componentwise from the axis laws -/ +theorem meet_comm (a b : Authority) : a ⊓ b = b ⊓ a := by + obtain ⟨ae, aa, asc⟩ := a; obtain ⟨be, ba, bsc⟩ := b + simp only [Authority.meet, Effect.meet_comm ae be, Assurance.meet_comm aa ba, Scope.meet_comm asc bsc] + +theorem meet_assoc (a b c : Authority) : (a ⊓ b) ⊓ c = a ⊓ (b ⊓ c) := by + obtain ⟨ae, aa, asc⟩ := a; obtain ⟨be, ba, bsc⟩ := b; obtain ⟨ce, ca, csc⟩ := c + simp only [Authority.meet, Effect.meet_assoc, Assurance.meet_assoc, Scope.meet_assoc] + +theorem meet_idem (a : Authority) : a ⊓ a = a := by + obtain ⟨ae, aa, asc⟩ := a + simp only [Authority.meet, Effect.meet_idem, Assurance.meet_idem, Scope.meet_idem] + +/-! ### Attenuation (L4 / PO-4): meet is contractive on both inputs — never amplifies -/ +theorem meet_le_left (a c : Authority) : (a ⊓ c) ≤ᴬ a := by + obtain ⟨ae, aa, asc⟩ := a; obtain ⟨ce, ca, csc⟩ := c + simp only [Authority.le, Authority.meet, Effect.absorbL, Assurance.absorbL, Scope.absorbL] + +theorem meet_le_right (a c : Authority) : (a ⊓ c) ≤ᴬ c := by + obtain ⟨ae, aa, asc⟩ := a; obtain ⟨ce, ca, csc⟩ := c + simp only [Authority.le, Authority.meet, Effect.absorbR, Assurance.absorbR, Scope.absorbR] + +/-- passing authority `a` through a ceiling `c` never exceeds either (L4). -/ +def attenuate (a c : Authority) : Authority := a ⊓ c +theorem attenuate_le_input (a c : Authority) : attenuate a c ≤ᴬ a := meet_le_left a c +theorem attenuate_le_ceiling (a c : Authority) : attenuate a c ≤ᴬ c := meet_le_right a c +/-- sequential ceilings collapse to one meet — order of independent ceilings is irrelevant. -/ +theorem attenuate_compose (a c d : Authority) : attenuate (attenuate a c) d = attenuate a (c ⊓ d) := + meet_assoc a c d + +/-! ### Resolution (L1) — `ask` is NOT an authority level -/ +inductive Resolution + | NeedsDecision -- was `ask`: control flow; headless ↦ deny + | Decided (a : Authority) +deriving DecidableEq, Repr + +/-- resolve matching rules by meet; empty match ⇒ NeedsDecision (NOT ⊤/approve; + the no-fail-open clause, OB-9/OB-12). -/ +def resolve : List Authority → Resolution + | [] => .NeedsDecision + | x :: xs => .Decided (xs.foldl Authority.meet x) + +/-- **No fail-open.** An unmatched request never resolves to authority. -/ +theorem resolve_empty : resolve [] = Resolution.NeedsDecision := rfl + +/-- **Order-independence, generating step (PO-1).** Swapping two adjacent + matched rules leaves the resolved authority unchanged; a full permutation is + a composition of adjacent swaps, so resolution is independent of rule / file + / load order. -/ +theorem resolve_swap (x y : Authority) (xs : List Authority) : + resolve (x :: y :: xs) = resolve (y :: x :: xs) := by + simp only [resolve, List.foldl, meet_comm x y] + +end Ceremony diff --git a/formal/tla/CeremonyStore.tla b/formal/tla/CeremonyStore.tla new file mode 100644 index 0000000..5f19d5c --- /dev/null +++ b/formal/tla/CeremonyStore.tla @@ -0,0 +1,99 @@ +---------------------------- MODULE CeremonyStore ---------------------------- +(* + Ceremony Suite — the chain-store append + anti-rollback state machine (P2). + Tier-3 (state-machine) companion to formal/lean/Authority.lean. + + Models ONE authority thread (store_id, thread_id fixed) as: + - a committed spine: seq |-> record-id (a function), monotone in length; + - a compare-and-swap append (OB-15, FROZEN): a proposer names the head it + read; it commits ONLY if the head is unchanged, else it retries (benign); + - an externally-protected checkpoint (P2 §4): the highest committed length + a verifier has anchored OUTSIDE the store; it never regresses; + - an untrusted step: an attacker with disk/network but no keys — it may + propose candidates but MUST NOT rewrite committed history or move the + checkpoint. + + Invariants map to the spec: + SpineFunctional -> OB-15 : one committed record per sequence (a fork is + two DIFFERENT committed ids at one seq). + NoRollback -> PO-2c : head length >= protected checkpoint always. + CheckpointMono -> PO-2/2a : the protected checkpoint only advances. + CASLoserBenign -> OB-15 : a lost CAS changes nothing (concurrent + proposals are not equivocation). +*) +EXTENDS Naturals, FiniteSets + +CONSTANTS RecordIds \* a finite pool of candidate record ids +ASSUME RecordIds # {} + +VARIABLES + spine, \* [1..len -> RecordIds] : the committed authority spine + len, \* Nat : committed length (the head is spine[len], seq = len) + checkpoint \* Nat : externally-protected highest-accepted length + +vars == << spine, len, checkpoint >> + +TypeOK == + /\ len \in Nat + /\ checkpoint \in Nat + /\ spine \in [ (1..len) -> RecordIds ] + +Init == + /\ len = 0 + /\ checkpoint = 0 + /\ spine = << >> \* empty function on 1..0 + +\* A proposer read `expected` as the head length and proposes record `r` as the +\* next. CAS: commit iff the head is still `expected` (= len). Otherwise the +\* proposer LOST the race and simply retries — no state change (benign). +Append(expected, r) == + /\ r \in RecordIds + /\ expected = len \* CAS success condition + /\ len' = len + 1 + /\ spine' = [ i \in 1..(len+1) |-> IF i = len+1 THEN r ELSE spine[i] ] + /\ UNCHANGED checkpoint + +\* A verifier anchors a fresher head: the checkpoint may only advance to the +\* current committed length, never backward. +AdvanceCheckpoint == + /\ checkpoint < len + /\ checkpoint' = len + /\ UNCHANGED << spine, len >> + +\* An attacker with disk/network but no keys. It cannot forge a committed +\* record (no signing key) and cannot move the protected checkpoint. The only +\* thing it can do to the *authority* state is nothing safety-relevant: we model +\* it as a no-op (candidate records live off the committed spine). +UntrustedStep == UNCHANGED vars + +Next == (\E e \in Nat, r \in RecordIds : Append(e, r)) + \/ AdvanceCheckpoint + \/ UntrustedStep + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------ +\* Invariants + +\* OB-15: the spine is a function — at most one committed record per sequence. +SpineFunctional == spine \in [ (1..len) -> RecordIds ] + +\* PO-2c: the committed head never rolls back below the protected checkpoint. +NoRollback == len >= checkpoint + +Inv == TypeOK /\ SpineFunctional /\ NoRollback + +THEOREM Spec => []Inv + +------------------------------------------------------------------------------ +\* Action properties (checked with a state constraint like len =< 4) + +\* PO-2/2a: the protected checkpoint is monotone across every step. +CheckpointMono == [][ checkpoint' >= checkpoint ]_vars + +\* OB-15: committed length is monotone — no committed record is ever removed +\* (a CAS-loser changes nothing; only successful CAS extends the spine). +LenMono == [][ len' >= len ]_vars + +THEOREM Spec => (CheckpointMono /\ LenMono) +=============================================================================