Uh oh!
There was an error while loading. Please reload this page.
schemas: A/B fallback update contract v0.1 — never ship an update you cannot brick with (W9.2) - #212
Merged
Merged
Conversation
… cannot brick with (W9.2) The estate ships updates to fog nodes, to installed applications and to itself, and has no path back from a bad one anywhere. The nearest thing that exists is generation-based and has three holes: no attempt bound (if the candidate never reaches userspace the health timer never fires, so nothing reverts it), no candidate marking (rollback infers its target as "highest non-current generation" — a guess standing in for a pointer), and no confirm step (a health pass is fire-and-forget, so "this worked" and "this has not failed yet" are never distinguished). Lands the EVE-OS shape as a contract: GPT priority-boot attributes plus dual watchdogs. - UpdateSlot: one of exactly two slots, carrying the attribute triple a slot selector reads (bootPriority / triesRemaining / successful), the installed payload digest, and a deliberate role-vs-currentlyRunning split so the fallback slot stays describable during a trial boot. - UpdateTransaction: one apply attempt — write target, pinned probe, per-attempt boot record naming where each failure fell back to, terminal outcome with a closed rollbackReason set. - UpdateHealthProbe: the digest-pinned promotion gate. Non-empty check set with at least one blocking check; mandatory hardware+software watchdog pair; evaluatedIn closed to post-boot userspace; onProbeUnavailable closed to fail. THE INVARIANT — the currently-good slot is never overwritten by the update being applied — is enforced three ways rather than asserted once, because it is the only property whose violation is unrecoverable: by schema within a document (a top-level not/anyOf enumerating the two illegal (fromSlot, toSlot) pairs, which is expressible precisely because the slot set is closed to two; plus state:writing implies role:candidate on the slot), by schema on the settle path (settledOnSlot pinned to fromSlot on rollback or refusal), and across documents by the validator (a settled transaction's preservedPayloadDigest still equals the active slot's payloadDigest). Three design points worth the reviewer's attention: - triesRemaining is decremented by the bootloader BEFORE control transfers, so a payload that hangs before userspace still consumes an attempt. A counter decremented after a successful boot never terminates for a payload that cannot reach userspace, which is the boot loop this contract exists to forbid. - Both watchdog kinds are required. Software cannot fire through a wedged kernel because the process that would notice is the process that is stuck; hardware only learns whether something petted it, so it cannot tell working from merely running. Requiring both makes "hung" and "running but failing" terminate in the same automatic fallback. - definitionDigest is RECOMPUTED by the validator from the probe's own check set rather than read back, so a failing candidate cannot be promoted by weakening the gate it failed. A stored digest is a claim about pinning; a recomputed one is pinning. Fourteen negative vectors in fixtures/ab-update/, none in examples/. The three cross-document invariants were mutation-tested — each was made to fire before being trusted. Also wires the duplicate schema $id guardrail into `make validate`; it ran only in CI, so a local run could not reproduce the check that gates the PR.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Lands the A/B fallback update contract —
UpdateSlot,UpdateTransaction,UpdateHealthProbe— as L0 normative schemas. TRUST FABRIC W9.2.Why
The estate ships updates to fog nodes, to installed applications and to itself, and has no path back from a bad one anywhere. The nearest thing that exists is generation-based (
sourceos-syncdapplies a switch, a health timer fires atOnBootSec=120s, failure shells out to a rollback that infers its target as "the highest non-current generation"). That has three holes no amount of care closes:The lesson taken is EVE-OS's: GRUB GPT priority-boot plus dual watchdogs — never ship an update you cannot brick with.
The invariant
Enforced three ways rather than asserted once, because it is the only property whose violation is unrecoverable:
UpdateTransactioncarries a top-levelnot/anyOfenumerating the two illegal(fromSlot, toSlot)pairs. This is expressible in JSON Schema precisely because the slot set is closed to exactly two — the illegal set is finite.UpdateSlotadds the rule from the other side:state: "writing"⇒role: "candidate".settledOnSlottofromSloton rollback/refusal and totoSloton promotion. A failed update leaves the target where it started, decided by the contract rather than by whoever writes the record.preservedPayloadDigestmust still equal the active slot'spayloadDigest.Three design points worth review attention
triesRemainingis decremented by the bootloader BEFORE control transfers, so a payload that hangs before userspace still consumes an attempt. A counter decremented after a successful boot never terminates for a payload that cannot reach userspace — the boot loop this contract forbids.refusedis terminal for the same reason.containsclauses). Software cannot fire through a wedged kernel — the process that would notice is the process that is stuck. Hardware only learns whether something petted it, so it cannot tell working from merely running. Requiring both makes "hung" and "running but failing" terminate in the same automatic fallback. The validator additionally requires the hardware timeout to exceed the software one, so the software watchdog gets the first, attributable word.definitionDigestis RECOMPUTED by the validator, not read back, so a failing candidate cannot be promoted by weakening the gate it failed. A stored digest is a claim about pinning; a recomputed one is pinning.Conformance
tools/validate_ab_update_examples.pyruns five checks: schema conformance, the tranche strictness bar (additionalProperties:false,specVersionconst, anchoredurn:srcos:id pattern,typeconst == title), the recomputed probe digest, cross-document invariants, and fourteen negative vectors infixtures/ab-update/conformance.json— negative by construction, infixtures/, never inexamples/.The three cross-document invariants were mutation-tested — each was made to fire before being trusted:
payloadDigestchangedthe good slot WAS overwritten — opened with sha256:b73d… in slot A, which now holds sha256:cccc…bootPriority: 5refused but the candidate slot is still selectable (state=written, bootPriority=5) — nothing ends the boot loopminConsecutivePassesloweredprobe definitionDigest is stale: recorded sha256:2e06… but the check set hashes to sha256:4632…Validation
AJV compile (the CI step) passes for all three new schemas, and all 7 new examples pass the CI example-vs-schema path.
Also wires the duplicate
$idguardrail intomake validate— it ran only in CI, so a local run could not reproduce the check that gates the PR.Scope / honest limits
source-os/scripts/install-image.shcreates two partitions (512M ESP + one rootfs); an A/B layout needs a second rootfs slot and a GRUB config reading the priority attributes. That is not verifiable without booting a machine, and a test claiming to verify a bootloader without one would be worth less than no test. Tracked as OI-1.tauri-plugin-updater, noupdaterblock intauri.conf.json, Homebrew-cask distribution. Its owndocs/WORKPLAN-111-gaps.mdrecords this as ship-blocker Define Secure Host Interface contracts for Agent Machine terminal browser editor and agent tools #77. The contract is written to cover it —targetRefis anyurn:srcos:URN and the example set includes an application target — but there is nothing on that side to wire yet.Reference implementation (
AbUpdateMachine) lands separately insourceos-boot.