formal(phase1): unify P0 authority + P1 signed-object Lean project + CI gate (integrates #233)#238
Merged
Merged
Conversation
…e Lean project + CI gate Phase 1 kickoff. Rather than rebuild, harvest the valuable P1 Lean work from PR #233 (GPT-5/Codex) and integrate the P0 authority algebra into it, giving one Lake project that builds P0 + P1 together. - formal/Ceremony/P0/Authority.lean — the P0 authority algebra (moved from formal/lean/; namespaced Ceremony.P0): product meet-lattice, attenuation (L4), no-fail-open (OB-9/OB-12), order-independence (L1). 25 theorems, 0 sorry. - formal/Ceremony/P1/SignedObject.lean, Gate.lean, Tests/ — harvested from PR #233: profile/algorithm allowlist, canonical-encoding injectivity, the universal SignaturePreimage binding profile/codec/domain/store/thread/body/ cid/signer (OB-13), + counterexample/contract tests + the formalGate proof-escape gate. - Lake project (lakefile, lean-toolchain v4.31, manifest) — lake build (9 jobs) plus lake exe formalGate, green; no mathlib, builds in seconds. - .github/workflows/formal.yml — Tier-3 CI gate (ubuntu+windows). - justfile check-formal (graceful skip if lake absent) + pre-push parity. - .gitignore: **/.lake/ build artifacts. - ROADMAP Phase 0 updated; only the opam leg remains before Charon/Aeneas Rust->Lean refinement (Phase 1c). Incorporates PR #233 (P1 signed-object Lean contracts, GPT-5/Codex); #233 can close as integrated. 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.
Phase 1 kickoff — the formal foundation
Per the roadmap (Phase 0.5/1a): rather than rebuild, this harvests the valuable P1 Lean work from #233 (GPT-5/Codex) and integrates the P0 authority algebra into it, giving one Lake project that builds P0 + P1 together under a CI gate.
What's here
formal/Ceremony/P0/Authority.lean— the P0 authority algebra (product meet-lattice, attenuation L4, no-fail-open OB-9/OB-12, order-independence L1). 25 theorems, 0sorry.formal/Ceremony/P1/SignedObject.lean+Gate.lean+Tests/— from formal: prove P1 signed-object contracts #233: profile/algorithm allowlist, canonical-encoding injectivity, the universalSignaturePreimagebinding profile/codec/domain/store/thread/body/cid/signer (OB-13), counterexample + contract tests, and theformalGateproof-escape check.lake build→ 9 jobs, exit 0;lake exe formalGate→ green. No Mathlib; builds in seconds..github/workflows/formal.yml— Tier-3 CI gate (ubuntu + windows).just check-formal(graceful skip if Lean absent) + pre-push parity (HOOK PARITY, ADR 0023)..gitignore**/.lake/; ROADMAP Phase 0 updated.Test plan
just check-formal→lake build(9 jobs) +lake exe formalGate, exit 0.[pre-push] OK).Integrates #233
The P1 signed-object Lean contracts were authored by GPT-5/Codex in #233; this PR incorporates them alongside P0. #233 can close as integrated once this lands.
Next (Phase 1c)
The pure Rust authority kernel mirroring
Ceremony/P0/Authority.lean, extracted by Charon and proven by Aeneas to refine it — gated on the opam/OCaml leg (docs/TOOLCHAIN.md). No wire structs frozen here; kernel stays pure.Refs #229 (merged spec), #233 (integrated), #232 (design plans).