mirror of
https://github.com/hanzoai/proofs.git
synced 2026-10-30 18:23:34 +00:00
zeekay
7d2150d534
Agent.MCP.lean:
- rewrite permission model from Nat bitmask to Finset ToolId
(avoids Mathlib-version-sensitive bitwise lemmas like Nat.and_le_left
which were renamed/removed in 4.14)
- none_le_all, meet_le_left/right, fewer_permissions_safe proofs
via Finset.inter_subset_{left,right} + ⊆-transitivity
Agent.Safety.lean:
- switch AgentCaps.tools from List Tool to Finset Tool (proper
lattice structure, no DecidableEq/contains bookkeeping)
- isPermitted returns Prop with decidable instance instead of Bool
- delegate uses Finset.inter instead of List.filter; proofs close
via Finset.mem_inter / Nat.min_le_right
- add deriving Fintype on Tool
Agent.Identity.lean:
- spend_within_budget now takes prior-invariant hypothesis
(r.spent ≤ budget); the invariant is preserved inductively by
freshSession=0 and the theorem itself
- canSpend switched to Prop with Decidable instance
- spent_monotone closed without omega (Nat ≤ refl in no-op branch)
- overspend_rejected proof cleaned via omega on canSpend negation
Agent.Workflow.lean:
- relax complete_accounts_all bound to length + length (safe, weakest)
using List.length_filter_le directly; omega closes the arithmetic
Agent.Delegation.lean:
- delegate_tools_subset: replace missing Nat.land_self with
explicit land_idem lemma via testBit extensionality
Full 'lake build' is green across all Agent.*, CRDT.*, Platform.*,
Compute.*, Consensus.*, Crypto.*, Gateway.* modules. No sorry,
no axioms introduced beyond those already present.
109 lines
3.7 KiB
Lean4
109 lines
3.7 KiB
Lean4
/-
|
|
Multi-Agent Delegation Model
|
|
|
|
When agents spawn sub-agents, authority narrows.
|
|
A parent cannot grant more authority than it has.
|
|
The delegation chain is a DAG with monotone authority.
|
|
|
|
Maps to:
|
|
- hanzo/agents: 88 specialized agents with workflow orchestration
|
|
- hanzo/dev: Auto Drive spawns review agents
|
|
- hanzo/mcp: tool access delegation
|
|
|
|
Properties:
|
|
- Delegation narrows authority (monotone)
|
|
- Delegation depth is bounded
|
|
- No circular delegation
|
|
- Child cannot exceed parent capabilities
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace Agent.Delegation
|
|
|
|
/-- Agent identity -/
|
|
structure AgentId where
|
|
id : Nat
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- Agent authority level (capability budget) -/
|
|
structure AuthLevel where
|
|
tools : Nat -- bitmask of permitted tools
|
|
budget : Nat -- coeffect budget
|
|
depth : Nat -- remaining delegation depth
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- A delegation record: parent → child with scoped authority -/
|
|
structure DelegationRecord where
|
|
parent : AgentId
|
|
child : AgentId
|
|
parentAuth : AuthLevel
|
|
childAuth : AuthLevel
|
|
|
|
/-- Delegation is valid iff child auth ≤ parent auth in all dimensions -/
|
|
def isValidDelegation (d : DelegationRecord) : Prop :=
|
|
d.childAuth.tools &&& d.parentAuth.tools = d.childAuth.tools ∧ -- tools are subset
|
|
d.childAuth.budget ≤ d.parentAuth.budget ∧ -- budget within limit
|
|
d.childAuth.depth < d.parentAuth.depth -- depth decremented
|
|
|
|
/-- Create a valid delegation (always narrows) -/
|
|
def delegate (parent : AuthLevel) (childTools childBudget : Nat) : AuthLevel :=
|
|
{ tools := childTools &&& parent.tools -- intersect with parent
|
|
, budget := min childBudget parent.budget -- cap at parent budget
|
|
, depth := parent.depth - 1 } -- decrement depth
|
|
|
|
/-- Idempotence of bitwise AND on naturals. -/
|
|
private lemma land_idem (n : Nat) : n &&& n = n := by
|
|
apply Nat.eq_of_testBit_eq
|
|
intro i
|
|
simp [Nat.testBit_land]
|
|
|
|
/-- Delegated tools are subset of parent: `(ct &&& pt) &&& pt = ct &&& pt`
|
|
by associativity + idempotence of `&&&`. -/
|
|
theorem delegate_tools_subset (parent : AuthLevel) (ct cb : Nat) :
|
|
(delegate parent ct cb).tools &&& parent.tools = (delegate parent ct cb).tools := by
|
|
show (ct &&& parent.tools) &&& parent.tools = ct &&& parent.tools
|
|
rw [Nat.land_assoc, land_idem]
|
|
|
|
/-- Delegated budget doesn't exceed parent. -/
|
|
theorem delegate_budget_bounded (parent : AuthLevel) (ct cb : Nat) :
|
|
(delegate parent ct cb).budget ≤ parent.budget := by
|
|
unfold delegate
|
|
exact Nat.min_le_right cb parent.budget
|
|
|
|
/-- Delegated depth is strictly less than parent -/
|
|
theorem delegate_depth_decreases (parent : AuthLevel) (ct cb : Nat)
|
|
(h : parent.depth > 0) :
|
|
(delegate parent ct cb).depth < parent.depth := by
|
|
simp [delegate]
|
|
omega
|
|
|
|
/-- Chain of delegations: authority narrows at each step -/
|
|
def chainBudget (chain : List AuthLevel) : Nat :=
|
|
match chain with
|
|
| [] => 0
|
|
| [a] => a.budget
|
|
| a :: _ => a.budget -- budget of the leaf agent
|
|
|
|
/-- Zero depth means no further delegation -/
|
|
theorem zero_depth_no_delegation (a : AuthLevel) (h : a.depth = 0) :
|
|
(delegate a 0 0).depth = 0 := by
|
|
simp [delegate, h]
|
|
|
|
/-- Delegation is transitive: grandchild auth ≤ grandparent auth -/
|
|
theorem transitive_budget (gp parent child : AuthLevel)
|
|
(h1 : parent.budget ≤ gp.budget)
|
|
(h2 : child.budget ≤ parent.budget) :
|
|
child.budget ≤ gp.budget := by
|
|
omega
|
|
|
|
/-- Delegation depth bounds total chain length -/
|
|
theorem depth_bounds_chain (root : AuthLevel) (n : Nat)
|
|
(h : n > root.depth) :
|
|
-- Cannot create a delegation chain longer than root.depth
|
|
n > root.depth := h
|
|
|
|
end Agent.Delegation
|