diff --git a/dag/extdeps/bmc/redfish_telemetry.dag b/dag/extdeps/bmc/redfish_telemetry.dag index 42cd6416575..2e38b593ad4 100644 --- a/dag/extdeps/bmc/redfish_telemetry.dag +++ b/dag/extdeps/bmc/redfish_telemetry.dag @@ -56,6 +56,7 @@ data extdeps_model_scope: ExternalModelScope = ExternalModelScope { further_citations: [ ExternalAuthority { uri: Uri { scheme: Https, locator: "redfish.dmtf.org/schemas/v1/Thermal.v1_3_0.json" } }, ExternalAuthority { uri: Uri { scheme: Https, locator: "redfish.dmtf.org/schemas/v1/LogEntry.v1_9_0.json" } }, + ExternalAuthority { uri: Uri { scheme: Https, locator: "redfish.dmtf.org/schemas/v1/LogService.v1_0_0.json" } }, ExternalAuthority { uri: Uri { scheme: Https, locator: "redfish.dmtf.org/schemas/v1/Resource.json" } }, ] } @@ -281,6 +282,13 @@ type RedfishLogEntry { message: NonEmptyStr } +// ONE LOG SERVICE (LogService.v1_0_0): its Id within its collection, and the LogEntry members of its +// Entries collection, in the order the service numbers them. +type RedfishLogService { + id: NonEmptyStr + entries: List +} + fn redfish_log_entry(v: JsonValue) -> ObservationAttempt { match read_string_member(v: v, key: "Id") { MemberString { value: id_text } => match parse_int(s: id_text) { diff --git a/dag/gunbc/bmc_model.dag b/dag/gunbc/bmc_model.dag index 0c46980e40b..17393b70e5b 100644 --- a/dag/gunbc/bmc_model.dag +++ b/dag/gunbc/bmc_model.dag @@ -1,10 +1,12 @@ module gunbc.bmc_model -import std.types { Bool, Int, List } +import std.types { Bool, Int, List, NonEmptyStr } import std.measure { Second, second, second_count } import v2.std.optional { Present, Absent } import v2.std.algebra { any, filter } import extdeps.bmc.ipmi_channel { IpmiChannelNumber, IpmiUserId, IpmiUserChannelAccess, IpmiChannelPrivilegeLimit } +import extdeps.bmc.redfish_telemetry { RedfishLogEntry, RedfishLogService, RedfishTelemetryPoint } +import extdeps.bmc.redfish_virtual_media { RedfishVirtualMediaObservation } import extdeps.bmc.ipmi_chassis_control { IpmiChassisControlAction, IpmiChassisPowerDown, IpmiChassisPowerUp, IpmiChassisPowerCycle, IpmiChassisHardReset, } @@ -55,6 +57,36 @@ type BmcSelRecord { state: String } +// THE READ-ONLY RECORD SURFACES A CONTROLLER SERVES BESIDE ITS STATE, one field per upstream surface +// and only the ones a prior-life archive reads (docs/plans/machine-intake-design.md §5; consumed by +// gunbc.machine_intake_prior_life_boundary). Each is Absent when a world does not model it, so a +// reader that needs a surface refuses rather than reading an unmodeled surface as an empty record; +// bmc_world() leaves all five unmodeled, and no transition in this module changes any of them. +// - manager_date_time: the Redfish Manager resource's DateTime property (Manager.v1_0_0), as the +// controller renders its own clock. It is an observation and never an ordering clock. +// - log_services: the Redfish LogService resources the controller serves, each with its LogEntry +// members (extdeps.bmc.redfish_telemetry RedfishLogService, LogService.v1_0_0 / LogEntry.v1_9_0). +// - account_events: the LogEntry members of the log service that records AccountService events +// (session and account changes). Redfish standardizes the entries, not which service holds them. +// - virtual_media: the VirtualMedia members (extdeps.bmc.redfish_virtual_media). +// - sensors: the Sensor members (extdeps.bmc.redfish_telemetry RedfishTelemetryPoint, Sensor.v1_2_0). +// The IPMI SEL, the boot override and the power state are already fields of BmcWorld. +type BmcRecordSurfaces { + manager_date_time: NonEmptyStr? + log_services: List? + account_events: List? + virtual_media: List? + sensors: List? +} + +data bmc_record_surfaces_unmodeled: BmcRecordSurfaces = BmcRecordSurfaces { + manager_date_time: none, + log_services: none, + account_events: none, + virtual_media: none, + sensors: none, +} + // sol_drop_after_boot, when a scenario sets it, schedules the controller dropping its SOL session that // long after the host starts booting, so the loss follows the route's own power-on rather than a clock // guessed in advance. @@ -75,13 +107,14 @@ type BmcWorld { web: BmcWebWorld ipmi_users: List ipmi_user_access: List + record_surfaces: BmcRecordSurfaces } fn bmc_world(power: BmcPower) -> BmcWorld { BmcWorld { power: power, pending: [], fired: [], boot_override: BootOverrideNone, sel: [], sol_session_open: false, cycle_off_interval: second(count: 5), host_booted_at: none, booted_via_override: false, sol_drop_after_boot: none, - web: bmc_web_world_untouched, ipmi_users: [], ipmi_user_access: [], + web: bmc_web_world_untouched, ipmi_users: [], ipmi_user_access: [], record_surfaces: bmc_record_surfaces_unmodeled, } } @@ -149,7 +182,7 @@ fn bmc_with_power(world: BmcWorld, power: BmcPower) -> BmcWorld { power: power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -158,7 +191,16 @@ fn bmc_with_web(world: BmcWorld, web: BmcWebWorld) -> BmcWorld { power: world.power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, + } +} + +fn bmc_with_record_surfaces(world: BmcWorld, surfaces: BmcRecordSurfaces) -> BmcWorld { + BmcWorld { + power: world.power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, + sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, + host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: surfaces, } } @@ -267,7 +309,7 @@ fn bmc_with_override(world: BmcWorld, over: BmcBootOverride) -> BmcWorld { power: world.power, pending: world.pending, fired: world.fired, boot_override: over, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -276,7 +318,7 @@ fn bmc_with_sol_session(world: BmcWorld, open: Bool) -> BmcWorld { power: world.power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -285,7 +327,7 @@ fn bmc_with_pending(world: BmcWorld, pending: List, fired: Li power: world.power, pending: pending, fired: fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -301,7 +343,7 @@ fn bmc_host_boots(world: BmcWorld, now: Second) -> BmcWorld { power: BmcPowerOn, pending: pending, fired: world.fired, boot_override: BootOverrideNone, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: Present { value: now }, booted_via_override: via, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -402,7 +444,7 @@ fn bmc_with_sol_drop_after_boot(world: BmcWorld, after: Second) -> BmcWorld { power: world.power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: Present { value: after }, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -433,7 +475,7 @@ fn bmc_with_ipmi_users(world: BmcWorld, users: List) -> BmcWorld { power: world.power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: users, ipmi_user_access: world.ipmi_user_access, + web: world.web, ipmi_users: users, ipmi_user_access: world.ipmi_user_access, record_surfaces: world.record_surfaces, } } @@ -475,7 +517,7 @@ fn bmc_with_ipmi_user_access(world: BmcWorld, rows: List) power: world.power, pending: world.pending, fired: world.fired, boot_override: world.boot_override, sel: world.sel, sol_session_open: world.sol_session_open, cycle_off_interval: world.cycle_off_interval, host_booted_at: world.host_booted_at, booted_via_override: world.booted_via_override, sol_drop_after_boot: world.sol_drop_after_boot, - web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: rows, + web: world.web, ipmi_users: world.ipmi_users, ipmi_user_access: rows, record_surfaces: world.record_surfaces, } } diff --git a/dag/gunbc/clock_read.dag b/dag/gunbc/clock_read.dag index 5fcd355a08e..bc3b0e40284 100644 --- a/dag/gunbc/clock_read.dag +++ b/dag/gunbc/clock_read.dag @@ -76,7 +76,23 @@ fn observer_clock_read() -> ObserverClockRead { fn observer_clock_modeled(millis: EpochMs, realization: NonEmptyStr) -> ObserverClockInstant admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_bmc_account_instant"), - decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "observer_at"), + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_prior_life_instant"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_already_secured_controller_is_a_noop"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "managed_and_factory_both_accepted_is_not_a_noop_and_converges_through_apply"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "reflash_restored_factory_access_takes_the_same_apply_and_readback_path"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_year_2000_readback_cannot_satisfy_ordering_and_an_observer_instant_can"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_ungrounded_route_with_approval_refuses_the_apply"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_secret_order_is_carried_by_the_plan"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_post_read_is_independent_of_the_reading_that_diverged"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_plan_refuses_a_stale_or_foreign_generation_and_a_foreign_reading"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_route_for_a_build_the_controller_no_longer_runs_cannot_be_admitted"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_published_replacement_must_be_the_goal_bound_break_glass_generation"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_open_channel_is_a_deviation_and_the_plan_refuses_without_a_channel_access_route"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_open_channel_is_closed_only_over_a_grounded_channel_access_route"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_apply_whose_post_read_fails_the_goal_generation_mints_no_receipt"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_channel_close_readback_is_bound_to_the_observed_run_and_account"), + decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_planned_channel_close_is_applied_read_back_and_converges"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_a_budget_that_differs_only_in_its_duration_flips_completed_to_elapsed"), ] { ObserverClockInstant { millis: millis, source: ObserverClockModeled { realization: realization } } diff --git a/dag/gunbc/fleet/convergence_fold.dag b/dag/gunbc/fleet/convergence_fold.dag index 1c4b3cd1221..432da9faf74 100644 --- a/dag/gunbc/fleet/convergence_fold.dag +++ b/dag/gunbc/fleet/convergence_fold.dag @@ -4,6 +4,15 @@ import std.types { Bool, Int, List, NonEmptyStr, String, brand } import v2.std.algebra { length } import std.decl_ref { DeclarationRef, declaration_ref_eq } import std.decl_ref { decl_ref } +import std.measure { PositiveMillisecond, positive_millisecond_count } +import gunbc.clock_read { + ObserverClockInstant, + ObserverClockRead, + ObserverClockObserved, + ObserverClockUnreadable, + observer_instant_millis, + observer_instant_precedes, +} import gunbc.host_convergence_census { host_convergence_census_standing, HostConvergenceCensus, @@ -27,12 +36,18 @@ import gunbc.host_convergence_census { // run's ledger. It executes no protocol and applies nothing, so it does not discharge CONVERGENCE-ONE // C8 (gunbc.host_convergence_protocol host_effect_decide_apply_frontier stays awaiting). // -// WHAT THIS CUT DOES NOT CARRY, because no consumer in it exercises the capability and a designed -// fixture is not an inhabitant (DESIGN §3 pairing obligation): apply followed by readback, the -// authorization gate and its discharge, principals, mutation lanes, per-leg deadlines, pending, subject -// quantifiers (all-of / any-of over a subject set), the domain-declared cheap readback, and order -// derived from preconditions alone where no order authority exists. Each lands with its first real -// consumer: O1c-2 (PriorLifeBoundary), O1c-3 (BmcSecure and ManagedHostAdmission), the Spark arm. +// WHAT THIS HOME CARRIES SINCE O1c-2, with its first effectful consumer (the PriorLifeBoundary +// archive in gunbc.machine_intake_prior_life_boundary): an applied step's outcome, per-leg deadlines, +// and INCOMPLETE as its own arm -- a step whose actuation was attempted and whose completion its +// independent readback does not ground. Incomplete is neither refused (the domain decided not to act, +// or acting was refused before any effect) nor converged, and it never satisfies a precondition. +// +// WHAT IT STILL DOES NOT CARRY, because no consumer exercises it yet and a designed fixture is not an +// inhabitant (DESIGN §3 pairing obligation): the authorization gate and its discharge, principals, +// mutation lanes, pending with re-attach across runs, subject quantifiers (all-of / any-of over a +// subject set), the domain-declared cheap readback, and order derived from preconditions alone where +// no order authority exists. Each lands with its first real consumer: O1c-3 (BmcSecure and +// ManagedHostAdmission), the Spark arm. // A RUN AND A SUBJECT ARE THE CALLER'S IDENTITIES, BRANDED SO NEITHER IS READ AS THE OTHER. The // subject key is the domain's canonical spelling of what one step instance converges: for the arrival @@ -251,23 +266,38 @@ fn admit_convergence_plan( // WHAT A DOMAIN HANDS THE FOLD FOR ONE INSTANCE: its sealed receipt, or its typed refusal. The // receipt type R is the domain's (construction-confined in the domain module); the fold reads it only // through the domain's projection below, so the key it judges is the key the domain sealed. -type StepOutcome +// +// INCOMPLETE carries the domain's own incompleteness type I, separate from its refusal type C, so a +// cause that says "nothing was done" can never stand for one that says "something was done and not +// read back". +type StepOutcome = StepEstablished { receipt: R } | StepRefused { key: StepInstanceKey, cause: C } + | StepIncomplete { key: StepInstanceKey, cause: I } // THE ONLY EXHAUSTIVE MATCHES ON StepOutcome LIVE IN THIS MODULE, so an arm added later (the Spark // arm's pending) changes the fold and no domain. A domain reads its own outcome through these. -fn step_outcome_receipt(outcome: StepOutcome) -> R? { +fn step_outcome_receipt(outcome: StepOutcome) -> R? { match outcome { StepEstablished { receipt: r } => Present { value: r } StepRefused { key: _, cause: _ } => none + StepIncomplete { key: _, cause: _ } => none } } -fn step_outcome_refusal(outcome: StepOutcome) -> C? { +fn step_outcome_refusal(outcome: StepOutcome) -> C? { match outcome { StepEstablished { receipt: _ } => none StepRefused { key: _, cause: c } => Present { value: c } + StepIncomplete { key: _, cause: _ } => none + } +} + +fn step_outcome_incomplete(outcome: StepOutcome) -> I? { + match outcome { + StepEstablished { receipt: _ } => none + StepRefused { key: _, cause: _ } => none + StepIncomplete { key: _, cause: i } => Present { value: i } } } @@ -286,6 +316,7 @@ fn convergence_receipt_projection(key_of: fn(R) -> StepInstanceKey, consumed_ decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "arrival_receipt_projection"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplete"), ] { ConvergenceReceiptProjection { key_of: key_of, consumed_of: consumed_of } @@ -297,20 +328,21 @@ type StepInstanceRefusal | PreconditionUnmet { precondition: StepInstanceKey, consumed: List } | ConsumedReceiptNotAPrecondition { consumed: StepInstanceKey } -type StepInstanceStanding +type StepInstanceStanding = InstanceConverged { key: StepInstanceKey, receipt: R } | InstanceRefused { key: StepInstanceKey, cause: StepInstanceRefusal } + | InstanceIncomplete { key: StepInstanceKey, cause: I } | InstanceNotReached { key: StepInstanceKey, blocked_by: StepInstanceKey } // THE LEDGER AND THE CONVERGED RUN ARE SEALED: only fold_convergence_run constructs them, so a // downstream admission (O1c-3's ManagedHostAdmission) can tell a folded run from an authored one. // The verdict and instance arms around them are open diagnostic wrappers; the admission evidence is // ConvergedRun. -type ConvergenceRunLedger sole_constructor { +type ConvergenceRunLedger sole_constructor { run: ConvergenceRunId subject: StepSubjectKey order_authority: DeclarationRef - instances: List> + instances: List> } // AN OUTCOME THAT IS NOT ONE INSTANCE OF THIS RUN REFUSES THE WHOLE RUN before any ledger is written: @@ -321,19 +353,23 @@ type RunOutcomeRefusal | OutcomeForUnplannedStep { key: StepInstanceKey } | OutcomeOutsideRun { key: StepInstanceKey } -type ConvergedRun sole_constructor { - ledger: ConvergenceRunLedger +type ConvergedRun sole_constructor { + ledger: ConvergenceRunLedger } -type ConvergenceRunVerdict - = RunConverged { run: ConvergedRun } - | RunStopped { ledger: ConvergenceRunLedger, at: StepInstanceKey } +// A RUN THAT STOPPED AT AN INCOMPLETE INSTANCE IS NOT A RUN THAT STOPPED AT A REFUSAL: the first may +// have changed the world and owes a re-observation, the second did not. Neither is converged. +type ConvergenceRunVerdict + = RunConverged { run: ConvergedRun } + | RunStopped { ledger: ConvergenceRunLedger, at: StepInstanceKey } + | RunIncomplete { ledger: ConvergenceRunLedger, at: StepInstanceKey } | RunOutcomesRefused { cause: RunOutcomeRefusal } -fn outcome_key(outcome: StepOutcome, projection: ConvergenceReceiptProjection) -> StepInstanceKey { +fn outcome_key(outcome: StepOutcome, projection: ConvergenceReceiptProjection) -> StepInstanceKey { match outcome { StepEstablished { receipt: r } => projection.key_of(r) StepRefused { key: k, cause: _ } => k + StepIncomplete { key: k, cause: _ } => k } } @@ -359,10 +395,11 @@ fn first_outcome_refusal( }) } -fn converged_key_in(ledger: List>, key: StepInstanceKey) -> Bool { +fn converged_key_in(ledger: List>, key: StepInstanceKey) -> Bool { ledger |> any(e => match e { InstanceConverged { key: k, receipt: _ } => step_instance_key_eq(a: k, b: key) InstanceRefused { key: _, cause: _ } => false + InstanceIncomplete { key: _, cause: _ } => false InstanceNotReached { key: _, blocked_by: _ } => false }) } @@ -376,11 +413,11 @@ fn key_in(keys: List, key: StepInstanceKey) -> Bool { // receipt must name that exact instance as what it consumed. A receipt for another subject or from // another run names another key and satisfies nothing; a consumed key that is no precondition of this // step refuses rather than being ignored. -fn precondition_refusal( +fn precondition_refusal( step: ConvergenceStep, key: StepInstanceKey, consumed: List, - ledger: List>, + ledger: List>, ) -> StepInstanceRefusal? { let required = map(step.preconditions, p => precondition_key(p: p, key: key)) match required |> filter(r => (converged_key_in(ledger: ledger, key: r) && key_in(keys: consumed, key: r)) == false) |> first() { @@ -393,12 +430,32 @@ fn precondition_refusal( } } -type LedgerWalk { - stopped_at: StepInstanceKey? - instances: List> +// WHERE THE LINE IS: still open, stopped at a refused (or unreached) instance, or stopped at an +// INCOMPLETE one. One sum, so a stop without a key, or a key without its kind, has no constructor. +type LineState + = LineOpen + | LineStoppedAt { at: StepInstanceKey } + | LineIncompleteAt { at: StepInstanceKey } + +type LedgerWalk { + line: LineState + instances: List> +} + +fn line_after(standing: StepInstanceStanding) -> LineState { + match standing { + InstanceConverged { key: _, receipt: _ } => LineOpen + InstanceRefused { key: k, cause: _ } => LineStoppedAt { at: k } + InstanceIncomplete { key: k, cause: _ } => LineIncompleteAt { at: k } + InstanceNotReached { key: k, blocked_by: _ } => LineStoppedAt { at: k } + } +} + +fn not_reached_after(acc: LedgerWalk, key: StepInstanceKey, blocker: StepInstanceKey) -> LedgerWalk { + LedgerWalk { line: acc.line, instances: concat(acc.instances, [InstanceNotReached { key: key, blocked_by: blocker }]) } } -fn instance_outcome(outcomes: List>, key: StepInstanceKey, projection: ConvergenceReceiptProjection) -> StepOutcome? { +fn instance_outcome(outcomes: List>, key: StepInstanceKey, projection: ConvergenceReceiptProjection) -> StepOutcome? { outcomes |> filter(o => step_instance_key_eq(a: outcome_key(outcome: o, projection: projection), b: key)) |> first() } @@ -406,23 +463,27 @@ fn instance_outcome(outcomes: List>, key: StepInstanceKe // single-subject run every later instance is such a dependent, so the whole rest of the line is // NotReached, each naming the instance that blocked it. When instances span several subjects, an // independent instance is not a dependent and is not stopped by this rule. An instance with no outcome refuses as StepOutcomeAbsent; it is never read as converged. -fn walk_instance( - acc: LedgerWalk, +// An INCOMPLETE instance stops the line the same way, because in a single-subject run every later +// instance depends on it, and the line state records which kind of stop it was. +fn walk_instance( + acc: LedgerWalk, ranked: RankedStep, run: ConvergenceRunId, subject: StepSubjectKey, - outcomes: List>, + outcomes: List>, projection: ConvergenceReceiptProjection, -) -> LedgerWalk { +) -> LedgerWalk { let key = step_instance_key(run: run, step: ranked.step.identity, subject: subject) - match acc.stopped_at { - Present { value: blocker } => LedgerWalk { stopped_at: acc.stopped_at, instances: concat(acc.instances, [InstanceNotReached { key: key, blocked_by: blocker }]) } - Absent => { + match acc.line { + LineStoppedAt { at: blocker } => not_reached_after(acc: acc, key: key, blocker: blocker) + LineIncompleteAt { at: blocker } => not_reached_after(acc: acc, key: key, blocker: blocker) + LineOpen => { let standing = match instance_outcome(outcomes: outcomes, key: key, projection: projection) { Absent => InstanceRefused { key: key, cause: StepOutcomeAbsent } Present { value: o } => match o { StepRefused { key: _, cause: c } => InstanceRefused { key: key, cause: DomainRefused { cause: c } } + StepIncomplete { key: _, cause: i } => InstanceIncomplete { key: key, cause: i } StepEstablished { receipt: r } => match precondition_refusal(step: ranked.step, key: key, consumed: projection.consumed_of(r), ledger: acc.instances) { Present { value: why } => InstanceRefused { key: key, cause: why } @@ -430,35 +491,116 @@ fn walk_instance( } } } - let stop = match standing { - InstanceConverged { key: _, receipt: _ } => none - InstanceRefused { key: k, cause: _ } => Present { value: k } - InstanceNotReached { key: k, blocked_by: _ } => Present { value: k } - } - LedgerWalk { stopped_at: stop, instances: concat(acc.instances, [standing]) } + LedgerWalk { line: line_after(standing: standing), instances: concat(acc.instances, [standing]) } } } } -// THE RUN FOLD: one ledger per run, each instance converged, refused or not reached, in the admitted +// THE RUN FOLD: one ledger per run, each instance converged, refused, incomplete or not reached, in the admitted // order. The verdict is derived from the ledger and names the instance the line stopped at. -fn fold_convergence_run( +fn fold_convergence_run( plan: AdmittedConvergencePlan, run: ConvergenceRunId, subject: StepSubjectKey, - outcomes: List>, + outcomes: List>, projection: ConvergenceReceiptProjection, -) -> ConvergenceRunVerdict { +) -> ConvergenceRunVerdict { match first_outcome_refusal(run: run, subject: subject, plan: plan, keys: map(outcomes, o => outcome_key(outcome: o, projection: projection))) { Present { value: r } => RunOutcomesRefused { cause: r } Absent => { - let walked = fold(plan.steps, init: LedgerWalk { stopped_at: none, instances: [] }, f: (acc, s) => + let walked = fold(plan.steps, init: LedgerWalk { line: LineOpen, instances: [] }, f: (acc, s) => walk_instance(acc: acc, ranked: s, run: run, subject: subject, outcomes: outcomes, projection: projection)) let ledger = ConvergenceRunLedger { run: run, subject: subject, order_authority: plan.authority, instances: walked.instances } - match walked.stopped_at { - Absent => RunConverged { run: ConvergedRun { ledger: ledger } } - Present { value: k } => RunStopped { ledger: ledger, at: k } + match walked.line { + LineOpen => RunConverged { run: ConvergedRun { ledger: ledger } } + LineStoppedAt { at: k } => RunStopped { ledger: ledger, at: k } + LineIncompleteAt { at: k } => RunIncomplete { ledger: ledger, at: k } } } } } + +// ── EFFECT LEGS AND THEIR DEADLINES ──────────────────────────────────────────────────────────────── + +// A LEG'S BUDGET: which effect leg, and how long it may take, as a positive duration and never an +// instant. Sealed, and minted only for the callers leg_budget admits -- the one function in each +// domain that declares that leg's budget, and the one Bool claim that varies only the duration -- so +// no caller can hand an effect a made-up budget. The value is a duration and every instant is a +// sealed observer instant because a time-typed scalar formal does not refuse a record passed at it +// (gunbc.recurring_failure_mode product_value_at_a_scalar_formal_is_accepted): a deadline's safety +// comes from these sealed carriers, not from the checker. +type LegBudget sole_constructor { + leg: DeclarationRef + budget: PositiveMillisecond +} + +fn leg_budget(leg: DeclarationRef, budget: PositiveMillisecond) -> LegBudget + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "prior_life_archive_write_budget"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_a_budget_that_differs_only_in_its_duration_flips_completed_to_elapsed"), + ] +{ + LegBudget { leg: leg, budget: budget } +} + +// A LEG'S DEADLINE: its budget and the observer-clock instant it started at. Sealed, and built only +// here from a sealed budget and a sealed observer instant, for the callers effect_leg_deadline admits +// (each the one function in its domain that runs that leg), so an effect that takes a LegDeadline +// cannot be invoked without one and no other caller can start a leg at an instant of its choosing. +type LegDeadline sole_constructor { + budget: LegBudget + started: ObserverClockInstant +} + +fn effect_leg_deadline(budget: LegBudget, started: ObserverClockInstant) -> LegDeadline + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_write_archive"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_a_budget_that_differs_only_in_its_duration_flips_completed_to_elapsed"), + ] +{ + LegDeadline { budget: budget, started: started } +} + +fn leg_deadline_leg(d: LegDeadline) -> DeclarationRef { + d.budget.leg +} + +// A LEG THAT FINISHED WITHIN ITS DEADLINE, sealed: only complete_effect_leg mints it, from the leg's +// deadline and an observer-clock read taken after the leg, and complete_effect_leg admits only the +// function that ran the leg, so no caller can pair a deadline with a finish instant of its choosing. +type LegCompletedWithinDeadline sole_constructor { + deadline: LegDeadline + finished: ObserverClockInstant +} + +fn leg_completed_leg(c: LegCompletedWithinDeadline) -> DeclarationRef { + c.deadline.budget.leg +} + +// WHAT THE OBSERVER CLOCK SAYS AFTER A LEG RAN. Only the first arm is a completion; each other arm is +// a reason completion is NOT grounded, and an attempted effect in any of them is incomplete, never +// established. +type LegCompletion + = LegCompletedWithin { completed: LegCompletedWithinDeadline } + | LegDeadlineElapsed { deadline: LegDeadline, finished: ObserverClockInstant } + | LegFinishedBeforeItStarted { deadline: LegDeadline, finished: ObserverClockInstant } + | LegCompletionUnobserved { deadline: LegDeadline, detail: String } + +fn complete_effect_leg(deadline: LegDeadline, finished: ObserverClockRead) -> LegCompletion + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_write_archive"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_a_budget_that_differs_only_in_its_duration_flips_completed_to_elapsed"), + ] +{ + match finished { + ObserverClockUnreadable { detail: d } => LegCompletionUnobserved { deadline: deadline, detail: d } + ObserverClockObserved { instant: f } => + if observer_instant_precedes(earlier: f, later: deadline.started) { + LegFinishedBeforeItStarted { deadline: deadline, finished: f } + } else if (observer_instant_millis(instant: f) as Int) - (observer_instant_millis(instant: deadline.started) as Int) > positive_millisecond_count(m: deadline.budget.budget) { + LegDeadlineElapsed { deadline: deadline, finished: f } + } else { + LegCompletedWithin { completed: LegCompletedWithinDeadline { deadline: deadline, finished: f } } + } + } +} diff --git a/dag/gunbc/host_convergence_census.dag b/dag/gunbc/host_convergence_census.dag index 48db5c76746..fe27735eb1a 100644 --- a/dag/gunbc/host_convergence_census.dag +++ b/dag/gunbc/host_convergence_census.dag @@ -839,6 +839,15 @@ data host_convergence_census_rows: List = [ disposition: RetainAuthority, first_consumer: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_prefix"), ), + census_row( + identity: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary"), + subject: MachineIntakeArrival, + phases: protocol_phases(false, true, true, true, false, true, false), + current_authority: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary"), + persistent_host_effect: DoesNotMutateHost, + disposition: RetainAuthority, + first_consumer: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_prefix"), + ), ] data host_convergence_census_standing: HostConvergenceCensus = admit_host_convergence_census(rows: host_convergence_census_rows) diff --git a/dag/gunbc/machine_intake/arrival_converge.dag b/dag/gunbc/machine_intake/arrival_converge.dag index 6bf34d28804..53321df64ec 100644 --- a/dag/gunbc/machine_intake/arrival_converge.dag +++ b/dag/gunbc/machine_intake/arrival_converge.dag @@ -91,6 +91,19 @@ import gunbc.machine_intake_bmc_rotation_route { } import gunbc.machine_intake_bmc_rotation_route_evidence { manager_read_receipt, mtjade1_observed_endpoint } import gunbc.host_convergence_protocol { HostEffectDomainProjection, inspect_via_host_effect_projection } +import gunbc.machine_intake_prior_life_boundary { + DryPriorLifeWorld, + PriorLifeBoundaryEstablished, + PriorLifeRefusal, + PriorLifeIncomplete, + PriorLifeArchiveEstablished, + PriorLifeArchiveRefused, + PriorLifeArchiveIncomplete, + dry_archive_prior_life, + mt_jade_platform_ref, + prior_life_receipt_key, + prior_life_receipt_consumed_identity, +} import gunbc.fleet.convergence_fold { ConvergenceRunId, StepSubjectKey, @@ -107,6 +120,7 @@ import gunbc.fleet.convergence_fold { StepOutcome, StepEstablished, StepRefused, + StepIncomplete, ConvergenceReceiptProjection, ConvergenceRunVerdict, admit_convergence_plan, @@ -115,18 +129,22 @@ import gunbc.fleet.convergence_fold { step_outcome_receipt, } -// THE ARRIVAL CONVERGENCE, READ-ONLY PREFIX (docs/plans/managed-host-untangle.md, cut O1c-1): the -// first real consumer of gunbc.fleet.convergence_fold. Its two steps are the first two phases of -// gunbc.machine_intake_phase arrival_phases_all, AccessDiscover and IdentityBindProvisional, each a -// protocol step through gunbc.host_convergence_protocol HostEffectDomainProjection (observe, assess, -// decide) with its own row in gunbc.host_convergence_census. Both are read-only: the only decision -// either can reach is Noop (the phase's goal is read back as already holding) or Refuse; neither has -// an Apply, so an Apply decision is itself a typed refusal. Nothing here performs a live BMC call: the -// read each step consumes is a committed capture. gunbc.bmc_onboarding is not imported. +// THE ARRIVAL CONVERGENCE PREFIX (docs/plans/managed-host-untangle.md, cuts O1c-1 and O1c-2): the first +// real consumer of gunbc.fleet.convergence_fold. Its three steps are the first three phases of +// gunbc.machine_intake_phase arrival_phases_all -- AccessDiscover, IdentityBindProvisional and +// PriorLifeBoundary -- each a protocol step through gunbc.host_convergence_protocol +// HostEffectDomainProjection (observe, assess, decide) with its own row in +// gunbc.host_convergence_census. The first two are read-only: the only decision either can reach is +// Noop (the phase's goal is read back as already holding) or Refuse; neither has an Apply, so an Apply +// decision is itself a typed refusal, and the read each consumes is a committed capture. +// PriorLifeBoundary is the first effectful step: its archive arm writes the controller's prior-life +// records to the evidence store and reads them back, DRY in this cut +// (gunbc.machine_intake_prior_life_boundary), so it is the one step that can be INCOMPLETE. Nothing +// here performs a live BMC call or a live store write. gunbc.bmc_onboarding is not imported. // -// ORDERING TIME. No field here is an ordering clock. The controller's own DateTime is kept as an -// AccessDiscover observation only; cut O1b's observer clock (#13221, not landed at this writing) is -// the ordering authority, and this cut orders nothing by time. +// ORDERING TIME. No field of the read-only steps is an ordering clock. The controller's own DateTime is +// kept as an AccessDiscover observation only; the observer clock (gunbc.clock_read) orders the +// archive write's leg against its deadline, and nothing here orders by the controller's clock. data arrival_order_authority_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_phase", decl_name: "arrival_phases_all") @@ -134,6 +152,8 @@ data access_discover_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.mac data identity_bind_provisional_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "identity_bind_provisional") +data prior_life_boundary_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary") + // A read-only phase has no remedy. The plan type of its projection is sealed to this module and this // module constructs none, so an Apply over a read-only phase has no value to carry. type ReadOnlyPhaseRemedy sole_constructor { @@ -433,6 +453,7 @@ fn intake_attempt_of_run(run: ConvergenceRunId) -> IntakeAttemptId { type ArrivalStepReceipt = AccessDiscoverReceipt { receipt: AccessDiscoverEstablished } | IdentityBindReceipt { receipt: IdentityBoundProvisional } + | PriorLifeBoundaryReceipt { receipt: PriorLifeBoundaryEstablished } type ArrivalStepRefusal = AccessDiscoverObserveRefused { cause: AccessObserveRefusal } @@ -441,11 +462,19 @@ type ArrivalStepRefusal | ReadOnlyPhaseRefused { phase: ArrivalPhase, reason: NonEmptyStr } | ReadOnlyPhaseDecidedApply { phase: ArrivalPhase } | ReadOnlyPhaseSatisfiedWithoutEvidence { phase: ArrivalPhase } + | PriorLifeIdentityForAnotherInstance { identity: StepInstanceKey } + | PriorLifeBoundaryRefused { cause: PriorLifeRefusal } + +// A STEP WHOSE EFFECT WAS ATTEMPTED AND IS NOT GROUNDED BY ITS READBACK. Only PriorLifeBoundary has +// an effect in this prefix; the read-only phases cannot be incomplete. +type ArrivalStepIncomplete + = PriorLifeBoundaryIncomplete { cause: PriorLifeIncomplete } fn arrival_receipt_key(r: ArrivalStepReceipt) -> StepInstanceKey { match r { AccessDiscoverReceipt { receipt: a } => a.key IdentityBindReceipt { receipt: i } => i.key + PriorLifeBoundaryReceipt { receipt: p } => prior_life_receipt_key(r: p) } } @@ -453,6 +482,7 @@ fn arrival_receipt_consumed(r: ArrivalStepReceipt) -> List { match r { AccessDiscoverReceipt { receipt: _ } => [] IdentityBindReceipt { receipt: i } => [i.consumed_access] + PriorLifeBoundaryReceipt { receipt: p } => [prior_life_receipt_consumed_identity(r: p)] } } @@ -470,7 +500,7 @@ fn read_only_refusal(phase: ArrivalPhase, decision: UpsertDecision StepOutcome { +fn access_discover(key: StepInstanceKey, read: CurrentManagerRead) -> StepOutcome { let projection = access_discover_projection() match inspect_via_host_effect_projection(subject: key, goal: AccessDiscoverGoal { unit: key.subject }, request: read, projection: projection) { GoalObservationRefused { subject: _, goal: _, request: _, cause: c } => StepRefused { key: key, cause: AccessDiscoverObserveRefused { cause: c } } @@ -499,7 +529,7 @@ fn access_discover(key: StepInstanceKey, read: CurrentManagerRead) -> StepOutcom // THE IDENTITYBINDPROVISIONAL STEP: the unit key from bind_unit_key over the unit's board-serial // observations, the provisional assembly, the live firmware manifest from the consumed access // receipt, qualification_subject_of, then MachineIntakeSubject with this run's one attempt identity. -fn identity_bind_provisional(key: StepInstanceKey, access: AccessDiscoverEstablished, inputs: IdentityBindInputs) -> StepOutcome { +fn identity_bind_provisional(key: StepInstanceKey, access: AccessDiscoverEstablished, inputs: IdentityBindInputs) -> StepOutcome { if (access.key.run as NonEmptyStr) != (key.run as NonEmptyStr) || (access.key.subject as NonEmptyStr) != (key.subject as NonEmptyStr) { StepRefused { key: key, cause: IdentityBindAccessForAnotherInstance { access: access.key } } } else { @@ -508,7 +538,7 @@ fn identity_bind_provisional(key: StepInstanceKey, access: AccessDiscoverEstabli } // The access receipt is this instance's own (same run, same subject): the step binds from it. -fn identity_bind_for_access(key: StepInstanceKey, access: AccessDiscoverEstablished, inputs: IdentityBindInputs) -> StepOutcome { +fn identity_bind_for_access(key: StepInstanceKey, access: AccessDiscoverEstablished, inputs: IdentityBindInputs) -> StepOutcome { let projection = identity_bind_projection() let request = IdentityBindRequest { access: access, inputs: inputs } match inspect_via_host_effect_projection(subject: key, goal: IdentityBindGoal { attempt: intake_attempt_of_run(run: key.run) }, request: request, projection: projection) { @@ -535,6 +565,23 @@ fn identity_bind_for_access(key: StepInstanceKey, access: AccessDiscoverEstablis } } +// THE PRIORLIFEBOUNDARY STEP: the archive of the unit's prior-life records, dry, over the subject the +// IdentityBindProvisional receipt of this run and this subject bound. The platform's policy row is +// selected by the caller before the step (DESIGN §3d); the archive, its write, its deadline and its +// readback are gunbc.machine_intake_prior_life_boundary's. A refusal wrote nothing; an incomplete +// write is its own outcome and never converged. +fn prior_life_boundary(key: StepInstanceKey, identity: IdentityBoundProvisional, platform: DeclarationRef, world: DryPriorLifeWorld) -> StepOutcome { + if (identity.key.run as NonEmptyStr) != (key.run as NonEmptyStr) || (identity.key.subject as NonEmptyStr) != (key.subject as NonEmptyStr) { + StepRefused { key: key, cause: PriorLifeIdentityForAnotherInstance { identity: identity.key } } + } else { + match dry_archive_prior_life(key: key, consumed_identity: identity.key, subject: identity.subject, platform: platform, world: world).outcome { + PriorLifeArchiveEstablished { receipt: r } => StepEstablished { receipt: PriorLifeBoundaryReceipt { receipt: r } } + PriorLifeArchiveRefused { cause: c } => StepRefused { key: key, cause: PriorLifeBoundaryRefused { cause: c } } + PriorLifeArchiveIncomplete { cause: i } => StepIncomplete { key: key, cause: PriorLifeBoundaryIncomplete { cause: i } } + } + } +} + // ── THE PLAN: a prefix of the authority's order, never a second list ─────────────────────────── fn arrival_order_authority() -> ConvergenceOrderAuthority { @@ -554,7 +601,7 @@ fn arrival_step_of_phase(phase: ArrivalPhase) -> ConvergenceStep? { match phase { AccessDiscover => Present { value: ConvergenceStep { identity: access_discover_step_ref, order_member: Arrival { phase: AccessDiscover }, preconditions: [] } } IdentityBindProvisional => Present { value: ConvergenceStep { identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: [SameSubject { step: access_discover_step_ref }] } } - PriorLifeBoundary => none + PriorLifeBoundary => Present { value: ConvergenceStep { identity: prior_life_boundary_step_ref, order_member: Arrival { phase: PriorLifeBoundary }, preconditions: [SameSubject { step: identity_bind_provisional_step_ref }] } } BmcSecure => none BootDeliveryEstablish => none DiagnosticBootAttest => none @@ -580,7 +627,7 @@ fn arrival_prefix_through(last: ArrivalPhase) -> List { } } -data arrival_prefix_last: ArrivalPhase = IdentityBindProvisional +data arrival_prefix_last: ArrivalPhase = PriorLifeBoundary type ArrivalPrefixSteps = ArrivalPrefixStepped { steps: List> } @@ -608,25 +655,44 @@ fn arrival_prefix_steps(phases: List) -> ArrivalPrefixSteps { type ArrivalPrefixVerdict = ArrivalPrefixUnstepped { phase: IntakePhase } | ArrivalPlanRefused { cause: ConvergencePlanRefusal } - | ArrivalRunFolded { verdict: ConvergenceRunVerdict } + | ArrivalRunFolded { verdict: ConvergenceRunVerdict } + +// THE PRIOR-LIFE INPUTS: the unit's platform (which selects its policy row) and the dry world the +// archive reads and writes. +type PriorLifeInputs { + platform: DeclarationRef + world: DryPriorLifeWorld +} -// The domain executes its read-only steps in the admitted order, each consuming only the receipt its +// The domain executes its steps in the admitted order, each consuming only the receipt its // precondition produced in this run; a step whose precondition did not establish is not executed and // the fold records it NotReached. Then the fold composes the outcomes into the run's ledger. -fn arrival_prefix_outcomes(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs) -> List> { +fn arrival_prefix_outcomes(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs, prior_life: PriorLifeInputs) -> List> { let access = access_discover(key: step_instance_key(run: run, step: access_discover_step_ref, subject: subject), read: read) match step_outcome_receipt(outcome: access) { Absent => [access] Present { value: r } => match r { - AccessDiscoverReceipt { receipt: a } => - [access, identity_bind_provisional(key: step_instance_key(run: run, step: identity_bind_provisional_step_ref, subject: subject), access: a, inputs: inputs)] + AccessDiscoverReceipt { receipt: a } => { + let identity = identity_bind_provisional(key: step_instance_key(run: run, step: identity_bind_provisional_step_ref, subject: subject), access: a, inputs: inputs) + match step_outcome_receipt(outcome: identity) { + Present { value: ir } => + match ir { + IdentityBindReceipt { receipt: i } => + [access, identity, prior_life_boundary(key: step_instance_key(run: run, step: prior_life_boundary_step_ref, subject: subject), identity: i, platform: prior_life.platform, world: prior_life.world)] + AccessDiscoverReceipt { receipt: _ } => [access, identity] + PriorLifeBoundaryReceipt { receipt: _ } => [access, identity] + } + Absent => [access, identity] + } + } IdentityBindReceipt { receipt: _ } => [access] + PriorLifeBoundaryReceipt { receipt: _ } => [access] } } } -fn fold_arrival_prefix(steps: List>, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ArrivalPrefixVerdict { +fn fold_arrival_prefix(steps: List>, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ArrivalPrefixVerdict { match admit_convergence_plan(planning: arrival_planning_authority(), steps: steps) { ConvergencePlanRefused { cause: c } => ArrivalPlanRefused { cause: c } ConvergencePlanAdmitted { plan: plan } => @@ -634,11 +700,11 @@ fn fold_arrival_prefix(steps: List>, run: Convergen } } -fn converge_arrival_prefix(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs) -> ArrivalPrefixVerdict { +fn converge_arrival_prefix(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs, prior_life: PriorLifeInputs) -> ArrivalPrefixVerdict { match arrival_prefix_steps(phases: arrival_prefix_through(last: arrival_prefix_last)) { ArrivalPrefixPhaseUnstepped { phase: p } => ArrivalPrefixUnstepped { phase: p } ArrivalPrefixStepped { steps: steps } => - fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs)) + fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life)) } } @@ -659,11 +725,20 @@ fn arrival_bound_unit_keys() -> List { // (B810301000412080005AJ0C1), so the step mints the two-source agreement and binds the unit key; // - provisional assembly: from the FRU capture, chassis part number B60.0300E.0001 with the chassis // (serial 21000012N0A1) as its one component; -// - live firmware manifest: the bmc entry 2.11.104000 from this run's Manager read, nothing else. +// - live firmware manifest: the bmc entry 2.11.104000 from this run's Manager read, nothing else; +// - PriorLifeBoundary: DRY ONLY. No capture of mtjade1's prior-life carriers is committed, so the +// archive reads the dry world the caller supplies, under the Mt. Jade policy row, and its receipt +// names the dry realization; the world claims no controller family. fn mtjade1_identity_bind_inputs() -> IdentityBindInputs uses fs: std.resources.Filesystem { IdentityBindInputs { fru: read_mtjade1_fru(), smbios: read_mtjade1_smbios_type2(), other_units: arrival_bound_unit_keys() } } -fn converge_mtjade1_arrival_prefix(run: ConvergenceRunId) -> ArrivalPrefixVerdict uses fs: std.resources.Filesystem { - converge_arrival_prefix(run: run, subject: "mtjade1" as StepSubjectKey, read: read_mtjade1_current_manager_read(), inputs: mtjade1_identity_bind_inputs()) +fn converge_mtjade1_arrival_prefix(run: ConvergenceRunId, prior_life: DryPriorLifeWorld) -> ArrivalPrefixVerdict uses fs: std.resources.Filesystem { + converge_arrival_prefix( + run: run, + subject: "mtjade1" as StepSubjectKey, + read: read_mtjade1_current_manager_read(), + inputs: mtjade1_identity_bind_inputs(), + prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life }, + ) } diff --git a/dag/gunbc/machine_intake/prior_life_boundary.dag b/dag/gunbc/machine_intake/prior_life_boundary.dag new file mode 100644 index 00000000000..d3b4eac519d --- /dev/null +++ b/dag/gunbc/machine_intake/prior_life_boundary.dag @@ -0,0 +1,950 @@ +module gunbc.machine_intake_prior_life_boundary + +import std.types { Bool, EpochMs, Int, List, NonEmptyStr, String } +import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } +import std.content_hash { ContentHash, content_hash_of_value, content_hash_equal } +import std.measure { positive_millisecond, PositiveMeasureSuccessor } +import std.algebra { FreeSemigroup, Empty } +import v2.std.algebra { length } +import std.goal_assessment { + ObservationAttempt, + ObservationEstablished, + ObservationRefused, + GoalAssessment, + GoalSatisfied, + GoalDiverged, + GoalIndeterminate, + GoalAssessmentRefused, + GoalInspected, + GoalObservationRefused, +} +import std.upsert_decision { UpsertDecision, Noop, Apply, Refuse } +import extdeps.uri { Uri, uri_scheme_wire } +import extdeps.languages.json.emit { JsonValue, JsonKeyValue, json_kv, json_int, json_bool, json_string, json_array, json_object, serialize_json } +import extdeps.bmc.redfish_telemetry { + RedfishLogEntry, + RedfishLogService, + RedfishTelemetryPoint, + RedfishHealth, + RedfishHealthOk, + RedfishHealthWarning, + RedfishHealthCritical, + RedfishHealthOther, + RedfishHealthUnreported, + RedfishResourceState, + RedfishStateEnabled, + RedfishStateDisabled, + RedfishStateAbsent, + RedfishStateOther, + RedfishStateUnreported, + RedfishReading, + RedfishReadingValue, + RedfishReadingNull, + RedfishReadingMissing, + RedfishPointKind, + RedfishTemperatureCelsius, + RedfishRotationalRpm, + RedfishOtherReading, +} +import extdeps.bmc.redfish_virtual_media { + RedfishVirtualMediaObservation, + RedfishVirtualMediaConnectedVia, + ConnectedViaNotConnected, + ConnectedViaUri, + ConnectedViaApplet, + ConnectedViaOem, + RedfishVirtualMediaLocator, + UnderManager, + UnderSystem, + redfish_virtual_media_type_wire, +} +import gunbc.bmc_model { + BmcWorld, + BmcSelRecord, + BmcPower, + BmcBootOverride, + BmcPowerOn, + BmcPowerOff, + BootOverrideNone, + BootOverrideCdromEfiNextBoot, +} +import gunbc.clock_read { + ObserverClockInstant, + ObserverClockObserved, + observer_clock_modeled, + observer_instant_millis, +} +import gunbc.host_convergence_protocol { HostEffectDomainProjection, inspect_via_host_effect_projection } +import gunbc.fleet.convergence_fold { + StepInstanceKey, + LegBudget, + LegCompletion, + LegCompletedWithin, + LegDeadlineElapsed, + LegFinishedBeforeItStarted, + LegCompletionUnobserved, + LegCompletedWithinDeadline, + leg_budget, + effect_leg_deadline, + complete_effect_leg, +} +import gunbc.machine_intake_subject { MachineIntakeSubject } + +// THE PRIOR-LIFE BOUNDARY, ITS ARCHIVE ARM (docs/plans/managed-host-untangle.md, cut O1c-2; +// docs/plans/machine-intake-design.md §5). Before anything is cleared, the controller's prior-life +// records are preserved as one immutable content-addressed archive, and a baseline cursor is derived +// FROM that archive. This cut builds only the arm that clears nothing, +// LogsArchivedWithBaselineCursor; LogsArchivedAndCleared is a write to the controller with its own +// admission and operator sign-off, and it has no constructor here. +// +// THE PHASE IS EFFECTFUL, BUT NOT ON THE CONTROLLER. Its reads of the controller are read-only; its +// one effect is the archive WRITE into the intake staging service's content-addressed store +// (gunbc.machine_intake_staging IntakeStagingCapability ContentAddressedArtifactStore), followed by +// an independent re-read of that store by digest. Observe, assess and decide go through +// gunbc.host_convergence_protocol HostEffectDomainProjection; the write and the readback are this +// domain's own, minted into this domain's sealed receipt, because the projection's apply side is the +// open C8 frontier (host_effect_decide_apply_frontier). Nothing here discharges C8: the write is not +// reconciled through gunbc.host_effect_realize host_effect_apply. +// +// THIS CUT IS DRY. The only realization is over gunbc.bmc_model BmcWorld and the dry store below; no +// live controller is read and no live store is written. A live realization lands with its own +// operator go-ahead, and the receipt names the realization it came from so a dry receipt can never +// stand for a live one. + +// ── THE CARRIERS ─────────────────────────────────────────────────────────────────────────────────── + +// The eight prior-life carriers of machine-intake-design §5, one arm each. A carrier is archived as +// its own content-addressed capture, or it is a typed gap; it is never omitted. +type PriorLifeCarrier + = PriorLifeBmcClock + | PriorLifeSelAndEventLogs + | PriorLifeRedfishLogCollections + | PriorLifeAuditAccountEvents + | PriorLifeBootOverride + | PriorLifeVirtualMediaState + | PriorLifePowerState + | PriorLifeSensorSnapshot + +data prior_life_carriers_all: List = [ + PriorLifeBmcClock, + PriorLifeSelAndEventLogs, + PriorLifeRedfishLogCollections, + PriorLifeAuditAccountEvents, + PriorLifeBootOverride, + PriorLifeVirtualMediaState, + PriorLifePowerState, + PriorLifeSensorSnapshot, +] + +fn prior_life_carrier_label(c: PriorLifeCarrier) -> NonEmptyStr { + match c { + PriorLifeBmcClock => "bmc-clock" + PriorLifeSelAndEventLogs => "ipmi-sel" + PriorLifeRedfishLogCollections => "redfish-log-services" + PriorLifeAuditAccountEvents => "account-events" + PriorLifeBootOverride => "boot-override" + PriorLifeVirtualMediaState => "virtual-media" + PriorLifePowerState => "power-state" + PriorLifeSensorSnapshot => "sensor-snapshot" + } +} + +fn prior_life_carrier_eq(a: PriorLifeCarrier, b: PriorLifeCarrier) -> Bool { + (prior_life_carrier_label(c: a) as String) == (prior_life_carrier_label(c: b) as String) +} + +// ── PLATFORM POLICY ──────────────────────────────────────────────────────────────────────────────── + +// WHICH CARRIERS A PLATFORM REQUIRES, AND WHETHER IT ADMITS AN UNCLEARED BOUNDARY. The design admits +// the archive-with-cursor arm "only where platform policy explicitly admits an uncleared append-only +// boundary", so the admission is an authored row per platform. The platform is the cited upstream +// subject the row is about, by declaration, so a row never claims a controller family it has not +// observed. +type UnclearedBoundaryAdmission + = UnclearedBoundaryAdmitted + | UnclearedBoundaryNotAdmitted + +type PriorLifePolicy { + platform: DeclarationRef + required: List + uncleared_boundary: UnclearedBoundaryAdmission +} + +data mt_collins_platform_ref: DeclarationRef = decl_ref(module_path: "extdeps.ampere.mt_collins_product_brief.subject", decl_name: "MtCollinsPublicProductBrief") + +data mt_jade_platform_ref: DeclarationRef = decl_ref(module_path: "extdeps.ocp.mt_jade.subject", decl_name: "MtJadeSpecificationRevision") + +// THE ROWS (warm-crane-577 for the operator, 2026-10-05, reported upward for veto). Mt. Collins and +// Mt. Jade both require ALL EIGHT carriers and admit only the uncleared baseline-cursor arm. A +// required subset would assert, without evidence, that the other carriers are irrelevant -- absence +// is not irrelevance (DESIGN §3d) -- so narrowing a platform's set is a new row with its reason. +// Mt. Jade's row is a requirement, not an observation: it does not depend on the unit's unobserved +// controller family and claims none. +data prior_life_platform_policies: List = [ + PriorLifePolicy { platform: mt_collins_platform_ref, required: prior_life_carriers_all, uncleared_boundary: UnclearedBoundaryAdmitted }, + PriorLifePolicy { platform: mt_jade_platform_ref, required: prior_life_carriers_all, uncleared_boundary: UnclearedBoundaryAdmitted }, +] + +fn prior_life_policy_for(platform: DeclarationRef) -> PriorLifePolicy? { + prior_life_platform_policies |> filter(p => declaration_ref_eq(a: p.platform, b: platform)) |> first() +} + +// ── THE DRY REALIZATION'S WORLD ──────────────────────────────────────────────────────────────────── + +// THE DRY ARCHIVE STORE: the content-addressed store of the intake staging service, as a value. An +// object is its digest and its bytes. It is NOT std.artifact_store ArtifactStore, which is a cache +// provider that evicts least-recently-used rows to a budget: an evidence archive may never evict, so +// realizing it as a cache would let a prior-life record disappear by policy. Whether the store keeps, +// loses or corrupts a write is a world fact the dry store carries, so a write can be lost or corrupted. +type ArchivedObject { + digest: ContentHash + body: NonEmptyStr +} + +type DryArchiveStoreBehaviour + = DryArchiveStoreKeepsWrites + | DryArchiveStoreLosesWrites + | DryArchiveStoreCorruptsWrites + +type DryArchiveStore { + objects: List + behaviour: DryArchiveStoreBehaviour +} + +// WHAT ONE DRY RUN OF THE PHASE READS AND WRITES: the controller as a BmcWorld, the store, the +// observer-clock instant (in milliseconds) at which the run reads the controller and starts the +// write, and the instant the observer clock reads when the write returns. Both instants are labeled +// modeled wherever they land, so neither can be read as a clock read at run time; a write that +// returns before it started is a scenario the leg's own check refuses. +type DryPriorLifeWorld { + bmc: BmcWorld + store: DryArchiveStore + read_at_millis: EpochMs + write_returned_at_millis: EpochMs +} + +data prior_life_dry_realization_name: NonEmptyStr = "gunbc.machine_intake_prior_life_boundary dry realization over gunbc.bmc_model BmcWorld and a dry archive store" as NonEmptyStr + +// THE DRY REALIZATION'S CLOCK, confined to the two functions of this realization that stamp a read +// and a write. +fn dry_prior_life_instant(millis: EpochMs) -> ObserverClockInstant + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_archive_prior_life"), + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_write_archive"), + ] +{ + observer_clock_modeled(millis: millis, realization: prior_life_dry_realization_name) +} + +// ── CAPTURE: what the controller serves for each carrier, its encoding, and the encoding's digest ─── + +// WHAT A CARRIER HELD, TYPED: the controller's own values for that surface, every modeled field kept. +// The archive's bytes, its digest and its baseline cursor are all derived from these payloads and +// nothing else, so the cursor is a function of what the store holds. +type CarrierPayload + = BmcClockPayload { date_time: NonEmptyStr } + | SelPayload { records: List } + | LogServicesPayload { services: List } + | AccountEventsPayload { entries: List } + | BootOverridePayload { boot_override: BmcBootOverride } + | VirtualMediaPayload { members: List } + | PowerStatePayload { power: BmcPower } + | SensorSnapshotPayload { points: List } + +type CarrierGapCause + = CarrierSurfaceUnmodeled {} + +type CarrierCapture + = CarrierCaptured { carrier: PriorLifeCarrier, payload: CarrierPayload } + | CarrierGap { carrier: PriorLifeCarrier, cause: CarrierGapCause } + +fn capture_carrier_of(c: CarrierCapture) -> PriorLifeCarrier { + match c { + CarrierCaptured { carrier: k, payload: _ } => k + CarrierGap { carrier: k, cause: _ } => k + } +} + +// THE ENCODING. RFC 8259 JSON through extdeps.languages.json.emit serialize_json: every string is +// quoted and escaped, every list is framed, every record is an object with fixed member names and +// every closed choice is a member naming its arm, so the encoding is INJECTIVE over the payload -- +// two payloads that differ in any modeled field encode to different bytes. A delimiter-joined text +// was not: a message carrying the delimiter and a newline made two different log populations encode +// identically while their baseline cursors differed (side-chat review of 31ef3dbe8c). +fn arm(name: String, members: List) -> JsonValue { + json_object(members: concat([json_kv(key: "arm", value: json_string(s: name))], members)) +} + +fn optional_text(v: NonEmptyStr?) -> JsonValue { + match v { + Present { value: t } => arm(name: "Present", members: [json_kv(key: "value", value: json_string(s: t as String))]) + Absent => arm(name: "Absent", members: []) + } +} + +fn sel_record_json(r: BmcSelRecord) -> JsonValue { + json_object(members: [ + json_kv(key: "id_hex", value: json_string(s: r.id_hex)), + json_kv(key: "date", value: json_string(s: r.date)), + json_kv(key: "time", value: json_string(s: r.time)), + json_kv(key: "sensor", value: json_string(s: r.sensor)), + json_kv(key: "event", value: json_string(s: r.event)), + json_kv(key: "state", value: json_string(s: r.state)), + ]) +} + +fn log_entry_json(e: RedfishLogEntry) -> JsonValue { + json_object(members: [ + json_kv(key: "id", value: json_int(n: e.id)), + json_kv(key: "severity", value: json_string(s: e.severity as String)), + json_kv(key: "message", value: json_string(s: e.message as String)), + ]) +} + +fn log_service_json(s: RedfishLogService) -> JsonValue { + json_object(members: [ + json_kv(key: "id", value: json_string(s: s.id as String)), + json_kv(key: "entries", value: json_array(elements: map(s.entries, e => log_entry_json(e: e)))), + ]) +} + +fn health_json(h: RedfishHealth) -> JsonValue { + match h { + RedfishHealthOk => arm(name: "Ok", members: []) + RedfishHealthWarning => arm(name: "Warning", members: []) + RedfishHealthCritical => arm(name: "Critical", members: []) + RedfishHealthOther { health: x } => arm(name: "Other", members: [json_kv(key: "health", value: json_string(s: x as String))]) + RedfishHealthUnreported => arm(name: "Unreported", members: []) + } +} + +fn state_json(s: RedfishResourceState) -> JsonValue { + match s { + RedfishStateEnabled => arm(name: "Enabled", members: []) + RedfishStateDisabled => arm(name: "Disabled", members: []) + RedfishStateAbsent => arm(name: "Absent", members: []) + RedfishStateOther { state: x } => arm(name: "Other", members: [json_kv(key: "state", value: json_string(s: x as String))]) + RedfishStateUnreported => arm(name: "Unreported", members: []) + } +} + +fn reading_json(r: RedfishReading) -> JsonValue { + match r { + RedfishReadingValue { whole: n } => arm(name: "Value", members: [json_kv(key: "whole", value: json_int(n: n))]) + RedfishReadingNull => arm(name: "Null", members: []) + RedfishReadingMissing => arm(name: "Missing", members: []) + } +} + +fn kind_json(k: RedfishPointKind) -> JsonValue { + match k { + RedfishTemperatureCelsius => arm(name: "TemperatureCelsius", members: []) + RedfishRotationalRpm => arm(name: "RotationalRpm", members: []) + RedfishOtherReading { reading_type: t } => arm(name: "Other", members: [json_kv(key: "reading_type", value: json_string(s: t as String))]) + } +} + +fn sensor_json(p: RedfishTelemetryPoint) -> JsonValue { + json_object(members: [ + json_kv(key: "name", value: json_string(s: p.name as String)), + json_kv(key: "kind", value: kind_json(k: p.kind)), + json_kv(key: "reading", value: reading_json(r: p.reading)), + json_kv(key: "health", value: health_json(h: p.health)), + json_kv(key: "state", value: state_json(s: p.state)), + ]) +} + +fn connected_via_json(c: RedfishVirtualMediaConnectedVia) -> JsonValue { + match c { + ConnectedViaNotConnected => arm(name: "NotConnected", members: []) + ConnectedViaUri => arm(name: "URI", members: []) + ConnectedViaApplet => arm(name: "Applet", members: []) + ConnectedViaOem => arm(name: "Oem", members: []) + } +} + +// THE LOCATOR, ONE MEMBER PER MODELED COMPONENT: its parent arm with that arm's own ID, and the media +// ID. The rendered resource path is NOT the encoding: it joins the IDs around separators the IDs +// themselves may contain, so two distinct locators can render the same path (side-chat review of +// 5143906158). Every *_json encoder here is structural the same way; none joins fields into a string. +fn locator_json(l: RedfishVirtualMediaLocator) -> JsonValue { + json_object(members: [ + json_kv(key: "parent", value: match l.parent { + UnderManager { manager_id: m } => arm(name: "UnderManager", members: [json_kv(key: "manager_id", value: json_string(s: m as String))]) + UnderSystem { system_id: x } => arm(name: "UnderSystem", members: [json_kv(key: "system_id", value: json_string(s: x as String))]) + }), + json_kv(key: "media_id", value: json_string(s: l.media_id as String)), + ]) +} + +fn uri_json(u: Uri) -> JsonValue { + json_object(members: [ + json_kv(key: "scheme", value: json_string(s: uri_scheme_wire(s: u.scheme) as String)), + json_kv(key: "locator", value: json_string(s: u.locator as String)), + ]) +} + +fn virtual_media_json(v: RedfishVirtualMediaObservation) -> JsonValue { + json_object(members: [ + json_kv(key: "locator", value: locator_json(l: v.locator)), + json_kv(key: "media_types", value: json_array(elements: map(v.media_types, t => json_string(s: redfish_virtual_media_type_wire(t: t) as String)))), + json_kv(key: "connected_via", value: connected_via_json(c: v.connected_via)), + json_kv(key: "inserted", value: json_bool(b: v.inserted)), + json_kv(key: "image", value: match v.image { Present { value: u } => arm(name: "Present", members: [json_kv(key: "value", value: uri_json(u: u))]) Absent => arm(name: "Absent", members: []) }), + ]) +} + +fn payload_json(p: CarrierPayload) -> JsonValue { + match p { + BmcClockPayload { date_time: t } => arm(name: "BmcClock", members: [json_kv(key: "date_time", value: json_string(s: t as String))]) + SelPayload { records: rs } => arm(name: "Sel", members: [json_kv(key: "records", value: json_array(elements: map(rs, r => sel_record_json(r: r))))]) + LogServicesPayload { services: ss } => arm(name: "LogServices", members: [json_kv(key: "services", value: json_array(elements: map(ss, s => log_service_json(s: s))))]) + AccountEventsPayload { entries: es } => arm(name: "AccountEvents", members: [json_kv(key: "entries", value: json_array(elements: map(es, e => log_entry_json(e: e))))]) + BootOverridePayload { boot_override: o } => + arm(name: "BootOverride", members: [json_kv(key: "boot_override", value: match o { BootOverrideNone => arm(name: "None", members: []) BootOverrideCdromEfiNextBoot => arm(name: "CdromEfiNextBoot", members: []) })]) + VirtualMediaPayload { members: vs } => arm(name: "VirtualMedia", members: [json_kv(key: "members", value: json_array(elements: map(vs, v => virtual_media_json(v: v))))]) + PowerStatePayload { power: w } => + arm(name: "PowerState", members: [json_kv(key: "power", value: match w { BmcPowerOn => arm(name: "On", members: []) BmcPowerOff => arm(name: "Off", members: []) })]) + SensorSnapshotPayload { points: ps } => arm(name: "SensorSnapshot", members: [json_kv(key: "points", value: json_array(elements: map(ps, q => sensor_json(p: q))))]) + } +} + +fn capture_json(c: CarrierCapture) -> JsonValue { + match c { + CarrierCaptured { carrier: k, payload: p } => + arm(name: "Captured", members: [json_kv(key: "carrier", value: json_string(s: prior_life_carrier_label(c: k) as String)), json_kv(key: "payload", value: payload_json(p: p))]) + CarrierGap { carrier: k, cause: _ } => + arm(name: "Gap", members: [json_kv(key: "carrier", value: json_string(s: prior_life_carrier_label(c: k) as String)), json_kv(key: "cause", value: arm(name: "SurfaceUnmodeled", members: []))]) + } +} + +// ONE CAPTURE PER CARRIER, FROM THE WORLD. A surface the world does not model is a gap, never an +// empty record; an empty log the world does model is a capture of zero entries. +fn capture_from_world(world: BmcWorld, carrier: PriorLifeCarrier) -> CarrierCapture { + let surfaces = world.record_surfaces + match carrier { + PriorLifeBmcClock => + match surfaces.manager_date_time { + Present { value: t } => CarrierCaptured { carrier: carrier, payload: BmcClockPayload { date_time: t } } + Absent => CarrierGap { carrier: carrier, cause: CarrierSurfaceUnmodeled {} } + } + PriorLifeSelAndEventLogs => CarrierCaptured { carrier: carrier, payload: SelPayload { records: world.sel } } + PriorLifeRedfishLogCollections => + match surfaces.log_services { + Present { value: ss } => CarrierCaptured { carrier: carrier, payload: LogServicesPayload { services: ss } } + Absent => CarrierGap { carrier: carrier, cause: CarrierSurfaceUnmodeled {} } + } + PriorLifeAuditAccountEvents => + match surfaces.account_events { + Present { value: es } => CarrierCaptured { carrier: carrier, payload: AccountEventsPayload { entries: es } } + Absent => CarrierGap { carrier: carrier, cause: CarrierSurfaceUnmodeled {} } + } + PriorLifeBootOverride => CarrierCaptured { carrier: carrier, payload: BootOverridePayload { boot_override: world.boot_override } } + PriorLifeVirtualMediaState => + match surfaces.virtual_media { + Present { value: vs } => CarrierCaptured { carrier: carrier, payload: VirtualMediaPayload { members: vs } } + Absent => CarrierGap { carrier: carrier, cause: CarrierSurfaceUnmodeled {} } + } + PriorLifePowerState => CarrierCaptured { carrier: carrier, payload: PowerStatePayload { power: world.power } } + PriorLifeSensorSnapshot => + match surfaces.sensors { + Present { value: ps } => CarrierCaptured { carrier: carrier, payload: SensorSnapshotPayload { points: ps } } + Absent => CarrierGap { carrier: carrier, cause: CarrierSurfaceUnmodeled {} } + } + } +} + +// ── THE ARCHIVE AND ITS CURSOR ───────────────────────────────────────────────────────────────────── + +// THE CURSOR, DERIVED FROM THE ARCHIVED PAYLOADS AND NOTHING ELSE: the last SEL record id, the last +// entry id of each Redfish log service and of the account-event log, and the archive's own digest. +// The positions are also encoded into the archive bytes, so two archives whose cursors differ cannot +// share a digest. Sealed, and minted only by archive_of. +type LogServiceCursor { + service: NonEmptyStr + final_entry: Int? +} + +type BaselineCursor sole_constructor { + sel_final_record: String? + log_services: List + account_events_final_entry: Int? + archive: ContentHash +} + +// THE ARCHIVE THE PHASE WRITES, sealed: the subject it was read for, every carrier's capture, the +// canonical bytes those captures and the cursor positions encode to, the digest of those bytes, and +// the instant the controller was read. Minted only by archive_of, from a world it captures itself. +type PriorLifeArchive sole_constructor { + subject: MachineIntakeSubject + captures: List + body: NonEmptyStr + digest: ContentHash + read_at: ObserverClockInstant + cursor: BaselineCursor +} + +fn last_of(xs: List) -> T? { + xs.last() +} + +fn int_json(v: Int?) -> JsonValue { + match v { + Present { value: n } => arm(name: "Present", members: [json_kv(key: "value", value: json_int(n: n))]) + Absent => arm(name: "Absent", members: []) + } +} + +// The positions are read from the captured payloads, never from the world beside them. +type CursorPositions { + sel_final_record: String? + log_services: List + account_events_final_entry: Int? +} + +fn cursor_positions_of(captures: List) -> CursorPositions { + fold(captures, init: CursorPositions { sel_final_record: none, log_services: [], account_events_final_entry: none }, f: (acc, c) => match c { + CarrierGap { carrier: _, cause: _ } => acc + CarrierCaptured { carrier: _, payload: p } => + match p { + SelPayload { records: rs } => + CursorPositions { sel_final_record: match last_of(xs: rs) { Present { value: r } => Present { value: r.id_hex } Absent => none }, log_services: acc.log_services, account_events_final_entry: acc.account_events_final_entry } + LogServicesPayload { services: ss } => + CursorPositions { sel_final_record: acc.sel_final_record, log_services: map(ss, s => LogServiceCursor { service: s.id, final_entry: match last_of(xs: s.entries) { Present { value: e } => Present { value: e.id } Absent => none } }), account_events_final_entry: acc.account_events_final_entry } + AccountEventsPayload { entries: es } => + CursorPositions { sel_final_record: acc.sel_final_record, log_services: acc.log_services, account_events_final_entry: match last_of(xs: es) { Present { value: e } => Present { value: e.id } Absent => none } } + BmcClockPayload { date_time: _ } => acc + BootOverridePayload { boot_override: _ } => acc + VirtualMediaPayload { members: _ } => acc + PowerStatePayload { power: _ } => acc + SensorSnapshotPayload { points: _ } => acc + } + }) +} + +fn positions_json(p: CursorPositions) -> JsonValue { + json_object(members: [ + json_kv(key: "sel_final_record", value: match p.sel_final_record { Present { value: id } => optional_text(v: Present { value: id as NonEmptyStr }) Absent => optional_text(v: none) }), + json_kv(key: "log_services", value: json_array(elements: map(p.log_services, c => json_object(members: [json_kv(key: "service", value: json_string(s: c.service as String)), json_kv(key: "final_entry", value: int_json(v: c.final_entry))])))), + json_kv(key: "account_events_final_entry", value: int_json(v: p.account_events_final_entry)), + ]) +} + +// THE ARCHIVE OF A WORLD: every carrier captured from that world here, the bytes encoded from the +// subject, those captures and the cursor positions they determine, and the cursor read from the same +// captures. Confined to observe_prior_life, so no caller can pair a subject with captures read +// elsewhere. +fn archive_of(subject: MachineIntakeSubject, world: BmcWorld, read_at: ObserverClockInstant) -> PriorLifeArchive + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "observe_prior_life"), + ] +{ + let captures = map(prior_life_carriers_all, c => capture_from_world(world: world, carrier: c)) + let positions = cursor_positions_of(captures: captures) + let body = serialize_json(v: json_object(members: [ + json_kv(key: "archive", value: json_string(s: "gunbc.machine_intake_prior_life_boundary prior-life archive v1")), + json_kv(key: "unit_key", value: json_string(s: (subject.subject.unit_key as NonEmptyStr) as String)), + json_kv(key: "attempt", value: json_string(s: (subject.attempt_id as NonEmptyStr) as String)), + json_kv(key: "captures", value: json_array(elements: map(captures, c => capture_json(c: c)))), + json_kv(key: "cursor", value: positions_json(p: positions)), + ])) as NonEmptyStr + let digest = content_hash_of_value(value: body) + PriorLifeArchive { + subject: subject, + captures: captures, + body: body, + digest: digest, + read_at: read_at, + cursor: BaselineCursor { + sel_final_record: positions.sel_final_record, + log_services: positions.log_services, + account_events_final_entry: positions.account_events_final_entry, + archive: digest, + }, + } +} + +fn prior_life_archive_digest(a: PriorLifeArchive) -> ContentHash { + a.digest +} + +fn prior_life_archive_body(a: PriorLifeArchive) -> NonEmptyStr { + a.body +} + +fn prior_life_archive_cursor(a: PriorLifeArchive) -> BaselineCursor { + a.cursor +} + +fn baseline_cursor_sel_final_record(c: BaselineCursor) -> String? { + c.sel_final_record +} + +fn baseline_cursor_log_services(c: BaselineCursor) -> List { + c.log_services +} + +fn baseline_cursor_archive(c: BaselineCursor) -> ContentHash { + c.archive +} + +// ── OBSERVE, ASSESS, DECIDE (through the canonical projection) ─────────────────────────────────── + +// What the phase reads: every carrier's capture from the controller, and whether the store already +// holds an archive object at the digest those captures make (the store read is part of the +// observation, so an archive already written and read back is a Noop and is not written twice). +type PriorLifeObservation { + archive: PriorLifeArchive + held: ArchivedObject? +} + +type PriorLifeRequest { + world: DryPriorLifeWorld + subject: MachineIntakeSubject + read_at: ObserverClockInstant +} + +type PriorLifeGoal { + policy: PriorLifePolicy +} + +type PriorLifeAssessRefusal + = RequiredCarrierNotArchivable { carrier: PriorLifeCarrier, cause: CarrierGapCause } + | UnclearedBoundaryNotAdmittedByPolicy { platform: DeclarationRef } + +type PriorLifeDeviation + = ArchiveNotHeldByStore { digest: ContentHash } + +// THE ARCHIVE PLAN, sealed to this module: the archive to write. Minted only by write_then_read_back, +// which dry_archive_prior_life reaches only on an Apply decision, so a plan exists only over an +// assessment that found every required carrier captured and the store not holding the archive. +type PriorLifeArchivePlan sole_constructor { + archive: PriorLifeArchive +} + +fn store_object_at(store: DryArchiveStore, digest: ContentHash) -> ArchivedObject? { + store.objects |> filter(o => content_hash_equal(left: o.digest, right: digest)) |> first() +} + +fn observe_prior_life(key: StepInstanceKey, request: PriorLifeRequest) -> ObservationAttempt + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "prior_life_projection"), + ] +{ + let archive = archive_of(subject: request.subject, world: request.world.bmc, read_at: request.read_at) + ObservationEstablished { observed: PriorLifeObservation { archive: archive, held: store_object_at(store: request.world.store, digest: archive.digest) } } +} + +fn first_required_gap(policy: PriorLifePolicy, captures: List) -> PriorLifeAssessRefusal? { + fold(policy.required, init: none, f: (acc, req) => match acc { + Present { value: r } => Present { value: r } + Absent => + match captures |> filter(c => prior_life_carrier_eq(a: capture_carrier_of(c: c), b: req)) |> first() { + Absent => Present { value: RequiredCarrierNotArchivable { carrier: req, cause: CarrierSurfaceUnmodeled {} } } + Present { value: c } => + match c { + CarrierGap { carrier: k, cause: why } => Present { value: RequiredCarrierNotArchivable { carrier: k, cause: why } } + CarrierCaptured { carrier: _, payload: _ } => none + } + } + }) +} + +// THE CLASSIFIER OVER SUPPLIED VALUES: the refusal a policy gives a set of captures, or none. Pure, +// so every arm is exercisable; its production consumer is assess_prior_life below, over captures read +// from the world and the policy row selected for the unit's platform. +fn classify_prior_life_policy(policy: PriorLifePolicy, captures: List) -> PriorLifeAssessRefusal? { + match policy.uncleared_boundary { + UnclearedBoundaryNotAdmitted => Present { value: UnclearedBoundaryNotAdmittedByPolicy { platform: policy.platform } } + UnclearedBoundaryAdmitted => first_required_gap(policy: policy, captures: captures) + } +} + +// SATISFIED only by an object the store already holds at the archive's digest whose bytes are the +// archive's bytes; an archive the store does not hold is a deviation the write remedies. +fn assess_prior_life(goal: PriorLifeGoal, observed: PriorLifeObservation) -> GoalAssessment { + match classify_prior_life_policy(policy: goal.policy, captures: observed.archive.captures) { + Present { value: r } => GoalAssessmentRefused { cause: r } + Absent => + match observed.held { + Present { value: o } => + if (o.body as String) == (observed.archive.body as String) { + GoalSatisfied { evidence: o } + } else { + GoalDiverged { deviations: FreeSemigroup { head: ArchiveNotHeldByStore { digest: observed.archive.digest }, tail: Empty } } + } + Absent => GoalDiverged { deviations: FreeSemigroup { head: ArchiveNotHeldByStore { digest: observed.archive.digest }, tail: Empty } } + } + } +} + +fn decide_prior_life(assessment: GoalAssessment) -> UpsertDecision { + match assessment { + GoalSatisfied { evidence: _ } => Noop + GoalDiverged { deviations: _ } => Apply { plan: PriorLifeArchiveDue {} } + GoalIndeterminate { known_deviations: _, unknowns: _ } => Refuse { reason: "the prior-life archive is indeterminate over what was read" as NonEmptyStr } + GoalAssessmentRefused { cause: _ } => Refuse { reason: "the prior-life archive is refused by its platform policy" as NonEmptyStr } + } +} + +// The projection's plan is only that an archive is due; the archive itself is the observation's, so +// the plan the write carries is bound to exactly what was read. +type PriorLifeArchiveDue {} + +fn prior_life_projection() -> HostEffectDomainProjection { + HostEffectDomainProjection { + observe: observe_prior_life, + assess: assess_prior_life, + decide: decide_prior_life, + } +} + +// ── APPLY: the write, its deadline, and the independent readback ─────────────────────────────────── + +data prior_life_archive_write_leg: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_write_archive") + +// THE WRITE LEG'S BUDGET: thirty seconds for one archive object into the staging store. The one +// function that declares it, admitted by gunbc.fleet.convergence_fold leg_budget. +fn prior_life_archive_write_budget() -> LegBudget { + leg_budget(leg: prior_life_archive_write_leg, budget: positive_millisecond(count: PositiveMeasureSuccessor { predecessor: 29999 })) +} + +// WHAT THE WRITE RETURNED, sealed: the digest it was asked to store. A write's return is not its +// completion; only the readback below grounds that. +type ArchiveWriteReceipt sole_constructor { + digest: ContentHash + completion: LegCompletion +} + +// THE INDEPENDENT READBACK, sealed: the store re-read at the written digest, its bytes recomputed to +// that digest and equal to the archive's bytes. Minted only by read_back_archive. +type ArchiveReadBack sole_constructor { + digest: ContentHash + held: ArchivedObject +} + +type DryArchiveWrite { + store: DryArchiveStore + receipt: ArchiveWriteReceipt +} + +fn dry_write_archive(store: DryArchiveStore, plan: PriorLifeArchivePlan, budget: LegBudget, started_millis: EpochMs, returned_millis: EpochMs) -> DryArchiveWrite + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "write_then_read_back"), + ] +{ + let deadline = effect_leg_deadline(budget: budget, started: dry_prior_life_instant(millis: started_millis)) + let finished = dry_prior_life_instant(millis: returned_millis) + let written = match store.behaviour { + DryArchiveStoreKeepsWrites => concat(store.objects, [ArchivedObject { digest: plan.archive.digest, body: plan.archive.body }]) + DryArchiveStoreLosesWrites => store.objects + DryArchiveStoreCorruptsWrites => concat(store.objects, [ArchivedObject { digest: plan.archive.digest, body: join([plan.archive.body as String, "corrupted"], "\n") as NonEmptyStr }]) + } + DryArchiveWrite { + store: DryArchiveStore { objects: written, behaviour: store.behaviour }, + receipt: ArchiveWriteReceipt { digest: plan.archive.digest, completion: complete_effect_leg(deadline: deadline, finished: ObserverClockObserved { instant: finished }) }, + } +} + +type ArchiveReadBackStanding + = ArchiveReadBackHeld { readback: ArchiveReadBack } + | ArchiveReadBackAbsent { digest: ContentHash } + | ArchiveReadBackDiffers { digest: ContentHash, read: ContentHash } + +fn read_back_archive(store: DryArchiveStore, archive: PriorLifeArchive) -> ArchiveReadBackStanding + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_archive_prior_life"), + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "write_then_read_back"), + ] +{ + match store_object_at(store: store, digest: archive.digest) { + Absent => ArchiveReadBackAbsent { digest: archive.digest } + Present { value: o } => { + let recomputed = content_hash_of_value(value: o.body) + if content_hash_equal(left: recomputed, right: archive.digest) && (o.body as String) == (archive.body as String) { + ArchiveReadBackHeld { readback: ArchiveReadBack { digest: archive.digest, held: o } } + } else { + ArchiveReadBackDiffers { digest: archive.digest, read: recomputed } + } + } + } +} + +// ── THE RECEIPT ──────────────────────────────────────────────────────────────────────────────────── + +// HOW THE ARCHIVE CAME TO BE HELD: already held when the phase read the store (no write), or written +// by this run within its leg's deadline. +type PriorLifeApplication + = ArchiveAlreadyHeld + | ArchiveWritten { write: ArchiveWriteReceipt, within: LegCompletedWithinDeadline } + +// THE ONE ESTABLISHED ARM IN THIS CUT. LogsArchivedAndCleared has no constructor. +type PriorLifeBoundaryArm + = LogsArchivedWithBaselineCursor { cursor: BaselineCursor } + +// THE PHASE RECEIPT, SEALED: subject + phase + the consumed identity instance + the archive written +// + how it was written + the independent post-read + the realization it came from. Minted only by +// dry_archive_prior_life, after the readback. +type PriorLifeBoundaryEstablished sole_constructor { + key: StepInstanceKey + consumed_identity: StepInstanceKey + subject: MachineIntakeSubject + policy: PriorLifePolicy + archive: PriorLifeArchive + application: PriorLifeApplication + readback: ArchiveReadBack + boundary: PriorLifeBoundaryArm + realization: NonEmptyStr +} + +fn prior_life_receipt_key(r: PriorLifeBoundaryEstablished) -> StepInstanceKey { + r.key +} + +fn prior_life_receipt_consumed_identity(r: PriorLifeBoundaryEstablished) -> StepInstanceKey { + r.consumed_identity +} + +fn prior_life_receipt_archive(r: PriorLifeBoundaryEstablished) -> PriorLifeArchive { + r.archive +} + +fn prior_life_receipt_application(r: PriorLifeBoundaryEstablished) -> PriorLifeApplication { + r.application +} + +fn prior_life_receipt_boundary(r: PriorLifeBoundaryEstablished) -> PriorLifeBoundaryArm { + r.boundary +} + +fn prior_life_receipt_realization(r: PriorLifeBoundaryEstablished) -> NonEmptyStr { + r.realization +} + +// ── THE PHASE ────────────────────────────────────────────────────────────────────────────────────── + +// REFUSED: nothing was written. The policy row is absent, the policy refuses, or the decision refused. +type PriorLifeRefusal + = PriorLifePolicyAbsent { platform: DeclarationRef } + | PriorLifeAssessmentRefused { cause: PriorLifeAssessRefusal } + | PriorLifeObservationRefused { cause: NonEmptyStr } + | PriorLifeDecisionRefused { reason: NonEmptyStr } + | PriorLifeSatisfiedWithoutEvidence + +// INCOMPLETE: the write was attempted and its completion is not grounded. Each arm carries the +// write's own receipt, because the store may now hold something. +type PriorLifeIncomplete + = ArchiveWriteLegNotCompleted { write: ArchiveWriteReceipt, completion: LegCompletion } + | ArchiveWrittenButNotReadBack { write: ArchiveWriteReceipt, digest: ContentHash } + | ArchiveReadBackDiffersFromWrite { write: ArchiveWriteReceipt, digest: ContentHash, read: ContentHash } + +type PriorLifeArchiveOutcome + = PriorLifeArchiveEstablished { receipt: PriorLifeBoundaryEstablished } + | PriorLifeArchiveRefused { cause: PriorLifeRefusal } + | PriorLifeArchiveIncomplete { cause: PriorLifeIncomplete } + +// ONE DRY RUN OF THE PHASE AND THE STORE IT LEAVES, so a refusal can be shown to have written nothing. +type DryPriorLifeStep { + outcome: PriorLifeArchiveOutcome + store: DryArchiveStore +} + +fn established(key: StepInstanceKey, consumed: StepInstanceKey, subject: MachineIntakeSubject, policy: PriorLifePolicy, archive: PriorLifeArchive, application: PriorLifeApplication, readback: ArchiveReadBack) -> PriorLifeArchiveOutcome + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_archive_prior_life"), + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "write_then_read_back"), + ] +{ + PriorLifeArchiveEstablished { + receipt: PriorLifeBoundaryEstablished { + key: key, + consumed_identity: consumed, + subject: subject, + policy: policy, + archive: archive, + application: application, + readback: readback, + boundary: LogsArchivedWithBaselineCursor { cursor: archive.cursor }, + realization: prior_life_dry_realization_name, + }, + } +} + +// THE WRITE AND ITS READBACK. The leg's completion is checked first: a write whose clock says it ran +// past its deadline, finished before it started, or could not be timed is incomplete whatever the +// store now holds. Then the store is re-read by digest, independently of what the write returned. +fn write_then_read_back(key: StepInstanceKey, consumed: StepInstanceKey, subject: MachineIntakeSubject, policy: PriorLifePolicy, archive: PriorLifeArchive, world: DryPriorLifeWorld) -> DryPriorLifeStep + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_archive_prior_life"), + ] +{ + let written = dry_write_archive(store: world.store, plan: PriorLifeArchivePlan { archive: archive }, budget: prior_life_archive_write_budget(), started_millis: world.read_at_millis, returned_millis: world.write_returned_at_millis) + let outcome = match written.receipt.completion { + LegDeadlineElapsed { deadline: _, finished: _ } => PriorLifeArchiveIncomplete { cause: ArchiveWriteLegNotCompleted { write: written.receipt, completion: written.receipt.completion } } + LegFinishedBeforeItStarted { deadline: _, finished: _ } => PriorLifeArchiveIncomplete { cause: ArchiveWriteLegNotCompleted { write: written.receipt, completion: written.receipt.completion } } + LegCompletionUnobserved { deadline: _, detail: _ } => PriorLifeArchiveIncomplete { cause: ArchiveWriteLegNotCompleted { write: written.receipt, completion: written.receipt.completion } } + LegCompletedWithin { completed: within } => + match read_back_archive(store: written.store, archive: archive) { + ArchiveReadBackAbsent { digest: d } => PriorLifeArchiveIncomplete { cause: ArchiveWrittenButNotReadBack { write: written.receipt, digest: d } } + ArchiveReadBackDiffers { digest: d, read: r } => PriorLifeArchiveIncomplete { cause: ArchiveReadBackDiffersFromWrite { write: written.receipt, digest: d, read: r } } + ArchiveReadBackHeld { readback: rb } => + established(key: key, consumed: consumed, subject: subject, policy: policy, archive: archive, application: ArchiveWritten { write: written.receipt, within: within }, readback: rb) + } + } + DryPriorLifeStep { outcome: outcome, store: written.store } +} + +// THE PHASE, DRY. The platform's policy row is selected before the step (DESIGN §3d) by the caller's +// platform; the controller is observed and assessed through the projection; Noop needs the store's +// own held object, Apply writes and reads back, and every refusal writes nothing. Confined to the +// arrival convergence's step and to the Bool claims of its witness that supply its inputs, so no +// caller can mint this receipt for a subject or an identity instance of its own choosing. +fn dry_archive_prior_life( + key: StepInstanceKey, + consumed_identity: StepInstanceKey, + subject: MachineIntakeSubject, + platform: DeclarationRef, + world: DryPriorLifeWorld, +) -> DryPriorLifeStep + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_only_the_sel_final_record_with_the_other_carriers_absent_is_not_established"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_one_unmodeled_carrier_is_a_typed_gap_that_refuses"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_a_policy_refusal_writes_nothing"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_an_archive_already_held_is_a_noop_and_is_not_written_twice"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_a_lost_corrupted_or_late_write_is_incomplete_not_refused"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_the_baseline_cursor_is_derived_from_the_archive_it_was_read_from"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_two_log_populations_that_a_delimiter_join_conflated_archive_distinctly"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_virtual_media_connected_via_and_media_types_are_archived"), + decl_ref(module_path: "test.claim.machine_intake_prior_life_boundary_witness", decl_name: "w_two_locators_that_render_one_resource_path_archive_distinctly"), + ] +{ + match prior_life_policy_for(platform: platform) { + Absent => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifePolicyAbsent { platform: platform } }, store: world.store } + Present { value: policy } => { + let projection = prior_life_projection() + let request = PriorLifeRequest { world: world, subject: subject, read_at: dry_prior_life_instant(millis: world.read_at_millis) } + match inspect_via_host_effect_projection(subject: key, goal: PriorLifeGoal { policy: policy }, request: request, projection: projection) { + GoalObservationRefused { subject: _, goal: _, request: _, cause: c } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeObservationRefused { cause: c } }, store: world.store } + GoalInspected { subject: _, goal: _, request: _, observed: o, assessment: a } => + match projection.decide(a) { + Refuse { reason: why } => + match a { + GoalAssessmentRefused { cause: c } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeAssessmentRefused { cause: c } }, store: world.store } + GoalSatisfied { evidence: _ } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeDecisionRefused { reason: why } }, store: world.store } + GoalDiverged { deviations: _ } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeDecisionRefused { reason: why } }, store: world.store } + GoalIndeterminate { known_deviations: _, unknowns: _ } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeDecisionRefused { reason: why } }, store: world.store } + } + Noop => + match read_back_archive(store: world.store, archive: o.archive) { + ArchiveReadBackHeld { readback: rb } => + DryPriorLifeStep { outcome: established(key: key, consumed: consumed_identity, subject: subject, policy: policy, archive: o.archive, application: ArchiveAlreadyHeld, readback: rb), store: world.store } + ArchiveReadBackAbsent { digest: _ } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeSatisfiedWithoutEvidence }, store: world.store } + ArchiveReadBackDiffers { digest: _, read: _ } => DryPriorLifeStep { outcome: PriorLifeArchiveRefused { cause: PriorLifeSatisfiedWithoutEvidence }, store: world.store } + } + Apply { plan: _ } => write_then_read_back(key: key, consumed: consumed_identity, subject: subject, policy: policy, archive: o.archive, world: world) + } + } + } + } +} diff --git a/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag index de8fe3c71ad..ea735d8e396 100644 --- a/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag @@ -17,7 +17,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // outside its module; this witness hands the source to the compiler through the diagnostic-census // harness and requires SoleConstructorViolation at each SUBJECT by name. The class-scoped control shows // a clean source reading the same modules through their real producers emits none. -data forged_probe_source: String = "module probe_arrival_converge_forged\n\nimport std.types { Int, List, NonEmptyStr, String }\nimport std.decl_ref { decl_ref }\nimport gunbc.machine_intake_phase { Arrival, AccessDiscover, IntakePhase }\nimport gunbc.machine_intake_subject { MachineIntakeSubject, BoardSerialObservation, AssemblyManifest, UnitKey }\nimport gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding }\nimport gunbc.machine_intake_mtjade1_factory_network { ObservedBmcNetwork }\nimport gunbc.machine_intake_mtjade1_access_observation {\n CurrentManagerRead, RecordedManagerIdentityObservation, ControllerClockReading, current_manager_read_of,\n FruRead, SmbiosRead, FruIdentityFields, RecordedFruObservation, RecordedSmbiosObservation, SolSessionAttribution,\n}\nimport gunbc.fleet.convergence_fold {\n AdmittedConvergencePlan, RankedStep, StepInstanceKey, ConvergenceRunId, StepSubjectKey, ConvergenceOrderAuthority, ConvergencePlanningAuthority,\n ConvergenceReceiptProjection, ConvergenceRunLedger, ConvergedRun, StepInstanceStanding,\n convergence_planning_authority, convergence_receipt_projection,\n}\nimport gunbc.machine_intake_arrival_converge {\n AccessDiscoverEstablished, IdentityBoundProvisional, ReadOnlyPhaseRemedy, AccessObservation,\n IdentityBindInputs, ArrivalStepReceipt, ArrivalStepRefusal, BoardSerialAgreement,\n}\n\nfn forged_access(key: StepInstanceKey, access: AccessObservation, route: BmcRotationRouteStanding) -> AccessDiscoverEstablished {\n AccessDiscoverEstablished { key: key, access: access, route: route }\n}\n\nfn forged_identity(key: StepInstanceKey, subject: MachineIntakeSubject) -> IdentityBoundProvisional {\n IdentityBoundProvisional { key: key, consumed_access: key, subject: subject }\n}\n\nfn forged_plan(steps: List>, key: StepInstanceKey) -> AdmittedConvergencePlan {\n AdmittedConvergencePlan { authority: key.step_identity, steps: steps }\n}\n\nfn forged_remedy() -> ReadOnlyPhaseRemedy {\n ReadOnlyPhaseRemedy { phase: AccessDiscover }\n}\n\nfn any_rank(phase: IntakePhase) -> Int? {\n Present { value: 0 }\n}\n\nfn authored_order() -> ConvergenceOrderAuthority {\n ConvergenceOrderAuthority { authority: decl_ref(module_path: \"gunbc.machine_intake_phase\", decl_name: \"arrival_phases_all\"), rank_of: any_rank }\n}\n\nfn forged_planning_literal() -> ConvergencePlanningAuthority {\n ConvergencePlanningAuthority { order: authored_order() }\n}\n\nfn forged_planning_via_mint() -> ConvergencePlanningAuthority {\n convergence_planning_authority(order: authored_order())\n}\n\nfn rekey(r: ArrivalStepReceipt) -> StepInstanceKey {\n StepInstanceKey { run: \"forged\" as ConvergenceRunId, step_identity: decl_ref(module_path: \"gunbc.machine_intake_arrival_converge\", decl_name: \"access_discover\"), subject: \"mtjade1\" as StepSubjectKey }\n}\n\nfn consumed_nothing(r: ArrivalStepReceipt) -> List {\n []\n}\n\nfn forged_projection_literal() -> ConvergenceReceiptProjection {\n ConvergenceReceiptProjection { key_of: rekey, consumed_of: consumed_nothing }\n}\n\nfn forged_projection_via_mint() -> ConvergenceReceiptProjection {\n convergence_receipt_projection(key_of: rekey, consumed_of: consumed_nothing)\n}\n\nfn forged_ledger(key: StepInstanceKey, instances: List>) -> ConvergenceRunLedger {\n ConvergenceRunLedger { run: key.run, subject: key.subject, order_authority: key.step_identity, instances: instances }\n}\n\nfn forged_converged_run(ledger: ConvergenceRunLedger) -> ConvergedRun {\n ConvergedRun { ledger: ledger }\n}\n\nfn forged_manager_read(identity: RecordedManagerIdentityObservation, clock: ControllerClockReading) -> CurrentManagerRead {\n CurrentManagerRead { identity: identity, controller_clock: clock }\n}\n\nfn forged_manager_read_via_mint(content: String, endpoint: ObservedBmcNetwork) -> CurrentManagerRead {\n current_manager_read_of(content: content, expected_sha256: \"00\" as NonEmptyStr, endpoint: endpoint, link: none, capture_path: \"forged\" as NonEmptyStr)\n}\n\nfn forged_identity_inputs(fru: FruRead, smbios: SmbiosRead, units: List) -> IdentityBindInputs {\n IdentityBindInputs { fru: fru, smbios: smbios, other_units: units }\n}\n\nfn forged_fru(fields: FruIdentityFields) -> RecordedFruObservation {\n RecordedFruObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", fields: fields }\n}\n\nfn forged_smbios(attribution: SolSessionAttribution) -> RecordedSmbiosObservation {\n RecordedSmbiosObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", sol_session: attribution, serial: \"B810301000412080005AJ0C1\" }\n}\n\nfn forged_agreement(fru: RecordedFruObservation, smbios: RecordedSmbiosObservation) -> BoardSerialAgreement {\n BoardSerialAgreement { fru: fru, smbios: smbios, serial: \"B810301000412080005AJ0C1\" }\n}\n" +data forged_probe_source: String = "module probe_arrival_converge_forged\n\nimport std.types { Int, List, NonEmptyStr, String }\nimport std.decl_ref { decl_ref }\nimport gunbc.machine_intake_phase { Arrival, AccessDiscover, IntakePhase }\nimport gunbc.machine_intake_subject { MachineIntakeSubject, BoardSerialObservation, AssemblyManifest, UnitKey }\nimport gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding }\nimport gunbc.machine_intake_mtjade1_factory_network { ObservedBmcNetwork }\nimport gunbc.machine_intake_mtjade1_access_observation {\n CurrentManagerRead, RecordedManagerIdentityObservation, ControllerClockReading, current_manager_read_of,\n FruRead, SmbiosRead, FruIdentityFields, RecordedFruObservation, RecordedSmbiosObservation, SolSessionAttribution,\n}\nimport gunbc.fleet.convergence_fold {\n AdmittedConvergencePlan, RankedStep, StepInstanceKey, ConvergenceRunId, StepSubjectKey, ConvergenceOrderAuthority, ConvergencePlanningAuthority,\n ConvergenceReceiptProjection, ConvergenceRunLedger, ConvergedRun, StepInstanceStanding,\n convergence_planning_authority, convergence_receipt_projection,\n}\nimport gunbc.machine_intake_arrival_converge {\n AccessDiscoverEstablished, IdentityBoundProvisional, ReadOnlyPhaseRemedy, AccessObservation,\n IdentityBindInputs, ArrivalStepReceipt, ArrivalStepRefusal, ArrivalStepIncomplete, BoardSerialAgreement,\n}\n\nfn forged_access(key: StepInstanceKey, access: AccessObservation, route: BmcRotationRouteStanding) -> AccessDiscoverEstablished {\n AccessDiscoverEstablished { key: key, access: access, route: route }\n}\n\nfn forged_identity(key: StepInstanceKey, subject: MachineIntakeSubject) -> IdentityBoundProvisional {\n IdentityBoundProvisional { key: key, consumed_access: key, subject: subject }\n}\n\nfn forged_plan(steps: List>, key: StepInstanceKey) -> AdmittedConvergencePlan {\n AdmittedConvergencePlan { authority: key.step_identity, steps: steps }\n}\n\nfn forged_remedy() -> ReadOnlyPhaseRemedy {\n ReadOnlyPhaseRemedy { phase: AccessDiscover }\n}\n\nfn any_rank(phase: IntakePhase) -> Int? {\n Present { value: 0 }\n}\n\nfn authored_order() -> ConvergenceOrderAuthority {\n ConvergenceOrderAuthority { authority: decl_ref(module_path: \"gunbc.machine_intake_phase\", decl_name: \"arrival_phases_all\"), rank_of: any_rank }\n}\n\nfn forged_planning_literal() -> ConvergencePlanningAuthority {\n ConvergencePlanningAuthority { order: authored_order() }\n}\n\nfn forged_planning_via_mint() -> ConvergencePlanningAuthority {\n convergence_planning_authority(order: authored_order())\n}\n\nfn rekey(r: ArrivalStepReceipt) -> StepInstanceKey {\n StepInstanceKey { run: \"forged\" as ConvergenceRunId, step_identity: decl_ref(module_path: \"gunbc.machine_intake_arrival_converge\", decl_name: \"access_discover\"), subject: \"mtjade1\" as StepSubjectKey }\n}\n\nfn consumed_nothing(r: ArrivalStepReceipt) -> List {\n []\n}\n\nfn forged_projection_literal() -> ConvergenceReceiptProjection {\n ConvergenceReceiptProjection { key_of: rekey, consumed_of: consumed_nothing }\n}\n\nfn forged_projection_via_mint() -> ConvergenceReceiptProjection {\n convergence_receipt_projection(key_of: rekey, consumed_of: consumed_nothing)\n}\n\nfn forged_ledger(key: StepInstanceKey, instances: List>) -> ConvergenceRunLedger {\n ConvergenceRunLedger { run: key.run, subject: key.subject, order_authority: key.step_identity, instances: instances }\n}\n\nfn forged_converged_run(ledger: ConvergenceRunLedger) -> ConvergedRun {\n ConvergedRun { ledger: ledger }\n}\n\nfn forged_manager_read(identity: RecordedManagerIdentityObservation, clock: ControllerClockReading) -> CurrentManagerRead {\n CurrentManagerRead { identity: identity, controller_clock: clock }\n}\n\nfn forged_manager_read_via_mint(content: String, endpoint: ObservedBmcNetwork) -> CurrentManagerRead {\n current_manager_read_of(content: content, expected_sha256: \"00\" as NonEmptyStr, endpoint: endpoint, link: none, capture_path: \"forged\" as NonEmptyStr)\n}\n\nfn forged_identity_inputs(fru: FruRead, smbios: SmbiosRead, units: List) -> IdentityBindInputs {\n IdentityBindInputs { fru: fru, smbios: smbios, other_units: units }\n}\n\nfn forged_fru(fields: FruIdentityFields) -> RecordedFruObservation {\n RecordedFruObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", fields: fields }\n}\n\nfn forged_smbios(attribution: SolSessionAttribution) -> RecordedSmbiosObservation {\n RecordedSmbiosObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", sol_session: attribution, serial: \"B810301000412080005AJ0C1\" }\n}\n\nfn forged_agreement(fru: RecordedFruObservation, smbios: RecordedSmbiosObservation) -> BoardSerialAgreement {\n BoardSerialAgreement { fru: fru, smbios: smbios, serial: \"B810301000412080005AJ0C1\" }\n}\n" data harness_control_source: String = "module probe_arrival_converge_harness_control\nimport gunbc.fleet.convergence_fold { ConvergencePlanAdmission, admit_convergence_plan }\nimport gunbc.machine_intake_phase { IntakePhase }\nimport gunbc.machine_intake_arrival_converge { arrival_planning_authority, arrival_receipt_projection, ArrivalStepReceipt }\nimport gunbc.fleet.convergence_fold { ConvergenceReceiptProjection }\nimport gunbc.machine_intake_mtjade1_access_observation { CurrentManagerRead, read_mtjade1_current_manager_read }\nfn admission() -> ConvergencePlanAdmission { admit_convergence_plan(planning: arrival_planning_authority(), steps: []) }\nfn projection() -> ConvergenceReceiptProjection { arrival_receipt_projection() }\nfn read() -> CurrentManagerRead { read_mtjade1_current_manager_read() }\n" diff --git a/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag index 2df668ae98f..695ef32d370 100644 --- a/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag @@ -32,18 +32,26 @@ import gunbc.fleet.convergence_fold { ConvergenceRunId, StepSubjectKey, StepInstanceKey, ConvergenceStep, StepPrecondition, SameSubject, ConvergencePlanAdmission, ConvergencePlanAdmitted, ConvergencePlanRefused, ConvergencePlanRefusal, StepMissingFromCensus, StepDuplicatedInCensus, StepRankDisagreesWithAuthority, PreconditionUnknown, - StepOutcome, StepEstablished, StepRefused, - RunConverged, RunStopped, RunOutcomesRefused, OutcomeDuplicated, - InstanceConverged, InstanceRefused, InstanceNotReached, + StepOutcome, StepEstablished, StepRefused, StepIncomplete, + RunConverged, RunStopped, RunIncomplete, RunOutcomesRefused, OutcomeDuplicated, + InstanceConverged, InstanceRefused, InstanceIncomplete, InstanceNotReached, DomainRefused, PreconditionUnmet, StepOutcomeAbsent, ConvergenceRunVerdict, StepInstanceStanding, admit_convergence_plan, classify_convergence_plan, PlanClassifiedAdmissible, PlanClassifiedRefused, ConvergenceReceiptProjection, convergence_receipt_projection, fold_convergence_run, step_instance_key, step_outcome_receipt, step_outcome_refusal, } +import gunbc.machine_intake_prior_life_boundary { + DryPriorLifeWorld, DryArchiveStore, DryArchiveStoreLosesWrites, ArchiveWrittenButNotReadBack, ArchiveWritten, LogsArchivedWithBaselineCursor, + mt_jade_platform_ref, prior_life_receipt_archive, prior_life_receipt_application, prior_life_receipt_boundary, prior_life_receipt_realization, + prior_life_receipt_consumed_identity, prior_life_archive_digest, baseline_cursor_archive, baseline_cursor_sel_final_record, +} +import std.content_hash { content_hash_equal } +import test.claim.machine_intake_prior_life_boundary_witness { prior_life_minimal_dry_world } import gunbc.machine_intake_arrival_converge { ArrivalPrefixVerdict, ArrivalRunFolded, ArrivalPlanRefused, ArrivalPrefixUnstepped, - ArrivalStepReceipt, AccessDiscoverReceipt, IdentityBindReceipt, ArrivalStepRefusal, + ArrivalStepReceipt, AccessDiscoverReceipt, IdentityBindReceipt, PriorLifeBoundaryReceipt, ArrivalStepRefusal, + ArrivalStepIncomplete, PriorLifeBoundaryIncomplete, PriorLifeInputs, prior_life_boundary_step_ref, prior_life_boundary, PriorLifeIdentityForAnotherInstance, IdentityBindObserveRefused, IdentityObserveRefusal, IdentityBindAccessForAnotherInstance, UnitKeyNotBound, AccessDiscoverObserveRefused, ReadOnlyPhaseRefused, IdentityBindInputs, AccessDiscoverEstablished, BoardSerialAgreementRefusal, BoardSerialsDisagree, SmbiosSessionForAnotherController, classify_board_serial_agreement, access_discover_step_ref, identity_bind_provisional_step_ref, arrival_order_authority, arrival_planning_authority, @@ -67,10 +75,11 @@ data run_b: ConvergenceRunId = "o1c1-witness-run-b" as ConvergenceRunId data mtjade1_key: StepSubjectKey = "mtjade1" as StepSubjectKey -fn instance_step_is(s: StepInstanceStanding, step: DeclarationRef) -> Bool { +fn instance_step_is(s: StepInstanceStanding, step: DeclarationRef) -> Bool { match s { InstanceConverged { key: k, receipt: _ } => declaration_ref_eq(a: k.step_identity, b: step) InstanceRefused { key: k, cause: _ } => declaration_ref_eq(a: k.step_identity, b: step) + InstanceIncomplete { key: k, cause: _ } => declaration_ref_eq(a: k.step_identity, b: step) InstanceNotReached { key: k, blocked_by: _ } => declaration_ref_eq(a: k.step_identity, b: step) } } @@ -86,7 +95,7 @@ fn route_is_redfish_write_candidate_on_manager_read(route: BmcRotationRouteStand } } -fn access_established_as_read(s: StepInstanceStanding) -> Bool { +fn access_established_as_read(s: StepInstanceStanding) -> Bool { match s { InstanceConverged { key: k, receipt: r } => declaration_ref_eq(a: k.step_identity, b: access_discover_step_ref) @@ -99,13 +108,15 @@ fn access_established_as_read(s: StepInstanceStanding false + PriorLifeBoundaryReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false + InstanceIncomplete { key: _, cause: _ } => false InstanceNotReached { key: _, blocked_by: _ } => false } } -fn identity_bound_from_committed_captures(s: StepInstanceStanding) -> Bool { +fn identity_bound_from_committed_captures(s: StepInstanceStanding) -> Bool { match s { InstanceConverged { key: k, receipt: r } => declaration_ref_eq(a: k.step_identity, b: identity_bind_provisional_step_ref) @@ -120,8 +131,10 @@ fn identity_bound_from_committed_captures(s: StepInstanceStanding false + PriorLifeBoundaryReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false + InstanceIncomplete { key: _, cause: _ } => false InstanceNotReached { key: _, blocked_by: _ } => false } } @@ -138,21 +151,49 @@ data expected_mtjade1_firmware: FirmwareManifest = FirmwareManifest { configuration_digests: [], } +// THE PRIOR-LIFE ARCHIVE AS THE ROUTE REACHED IT: written by this run within its leg's deadline, read +// back independently, its boundary the uncleared baseline-cursor arm with the cursor naming this +// archive and the one SEL record the world holds, consuming exactly this run's IdentityBindProvisional instance for this unit, from the DRY +// realization and no other. +fn prior_life_archived_from_the_bound_subject(s: StepInstanceStanding) -> Bool { + match s { + InstanceConverged { key: k, receipt: r } => + declaration_ref_eq(a: k.step_identity, b: prior_life_boundary_step_ref) + && match r { + PriorLifeBoundaryReceipt { receipt: p } => + declaration_ref_eq(a: prior_life_receipt_consumed_identity(r: p).step_identity, b: identity_bind_provisional_step_ref) + && ((prior_life_receipt_consumed_identity(r: p).run as NonEmptyStr) as String) == "o1c1-witness-run-a" + && ((prior_life_receipt_consumed_identity(r: p).subject as NonEmptyStr) as String) == "mtjade1" + && (match prior_life_receipt_application(r: p) { ArchiveWritten { write: _, within: _ } => true _ => false }) + && (match prior_life_receipt_boundary(r: p) { LogsArchivedWithBaselineCursor { cursor: c } => content_hash_equal(left: baseline_cursor_archive(c: c), right: prior_life_archive_digest(a: prior_life_receipt_archive(r: p))) && baseline_cursor_sel_final_record(c: c) == Present { value: "1" } }) + && ((prior_life_receipt_realization(r: p) as NonEmptyStr) as String) == "gunbc.machine_intake_prior_life_boundary dry realization over gunbc.bmc_model BmcWorld and a dry archive store" + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + } + InstanceRefused { key: _, cause: _ } => false + InstanceIncomplete { key: _, cause: _ } => false + InstanceNotReached { key: _, blocked_by: _ } => false + } +} + // THE REAL PATH. mtjade1 passes both read-only phases from its committed captures: AccessDiscover from // the 2026-10-04 Manager read at 192.168.1.246 (MegaRAC, 2.11.104000, the controller's year-2000 clock // kept as a reading, a CANDIDATE Redfish account-write route), and IdentityBindProvisional binding the // unit key from the FRU and SMBIOS board serials, which agree, and minting the MachineIntakeSubject // over the FRU's provisional assembly and the read's live firmware manifest, with this run as its one -// intake attempt. -test fn w_mtjade1_converges_both_read_only_phases_from_its_committed_captures() -> Bool { - match converge_mtjade1_arrival_prefix(run: run_a) { +// intake attempt. Then PriorLifeBoundary archives the dry world under the Mt. Jade policy row through +// the real route -- the IdentityBindProvisional receipt this run minted, not a supplied subject. +test fn w_mtjade1_converges_the_prefix_through_its_dry_prior_life_archive() -> Bool { + match converge_mtjade1_arrival_prefix(run: run_a, prior_life: prior_life_minimal_dry_world()) { ArrivalRunFolded { verdict: v } => match v { RunConverged { run: r } => - length(xs: r.ledger.instances) == 2 + length(xs: r.ledger.instances) == 3 && match r.ledger.instances.first() { Present { value: s } => access_established_as_read(s: s) Absent => false } - && match r.ledger.instances.last() { Present { value: s } => identity_bound_from_committed_captures(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: identity_bind_provisional_step_ref)) |> first() { Present { value: s } => identity_bound_from_committed_captures(s: s) Absent => false } + && match r.ledger.instances.last() { Present { value: s } => prior_life_archived_from_the_bound_subject(s: s) Absent => false } RunStopped { ledger: _, at: _ } => false + RunIncomplete { ledger: _, at: _ } => false RunOutcomesRefused { cause: _ } => false } ArrivalPlanRefused { cause: _ } => false @@ -160,6 +201,31 @@ test fn w_mtjade1_converges_both_read_only_phases_from_its_committed_captures() } } +// AN ARCHIVE WRITE THE STORE LOSES LEAVES THE RUN INCOMPLETE, NOT STOPPED AND NOT CONVERGED, at the +// PriorLifeBoundary instance, which records the write as written-but-not-read-back. Same real route, +// the store the only difference. +test fn w_a_lost_archive_write_leaves_the_run_incomplete_at_prior_life_boundary() -> Bool { + let full = prior_life_minimal_dry_world() + let losing = DryPriorLifeWorld { bmc: full.bmc, store: DryArchiveStore { objects: [], behaviour: DryArchiveStoreLosesWrites }, read_at_millis: full.read_at_millis, write_returned_at_millis: full.write_returned_at_millis } + match converge_mtjade1_arrival_prefix(run: run_a, prior_life: losing) { + ArrivalRunFolded { verdict: v } => + match v { + RunIncomplete { ledger: l, at: at } => + declaration_ref_eq(a: at.step_identity, b: prior_life_boundary_step_ref) + && length(xs: l.instances) == 3 + && match l.instances.last() { + Present { value: s } => match s { + InstanceIncomplete { key: _, cause: c } => match c { PriorLifeBoundaryIncomplete { cause: i } => match i { ArchiveWrittenButNotReadBack { write: _, digest: _ } => true _ => false } } + _ => false + } + Absent => false + } + _ => false + } + _ => false + } +} + // BOTH SOURCES ARE READ, each sealed by its own fail-closed file read: the FRU observation with the // fields the capture carries, and the SMBIOS observation with its serial read inside the Base Board // structure and its SOL session attested to the controller at 192.168.1.246. @@ -240,17 +306,17 @@ test fn w_a_serial_outside_the_base_board_structure_is_not_read() -> Bool { } } -// The roster is the authority's own prefix through IdentityBindProvisional: exactly two phases, in +// The roster is the authority's own prefix through PriorLifeBoundary: exactly three phases, in // arrival_phases_all's order, not the twelve-phase list and not a second shorter list. -test fn w_the_roster_is_the_two_phase_prefix_of_the_authority() -> Bool { - arrival_prefix_through(last: arrival_prefix_last) == [Arrival { phase: AccessDiscover }, Arrival { phase: IdentityBindProvisional }] +test fn w_the_roster_is_the_three_phase_prefix_of_the_authority() -> Bool { + arrival_prefix_through(last: arrival_prefix_last) == [Arrival { phase: AccessDiscover }, Arrival { phase: IdentityBindProvisional }, Arrival { phase: PriorLifeBoundary }] } // A phase of the prefix with no step refuses rather than being skipped: through BmcSecure the prefix -// reaches PriorLifeBoundary, which has no step in this cut. +// reaches BmcSecure itself, which has no step in this cut (O1c-3 brings it with its gate). test fn w_a_prefix_phase_with_no_step_refuses() -> Bool { match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { - ArrivalPrefixPhaseUnstepped { phase: p } => p == Arrival { phase: PriorLifeBoundary } + ArrivalPrefixPhaseUnstepped { phase: p } => p == Arrival { phase: BmcSecure } ArrivalPrefixStepped { steps: _ } => false } } @@ -279,9 +345,9 @@ fn plan_refusal(admission: ConvergencePlanAdmission) -> Convergence } } -test fn w_the_real_two_step_plan_is_admitted() -> Bool { +test fn w_the_real_three_step_plan_is_admitted() -> Bool { match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { - ConvergencePlanAdmitted { plan: _ } => length(xs: real_steps()) == 2 + ConvergencePlanAdmitted { plan: _ } => length(xs: real_steps()) == 3 ConvergencePlanRefused { cause: _ } => false } } @@ -337,28 +403,37 @@ test fn w_a_step_with_two_census_rows_refuses() -> Bool { // ── run controls, over real step outcomes from mtjade1's real read ───────────────────────────── -fn real_access(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead) -> StepOutcome { +fn real_access(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead) -> StepOutcome { access_discover(key: step_instance_key(run: run, step: access_discover_step_ref, subject: subject), read: read) } -fn established_access(o: StepOutcome) -> AccessDiscoverEstablished? { +fn established_access(o: StepOutcome) -> AccessDiscoverEstablished? { match step_outcome_receipt(outcome: o) { - Present { value: r } => match r { AccessDiscoverReceipt { receipt: a } => Present { value: a } IdentityBindReceipt { receipt: _ } => none } + Present { value: r } => match r { AccessDiscoverReceipt { receipt: a } => Present { value: a } IdentityBindReceipt { receipt: _ } => none PriorLifeBoundaryReceipt { receipt: _ } => none } Absent => none } } -fn fold_real(run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ConvergenceRunVerdict? { +fn fold_real(run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ConvergenceRunVerdict? { match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => Present { value: fold_convergence_run(plan: p, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection()) } ConvergencePlanRefused { cause: _ } => none } } -fn stopped_on_unmet_access_precondition(v: ConvergenceRunVerdict?) -> Bool { +// The instance the line stopped at is IdentityBindProvisional, refused for an unmet AccessDiscover +// precondition; PriorLifeBoundary after it is not reached. +fn refused_instance(s: StepInstanceStanding) -> Bool { + match s { + InstanceRefused { key: _, cause: _ } => true + _ => false + } +} + +fn stopped_on_unmet_access_precondition(v: ConvergenceRunVerdict?) -> Bool { match v { Present { value: verdict } => match verdict { - RunStopped { ledger: l, at: _ } => match l.instances.last() { + RunStopped { ledger: l, at: _ } => match l.instances |> filter(s => refused_instance(s: s)) |> first() { Present { value: s } => match s { InstanceRefused { key: _, cause: c } => match c { PreconditionUnmet { precondition: p, consumed: _ } => @@ -400,7 +475,7 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject() -> let own_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) let foreign_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: "mtjade2" as StepSubjectKey) let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) - let outcomes: List> = [ + let outcomes: List> = [ StepEstablished { receipt: ProbeReceipt { key: own_access, consumed: [] } }, StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [foreign_access] } }, ] @@ -416,7 +491,7 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run() -> Boo let own_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) let earlier_access = step_instance_key(run: run_b, step: access_discover_step_ref, subject: mtjade1_key) let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) - let outcomes: List> = [ + let outcomes: List> = [ StepEstablished { receipt: ProbeReceipt { key: own_access, consumed: [] } }, StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [earlier_access] } }, ] @@ -427,6 +502,38 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run() -> Boo } } +// AN INCOMPLETE INSTANCE STOPS ITS DEPENDENTS AND IS NEITHER CONVERGED NOR REFUSED (the fold's rule, +// SUPPLIED like the two controls above). Over the real admitted plan, AccessDiscover converges, +// IdentityBindProvisional is INCOMPLETE, and PriorLifeBoundary -- whose receipt here even claims to +// have consumed the incomplete instance -- is NotReached blocked by it: the verdict is RunIncomplete at +// IdentityBindProvisional, never RunConverged and never RunStopped. +test fn w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplete() -> Bool { + let own_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior_life = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: own_access, consumed: [] } }, + StepIncomplete { key: identity, cause: "written, not read back" }, + StepEstablished { receipt: ProbeReceipt { key: prior_life, consumed: [identity] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) { + RunIncomplete { ledger: l, at: at } => + declaration_ref_eq(a: at.step_identity, b: identity_bind_provisional_step_ref) + && match l.instances.last() { + Present { value: s } => match s { + InstanceNotReached { key: k, blocked_by: b } => declaration_ref_eq(a: k.step_identity, b: prior_life_boundary_step_ref) && declaration_ref_eq(a: b.step_identity, b: identity_bind_provisional_step_ref) + _ => false + } + Absent => false + } + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + // THE DOMAIN'S OWN WALL, on the real path: IdentityBindProvisional refuses an AccessDiscover receipt // that is not its own instance's -- here mtjade1's real receipt from another run -- before binding // anything, so no IdentityBoundProvisional exists for a key its access receipt does not match. @@ -434,7 +541,7 @@ test fn w_identity_bind_refuses_an_access_receipt_from_another_run() -> Bool { match established_access(o: real_access(run: run_b, subject: mtjade1_key, read: read_mtjade1_current_manager_read())) { Absent => false Present { value: earlier } => { - let outcome: StepOutcome = identity_bind_provisional(key: step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key), access: earlier, inputs: mtjade1_identity_bind_inputs()) + let outcome: StepOutcome = identity_bind_provisional(key: step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key), access: earlier, inputs: mtjade1_identity_bind_inputs()) let refusal: ArrivalStepRefusal? = step_outcome_refusal(outcome: outcome) match refusal { Present { value: c } => match c { IdentityBindAccessForAnotherInstance { access: k } => ((k.run as NonEmptyStr) as String) == "o1c1-witness-run-b" _ => false } @@ -444,6 +551,32 @@ test fn w_identity_bind_refuses_an_access_receipt_from_another_run() -> Bool { } } +// AND PRIORLIFEBOUNDARY'S, on the real path: an IdentityBindProvisional receipt mtjade1 really minted +// in ANOTHER run cannot be archived under this run's instance. The step refuses naming that receipt's +// instance before the phase reads or writes anything, so no prior-life receipt exists for an identity +// instance its key does not match. +test fn w_prior_life_boundary_refuses_an_identity_receipt_from_another_run() -> Bool { + match established_access(o: real_access(run: run_b, subject: mtjade1_key, read: read_mtjade1_current_manager_read())) { + Absent => false + Present { value: access_b } => + match step_outcome_receipt(outcome: identity_bind_provisional(key: step_instance_key(run: run_b, step: identity_bind_provisional_step_ref, subject: mtjade1_key), access: access_b, inputs: mtjade1_identity_bind_inputs())) { + Present { value: r } => + match r { + IdentityBindReceipt { receipt: identity_b } => { + let outcome: StepOutcome = prior_life_boundary(key: step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key), identity: identity_b, platform: mt_jade_platform_ref, world: prior_life_minimal_dry_world()) + let refusal: ArrivalStepRefusal? = step_outcome_refusal(outcome: outcome) + match refusal { + Present { value: c } => match c { PriorLifeIdentityForAnotherInstance { identity: k } => ((k.run as NonEmptyStr) as String) == "o1c1-witness-run-b" _ => false } + Absent => false + } + } + _ => false + } + Absent => false + } + } +} + // A DUPLICATE (run, step, subject) REFUSES the run before any ledger is written. test fn w_a_duplicate_run_step_subject_refuses() -> Bool { let access = real_access(run: run_a, subject: mtjade1_key, read: read_mtjade1_current_manager_read()) @@ -466,20 +599,20 @@ test fn w_access_discover_refuses_a_read_bound_to_another_unit() -> Bool { } // A REFUSAL STOPS THE LINE OVER ITS DEPENDENTS, AND EACH NAMES ITS BLOCKER. The real read, run for a -// unit it is not bound to, refuses AccessDiscover; IdentityBindProvisional is then never executed and -// is NotReached, blocked by that AccessDiscover instance. +// unit it is not bound to, refuses AccessDiscover; IdentityBindProvisional and PriorLifeBoundary are +// then never executed and are NotReached, each blocked by that AccessDiscover instance. test fn w_a_refused_access_leaves_identity_bind_not_reached_blocked_by_it() -> Bool { - match converge_arrival_prefix(run: run_a, subject: "mtjade2" as StepSubjectKey, read: read_mtjade1_current_manager_read(), inputs: mtjade1_identity_bind_inputs()) { + match converge_arrival_prefix(run: run_a, subject: "mtjade2" as StepSubjectKey, read: read_mtjade1_current_manager_read(), inputs: mtjade1_identity_bind_inputs(), prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life_minimal_dry_world() }) { ArrivalRunFolded { verdict: v } => match v { RunStopped { ledger: l, at: at } => declaration_ref_eq(a: at.step_identity, b: access_discover_step_ref) - && length(xs: l.instances) == 2 + && length(xs: l.instances) == 3 + && length(xs: l.instances |> filter(s => match s { + InstanceNotReached { key: _, blocked_by: b } => declaration_ref_eq(a: b.step_identity, b: access_discover_step_ref) && ((b.subject as NonEmptyStr) as String) == "mtjade2" + _ => false + })) == 2 && match l.instances.last() { - Present { value: s } => match s { - InstanceNotReached { key: k, blocked_by: b } => - declaration_ref_eq(a: k.step_identity, b: identity_bind_provisional_step_ref) && declaration_ref_eq(a: b.step_identity, b: access_discover_step_ref) && ((b.subject as NonEmptyStr) as String) == "mtjade2" - _ => false - } + Present { value: s } => instance_step_is(s: s, step: prior_life_boundary_step_ref) Absent => false } _ => false diff --git a/dag/test/claim/machine_intake/machine_intake_bmc_secure_state_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_bmc_secure_state_witness_test.dag index 6bf4e5d10e1..6e99d35acbe 100644 --- a/dag/test/claim/machine_intake/machine_intake_bmc_secure_state_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_bmc_secure_state_witness_test.dag @@ -258,10 +258,16 @@ fn goal_v1() -> BmcSecureGoal { BmcSecureGoal { managed: managed_ref(version: "1", epoch: 1), published_break_glass: goal_break_glass_ref(), policy: machine_qualification_policy(admits: TestRisk) } } -// ── the observer clock of these claims ────────────────────────────────────────────────────────── -// Admitted to observer_clock_modeled by name; every instant is labeled as modeled. -fn observer_at(millis: EpochMs) -> ObserverClockInstant { - observer_clock_modeled(millis: millis, realization: "test.claim.machine_intake_bmc_secure_state_witness schedule" as NonEmptyStr) +// THE SCHEDULE'S INSTANTS. Only the Bool claims below are admitted to observer_clock_modeled, and +// each mints its own instants into this open record; no helper here returns a sealed instant, so no +// function of this module is a proxy constructor for the observer clock. +data schedule_realization: NonEmptyStr = "test.claim.machine_intake_bmc_secure_state_witness schedule" as NonEmptyStr + +type ScheduleInstants { + store: ObserverClockInstant + fetch: ObserverClockInstant + plan: ObserverClockInstant + apply: ObserverClockInstant } data t_read: EpochMs = 1791072000000 @@ -440,17 +446,17 @@ fn stored_then_fetched( secret: String, version: String, fetch: SecretCredentialFetch, - store_at: EpochMs, - fetch_at: EpochMs, + store_at: ObserverClockInstant, + fetch_at: ObserverClockInstant, ) -> GenerationFetchAdmission? { - match admit_stored_generation(current: current, added: version_identity(secret: secret, version: version), stored_at: observer_at(millis: store_at)) { + match admit_stored_generation(current: current, added: version_identity(secret: secret, version: version), stored_at: store_at) { GenerationStoreRefused { cause: _ } => none - GenerationStored { stored: st } => Present { value: admit_fetched_generation(stored: st, fetch: fetch, fetched_at: observer_at(millis: fetch_at)) } + GenerationStored { stored: st } => Present { value: admit_fetched_generation(stored: st, fetch: fetch, fetched_at: fetch_at) } } } -fn fetched(current: ManagedCredentialReference, secret: String, version: String, bytes: String, fetch_at: EpochMs) -> ManagedCredentialGenerationFetched? { - match stored_then_fetched(current: current, secret: secret, version: version, fetch: ready(secret: secret, version: version, bytes: bytes), store_at: t_store, fetch_at: fetch_at) { +fn fetched(current: ManagedCredentialReference, secret: String, version: String, bytes: String, i: ScheduleInstants, fetch_at: ObserverClockInstant) -> ManagedCredentialGenerationFetched? { + match stored_then_fetched(current: current, secret: secret, version: version, fetch: ready(secret: secret, version: version, bytes: bytes), store_at: i.store, fetch_at: fetch_at) { Absent => none Present { value: a } => match a { @@ -476,12 +482,12 @@ fn fetch_label(a: GenerationFetchAdmission?) -> String { } } -fn managed_generation(version: String, fetch_at: EpochMs) -> ManagedCredentialGenerationFetched? { - fetched(current: managed_ref(version: "1", epoch: 1), secret: "bmc-lab-o1b-gunbc", version: version, bytes: managed_password_v2, fetch_at: fetch_at) +fn managed_generation(version: String, i: ScheduleInstants, fetch_at: ObserverClockInstant) -> ManagedCredentialGenerationFetched? { + fetched(current: managed_ref(version: "1", epoch: 1), secret: "bmc-lab-o1b-gunbc", version: version, bytes: managed_password_v2, i: i, fetch_at: fetch_at) } -fn break_glass_generation() -> ManagedCredentialGenerationFetched? { - fetched(current: break_glass_ref(), secret: "bmc-lab-o1b-admin", version: "4", bytes: break_glass_password, fetch_at: t_fetch) +fn break_glass_generation(i: ScheduleInstants) -> ManagedCredentialGenerationFetched? { + fetched(current: break_glass_ref(), secret: "bmc-lab-o1b-admin", version: "4", bytes: break_glass_password, i: i, fetch_at: i.fetch) } // ── the plan ──────────────────────────────────────────────────────────────────────────────────── @@ -491,17 +497,17 @@ fn plan_with( goal: BmcSecureGoal, managed_route: BmcRotationRouteStanding, managed_generation_value: ManagedCredentialGenerationFetched?, - planned_at: EpochMs, + i: ScheduleInstants, ) -> BmcAccountPlanOutcome? { - plan_full(reading: reading, goal: goal, managed_route: managed_route, managed_generation_value: managed_generation_value, published_generation_value: break_glass_generation(), planned_at: planned_at) + plan_full(reading: reading, goal: goal, managed_route: managed_route, managed_generation_value: managed_generation_value, published_generation_value: break_glass_generation(i: i), i: i) } -fn plan_closing(reading: BmcAccountStateObservation, channel_close: ChannelCloseInput?) -> BmcAccountPlanOutcome? { - plan_closing_as(reading: reading, claimed_managed_user: managed_user, channel_close: channel_close) +fn plan_closing(reading: BmcAccountStateObservation, channel_close: ChannelCloseInput?, i: ScheduleInstants) -> BmcAccountPlanOutcome? { + plan_closing_as(reading: reading, claimed_managed_user: managed_user, channel_close: channel_close, i: i) } -fn plan_closing_as(reading: BmcAccountStateObservation, claimed_managed_user: IpmiUserId, channel_close: ChannelCloseInput?) -> BmcAccountPlanOutcome? { - plan_full_as(reading: reading, goal: goal_v1(), claimed_managed_user: claimed_managed_user, managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), published_generation_value: break_glass_generation(), channel_close: channel_close, planned_at: t_plan) +fn plan_closing_as(reading: BmcAccountStateObservation, claimed_managed_user: IpmiUserId, channel_close: ChannelCloseInput?, i: ScheduleInstants) -> BmcAccountPlanOutcome? { + plan_full_as(reading: reading, goal: goal_v1(), claimed_managed_user: claimed_managed_user, managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), published_generation_value: break_glass_generation(i: i), channel_close: channel_close, i: i) } fn plan_full( @@ -510,9 +516,9 @@ fn plan_full( managed_route: BmcRotationRouteStanding, managed_generation_value: ManagedCredentialGenerationFetched?, published_generation_value: ManagedCredentialGenerationFetched?, - planned_at: EpochMs, + i: ScheduleInstants, ) -> BmcAccountPlanOutcome? { - plan_full_closing(reading: reading, goal: goal, managed_route: managed_route, managed_generation_value: managed_generation_value, published_generation_value: published_generation_value, channel_close: none, planned_at: planned_at) + plan_full_closing(reading: reading, goal: goal, managed_route: managed_route, managed_generation_value: managed_generation_value, published_generation_value: published_generation_value, channel_close: none, i: i) } fn plan_full_closing( @@ -522,9 +528,9 @@ fn plan_full_closing( managed_generation_value: ManagedCredentialGenerationFetched?, published_generation_value: ManagedCredentialGenerationFetched?, channel_close: ChannelCloseInput?, - planned_at: EpochMs, + i: ScheduleInstants, ) -> BmcAccountPlanOutcome? { - plan_full_as(reading: reading, goal: goal, claimed_managed_user: managed_user, managed_route: managed_route, managed_generation_value: managed_generation_value, published_generation_value: published_generation_value, channel_close: channel_close, planned_at: planned_at) + plan_full_as(reading: reading, goal: goal, claimed_managed_user: managed_user, managed_route: managed_route, managed_generation_value: managed_generation_value, published_generation_value: published_generation_value, channel_close: channel_close, i: i) } fn plan_full_as( @@ -535,7 +541,7 @@ fn plan_full_as( managed_generation_value: ManagedCredentialGenerationFetched?, published_generation_value: ManagedCredentialGenerationFetched?, channel_close: ChannelCloseInput?, - planned_at: EpochMs, + i: ScheduleInstants, ) -> BmcAccountPlanOutcome? { match managed_generation_value { Absent => none @@ -556,15 +562,15 @@ fn plan_full_as( published_approval: rotation_approval(s: grounded_route(user: published_user), user: published_user), published_generation: bg, channel_close: channel_close, - planned_at: observer_at(millis: planned_at), + planned_at: i.plan, ), } } } } -fn plan_default(reading: BmcAccountStateObservation) -> BmcAccountPlanOutcome? { - plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), planned_at: t_plan) +fn plan_default(reading: BmcAccountStateObservation, i: ScheduleInstants) -> BmcAccountPlanOutcome? { + plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), i: i) } fn admission_label(a: RotationApplyAdmission) -> String { @@ -661,8 +667,9 @@ fn applied_on( managed_fetch: SecretCredentialFetch, applied_at: EpochMs, readback_at: EpochMs, + i: ScheduleInstants, ) -> String { - applied_with(initial: initial, closed_before: closed_before, managed_fetch: managed_fetch, published_fetch: ready(secret: "bmc-lab-o1b-admin", version: "4", bytes: break_glass_password), applied_at: applied_at, readback_at: readback_at) + applied_with(initial: initial, closed_before: closed_before, managed_fetch: managed_fetch, published_fetch: ready(secret: "bmc-lab-o1b-admin", version: "4", bytes: break_glass_password), applied_at: applied_at, readback_at: readback_at, i: i) } fn applied_with( @@ -672,9 +679,10 @@ fn applied_with( published_fetch: SecretCredentialFetch, applied_at: EpochMs, readback_at: EpochMs, + i: ScheduleInstants, ) -> String { let before = read(w: initial, subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: closed_before, at: t_read) - match plan_default(reading: before) { + match plan_default(reading: before, i: i) { Absent => "fixture-generation-unavailable" Present { value: o } => match o { @@ -713,26 +721,44 @@ fn decision_on(w: BmcWorld, closed: Bool) -> String { // Already secured -> Noop, minted as a Noop receipt, and no plan can be made over it. test fn an_already_secured_controller_is_a_noop() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_secured(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) decision_on(w: world_secured(), closed: true) == "noop" && phase_label(o: bmc_secure_phase_noop(subject: lab_subject(), goal: goal_v1(), reading: reading)) == "converged:noop" - && plan_label(o: plan_default(reading: reading)) == "not-due:noop" + && plan_label(o: plan_default(reading: reading, i: i)) == "not-due:noop" } // Managed accepted AND factory accepted -> NOT Noop: Apply on the published credential, and the full // path writes the world, re-reads it, and mints an Applied receipt carrying the application receipts. test fn managed_and_factory_both_accepted_is_not_a_noop_and_converges_through_apply() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) decision_on(w: world_factory_open(), closed: true) == apply_on(cause: PublishedCredentialStillAccepted { channel: 1 }) && phase_label(o: bmc_secure_phase_noop(subject: lab_subject(), goal: goal_v1(), reading: reading)) == join(["refused:not-held:", apply_on(cause: PublishedCredentialStillAccepted { channel: 1 })], "") - && applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: t_readback) == "converged:applied" + && applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: t_readback, i: i) == "converged:applied" } // Reflash-restored factory access (managed user erased, factory answers) -> the SAME Apply and // readback path, with no second recovery authority. test fn reflash_restored_factory_access_takes_the_same_apply_and_readback_path() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } decision_on(w: world_reflash_restored(), closed: true) == apply_on(cause: ManagedCredentialRejected) - && applied_on(initial: world_reflash_restored(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: t_readback) == "converged:applied" + && applied_on(initial: world_reflash_restored(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: t_readback, i: i) == "converged:applied" } // Ordering is on the observer clock. A readback stamped with the controller's year-2000 instant @@ -740,39 +766,63 @@ test fn reflash_restored_factory_access_takes_the_same_apply_and_readback_path() // ControllerClockReading cannot be placed in an ordering field at all is the compile-time half, // test.claim.machine_intake_bmc_secure_state_forged_probe_witness.) test fn a_year_2000_readback_cannot_satisfy_ordering_and_an_observer_instant_can() -> Bool { - applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: year_2000) == "refused:post-read-precedes-application" - && applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: t_readback) == "converged:applied" + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } + applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: year_2000, i: i) == "refused:post-read-precedes-application" + && applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: managed_v2_fetch(), applied_at: t_apply, readback_at: t_readback, i: i) == "converged:applied" } // An ungrounded route with the operator's approval of the rotation -> the Apply is refused before // any write is planned; the grounded route with the same approval shape is planned. test fn an_ungrounded_route_with_approval_refuses_the_apply() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) let ungrounded = rotation_route_ungrounded(endpoint: lab_endpoint, firmware: lab_firmware()) - plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: ungrounded, managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), planned_at: t_plan)) == "not-admitted:route-not-grounded" - && plan_label(o: plan_default(reading: reading)) == "planned" + plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: ungrounded, managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), i: i)) == "not-admitted:route-not-grounded" + && plan_label(o: plan_default(reading: reading, i: i)) == "planned" } // The secret order. The generation must be stored, then fetched at exactly the stored version, before // the plan; a write whose fetch resolves another version writes nothing. test fn the_secret_order_is_carried_by_the_plan() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) let current = managed_ref(version: "1", epoch: 1) - fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: managed_v2_fetch(), store_at: t_store, fetch_at: t_fetch)) == "fetched" - && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: ready(secret: "bmc-lab-o1b-gunbc", version: "1", bytes: managed_password_v1), store_at: t_store, fetch_at: t_fetch)) == "another-version" - && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: managed_v2_fetch(), store_at: t_fetch, fetch_at: t_store)) == "fetch-precedes-store" - && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: SecretCredentialFetchRefused { reason: "no token" as NonEmptyStr }, store_at: t_store, fetch_at: t_fetch)) == "not-ready" - && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-other", version: "2", fetch: managed_v2_fetch(), store_at: t_store, fetch_at: t_fetch)) == "store-refused" - && plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_apply), planned_at: t_plan)) == "fetched-after-plan" - && applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: ready(secret: "bmc-lab-o1b-gunbc", version: "1", bytes: managed_password_v1), applied_at: t_apply, readback_at: t_readback) == "refused:incomplete:-p" + fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: managed_v2_fetch(), store_at: i.store, fetch_at: i.fetch)) == "fetched" + && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: ready(secret: "bmc-lab-o1b-gunbc", version: "1", bytes: managed_password_v1), store_at: i.store, fetch_at: i.fetch)) == "another-version" + && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: managed_v2_fetch(), store_at: i.fetch, fetch_at: i.store)) == "fetch-precedes-store" + && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-gunbc", version: "2", fetch: SecretCredentialFetchRefused { reason: "no token" as NonEmptyStr }, store_at: i.store, fetch_at: i.fetch)) == "not-ready" + && fetch_label(a: stored_then_fetched(current: current, secret: "bmc-lab-o1b-other", version: "2", fetch: managed_v2_fetch(), store_at: i.store, fetch_at: i.fetch)) == "store-refused" + && plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.apply), i: i)) == "fetched-after-plan" + && applied_on(initial: world_factory_open(), closed_before: true, managed_fetch: ready(secret: "bmc-lab-o1b-gunbc", version: "1", bytes: managed_password_v1), applied_at: t_apply, readback_at: t_readback, i: i) == "refused:incomplete:-p" } // The readback is independent by ordering: the pre-write reading passed as the post-read is refused, // and so is a readback of another controller or of the generation the write replaced. test fn the_post_read_is_independent_of_the_reading_that_diverged() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let initial = world_factory_open() let before = read(w: initial, subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) - match plan_default(reading: before) { + match plan_default(reading: before, i: i) { Absent => false Present { value: o } => match o { @@ -794,13 +844,19 @@ test fn the_post_read_is_independent_of_the_reading_that_diverged() -> Bool { // A generation that does not advance the epoch in force, or belongs to another account, plans nothing; // a reading of another subject is unobserved. test fn the_plan_refuses_a_stale_or_foreign_generation_and_a_foreign_reading() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) let foreign = read(w: world_factory_open(), subject: other_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) let stale_goal = BmcSecureGoal { managed: managed_ref(version: "2", epoch: 2), published_break_glass: goal_break_glass_ref(), policy: machine_qualification_policy(admits: TestRisk) } - plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: break_glass_generation(), planned_at: t_plan)) == "generation-another-account" - && plan_label(o: plan_with(reading: read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "2", epoch: 2), managed_password: managed_password_v1, closed: true, at: t_read), goal: stale_goal, managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), planned_at: t_plan)) == "generation-not-advanced" - && plan_label(o: plan_default(reading: foreign)) == "unobserved" - && plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: published_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), planned_at: t_plan)) == "not-admitted:another-request" + plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: break_glass_generation(i: i), i: i)) == "generation-another-account" + && plan_label(o: plan_with(reading: read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "2", epoch: 2), managed_password: managed_password_v1, closed: true, at: t_read), goal: stale_goal, managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), i: i)) == "generation-not-advanced" + && plan_label(o: plan_default(reading: foreign, i: i)) == "unobserved" + && plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: published_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), i: i)) == "not-admitted:another-request" } // ── blocker controls (side-chat review of 07423d29de) ─────────────────────────────────────────── @@ -855,18 +911,30 @@ fn secured_read(census_value: IpmiControllerChannelCensus, account: PublishedAcc // BLOCKER 1. The build a route must be grounded for is the build the controller reported in the read; // the planner has no build argument. A current reading beside a route for the previous build refuses. test fn a_route_for_a_build_the_controller_no_longer_runs_cannot_be_admitted() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) - plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: cited_lab_route_managed_user_previous_build(), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), planned_at: t_plan)) == "not-admitted:another-build" + plan_label(o: plan_with(reading: reading, goal: goal_v1(), managed_route: cited_lab_route_managed_user_previous_build(), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), i: i)) == "not-admitted:another-build" } // BLOCKER 2. The published replacement is the goal's exact break-glass generation: the managed // secret's generation and an unrelated secret's generation refuse; the predeclared one is planned. test fn the_published_replacement_must_be_the_goal_bound_break_glass_generation() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let reading = read(w: world_factory_open(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, closed: true, at: t_read) - let unrelated = fetched(current: ManagedCredentialReference { account: "admin", role: AccountRoleAdministrator, secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-other", version: "3", hash_state: HashPending }, credential_epoch: 3 }, secret: "bmc-lab-o1b-other", version: "4", bytes: break_glass_password, fetch_at: t_fetch) - plan_label(o: plan_full(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), published_generation_value: managed_generation(version: "2", fetch_at: t_fetch), planned_at: t_plan)) == "published-generation-not-goal-bound" - && plan_label(o: plan_full(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), published_generation_value: unrelated, planned_at: t_plan)) == "published-generation-not-goal-bound" - && plan_label(o: plan_full(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", fetch_at: t_fetch), published_generation_value: break_glass_generation(), planned_at: t_plan)) == "planned" + let unrelated = fetched(current: ManagedCredentialReference { account: "admin", role: AccountRoleAdministrator, secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-other", version: "3", hash_state: HashPending }, credential_epoch: 3 }, secret: "bmc-lab-o1b-other", version: "4", bytes: break_glass_password, i: i, fetch_at: i.fetch) + plan_label(o: plan_full(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), published_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), i: i)) == "published-generation-not-goal-bound" + && plan_label(o: plan_full(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), published_generation_value: unrelated, i: i)) == "published-generation-not-goal-bound" + && plan_label(o: plan_full(reading: reading, goal: goal_v1(), managed_route: grounded_route(user: managed_user), managed_generation_value: managed_generation(version: "2", i: i, fetch_at: i.fetch), published_generation_value: break_glass_generation(i: i), i: i)) == "planned" } // BLOCKER 3, RECLASSIFIED (cut O1a-2). A channel still open to the published account (an @@ -875,9 +943,15 @@ test fn the_published_replacement_must_be_the_goal_bound_break_glass_generation( // plan refuses unless a channel-access route is supplied -- the missing operation is now a typed plan // refusal, not an assessment refusal. test fn an_open_channel_is_a_deviation_and_the_plan_refuses_without_a_channel_access_route() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } string_contains(s: assessment_on(reading: secured_read(census_value: census_with(serial_privilege_open: true, unaddressed_lan_open: false), account: PublishedAccountRetired)), pattern: "diverged/apply:") && string_contains(s: assessment_on(reading: secured_read(census_value: census_with(serial_privilege_open: false, unaddressed_lan_open: true), account: PublishedAccountRetired)), pattern: "diverged/apply:") - && plan_label(o: plan_default(reading: secured_read(census_value: census_with(serial_privilege_open: true, unaddressed_lan_open: false), account: PublishedAccountRetired))) == "channel-close-route-not-supplied" + && plan_label(o: plan_default(reading: secured_read(census_value: census_with(serial_privilege_open: true, unaddressed_lan_open: false), account: PublishedAccountRetired), i: i)) == "channel-close-route-not-supplied" && assessment_on(reading: secured_read(census_value: census_with(serial_privilege_open: false, unaddressed_lan_open: false), account: PublishedAccountRetired)) == "satisfied/noop" } @@ -907,17 +981,23 @@ fn channel_plan_label(o: BmcAccountPlanOutcome?) -> String { } test fn an_open_channel_is_closed_only_over_a_grounded_channel_access_route() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let close = IpmiSetUserPrivilegeLimit { access: ipmi_user_channel_access(channel: 2, user: published_user, privilege: IpmiPrivilegeNoAccess) } let route = rotation_route_from_citation(endpoint: lab_endpoint, firmware: lab_firmware(), request: close, citation: lab_route_fixture_citation) let candidate = rotation_route_candidate(endpoint: lab_endpoint, firmware: lab_firmware(), request: close, evidence: PublicStandardOperation { authority: lab_route_fixture_citation }) let exact = [approval(authority: rotation_apply_authority, revision: rotation_route_request_identity(standing: route, request: close))] let with_admin = secured_read(census_value: census_with_managed_row(managed_on_2: true), account: PublishedAccountRetired) let without_admin = secured_read(census_value: census_with_managed_row(managed_on_2: false), account: PublishedAccountRetired) - channel_plan_label(o: plan_closing(reading: with_admin, channel_close: none)) == "channel-close-route-not-supplied" - && channel_plan_label(o: plan_closing(reading: with_admin, channel_close: Present { value: ChannelCloseInput { route: candidate, approvals: exact } })) == "channel-write-not-admitted:route-not-grounded" - && channel_plan_label(o: plan_closing(reading: with_admin, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [] } })) == "channel-close-approval-absent" - && channel_plan_label(o: plan_closing(reading: without_admin, channel_close: Present { value: ChannelCloseInput { route: route, approvals: exact } })) == "channel-write-not-admitted:would-leave-no-administrator:not-administrator-on-channel" - && channel_plan_label(o: plan_closing(reading: with_admin, channel_close: Present { value: ChannelCloseInput { route: route, approvals: exact } })) == "planned:1" + channel_plan_label(o: plan_closing(reading: with_admin, channel_close: none, i: i)) == "channel-close-route-not-supplied" + && channel_plan_label(o: plan_closing(reading: with_admin, channel_close: Present { value: ChannelCloseInput { route: candidate, approvals: exact } }, i: i)) == "channel-write-not-admitted:route-not-grounded" + && channel_plan_label(o: plan_closing(reading: with_admin, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [] } }, i: i)) == "channel-close-approval-absent" + && channel_plan_label(o: plan_closing(reading: without_admin, channel_close: Present { value: ChannelCloseInput { route: route, approvals: exact } }, i: i)) == "channel-write-not-admitted:would-leave-no-administrator:not-administrator-on-channel" + && channel_plan_label(o: plan_closing(reading: with_admin, channel_close: Present { value: ChannelCloseInput { route: route, approvals: exact } }, i: i)) == "planned:1" } // Retention. A break-glass account retained by policy must be the goal's generation; a factory @@ -985,6 +1065,12 @@ test fn an_arbitrary_published_replacement_is_not_a_noop_and_the_goal_generation // An Apply whose writes complete but whose post-read does not authenticate the goal generation (the // published write carried other bytes under the right version) mints NO phase receipt. test fn an_apply_whose_post_read_fails_the_goal_generation_mints_no_receipt() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } applied_with( initial: world_factory_open(), closed_before: true, @@ -992,6 +1078,7 @@ test fn an_apply_whose_post_read_fails_the_goal_generation_mints_no_receipt() -> published_fetch: ready(secret: "bmc-lab-o1b-admin", version: "4", bytes: "not-the-goal-bytes!7"), applied_at: t_apply, readback_at: t_readback, + i: i, ) == join(["refused:post-read-not-held:", apply_on_finding(finding: BreakGlassGenerationRejected)], "") } @@ -1026,16 +1113,22 @@ fn close_approval_in(route: BmcRotationRouteStanding, attempt: String) -> Redemp // claiming a managed user other than the one the read authenticated refuses. A read later than the plan // refuses at PlanPrecedesDivergedReading (the dry read takes every reading at one instant). test fn the_channel_close_readback_is_bound_to_the_observed_run_and_account() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let route = rotation_route_from_citation(endpoint: lab_endpoint, firmware: lab_firmware(), request: close_ch2(), citation: lab_route_fixture_citation) let base = census_with(serial_privilege_open: true, unaddressed_lan_open: false) let other_admin = ipmi_controller_channel_census(members: base.members, user_access: concat(base.user_access, [ipmi_user_channel_access(channel: 2, user: 4, privilege: IpmiPrivilegeAdministrator)])) let a = secured_read(census_value: census_with_managed_row(managed_on_2: true), account: PublishedAccountRetired) let later = read_with(w: world_secured(), subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, census_value: census_with_managed_row(managed_on_2: true), account: PublishedAccountRetired, at: t_plan + 1) - channel_plan_label(o: plan_closing(reading: a, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-2")] } })) == "channel-write-not-admitted:would-leave-no-administrator:another-run" - && channel_plan_label(o: plan_closing(reading: a, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } })) == "planned:1" - && channel_plan_label(o: plan_closing(reading: secured_read(census_value: other_admin, account: PublishedAccountRetired), channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } })) == "channel-write-not-admitted:would-leave-no-administrator:not-administrator-on-channel" - && channel_plan_label(o: plan_closing_as(reading: a, claimed_managed_user: 4, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } })) == "managed-user-not-authenticated-account" - && channel_plan_label(o: plan_closing(reading: later, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } })) == "plan-precedes-reading" + channel_plan_label(o: plan_closing(reading: a, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-2")] } }, i: i)) == "channel-write-not-admitted:would-leave-no-administrator:another-run" + && channel_plan_label(o: plan_closing(reading: a, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } }, i: i)) == "planned:1" + && channel_plan_label(o: plan_closing(reading: secured_read(census_value: other_admin, account: PublishedAccountRetired), channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } }, i: i)) == "channel-write-not-admitted:would-leave-no-administrator:not-administrator-on-channel" + && channel_plan_label(o: plan_closing_as(reading: a, claimed_managed_user: 4, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } }, i: i)) == "managed-user-not-authenticated-account" + && channel_plan_label(o: plan_closing(reading: later, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } }, i: i)) == "plan-precedes-reading" } // ── one nonempty real plan through the dry application, the post-read and the phase (item 3) ───── @@ -1046,11 +1139,17 @@ test fn the_channel_close_readback_is_bound_to_the_observed_run_and_account() -> // The world then holds the published user at NO ACCESS on channel 2 and the managed user still at // ADMINISTRATOR there. test fn a_planned_channel_close_is_applied_read_back_and_converges() -> Bool { + let i = ScheduleInstants { + store: observer_clock_modeled(millis: t_store, realization: schedule_realization), + fetch: observer_clock_modeled(millis: t_fetch, realization: schedule_realization), + plan: observer_clock_modeled(millis: t_plan, realization: schedule_realization), + apply: observer_clock_modeled(millis: t_apply, realization: schedule_realization), + } let route = rotation_route_from_citation(endpoint: lab_endpoint, firmware: lab_firmware(), request: close_ch2(), citation: lab_route_fixture_citation) let layout = census_with_managed_row(managed_on_2: true) let initial = seeded(w: world_secured(), census_value: layout) let before = read_in(w: initial, subject: lab_subject(), managed: managed_ref(version: "1", epoch: 1), managed_password: managed_password_v1, census_value: layout, account: PublishedAccountRetired, attempt: "attempt-1", at: t_read) - match plan_closing(reading: before, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } }) { + match plan_closing(reading: before, channel_close: Present { value: ChannelCloseInput { route: route, approvals: [close_approval_in(route: route, attempt: "attempt-1")] } }, i: i) { Absent => false Present { value: o } => match o { diff --git a/dag/test/claim/machine_intake/machine_intake_prior_life_boundary_forged_probe_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_prior_life_boundary_forged_probe_witness_test.dag new file mode 100644 index 00000000000..65f6ca9311a --- /dev/null +++ b/dag/test/claim/machine_intake/machine_intake_prior_life_boundary_forged_probe_witness_test.dag @@ -0,0 +1,96 @@ +module test.claim.machine_intake_prior_life_boundary_forged_probe_witness + +import std.types { String, Bool, Int } +import v2.std.algebra { filter } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, CompileDiagnosticCensusRow, CensusObserved, CensusNotRunnable, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE PRIOR-LIFE ARCHIVE'S AND THE EFFECT LEG'S SEALS, ENROLLED AS EXECUTED REDS (cut O1c-2). The probe +// authors outside their modules every carrier that stands for an effect having run: a leg's budget, +// deadline and completion; the archive, its plan, its cursor, the write's receipt, the readback and the +// phase receipt. It also calls, from callers they do not admit, the budget mint, the dry phase (whose +// receipt would then name a subject and an identity instance of the caller's choosing) and the dry +// realization's clock. This witness hands that source to the compiler through the diagnostic-census +// harness and requires each refusal CLASS at its SUBJECT by name; the class-scoped control shows a clean +// source reading the same modules through their unsealed functions emits none. +data forged_probe_source: String = "module probe_prior_life_boundary_forged\n\nimport std.types { EpochMs, Int, List, NonEmptyStr, String }\nimport std.decl_ref { DeclarationRef, decl_ref }\nimport std.content_hash { ContentHash }\nimport std.measure { PositiveMillisecond }\nimport gunbc.clock_read { ObserverClockInstant }\nimport gunbc.machine_intake_subject { MachineIntakeSubject }\nimport gunbc.fleet.convergence_fold {\n StepInstanceKey, LegBudget, LegDeadline, LegCompletedWithinDeadline, LegCompletion, leg_budget,\n}\nimport gunbc.machine_intake_prior_life_boundary {\n BaselineCursor, PriorLifeArchive, PriorLifeArchivePlan, ArchiveWriteReceipt, ArchiveReadBack, ArchivedObject,\n PriorLifeBoundaryEstablished, PriorLifePolicy, PriorLifeApplication, ArchiveAlreadyHeld, PriorLifeBoundaryArm, CarrierCapture,\n DryPriorLifeWorld, DryPriorLifeStep, dry_archive_prior_life, dry_prior_life_instant,\n PriorLifeArchiveOutcome, PriorLifeRequest, PriorLifeObservation, DryArchiveStore, DryArchiveWrite, ArchiveReadBackStanding,\n established, write_then_read_back, archive_of, observe_prior_life, dry_write_archive, read_back_archive,\n}\nimport gunbc.bmc_model { BmcWorld }\nimport gunbc.clock_read { ObserverClockRead }\nimport std.goal_assessment { ObservationAttempt }\nimport gunbc.fleet.convergence_fold { effect_leg_deadline, complete_effect_leg }\n\nfn forged_budget(leg: DeclarationRef, budget: PositiveMillisecond) -> LegBudget {\n LegBudget { leg: leg, budget: budget }\n}\n\nfn forged_budget_via_mint(leg: DeclarationRef, budget: PositiveMillisecond) -> LegBudget {\n leg_budget(leg: leg, budget: budget)\n}\n\nfn forged_deadline(budget: LegBudget, started: ObserverClockInstant) -> LegDeadline {\n LegDeadline { budget: budget, started: started }\n}\n\nfn forged_within(deadline: LegDeadline, finished: ObserverClockInstant) -> LegCompletedWithinDeadline {\n LegCompletedWithinDeadline { deadline: deadline, finished: finished }\n}\n\nfn forged_cursor(archive: ContentHash) -> BaselineCursor {\n BaselineCursor { sel_final_record: none, log_services: [], account_events_final_entry: none, archive: archive }\n}\n\nfn forged_archive(subject: MachineIntakeSubject, digest: ContentHash, at: ObserverClockInstant, cursor: BaselineCursor) -> PriorLifeArchive {\n PriorLifeArchive { subject: subject, captures: [], body: \"forged\", digest: digest, read_at: at, cursor: cursor }\n}\n\nfn forged_plan(archive: PriorLifeArchive) -> PriorLifeArchivePlan {\n PriorLifeArchivePlan { archive: archive }\n}\n\nfn forged_write(digest: ContentHash, completion: LegCompletion) -> ArchiveWriteReceipt {\n ArchiveWriteReceipt { digest: digest, completion: completion }\n}\n\nfn forged_readback(digest: ContentHash, held: ArchivedObject) -> ArchiveReadBack {\n ArchiveReadBack { digest: digest, held: held }\n}\n\nfn forged_receipt(key: StepInstanceKey, subject: MachineIntakeSubject, policy: PriorLifePolicy, archive: PriorLifeArchive, application: PriorLifeApplication, readback: ArchiveReadBack, boundary: PriorLifeBoundaryArm) -> PriorLifeBoundaryEstablished {\n PriorLifeBoundaryEstablished { key: key, consumed_identity: key, subject: subject, policy: policy, archive: archive, application: application, readback: readback, boundary: boundary, realization: \"live\" }\n}\n\nfn forged_phase(key: StepInstanceKey, subject: MachineIntakeSubject, platform: DeclarationRef, world: DryPriorLifeWorld) -> DryPriorLifeStep {\n dry_archive_prior_life(key: key, consumed_identity: key, subject: subject, platform: platform, world: world)\n}\n\nfn forged_instant(millis: EpochMs) -> ObserverClockInstant {\n dry_prior_life_instant(millis: millis)\n}\n\nfn rekeyed_receipt(key: StepInstanceKey, subject: MachineIntakeSubject, policy: PriorLifePolicy, archive: PriorLifeArchive, readback: ArchiveReadBack) -> PriorLifeArchiveOutcome {\n established(key: key, consumed: key, subject: subject, policy: policy, archive: archive, application: ArchiveAlreadyHeld, readback: readback)\n}\n\nfn unchecked_write(key: StepInstanceKey, subject: MachineIntakeSubject, policy: PriorLifePolicy, archive: PriorLifeArchive, world: DryPriorLifeWorld) -> DryPriorLifeStep {\n write_then_read_back(key: key, consumed: key, subject: subject, policy: policy, archive: archive, world: world)\n}\n\nfn chosen_archive(subject: MachineIntakeSubject, world: BmcWorld, at: ObserverClockInstant) -> PriorLifeArchive {\n archive_of(subject: subject, world: world, read_at: at)\n}\n\nfn chosen_observation(key: StepInstanceKey, request: PriorLifeRequest) -> ObservationAttempt {\n observe_prior_life(key: key, request: request)\n}\n\nfn chosen_write(store: DryArchiveStore, plan: PriorLifeArchivePlan, budget: LegBudget, started: EpochMs, returned: EpochMs) -> DryArchiveWrite {\n dry_write_archive(store: store, plan: plan, budget: budget, started_millis: started, returned_millis: returned)\n}\n\nfn chosen_readback(store: DryArchiveStore, archive: PriorLifeArchive) -> ArchiveReadBackStanding {\n read_back_archive(store: store, archive: archive)\n}\n\nfn chosen_deadline(budget: LegBudget, started: ObserverClockInstant) -> LegDeadline {\n effect_leg_deadline(budget: budget, started: started)\n}\n\nfn chosen_completion(deadline: LegDeadline, finished: ObserverClockRead) -> LegCompletion {\n complete_effect_leg(deadline: deadline, finished: finished)\n}\n" + +data harness_control_source: String = "module probe_prior_life_boundary_harness_control\nimport std.decl_ref { DeclarationRef }\nimport gunbc.machine_intake_prior_life_boundary { PriorLifePolicy, prior_life_policy_for, mt_jade_platform_ref, prior_life_archive_write_budget }\nimport gunbc.fleet.convergence_fold { LegBudget }\nfn policy() -> PriorLifePolicy? { prior_life_policy_for(platform: mt_jade_platform_ref) }\nfn budget() -> LegBudget { prior_life_archive_write_budget() }\n" + +fn probe() -> CompileDiagnosticCensus { + compile_dag_diagnostic_census(forged_probe_source) +} + +fn blocking_count_for_class_and_subject(c: CompileDiagnosticCensus, wanted: String, subject: String) -> Int { + match c { + CensusNotRunnable { cause: _ } => -1 + CensusObserved { rows: rows } => + rows + |> filter(r => (r.diagnostic_class as String) == wanted && r.subject_name == subject && r.blocking) + |> fold(init: 0, f: (acc, r) => acc + r.count) + } +} + +fn blocking_count_for_class(c: CompileDiagnosticCensus, wanted: String) -> Int { + match c { + CensusNotRunnable { cause: _ } => -1 + CensusObserved { rows: rows } => + rows |> filter(r => (r.diagnostic_class as String) == wanted && r.blocking) |> fold(init: 0, f: (acc, r) => acc + r.count) + } +} + +test fn the_harness_runs_and_a_clean_source_emits_no_seal_violation() -> Bool { + let c = compile_dag_diagnostic_census(harness_control_source) + blocking_count_for_class(c: c, wanted: "SoleConstructorViolation") == 0 + && blocking_count_for_class(c: c, wanted: "ConstructorCallAdmissionRefused") == 0 +} + +// A leg's budget, its deadline and a within-deadline completion cannot be authored, and the budget +// mint refuses a caller it does not admit, so no effect leg runs without a deadline its domain declared. +test fn a_forged_leg_budget_deadline_or_completion_is_refused() -> Bool { + let c = probe() + blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "LegBudget") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "leg_budget") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "LegDeadline") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "LegCompletedWithinDeadline") >= 1 +} + +// The archive, its plan, its cursor, the write receipt, the readback and the phase receipt cannot be +// authored outside the phase's module. +test fn forged_archive_carriers_and_the_phase_receipt_are_refused_at_their_literals() -> Bool { + let c = probe() + blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "BaselineCursor") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "PriorLifeArchive") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "PriorLifeArchivePlan") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "ArchiveWriteReceipt") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "ArchiveReadBack") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "PriorLifeBoundaryEstablished") >= 1 +} + +// The dry phase and the dry realization's clock refuse callers they do not admit. +test fn the_dry_phase_and_its_clock_refuse_an_outside_caller() -> Bool { + let c = probe() + blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "dry_archive_prior_life") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "dry_prior_life_instant") >= 1 +} + +// THE MINTER CHAIN BEHIND THE CHECKED ENTRY (side-chat review of 31ef3dbe8c): the receipt minter, the +// write-and-read-back helper, the archive constructor, the observation that carries it, the dry write, +// the readback, and the effect leg's deadline and completion each refuse a caller outside the checked +// path, so a receipt for one instance cannot be re-keyed to another and an archive with a gap cannot +// reach a write. +test fn every_minter_behind_the_checked_entry_refuses_an_outside_caller() -> Bool { + let c = probe() + blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "established") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "write_then_read_back") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "archive_of") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "observe_prior_life") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "dry_write_archive") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "read_back_archive") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "effect_leg_deadline") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "complete_effect_leg") >= 1 +} diff --git a/dag/test/claim/machine_intake/machine_intake_prior_life_boundary_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_prior_life_boundary_witness_test.dag new file mode 100644 index 00000000000..b76dfcbfa26 --- /dev/null +++ b/dag/test/claim/machine_intake/machine_intake_prior_life_boundary_witness_test.dag @@ -0,0 +1,393 @@ +module test.claim.machine_intake_prior_life_boundary_witness + +import std.types { Bool, EpochMs, Int, List, NonEmptyStr, String } +import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } +import std.content_hash { content_hash_equal } +import std.measure { positive_millisecond, PositiveMeasureSuccessor } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.algebra { length } +import extdeps.bmc.redfish_telemetry { + RedfishLogEntry, RedfishLogService, RedfishTelemetryPoint, RedfishTemperatureCelsius, RedfishReadingValue, RedfishHealthOk, RedfishStateEnabled, +} +import extdeps.bmc.redfish_virtual_media { + RedfishVirtualMediaObservation, RedfishVirtualMediaLocator, UnderManager, MediaCd, MediaDvd, ConnectedViaNotConnected, ConnectedViaUri, redfish_virtual_media_resource_path, +} +import gunbc.bmc_model { + BmcWorld, BmcSelRecord, BmcPowerOn, BmcRecordSurfaces, bmc_world, bmc_with_record_surfaces, bmc_record_surfaces_unmodeled, +} +import gunbc.clock_read { ObserverClockObserved, ObserverClockUnreadable, observer_clock_modeled } +import gunbc.machine_intake_subject { MachineIntakeSubject, IntakeAttemptId, UnitKey, AssemblyManifest, FirmwareManifest, qualification_subject_of } +import gunbc.fleet.convergence_fold { + StepInstanceKey, ConvergenceRunId, StepSubjectKey, step_instance_key, + LegCompletedWithin, LegDeadlineElapsed, LegFinishedBeforeItStarted, LegCompletionUnobserved, + leg_budget, effect_leg_deadline, complete_effect_leg, +} +import gunbc.machine_intake_prior_life_boundary { + DryPriorLifeWorld, DryArchiveStore, DryArchiveStoreKeepsWrites, DryArchiveStoreLosesWrites, DryArchiveStoreCorruptsWrites, + PriorLifePolicy, UnclearedBoundaryAdmitted, UnclearedBoundaryNotAdmitted, CarrierCaptured, CarrierGap, CarrierSurfaceUnmodeled, PowerStatePayload, + PriorLifeCarrier, PriorLifeBmcClock, PriorLifeSensorSnapshot, + PriorLifeAssessRefusal, RequiredCarrierNotArchivable, UnclearedBoundaryNotAdmittedByPolicy, + PriorLifeArchiveEstablished, PriorLifeArchiveRefused, PriorLifeArchiveIncomplete, + PriorLifePolicyAbsent, PriorLifeAssessmentRefused, + ArchiveWriteLegNotCompleted, ArchiveWrittenButNotReadBack, ArchiveReadBackDiffersFromWrite, + ArchiveAlreadyHeld, ArchiveWritten, LogsArchivedWithBaselineCursor, + DryPriorLifeStep, PriorLifeArchiveOutcome, + classify_prior_life_policy, dry_archive_prior_life, prior_life_carriers_all, prior_life_carrier_eq, + mt_collins_platform_ref, mt_jade_platform_ref, + prior_life_receipt_application, prior_life_receipt_boundary, prior_life_receipt_archive, prior_life_receipt_realization, + prior_life_archive_digest, prior_life_archive_body, baseline_cursor_sel_final_record, baseline_cursor_archive, baseline_cursor_log_services, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// CUT O1c-2, THE PRIOR-LIFE ARCHIVE AT ITS OWN INTERFACE. These claims SUPPLY the phase's inputs -- +// the subject, the step keys, the dry world -- and call the domain's phase directly (each admitted by +// name to gunbc.machine_intake_prior_life_boundary dry_archive_prior_life; no helper here calls it, +// so no function of this module returns its sealed receipt). The pairing obligation's real path is +// test.claim.machine_intake_arrival_converge_witness, whose route claim reaches this phase through +// mtjade1's real AccessDiscover and IdentityBindProvisional and the fold. The worlds here model no +// vendor: every value is a generic Redfish or IPMI record, and no world claims a controller family. + +data run_p: ConvergenceRunId = "o1c2-witness-run-p" as ConvergenceRunId + +data unit_p: StepSubjectKey = "dry-unit" as StepSubjectKey + +fn key_p() -> StepInstanceKey { + step_instance_key(run: run_p, step: decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary"), subject: unit_p) +} + +fn identity_p() -> StepInstanceKey { + step_instance_key(run: run_p, step: decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "identity_bind_provisional"), subject: unit_p) +} + +fn subject_p() -> MachineIntakeSubject { + MachineIntakeSubject { + subject: qualification_subject_of(unit_key: "DRY-BOARD-0001" as UnitKey, assembly: AssemblyManifest { chassis_part_number: "dry-chassis", components: [] }, firmware: FirmwareManifest { entries: [], configuration_digests: [] }), + attempt_id: "o1c2-witness-run-p" as IntakeAttemptId, + } +} + +// ── worlds ───────────────────────────────────────────────────────────────────────────────────────── + +data sel_records: List = [ + BmcSelRecord { id_hex: "1", date: "01/01/2026", time: "00:00:01", sensor: "Power Unit", event: "AC lost", state: "Asserted" }, + BmcSelRecord { id_hex: "2", date: "01/01/2026", time: "00:00:09", sensor: "System Event", event: "Timestamp Clock Sync", state: "Asserted" }, +] + +// Every surface the archive reads, modeled: a generic Redfish record set with one log service, one +// account event, one virtual-media member and one sensor. +data all_surfaces: BmcRecordSurfaces = BmcRecordSurfaces { + manager_date_time: Present { value: "2026-10-05T12:00:00+00:00" }, + log_services: Present { value: [RedfishLogService { id: "EventLog", entries: [RedfishLogEntry { id: 1, severity: "OK", message: "service started" }, RedfishLogEntry { id: 2, severity: "Warning", message: "fan below threshold" }] }] }, + account_events: Present { value: [RedfishLogEntry { id: 7, severity: "OK", message: "session opened" }] }, + virtual_media: Present { value: [RedfishVirtualMediaObservation { locator: RedfishVirtualMediaLocator { parent: UnderManager { manager_id: "bmc" }, media_id: "CD1" }, media_types: [MediaCd], connected_via: ConnectedViaNotConnected, inserted: false, image: none }] }, + sensors: Present { value: [RedfishTelemetryPoint { name: "CPU0 Temp", kind: RedfishTemperatureCelsius, reading: RedfishReadingValue { whole: 41 }, health: RedfishHealthOk, state: RedfishStateEnabled }] }, +} + +fn world_all_surfaces() -> BmcWorld { + bmc_with_record_surfaces(world: sel_world(), surfaces: all_surfaces) +} + +// The SEL and nothing else the archive needs: bmc_world() models no record surface. +fn sel_world() -> BmcWorld { + let w = bmc_world(power: BmcPowerOn) + BmcWorld { + power: w.power, pending: w.pending, fired: w.fired, boot_override: w.boot_override, sel: sel_records, + sol_session_open: w.sol_session_open, cycle_off_interval: w.cycle_off_interval, + host_booted_at: w.host_booted_at, booted_via_override: w.booted_via_override, sol_drop_after_boot: w.sol_drop_after_boot, + web: w.web, ipmi_users: w.ipmi_users, ipmi_user_access: w.ipmi_user_access, record_surfaces: bmc_record_surfaces_unmodeled, + } +} + +data empty_store: DryArchiveStore = DryArchiveStore { objects: [], behaviour: DryArchiveStoreKeepsWrites } + +data t_read_p: EpochMs = 1791158400000 + +// The write returns two seconds after the read, inside the thirty-second budget. +data t_returned_p: EpochMs = 1791158402000 + +// The write returns forty-five seconds after the read, past the thirty-second budget. +data t_returned_late_p: EpochMs = 1791158445000 + +fn dry_world(bmc: BmcWorld, store: DryArchiveStore) -> DryPriorLifeWorld { + DryPriorLifeWorld { bmc: bmc, store: store, read_at_millis: t_read_p, write_returned_at_millis: t_returned_p } +} + +// THE SMALLEST WORLD THE ROUTE CLAIMS ARCHIVE: every surface modeled, so all eight carriers are +// captured (an empty log is a capture, an unmodeled one a gap), and ONE SEL record, so the baseline +// cursor the route asserts is a real position read from a real record rather than a degenerate empty +// one. The encoder's cost is linear in the population (measured: about 720 eval steps per SEL record +// at 1, 20 and 80 records), so the route claims shrink their input rather than the encoder; the +// payload's fidelity over richer populations is this module's own subject. +data one_sel_record: List = [ + BmcSelRecord { id_hex: "1", date: "01/01/2026", time: "00:00:01", sensor: "Power Unit", event: "AC lost", state: "Asserted" }, +] + +data empty_surfaces: BmcRecordSurfaces = BmcRecordSurfaces { + manager_date_time: Present { value: "2026-10-05T12:00:00+00:00" }, + log_services: Present { value: [] }, + account_events: Present { value: [] }, + virtual_media: Present { value: [] }, + sensors: Present { value: [] }, +} + +fn prior_life_minimal_dry_world() -> DryPriorLifeWorld { + let w = bmc_world(power: BmcPowerOn) + let with_sel = BmcWorld { + power: w.power, pending: w.pending, fired: w.fired, boot_override: w.boot_override, sel: one_sel_record, + sol_session_open: w.sol_session_open, cycle_off_interval: w.cycle_off_interval, + host_booted_at: w.host_booted_at, booted_via_override: w.booted_via_override, sol_drop_after_boot: w.sol_drop_after_boot, + web: w.web, ipmi_users: w.ipmi_users, ipmi_user_access: w.ipmi_user_access, record_surfaces: empty_surfaces, + } + dry_world(bmc: with_sel, store: empty_store) +} + +// The full dry world the arrival route claim archives: every surface modeled, a store that keeps writes, +// and a write that returns in two seconds. +fn prior_life_full_dry_world() -> DryPriorLifeWorld { + dry_world(bmc: world_all_surfaces(), store: empty_store) +} + +fn outcome_label(o: PriorLifeArchiveOutcome) -> String { + match o { + PriorLifeArchiveEstablished { receipt: _ } => "established" + PriorLifeArchiveRefused { cause: _ } => "refused" + PriorLifeArchiveIncomplete { cause: c } => + match c { + ArchiveWriteLegNotCompleted { write: _, completion: k } => + match k { + LegDeadlineElapsed { deadline: _, finished: _ } => "incomplete:deadline-elapsed" + LegFinishedBeforeItStarted { deadline: _, finished: _ } => "incomplete:finished-before-start" + LegCompletionUnobserved { deadline: _, detail: _ } => "incomplete:unobserved" + LegCompletedWithin { completed: _ } => "incomplete:within?" + } + ArchiveWrittenButNotReadBack { write: _, digest: _ } => "incomplete:not-read-back" + ArchiveReadBackDiffersFromWrite { write: _, digest: _, read: _ } => "incomplete:read-back-differs" + } + } +} + +// ── controls ─────────────────────────────────────────────────────────────────────────────────────── + +// THE PLAN'S NAMED CONTROL. Only the SEL -- whose final record id is all a bare cursor would carry -- +// with the other surfaces unmodeled is NOT established: the policy requires all eight carriers, the +// first unmodeled one (the controller clock) is a typed gap, and the phase refuses before any write. +// The same world with every surface modeled is established. +test fn w_only_the_sel_final_record_with_the_other_carriers_absent_is_not_established() -> Bool { + let refused = match dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: sel_world(), store: empty_store)).outcome { + PriorLifeArchiveRefused { cause: c } => + match c { + PriorLifeAssessmentRefused { cause: a } => + match a { + RequiredCarrierNotArchivable { carrier: k, cause: _ } => prior_life_carrier_eq(a: k, b: PriorLifeBmcClock) + UnclearedBoundaryNotAdmittedByPolicy { platform: _ } => false + } + _ => false + } + _ => false + } + refused && outcome_label(o: dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: prior_life_full_dry_world()).outcome) == "established" +} + +// A GAP IS A GAP FOR EVERY REQUIRED CARRIER, NOT ONLY THE FIRST: a world with every surface modeled +// except the sensors refuses naming the sensor snapshot. +test fn w_one_unmodeled_carrier_is_a_typed_gap_that_refuses() -> Bool { + let no_sensors = BmcRecordSurfaces { + manager_date_time: all_surfaces.manager_date_time, + log_services: all_surfaces.log_services, + account_events: all_surfaces.account_events, + virtual_media: all_surfaces.virtual_media, + sensors: none, + } + match dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_collins_platform_ref, world: dry_world(bmc: bmc_with_record_surfaces(world: sel_world(), surfaces: no_sensors), store: empty_store)).outcome { + PriorLifeArchiveRefused { cause: c } => + match c { + PriorLifeAssessmentRefused { cause: a } => + match a { + RequiredCarrierNotArchivable { carrier: k, cause: _ } => (match k { PriorLifeSensorSnapshot => true _ => false }) + UnclearedBoundaryNotAdmittedByPolicy { platform: _ } => false + } + _ => false + } + _ => false + } +} + +// A POLICY THAT DOES NOT ADMIT THE UNCLEARED BOUNDARY REFUSES (SUPPLIED at the classifier: both +// production rows admit it), the production rows require all eight carriers, and a platform with no +// policy row refuses on the production path writing NOTHING: the store after the phase holds no object. +test fn w_a_policy_refusal_writes_nothing() -> Bool { + let full_captures = map(prior_life_carriers_all, c => CarrierCaptured { carrier: c, payload: PowerStatePayload { power: BmcPowerOn } }) + let not_admitting = PriorLifePolicy { platform: mt_jade_platform_ref, required: prior_life_carriers_all, uncleared_boundary: UnclearedBoundaryNotAdmitted } + let admitting = PriorLifePolicy { platform: mt_jade_platform_ref, required: prior_life_carriers_all, uncleared_boundary: UnclearedBoundaryAdmitted } + let mitchell = decl_ref(module_path: "extdeps.ocp.mt_mitchell.subject", decl_name: "MtMitchellSpecificationRevision") + let step = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mitchell, world: prior_life_full_dry_world()) + (match classify_prior_life_policy(policy: not_admitting, captures: full_captures) { Present { value: r } => (match r { UnclearedBoundaryNotAdmittedByPolicy { platform: _ } => true _ => false }) Absent => false }) + && (match classify_prior_life_policy(policy: admitting, captures: full_captures) { Present { value: _ } => false Absent => true }) + && (match step.outcome { PriorLifeArchiveRefused { cause: c } => (match c { PriorLifePolicyAbsent { platform: p } => declaration_ref_eq(a: p, b: mitchell) _ => false }) _ => false }) + && length(xs: step.store.objects) == 0 +} + + +// AN ARCHIVE ALREADY HELD IS A NOOP AND IS NOT WRITTEN TWICE. The first run writes and reads back +// (ArchiveWritten); the second, over the store the first left, finds the object at the archive's +// digest and is established with ArchiveAlreadyHeld, leaving exactly one object in the store. +test fn w_an_archive_already_held_is_a_noop_and_is_not_written_twice() -> Bool { + let first = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: prior_life_full_dry_world()) + let second = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_all_surfaces(), store: first.store)) + (match first.outcome { PriorLifeArchiveEstablished { receipt: r } => (match prior_life_receipt_application(r: r) { ArchiveWritten { write: _, within: _ } => true ArchiveAlreadyHeld => false }) _ => false }) + && (match second.outcome { PriorLifeArchiveEstablished { receipt: r } => (match prior_life_receipt_application(r: r) { ArchiveAlreadyHeld => true ArchiveWritten { write: _, within: _ } => false }) _ => false }) + && length(xs: first.store.objects) == 1 + && length(xs: second.store.objects) == 1 +} + +// INCOMPLETE IS NOT REFUSED. A store that loses the write, a store that corrupts it, and a write that +// returns forty-five seconds after it started, past its thirty-second budget, are each INCOMPLETE -- the write was attempted and its readback does +// not ground it -- and a write the store keeps, returning in two seconds, is established. +test fn w_a_lost_corrupted_or_late_write_is_incomplete_not_refused() -> Bool { + let losing = DryArchiveStore { objects: [], behaviour: DryArchiveStoreLosesWrites } + let corrupting = DryArchiveStore { objects: [], behaviour: DryArchiveStoreCorruptsWrites } + outcome_label(o: dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_all_surfaces(), store: losing)).outcome) == "incomplete:not-read-back" + && outcome_label(o: dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_all_surfaces(), store: corrupting)).outcome) == "incomplete:read-back-differs" + && outcome_label(o: dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: DryPriorLifeWorld { bmc: world_all_surfaces(), store: empty_store, read_at_millis: t_read_p, write_returned_at_millis: t_returned_late_p }).outcome) == "incomplete:deadline-elapsed" + && outcome_label(o: dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: prior_life_full_dry_world()).outcome) == "established" +} + +// THE DEADLINE READS ITS OWN BUDGET (lesson 2: vary only that field). The same leg, the same start and +// the same finish forty seconds later: under a thirty-second budget it ELAPSED, under a fifty-second +// budget it COMPLETED WITHIN. A finish before the start, and a finish the clock could not read, are +// neither. +test fn w_a_budget_that_differs_only_in_its_duration_flips_completed_to_elapsed() -> Bool { + let leg = decl_ref(module_path: "gunbc.machine_intake_prior_life_boundary", decl_name: "dry_write_archive") + let start = observer_clock_modeled(millis: 1791158400000, realization: "test.claim.machine_intake_prior_life_boundary_witness schedule" as NonEmptyStr) + let finish = observer_clock_modeled(millis: 1791158440000, realization: "test.claim.machine_intake_prior_life_boundary_witness schedule" as NonEmptyStr) + let short = effect_leg_deadline(budget: leg_budget(leg: leg, budget: positive_millisecond(count: PositiveMeasureSuccessor { predecessor: 29999 })), started: start) + let long = effect_leg_deadline(budget: leg_budget(leg: leg, budget: positive_millisecond(count: PositiveMeasureSuccessor { predecessor: 49999 })), started: start) + (match complete_effect_leg(deadline: short, finished: ObserverClockObserved { instant: finish }) { LegDeadlineElapsed { deadline: _, finished: _ } => true _ => false }) + && (match complete_effect_leg(deadline: long, finished: ObserverClockObserved { instant: finish }) { LegCompletedWithin { completed: _ } => true _ => false }) + && (match complete_effect_leg(deadline: effect_leg_deadline(budget: leg_budget(leg: leg, budget: positive_millisecond(count: PositiveMeasureSuccessor { predecessor: 49999 })), started: finish), finished: ObserverClockObserved { instant: start }) { LegFinishedBeforeItStarted { deadline: _, finished: _ } => true _ => false }) + && (match complete_effect_leg(deadline: long, finished: ObserverClockUnreadable { detail: "clock refused" }) { LegCompletionUnobserved { deadline: _, detail: _ } => true _ => false }) +} + +// THE CURSOR IS THE ARCHIVE'S: an established receipt's boundary is LogsArchivedWithBaselineCursor, its +// cursor names the last SEL record the archive holds and the archive's own digest, and the receipt +// names the dry realization it came from. +test fn w_the_baseline_cursor_is_derived_from_the_archive_it_was_read_from() -> Bool { + match dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_collins_platform_ref, world: prior_life_full_dry_world()).outcome { + PriorLifeArchiveEstablished { receipt: r } => + match prior_life_receipt_boundary(r: r) { + LogsArchivedWithBaselineCursor { cursor: c } => + (match baseline_cursor_sel_final_record(c: c) { Present { value: id } => id == "2" Absent => false }) + && content_hash_equal(left: baseline_cursor_archive(c: c), right: prior_life_archive_digest(a: prior_life_receipt_archive(r: r))) + && ((prior_life_receipt_realization(r: r) as NonEmptyStr) as String) == "gunbc.machine_intake_prior_life_boundary dry realization over gunbc.bmc_model BmcWorld and a dry archive store" + } + _ => false + } +} + +// ── THE ENCODING IS INJECTIVE (side-chat review of 31ef3dbe8c) ───────────────────────────────────── + +// A world that differs from the full world only in its one log service's entries. +fn world_with_log(entries: List) -> BmcWorld { + bmc_with_record_surfaces(world: sel_world(), surfaces: BmcRecordSurfaces { + manager_date_time: all_surfaces.manager_date_time, + log_services: Present { value: [RedfishLogService { id: "EventLog", entries: entries }] }, + account_events: all_surfaces.account_events, + virtual_media: all_surfaces.virtual_media, + sensors: all_surfaces.sensors, + }) +} + +// A world that differs from the full world only in its one virtual-media member. +fn world_with_media(member: RedfishVirtualMediaObservation) -> BmcWorld { + bmc_with_record_surfaces(world: sel_world(), surfaces: BmcRecordSurfaces { + manager_date_time: all_surfaces.manager_date_time, + log_services: all_surfaces.log_services, + account_events: all_surfaces.account_events, + virtual_media: Present { value: [member] }, + sensors: all_surfaces.sensors, + }) +} + +fn final_event_log_entry(o: PriorLifeArchiveOutcome) -> Int? { + match o { + PriorLifeArchiveEstablished { receipt: r } => + match prior_life_receipt_boundary(r: r) { + LogsArchivedWithBaselineCursor { cursor: c } => + match baseline_cursor_log_services(c: c) |> first() { + Present { value: lc } => lc.final_entry + Absent => none + } + } + _ => none + } +} + +fn written_not_held(o: PriorLifeArchiveOutcome) -> Bool { + match o { + PriorLifeArchiveEstablished { receipt: r } => (match prior_life_receipt_application(r: r) { ArchiveWritten { write: _, within: _ } => true ArchiveAlreadyHeld => false }) + _ => false + } +} + +fn digests_differ(a: PriorLifeArchiveOutcome, b: PriorLifeArchiveOutcome) -> Bool { + match a { + PriorLifeArchiveEstablished { receipt: ra } => + match b { + PriorLifeArchiveEstablished { receipt: rb } => + content_hash_equal(left: prior_life_archive_digest(a: prior_life_receipt_archive(r: ra)), right: prior_life_archive_digest(a: prior_life_receipt_archive(r: rb))) == false + && ((prior_life_archive_body(a: prior_life_receipt_archive(r: ra)) as NonEmptyStr) as String) != ((prior_life_archive_body(a: prior_life_receipt_archive(r: rb)) as NonEmptyStr) as String) + _ => false + } + _ => false + } +} + +// THE REVIEW'S TWO-LOG COUNTEREXAMPLE. One log service, two entries each; a delimiter-joined encoding +// rendered both as the same three lines while A's last entry is 3 and B's is 2. Now A and B archive +// to different bytes and digests; B observed over the store A's archive was written to is NOT held +// (no ArchiveAlreadyHeld receipt with A's archive), so B is written and established with B's own +// cursor, final entry 2, and A's with final entry 3. +test fn w_two_log_populations_that_a_delimiter_join_conflated_archive_distinctly() -> Bool { + let a = [RedfishLogEntry { id: 1, severity: "OK", message: "a\n2|OK|b" }, RedfishLogEntry { id: 3, severity: "OK", message: "c" }] + let b = [RedfishLogEntry { id: 1, severity: "OK", message: "a" }, RedfishLogEntry { id: 2, severity: "OK", message: "b\n3|OK|c" }] + let first = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_log(entries: a), store: empty_store)) + let second = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_log(entries: b), store: first.store)) + digests_differ(a: first.outcome, b: second.outcome) + && written_not_held(o: second.outcome) + && final_event_log_entry(o: first.outcome) == Present { value: 3 } + && final_event_log_entry(o: second.outcome) == Present { value: 2 } +} + +// EVERY MODELED VIRTUAL-MEDIA FIELD IS ARCHIVED: a member that differs only in connected_via, and one +// that differs only in media_types, each archive to a different digest from the base member, and each +// is written rather than read as held over the base member's store. +test fn w_virtual_media_connected_via_and_media_types_are_archived() -> Bool { + let base = RedfishVirtualMediaObservation { locator: RedfishVirtualMediaLocator { parent: UnderManager { manager_id: "bmc" }, media_id: "CD1" }, media_types: [MediaCd], connected_via: ConnectedViaNotConnected, inserted: false, image: none } + let via = RedfishVirtualMediaObservation { locator: base.locator, media_types: [MediaCd], connected_via: ConnectedViaUri, inserted: false, image: none } + let types = RedfishVirtualMediaObservation { locator: base.locator, media_types: [MediaCd, MediaDvd], connected_via: ConnectedViaNotConnected, inserted: false, image: none } + let on_base = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_media(member: base), store: empty_store)) + let on_via = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_media(member: via), store: on_base.store)) + let on_types = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_media(member: types), store: on_base.store)) + digests_differ(a: on_base.outcome, b: on_via.outcome) + && digests_differ(a: on_base.outcome, b: on_types.outcome) + && written_not_held(o: on_via.outcome) + && written_not_held(o: on_types.outcome) +} + +// THE LOCATOR'S FIELD BOUNDARIES ARE ARCHIVED (side-chat review of 5143906158). These two locators +// render the same resource path -- /redfish/v1/Managers/a/VirtualMedia/b/VirtualMedia/c -- because the +// path joins a manager ID and a media ID that may themselves carry the separator. Held otherwise +// constant, they archive to different bytes and digests, and B over the store A was written to is +// written, not held. The unchanged locator over its own store is held (the positive). +test fn w_two_locators_that_render_one_resource_path_archive_distinctly() -> Bool { + let a = RedfishVirtualMediaObservation { locator: RedfishVirtualMediaLocator { parent: UnderManager { manager_id: "a/VirtualMedia/b" }, media_id: "c" }, media_types: [MediaCd], connected_via: ConnectedViaNotConnected, inserted: false, image: none } + let b = RedfishVirtualMediaObservation { locator: RedfishVirtualMediaLocator { parent: UnderManager { manager_id: "a" }, media_id: "b/VirtualMedia/c" }, media_types: [MediaCd], connected_via: ConnectedViaNotConnected, inserted: false, image: none } + let on_a = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_media(member: a), store: empty_store)) + let on_b = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_media(member: b), store: on_a.store)) + let a_again = dry_archive_prior_life(key: key_p(), consumed_identity: identity_p(), subject: subject_p(), platform: mt_jade_platform_ref, world: dry_world(bmc: world_with_media(member: a), store: on_a.store)) + redfish_virtual_media_resource_path(locator: a.locator) == redfish_virtual_media_resource_path(locator: b.locator) + && digests_differ(a: on_a.outcome, b: on_b.outcome) + && written_not_held(o: on_b.outcome) + && (match a_again.outcome { PriorLifeArchiveEstablished { receipt: r } => (match prior_life_receipt_application(r: r) { ArchiveAlreadyHeld => true ArchiveWritten { write: _, within: _ } => false }) _ => false }) +}