Expand description
Units, desired state, the graph, risk metadata and probes (§8).
Structs§
- Confidence
- Confidence in per-mille (0..=1000). Used instead of
f32to stay in the Verus subset and keep comparisons exact. - Desired
- Edge
- Evidence
probeis not in §8; status derivation cannot match evidence to probes without it (G11).- Hold
Endpoint - An endpoint a held unit still needs to reconnect (§12d
holdAllow). - Override
- Parse
Unit IdError - Probe
Def - Probe
Sandbox - Sensitivities
- A set of
Sensitivityvalues, as flags so the proofs can read it. Serialized as the list of members in declaration order, as theBTreeSetit replaces was. - Systemd
Restart Policy - UnitDef
- UnitId
- Written
<kind>:<name>for system scope and<kind>@<uid>[/<session>]:<name>for user scope, e.g.service:sshd,service@1000:pipewire,service:external:gym-upstream. Serialized in that form so it can key JSON maps.
Enums§
- Actor
- Attribution
- Cadence
- Condition
- Desired
Status - Disruption
- Ordered by how much it costs the user; §11 compares with
>=. - Edge
Kind - Edge
Origin - Override
Desired - What the override holds the unit to (§8). A
Stoppedoverride also undoes a generation activation that starts the unit again (principle 9). - Probe
Contract Error - Probe
Cost - Probe
Kind - Probe
Origin - Probe
Result - Probe
Role - Recovery
- Ordered from most to least reversible (§13 step 3).
- Scope
- Sensitivity
- Side
Effects - Unit
Kind Targetis not in §8; added for units such asgraphical-session(G4).- Until