diff --git a/CHANGELOG.md b/CHANGELOG.md index 1c7c806..7a99f8c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,8 @@ The format follows [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). Thi ## [Unreleased] ### Added +- A/B fallback update contract v0.1 (TRUST FABRIC W9.2): `UpdateSlot` (one of exactly two slots, carrying the GPT priority-boot attribute triple `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 `promoted`/`rolled-back`/`refused` outcome with a closed `rollbackReason` set), and `UpdateHealthProbe` (the digest-pinned promotion gate: non-empty check set with at least one blocking check, mandatory hardware+software watchdog pair enforced by two `contains` clauses, `evaluatedIn` closed to post-boot userspace, `onProbeUnavailable` closed to `fail`). **Normative invariant — the currently-good slot is never overwritten by the update being applied** — enforced three ways: by schema within a document (a top-level `not`/`anyOf` enumerating the two illegal `(fromSlot, toSlot)` pairs, plus `UpdateSlot`'s `state: writing` ⇒ `role: candidate`), by schema on the settle path (four if/then clauses pinning `settledOnSlot` to `fromSlot` on rollback/refusal and to `toSlot` on promotion), and across documents by the validator (a settled transaction's `preservedPayloadDigest` still equals the active slot's `payloadDigest`). The attempt budget follows the GPT attribute — decremented by the bootloader *before* control transfers, so a payload that hangs before userspace still consumes an attempt — and `refused` is terminal, which is what ends the boot loop. Includes a refused-update and a promoted-update example set telling two coherent end-to-end stories, fourteen negative conformance vectors (`fixtures/ab-update/conformance.json`), a `validate-ab-update-examples` target whose probe-digest check is *recomputed* rather than read back, and a normative spec note (`specs/ab-fallback-update-contract.md`). Reference implementation: `AbUpdateMachine` in `sourceos-boot`. +- `make validate` now also runs the duplicate schema `$id` guardrail, which previously ran only in CI — a local run could not reproduce the check that gates the PR. - KnowledgeNugget contract v0.1 (the estate's L2 content grain): warrant-typed knowledge fragments generalizing the production IFM warrant-typed extraction — content-addressed source spans (`docRef` + span + `sha256-` content hash), a closed four-kind warrant taxonomy (`direct-quote`/`computed`/`inferred`/`model-generated`) with evidence refs and confidence, ontology type refs (`kkoTypeRefs`), normalized `canonicalPayload`, typed provenance chain links, and `wallTime`/`logicalTime` carried verbatim from the MPCC `ConversationEvent` envelope (parity machine-enforced). Normative: `model-generated` nuggets MUST stay visibly distinguishable downstream (admissibility discounting), and `computed`/`inferred` warrants must cite evidence (schema-enforced). Includes direct-quote and model-generated examples, negative conformance vectors (`fixtures/knowledge-nugget/conformance.json`), a `validate-knowledge-nugget-examples` target, and a normative spec note (`specs/knowledge-nugget-contract.md`). - SemanticAction contract v0.1 (the declarative typed-action registry for the NL→plan compiler): ontology-typed inputs and output (KKO concept URIs recommended, shared with `KnowledgeNugget.kkoTypeRefs`), a closed constraint taxonomy (`subClassOf`/`instanceOf`/`sameAs` — polymorphism via subsumption), executor binding, registry metadata (owner + deprecated), and a two-value effect posture: actions are side-effect-free at plan-search time, and `sideEffects: "effect-request"` declares the executor emits an MPCC `EffectRequest` and defers to an `EffectDecision` rather than acting directly — no direct-mutation vocabulary exists (validator-pinned). Includes pure-lookup and effect-request examples, negative conformance vectors (`fixtures/semantic-action/conformance.json`), a `validate-semantic-action-examples` target, and a normative spec note (`specs/semantic-action-contract.md`). - MPCC event contract v0.1 (conversation + trading event family): `ConversationEvent` (the canonical 26-field conversation-fabric event — causal parents, authority context with delegation chain, visibility scope, requested/approved/actual effect references, modality, speech act), `EffectRequest` / `EffectDecision` / `EffectRecord` (the requested → approved → actual → compensated effect lifecycle with idempotency keys, referencing `PolicyDecision` / `ExecutionDecision` rather than duplicating them), `NullAbsenceRecord` (12-kind null/absence taxonomy), and the trading families `MarketDataEvent`, `OrderIntent`, `ExecutionReport`, `PositionChange`, `ReconciliationRecord` as profiles of the ConversationEvent envelope (one shared envelope vocabulary; parity machine-enforced). Includes canonical examples telling one end-to-end governed trade story, negative conformance vectors (`fixtures/mpcc-event-contract/conformance.json`), a `validate-mpcc-event-examples` target, and a normative spec note (`specs/mpcc-event-contract.md`). Provenance: SocioProphet/profit-mpcc, hardened to the policy-integrity tranche-0001 strictness bar. diff --git a/Makefile b/Makefile index ff0e2f5..54d3c0e 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,19 @@ -.PHONY: validate validate-control-plane-examples validate-nlboot-examples validate-lattice-data-governai-examples validate-ops-history-examples validate-runtime-observability-examples validate-interpretability-examples validate-lifecycle-boundary-examples validate-svf-contracts validate-sync-cycle-receipts validate-onboarding-examples validate-runtime-causality-examples validate-agentic-os-examples validate-triparty-examples validate-labor-market-examples validate-supply-chain-risk-examples validate-reasoning-examples validate-mpcc-event-examples validate-knowledge-nugget-examples validate-semantic-action-examples validate-epistemic-kernel-examples +.PHONY: validate validate-control-plane-examples validate-nlboot-examples validate-lattice-data-governai-examples validate-ops-history-examples validate-runtime-observability-examples validate-interpretability-examples validate-lifecycle-boundary-examples validate-svf-contracts validate-sync-cycle-receipts validate-onboarding-examples validate-runtime-causality-examples validate-agentic-os-examples validate-triparty-examples validate-labor-market-examples validate-supply-chain-risk-examples validate-reasoning-examples validate-mpcc-event-examples validate-knowledge-nugget-examples validate-semantic-action-examples validate-epistemic-kernel-examples validate-ab-update-examples validate-duplicate-schema-ids -validate: validate-control-plane-examples validate-nlboot-examples validate-lattice-data-governai-examples validate-ops-history-examples validate-runtime-observability-examples validate-interpretability-examples validate-lifecycle-boundary-examples validate-svf-contracts validate-sync-cycle-receipts validate-onboarding-examples validate-runtime-causality-examples validate-agentic-os-examples validate-triparty-examples validate-labor-market-examples validate-supply-chain-risk-examples validate-reasoning-examples validate-mpcc-event-examples validate-knowledge-nugget-examples validate-semantic-action-examples validate-epistemic-kernel-examples +validate: validate-control-plane-examples validate-nlboot-examples validate-lattice-data-governai-examples validate-ops-history-examples validate-runtime-observability-examples validate-interpretability-examples validate-lifecycle-boundary-examples validate-svf-contracts validate-sync-cycle-receipts validate-onboarding-examples validate-runtime-causality-examples validate-agentic-os-examples validate-triparty-examples validate-labor-market-examples validate-supply-chain-risk-examples validate-reasoning-examples validate-mpcc-event-examples validate-knowledge-nugget-examples validate-semantic-action-examples validate-epistemic-kernel-examples validate-ab-update-examples validate-duplicate-schema-ids @echo "OK: validate" +validate-ab-update-examples: + python3 -m pip install --user jsonschema >/dev/null + python3 tools/validate_ab_update_examples.py + +# The duplicate-$$id guardrail already runs in CI (.github/workflows/validate.yml) +# but was not reachable from `make validate`, so a local run could not reproduce +# the check that gates the PR. Wiring it in costs nothing and removes a way for +# local and CI verdicts to disagree. +validate-duplicate-schema-ids: + python3 scripts/check_duplicate_schema_ids.py + validate-knowledge-nugget-examples: python3 -m pip install --user jsonschema >/dev/null python3 tools/validate_knowledge_nugget_examples.py diff --git a/examples/update_health_probe.json b/examples/update_health_probe.json new file mode 100644 index 0000000..46461d9 --- /dev/null +++ b/examples/update_health_probe.json @@ -0,0 +1,59 @@ +{ + "id": "urn:srcos:update-health-probe:sourceos_node_v1", + "type": "UpdateHealthProbe", + "specVersion": "0.1.0", + "definitionDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "evaluatedIn": "post-boot-userspace", + "onProbeUnavailable": "fail", + "timeoutSeconds": 180, + "minConsecutivePasses": 2, + "description": "Promotion gate for SourceOS fog-node images and for Noetica desktop installs. Both targets run the same five checks because both fail the same way: a payload that starts, answers one request, and then cannot reach its control plane.", + "checks": [ + { + "name": "supervisor-alive", + "kind": "process-liveness", + "blocking": true, + "description": "The node supervisor reached its ready state and has stayed there for the probe window." + }, + { + "name": "local-api-200", + "kind": "endpoint-health", + "blocking": true, + "description": "The local control endpoint answers with a 200 and reports the payload version this transaction wrote." + }, + { + "name": "state-store-readable", + "kind": "data-integrity", + "blocking": true, + "description": "The persistent state store opens and its schema version is one this payload can serve. A payload that boots but cannot read the state it inherited is a brick with a login prompt." + }, + { + "name": "control-plane-reachable", + "kind": "connectivity", + "blocking": true, + "description": "The target reached its control plane at least once. Blocking on purpose: an edge node that cannot be reached cannot be remotely rolled back, so promoting it converts a recoverable fault into a site visit." + }, + { + "name": "fallback-slot-bootable", + "kind": "rollback-capability", + "blocking": true, + "description": "The other slot still holds a digest-verified payload with a non-zero boot priority. Checked BEFORE promotion because promotion is the moment the previous payload stops being the guaranteed way back." + } + ], + "watchdogs": [ + { + "kind": "software", + "timeoutSeconds": 90, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot-to-fallback", + "description": "Petted only by the health loop after a full passing check sweep, never on a timer. A supervisor that pets on a schedule proves the supervisor is alive and says nothing about the payload." + }, + { + "kind": "hardware", + "timeoutSeconds": 300, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot", + "description": "Independent SoC timer. Longer than the software timeout so the software watchdog gets the first, attributable word; it exists for the case where the kernel wedges and the software watchdog can never run to fire." + } + ] +} diff --git a/examples/update_slot.fog07_a_active.json b/examples/update_slot.fog07_a_active.json new file mode 100644 index 0000000..a8a1a89 --- /dev/null +++ b/examples/update_slot.fog07_a_active.json @@ -0,0 +1,19 @@ +{ + "id": "urn:srcos:update-slot:fog_edge_07_a", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "A", + "role": "active", + "state": "good", + "bootPriority": 15, + "triesRemaining": 0, + "successful": true, + "currentlyRunning": true, + "payloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "payloadRef": "urn:srcos:image:sourceos_node_2026.07.3", + "version": "2026.07.3", + "installedAt": "2026-07-14T11:40:02.000Z", + "lastBootedAt": "2026-07-27T02:26:59.000Z", + "lastProbeVerdict": "pass" +} diff --git a/examples/update_slot.fog07_b_unbootable.json b/examples/update_slot.fog07_b_unbootable.json new file mode 100644 index 0000000..61b8a76 --- /dev/null +++ b/examples/update_slot.fog07_b_unbootable.json @@ -0,0 +1,19 @@ +{ + "id": "urn:srcos:update-slot:fog_edge_07_b", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "B", + "role": "candidate", + "state": "unbootable", + "bootPriority": 0, + "triesRemaining": 0, + "successful": false, + "currentlyRunning": false, + "payloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0", + "payloadRef": "urn:srcos:image:sourceos_node_2026.07.4", + "version": "2026.07.4", + "installedAt": "2026-07-27T02:17:11.000Z", + "lastBootedAt": "2026-07-27T02:26:12.000Z", + "lastProbeVerdict": "fail" +} diff --git a/examples/update_slot.noetica_a_fallback.json b/examples/update_slot.noetica_a_fallback.json new file mode 100644 index 0000000..2a3c744 --- /dev/null +++ b/examples/update_slot.noetica_a_fallback.json @@ -0,0 +1,19 @@ +{ + "id": "urn:srcos:update-slot:noetica_a41_a", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:install:noetica_desktop_a41", + "slot": "A", + "role": "candidate", + "state": "good", + "bootPriority": 14, + "triesRemaining": 0, + "successful": true, + "currentlyRunning": false, + "payloadDigest": "sha256:aa850dde865a39601a8b2f5af88cfb18878a59d91f4fc01b2e465826da90d356", + "payloadRef": "urn:srcos:release:noetica_desktop_1.8.2", + "version": "1.8.2", + "installedAt": "2026-06-30T18:22:40.000Z", + "lastBootedAt": "2026-07-28T09:01:12.000Z", + "lastProbeVerdict": "pass" +} diff --git a/examples/update_slot.noetica_b_active.json b/examples/update_slot.noetica_b_active.json new file mode 100644 index 0000000..9fb4703 --- /dev/null +++ b/examples/update_slot.noetica_b_active.json @@ -0,0 +1,19 @@ +{ + "id": "urn:srcos:update-slot:noetica_a41_b", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:install:noetica_desktop_a41", + "slot": "B", + "role": "active", + "state": "good", + "bootPriority": 15, + "triesRemaining": 0, + "successful": true, + "currentlyRunning": true, + "payloadDigest": "sha256:22e07d29331b31e37a137ce875de35689ad1d719690cc7a0a6e592a76cb7fcb8", + "payloadRef": "urn:srcos:release:noetica_desktop_1.9.0", + "version": "1.9.0", + "installedAt": "2026-07-28T09:07:55.000Z", + "lastBootedAt": "2026-07-28T09:08:21.000Z", + "lastProbeVerdict": "pass" +} diff --git a/examples/update_transaction.promoted.json b/examples/update_transaction.promoted.json new file mode 100644 index 0000000..b5e485f --- /dev/null +++ b/examples/update_transaction.promoted.json @@ -0,0 +1,29 @@ +{ + "id": "urn:srcos:update-transaction:noetica_a41_0007", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:install:noetica_desktop_a41", + "fromSlot": "A", + "toSlot": "B", + "preservedPayloadDigest": "sha256:aa850dde865a39601a8b2f5af88cfb18878a59d91f4fc01b2e465826da90d356", + "candidatePayloadDigest": "sha256:22e07d29331b31e37a137ce875de35689ad1d719690cc7a0a6e592a76cb7fcb8", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 2, + "outcome": "promoted", + "rollbackReason": null, + "openedAt": "2026-07-28T09:02:00.000Z", + "settledAt": "2026-07-28T09:14:38.000Z", + "settledOnSlot": "B", + "receiptRef": "urn:srcos:reasoning:receipt:noetica_a41_update_0007", + "attempts": [ + { + "attemptNumber": 1, + "startedAt": "2026-07-28T09:08:21.000Z", + "result": "pass", + "fellBackTo": null, + "triesRemainingAfter": 1, + "detail": "All five blocking checks passed on two consecutive sweeps, satisfying minConsecutivePasses; successful set by userspace." + } + ] +} diff --git a/examples/update_transaction.refused.json b/examples/update_transaction.refused.json new file mode 100644 index 0000000..6095a0f --- /dev/null +++ b/examples/update_transaction.refused.json @@ -0,0 +1,37 @@ +{ + "id": "urn:srcos:update-transaction:fog_edge_07_0042", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "fromSlot": "A", + "toSlot": "B", + "preservedPayloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "candidatePayloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 2, + "outcome": "refused", + "rollbackReason": "attempts-exhausted", + "openedAt": "2026-07-27T02:10:00.000Z", + "settledAt": "2026-07-27T02:31:44.000Z", + "settledOnSlot": "A", + "receiptRef": "urn:srcos:reasoning:receipt:fog_edge_07_update_0042", + "attempts": [ + { + "attemptNumber": 1, + "startedAt": "2026-07-27T02:18:03.000Z", + "result": "probe-failed", + "fellBackTo": "A", + "triesRemainingAfter": 1, + "detail": "control-plane-reachable failed: no successful control-plane call within the 180s probe window." + }, + { + "attemptNumber": 2, + "startedAt": "2026-07-27T02:26:12.000Z", + "result": "watchdog-expired", + "fellBackTo": "A", + "triesRemainingAfter": 0, + "detail": "software watchdog expired after 90s without a pet; expiryAction reboot-to-fallback zeroed the candidate's remaining tries." + } + ] +} diff --git a/fixtures/ab-update/conformance.json b/fixtures/ab-update/conformance.json new file mode 100644 index 0000000..8cc3439 --- /dev/null +++ b/fixtures/ab-update/conformance.json @@ -0,0 +1,355 @@ +{ + "description": "Negative conformance vectors for the A/B fallback update contract v0.1. Each document MUST FAIL validation against its schema for the stated reason; tools/validate_ab_update_examples.py enforces this and fails the build if any of them validates. Every case is otherwise complete, so a failure is attributable to the named defect rather than to a missing required field. The vectors encode the failure modes that make an update irreversible: writing the slot you fall back to, settling on the slot that failed, promoting through a gate that cannot fail, an unbootable slot the selector will still pick, and a watchdog pair with only one kind in it.", + "cases": [ + { + "schema": "UpdateTransaction.json", + "reason": "fromSlot == toSlot writes the known-good slot. This is the defect the whole family exists to prevent and it must be rejected by schema, not by a runtime check a caller can skip.", + "document": { + "id": "urn:srcos:update-transaction:neg_writes_active_slot", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "fromSlot": "A", + "toSlot": "A", + "preservedPayloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "candidatePayloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 2, + "outcome": "pending", + "rollbackReason": null, + "openedAt": "2026-07-27T02:10:00.000Z", + "settledAt": null, + "settledOnSlot": null, + "attempts": [] + } + }, + { + "schema": "UpdateTransaction.json", + "reason": "A refused transaction that settled on toSlot left the target running the candidate that exhausted its attempts. Refusal must return the target to fromSlot.", + "document": { + "id": "urn:srcos:update-transaction:neg_refused_on_candidate", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "fromSlot": "A", + "toSlot": "B", + "preservedPayloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "candidatePayloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 2, + "outcome": "refused", + "rollbackReason": "attempts-exhausted", + "openedAt": "2026-07-27T02:10:00.000Z", + "settledAt": "2026-07-27T02:31:44.000Z", + "settledOnSlot": "B", + "attempts": [ + { + "attemptNumber": 1, + "startedAt": "2026-07-27T02:18:03.000Z", + "result": "probe-failed", + "fellBackTo": "A", + "triesRemainingAfter": 1 + }, + { + "attemptNumber": 2, + "startedAt": "2026-07-27T02:26:12.000Z", + "result": "watchdog-expired", + "fellBackTo": "A", + "triesRemainingAfter": 0 + } + ] + } + }, + { + "schema": "UpdateTransaction.json", + "reason": "A rolled-back transaction with a null rollbackReason is an unattributed rollback — indistinguishable from one that was never diagnosed.", + "document": { + "id": "urn:srcos:update-transaction:neg_rollback_unattributed", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "fromSlot": "A", + "toSlot": "B", + "preservedPayloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "candidatePayloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 2, + "outcome": "rolled-back", + "rollbackReason": null, + "openedAt": "2026-07-27T02:10:00.000Z", + "settledAt": "2026-07-27T02:20:00.000Z", + "settledOnSlot": "A", + "attempts": [] + } + }, + { + "schema": "UpdateTransaction.json", + "reason": "A promoted transaction carrying a rollbackReason claims both that the update succeeded and that it was rolled back.", + "document": { + "id": "urn:srcos:update-transaction:neg_promoted_with_reason", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:install:noetica_desktop_a41", + "fromSlot": "A", + "toSlot": "B", + "preservedPayloadDigest": "sha256:aa850dde865a39601a8b2f5af88cfb18878a59d91f4fc01b2e465826da90d356", + "candidatePayloadDigest": "sha256:22e07d29331b31e37a137ce875de35689ad1d719690cc7a0a6e592a76cb7fcb8", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 2, + "outcome": "promoted", + "rollbackReason": "probe-failed", + "openedAt": "2026-07-28T09:02:00.000Z", + "settledAt": "2026-07-28T09:14:38.000Z", + "settledOnSlot": "B", + "attempts": [ + { + "attemptNumber": 1, + "startedAt": "2026-07-28T09:08:21.000Z", + "result": "pass", + "fellBackTo": null, + "triesRemainingAfter": 1 + } + ] + } + }, + { + "schema": "UpdateTransaction.json", + "reason": "maxAttempts above the GPT tries width is an attempt budget the on-device attribute cannot hold — in practice an unbounded retry, which is a boot loop.", + "document": { + "id": "urn:srcos:update-transaction:neg_unbounded_attempts", + "type": "UpdateTransaction", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "fromSlot": "A", + "toSlot": "B", + "preservedPayloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "candidatePayloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0", + "healthProbeRef": "urn:srcos:update-health-probe:sourceos_node_v1", + "healthProbeDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "maxAttempts": 99, + "outcome": "pending", + "rollbackReason": null, + "openedAt": "2026-07-27T02:10:00.000Z", + "settledAt": null, + "settledOnSlot": null, + "attempts": [] + } + }, + { + "schema": "UpdateSlot.json", + "reason": "state 'writing' on the active slot is the write that destroys the way back. The if/then clause forbids it.", + "document": { + "id": "urn:srcos:update-slot:neg_writing_active", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "A", + "role": "active", + "state": "writing", + "bootPriority": 15, + "triesRemaining": 0, + "successful": true, + "currentlyRunning": true, + "payloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e" + } + }, + { + "schema": "UpdateSlot.json", + "reason": "An active slot with successful=false is a fallback that was never proven good — the target has nowhere safe to return to.", + "document": { + "id": "urn:srcos:update-slot:neg_active_unproven", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "A", + "role": "active", + "state": "written", + "bootPriority": 15, + "triesRemaining": 1, + "successful": false, + "currentlyRunning": true, + "payloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e" + } + }, + { + "schema": "UpdateSlot.json", + "reason": "An unbootable slot with a non-zero bootPriority is still selectable by the bootloader — the marking that makes fallback permanent was not applied.", + "document": { + "id": "urn:srcos:update-slot:neg_unbootable_selectable", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "B", + "role": "candidate", + "state": "unbootable", + "bootPriority": 3, + "triesRemaining": 0, + "successful": false, + "currentlyRunning": false, + "payloadDigest": "sha256:9da88dc197887a52961b7846083b868e0a2e4ed0f1846abdfa6e9f4d566c66d0" + } + }, + { + "schema": "UpdateSlot.json", + "reason": "successful=true without a payloadDigest records a slot as good without pinning what was proven good.", + "document": { + "id": "urn:srcos:update-slot:neg_good_unpinned", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "B", + "role": "candidate", + "state": "good", + "bootPriority": 14, + "triesRemaining": 0, + "successful": true, + "currentlyRunning": false + } + }, + { + "schema": "UpdateSlot.json", + "reason": "Unknown top-level property must be rejected (additionalProperties: false).", + "document": { + "id": "urn:srcos:update-slot:neg_unknown_prop", + "type": "UpdateSlot", + "specVersion": "0.1.0", + "targetRef": "urn:srcos:node:sourceos_fog_edge_07", + "slot": "A", + "role": "active", + "state": "good", + "bootPriority": 15, + "triesRemaining": 0, + "successful": true, + "currentlyRunning": true, + "payloadDigest": "sha256:b73d34fdc15b73c8efeb4527811459b62addf6e4c4a69730f81244ff0beab97e", + "forceBootAnyway": true + } + }, + { + "schema": "UpdateHealthProbe.json", + "reason": "A watchdog set with no hardware watchdog cannot fire through a wedged kernel — the process that would notice is the process that is stuck.", + "document": { + "id": "urn:srcos:update-health-probe:neg_software_only", + "type": "UpdateHealthProbe", + "specVersion": "0.1.0", + "definitionDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "evaluatedIn": "post-boot-userspace", + "onProbeUnavailable": "fail", + "timeoutSeconds": 180, + "minConsecutivePasses": 1, + "checks": [ + { "name": "supervisor-alive", "kind": "process-liveness", "blocking": true } + ], + "watchdogs": [ + { + "kind": "software", + "timeoutSeconds": 90, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot-to-fallback" + }, + { + "kind": "software", + "timeoutSeconds": 120, + "pettedBy": "urn:srcos:component:node_secondary_loop", + "expiryAction": "reboot" + } + ] + } + }, + { + "schema": "UpdateHealthProbe.json", + "reason": "onProbeUnavailable other than 'fail' promotes payloads through a gate that never ran.", + "document": { + "id": "urn:srcos:update-health-probe:neg_inconclusive_passes", + "type": "UpdateHealthProbe", + "specVersion": "0.1.0", + "definitionDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "evaluatedIn": "post-boot-userspace", + "onProbeUnavailable": "pass", + "timeoutSeconds": 180, + "minConsecutivePasses": 1, + "checks": [ + { "name": "supervisor-alive", "kind": "process-liveness", "blocking": true } + ], + "watchdogs": [ + { + "kind": "software", + "timeoutSeconds": 90, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot-to-fallback" + }, + { + "kind": "hardware", + "timeoutSeconds": 300, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot" + } + ] + } + }, + { + "schema": "UpdateHealthProbe.json", + "reason": "A probe evaluated in the bootloader can only observe that control transferred. Letting the boot path declare its own success is having no gate at all.", + "document": { + "id": "urn:srcos:update-health-probe:neg_bootloader_evaluated", + "type": "UpdateHealthProbe", + "specVersion": "0.1.0", + "definitionDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "evaluatedIn": "bootloader", + "onProbeUnavailable": "fail", + "timeoutSeconds": 180, + "minConsecutivePasses": 1, + "checks": [ + { "name": "supervisor-alive", "kind": "process-liveness", "blocking": true } + ], + "watchdogs": [ + { + "kind": "software", + "timeoutSeconds": 90, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot-to-fallback" + }, + { + "kind": "hardware", + "timeoutSeconds": 300, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot" + } + ] + } + }, + { + "schema": "UpdateHealthProbe.json", + "reason": "A probe with an empty check set passes everything while producing a passing record — worse than no probe, because it looks like evidence.", + "document": { + "id": "urn:srcos:update-health-probe:neg_empty_checks", + "type": "UpdateHealthProbe", + "specVersion": "0.1.0", + "definitionDigest": "sha256:2e0672e76fbc68c30cad6542a5f0a778596cb8700e77a222715738d4731da86c", + "evaluatedIn": "post-boot-userspace", + "onProbeUnavailable": "fail", + "timeoutSeconds": 180, + "minConsecutivePasses": 1, + "checks": [], + "watchdogs": [ + { + "kind": "software", + "timeoutSeconds": 90, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot-to-fallback" + }, + { + "kind": "hardware", + "timeoutSeconds": 300, + "pettedBy": "urn:srcos:component:node_supervisor_health_loop", + "expiryAction": "reboot" + } + ] + } + } + ] +} diff --git a/schemas/README.md b/schemas/README.md index 456764c..a1e0a33 100644 --- a/schemas/README.md +++ b/schemas/README.md @@ -5,6 +5,26 @@ This directory contains the JSON Schema (draft 2020-12) files that make up the S --- +## Recent additions — A/B Fallback Update Contract v0.1 + +The dual-slot update contract adds the following top-level schemas: + +| File | Type | URN prefix | +|------|------|-----------| +| `UpdateSlot.json` | UpdateSlot | `urn:srcos:update-slot:` | +| `UpdateTransaction.json` | UpdateTransaction | `urn:srcos:update-transaction:` | +| `UpdateHealthProbe.json` | UpdateHealthProbe | `urn:srcos:update-health-probe:` | + +These types support: +- the A/B slot model the estate had nowhere: two slots carrying the GPT attribute triple (`bootPriority`, `triesRemaining`, `successful`) that a priority-boot selector reads, with `role` (active/candidate) and `currentlyRunning` deliberately separate so the fallback slot stays describable during a trial boot +- **the invariant the family exists for — the currently-good slot is never overwritten by the update being applied.** Enforced by schema within a document (`UpdateTransaction`'s `not`/`anyOf` over the two illegal `(fromSlot, toSlot)` pairs; `UpdateSlot`'s `state: writing` ⇒ `role: candidate`), by schema on the settle path (`settledOnSlot` pinned to `fromSlot` on rollback/refusal), and across documents by the validator (`preservedPayloadDigest` still equals the active slot's `payloadDigest`) +- automatic rollback with a bounded attempt budget: `triesRemaining` is decremented by the bootloader *before* control transfers, so a payload that hangs before userspace still consumes an attempt; `refused` is terminal and is what ends the boot loop +- a digest-pinned promotion gate: `UpdateHealthProbe.definitionDigest` is recomputed by the validator from the probe's own check set, so a failing candidate cannot be promoted by weakening the gate it failed. Normative: promotion is evaluated in post-boot userspace only, an inconclusive probe is a `fail`, and a hardware+software watchdog pair is mandatory (two `contains` clauses) — software cannot fire through a wedged kernel, hardware cannot tell working from merely running + +Validation: `make validate-ab-update-examples` (schema conformance, tranche strictness bar, recomputed probe digest, cross-document invariants, and fourteen negative vectors under `fixtures/ab-update/`). Normative notes: `specs/ab-fallback-update-contract.md`. Reference implementation: `AbUpdateMachine` in `sourceos-boot`. + +--- + ## Recent additions — Knowledge Nugget + Semantic Action registry v0.1 The L2 content-grain and typed-action-registry contracts add the following top-level schemas: diff --git a/schemas/UpdateHealthProbe.json b/schemas/UpdateHealthProbe.json new file mode 100644 index 0000000..3b7873e --- /dev/null +++ b/schemas/UpdateHealthProbe.json @@ -0,0 +1,151 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://schemas.srcos.ai/v2/UpdateHealthProbe.json", + "title": "UpdateHealthProbe", + "description": "The pinned definition of what a candidate slot must prove before it may be promoted. Separate from the transaction on purpose: the probe is authored and digest-pinned BEFORE the payload it gates, so an update cannot ship a weakened version of its own gate. Two detection surfaces are mandatory and they answer different questions. The check set answers 'does the payload work'. The watchdog pair answers 'is the payload alive' — and it takes both kinds, because a software watchdog cannot fire when the kernel wedges (the process that would notice is the process that is stuck), while a hardware watchdog only ever learns whether something petted it and so cannot distinguish a live-but-broken payload from a healthy one. Requiring one of each is what makes 'hung' and 'running but failing' terminate in the same automatic fallback.", + "type": "object", + "additionalProperties": false, + "required": [ + "id", + "type", + "specVersion", + "definitionDigest", + "evaluatedIn", + "onProbeUnavailable", + "timeoutSeconds", + "minConsecutivePasses", + "checks", + "watchdogs" + ], + "properties": { + "id": { + "type": "string", + "pattern": "^urn:srcos:update-health-probe:[A-Za-z0-9._~-]+$", + "description": "Stable URN identifier. Pattern: urn:srcos:update-health-probe:" + }, + "type": { + "const": "UpdateHealthProbe", + "description": "Discriminator constant — always \"UpdateHealthProbe\"." + }, + "specVersion": { + "const": "0.1.0", + "description": "A/B fallback update contract version, pinned. Changing this const is a contract change." + }, + "definitionDigest": { + "type": "string", + "pattern": "^sha256:[a-f0-9]{64}$", + "description": "Content digest of the normative check set and watchdog configuration. An UpdateTransaction pins this value; if the probe definition is edited after a transaction is opened, the digests diverge and the family validator rejects the pair. This is what stops a failing candidate from being promoted by relaxing the gate it failed." + }, + "evaluatedIn": { + "const": "post-boot-userspace", + "description": "Where the probe runs. Closed to post-boot userspace: the bootloader can observe that control transferred and nothing more, so it is structurally incapable of evaluating health. Any design that lets the boot path declare its own success has no gate at all." + }, + "onProbeUnavailable": { + "const": "fail", + "description": "Verdict when the probe cannot be executed or returns inconclusive. Closed to fail. An update system that reads 'could not determine' as 'proceed' promotes broken payloads through probes that never ran — the declared-unenforced gap, applied to the one gate that stands between a target and a brick." + }, + "timeoutSeconds": { + "type": "number", + "exclusiveMinimum": 0, + "description": "Wall-clock budget for one full probe evaluation. Exceeding it is a fail, not a retry: a probe with no deadline holds the candidate in 'trying' forever, which is a boot loop wearing different clothes." + }, + "minConsecutivePasses": { + "type": "integer", + "minimum": 1, + "description": "Consecutive passing evaluations required before successful may be set. Values above 1 buy protection against a payload that comes up briefly and then degrades; the cost is a longer window in which the target is running unpromoted." + }, + "checks": { + "type": "array", + "minItems": 1, + "uniqueItems": true, + "description": "The check set. Non-empty by construction — a probe with no checks passes everything, which is worse than having no probe because it produces a passing record.", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["name", "kind", "blocking"], + "properties": { + "name": { + "type": "string", + "minLength": 1, + "maxLength": 120, + "description": "Stable check name, unique within this probe." + }, + "kind": { + "type": "string", + "enum": ["process-liveness", "endpoint-health", "data-integrity", "connectivity", "rollback-capability"], + "description": "What the check exercises. rollback-capability is deliberately in the closed set: a candidate that cannot demonstrate it is still able to roll back must not be promoted, because promotion is the moment the previous payload stops being guaranteed." + }, + "blocking": { + "type": "boolean", + "description": "Whether failing this check fails the probe. At least one check must be blocking (enforced by the family validator) — a probe composed entirely of advisory checks cannot gate anything." + }, + "description": { + "type": "string", + "minLength": 1, + "description": "What this check asserts and why it is part of the promotion gate." + } + } + } + }, + "watchdogs": { + "type": "array", + "minItems": 2, + "maxItems": 4, + "uniqueItems": true, + "allOf": [ + { + "contains": { + "type": "object", + "properties": { "kind": { "const": "hardware" } }, + "required": ["kind"] + } + }, + { + "contains": { + "type": "object", + "properties": { "kind": { "const": "software" } }, + "required": ["kind"] + } + } + ], + "description": "Liveness bounds armed for the trial boot. At least one hardware and one software watchdog are required (enforced by the two contains clauses). Neither kind alone closes the gap: software cannot fire through a wedged kernel, hardware cannot tell working from merely running.", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["kind", "timeoutSeconds", "pettedBy", "expiryAction"], + "properties": { + "kind": { + "type": "string", + "enum": ["hardware", "software"], + "description": "hardware = an independent timer (SoC/BMC/TPM-adjacent) that resets the target regardless of software state; software = a supervisor process that only pets while its checks pass." + }, + "timeoutSeconds": { + "type": "number", + "exclusiveMinimum": 0, + "description": "Time without a pet before expiryAction fires. The hardware timeout must exceed the software timeout (enforced by the family validator) so the software watchdog gets the first, attributable word; inverted, every software-detectable fault is reported as an unexplained hardware reset." + }, + "pettedBy": { + "type": "string", + "minLength": 1, + "description": "The component that pets this watchdog. A software watchdog must be petted by something downstream of the health checks, not by a timer — a supervisor that pets on a schedule is a liveness signal for the supervisor, not for the payload." + }, + "expiryAction": { + "type": "string", + "enum": ["reboot-to-fallback", "reboot"], + "description": "What expiry does. reboot-to-fallback additionally zeroes the candidate's remaining tries before resetting, converting a hang into an immediate fallback rather than one that costs the full attempt budget." + }, + "description": { + "type": "string", + "minLength": 1, + "description": "What this watchdog covers and why its timeout is set where it is." + } + } + } + }, + "description": { + "type": "string", + "minLength": 1, + "description": "What this probe gates and for which class of target." + } + } +} diff --git a/schemas/UpdateSlot.json b/schemas/UpdateSlot.json new file mode 100644 index 0000000..862f03f --- /dev/null +++ b/schemas/UpdateSlot.json @@ -0,0 +1,163 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://schemas.srcos.ai/v2/UpdateSlot.json", + "title": "UpdateSlot", + "description": "One of exactly two boot/install slots on an update target. Models the GPT priority-boot attribute triple (bootPriority, triesRemaining, successful) that a GRUB/bootloader slot selector reads, plus the payload digest installed in the slot. THE INVARIANT THIS FAMILY EXISTS FOR: the slot holding the currently-good payload is never the write target of an update. It is enforced structurally here (state 'writing' requires role 'candidate') and again on UpdateTransaction (fromSlot != toSlot, enumerated over the closed two-slot set). Role and running are deliberately separate: 'active' is the known-good fallback the target returns to, 'currentlyRunning' is what the CPU is executing right now — during a trial boot the candidate is running while the active slot is still the fallback, and collapsing the two would make the fallback slot indescribable exactly when it matters.", + "type": "object", + "additionalProperties": false, + "required": [ + "id", + "type", + "specVersion", + "targetRef", + "slot", + "role", + "state", + "bootPriority", + "triesRemaining", + "successful", + "currentlyRunning" + ], + "allOf": [ + { + "if": { + "properties": { "state": { "const": "writing" } }, + "required": ["state"] + }, + "then": { + "properties": { "role": { "const": "candidate" } }, + "required": ["role"] + } + }, + { + "if": { + "properties": { "role": { "const": "active" } }, + "required": ["role"] + }, + "then": { + "properties": { + "successful": { "const": true }, + "bootPriority": { "minimum": 1 } + }, + "required": ["successful", "bootPriority"] + } + }, + { + "if": { + "properties": { "state": { "const": "unbootable" } }, + "required": ["state"] + }, + "then": { + "properties": { + "bootPriority": { "const": 0 }, + "successful": { "const": false } + }, + "required": ["bootPriority", "successful"] + } + }, + { + "if": { + "properties": { "state": { "const": "good" } }, + "required": ["state"] + }, + "then": { + "properties": { "successful": { "const": true } }, + "required": ["successful"] + } + }, + { + "if": { + "properties": { "successful": { "const": true } }, + "required": ["successful"] + }, + "then": { + "required": ["payloadDigest"] + } + } + ], + "properties": { + "id": { + "type": "string", + "pattern": "^urn:srcos:update-slot:[A-Za-z0-9._~-]+$", + "description": "Stable URN identifier. Pattern: urn:srcos:update-slot:" + }, + "type": { + "const": "UpdateSlot", + "description": "Discriminator constant — always \"UpdateSlot\"." + }, + "specVersion": { + "const": "0.1.0", + "description": "A/B fallback update contract version, pinned. Changing this const is a contract change." + }, + "targetRef": { + "type": "string", + "pattern": "^urn:srcos:", + "description": "URN of the update target owning this slot — a node, device, or installed application. Exactly two UpdateSlot documents share one targetRef." + }, + "slot": { + "type": "string", + "enum": ["A", "B"], + "description": "Physical slot label. Closed to exactly two at v0.1: A/B is not a shorthand for 'N slots'. The fallback guarantee is that one slot is always retained known-good while the other is written, and that argument does not generalise to N without a new arbitration rule — a third slot is a contract change, not a new enum value." + }, + "role": { + "type": "string", + "enum": ["active", "candidate"], + "description": "active = the known-good slot the target falls back to; candidate = the slot an update writes to and trials. Roles swap only on promotion (a passing health probe), never on a boot attempt." + }, + "state": { + "type": "string", + "enum": ["empty", "writing", "written", "trying", "good", "unbootable"], + "description": "Slot lifecycle. empty = never written; writing = receiving a payload (candidate only, enforced by if/then); written = payload complete and digest-verified, not yet booted; trying = armed and being trial-booted with the probe pending; good = health probe passed and successful was set; unbootable = priority zeroed, the selector will never choose it again." + }, + "bootPriority": { + "type": "integer", + "minimum": 0, + "maximum": 15, + "description": "GPT priority attribute. The slot selector boots the highest-priority slot that is either successful or still has tries remaining. 0 means unbootable and is the value written when a candidate exhausts its tries — that write is what makes fallback automatic rather than operator-driven." + }, + "triesRemaining": { + "type": "integer", + "minimum": 0, + "maximum": 7, + "description": "GPT tries attribute. Decremented by the bootloader BEFORE control is handed to the slot, so a payload that hangs before userspace still consumes an attempt. A counter decremented after boot would never terminate for a payload that cannot reach userspace — which is precisely the boot loop this contract forbids." + }, + "successful": { + "type": "boolean", + "description": "GPT successful attribute. Set true ONLY by userspace after the pinned health probe passes; the bootloader never sets it. A bootloader that marks its own boot successful is attesting that control transferred, not that the payload works, and that is the failure this whole family is built to prevent." + }, + "currentlyRunning": { + "type": "boolean", + "description": "Whether the target is executing this slot right now. Distinct from role: during a trial boot the candidate is running while the active slot remains the known-good fallback. Exactly one slot per targetRef may be true (cross-document invariant, enforced by the family validator)." + }, + "payloadDigest": { + "type": "string", + "pattern": "^sha256:[a-f0-9]{64}$", + "description": "Content digest of the payload installed in this slot. Required once successful is true. Digest-pinned, never a tag: a slot recorded as good by a moving tag cannot be proven to still hold the payload that passed the probe." + }, + "payloadRef": { + "type": "string", + "minLength": 1, + "description": "Stable reference of the payload artifact (image URN, release URN, registry reference)." + }, + "version": { + "type": "string", + "minLength": 1, + "description": "Human-readable version string of the payload in this slot. Advisory only — arbitration reads bootPriority/triesRemaining/successful, never this field." + }, + "installedAt": { + "type": ["string", "null"], + "format": "date-time", + "description": "When the current payload finished writing and passed digest verification. Null while empty." + }, + "lastBootedAt": { + "type": ["string", "null"], + "format": "date-time", + "description": "When the target last handed control to this slot. Null if never booted." + }, + "lastProbeVerdict": { + "type": ["string", "null"], + "enum": ["pass", "fail", null], + "description": "Verdict of the most recent health probe run against this slot. Null before the first run. This is an operations verdict, not a claims verdict: it says the payload works, never that it is correct." + } + } +} diff --git a/schemas/UpdateTransaction.json b/schemas/UpdateTransaction.json new file mode 100644 index 0000000..505a6da --- /dev/null +++ b/schemas/UpdateTransaction.json @@ -0,0 +1,264 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://schemas.srcos.ai/v2/UpdateTransaction.json", + "title": "UpdateTransaction", + "description": "One attempt to move an update target from the payload in its active slot to a new payload, with an enforced path back. Records the write target, the pinned health probe, every boot attempt and its outcome, and which slot the target ended up on. THE INVARIANT: fromSlot != toSlot — the known-good slot is never the write target. Because the slot set is closed to exactly two, that invariant is enumerable and is enforced here by schema (the `not`/`anyOf` clause) rather than by prose or by a runtime check that a caller can forget. A second family of if/then clauses enforces the other half of the guarantee: a transaction that does not end in promotion must leave the target running the slot it started on. Together those two say the whole thing — you may fail an update, but you may not lose the payload that worked.", + "type": "object", + "additionalProperties": false, + "required": [ + "id", + "type", + "specVersion", + "targetRef", + "fromSlot", + "toSlot", + "preservedPayloadDigest", + "candidatePayloadDigest", + "healthProbeRef", + "healthProbeDigest", + "maxAttempts", + "outcome", + "attempts", + "openedAt" + ], + "not": { + "anyOf": [ + { + "properties": { + "fromSlot": { "const": "A" }, + "toSlot": { "const": "A" } + }, + "required": ["fromSlot", "toSlot"] + }, + { + "properties": { + "fromSlot": { "const": "B" }, + "toSlot": { "const": "B" } + }, + "required": ["fromSlot", "toSlot"] + } + ] + }, + "allOf": [ + { + "if": { + "properties": { "outcome": { "enum": ["rolled-back", "refused"] } }, + "required": ["outcome"] + }, + "then": { + "required": ["rollbackReason", "settledAt", "settledOnSlot"], + "properties": { "rollbackReason": { "type": "string" } } + } + }, + { + "if": { + "properties": { "outcome": { "const": "refused" } }, + "required": ["outcome"] + }, + "then": { + "properties": { "rollbackReason": { "const": "attempts-exhausted" } }, + "required": ["rollbackReason"] + } + }, + { + "if": { + "properties": { "outcome": { "const": "promoted" } }, + "required": ["outcome"] + }, + "then": { + "required": ["settledAt", "settledOnSlot"], + "properties": { "rollbackReason": { "type": "null" } } + } + }, + { + "if": { + "properties": { "outcome": { "const": "pending" } }, + "required": ["outcome"] + }, + "then": { + "properties": { + "settledAt": { "type": "null" }, + "settledOnSlot": { "type": "null" } + } + } + }, + { + "if": { + "properties": { + "outcome": { "const": "promoted" }, + "toSlot": { "const": "A" } + }, + "required": ["outcome", "toSlot"] + }, + "then": { "properties": { "settledOnSlot": { "const": "A" } } } + }, + { + "if": { + "properties": { + "outcome": { "const": "promoted" }, + "toSlot": { "const": "B" } + }, + "required": ["outcome", "toSlot"] + }, + "then": { "properties": { "settledOnSlot": { "const": "B" } } } + }, + { + "if": { + "properties": { + "outcome": { "enum": ["rolled-back", "refused"] }, + "fromSlot": { "const": "A" } + }, + "required": ["outcome", "fromSlot"] + }, + "then": { "properties": { "settledOnSlot": { "const": "A" } } } + }, + { + "if": { + "properties": { + "outcome": { "enum": ["rolled-back", "refused"] }, + "fromSlot": { "const": "B" } + }, + "required": ["outcome", "fromSlot"] + }, + "then": { "properties": { "settledOnSlot": { "const": "B" } } } + } + ], + "properties": { + "id": { + "type": "string", + "pattern": "^urn:srcos:update-transaction:[A-Za-z0-9._~-]+$", + "description": "Stable URN identifier. Pattern: urn:srcos:update-transaction:" + }, + "type": { + "const": "UpdateTransaction", + "description": "Discriminator constant — always \"UpdateTransaction\"." + }, + "specVersion": { + "const": "0.1.0", + "description": "A/B fallback update contract version, pinned. Changing this const is a contract change." + }, + "targetRef": { + "type": "string", + "pattern": "^urn:srcos:", + "description": "URN of the update target — the same targetRef carried by both of its UpdateSlot documents." + }, + "fromSlot": { + "type": "string", + "enum": ["A", "B"], + "description": "The slot that was active (known-good) when this transaction opened. It is the fallback for the whole life of the transaction and must not be written." + }, + "toSlot": { + "type": "string", + "enum": ["A", "B"], + "description": "The slot the candidate payload is written to. Must differ from fromSlot — enforced by the top-level `not` clause, which enumerates the two illegal pairs because the slot set is closed." + }, + "preservedPayloadDigest": { + "type": "string", + "pattern": "^sha256:[a-f0-9]{64}$", + "description": "Digest of the payload in fromSlot at open. The family validator asserts this still matches the active slot's payloadDigest after the transaction settles — that comparison is the executable form of 'the good slot was never overwritten', as opposed to an assurance that it was not." + }, + "candidatePayloadDigest": { + "type": "string", + "pattern": "^sha256:[a-f0-9]{64}$", + "description": "Digest of the payload being written to toSlot, verified after write and before the slot is armed. A write that ends with a digest mismatch settles as rolled-back and never arms." + }, + "healthProbeRef": { + "type": "string", + "pattern": "^urn:srcos:update-health-probe:[A-Za-z0-9._~-]+$", + "description": "URN of the UpdateHealthProbe that gates promotion." + }, + "healthProbeDigest": { + "type": "string", + "pattern": "^sha256:[a-f0-9]{64}$", + "description": "The probe's definitionDigest as pinned at open. Must equal the referenced probe's current definitionDigest (family validator). Pinning at open is what prevents the gate being edited to admit the candidate that failed it." + }, + "maxAttempts": { + "type": "integer", + "minimum": 1, + "maximum": 7, + "description": "Boot attempts the candidate is allowed before it is marked unbootable and the transaction is refused. Bounded above by the GPT tries attribute width. There is no unbounded setting: the reason this field exists is that 'retry until it works' and 'boot loop' are the same program." + }, + "outcome": { + "type": "string", + "enum": ["pending", "promoted", "rolled-back", "refused"], + "description": "pending = in flight; promoted = probe passed and roles swapped; rolled-back = abandoned before the attempt budget was spent (write failure, digest mismatch, operator abort, or a single-attempt policy); refused = the budget was spent, the candidate is unbootable, and no further automatic attempt will be made. refused is a terminal state on purpose — it is the state that ends the boot loop, and a system without it retries a fatal payload forever." + }, + "rollbackReason": { + "type": ["string", "null"], + "enum": [ + "probe-failed", + "watchdog-expired", + "attempts-exhausted", + "write-failed", + "digest-mismatch", + "operator-abort", + null + ], + "description": "Why the target stayed on (or returned to) fromSlot. Required and non-null whenever outcome is rolled-back or refused; null when promoted. Closed set — an unattributed rollback teaches nothing and is indistinguishable from a rollback that was never diagnosed." + }, + "attempts": { + "type": "array", + "minItems": 0, + "description": "Ordered record of boot attempts into toSlot. Empty only while the payload is still being written. Every failed attempt records the slot the target fell back to, so 'we rolled back' is a fact in the record rather than an inference from the absence of a promotion.", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["attemptNumber", "startedAt", "result"], + "properties": { + "attemptNumber": { + "type": "integer", + "minimum": 1, + "maximum": 7, + "description": "1-based attempt index. Must be contiguous from 1 and must not exceed maxAttempts (family validator)." + }, + "startedAt": { + "type": "string", + "format": "date-time", + "description": "When the bootloader handed control to toSlot for this attempt." + }, + "result": { + "type": "string", + "enum": ["pass", "probe-failed", "watchdog-expired", "write-failed", "aborted"], + "description": "Outcome of this attempt. pass may appear only once and only as the final attempt (family validator) — a transaction that keeps trying after a pass has not understood that promotion is terminal." + }, + "fellBackTo": { + "type": ["string", "null"], + "enum": ["A", "B", null], + "description": "Slot the target booted after this attempt failed. Null on a passing attempt. Non-null on every failing attempt — a failed trial boot that fell back nowhere is a target left running an unproven payload." + }, + "triesRemainingAfter": { + "type": "integer", + "minimum": 0, + "maximum": 7, + "description": "The candidate slot's triesRemaining after the bootloader decremented for this attempt. Recorded so attempt accounting can be audited against the on-device attribute rather than trusted." + }, + "detail": { + "type": "string", + "minLength": 1, + "description": "Which check or watchdog produced the result." + } + } + } + }, + "settledOnSlot": { + "type": ["string", "null"], + "enum": ["A", "B", null], + "description": "Slot the target is running once the transaction is terminal. Constrained by if/then to equal toSlot on promotion and fromSlot on rollback or refusal — the schema, not the operator, decides that a failed update leaves you where you started." + }, + "openedAt": { + "type": "string", + "format": "date-time", + "description": "When the transaction opened and preservedPayloadDigest was recorded." + }, + "settledAt": { + "type": ["string", "null"], + "format": "date-time", + "description": "When the transaction reached a terminal outcome. Null while pending." + }, + "receiptRef": { + "type": "string", + "minLength": 1, + "description": "Reference to the sealed receipt covering this transaction, if the target emits into the reasoning-evidence fabric." + } + } +} diff --git a/specs/ab-fallback-update-contract.md b/specs/ab-fallback-update-contract.md new file mode 100644 index 0000000..410f525 --- /dev/null +++ b/specs/ab-fallback-update-contract.md @@ -0,0 +1,189 @@ +# A/B Fallback Update Contract v0.1 + +Status: v0.1 (tranche strictness bar). Program: TRUST FABRIC W9.2. + +## Why this family + +The estate ships updates to fog nodes, to installed applications, and to itself, +and until this contract there was **no path back from a bad one anywhere in it**. +The closest thing that exists is generation-based: `sourceos-syncd` applies a +`nixos-rebuild switch`, a `sourceos-health-check.timer` fires at `OnBootSec=120s`, +and on failure it shells out to a rollback that infers its target as "the highest +non-current generation". That is a heuristic standing in for a recorded pointer, +and it has three holes that no amount of care closes: + +1. **No attempt bound.** If the candidate never reaches userspace, the health + timer never fires, so nothing reverts it. The failure mode that most needs + automatic fallback is the one the mechanism cannot observe. +2. **No candidate marking.** Nothing records which payload is on trial, so + "roll back" means "guess backwards" rather than "return to the slot that + passed". +3. **No confirm step.** A health pass is fire-and-forget. Nothing promotes a + candidate or pins a last-known-good, so the difference between "this worked" + and "this has not failed yet" is never written down. + +The lesson taken is EVE-OS's: GRUB GPT priority-boot plus dual watchdogs — never +ship an update you cannot brick with. This family lands that shape as a contract +so the OS-image path and the application-update path use one vocabulary instead +of two, and so the rollback path is a recorded transition rather than an inference. + +## Schemas + +| Schema | Role | +| --- | --- | +| `UpdateSlot` | One of exactly two slots on a target. Carries the GPT attribute triple (`bootPriority`, `triesRemaining`, `successful`) the slot selector reads, the digest of the payload installed, and the role/running split. | +| `UpdateTransaction` | One attempt to move a target from the active payload to a new one. Records the write target, the pinned probe, every boot attempt and where it fell back to, and which slot the target ended on. | +| `UpdateHealthProbe` | The digest-pinned definition of what a candidate must prove before promotion: a non-empty check set with at least one blocking check, and a mandatory hardware+software watchdog pair. | + +## The invariant + +> **The currently-good slot is never overwritten by the update being applied.** + +It is enforced in three independent places, on purpose, because it is the only +property whose violation is unrecoverable: + +- **By schema, within one document.** `UpdateTransaction` carries a top-level + `not`/`anyOf` clause enumerating the two illegal `(fromSlot, toSlot)` pairs. + The slot set is closed to exactly two, so the illegal set is finite and the + constraint is expressible in JSON Schema rather than deferred to a runtime + check a caller can forget. `UpdateSlot` adds the same rule from the other side: + `state: "writing"` requires `role: "candidate"`. +- **By schema, on the settle path.** Four if/then clauses pin `settledOnSlot` to + `toSlot` on promotion and to `fromSlot` on rollback or refusal. A failed update + leaves the target where it started, and that is decided by the contract rather + than by the operator writing the record. +- **Across documents, by the validator.** `tools/validate_ab_update_examples.py` + asserts that a settled transaction's `preservedPayloadDigest` still equals the + active slot's `payloadDigest`. This is the executable form of the invariant, as + opposed to an assurance that it holds. A mutation test in the same tranche + confirms it fires. + +## State machine + +`UpdateTransaction.outcome` is the terminal projection of this machine. The +reference implementation is `AbUpdateMachine` in `sourceos-boot` +(`src/sourceos_boot/ab_update_machine.py`). + +| From | Event | To | Slot effects | +| --- | --- | --- | --- | +| `idle` | `begin(payload)` | `writing` | candidate → `writing`; **active untouched** | +| `writing` | `write_complete(digest match)` | `candidate_ready` | candidate → `written` | +| `writing` | `write_complete(digest mismatch)` | `rolled_back` (`digest-mismatch`) | candidate → `unbootable`; active retained | +| `writing` | `write_failed` | `rolled_back` (`write-failed`) | candidate → `unbootable`; active retained | +| `candidate_ready` | `arm()` | `armed` | candidate `bootPriority` > active, `triesRemaining = maxAttempts`, `successful = false` | +| `armed` | `boot_attempt()` | `trying` | bootloader decrements `triesRemaining` **before** handing over control | +| `trying` | `probe_pass()` | `promoted` | candidate → `good`, `successful = true`, roles swap; **previous payload retained bootable at lower priority** | +| `trying` | `probe_fail()` \| `watchdog_expired()` (tries remain) | `armed` | fall back to active; candidate stays armed | +| `trying` | `probe_fail()` \| `watchdog_expired()` (tries exhausted) | `refused` | candidate → `unbootable`, `bootPriority = 0`; target stays on active | +| `armed` \| `trying` \| `candidate_ready` | `operator_abort()` | `rolled_back` (`operator-abort`) | candidate → `unbootable`; active retained | + +`refused` is terminal on purpose. It is the state that ends the boot loop, and a +system without it retries a fatal payload forever. `promoted` is terminal for the +same reason in the opposite direction: a machine that keeps trying after a pass +has not understood that promotion is the end. + +Attempt accounting follows the GPT attribute rather than a software counter: +`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 exactly the boot loop this contract exists to forbid. + +## Probe digest (normative) + +`UpdateHealthProbe.definitionDigest` is: + +``` +sha256( canonical_json({ checks, evaluatedIn, minConsecutivePasses, + onProbeUnavailable, timeoutSeconds, watchdogs }) ) +``` + +where `canonical_json` is `json.dumps(..., sort_keys=True, separators=(",", ":"))`. +The projection covers the check and watchdog objects **entire, descriptions +included**: an exclusion list is somewhere to hide a weakening, and the cost of +re-pinning after a comment edit is far below the cost of a gate that can be edited +without the pin noticing. `UpdateTransaction.healthProbeDigest` records this value +at open. If the probe is edited while a transaction is in flight, the digests +diverge and the family validator rejects the pair — which is what stops a failing +candidate being promoted by relaxing the gate it failed. + +## Deliberate deltas from the source patterns + +1. **Dual watchdogs are mandatory, not recommended.** `watchdogs` requires at + least one `hardware` and one `software` entry, enforced by two `contains` + clauses. Neither kind alone closes the gap: a software watchdog cannot fire + through a wedged kernel, because the process that would notice is the process + that is stuck; a hardware watchdog only ever learns whether something petted + it, so it cannot distinguish a live-but-broken payload from a healthy one. + Requiring both is what makes "hung" and "running but failing" terminate in the + same automatic fallback. The software timeout must be shorter (validator), so + the software watchdog gets the first, attributable word. +2. **The bootloader may not declare its own success.** `evaluatedIn` is closed to + `post-boot-userspace` and `successful` is set only by userspace. A bootloader + can observe that control transferred and nothing more; a design that lets the + boot path mark its own boot good has no gate at all. +3. **An inconclusive probe is a failure.** `onProbeUnavailable` is closed to + `fail`. Reading "could not determine" as "proceed" is the declared-unenforced + gap applied to the one control standing between a target and a brick. +4. **Two slots, closed.** `slot` is `A`/`B` and not an open label set. The + fallback guarantee is that one slot is retained known-good while the other is + written, and that argument does not generalise to N without a new arbitration + rule. A third slot is a contract change, not a new enum value. +5. **Role and running are separate fields.** During a trial boot the candidate is + executing while the active slot is still the fallback. Collapsing the two makes + the fallback slot indescribable at exactly the moment it matters. +6. **Promotion retains the slot it replaces.** After promotion the previous active + becomes the candidate but keeps `successful: true` and a non-zero priority + until it is overwritten by the next update. The check set includes a + `rollback-capability` kind for the same reason: promotion is the moment the + previous payload stops being the guaranteed way back, so the ability to go back + is verified *before* it is spent, not after. +7. **Every rollback is attributed.** `rollbackReason` is a closed set and is + required whenever the outcome is `rolled-back` or `refused`. An unattributed + rollback teaches nothing and is indistinguishable from one that was never + diagnosed. + +## Repo placement + +| Layer | Repo | Delivers | +| --- | --- | --- | +| L0 | `sourceos-spec` | these normative schemas + fixtures (this document) | +| L1 | `sourceos-boot` | `AbUpdateMachine` reference implementation + `sourceos-boot ab-update` CLI surface | +| L2 | `sourceos-syncd` | emits `UpdateTransaction` from its apply path; `check-health` becomes the probe runner | +| L3 | `source-os` | GPT A/B partition layout + GRUB priority-boot slot selector; the `sourceos.syncd.slots.*` NixOS option surface | +| L4 | `Noetica` | application-update consumer once an updater exists (see below) | + +**L3 is where hardware enters and where this contract stops being testable in +software.** `source-os/scripts/install-image.sh` currently creates two partitions +(512M ESP + a single rootfs). An A/B layout needs a second rootfs slot and a GRUB +config that reads the priority attributes. That work is real and is not in this +tranche; nothing in it is verifiable without booting a machine, and a test that +claims to verify a bootloader without one would be worth less than no test. + +**L4 has no updater to consume this.** Noetica ships no `tauri-plugin-updater`, +no `updater` block in `tauri.conf.json`, and distributes via Homebrew cask. Its +own `docs/WORKPLAN-111-gaps.md` records this as ship-blocker #77: *"No Tauri +auto-updater at all — no in-app updates, no rollback, brew-only."* The contract is +written to cover it (`targetRef` is any `urn:srcos:` URN, and the example set +includes an application target) but there is nothing on that side to wire yet. + +## Conformance + +`fixtures/ab-update/conformance.json` holds fourteen negative vectors. Each MUST +FAIL validation for its stated reason, and `tools/validate_ab_update_examples.py` +fails the build if any of them validates. They are negative by construction and +live in `fixtures/`, never in `examples/`. + +Run: `make validate-ab-update-examples`. + +## Open items + +- **OI-1** GRUB slot-selector implementation and the A/B partition layout (L3). + Requires a hardware or VM boot loop to verify; explicitly out of the v0.1 + tranche. +- **OI-2** `bootPriority` is typed 0–15 after the GPT attribute width. If a target + ever needs a non-GPT selector (an application updater, say), the field keeps its + ordering semantics but loses its hardware meaning. Left as-is rather than + abstracted early. +- **OI-3** `UpdateTransaction.receiptRef` is optional at v0.1. Once targets emit + into the reasoning-evidence fabric it should become required for any + transaction that mutates a slot. diff --git a/tools/validate_ab_update_examples.py b/tools/validate_ab_update_examples.py new file mode 100644 index 0000000..0223a2a --- /dev/null +++ b/tools/validate_ab_update_examples.py @@ -0,0 +1,285 @@ +#!/usr/bin/env python3 +"""Validate the A/B fallback update contract family (UpdateSlot, UpdateTransaction, +UpdateHealthProbe). + +Five checks, not one: + 1. schema conformance — every schema is a valid draft-2020-12 document and every + canonical example validates against its schema; + 2. strictness bar — every schema in the family holds the tranche bar: top-level + "additionalProperties": false, specVersion pinned to the 0.1.0 const, and an + anchored urn:srcos: id pattern; + 3. recomputed probe digest — UpdateHealthProbe.definitionDigest is RECOMPUTED + from the probe's own check set and watchdog configuration rather than read + back. A digest that is merely stored is an assertion about pinning; a digest + that is recomputed is pinning. This is what makes "the gate cannot be + weakened to admit the candidate that failed it" a build failure instead of a + paragraph; + 4. cross-invariants — the properties JSON Schema cannot express, checked over + the example set. Chief among them: a settled transaction's + preservedPayloadDigest still equals the active slot's payloadDigest, which is + the executable form of "the currently-good slot was never overwritten by the + update being applied". That is the invariant this family exists for, and it + is the one that has to be checked across two documents rather than inside + one; + 5. negative vectors — every case in fixtures/ab-update/conformance.json FAILS + for its stated reason. +""" +from __future__ import annotations + +import hashlib +import json +import sys +from collections import defaultdict +from pathlib import Path + +import jsonschema + +ROOT = Path(__file__).resolve().parents[1] + +SCHEMA_NAMES = [ + "UpdateSlot.json", + "UpdateTransaction.json", + "UpdateHealthProbe.json", +] + +SLOT_EXAMPLES = [ + "update_slot.fog07_a_active.json", + "update_slot.fog07_b_unbootable.json", + "update_slot.noetica_a_fallback.json", + "update_slot.noetica_b_active.json", +] +TRANSACTION_EXAMPLES = [ + "update_transaction.refused.json", + "update_transaction.promoted.json", +] +PROBE_EXAMPLES = ["update_health_probe.json"] + +PAIRS = ( + [("UpdateSlot.json", name) for name in SLOT_EXAMPLES] + + [("UpdateTransaction.json", name) for name in TRANSACTION_EXAMPLES] + + [("UpdateHealthProbe.json", name) for name in PROBE_EXAMPLES] +) + +FIXTURE = ROOT / "fixtures" / "ab-update" / "conformance.json" + +# The fields the probe's definitionDigest covers. Deliberately the whole check and +# watchdog objects, descriptions included: an exclusion list is somewhere to hide a +# weakening, and the cost of re-pinning after a comment edit is far below the cost +# of a gate that can be edited without the pin noticing. +DIGEST_FIELDS = ( + "checks", + "evaluatedIn", + "minConsecutivePasses", + "onProbeUnavailable", + "timeoutSeconds", + "watchdogs", +) + +failures: list[str] = [] + + +def fail(msg: str) -> None: + failures.append(msg) + print(f"FAIL: {msg}") + + +def ok(msg: str) -> None: + print(f"ok: {msg}") + + +def load(path: Path) -> dict: + with path.open() as fh: + return json.load(fh) + + +def definition_digest(probe: dict) -> str: + """Recompute UpdateHealthProbe.definitionDigest. Normative: sha256 over the + canonical JSON (sorted keys, no whitespace) of the DIGEST_FIELDS projection.""" + core = {field: probe[field] for field in DIGEST_FIELDS} + canonical = json.dumps(core, sort_keys=True, separators=(",", ":")) + return "sha256:" + hashlib.sha256(canonical.encode("utf-8")).hexdigest() + + +def main() -> int: # noqa: C901 - a validator is a list of checks; splitting it hides them + schemas = {name: load(ROOT / "schemas" / name) for name in SCHEMA_NAMES} + examples = {name: load(ROOT / "examples" / name) for _, name in PAIRS} + + # 1. schema conformance + for name, schema in schemas.items(): + try: + jsonschema.Draft202012Validator.check_schema(schema) + ok(f"schema valid: {name}") + except jsonschema.SchemaError as exc: + fail(f"schema invalid: {name}: {exc.message}") + + for schema_name, example_name in PAIRS: + validator = jsonschema.Draft202012Validator(schemas[schema_name]) + errors = sorted(validator.iter_errors(examples[example_name]), key=str) + if errors: + for err in errors: + fail(f"example {example_name} vs {schema_name}: {err.message}") + else: + ok(f"example validates: {example_name} vs {schema_name}") + + # 2. strictness bar + bar_failures = len(failures) + for name, schema in schemas.items(): + if schema.get("additionalProperties") is not False: + fail(f"strictness: {name} must set top-level additionalProperties:false") + spec_version = schema.get("properties", {}).get("specVersion", {}) + if spec_version.get("const") != "0.1.0": + fail(f"strictness: {name} specVersion must be const 0.1.0") + id_pattern = schema.get("properties", {}).get("id", {}).get("pattern", "") + if not id_pattern.startswith("^urn:srcos:"): + fail(f"strictness: {name} id pattern must anchor on urn:srcos:") + if schema.get("properties", {}).get("type", {}).get("const") != schema.get("title"): + fail(f"strictness: {name} type const must equal the schema title") + if len(failures) == bar_failures: + ok(f"strictness bar holds for all {len(schemas)} schemas") + + # 3. recomputed probe digest + probe = examples["update_health_probe.json"] + recomputed = definition_digest(probe) + if probe["definitionDigest"] != recomputed: + fail( + "probe definitionDigest is stale: recorded " + f"{probe['definitionDigest']} but the check set hashes to {recomputed}" + ) + else: + ok("probe definitionDigest recomputes from its own check set + watchdogs") + + # A gate with no blocking check cannot gate anything. + if not any(check["blocking"] for check in probe["checks"]): + fail("probe has no blocking check — it cannot refuse a promotion") + else: + ok("probe has at least one blocking check") + + # The software watchdog must get the first word, or every software-detectable + # fault is reported as an unexplained hardware reset. + sw = [w for w in probe["watchdogs"] if w["kind"] == "software"] + hw = [w for w in probe["watchdogs"] if w["kind"] == "hardware"] + if min(w["timeoutSeconds"] for w in hw) <= max(w["timeoutSeconds"] for w in sw): + fail("watchdog ordering: hardware timeout must exceed software timeout") + else: + ok("watchdog ordering: software fires first, hardware is the backstop") + + # 4. cross-invariants over the example set + slots_by_target: dict[str, list[dict]] = defaultdict(list) + for name in SLOT_EXAMPLES: + slots_by_target[examples[name]["targetRef"]].append(examples[name]) + + for target, slots in sorted(slots_by_target.items()): + short = target.rsplit(":", 1)[-1] + if len(slots) != 2: + fail(f"{short}: a target must have exactly two slots, found {len(slots)}") + continue + if {s["slot"] for s in slots} != {"A", "B"}: + fail(f"{short}: slot labels must be exactly {{A, B}}") + if sum(1 for s in slots if s["role"] == "active") != 1: + fail(f"{short}: exactly one slot must hold role 'active'") + elif sum(1 for s in slots if s["currentlyRunning"]) != 1: + fail(f"{short}: exactly one slot may be currentlyRunning") + else: + ok(f"{short}: two slots, one active, one running") + + for name in TRANSACTION_EXAMPLES: + tx = examples[name] + short = tx["id"].rsplit(":", 1)[-1] + slots = {s["slot"]: s for s in slots_by_target[tx["targetRef"]]} + if set(slots) != {"A", "B"}: + fail(f"{short}: transaction targetRef has no slot pair in the example set") + continue + from_slot, to_slot = slots[tx["fromSlot"]], slots[tx["toSlot"]] + + # THE invariant: the good slot was never overwritten. + if from_slot["payloadDigest"] != tx["preservedPayloadDigest"]: + fail( + f"{short}: the good slot WAS overwritten — opened with " + f"{tx['preservedPayloadDigest']} in slot {tx['fromSlot']}, which now " + f"holds {from_slot['payloadDigest']}" + ) + else: + ok(f"{short}: fromSlot still holds its opening digest (never overwritten)") + + if to_slot["payloadDigest"] != tx["candidatePayloadDigest"]: + fail(f"{short}: toSlot does not hold the candidate payload digest") + + # The probe was pinned, and the pin still resolves. + if tx["healthProbeRef"] != probe["id"]: + fail(f"{short}: healthProbeRef does not resolve to the example probe") + elif tx["healthProbeDigest"] != probe["definitionDigest"]: + fail(f"{short}: pinned probe digest does not match the probe definition") + else: + ok(f"{short}: probe pin resolves and matches") + + # Attempt accounting. + attempts = tx["attempts"] + numbers = [a["attemptNumber"] for a in attempts] + if numbers != list(range(1, len(attempts) + 1)): + fail(f"{short}: attemptNumbers must be contiguous from 1, got {numbers}") + if len(attempts) > tx["maxAttempts"]: + fail(f"{short}: {len(attempts)} attempts exceeds maxAttempts {tx['maxAttempts']}") + passes = [i for i, a in enumerate(attempts) if a["result"] == "pass"] + if len(passes) > 1 or (passes and passes[0] != len(attempts) - 1): + fail(f"{short}: 'pass' must appear at most once and only as the final attempt") + for attempt in attempts: + if attempt["result"] == "pass": + continue + if attempt["fellBackTo"] is None: + fail( + f"{short}: attempt {attempt['attemptNumber']} failed and fell back " + "nowhere — the target was left running an unproven payload" + ) + elif attempt["fellBackTo"] != tx["fromSlot"]: + fail( + f"{short}: attempt {attempt['attemptNumber']} fell back to " + f"{attempt['fellBackTo']}, not to the known-good slot {tx['fromSlot']}" + ) + if not failures or all("attempt" not in f for f in failures[-4:]): + ok(f"{short}: attempt accounting consistent, every failure fell back to active") + + # Terminal-state consistency with the slot pair. + if tx["outcome"] == "refused": + if len(attempts) != tx["maxAttempts"]: + fail(f"{short}: refused before the attempt budget was spent") + elif to_slot["state"] != "unbootable" or to_slot["bootPriority"] != 0: + fail( + f"{short}: refused but the candidate slot is still selectable " + f"(state={to_slot['state']}, bootPriority={to_slot['bootPriority']}) " + "— nothing ends the boot loop" + ) + elif not from_slot["successful"] or not from_slot["currentlyRunning"]: + fail(f"{short}: refused but the target is not running the known-good slot") + else: + ok(f"{short}: refused — candidate unbootable, target running active") + elif tx["outcome"] == "promoted": + if attempts[-1]["result"] != "pass": + fail(f"{short}: promoted without a passing final attempt") + elif to_slot["role"] != "active" or not to_slot["successful"]: + fail(f"{short}: promoted but the candidate did not become the active slot") + elif not from_slot["successful"] or from_slot["bootPriority"] == 0: + fail( + f"{short}: promoted and the previous payload is no longer a usable " + "fallback — promotion must retain the slot it replaced" + ) + else: + ok(f"{short}: promoted — roles swapped, previous payload retained bootable") + + # 5. negative vectors must FAIL + fixture = load(FIXTURE) + for case in fixture["cases"]: + validator = jsonschema.Draft202012Validator(schemas[case["schema"]]) + if list(validator.iter_errors(case["document"])): + ok(f"negative vector fails as required: {case['reason'][:72]}") + else: + fail(f"negative vector VALIDATED but must fail: {case['reason']}") + + if failures: + print(f"\n{len(failures)} failure(s)") + return 1 + print("\nOK: ab-update family — all five checks passed") + return 0 + + +if __name__ == "__main__": + sys.exit(main())