docs(spec): the Ceremony Contract v0.1 draft — five laws, wire objects, chained store

[hartsock]

What this PR does

Adds docs/spec/ceremony-contract.md — the keystone specification for the
decision-surface seam (#225): the contract between agent-* libraries
(decision semantics) and harnesses (rendering). Now at DRAFT v0.1.4
(revised across three review rounds; see the thread).

• Wire objects (one schema; JSON interchange / TOML at rest / canonical
  DAG-CBOR for anything hashed or signed): PermissionRequest,
  DecisionMatrix, Decision, Introduction (with proof-of-possession),
  chained PinRecord/GrantRecord, AuditRecord, RevocationRecord, and
  the DecisionSurface seam. Every object is a Memo-descendant (WF-2:
  content-CID unconditional, sig at trust boundaries, Sealed at load).
• Five normative laws, each with a proof obligation mapped to the
  Lean/Aeneas formal track: L1 meet-resolution, L2 tamper-boundedness
  (widening AND load-bearing-identity narrowing; quorum revocation),
  L3 fail-closed totality, L4 attenuation, L5 the ceremony gate
  (self-certifying multihash identity; re-key ⇒ re-ceremony).
• Mechanism below the law line: the chain-store (content-addressable
  crate), signed loosening verdicts (policy: signed approve entries — tamper-resistance for the loosening verdict (newt#1207) #226/policy: signed approve entries — tamper-resistance for the loosening verdict (#226) #227), presence-attested pins
  (PR docs(design): LLM flight recorder + WebAuthn presence + mesh discharge plan #214 lineage), SAS enrollment, external anchors, and a MITM ledger.
• Identity model: every participant is a fingerprint; roles
  (principal/agent/surface/gate); delegation = chain-to-pinned-principal.
• Profile v1 (§8): algorithms are pins, not laws — multihash/multicodec
  identifiers, "BLAKE3 is an implementation detail."
• Governance: law minimalism — six laws became five (L6 → WF-1); every
  subsequent review round added mechanism/wire-objects at zero law cost.

Test plan

• Docs-only; just check passes via the pre-push hook each revision.
• The spec's own executable gates (conformance vectors, kernel proofs
  PO-1/PO-2/PO-2b) are staged as explicit follow-up (§6), not claimed here.

Review status

Under active adversarial review (rounds 1–3 by the author; a round-3
security review by GPT-5/Codex is being adjudicated). Not yet ready to
merge — see the open security-contract findings in the thread. Merge and
implementation are on hold pending resolution; spec revisions continue.

Out of scope

• The decision-kernel carve in agent-bridle-core (separate code PR).
• Aeneas/Charon toolchain bootstrap and the pilot proofs.
• Conformance vectors and client-lib scaffolds (Rust/Python/Dart/TS).
• The passkey → attest rename (rename: Verdict::Passkey → Attest — coordinated pre-1.0 vocabulary pass #231).

Refs #225, #220, #226, #231. Companions: agent-mesh#65, #66, newt-agent#1209.

[hartsock]

Some modifications needed and we need to think harder before committing to a path here.

[hartsock]

v0.1.1 pushed (efcc7ca) — every review thread landed, law count went DOWN.

Review thread	Disposition
Missed verb	Surfaced as attest in the matrix verbs — it was the passkey verdict all along; zero new laws. attest × once = ceremony every time; attest × session = one discharge per generation (your User-Verification affordance). Rename tracked in #231 (verdict + passkey.toml → attest.toml, read-both migration; "passkey" stays correct for the hardware mechanism only).
Admin opinion / parental controls	§3.2: default documented as the administrator/packager opinion surface (rm -rf → ["deny","session"]); negative pins = signed durable denies with provenance in the chain-store, transportable over mesh/config. Mechanism, not law.
Merkle-ized JSONL + where's the sig	§5.1 formalized: content-CID (signed, sig-trimmed canonical form — your plan 1) vs line-CID (full line incl. sig — your plan 2, adopted: parents now reference line-CIDs, so sig-stripping breaks the chain; strictly stronger than the draft). JSONL = lossless at-rest view of canonical DAG-CBOR.
The entropy identity	Stated as assumption 1 of §5.1: `H(sig
Audit ceremony	New §3.6 AuditRecord: witness signs the chain head (line-CID) with presence discharge — literal finger on hardware — appended to the same chain. L5 composed with the log; one record type, zero laws.
Cut a law	Done: L6 → WF-1 (well-formedness predicate on the wire object, §3.2 + conformance table). Five laws. Governance §7 records the executed cut; L1+L4 merge is the next candidate (five → four).
Bonus honesty	Your negative-pins thread exposed that L2 overclaimed: flat files can't detect deletion of a restrictive entry (widening). L2 restated; the chain-store is now load-bearing for the law, not an optimization.

Term of art recorded: chain-store (§1 Terms).

[hartsock]

v0.1.2 pushed (5ad88f9) — the identity model, from the delegation/fleet/mobile discussion. §2.1 roles table (principal/agent/surface/gate — monolith newt = one fingerprint, all roles; no-compute mobile = keypair + renderer); L5's pinned predicate completed transitively (chain-to-pinned-principal, PoP at every link — already shipped as mesh CertChain #39/#40; root involved at issuance NOT per-delegation, so headless fleets verify offline); §5.4 SAS enrollment (commit-then-reveal, transcript-bound, human-compares — the naive phrase-echo is MITM-relayable; paranoia = (entropy × rounds, witnesses, presence), minima by caveat ceiling); §5.5 external anchors — GitHub keys corroborate a self-sovereign root, never ARE it (floating-identity law 1; no-GitHub users lose nothing). Remote surfaces sign their Decisions. Zero new laws — still five. Protocol work filed as agent-mesh#66.

[hartsock]

v0.1.3 pushed (7f77cda) — quorum revocation + the no-MITM-hole-anywhere sweep.

• L2 → Tamper-boundedness, two directions in one law: sub-quorum actors can neither widen authority nor shrink load-bearing identity structure. Your DoS observation absorbed as L2's upward half (zero count change; PO-2b). Reversible narrowing stays cheap; punting a pinned identity requires k-of-n quorum — 'reset mesh' is not an attack surface. Punting ≥ pinning: revocation strength floors at enrollment strength.
• RevocationRecord (§3.6): quorum signers; the quorum policy itself is a principal-signed loosening entry; last-root revocation refused without succession or an explicit tombstone.
• Anchors bless-then-participate (§5.5): AnchorRecord = principal-signed binding; ANY public-key display surface qualifies once blessed (GitHub participates, nothing depends on it); captured anchors cut loose by the same quorum path — corroboration is k-of-n and n just shrank.
• §5.6 MITM ledger — nine channels enumerated (first contact, enrollment, post-pin transport, delegation, remote surface, sync-forgery, sync-rollback, anchors, the human), each with attack/closure/residual. Two holes this sweep found and closed: key-substitution (SAS transcript now MUST cover the long-term keys being enrolled, not just session material) and render-swap (Decision carries the request's content-CID under signature — what the human saw is bound to what was granted; gate matches CIDs). Rollback closed by monotonic heads + AuditRecords as witnessed freshness checkpoints.

The ledger's unifying row-pattern is the doctrine itself: the authenticated thing is always the key, never the channel.

[hartsock]

Queued v0.1.4 (NOT pushed — pause holds until Thursday per Shawn)

From the sig-everywhere / Memo-as-base discussion:

The Memo discipline (§3 preamble, WF-2): every wire object is a Memo-descendant with capabilities attached by mechanical criteria — CID unconditional (all serializable data), sig at trust boundaries (remote MUST, in-process MAY omit), parents for durability (chain-store), Sealed-at-load (parse-don't-validate: nothing enters the kernel unverified; the Rust heir of Memo's __getitem__ tamper check, verified once at construction, immutable after). ALL of the data layer, NONE of the resource layer — the same line Aeneas forces (kernel = values, shell = resources).

Two sig gaps found by applying it:

1. Introduction gains a proof-of-possession sig by the introduced key over transcript-bound freshness — closes unknown-key-share / introduction replay (parity with mesh feat(shell): file redirections, increment 3 (#34) #40 PoP-to-certify). MITM-ledger row.
2. Remote PermissionRequest gains a gate sig; surfaces verify chain-to-pinned-principal before rendering — closes the phishing-canvas (fake prompts training the human). MITM-ledger row.

Lineage note for §1 Terms: Memo (content-addressable-python data.py) contributes verification-at-access; MerkleNode added chaining+sigs; Sealed<T> completes the trinity. Law count unchanged: five.

Thursday build menu (on green light): #[derive(ContentAddressable)] proc-macro + Sealed<T> in the content-addressable crate → kernel carve in bridle-core → opam/Aeneas leg → PO-1/PO-2/PO-2b.

[hartsock]

Queued v0.1.4 addendum — multihash directive (Shawn): "BLAKE3 is an implementation DETAIL, not a law." L5's formula de-blake3s to fingerprint = H(pubkey) where H is multihash-named and the law states H's required properties (collision resistance; self-certification = computationally hard to find a key matching a name). Terms + §2.1/§3.4 self-cert checks rephrase over multihash bytes (opaque comparison, code included). New profile appendix: v1 pins blake3-256 (0x1e), Ed25519 (deterministic — §5.1 assumption 1 already demands this property), dag-cbor (0x71), CIDv1. Hash migration = re-NAMING ceremony (key signs its new name; identity never moves — the key is the identity, the fingerprint is its self-describing name). §5.1's assumptions were already property-shaped; L5 now matches. Wire-format code change (mesh Fingerprint → multihash) is a Thursday item, detailed on agent-mesh#66.

[hartsock]

v0.1.4 pushed (b746039) — the queued manifest, now ink: Memo discipline as WF-2 (CID unconditional · sig at trust boundaries · parents for durability · Sealed at load — Memo's read-time tamper check reborn as parse-don't-validate); PoP Introductions (fresh + sig by the introduced key — unknown-key-share closed); gate-signed remote requests (phishing-canvas closed; surface verifies chain before rendering); multihash everywhere — L5 now reads fingerprint = H(pubkey) with required properties, and the new §8 Profile v1 pins blake3-256/Ed25519/dag-cbor/CIDv1 each annotated with the property a replacement must preserve (Ed25519's determinism is load-bearing, §5.1). Hash rotation = re-naming ceremony; sig rotation = re-keying. Two new MITM-ledger rows. Laws: five, unchanged through three review rounds. Spec is 700 lines, review-ready. Hold on merge/implement respected — mesh#66 carries the Fingerprint wire-format code change for Thursday.

[hartsock]

Adversarial review - security contract gaps

The current head is mergeable and CI is green, but this specification makes several security claims that its wire contract does not yet enforce.

Blocking findings

1. [P1] The chain-store does not discharge rollback. Parent links detect interior deletion only when the verifier already possesses a trusted head. A disk attacker can truncate a restrictive suffix and its head pointer, or present an older valid fork; the surviving prefix still verifies. An AuditRecord stored in that same chain rolls back with it. H1/PO-2a therefore remains unproven as written. Require an independently protected monotonic head or mandatory external witness/quorum checkpoint, plus explicit fork handling.

2. [P1] Approval is not bound to the executable effect. PermissionRequest.action contains only class and a free-form display; Decision.request binds that presentation object, not canonical tool arguments and resolved resources. A stale or lossy mapping can approve X and execute Y while the CID matches. Carry the existing canonical CallRequest content ID in the request and require the gate to recompute it before minting authority.

3. [P1] The gate never validates that a grant belongs to the issued matrix. Acceptance only requires a matching request CID. Nothing requires the verb to appear in matrix.verbs, the scope to appear in matrix.scopes, or the result to remain below the request ceiling. A buggy or compromised surface can answer a once/session request with allow/always, violating L4. Make matrix-membership and ceiling validation a gate-side MUST.

4. [P1] attest has no attestation on the wire. The decision is a bare {verb:attest} with only a comment saying + presence discharge. There is no challenge, nonce, generation, authenticator proof, or normative verification step. Reuse the existing domain-separated, single-use Challenge/DischargeAttempt contract and require successful gate verification before an attest grant is effective.

5. [P1] Introduction.fresh does not itself provide freshness. A nonce included in a self-signed object can be replayed byte-for-byte unless the recipient issued it and records its consumption. Define the challenge issuer, transcript and identity bindings, and replay-state/generation rules before claiming replay and unknown-key-share closure.

6. [P1] The quorum signature format is circular. RevocationRecord.signers[].sig lives inside the record, while the generic signing formula removes only a top-level sig. Signers must therefore sign different progressively modified records or a final record already containing their own signatures. Define a canonical unsigned revocation payload that every signer signs; sort and deduplicate signer identities; keep the chain append signature separate.

Additional findings

7. [P2] Ignoring unknown fields conflicts with signed canonical objects. Typed deserialization normally discards unknown fields, so reserialization cannot reproduce the signed CID. Preserving them avoids that failure but permits version-dependent authority semantics. Define explicit version dispatch and canonical unknown-field preservation, or reject unknown authority-bearing fields fail-closed. Also require exactly one of grant and escalate.

8. [P2] Multihash agility needs a trusted allowlist. Introduction verification dispatches on the fingerprint's own hash code. An attacker therefore chooses the algorithm unless the verifier first checks it against a locally trusted profile. Require profile membership and define profile-rotation negotiation before dispatch.

9. [P2] The PR body is stale. It still describes v0.1.0 and six laws, while the head is v0.1.4 with five laws, quorum revocation, anchors, and Memo semantics. Update it before the next review pass.

Verdict

Not ready to merge. The algebraic direction is strong, but these gaps sit exactly where prose becomes authority-bearing protocol. The chain needs an external anti-rollback anchor; decisions need effect, matrix, and discharge validation; and every signed object needs one unambiguous canonical payload.

(Reviewed by OpenAI GPT-5, running in the Codex desktop harness on Windows.)

[hartsock]

Adjudication of the two security reviews (v0.1.5 + v0.1.6)

Both adversarial reviews were substantially correct. A verified deep-research pass (19 confirmed claims, 3-0 votes) adjudicated round 4 against the canon — zero findings refuted, the rollback finding overwhelmingly confirmed across RFC 6962 (CT gossip/STH), TUF (monotonic version), Schneier-Kelsey (external commitment), and FssAgg (eprint 2008/185).

Round 4 (GPT-5/Codex) — 8 true positives, all closed in v0.1.5

#	Finding	Fix	Cite
1	chain ⇏ rollback resistance	§5.7 external anti-rollback anchor (monotonic head + witness cosign + fork=proof); L2·H1 honestly split chain(interior)+anchor(tail/fork); in-chain audit no longer claimed as checkpoint	RFC 6962; Schneier-Kelsey; FssAgg; TUF
2	approve-X/execute-Y	action.effect = canonical resolved-call CID; gate recomputes before minting	Landrock-Pedersen (WYSIWYS)
3	grant∉matrix	§3.3 gate acceptance MUST-checklist (request-CID, matrix membership, ceiling, effect, discharge)	never-trust-client
4	attest had no attestation	§3.3.1 wires shipped Challenge/DischargeVerifier; grant inert until verified	WebAuthn/FIDO2
5	fresh wasn't fresh	Introduction → 2-message challenge-response; recipient issues+consumes	station-to-station
6	circular quorum sig	one canonical unsigned payload; signers sorted+deduped; chain sig separate	detached multisig
7	unknown-fields vs canonical	verify over received bytes; version dispatch; unknown authority-bearing fields fail closed	RFC 8785 / JWS
8	multihash downgrade	allowlist-before-dispatch (§3.4, §8)	alg:none / algorithm-confusion
9	stale PR body	fixed	—

Round 5 (second LLM) — confirmed all of the above independently; 5 refinements applied in v0.1.6

deterministic-signature prose over entropy notation (§5.1) · human SAS comparison is measurable-error, not "unspoofable" (§5.4) · rendering-faithfulness residual named + deterministic display-from-effect (§3.1) · break-glass/succession made a required subsystem (§3.6) · anti-rollback head location made explicit in conformance (§6.3).

The through-line

Both reviews found the same shape: claims true only because unstated mechanisms did the real work. The fix was always to name and bind the mechanism, never to add a law. Law count held at five across two adversarial reviews — L2 was corrected (its H1 was over-claimed), not multiplied. This is the argument FOR the Lean/Aeneas track, made by adversaries: "prose becomes authority-bearing protocol" is exactly the failure a proof assistant refuses to compile.

Two forks left to the author (recorded in §7, not agent-decided)

1. attest factorization — effect × assurance × scope (3 axes, cleaner) vs one verb axis (minimal). L1 survives either way (product of lattices is a lattice).
2. Partition into profiles — the doc has become a security constitution (~900 lines). Recommended split (Ceremony Contract + Signed-Object + Chain-Store + Enrollment + Identity-Lifecycle + Rendering profiles), five laws as the narrow waist. This is the loosely-coupled/functionally-cohesive doctrine applied to the spec itself.

Merge + implementation remain on hold; revisions continue. Thanks to both reviewers — this is heterogeneous-adversary review working exactly as intended.

[hartsock]

Partitioned into the Ceremony Suite (author-approved)

The monolith is now a dependency-ordered suite under docs/spec/ — the loosely-coupled/functionally-cohesive doctrine applied to the spec itself, and the synthesis of review-5's partition with #232's formal kernel.

The dependency DAG (each node is a decision: Proposed → Accepted → Proven; a downstream decision can't be Accepted until its deps are Proven):

P1 Signed-Object → P2 Chain-Store → P0 Ceremony Contract (WAIST: 5 laws)
                                     → P3 Enrollment · P4 Identity-Lifecycle · P5 Rendering

Three tiers of teeth, deliberately not confused:

• Tier 3 (Lean+Aeneas) — the algebra + trusted state machine (P0/P1/P2/P4): kernel refines model, CI gate blocks any Rust kernel whose refinement proof fails.
• Tier 2 (Tamarin/ProVerif) — the ceremonies (P3, part of P5): a lattice can be flawless behind a leaky handshake, so MITM/replay/unknown-key-share get symbolic proof, not algebraic.
• Tier 1 (assumed) — Ed25519/BLAKE3 primitives, cited not proven.
• Cross-cutting: shared conformance vectors bind the four client languages to one behaviour.

On #232: your formal kernel is exactly the P0+P1+P2 provable MVP — I've adopted it as such in the suite index and mapped its pieces: the product lattice → P0 §4 (this also resolves the attest-factorization fork toward product-of-lattices, still an L1 meet); the trusted state machine / untrusted_step_safe / checkpoint-Extends monotonicity → P2 §5; effect binding → P5; single-use challenge → P0 §3 + P3. Two refinements your design and the suite should reconcile: (1) the rollback theorems need the checkpoint to live in P2's external anchor (outside the store), which your §9 already gestures at — the suite makes it normative and names where; (2) the enrollment handshake is Tier-2 (protocol), not Tier-3 (algebra) — Aeneas proves the kernel refines the model, but PoP/SAS freshness wants Tamarin. Suggest #232's Lean/Rust/Aeneas commits target P0+P1+P2 first (the waist), and we open a separate protocol-verification track for P3.

Build order: P1 → P2 → P0 → {P3,P4,P5}. Still five laws; the PO ledger just relocated to the owning profiles. Merge/implement remain on hold; this is the design restructure.

[hartsock]

v0.3.0 repair cut — all 11 review-6 obligations closed in text (65bc1ec)

Not tracking this time — actual repairs across the suite. The review's own recommendation ("approve the split, request-changes on the four blockers, list the rest") is now: four blockers + the OB-9 soundness bug closed, high/medium closed, one author's-call adopted.

OB	Fix
OB-1 dependency cycle	dependency inversion — P0 defines abstract AttestEvidence + ValidAssociationProof; P4 implements. DAG now truly acyclic: P1→P2→P0→P4→P3, P5 on {P0,P1,P4}.
OB-2 DAG vs scalar head	linear authority spine per causal thread (store_id, thread_id, sequence) — conversation branches, authority is a railway; equivocation = two records at one (store,thread,sequence). (Frontier alt rejected as harder to prove. Adopted pending your veto.)
OB-3 attestation txn	one canonical challenge preimage; CAS commit (verify-checkpoint→presence→construct→append→advance-anchor→mint); four roles — the WebAuthn authenticator is not the DAG verifier.
OB-4 byte carriage	signed-bytes-in-envelope {profile,codec,body,cid,by,sig}; JSON/TOML are views.
OB-9 fail-open	resolve(∅,q)=ask (piecewise — a seed would downgrade legitimate approve, so I used an explicit no-match clause); vocabulary glossary.
OB-5/6/7/8/10/11	consume-last challenge · universal domain separation + normative store_id · epoch-bound revocation policy · conditional PO-R + veto-suppression threat · per-class sealed resource identities (container digest not tag) · suite.toml manifest.

On OB-9 specifically: the reviewer suggested seeding the meet with ask, but seeding ⨅({ask} ∪ matching) would pull a legitimate approve match down to ask (ask ⊏ approve). The correct fix is a piecewise definition — empty match → ask, non-empty → ⨅(matching) — which is total, fail-closed, and doesn't clobber grants. Flagging the deviation.

Plus (author direction, not from the review): P5 surface attestation — binary attestation (blessed code measurement = what the surface is) + a witness-token rendering ceremony (what it did) to shrink the faithfulness residual, honestly kept as shrunk-not-eliminated.

Still five laws. The proofs that discharge these are the implementation phase (held). Two decisions remain yours: confirm/veto the OB-2 linear spine, and the attest factorization.

[hartsock]

v0.3.1 PROTOCOL FREEZE — review-7's seven findings closed (60ff13e)

The protocol-freeze pass. Seven places two implementers would build incompatibly, now frozen to tolerances. Two author's-calls decided; conformance vectors are the one remaining implementation-phase item.

OB	Freeze
OB-12 type FROZEN	Authority = Effect × Assurance × Scope (componentwise meet); ask→NeedsDecision (control-flow, not an authority level); deny=⊥; explicit signed ceiling; scope = profile-declared closed order. Decides the attest factorization (4-way converged). Five laws hold — carrier change, lifts componentwise.
OB-13	ONE signed-object constructor; sig covers a canonical protected tuple (profile, codec, cid, signer, domain-sep), not bare cid.
OB-14	genesis STORE_ID_SELF sentinel breaks the store_id = CID(genesis) fixed point.
OB-15 CAS FROZEN	CAS on expected head; concurrent candidates + CAS-losers are NOT equivocation.
OB-16 law corrected	L2 upward is now equality over authority-generating structure, not ⊆ — a sub-quorum actor can't add a trusted issuer either (closes time-delayed privilege escalation).
OB-17	drop "punting ≥ pinning" scalar; revocation = P4's exact policy-CID predicate; P3 depends on P4.
OB-18	token → attention-aid; faithfulness = byte-compare vs a gate-produced canonical render; raw secrets forbidden in signed records.

Exit gate: every item ✅ except conformance vectors (positive+negative) — the one implementation-phase deliverable, tracked in suite.toml.

Store roadmap (adopted): CAS → Byzantine Vertical Paxos. The frozen CAS is the threshold-1 steady-state case of a vertically-reconfigurable store. Sequencing: prove the P1→P2→P0 waist on CAS first; then evolve P2 to separate lean steady-state from a stronger wedge-based reconfiguration (safe 2-node failover: f+1 steady / 2f+1 reconfig; operation-sensitive partition ceiling on the §2.0 lattice). Reference: (Byzantine) Vertical Paxos — Abraham & Malkhi, IBM Zurich DCCL; VP orig. Lamport-Malkhi-Zhou PODC 2009. Its wedge/closing-state correctness gets its own ADR + TLA+/Lean model; not part of this freeze.

Per the reviewer: "the last prose-heavy pass." Next is nonbinding spikes (kernel, Sealed, DAG-CBOR, Lean/TLA+ models) → then implementation in P1 → P2 → P0 order. Merge + implementation remain HELD for author sign-off.