Crate agent_frame 

agent-frame — the derivation kernel.

Not “context management with a hash on it”. This is a content-addressed derivation system whose principal output happens to be a model’s working frame. Nothing in the core mentions context windows; it is about what a derived thing may assert, what it owes its source, and how far it may travel from that source before it stops being accountable.

It is the third question in a stack: agent-bridle asks what am I allowed to do, agent-mesh asks who am I talking to, agent-frame asks what do I know and how do I know it, and agent-store holds durable ordering.

A unit’s address is self-validating

The single property this crate exists to provide: given a unit’s id and the source bytes, a consumer who did not run the build can establish which material the unit represents and how it was derived.

That is a claim about the hash, not about a comment. A Unit’s id is the id of its Derivation — { op, source, span, elided, root } — so two elisions over different sources, or over different ranges of one source, cannot collide. verify::verify_unit recomputes all three claims from the bytes and compares.

An earlier revision failed this. It hashed { op, depth, root_kind, life, addressed }, which names no material: every elision with the same root kind minted the same id, and addressed: true was a declaration rather than an address. See docs/decisions/agent-frame-v0-monorepo.md.

The admission boundary is closed

Unit does not implement serde::Deserialize. Foreign bytes decode to RawUnit and cross into a Unit only through the fallible TryFrom impl, which enforces the v0 contract. Deriving Deserialize made the constructor one path of two, and the decoder was the unchecked one.

Packet is closed the same way and for the same reason. It is a MerkleNode, which carries a parent set; v0 mints a chain, whose Lean referent has no multi-parent constructor. Decoding therefore lands in RawPacket and admission refuses two or more parents — the state that satisfied is_genesis() == false and prior() == None at once.

The machine-checked referent

Every table in op and every rule in [unit] mirrors formal/ContextOps/Basic.lean, which CI builds.

Op          concise | elide | generate
depthAfter  generate => d+1 ;  concise, elide => d
Unit.wf     depth <= 1
checkOf     .elide = .rederive

v0 mints elision only

Op::Concise and Op::Generate exist in the type; Unit::seal and the admission boundary both refuse them. The referent is checkOf .elide = .rederive: elision asserts nothing and is verified by re-derivation, so every v0 assertion is a deterministic recompute — and verify::verify_unit is that recompute, not a word for one.

What this crate is not

No daemon, no socket, no async, no wire format, no storage. A layer is a crate. tests/no_service_edge.rs asserts the absence of any HTTP or inference dependency edge, so the crate stays daemon-able for free without being a daemon today.

Re-exports

pub use derivation::Derivation;

pub use derivation::Span;

pub use event::Event;

pub use event::EventBody;

pub use event::EventError;

pub use event::EventKind;

pub use event::EventOrigin;

pub use event::RawEvent;

pub use event::ReplyVerdict;

pub use op::Check;

pub use op::Op;

pub use packet::Packet;

pub use packet::PacketAdmitError;

pub use packet::PacketBody;

pub use packet::PacketId;

pub use packet::RawPacket;

pub use packet::UnitId;

pub use root::RootEvent;

pub use root::RootKind;

pub use unit::AdmitError;

pub use unit::Life;

pub use unit::RawUnit;

pub use unit::SealError;

pub use unit::Unit;

pub use verify::verify_unit;

pub use verify::verify_unit_with;

pub use verify::Mismatch;

pub use verify::SourceResolver;

pub use verify::Verified;

pub use verify::VerifyError;

Modules

derivation

Derivations: the addressed fact a unit’s identity is computed over. Derivations: the addressed fact a unit’s identity is computed over.

event

Causal events: observations, interventions, and checked derivation ancestry. Causal events over the existing derivation kernel.

op

The operation algebra: what was done, what it asserts, how it is checked. The operation algebra, mirrored from formal/ContextOps/Basic.lean.

packet

Packets: the chain, and identity over the whole body. Packets: the chain that makes “never derive from a derivation” a shape.

root

Roots: which event caused a derivation. Roots: which event caused a derivation, not merely what kind it was.

unit

Units: what a derived thing is, and what it owes its source. Units: what a derived thing is, what it owes its source, and what it takes to get one into the system.

verify

The one verification decision, and its resolver seam. One verifier. Every surface calls it.