1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
//! **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.
//!
//! [`MerkleNode`]: content_addressable::MerkleNode
//!
//! # The machine-checked referent
//!
//! Every table in [`op`] and every rule in [`unit`] mirrors
//! `formal/ContextOps/Basic.lean`, which CI builds.
//!
//! ```text
//! 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.
/// Derivations: the addressed fact a unit's identity is computed over.
/// Causal events: observations, interventions, and checked derivation ancestry.
/// The operation algebra: what was done, what it asserts, how it is checked.
/// Packets: the chain, and identity over the whole body.
/// Roots: which event caused a derivation.
/// Units: what a derived thing is, and what it owes its source.
/// The one verification decision, and its resolver seam.
pub use ;
pub use ;
pub use ;
pub use ;
pub use ;
pub use ;
pub use ;