Skip to main content

Module unit

Module unit 

Source
Expand description

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.

§The admission boundary

Unit deliberately does not derive serde::Deserialize. An earlier revision did, and that made Unit::seal one construction path among two: a caller could decode {"op":"generate","depth":0,...} straight past every check the constructor performs. The claim that depth <= 1 was “unreachable” was false for exactly that reason — it held for the mint and not for the decoder, which is the half an attacker uses.

Decoding therefore lands in RawUnit, a transparent DTO that asserts nothing, and the only way from there to a Unit is the fallible TryFrom below, which enforces the whole v0 contract:

rulewhy
op must be Op::Elidev0 mints only what it can check; the others’ verification classes have no implementation
depth == op.depth_after(0)rejects a decoded depth 2, and any other declared depth the operation does not imply
span.start < span.enda range covering no bytes addresses nothing — this is what addressed: bool was pretending to be

Whether the span lies inside the actual source is not knowable here — it needs the bytes — so it is checked by crate::verify, and the negative case is tested there.

§What admission does NOT prove about root

Stated because the omission is easy to read as an oversight, and because a boundary whose limits are undocumented gets trusted for more than it checks.

Admission establishes that root is present and is a syntactically valid dag-cbor-profile ContentId. It establishes nothing else. In particular it does not establish that the id resolves to a stored crate::RootEvent, and a RawUnit naming an id nothing ever minted admits — and verifies — exactly like one that names a real event.

That is not a gap to be closed here. Resolving an id needs a store, and this crate has none; giving it one to answer a structural question is v0 growing the storage service its scope refuses. It is the same shape as the span rule one paragraph up: the check exists, and it lives where the data does.

The layer that owns it is the store. newt frame’s FrameStore resolves the root and reports root_kind / root_seq / root_content when it can and root_unresolved when it cannot — never a silent absence, which is the same discipline parents applies to a missing link.

Read together with the Lean referent this is a weakening paired with a strengthening. fabricated u := u.root.isNone is unrepresentable in Rust, because root is mandatory rather than an Option. What replaces the orphan is a root that dangles, which the Lean model has no way to express — its Root is an inhabitant, not a reference. agent-frame is stricter about presence and cannot be strict about resolution.

§Identity is the derivation, not the lifecycle

Unit::id is the id of the Derivation. life is deliberately outside it: superseding a root is a fact about a derivation, not a different derivation, and if it changed the id then marking a unit superseded would fork every reference to it.

Structs§

RawUnit
The transparent decode target: asserts nothing.
Unit
A single unit of compacted context, addressed by its derivation.

Enums§

AdmitError
Why a decoded unit was refused admission.
Life
Lifecycle of a unit’s root.
SealError
Why a mint was refused.