Managed-host cut O1c-2: PriorLifeBoundary archive, effect-leg deadlines, incomplete vs refused (dry)

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<RedfishLogEntry>
+}
+
 fn redfish_log_entry(v: JsonValue) -> ObservationAttempt<RedfishLogEntry, NonEmptyStr> {
   match read_string_member(v: v, key: "Id") {
     MemberString { value: id_text } => match parse_int(s: id_text) {

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<RedfishLogService>?
+  account_events: List<RedfishLogEntry>?
+  virtual_media: List<RedfishVirtualMediaObservation>?
+  sensors: List<RedfishTelemetryPoint>?
+}
+
+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<BmcIpmiUser>
   ipmi_user_access: List<IpmiUserChannelAccess>
+  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<BmcScheduledEvent>, 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<BmcIpmiUser>) -> 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<IpmiUserChannelAccess>)
     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,
   }
 }
 

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 } }