diff --git a/.github/workflows/fleet-converge.yml b/.github/workflows/fleet-converge.yml index fd042b81247..a385c7b0a13 100644 --- a/.github/workflows/fleet-converge.yml +++ b/.github/workflows/fleet-converge.yml @@ -67,7 +67,11 @@ on: required: false type: string transaction_nonce: - description: Operator-minted unique nonce for one RLM transaction; echoed into run-name so each dispatched run is API-selectable by its displayTitle, closing the run-id correlation gap (review 5062738052 B4). Not consumed by any step + description: "Operator-minted unique nonce for one RLM transaction; echoed into run-name so each dispatched run is API-selectable by its displayTitle, closing the run-id correlation gap (review 5062738052 B4). mtcollins1_boot only, when attempt_receipt is named: it is the boot attempt's identity, joined to the receipt's attempt and consumed once (gunbc.host_boot_attempt_admission), so a nonce admits one boot; [A-Za-z0-9_-] only" + required: false + type: string + attempt_receipt: + description: "mtcollins1_boot only: a committed artifacts/receipts/*.json naming this attempt's plan and the operator's inspection (gunbc.host_boot_attempt_admission). Empty records the configuration as not recorded; a named receipt that fails any check refuses the boot before power-on. Requires transaction_nonce" required: false type: string jobs: @@ -2341,6 +2345,8 @@ jobs: env: WIF_ACCESS_TOKEN: ${{ steps.wif_auth.outputs.access_token }} FLEET_CONVERGE_EXPECTED_HOST: ${{ github.event.inputs.host }} + GUNBC_BOOT_ATTEMPT_RECEIPT: ${{ github.event.inputs.attempt_receipt }} + GUNBC_BOOT_ATTEMPT_NONCE: ${{ github.event.inputs.transaction_nonce }} if: github.event.inputs.mode == 'mtcollins1_boot' timeout-minutes: 134 - name: Upload Mt. Collins unit 1 boot SOL capture and receipts diff --git a/dag/extdeps/git/inspect.dag b/dag/extdeps/git/inspect.dag index 40ce56ab231..ac3cd5690a6 100644 --- a/dag/extdeps/git/inspect.dag +++ b/dag/extdeps/git/inspect.dag @@ -148,6 +148,9 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { // later stage -- and it carries the object id, so a population read out of a revision can name each // member by content identity instead of by path alone. // +// ListTreeEntryAtPath is the same record for ONE path: a consumer that needs one file's mode and +// object id at a revision asks for that path rather than enumerating the tree. +// // BOTH OPERATIONS SURVIVE. A consumer that only needs paths pays neither the wider output nor the // parse, and asking for identity when you wanted names is the same collapse ResolveRefCommit and // ShowTree are kept apart to prevent. The record separator is NUL and the fields are separated by @@ -361,6 +364,22 @@ service git.Inspect { } } + operation ListTreeEntryAtPath { + requires opaque + input { ref: GitRef, path: String } + output { + entries_nul: String from "stdout" + success: Bool from "exit_success" + stderr: String from "stderr" + } + readonly + transport shell { argv: ["git", "ls-tree", "-z", "{ref}", "--", "{path}"] } + exit { + 0 => Unit + 128 => String "Invalid ref or not a git repository" + } + } + operation GrepMatchesAtRevision { requires opaque input { pattern: String, ref: GitRef, pathspec: String } diff --git a/dag/gunbc/ci/ci_layer_roots.dag b/dag/gunbc/ci/ci_layer_roots.dag index 7cf6a508e68..364ce9051a9 100644 --- a/dag/gunbc/ci/ci_layer_roots.dag +++ b/dag/gunbc/ci/ci_layer_roots.dag @@ -1089,6 +1089,11 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_tempdir_write_reason, dissolution: excl_local_repo_wet_dissolve}, + WitnessExclusionRow { + pattern: "host_boot_attempt_admission_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_local_repo_wet_tempdir_write_reason, + dissolution: excl_local_repo_wet_dissolve}, WitnessExclusionRow { pattern: "durable_cas_file_store_wet_witness_test.dag", classification: LocalRepoWetLane, diff --git a/dag/gunbc/fleet/fleet_converge_workflow.dag b/dag/gunbc/fleet/fleet_converge_workflow.dag index 8f75f1d02eb..9bb3a7bfd62 100644 --- a/dag/gunbc/fleet/fleet_converge_workflow.dag +++ b/dag/gunbc/fleet/fleet_converge_workflow.dag @@ -130,6 +130,7 @@ import gunbc.auth.ci_app_key_rotation { app_key_verify_receipt_path, } import gunbc.machine_intake_mtcollins1_boot_run { mtcollins1_boot_artifact_glob, mtcollins1_boot_step_timeout_minutes } +import gunbc.host_boot_attempt_admission { boot_attempt_receipt_env_name, boot_attempt_nonce_env_name } import gunbc.runner_group_restriction_ensure_run { microvm_runner_group_ensure_artifact_glob, microvm_runner_group_step_timeout_minutes } import gunbc.ci_spec { site_pxe_edge_converge_receipt_path, @@ -2807,6 +2808,8 @@ fn fleet_converge_mtcollins1_boot_step() -> Step { env: Present { value: [ kv(key: "WIF_ACCESS_TOKEN", value: yaml_string(s: "${{ steps.wif_auth.outputs.access_token }}")), kv(key: fleet_converge_expected_host_env_name, value: yaml_string(s: "${{ github.event.inputs.host }}")), + kv(key: boot_attempt_receipt_env_name as String, value: yaml_string(s: "${{ github.event.inputs.attempt_receipt }}")), + kv(key: boot_attempt_nonce_env_name as String, value: yaml_string(s: "${{ github.event.inputs.transaction_nonce }}")), ] }, working_directory: none, if_condition: Present { value: fleet_converge_mtcollins1_boot_step_if }, @@ -4493,7 +4496,14 @@ data fleet_converge_dispatch_inputs: List = [ }, DispatchInput { name: "transaction_nonce", - description: Present { value: "Operator-minted unique nonce for one RLM transaction; echoed into run-name so each dispatched run is API-selectable by its displayTitle, closing the run-id correlation gap (review 5062738052 B4). Not consumed by any step" }, + description: Present { value: "Operator-minted unique nonce for one RLM transaction; echoed into run-name so each dispatched run is API-selectable by its displayTitle, closing the run-id correlation gap (review 5062738052 B4). mtcollins1_boot only, when attempt_receipt is named: it is the boot attempt's identity, joined to the receipt's attempt and consumed once (gunbc.host_boot_attempt_admission), so a nonce admits one boot; [A-Za-z0-9_-] only" }, + required: false, + default: none, + type: InputString, + }, + DispatchInput { + name: "attempt_receipt", + description: Present { value: "mtcollins1_boot only: a committed artifacts/receipts/*.json naming this attempt's plan and the operator's inspection (gunbc.host_boot_attempt_admission). Empty records the configuration as not recorded; a named receipt that fails any check refuses the boot before power-on. Requires transaction_nonce" }, required: false, default: none, type: InputString, diff --git a/dag/gunbc/host/host_boot_attempt_admission.dag b/dag/gunbc/host/host_boot_attempt_admission.dag new file mode 100644 index 00000000000..024ccb02ded --- /dev/null +++ b/dag/gunbc/host/host_boot_attempt_admission.dag @@ -0,0 +1,901 @@ +module gunbc.host_boot_attempt_admission + +import v2.std.algebra { any } +import std.types { Bool, FilePath, GitRef, Int, List, NonEmptyStr, String } +import v2.std.optional { Present, Absent } +import std.decl_ref { decl_ref } +import std.algebra { trim } +import std.human_intervention { HumanIntervention, EveryProvision, DischargedAt } +import std.durable_compare_and_set { + ExpectSlotAbsent, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasReadableAbsent, CasReadablePresent, + CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, CasGenerationSpaceExhausted, + cas_generation_count, cas_unreadable_slot_detail, +} +import gunbc.durable_cas_file_store { + DefaultAccessCreateOnly, DerivedPayloadAdmitted, DerivedPayloadKeyNotSlotAddressable, + admit_cas_attempt_for_derived_payload, file_compare_and_set, +} +import extdeps.git.inspect +import extdeps.git +import extdeps.tools.sha256sum { Sha256FileDigest, Sha256FileDigestUnavailable, sha256sum_stdin_digest_via_shell } +import gunbc.namespace_step0_subject_collector { Step0TreeEntryDecoded, Step0TreeEntryUndecodable, step0_decode_tree_entry, step0_entry_is_regular_blob, step0_subject_entries_at } +import extdeps.languages.json.emit { JsonValue, JsonNull, JsonBool, JsonNumber, JsonString, JsonArray, JsonObject } +import extdeps.languages.json.parse { + JsonDocumentParsed, JsonDocumentUnreadable, parse_json_document, json_document_gap_text, + JsonFieldRead, FieldAbsent, FieldRead, FieldMalformed, json_field, json_field_string, + JsonMemberPresence, JsonMemberMissing, JsonMemberNull, JsonMemberValue, JsonMemberUnreadable, json_member_presence, +} +import product.placement_supply { HostIdentity, host_identity_eq } +import extdeps.ampere.mt_collins_getting_started_guide.dimm_layout { MtCollinsDimmFigureBank, dimm_figure_banks, dimm_figure_connector_label_prefix } +import gunbc.auth.approval_capability { utc_instant_is_canonical, utc_instant_before } +import gunbc.actions_run_binding { ActionsVariableRead, ActionsVariablePresent, ActionsVariableAbsent, actions_variable_read } +import gunbc.fleet_intent_network { operator_host_mtcollins1 } +import gunbc.managed_host { + ManagedHost, ManagedHostBinding, managed_host_binding, + ManagedHostBound, ManagedHostAccessUnobserved, ManagedHostNotSecured, ManagedHostEndpointMismatch, +} +import gunbc.managed_host_unit_hold { UnitHoldProof, UnitHoldStoreExecutor, UnitHoldOnStoreHost, UnitHoldNotOnStoreHost, unit_hold_store_executor } +import gunbc.machine_intake_mtcollins1_power_on_account { + AttemptConfigurationReceipt, digest_label, ExpectedTopology, ExpectedSockets, ExpectedTopologyNotRecorded, + StimulusRequest, StimulusRequested, NoStimulusRequested, StimulusRequestNotRecorded, + StimulusApplication, StimulusAppliedByReceipt, StimulusApplicationNotRecorded, + SocketCpuRow, SlotRow, PopulationReading, PopulationOperatorAttested, PopulationNotRecorded, + FirmwareReadbacksNotRecorded, +} + +// THE ADMISSION OF ONE BOOT ATTEMPT'S CONFIGURATION RECEIPT, host-generic over a gunbc.managed_host +// ManagedHostBinding (docs/plans/power-on-sequence-model.md section 12; Q5 decided by eager-gull-22 +// 2026-10-03; Q6 decided by the operator, escalation msg_1b57e749 approved by default after 15 +// minutes without an answer). It sits BEHIND the boot's existing refusals -- boot admission, boot +// authorization and the unit hold -- because it consumes the unit hold's store-host executor, and +// before any pre-power read or actuation: the boot entry holds a BootAttemptClearance or does not run. +// +// A REQUEST IS NOT EVIDENCE THAT A PHYSICAL CHANGE HAPPENED. The plan (what this attempt expects and +// asks for) and the inspection (what a person then saw on the machine) are committed JSON under +// artifacts/receipts/, reviewed like any change; the dispatch names the file. A workflow-authored +// value is never read as either. +// +// THE ATTEMPT IDENTITY IS THE DISPATCH'S, NOT THE FILE'S. The fleet-converge transaction_nonce is +// minted by the operator outside the artifact; admission joins the receipt's attempt to it and then +// consumes it in a create-once slot, so a valid receipt for attempt A can neither be selected by a +// dispatch of attempt B nor replayed after it. EVERY CHECK ON THE FILE COMPLETES BEFORE THE SLOT IS +// TOUCHED, so a malformed or mismatched receipt cannot burn a valid attempt. +// +// ABSENT IS NOT REFUSED. A dispatch that names no receipt proceeds with the configuration NotRecorded +// and no topology judgement (slice A's semantics); a NAMED receipt that fails any check refuses the +// boot before actuation with its typed cause. +// +// ── THE PER-HOST ROUTE ────────────────────────────────────────────────────────────────────────── +// THE VARIABLES A DISPATCH NAMES ITS RECEIPT AND NONCE THROUGH ARE POLICY, beside the operation they +// feed (the gunbc.host_maintenance_hold_reason pattern). A host with no row has no receipt route and +// refuses rather than deriving variable names from its label. +data boot_attempt_receipt_env_name: NonEmptyStr = "GUNBC_BOOT_ATTEMPT_RECEIPT" + +data boot_attempt_nonce_env_name: NonEmptyStr = "GUNBC_BOOT_ATTEMPT_NONCE" + +// THE HOST'S STATIC SLOT ROSTER: every DIMM slot the board has, by the label an inspection names it +// with and the socket it belongs to. An inspection's DIMM rows are joined to it exactly -- known +// label, that label's socket, every slot once -- so a partial or mislabelled list never becomes an +// attested population. +type RosterSlot { + label: NonEmptyStr + socket: Int +} + +type AttemptReceiptRoute { + receipt_env: NonEmptyStr + nonce_env: NonEmptyStr + slots: List +} + +// Mt. Collins: the 32 memory connectors of the Getting Started Guide's Figure 9 +// (extdeps.ampere.mt_collins_getting_started_guide.dimm_layout dimm_figure_banks), labelled as the guide +// labels them -- its connector prefix (dimm_figure_connector_label_prefix, "J") and the connector number, +// the same derivation gunbc.mt_collins_dimm_physical_identity uses -- on the socket of their bank. +fn mt_collins_slot_roster(banks: List) -> List { + flat_map(banks, b => map(b.connectors_left_to_right, c => RosterSlot { label: concat(dimm_figure_connector_label_prefix as String, to_string(c as Int)) as NonEmptyStr, socket: b.processor_socket as Int })) +} + +fn attempt_receipt_route(host: ManagedHost) -> AttemptReceiptRoute? { + if host_identity_eq(a: host.host, b: operator_host_mtcollins1) { + Present { value: AttemptReceiptRoute { receipt_env: boot_attempt_receipt_env_name, nonce_env: boot_attempt_nonce_env_name, slots: mt_collins_slot_roster(banks: dimm_figure_banks) } } + } else { + none + } +} + +// ── THE OPERATOR-ATTESTED STEP ────────────────────────────────────────────────────────────────── +// A physical change has no API, so the inspection is a human step. Its discharge cites the producer +// that turns the committed file into a receipt, never a flag beside it (std.human_intervention). +data boot_attempt_inspection_step: HumanIntervention = HumanIntervention { + identity: "boot_attempt_configuration_inspection", + frequency: EveryProvision, + subject: "a managed host's CPU and DIMM population and the physical change applied before one boot attempt", + instruction: "After making the planned change, inspect the machine and commit the attempt's plan and inspection under artifacts/receipts/, naming the dispatch transaction_nonce as the attempt; dispatch the boot with that file as attempt_receipt.", + completion_evidence: DischargedAt { + evidence: decl_ref(module_path: "gunbc.host_boot_attempt_admission", decl_name: "validate_attempt_receipt"), + }, +} + +// ── THE RECORDS ───────────────────────────────────────────────────────────────────────────────── +// A TIME A PERSON WROTE, NEVER AN OBSERVER CLOCK READING. It is ordered only against another attested +// time; "before the power write" is structural (admission completes before actuation), never a +// comparison with a clock. The rendering is admitted only as a canonical UTC instant +// (gunbc.auth.approval_capability utc_instant_is_canonical: YYYY-MM-DDTHH:MM:SSZ with calendar-valid +// fields), and ordered only by that module's utc_instant_before. +type OperatorAttestedTime { + rendering: NonEmptyStr + attested_by: NonEmptyStr +} + +// THE BLOB THE RUN READ: the regular file tracked at `path` in the bound revision (the boot run's own +// execution revision), and the SHA-256 of exactly those bytes. A worktree file, an untracked file or a +// symlink is not this, so none can mint one. +type ReceiptEvidence { + path: NonEmptyStr + digest: Sha256FileDigest + commit: NonEmptyStr +} + +// expected and requested are stated ONCE, here. +type AttemptConfigurationPlan sole_constructor { + subject: HostIdentity + attempt: NonEmptyStr + expected: List + requested: StimulusRequest + fixed_at: OperatorAttestedTime +} + +type AttemptInspectionReceipt sole_constructor { + plan: AttemptConfigurationPlan + applied: NonEmptyStr + cpus: List + dimms: List + completed_at: OperatorAttestedTime + evidence: ReceiptEvidence + witnessed_by: NonEmptyStr +} + +// ── THE REFUSALS ──────────────────────────────────────────────────────────────────────────────── +type AttemptReceiptRefusal + = ReceiptHostHasNoRoute { host: HostIdentity } + | ReceiptExecutorForAnotherHost { executor_host: HostIdentity, bound: HostIdentity } + | ReceiptExecutorNotOnStoreHost { reason: NonEmptyStr } + | ReceiptHostUnbound { detail: NonEmptyStr } + | ReceiptNonceMissing { variable: NonEmptyStr, detail: String } + | ReceiptNonceNotSlotSafe { nonce: NonEmptyStr } + | ReceiptHostNotSlotSafe { host: HostIdentity } + | ReceiptPathOutsideReceipts { path: NonEmptyStr } + | ReceiptNotTracked { path: NonEmptyStr, commit: NonEmptyStr } + | ReceiptNotRegularFile { path: NonEmptyStr, mode: String, kind: String } + | ReceiptFileUnreadable { path: NonEmptyStr, detail: String } + | ReceiptDigestUnavailable { path: NonEmptyStr, reason: String } + | ReceiptNotJson { path: NonEmptyStr, detail: String } + | ReceiptSchemaMismatch { observed: String } + | ReceiptFieldUnreadable { field: NonEmptyStr, cause: String } + | ReceiptTimeUnreadable { field: NonEmptyStr, rendering: String } + | ReceiptSubjectMismatch { receipt: String, bound: HostIdentity } + | ReceiptAttemptMismatch { receipt: String, dispatched: NonEmptyStr } + | ReceiptPlanMismatch { field: NonEmptyStr, plan: String, inspection: String } + | ReceiptOrderingViolated { fixed_at: NonEmptyStr, completed_at: NonEmptyStr } + | ReceiptCpusNotTheExpectedSockets { expected: List, recorded: List } + | ReceiptDimmUnknownSlot { label: NonEmptyStr } + | ReceiptDimmOnWrongSocket { label: NonEmptyStr, recorded: Int, roster: Int } + | ReceiptDimmSlotOmitted { label: NonEmptyStr } + | AttemptAlreadyConsumed { slot: NonEmptyStr, consumed_by: String } + | AttemptSlotKeyNotAddressable { slot: NonEmptyStr } + | AttemptSlotPreconditionIncoherent { slot: NonEmptyStr } + | AttemptSlotStoreRefused { slot: NonEmptyStr, cause: CasStoreFailure } + +// ── THE CLEARANCE THE BOOT ENTRY MUST HOLD ────────────────────────────────────────────────────── +type AttemptConfigurationSource + = ConfigurationReceiptNotNamed + | ConfigurationReceiptAdmitted { receipt: AttemptInspectionReceipt, slot: NonEmptyStr } + +type BootAttemptClearance sole_constructor { + host: HostIdentity + source: AttemptConfigurationSource +} + +type BootAttemptAdmission + = BootAttemptCleared { clearance: BootAttemptClearance } + | BootAttemptRefused { cause: AttemptReceiptRefusal } + +// ── THE PURE VALIDATION (the inspection step's discharge producer) ────────────────────────────── +data boot_attempt_receipt_schema: NonEmptyStr = "gunbc.boot_attempt_receipt.v1" + +data boot_attempt_receipt_dir: NonEmptyStr = "artifacts/receipts/" + +type ReceiptValidation + = ReceiptValidated { receipt: AttemptInspectionReceipt } + | ReceiptRefused { cause: AttemptReceiptRefusal } + +// A PATH IS ADMITTED ONLY AS A FILE UNDER artifacts/receipts/ IN THE CHECKOUT: relative, no parent +// step, ending .json. The dispatch names it; it never names where the reader looks outside the tree. +fn receipt_path_admitted(path: String) -> Bool { + starts_with(s: path, prefix: boot_attempt_receipt_dir as String) + && ends_with(s: path, suffix: ".json") + && !string_contains(s: path, pattern: "..") + && string_length(s: path) > string_length(s: boot_attempt_receipt_dir as String) + 5 +} + +fn validate_attempt_receipt(subject: HostIdentity, nonce: NonEmptyStr, path: NonEmptyStr, commit: NonEmptyStr, slots: List, content: String, digest: Sha256FileDigest) -> ReceiptValidation { + match digest { + Sha256FileDigestUnavailable { path: _, reason: r } => ReceiptRefused { cause: ReceiptDigestUnavailable { path: path, reason: r } } + Sha256FileDigest { digest: _ } => + match parse_json_document(s: content) { + JsonDocumentUnreadable { gap: g } => ReceiptRefused { cause: ReceiptNotJson { path: path, detail: json_document_gap_text(gap: g) } } + JsonDocumentParsed { value: doc } => validate_document(subject: subject, nonce: nonce, evidence: ReceiptEvidence { path: path, digest: digest, commit: commit }, slots: slots, doc: doc) + } + } +} + +// THE TREE ENTRY AT `path` IN THE REVISION, decoded by the step0 collector's ls-tree reader: no entry +// is an untracked path, and an entry that is not a regular blob (a symlink, a gitlink, a directory) is +// not a receipt. +fn tracked_entry_refusal(path: NonEmptyStr, commit: NonEmptyStr, entries_nul: String) -> AttemptReceiptRefusal? { + let records: List = step0_subject_entries_at(entries_nul: entries_nul) + match records.first() { + Absent => Present { value: ReceiptNotTracked { path: path, commit: commit } } + Present { value: record } => + if count(records) != 1 { + Present { value: ReceiptNotRegularFile { path: path, mode: "", kind: concat(to_string(count(records)), " tree entries") } } + } else { + match step0_decode_tree_entry(record: record) { + Step0TreeEntryUndecodable { record: r } => Present { value: ReceiptFileUnreadable { path: path, detail: concat("undecodable ls-tree record: ", r) } } + Step0TreeEntryDecoded { entry: e } => + if e.path != (path as String) { + Present { value: ReceiptNotTracked { path: path, commit: commit } } + } else if !step0_entry_is_regular_blob(entry: e) { + Present { value: ReceiptNotRegularFile { path: path, mode: e.mode, kind: e.kind } } + } else { + none + } + } + } + } +} + +fn validate_document(subject: HostIdentity, nonce: NonEmptyStr, evidence: ReceiptEvidence, slots: List, doc: JsonValue) -> ReceiptValidation { + match required_string(obj: doc, key: "schema") { + TextRefused { cause: c } => ReceiptRefused { cause: c } + TextRead { value: schema } => + if schema != (boot_attempt_receipt_schema as String) { + ReceiptRefused { cause: ReceiptSchemaMismatch { observed: schema } } + } else { + match required_object(obj: doc, key: "plan") { + ValueRefused { cause: c } => ReceiptRefused { cause: c } + ValueRead { value: plan_doc } => + match plan_of(subject: subject, nonce: nonce, doc: plan_doc) { + PlanRefused { cause: c } => ReceiptRefused { cause: c } + PlanRead { plan: plan } => + match required_object(obj: doc, key: "inspection") { + ValueRefused { cause: c } => ReceiptRefused { cause: c } + ValueRead { value: inspection_doc } => inspection_of(plan: plan, evidence: evidence, slots: slots, doc: inspection_doc) + } + } + } + } + } +} + +type PlanOf + = PlanRead { plan: AttemptConfigurationPlan } + | PlanRefused { cause: AttemptReceiptRefusal } + +fn plan_of(subject: HostIdentity, nonce: NonEmptyStr, doc: JsonValue) -> PlanOf { + match required_string(obj: doc, key: "subject") { + TextRefused { cause: c } => PlanRefused { cause: c } + TextRead { value: s } => + if s != (subject as String) { + PlanRefused { cause: ReceiptSubjectMismatch { receipt: s, bound: subject } } + } else { + match required_string(obj: doc, key: "attempt") { + TextRefused { cause: c } => PlanRefused { cause: c } + TextRead { value: a } => + if a != (nonce as String) { + PlanRefused { cause: ReceiptAttemptMismatch { receipt: a, dispatched: nonce } } + } else { + match socket_list(obj: doc, key: "expected_sockets") { + SocketsRefused { cause: c } => PlanRefused { cause: c } + SocketsRead { sockets: expected } => + match requested_of(doc: doc) { + RequestRefused { cause: c } => PlanRefused { cause: c } + RequestRead { request: requested } => + match attested_time(obj: doc, key: "fixed_at", by_key: "fixed_by") { + TimeRefused { cause: c } => PlanRefused { cause: c } + TimeRead { time: fixed } => + PlanRead { plan: AttemptConfigurationPlan { subject: subject, attempt: nonce, expected: expected, requested: requested, fixed_at: fixed } } + } + } + } + } + } + } + } +} + +fn inspection_of(plan: AttemptConfigurationPlan, evidence: ReceiptEvidence, slots: List, doc: JsonValue) -> ReceiptValidation { + match required_string(obj: doc, key: "plan_subject") { + TextRefused { cause: c } => ReceiptRefused { cause: c } + TextRead { value: ps } => + if ps != (plan.subject as String) { + ReceiptRefused { cause: ReceiptPlanMismatch { field: "subject", plan: plan.subject as String, inspection: ps } } + } else { + match required_string(obj: doc, key: "plan_attempt") { + TextRefused { cause: c } => ReceiptRefused { cause: c } + TextRead { value: pa } => + if pa != (plan.attempt as String) { + ReceiptRefused { cause: ReceiptPlanMismatch { field: "attempt", plan: plan.attempt as String, inspection: pa } } + } else { + inspection_body(plan: plan, evidence: evidence, slots: slots, doc: doc) + } + } + } + } +} + +fn inspection_body(plan: AttemptConfigurationPlan, evidence: ReceiptEvidence, slots: List, doc: JsonValue) -> ReceiptValidation { + match required_string(obj: doc, key: "applied") { + TextRefused { cause: c } => ReceiptRefused { cause: c } + TextRead { value: applied } => + match cpu_rows(obj: doc) { + CpusRefused { cause: c } => ReceiptRefused { cause: c } + CpusRead { rows: cpus } => + match dimm_rows(obj: doc) { + DimmsRefused { cause: c } => ReceiptRefused { cause: c } + DimmsRead { rows: dimms } => + match population_join_refusal(expected: plan.expected, cpus: cpus, slots: slots, dimms: dimms) { + Present { value: c } => ReceiptRefused { cause: c } + Absent => + match required_string(obj: doc, key: "witnessed_by") { + TextRefused { cause: c } => ReceiptRefused { cause: c } + TextRead { value: witness } => + match attested_time(obj: doc, key: "completed_at", by_key: "witnessed_by") { + TimeRefused { cause: c } => ReceiptRefused { cause: c } + TimeRead { time: completed } => + if utc_instant_before(a: completed.rendering as String, b: plan.fixed_at.rendering as String) { + ReceiptRefused { cause: ReceiptOrderingViolated { fixed_at: plan.fixed_at.rendering, completed_at: completed.rendering } } + } else { + ReceiptValidated { + receipt: AttemptInspectionReceipt { + plan: plan, applied: applied as NonEmptyStr, cpus: cpus, dimms: dimms, + completed_at: completed, evidence: evidence, witnessed_by: witness as NonEmptyStr, + } + } + } + } + } + } + } + } + } +} + +// ── THE POPULATION JOINS ───────────────────────────────────────────────────────────────────────── +// CPU rows name exactly the plan's expected sockets, once each. DIMM rows name exactly the host's +// roster: every label known, on its roster socket, and every slot present. +fn population_join_refusal(expected: List, cpus: List, slots: List, dimms: List) -> AttemptReceiptRefusal? { + let recorded = map(cpus, r => r.socket) + let wrong_socket: List = flat_map(dimms, d => flat_map(slots, sl => if (sl.label as String) == (d.label as String) && sl.socket != d.socket { [ReceiptDimmOnWrongSocket { label: d.label, recorded: d.socket, roster: sl.socket }] } else { [] })) + if count(recorded) != count(expected) || any(expected, k => !any(recorded, j => j == k)) || any(recorded, k => !any(expected, j => j == k)) { + Present { value: ReceiptCpusNotTheExpectedSockets { expected: expected, recorded: recorded } } + } else { + match filter(dimms, d => !any(slots, sl => (sl.label as String) == (d.label as String))).first() { + Present { value: d } => Present { value: ReceiptDimmUnknownSlot { label: d.label } } + Absent => + match wrong_socket.first() { + Present { value: c } => Present { value: c } + Absent => + match filter(slots, sl => !any(dimms, d => (d.label as String) == (sl.label as String))).first() { + Present { value: sl } => Present { value: ReceiptDimmSlotOmitted { label: sl.label } } + Absent => none + } + } + } + } +} + +// ── FIELD READERS: a missing, null, empty or mistyped field refuses by name ───────────────────── +type TextOf + = TextRead { value: String } + | TextRefused { cause: AttemptReceiptRefusal } + +fn required_string(obj: JsonValue, key: String) -> TextOf { + match json_field_string(obj: obj, key: key) { + FieldAbsent => TextRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "missing or null" } } + FieldMalformed { cause: c } => TextRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: c } } + FieldRead { value: v } => + if trim(s: v) == "" { + TextRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "empty" } } + } else { + TextRead { value: trim(s: v) } + } + } +} + +type ValueOf + = ValueRead { value: JsonValue } + | ValueRefused { cause: AttemptReceiptRefusal } + +fn required_object(obj: JsonValue, key: String) -> ValueOf { + match json_field(obj: obj, key: key) { + FieldAbsent => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "missing or null" } } + FieldMalformed { cause: c } => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: c } } + FieldRead { value: v } => + match v { + JsonObject { members: _ } => ValueRead { value: v } + JsonNull => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "null where an object was expected" } } + JsonBool { value: _ } => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "a bool where an object was expected" } } + JsonNumber { lexeme: _ } => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "a number where an object was expected" } } + JsonString { value: _ } => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "a string where an object was expected" } } + JsonArray { elements: _ } => ValueRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "an array where an object was expected" } } + } + } +} + +// THE REQUEST DISTINGUISHES "SAID NOTHING" FROM "ASKED FOR NOTHING": a missing member refuses, an +// explicit null is NoStimulusRequested, a string is the request. +type RequestOf + = RequestRead { request: StimulusRequest } + | RequestRefused { cause: AttemptReceiptRefusal } + +fn requested_of(doc: JsonValue) -> RequestOf { + match json_member_presence(obj: doc, key: "requested") { + JsonMemberMissing => RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: "missing; write null when no change was requested" } } + JsonMemberNull => RequestRead { request: NoStimulusRequested } + JsonMemberUnreadable { cause: c } => RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: c } } + JsonMemberValue { value: v } => + match v { + JsonString { value: s } => + if trim(s: s) == "" { + RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: "empty; write null when no change was requested" } } + } else { + RequestRead { request: StimulusRequested { description: trim(s: s) as NonEmptyStr } } + } + JsonNull => RequestRead { request: NoStimulusRequested } + JsonBool { value: _ } => RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: "a bool where a string or null was expected" } } + JsonNumber { lexeme: _ } => RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: "a number where a string or null was expected" } } + JsonArray { elements: _ } => RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: "an array where a string or null was expected" } } + JsonObject { members: _ } => RequestRefused { cause: ReceiptFieldUnreadable { field: "requested", cause: "an object where a string or null was expected" } } + } + } +} + +type TimeOf + = TimeRead { time: OperatorAttestedTime } + | TimeRefused { cause: AttemptReceiptRefusal } + +fn attested_time(obj: JsonValue, key: String, by_key: String) -> TimeOf { + match required_string(obj: obj, key: key) { + TextRefused { cause: c } => TimeRefused { cause: c } + TextRead { value: t } => + if !utc_instant_is_canonical(t: t) { + TimeRefused { cause: ReceiptTimeUnreadable { field: key as NonEmptyStr, rendering: t } } + } else { + match required_string(obj: obj, key: by_key) { + TextRefused { cause: c } => TimeRefused { cause: c } + TextRead { value: by } => TimeRead { time: OperatorAttestedTime { rendering: t as NonEmptyStr, attested_by: by as NonEmptyStr } } + } + } + } +} + +fn socket_number(v: JsonValue) -> Int? { + match v { + JsonNumber { lexeme: lx } => + match parse_int(s: lx) { + Present { value: n } => if n < 0 { none } else { Present { value: n } } + Absent => none + } + JsonNull => none + JsonBool { value: _ } => none + JsonString { value: _ } => none + JsonArray { elements: _ } => none + JsonObject { members: _ } => none + } +} + +type SocketsOf + = SocketsRead { sockets: List } + | SocketsRefused { cause: AttemptReceiptRefusal } + +type SocketAcc { + sockets: List + bad: Bool +} + +fn socket_list(obj: JsonValue, key: String) -> SocketsOf { + match json_field(obj: obj, key: key) { + FieldAbsent => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "missing or null" } } + FieldMalformed { cause: c } => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: c } } + FieldRead { value: v } => + match v { + JsonArray { elements: es } => { + let none_yet: List = [] + let acc = fold(es, init: SocketAcc { sockets: none_yet, bad: false }, f: (a, e) => match socket_number(v: e) { + Present { value: n } => SocketAcc { sockets: concat(a.sockets, [n]), bad: a.bad || any(a.sockets, k => k == n) } + Absent => SocketAcc { sockets: a.sockets, bad: true } + }) + if acc.bad || acc.sockets.length() == 0 { + SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "must be a non-empty list of distinct non-negative socket numbers" } } + } else { + SocketsRead { sockets: acc.sockets } + } + } + JsonNull => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "null where a list was expected" } } + JsonBool { value: _ } => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "a bool where a list was expected" } } + JsonNumber { lexeme: _ } => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "a number where a list was expected" } } + JsonString { value: _ } => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "a string where a list was expected" } } + JsonObject { members: _ } => SocketsRefused { cause: ReceiptFieldUnreadable { field: key as NonEmptyStr, cause: "an object where a list was expected" } } + } + } +} + +fn bool_field(obj: JsonValue, key: String) -> Bool? { + match json_field(obj: obj, key: key) { + FieldRead { value: v } => + match v { + JsonBool { value: b } => Present { value: b } + JsonNull => none + JsonNumber { lexeme: _ } => none + JsonString { value: _ } => none + JsonArray { elements: _ } => none + JsonObject { members: _ } => none + } + FieldAbsent => none + FieldMalformed { cause: _ } => none + } +} + +fn int_field(obj: JsonValue, key: String) -> Int? { + match json_field(obj: obj, key: key) { + FieldRead { value: v } => socket_number(v: v) + FieldAbsent => none + FieldMalformed { cause: _ } => none + } +} + +fn row_array(obj: JsonValue, key: String) -> List? { + match json_field(obj: obj, key: key) { + FieldRead { value: v } => + match v { + JsonArray { elements: es } => Present { value: es } + JsonNull => none + JsonBool { value: _ } => none + JsonNumber { lexeme: _ } => none + JsonString { value: _ } => none + JsonObject { members: _ } => none + } + FieldAbsent => none + FieldMalformed { cause: _ } => none + } +} + +type CpusOf + = CpusRead { rows: List } + | CpusRefused { cause: AttemptReceiptRefusal } + +type CpuAcc { + rows: List + bad: Bool +} + +fn cpu_row(e: JsonValue) -> SocketCpuRow? { + match int_field(obj: e, key: "socket") { + Absent => none + Present { value: s } => + match bool_field(obj: e, key: "installed") { + Absent => none + Present { value: b } => Present { value: SocketCpuRow { socket: s, installed: b } } + } + } +} + +fn cpu_rows(obj: JsonValue) -> CpusOf { + match row_array(obj: obj, key: "cpus") { + Absent => CpusRefused { cause: ReceiptFieldUnreadable { field: "cpus", cause: "must be a list of (socket, installed) rows" } } + Present { value: es } => { + let none_yet: List = [] + let acc = fold(es, init: CpuAcc { rows: none_yet, bad: false }, f: (a, e) => match cpu_row(e: e) { + Present { value: r } => CpuAcc { rows: concat(a.rows, [r]), bad: a.bad || any(a.rows, x => x.socket == r.socket) } + Absent => CpuAcc { rows: a.rows, bad: true } + }) + if acc.bad || acc.rows.length() == 0 { + CpusRefused { cause: ReceiptFieldUnreadable { field: "cpus", cause: "must be a non-empty list of (socket, installed) rows, one per socket" } } + } else { + CpusRead { rows: acc.rows } + } + } + } +} + +type DimmsOf + = DimmsRead { rows: List } + | DimmsRefused { cause: AttemptReceiptRefusal } + +type DimmAcc { + rows: List + bad: Bool +} + +fn dimm_row(e: JsonValue) -> SlotRow? { + match required_string(obj: e, key: "label") { + TextRefused { cause: _ } => none + TextRead { value: l } => + match int_field(obj: e, key: "socket") { + Absent => none + Present { value: s } => + match bool_field(obj: e, key: "populated") { + Absent => none + Present { value: p } => Present { value: SlotRow { label: l as NonEmptyStr, socket: s, populated: p } } + } + } + } +} + +fn dimm_rows(obj: JsonValue) -> DimmsOf { + match row_array(obj: obj, key: "dimms") { + Absent => DimmsRefused { cause: ReceiptFieldUnreadable { field: "dimms", cause: "must be a list of (label, socket, populated) rows" } } + Present { value: es } => { + let none_yet: List = [] + let acc = fold(es, init: DimmAcc { rows: none_yet, bad: false }, f: (a, e) => match dimm_row(e: e) { + Present { value: r } => DimmAcc { rows: concat(a.rows, [r]), bad: a.bad || any(a.rows, x => (x.label as String) == (r.label as String)) } + Absent => DimmAcc { rows: a.rows, bad: true } + }) + if acc.bad || acc.rows.length() == 0 { + DimmsRefused { cause: ReceiptFieldUnreadable { field: "dimms", cause: "must be a non-empty list of (label, socket, populated) rows, one per slot label" } } + } else { + DimmsRead { rows: acc.rows } + } + } + } +} + +// ── THE CREATE-ONCE ATTEMPT SLOT ──────────────────────────────────────────────────────────────── +// ITS OWN NAMESPACE: a store root beside, not inside, the unit hold store, so no hold release, +// recovery or cleanup reaches it. Absent -> Consumed is the only successful transition (the CAS +// expects the slot absent), and nothing in this repository writes a later generation or deletes one. +data boot_attempt_slot_root: NonEmptyStr = "/var/lib/gunbc/boot-attempts" + +// THE KEY IS INJECTIVE BY CONSTRUCTION, NOT BY A HASH. The stable host identity is length-prefixed, +// and both it and the nonce are admitted only over [A-Za-z0-9_-], so the encoding parses back +// uniquely, carries no path separator or dot (the CAS store's generation delimiter), and never +// embeds a serialized ManagedHost. A nonce or host outside that set refuses; nothing is escaped or +// rewritten into it. +fn slot_safe_char(c: String) -> Bool { + (c >= "0" && c <= "9") || (c >= "A" && c <= "Z") || (c >= "a" && c <= "z") || c == "-" || c == "_" +} + +fn slot_safe_from(s: String, i: Int) -> Bool { + if i >= string_length(s: s) { true } else { slot_safe_char(c: char_at(s: s, pos: i)) && slot_safe_from(s: s, i: i + 1) } +} + +fn slot_safe(s: String) -> Bool { + s != "" && slot_safe_from(s: s, i: 0) +} + +fn attempt_slot_key(host: HostIdentity, nonce: NonEmptyStr) -> NonEmptyStr { + join(["attempt-", to_string(string_length(s: host as String)), "-", host as String, "-", nonce as String], "") as NonEmptyStr +} + +type SlotConsumption + = SlotConsumed { slot: NonEmptyStr } + | SlotRefused { cause: AttemptReceiptRefusal } + +fn slot_consumption_payload(receipt: AttemptInspectionReceipt) -> NonEmptyStr { + join(["consumed by ", receipt_label(e: receipt.evidence) as String], "") as NonEmptyStr +} + +// THE ONLY WRITE, reachable only from admit_named_receipt (itself reachable only from +// admit_boot_attempt, which holds the store-host executor) and from the wet witness that exercises it +// against a temporary root. +fn consume_attempt_slot(root: NonEmptyStr, key: NonEmptyStr, payload: NonEmptyStr) -> SlotConsumption + admit_callers: [ + decl_ref(module_path: "gunbc.host_boot_attempt_admission", decl_name: "admit_named_receipt"), + decl_ref(module_path: "test.claim.host_boot_attempt_admission_wet_witness", decl_name: "attempt_slot_controls"), + ] +{ + match admit_cas_attempt_for_derived_payload(key: key, expected: ExpectSlotAbsent, proposed: payload) { + DerivedPayloadKeyNotSlotAddressable { key: k } => SlotRefused { cause: AttemptSlotKeyNotAddressable { slot: k } } + DerivedPayloadAdmitted { verified: v } => + match file_compare_and_set(root: root, publication: DefaultAccessCreateOnly, verified: v) { + CasCommitted { committed: _ } => SlotConsumed { slot: key } + CasPreconditionFailed { expected: _, observed: o } => + match o { + CasReadablePresent { version: ver } => SlotRefused { cause: AttemptAlreadyConsumed { slot: key, consumed_by: ver.value as String } } + CasReadableAbsent => SlotRefused { cause: AttemptSlotPreconditionIncoherent { slot: key } } + } + CasStoreRefused { cause: c } => SlotRefused { cause: AttemptSlotStoreRefused { slot: key, cause: c } } + } + } +} + +// ── THE ADMISSION ─────────────────────────────────────────────────────────────────────────────── +// TAKEN UNDER THE UNIT HOLD, FROM ITS PROOF: the host is the hold's admitted subject, never a label, +// and the store-host executor is minted from that subject by gunbc.managed_host_unit_hold's own read +// of this process's hostname. THE ORDER IS THE CONTRACT: route, receipt variable (absent clears as +// NotNamed and touches nothing), executor, binding, nonce, slot-safety, path, read, every check on the +// file, and only then the slot. +fn admit_boot_attempt(proof: UnitHoldProof, revision: NonEmptyStr) -> BootAttemptAdmission { + let host = proof.subject.host + match attempt_receipt_route(host: host) { + Absent => BootAttemptRefused { cause: ReceiptHostHasNoRoute { host: host.host } } + Present { value: route } => + match actions_variable_read(name: route.receipt_env as String) { + ActionsVariableAbsent { variable: _, detail: _ } => BootAttemptCleared { clearance: BootAttemptClearance { host: host.host, source: ConfigurationReceiptNotNamed } } + ActionsVariablePresent { value: path } => + match unit_hold_store_executor(subject: proof.subject) { + UnitHoldNotOnStoreHost { reason: r } => BootAttemptRefused { cause: ReceiptExecutorNotOnStoreHost { reason: r } } + UnitHoldOnStoreHost { executor: e } => + match managed_host_binding(host: host) { + ManagedHostAccessUnobserved { endpoint: _ } => BootAttemptRefused { cause: ReceiptHostUnbound { detail: "its controller access is unobserved" } } + ManagedHostNotSecured { cause: _ } => BootAttemptRefused { cause: ReceiptHostUnbound { detail: "its controller is not secured" } } + ManagedHostEndpointMismatch { observed: _, secured: _ } => BootAttemptRefused { cause: ReceiptHostUnbound { detail: "its access and secure standings name different controllers" } } + ManagedHostBound { binding: b } => + if !host_identity_eq(a: e.subject.host.host, b: b.host.host) { + BootAttemptRefused { cause: ReceiptExecutorForAnotherHost { executor_host: e.subject.host.host, bound: b.host.host } } + } else { + match actions_variable_read(name: route.nonce_env as String) { + ActionsVariableAbsent { variable: v, detail: d } => BootAttemptRefused { cause: ReceiptNonceMissing { variable: v as NonEmptyStr, detail: d } } + ActionsVariablePresent { value: nonce } => admit_named_receipt(host: b.host.host, nonce: nonce, path: path, revision: revision, slots: route.slots) + } + } + } + } + } + } +} + +// REACHABLE ONLY FROM admit_boot_attempt, which established the store-host executor for this host. +fn admit_named_receipt(host: HostIdentity, nonce: String, path: String, revision: NonEmptyStr, slots: List) -> BootAttemptAdmission + admit_callers: [decl_ref(module_path: "gunbc.host_boot_attempt_admission", decl_name: "admit_boot_attempt")] +{ + match named_receipt_validation(host: host, nonce: nonce, path: path, revision: revision, slots: slots) { + ReceiptRefused { cause: c } => BootAttemptRefused { cause: c } + ReceiptValidated { receipt: r } => + match consume_attempt_slot(root: boot_attempt_slot_root, key: attempt_slot_key(host: host, nonce: r.plan.attempt), payload: slot_consumption_payload(receipt: r)) { + SlotRefused { cause: c } => BootAttemptRefused { cause: c } + SlotConsumed { slot: k } => BootAttemptCleared { clearance: BootAttemptClearance { host: host, source: ConfigurationReceiptAdmitted { receipt: r, slot: k } } } + } + } +} + +// EVERYTHING BEFORE THE SLOT: the named values, then the tracked blob at the bound revision and its +// SHA-256, then the document. +fn named_receipt_validation(host: HostIdentity, nonce: String, path: String, revision: NonEmptyStr, slots: List) -> ReceiptValidation { + if !slot_safe(s: host as String) { + ReceiptRefused { cause: ReceiptHostNotSlotSafe { host: host } } + } else if !slot_safe(s: nonce) { + ReceiptRefused { cause: ReceiptNonceNotSlotSafe { nonce: nonce as NonEmptyStr } } + } else if !receipt_path_admitted(path: path) { + ReceiptRefused { cause: ReceiptPathOutsideReceipts { path: path as NonEmptyStr } } + } else { + let listed = git.Inspect.ListTreeEntryAtPath(ref: revision as GitRef, path: path) + if !listed.success { + ReceiptRefused { cause: ReceiptFileUnreadable { path: path as NonEmptyStr, detail: trim(s: listed.stderr) } } + } else { + match tracked_entry_refusal(path: path as NonEmptyStr, commit: revision, entries_nul: listed.entries_nul) { + Present { value: c } => ReceiptRefused { cause: c } + Absent => { + let shown = git.Core.Show(ref: revision as GitRef, path: path as FilePath) + if !shown.success { + ReceiptRefused { cause: ReceiptFileUnreadable { path: path as NonEmptyStr, detail: trim(s: shown.stderr) } } + } else { + validate_attempt_receipt( + subject: host, nonce: nonce as NonEmptyStr, path: path as NonEmptyStr, commit: revision, slots: slots, + content: shown.content, digest: sha256sum_stdin_digest_via_shell(content: shown.content), + ) + } + } + } + } + } +} + +// ── THE PROJECTION THE POWER-ON ACCOUNT READS ─────────────────────────────────────────────────── +// THE REASON NAMES THE HUMAN STEP THAT WOULD HAVE RECORDED IT, read off the step itself. +fn boot_attempt_receipt_not_named_reason() -> NonEmptyStr { + join([ + "the dispatch named no attempt receipt, so this attempt's configuration was not recorded; the human step ", + boot_attempt_inspection_step.identity as String, " records it: ", boot_attempt_inspection_step.instruction as String, + ], "") as NonEmptyStr +} + +data boot_attempt_firmware_frontier: NonEmptyStr = "the pre-power-on firmware readback is slice B2 of docs/plans/power-on-sequence-model.md section 12 and is not read yet" + +fn receipt_label(e: ReceiptEvidence) -> NonEmptyStr { + join([e.path as String, "@", e.commit as String, " (", digest_label(d: e.digest) as String, ")"], "") as NonEmptyStr +} + +fn attempt_configuration_receipt(clearance: BootAttemptClearance, attempt: NonEmptyStr) -> AttemptConfigurationReceipt { + attempt_configuration_receipt_of(host: clearance.host, source: clearance.source, attempt: attempt) +} + +// THE PROJECTION OVER ITS SOURCE, so a claim can supply the source a clearance would carry. +fn attempt_configuration_receipt_of(host: HostIdentity, source: AttemptConfigurationSource, attempt: NonEmptyStr) -> AttemptConfigurationReceipt { + match source { + ConfigurationReceiptNotNamed => + AttemptConfigurationReceipt { + subject: host as NonEmptyStr, + attempt: attempt, + expected: ExpectedTopologyNotRecorded { reason: boot_attempt_receipt_not_named_reason() }, + requested: StimulusRequestNotRecorded { reason: boot_attempt_receipt_not_named_reason() }, + applied: StimulusApplicationNotRecorded { reason: boot_attempt_receipt_not_named_reason() }, + cpus: PopulationNotRecorded { reason: boot_attempt_receipt_not_named_reason() }, + dimms: PopulationNotRecorded { reason: boot_attempt_receipt_not_named_reason() }, + firmware: FirmwareReadbacksNotRecorded { reason: boot_attempt_firmware_frontier }, + } + ConfigurationReceiptAdmitted { receipt: r, slot: _ } => + AttemptConfigurationReceipt { + subject: host as NonEmptyStr, + attempt: r.plan.attempt, + expected: ExpectedSockets { sockets: r.plan.expected, source: receipt_label(e: r.evidence) }, + requested: r.plan.requested, + applied: StimulusAppliedByReceipt { receipt: concat(concat(receipt_label(e: r.evidence) as String, ": "), r.applied as String) as NonEmptyStr, attested_by: r.witnessed_by }, + cpus: PopulationOperatorAttested { rows: r.cpus, receipt: receipt_label(e: r.evidence) }, + dimms: PopulationOperatorAttested { rows: r.dimms, receipt: receipt_label(e: r.evidence) }, + firmware: FirmwareReadbacksNotRecorded { reason: boot_attempt_firmware_frontier }, + } + } +} + +// THE CONFIGURATION OF AN ATTEMPT THAT NEVER REACHED ADMISSION, or whose named receipt was refused: +// nothing was recorded, and the reason says which. +fn attempt_configuration_not_recorded(host: NonEmptyStr, attempt: NonEmptyStr, reason: NonEmptyStr) -> AttemptConfigurationReceipt { + AttemptConfigurationReceipt { + subject: host, + attempt: attempt, + expected: ExpectedTopologyNotRecorded { reason: reason }, + requested: StimulusRequestNotRecorded { reason: reason }, + applied: StimulusApplicationNotRecorded { reason: reason }, + cpus: PopulationNotRecorded { reason: reason }, + dimms: PopulationNotRecorded { reason: reason }, + firmware: FirmwareReadbacksNotRecorded { reason: reason }, + } +} + +fn attempt_configuration_refused(host: NonEmptyStr, attempt: NonEmptyStr, cause: AttemptReceiptRefusal) -> AttemptConfigurationReceipt { + attempt_configuration_not_recorded(host: host, attempt: attempt, reason: concat("the named attempt receipt was refused: ", attempt_receipt_refusal_text(cause: cause)) as NonEmptyStr) +} + +fn attempt_receipt_refusal_text(cause: AttemptReceiptRefusal) -> String { + match cause { + ReceiptHostHasNoRoute { host: h } => join(["managed host '", h as String, "' has no attempt receipt route in gunbc.host_boot_attempt_admission"], "") + ReceiptExecutorForAnotherHost { executor_host: e, bound: b } => join(["the store-host executor was admitted for '", e as String, "' and the boot is bound to '", b as String, "'"], "") + ReceiptExecutorNotOnStoreHost { reason: r } => r as String + ReceiptHostUnbound { detail: d } => join(["the managed host does not bind (", d as String, "), so a named receipt cannot be joined to it"], "") + ReceiptNonceMissing { variable: v, detail: d } => join(["an attempt receipt was named but the attempt nonce ", v as String, " is ", d], "") + ReceiptNonceNotSlotSafe { nonce: n } => join(["the attempt nonce '", n as String, "' is outside [A-Za-z0-9_-]"], "") + ReceiptHostNotSlotSafe { host: h } => join(["the host identity '", h as String, "' is outside [A-Za-z0-9_-]"], "") + ReceiptPathOutsideReceipts { path: p } => join(["the attempt receipt '", p as String, "' is not a .json file under ", boot_attempt_receipt_dir as String], "") + ReceiptNotTracked { path: p, commit: c } => join(["the attempt receipt '", p as String, "' is not tracked at ", c as String], "") + ReceiptNotRegularFile { path: p, mode: m, kind: k } => join(["the attempt receipt '", p as String, "' is not a regular file at the revision (mode ", m, ", ", k, ")"], "") + ReceiptDigestUnavailable { path: p, reason: r } => join(["the attempt receipt '", p as String, "' could not be digested: ", r], "") + ReceiptFileUnreadable { path: p, detail: d } => join(["the attempt receipt '", p as String, "' could not be read: ", d], "") + ReceiptNotJson { path: p, detail: d } => join(["the attempt receipt '", p as String, "' is ", d], "") + ReceiptSchemaMismatch { observed: o } => join(["the attempt receipt's schema is '", o, "', expected '", boot_attempt_receipt_schema as String, "'"], "") + ReceiptFieldUnreadable { field: f, cause: c } => join(["the attempt receipt's ", f as String, " is unreadable: ", c], "") + ReceiptTimeUnreadable { field: f, rendering: r } => join(["the attempt receipt's ", f as String, " '", r, "' is not YYYY-MM-DDTHH:MM:SSZ"], "") + ReceiptSubjectMismatch { receipt: r, bound: b } => join(["the attempt receipt is for '", r, "' and the boot is bound to '", b as String, "'"], "") + ReceiptAttemptMismatch { receipt: r, dispatched: d } => join(["the attempt receipt is for attempt '", r, "' and this dispatch is attempt '", d as String, "'"], "") + ReceiptPlanMismatch { field: f, plan: p, inspection: i } => join(["the inspection names plan ", f as String, " '", i, "' and the plan's is '", p, "'"], "") + ReceiptOrderingViolated { fixed_at: a, completed_at: b } => join(["the inspection completed at ", b as String, ", before the plan was fixed at ", a as String], "") + ReceiptCpusNotTheExpectedSockets { expected: e, recorded: r } => join(["the inspection's CPU rows name sockets [", join(map(r, k => to_string(k)), ", "), "] and the plan expects [", join(map(e, k => to_string(k)), ", "), "]"], "") + ReceiptDimmUnknownSlot { label: l } => join(["the inspection names DIMM slot '", l as String, "', which the host's slot roster does not have"], "") + ReceiptDimmOnWrongSocket { label: l, recorded: r, roster: k } => join(["the inspection places DIMM slot '", l as String, "' on socket ", to_string(r), " and the host's roster puts it on socket ", to_string(k)], "") + ReceiptDimmSlotOmitted { label: l } => join(["the inspection omits DIMM slot '", l as String, "'; every slot is recorded, populated or not"], "") + AttemptAlreadyConsumed { slot: k, consumed_by: c } => join(["attempt slot ", k as String, " was already consumed (", c, "); a nonce admits one boot"], "") + AttemptSlotKeyNotAddressable { slot: k } => join(["attempt slot key ", k as String, " does not address a slot"], "") + AttemptSlotPreconditionIncoherent { slot: k } => join(["attempt slot ", k as String, ": the store refused a create against a slot it reported absent"], "") + AttemptSlotStoreRefused { slot: k, cause: c } => join(["attempt slot ", k as String, " could not be consumed: ", cas_store_failure_text(cause: c)], "") + } +} + +fn cas_store_failure_text(cause: CasStoreFailure) -> String { + match cause { + CasSlotObservationRefused { cause: u } => cas_unreadable_slot_detail(cause: u) + CasGenerationPublicationRefused { detail: d } => d as String + CasGenerationSpaceExhausted { head: h } => join(["the slot's generation space is exhausted at ", to_string(cas_generation_count(g: h))], "") + } +} diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag b/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag index 57759f7a2e1..361b7c34a00 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag @@ -66,8 +66,8 @@ import gunbc.machine_intake_mtcollins1_power_on_account { Carrier, SolConsole, KvmScreen, SmproRegisters, SmproErrorRegisters, SystemEventLog, SensorTable, ChassisPower, RedfishInventory, VirtualMedia, HostCaptureMarkers, CarrierCoverage, CarrierStanding, CarrierRead, CarrierReadEmpty, CarrierPartial, CarrierRefused, CarrierNotTaken, PowerOnHandoff, HandoffPoweredOn, HandoffNotConfirmed, SelEvidence, SelEventsRead, SelEventsNotRead, - WatchdogUnobserved, ExpectedSockets, ExpectedTopologyNotRecorded, StimulusRequestNotRecorded, - PopulationLiveObserved, PopulationOperatorAttested, PopulationConflicted, SlotRow, StimulusApplicationNotRecorded, PopulationNotRecorded, FirmwareReadbacksNotRecorded, + WatchdogUnobserved, ExpectedSockets, ExpectedTopologyNotRecorded, + PopulationLiveObserved, PopulationOperatorAttested, PopulationConflicted, SlotRow, PopulationNotRecorded, ProcessorMissingOnExpectedSocket, ProcessorSocketDuplicated, ProcessorSocketUnreadable, ProcessorNotNominal, ProcessorAbsentOnExpectedSocket, MemoryBelowRecordedPopulation, MemoryNotNominal, SelHardwareEvent, mtcollins1_power_on_account, mtcollins1_power_on_account_text, mtcollins1_power_on_account_notes, SpanConsoleReading, span_console_readings, } @@ -1031,6 +1031,7 @@ type MtCollins1BootDiagnosticBundle { console: ConsoleReading run: MtCollins1BootRunRecord screen: KvmObserverRecord + configuration: AttemptConfigurationReceipt } fn inventory_not_taken(reason: NonEmptyStr) -> InventoryReading { @@ -1540,31 +1541,9 @@ fn mtcollins1_boot_coverage(bundle: MtCollins1BootDiagnosticBundle) -> List AttemptConfigurationReceipt { - AttemptConfigurationReceipt { - subject: "mtcollins1", - attempt: attempt_identity_text(a: attempt) as NonEmptyStr, - expected: ExpectedTopologyNotRecorded { reason: mtcollins1_receipt_input_frontier }, - requested: StimulusRequestNotRecorded { reason: mtcollins1_receipt_input_frontier }, - applied: StimulusApplicationNotRecorded { reason: mtcollins1_receipt_input_frontier }, - cpus: PopulationNotRecorded { reason: mtcollins1_receipt_input_frontier }, - dimms: PopulationNotRecorded { reason: mtcollins1_receipt_input_frontier }, - firmware: FirmwareReadbacksNotRecorded { reason: mtcollins1_receipt_input_frontier }, - } -} - fn mtcollins1_boot_evidence(bundle: MtCollins1BootDiagnosticBundle) -> PowerOnEvidence { let delta = sel_delta_reading(before: bundle.sel_before, after: bundle.sel_after) - let receipt = mtcollins1_attempt_configuration_receipt(attempt: bundle.attempt) + let receipt = bundle.configuration PowerOnEvidence { configuration: receipt, handoff: handoff_standing(h: bundle.run.handoff_media), diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag index 583fc252dc5..b11ec4d4de9 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag @@ -87,7 +87,11 @@ import gunbc.managed_host { } import extdeps.bmc.ipmi_boot_selection { IpmiBootSelection } import extdeps.bmc.ipmi_chassis_control { ChassisPowerObservation, chassis_observation_text } -import gunbc.machine_intake_mtcollins1_power_on_account { CarrierRead, CarrierReadEmpty, CarrierPartial, CarrierRefused, CarrierNotTaken, mtcollins1_power_on_account_notes, carrier_text, carrier_standing_text } +import gunbc.host_boot_attempt_admission { + BootAttemptCleared, BootAttemptRefused, admit_boot_attempt, attempt_configuration_receipt, + attempt_configuration_not_recorded, attempt_configuration_refused, attempt_receipt_refusal_text, +} +import gunbc.machine_intake_mtcollins1_power_on_account { AttemptConfigurationReceipt, CarrierRead, CarrierReadEmpty, CarrierPartial, CarrierRefused, CarrierNotTaken, mtcollins1_power_on_account_notes, carrier_text, carrier_standing_text } import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle { MtCollins1BootDiagnosticBundle, SelSnapshotReading, SelSnapshotNotTaken, inventory_not_taken, SdrCacheReading, SdrCacheNotTaken, mtcollins1_boot_sdr_cache, @@ -2287,7 +2291,7 @@ fn mtcollins1_boot_actuate( resolve_toolchain: fn() -> RunnerBrowserToolchainResolution, ) -> MtCollins1BootActuation admit_callers: [ - decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_under_live_unit_hold"), + decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_actuate_held"), ] { let hold_acquired = proc_uptime_read() @@ -2451,6 +2455,25 @@ fn mtcollins1_boot_actuate( // the only arm that reaches a BMC write is UnitHeld, whose proof exists only because the // compare-and-set this call made committed. Nothing is supplied: there is no admission parameter a // caller could author. The hold is freed whatever the actuation answered. +// THE ACTUATION AND THE ATTEMPT CONFIGURATION IT RAN UNDER, frozen by gunbc.host_boot_attempt_admission +// before any pre-power read or write. +type MtCollins1HeldBoot { + actuation: MtCollins1BootActuation + configuration: AttemptConfigurationReceipt + baseline: MtCollins1BootBaseline +} + +// THE ATTEMPT'S BMC BASELINE (the SDR cache and the SEL before), taken only under the unit hold and +// after the attempt's configuration is admitted: a refused receipt reads nothing from the controller. +type MtCollins1BootBaseline { + sdr: SdrCacheReading + sel_before: SelSnapshotReading +} + +fn baseline_not_taken(reason: NonEmptyStr) -> MtCollins1BootBaseline { + MtCollins1BootBaseline { sdr: SdrCacheNotTaken { reason: reason }, sel_before: SelSnapshotNotTaken { reason: reason } } +} + fn mtcollins1_boot_under_live_unit_hold( run_id: NonEmptyStr, subject: MtCollins1BootSubject, @@ -2458,28 +2481,69 @@ fn mtcollins1_boot_under_live_unit_hold( sol_pid_path: String, sol_capture_path: String, resolve_toolchain: fn() -> RunnerBrowserToolchainResolution, -) -> MtCollins1BootActuation + baseline: fn() -> MtCollins1BootBaseline, +) -> MtCollins1HeldBoot admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_on_srv1_resolving_toolchain"), ] { match boot_run_acquire_unit_hold(host: operator_host_mtcollins1, run_id: run_id) { - UnitHoldRefused { reason: r } => actuation_not_powered_on(outcome: exit_failure(reason: concat("mtcollins1 boot: ", r as String)), reason: "the unit hold was refused, so nothing was written") - UnitHeld { proof: p } => { - let act = mtcollins1_boot_actuate( - proof: p, - subject: subject, - password_file: password_file, - attempt: run_id as String, - sol_pid_path: sol_pid_path, - sol_capture_path: sol_capture_path, - resolve_toolchain: resolve_toolchain, - ) - MtCollins1BootActuation { outcome: unit_hold_release(proof: p, outcome: act.outcome), media: act.media, handoff_media: act.handoff_media, end_media: act.end_media, stage: act.stage, override_before: act.override_before, override_after: act.override_after, power_after: act.power_after, timing: act.timing, screen: act.screen } - } + UnitHoldRefused { reason: r } => + MtCollins1HeldBoot { + actuation: actuation_not_powered_on(outcome: exit_failure(reason: concat("mtcollins1 boot: ", r as String)), reason: "the unit hold was refused, so nothing was written"), + configuration: attempt_configuration_not_recorded(host: operator_host_mtcollins1 as NonEmptyStr, attempt: run_id, reason: "the unit hold was refused, so the attempt receipt was not admitted"), + baseline: baseline_not_taken(reason: "the unit hold was refused, so the controller was not read"), + } + UnitHeld { proof: p } => + match admit_boot_attempt(proof: p, revision: subject.execution_revision) { + BootAttemptRefused { cause: c } => { + let why = concat("mtcollins1 boot: attempt receipt refused: ", attempt_receipt_refusal_text(cause: c)) + MtCollins1HeldBoot { + actuation: actuation_not_powered_on(outcome: unit_hold_release(proof: p, outcome: exit_failure(reason: why)), reason: "the named attempt receipt was refused, so nothing was written"), + configuration: attempt_configuration_refused(host: operator_host_mtcollins1 as NonEmptyStr, attempt: run_id, cause: c), + baseline: baseline_not_taken(reason: "the named attempt receipt was refused, so the controller was not read"), + } + } + BootAttemptCleared { clearance: clearance } => { + let configuration = attempt_configuration_receipt(clearance: clearance, attempt: run_id) + let taken = baseline() + let actuation = mtcollins1_boot_actuate_held(proof: p, subject: subject, password_file: password_file, run_id: run_id, sol_pid_path: sol_pid_path, sol_capture_path: sol_capture_path, resolve_toolchain: resolve_toolchain) + MtCollins1HeldBoot { actuation: actuation, configuration: configuration, baseline: taken } + } + } } } +fn mtcollins1_boot_baseline(username: NonEmptyStr, password_file: NonEmptyStr) -> MtCollins1BootBaseline { + let sdr = mtcollins1_boot_sdr_cache(username: username, password_file: password_file, path: concat(password_file as String, mtcollins1_boot_sdr_cache_suffix) as NonEmptyStr) + MtCollins1BootBaseline { sdr: sdr, sel_before: mtcollins1_boot_sel_snapshot(username: username, password_file: password_file, sdr: sdr) } +} + +fn mtcollins1_boot_actuate_held( + proof: UnitHoldProof, + subject: MtCollins1BootSubject, + password_file: String, + run_id: NonEmptyStr, + sol_pid_path: String, + sol_capture_path: String, + resolve_toolchain: fn() -> RunnerBrowserToolchainResolution, +) -> MtCollins1BootActuation + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_under_live_unit_hold"), + ] +{ + let act = mtcollins1_boot_actuate( + proof: proof, + subject: subject, + password_file: password_file, + attempt: run_id as String, + sol_pid_path: sol_pid_path, + sol_capture_path: sol_capture_path, + resolve_toolchain: resolve_toolchain, + ) + MtCollins1BootActuation { outcome: unit_hold_release(proof: proof, outcome: act.outcome), media: act.media, handoff_media: act.handoff_media, end_media: act.end_media, stage: act.stage, override_before: act.override_before, override_after: act.override_after, power_after: act.power_after, timing: act.timing, screen: act.screen } +} + // EVERY TERMINAL ARM OF A BOOT ATTEMPT GOES THROUGH mtcollins1_boot_conclude (gunbc#12093), which // writes the diagnostic bundle (gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle) and the // receipt, and appends the bundle's decisive findings to a refusal reason. The attempt returns a @@ -2507,6 +2571,7 @@ type MtCollins1BootAttempt { power_after: PowerAfterAttempt timing: MtCollins1BootPhaseTiming screen: KvmObserverRecord + configuration: AttemptConfigurationReceipt } fn mtcollins1_boot_exit_reason(outcome: ProcessExit) -> String { @@ -2529,6 +2594,7 @@ fn mtcollins1_boot_ended_before_bmc(outcome: ProcessExit) -> MtCollins1BootAttem power_after: PowerAfterNotTaken { reason: "the attempt ended before the unit hold" }, timing: mtcollins1_boot_phase_timing_not_taken(reason: "the attempt ended before the unit hold"), screen: kvm_observer_record_not_started(attempt: "", reason: "the attempt ended before the unit hold"), + configuration: attempt_configuration_not_recorded(host: operator_host_mtcollins1 as NonEmptyStr, attempt: "not reached", reason: "the attempt ended before the unit hold, so no attempt receipt was admitted"), } } @@ -2548,6 +2614,7 @@ fn mtcollins1_boot_bundle_of_attempt(attempt: MtCollins1BootAttempt, run: Attemp console: mtcollins1_boot_console(path: capture_path), run: run_record_not_taken(reason: why), screen: attempt.screen, + configuration: attempt.configuration, } BmcAccessHeld { username: user, password_file: pf, password: pw, sdr_cache: sdr, sel_before: before } => { let sel_after = mtcollins1_boot_sel_snapshot(username: user, password_file: pf, sdr: sdr) @@ -2570,6 +2637,7 @@ fn mtcollins1_boot_bundle_of_attempt(attempt: MtCollins1BootAttempt, run: Attemp console: mtcollins1_boot_console(path: capture_path), run: mtcollins1_boot_run_record(media: attempt.media, handoff_media: attempt.handoff_media, end_media: attempt.end_media, stage: attempt.stage, before: attempt.override_before, after: attempt.override_after, power_after: power_after, timing: attempt.timing), screen: attempt.screen, + configuration: attempt.configuration, } } } @@ -2735,7 +2803,8 @@ fn mtcollins1_boot_on_srv1_resolving_toolchain(resolve_toolchain: fn() -> Runner let subject = mtcollins1_boot_subject(execution_revision: sha as NonEmptyStr) match mtcollins1_bmc_username { Absent => { - let act = mtcollins1_boot_under_live_unit_hold(run_id: run_id as NonEmptyStr, subject: subject, password_file: cred, sol_pid_path: sol_pid_path, sol_capture_path: sol_capture_path, resolve_toolchain: resolve_toolchain) + let held = mtcollins1_boot_under_live_unit_hold(run_id: run_id as NonEmptyStr, subject: subject, password_file: cred, sol_pid_path: sol_pid_path, sol_capture_path: sol_capture_path, resolve_toolchain: resolve_toolchain, baseline: fn() { baseline_not_taken(reason: "mtcollins1's BMC is not BmcSecured, so no account is modeled to read it with") }) + let act = held.actuation MtCollins1BootAttempt { outcome: act.outcome, media: act.media, @@ -2748,24 +2817,25 @@ fn mtcollins1_boot_on_srv1_resolving_toolchain(resolve_toolchain: fn() -> Runner power_after: act.power_after, timing: act.timing, screen: act.screen, + configuration: held.configuration, } } Present { value: user } => { - let sdr = mtcollins1_boot_sdr_cache(username: user, password_file: cred as NonEmptyStr, path: concat(cred, mtcollins1_boot_sdr_cache_suffix) as NonEmptyStr) - let before = mtcollins1_boot_sel_snapshot(username: user, password_file: cred as NonEmptyStr, sdr: sdr) - let act = mtcollins1_boot_under_live_unit_hold(run_id: run_id as NonEmptyStr, subject: subject, password_file: cred, sol_pid_path: sol_pid_path, sol_capture_path: sol_capture_path, resolve_toolchain: resolve_toolchain) + let held = mtcollins1_boot_under_live_unit_hold(run_id: run_id as NonEmptyStr, subject: subject, password_file: cred, sol_pid_path: sol_pid_path, sol_capture_path: sol_capture_path, resolve_toolchain: resolve_toolchain, baseline: fn() { mtcollins1_boot_baseline(username: user, password_file: cred as NonEmptyStr) }) + let act = held.actuation MtCollins1BootAttempt { outcome: act.outcome, media: act.media, handoff_media: act.handoff_media, end_media: act.end_media, - bmc: BmcAccessHeld { username: user, password_file: cred as NonEmptyStr, password: pw_read.content, sdr_cache: sdr, sel_before: before }, + bmc: BmcAccessHeld { username: user, password_file: cred as NonEmptyStr, password: pw_read.content, sdr_cache: held.baseline.sdr, sel_before: held.baseline.sel_before }, stage: act.stage, override_before: act.override_before, override_after: act.override_after, power_after: act.power_after, timing: act.timing, screen: act.screen, + configuration: held.configuration, } } } diff --git a/dag/gunbc/runner/runner_host_grants.dag b/dag/gunbc/runner/runner_host_grants.dag index d42abf5811e..cb74fee932b 100644 --- a/dag/gunbc/runner/runner_host_grants.dag +++ b/dag/gunbc/runner/runner_host_grants.dag @@ -53,6 +53,7 @@ import gunbc.runner_host_deploy { runner_index_seq } import gunbc.runner_microvm_network_converge { microvm_network_granted_operations } import gunbc.runner_unit { runner_unit_name_of_registration } import gunbc.managed_host_unit_hold { unit_hold_store_root, unit_hold_store_hosts } +import gunbc.host_boot_attempt_admission { boot_attempt_slot_root } // THE MANAGED STATE DIRECTORY, DECLARED ONCE. It is currently spelled THREE times in // gunbc.fleet_converge_plan and named nowhere: once as a bare literal in the lease guard's argv, and @@ -326,6 +327,11 @@ fn runner_host_wide_refused_operations(spec: RunnerHostSpec) -> List List { if any(unit_hold_store_hosts(), h => (h as String) == (spec.host_label as String)) { [ @@ -335,6 +341,12 @@ fn unit_hold_store_operations(spec: RunnerHostSpec) -> List Bool { + match c { + SlotConsumed { slot: _ } => true + SlotRefused { cause: _ } => false + } +} + +fn already_consumed(c: SlotConsumption) -> Bool { + match c { + SlotConsumed { slot: _ } => false + SlotRefused { cause: r } => refused_as_consumed(cause: r) + } +} + +fn refused_as_consumed(cause: AttemptReceiptRefusal) -> Bool { + match cause { + AttemptAlreadyConsumed { slot: _, consumed_by: _ } => true + ReceiptHostHasNoRoute { host: _ } => false + ReceiptExecutorForAnotherHost { executor_host: _, bound: _ } => false + ReceiptExecutorNotOnStoreHost { reason: _ } => false + ReceiptHostUnbound { detail: _ } => false + ReceiptNonceMissing { variable: _, detail: _ } => false + ReceiptNonceNotSlotSafe { nonce: _ } => false + ReceiptHostNotSlotSafe { host: _ } => false + ReceiptPathOutsideReceipts { path: _ } => false + ReceiptNotTracked { path: _, commit: _ } => false + ReceiptNotRegularFile { path: _, mode: _, kind: _ } => false + ReceiptDigestUnavailable { path: _, reason: _ } => false + ReceiptCpusNotTheExpectedSockets { expected: _, recorded: _ } => false + ReceiptDimmUnknownSlot { label: _ } => false + ReceiptDimmOnWrongSocket { label: _, recorded: _, roster: _ } => false + ReceiptDimmSlotOmitted { label: _ } => false + ReceiptFileUnreadable { path: _, detail: _ } => false + ReceiptNotJson { path: _, detail: _ } => false + ReceiptSchemaMismatch { observed: _ } => false + ReceiptFieldUnreadable { field: _, cause: _ } => false + ReceiptTimeUnreadable { field: _, rendering: _ } => false + ReceiptSubjectMismatch { receipt: _, bound: _ } => false + ReceiptAttemptMismatch { receipt: _, dispatched: _ } => false + ReceiptPlanMismatch { field: _, plan: _, inspection: _ } => false + ReceiptOrderingViolated { fixed_at: _, completed_at: _ } => false + AttemptSlotKeyNotAddressable { slot: _ } => false + AttemptSlotPreconditionIncoherent { slot: _ } => false + AttemptSlotStoreRefused { slot: _, cause: _ } => false + } +} + +// THE UNIT HOLD IS TAKEN AND RELEASED IN THE SAME DIRECTORY, keyed by the same host: even co-located, +// a release frees only the hold's own slot. +fn hold_taken_and_released(root: NonEmptyStr) -> Bool { + let owner = "boot-run:wet-witness" as DurableHoldOwnerRef + match file_hold_acquire(root: root, slot_key: operator_host_mtcollins1 as NonEmptyStr, requested_owner: owner) { + FileHoldAcquired { slot_key: k, owner: o, generation: g } => + match file_hold_release_assess(root: root, slot_key: k, owner: o, acquired_generation: g, released_by: "boot-run:wet-witness" as DurableHoldReleaseRef) { + FileHoldReleasePlanned { plan: p } => + match file_hold_release_commit(plan: p) { + FileHoldReleased { slot_key: _, generation: _ } => true + FileHoldReleaseLost { slot_key: _ } => false + FileHoldReleaseStoreUnavailable { slot_key: _, cause: _ } => false + FileHoldReleaseKeyNotSlotAddressable { slot_key: _ } => false + } + FileHoldReleaseNotEligible { slot_key: _, refusal: _ } => false + } + FileHoldOccupied { slot_key: _, holder: _, generation: _ } => false + FileHoldAcquireLost { slot_key: _ } => false + FileHoldAcquireStoreUnavailable { slot_key: _, cause: _ } => false + FileHoldSlotUndecodable { slot_key: _, generation: _, detail: _ } => false + FileHoldKeyNotSlotAddressable { slot_key: _ } => false + } +} + +// THE FIVE CONTROLS IN ONE ORDERED RUN over one store: the first A is consumed; a repeated A refuses +// as already consumed; B is then consumed; A still refuses after B; and after a unit hold on the same +// host is taken and released in the same directory, A still refuses. +fn attempt_slot_controls(root: NonEmptyStr) -> Bool { + let a = attempt_slot_key(host: operator_host_mtcollins1, nonce: "nonce-a") + let b = attempt_slot_key(host: operator_host_mtcollins1, nonce: "nonce-b") + let first_a = consumed(c: consume_attempt_slot(root: root, key: a, payload: "consumed by receipt-a")) + let repeated_a = already_consumed(c: consume_attempt_slot(root: root, key: a, payload: "consumed by receipt-a")) + let then_b = consumed(c: consume_attempt_slot(root: root, key: b, payload: "consumed by receipt-b")) + let a_after_b = already_consumed(c: consume_attempt_slot(root: root, key: a, payload: "consumed by receipt-a")) + let released = hold_taken_and_released(root: root) + let a_after_release = already_consumed(c: consume_attempt_slot(root: root, key: a, payload: "consumed by receipt-a")) + first_a && repeated_a && then_b && a_after_b && released && a_after_release +} + +test fn an_attempt_slot_admits_each_nonce_once_across_later_attempts_and_hold_releases_by_real_execution() -> Bool { + let root_path = shell.Mktemp.DirWithTemplate(template: "/tmp/gunbc_boot_attempt.XXXXXX").path + let held = attempt_slot_controls(root: root_path as NonEmptyStr) + let removed = shell.Remove.RecursiveForce(path: root_path) + held && removed.success +} + +// THE RECEIPT'S EVIDENCE IS THE SHA-256 OF ITS BYTES, taken by the same authority admission uses: one +// changed byte changes it, and the same bytes give the same digest. +fn digest_of(content: String) -> Digest? { + match sha256sum_stdin_digest_via_shell(content: content) { + Sha256FileDigest { digest: d } => Present { value: d } + Sha256FileDigestUnavailable { path: _, reason: _ } => none + } +} + +test fn one_changed_byte_changes_the_receipt_digest_by_real_execution() -> Bool { + match digest_of(content: "{\"schema\":\"gunbc.boot_attempt_receipt.v1\"}") { + Absent => false + Present { value: a } => + match digest_of(content: "{\"schema\":\"gunbc.boot_attempt_receipt.v2\"}") { + Absent => false + Present { value: b } => + match digest_of(content: "{\"schema\":\"gunbc.boot_attempt_receipt.v1\"}") { + Absent => false + Present { value: a2 } => (a.hex as String) != (b.hex as String) && (a.hex as String) == (a2.hex as String) + } + } + } +} diff --git a/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag b/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag new file mode 100644 index 00000000000..45e33077920 --- /dev/null +++ b/dag/test/claim/host/host_boot_attempt_admission_witness_test.dag @@ -0,0 +1,337 @@ +module test.claim.host_boot_attempt_admission_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { Bool, Int, List, NonEmptyStr, String } +import v2.std.optional { Present, Absent } +import extdeps.crypto.hash { sha256_digest } +import extdeps.tools.sha256sum { Sha256FileDigest, Sha256FileDigestUnavailable } +import extdeps.ampere.mt_collins_getting_started_guide.dimm_layout { dimm_figure_banks } +import product.placement_supply { HostIdentity } +import gunbc.fleet_intent_network { operator_host_mtcollins1 } +import gunbc.machine_intake_mtcollins1_power_on_account { + ExpectedSockets, ExpectedTopologyNotRecorded, StimulusRequested, NoStimulusRequested, StimulusRequestNotRecorded, + StimulusAppliedByReceipt, StimulusApplicationNotRecorded, PopulationOperatorAttested, PopulationNotRecorded, + PopulationLiveObserved, PopulationConflicted, +} +import gunbc.host_boot_attempt_admission { + AttemptReceiptRefusal, ReceiptValidation, ReceiptValidated, ReceiptRefused, + ReceiptHostHasNoRoute, ReceiptExecutorForAnotherHost, ReceiptExecutorNotOnStoreHost, ReceiptHostUnbound, ReceiptNonceMissing, ReceiptNonceNotSlotSafe, ReceiptHostNotSlotSafe, + ReceiptPathOutsideReceipts, ReceiptFileUnreadable, ReceiptNotJson, ReceiptSchemaMismatch, + ReceiptFieldUnreadable, ReceiptTimeUnreadable, ReceiptSubjectMismatch, ReceiptAttemptMismatch, ReceiptPlanMismatch, + ReceiptOrderingViolated, AttemptAlreadyConsumed, AttemptSlotKeyNotAddressable, AttemptSlotPreconditionIncoherent, AttemptSlotStoreRefused, + ConfigurationReceiptNotNamed, ConfigurationReceiptAdmitted, + validate_attempt_receipt, named_receipt_validation, attempt_slot_key, attempt_configuration_receipt_of, + RosterSlot, mt_collins_slot_roster, tracked_entry_refusal, + ReceiptNotTracked, ReceiptNotRegularFile, ReceiptDigestUnavailable, + ReceiptCpusNotTheExpectedSockets, ReceiptDimmUnknownSlot, ReceiptDimmOnWrongSocket, ReceiptDimmSlotOmitted, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE SUBJECT IS THE VALIDATION FOLD AT ITS INTERFACE: each claim supplies the one file read the +// fold is handed and asserts the typed answer. The real read and the slot are exercised by +// test.claim.host_boot_attempt_admission_wet_witness. +fn q(s: String) -> String { + concat(concat("\"", s), "\"") +} + +fn receipt_text(subject: String, attempt: String, plan_subject: String, plan_attempt: String, requested: String, fixed_at: String, completed_at: String) -> String { + receipt_text_with(subject: subject, attempt: attempt, plan_subject: plan_subject, plan_attempt: plan_attempt, requested: requested, fixed_at: fixed_at, completed_at: completed_at, cpus: cpus_json(sockets: [0, 1]), dimms: dimms_json(rows: [dimm(label: "J1", socket: 0), dimm(label: "J25", socket: 1)])) +} + +fn receipt_text_with(subject: String, attempt: String, plan_subject: String, plan_attempt: String, requested: String, fixed_at: String, completed_at: String, cpus: String, dimms: String) -> String { + join([ + "{", q(s: "schema"), ":", q(s: "gunbc.boot_attempt_receipt.v1"), ",", + q(s: "plan"), ":{", q(s: "subject"), ":", q(s: subject), ",", q(s: "attempt"), ":", q(s: attempt), ",", + q(s: "expected_sockets"), ":[0,1],", q(s: "requested"), ":", requested, ",", + q(s: "fixed_at"), ":", q(s: fixed_at), ",", q(s: "fixed_by"), ":", q(s: "eager-gull-22"), "},", + q(s: "inspection"), ":{", q(s: "plan_subject"), ":", q(s: plan_subject), ",", q(s: "plan_attempt"), ":", q(s: plan_attempt), ",", + q(s: "applied"), ":", q(s: "socket 1 CPU reseated"), ",", + q(s: "cpus"), ":", cpus, ",", + q(s: "dimms"), ":", dimms, ",", + q(s: "completed_at"), ":", q(s: completed_at), ",", q(s: "witnessed_by"), ":", q(s: "operator"), "}}", + ], "") +} + +fn cpus_json(sockets: List) -> String { + concat(concat("[", join(map(sockets, k => join(["{", q(s: "socket"), ":", to_string(k), ",", q(s: "installed"), ":true}"], "")), ",")), "]") +} + +type DimmFixture { + label: String + socket: Int +} + +fn dimm(label: String, socket: Int) -> DimmFixture { + DimmFixture { label: label, socket: socket } +} + +fn dimms_json(rows: List) -> String { + concat(concat("[", join(map(rows, r => join(["{", q(s: "label"), ":", q(s: r.label), ",", q(s: "socket"), ":", to_string(r.socket), ",", q(s: "populated"), ":true}"], "")), ",")), "]") +} + +// A TWO-SLOT ROSTER keeps each claim's parse small; one claim below joins the real 32-connector roster. +fn small_roster() -> List { + [RosterSlot { label: "J1", socket: 0 }, RosterSlot { label: "J25", socket: 1 }] +} + +fn a_digest() -> Sha256FileDigest { + Sha256FileDigest { digest: sha256_digest(hex: "689624b261a32784a3a7d0373b1f05cfd7a46c1cff63e1ff761736cd9184a590") } +} + +data path: NonEmptyStr = "artifacts/receipts/mtcollins1-n42.json" + +fn valid_text() -> String { + receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: q(s: "reseat socket 1 CPU"), fixed_at: "2026-10-04T05:00:00Z", completed_at: "2026-10-04T05:30:00Z") +} + +fn validate(text: String, nonce: NonEmptyStr) -> ReceiptValidation { + validate_attempt_receipt(subject: operator_host_mtcollins1, nonce: nonce, path: path, commit: "0123abc", slots: small_roster(), content: text, digest: a_digest()) +} + +fn refused_with(v: ReceiptValidation) -> AttemptReceiptRefusal? { + match v { + ReceiptRefused { cause: c } => Present { value: c } + ReceiptValidated { receipt: _ } => none + } +} + +fn refusal_tag(cause: AttemptReceiptRefusal) -> String { + match cause { + ReceiptHostHasNoRoute { host: _ } => "ReceiptHostHasNoRoute" + ReceiptExecutorForAnotherHost { executor_host: _, bound: _ } => "ReceiptExecutorForAnotherHost" + ReceiptExecutorNotOnStoreHost { reason: _ } => "ReceiptExecutorNotOnStoreHost" + ReceiptHostUnbound { detail: _ } => "ReceiptHostUnbound" + ReceiptNonceMissing { variable: _, detail: _ } => "ReceiptNonceMissing" + ReceiptNonceNotSlotSafe { nonce: _ } => "ReceiptNonceNotSlotSafe" + ReceiptHostNotSlotSafe { host: _ } => "ReceiptHostNotSlotSafe" + ReceiptPathOutsideReceipts { path: _ } => "ReceiptPathOutsideReceipts" + ReceiptNotTracked { path: _, commit: _ } => "ReceiptNotTracked" + ReceiptNotRegularFile { path: _, mode: _, kind: _ } => "ReceiptNotRegularFile" + ReceiptDigestUnavailable { path: _, reason: _ } => "ReceiptDigestUnavailable" + ReceiptCpusNotTheExpectedSockets { expected: _, recorded: _ } => "ReceiptCpusNotTheExpectedSockets" + ReceiptDimmUnknownSlot { label: _ } => "ReceiptDimmUnknownSlot" + ReceiptDimmOnWrongSocket { label: _, recorded: _, roster: _ } => "ReceiptDimmOnWrongSocket" + ReceiptDimmSlotOmitted { label: _ } => "ReceiptDimmSlotOmitted" + ReceiptFileUnreadable { path: _, detail: _ } => "ReceiptFileUnreadable" + ReceiptNotJson { path: _, detail: _ } => "ReceiptNotJson" + ReceiptSchemaMismatch { observed: _ } => "ReceiptSchemaMismatch" + ReceiptFieldUnreadable { field: _, cause: _ } => "ReceiptFieldUnreadable" + ReceiptTimeUnreadable { field: _, rendering: _ } => "ReceiptTimeUnreadable" + ReceiptSubjectMismatch { receipt: _, bound: _ } => "ReceiptSubjectMismatch" + ReceiptAttemptMismatch { receipt: _, dispatched: _ } => "ReceiptAttemptMismatch" + ReceiptPlanMismatch { field: _, plan: _, inspection: _ } => "ReceiptPlanMismatch" + ReceiptOrderingViolated { fixed_at: _, completed_at: _ } => "ReceiptOrderingViolated" + AttemptAlreadyConsumed { slot: _, consumed_by: _ } => "AttemptAlreadyConsumed" + AttemptSlotKeyNotAddressable { slot: _ } => "AttemptSlotKeyNotAddressable" + AttemptSlotPreconditionIncoherent { slot: _ } => "AttemptSlotPreconditionIncoherent" + AttemptSlotStoreRefused { slot: _, cause: _ } => "AttemptSlotStoreRefused" + } +} + +fn refusal_detail(cause: AttemptReceiptRefusal) -> String { + match cause { + ReceiptHostHasNoRoute { host: h } => h as String + ReceiptExecutorForAnotherHost { executor_host: e, bound: b } => join([e as String, b as String], "|") + ReceiptExecutorNotOnStoreHost { reason: r } => r as String + ReceiptHostUnbound { detail: d } => d as String + ReceiptNonceMissing { variable: v, detail: d } => join([v as String, d], "|") + ReceiptNonceNotSlotSafe { nonce: n } => n as String + ReceiptHostNotSlotSafe { host: h } => h as String + ReceiptPathOutsideReceipts { path: x } => x as String + ReceiptNotTracked { path: x, commit: c } => join([x as String, c as String], "|") + ReceiptNotRegularFile { path: x, mode: m, kind: k } => join([x as String, m, k], "|") + ReceiptDigestUnavailable { path: x, reason: r } => join([x as String, r], "|") + ReceiptCpusNotTheExpectedSockets { expected: e, recorded: r } => join([join(map(e, k => to_string(k)), ","), join(map(r, k => to_string(k)), ",")], "|") + ReceiptDimmUnknownSlot { label: l } => l as String + ReceiptDimmOnWrongSocket { label: l, recorded: r, roster: k } => join([l as String, to_string(r), to_string(k)], "|") + ReceiptDimmSlotOmitted { label: l } => l as String + ReceiptFileUnreadable { path: x, detail: d } => join([x as String, d], "|") + ReceiptNotJson { path: x, detail: d } => join([x as String, d], "|") + ReceiptSchemaMismatch { observed: o } => o + ReceiptFieldUnreadable { field: f, cause: _ } => f as String + ReceiptTimeUnreadable { field: f, rendering: r } => join([f as String, r], "|") + ReceiptSubjectMismatch { receipt: r, bound: b } => join([r, b as String], "|") + ReceiptAttemptMismatch { receipt: r, dispatched: d } => join([r, d as String], "|") + ReceiptPlanMismatch { field: f, plan: x, inspection: i } => join([f as String, x, i], "|") + ReceiptOrderingViolated { fixed_at: a, completed_at: b } => join([a as String, b as String], "|") + AttemptAlreadyConsumed { slot: k, consumed_by: c2 } => join([k as String, c2], "|") + AttemptSlotKeyNotAddressable { slot: k } => k as String + AttemptSlotPreconditionIncoherent { slot: k } => k as String + AttemptSlotStoreRefused { slot: k, cause: _ } => k as String + } +} + +// ── THE POSITIVE CONTROL: a valid receipt projects into the account's operator-attested fields ─── +test fn w_a_valid_receipt_projects_its_plan_and_inspection_into_the_attempt_configuration() -> Bool { + match validate(text: valid_text(), nonce: "n42") { + ReceiptRefused { cause: _ } => false + ReceiptValidated { receipt: r } => { + let projected = attempt_configuration_receipt_of(host: operator_host_mtcollins1, source: ConfigurationReceiptAdmitted { receipt: r, slot: "attempt-10-mtcollins1-n42" }, attempt: "run-1") + let expected_ok = match projected.expected { ExpectedSockets { sockets: ks, source: _ } => ks.length() == 2 ExpectedTopologyNotRecorded { reason: _ } => false } + let requested_ok = match projected.requested { StimulusRequested { description: d } => (d as String) == "reseat socket 1 CPU" NoStimulusRequested => false StimulusRequestNotRecorded { reason: _ } => false } + let applied_ok = match projected.applied { StimulusAppliedByReceipt { receipt: _, attested_by: a } => (a as String) == "operator" StimulusApplicationNotRecorded { reason: _ } => false } + let cpus_ok = match projected.cpus { + PopulationOperatorAttested { rows: rs, receipt: rc } => rs.length() == 2 && string_contains(s: rc as String, pattern: "artifacts/receipts/mtcollins1-n42.json@0123abc") + PopulationLiveObserved { rows: _, source: _ } => false + PopulationConflicted { readings: _ } => false + PopulationNotRecorded { reason: _ } => false + } + expected_ok && requested_ok && applied_ok && cpus_ok && (projected.attempt as String) == "n42" + } + } +} + +test fn w_an_explicit_null_request_is_no_stimulus_and_a_missing_one_refuses() -> Bool { + let null_text = receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: "null", fixed_at: "2026-10-04T05:00:00Z", completed_at: "2026-10-04T05:30:00Z") + let null_ok = match validate(text: null_text, nonce: "n42") { + ReceiptValidated { receipt: r } => match r.plan.requested { NoStimulusRequested => true StimulusRequested { description: _ } => false StimulusRequestNotRecorded { reason: _ } => false } + ReceiptRefused { cause: _ } => false + } + let missing_text = replace(s: valid_text(), from: concat(q(s: "requested"), ":"), to: concat(q(s: "requested_by_nobody"), ":")) + let missing_ok = match refused_with(v: validate(text: missing_text, nonce: "n42")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptFieldUnreadable" && refusal_detail(cause: c) == "requested" + Absent => false + } + null_ok && missing_ok +} + +// ── THE ATTEMPT BINDING: a valid receipt for attempt A, dispatched as attempt B, refuses ───────── +test fn w_a_valid_receipt_for_another_attempt_refuses() -> Bool { + match refused_with(v: validate(text: valid_text(), nonce: "n43")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptAttemptMismatch" && refusal_detail(cause: c) == "n42|n43" + Absent => false + } +} + +test fn w_a_receipt_for_another_host_refuses() -> Bool { + let other = receipt_text(subject: "mtjade1", attempt: "n42", plan_subject: "mtjade1", plan_attempt: "n42", requested: "null", fixed_at: "2026-10-04T05:00:00Z", completed_at: "2026-10-04T05:30:00Z") + match refused_with(v: validate(text: other, nonce: "n42")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptSubjectMismatch" && refusal_detail(cause: c) == "mtjade1|mtcollins1" + Absent => false + } +} + +test fn w_an_inspection_naming_another_plan_refuses() -> Bool { + let crossed = receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n41", requested: "null", fixed_at: "2026-10-04T05:00:00Z", completed_at: "2026-10-04T05:30:00Z") + match refused_with(v: validate(text: crossed, nonce: "n42")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptPlanMismatch" && refusal_detail(cause: c) == "attempt|n42|n41" + Absent => false + } +} + +// ── THE ATTESTED TIMES: ordered only against each other, and only in the admitted shape ────────── +test fn w_an_inspection_attested_before_its_plan_refuses_and_an_unshaped_time_refuses() -> Bool { + let early = receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: "null", fixed_at: "2026-10-04T05:00:00Z", completed_at: "2026-10-04T04:59:59Z") + let early_ok = match refused_with(v: validate(text: early, nonce: "n42")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptOrderingViolated" && refusal_detail(cause: c) == "2026-10-04T05:00:00Z|2026-10-04T04:59:59Z" + Absent => false + } + let local = receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: "null", fixed_at: "2026-10-04 05:00", completed_at: "2026-10-04T05:30:00Z") + let shape_ok = match refused_with(v: validate(text: local, nonce: "n42")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptTimeUnreadable" && refusal_detail(cause: c) == "fixed_at|2026-10-04 05:00" + Absent => false + } + early_ok && shape_ok +} + +// ── THE FILE: malformed and absent both refuse, never NotRecorded ─────────────────────────────── +test fn w_a_named_receipt_that_is_malformed_or_undigested_refuses() -> Bool { + let malformed_ok = match refused_with(v: validate(text: "{\"schema\":", nonce: "n42")) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptNotJson" + Absent => false + } + let undigested_ok = match refused_with(v: validate_attempt_receipt(subject: operator_host_mtcollins1, nonce: "n42", path: path, commit: "0123abc", slots: small_roster(), content: valid_text(), digest: Sha256FileDigestUnavailable { path: "-", reason: "sha256sum could not digest the input" })) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptDigestUnavailable" + Absent => false + } + malformed_ok && undigested_ok +} + +// ── BEFORE ANY READ: a nonce or path outside the admitted shape refuses ───────────────────────── +test fn w_an_unsafe_nonce_or_a_path_outside_receipts_refuses_before_the_file_is_read() -> Bool { + let nonce_ok = match refused_with(v: named_receipt_validation(host: operator_host_mtcollins1, nonce: "n42/../x", path: path as String, revision: "0123abc", slots: small_roster())) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptNonceNotSlotSafe" + Absent => false + } + let path_ok = match refused_with(v: named_receipt_validation(host: operator_host_mtcollins1, nonce: "n42", path: "artifacts/receipts/../../etc/passwd.json", revision: "0123abc", slots: small_roster())) { + Present { value: c } => refusal_tag(cause: c) == "ReceiptPathOutsideReceipts" + Absent => false + } + nonce_ok && path_ok +} + +// ── THE SLOT KEY IS INJECTIVE: the length prefix separates hosts whose labels share a prefix ───── +test fn w_two_host_and_nonce_pairs_that_concatenate_alike_get_distinct_slots() -> Bool { + let a = attempt_slot_key(host: "ab" as HostIdentity, nonce: "c-d") + let b = attempt_slot_key(host: "ab-c" as HostIdentity, nonce: "d") + (a as String) != (b as String) && (a as String) == "attempt-2-ab-c-d" && !string_contains(s: a as String, pattern: ".") && !string_contains(s: a as String, pattern: "/") +} + +// ── ABSENT IS NOT REFUSED: a dispatch that names no receipt records nothing and judges nothing ─── +test fn w_no_named_receipt_leaves_every_field_not_recorded() -> Bool { + let projected = attempt_configuration_receipt_of(host: operator_host_mtcollins1, source: ConfigurationReceiptNotNamed, attempt: "run-1") + let expected_ok = match projected.expected { ExpectedTopologyNotRecorded { reason: r } => string_contains(s: r as String, pattern: "boot_attempt_configuration_inspection") ExpectedSockets { sockets: _, source: _ } => false } + let cpus_ok = match projected.cpus { + PopulationNotRecorded { reason: _ } => true + PopulationOperatorAttested { rows: _, receipt: _ } => false + PopulationLiveObserved { rows: _, source: _ } => false + PopulationConflicted { readings: _ } => false + } + expected_ok && cpus_ok && (projected.attempt as String) == "run-1" +} + +// ── THE TRACKED BLOB: only a regular file tracked at the revision can be a receipt ─────────────── +fn tab() -> String { from_code_point(9) } +fn nul() -> String { from_code_point(0) } + +fn refusal_tag_of(c: AttemptReceiptRefusal?) -> String { + match c { + Present { value: x } => refusal_tag(cause: x) + Absent => "none" + } +} + +test fn w_only_a_regular_tracked_blob_at_the_revision_is_a_receipt() -> Bool { + let regular = refusal_tag_of(c: tracked_entry_refusal(path: path, commit: "0123abc", entries_nul: join(["100644 blob 1111111111111111111111111111111111111111", tab(), path as String, nul()], ""))) + let symlink = refusal_tag_of(c: tracked_entry_refusal(path: path, commit: "0123abc", entries_nul: join(["120000 blob 2222222222222222222222222222222222222222", tab(), path as String, nul()], ""))) + let untracked = refusal_tag_of(c: tracked_entry_refusal(path: path, commit: "0123abc", entries_nul: "")) + regular == "none" && symlink == "ReceiptNotRegularFile" && untracked == "ReceiptNotTracked" +} + +// ── THE ATTESTED TIMES ARE CANONICAL UTC INSTANTS (gunbc.auth.approval_capability) ─────────────── +fn with_fixed_at(t: String) -> String { + refusal_tag_of(c: refused_with(v: validate(text: receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: "null", fixed_at: t, completed_at: "2026-10-04T05:30:00Z"), nonce: "n42"))) +} + +test fn w_an_impossible_calendar_time_refuses_and_equal_instants_are_admitted() -> Bool { + let equal = receipt_text(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: "null", fixed_at: "2026-10-04T05:30:00Z", completed_at: "2026-10-04T05:30:00Z") + with_fixed_at(t: "2026-99-04T05:00:00Z") == "ReceiptTimeUnreadable" + && with_fixed_at(t: "2026-02-30T05:00:00Z") == "ReceiptTimeUnreadable" + && with_fixed_at(t: "2026-10-04T24:00:00Z") == "ReceiptTimeUnreadable" + && refusal_tag_of(c: refused_with(v: validate(text: equal, nonce: "n42"))) == "none" +} + +// ── THE POPULATIONS JOIN EXACTLY: expected sockets, and the host's slot roster ─────────────────── +fn with_rows(cpus: List, dimms: List) -> String { + refusal_tag_of(c: refused_with(v: validate(text: receipt_text_with(subject: "mtcollins1", attempt: "n42", plan_subject: "mtcollins1", plan_attempt: "n42", requested: "null", fixed_at: "2026-10-04T05:00:00Z", completed_at: "2026-10-04T05:30:00Z", cpus: cpus_json(sockets: cpus), dimms: dimms_json(rows: dimms)), nonce: "n42"))) +} + +test fn w_a_population_that_does_not_join_its_roster_refuses() -> Bool { + let full = [dimm(label: "J1", socket: 0), dimm(label: "J25", socket: 1)] + with_rows(cpus: [0], dimms: full) == "ReceiptCpusNotTheExpectedSockets" + && with_rows(cpus: [0, 1], dimms: [dimm(label: "J1", socket: 0), dimm(label: "25", socket: 1)]) == "ReceiptDimmUnknownSlot" + && with_rows(cpus: [0, 1], dimms: [dimm(label: "J1", socket: 0), dimm(label: "J25", socket: 0)]) == "ReceiptDimmOnWrongSocket" + && with_rows(cpus: [0, 1], dimms: [dimm(label: "J1", socket: 0)]) == "ReceiptDimmSlotOmitted" + && with_rows(cpus: [0, 1], dimms: full) == "none" +} + +// THE REAL ROSTER: 32 connectors, J1-J16 on socket 0 and J17-J32 on socket 1, from the guide's Figure 9. +test fn w_the_mt_collins_roster_is_the_guides_32_connectors_by_socket() -> Bool { + let roster = mt_collins_slot_roster(banks: dimm_figure_banks) + count(roster) == 32 + && count(filter(roster, r => r.socket == 0)) == 16 + && any(roster, r => (r.label as String) == "J25" && r.socket == 1) + && any(roster, r => (r.label as String) == "J16" && r.socket == 0) + && !any(roster, r => (r.label as String) == "25") +} diff --git a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag index c9c8c227d6d..0084df56d19 100644 --- a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag +++ b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag @@ -896,3 +896,26 @@ test fn a_foreign_presented_image_is_not_stopped() -> Bool { _ => false } } + +// A NAMED RECEIPT THAT REFUSES READS NOTHING FROM THE CONTROLLER AND WRITES NOTHING: admission +// (gunbc.host_boot_attempt_admission) runs under the unit hold and before the SDR/SEL baseline, so a +// receipt path outside artifacts/receipts/ refuses before any BMC read or power action. +fn with_named_receipt(w: MtCollins1BootWorld, path: String, nonce: String) -> MtCollins1BootWorld { + MtCollins1BootWorld { + bmc: w.bmc, fs: w.fs, + environment: concat(w.environment, [ModeledVariable { name: "GUNBC_BOOT_ATTEMPT_RECEIPT", value: path }, ModeledVariable { name: "GUNBC_BOOT_ATTEMPT_NONCE", value: nonce }]), + agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media, screen: w.screen, + } +} + +test fn a_refused_named_receipt_reads_no_baseline_and_writes_nothing() -> Bool { + match run_attempt(world: with_named_receipt(w: world_with_console(lines: console_of(capture: one_socket_census_capture, begin_after: 60, end_after: 240)), path: "artifacts/receipts/../escape.json", nonce: "n1")) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "attempt receipt refused") + && count_named(route: route, name: "diagnostic.ipmi.Tool.SdrDumpAuthenticated") == 0 + && count_named(route: route, name: "diagnostic.ipmi.Tool.SelListAuthenticated") == 0 + && count_named(route: route, name: "diagnostic.ipmi.Tool.SelListAuthenticatedCached") == 0 + && reached_no_power_action(route: route) + _ => false + } +} diff --git a/dag/test/claim/machine_intake/mtcollins1_boot_diagnostic_bundle_witness_test.dag b/dag/test/claim/machine_intake/mtcollins1_boot_diagnostic_bundle_witness_test.dag index 8a0623e185d..26e44c72802 100644 --- a/dag/test/claim/machine_intake/mtcollins1_boot_diagnostic_bundle_witness_test.dag +++ b/dag/test/claim/machine_intake/mtcollins1_boot_diagnostic_bundle_witness_test.dag @@ -5,6 +5,7 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.types { Bool, Int, List, NonEmptyStr, String } import std.goal_assessment { ObservationEstablished, ObservationRefused } import std.process { ExitSuccess, ExitFailure, exit_failure } +import gunbc.host_boot_attempt_admission { attempt_configuration_not_recorded } import v2.std.optional { Present } import extdeps.bmc.redfish_memory_inventory { RedfishMemoryMember, RedfishProcessorMember, StateAbsent, StateEnabled, StateUnrecognized, HealthOk, HealthCritical, @@ -29,7 +30,7 @@ import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle { SdrCacheDumped, SdrCacheUnread, SdrCacheNotTaken, SensorsRead, SensorsNotTaken, SmproProbed, SmproNotTaken, SmproReading, BmcUnreachable, BmcTimeout, BmcAuthRefused, BmcHttpRefused, BmcSessionUnestablished, bmc_curl_read_cause, bmc_ipmitool_read_cause, inventory_not_taken, - mtcollins1_boot_findings, harness_finding_text, processor_anomalies, memory_anomalies, mtcollins1_attempt_configuration_receipt, mtcollins1_boot_bundle_text, mtcollins1_boot_outcome_with_findings, + mtcollins1_boot_findings, harness_finding_text, processor_anomalies, memory_anomalies, mtcollins1_boot_bundle_text, mtcollins1_boot_outcome_with_findings, mtcollins1_boot_console_reading, ReferenceCaptureRead, ConsoleRetained, ConsoleNotRetained, ConsoleExceedsBound, mtcollins1_boot_console_bound, AttemptRunId, AttemptIdentityUnavailable, BmcDeadlineReached, BmcCollectionIncomplete, CollectionComplete, CollectionRefused, redfish_collection_assembly, redfish_budget_refusal, member_not_reached, @@ -118,7 +119,7 @@ fn no_run() -> MtCollins1BootRunRecord { } fn bundle_socket1_absent() -> MtCollins1BootDiagnosticBundle { - MtCollins1BootDiagnosticBundle { + MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptRunId { run_id: "35793279839" }, outcome: "refused: mtcollins1 boot: host qualification REFUSED (nproc observed 80, qualification expects 160)", sel_before: SelSnapshotRead { raw: sel_before_fixture, at: "2026-09-23T00:59:00Z" }, @@ -141,7 +142,7 @@ fn bundle_socket1_absent() -> MtCollins1BootDiagnosticBundle { fn bundle_bmc_silent() -> MtCollins1BootDiagnosticBundle { let cause = bmc_curl_read_cause(endpoint: "https://192.168.1.228/redfish/v1/Systems", at: "2026-09-23T01:10:00Z", exit_code: 7, stderr: "curl: (7) Failed to connect to 192.168.1.228 port 443: Couldn't connect to server") let ipmi = bmc_ipmitool_read_cause(endpoint: "ipmi lanplus 192.168.1.228", at: "2026-09-23T00:59:00Z", exit_code: 1, stderr: "Error: Unable to establish IPMI v2 / RMCP+ session") - MtCollins1BootDiagnosticBundle { + MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptRunId { run_id: "35800000000" }, outcome: "refused: mtcollins1 boot: approval window expired; controller untouched", sel_before: SelSnapshotUnread { cause: ipmi }, @@ -278,7 +279,7 @@ test fn a_link_is_used_exactly_or_refused_never_rebuilt() -> Bool { test fn an_incomplete_memory_collection_mints_no_short_inventory_finding() -> Bool { let cause = BmcCollectionIncomplete { endpoint: "https://192.168.1.228/redfish/v1/Systems/Self/Memory", at: "2026-09-23T01:00:00Z", detail: "Members@odata.nextLink not followed" } let b = bundle_socket1_absent() - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: InventoryReading { system_id: "/redfish/v1/Systems/Self", memory: MembersUnread { cause: cause }, processors: b.inventory.processors, credential_removed: true }, console: ConsoleNotConfigured, run: no_run(), screen: no_screen() } !any_contains(xs: found(bundle: bundle), pattern: "Memory member(s); the board has") @@ -306,7 +307,7 @@ test fn a_spent_budget_refuses_the_read_and_names_what_was_not_reached() -> Bool test fn a_partial_bundle_renders_the_reads_not_reached() -> Bool { let b = bundle_socket1_absent() let cause = BmcDeadlineReached { endpoint: "https://192.168.1.228/redfish/v1/Systems/Self/Memory/DIMM_20", at: "t", not_reached: member_not_reached(total: 32, read: 20) } - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: InventoryReading { system_id: "/redfish/v1/Systems/Self", memory: MembersUnread { cause: cause }, processors: b.inventory.processors, credential_removed: true }, console: ConsoleNotConfigured, run: no_run(), screen: no_screen() } contains(mtcollins1_boot_bundle_text(bundle: bundle), "memory: UNREAD: diagnostics read budget spent before https://192.168.1.228/redfish/v1/Systems/Self/Memory/DIMM_20 (t); not reached: 12 of 32 member read(s)") @@ -362,8 +363,14 @@ test fn with_no_recorded_topology_a_missing_processor_is_a_question_not_a_shortf !any_contains(xs: f, pattern: "Processor member(s);") && any_contains(xs: f, pattern: "the expected topology was not recorded for this attempt") } +// A BUNDLE WHOSE ATTEMPT NAMED NO RECEIPT: the configuration gunbc.host_boot_attempt_admission +// projects then, every field not recorded. +fn no_receipt_configuration() -> AttemptConfigurationReceipt { + attempt_configuration_not_recorded(host: "mtcollins1", attempt: "witness", reason: "the witness attempt named no attempt receipt") +} + fn expecting_two_sockets() -> AttemptConfigurationReceipt { - let r = mtcollins1_attempt_configuration_receipt(attempt: AttemptRunId { run_id: "witness" }) + let r = no_receipt_configuration() AttemptConfigurationReceipt { subject: r.subject, attempt: r.attempt, expected: ExpectedSockets { sockets: [0, 1], source: "witness" }, requested: r.requested, applied: r.applied, cpus: r.cpus, dimms: r.dimms, firmware: r.firmware } } @@ -391,7 +398,7 @@ test fn two_members_both_on_socket_0_leave_socket_1_missing_and_socket_0_duplica // (nothing recorded) the socket-1 member reading Absent mints nothing; a receipt recording that slot // populated makes it an anomaly, and one recording it unpopulated does not. fn receipt_with_rows(rows: List) -> AttemptConfigurationReceipt { - let r = mtcollins1_attempt_configuration_receipt(attempt: AttemptRunId { run_id: "witness" }) + let r = no_receipt_configuration() AttemptConfigurationReceipt { subject: r.subject, attempt: r.attempt, expected: r.expected, requested: r.requested, applied: r.applied, cpus: r.cpus, dimms: PopulationOperatorAttested { rows: rows, receipt: "witness inspection" }, firmware: r.firmware } } @@ -448,7 +455,7 @@ test fn an_ambiguous_ipmi_failure_is_not_rendered_as_did_not_answer() -> Bool { test fn only_definitive_no_answers_say_the_bmc_did_not_answer() -> Bool { let b = bundle_bmc_silent() let timeout = bmc_ipmitool_read_cause(endpoint: "ipmi lanplus 192.168.1.228", at: "2026-09-23T00:59:00Z", exit_code: 124, stderr: "") - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: SelSnapshotUnread { cause: timeout }, sel_after: SelSnapshotUnread { cause: timeout }, sdr_cache: SdrCacheUnread { cause: timeout }, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: SelSnapshotUnread { cause: timeout }, sel_after: SelSnapshotUnread { cause: timeout }, sdr_cache: SdrCacheUnread { cause: timeout }, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } any_contains(xs: found(bundle: bundle), pattern: "every BMC read failed and the BMC did not answer; first: BMC timed out at ipmi lanplus 192.168.1.228") } @@ -458,7 +465,7 @@ test fn only_definitive_no_answers_say_the_bmc_did_not_answer() -> Bool { test fn a_bmc_that_answered_on_the_sensor_channel_is_not_all_failed() -> Bool { let b = bundle_bmc_silent() let good = bundle_socket1_absent() - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: good.sdr_cache, sensors: good.sensors, smpro: b.smpro, inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } let findings = found(bundle: bundle) !any_contains(xs: findings, pattern: "every BMC read failed") @@ -488,7 +495,7 @@ test fn a_silent_bmc_still_renders_every_section_with_its_cause() -> Bool { // an arm where nothing was read. test fn a_bundle_from_an_attempt_that_never_reached_the_bmc_names_why_in_every_section() -> Bool { let why: NonEmptyStr = "the attempt ended before the BMC credential was read (refused: mtcollins1 boot: approval window expired; controller untouched)" - let bundle = MtCollins1BootDiagnosticBundle { + let bundle = MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptRunId { run_id: "1" }, outcome: "refused: mtcollins1 boot: approval window expired; controller untouched", sel_before: SelSnapshotNotTaken { reason: why }, @@ -560,7 +567,7 @@ test fn a_missing_run_id_is_a_typed_unavailable_identity_not_a_blank() -> Bool { test fn the_unavailable_identity_is_rendered_as_such() -> Bool { let b = bundle_bmc_silent() - let bundle = MtCollins1BootDiagnosticBundle { attempt: AttemptIdentityUnavailable { variable: "GITHUB_RUN_ID", detail: "not set" }, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } + let bundle = MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptIdentityUnavailable { variable: "GITHUB_RUN_ID", detail: "not set" }, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } contains(mtcollins1_boot_bundle_text(bundle: bundle), "attempt=UNAVAILABLE: GITHUB_RUN_ID could not be read: not set") } @@ -568,7 +575,7 @@ test fn the_unavailable_identity_is_rendered_as_such() -> Bool { // (mtcollins1_boot_console_reading -> ampere_dram_console_observation -> bundle findings). test fn an_empty_dram_socket_in_the_console_reaches_the_refusal() -> Bool { let capture = "NOTICE: DRAM FW version 210525\r\nMEMC param:\r\n mcu_enable_mask = 00000011 [default: 000000ff]\r\nDRAM populated DIMMs:\r\n SK0 MC0 S0: RDIMM[ad:80] 16GB 2666 ECC 1R x4 RCD[b3:80] HMA82GR7AFR4N-VK \r\nCP: 3ff00100\r\n" - let bundle = MtCollins1BootDiagnosticBundle { + let bundle = MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptRunId { run_id: "35801475989" }, outcome: "refused: x", sel_before: SelSnapshotNotTaken { reason: "t" }, @@ -621,7 +628,7 @@ test fn an_unread_sensor_section_says_why() -> Bool { test fn a_one_socket_firmware_summary_reaches_the_refusal() -> Bool { let capture = "UEFI RC version: 1.08\r\n Number of active sockets : 1\r\n Number of active cores : 80\r\n Socket[0]: Core voltage : 1065\r\n[ 0.08] {2}[Hardware Error]: Hardware error from APEI Generic Hardware Error Source: 2\r\n[ 0.08] {2}[Hardware Error]: event severity: info\r\n[ 0.08] {2}[Hardware Error]: section type: unknown, e8ed898d-df16-43cc-8ecc-54f060ef157f\r\n[ 0.08] {2}[Hardware Error]: 00000000: 000003ce 22440074 00000000 00000000 ....t.D\"........\r\n" let b = bundle_socket1_absent() - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: mtcollins1_boot_console_reading(path: "artifacts/mtcollins1-boot-sol.capture", size: byte_size(count: 400), capture: capture, read_ok: true, read_error: "", capture_digest: unread_digest, reference: no_reference), run: no_run(), screen: no_screen() } let text = mtcollins1_boot_bundle_text(bundle: bundle) any_contains(found(bundle: bundle), "the expected topology was not recorded for this attempt") && !any_contains(found(bundle: bundle), "active socket(s), 2 expected") @@ -636,7 +643,7 @@ test fn a_supplied_reference_renders_its_differences() -> Bool { match mtcollins1_boot_console_reading(path: "artifacts/mtcollins1-boot-sol.capture", size: byte_size(count: 100), capture: capture, read_ok: true, read_error: "", capture_digest: unread_digest, reference: reference_of(text: reference)) { ConsoleRetained { path: _, size: _, lines: _, firmware: _, firmware_error_lines: _, capture_digest: _, dram: _, checkpoints: _, checkpoint_relations: _, milestones: _, sockets: _, against_reference: _, loader: _, linux: _, modules: _, nvparam: _, span_readings: _ } => { let b = bundle_socket1_absent() - let text = mtcollins1_boot_bundle_text(bundle: MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, + let text = mtcollins1_boot_bundle_text(bundle: MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: mtcollins1_boot_console_reading(path: "artifacts/mtcollins1-boot-sol.capture", size: byte_size(count: 100), capture: capture, read_ok: true, read_error: "", capture_digest: unread_digest, reference: reference_of(text: reference)), run: no_run(), screen: no_screen() }) contains(text, "3 difference(s)") && contains(text, "Socket[1] printed in the reference summary, absent from this boot's") && contains(text, "Inter Socket Connection 0 (reference: Width: x16 / Speed 25 GT/s) not printed by this boot") @@ -661,7 +668,7 @@ test fn a_socket_one_smpro_stage_reaches_the_refusal() -> Bool { smpro_probe_outcome(raw: smpro_raw(socket: 1, register: smpro_cur_bootstage_reg.name, exit_code: 0, stdout: "00 03", stderr: "")), smpro_probe_outcome(raw: smpro_raw(socket: 1, register: smpro_bootstage_reg.name, exit_code: 0, stdout: "03 03", stderr: "")), ] - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: smpro_probed(outcomes: outcomes), inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } (match mtcollins1_boot_outcome_with_findings(outcome: exit_failure(reason: "q"), findings: mtcollins1_boot_findings(bundle: bundle)) { ExitFailure { code: _, reason: r } => contains(r, "socket 1 SMpro reports a FAILED stage") && contains(r, "reported DDR initialization") @@ -674,7 +681,7 @@ test fn a_socket_one_smpro_stage_reaches_the_refusal() -> Bool { test fn an_smpro_nak_means_the_bmc_answered() -> Bool { let b = bundle_bmc_silent() let nak = smpro_probe_outcome(raw: smpro_raw(socket: 0, register: smpro_manufacturer_id_reg.name, exit_code: 1, stdout: "", stderr: "Unable to send RAW command (channel=0x0 netfn=0x6 lun=0x0 cmd=0x52 rsp=0x83): Unknown (0x83)")) - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: smpro_probed(outcomes: [nak]), inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } !any_contains(xs: found(bundle: bundle), pattern: "every BMC read failed") && any_contains(xs: found(bundle: bundle_bmc_silent()), pattern: "every BMC read failed") @@ -686,7 +693,7 @@ test fn an_smpro_nak_means_the_bmc_answered() -> Bool { test fn a_malformed_smpro_answer_means_the_bmc_answered() -> Bool { let b = bundle_bmc_silent() let bad = smpro_probe_outcome(raw: smpro_raw(socket: 0, register: smpro_manufacturer_id_reg.name, exit_code: 0, stdout: " cd\n", stderr: "")) - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: smpro_probed(outcomes: [bad]), inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } let findings = found(bundle: bundle) !any_contains(xs: findings, pattern: "every BMC read failed") && !any_contains(xs: findings, pattern: "did not answer") @@ -806,7 +813,7 @@ test fn a_negative_or_non_numeric_stat_size_is_no_size() -> Bool { test fn a_post_boot_sel_timeout_is_a_typed_after_section_and_moves_no_verdict() -> Bool { let b = bundle_socket1_absent() let timeout = bmc_ipmitool_read_cause(endpoint: "ipmi lanplus 192.168.1.228", at: "2026-09-23T15:12:43Z", exit_code: 124, stderr: "") - let bundle = MtCollins1BootDiagnosticBundle { attempt: AttemptRunId { run_id: "35871654468" }, outcome: "accepted", sel_before: b.sel_before, sel_after: SelSnapshotUnread { cause: timeout }, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: ConsoleNotConfigured, run: no_run(), screen: no_screen() } + let bundle = MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptRunId { run_id: "35871654468" }, outcome: "accepted", sel_before: b.sel_before, sel_after: SelSnapshotUnread { cause: timeout }, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: ConsoleNotConfigured, run: no_run(), screen: no_screen() } let text = mtcollins1_boot_bundle_text(bundle: bundle) let findings = mtcollins1_boot_findings(bundle: bundle) contains(text, "after: UNREAD: BMC timed out at ipmi lanplus 192.168.1.228 (2026-09-23T15:12:43Z): no answer within the diagnostics deadline (coreutils timeout exit 124)") @@ -932,7 +939,7 @@ data run_37069907299_firmware: String = "[SOL Session operational. Use ~? for h test fn the_real_route_binds_two_dram_spans_to_two_typed_cycles() -> Bool { let b = bundle_bmc_silent() - let bundle = MtCollins1BootDiagnosticBundle { attempt: AttemptRunId { run_id: "37069907299" }, outcome: b.outcome, + let bundle = MtCollins1BootDiagnosticBundle { configuration: no_receipt_configuration(), attempt: AttemptRunId { run_id: "37069907299" }, outcome: b.outcome, sel_before: SelSnapshotRead { raw: run_37069907299_sel_before, at: "2026-10-02T22:12:06Z" }, sel_after: SelSnapshotRead { raw: run_37069907299_sel_after, at: "2026-10-02T22:21:30Z" }, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: b.smpro, inventory: b.inventory, console: mtcollins1_boot_console_reading(path: "artifacts/mtcollins1-boot-sol.capture", size: byte_size(count: 3465), capture: run_37069907299_firmware, read_ok: true, read_error: "", capture_digest: unread_digest, reference: no_reference), @@ -955,7 +962,7 @@ test fn refused_error_registers_beside_a_read_stage_pair_are_their_own_coverage_ smpro_probe_outcome(raw: smpro_raw(socket: 0, register: smpro_gpi_ras_err_reg.name, exit_code: 1, stdout: "", stderr: nak)), smpro_probe_outcome(raw: smpro_raw(socket: 0, register: smpro_err_pmpro_type_reg.name, exit_code: 1, stdout: "", stderr: nak)), ] - let bundle = MtCollins1BootDiagnosticBundle { attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, + let bundle = MtCollins1BootDiagnosticBundle { configuration: b.configuration, attempt: b.attempt, outcome: b.outcome, sel_before: b.sel_before, sel_after: b.sel_after, sdr_cache: b.sdr_cache, sensors: b.sensors, smpro: smpro_probed(outcomes: outcomes), inventory: b.inventory, console: b.console, run: no_run(), screen: no_screen() } let cov = mtcollins1_boot_findings(bundle: bundle).account.coverage any(cov, c => (match c.carrier { SmproRegisters => true _ => false }) && (match c.standing { CarrierRead => true _ => false })) diff --git a/docs/plans/power-on-sequence-model.md b/docs/plans/power-on-sequence-model.md index c9e23c213b4..e713f9ae8ea 100644 --- a/docs/plans/power-on-sequence-model.md +++ b/docs/plans/power-on-sequence-model.md @@ -290,13 +290,13 @@ These were settled while building slice A and through its side-chat reviews. Eac ## 11. Questions -Q1 and Q2 were decided by the side chat on `75f0bd113c` and are encoded in §1, §3 and §5. Q3 (delete `secondary_checkpoints`) and Q4 (add the receipt inputs, as slice B) were decided during slice A (§10a). Q5 is decided; Q6 is the only one open: +Q1 and Q2 were decided by the side chat on `75f0bd113c` and are encoded in §1, §3 and §5. Q3 (delete `secondary_checkpoints`) and Q4 (add the receipt inputs, as slice B) were decided during slice A (§10a). Q5 and Q6 are decided; none is open: - **Q5 (decided by eager-gull-22, 2026-10-03):** the plan and the inspection receipt are committed JSON under `artifacts/receipts/`, read from the checkout by a fail-closed typed reader that records the file's digest. One dispatch input names the file. Inline JSON in a dispatch input is refused. -- **Q6 (open, with the operator):** adding that dispatch input to the fleet-converge workflow surface. +- **Q6 (decided, 2026-10-04):** add the `attempt_receipt` input to the fleet-converge `mtcollins1_boot` mode. It was operator escalation msg_1b57e749, approved by default after 15 minutes with no answer, and relayed by eager-gull-22. ## 12. Slice B: the attempt receipt's live inputs (plan, for review before code) -Slice B fills the `AttemptConfigurationReceipt` fields that slice A records as `NotRecorded` (decided Q4). The boot run takes its host as a `ManagedHost` / `ManagedHostBinding` (`gunbc.managed_host`), not as mtcollins1 constants; cut 4d of the managed-host untangle will re-root the rest of the run. Code waits on Q6 and this section's approval. +Slice B fills the `AttemptConfigurationReceipt` fields that slice A records as `NotRecorded` (decided Q4). The boot run takes its host as a `ManagedHost` / `ManagedHostBinding` (`gunbc.managed_host`), not as mtcollins1 constants; cut 4d of the managed-host untangle will re-root the rest of the run. **Two records, each minted only by its checks.** @@ -370,4 +370,33 @@ The pre-power-on firmware readback is bound to the same plan (`FirmwareReadBefor | applied stimulus and population | the inspection receipt; the controller reading only corroborates or conflicts | | firmware | a new pre-power-on `hpm check` read through `extdeps.bmc.ipmi` (none exists on main; `gunbc.fleet.mtcollins_firmware_converge` only renders a dry argv), plus the SMpro version word where it answers, both bound to the plan | -**Delivery (Q5, decided by eager-gull-22 on 2026-10-03).** The plan and the inspection receipt are committed JSON under `artifacts/receipts/`, reviewed and versioned like any change. eager-gull-22 authors them from what the operator reports about the physical change. One fleet-converge dispatch input names the receipt file, and the boot run reads it from the checkout with the fail-closed typed reader above. Inline JSON in a dispatch input is refused because it is not reviewable. Adding that input is Q6, which is open. +**Delivery (Q5, decided by eager-gull-22 on 2026-10-03).** The plan and the inspection receipt are committed JSON under `artifacts/receipts/`, reviewed and versioned like any change. eager-gull-22 authors them from what the operator reports about the physical change. One fleet-converge dispatch input names the receipt file, and the boot run reads it from the checkout with the fail-closed typed reader above. Inline JSON in a dispatch input is refused because it is not reviewable. Adding that input is Q6, decided. + +### 12a. Slice B1 as built + +Slice B1 is `gunbc.host_boot_attempt_admission`. It holds the plan and inspection records, the reader, the create-once attempt slot, and the projection into `AttemptConfigurationReceipt`. It is host-generic: mtcollins1 appears only as its route row (the receipt variables and the slot roster), in the `gunbc.host_maintenance_hold_reason` pattern. It returns one sealed `BootAttemptClearance`. + +**Placement** (agreed with warm-crane-577): the module sits beside the boot authorization. `mtcollins1_boot_under_live_unit_hold` calls `admit_boot_attempt(proof, revision)` right after `UnitHeld`, so admission runs under the hold and **before any controller read**. +- **Baseline:** the SDR cache and SEL baseline (`mtcollins1_boot_baseline`) are taken only after clearance. +- **Refused receipt:** the boot reads nothing from the controller, releases the hold, writes nothing, and fails with the typed cause. The matrix control is `a_refused_named_receipt_reads_no_baseline_and_writes_nothing`. +- **Configuration record:** the frozen configuration travels on the attempt record into the bundle. Slice A's always-`NotRecorded` placeholder is deleted. +- **Untangle cuts:** cuts 4a and 4d move the call site, and O2 carries its refusals. + +**The receipt is a tracked blob, digested.** +- **Revision binding:** admission reads the receipt at the boot's bound revision, not from the worktree. `extdeps.git.inspect` `ListTreeEntryAtPath` finds the entry, decoded by the existing `gunbc.namespace_step0_subject_collector` ls-tree reader. `git show :` reads the content. +- **Refusals:** no entry is `ReceiptNotTracked`. A symlink, gitlink or directory is `ReceiptNotRegularFile`. +- **Evidence:** `ReceiptEvidence { path, digest: Sha256FileDigest, commit }` carries the SHA-256 of exactly those bytes, from `extdeps.tools.sha256sum`. +- **Follow-up:** the step0 decoder belongs in `extdeps.git`. Extracting it is left to the namespace lane rather than forked here. + +**Times** are admitted only as canonical UTC instants, using `gunbc.auth.approval_capability` `utc_instant_is_canonical`, which checks calendar-valid fields. They are ordered with `utc_instant_before`, and equal instants are admitted. + +**Populations join exactly, or the receipt refuses.** +- **CPUs:** the CPU rows name exactly the plan's expected sockets. +- **DIMMs:** the DIMM rows name exactly the host's slot roster. For Mt. Collins that is the Getting Started Guide's 32 connectors (`dimm_figure_banks`), labelled as the guide labels them (its `J` prefix and the connector number) and placed on their bank's socket. Every label must be known and on its roster socket, and every slot must appear, populated or not. +- **Refusal causes:** a missing socket, an unknown label, a label on another socket, and an omitted slot each refuse with their own cause. + +**The slot store** is `/var/lib/gunbc/boot-attempts`, provisioned by `gunbc.runner_host_grants` `unit_hold_store_operations` beside the unit-hold store: same hosts, owner and mode. It is a separate directory, so a hold's release or recovery cannot reach it. Its executed control on the real store host is the first grant convergence followed by a receipt-carrying boot on srv1. + +Where the build differs from the plan above, with reasons: +- **Slot key.** The key is `attempt---`, with the host and nonce admitted only over `[A-Za-z0-9_-]`. It is injective by construction and is not a hash: the corpus's `content_hash_of_value` is a 64-bit structural hash, which does not meet "collision-safe" against a chosen nonce. +- **The plan's identity.** The inspection names its plan by `plan_subject` and `plan_attempt`. Because an attempt identity admits one boot, that pair identifies the plan. diff --git a/provisioning/srv1/gunbc-ghrunner.sudoers b/provisioning/srv1/gunbc-ghrunner.sudoers index 2e734efdadc..7885899b59e 100644 --- a/provisioning/srv1/gunbc-ghrunner.sudoers +++ b/provisioning/srv1/gunbc-ghrunner.sudoers @@ -109,6 +109,7 @@ ghrunner ALL=(root) NOPASSWD: /usr/bin/install -d -m 755 -o briansrls -g briansr ghrunner ALL=(root) NOPASSWD: /usr/sbin/usermod -aG kvm ghrunner ghrunner ALL=(root) NOPASSWD: /usr/bin/systemctl daemon-reload ghrunner ALL=(root) NOPASSWD: /usr/bin/install -d -m 755 -o ghrunner -g ghrunner /var/lib/gunbc/unit-holds +ghrunner ALL=(root) NOPASSWD: /usr/bin/install -d -m 755 -o ghrunner -g ghrunner /var/lib/gunbc/boot-attempts ghrunner ALL=(root) NOPASSWD: /usr/sbin/nft list table inet gunbc_microvm ghrunner ALL=(root) NOPASSWD: /usr/sbin/nft list ruleset ghrunner ALL=(root) NOPASSWD: /usr/sbin/iptables-legacy-save diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index 1fb839e8095..1af5173f960 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -1129,7 +1129,10 @@ fn floor_route_gap_expectation_chunk_11() -> List { } } -// The five test.claim.durable_cas_file_store_wet_witness identities: CAS publication read-back, +// The test.claim.host_boot_attempt_admission_wet_witness identity (the create-once attempt slot over +// the same file CAS; first effect the same Mktemp) and its digest identity (first effect sha256sum +// DigestStdin, no mock_response), then the five +// test.claim.durable_cas_file_store_wet_witness identities: CAS publication read-back, // sequential loser naming the winner, generation-two advance, a non-contention store refusal, and the // head search reaching the Int maximum without overflowing -- plus the five // test.claim.approval_assertion_counter_wet_witness_test identities (replay refused, per-enrolment @@ -1143,6 +1146,10 @@ fn floor_route_gap_expectation_chunk_11() -> List { // DirWithTemplate / NoMockResponse gap on each identity. fn floor_route_gap_expectation_chunk_12() -> List { Cons { + head: FloorRouteGapExpectation { identity: "test.claim.host_boot_attempt_admission_wet_witness.one_changed_byte_changes_the_receipt_digest_by_real_execution", operation: "DigestStdin", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.host_boot_attempt_admission_wet_witness.an_attempt_slot_admits_each_nonce_once_across_later_attempts_and_hold_releases_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.commit_then_independent_read_back_agrees_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.a_second_eligible_writer_loses_to_the_observed_winner_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, @@ -1191,6 +1198,8 @@ fn floor_route_gap_expectation_chunk_12() -> List { } } } + } + } } // V4.1 apply-seam DigestFile / DigestStdin claims (gunbc#11476, floor 35151938937). Hermetic diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index 4ee564549af..326e982ff5e 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -1665,6 +1665,18 @@ fn local_repo_wet_schedule() -> List { function: "a_selected_declaration_missing_its_file_id_offers_no_selection_by_real_execution", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.host_boot_attempt_admission_wet_witness", function: "one_changed_byte_changes_the_receipt_digest_by_real_execution" }, + entry: "dag/test/claim/host/host_boot_attempt_admission_wet_witness_test.dag", + function: "one_changed_byte_changes_the_receipt_digest_by_real_execution", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.host_boot_attempt_admission_wet_witness", function: "an_attempt_slot_admits_each_nonce_once_across_later_attempts_and_hold_releases_by_real_execution" }, + entry: "dag/test/claim/host/host_boot_attempt_admission_wet_witness_test.dag", + function: "an_attempt_slot_admits_each_nonce_once_across_later_attempts_and_hold_releases_by_real_execution", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.durable_cas_file_store_wet_witness", function: "commit_then_independent_read_back_agrees_by_real_execution" }, entry: "dag/test/claim/durable_cas_file_store_wet_witness_test.dag",