formal: prove P1 signed-object contracts

.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 + integrity gate)"
+just check-formal
+
 echo "[pre-push] running 'just check-windows' (AppContainer backend + kernel proofs; skips off Windows)"
 just check-windows
 

.github/workflows/formal.yml

@@ -0,0 +1,49 @@
+# Ceremony Suite formal proof gate.
+#
+# HOOK PARITY: `just check-formal` and `.githooks/pre-push` run the same
+# `lake build` plus `lake exe formalGate` 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
+      - name: Reject proof escapes and omitted modules
+        working-directory: formal
+        shell: bash
+        run: |
+          "$HOME/.elan/bin/lake" exe formalGate

.gitignore

@@ -3,6 +3,9 @@
 **/target
 Cargo.lock.orig
 
+# Lean / Lake
+**/.lake/
+
 # Coverage
 *.profraw
 /coverage

docs/TOOLCHAIN.md

@@ -9,10 +9,11 @@ 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,
-then verify, then update this line.
+**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 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.
 
 ---
 
@@ -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 build plus proof-escape/import-completeness gate
 ```
 
 `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)
 
@@ -131,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).