proofs/lean/Agent/NFTOwnership.lean at salvage/main

mirror of https://github.com/zooai/proofs.git synced 2026-10-30 14:49:47 +00:00

Files

T

zooqueenandHanzo Dev d3bff5e2dc proofs: drive Lean library to 0 errors, eliminate proof-by-assumption axioms

The lean/ proof library (88 files) had ~180 type-check errors across ~45 files
plus 31 proof-by-assumption axiom cheats. It now type-checks cleanly under
Lean 4.14.0 + Mathlib, with every theorem genuinely proven from definitions.

Errors fixed:
- Stale Mathlib imports: Data.Nat.Basic / Data.Int.Basic were removed this rev
  -> Data.Nat.Defs / Data.Int.Defs (57 files).
- Shared AI/Agent/Governance/Contract/DeFi/Ecology draft files: same proof-rot
  as the zoo-labs sibling library (now reconciled): omega missing in-scope
  bounds, dead tactics after simp, simp over-reduction, doc-comment placement,
  reserved-word binders, deriving Repr on Finset-bearing structs, noncomputable
  defs over opaque primitives.
- Consensus/Liveness: collapsed a 74-error cascade (undefined shared state model
  inlined from Safety.lean; the |>. pipe-projection vs comparison parse trap on
  14 lines rewritten to explicit dot projection).
- Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE), Consensus, Protocol, Warp,
  Trust, GPU, Compute, Network, DeFi: brought structure invariants into scope
  for omega, Nat-division bounds via Nat.div_le_of_le_mul / Nat.div_mul_le_self,
  noncomputable over opaque crypto ops, deriving Inhabited for index access.

Integrity:
- Removed all 31 `theorem X := X_ax` cheats (axiom asserting the identical
  statement) and proved each from definitions; removed the UNSOUND
  content_addressed axiom (hash-injectivity over a struct with free fields).
- Quorum-intersection theorems (BFT/Quasar/Flare/Warp/BLS/GPU/Bridge): the draft
  hypothesis 3f<n is insufficient (n unbounded above makes them false); tightened
  to the optimal-resilience invariant n=3f+1 / 2t>n. Statement intent preserved.
- Net axiom change: -35 / +1 (the one addition, honesty_static, is a
  fixed-validator-set modeling assumption matching sibling files).
- Remaining axioms are trusted-base only: opaque crypto primitives (groups,
  pairings, hardness, hashes, FHE encrypt/decrypt, BLS soundness, forward
  secrecy, Fisher-Yates uniformity) and protocol modeling assumptions. No
  sorry/admit/native_decide. Verified all theorems trace to
  [propext, Classical.choice, Quot.sound] plus those primitives.

Co-authored-by: Hanzo Dev <[email protected]>

2026-06-02 05:54:28 -07:00

182 lines

6.5 KiB

Lean4

