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.
65 lines
2.1 KiB
Lean4
65 lines
2.1 KiB
Lean4
/-
|
|
MCP Tool Permission Lattice
|
|
|
|
Models the Model Context Protocol tool surface as a permission
|
|
lattice with subset ordering.
|
|
|
|
Maps to:
|
|
- hanzo/mcp: HIP-0300 MCP server (13 unified tools)
|
|
- hanzo/agents: agent permission configuration
|
|
|
|
Properties:
|
|
- Permission check is monotone under subset
|
|
- Empty permissions deny everything
|
|
- Full permissions allow everything
|
|
|
|
Model: permissions are represented as a `Finset` of tool identifiers,
|
|
which gives us lattice structure for free (subset / meet / empty) and
|
|
avoids the Lean-4-version-sensitive bitwise lemmas.
|
|
-/
|
|
|
|
import Mathlib.Data.Finset.Basic
|
|
import Mathlib.Data.Finset.Lattice.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace Agent.MCP
|
|
|
|
/-- A tool is identified by a natural-number index. -/
|
|
abbrev ToolId := Nat
|
|
|
|
/-- Permission set: the set of tool ids the holder may call. -/
|
|
abbrev Permissions := Finset ToolId
|
|
|
|
/-- No permissions: deny everything. -/
|
|
def Permissions.none : Permissions := ∅
|
|
|
|
-- Permission subset ordering is inherited from `Finset.instLE`.
|
|
-- `Permissions.subset a b ↔ a ⊆ b` holds by definition.
|
|
|
|
/-- A principal *has* tool `t` iff `t ∈ p`. -/
|
|
def Permissions.has (p : Permissions) (t : ToolId) : Prop := t ∈ p
|
|
|
|
/-- **Theorem:** `Permissions.none` is the bottom of the lattice. -/
|
|
theorem none_le_all (p : Permissions) : Permissions.none ⊆ p := by
|
|
simp [Permissions.none]
|
|
|
|
/-- **Theorem:** meet (intersection) is a lower bound on the left. -/
|
|
theorem meet_le_left (a b : Permissions) : a ∩ b ⊆ a :=
|
|
Finset.inter_subset_left
|
|
|
|
/-- **Theorem:** meet is a lower bound on the right. -/
|
|
theorem meet_le_right (a b : Permissions) : a ∩ b ⊆ b :=
|
|
Finset.inter_subset_right
|
|
|
|
/-- **Theorem (monotone delegation):** if a child holds a subset of the
|
|
parent's permissions, every tool the child may call is one the
|
|
parent may also call. This is the core safety property for
|
|
capability-style permission delegation. -/
|
|
theorem fewer_permissions_safe
|
|
(parent child : Permissions) (h : child ⊆ parent)
|
|
(t : ToolId) (hc : child.has t) : parent.has t := by
|
|
unfold Permissions.has at *
|
|
exact h hc
|
|
|
|
end Agent.MCP
|