mirror of
https://github.com/hanzoai/proofs.git
synced 2026-10-30 18:23:34 +00:00
zeekayandHanzo Dev
6a0bfb7c9d
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning. Co-authored-by: Hanzo Dev <[email protected]>
72 lines
2.0 KiB
Lean4
72 lines
2.0 KiB
Lean4
/-
|
|
Agent Persistent Memory Correctness
|
|
|
|
Agents have persistent memory across sessions.
|
|
Memory is content-addressed, versioned, and scoped.
|
|
|
|
Maps to:
|
|
- hanzo/mcp: memory MCP tool
|
|
- hanzo/agents: agent memory system
|
|
- uor.foundation: content-addressed storage
|
|
|
|
Properties:
|
|
- Append-only: memories are never silently deleted
|
|
- Versioned: updates create new versions
|
|
- Scoped: agent can only access its own memories
|
|
- Content-addressed: deduplication by hash
|
|
|
|
Author: Hanzo AI Research, Woo Bin
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace Agent.Memory
|
|
|
|
structure MemoryEntry where
|
|
hash : Nat
|
|
agentId : Nat
|
|
version : Nat
|
|
content : Nat -- hash of content
|
|
deriving DecidableEq, Repr
|
|
|
|
structure MemoryStore where
|
|
entries : List MemoryEntry
|
|
owner : Nat
|
|
|
|
def write (s : MemoryStore) (e : MemoryEntry) : MemoryStore :=
|
|
if e.agentId = s.owner then
|
|
{ s with entries := e :: s.entries }
|
|
else s -- wrong agent, rejected
|
|
|
|
def read (s : MemoryStore) (agentId hash : Nat) : Option MemoryEntry :=
|
|
if agentId = s.owner then
|
|
s.entries.find? (·.hash = hash)
|
|
else none
|
|
|
|
/-- SCOPED: Can't write to another agent's memory -/
|
|
theorem scoped_write (s : MemoryStore) (e : MemoryEntry)
|
|
(h : e.agentId ≠ s.owner) :
|
|
write s e = s := by simp [write, h]
|
|
|
|
/-- SCOPED: Can't read another agent's memory -/
|
|
theorem scoped_read (s : MemoryStore) (agentId hash : Nat)
|
|
(h : agentId ≠ s.owner) :
|
|
read s agentId hash = none := by simp [read, h]
|
|
|
|
/-- APPEND-ONLY: Writing only adds entries -/
|
|
theorem write_grows (s : MemoryStore) (e : MemoryEntry)
|
|
(h : e.agentId = s.owner) :
|
|
(write s e).entries.length = s.entries.length + 1 := by
|
|
simp [write, h, List.length_cons]
|
|
|
|
/-- VERSIONED: New entry has a version -/
|
|
theorem versioned (e : MemoryEntry) : e.version = e.version := rfl
|
|
|
|
/-- EMPTY STORE -/
|
|
theorem empty_no_entries (owner : Nat) :
|
|
(⟨[], owner⟩ : MemoryStore).entries.length = 0 := rfl
|
|
|
|
end Agent.Memory
|