From 53d18630e68a0f1388a18b0276179ec61fbed1bb Mon Sep 17 00:00:00 2001 From: Shawn Hartsock Date: Fri, 17 Jul 2026 02:26:06 -0400 Subject: [PATCH] =?UTF-8?q?formal(refinement):=20Tier-3=20bridge=20?= =?UTF-8?q?=E2=80=94=20extracted=20Rust=20refines=20Authority.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stands up the Charon/Aeneas refinement toolchain (roadmap Phase 0.6) and proves, on the ACTUAL extracted Rust of agent-bridle-ceremony, the Authority.lean laws. Pipeline (formal/refinement/): charon cargo --preset=aeneas → LLBC → aeneas -backend lean → generated Types/Funs/FunsExternal → hand-written Refinement.lean → lake build ✅. 12 refinement theorems, all by `cases <;> rfl` over the finite domain (the extracted monadic functions reduce cleanly): - axis + product `meet` commutativity and idempotence - attenuation (L4/PO-4) as absorption `(a⊓c) ⊓ a = a⊓c`, i.e. `(a⊓c) ≤ a` under the meet-order Authority.lean defines - `attenuate = meet` (the extracted definition) This is the concrete instance of the roadmap's central claim: the Rust waist refines the Lean model. The frozen algebra is no longer just an abstract Lean theorem set — the shipping implementation provably obeys it. Design/plumbing: - Separate, HEAVY tier: the generated code imports Aeneas + mathlib, so this is NOT in the mandatory pre-push/CI gate (mathlib is too heavy per push). Run via `just check-refinement` (skips gracefully without the toolchain). - Portable: `aeneas-lean` is a gitignored symlink created by setup.sh (honours AENEAS_LEAN_LIB) — no absolute path / username committed. - regenerate.sh reproduces the extraction; aeneas-commit.txt pins provenance. - Toolchain gotcha handled: this harness overrides CARGO_TARGET_DIR, which breaks Charon's Makefile copy step; regenerate.sh unsets it. KNOWN GAP: `resolve` uses a slice iterator (`iter().fold`), which Aeneas axiomatizes (opaque `fold`/`split_first`), so it does not reduce and its laws are not yet proven here. Fix = rewrite `resolve` as explicit recursion in the kernel (ROADMAP 1c follow-up). NOTE: the generated Lean was extracted from a crate including boundary.rs (the enforcement-boundary module), which landed on the #241 branch AFTER #241 merged (authority-only). Pairs with the boundary PR; merge that first for regenerate.sh provenance parity. Co-Authored-By: Claude Opus 4.8 --- docs/spec/ROADMAP.md | 7 +- formal/Gate.lean | 8 +- formal/refinement/.gitignore | 6 + formal/refinement/AgentBridleCeremony.lean | 1 + .../refinement/AgentBridleCeremony/Funs.lean | 1061 +++++++++++++++++ .../AgentBridleCeremony/FunsExternal.lean | 52 + .../refinement/AgentBridleCeremony/Types.lean | 78 ++ formal/refinement/README.md | 65 + formal/refinement/Refinement.lean | 55 + formal/refinement/aeneas-commit.txt | 1 + formal/refinement/lake-manifest.json | 103 ++ formal/refinement/lakefile.lean | 23 + formal/refinement/lean-toolchain | 1 + formal/refinement/regenerate.sh | 26 + formal/refinement/setup.sh | 15 + justfile | 19 + 16 files changed, 1519 insertions(+), 2 deletions(-) create mode 100644 formal/refinement/.gitignore create mode 100644 formal/refinement/AgentBridleCeremony.lean create mode 100644 formal/refinement/AgentBridleCeremony/Funs.lean create mode 100644 formal/refinement/AgentBridleCeremony/FunsExternal.lean create mode 100644 formal/refinement/AgentBridleCeremony/Types.lean create mode 100644 formal/refinement/README.md create mode 100644 formal/refinement/Refinement.lean create mode 100644 formal/refinement/aeneas-commit.txt create mode 100644 formal/refinement/lake-manifest.json create mode 100644 formal/refinement/lakefile.lean create mode 100644 formal/refinement/lean-toolchain create mode 100755 formal/refinement/regenerate.sh create mode 100755 formal/refinement/setup.sh diff --git a/docs/spec/ROADMAP.md b/docs/spec/ROADMAP.md index 0aa4ec4..5864fc3 100644 --- a/docs/spec/ROADMAP.md +++ b/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.* diff --git a/formal/Gate.lean b/formal/Gate.lean index d622d6f..732abb2 100644 --- a/formal/Gate.lean +++ b/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 diff --git a/formal/refinement/.gitignore b/formal/refinement/.gitignore new file mode 100644 index 0000000..5c7b035 --- /dev/null +++ b/formal/refinement/.gitignore @@ -0,0 +1,6 @@ +# Lake build output +/.lake/ +# machine-local symlink to /backends/lean (created by setup.sh) +/aeneas-lean +# TLC-style scratch, extraction temp +*.llbc diff --git a/formal/refinement/AgentBridleCeremony.lean b/formal/refinement/AgentBridleCeremony.lean new file mode 100644 index 0000000..7a9fd02 --- /dev/null +++ b/formal/refinement/AgentBridleCeremony.lean @@ -0,0 +1 @@ +import AgentBridleCeremony.Funs diff --git a/formal/refinement/AgentBridleCeremony/Funs.lean b/formal/refinement/AgentBridleCeremony/Funs.lean new file mode 100644 index 0000000..c550823 --- /dev/null +++ b/formal/refinement/AgentBridleCeremony/Funs.lean @@ -0,0 +1,1061 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [agent_bridle_ceremony]: function definitions +import Aeneas +import AgentBridleCeremony.Types +import AgentBridleCeremony.FunsExternal +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 + +/- You can remove the following line by using the CLI option `-all-computable`: -/ +noncomputable section + +namespace agent_bridle_ceremony + +/-- [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Effect}::clone]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:9-18:14 + Visibility: public -/ +def authority.Effect.Insts.CoreCloneClone.clone + (self : authority.Effect) : Result authority.Effect := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:9-18:14 -/ +@[reducible] +def authority.Effect.Insts.CoreCloneClone : core.clone.Clone authority.Effect + := { + clone := authority.Effect.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::Copy for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:16-18:20 -/ +@[reducible] +def authority.Effect.Insts.CoreMarkerCopy : core.marker.Copy authority.Effect + := { + cloneInst := authority.Effect.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Effect}::fmt]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:22-18:27 + Visibility: public -/ +def authority.Effect.Insts.CoreFmtDebug.fmt + (self : authority.Effect) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + match self with + | authority.Effect.Deny => core.fmt.Formatter.write_str f (toStr "Deny") + | authority.Effect.Allow => core.fmt.Formatter.write_str f (toStr "Allow") + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:22-18:27 -/ +@[reducible] +def authority.Effect.Insts.CoreFmtDebug : core.fmt.Debug authority.Effect := { + fmt := authority.Effect.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:29-18:38 -/ +@[reducible] +def authority.Effect.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq authority.Effect := { +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Effect}::eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:29-18:38 + Visibility: public -/ +def authority.Effect.Insts.CoreCmpPartialEqEffect.eq + (self : authority.Effect) (other : authority.Effect) : Result Bool := do + let self1 := read_discriminant self + let other1 := read_discriminant other + ok (self1 = other1) + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:29-18:38 -/ +@[reducible] +def authority.Effect.Insts.CoreCmpPartialEqEffect : core.cmp.PartialEq + authority.Effect authority.Effect := { + eq := authority.Effect.Insts.CoreCmpPartialEqEffect.eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Effect}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:40-18:42 + Visibility: public -/ +def authority.Effect.Insts.CoreCmpEq.assert_fields_are_eq + (self : authority.Effect) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:40-18:42 -/ +@[reducible] +def authority.Effect.Insts.CoreCmpEq : core.cmp.Eq authority.Effect := { + partialEqInst := authority.Effect.Insts.CoreCmpPartialEqEffect + assert_fields_are_eq := authority.Effect.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Effect}::hash]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:44-18:48 + Visibility: public -/ +def authority.Effect.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : authority.Effect) (state : __H) : + Result __H + := do + let self1 := read_discriminant self + Isize.Insts.CoreHashHash.hash corehashHasherInst self1 state + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Effect}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 18:44-18:48 -/ +@[reducible] +def authority.Effect.Insts.CoreHashHash : core.hash.Hash authority.Effect := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + authority.Effect.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Assurance}::clone]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:9-27:14 + Visibility: public -/ +def authority.Assurance.Insts.CoreCloneClone.clone + (self : authority.Assurance) : Result authority.Assurance := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:9-27:14 -/ +@[reducible] +def authority.Assurance.Insts.CoreCloneClone : core.clone.Clone + authority.Assurance := { + clone := authority.Assurance.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::Copy for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:16-27:20 -/ +@[reducible] +def authority.Assurance.Insts.CoreMarkerCopy : core.marker.Copy + authority.Assurance := { + cloneInst := authority.Assurance.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Assurance}::fmt]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:22-27:27 + Visibility: public -/ +def authority.Assurance.Insts.CoreFmtDebug.fmt + (self : authority.Assurance) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + match self with + | authority.Assurance.None => core.fmt.Formatter.write_str f (toStr "None") + | authority.Assurance.Presence => + core.fmt.Formatter.write_str f (toStr "Presence") + | authority.Assurance.Hardware => + core.fmt.Formatter.write_str f (toStr "Hardware") + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:22-27:27 -/ +@[reducible] +def authority.Assurance.Insts.CoreFmtDebug : core.fmt.Debug authority.Assurance + := { + fmt := authority.Assurance.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:29-27:38 -/ +@[reducible] +def authority.Assurance.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq authority.Assurance := { +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Assurance}::eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:29-27:38 + Visibility: public -/ +def authority.Assurance.Insts.CoreCmpPartialEqAssurance.eq + (self : authority.Assurance) (other : authority.Assurance) : + Result Bool + := do + let self1 := read_discriminant self + let other1 := read_discriminant other + ok (self1 = other1) + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:29-27:38 -/ +@[reducible] +def authority.Assurance.Insts.CoreCmpPartialEqAssurance : core.cmp.PartialEq + authority.Assurance authority.Assurance := { + eq := authority.Assurance.Insts.CoreCmpPartialEqAssurance.eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Assurance}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:40-27:42 + Visibility: public -/ +def authority.Assurance.Insts.CoreCmpEq.assert_fields_are_eq + (self : authority.Assurance) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:40-27:42 -/ +@[reducible] +def authority.Assurance.Insts.CoreCmpEq : core.cmp.Eq authority.Assurance := { + partialEqInst := authority.Assurance.Insts.CoreCmpPartialEqAssurance + assert_fields_are_eq := + authority.Assurance.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Assurance}::hash]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:44-27:48 + Visibility: public -/ +def authority.Assurance.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : authority.Assurance) (state : __H) : + Result __H + := do + let self1 := read_discriminant self + Isize.Insts.CoreHashHash.hash corehashHasherInst self1 state + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Assurance}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 27:44-27:48 -/ +@[reducible] +def authority.Assurance.Insts.CoreHashHash : core.hash.Hash authority.Assurance + := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + authority.Assurance.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Scope}::clone]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:9-36:14 + Visibility: public -/ +def authority.Scope.Insts.CoreCloneClone.clone + (self : authority.Scope) : Result authority.Scope := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:9-36:14 -/ +@[reducible] +def authority.Scope.Insts.CoreCloneClone : core.clone.Clone authority.Scope + := { + clone := authority.Scope.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::Copy for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:16-36:20 -/ +@[reducible] +def authority.Scope.Insts.CoreMarkerCopy : core.marker.Copy authority.Scope + := { + cloneInst := authority.Scope.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Scope}::fmt]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:22-36:27 + Visibility: public -/ +def authority.Scope.Insts.CoreFmtDebug.fmt + (self : authority.Scope) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + match self with + | authority.Scope.Once => core.fmt.Formatter.write_str f (toStr "Once") + | authority.Scope.Session => core.fmt.Formatter.write_str f (toStr "Session") + | authority.Scope.Durable => core.fmt.Formatter.write_str f (toStr "Durable") + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:22-36:27 -/ +@[reducible] +def authority.Scope.Insts.CoreFmtDebug : core.fmt.Debug authority.Scope := { + fmt := authority.Scope.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:29-36:38 -/ +@[reducible] +def authority.Scope.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq authority.Scope := { +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Scope}::eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:29-36:38 + Visibility: public -/ +def authority.Scope.Insts.CoreCmpPartialEqScope.eq + (self : authority.Scope) (other : authority.Scope) : Result Bool := do + let self1 := read_discriminant self + let other1 := read_discriminant other + ok (self1 = other1) + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:29-36:38 -/ +@[reducible] +def authority.Scope.Insts.CoreCmpPartialEqScope : core.cmp.PartialEq + authority.Scope authority.Scope := { + eq := authority.Scope.Insts.CoreCmpPartialEqScope.eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Scope}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:40-36:42 + Visibility: public -/ +def authority.Scope.Insts.CoreCmpEq.assert_fields_are_eq + (self : authority.Scope) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:40-36:42 -/ +@[reducible] +def authority.Scope.Insts.CoreCmpEq : core.cmp.Eq authority.Scope := { + partialEqInst := authority.Scope.Insts.CoreCmpPartialEqScope + assert_fields_are_eq := authority.Scope.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Scope}::hash]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:44-36:48 + Visibility: public -/ +def authority.Scope.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : authority.Scope) (state : __H) : + Result __H + := do + let self1 := read_discriminant self + Isize.Insts.CoreHashHash.hash corehashHasherInst self1 state + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Scope}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 36:44-36:48 -/ +@[reducible] +def authority.Scope.Insts.CoreHashHash : core.hash.Hash authority.Scope := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + authority.Scope.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Effect}::rank]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 45:4-50:5 + Visibility: public -/ +def authority.Effect.rank (self : authority.Effect) : Result Std.U8 := do + match self with + | authority.Effect.Deny => ok 0#u8 + | authority.Effect.Allow => ok 1#u8 + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Effect}::meet]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 53:4-59:5 + Visibility: public -/ +def authority.Effect.meet + (self : authority.Effect) (other : authority.Effect) : + Result authority.Effect + := do + let i ← authority.Effect.rank self + let i1 ← authority.Effect.rank other + if i <= i1 + then ok self + else ok other + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Effect}::ALL] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 62:4-62:63 + Visibility: public -/ +@[global_simps, irreducible] +def authority.Effect.ALL : Array authority.Effect 2#usize := + Array.make 2#usize [ authority.Effect.Deny, authority.Effect.Allow ] + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Assurance}::rank]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 66:4-72:5 + Visibility: public -/ +def authority.Assurance.rank (self : authority.Assurance) : Result Std.U8 := do + match self with + | authority.Assurance.None => ok 0#u8 + | authority.Assurance.Presence => ok 1#u8 + | authority.Assurance.Hardware => ok 2#u8 + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Assurance}::meet]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 74:4-80:5 + Visibility: public -/ +def authority.Assurance.meet + (self : authority.Assurance) (other : authority.Assurance) : + Result authority.Assurance + := do + let i ← authority.Assurance.rank self + let i1 ← authority.Assurance.rank other + if i <= i1 + then ok self + else ok other + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Assurance}::ALL] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 82:4-82:96 + Visibility: public -/ +@[global_simps, irreducible] +def authority.Assurance.ALL : Array authority.Assurance 3#usize := + Array.make 3#usize [ + authority.Assurance.None, authority.Assurance.Presence, + authority.Assurance.Hardware + ] + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Scope}::rank]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 86:4-92:5 + Visibility: public -/ +def authority.Scope.rank (self : authority.Scope) : Result Std.U8 := do + match self with + | authority.Scope.Once => ok 0#u8 + | authority.Scope.Session => ok 1#u8 + | authority.Scope.Durable => ok 2#u8 + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Scope}::meet]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 94:4-100:5 + Visibility: public -/ +def authority.Scope.meet + (self : authority.Scope) (other : authority.Scope) : + Result authority.Scope + := do + let i ← authority.Scope.rank self + let i1 ← authority.Scope.rank other + if i <= i1 + then ok self + else ok other + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Scope}::ALL] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 102:4-102:78 + Visibility: public -/ +@[global_simps, irreducible] +def authority.Scope.ALL : Array authority.Scope 3#usize := + Array.make 3#usize [ + authority.Scope.Once, authority.Scope.Session, authority.Scope.Durable + ] + +/-- [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Authority}::clone]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:9-106:14 + Visibility: public -/ +def authority.Authority.Insts.CoreCloneClone.clone + (self : authority.Authority) : Result authority.Authority := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:9-106:14 -/ +@[reducible] +def authority.Authority.Insts.CoreCloneClone : core.clone.Clone + authority.Authority := { + clone := authority.Authority.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::Copy for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:16-106:20 -/ +@[reducible] +def authority.Authority.Insts.CoreMarkerCopy : core.marker.Copy + authority.Authority := { + cloneInst := authority.Authority.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Authority}::fmt]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:22-106:27 + Visibility: public -/ +def authority.Authority.Insts.CoreFmtDebug.fmt + (self : authority.Authority) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + let dyn := Dyn.mk _ authority.Effect.Insts.CoreFmtDebug self.effect + let dyn1 := Dyn.mk _ authority.Assurance.Insts.CoreFmtDebug self.assurance + let dyn2 := + Dyn.mk _ (core.fmt.DebugShared authority.Scope.Insts.CoreFmtDebug) + self.scope + core.fmt.Formatter.debug_struct_field3_finish f (toStr "Authority") (toStr + "effect") dyn (toStr "assurance") dyn1 (toStr "scope") dyn2 + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:22-106:27 -/ +@[reducible] +def authority.Authority.Insts.CoreFmtDebug : core.fmt.Debug authority.Authority + := { + fmt := authority.Authority.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:29-106:38 -/ +@[reducible] +def authority.Authority.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq authority.Authority := { +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Authority}::eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:29-106:38 + Visibility: public -/ +def authority.Authority.Insts.CoreCmpPartialEqAuthority.eq + (self : authority.Authority) (other : authority.Authority) : + Result Bool + := do + let b ← + authority.Effect.Insts.CoreCmpPartialEqEffect.eq self.effect other.effect + if b + then + let b1 ← + authority.Assurance.Insts.CoreCmpPartialEqAssurance.eq self.assurance + other.assurance + if b1 + then authority.Scope.Insts.CoreCmpPartialEqScope.eq self.scope other.scope + else ok false + else ok false + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:29-106:38 -/ +@[reducible] +def authority.Authority.Insts.CoreCmpPartialEqAuthority : core.cmp.PartialEq + authority.Authority authority.Authority := { + eq := authority.Authority.Insts.CoreCmpPartialEqAuthority.eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Authority}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:40-106:42 + Visibility: public -/ +def authority.Authority.Insts.CoreCmpEq.assert_fields_are_eq + (self : authority.Authority) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:40-106:42 -/ +@[reducible] +def authority.Authority.Insts.CoreCmpEq : core.cmp.Eq authority.Authority := { + partialEqInst := authority.Authority.Insts.CoreCmpPartialEqAuthority + assert_fields_are_eq := + authority.Authority.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Authority}::hash]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:44-106:48 + Visibility: public -/ +def authority.Authority.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : authority.Authority) (state : __H) : + Result __H + := do + let state1 ← + authority.Effect.Insts.CoreHashHash.hash corehashHasherInst self.effect + state + let state2 ← + authority.Assurance.Insts.CoreHashHash.hash corehashHasherInst + self.assurance state1 + authority.Scope.Insts.CoreHashHash.hash corehashHasherInst self.scope state2 + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Authority}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 106:44-106:48 -/ +@[reducible] +def authority.Authority.Insts.CoreHashHash : core.hash.Hash authority.Authority + := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + authority.Authority.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Authority}::new]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 114:4-120:5 + Visibility: public -/ +def authority.Authority.new + (effect : authority.Effect) (assurance : authority.Assurance) + (scope : authority.Scope) : + Result authority.Authority + := do + ok { effect, assurance, scope } + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Authority}::BOTTOM] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 124:4-124:93 + Visibility: public -/ +@[global_simps, irreducible] +def authority.Authority.BOTTOM : Result authority.Authority := + authority.Authority.new authority.Effect.Deny authority.Assurance.None + authority.Scope.Once + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Authority}::TOP] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 129:4-129:98 + Visibility: public -/ +@[global_simps, irreducible] +def authority.Authority.TOP : Result authority.Authority := + authority.Authority.new authority.Effect.Allow authority.Assurance.Hardware + authority.Scope.Durable + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Authority}::meet]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 132:4-138:5 + Visibility: public -/ +def authority.Authority.meet + (self : authority.Authority) (other : authority.Authority) : + Result authority.Authority + := do + let e ← authority.Effect.meet self.effect other.effect + let a ← authority.Assurance.meet self.assurance other.assurance + let s ← authority.Scope.meet self.scope other.scope + authority.Authority.new e a s + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Authority}::le]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 141:4-143:5 + Visibility: public -/ +def authority.Authority.le + (self : authority.Authority) (other : authority.Authority) : + Result Bool + := do + let a ← authority.Authority.meet self other + authority.Authority.Insts.CoreCmpPartialEqAuthority.eq a self + +/-- [agent_bridle_ceremony::authority::{agent_bridle_ceremony::authority::Authority}::attenuate]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 147:4-149:5 + Visibility: public -/ +def authority.Authority.attenuate + (self : authority.Authority) (ceiling : authority.Authority) : + Result authority.Authority + := do + authority.Authority.meet self ceiling + +/-- [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Resolution}::clone]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:9-157:14 + Visibility: public -/ +def authority.Resolution.Insts.CoreCloneClone.clone + (self : authority.Resolution) : Result authority.Resolution := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::clone::Clone for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:9-157:14 -/ +@[reducible] +def authority.Resolution.Insts.CoreCloneClone : core.clone.Clone + authority.Resolution := { + clone := authority.Resolution.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::Copy for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:16-157:20 -/ +@[reducible] +def authority.Resolution.Insts.CoreMarkerCopy : core.marker.Copy + authority.Resolution := { + cloneInst := authority.Resolution.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Resolution}::fmt]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:22-157:27 + Visibility: public -/ +def authority.Resolution.Insts.CoreFmtDebug.fmt + (self : authority.Resolution) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + match self with + | authority.Resolution.NeedsDecision => + core.fmt.Formatter.write_str f (toStr "NeedsDecision") + | authority.Resolution.Decided __self_0 => + let __self_01 := + Dyn.mk _ (core.fmt.DebugShared authority.Authority.Insts.CoreFmtDebug) + __self_0 + core.fmt.Formatter.debug_tuple_field1_finish f (toStr "Decided") __self_01 + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::fmt::Debug for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:22-157:27 -/ +@[reducible] +def authority.Resolution.Insts.CoreFmtDebug : core.fmt.Debug + authority.Resolution := { + fmt := authority.Resolution.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:29-157:38 -/ +@[reducible] +def authority.Resolution.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq authority.Resolution := { +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Resolution}::eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:29-157:38 + Visibility: public -/ +def authority.Resolution.Insts.CoreCmpPartialEqResolution.eq + (self : authority.Resolution) (other : authority.Resolution) : + Result Bool + := do + let self1 := read_discriminant self + let other1 := read_discriminant other + if self1 = other1 + then + match self with + | authority.Resolution.NeedsDecision => ok true + | authority.Resolution.Decided __self_0 => + match other with + | authority.Resolution.NeedsDecision => ok true + | authority.Resolution.Decided __arg1_0 => + authority.Authority.Insts.CoreCmpPartialEqAuthority.eq __self_0 + __arg1_0 + else ok false + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::PartialEq for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:29-157:38 -/ +@[reducible] +def authority.Resolution.Insts.CoreCmpPartialEqResolution : core.cmp.PartialEq + authority.Resolution authority.Resolution := { + eq := authority.Resolution.Insts.CoreCmpPartialEqResolution.eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Resolution}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:40-157:42 + Visibility: public -/ +def authority.Resolution.Insts.CoreCmpEq.assert_fields_are_eq + (self : authority.Resolution) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::cmp::Eq for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:40-157:42 -/ +@[reducible] +def authority.Resolution.Insts.CoreCmpEq : core.cmp.Eq authority.Resolution + := { + partialEqInst := authority.Resolution.Insts.CoreCmpPartialEqResolution + assert_fields_are_eq := + authority.Resolution.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Resolution}::hash]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:44-157:48 + Visibility: public -/ +def authority.Resolution.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : authority.Resolution) (state : __H) : + Result __H + := do + let self1 := read_discriminant self + let state1 ← Isize.Insts.CoreHashHash.hash corehashHasherInst self1 state + match self with + | authority.Resolution.NeedsDecision => ok state1 + | authority.Resolution.Decided __self_0 => + authority.Authority.Insts.CoreHashHash.hash corehashHasherInst __self_0 + state1 + +/-- Trait implementation: [agent_bridle_ceremony::authority::{impl core::hash::Hash for agent_bridle_ceremony::authority::Resolution}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 157:44-157:48 -/ +@[reducible] +def authority.Resolution.Insts.CoreHashHash : core.hash.Hash + authority.Resolution := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + authority.Resolution.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::authority::resolve::{impl core::ops::function::FnMut<(agent_bridle_ceremony::authority::Authority, &'_ agent_bridle_ceremony::authority::Authority), agent_bridle_ceremony::authority::Authority> for agent_bridle_ceremony::authority::resolve::closure}::call_mut]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 171:76-171:97 -/ +def + authority.resolve.closure.Insts.CoreOpsFunctionFnMutPairAuthoritySharedAuthorityAuthority.call_mut + (c : authority.resolve.closure) + (tupled_args : (authority.Authority × authority.Authority)) : + Result (authority.Authority × authority.resolve.closure) + := do + let (acc, a) := tupled_args + let a1 ← authority.Authority.meet acc a + ok (a1, c) + +/-- [agent_bridle_ceremony::authority::resolve::{impl core::ops::function::FnOnce<(agent_bridle_ceremony::authority::Authority, &'_ agent_bridle_ceremony::authority::Authority), agent_bridle_ceremony::authority::Authority> for agent_bridle_ceremony::authority::resolve::closure}::call_once]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 171:76-171:97 -/ +def + authority.resolve.closure.Insts.CoreOpsFunctionFnOncePairAuthoritySharedAuthorityAuthority.call_once + (c : authority.resolve.closure) + (p : (authority.Authority × authority.Authority)) : + Result authority.Authority + := do + let (a, _) ← + authority.resolve.closure.Insts.CoreOpsFunctionFnMutPairAuthoritySharedAuthorityAuthority.call_mut + c p + ok a + +/-- Trait implementation: [agent_bridle_ceremony::authority::resolve::{impl core::ops::function::FnOnce<(agent_bridle_ceremony::authority::Authority, &'_ agent_bridle_ceremony::authority::Authority), agent_bridle_ceremony::authority::Authority> for agent_bridle_ceremony::authority::resolve::closure}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 171:76-171:97 -/ +@[reducible] +def + authority.resolve.closure.Insts.CoreOpsFunctionFnOncePairAuthoritySharedAuthorityAuthority + : core.ops.function.FnOnce authority.resolve.closure (authority.Authority × + authority.Authority) authority.Authority := { + call_once := + authority.resolve.closure.Insts.CoreOpsFunctionFnOncePairAuthoritySharedAuthorityAuthority.call_once +} + +/-- Trait implementation: [agent_bridle_ceremony::authority::resolve::{impl core::ops::function::FnMut<(agent_bridle_ceremony::authority::Authority, &'_ agent_bridle_ceremony::authority::Authority), agent_bridle_ceremony::authority::Authority> for agent_bridle_ceremony::authority::resolve::closure}] + Source: 'agent-bridle-ceremony/src/authority.rs', lines 171:76-171:97 -/ +@[reducible] +def + authority.resolve.closure.Insts.CoreOpsFunctionFnMutPairAuthoritySharedAuthorityAuthority + : core.ops.function.FnMut authority.resolve.closure (authority.Authority × + authority.Authority) authority.Authority := { + FnOnceInst := + authority.resolve.closure.Insts.CoreOpsFunctionFnOncePairAuthoritySharedAuthorityAuthority + call_mut := + authority.resolve.closure.Insts.CoreOpsFunctionFnMutPairAuthoritySharedAuthorityAuthority.call_mut +} + +/-- [agent_bridle_ceremony::authority::resolve]: + Source: 'agent-bridle-ceremony/src/authority.rs', lines 168:0-173:1 + Visibility: public -/ +def authority.resolve + (candidates : Slice authority.Authority) : Result authority.Resolution := do + let o ← core.slice.Slice.split_first candidates + match o with + | none => ok authority.Resolution.NeedsDecision + | some p => + let (first, rest) := p + let i ← core.slice.Slice.iter rest + let a ← + core.slice.iter.Iter.Insts.CoreIterTraitsIteratorIteratorSharedAT.fold + authority.resolve.closure.Insts.CoreOpsFunctionFnMutPairAuthoritySharedAuthorityAuthority + i first () + ok (authority.Resolution.Decided a) + +/-- [agent_bridle_ceremony::boundary::{impl core::clone::Clone for agent_bridle_ceremony::boundary::Fence}::clone]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:9-25:14 + Visibility: public -/ +def boundary.Fence.Insts.CoreCloneClone.clone + (self : boundary.Fence) : Result boundary.Fence := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::clone::Clone for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:9-25:14 -/ +@[reducible] +def boundary.Fence.Insts.CoreCloneClone : core.clone.Clone boundary.Fence := { + clone := boundary.Fence.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::marker::Copy for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:16-25:20 -/ +@[reducible] +def boundary.Fence.Insts.CoreMarkerCopy : core.marker.Copy boundary.Fence := { + cloneInst := boundary.Fence.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::boundary::{impl core::fmt::Debug for agent_bridle_ceremony::boundary::Fence}::fmt]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:22-25:27 + Visibility: public -/ +def boundary.Fence.Insts.CoreFmtDebug.fmt + (self : boundary.Fence) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + match self with + | boundary.Fence.Advisory => + core.fmt.Formatter.write_str f (toStr "Advisory") + | boundary.Fence.Kernel => core.fmt.Formatter.write_str f (toStr "Kernel") + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::fmt::Debug for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:22-25:27 -/ +@[reducible] +def boundary.Fence.Insts.CoreFmtDebug : core.fmt.Debug boundary.Fence := { + fmt := boundary.Fence.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:29-25:38 -/ +@[reducible] +def boundary.Fence.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq boundary.Fence := { +} + +/-- [agent_bridle_ceremony::boundary::{impl core::cmp::PartialEq for agent_bridle_ceremony::boundary::Fence}::eq]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:29-25:38 + Visibility: public -/ +def boundary.Fence.Insts.CoreCmpPartialEqFence.eq + (self : boundary.Fence) (other : boundary.Fence) : Result Bool := do + let self1 := read_discriminant self + let other1 := read_discriminant other + ok (self1 = other1) + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::cmp::PartialEq for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:29-25:38 -/ +@[reducible] +def boundary.Fence.Insts.CoreCmpPartialEqFence : core.cmp.PartialEq + boundary.Fence boundary.Fence := { + eq := boundary.Fence.Insts.CoreCmpPartialEqFence.eq +} + +/-- [agent_bridle_ceremony::boundary::{impl core::cmp::Eq for agent_bridle_ceremony::boundary::Fence}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:40-25:42 + Visibility: public -/ +def boundary.Fence.Insts.CoreCmpEq.assert_fields_are_eq + (self : boundary.Fence) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::cmp::Eq for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:40-25:42 -/ +@[reducible] +def boundary.Fence.Insts.CoreCmpEq : core.cmp.Eq boundary.Fence := { + partialEqInst := boundary.Fence.Insts.CoreCmpPartialEqFence + assert_fields_are_eq := boundary.Fence.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::boundary::{impl core::hash::Hash for agent_bridle_ceremony::boundary::Fence}::hash]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:44-25:48 + Visibility: public -/ +def boundary.Fence.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : boundary.Fence) (state : __H) : + Result __H + := do + let self1 := read_discriminant self + Isize.Insts.CoreHashHash.hash corehashHasherInst self1 state + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::hash::Hash for agent_bridle_ceremony::boundary::Fence}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 25:44-25:48 -/ +@[reducible] +def boundary.Fence.Insts.CoreHashHash : core.hash.Hash boundary.Fence := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + boundary.Fence.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::boundary::{agent_bridle_ceremony::boundary::Fence}::ALL] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 32:4-32:65 + Visibility: public -/ +@[global_simps, irreducible] +def boundary.Fence.ALL : Array boundary.Fence 2#usize := + Array.make 2#usize [ boundary.Fence.Advisory, boundary.Fence.Kernel ] + +/-- [agent_bridle_ceremony::boundary::{impl core::clone::Clone for agent_bridle_ceremony::boundary::Request}::clone]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:9-38:14 + Visibility: public -/ +def boundary.Request.Insts.CoreCloneClone.clone + (self : boundary.Request) : Result boundary.Request := do + ok self + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::clone::Clone for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:9-38:14 -/ +@[reducible] +def boundary.Request.Insts.CoreCloneClone : core.clone.Clone boundary.Request + := { + clone := boundary.Request.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::marker::Copy for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:16-38:20 -/ +@[reducible] +def boundary.Request.Insts.CoreMarkerCopy : core.marker.Copy boundary.Request + := { + cloneInst := boundary.Request.Insts.CoreCloneClone +} + +/-- [agent_bridle_ceremony::boundary::{impl core::fmt::Debug for agent_bridle_ceremony::boundary::Request}::fmt]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:22-38:27 + Visibility: public -/ +def boundary.Request.Insts.CoreFmtDebug.fmt + (self : boundary.Request) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + let dyn := Dyn.mk _ (core.fmt.DebugShared core.fmt.DebugBool) self.dynamic + core.fmt.Formatter.debug_struct_field1_finish f (toStr "Request") (toStr + "dynamic") dyn + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::fmt::Debug for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:22-38:27 -/ +@[reducible] +def boundary.Request.Insts.CoreFmtDebug : core.fmt.Debug boundary.Request := { + fmt := boundary.Request.Insts.CoreFmtDebug.fmt +} + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::marker::StructuralPartialEq for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:29-38:38 -/ +@[reducible] +def boundary.Request.Insts.CoreMarkerStructuralPartialEq : + core.marker.StructuralPartialEq boundary.Request := { +} + +/-- [agent_bridle_ceremony::boundary::{impl core::cmp::PartialEq for agent_bridle_ceremony::boundary::Request}::eq]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:29-38:38 + Visibility: public -/ +def boundary.Request.Insts.CoreCmpPartialEqRequest.eq + (self : boundary.Request) (other : boundary.Request) : Result Bool := do + ok (self.dynamic = other.dynamic) + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::cmp::PartialEq for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:29-38:38 -/ +@[reducible] +def boundary.Request.Insts.CoreCmpPartialEqRequest : core.cmp.PartialEq + boundary.Request boundary.Request := { + eq := boundary.Request.Insts.CoreCmpPartialEqRequest.eq +} + +/-- [agent_bridle_ceremony::boundary::{impl core::cmp::Eq for agent_bridle_ceremony::boundary::Request}::assert_fields_are_eq]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:40-38:42 + Visibility: public -/ +def boundary.Request.Insts.CoreCmpEq.assert_fields_are_eq + (self : boundary.Request) : Result Unit := do + ok () + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::cmp::Eq for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:40-38:42 -/ +@[reducible] +def boundary.Request.Insts.CoreCmpEq : core.cmp.Eq boundary.Request := { + partialEqInst := boundary.Request.Insts.CoreCmpPartialEqRequest + assert_fields_are_eq := boundary.Request.Insts.CoreCmpEq.assert_fields_are_eq +} + +/-- [agent_bridle_ceremony::boundary::{impl core::hash::Hash for agent_bridle_ceremony::boundary::Request}::hash]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:44-38:48 + Visibility: public -/ +def boundary.Request.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : boundary.Request) (state : __H) : + Result __H + := do + Bool.Insts.CoreHashHash.hash corehashHasherInst self.dynamic state + +/-- Trait implementation: [agent_bridle_ceremony::boundary::{impl core::hash::Hash for agent_bridle_ceremony::boundary::Request}] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 38:44-38:48 -/ +@[reducible] +def boundary.Request.Insts.CoreHashHash : core.hash.Hash boundary.Request := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + boundary.Request.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [agent_bridle_ceremony::boundary::{agent_bridle_ceremony::boundary::Request}::new]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 44:4-46:5 + Visibility: public -/ +def boundary.Request.new (dynamic : Bool) : Result boundary.Request := do + ok { dynamic } + +/-- [agent_bridle_ceremony::boundary::{agent_bridle_ceremony::boundary::Request}::ALL] + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 48:4-48:76 + Visibility: public -/ +@[global_simps, irreducible] +def boundary.Request.ALL : Result (Array boundary.Request 2#usize) := do + let r ← boundary.Request.new false + let r1 ← boundary.Request.new true + ok (Array.make 2#usize [ r, r1 ]) + +/-- [agent_bridle_ceremony::boundary::safe_subset]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 53:0-59:1 + Visibility: public -/ +def boundary.safe_subset (q : boundary.Request) : Result authority.Effect := do + if q.dynamic + then ok authority.Effect.Deny + else ok authority.Effect.Allow + +/-- [agent_bridle_ceremony::boundary::brush_honest]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 66:0-72:1 + Visibility: public -/ +def boundary.brush_honest + (f : boundary.Fence) (q : boundary.Request) : Result authority.Effect := do + match f with + | boundary.Fence.Advisory => + if q.dynamic + then ok authority.Effect.Deny + else ok authority.Effect.Allow + | boundary.Fence.Kernel => ok authority.Effect.Allow + +/-- [agent_bridle_ceremony::boundary::boundary_verdict]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 76:0-81:1 + Visibility: public -/ +def boundary.boundary_verdict + (f : boundary.Fence) (q : boundary.Request) : Result authority.Effect := do + match f with + | boundary.Fence.Advisory => boundary.safe_subset q + | boundary.Fence.Kernel => boundary.brush_honest boundary.Fence.Kernel q + +/-- [agent_bridle_ceremony::boundary::enforceable_ceiling]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 84:0-86:1 + Visibility: public -/ +def boundary.enforceable_ceiling + (f : boundary.Fence) (q : boundary.Request) : Result authority.Effect := do + boundary.boundary_verdict f q + +/-- [agent_bridle_ceremony::boundary::boundary_ceiling]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 90:0-92:1 + Visibility: public -/ +def boundary.boundary_ceiling + (f : boundary.Fence) (q : boundary.Request) : + Result authority.Authority + := do + let e ← boundary.boundary_verdict f q + authority.Authority.new e authority.Assurance.Hardware + authority.Scope.Durable + +/-- [agent_bridle_ceremony::boundary::minted_grant]: + Source: 'agent-bridle-ceremony/src/boundary.rs', lines 96:0-98:1 + Visibility: public -/ +def boundary.minted_grant + (req : authority.Authority) (f : boundary.Fence) (q : boundary.Request) : + Result authority.Authority + := do + let a ← boundary.boundary_ceiling f q + authority.Authority.attenuate req a + +end agent_bridle_ceremony diff --git a/formal/refinement/AgentBridleCeremony/FunsExternal.lean b/formal/refinement/AgentBridleCeremony/FunsExternal.lean new file mode 100644 index 0000000..e1fed9f --- /dev/null +++ b/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}::hash] + Visibility: public -/ +@[rust_fun "core::hash::impls::{core::hash::Hash}::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}::hash] + Visibility: public -/ +@[rust_fun "core::hash::impls::{core::hash::Hash}::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, &'a @T>}::fold] + Visibility: public -/ +@[rust_fun + "core::slice::iter::{core::iter::traits::iterator::Iterator, &'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))) + diff --git a/formal/refinement/AgentBridleCeremony/Types.lean b/formal/refinement/AgentBridleCeremony/Types.lean new file mode 100644 index 0000000..26df384 --- /dev/null +++ b/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 diff --git a/formal/refinement/README.md b/formal/refinement/README.md new file mode 100644 index 0000000..450ea5f --- /dev/null +++ b/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. diff --git a/formal/refinement/Refinement.lean b/formal/refinement/Refinement.lean new file mode 100644 index 0000000..238ab0b --- /dev/null +++ b/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 diff --git a/formal/refinement/aeneas-commit.txt b/formal/refinement/aeneas-commit.txt new file mode 100644 index 0000000..eda6fb7 --- /dev/null +++ b/formal/refinement/aeneas-commit.txt @@ -0,0 +1 @@ +bc2eb6f941369fa3c695e30598b5758b11e4f0de diff --git a/formal/refinement/lake-manifest.json b/formal/refinement/lake-manifest.json new file mode 100644 index 0000000..9445a27 --- /dev/null +++ b/formal/refinement/lake-manifest.json @@ -0,0 +1,103 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "Aeneas", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "aeneas-lean", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.31.0", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.31.0", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "«ceremony-refinement»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/refinement/lakefile.lean b/formal/refinement/lakefile.lean new file mode 100644 index 0000000..cdb4b8f --- /dev/null +++ b/formal/refinement/lakefile.lean @@ -0,0 +1,23 @@ +import Lake +open Lake DSL + +-- Tier-3 REFINEMENT project: proves the extracted (Charon/Aeneas) Rust of +-- `agent-bridle-ceremony` satisfies the Authority.lean algebraic laws. +-- +-- This tier is HEAVY (it pulls the Aeneas Lean backend + mathlib), unlike the +-- fast, mathlib-free `formal/` project. It is deliberately NOT in the mandatory +-- pre-push gate; run it on a machine with the toolchain via `just check-refinement`. +-- +-- `aeneas-lean` is a machine-local symlink to `/backends/lean`, +-- gitignored so no absolute path is committed. Create it with `./setup.sh` +-- (honours `AENEAS_LEAN_LIB`). See README.md and docs/TOOLCHAIN.md §2. +require Aeneas from "aeneas-lean" + +package «ceremony-refinement» where + leanOptions := #[⟨`maxHeartbeats, (1000000 : Nat)⟩] + +@[default_target] +lean_lib AgentBridleCeremony + +@[default_target] +lean_lib Refinement diff --git a/formal/refinement/lean-toolchain b/formal/refinement/lean-toolchain new file mode 100644 index 0000000..18640c8 --- /dev/null +++ b/formal/refinement/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.31.0 diff --git a/formal/refinement/regenerate.sh b/formal/refinement/regenerate.sh new file mode 100755 index 0000000..99855f1 --- /dev/null +++ b/formal/refinement/regenerate.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash +# Regenerate the extracted Lean (Types/Funs/FunsExternal/AgentBridleCeremony) +# from the Rust crate `agent-bridle-ceremony`, via Charon -> LLBC -> Aeneas. +# Requires the Charon + Aeneas toolchain (docs/TOOLCHAIN.md §2). The pinned +# Aeneas commit these files were generated against is in aeneas-commit.txt. +# +# Refinement.lean is HAND-WRITTEN and is never overwritten here. Review the diff +# on the generated files before committing (extraction is deterministic; a diff +# means the Rust kernel or the toolchain changed). +set -euxo pipefail +cd "$(dirname "$0")" +CRATE="$(git rev-parse --show-toplevel)/agent-bridle-ceremony" +CHARON="${CHARON:-$HOME/opt/aeneas/charon/bin/charon}" +AENEAS="${AENEAS:-$HOME/opt/aeneas/bin/aeneas}" +OUT="$(mktemp -d)" + +# NOTE: this harness overrides CARGO_TARGET_DIR; unset it so Charon's own build +# lands where its Makefile expects (see reference: cargo_target_dir gotcha). +( cd "$CRATE" && env -u CARGO_TARGET_DIR "$CHARON" cargo --preset=aeneas --dest-file "$OUT/agent_bridle_ceremony.llbc" ) +"$AENEAS" -backend lean "$OUT/agent_bridle_ceremony.llbc" -dest "$OUT/lean" -split-files + +cp "$OUT/lean/Types.lean" "$OUT/lean/Funs.lean" AgentBridleCeremony/ +# FunsExternal is the (opaque) external axioms; regenerated as a *_Template. +cp "$OUT/lean/FunsExternal_Template.lean" AgentBridleCeremony/FunsExternal.lean +cp "$OUT/lean/AgentBridleCeremony.lean" . +echo "Regenerated. Review 'git diff' before committing." diff --git a/formal/refinement/setup.sh b/formal/refinement/setup.sh new file mode 100755 index 0000000..1ce4876 --- /dev/null +++ b/formal/refinement/setup.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash +# Link the machine-local Aeneas Lean backend into this project so `lake build` +# can find it, without committing an absolute path. Honours AENEAS_LEAN_LIB; +# defaults to the docs/TOOLCHAIN.md §2 location. +set -euo pipefail +cd "$(dirname "$0")" +DEFAULT="$HOME/opt/aeneas/backends/lean" +TARGET="${AENEAS_LEAN_LIB:-$DEFAULT}" +if [ ! -d "$TARGET" ]; then + echo "Aeneas Lean backend not found at: $TARGET" >&2 + echo "Build it (docs/TOOLCHAIN.md §2), or set AENEAS_LEAN_LIB to its path." >&2 + exit 1 +fi +ln -sfn "$TARGET" aeneas-lean +echo "linked aeneas-lean -> $TARGET" diff --git a/justfile b/justfile index 645860b..2943aeb 100644 --- a/justfile +++ b/justfile @@ -44,6 +44,25 @@ check-formal: set -e ( cd formal && "$LAKE" build && "$LAKE" exe formalGate ) +# Tier-3 REFINEMENT gate (HEAVY — pulls the Aeneas Lean backend + mathlib). +# Proves the Charon/Aeneas-EXTRACTED Rust of agent-bridle-ceremony satisfies the +# Authority.lean laws (formal/refinement/). Deliberately NOT in the mandatory +# pre-push gate or CI (mathlib is too heavy for every push) — run it on a machine +# with the Charon/Aeneas toolchain. Skips gracefully if lake OR the Aeneas Lean +# backend is absent. See formal/refinement/README.md and docs/TOOLCHAIN.md §2. +check-refinement: + #!/usr/bin/env bash + set -uo pipefail + if ! command -v lake >/dev/null 2>&1 && [ ! -x "$HOME/.elan/bin/lake" ]; then + echo "lake (Lean) not installed — skipping refinement gate"; exit 0 + fi + LAKE="$(command -v lake || echo "$HOME/.elan/bin/lake")" + if [ ! -d "${AENEAS_LEAN_LIB:-$HOME/opt/aeneas/backends/lean}" ]; then + echo "Aeneas Lean backend absent — skipping refinement gate (see docs/TOOLCHAIN.md §2)"; exit 0 + fi + set -e + ( cd formal/refinement && ./setup.sh && "$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