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:
| rule | why |
|---|---|
op must be Op::Elide | v0 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.end | a 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§
- Admit
Error - Why a decoded unit was refused admission.
- Life
- Lifecycle of a unit’s root.
- Seal
Error - Why a mint was refused.