formal(refinement): Tier-3 bridge — extracted Rust refines Authority.lean (Aeneas)

docs/spec/ROADMAP.md

@@ -34,7 +34,7 @@ Tamarin/ProVerif, Tier-1 assumed crypto).
 | 0.3 | **Lean P0 authority model** — `formal/Ceremony/P0/Authority.lean`, 25 theorems, 0 `sorry` | ✅ |
 | 0.4 | **TLA+ store model** — `formal/tla/CeremonyStore.tla` (CAS + anti-rollback invariants) | ✅ |
 | 0.5 | **Lean P1 signed-object contracts** + Lake project + `formalGate` proof-escape gate + CI (`formal.yml`) + `just check-formal` | ✅ (harvested from PR #233 / GPT-5, integrated with P0) |
-| 0.6 | Aeneas/Charon toolchain green on gnuc (opam/OCaml leg) | pending (`../TOOLCHAIN.md`) |
+| 0.6 | Aeneas/Charon toolchain green on gnuc (opam/OCaml leg) | ✅ built on gnuc; `agent-bridle-ceremony` extracts Rust→LLBC→Lean and the first refinement proofs pass (`formal/refinement/`) |
 
 **Exit:** ADRs merged; the unified Lean project (P0 + P1) builds under CI + the
 pre-push gate; TLA+ store model in place; only the opam leg remains before
@@ -57,6 +57,11 @@ formal proof → conformance vectors.
   precedence + the gate-acceptance checklist. **Charon extracts the Rust
   kernel; Aeneas proves it refines `Authority.lean`.** *Gate:* PO-1/3/4/5
   + the refinement bridge theorem; CI blocks any kernel that fails it.
+  - *Started:* `agent-bridle-ceremony` (`authority.rs` + `boundary.rs`) is the
+    pure kernel; `formal/refinement/` proves the `meet`/`attenuate` laws on the
+    Charon/Aeneas-extracted code. **Remaining:** rewrite `resolve` from an
+    iterator-`fold` (Aeneas axiomatizes slice iterators, so it won't reduce) to
+    explicit recursion, then extend the refinement proof to cover it.
 - **1d Conformance vectors.** `tests/vectors/*.json` — positive **and
   negative** — the cross-language behavioral contract. *This unblocks the
   "held" wire freeze.*

formal/Gate.lean

@@ -23,8 +23,14 @@ def main : IO Unit := do
   let ceremonyRoot <- IO.FS.readFile "Ceremony.lean"
   let testsRoot <- IO.FS.readFile "Tests.lean"
   let mut errors := #[]
+  -- `refinement/` is a SEPARATE, heavy Lake project (Aeneas + mathlib + Aeneas-
+  -- generated code that legitimately uses opaque externals, plus a machine-local
+  -- `aeneas-lean` symlink into the Aeneas source). It is gated on its own by
+  -- `just check-refinement`, NOT by this fast mathlib-free gate — so prune it.
+  -- (This comment avoids the literal escape words on purpose — the gate scans
+  -- its own source too.)
   let paths <- (System.FilePath.mk ".").walkDir fun path =>
-    pure (!path.components.contains ".lake")
+    pure (!path.components.contains ".lake" && !path.components.contains "refinement")
   for path in paths do
     if path.extension == some "lean" && !path.components.contains ".lake" then
       let source <- IO.FS.readFile path

formal/refinement/.gitignore

@@ -0,0 +1,6 @@
+# Lake build output
+/.lake/
+# machine-local symlink to <aeneas>/backends/lean (created by setup.sh)
+/aeneas-lean
+# TLC-style scratch, extraction temp
+*.llbc

formal/refinement/AgentBridleCeremony.lean

@@ -0,0 +1 @@
+import AgentBridleCeremony.Funs

formal/refinement/AgentBridleCeremony/FunsExternal.lean

@@ -0,0 +1,52 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [agent_bridle_ceremony]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
+import Aeneas
+import AgentBridleCeremony.Types
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+open agent_bridle_ceremony
+
+/-- [core::hash::impls::{impl core::hash::Hash for isize}::hash]:
+    Source: '/rustc/library/core/src/hash/mod.rs', lines 812:16-812:56
+    Name pattern: [core::hash::impls::{core::hash::Hash<isize>}::hash]
+    Visibility: public -/
+@[rust_fun "core::hash::impls::{core::hash::Hash<isize>}::hash"]
+axiom Isize.Insts.CoreHashHash.hash
+  {H : Type} (HasherInst : core.hash.Hasher H) : Std.Isize → H → Result H
+
+/-- [core::hash::impls::{impl core::hash::Hash for bool}::hash]:
+    Source: '/rustc/library/core/src/hash/mod.rs', lines 848:8-848:48
+    Name pattern: [core::hash::impls::{core::hash::Hash<bool>}::hash]
+    Visibility: public -/
+@[rust_fun "core::hash::impls::{core::hash::Hash<bool>}::hash"]
+axiom Bool.Insts.CoreHashHash.hash
+  {H : Type} (HasherInst : core.hash.Hasher H) : Bool → H → Result H
+
+/-- [core::slice::iter::{impl core::iter::traits::iterator::Iterator<&'a T> for core::slice::iter::Iter<'a, T>}::fold]:
+    Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 259:12-261:49
+    Name pattern: [core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::Iter<'a, @T>, &'a @T>}::fold]
+    Visibility: public -/
+@[rust_fun
+  "core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::Iter<'a, @T>, &'a @T>}::fold"]
+axiom core.slice.iter.Iter.Insts.CoreIterTraitsIteratorIteratorSharedAT.fold
+  {T : Type} {B : Type} {F : Type} (opsfunctionFnMutFPairBSharedATBInst :
+  core.ops.function.FnMut F (B × T) B) :
+  core.slice.iter.Iter T → B → F → Result B
+
+/-- [core::slice::{[T]}::split_first]:
+    Source: '/rustc/library/core/src/slice/mod.rs', lines 198:4-198:57
+    Name pattern: [core::slice::{[@T]}::split_first]
+    Visibility: public -/
+@[rust_fun "core::slice::{[@T]}::split_first"]
+axiom core.slice.Slice.split_first
+  {T : Type} : Slice T → Result (Option (T × (Slice T)))
+

formal/refinement/AgentBridleCeremony/Types.lean

@@ -0,0 +1,78 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [agent_bridle_ceremony]: type definitions
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+namespace agent_bridle_ceremony
+
+/-- [agent_bridle_ceremony::authority::Effect]
+    Source: 'agent-bridle-ceremony/src/authority.rs', lines 19:0-22:1
+    Visibility: public -/
+@[discriminant isize]
+inductive authority.Effect where
+| Deny : authority.Effect
+| Allow : authority.Effect
+
+/-- [agent_bridle_ceremony::authority::Assurance]
+    Source: 'agent-bridle-ceremony/src/authority.rs', lines 28:0-32:1
+    Visibility: public -/
+@[discriminant isize]
+inductive authority.Assurance where
+| None : authority.Assurance
+| Presence : authority.Assurance
+| Hardware : authority.Assurance
+
+/-- [agent_bridle_ceremony::authority::Scope]
+    Source: 'agent-bridle-ceremony/src/authority.rs', lines 37:0-41:1
+    Visibility: public -/
+@[discriminant isize]
+inductive authority.Scope where
+| Once : authority.Scope
+| Session : authority.Scope
+| Durable : authority.Scope
+
+/-- [agent_bridle_ceremony::authority::Authority]
+    Source: 'agent-bridle-ceremony/src/authority.rs', lines 107:0-111:1
+    Visibility: public -/
+structure authority.Authority where
+  effect : authority.Effect
+  assurance : authority.Assurance
+  scope : authority.Scope
+
+/-- [agent_bridle_ceremony::authority::Resolution]
+    Source: 'agent-bridle-ceremony/src/authority.rs', lines 158:0-161:1
+    Visibility: public -/
+@[discriminant isize]
+inductive authority.Resolution where
+| NeedsDecision : authority.Resolution
+| Decided : authority.Authority → authority.Resolution
+
+/-- [agent_bridle_ceremony::authority::resolve::closure]
+    Source: 'agent-bridle-ceremony/src/authority.rs', lines 171:76-171:97 -/
+@[reducible]
+def authority.resolve.closure := Unit
+
+/-- [agent_bridle_ceremony::boundary::Fence]
+    Source: 'agent-bridle-ceremony/src/boundary.rs', lines 26:0-29:1
+    Visibility: public -/
+@[discriminant isize]
+inductive boundary.Fence where
+| Advisory : boundary.Fence
+| Kernel : boundary.Fence
+
+/-- [agent_bridle_ceremony::boundary::Request]
+    Source: 'agent-bridle-ceremony/src/boundary.rs', lines 39:0-41:1
+    Visibility: public -/
+structure boundary.Request where
+  dynamic : Bool
+
+end agent_bridle_ceremony

formal/refinement/README.md

@@ -0,0 +1,65 @@
+# formal/refinement/ — the Tier-3 refinement bridge
+
+Proves that the **extracted Rust** of `agent-bridle-ceremony` satisfies the
+`Authority.lean` algebraic laws. This is the concrete instance of the
+roadmap's central claim: *the Rust waist refines the Lean model.*
+
+## The pipeline
+
+```
+agent-bridle-ceremony (Rust)
+      │  charon cargo --preset=aeneas        (Rust → LLBC)
+      ▼
+agent_bridle_ceremony.llbc
+      │  aeneas -backend lean                (LLBC → Lean)
+      ▼
+AgentBridleCeremony/{Types,Funs,FunsExternal}.lean   ← GENERATED (do not hand-edit)
+      │  Refinement.lean                     ← HAND-WRITTEN proofs
+      ▼
+lake build                                    ✅ laws hold on the extracted code
+```
+
+`Refinement.lean` re-proves, on the **extracted monadic functions**, the same
+laws `formal/Ceremony/P0/Authority.lean` proves abstractly: axis + product
+`meet` commutativity/idempotence and attenuation (`(a⊓c) ⊓ a = a⊓c`, i.e.
+`(a⊓c) ≤ a` under the meet-order `Authority.lean` defines). All by
+`cases <;> rfl` over the finite domain — the extraction reduces cleanly.
+
+## Why this is a separate, heavier tier
+
+The generated code `import Aeneas`, which pulls the Aeneas Lean backend **and
+mathlib**. That is far heavier than the fast, mathlib-free `formal/` project
+(which builds in seconds and IS in the mandatory pre-push gate). So this tier is
+**not** in the mandatory gate; run it on a machine with the toolchain via
+`just check-refinement` (which skips gracefully if the toolchain is absent).
+
+## Verifying locally
+
+```sh
+# 1. Build the Charon/Aeneas toolchain once (docs/TOOLCHAIN.md §2).
+# 2. Link the Aeneas Lean backend (honours AENEAS_LEAN_LIB):
+./setup.sh
+# 3. Check the proofs:
+lake build            # or: just check-refinement (from repo root)
+```
+
+`aeneas-lean` (the symlink `setup.sh` creates) and `.lake/` are gitignored — no
+absolute path is committed.
+
+## Regenerating after a kernel change
+
+```sh
+./regenerate.sh       # re-extracts the generated files; review the diff
+lake build            # re-check the proofs against the new extraction
+```
+
+Generated against the Aeneas commit in `aeneas-commit.txt`.
+
+## Known gap: `resolve`
+
+`resolve` uses a slice iterator (`iter().fold(...)`), which Aeneas models with
+the **opaque axioms** `core.slice.iter.Iter…fold` / `split_first` (see
+`AgentBridleCeremony/FunsExternal.lean`). Opaque ⇒ it does not reduce ⇒ its laws
+are not yet provable here. The fix is to rewrite `resolve` in the Rust kernel as
+**explicit recursion** (no iterator), which extracts to a real recursive
+function. Tracked as a follow-up; the algebra (`meet`/`attenuate`) is complete.

formal/refinement/Refinement.lean

@@ -0,0 +1,55 @@
+-- Refinement proofs: the Authority.lean algebraic laws, discharged on the
+-- EXTRACTED (Charon/Aeneas) implementation of `agent-bridle-ceremony`. Same
+-- laws as formal/Ceremony/P0/Authority.lean, now on the actual Rust as
+-- extracted — the Tier-3 refinement bridge, machine-checked.
+--
+-- The meet-order is stated as Authority.lean defines it: `a ≤ b  ↔  a ⊓ b = a`.
+-- So attenuation is the absorption identity `(a⊓c) ⊓ a = a⊓c`, pure `meet`.
+--
+-- `resolve` is intentionally absent: its extraction goes through the opaque
+-- axioms `core.slice.iter.Iter...fold` / `split_first` (Aeneas axiomatizes slice
+-- iterators), so it does not reduce. Making it provable means rewriting `resolve`
+-- as explicit recursion in the Rust kernel (tracked follow-up).
+import AgentBridleCeremony.Funs
+open Aeneas Aeneas.Std Result
+open agent_bridle_ceremony
+
+namespace CeremonyRefinement
+
+-- ── axis meet: commutative, idempotent ──
+theorem effect_meet_comm (a b : authority.Effect) :
+    authority.Effect.meet a b = authority.Effect.meet b a := by cases a <;> cases b <;> rfl
+theorem assurance_meet_comm (a b : authority.Assurance) :
+    authority.Assurance.meet a b = authority.Assurance.meet b a := by cases a <;> cases b <;> rfl
+theorem scope_meet_comm (a b : authority.Scope) :
+    authority.Scope.meet a b = authority.Scope.meet b a := by cases a <;> cases b <;> rfl
+theorem effect_meet_idem (a : authority.Effect) : authority.Effect.meet a a = ok a := by cases a <;> rfl
+theorem assurance_meet_idem (a : authority.Assurance) : authority.Assurance.meet a a = ok a := by cases a <;> rfl
+theorem scope_meet_idem (a : authority.Scope) : authority.Scope.meet a a = ok a := by cases a <;> rfl
+
+-- ── product meet: commutative (L1 carrier), idempotent ──
+theorem authority_meet_comm (a b : authority.Authority) :
+    authority.Authority.meet a b = authority.Authority.meet b a := by
+  obtain ⟨e1, a1, s1⟩ := a; obtain ⟨e2, a2, s2⟩ := b
+  cases e1 <;> cases a1 <;> cases s1 <;> cases e2 <;> cases a2 <;> cases s2 <;> rfl
+theorem authority_meet_idem (a : authority.Authority) : authority.Authority.meet a a = ok a := by
+  obtain ⟨e, av, s⟩ := a; cases e <;> cases av <;> cases s <;> rfl
+
+-- ── attenuation (L4 / PO-4): the meet is ≤ each input — never amplifies.
+-- `x ≤ y  ↔  x ⊓ y = x`, so this is absorption: (a⊓c) ⊓ a = a⊓c, (a⊓c) ⊓ c = a⊓c. ──
+theorem attenuate_le_input (a c : authority.Authority) :
+    (do let m ← authority.Authority.meet a c; authority.Authority.meet m a)
+      = authority.Authority.meet a c := by
+  obtain ⟨e1, a1, s1⟩ := a; obtain ⟨e2, a2, s2⟩ := c
+  cases e1 <;> cases a1 <;> cases s1 <;> cases e2 <;> cases a2 <;> cases s2 <;> rfl
+theorem attenuate_le_ceiling (a c : authority.Authority) :
+    (do let m ← authority.Authority.meet a c; authority.Authority.meet m c)
+      = authority.Authority.meet a c := by
+  obtain ⟨e1, a1, s1⟩ := a; obtain ⟨e2, a2, s2⟩ := c
+  cases e1 <;> cases a1 <;> cases s1 <;> cases e2 <;> cases a2 <;> cases s2 <;> rfl
+
+-- ── attenuate is exactly meet (the extracted definition) ──
+theorem attenuate_is_meet (a c : authority.Authority) :
+    authority.Authority.attenuate a c = authority.Authority.meet a c := by rfl
+
+end CeremonyRefinement

formal/refinement/aeneas-commit.txt

@@ -0,0 +1 @@
+bc2eb6f941369fa3c695e30598b5758b11e4f0de