formal: prove ceremony algebra and protocol safety kernel#232
Draft
hartsock wants to merge 3 commits into
Draft
Conversation
hartsock
added a commit
that referenced
this pull request
Jul 16, 2026
…uite The monolith (~1025 lines) becomes a dependency-ordered suite of loosely- coupled, functionally-cohesive profiles — the architecture doctrine applied to the spec itself, and the synthesis of review-5's partition + GPT-5 #232's formal kernel. - README.md — the suite index: dependency DAG, the three-tier proof-teeth stack (Tier 1 crypto axioms / Tier 2 protocol Tamarin-ProVerif / Tier 3 kernel Lean-Aeneas + cross-language conformance vectors), build order (P1→P2→P0→{P3,P4,P5}), and the relocated PO ledger. Each profile is a DECISION: Proposed → Accepted → Proven, and a downstream decision cannot be Accepted until its dependencies are Proven. - P0 ceremony-contract.md — slimmed to THE NARROW WAIST: five laws, the authority lattice, the DecisionSurface seam, gate acceptance, the MITM ledger (cross-cutting), governance. 242 lines. - P1 signed-object-profile.md — CID/canon/Sealed/deterministic-sig/ allowlist/Profile v1 (foundation). - P2 chain-store-profile.md — causal-transcript DAG, content/line CID, external anti-rollback anchor, the trusted-state-machine model. - P3 enrollment-protocol.md — Introduction, SAS, anchors; teeth are Tier-2 symbolic protocol analysis, NOT Lean (a key boundary the reviews implied). - P4 identity-lifecycle.md — roles/delegation, PinRecord/Audit/Attestation/ Revocation, break-glass + succession (required, PO-R liveness). - P5 rendering-security-profile.md — effect binding, gate-signed requests, and the honest human-factors residual. Still five laws; the PO ledger just relocated to the profiles that own each obligation. GPT-5 #232's kernel is adopted as the P0+P1+P2 provable MVP. Refs #229, #232, #225, agent-mesh#67. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hartsock
force-pushed
the
feat/formal-ceremony-kernel
branch
from
July 16, 2026 02:08
c4072ee to
5ceb85b
Compare
Define the product lattice, trusted protocol state, explicit crypto assumptions, and the Rust-to-Lean refinement gate for the stacked formal-verification work. Co-authored-by: OpenAI GPT-5 <codex@openai.com>
Split the proof work by the P1 to P2 to P0 dependency order, place rollback state in P2's external anchor, and move enrollment freshness to the Tier-2 protocol track. Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
Reconcile the formal kernel with PR #229 OB-4 and OB-6: exact envelope recomposition, universal signature domains, named crypto soundness, private verified constructors, and trusted-profile dispatch. Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
hartsock
force-pushed
the
feat/formal-ceremony-kernel
branch
from
July 16, 2026 03:42
5ceb85b to
f9593d0
Compare
hartsock
added a commit
that referenced
this pull request
Jul 16, 2026
…urface attestation
The next cut Shawn asked for: turn the tracked OB-1..OB-11 into actual spec
repairs across the suite. All four blockers + the OB-9 soundness bug closed
in text (proofs are the held implementation phase).
Blockers:
- OB-1 dependency inversion: P0 defines abstract AttestEvidence +
ValidAssociationProof; P4 implements. DAG is now truly acyclic
(P1→P2→P0→P4→P3; P5 on {P0,P1,P4}).
- OB-2 (author's-call, adopted): 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).
- OB-3 attestation transaction: one canonical challenge preimage; CAS commit
(verify-checkpoint→presence→construct→append→advance-anchor→mint); four
separate 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, never authority-bearing serializations.
- OB-9 fail-open: resolve(∅,q)=ask (piecewise — a seed would downgrade
legitimate approve); vocabulary glossary (allow=approve; ask is a verdict;
escalate is neither).
High/medium: OB-5 reserve→validate→consume-last; OB-6 universal
domain-separation + normative store_id; OB-7 epoch-bound revocation policy +
exact-predicate enrollment; OB-8 conditional PO-R liveness + veto-suppression
threat; OB-10 per-class sealed resource identities; OB-11 suite.toml manifest.
Plus, per Shawn: P5 gains SURFACE ATTESTATION — binary attestation (blessed
measurement, what the surface IS) + rendering attestation (witness-token
ceremony, what it DID) to shrink the faithfulness residual; honestly kept
as shrunk-not-eliminated.
Still five laws. Refs #229 review round 6, GPT-5 #232.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this PR does
9e7a245.Authored by OpenAI GPT-5 in the Codex desktop harness on Windows.
Test plan
git diff --check origin/docs/spec-ceremony-contract..HEADcargo fmt --all -- --check9e7a245.Toolandctxinagent-bridle-tool-shell/tests/unbridle.rs; the force update used the author's previously approved--no-verifyfallback only after that reproduction.Out of scope