Expand description
Delegation: two delegate kinds, one level deep.
The guard is two-layered on purpose: statically, a Delegate value
has no delegate method — minting a grandchild cannot be spelled;
dynamically, admit re-checks depth at every spawn so a hand-rolled
path cannot sneak past the type. One level is an invariant, not a
constant — a constant would imply it is tunable.
The part crates/kernel/spec/Delegation.lean specifies this module.
Structs§
- Delegate
- A delegated position. No delegate method — the compile error is the design (trybuild counterexample).
- Delegator
- The depth-zero position: the only type with a
delegatemethod (15.3-10). Who holds aDelegatoris assembly’s discipline; what aDelegatevalue can mint is this module’s — nothing.
Enums§
- Delegate
Kind - Resident delegates join society and answer for output; Ephemerals are tools — one clarification channel up, nothing else.
- Delegation
Verdict - Deliberately exhaustive verdict; the refusal (E_DELEGATION_DEPTH, three parts) is shaped by gate::spawn — the sole gate-code producer.
- Depth
- Where a spawner stands.
Functions§
- admit
- The dynamic half of the two-layer guard: a delegated position spawns nothing, whatever kind it asks for.