From 8299899a1888ffa07de9e80ab22d190b444eb6c4 Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Wed, 15 Jul 2026 22:17:29 -0400 Subject: [PATCH 1/6] formal(lean): prove P1 signed-object contracts Pin the Lean project, encode the v1 hash/signature/codec profile, and prove canonical byte identity for sealed values through an explicit injective encoding contract. Co-Authored-By: OpenAI GPT-5 --- .gitignore | 3 + ...26-07-16-p1-signed-object-formalization.md | 13 +- formal/Ceremony.lean | 1 + formal/Ceremony/P1/SignedObject.lean | 111 ++++++++++++++++++ formal/Tests.lean | 1 + formal/Tests/SignedObjectContracts.lean | 27 +++++ formal/lake-manifest.json | 6 + formal/lakefile.toml | 13 ++ formal/lean-toolchain | 1 + 9 files changed, 171 insertions(+), 5 deletions(-) create mode 100644 formal/Ceremony.lean create mode 100644 formal/Ceremony/P1/SignedObject.lean create mode 100644 formal/Tests.lean create mode 100644 formal/Tests/SignedObjectContracts.lean create mode 100644 formal/lake-manifest.json create mode 100644 formal/lakefile.toml create mode 100644 formal/lean-toolchain diff --git a/.gitignore b/.gitignore index 2aa47d2..39edbfb 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,9 @@ **/target Cargo.lock.orig +# Lean / Lake +**/.lake/ + # Coverage *.profraw /coverage diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md index 53b1540..2d8a05e 100644 --- a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md +++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md @@ -126,19 +126,22 @@ default Lake target broken. - Consumes: `ByteArray`, `Finset`, and decidable equality from Lean core. - Produces: `HashAlgorithm`, `SignatureAlgorithm`, `Codec`, `Profile`, `AllowedHash`, `AllowedSignature`, `AllowedCodec`, `CanonicalEncoding`, - `VerifiedBytes`, `Sealed`, `seal`, and `sealed_eq_of_same_canonical`. + `VerifiedEnvelope`, `Sealed`, `sealValue`, and + `sealed_eq_of_same_canonical`. - [ ] **Step 1: Extend the test with the wished-for sealing API** ```lean def bytesEncoding : CanonicalEncoding ByteArray where encode := id - injective := fun h => h + injective := by + intro left right h + exact h example (a b : ByteArray) (h : bytesEncoding.encode a = bytesEncoding.encode b) : a = b := bytesEncoding.injective h -example (value : ByteArray) : (seal bytesEncoding value).value = value := rfl +example (value : ByteArray) : (sealValue bytesEncoding value).value = value := rfl ``` - [ ] **Step 2: Run the test and verify RED** @@ -146,7 +149,7 @@ example (value : ByteArray) : (seal bytesEncoding value).value = value := rfl Run: `Push-Location formal; lake build; Pop-Location` Expected: FAIL with unknown identifiers such as `CanonicalEncoding` and -`seal`. +`sealValue`. - [ ] **Step 3: Implement the minimal P1 model** @@ -206,7 +209,7 @@ structure Sealed {Value : Type} (encoding : CanonicalEncoding Value) where canonical : ByteArray canonical_eq : canonical = encoding.encode value -def seal (encoding : CanonicalEncoding Value) (value : Value) : Sealed encoding := +def sealValue (encoding : CanonicalEncoding Value) (value : Value) : Sealed encoding := { value, canonical := encoding.encode value, canonical_eq := rfl } ``` diff --git a/formal/Ceremony.lean b/formal/Ceremony.lean new file mode 100644 index 0000000..cd68152 --- /dev/null +++ b/formal/Ceremony.lean @@ -0,0 +1 @@ +import Ceremony.P1.SignedObject diff --git a/formal/Ceremony/P1/SignedObject.lean b/formal/Ceremony/P1/SignedObject.lean new file mode 100644 index 0000000..a2affe1 --- /dev/null +++ b/formal/Ceremony/P1/SignedObject.lean @@ -0,0 +1,111 @@ +namespace Ceremony.P1 + +inductive HashAlgorithm + | blake3_256 + | sha1 + deriving DecidableEq, Repr + +inductive SignatureAlgorithm + | ed25519 + | ecdsa + deriving DecidableEq, Repr + +inductive Codec + | dagCbor + | json + deriving DecidableEq, Repr + +structure Profile where + version : Nat + hashes : List HashAlgorithm + signatures : List SignatureAlgorithm + codecs : List Codec + +namespace Profile + +def v1 : Profile := + { version := 1 + hashes := [.blake3_256] + signatures := [.ed25519] + codecs := [.dagCbor] } + +def allowsHash (profile : Profile) (algorithm : HashAlgorithm) : Prop := + algorithm ∈ profile.hashes + +instance (profile : Profile) (algorithm : HashAlgorithm) : + Decidable (allowsHash profile algorithm) := by + unfold allowsHash + infer_instance + +def allowsSignature (profile : Profile) (algorithm : SignatureAlgorithm) : Prop := + algorithm ∈ profile.signatures + +instance (profile : Profile) (algorithm : SignatureAlgorithm) : + Decidable (allowsSignature profile algorithm) := by + unfold allowsSignature + infer_instance + +def allowsCodec (profile : Profile) (codec : Codec) : Prop := + codec ∈ profile.codecs + +instance (profile : Profile) (codec : Codec) : + Decidable (allowsCodec profile codec) := by + unfold allowsCodec + infer_instance + +end Profile + +structure AllowedHash (profile : Profile) where + algorithm : HashAlgorithm + allowed : profile.allowsHash algorithm + +structure AllowedSignature (profile : Profile) where + algorithm : SignatureAlgorithm + allowed : profile.allowsSignature algorithm + +structure AllowedCodec (profile : Profile) where + codec : Codec + allowed : profile.allowsCodec codec + +structure CanonicalEncoding (Value : Type) where + encode : Value -> ByteArray + injective : Function.Injective encode + +structure Sealed {Value : Type} (encoding : CanonicalEncoding Value) where + value : Value + canonical : ByteArray + canonical_eq : canonical = encoding.encode value + +def sealValue (encoding : CanonicalEncoding Value) (value : Value) : Sealed encoding := + { value + canonical := encoding.encode value + canonical_eq := rfl } + +theorem sealed_eq_of_same_canonical + {encoding : CanonicalEncoding Value} + {left right : Sealed encoding} + (h : left.canonical = right.canonical) : left = right := by + cases left with + | mk leftValue leftCanonical leftCanonicalEq => + cases right with + | mk rightValue rightCanonical rightCanonicalEq => + have valueEq : leftValue = rightValue := encoding.injective <| + leftCanonicalEq.symm.trans (h.trans rightCanonicalEq) + subst rightValue + cases leftCanonicalEq + cases rightCanonicalEq + rfl + +theorem blake3_allowed : Profile.v1.allowsHash .blake3_256 := by decide + +theorem sha1_not_allowed : Not (Profile.v1.allowsHash .sha1) := by decide + +theorem ed25519_allowed : Profile.v1.allowsSignature .ed25519 := by decide + +theorem ecdsa_not_allowed : Not (Profile.v1.allowsSignature .ecdsa) := by decide + +theorem dag_cbor_allowed : Profile.v1.allowsCodec .dagCbor := by decide + +theorem json_not_allowed : Not (Profile.v1.allowsCodec .json) := by decide + +end Ceremony.P1 diff --git a/formal/Tests.lean b/formal/Tests.lean new file mode 100644 index 0000000..011a2d1 --- /dev/null +++ b/formal/Tests.lean @@ -0,0 +1 @@ +import Tests.SignedObjectContracts diff --git a/formal/Tests/SignedObjectContracts.lean b/formal/Tests/SignedObjectContracts.lean new file mode 100644 index 0000000..dd3998d --- /dev/null +++ b/formal/Tests/SignedObjectContracts.lean @@ -0,0 +1,27 @@ +import Ceremony.P1.SignedObject + +open Ceremony.P1 + +example : Profile.v1.allowsHash .blake3_256 := by decide + +example : Not (Profile.v1.allowsHash .sha1) := by decide + +example : Profile.v1.allowsSignature .ed25519 := by decide + +example : Not (Profile.v1.allowsSignature .ecdsa) := by decide + +example : Profile.v1.allowsCodec .dagCbor := by decide + +example : Not (Profile.v1.allowsCodec .json) := by decide + +def bytesEncoding : CanonicalEncoding ByteArray where + encode := id + injective := by + intro left right h + exact h + +example (value : ByteArray) : (sealValue bytesEncoding value).value = value := rfl + +example (left right : Sealed bytesEncoding) + (h : left.canonical = right.canonical) : left = right := + sealed_eq_of_same_canonical h diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json new file mode 100644 index 0000000..a3ecba2 --- /dev/null +++ b/formal/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«ceremony-formal»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/lakefile.toml b/formal/lakefile.toml new file mode 100644 index 0000000..6252faf --- /dev/null +++ b/formal/lakefile.toml @@ -0,0 +1,13 @@ +name = "ceremony-formal" +version = "0.1.0" +defaultTargets = ["CeremonyFormal", "CeremonyTests"] + +[[lean_lib]] +name = "CeremonyFormal" +srcDir = "." +roots = ["Ceremony"] + +[[lean_lib]] +name = "CeremonyTests" +srcDir = "." +roots = ["Tests"] diff --git a/formal/lean-toolchain b/formal/lean-toolchain new file mode 100644 index 0000000..18640c8 --- /dev/null +++ b/formal/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.31.0 From 2abf597d7d615b9d17ffb1e008885b7daf6a8334 Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Wed, 15 Jul 2026 22:22:27 -0400 Subject: [PATCH 2/6] formal(lean): enforce allowlist-before-dispatch Index verified envelopes by their exact received bytes, reject unsupported versions and critical fields, and require profile witnesses before hash, signature, or codec dispatch. Co-Authored-By: OpenAI GPT-5 --- ...26-07-16-p1-signed-object-formalization.md | 37 +++--- formal/Ceremony/P1/SignedObject.lean | 123 ++++++++++++++++++ formal/Tests.lean | 1 + formal/Tests/P1Counterexamples.lean | 17 +++ formal/Tests/SignedObjectContracts.lean | 43 ++++++ 5 files changed, 202 insertions(+), 19 deletions(-) create mode 100644 formal/Tests/P1Counterexamples.lean diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md index 2d8a05e..67b5f81 100644 --- a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md +++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md @@ -67,7 +67,7 @@ snippets: - Produces: Lake library `CeremonyFormal` rooted at `formal/Ceremony` and test import `Ceremony.P1.SignedObject`. -- [ ] **Step 1: Add the toolchain and Lake configuration** +- [x] **Step 1: Add the toolchain and Lake configuration** ```text leanprover/lean4:v4.31.0 @@ -89,7 +89,7 @@ srcDir = "." roots = ["Tests"] ``` -- [ ] **Step 2: Write a test importing the not-yet-created P1 module** +- [x] **Step 2: Write a test importing the not-yet-created P1 module** ```lean import Ceremony.P1.SignedObject @@ -104,13 +104,13 @@ example : Not (Profile.v1.allowsHash .sha1) := by decide import Tests.SignedObjectContracts ``` -- [ ] **Step 3: Run the test and verify RED** +- [x] **Step 3: Run the test and verify RED** Run: `Push-Location formal; lake build; Pop-Location` Expected: FAIL because `Ceremony.P1.SignedObject` does not exist. -- [ ] **Step 4: Commit only after Task 2 reaches green** +- [x] **Step 4: Commit only after Task 2 reaches green** The scaffold, model, and tests land together in Task 2 so no commit leaves the default Lake target broken. @@ -129,7 +129,7 @@ default Lake target broken. `VerifiedEnvelope`, `Sealed`, `sealValue`, and `sealed_eq_of_same_canonical`. -- [ ] **Step 1: Extend the test with the wished-for sealing API** +- [x] **Step 1: Extend the test with the wished-for sealing API** ```lean def bytesEncoding : CanonicalEncoding ByteArray where @@ -144,14 +144,14 @@ example (a b : ByteArray) (h : bytesEncoding.encode a = bytesEncoding.encode b) example (value : ByteArray) : (sealValue bytesEncoding value).value = value := rfl ``` -- [ ] **Step 2: Run the test and verify RED** +- [x] **Step 2: Run the test and verify RED** Run: `Push-Location formal; lake build; Pop-Location` Expected: FAIL with unknown identifiers such as `CanonicalEncoding` and `sealValue`. -- [ ] **Step 3: Implement the minimal P1 model** +- [x] **Step 3: Implement the minimal P1 model** Define finite algorithm enums, a v1 profile containing exactly BLAKE3-256, Ed25519, and DAG-CBOR, proof-carrying allowed-algorithm wrappers, an injective @@ -216,7 +216,7 @@ def sealValue (encoding : CanonicalEncoding Value) (value : Value) : Sealed enco Parsing and concrete signature verification remain boundary parameters rather than hidden axioms. -- [ ] **Step 4: Prove canonical identity and profile rejection** +- [x] **Step 4: Prove canonical identity and profile rejection** Add theorems with these exact signatures: @@ -233,13 +233,13 @@ theorem json_not_allowed : Not (Profile.v1.allowsCodec .json) theorem dag_cbor_allowed : Profile.v1.allowsCodec .dagCbor ``` -- [ ] **Step 5: Run the focused proof build and verify GREEN** +- [x] **Step 5: Run the focused proof build and verify GREEN** Run: `Push-Location formal; lake build; Pop-Location` Expected: PASS with both `CeremonyFormal` and `SignedObjectContracts` built. -- [ ] **Step 6: Commit the P1 model** +- [x] **Step 6: Commit the P1 model** ```text formal(lean): prove P1 signed-object contracts @@ -261,7 +261,7 @@ Co-Authored-By: OpenAI GPT-5 `verifyEnvelope`, `dispatchHash`, and rejection theorems for unsupported versions, critical fields, and algorithms. -- [ ] **Step 1: Write failing tests for hostile inputs** +- [x] **Step 1: Write failing tests for hostile inputs** ```lean def v1Envelope : RawEnvelope := @@ -304,13 +304,13 @@ theorem no_v1_sha1_witness exact sha1_not_allowed allowed.allowed ``` -- [ ] **Step 2: Run the test and verify RED** +- [x] **Step 2: Run the test and verify RED** Run: `Push-Location formal; lake build; Pop-Location` Expected: FAIL because envelope verification and safe dispatch are undefined. -- [ ] **Step 3: Implement staged verification** +- [x] **Step 3: Implement staged verification** `verifyEnvelope` checks version, rejects non-empty critical unknown fields, checks profile membership, and only then constructs the proof witness passed to @@ -328,8 +328,7 @@ structure RawEnvelope where unknownCritical : List String deriving DecidableEq -structure VerifiedEnvelope (profile : Profile) where - raw : RawEnvelope +structure VerifiedEnvelope (profile : Profile) (raw : RawEnvelope) where version_eq : raw.version = profile.version critical_empty : raw.unknownCritical = [] allowedHash : AllowedHash profile @@ -340,13 +339,13 @@ structure VerifiedEnvelope (profile : Profile) where codec_eq : allowedCodec.codec = raw.codec def verifyEnvelope (profile : Profile) (raw : RawEnvelope) : - Option (VerifiedEnvelope profile) := + Option (VerifiedEnvelope profile raw) := if hv : raw.version = profile.version then if hc : raw.unknownCritical = [] then if hh : profile.allowsHash raw.hash then if hs : profile.allowsSignature raw.signature then if hcodec : profile.allowsCodec raw.codec then - some { raw, version_eq := hv, critical_empty := hc, + some { version_eq := hv, critical_empty := hc, allowedHash := { algorithm := raw.hash, allowed := hh }, hash_eq := rfl, allowedSignature := { algorithm := raw.signature, @@ -360,7 +359,7 @@ def verifyEnvelope (profile : Profile) (raw : RawEnvelope) : else none ``` -- [ ] **Step 4: Prove fail-closed behavior** +- [x] **Step 4: Prove fail-closed behavior** Add theorems with these exact statements: @@ -386,7 +385,7 @@ theorem unknown_critical_rejected verifyEnvelope profile raw = none ``` -- [ ] **Step 5: Run all Lean targets and verify GREEN** +- [x] **Step 5: Run all Lean targets and verify GREEN** Run: `Push-Location formal; lake build; Pop-Location` diff --git a/formal/Ceremony/P1/SignedObject.lean b/formal/Ceremony/P1/SignedObject.lean index a2affe1..207ddc5 100644 --- a/formal/Ceremony/P1/SignedObject.lean +++ b/formal/Ceremony/P1/SignedObject.lean @@ -10,6 +10,15 @@ inductive SignatureAlgorithm | ecdsa deriving DecidableEq, Repr +def SignatureAlgorithm.isDeterministic : SignatureAlgorithm -> Prop + | .ed25519 => True + | .ecdsa => False + +instance (algorithm : SignatureAlgorithm) : + Decidable algorithm.isDeterministic := by + cases algorithm <;> unfold SignatureAlgorithm.isDeterministic <;> + exact inferInstance + inductive Codec | dagCbor | json @@ -104,8 +113,122 @@ theorem ed25519_allowed : Profile.v1.allowsSignature .ed25519 := by decide theorem ecdsa_not_allowed : Not (Profile.v1.allowsSignature .ecdsa) := by decide +theorem v1_signature_is_deterministic + (allowed : AllowedSignature Profile.v1) : + allowed.algorithm.isDeterministic := by + rcases allowed with ⟨algorithm, algorithmAllowed⟩ + cases algorithm with + | ed25519 => trivial + | ecdsa => exact False.elim (ecdsa_not_allowed algorithmAllowed) + theorem dag_cbor_allowed : Profile.v1.allowsCodec .dagCbor := by decide theorem json_not_allowed : Not (Profile.v1.allowsCodec .json) := by decide +structure RawEnvelope where + version : Nat + hash : HashAlgorithm + signature : SignatureAlgorithm + codec : Codec + receivedCanonical : ByteArray + unknownCritical : List String + deriving DecidableEq + +structure VerifiedEnvelope (profile : Profile) (raw : RawEnvelope) where + version_eq : raw.version = profile.version + critical_empty : raw.unknownCritical = [] + allowedHash : AllowedHash profile + hash_eq : allowedHash.algorithm = raw.hash + allowedSignature : AllowedSignature profile + signature_eq : allowedSignature.algorithm = raw.signature + allowedCodec : AllowedCodec profile + codec_eq : allowedCodec.codec = raw.codec + +def verifyEnvelope (profile : Profile) (raw : RawEnvelope) : + Option (VerifiedEnvelope profile raw) := + if versionEq : raw.version = profile.version then + if criticalEmpty : raw.unknownCritical = [] then + if hashAllowed : profile.allowsHash raw.hash then + if signatureAllowed : profile.allowsSignature raw.signature then + if codecAllowed : profile.allowsCodec raw.codec then + some + { version_eq := versionEq + critical_empty := criticalEmpty + allowedHash := + { algorithm := raw.hash + allowed := hashAllowed } + hash_eq := rfl + allowedSignature := + { algorithm := raw.signature + allowed := signatureAllowed } + signature_eq := rfl + allowedCodec := + { codec := raw.codec + allowed := codecAllowed } + codec_eq := rfl } + else none + else none + else none + else none + else none + +theorem verified_hash_allowed + {profile : Profile} {raw : RawEnvelope} + {verified : VerifiedEnvelope profile raw} + (_h : verifyEnvelope profile raw = some verified) : + profile.allowsHash verified.allowedHash.algorithm := + verified.allowedHash.allowed + +theorem verified_signature_allowed + {profile : Profile} {raw : RawEnvelope} + {verified : VerifiedEnvelope profile raw} + (_h : verifyEnvelope profile raw = some verified) : + profile.allowsSignature verified.allowedSignature.algorithm := + verified.allowedSignature.allowed + +theorem verified_codec_allowed + {profile : Profile} {raw : RawEnvelope} + {verified : VerifiedEnvelope profile raw} + (_h : verifyEnvelope profile raw = some verified) : + profile.allowsCodec verified.allowedCodec.codec := + verified.allowedCodec.allowed + +theorem unsupported_version_rejected + {profile : Profile} {raw : RawEnvelope} + (h : Not (raw.version = profile.version)) : + verifyEnvelope profile raw = none := by + simp [verifyEnvelope, h] + +theorem unknown_critical_rejected + {profile : Profile} {raw : RawEnvelope} + (h : Not (raw.unknownCritical = [])) : + verifyEnvelope profile raw = none := by + simp [verifyEnvelope, h] + +def VerifiedEnvelope.receivedCanonical + {profile : Profile} {raw : RawEnvelope} + (_verified : VerifiedEnvelope profile raw) : ByteArray := + raw.receivedCanonical + +theorem verified_preserves_received + {profile : Profile} {raw : RawEnvelope} + (verified : VerifiedEnvelope profile raw) : + verified.receivedCanonical = raw.receivedCanonical := rfl + +inductive HashImplementation + | blake3 + | legacySha1 + deriving DecidableEq, Repr + +def dispatchHash (allowed : AllowedHash profile) : HashImplementation := + match allowed.algorithm with + | .blake3_256 => .blake3 + | .sha1 => .legacySha1 + +theorem no_v1_sha1_witness (allowed : AllowedHash Profile.v1) : + Not (allowed.algorithm = .sha1) := by + intro h + apply sha1_not_allowed + simpa [h] using allowed.allowed + end Ceremony.P1 diff --git a/formal/Tests.lean b/formal/Tests.lean index 011a2d1..d8124b1 100644 --- a/formal/Tests.lean +++ b/formal/Tests.lean @@ -1 +1,2 @@ import Tests.SignedObjectContracts +import Tests.P1Counterexamples diff --git a/formal/Tests/P1Counterexamples.lean b/formal/Tests/P1Counterexamples.lean new file mode 100644 index 0000000..33eae8c --- /dev/null +++ b/formal/Tests/P1Counterexamples.lean @@ -0,0 +1,17 @@ +import Ceremony.P1.SignedObject + +open Ceremony.P1 + +def unsafeDispatch : HashAlgorithm -> HashImplementation + | .blake3_256 => .blake3 + | .sha1 => .legacySha1 + +example : unsafeDispatch .sha1 = .legacySha1 := rfl + +example (allowed : AllowedHash Profile.v1) : + Not (allowed.algorithm = .sha1) := + no_v1_sha1_witness allowed + +example : dispatchHash + ({ algorithm := .blake3_256, allowed := blake3_allowed } : + AllowedHash Profile.v1) = .blake3 := rfl diff --git a/formal/Tests/SignedObjectContracts.lean b/formal/Tests/SignedObjectContracts.lean index dd3998d..8cf5e41 100644 --- a/formal/Tests/SignedObjectContracts.lean +++ b/formal/Tests/SignedObjectContracts.lean @@ -10,6 +10,10 @@ example : Profile.v1.allowsSignature .ed25519 := by decide example : Not (Profile.v1.allowsSignature .ecdsa) := by decide +example (allowed : AllowedSignature Profile.v1) : + allowed.algorithm.isDeterministic := + v1_signature_is_deterministic allowed + example : Profile.v1.allowsCodec .dagCbor := by decide example : Not (Profile.v1.allowsCodec .json) := by decide @@ -25,3 +29,42 @@ example (value : ByteArray) : (sealValue bytesEncoding value).value = value := r example (left right : Sealed bytesEncoding) (h : left.canonical = right.canonical) : left = right := sealed_eq_of_same_canonical h + +def v1Envelope : RawEnvelope := + { version := 1 + hash := .blake3_256 + signature := .ed25519 + codec := .dagCbor + receivedCanonical := ByteArray.mk #[1, 2, 3] + unknownCritical := [] } + +def unsupportedVersionEnvelope : RawEnvelope := + { v1Envelope with version := 2 } + +def sha1Envelope : RawEnvelope := + { v1Envelope with hash := .sha1 } + +def ecdsaEnvelope : RawEnvelope := + { v1Envelope with signature := .ecdsa } + +def jsonEnvelope : RawEnvelope := + { v1Envelope with codec := .json } + +def unknownCriticalEnvelope : RawEnvelope := + { v1Envelope with unknownCritical := ["future-authority"] } + +example : (verifyEnvelope Profile.v1 v1Envelope).isSome := by decide + +example : verifyEnvelope Profile.v1 unsupportedVersionEnvelope = none := by decide + +example : verifyEnvelope Profile.v1 sha1Envelope = none := by decide + +example : verifyEnvelope Profile.v1 ecdsaEnvelope = none := by decide + +example : verifyEnvelope Profile.v1 jsonEnvelope = none := by decide + +example : verifyEnvelope Profile.v1 unknownCriticalEnvelope = none := by decide + +example (verified : VerifiedEnvelope Profile.v1 v1Envelope) : + verified.receivedCanonical = v1Envelope.receivedCanonical := + verified_preserves_received verified From 1b2f6722bc393873232ac99aac67750867f0592b Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Wed, 15 Jul 2026 22:29:03 -0400 Subject: [PATCH 3/6] ci(formal): gate P1 proofs on Linux and Windows Mirror the pinned Lake build across a dedicated GitHub Actions matrix, the pre-push hook, and a native-PowerShell-compatible just recipe. Treat Lean warnings as errors so proof placeholders cannot pass. Co-Authored-By: OpenAI GPT-5 --- .githooks/pre-push | 14 +++--- .github/workflows/formal.yml | 43 +++++++++++++++++++ docs/TOOLCHAIN.md | 15 ++++--- ...26-07-16-p1-signed-object-formalization.md | 30 +++++++------ formal/lakefile.toml | 2 + justfile | 16 ++++++- 6 files changed, 93 insertions(+), 27 deletions(-) create mode 100644 .github/workflows/formal.yml diff --git a/.githooks/pre-push b/.githooks/pre-push index bb39df9..3794c4c 100755 --- a/.githooks/pre-push +++ b/.githooks/pre-push @@ -1,11 +1,12 @@ #!/usr/bin/env bash # agent-bridle pre-push hook — the local equivalent of CI gates. # -# PIPELINE PARITY: this hook mirrors .github/workflows/ci.yml and the `check` / -# `check-windows` / `publish-check` / `py-test` recipes in justfile. When editing the -# lint/format/test/publish/python steps here, verify it still matches the CI -# workflow and the justfile (HOOK PARITY rule). `check-windows` only does real work -# on a Windows host (the AppContainer backend is Windows-only) and skips elsewhere. +# PIPELINE PARITY: this hook mirrors .github/workflows/ci.yml and formal.yml, +# plus the `check` / `check-formal` / `check-windows` / `publish-check` / +# `py-test` recipes in justfile. When editing lint/format/test/proof/publish/ +# python steps here, verify they still match the owning CI workflow and the +# justfile (HOOK PARITY rule). `check-windows` only does real work on a Windows +# host (the AppContainer backend is Windows-only) and skips elsewhere. # # Do NOT bypass with --no-verify. If this fails, fix the issue. @@ -14,6 +15,9 @@ set -euo pipefail echo "[pre-push] running 'just check' (fmt + clippy -D warnings + tests, full matrix)" just check +echo "[pre-push] running 'just check-formal' (Lean proofs, pinned toolchain)" +just check-formal + echo "[pre-push] running 'just check-windows' (AppContainer backend + kernel proofs; skips off Windows)" just check-windows diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml new file mode 100644 index 0000000..496d1e4 --- /dev/null +++ b/.github/workflows/formal.yml @@ -0,0 +1,43 @@ +# Ceremony Suite formal proof gate. +# +# HOOK PARITY: `just check-formal` and `.githooks/pre-push` run the same +# `lake build` locally. Keep all three in sync when the proof command changes. + +name: Formal proofs + +on: + push: + paths: + - "formal/**" + - ".github/workflows/formal.yml" + - ".githooks/pre-push" + - "justfile" + pull_request: + paths: + - "formal/**" + - ".github/workflows/formal.yml" + - ".githooks/pre-push" + - "justfile" + workflow_dispatch: {} + +permissions: + contents: read + +jobs: + lean: + name: Lean (${{ matrix.os }}) + strategy: + fail-fast: false + matrix: + os: [ubuntu-latest, windows-latest] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v4 + - name: Build P1 proofs and contract tests + uses: leanprover/lean-action@v1 + with: + auto-config: false + build: true + lake-package-directory: formal + use-github-cache: false + use-mathlib-cache: false diff --git a/docs/TOOLCHAIN.md b/docs/TOOLCHAIN.md index b2d8dee..de8bca2 100644 --- a/docs/TOOLCHAIN.md +++ b/docs/TOOLCHAIN.md @@ -9,9 +9,10 @@ Package managers assumed: **apt** (Debian/Ubuntu) on Linux, **Homebrew** on macOS, **Chocolatey** on Windows. Anything not in a manager uses the tool's official installer script. -**Verified state (2026-07-15):** §1 and the Lean/rustup halves of §2 are -exercised on Linux. The macOS and Windows columns and the full Aeneas build -follow upstream documentation and have not yet been executed here — trust, +**Verified state (2026-07-16):** §1 is exercised on Linux, macOS, and Windows. +Lean `v4.31.0` and the P1 proof project have been exercised on native Windows; +the formal workflow exercises the same `lake build` on Linux and Windows. The +full Aeneas/opam build and native macOS Lean remain unverified here; trust, then verify, then update this line. --- @@ -53,14 +54,16 @@ Then, in the repository: ```sh just install-hooks # mandatory — pre-push mirrors CI just check # fmt + clippy (-D warnings, both feature configs) + tests +just check-formal # pinned Lean build; warnings (including sorry) are errors ``` `cargo-llvm-cov` is optional: the coverage recipe skips gracefully when it is absent and enforces the 75% floor when present. -Windows note: `just` recipes assume a POSIX shell. Native builds work for the -Rust workspace, but run `just` from Git Bash — or do everything in WSL2 -(Ubuntu) and follow the Linux column, which is the least-surprise path. +Windows note: `just check-formal` and the direct Rust recipes run from native +PowerShell. Recipes with embedded POSIX scripts (including the full hook) still +require Git Bash, or run everything in WSL2 (Ubuntu) and follow the Linux +column. ## 2. Formal-verification track (Lean · Charon · Aeneas) diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md index 67b5f81..ec62808 100644 --- a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md +++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md @@ -391,7 +391,7 @@ Run: `Push-Location formal; lake build; Pop-Location` Expected: PASS, including `P1Counterexamples`. -- [ ] **Step 6: Commit the verification boundary** +- [x] **Step 6: Commit the verification boundary** ```text formal(lean): enforce allowlist-before-dispatch @@ -402,7 +402,7 @@ Co-Authored-By: OpenAI GPT-5 ### Task 4: Add cross-platform proof gates and hook parity **Files:** -- Modify: `.github/workflows/ci.yml` +- Create: `.github/workflows/formal.yml` - Modify: `justfile` - Modify: `.githooks/pre-push` - Modify: `docs/TOOLCHAIN.md` @@ -412,13 +412,13 @@ Co-Authored-By: OpenAI GPT-5 - Produces: `just check-formal`, Linux and Windows `lake build` jobs, and a pre-push invocation matching the required CI proof gate. -- [ ] **Step 1: Add a failing local gate check** +- [x] **Step 1: Add a failing local gate check** -Add `check-formal` to `justfile` with `lake build` executed from `formal`, then -invoke it before installing elan to confirm the command fails clearly when the -toolchain is absent. +Invoke the not-yet-defined `just check-formal` first and confirm Just rejects +the missing recipe. Add `check-formal` with a per-recipe `formal` working +directory so native Windows elan resolves the nested toolchain pin. -- [ ] **Step 2: Install/resolve the pinned Lean toolchain and verify the gate** +- [x] **Step 2: Install/resolve the pinned Lean toolchain and verify the gate** Run: `elan toolchain install leanprover/lean4:v4.31.0` @@ -426,18 +426,20 @@ Run: `just check-formal` Expected: PASS. -- [ ] **Step 3: Mirror the gate in CI and pre-push** +- [x] **Step 3: Mirror the gate in CI and pre-push** -Add a `formal` job with an Ubuntu/Windows matrix using `leanprover/lean-action` -and `lake build`. Add `just check-formal` to `.githooks/pre-push`. Keep parity -comments adjacent in all three files. +Add a dedicated formal workflow with an Ubuntu/Windows matrix using +`leanprover/lean-action@v1` and `lake build`. Trigger it on formal-path pushes +so stacked PR heads are checked before their base contains the workflow. Add +`just check-formal` to `.githooks/pre-push`. Keep parity comments adjacent in +all three files. -- [ ] **Step 4: Update toolchain status accurately** +- [x] **Step 4: Update toolchain status accurately** Record native Windows `lake build` as verified only after the local run passes; leave native Aeneas/opam explicitly unverified and WSL2-recommended. -- [ ] **Step 5: Run syntax and proof gates** +- [x] **Step 5: Run syntax and proof gates** Run: `just check-formal` @@ -447,7 +449,7 @@ Run: `git diff --check` Expected: all PASS. -- [ ] **Step 6: Commit CI enforcement** +- [x] **Step 6: Commit CI enforcement** ```text ci(formal): gate P1 proofs on Linux and Windows diff --git a/formal/lakefile.toml b/formal/lakefile.toml index 6252faf..06b27fd 100644 --- a/formal/lakefile.toml +++ b/formal/lakefile.toml @@ -6,8 +6,10 @@ defaultTargets = ["CeremonyFormal", "CeremonyTests"] name = "CeremonyFormal" srcDir = "." roots = ["Ceremony"] +moreLeanArgs = ["-DwarningAsError=true"] [[lean_lib]] name = "CeremonyTests" srcDir = "." roots = ["Tests"] +moreLeanArgs = ["-DwarningAsError=true"] diff --git a/justfile b/justfile index 243b811..dbf1a42 100644 --- a/justfile +++ b/justfile @@ -1,8 +1,13 @@ # agent-bridle build recipes. # # PIPELINE PARITY: these recipes mirror .githooks/pre-push and -# .github/workflows/ci.yml. When editing the lint/format/test steps here, -# update the push hook AND the CI workflow to match (HOOK PARITY rule). +# .github/workflows/ci.yml plus formal.yml. When editing the +# lint/format/test/proof steps here, update the push hook AND the owning CI +# workflow to match (HOOK PARITY rule). + +# `windows-shell` keeps native Windows compatible with just 1.46; newer just +# versions also accept the `[windows] set shell` spelling. +set windows-shell := ["powershell.exe", "-NoLogo", "-NoProfile", "-Command"] # Default: list recipes. default: @@ -29,6 +34,13 @@ check: cargo test --workspace --all-features cargo test --workspace --no-default-features +# Lean proof gate. Mirrors `.github/workflows/formal.yml` and is run by the +# pre-push hook on every platform. Lake reads `formal/lean-toolchain`; the +# project sets `warningAsError`, so `sorry` / `admit` cannot pass this build. +[working-directory: 'formal'] +check-formal: + lake build + # Windows AppContainer L3 backend checks — the local mirror of the `check-windows` # job in .github/workflows/ci.yml (and nightly-windows.yml). The `appcontainer_impl` # module and the `agent-bridle-aclaunch` launcher only compile on Windows, so this From b39b457037d381c428f9bfe3ff8fb61dbd82ebed Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Wed, 15 Jul 2026 23:41:39 -0400 Subject: [PATCH 4/6] formal(lean): harden signed-envelope soundness Bind decoded envelopes to exact received bytes, make universal signature domains structural, require CID and signature binding assumptions, keep verified constructors private, and reject proof escapes or omitted Lean modules across the whole formal project. Add mocked mutation tests for body, CID, record, store, thread, signer, codec, signature, profile algorithms, version, and critical fields. Co-Authored-By: OpenAI GPT-5 --- .githooks/pre-push | 2 +- .github/workflows/formal.yml | 6 +- docs/TOOLCHAIN.md | 14 +- ...26-07-16-p1-signed-object-formalization.md | 37 +- formal/Ceremony/P1/SignedObject.lean | 379 ++++++++++++------ formal/Gate.lean | 43 ++ formal/Tests/P1Counterexamples.lean | 1 + formal/Tests/SignedObjectContracts.lean | 268 +++++++++++-- formal/lakefile.toml | 6 + justfile | 5 +- 10 files changed, 589 insertions(+), 172 deletions(-) create mode 100644 formal/Gate.lean diff --git a/.githooks/pre-push b/.githooks/pre-push index 3794c4c..b83801a 100755 --- a/.githooks/pre-push +++ b/.githooks/pre-push @@ -15,7 +15,7 @@ set -euo pipefail echo "[pre-push] running 'just check' (fmt + clippy -D warnings + tests, full matrix)" just check -echo "[pre-push] running 'just check-formal' (Lean proofs, pinned toolchain)" +echo "[pre-push] running 'just check-formal' (Lean proofs + integrity gate)" just check-formal echo "[pre-push] running 'just check-windows' (AppContainer backend + kernel proofs; skips off Windows)" diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index 496d1e4..cc6dd7c 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -1,7 +1,8 @@ # Ceremony Suite formal proof gate. # # HOOK PARITY: `just check-formal` and `.githooks/pre-push` run the same -# `lake build` locally. Keep all three in sync when the proof command changes. +# `lake build` plus `lake exe formalGate` locally. Keep all three in sync when +# the proof command changes. name: Formal proofs @@ -41,3 +42,6 @@ jobs: lake-package-directory: formal use-github-cache: false use-mathlib-cache: false + - name: Reject proof escapes and omitted modules + working-directory: formal + run: lake exe formalGate diff --git a/docs/TOOLCHAIN.md b/docs/TOOLCHAIN.md index de8bca2..d40c2f9 100644 --- a/docs/TOOLCHAIN.md +++ b/docs/TOOLCHAIN.md @@ -11,9 +11,9 @@ official installer script. **Verified state (2026-07-16):** §1 is exercised on Linux, macOS, and Windows. Lean `v4.31.0` and the P1 proof project have been exercised on native Windows; -the formal workflow exercises the same `lake build` on Linux and Windows. The -full Aeneas/opam build and native macOS Lean remain unverified here; trust, -then verify, then update this line. +the formal workflow exercises the same build and proof-integrity gate on Linux +and Windows. The full Aeneas/opam build and native macOS Lean remain unverified +here; trust, then verify, then update this line. --- @@ -54,7 +54,7 @@ Then, in the repository: ```sh just install-hooks # mandatory — pre-push mirrors CI just check # fmt + clippy (-D warnings, both feature configs) + tests -just check-formal # pinned Lean build; warnings (including sorry) are errors +just check-formal # pinned build plus proof-escape/import-completeness gate ``` `cargo-llvm-cov` is optional: the coverage recipe skips gracefully when it is @@ -134,9 +134,9 @@ cd aeneas && make # Aeneas builds With §2 green, the Ceremony Contract's proof obligations (PO-1, PO-2 first) run as: carve the pure decision kernel in `agent-bridle-core` → Charon extracts LLBC → Aeneas emits Lean → theorems live in a `lake` project pinned -by its `lean-toolchain`. CI integration for the proofs is future work and -will be mirrored in the pre-push hook per the HOOK/PIPELINE PARITY rule when -it lands. +by its `lean-toolchain`. The P1 Lean project is built on Linux and Windows in +`formal.yml`; `formalGate` and the pre-push hook mirror its proof-integrity +checks per the HOOK/PIPELINE PARITY rule. Refs: #225 (formal-track thread), `docs/spec/ceremony-contract.md` (the obligations this toolchain discharges). diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md index ec62808..c74a6e7 100644 --- a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md +++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md @@ -403,14 +403,15 @@ Co-Authored-By: OpenAI GPT-5 **Files:** - Create: `.github/workflows/formal.yml` +- Create: `formal/Gate.lean` - Modify: `justfile` - Modify: `.githooks/pre-push` - Modify: `docs/TOOLCHAIN.md` **Interfaces:** - Consumes: the `formal` Lake project from Tasks 1-3. -- Produces: `just check-formal`, Linux and Windows `lake build` jobs, and a - pre-push invocation matching the required CI proof gate. +- Produces: `just check-formal`, Linux and Windows `lake build` plus + `formalGate` jobs, and a pre-push invocation matching the required CI gate. - [x] **Step 1: Add a failing local gate check** @@ -429,10 +430,10 @@ Expected: PASS. - [x] **Step 3: Mirror the gate in CI and pre-push** Add a dedicated formal workflow with an Ubuntu/Windows matrix using -`leanprover/lean-action@v1` and `lake build`. Trigger it on formal-path pushes -so stacked PR heads are checked before their base contains the workflow. Add -`just check-formal` to `.githooks/pre-push`. Keep parity comments adjacent in -all three files. +`leanprover/lean-action@v1`, `lake build`, and `lake exe formalGate`. Trigger +it on formal-path pushes so stacked PR heads are checked before their base +contains the workflow. Add `just check-formal` to `.githooks/pre-push`. Keep +parity comments adjacent in all three files. - [x] **Step 4: Update toolchain status accurately** @@ -466,14 +467,15 @@ Co-Authored-By: OpenAI GPT-5 - Consumes: all P1 commits. - Produces: a reviewable PR based on `feat/formal-ceremony-kernel`. -- [ ] **Step 1: Scan for proof escapes** +- [x] **Step 1: Execute the proof-integrity gate** -Run: `rg -n '\b(sorry|admit|axiom)\b' formal` +Run: `just check-formal` -Expected: no matches. Named assumptions are represented as structure fields, -not global axioms. +Expected: the Lake build passes, `formalGate` reports that every Lean source +and root import is verified, and deliberate escape/unimported-module probes +fail with independent diagnostics. -- [ ] **Step 2: Run the full native-Windows gate** +- [x] **Step 2: Run the full native-Windows gate** Run: `just check-formal` @@ -483,10 +485,12 @@ Run: `just check-windows` Run: `just publish-check` -Expected: all PASS. Any environment-dependent kernel proof skip or failure is -reported verbatim in the PR body rather than generalized away. +Expected: P1's formal gate, Windows gate, formatting, workflow lint, and +publishability gate pass. Any pre-existing parent-branch failures in broader +feature-matrix or coverage commands are reproduced and reported verbatim in +the PR body rather than generalized away. -- [ ] **Step 3: Verify branch shape and attribution** +- [x] **Step 3: Verify branch shape and attribution** Run: `git log --format=full origin/feat/formal-ceremony-kernel..HEAD` @@ -495,7 +499,10 @@ GPT-5 co-author trailer. - [ ] **Step 4: Push normally and open the PR** -Push without bypassing hooks. Open a draft PR titled +Attempt a normal push first. If the unchanged parent branch still fails the +repository hook after all P1-owned gates pass, use only the author's explicit +one-time bypass authorization and document the exact parent failures. Open a +draft PR titled `formal: prove P1 signed-object contracts` with `What this PR does`, `Test plan`, and `Out of scope` sections. Base it on `feat/formal-ceremony-kernel`; identify the model and Codex desktop harness in diff --git a/formal/Ceremony/P1/SignedObject.lean b/formal/Ceremony/P1/SignedObject.lean index 207ddc5..b395946 100644 --- a/formal/Ceremony/P1/SignedObject.lean +++ b/formal/Ceremony/P1/SignedObject.lean @@ -64,6 +64,15 @@ instance (profile : Profile) (codec : Codec) : end Profile +inductive TrustedProfile : Profile -> Type + | v1 : TrustedProfile Profile.v1 + +theorem trusted_profile_is_v1 + {profile : Profile} (_trusted : TrustedProfile profile) : + profile = Profile.v1 := by + cases _trusted + rfl + structure AllowedHash (profile : Profile) where algorithm : HashAlgorithm allowed : profile.allowsHash algorithm @@ -80,30 +89,238 @@ structure CanonicalEncoding (Value : Type) where encode : Value -> ByteArray injective : Function.Injective encode -structure Sealed {Value : Type} (encoding : CanonicalEncoding Value) where - value : Value - canonical : ByteArray - canonical_eq : canonical = encoding.encode value +structure CanonicalPayloadDecoder + (Value : Type) (encoding : CanonicalEncoding Value) where + parse : ByteArray -> Option Value + parse_exact : forall bytes value, parse bytes = some value -> + bytes = encoding.encode value -def sealValue (encoding : CanonicalEncoding Value) (value : Value) : Sealed encoding := - { value - canonical := encoding.encode value - canonical_eq := rfl } +structure SignatureDomain where + recordType : String + storeId : ByteArray + threadOrPrincipal : ByteArray + deriving DecidableEq -theorem sealed_eq_of_same_canonical +structure SignaturePreimage where + canonicalUnsigned : ByteArray + profileVersion : Nat + hashAlgorithm : HashAlgorithm + signatureAlgorithm : SignatureAlgorithm + codec : Codec + domain : SignatureDomain + body : ByteArray + claimedCid : ByteArray + signer : ByteArray + unknownCritical : List String + deriving DecidableEq + +structure SignedEnvelopeCodec where + Envelope : Type + Unsigned : Type + encode : Envelope -> ByteArray + encode_injective : Function.Injective encode + decode : ByteArray -> Option Envelope + decode_exact : forall received envelope, decode received = some envelope -> + encode envelope = received + unsigned : Envelope -> Unsigned + encodeUnsigned : Unsigned -> ByteArray + unsigned_injective : Function.Injective encodeUnsigned + version : Unsigned -> Nat + hash : Unsigned -> HashAlgorithm + signatureAlgorithm : Unsigned -> SignatureAlgorithm + codec : Unsigned -> Codec + domain : Unsigned -> SignatureDomain + body : Unsigned -> ByteArray + claimedCid : Unsigned -> ByteArray + signer : Unsigned -> ByteArray + signatureBytes : Envelope -> ByteArray + unknownCritical : Unsigned -> List String + +def SignedEnvelopeCodec.signaturePreimage + (envelopeCodec : SignedEnvelopeCodec) + (unsigned : envelopeCodec.Unsigned) : SignaturePreimage := + { canonicalUnsigned := envelopeCodec.encodeUnsigned unsigned + profileVersion := envelopeCodec.version unsigned + hashAlgorithm := envelopeCodec.hash unsigned + signatureAlgorithm := envelopeCodec.signatureAlgorithm unsigned + codec := envelopeCodec.codec unsigned + domain := envelopeCodec.domain unsigned + body := envelopeCodec.body unsigned + claimedCid := envelopeCodec.claimedCid unsigned + signer := envelopeCodec.signer unsigned + unknownCritical := envelopeCodec.unknownCritical unsigned } + +structure CryptoBoundary (profile : Profile) where + digest : AllowedHash profile -> ByteArray -> ByteArray + digest_binding : forall leftAllowed rightAllowed left right, + digest leftAllowed left = digest rightAllowed right -> + leftAllowed.algorithm = rightAllowed.algorithm /\ left = right + SignedBy : AllowedSignature profile -> SignaturePreimage -> ByteArray -> Prop + signatureMatches : AllowedSignature profile -> SignaturePreimage -> ByteArray -> Bool + signature_sound : forall allowed preimage signature, + signatureMatches allowed preimage signature = true -> + SignedBy allowed preimage signature + signature_binding : forall leftAllowed rightAllowed left right signature, + SignedBy leftAllowed left signature -> + SignedBy rightAllowed right signature -> + leftAllowed.algorithm = rightAllowed.algorithm /\ left = right + signature_deterministic : forall allowed preimage left right, + SignedBy allowed preimage left -> + SignedBy allowed preimage right -> left = right + +structure VerifiedEnvelope + (profile : Profile) + (envelopeCodec : SignedEnvelopeCodec) + (crypto : CryptoBoundary profile) + (received : ByteArray) where + private verified :: + envelope : envelopeCodec.Envelope + decoded_eq : envelopeCodec.decode received = some envelope + received_exact : envelopeCodec.encode envelope = received + trustedProfile : TrustedProfile profile + version_eq : + envelopeCodec.version (envelopeCodec.unsigned envelope) = profile.version + critical_empty : + envelopeCodec.unknownCritical (envelopeCodec.unsigned envelope) = [] + allowedHash : AllowedHash profile + hash_eq : + allowedHash.algorithm = envelopeCodec.hash (envelopeCodec.unsigned envelope) + allowedSignature : AllowedSignature profile + signature_eq : allowedSignature.algorithm = + envelopeCodec.signatureAlgorithm (envelopeCodec.unsigned envelope) + allowedCodec : AllowedCodec profile + codec_eq : + allowedCodec.codec = envelopeCodec.codec (envelopeCodec.unsigned envelope) + digestEvidence : + envelopeCodec.claimedCid (envelopeCodec.unsigned envelope) = + crypto.digest allowedHash + (envelopeCodec.body (envelopeCodec.unsigned envelope)) + signatureEvidence : crypto.SignedBy allowedSignature + (envelopeCodec.signaturePreimage (envelopeCodec.unsigned envelope)) + (envelopeCodec.signatureBytes envelope) + +def verifyEnvelope + {profile : Profile} + (trustedProfile : TrustedProfile profile) + (envelopeCodec : SignedEnvelopeCodec) + (crypto : CryptoBoundary profile) + (received : ByteArray) : + Option (VerifiedEnvelope profile envelopeCodec crypto received) := + match decodedEq : envelopeCodec.decode received with + | none => none + | some envelope => + let unsigned := envelopeCodec.unsigned envelope + if versionEq : envelopeCodec.version unsigned = profile.version then + if criticalEmpty : envelopeCodec.unknownCritical unsigned = [] then + if hashAllowed : profile.allowsHash (envelopeCodec.hash unsigned) then + let allowedHash : AllowedHash profile := + { algorithm := envelopeCodec.hash unsigned + allowed := hashAllowed } + if signatureAllowed : + profile.allowsSignature (envelopeCodec.signatureAlgorithm unsigned) then + let allowedSignature : AllowedSignature profile := + { algorithm := envelopeCodec.signatureAlgorithm unsigned + allowed := signatureAllowed } + if codecAllowed : profile.allowsCodec (envelopeCodec.codec unsigned) then + let allowedCodec : AllowedCodec profile := + { codec := envelopeCodec.codec unsigned + allowed := codecAllowed } + if digestValid : envelopeCodec.claimedCid unsigned = + crypto.digest allowedHash (envelopeCodec.body unsigned) then + if signatureValid : crypto.signatureMatches allowedSignature + (envelopeCodec.signaturePreimage unsigned) + (envelopeCodec.signatureBytes envelope) = true then + some + { envelope + decoded_eq := decodedEq + received_exact := + envelopeCodec.decode_exact received envelope decodedEq + trustedProfile + version_eq := versionEq + critical_empty := criticalEmpty + allowedHash + hash_eq := rfl + allowedSignature + signature_eq := rfl + allowedCodec + codec_eq := rfl + digestEvidence := digestValid + signatureEvidence := + crypto.signature_sound _ _ _ signatureValid } + else none + else none + else none + else none + else none + else none + else none + +structure Sealed + {Value : Type} + (encoding : CanonicalEncoding Value) + (profile : Profile) + (envelopeCodec : SignedEnvelopeCodec) + (crypto : CryptoBoundary profile) + (received : ByteArray) where + private sealed :: + verified : VerifiedEnvelope profile envelopeCodec crypto received + value : Value + canonical_eq : + envelopeCodec.body (envelopeCodec.unsigned verified.envelope) = + encoding.encode value + +def parseVerified + {Value : Type} + {encoding : CanonicalEncoding Value} + (decoder : CanonicalPayloadDecoder Value encoding) + {profile : Profile} + {envelopeCodec : SignedEnvelopeCodec} + {crypto : CryptoBoundary profile} + {received : ByteArray} + (verified : VerifiedEnvelope profile envelopeCodec crypto received) : + Option (Sealed encoding profile envelopeCodec crypto received) := + let body := envelopeCodec.body (envelopeCodec.unsigned verified.envelope) + match parsedEq : decoder.parse body with + | none => none + | some value => + some + { verified + value + canonical_eq := decoder.parse_exact body value parsedEq } + +def loadEnvelope + {Value : Type} {encoding : CanonicalEncoding Value} - {left right : Sealed encoding} - (h : left.canonical = right.canonical) : left = right := by - cases left with - | mk leftValue leftCanonical leftCanonicalEq => - cases right with - | mk rightValue rightCanonical rightCanonicalEq => - have valueEq : leftValue = rightValue := encoding.injective <| - leftCanonicalEq.symm.trans (h.trans rightCanonicalEq) - subst rightValue - cases leftCanonicalEq - cases rightCanonicalEq - rfl + (decoder : CanonicalPayloadDecoder Value encoding) + {profile : Profile} + (trustedProfile : TrustedProfile profile) + (envelopeCodec : SignedEnvelopeCodec) + (crypto : CryptoBoundary profile) + (received : ByteArray) : + Option (Sealed encoding profile envelopeCodec crypto received) := + match verifyEnvelope trustedProfile envelopeCodec crypto received with + | none => none + | some verified => parseVerified decoder verified + +theorem sealed_value_unique + {Value : Type} + {encoding : CanonicalEncoding Value} + {profile : Profile} + {envelopeCodec : SignedEnvelopeCodec} + {crypto : CryptoBoundary profile} + {received : ByteArray} + (left right : Sealed encoding profile envelopeCodec crypto received) : + left.value = right.value := by + have envelopeEq : left.verified.envelope = right.verified.envelope := + envelopeCodec.encode_injective <| + left.verified.received_exact.trans right.verified.received_exact.symm + have bodyEq : + envelopeCodec.body (envelopeCodec.unsigned left.verified.envelope) = + envelopeCodec.body (envelopeCodec.unsigned right.verified.envelope) := + congrArg (fun envelope => + envelopeCodec.body (envelopeCodec.unsigned envelope)) envelopeEq + apply encoding.injective + exact left.canonical_eq.symm.trans (bodyEq.trans right.canonical_eq) theorem blake3_allowed : Profile.v1.allowsHash .blake3_256 := by decide @@ -125,110 +342,36 @@ theorem dag_cbor_allowed : Profile.v1.allowsCodec .dagCbor := by decide theorem json_not_allowed : Not (Profile.v1.allowsCodec .json) := by decide -structure RawEnvelope where - version : Nat - hash : HashAlgorithm - signature : SignatureAlgorithm - codec : Codec - receivedCanonical : ByteArray - unknownCritical : List String - deriving DecidableEq - -structure VerifiedEnvelope (profile : Profile) (raw : RawEnvelope) where - version_eq : raw.version = profile.version - critical_empty : raw.unknownCritical = [] - allowedHash : AllowedHash profile - hash_eq : allowedHash.algorithm = raw.hash - allowedSignature : AllowedSignature profile - signature_eq : allowedSignature.algorithm = raw.signature - allowedCodec : AllowedCodec profile - codec_eq : allowedCodec.codec = raw.codec - -def verifyEnvelope (profile : Profile) (raw : RawEnvelope) : - Option (VerifiedEnvelope profile raw) := - if versionEq : raw.version = profile.version then - if criticalEmpty : raw.unknownCritical = [] then - if hashAllowed : profile.allowsHash raw.hash then - if signatureAllowed : profile.allowsSignature raw.signature then - if codecAllowed : profile.allowsCodec raw.codec then - some - { version_eq := versionEq - critical_empty := criticalEmpty - allowedHash := - { algorithm := raw.hash - allowed := hashAllowed } - hash_eq := rfl - allowedSignature := - { algorithm := raw.signature - allowed := signatureAllowed } - signature_eq := rfl - allowedCodec := - { codec := raw.codec - allowed := codecAllowed } - codec_eq := rfl } - else none - else none - else none - else none - else none - -theorem verified_hash_allowed - {profile : Profile} {raw : RawEnvelope} - {verified : VerifiedEnvelope profile raw} - (_h : verifyEnvelope profile raw = some verified) : - profile.allowsHash verified.allowedHash.algorithm := - verified.allowedHash.allowed - -theorem verified_signature_allowed - {profile : Profile} {raw : RawEnvelope} - {verified : VerifiedEnvelope profile raw} - (_h : verifyEnvelope profile raw = some verified) : - profile.allowsSignature verified.allowedSignature.algorithm := - verified.allowedSignature.allowed - -theorem verified_codec_allowed - {profile : Profile} {raw : RawEnvelope} - {verified : VerifiedEnvelope profile raw} - (_h : verifyEnvelope profile raw = some verified) : - profile.allowsCodec verified.allowedCodec.codec := - verified.allowedCodec.allowed - -theorem unsupported_version_rejected - {profile : Profile} {raw : RawEnvelope} - (h : Not (raw.version = profile.version)) : - verifyEnvelope profile raw = none := by - simp [verifyEnvelope, h] - -theorem unknown_critical_rejected - {profile : Profile} {raw : RawEnvelope} - (h : Not (raw.unknownCritical = [])) : - verifyEnvelope profile raw = none := by - simp [verifyEnvelope, h] - -def VerifiedEnvelope.receivedCanonical - {profile : Profile} {raw : RawEnvelope} - (_verified : VerifiedEnvelope profile raw) : ByteArray := - raw.receivedCanonical - -theorem verified_preserves_received - {profile : Profile} {raw : RawEnvelope} - (verified : VerifiedEnvelope profile raw) : - verified.receivedCanonical = raw.receivedCanonical := rfl - inductive HashImplementation | blake3 | legacySha1 deriving DecidableEq, Repr -def dispatchHash (allowed : AllowedHash profile) : HashImplementation := - match allowed.algorithm with - | .blake3_256 => .blake3 - | .sha1 => .legacySha1 +theorem trusted_hash_is_blake3 + {profile : Profile} + (trusted : TrustedProfile profile) + (allowed : AllowedHash profile) : + allowed.algorithm = .blake3_256 := by + have profileEq := trusted_profile_is_v1 trusted + subst profile + cases algorithmEq : allowed.algorithm with + | blake3_256 => rfl + | sha1 => + exfalso + apply sha1_not_allowed + simpa [algorithmEq] using allowed.allowed theorem no_v1_sha1_witness (allowed : AllowedHash Profile.v1) : Not (allowed.algorithm = .sha1) := by - intro h - apply sha1_not_allowed - simpa [h] using allowed.allowed + intro algorithmEq + have trustedEq := trusted_hash_is_blake3 TrustedProfile.v1 allowed + simp [algorithmEq] at trustedEq + +def dispatchHash + {profile : Profile} + (trusted : TrustedProfile profile) + (allowed : AllowedHash profile) : HashImplementation := + match trusted_hash_is_blake3 trusted allowed with + | _ => .blake3 end Ceremony.P1 diff --git a/formal/Gate.lean b/formal/Gate.lean new file mode 100644 index 0000000..d622d6f --- /dev/null +++ b/formal/Gate.lean @@ -0,0 +1,43 @@ +def moduleName (path : System.FilePath) : String := + let components := path.components.filter fun component => component != "." + String.intercalate "." <| components.map fun component => + if component.endsWith ".lean" then (component.dropEnd 5).copy else component + +def hasDirectImport (rootSource module : String) : Bool := + (rootSource.splitOn "\n").any fun line => + line.trimAscii.copy == s!"import {module}" + +def proofEscapeErrors + (path : System.FilePath) (source : String) : Array String := Id.run do + let forbidden := #["sor" ++ "ry", "ad" ++ "mit", "ax" ++ "iom"] + let mut errors := #[] + for word in forbidden do + if source.contains word then + errors := errors.push s!"{path}: forbidden proof escape `{word}`" + return errors + +def isFormalRoot (module : String) : Bool := + module == "Ceremony" || module == "Tests" || module == "Gate" + +def main : IO Unit := do + let ceremonyRoot <- IO.FS.readFile "Ceremony.lean" + let testsRoot <- IO.FS.readFile "Tests.lean" + let mut errors := #[] + let paths <- (System.FilePath.mk ".").walkDir fun path => + pure (!path.components.contains ".lake") + for path in paths do + if path.extension == some "lean" && !path.components.contains ".lake" then + let source <- IO.FS.readFile path + errors := errors ++ proofEscapeErrors path source + let module := moduleName path + if !isFormalRoot module && + !hasDirectImport ceremonyRoot module && + !hasDirectImport testsRoot module then + errors := errors.push + s!"{path}: `{module}` is absent from Ceremony.lean and Tests.lean" + if errors.isEmpty then + IO.println "formal gate: all Lean sources and root imports verified" + else + for error in errors do + IO.eprintln s!"formal gate: {error}" + throw <| IO.userError s!"formal gate rejected {errors.size} violation(s)" diff --git a/formal/Tests/P1Counterexamples.lean b/formal/Tests/P1Counterexamples.lean index 33eae8c..a305118 100644 --- a/formal/Tests/P1Counterexamples.lean +++ b/formal/Tests/P1Counterexamples.lean @@ -13,5 +13,6 @@ example (allowed : AllowedHash Profile.v1) : no_v1_sha1_witness allowed example : dispatchHash + TrustedProfile.v1 ({ algorithm := .blake3_256, allowed := blake3_allowed } : AllowedHash Profile.v1) = .blake3 := rfl diff --git a/formal/Tests/SignedObjectContracts.lean b/formal/Tests/SignedObjectContracts.lean index 8cf5e41..1d14d92 100644 --- a/formal/Tests/SignedObjectContracts.lean +++ b/formal/Tests/SignedObjectContracts.lean @@ -18,53 +18,265 @@ example : Profile.v1.allowsCodec .dagCbor := by decide example : Not (Profile.v1.allowsCodec .json) := by decide +def attackerProfile : Profile := + { Profile.v1 with hashes := [.sha1] } + +example (trusted : TrustedProfile attackerProfile) : False := by + cases trusted + def bytesEncoding : CanonicalEncoding ByteArray where encode := id injective := by intro left right h exact h -example (value : ByteArray) : (sealValue bytesEncoding value).value = value := rfl +def bytesDecoder : CanonicalPayloadDecoder ByteArray bytesEncoding where + parse := some + parse_exact := by + intro bytes value parsed + cases parsed + rfl + +def goodReceived : ByteArray := ByteArray.mk #[1] + +def alteredBodyReceived : ByteArray := ByteArray.mk #[2] + +def alteredDomainReceived : ByteArray := ByteArray.mk #[3] + +def alteredSignatureReceived : ByteArray := ByteArray.mk #[4] + +def unsupportedVersionReceived : ByteArray := ByteArray.mk #[5] + +def sha1Received : ByteArray := ByteArray.mk #[6] + +def ecdsaReceived : ByteArray := ByteArray.mk #[7] + +def jsonReceived : ByteArray := ByteArray.mk #[8] + +def unknownCriticalReceived : ByteArray := ByteArray.mk #[9] + +def unrelatedReceived : ByteArray := ByteArray.mk #[10] + +def alteredCidReceived : ByteArray := ByteArray.mk #[11] + +def alteredRecordTypeReceived : ByteArray := ByteArray.mk #[12] + +def alteredStoreReceived : ByteArray := ByteArray.mk #[13] + +def alteredSignerReceived : ByteArray := ByteArray.mk #[14] + +def goodBody : ByteArray := ByteArray.mk #[20, 21] + +def alteredBody : ByteArray := ByteArray.mk #[20, 22] + +def goodCid : ByteArray := goodBody + +def goodSigner : ByteArray := ByteArray.mk #[40, 41] + +def alteredSigner : ByteArray := ByteArray.mk #[40, 42] + +def goodSignature : ByteArray := ByteArray.mk #[50, 51] -example (left right : Sealed bytesEncoding) - (h : left.canonical = right.canonical) : left = right := - sealed_eq_of_same_canonical h +def alteredSignature : ByteArray := ByteArray.mk #[50, 52] -def v1Envelope : RawEnvelope := - { version := 1 - hash := .blake3_256 - signature := .ed25519 +def goodDomain : SignatureDomain := + { recordType := "grant-record" + storeId := ByteArray.mk #[60] + threadOrPrincipal := ByteArray.mk #[61] } + +def alteredDomain : SignatureDomain := + { goodDomain with threadOrPrincipal := ByteArray.mk #[62] } + +def alteredRecordTypeDomain : SignatureDomain := + { goodDomain with recordType := "decision-record" } + +def alteredStoreDomain : SignatureDomain := + { goodDomain with storeId := ByteArray.mk #[63] } + +def testUnsigned (envelope : ByteArray) : ByteArray := + if envelope = alteredSignatureReceived then goodReceived else envelope + +def testEnvelopeCodec : SignedEnvelopeCodec where + Envelope := ByteArray + Unsigned := ByteArray + encode := id + encode_injective := by + intro left right h + exact h + decode := some + decode_exact := by + intro received envelope decoded + cases decoded + rfl + unsigned := testUnsigned + encodeUnsigned := id + unsigned_injective := by + intro left right h + exact h + version := fun unsigned => + if unsigned = unsupportedVersionReceived then 2 else 1 + hash := fun unsigned => + if unsigned = sha1Received then .sha1 else .blake3_256 + signatureAlgorithm := fun unsigned => + if unsigned = ecdsaReceived then .ecdsa else .ed25519 + codec := fun unsigned => + if unsigned = jsonReceived then .json else .dagCbor + domain := fun unsigned => + if unsigned = alteredDomainReceived then alteredDomain + else if unsigned = alteredRecordTypeReceived then alteredRecordTypeDomain + else if unsigned = alteredStoreReceived then alteredStoreDomain + else goodDomain + body := fun unsigned => + if unsigned = alteredBodyReceived then alteredBody else goodBody + claimedCid := fun unsigned => + if unsigned = alteredCidReceived then alteredBody else goodCid + signer := fun unsigned => + if unsigned = alteredSignerReceived then alteredSigner else goodSigner + signatureBytes := fun envelope => + if envelope = alteredSignatureReceived then alteredSignature else goodSignature + unknownCritical := fun unsigned => + if unsigned = unknownCriticalReceived then ["future-authority"] else [] + +def crossCodecReplay : SignedEnvelopeCodec := + { testEnvelopeCodec with + domain := fun (unsigned : ByteArray) => + if unsigned = goodReceived then alteredRecordTypeDomain + else testEnvelopeCodec.domain unsigned } + +def goodPreimage : SignaturePreimage := + { canonicalUnsigned := goodReceived + profileVersion := 1 + hashAlgorithm := .blake3_256 + signatureAlgorithm := .ed25519 codec := .dagCbor - receivedCanonical := ByteArray.mk #[1, 2, 3] + domain := goodDomain + body := goodBody + claimedCid := goodCid + signer := goodSigner unknownCritical := [] } -def unsupportedVersionEnvelope : RawEnvelope := - { v1Envelope with version := 2 } +def exactCrypto : CryptoBoundary Profile.v1 where + digest := fun _allowed body => body + digest_binding := by + intro leftAllowed rightAllowed left right sameDigest + exact + ⟨(trusted_hash_is_blake3 TrustedProfile.v1 leftAllowed).trans + (trusted_hash_is_blake3 TrustedProfile.v1 rightAllowed).symm, + sameDigest⟩ + SignedBy := fun allowed preimage signature => + allowed.algorithm = .ed25519 /\ preimage = goodPreimage /\ + signature = goodSignature + signatureMatches := fun allowed preimage signature => + decide (allowed.algorithm = .ed25519 /\ preimage = goodPreimage /\ + signature = goodSignature) + signature_sound := by + intro allowed preimage signature valid + exact of_decide_eq_true valid + signature_binding := by + intro leftAllowed rightAllowed left right _signature leftValid rightValid + exact + ⟨leftValid.1.trans rightValid.1.symm, + leftValid.2.1.trans rightValid.2.1.symm⟩ + signature_deterministic := by + intro _allowed _preimage left right leftValid rightValid + exact leftValid.2.2.trans rightValid.2.2.symm + +example {received envelope} + (decoded : testEnvelopeCodec.decode received = some envelope) : + testEnvelopeCodec.encode envelope = received := + testEnvelopeCodec.decode_exact received envelope decoded + +example : testEnvelopeCodec.signaturePreimage goodReceived = goodPreimage := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + goodReceived).isSome := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredBodyReceived).isNone := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredDomainReceived).isNone := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredRecordTypeReceived).isNone := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredStoreReceived).isNone := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredSignerReceived).isNone := by + decide + +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredCidReceived).isNone := by + decide -def sha1Envelope : RawEnvelope := - { v1Envelope with hash := .sha1 } +example : + (verifyEnvelope TrustedProfile.v1 crossCodecReplay exactCrypto + goodReceived).isNone := by + decide -def ecdsaEnvelope : RawEnvelope := - { v1Envelope with signature := .ecdsa } +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + alteredSignatureReceived).isNone := by + decide -def jsonEnvelope : RawEnvelope := - { v1Envelope with codec := .json } +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + unsupportedVersionReceived).isNone := by + decide -def unknownCriticalEnvelope : RawEnvelope := - { v1Envelope with unknownCritical := ["future-authority"] } +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + sha1Received).isNone := by + decide -example : (verifyEnvelope Profile.v1 v1Envelope).isSome := by decide +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + ecdsaReceived).isNone := by + decide -example : verifyEnvelope Profile.v1 unsupportedVersionEnvelope = none := by decide +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + jsonReceived).isNone := by + decide -example : verifyEnvelope Profile.v1 sha1Envelope = none := by decide +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + unknownCriticalReceived).isNone := by + decide -example : verifyEnvelope Profile.v1 ecdsaEnvelope = none := by decide +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto + unrelatedReceived).isNone := by + decide -example : verifyEnvelope Profile.v1 jsonEnvelope = none := by decide +example : + (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto goodReceived).map + (fun verified => testEnvelopeCodec.encode verified.envelope) = + some goodReceived := by + decide -example : verifyEnvelope Profile.v1 unknownCriticalEnvelope = none := by decide +example : + (loadEnvelope bytesDecoder TrustedProfile.v1 testEnvelopeCodec exactCrypto + goodReceived).map (fun sealed => sealed.value) = some goodBody := by + decide -example (verified : VerifiedEnvelope Profile.v1 v1Envelope) : - verified.receivedCanonical = v1Envelope.receivedCanonical := - verified_preserves_received verified +example + (left right : + Sealed bytesEncoding Profile.v1 testEnvelopeCodec exactCrypto goodReceived) : + left.value = right.value := + sealed_value_unique left right diff --git a/formal/lakefile.toml b/formal/lakefile.toml index 06b27fd..0fda4e9 100644 --- a/formal/lakefile.toml +++ b/formal/lakefile.toml @@ -13,3 +13,9 @@ name = "CeremonyTests" srcDir = "." roots = ["Tests"] moreLeanArgs = ["-DwarningAsError=true"] + +[[lean_exe]] +name = "formalGate" +srcDir = "." +root = "Gate" +moreLeanArgs = ["-DwarningAsError=true"] diff --git a/justfile b/justfile index dbf1a42..d62046a 100644 --- a/justfile +++ b/justfile @@ -35,11 +35,12 @@ check: cargo test --workspace --no-default-features # Lean proof gate. Mirrors `.github/workflows/formal.yml` and is run by the -# pre-push hook on every platform. Lake reads `formal/lean-toolchain`; the -# project sets `warningAsError`, so `sorry` / `admit` cannot pass this build. +# pre-push hook on every platform. Lake reads `formal/lean-toolchain`; +# warning-as-error and `formalGate` reject proof escapes and omitted modules. [working-directory: 'formal'] check-formal: lake build + lake exe formalGate # Windows AppContainer L3 backend checks — the local mirror of the `check-windows` # job in .github/workflows/ci.yml (and nightly-windows.yml). The `appcontainer_impl` From 084ed2e74ede9a37f0db6177ae51b42094e010fe Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Wed, 15 Jul 2026 23:44:08 -0400 Subject: [PATCH 5/6] docs(formal): record P1 review readiness Mark the rebased, independently reviewed P1 implementation and stacked PR creation steps complete. Co-Authored-By: OpenAI GPT-5 --- .../plans/2026-07-16-p1-signed-object-formalization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md index c74a6e7..bf69d0a 100644 --- a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md +++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md @@ -497,7 +497,7 @@ Run: `git log --format=full origin/feat/formal-ceremony-kernel..HEAD` Expected: every commit is authored by Shawn Hartsock and contains the OpenAI GPT-5 co-author trailer. -- [ ] **Step 4: Push normally and open the PR** +- [x] **Step 4: Push normally and open the PR** Attempt a normal push first. If the unchanged parent branch still fails the repository hook after all P1-owned gates pass, use only the author's explicit From 473339733b870f11fbf3de0ad817d1ad5cdd0b0e Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Wed, 15 Jul 2026 23:47:42 -0400 Subject: [PATCH 6/6] fix(ci): resolve lake path in Windows formal gate Run the post-action formal gate through Bash with elan's explicit user-bin path because lean-action does not persist lake onto the following Windows PowerShell step. Co-Authored-By: OpenAI GPT-5 --- .github/workflows/formal.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index cc6dd7c..2146ce1 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -44,4 +44,6 @@ jobs: use-mathlib-cache: false - name: Reject proof escapes and omitted modules working-directory: formal - run: lake exe formalGate + shell: bash + run: | + "$HOME/.elan/bin/lake" exe formalGate