Raw Permalink Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 /-
   Authors: Antje Worring, Zach Kelling
   NFT-Bound Agent Ownership and Delegation
   Formal proofs about the Agent NFT Standard's ownership model.
   Agents are ERC-721 tokens that encapsulate autonomous AI systems
   with wallets, governance rights, and configurable autonomy parameters.
   Maps to:
   - zoo/papers/zoo-agent-nft.tex: Agent NFT Standard specification
   - Governance/AgentNFT.lean: basic transfer/revoke (extended here)
   Key results:
   - Transfer correctly updates the full capability set
   - Delegated permissions are transitive
   - Revoking owner propagates to all delegates
   - No agent can exceed its granted capabilities (no escalation)
   Author: Zach Kelling
 -/
 import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Finset.Basic
 import Mathlib.Tactic
 namespace Agent.NFTOwnership
 /-! ## Core Structures -/
 /-- Address (represented as Nat for simplicity). -/
 abbrev Address := Nat
 /-- Capability identifier (e.g., TRADE=1, GOVERN=2, STAKE=4, TRANSFER=8). -/
 abbrev Capability := Nat
 /-- A capability set is a finite set of capabilities. -/
 abbrev CapSet := Finset Capability
 /-- An Agent NFT with ownership, delegation, and capability tracking. -/
 structure AgentNFT where
   tokenId : Nat
   owner : Address
   /-- Capabilities granted to this agent by its owner -/
   capabilities : CapSet
   /-- Delegates: address -> subset of capabilities delegated to them -/
   delegates : Address → CapSet
   /-- Whether the agent is active (not revoked) -/
   active : Bool
 /-- The empty capability set. -/
 def emptyCaps : CapSet := ∅
 /-! ## Transfer -/
 /-- Transfer ownership: new owner inherits the full capability set,
     all existing delegations are cleared (security: new owner should
     explicitly re-delegate). -/
 def transfer (nft : AgentNFT) (newOwner : Address) : AgentNFT :=
   { nft with
     owner := newOwner
     delegates := fun _ => emptyCaps }
 /-- Transfer correctly updates the capability set: the new owner
     retains all capabilities that existed before transfer.
     The agent itself doesn't lose capabilities, only delegations reset. -/
 theorem ownership_transfer_updates_caps (nft : AgentNFT) (newOwner : Address) :
     (transfer nft newOwner).capabilities = nft.capabilities := by
   simp [transfer]
 /-- Transfer changes the owner. -/
 theorem transfer_changes_owner (nft : AgentNFT) (newOwner : Address) :
     (transfer nft newOwner).owner = newOwner := by
   simp [transfer]
 /-- Transfer clears all delegations. -/
 theorem transfer_clears_delegates (nft : AgentNFT) (newOwner : Address) (addr : Address) :
     (transfer nft newOwner).delegates addr = emptyCaps := by
   simp [transfer]
 /-! ## Delegation -/
 /-- Delegate a subset of capabilities to an address.
     The delegated set must be a subset of the agent's capabilities. -/
 def delegate (nft : AgentNFT) (to_ : Address) (caps : CapSet)
     (_ : caps ⊆ nft.capabilities) : AgentNFT :=
   { nft with
     delegates := fun addr =>
       if addr = to_ then nft.delegates to_ ∪ caps
       else nft.delegates addr }
 /-- Transitive delegation: if A delegates to B, and B delegates a subset
     of those capabilities to C, then C has those capabilities.
     We model this as a chain of delegation records. -/
 structure DelegationChain where
   /-- The original agent -/
   agent : AgentNFT
   /-- Intermediate delegate -/
   intermediate : Address
   /-- Final delegate -/
   final : Address
   /-- Capabilities delegated to intermediate -/
   intermediateCaps : CapSet
   /-- Capabilities sub-delegated to final (must be subset of intermediate's) -/
   finalCaps : CapSet
   /-- Proof that intermediate actually has those capabilities -/
   hIntermediate : intermediateCaps ⊆ agent.capabilities
   /-- Proof that final's capabilities are subset of intermediate's -/
   hFinal : finalCaps ⊆ intermediateCaps
 /-- Delegation is transitive: if the agent grants caps to B and B
     sub-delegates a subset to C, then C's capabilities are a subset
     of the agent's original capabilities. -/
 theorem delegation_transitive (chain : DelegationChain) :
     chain.finalCaps ⊆ chain.agent.capabilities :=
   Finset.Subset.trans chain.hFinal chain.hIntermediate
 /-! ## Revocation -/
 /-- Revoke the agent entirely: deactivates it and clears all delegations. -/
 def revoke (nft : AgentNFT) : AgentNFT :=
   { nft with
     active := false
     delegates := fun _ => emptyCaps }
 /-- Revoking the agent propagates to all delegates:
     no delegate retains any capabilities after revocation. -/
 theorem revocation_propagates (nft : AgentNFT) (addr : Address) :
     (revoke nft).delegates addr = emptyCaps := by
   simp [revoke]
 /-- Revocation deactivates the agent. -/
 theorem revocation_deactivates (nft : AgentNFT) :
     (revoke nft).active = false := by
   simp [revoke]
 /-- Revocation preserves the token identity. -/
 theorem revocation_preserves_id (nft : AgentNFT) :
     (revoke nft).tokenId = nft.tokenId := by
   simp [revoke]
 /-! ## No Escalation -/
 /-- A delegate's capabilities are always a subset of the agent's capabilities.
     This is the fundamental no-escalation invariant: an agent can never
     grant more capabilities than it possesses.
     The `delegate` operation sets the delegate's caps to `old ∪ new` where
     `new = caps ⊆ capabilities` by construction (`h`). For the union to stay
     within `capabilities`, the pre-existing delegation `nft.delegates to_` must
     already be bounded — exactly the no-escalation invariant maintained across
     operations (transfer/revoke reset delegations to `∅`, which trivially
     satisfies it). We therefore take that invariant as hypothesis `h_inv` and
     prove the union is bounded honestly. -/
 theorem no_escalation (nft : AgentNFT) (to_ : Address) (caps : CapSet)
     (h : caps ⊆ nft.capabilities)
     (h_inv : ∀ c ∈ nft.delegates to_, c ∈ nft.capabilities) :
     ∀ c ∈ (delegate nft to_ caps h).delegates to_, c ∈ nft.capabilities := by
   intro c hc
   have hc' : c ∈ nft.delegates to_ ∪ caps := by
     simpa only [delegate, if_pos rfl] using hc
   rw [Finset.mem_union] at hc'
   rcases hc' with hc' | hc'
   · exact h_inv c hc'
   · exact h hc'
 /-- Simpler no-escalation: delegated set is bounded by agent capabilities. -/
 theorem no_escalation_set (_nft : AgentNFT) (_to_ : Address) (caps : CapSet)
     (h : caps ⊆ _nft.capabilities) :
     caps ⊆ _nft.capabilities := h
 /-- An inactive agent cannot perform any actions.
     This is enforced at the contract level: all action functions
     check `require(agent.active)` before proceeding. -/
 def canAct (nft : AgentNFT) : Prop := nft.active = true
 theorem revoked_cannot_act (nft : AgentNFT) :
     ¬canAct (revoke nft) := by
   simp [canAct, revoke]
 end Agent.NFTOwnership

182 lines 6.5 KiB Lean4 Raw Permalink Blame History Unescape Escape

182 lines

6.5 KiB

Lean4

Raw Permalink Blame History