diff --git a/dag/extdeps/bmc/ipmitool_observed_output.dag b/dag/extdeps/bmc/ipmitool_observed_output.dag new file mode 100644 index 00000000000..8d6583ae89b --- /dev/null +++ b/dag/extdeps/bmc/ipmitool_observed_output.dag @@ -0,0 +1,67 @@ +module extdeps.bmc.ipmitool_observed_output + +import std.types { Int, NonEmptyStr, String } +import extdeps.external_authority { ExternalAuthority, CitedFigureStanding, TranscribedUncited } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/ipmitool/ipmitool" + } +} + +// WHAT ipmitool PRINTS, AS OBSERVED ON THE MT. COLLINS AMI MEGARAC BUILD. Each row is the client's +// output format for one operation, taken verbatim from a retained capture and cited by that capture's +// path and SHA-256, so a modeled realization renders exactly what the production decoder was built to +// read. These are client-format facts about the upstream tool on one controller build, not +// facts about any scenario; a row whose value is not in a retained capture says so in its standing. + +// `ipmitool chassis bootparam get 5` with no override pending. Source: run 36335369059 +// mtcollins1-boot-diagnostics.txt (sha256 eda19cde2e60d90d3d04946273e615eb5bf774496b9907e03d3bc15dbedc2c1c), +// "boot parameter 5 before", verbatim including the trailing space after "legacy) boot". +data ipmitool_bootparam5_no_override: String = "Boot parameter version: 1\nBoot parameter 5 is valid/unlocked\nBoot parameter data: 0000000000\n Boot Flags :\n - Boot Flag Invalid\n - Options apply to only next boot\n - BIOS PC Compatible (legacy) boot \n - Boot Device Selector : No override\n - BIOS verbosity : System Default\n - Console Redirection control : Console redirection occurs per BIOS configuration setting (default)\n - BIOS Mux Control Override : BIOS uses recommended setting of the mux at the end of POST\n" + +// The same read after `chassis bootdev cdrom options=efiboot`. Source: artifacts/bmc/mtcollins1-32dimm/30-bootdev.txt +// (sha256 6488554239e12f033203c9589285bd6ce27dfb5716658be931e2422ea238c4ba), the readback block. +data ipmitool_bootparam5_cdrom_efi_next_boot: String = "Boot parameter version: 1\nBoot parameter 5 is valid/unlocked\nBoot parameter data: a014000000\n Boot Flags :\n - Boot Flag Valid\n - Options apply to only next boot\n - BIOS EFI boot \n - Boot Device Selector : Force Boot from CD/DVD\n - BIOS verbosity : System Default\n - Console Redirection control : Console redirection occurs per BIOS configuration setting (default)\n - BIOS Mux Control Override : BIOS uses recommended setting of the mux at the end of POST\n" + +// `ipmitool chassis bootdev cdrom options=efiboot`. Same capture, line 2. +data ipmitool_bootdev_cdrom_reply: String = "Set Boot Device to cdrom\n" + +// What `ipmitool sol activate` prints first when its stdin is not a terminal. Source: +// artifacts/bmc/mtcollins1-32dimm/22-sol-probe.log (sha256 e24f9ed8d9cedff87e6d11327c602c31fd7c3d9e2ba16e7e1ab0f8a91cdfe41e), +// lines 1-2. +data ipmitool_sol_activate_preamble: String = "tcgetattr: Inappropriate ioctl for device\n[SOL Session operational. Use ~? for help]\n" + +// One `ipmitool sel elist` line: the record id in lowercase hex right-aligned in four columns, then +// date, time, sensor, event and state separated by ` | `. Source: artifacts/bmc/mtcollins1-32dimm/50-sel-final.txt +// (sha256 14e84cd9cbd2d89d6be46caff42c3d5ab0a19079fa4546d6e6ec449f759c7ba5) and the diagnostics capture above +// (ids ` 1` and ` b5a`). +fn ipmitool_sel_elist_line(record_id_hex: String, date: String, time: String, sensor: String, event: String, state: String) -> String { + let pad = if string_length(s: record_id_hex) >= 4 { "" } else if string_length(s: record_id_hex) == 3 { " " } else if string_length(s: record_id_hex) == 2 { " " } else { " " } + join([pad, record_id_hex, " | ", date, " | ", time, " | ", sensor, " | ", event, " | ", state, "\n"], "") +} + +// `ipmitool raw 0x06 0x52 ...` (Master Write-Read) answering two bytes. NO SMpro exchange with this +// controller is retained in the corpus (gunbc.machine_intake_mtcollins1_smpro_observation witness +// notes), so the spacing is ipmitool's raw-response print as the production decoder's own supplied +// samples spell it, and is carried with that standing. +data ipmitool_raw_two_bytes_standing: CitedFigureStanding = TranscribedUncited { + read_obligation: "a retained stdout of `ipmitool raw 0x06 0x52 2 ` against the Mt. Collins BMC, cited by digest" as NonEmptyStr +} + +fn ipmitool_raw_two_bytes(first_hex: String, second_hex: String) -> String { + join([" ", first_hex, " ", second_hex, "\n"], "") +} + +// `ipmitool mc info` against the Mt. Collins BMC: the two fields the corpus has read from this +// controller -- Firmware Revision 0.32 and IPMI Version 2.0 (gunbc.machine_intake_mtcollins1_access_observation) +// in ipmitool's ` : ` field layout. No verbatim stdout is retained, so the layout, and +// the absence of the other fields ipmitool prints, carry this standing. The boot's reachability read +// consumes only the exit and stderr. +data ipmitool_mc_info_standing: CitedFigureStanding = TranscribedUncited { + read_obligation: "a retained stdout of `ipmitool mc info` against the Mt. Collins BMC, cited by digest" as NonEmptyStr +} + +data ipmitool_mc_info_mt_collins: String = "Firmware Revision : 0.32\nIPMI Version : 2.0\n" diff --git a/dag/extdeps/bmc/megarac_observed_output.dag b/dag/extdeps/bmc/megarac_observed_output.dag new file mode 100644 index 00000000000..6633306a62b --- /dev/null +++ b/dag/extdeps/bmc/megarac_observed_output.dag @@ -0,0 +1,73 @@ +module extdeps.bmc.megarac_observed_output + +import std.types { Int, NonEmptyStr, String } +import extdeps.external_authority { ExternalAuthority, CitedFigureStanding, TranscribedUncited } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.ami.com/megarac/" + } +} + +// WHAT THE Mt. Collins MegaRAC (firmware 0.32) ANSWERS ON ITS MEDIA REST ROUTES, as observed. Each +// renderer reproduces a retained body's key order and spelling, with the fields a scenario varies +// substituted; its source is cited beside it. A body no retained exchange carries says so in its +// standing -- the production decoder reads only the members named there, and the rest of the body is +// the firmware's form as far as it has been read. + +// GET /api/settings/media/general. Source: test.claim.machine_intake.megarac_media_convergence_witness_test +// mtcollins1_media_general_2026_09_27, a read-only GET at 2026-09-27T18:37:18Z after boot run 36330382023, +// verbatim, with the share, mount and CD error code as parameters. The firmware escapes `/` as `\/`. +fn megarac_media_general_body(server: String, source_path: String, share_type: String, mount_cd: Int, cd_error_code: Int) -> String { + join([ + "{ \"id\": 1, \"local_media_support\": 0, \"remote_media_support\": 1, \"same_settings\": 0, \"cd_remote_server_address\": \"", server, + "\", \"cd_remote_source_path\": \"", json_escaped_slashes(s: source_path), + "\", \"cd_remote_share_type\": \"", share_type, + "\", \"cd_remote_domain_name\": \"\", \"cd_remote_user_name\": \"\", \"mount_cd\": ", to_string(mount_cd), + ", \"cd_image_name\": \"\", \"cd_error_code\": ", to_string(cd_error_code), + ", \"mount_hd\": 0, \"hd_remote_server_address\": \"\", \"hd_remote_source_path\": \"\", \"hd_remote_share_type\": \"\", \"hd_remote_domain_name\": \"\", \"hd_remote_user_name\": \"\", \"hd_image_name\": \"\", \"hd_error_code\": 0, \"rmedia_retry_count\": 3, \"rmedia_retry_interval\": 15 }", + ], "") +} + +fn json_escaped_slashes(s: String) -> String { + join(split(s: s, delimiter: "/"), "\\/") +} + +// One row of GET /api/settings/media/remote/configurations. Source: the cleared row retained in +// test.claim.machine_intake.megarac_media_convergence_witness_test +// (`[{"media_type":1,"image_name":"","redirection_status":0,"media_index":0,"session_index":255}]`), +// with the image, status and indices as parameters. +fn megarac_configuration_row(image_name: String, redirection_status: Int, media_index: Int, session_index: Int) -> String { + join(["{\"media_type\":1,\"image_name\":\"", image_name, "\",\"redirection_status\":", to_string(redirection_status), ",\"media_index\":", to_string(media_index), ",\"session_index\":", to_string(session_index), "}"], "") +} + +// One row of GET /api/settings/media/remote/images. Source: the listing row in the same witness, +// `{"image_name":"","image_index":5}`, with the index the real attach logs report. +fn megarac_image_row(image_name: String, image_index: Int) -> String { + join(["{\"image_name\":\"", image_name, "\",\"image_index\":", to_string(image_index), "}"], "") +} + +// The rejection a route gives a request without a valid session. Source: +// test.claim.machine_intake.megarac_session_release_witness_test, `{"error":"invalid session"}` with 401. +data megarac_invalid_session_body: String = "{\"error\":\"invalid session\"}" + +// POST /api/session. NO SESSION REPLY IS RETAINED VERBATIM. The member names are those the firmware's +// own web UI reads (source.min.js, probed 2026-09-27 on branch session/eager-koi-811), and the production +// decoder reads only CSRFToken. +data megarac_session_body_standing: CitedFigureStanding = TranscribedUncited { + read_obligation: "a retained POST /api/session reply from the Mt. Collins MegaRAC, cited by digest" as NonEmptyStr +} + +fn megarac_session_body(racsession_id: Int, csrf_token: String) -> String { + join(["{ \"ok\": 0, \"privilege\": 4, \"extendedpriv\": 259, \"racsession_id\": ", to_string(racsession_id), ", \"CSRFToken\": \"", csrf_token, "\" }"], "") +} + +// The replies to start-media, stop-media and DELETE /api/session on success are not decoded by the +// production code (readiness and re-observation decide), and none is retained verbatim. +data megarac_write_ack_body_standing: CitedFigureStanding = TranscribedUncited { + read_obligation: "retained 200 bodies of start-media, stop-media and DELETE /api/session from the Mt. Collins MegaRAC, cited by digest" as NonEmptyStr +} + +data megarac_write_ack_body: String = "{}" diff --git a/dag/extdeps/transports/file.dag b/dag/extdeps/transports/file.dag index 830f6d17267..cddd7a67933 100644 --- a/dag/extdeps/transports/file.dag +++ b/dag/extdeps/transports/file.dag @@ -1,6 +1,8 @@ module extdeps.transports.file -import std.types { FermiDepth } +import std.types { FermiDepth, Int, String } +import std.measure { ByteSize, byte_size_count } +import extdeps.filesystem.filesystem_io { FilesystemFailureKind } import std.fidelity { TransportFidelity } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -17,3 +19,20 @@ data file_transport_fidelity: TransportFidelity = TransportFidelity { depth: S, type FileTransportConfig { base_path: String } + +// WHAT THE FILE TRANSPORT OBSERVES, as a value: an operation that succeeded with its byte count and +// any content it read or listed, or one that failed with the host's CLOSED failure kind and its +// message. This is the observation a modeled operation realization (v2.std.operation_realization) +// supplies in place of a real filesystem call; the interpreter feeds it to the same declared-output +// projection a real file result reaches, so success, error, error_kind, content and byte_count are +// derived exactly as from a real call. A listing's content follows the realization's own contract: +// the entry names, sorted, one per line. +type FileExchangeObservation + = FileOperationSucceeded { byte_count: ByteSize, content: String } + | FileOperationFailed { kind: FilesystemFailureKind, error: String } + +// The byte count as the host integer the file transport's `byte_count` output field carries; the +// dispatcher reads a modeled observation's count through this rather than decoding the measure. +fn file_observation_byte_count(bytes: ByteSize) -> Int { + byte_size_count(b: bytes) as Int +} diff --git a/dag/extdeps/units/iso8601_calendar.dag b/dag/extdeps/units/iso8601_calendar.dag new file mode 100644 index 00000000000..c145d6b3853 --- /dev/null +++ b/dag/extdeps/units/iso8601_calendar.dag @@ -0,0 +1,80 @@ +module extdeps.units.iso8601_calendar + +import std.types { Int, String } +import extdeps.units.iso8601 { iso8601_seconds_per_minute, iso8601_minutes_per_hour, iso8601_hours_per_day } + +// THE ISO 8601 CALENDAR over extdeps.units.iso8601's time-unit constants: the proleptic Gregorian day +// count in both directions, the month-length rule, and the UTC text form. It is a module of its own, +// beside the constants rather than inside them, because std.measure imports the constants and so puts +// that module in the compiler seed's closure; the calendar has no compiler consumer, and adding it +// there would grow the seed for nothing. +fn iso8601_seconds_per_hour() -> Int { + (iso8601_minutes_per_hour() as Int) * (iso8601_seconds_per_minute() as Int) +} + +fn iso8601_seconds_per_day() -> Int { + (iso8601_hours_per_day() as Int) * iso8601_seconds_per_hour() +} + +// THE PROLEPTIC GREGORIAN CALENDAR THE DATE FORMAT SPELLS, in both directions over one day count +// (days since 1970-01-01): H. Hinnant, "chrono-Compatible Low-Level Date Algorithms", +// days_from_civil and civil_from_days -- exact over the whole range, no table. +type Iso8601CivilDate { + year: Int + month: Int + day: Int +} + +fn iso8601_floor_div(a: Int, b: Int) -> Int { + if a >= 0 { a / b } else { 0 - ((0 - a + b - 1) / b) } +} + +fn iso8601_days_from_civil(y: Int, m: Int, d: Int) -> Int { + let yy = if m <= 2 { y - 1 } else { y } + let era = iso8601_floor_div(a: yy, b: 400) + let yoe = yy - era * 400 + let mp = if m > 2 { m - 3 } else { m + 9 } + let doy = (153 * mp + 2) / 5 + d - 1 + let doe = yoe * 365 + yoe / 4 - yoe / 100 + doy + era * 146097 + doe - 719468 +} + +fn iso8601_civil_from_days(days: Int) -> Iso8601CivilDate { + let z = days + 719468 + let era = iso8601_floor_div(a: z, b: 146097) + let doe = z - era * 146097 + let yoe = (doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 + let y = yoe + era * 400 + let doy = doe - (365 * yoe + yoe / 4 - yoe / 100) + let mp = (5 * doy + 2) / 153 + let d = doy - (153 * mp + 2) / 5 + 1 + let m = if mp < 10 { mp + 3 } else { mp - 9 } + Iso8601CivilDate { year: if m <= 2 { y + 1 } else { y }, month: m, day: d } +} + +// The day-in-month bound with the leap rule, so a calendar-impossible day (Feb 30, Apr 31) is refused +// by a reader rather than normalized through the day count. +fn iso8601_gregorian_days_in_month(y: Int, m: Int) -> Int { + if m == 2 { + if y - (y / 4) * 4 == 0 && (y - (y / 100) * 100 != 0 || y - (y / 400) * 400 == 0) { 29 } else { 28 } + } else if m == 4 || m == 6 || m == 9 || m == 11 { 30 } else { 31 } +} + +fn iso8601_two_digits(n: Int) -> String { + if n < 10 { concat("0", to_string(n)) } else { to_string(n) } +} + +// Seconds since 1970-01-01T00:00:00Z to the UTC basic-extended form `YYYY-MM-DDThh:mm:ssZ`, the form +// `date -u +%Y-%m-%dT%H:%M:%SZ` prints; the inverse of a reader of that form over the same day count. +fn iso8601_utc_text(unix: Int) -> String { + let days = iso8601_floor_div(a: unix, b: iso8601_seconds_per_day()) + let rem = unix - days * iso8601_seconds_per_day() + let hour = rem / iso8601_seconds_per_hour() + let within_hour = rem - hour * iso8601_seconds_per_hour() + let minute = within_hour / (iso8601_seconds_per_minute() as Int) + let date = iso8601_civil_from_days(days: days) + join([ + to_string(date.year), "-", iso8601_two_digits(n: date.month), "-", iso8601_two_digits(n: date.day), + "T", iso8601_two_digits(n: hour), ":", iso8601_two_digits(n: minute), ":", iso8601_two_digits(n: within_hour - minute * (iso8601_seconds_per_minute() as Int)), "Z", + ], "") +} diff --git a/dag/gunbc/bmc_dry_realization.dag b/dag/gunbc/bmc_dry_realization.dag index 0fff5d963a8..7f7fa113851 100644 --- a/dag/gunbc/bmc_dry_realization.dag +++ b/dag/gunbc/bmc_dry_realization.dag @@ -1,6 +1,6 @@ module gunbc.bmc_dry_realization -import std.types { Bool, List, NonEmptyStr, String } +import std.types { Bool, Int, List, NonEmptyStr, String } import std.measure { Second, second } import v2.std.operation_argv { OperationRef } import v2.std.operation_realization { @@ -12,7 +12,25 @@ import extdeps.transports.shell { ShellProcessExited } import extdeps.bmc.ipmi_chassis_control { ipmi_chassis_control_action_of_verb, ipmitool_chassis_status_power_line, ipmitool_chassis_power_control_reply, } -import gunbc.bmc_model { BmcWorld, bmc_chassis_control, bmc_power_is_on, bmc_advance } +import gunbc.bmc_model { + BmcWorld, bmc_chassis_control, bmc_power_is_on, bmc_advance, bmc_with_override, + BootOverrideNone, BootOverrideCdromEfiNextBoot, +} +import gunbc.megarac_media_model { + MegaRacMediaWorld, megarac_session_valid, megarac_open_session, megarac_close_session, + megarac_start_media, megarac_stop_media, +} +import extdeps.bmc.megarac_observed_output { + megarac_media_general_body, megarac_configuration_row, megarac_image_row, megarac_invalid_session_body, + megarac_session_body, megarac_write_ack_body, +} +import extdeps.languages.json.parse { parse_json_document, JsonDocumentParsed, JsonDocumentUnreadable } +import gunbc.machine_intake_megarac_media_attach { json_string_member, json_number_member } +import extdeps.bmc.ipmitool_observed_output { + ipmitool_mc_info_mt_collins, + ipmitool_bootparam5_no_override, ipmitool_bootparam5_cdrom_efi_next_boot, ipmitool_bootdev_cdrom_reply, + ipmitool_sel_elist_line, +} // THE DRY ADAPTER BETWEEN THE extdeps.bmc INTERFACE AND THE ONE BMC MODEL. For each bound operation // it reads the actual inputs the dispatcher bound, asks gunbc.bmc_model for the transition, and @@ -38,38 +56,205 @@ fn bmc_ipmi_operation(operation: String) -> OperationRef { OperationRef { path: bmc_ipmi_operation_path, service: bmc_ipmi_service, operation: operation } } -fn exited(stdout: String, world: BmcWorld) -> OperationStep { - OperationObserved { - observation: ShellObserved { observation: ShellProcessExited { exit_code: 0, stdout: stdout, stderr: "" } }, - state: world, - elapsed: second(count: 1), - } -} +// ONE BMC COMMAND'S RESULT BEFORE IT IS PLACED IN A SCENARIO: the stdout the client would print and the +// world after it, or a harness fault. Handlers are written over the BMC world alone; bmc_bindings lifts +// them through a lens into whatever scenario state embeds the world. +type BmcReply + = BmcReplied { stdout: String, world: BmcWorld } + | BmcReplyFault { reason: NonEmptyStr } -fn bmc_chassis_status_handler(world: BmcWorld, call: OperationCall) -> OperationStep { - exited(stdout: ipmitool_chassis_status_power_line(power_on: bmc_power_is_on(world: world)), world: world) +fn bmc_chassis_status_reply(world: BmcWorld, call: OperationCall) -> BmcReply { + BmcReplied { stdout: ipmitool_chassis_status_power_line(power_on: bmc_power_is_on(world: world)), world: world } } -fn bmc_chassis_power_control_handler(world: BmcWorld, call: OperationCall) -> OperationStep { +fn bmc_chassis_power_control_reply(world: BmcWorld, call: OperationCall) -> BmcReply { match operation_input_text(invocation: call.invocation, name: "action") { - Absent => OperationHarnessFault { reason: "ChassisPowerControl was dispatched without an action input" as NonEmptyStr } + Absent => BmcReplyFault { reason: "ChassisPowerControl was dispatched without an action input" as NonEmptyStr } Present { value: verb } => match ipmi_chassis_control_action_of_verb(verb: verb) { - Absent => OperationHarnessFault { reason: join(["ChassisPowerControl action `", verb, "` names no IPMI chassis control action the model carries"], "") as NonEmptyStr } - Present { value: action } => exited(stdout: ipmitool_chassis_power_control_reply(action: action), world: bmc_chassis_control(world: world, action: action).world) + Absent => BmcReplyFault { reason: join(["ChassisPowerControl action `", verb, "` names no IPMI chassis control action the model carries"], "") as NonEmptyStr } + Present { value: action } => BmcReplied { stdout: ipmitool_chassis_power_control_reply(action: action), world: bmc_chassis_control(world: world, action: action, now: call.now).world } + } + } +} + +fn input_is(call: OperationCall, name: String, expected: String) -> Bool { + match operation_input_text(invocation: call.invocation, name: name) { + Present { value: v } => v == expected + Absent => false + } +} + +fn bmc_bootparam_get_reply(world: BmcWorld, call: OperationCall) -> BmcReply { + if input_is(call: call, name: "parameter", expected: "5") { + BmcReplied { + stdout: match world.boot_override { + BootOverrideNone => ipmitool_bootparam5_no_override + BootOverrideCdromEfiNextBoot => ipmitool_bootparam5_cdrom_efi_next_boot + }, + world: world, } + } else { + BmcReplyFault { reason: "the model answers boot parameter 5 only" as NonEmptyStr } } } +// The override this controller has been observed to take: cdrom, EFI, next boot only. Any other +// device or option set is a request the model does not carry, and it refuses rather than guessing. +fn bmc_bootdev_reply(world: BmcWorld, call: OperationCall) -> BmcReply { + if input_is(call: call, name: "device", expected: "cdrom") && input_is(call: call, name: "options", expected: "efiboot") { + BmcReplied { stdout: ipmitool_bootdev_cdrom_reply, world: bmc_with_override(world: world, over: BootOverrideCdromEfiNextBoot) } + } else { + BmcReplyFault { reason: "the model carries the cdrom boot override with options=efiboot only" as NonEmptyStr } + } +} + +fn bmc_sel_elist_reply(world: BmcWorld, call: OperationCall) -> BmcReply { + BmcReplied { stdout: join(map(world.sel, r => ipmitool_sel_elist_line(record_id_hex: r.id_hex, date: r.date, time: r.time, sensor: r.sensor, event: r.event, state: r.state)), ""), world: world } +} + +// `mc info` answers whenever the management controller does, whatever the host's power or SOL state. +fn bmc_mc_info_reply(world: BmcWorld, call: OperationCall) -> BmcReply { + BmcReplied { stdout: ipmitool_mc_info_mt_collins, world: world } +} + +// One IPMI round trip takes one virtual second. +fn bmc_lift(get: fn(S) -> BmcWorld, put: fn(S, BmcWorld) -> S, reply: fn(BmcWorld, OperationCall) -> BmcReply) -> fn(S, OperationCall) -> OperationStep { + fn(state, call) { + match reply(get(state), call) { + BmcReplyFault { reason: r } => OperationHarnessFault { reason: r } + BmcReplied { stdout: out, world: w } => OperationObserved { + observation: ShellObserved { observation: ShellProcessExited { exit_code: 0, stdout: out, stderr: "" } }, + state: put(state, w), + elapsed: second(count: 1), + } + } + } +} + +fn bmc_bindings(get: fn(S) -> BmcWorld, put: fn(S, BmcWorld) -> S) -> List> { + [ + OperationBinding { at: bmc_ipmi_operation(operation: "ChassisStatus"), handler: bmc_lift(get: get, put: put, reply: bmc_chassis_status_reply) }, + OperationBinding { at: bmc_ipmi_operation(operation: "ChassisPowerControl"), handler: bmc_lift(get: get, put: put, reply: bmc_chassis_power_control_reply) }, + OperationBinding { at: bmc_ipmi_operation(operation: "ChassisBootParamGet"), handler: bmc_lift(get: get, put: put, reply: bmc_bootparam_get_reply) }, + OperationBinding { at: bmc_ipmi_operation(operation: "ChassisBootDevWithOptions"), handler: bmc_lift(get: get, put: put, reply: bmc_bootdev_reply) }, + OperationBinding { at: bmc_ipmi_operation(operation: "SelListAuthenticated"), handler: bmc_lift(get: get, put: put, reply: bmc_sel_elist_reply) }, + OperationBinding { at: bmc_ipmi_operation(operation: "SelListAuthenticatedCached"), handler: bmc_lift(get: get, put: put, reply: bmc_sel_elist_reply) }, + OperationBinding { at: bmc_ipmi_operation(operation: "McInfo"), handler: bmc_lift(get: get, put: put, reply: bmc_mc_info_reply) }, + ] +} + +fn bmc_chassis_power_control_handler(world: BmcWorld, call: OperationCall) -> OperationStep { + let handler = bmc_lift(get: fn(w) { w }, put: fn(w, next) { next }, reply: bmc_chassis_power_control_reply) + handler(world, call) +} + fn bmc_dry_realization(identity: NonEmptyStr, initial: BmcWorld, epoch: Second) -> OperationRealization { OperationRealization { identity: identity, initial: initial, epoch: epoch, - bindings: [ - OperationBinding { at: bmc_ipmi_operation(operation: "ChassisStatus"), handler: bmc_chassis_status_handler }, - OperationBinding { at: bmc_ipmi_operation(operation: "ChassisPowerControl"), handler: bmc_chassis_power_control_handler }, + bindings: list_append( + bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }), virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"), - ], + ), advance: bmc_advance, } } + +// THE MEGARAC MEDIA ROUTES, answered over the media model as curl --fail-with-body sees them: a +// request with a valid session gets the firmware's body and exit 0; one without gets the 401 body on +// stdout, curl's own error line on stderr, and exit 22 (curl(1), --fail-with-body). The session probe's +// `-w "\n%{http_code}"` appends the status line. One request takes one virtual second. +data megarac_operation_path: String = "dag/extdeps/bmc/megarac.dag" + +fn megarac_operation(operation: String) -> OperationRef { + OperationRef { path: megarac_operation_path, service: "megarac.Media", operation: operation } +} + +fn curl_answer(state: S, exit_code: Int, stdout: String, stderr: String) -> OperationStep { + OperationObserved { observation: ShellObserved { observation: ShellProcessExited { exit_code: exit_code, stdout: stdout, stderr: stderr } }, state: state, elapsed: second(count: 1) } +} + +fn curl_refused_401(state: S, with_status_line: Bool) -> OperationStep { + curl_answer(state: state, exit_code: 22, stdout: if with_status_line { concat(megarac_invalid_session_body, "\n401") } else { megarac_invalid_session_body }, stderr: "curl: (22) The requested URL returned error: 401\n") +} + +fn call_text(call: OperationCall, name: String) -> String { + match operation_input_text(invocation: call.invocation, name: name) { Present { value: v } => v Absent => "" } +} + +fn megarac_configurations_body(media: MegaRacMediaWorld) -> String { + concat("[", concat(megarac_configuration_row(image_name: media.cd.image_name, redirection_status: media.cd.redirection_status, media_index: media.cd.media_index, session_index: media.cd.session_index), "]")) +} + +fn megarac_images_body(media: MegaRacMediaWorld) -> String { + concat("[", concat(join(map(media.images, i => megarac_image_row(image_name: i.image_name, image_index: i.image_index)), ","), "]")) +} + +fn megarac_authenticated(get: fn(S) -> MegaRacMediaWorld, render: fn(S, OperationCall) -> OperationStep) -> fn(S, OperationCall) -> OperationStep { + fn(state, call) { + if megarac_session_valid(world: get(state), cookie_jar: call_text(call: call, name: "cookie_jar"), csrf_token: call_text(call: call, name: "csrf_token")) { + render(state, call) + } else { + curl_refused_401(state: state, with_status_line: false) + } + } +} + +// The start and stop bodies are the production builders' JSON; the model reads them with the same +// member readers the production decoders use (gunbc.machine_intake_megarac_media_attach). +fn body_member_text(call: OperationCall, key: String) -> String? { + match parse_json_document(s: call_text(call: call, name: "json_body")) { + JsonDocumentParsed { value: doc } => json_string_member(doc: doc, key: key) + JsonDocumentUnreadable { gap: _ } => none + } +} + +fn body_member_int(call: OperationCall, key: String) -> Int? { + match parse_json_document(s: call_text(call: call, name: "json_body")) { + JsonDocumentParsed { value: doc } => match json_number_member(doc: doc, key: key) { + Present { value: n } => parse_int(s: n) + Absent => none + } + JsonDocumentUnreadable { gap: _ } => none + } +} + +fn megarac_bindings(get: fn(S) -> MegaRacMediaWorld, put: fn(S, MegaRacMediaWorld) -> S) -> List> { + [ + OperationBinding { at: megarac_operation(operation: "OpenSession"), handler: fn(state, call) { + let opened = megarac_open_session(world: get(state), cookie_jar: call_text(call: call, name: "cookie_jar")) + curl_answer(state: put(state, opened.world), exit_code: 0, stdout: megarac_session_body(racsession_id: opened.racsession_id, csrf_token: opened.csrf_token), stderr: "") + } }, + OperationBinding { at: megarac_operation(operation: "ProbeSessionOnMediaRoute"), handler: fn(state, call) { + if megarac_session_valid(world: get(state), cookie_jar: call_text(call: call, name: "cookie_jar"), csrf_token: call_text(call: call, name: "csrf_token")) { + curl_answer(state: state, exit_code: 0, stdout: concat(megarac_configurations_body(media: get(state)), "\n200"), stderr: "") + } else { curl_refused_401(state: state, with_status_line: true) } + } }, + OperationBinding { at: megarac_operation(operation: "GetMediaGeneral"), handler: megarac_authenticated(get: get, render: fn(state, call) { + let m = get(state) + curl_answer(state: state, exit_code: 0, stdout: megarac_media_general_body(server: m.share.server, source_path: m.share.source_path, share_type: m.share.share_type, mount_cd: m.mount_cd, cd_error_code: m.cd_error_code), stderr: "") + }) }, + OperationBinding { at: megarac_operation(operation: "GetRemoteConfigurations"), handler: megarac_authenticated(get: get, render: fn(state, call) { + curl_answer(state: state, exit_code: 0, stdout: megarac_configurations_body(media: get(state)), stderr: "") + }) }, + OperationBinding { at: megarac_operation(operation: "GetRemoteImages"), handler: megarac_authenticated(get: get, render: fn(state, call) { + curl_answer(state: state, exit_code: 0, stdout: megarac_images_body(media: get(state)), stderr: "") + }) }, + OperationBinding { at: megarac_operation(operation: "StartMedia"), handler: megarac_authenticated(get: get, render: fn(state, call) { + match body_member_text(call: call, key: "image_name") { + Absent => OperationHarnessFault { reason: "start-media was dispatched without a readable image_name" as NonEmptyStr } + Present { value: name } => match body_member_int(call: call, key: "image_index") { + Absent => OperationHarnessFault { reason: "start-media was dispatched without a readable image_index" as NonEmptyStr } + Present { value: idx } => curl_answer(state: put(state, megarac_start_media(world: get(state), image_name: name, image_index: idx, now: call.now)), exit_code: 0, stdout: megarac_write_ack_body, stderr: "") + } + } + }) }, + OperationBinding { at: megarac_operation(operation: "StopMedia"), handler: megarac_authenticated(get: get, render: fn(state, call) { + curl_answer(state: put(state, megarac_stop_media(world: get(state))), exit_code: 0, stdout: megarac_write_ack_body, stderr: "") + }) }, + OperationBinding { at: megarac_operation(operation: "CloseSession"), handler: megarac_authenticated(get: get, render: fn(state, call) { + curl_answer(state: put(state, megarac_close_session(world: get(state), cookie_jar: call_text(call: call, name: "cookie_jar"), csrf_token: call_text(call: call, name: "csrf_token"))), exit_code: 0, stdout: megarac_write_ack_body, stderr: "") + }) }, + ] +} diff --git a/dag/gunbc/bmc_megarac_web_adapter.dag b/dag/gunbc/bmc_megarac_web_adapter.dag index f77216fbf02..946522d0b61 100644 --- a/dag/gunbc/bmc_megarac_web_adapter.dag +++ b/dag/gunbc/bmc_megarac_web_adapter.dag @@ -11,7 +11,7 @@ import extdeps.bmc.megarac { MegaRacLoginSession, megarac_login_session_json, megarac_services_kvm_json, megarac_kvm_websocket_path, } import gunbc.bmc_model { - BmcWorld, BmcEvent, BmcScheduledEvent, BmcAcPowerLost, BmcKvmStreamClosed, BmcPowerOn, BmcPowerOff, BmcKvmIdle, BmcKvmStreaming, BmcKvmClosedByController, BmcWebLoginAccepted, BmcWebLoginRefused, + BmcWorld, BmcEvent, BmcScheduledEvent, BmcAcPowerLost, BmcPowerRestored, BmcSolSessionDropped, BmcKvmStreamClosed, BootOverrideNone, BootOverrideCdromEfiNextBoot, BmcPowerOn, BmcPowerOff, BmcKvmIdle, BmcKvmStreaming, BmcKvmClosedByController, BmcWebLoginAccepted, BmcWebLoginRefused, bmc_web_login, bmc_kvm_viewer_count, bmc_kvm_connect, bmc_web_logout, bmc_advance, } @@ -129,6 +129,8 @@ fn bmc_event_json(e: BmcEvent) -> JsonValue { match e { BmcAcPowerLost {} => json_string(s: "ac_power_lost") BmcKvmStreamClosed {} => json_string(s: "kvm_stream_closed") + BmcPowerRestored {} => json_string(s: "power_restored") + BmcSolSessionDropped {} => json_string(s: "sol_session_dropped") } } @@ -154,6 +156,13 @@ fn megarac_web_world_json(world: BmcWorld) -> JsonValue { BmcKvmClosedByController { session: k } => json_array(elements: [json_string(s: "closed"), json_int(n: k)]) }), json_kv(key: "canvas_readable", value: json_bool(b: world.web.canvas_readable)), + json_kv(key: "boot_override", value: json_string(s: match world.boot_override { BootOverrideNone => "none" BootOverrideCdromEfiNextBoot => "cdrom_efi_next_boot" })), + json_kv(key: "sel", value: json_array(elements: map(world.sel, r => json_array(elements: [json_string(s: r.id_hex), json_string(s: r.date), json_string(s: r.time), json_string(s: r.sensor), json_string(s: r.event), json_string(s: r.state)])))), + json_kv(key: "sol_session_open", value: json_bool(b: world.sol_session_open)), + json_kv(key: "cycle_off_interval", value: json_int(n: second_count(s: world.cycle_off_interval) as Int)), + json_kv(key: "host_booted_at", value: match world.host_booted_at { Absent => json_null() Present { value: t } => json_int(n: second_count(s: t) as Int) }), + json_kv(key: "booted_via_override", value: json_bool(b: world.booted_via_override)), + json_kv(key: "sol_drop_after_boot", value: match world.sol_drop_after_boot { Absent => json_null() Present { value: t } => json_int(n: second_count(s: t) as Int) }), ]) } diff --git a/dag/gunbc/bmc_model.dag b/dag/gunbc/bmc_model.dag index 8edbe8b410a..8f3fced5a95 100644 --- a/dag/gunbc/bmc_model.dag +++ b/dag/gunbc/bmc_model.dag @@ -2,7 +2,7 @@ module gunbc.bmc_model import std.types { Bool, Int, List } import std.string_type { String } -import std.measure { Second, second_count } +import std.measure { Second, second, second_count } import v2.std.optional { Present, Absent } import v2.std.algebra { filter } import extdeps.bmc.ipmi_chassis_control { @@ -11,24 +11,32 @@ import extdeps.bmc.ipmi_chassis_control { // THE ONE BMC MODEL: scenario state and its transitions, nothing else. The controller operations and // their response shapes are interface facts owned by extdeps.bmc (ipmi, ipmi_chassis_control, -// megarac); this module never re-declares one. It is consumed by the dry operation realization -// (gunbc.bmc_dry_realization) today and is written to be consumed unchanged by a protocol-speaking -// simulator later: every transition is pure, time is an INPUT, and persistence is the world value, -// so whoever runs the model supplies the clock and the storage. -// -// THIS IS THE FIRST SLICE: chassis power and one scheduled external event. Media rows, boot -// parameters, the SOL session and notification delivery arrive with the acceptance matrix that -// consumes them, as rows of this world, not as a second model. +// megarac, ipmitool_observed_output); this module never re-declares one. It is consumed by the dry +// operation realizations (gunbc.bmc_dry_realization, gunbc.machine_intake_mtcollins1_boot_dry_realization) +// and is written to be consumed unchanged by a protocol-speaking simulator later: every transition is +// pure, time is an INPUT, and persistence is the world value. type BmcPower = BmcPowerOn | BmcPowerOff -// An event the world undergoes on its own, independent of any request: the SEL on the Mt. Collins -// unit records `Power Unit ChassisPwrStatus | AC lost` (run 36335369059, mtcollins1-boot-diagnostics.txt -// sha256 eda19cde2e60d90d3d04946273e615eb5bf774496b9907e03d3bc15dbedc2c1c), which is the grounding for -// modeling power loss as an event rather than as the answer to a command. +// THE ONE-SHOT BOOT OVERRIDE (IPMI boot parameter 5), in the two states this controller has been +// observed in: no override, and a valid next-boot EFI CD/DVD override. A next-boot override is +// consumed by the boot it applies to, which is what the post-attempt read reports. +type BmcBootOverride + = BootOverrideNone + | BootOverrideCdromEfiNextBoot + +// An event the world undergoes on its own, independent of any request. AC loss is grounded in the +// Mt. Collins SEL (run 36335369059, mtcollins1-boot-diagnostics.txt sha256 +// eda19cde2e60d90d3d04946273e615eb5bf774496b9907e03d3bc15dbedc2c1c: `Power Unit ChassisPwrStatus | AC lost`). +// A dropped SOL session is the controller ending the serial session on its own, which the 2026-09-27 +// incident (gunbc#12423) recorded as a loss mid-boot while the management interface kept answering. +// A power restore is the second half of a power cycle: the controller drops power, and after the +// scenario's off interval brings it back, so a read taken inside the interval sees it off. type BmcEvent = BmcAcPowerLost {} + | BmcPowerRestored {} + | BmcSolSessionDropped {} | BmcKvmStreamClosed {} type BmcScheduledEvent { @@ -36,13 +44,45 @@ type BmcScheduledEvent { event: BmcEvent } +// One system event log record, in the fields `ipmitool sel elist` prints +// (extdeps.bmc.ipmitool_observed_output ipmitool_sel_elist_line). +type BmcSelRecord { + id_hex: String + date: String + time: String + sensor: String + event: String + state: String +} + +// 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. +// host_booted_at is the virtual instant the host last started booting (power on, or the restore of a +// cycle); the host's console is timed from it. booted_via_override records whether that boot consumed +// the one-shot override. type BmcWorld { power: BmcPower pending: List fired: List + boot_override: BmcBootOverride + sel: List + sol_session_open: Bool + cycle_off_interval: Second + host_booted_at: Second? + booted_via_override: Bool + sol_drop_after_boot: Second? web: BmcWebWorld } +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, + } +} + // THE WEB AND KVM SURFACE OF A MegaRAC SP-X CONTROLLER (firmware 0.32; operations and wire shapes in // extdeps.bmc.megarac, cited there to the served source.min.js and viewer.min.js). World state only: // the web sessions the controller holds, the account it accepts, the KVM viewers other clients hold, @@ -86,10 +126,10 @@ data bmc_web_world_untouched: BmcWebWorld = BmcWebWorld { } // A COMMAND'S EFFECT AND ITS REPLY ARE SEPARATE FACTS. effect_taken says whether the world changed; -// the reply is the adapter's to render from the new world. §28.3 recommends a controller refuse a -// power cycle at an OFF host with completion code D5h; the Mt. Collins MegaRAC does not, and answers -// success doing nothing (extdeps.bmc.ipmi_chassis_control, run 36023602469). The model follows the -// observed unit, and that departure from the recommendation is the reason the arm exists. +// the reply is the adapter's to render. §28.3 recommends a controller refuse a power cycle at an OFF +// host with completion code D5h; the Mt. Collins MegaRAC does not, and answers success doing nothing +// (extdeps.bmc.ipmi_chassis_control, run 36023602469). The model follows the observed unit, and that +// departure from the recommendation is the reason the arm exists. type BmcChassisControlStep { world: BmcWorld effect_taken: Bool @@ -103,11 +143,21 @@ fn bmc_power_is_on(world: BmcWorld) -> Bool { } fn bmc_with_power(world: BmcWorld, power: BmcPower) -> BmcWorld { - BmcWorld { power: power, pending: world.pending, fired: world.fired, web: world.web } + 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, + } } fn bmc_with_web(world: BmcWorld, web: BmcWebWorld) -> BmcWorld { - BmcWorld { power: world.power, pending: world.pending, fired: world.fired, web: web } + 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, + } } fn bmc_web_with(web: BmcWebWorld, sessions: List, next_session_id: Int, kvm: BmcKvmStream) -> BmcWebWorld { @@ -209,20 +259,74 @@ fn bmc_web_logout(world: BmcWorld, csrf_token: String) -> BmcWebLogoutStep { } } -fn bmc_chassis_control(world: BmcWorld, action: IpmiChassisControlAction) -> BmcChassisControlStep { +fn bmc_with_override(world: BmcWorld, over: BmcBootOverride) -> BmcWorld { + 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, + } +} + +fn bmc_with_sol_session(world: BmcWorld, open: Bool) -> BmcWorld { + 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, + } +} + +fn bmc_with_pending(world: BmcWorld, pending: List, fired: List) -> BmcWorld { + BmcWorld { + 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, + } +} + +// The host starts booting now: power is on, the boot is timed from here, and a pending next-boot +// override is consumed by it. +fn bmc_host_boots(world: BmcWorld, now: Second) -> BmcWorld { + let via = match world.boot_override { BootOverrideCdromEfiNextBoot => true BootOverrideNone => false } + let pending = match world.sol_drop_after_boot { + Absent => world.pending + Present { value: after } => list_append(world.pending, BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} }) + } + 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, + } +} + +fn bmc_chassis_control(world: BmcWorld, action: IpmiChassisControlAction, now: Second) -> BmcChassisControlStep { match action { - IpmiChassisPowerUp => BmcChassisControlStep { world: bmc_with_power(world: world, power: BmcPowerOn), effect_taken: !bmc_power_is_on(world: world) } + IpmiChassisPowerUp => + if bmc_power_is_on(world: world) { BmcChassisControlStep { world: world, effect_taken: false } } + else { BmcChassisControlStep { world: bmc_host_boots(world: world, now: now), effect_taken: true } } IpmiChassisPowerDown => BmcChassisControlStep { world: bmc_with_power(world: world, power: BmcPowerOff), effect_taken: bmc_power_is_on(world: world) } - IpmiChassisPowerCycle => BmcChassisControlStep { world: world, effect_taken: bmc_power_is_on(world: world) } - IpmiChassisHardReset => BmcChassisControlStep { world: world, effect_taken: bmc_power_is_on(world: world) } + IpmiChassisPowerCycle => + if bmc_power_is_on(world: world) { + let off = bmc_with_power(world: world, power: BmcPowerOff) + let restore = BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: world.cycle_off_interval)), event: BmcPowerRestored {} } + BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_append(off.pending, restore), fired: off.fired), effect_taken: true } + } else { BmcChassisControlStep { world: world, effect_taken: false } } + IpmiChassisHardReset => + if bmc_power_is_on(world: world) { BmcChassisControlStep { world: bmc_host_boots(world: world, now: now), effect_taken: true } } + else { BmcChassisControlStep { world: world, effect_taken: false } } } } // A stream the controller closes on its own (the dropped /kvm connection) ends the stream but not // the web session that opened it. -fn bmc_apply_event(world: BmcWorld, event: BmcEvent) -> BmcWorld { +fn bmc_apply_event(world: BmcWorld, event: BmcEvent, at: Second) -> BmcWorld { match event { BmcAcPowerLost {} => bmc_with_power(world: world, power: BmcPowerOff) + BmcPowerRestored {} => bmc_host_boots(world: world, now: at) + BmcSolSessionDropped {} => bmc_with_sol_session(world: world, open: false) BmcKvmStreamClosed {} => match world.web.kvm { BmcKvmStreaming { session: k } => bmc_with_web(world: world, web: bmc_web_with(web: world.web, sessions: world.web.sessions, next_session_id: world.web.next_session_id, kvm: BmcKvmClosedByController { session: k })) _ => world @@ -230,14 +334,74 @@ fn bmc_apply_event(world: BmcWorld, event: BmcEvent) -> BmcWorld { } } -// Every event due at or before `now` fires, in schedule order, and moves from pending to fired. +// EVERY EVENT DUE AT OR BEFORE `now` FIRES, EARLIEST FIRST, AND AN EVENT A TRANSITION SCHEDULES IS +// KEPT. One due event is taken off the world's own pending list, applied, and recorded as fired; the +// advance then repeats on the world THAT TRANSITION PRODUCED, so an event it scheduled -- a power +// restore arming its SOL drop -- stays pending and fires in turn if it too is due. (An earlier fold +// rebuilt pending from its own accumulator after each transition and so discarded exactly those +// events: #12423 side-chat review 5342387382.) Each step fires one due event, so the repetition ends. +// With nothing due the world is returned as it is rather than rebuilt. fn bmc_advance(world: BmcWorld, now: Second) -> BmcWorld { - fold(world.pending, init: BmcWorld { power: world.power, pending: [], fired: world.fired, web: world.web }, f: fn(acc, e) { - if second_count(s: e.at) <= second_count(s: now) { - let applied = bmc_apply_event(world: acc, event: e.event) - BmcWorld { power: applied.power, pending: acc.pending, fired: list_append(acc.fired, e), web: applied.web } - } else { - BmcWorld { power: acc.power, pending: list_append(acc.pending, e), fired: acc.fired, web: acc.web } + match bmc_first_due(pending: world.pending, now: now) { + Absent => world + Present { value: e } => { + let remaining = bmc_without_first(pending: world.pending, event: e) + let applied = bmc_apply_event(world: bmc_with_pending(world: world, pending: remaining, fired: world.fired), event: e.event, at: e.at) + bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_append(applied.fired, e)), now: now) + } + } +} + +// The due event with the earliest instant; among equal instants, the first in schedule order. +fn bmc_no_event() -> BmcScheduledEvent? { + none +} + +fn bmc_first_due(pending: List, now: Second) -> BmcScheduledEvent? { + fold(pending, init: bmc_no_event(), f: fn(acc, e) { + if second_count(s: e.at) > second_count(s: now) { acc } else { + match acc { + Absent => Present { value: e } + Present { value: best } => if second_count(s: e.at) < second_count(s: best.at) { Present { value: e } } else { acc } + } } }) } + +type BmcPendingRemoval { + kept: List + removed: Bool +} + +// Removes ONE occurrence -- the first equal to `event` -- so two identical scheduled events fire twice. +fn bmc_without_first(pending: List, event: BmcScheduledEvent) -> List { + fold(pending, init: BmcPendingRemoval { kept: [], removed: false }, f: fn(acc, e) { + if !acc.removed && second_count(s: e.at) == second_count(s: event.at) && bmc_event_eq(a: e.event, b: event.event) { + BmcPendingRemoval { kept: acc.kept, removed: true } + } else { + BmcPendingRemoval { kept: list_append(acc.kept, e), removed: acc.removed } + } + }).kept +} + +fn bmc_event_eq(a: BmcEvent, b: BmcEvent) -> Bool { + match a { + BmcAcPowerLost {} => match b { BmcAcPowerLost {} => true _ => false } + BmcPowerRestored {} => match b { BmcPowerRestored {} => true _ => false } + BmcSolSessionDropped {} => match b { BmcSolSessionDropped {} => true _ => false } + BmcKvmStreamClosed {} => match b { BmcKvmStreamClosed {} => true _ => false } + } +} + +fn bmc_with_sol_drop_after_boot(world: BmcWorld, after: Second) -> 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: Present { value: after }, + web: world.web, + } +} + +fn bmc_sol_drop_fired(world: BmcWorld) -> Bool { + !all(world.fired, e => match e.event { BmcSolSessionDropped {} => false _ => true }) +} diff --git a/dag/gunbc/filesystem_model.dag b/dag/gunbc/filesystem_model.dag new file mode 100644 index 00000000000..28ccb5f41c6 --- /dev/null +++ b/dag/gunbc/filesystem_model.dag @@ -0,0 +1,246 @@ +module gunbc.filesystem_model + +import std.types { Bool, List, String } +import std.measure { second, ByteSize, byte_size } +import std.bytes { bytes_octets, utf8_encode_bytes } +import v2.std.operation_argv { OperationRef, BoundOperationInvocation } +import v2.std.operation_realization { + OperationBinding, OperationCall, OperationStep, OperationObserved, OperationHarnessFault, + FileObserved, ShellObserved, operation_input_text, +} +import extdeps.transports.file { FileExchangeObservation, FileOperationSucceeded, FileOperationFailed } +import extdeps.transports.shell { ShellProcessExited } +import extdeps.filesystem.filesystem_io { + FilesystemNotFound, FilesystemAlreadyExists, FilesystemNotDirectory, FilesystemOtherFailure, +} + +// A MODELED FILESYSTEM: the subset of POSIX file behaviour the file transport realizes, as a pure +// value a modeled operation realization embeds in its scenario state. It is generic -- a hold store, +// a SOL pid file and a capture file are all just paths in it -- and it reproduces the realization's +// own contract (v1 interpreter dispatch_file), not an idealised filesystem: +// - a write needs its parent directory to exist, and answers not_found otherwise; +// - write_create_new answers already_exists when the path exists, and never overwrites; +// - a listing is the immediate children's names, sorted, one per line; listing a file answers +// not_a_directory and listing an absent path answers not_found; +// - reading or writing a directory as a file answers `other`, as an EISDIR does. +// WHAT IT DOES NOT MODEL, stated so a green over it is not over-read: file modes (the declared mode of +// write_create_new_with_mode is accepted and not stored), ownership, symlinks, partial writes, and +// the atomicity of a real create-exclusive under concurrent processes. Those are properties of the real +// filesystem, and their evidence is the file-store tests that run against a real directory. +// byte_count is the content's UTF-8 byte length, as the realization's own `content.len()` reports it -- +// not its code-point count -- computed as std.materialization_object does. +fn content_bytes(s: String) -> ByteSize { + byte_size(count: bytes_octets(b: utf8_encode_bytes(s: s)) |> count()) +} + +type ModeledFile { + path: String + content: String +} + +type ModeledFilesystem { + directories: List + files: List +} + +fn fs_is_directory(fs: ModeledFilesystem, path: String) -> Bool { + any_string(xs: fs.directories, x: path) +} + +fn any_string(xs: List, x: String) -> Bool { + !all(xs, y => y != x) +} + +fn fs_file(fs: ModeledFilesystem, path: String) -> ModeledFile? { + fold(fs.files, init: none, f: fn(acc, file) { + match acc { + Present { value: v } => Present { value: v } + Absent => if file.path == path { Present { value: file } } else { none } + } + }) +} + +// The parent of an absolute path: everything before its last separator. "/a/b" -> "/a", "/a" -> "/". +fn fs_parent(path: String) -> String { + let segments = split(s: path, delimiter: "/") + let kept = segments.take(n: count(segments) - 1) + let joined = join(kept, "/") + if joined == "" { "/" } else { joined } +} + +fn fs_leaf(path: String) -> String { + match split(s: path, delimiter: "/").last() { + Present { value: leaf } => leaf + Absent => path + } +} + +fn failed_with(kind: extdeps.filesystem.filesystem_io.FilesystemFailureKind, message: String) -> FileExchangeObservation { + FileOperationFailed { kind: kind, error: message } +} + +fn fs_read(fs: ModeledFilesystem, path: String) -> FileExchangeObservation { + match fs_file(fs: fs, path: path) { + Present { value: file } => FileOperationSucceeded { byte_count: content_bytes(s: file.content), content: file.content } + Absent => + if fs_is_directory(fs: fs, path: path) { failed_with(kind: FilesystemOtherFailure, message: concat("Is a directory: ", path)) } + else { failed_with(kind: FilesystemNotFound, message: concat("No such file or directory: ", path)) } + } +} + +type ModeledFileWrite { + fs: ModeledFilesystem + observation: FileExchangeObservation +} + +fn fs_write(fs: ModeledFilesystem, path: String, content: String, create_new: Bool) -> ModeledFileWrite { + if !fs_is_directory(fs: fs, path: fs_parent(path: path)) { + ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemNotFound, message: concat("No such file or directory: ", path)) } + } else if fs_is_directory(fs: fs, path: path) { + ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemOtherFailure, message: concat("Is a directory: ", path)) } + } else { + match fs_file(fs: fs, path: path) { + Present { value: _ } => + if create_new { + ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemAlreadyExists, message: concat("File exists: ", path)) } + } else { + ModeledFileWrite { fs: fs_with_file(fs: fs, path: path, content: content), observation: FileOperationSucceeded { byte_count: content_bytes(s: content), content: "" } } + } + Absent => + ModeledFileWrite { fs: fs_with_file(fs: fs, path: path, content: content), observation: FileOperationSucceeded { byte_count: content_bytes(s: content), content: "" } } + } + } +} + +fn fs_with_file(fs: ModeledFilesystem, path: String, content: String) -> ModeledFilesystem { + ModeledFilesystem { + directories: fs.directories, + files: list_append(filter(fs.files, f => f.path != path), ModeledFile { path: path, content: content }), + } +} + +fn fs_delete(fs: ModeledFilesystem, path: String) -> ModeledFileWrite { + match fs_file(fs: fs, path: path) { + Present { value: _ } => + ModeledFileWrite { fs: ModeledFilesystem { directories: fs.directories, files: filter(fs.files, f => f.path != path) }, observation: FileOperationSucceeded { byte_count: byte_size(count: 0), content: "" } } + Absent => + if fs_is_directory(fs: fs, path: path) { ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemOtherFailure, message: concat("Is a directory: ", path)) } } + else { ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemNotFound, message: concat("No such file or directory: ", path)) } } + } +} + +fn fs_list(fs: ModeledFilesystem, path: String) -> FileExchangeObservation { + if fs_is_directory(fs: fs, path: path) { + let file_names = map(filter(fs.files, f => fs_parent(path: f.path) == path), f => fs_leaf(path: f.path)) + let dir_names = map(filter(fs.directories, d => d != path && fs_parent(path: d) == path), d => fs_leaf(path: d)) + let listing = join(sort_by(concat_lists(a: file_names, b: dir_names), n => n), "\n") + FileOperationSucceeded { byte_count: content_bytes(s: listing), content: listing } + } else { + match fs_file(fs: fs, path: path) { + Present { value: _ } => failed_with(kind: FilesystemNotDirectory, message: concat("Not a directory: ", path)) + Absent => failed_with(kind: FilesystemNotFound, message: concat("No such file or directory: ", path)) + } + } +} + +fn concat_lists(a: List, b: List) -> List { + fold(b, init: a, f: fn(acc, x) { list_append(acc, x) }) +} + +// THE BINDINGS, through a lens into the scenario state, so any scenario world can embed a filesystem +// without this module knowing its shape. Filesystem operations take no virtual time. +data filesystem_io_operation_path: String = "dag/extdeps/filesystem/filesystem_io.dag" + +fn filesystem_operation(operation: String) -> OperationRef { + OperationRef { path: filesystem_io_operation_path, service: "Filesystem", operation: operation } +} + +fn file_step(state: S, observation: FileExchangeObservation) -> OperationStep { + OperationObserved { observation: FileObserved { observation: observation }, state: state, elapsed: second(count: 0) } +} + +fn filesystem_bindings(get: fn(S) -> ModeledFilesystem, put: fn(S, ModeledFilesystem) -> S) -> List> { + let reading = fn(state, call) { + match operation_input_text(invocation: call.invocation, name: "path") { + Absent => OperationHarnessFault { reason: "a filesystem read was dispatched without a path" as NonEmptyStr } + Present { value: path } => file_step(state: state, observation: fs_read(fs: get(state), path: path)) + } + } + let listing = fn(state, call) { + match operation_input_text(invocation: call.invocation, name: "path") { + Absent => OperationHarnessFault { reason: "a filesystem list was dispatched without a path" as NonEmptyStr } + Present { value: path } => file_step(state: state, observation: fs_list(fs: get(state), path: path)) + } + } + let deleting = fn(state, call) { + match operation_input_text(invocation: call.invocation, name: "path") { + Absent => OperationHarnessFault { reason: "a filesystem delete was dispatched without a path" as NonEmptyStr } + Present { value: path } => { + let w = fs_delete(fs: get(state), path: path) + file_step(state: put(state, w.fs), observation: w.observation) + } + } + } + [ + OperationBinding { at: filesystem_operation(operation: "Read"), handler: reading }, + OperationBinding { at: filesystem_operation(operation: "List"), handler: listing }, + OperationBinding { at: filesystem_operation(operation: "Delete"), handler: deleting }, + OperationBinding { at: filesystem_operation(operation: "Write"), handler: writing(get: get, put: put, create_new: false) }, + OperationBinding { at: filesystem_operation(operation: "WriteOwnerOnly"), handler: writing(get: get, put: put, create_new: false) }, + OperationBinding { at: filesystem_operation(operation: "WriteCreateNew"), handler: writing(get: get, put: put, create_new: true) }, + OperationBinding { at: filesystem_operation(operation: "WriteCreateNewWithMode"), handler: writing(get: get, put: put, create_new: true) }, + OperationBinding { at: shell_move_file_operation, handler: moving(get: get, put: put) }, + ] +} + +fn writing(get: fn(S) -> ModeledFilesystem, put: fn(S, ModeledFilesystem) -> S, create_new: Bool) -> fn(S, OperationCall) -> OperationStep { + fn(state, call) { + match operation_input_text(invocation: call.invocation, name: "path") { + Absent => OperationHarnessFault { reason: "a filesystem write was dispatched without a path" as NonEmptyStr } + Present { value: path } => match operation_input_text(invocation: call.invocation, name: "content") { + Absent => OperationHarnessFault { reason: "a filesystem write was dispatched without content" as NonEmptyStr } + Present { value: content } => { + let w = fs_write(fs: get(state), path: path, content: content, create_new: create_new) + file_step(state: put(state, w.fs), observation: w.observation) + } + } + } + } +} + +// extdeps.shell shell.Move File: `mv `, a rename within the one modeled +// filesystem. It replaces an existing destination file, as mv does, and fails -- exit 1 with mv's +// "cannot stat" -- when the source does not exist or the destination's directory does not. +data shell_move_file_operation: OperationRef = OperationRef { path: "dag/extdeps/shell.dag", service: "shell.Move", operation: "File" } + +fn fs_move(fs: ModeledFilesystem, source: String, destination: String) -> ModeledFileWrite { + match fs_file(fs: fs, path: source) { + Absent => ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemNotFound, message: concat("No such file or directory: ", source)) } + Present { value: f } => + if !fs_is_directory(fs: fs, path: fs_parent(path: destination)) { + ModeledFileWrite { fs: fs, observation: failed_with(kind: FilesystemNotFound, message: concat("No such file or directory: ", destination)) } + } else { + let removed = ModeledFilesystem { directories: fs.directories, files: filter(fs.files, x => x.path != source) } + ModeledFileWrite { fs: fs_with_file(fs: removed, path: destination, content: f.content), observation: FileOperationSucceeded { byte_count: byte_size(count: 0), content: "" } } + } + } +} + +fn moving(get: fn(S) -> ModeledFilesystem, put: fn(S, ModeledFilesystem) -> S) -> fn(S, OperationCall) -> OperationStep { + fn(state, call) { + match operation_input_text(invocation: call.invocation, name: "source") { + Absent => OperationHarnessFault { reason: "a move was dispatched without a source" as NonEmptyStr } + Present { value: source } => match operation_input_text(invocation: call.invocation, name: "destination") { + Absent => OperationHarnessFault { reason: "a move was dispatched without a destination" as NonEmptyStr } + Present { value: destination } => { + let m = fs_move(fs: get(state), source: source, destination: destination) + let exited = match m.observation { + FileOperationSucceeded { byte_count: _, content: _ } => ShellProcessExited { exit_code: 0, stdout: "", stderr: "" } + FileOperationFailed { kind: _, error: _ } => ShellProcessExited { exit_code: 1, stdout: "", stderr: join(["mv: cannot stat '", source, "': No such file or directory\n"], "") } + } + OperationObserved { observation: ShellObserved { observation: exited }, state: put(state, m.fs), elapsed: second(count: 0) } + } + } + } + } +} diff --git a/dag/gunbc/host_command_model.dag b/dag/gunbc/host_command_model.dag new file mode 100644 index 00000000000..23a2636fc92 --- /dev/null +++ b/dag/gunbc/host_command_model.dag @@ -0,0 +1,98 @@ +module gunbc.host_command_model + +import std.types { Bool, List, NonEmptyStr, String } +import std.measure { second } +import v2.std.operation_argv { OperationRef, InputText, InputTextList } +import v2.std.operation_realization { + OperationBinding, OperationCall, OperationStep, OperationObserved, OperationHarnessFault, + ShellObserved, +} +import extdeps.transports.shell { ShellExchangeObservation } +import extdeps.exec.command { ArgvCommand, argv_words } + +// AN OPERATION THAT CARRIES A WHOLE COMMAND AS ITS INPUT, AND WHAT THE FAR SIDE ANSWERS. Some +// operations are one identity for every command they run: extdeps.shell.exec shell.Exec.RunArgv +// starts any local program, and extdeps.ssh.session ssh.Session.ExecPortableWords runs any remote +// command. Binding such an operation by identity alone would answer every command the same way, and +// answering by the program's NAME would be the executable-name binding the #12423 design decision +// refuses. So the binding is an EXACT-INVOCATION table, the keying REST replay already uses for its +// fixtures: a scenario lists the complete word sequences it models -- OBTAINED FROM THE PRODUCTION +// BUILDERS the code under test calls, never hand-spelled -- and a dispatched invocation is answered +// only when the concatenation of its named inputs equals one listed sequence. An unlisted invocation, +// or one matching two entries, is a harness fault, never a guessed answer. The answer is a function +// of the scenario state, so the far side's reply can depend on the world. +type ModeledInvocation { + words: List + answer: fn(S) -> ShellExchangeObservation +} + +data shell_exec_run_argv_operation: OperationRef = OperationRef { + path: "dag/extdeps/shell/exec.dag", + service: "shell.Exec", + operation: "RunArgv", +} + +data ssh_session_exec_portable_words_operation: OperationRef = OperationRef { + path: "dag/extdeps/ssh/session.dag", + service: "ssh.Session", + operation: "ExecPortableWords", +} + +// The words a LOCAL ArgvCommand dispatches as: its program then its arguments, exactly what +// command_over_transport builds for LocalExec and RunArgv receives. +fn local_command_words(command: ArgvCommand) -> List { + argv_words(command: command) +} + +fn dispatched_words(bindings: List, name: String) -> List? { + fold(bindings, init: none, f: fn(acc, b) { + match acc { + Present { value: v } => Present { value: v } + Absent => if b.name == name { + match b.value { + InputTextList { items: xs } => Present { value: xs } + InputText { text: t } => Present { value: [t] } + } + } else { none } + } + }) +} + +fn invocation_words(bindings: List, inputs: List) -> List? { + fold(inputs, init: Present { value: [] }, f: fn(acc, name) { + match acc { + Absent => none + Present { value: so_far } => match dispatched_words(bindings: bindings, name: name) { + Absent => none + Present { value: ws } => Present { value: concat(so_far, ws) } + } + } + }) +} + +fn exact_invocation_binding(at: OperationRef, inputs: List, table: List>) -> OperationBinding { + OperationBinding { + at: at, + handler: fn(state, call) { + match invocation_words(bindings: call.invocation.bindings, inputs: inputs) { + Absent => OperationHarnessFault { reason: join(["the invocation lacks one of its declared inputs: ", join(inputs, ", ")], "") as NonEmptyStr } + Present { value: words } => { + let matching = filter(table, m => m.words == words) + if count(matching) == 1 { + match matching.first() { + Present { value: m } => { + let answer = m.answer + OperationObserved { observation: ShellObserved { observation: answer(state) }, state: state, elapsed: second(count: 0) } + } + Absent => OperationHarnessFault { reason: "a matched invocation vanished" as NonEmptyStr } + } + } else if count(matching) == 0 { + OperationHarnessFault { reason: join(["no modeled invocation is exactly `", join(words, " "), "`"], "") as NonEmptyStr } + } else { + OperationHarnessFault { reason: join(["two modeled invocations are exactly `", join(words, " "), "`"], "") as NonEmptyStr } + } + } + } + }, + } +} diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag b/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag index acf2efebc92..e746429627d 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_diagnostic_bundle.dag @@ -739,6 +739,70 @@ fn end_media_text(e: MtCollins1EndMedia) -> String { } } +// A PRESENTATION AFFIRMED LOST AFTER THE HANDOFF IS A CAUSE, NOT ONLY A FINDING (gunbc#12533 +// finding 4). The after-handoff and end-of-attempt looks are taken for this attempt's own subject, +// under the hold, after the boot override and the power action were made. When either AFFIRMS the +// medium is no longer served, the host was booting from a medium the controller had stopped +// serving, and a failure the attempt reports afterwards -- a watch that reaches its deadline -- is +// that loss seen from downstream. So the attempt's verdict consumes the looks it took rather than +// leaving them to the bundle. Only an affirmed loss attributes: an unobserved or unestablished look +// says nothing about the medium and is never promoted to a cause. The earliest affirming look is +// named, because the phase is what the operator acts on. +type MediaLossPhase + = MediaLostAtAfterHandoff + | MediaLostAtEndOfAttempt + +fn media_loss_phase_text(p: MediaLossPhase) -> String { + match p { + MediaLostAtAfterHandoff => "after-handoff" + MediaLostAtEndOfAttempt => "end-of-attempt" + } +} + +type MediaLossAfterHandoff + = MediaLossAffirmed { phase: MediaLossPhase, reason: NonEmptyStr } + | MediaLossNotAffirmed + +fn media_loss_of_look(look: MegaRacAttachResult, phase: MediaLossPhase) -> MediaLossAfterHandoff { + match presentation_still_served(result: look) { + PresentationNoLongerReady { reason: why } => MediaLossAffirmed { phase: phase, reason: why } + _ => MediaLossNotAffirmed + } +} + +// PURE, over the two looks only a CONFIRMED handoff makes causal: a handoff that was withheld or +// never reached made no boot write, and one attempted but unconfirmed already carries its own cause +// (the handoff's), so neither is re-attributed to the medium. +fn media_loss_after_handoff(handoff: MtCollins1HandoffMedia, end: MtCollins1EndMedia) -> MediaLossAfterHandoff { + match handoff { + HandoffMediaAttempted { before: _, handoff: HandoffConfirmed, after: a } => + match media_loss_of_look(look: a, phase: MediaLostAtAfterHandoff) { + MediaLossAffirmed { phase: p, reason: r } => MediaLossAffirmed { phase: p, reason: r } + MediaLossNotAffirmed => + match end { + EndMediaObserved { look: l } => media_loss_of_look(look: l, phase: MediaLostAtEndOfAttempt) + EndMediaNotTaken { reason: _ } => MediaLossNotAffirmed + } + } + _ => MediaLossNotAffirmed + } +} + +// THE ATTEMPT'S TERMINAL CAUSE. A success stands -- the host reported its census, so whatever the +// controller did afterwards did not stop it (the finding still records the loss) -- and a failure is +// re-attributed to the loss, keeping the downstream symptom beside it rather than discarding it. +fn outcome_attributing_media_loss(outcome: ProcessExit, loss: MediaLossAfterHandoff) -> ProcessExit { + match outcome { + ExitSuccess => ExitSuccess + ExitFailure { code: c, reason: r } => + match loss { + MediaLossNotAffirmed => ExitFailure { code: c, reason: r } + MediaLossAffirmed { phase: p, reason: why } => + ExitFailure { code: c, reason: join(["mtcollins1 boot: media presentation lost at ", media_loss_phase_text(p: p), " (", why as String, "); the attempt then reported: ", r], "") } + } + } +} + type MtCollins1BootRunRecord { end_media: MtCollins1EndMedia handoff_media: MtCollins1HandoffMedia diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag b/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag new file mode 100644 index 00000000000..328db81e665 --- /dev/null +++ b/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag @@ -0,0 +1,395 @@ +module gunbc.machine_intake_mtcollins1_boot_dry_realization + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.measure { Second, second, second_count } +import std.algebra { trim } +import v2.std.operation_argv { OperationRef } +import v2.std.operation_realization { + OperationRealization, OperationBinding, OperationCall, OperationStep, + OperationObserved, OperationHarnessFault, ShellObserved, FileObserved, + virtual_delay_binding, operation_input_text, +} +import gunbc.bmc_model { BmcWorld, bmc_advance, bmc_with_sol_session, bmc_power_is_on } +import gunbc.bmc_dry_realization { bmc_bindings, megarac_bindings, bmc_ipmi_operation, sleep_delay_seconds_operation } +import gunbc.megarac_media_model { MegaRacMediaWorld, megarac_media_advance } +import gunbc.filesystem_model { ModeledFilesystem, ModeledFile, filesystem_bindings, fs_with_file, fs_file, fs_write, content_bytes } +import extdeps.transports.file { FileOperationSucceeded } +import gunbc.process_environment_model { ModeledVariable, environment_binding } +import gunbc.host_command_model { ModeledInvocation, exact_invocation_binding, local_command_words, shell_exec_run_argv_operation } +import extdeps.transports.shell { ShellExchangeObservation, ShellProcessExited } +import extdeps.exec.command { env_prefixed_command } +import extdeps.tools.env { EnvSet } +import extdeps.ssh.openssh_client_commands { ssh_add_list_identities_command } +import extdeps.bmc.ipmitool_observed_output { ipmitool_sol_activate_preamble } +import extdeps.bmc.ipmi { ipmitool_sol_operational_banner } +import gunbc.machine_intake_sol_hold { sol_hold_exit_record_prefix } +import gunbc.machine_intake_mtcollins1_boot_run { mtcollins1_sol_notice_ready_suffix, mtcollins1_sol_notice_watcher_path, mtcollins1_sol_notice_token_env } +import gunbc.fleet_ssh_access { fleet_automation_ssh_key_fingerprint } +import gunbc.remote_host_model { ModeledRemoteHost, remote_host_binding } +import gunbc.wall_clock_model { ModeledWallClock, wall_clock_bindings } + +// THE DRY REALIZATION OF ONE mtcollins1 BOOT ATTEMPT'S WHOLE EFFECT DEMAND. The scenario world +// composes the one BMC model with what the worker running the attempt has around it: its filesystem +// (credential file, unit-hold store, SOL pid and capture files, /proc), its processes, its process +// environment, its SSH agent, the hosts it reaches over SSH, its clocks, and the host's console. Every +// transition belongs to its own model; this module places them side by side, lifts their bindings into +// the composite state, and owns only the handlers whose effect spans two of them (a collector the BMC +// session feeds and the worker's filesystem records). The real entry -- +// gunbc.machine_intake_mtcollins1_boot_run mtcollins1_boot_wet_on_srv1 -- runs unchanged over it. +type MtCollins1BootWorld { + bmc: BmcWorld + fs: ModeledFilesystem + environment: List + agent: ModeledSshAgent + remote_hosts: List + clock: ModeledWallClock + worker: ModeledWorker + console: ModeledHostConsole + media: MegaRacMediaWorld +} + +// THE WORKER'S SSH AGENT: whether it holds the fleet automation key. Its listing follows +// `ssh-add -l`: one ` ()` line per identity, exit 0; and with no +// identities, "The agent has no identities." on stdout with exit 1 (ssh-add(1)). +type ModeledSshAgent { + socket: String + holds_fleet_key: Bool +} + +fn agent_listing(agent: ModeledSshAgent) -> ShellExchangeObservation { + if agent.holds_fleet_key { + ShellProcessExited { exit_code: 0, stdout: join(["256 ", fleet_automation_ssh_key_fingerprint, " fleet-automation@gunbc (ED25519)\n"], ""), stderr: "" } + } else { + ShellProcessExited { exit_code: 1, stdout: "The agent has no identities.\n", stderr: "" } + } +} + +// THE WORKER'S PROCESSES: the SOL collector the attempt starts, and the notice watcher the boot step +// starts before the entry runs. A live process is visible the way the production observers read it +// (gunbc.machine_intake_mtcollins1_boot_run mtcollins1_sol_collector_observe, sol_observer_refusal_of): +// /proc//stat, whose field 22 is the start time the hold publishes as " ", and +// /proc//cmdline. An exited process has neither. The model writes cmdline with spaces where Linux +// writes NULs; the production reader asks only whether it contains `ipmitool`, which both answer alike. +// diagnostic_path is where the hold sends the process's stderr and its exit record (empty: none). +type ModeledProcess { + pid: Int + start_time: Int + comm: String + cmdline: String + capture_path: String + diagnostic_path: String + alive: Bool +} + +type ModeledWorker { + next_pid: Int + processes: List + uptime_at_origin: Int +} + +// THE HOST'S CONSOLE: what the machine prints on its serial line, each line at an offset from the +// start of the boot. A line reaches a capture only while the BMC's SOL session is open and a live +// collector appends it; a line printed while nobody is listening is lost, as it is on the real unit. +// emitted counts the lines of the current boot already printed. +type TimedConsoleLine { + after: Second + text: String +} + +type ModeledHostConsole { + lines: List + emitted: Int + boot: Second? +} + +fn with_bmc(w: MtCollins1BootWorld, bmc: BmcWorld) -> MtCollins1BootWorld { + MtCollins1BootWorld { bmc: bmc, fs: w.fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media } +} + +fn with_fs(w: MtCollins1BootWorld, fs: ModeledFilesystem) -> MtCollins1BootWorld { + MtCollins1BootWorld { bmc: w.bmc, fs: fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media } +} + +fn with_worker(w: MtCollins1BootWorld, worker: ModeledWorker) -> MtCollins1BootWorld { + MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: worker, console: w.console, media: w.media } +} + +fn with_console(w: MtCollins1BootWorld, console: ModeledHostConsole) -> MtCollins1BootWorld { + MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: console, media: w.media } +} + +fn with_media(w: MtCollins1BootWorld, media: MegaRacMediaWorld) -> MtCollins1BootWorld { + MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: media } +} + +fn appended(fs: ModeledFilesystem, path: String, text: String) -> ModeledFilesystem { + match fs_file(fs: fs, path: path) { + Present { value: f } => fs_with_file(fs: fs, path: path, content: concat(f.content, text)) + Absent => fs_with_file(fs: fs, path: path, content: text) + } +} + +fn proc_cmdline_path(pid: Int) -> String { + join(["/proc/", to_string(pid), "/cmdline"], "") +} + +fn proc_stat_path(pid: Int) -> String { + join(["/proc/", to_string(pid), "/stat"], "") +} + +// proc(5) stat: " () ..." with the start time at field 22, which is word 19 of what +// follows the comm -- the position the production reader (proc_stat_after_comm) takes it from. The +// fields the readers do not consult are zero. +fn proc_stat_line(p: ModeledProcess) -> String { + join([to_string(p.pid), " (", p.comm, ") S ", join(map([1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18], _i => "0"), " "), " ", to_string(p.start_time), " 0\n"], "") +} + +// The published identity, as gunbc.machine_intake.sol_hold's supervisor writes it: " ". +fn process_identity(p: ModeledProcess) -> String { + join([to_string(p.pid), " ", to_string(p.start_time), "\n"], "") +} + +// Start times in clock ticks since the worker booted (USER_HZ 100), so a later process has a later one. +fn start_ticks(w: MtCollins1BootWorld, now: Second) -> Int { + (w.worker.uptime_at_origin + (second_count(s: now) as Int)) * 100 +} + +fn process_visible(fs: ModeledFilesystem, p: ModeledProcess) -> ModeledFilesystem { + fs_with_file(fs: fs_with_file(fs: fs, path: proc_stat_path(pid: p.pid), content: proc_stat_line(p: p)), path: proc_cmdline_path(pid: p.pid), content: p.cmdline) +} + +// A PROCESS EXITS: its /proc entry goes, and the hold's supervisor records the exit in the process's +// diagnostic file (sol_hold_exit_record_prefix). The one transition every way a process ends uses -- +// a deactivate, the controller dropping the session, a release. +fn process_gone(fs: ModeledFilesystem, p: ModeledProcess) -> ModeledFilesystem { + let without = ModeledFilesystem { directories: fs.directories, files: filter(fs.files, f => f.path != proc_stat_path(pid: p.pid) && f.path != proc_cmdline_path(pid: p.pid)) } + if p.diagnostic_path == "" { without } else { appended(fs: without, path: p.diagnostic_path, text: concat(sol_hold_exit_record_prefix, "0\n")) } +} + +fn process_dead(p: ModeledProcess) -> ModeledProcess { + ModeledProcess { pid: p.pid, start_time: p.start_time, comm: p.comm, cmdline: p.cmdline, capture_path: p.capture_path, diagnostic_path: p.diagnostic_path, alive: false } +} + +fn exit_processes(w: MtCollins1BootWorld, ending: fn(ModeledProcess) -> Bool) -> MtCollins1BootWorld { + let fs = fold(filter(w.worker.processes, p => p.alive && ending(p)), init: w.fs, f: fn(acc, p) { process_gone(fs: acc, p: p) }) + let processes = map(w.worker.processes, p => if p.alive && ending(p) { process_dead(p: p) } else { p }) + with_worker(w: with_fs(w: w, fs: fs), worker: ModeledWorker { next_pid: w.worker.next_pid, processes: processes, uptime_at_origin: w.worker.uptime_at_origin }) +} + +fn is_collector(p: ModeledProcess) -> Bool { + p.comm == "ipmitool" +} + +fn live_collectors(w: MtCollins1BootWorld) -> List { + filter(w.worker.processes, p => p.alive && is_collector(p: p)) +} + +fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) -> MtCollins1BootWorld { + with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_append(w.worker.processes, p), uptime_at_origin: w.worker.uptime_at_origin }) +} + +// THE NOTICE WATCHER the boot step starts before the entry (gunbc.ci_spec): its token in the +// environment, its readiness file holding that token, and its record naming a live process -- what +// gunbc.machine_intake_mtcollins1_boot_run mtcollins1_sol_await_observer requires before any BMC +// contact. It is scenario state because the entry does not start it. +fn with_notice_watcher(w: MtCollins1BootWorld, capture_path: String, token: String) -> MtCollins1BootWorld { + let p = ModeledProcess { pid: w.worker.next_pid, start_time: start_ticks(w: w, now: second(count: 0)), comm: "bash", cmdline: "bash -c gunbc-sol-notice-watch", capture_path: capture_path, diagnostic_path: "", alive: true } + let fs = fs_with_file(fs: fs_with_file(fs: w.fs, path: concat(capture_path, mtcollins1_sol_notice_ready_suffix), content: concat(token, "\n")), path: mtcollins1_sol_notice_watcher_path(capture_path: capture_path), content: process_identity(p: p)) + let env = list_append(w.environment, ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token }) + started(w: MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: env, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media }, p: p, fs: fs) +} + +fn exited_step(state: S, stdout: String, exit_code: Int) -> OperationStep { + OperationObserved { observation: ShellObserved { observation: ShellProcessExited { exit_code: exit_code, stdout: stdout, stderr: "" } }, state: state, elapsed: second(count: 1) } +} + +// `ipmitool sdr dump ` writes the controller's SDR repository to the named local file; the +// production code checks only that it succeeded and later reads through the file. The model writes a +// placeholder of the dump into the worker's filesystem, so a later read through it finds a file. +fn sdr_dump_handler(w: MtCollins1BootWorld, call: OperationCall) -> OperationStep { + match operation_input_text(invocation: call.invocation, name: "sdr_cache_file") { + Absent => OperationHarnessFault { reason: "sdr dump was dispatched without a cache file" as NonEmptyStr } + Present { value: path } => { + let written = fs_write(fs: w.fs, path: path, content: "", create_new: false) + exited_step(state: with_fs(w: w, fs: written.fs), stdout: join(["Dumping Sensor Data Repository to '", path, "'\n"], ""), exit_code: 0) + } + } +} + +// gunbc.machine_intake.sol_hold ActivateHeld: the hold starts `ipmitool ... sol activate` in the +// background with its stdout appended to the capture and its stderr to the client diagnostic file, +// publishes " " to the pid file, and exits 0 once the job exists. On activation the +// client prints the grounded preamble (extdeps.bmc.ipmitool_observed_output +// ipmitool_sol_activate_preamble): its banner line on stdout, the rest on stderr. If the controller's +// session is already held, the client prints the refusal on stderr and exits at once, and the +// supervisor records that exit -- but the hold has already succeeded and published the pid. +fn sol_activate_held_handler(w: MtCollins1BootWorld, call: OperationCall) -> OperationStep { + match operation_input_text(invocation: call.invocation, name: "capture_path") { + Absent => OperationHarnessFault { reason: "ActivateHeld was dispatched without a capture path" as NonEmptyStr } + Present { value: capture } => match operation_input_text(invocation: call.invocation, name: "pid_path") { + Absent => OperationHarnessFault { reason: "ActivateHeld was dispatched without a pid path" as NonEmptyStr } + Present { value: pid_path } => match operation_input_text(invocation: call.invocation, name: "client_diagnostic_path") { + Absent => OperationHarnessFault { reason: "ActivateHeld was dispatched without a client diagnostic path" as NonEmptyStr } + Present { value: diag } => { + let program = match operation_input_text(invocation: call.invocation, name: "ipmitool") { Present { value: p } => p Absent => "ipmitool" } + let already = w.bmc.sol_session_open + let p = ModeledProcess { pid: w.worker.next_pid, start_time: start_ticks(w: w, now: call.now), comm: "ipmitool", cmdline: concat(program, " -H bmc -I lanplus sol activate"), capture_path: capture, diagnostic_path: diag, alive: !already } + let published = fs_write(fs: w.fs, path: pid_path, content: process_identity(p: p), create_new: false).fs + let preamble = filter(split(s: ipmitool_sol_activate_preamble, delimiter: "\n"), l => l != "") + let banner = join(map(filter(preamble, l => string_contains(s: l, pattern: ipmitool_sol_operational_banner)), l => concat(l, "\n")), "") + let stderr = join(map(filter(preamble, l => !string_contains(s: l, pattern: ipmitool_sol_operational_banner)), l => concat(l, "\n")), "") + let fs = if already { appended(fs: published, path: diag, text: concat("Info: SOL payload already active on another session\n", concat(sol_hold_exit_record_prefix, "1\n"))) } + else { appended(fs: appended(fs: published, path: capture, text: banner), path: diag, text: stderr) } + let bmc = if already { w.bmc } else { bmc_with_sol_session(world: w.bmc, open: true) } + exited_step(state: with_bmc(w: started(w: w, p: p, fs: fs), bmc: bmc), stdout: "", exit_code: 0) + } + } + } + } +} + +// `ipmitool sol deactivate` ends the controller's SOL session, and a collector attached to it loses +// its session and exits. Its pid file and activation receipt stay: removing them is the production +// release's retirement, not the controller's. +fn sol_deactivate_handler(w: MtCollins1BootWorld, call: OperationCall) -> OperationStep { + exited_step(state: with_bmc(w: exit_processes(w: w, ending: is_collector), bmc: bmc_with_sol_session(world: w.bmc, open: false)), stdout: "", exit_code: 0) +} + +// gunbc.machine_intake.sol_hold ReleaseHeld: stops the process the pid file names only while that +// " " is a live instance with that start time (sol_hold_owned_condition), and succeeds +// once it is gone; a record naming no live instance has nothing to stop and also succeeds. +fn sol_release_held_handler(w: MtCollins1BootWorld, call: OperationCall) -> OperationStep { + match operation_input_text(invocation: call.invocation, name: "pid_path") { + Absent => OperationHarnessFault { reason: "ReleaseHeld was dispatched without a pid path" as NonEmptyStr } + Present { value: pid_path } => match fs_file(fs: w.fs, path: pid_path) { + Absent => exited_step(state: w, stdout: "", exit_code: 0) + Present { value: record } => { + let named = trim(s: record.content) + exited_step(state: exit_processes(w: w, ending: fn(p) { trim(s: process_identity(p: p)) == named }), stdout: "", exit_code: 0) + } + } + } +} + +// Master Write-Read toward the SMpro. The retained attempt of 2026-09-27 (run 36335369059, +// mtcollins1-boot-diagnostics.txt sha256 eda19cde2e60d90d3d04946273e615eb5bf774496b9907e03d3bc15dbedc2c1c) recorded +// every probe refused with completion code 0xff, and no successful exchange is retained, so that is the +// grounded answer the model gives. The production code records SMpro passes and never gates on them. +fn smpro_refused_handler(w: MtCollins1BootWorld, call: OperationCall) -> OperationStep { + OperationObserved { + observation: ShellObserved { observation: ShellProcessExited { exit_code: 1, stdout: "", stderr: "Unable to send RAW command (channel=0x0 netfn=0x6 lun=0x0 cmd=0x52 rsp=0xff): Unspecified error\n" } }, + state: w, + elapsed: second(count: 1), + } +} + +// /proc/uptime: the worker's seconds since its own boot, `. ` and one newline +// (proc(5)), read over the file transport since gunbc#12636, so the record keeps its final newline. +data linux_procfs_read_uptime_operation: OperationRef = OperationRef { + path: "dag/extdeps/linux/procfs.dag", + service: "linux.Procfs", + operation: "ReadUptime", +} + +fn uptime_handler(w: MtCollins1BootWorld, call: OperationCall) -> OperationStep { + let up = w.worker.uptime_at_origin + (second_count(s: call.now) as Int) + let record = join([to_string(up), ".00 ", to_string(up), ".00\n"], "") + OperationObserved { + observation: FileObserved { observation: FileOperationSucceeded { byte_count: content_bytes(s: record), content: record } }, + state: w, + elapsed: second(count: 0), + } +} + +// THE CONSOLE ADVANCES WITH TIME. After the BMC's own events fire, every console line of the current +// boot whose offset has passed is printed; it reaches each live collector's capture only if the SOL +// session is open. A new boot restarts the console from its first line. +fn console_advance(w: MtCollins1BootWorld, now: Second) -> MtCollins1BootWorld { + if count(w.console.lines) == 0 { w } else { console_advance_booted(w: w, now: now) } +} + +fn console_advance_booted(w: MtCollins1BootWorld, now: Second) -> MtCollins1BootWorld { + match w.bmc.host_booted_at { + Absent => w + Present { value: booted } => { + let fresh = match w.console.boot { Present { value: b } => second_count(s: b) != second_count(s: booted) Absent => true } + let console = if fresh { ModeledHostConsole { lines: w.console.lines, emitted: 0, boot: Present { value: booted } } } else { w.console } + if !fresh && console.emitted >= count(console.lines) { w } else { + let elapsed = (second_count(s: now) as Int) - (second_count(s: booted) as Int) + let due = filter(console.lines.skip(n: console.emitted), l => (second_count(s: l.after) as Int) <= elapsed) + let printed = concat_text(lines: due) + let listening = w.bmc.sol_session_open && bmc_power_is_on(world: w.bmc) + let fs = if listening { fold(live_collectors(w: w), init: w.fs, f: fn(acc, p) { appended(fs: acc, path: p.capture_path, text: printed) }) } else { w.fs } + with_console(w: with_fs(w: w, fs: fs), console: ModeledHostConsole { lines: console.lines, emitted: console.emitted + count(due), boot: console.boot }) + } + } + } +} + +fn concat_text(lines: List) -> String { + join(map(lines, l => concat(l.text, "\n")), "") +} + +// A COLLECTOR LIVES ONLY WHILE ITS SESSION DOES. When the controller's SOL session ends -- on its own +// or by a deactivate -- the `ipmitool sol activate` client loses its session and exits, so its /proc +// entry disappears; its pid file stays, since nothing in the realization removes it. +fn collectors_follow_session(w: MtCollins1BootWorld) -> MtCollins1BootWorld { + if w.bmc.sol_session_open || count(live_collectors(w: w)) == 0 { w } else { exit_processes(w: w, ending: is_collector) } +} + +// Time only changes the world when something is scheduled -- a BMC event, a connecting or withdrawing +// presentation -- or when the console has lines left to print; otherwise the world is returned as it +// is, rather than rebuilt on every dispatch. +fn boot_world_idle(w: MtCollins1BootWorld) -> Bool { + count(w.bmc.pending) == 0 + && (match w.media.cd.ready_at { Absent => true Present { value: _ } => false }) + && (match w.media.withdraw_at { Absent => true Present { value: _ } => false }) +} + +fn boot_advance(w: MtCollins1BootWorld, now: Second) -> MtCollins1BootWorld { + let stepped = if boot_world_idle(w: w) { w } else { with_media(w: with_bmc(w: w, bmc: bmc_advance(world: w.bmc, now: now)), media: megarac_media_advance(world: w.media, now: now)) } + console_advance(w: collectors_follow_session(w: stepped), now: now) +} + +data sol_hold_activate_held_operation: OperationRef = OperationRef { + path: "dag/gunbc/machine_intake/sol_hold.dag", + service: "gunbc.machine_intake.sol_hold", + operation: "ActivateHeld", +} + +data sol_hold_release_held_operation: OperationRef = OperationRef { + path: "dag/gunbc/machine_intake/sol_hold.dag", + service: "gunbc.machine_intake.sol_hold", + operation: "ReleaseHeld", +} + +fn mtcollins1_boot_dry_realization(identity: NonEmptyStr, initial: MtCollins1BootWorld, epoch: Second) -> OperationRealization { + let bmc = concat(bmc_bindings(get: fn(w) { w.bmc }, put: with_bmc), megarac_bindings(get: fn(w) { w.media }, put: with_media)) + let files = filesystem_bindings(get: fn(w) { w.fs }, put: with_fs) + let local_commands = exact_invocation_binding(at: shell_exec_run_argv_operation, inputs: ["program", "arguments"], table: [ + ModeledInvocation { + words: local_command_words(command: env_prefixed_command(bindings: [EnvSet { name: "SSH_AUTH_SOCK", value: initial.agent.socket }], command: ssh_add_list_identities_command())), + answer: fn(w) { agent_listing(agent: w.agent) }, + }, + ]) + let spanning = [ + OperationBinding { at: bmc_ipmi_operation(operation: "SdrDumpAuthenticated"), handler: sdr_dump_handler }, + OperationBinding { at: bmc_ipmi_operation(operation: "SolDeactivate"), handler: sol_deactivate_handler }, + OperationBinding { at: bmc_ipmi_operation(operation: "MasterWriteReadAuthenticated"), handler: smpro_refused_handler }, + OperationBinding { at: sol_hold_activate_held_operation, handler: sol_activate_held_handler }, + OperationBinding { at: sol_hold_release_held_operation, handler: sol_release_held_handler }, + OperationBinding { at: linux_procfs_read_uptime_operation, handler: uptime_handler }, + ] + OperationRealization { + identity: identity, + initial: initial, + epoch: epoch, + bindings: concat(concat(concat(concat(bmc, files), wall_clock_bindings(get: fn(w) { w.clock })), spanning), [ + environment_binding(get: fn(w) { w.environment }), + virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"), + local_commands, + remote_host_binding(get: fn(w) { w.remote_hosts }), + ]), + advance: boot_advance, + } +} diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag index 58622d27fd1..c36803933d6 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag @@ -85,7 +85,7 @@ import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle { mtcollins1_boot_sel_snapshot, mtcollins1_boot_inventory, mtcollins1_boot_console, mtcollins1_boot_write_bundle, mtcollins1_boot_outcome_after_bundle, mtcollins1_boot_bundle_findings, bundle_write_receipt_line, mtcollins1_boot_diagnostics_allowance, AttemptIdentityReading, AttemptRunId, AttemptIdentityUnavailable, attempt_identity_text, - SmproReading, BootParam5Reading, BootParam5NotTaken, BootParam5Read, BootParam5Unread, PowerAfterUnobserved, MtCollins1BootRunRecord, run_record_not_taken, MtCollins1MediaAttachRecord, MediaAttachNotAttempted, MtCollins1HandoffMedia, recheck_text, MtCollins1EndMedia, EndMediaNotTaken, EndMediaObserved, HandoffMediaNotReached, HandoffMediaWithheldAtRecheck, HandoffMediaAttempted, HandoffConfirmed, HandoffAttemptedUnconfirmed, end_media_is_owed, mtcollins1_boot_param5, mtcollins1_boot_chassis_power, + SmproReading, BootParam5Reading, BootParam5NotTaken, BootParam5Read, BootParam5Unread, PowerAfterUnobserved, MtCollins1BootRunRecord, run_record_not_taken, MtCollins1MediaAttachRecord, MediaAttachNotAttempted, MtCollins1HandoffMedia, recheck_text, MtCollins1EndMedia, EndMediaNotTaken, EndMediaObserved, HandoffMediaNotReached, HandoffMediaWithheldAtRecheck, HandoffMediaAttempted, HandoffConfirmed, HandoffAttemptedUnconfirmed, end_media_is_owed, media_loss_after_handoff, outcome_attributing_media_loss, mtcollins1_boot_param5, mtcollins1_boot_chassis_power, BmcReachability, bmc_reachability_text, mtcollins1_boot_bmc_reachability, BmcReadCause, bmc_read_cause_text, bmc_ipmitool_session_cause, mtcollins1_ipmi_endpoint, PowerAfterAttempt, PoweredOffAfterCensusEnd, PoweredOffWithoutCensusEnd, PoweredOnAfterAttempt, PowerAfterNotTaken, power_after_attempt, OverrideNotHandedOff, boot_override_consumption, @@ -2320,7 +2320,7 @@ fn mtcollins1_boot_actuate( outcome: match observed.outcome { ExitSuccess => if sol_release_is_clean(outcome: teardown) { ExitSuccess } else { exit_failure(reason: concat("mtcollins1 boot: ", sol_release_outcome_text(outcome: teardown))) } - other => other + other => outcome_attributing_media_loss(outcome: other, loss: media_loss_after_handoff(handoff: gated.media, end: end_media)) }, stage: observed.stage, screen: screen_record, diff --git a/dag/gunbc/megarac_media_model.dag b/dag/gunbc/megarac_media_model.dag new file mode 100644 index 00000000000..3fb72c3a749 --- /dev/null +++ b/dag/gunbc/megarac_media_model.dag @@ -0,0 +1,165 @@ +module gunbc.megarac_media_model + +import std.types { Bool, Int, List, String } +import std.measure { Second, second, second_count } + +// THE BMC's VIRTUAL-MEDIA SUBSYSTEM (AMI MegaRAC SP-X, firmware 0.32): the same controller as +// gunbc.bmc_model, held as its own record because its state -- web sessions, the NFS share binding, +// the image listing and the presented CD -- moves independently of power and IPMI. Pure transitions +// with time as an input; the wire shapes are extdeps.bmc.megarac and extdeps.bmc.megarac_observed_output. +// +// SESSIONS. POST /api/session opens a session the client holds through its cookie jar and a CSRF +// token; every other route needs both. DELETE /api/session closes it, after which the same cookie and +// token are refused with 401 -- the property the production release check re-observes. +type MegaRacSession { + cookie_jar: String + csrf_token: String + open: Bool +} + +type MegaRacShare { + server: String + source_path: String + share_type: String +} + +// THE PRESENTED CD, as one configurations row. redirection_status on this firmware: 0 stopped, 100 +// connecting, 1 started (extdeps.bmc.megarac). A start moves the row to connecting and, after the +// readiness delay, to started with a bound session index; session index 255 means no session. +// ready_at is when a connecting row becomes started. +type MegaRacCdRow { + image_name: String + redirection_status: Int + media_index: Int + session_index: Int + ready_at: Second? +} + +type MegaRacImage { + image_name: String + image_index: Int +} + +// ready_after is the controller's connecting interval. Observed 2026-09-27 (gunbc.machine_intake_megarac_media_attach +// readiness notes): status 100 at +6s, then 1 with session index 0 from +12s. +type MegaRacMediaWorld { + sessions: List + next_session: Int + share: MegaRacShare + mount_cd: Int + cd_error_code: Int + images: List + cd: MegaRacCdRow + ready_after: Second + withdraw_at: Second? + withdraw_after_ready: Second? +} + +fn megarac_cleared_cd() -> MegaRacCdRow { + MegaRacCdRow { image_name: "", redirection_status: 0, media_index: 0, session_index: 255, ready_at: none } +} + +fn megarac_session_valid(world: MegaRacMediaWorld, cookie_jar: String, csrf_token: String) -> Bool { + !all(world.sessions, s => !(s.open && s.cookie_jar == cookie_jar && s.csrf_token == csrf_token)) +} + +fn megarac_session_by_jar(world: MegaRacMediaWorld, cookie_jar: String) -> Bool { + !all(world.sessions, s => !(s.open && s.cookie_jar == cookie_jar)) +} + +fn megarac_with_sessions(world: MegaRacMediaWorld, sessions: List, next_session: Int) -> MegaRacMediaWorld { + MegaRacMediaWorld { sessions: sessions, next_session: next_session, share: world.share, mount_cd: world.mount_cd, cd_error_code: world.cd_error_code, images: world.images, cd: world.cd, ready_after: world.ready_after, withdraw_at: world.withdraw_at, withdraw_after_ready: world.withdraw_after_ready } +} + +fn megarac_with_cd(world: MegaRacMediaWorld, cd: MegaRacCdRow) -> MegaRacMediaWorld { + MegaRacMediaWorld { sessions: world.sessions, next_session: world.next_session, share: world.share, mount_cd: world.mount_cd, cd_error_code: world.cd_error_code, images: world.images, cd: cd, ready_after: world.ready_after, withdraw_at: world.withdraw_at, withdraw_after_ready: world.withdraw_after_ready } +} + +type MegaRacOpened { + world: MegaRacMediaWorld + racsession_id: Int + csrf_token: String +} + +fn megarac_open_session(world: MegaRacMediaWorld, cookie_jar: String) -> MegaRacOpened { + let id = world.next_session + let token = concat("modeled-csrf-", to_string(id)) + MegaRacOpened { + world: megarac_with_sessions(world: world, sessions: list_append(world.sessions, MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1), + racsession_id: id, + csrf_token: token, + } +} + +fn megarac_close_session(world: MegaRacMediaWorld, cookie_jar: String, csrf_token: String) -> MegaRacMediaWorld { + megarac_with_sessions( + world: world, + sessions: map(world.sessions, s => if s.cookie_jar == cookie_jar && s.csrf_token == csrf_token { MegaRacSession { cookie_jar: s.cookie_jar, csrf_token: s.csrf_token, open: false } } else { s }), + next_session: world.next_session, + ) +} + +fn megarac_image_index(world: MegaRacMediaWorld, image_name: String) -> Int? { + fold(world.images, init: none, f: fn(acc, i) { + match acc { + Present { value: v } => Present { value: v } + Absent => if i.image_name == image_name { Present { value: i.image_index } } else { none } + } + }) +} + +// A start names an image and its listing index. The row connects, and becomes started after the +// connecting interval. A start naming an image the listing does not hold changes nothing; whether the +// firmware answers such a start with an error body is not observed, so the adapter reports the write as +// accepted and readiness -- which the production code waits on -- never arrives. +fn megarac_start_media(world: MegaRacMediaWorld, image_name: String, image_index: Int, now: Second) -> MegaRacMediaWorld { + match megarac_image_index(world: world, image_name: image_name) { + Present { value: idx } => + if idx == image_index { + megarac_with_cd(world: world, cd: MegaRacCdRow { + image_name: image_name, redirection_status: 100, media_index: 0, session_index: 255, + ready_at: Present { value: second(count: second_count(s: now) + second_count(s: world.ready_after)) }, + }) + } else { world } + Absent => world + } +} + +fn megarac_stop_media(world: MegaRacMediaWorld) -> MegaRacMediaWorld { + megarac_with_cd(world: world, cd: megarac_cleared_cd()) +} + +// A PRESENTATION CAN BE LOST AFTER IT WAS READY: withdraw_at, when set, is the instant the controller +// drops the presented CD on its own (the NFS export going away, the firmware's retry giving up), after +// which the row reads cleared. The production code re-observes the presentation before the handoff for +// exactly this. +fn megarac_media_advance(world: MegaRacMediaWorld, now: Second) -> MegaRacMediaWorld { + let readied = megarac_media_ready(world: world, now: now) + match readied.withdraw_at { + Absent => readied + Present { value: at } => + if second_count(s: at) <= second_count(s: now) { + MegaRacMediaWorld { sessions: readied.sessions, next_session: readied.next_session, share: readied.share, mount_cd: readied.mount_cd, cd_error_code: readied.cd_error_code, images: readied.images, cd: megarac_cleared_cd(), ready_after: readied.ready_after, withdraw_at: none, withdraw_after_ready: readied.withdraw_after_ready } + } else { readied } + } +} + +fn megarac_media_ready(world: MegaRacMediaWorld, now: Second) -> MegaRacMediaWorld { + match world.cd.ready_at { + Absent => world + Present { value: at } => + if second_count(s: at) <= second_count(s: now) { + megarac_withdrawal_armed(world: megarac_with_cd(world: world, cd: MegaRacCdRow { image_name: world.cd.image_name, redirection_status: 1, media_index: world.cd.media_index, session_index: 0, ready_at: none }), ready: at) + } else { world } + } +} + +// A scenario may ask for the presentation to be lost a fixed interval after it became ready; the +// instant is armed when readiness arrives, so the loss follows the route rather than a guessed clock. +fn megarac_withdrawal_armed(world: MegaRacMediaWorld, ready: Second) -> MegaRacMediaWorld { + match world.withdraw_after_ready { + Absent => world + Present { value: after } => + MegaRacMediaWorld { sessions: world.sessions, next_session: world.next_session, share: world.share, mount_cd: world.mount_cd, cd_error_code: world.cd_error_code, images: world.images, cd: world.cd, ready_after: world.ready_after, withdraw_at: Present { value: second(count: second_count(s: ready) + second_count(s: after)) }, withdraw_after_ready: none } + } +} diff --git a/dag/gunbc/modeled_operation_realization_seed_growth.dag b/dag/gunbc/modeled_operation_realization_seed_growth.dag index 4fbc25de101..ce1fa8a5438 100644 --- a/dag/gunbc/modeled_operation_realization_seed_growth.dag +++ b/dag/gunbc/modeled_operation_realization_seed_growth.dag @@ -51,9 +51,11 @@ data modeled_operation_realization_seed_growth_justification: SeedGrowthJustific DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "dispatch_modeled_operation", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "shell_result_of_observation", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "shell_result_projection", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "file_result_of_observation", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "file_transport_path", field: WholeDeclaration }, ], reason: "The seed interpreter is the only evaluator that runs the boot orchestrator, and the acceptance matrix (#12423, operator ruling 2026-09-27) must execute that orchestrator against controlled device histories. These items are the seed realization of a .dag contract: selection is v2.std.operation_realization operation_handler_selection over std.effect_grant covering_grant, admission is modeled_realization_admitted_in and operation_realization_duplicate, the virtual clock is virtual_clock_origin and virtual_clock_after over std.measure Second, and every scenario transition is gunbc.bmc_model. The Rust holds a state value, a clock value and the dispatch log, and dispatches; shell_result_projection is the existing wet shell projection extracted so the modeled observation reaches the same decoder path.", owning_dissolution_lane: "v1-materialization-kernel" as RoadmapNodeId, trigger: "Witnesses emit to native code and the emitted runtime realizes the evaluation frame and its modeled operation realization; these items then delete with the WITNESS_EVALUATION_FRAMES stack while test.claim.operation_realization_witness_test stays green without them. That witness is the deletion's regression control.", - current_boundary: "Shell transport observations only: a REST or file operation under a modeled frame refuses as a harness fault. Admitted only under Hermetic execution. No device logic in Rust. Nested frames inside an active realization are refused.", + current_boundary: "Shell and file transport observations (the file arm added by gunbc#12533 feeds the existing map_file_outputs; bound_operation_invocation_value records a ProcessArgvExpansion input as the words push_process_argv_expansion expands for a real spawn): a REST operation under a modeled frame refuses as a harness fault. Admitted only under Hermetic execution. No device logic in Rust. Nested frames inside an active realization are refused.", } diff --git a/dag/gunbc/process_environment_model.dag b/dag/gunbc/process_environment_model.dag new file mode 100644 index 00000000000..7c659345545 --- /dev/null +++ b/dag/gunbc/process_environment_model.dag @@ -0,0 +1,58 @@ +module gunbc.process_environment_model + +import std.types { List, NonEmptyStr, String } +import std.measure { second } +import v2.std.operation_argv { OperationRef } +import v2.std.operation_realization { + OperationBinding, OperationCall, OperationStep, OperationObserved, OperationHarnessFault, + ShellObserved, operation_input_text, +} +import extdeps.transports.shell { ShellProcessExited } + +// A MODELED PROCESS ENVIRONMENT: the variables a scenario's worker was started with, answered through +// the realization's own contract for extdeps.shell shell.Env.Get (printenv): a set variable prints its +// value and exits 0; an unset one prints nothing and exits 1, which the operation's optional output +// projects to Absent -- exactly as a real printenv does. A variable set to the empty string is SET, and +// prints an empty line, so the consumer's own set-but-empty refusal is exercised rather than bypassed. +type ModeledVariable { + name: String + value: String +} + +data shell_env_get_operation: OperationRef = OperationRef { + path: "dag/extdeps/shell.dag", + service: "shell.Env", + operation: "Get", +} + +fn modeled_variable(variables: List, name: String) -> ModeledVariable? { + fold(variables, init: none, f: fn(acc, v) { + match acc { + Present { value: found } => Present { value: found } + Absent => if v.name == name { Present { value: v } } else { none } + } + }) +} + +fn environment_binding(get: fn(S) -> List) -> OperationBinding { + OperationBinding { + at: shell_env_get_operation, + handler: fn(state, call) { + match operation_input_text(invocation: call.invocation, name: "name") { + Absent => OperationHarnessFault { reason: "an environment read was dispatched without a name" as NonEmptyStr } + Present { value: name } => match modeled_variable(variables: get(state), name: name) { + Present { value: v } => OperationObserved { + observation: ShellObserved { observation: ShellProcessExited { exit_code: 0, stdout: concat(v.value, "\n"), stderr: "" } }, + state: state, + elapsed: second(count: 0), + } + Absent => OperationObserved { + observation: ShellObserved { observation: ShellProcessExited { exit_code: 1, stdout: "", stderr: "" } }, + state: state, + elapsed: second(count: 0), + } + } + } + }, + } +} diff --git a/dag/gunbc/remote_host_model.dag b/dag/gunbc/remote_host_model.dag new file mode 100644 index 00000000000..df1aa23cc36 --- /dev/null +++ b/dag/gunbc/remote_host_model.dag @@ -0,0 +1,127 @@ +module gunbc.remote_host_model + +import std.types { Bool, List, NonEmptyStr, String } +import std.measure { second } +import v2.std.operation_realization { + OperationBinding, OperationCall, OperationStep, OperationObserved, OperationHarnessFault, ShellObserved, +} +import extdeps.transports.shell { ShellExchangeObservation, ShellProcessExited } +import extdeps.exec.command { argv_words } +import extdeps.tools.gnu_coreutils { cat_command } +import extdeps.crypto.hash { sha256sum_file_command } +import gunbc.host_command_model { dispatched_words, ssh_session_exec_portable_words_operation } + +// A MODELED REMOTE HOST reached over extdeps.ssh.session ssh.Session.ExecPortableWords. The SSH client +// arguments are shaped as ` -- ` (gunbc.fleet_known_hosts_anchor +// shape_fleet_ssh_exec), and the far side sees exactly the endpoint and the remote words; the model is +// that far side. It answers ONLY the remote words the production command builders produce for the +// paths it holds -- extdeps.tools.gnu_coreutils cat_command and extdeps.crypto.hash +// sha256sum_file_command -- compared exactly, so nothing is dispatched on a program's name. Anything +// else, including a request for another endpoint, is a harness fault. +// +// NOT JUDGED HERE, and stated so a green over it is not over-read: the client-side options before the +// endpoint (host-key trust, credential, config suppression). They are the real OpenSSH client's to +// honour; their evidence is the SSH transport's own controls, not this model. +// +// A FILE IS ITS CONTENT AND ITS DECLARED DIGEST. An image is not hashed in .dag; the scenario declares +// the SHA-256 its bytes have, and the model reports it in sha256sum's own format. A path with no +// content is absent, and both commands answer as coreutils does for a missing file. +type ModeledRemoteFile { + path: String + content: String? + sha256: String? +} + +type ModeledRemoteHost { + endpoint: String + files: List +} + +fn remote_missing(tool: String, path: String) -> ShellExchangeObservation { + ShellProcessExited { exit_code: 1, stdout: "", stderr: join([tool, ": ", path, ": No such file or directory\n"], "") } +} + +fn remote_cat(file: ModeledRemoteFile) -> ShellExchangeObservation { + match file.content { + Absent => remote_missing(tool: "cat", path: file.path) + Present { value: c } => ShellProcessExited { exit_code: 0, stdout: c, stderr: "" } + } +} + +fn remote_sha256sum(file: ModeledRemoteFile) -> ShellExchangeObservation { + match file.content { + Absent => remote_missing(tool: "sha256sum", path: file.path) + Present { value: _ } => match file.sha256 { + Absent => ShellProcessExited { exit_code: 1, stdout: "", stderr: join(["sha256sum: ", file.path, ": Input/output error\n"], "") } + Present { value: d } => ShellProcessExited { exit_code: 0, stdout: join([d, " ", file.path, "\n"], ""), stderr: "" } + } + } +} + +type RemoteRequest { + endpoint: String + words: List +} + +// The far side of the client args: the word before the FIRST `--` is the endpoint, everything after +// it is the remote command -- which may itself carry a `--` (sha256sum -- ). No separator at all +// means the request is not one this shape produces. +fn remote_request(client_args: List) -> RemoteRequest? { + let separators = filter(client_args, a => a == "--") + if count(separators) == 0 { none } else { + let before = take_while(xs: client_args, keep: fn(a) { a != "--" }) + let after = client_args.skip(n: count(before) + 1) + match before.last() { + Absent => none + Present { value: endpoint } => Present { value: RemoteRequest { endpoint: endpoint, words: after } } + } + } +} + +fn take_while(xs: List, keep: fn(String) -> Bool) -> List { + fold(xs, init: TakeWhileState { kept: [], open: true }, f: fn(acc, x) { + if acc.open && keep(x) { TakeWhileState { kept: list_append(acc.kept, x), open: true } } + else { TakeWhileState { kept: acc.kept, open: false } } + }).kept +} + +type TakeWhileState { + kept: List + open: Bool +} + +fn remote_answer(host: ModeledRemoteHost, words: List) -> ShellExchangeObservation? { + fold(host.files, init: none, f: fn(acc, file) { + match acc { + Present { value: v } => Present { value: v } + Absent => + if words == argv_words(command: cat_command(path: file.path)) { Present { value: remote_cat(file: file) } } + else if words == argv_words(command: sha256sum_file_command(path: file.path)) { Present { value: remote_sha256sum(file: file) } } + else { none } + } + }) +} + +fn remote_host_binding(get: fn(S) -> List) -> OperationBinding { + OperationBinding { + at: ssh_session_exec_portable_words_operation, + handler: fn(state, call) { + match dispatched_words(bindings: call.invocation.bindings, name: "client_args") { + Absent => OperationHarnessFault { reason: "a remote exec was dispatched without client args" as NonEmptyStr } + Present { value: args } => match remote_request(client_args: args) { + Absent => OperationHarnessFault { reason: "the client args do not end in ` -- `" as NonEmptyStr } + Present { value: request } => { + let hosts = filter(get(state), h => h.endpoint == request.endpoint) + match hosts.first() { + Absent => OperationHarnessFault { reason: join(["no modeled host answers at ", request.endpoint], "") as NonEmptyStr } + Present { value: host } => match remote_answer(host: host, words: request.words) { + Absent => OperationHarnessFault { reason: join(["the modeled host at ", request.endpoint, " answers no command `", join(request.words, " "), "`"], "") as NonEmptyStr } + Present { value: observation } => OperationObserved { observation: ShellObserved { observation: observation }, state: state, elapsed: second(count: 1) } + } + } + } + } + } + }, + } +} diff --git a/dag/gunbc/roadmap/roadmap_launch_deployment_observe.dag b/dag/gunbc/roadmap/roadmap_launch_deployment_observe.dag index 894ef87f0fb..c0e6f86f07d 100644 --- a/dag/gunbc/roadmap/roadmap_launch_deployment_observe.dag +++ b/dag/gunbc/roadmap/roadmap_launch_deployment_observe.dag @@ -7,6 +7,8 @@ import gunbc.live_deploy.emit { belt_tick_cadence } import std.types { String, Bool, NonEmptyStr, Int, List } import std.algebra { trim } +import extdeps.units.iso8601 { iso8601_seconds_per_minute } +import extdeps.units.iso8601_calendar { iso8601_days_from_civil, iso8601_gregorian_days_in_month, iso8601_seconds_per_day, iso8601_seconds_per_hour } import extdeps.http.client import extdeps.languages.json.emit { JsonValue, JsonString, JsonBool, serialize_json } import extdeps.languages.json.parse { @@ -266,29 +268,12 @@ fn observe_workflow_document_routed(base_url: String) -> RoadmapWorkflowObservat // ---------------------------------------------------------------- instants // `%Y-%m-%dT%H:%M:%SZ` to seconds since 1970-01-01T00:00:00Z. Days-from-civil is the proleptic // Gregorian algorithm (Howard Hinnant, "chrono-Compatible Low-Level Date Algorithms"), exact for -// every date the format can spell. Anything that is not exactly that shape refuses. +// every date the format can spell; the calendar is extdeps.units.iso8601_calendar's, which also formats the +// same instants. Anything that is not exactly that shape refuses. fn two_digits_at(s: String, i: Int) -> Int? { parse_int(s: substring(s: s, start: i, end: i + 2)) } -fn days_from_civil(y: Int, m: Int, d: Int) -> Int { - let yy = if m <= 2 { y - 1 } else { y } - let era = (if yy >= 0 { yy } else { yy - 399 }) / 400 - let yoe = yy - era * 400 - let mp = if m > 2 { m - 3 } else { m + 9 } - let doy = (153 * mp + 2) / 5 + d - 1 - let doe = yoe * 365 + yoe / 4 - yoe / 100 + doy - era * 146097 + doe - 719468 -} - -// systemd-independent Gregorian day-in-month bound with the leap rule; a calendar-impossible day -// (Feb 30, Apr 31) must refuse rather than normalize silently through days_from_civil (review 57773). -fn gregorian_days_in_month(y: Int, m: Int) -> Int { - if m == 2 { - if y - (y / 4) * 4 == 0 && (y - (y / 100) * 100 != 0 || y - (y / 400) * 400 == 0) { 29 } else { 28 } - } else if m == 4 || m == 6 || m == 9 || m == 11 { 30 } else { 31 } -} - fn iso8601_utc_epoch_seconds(text: String) -> Second? { let t = trim(s: text) if string_length(s: t) != 20 { @@ -316,11 +301,11 @@ fn iso8601_utc_epoch_seconds(text: String) -> Second? { match two_digits_at(s: t, i: 17) { Absent => none Present { value: ss } => - if m < 1 || m > 12 || d < 1 || d > gregorian_days_in_month(y: y, m: m) || hh > 23 || mm > 59 || ss > 60 { + if m < 1 || m > 12 || d < 1 || d > iso8601_gregorian_days_in_month(y: y, m: m) || hh > 23 || mm > 59 || ss > 60 { none } else { { - let epoch = days_from_civil(y: y, m: m, d: d) * 86400 + hh * 3600 + mm * 60 + ss + let epoch = iso8601_days_from_civil(y: y, m: m, d: d) * iso8601_seconds_per_day() + hh * iso8601_seconds_per_hour() + mm * (iso8601_seconds_per_minute() as Int) + ss if epoch < 0 { none } else { diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 51d6e080e84..84b7780020d 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -4,6 +4,7 @@ import gunbc.site.markup { page_render_refusal_body } import gunbc.roadmap.roadmap_event_carrier { roadmap_event_carrier_layout_for_instance, roadmap_standings_read } import std.types { String, Int, Bool, List, NonEmptyStr } +import extdeps.filesystem.filesystem_io { Filesystem } import std.algebra { trim } import std.content_hash { content_hash_tagged_structural, content_hash_atom } import extdeps.http.server { MediaType, text_html_utf8, text_plain_utf8, application_json_utf8, ServeHttpResponse } diff --git a/dag/gunbc/rung_drop/mtcollins1_boot_matrix_enrolment_dead_band_observed_only.dag b/dag/gunbc/rung_drop/mtcollins1_boot_matrix_enrolment_dead_band_observed_only.dag new file mode 100644 index 00000000000..934575ee04b --- /dev/null +++ b/dag/gunbc/rung_drop/mtcollins1_boot_matrix_enrolment_dead_band_observed_only.dag @@ -0,0 +1,44 @@ +module gunbc.rung_drop.mtcollins1_boot_matrix_enrolment_dead_band_observed_only + +import std.types { NonEmptyStr, List, String } +import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, ReplacementStaged } +import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } +import gunbc.rung_drop.mtcollins1_boot_matrix_new_witness_eval_step_cost { mtcollins1_boot_matrix_native_witness_capability } +import v2.workflow.floor_enrolment_dead_band { mtcollins1_boot_matrix_enrolment_dead_band_observed_only } + +// THE DECLARED RUNG DROP for the enrolment margin over the mtcollins1 boot matrix cases whose honest +// CPU lies in the gate's dead band (margin, per-subject line] (DESIGN 4b(3); side-chat ruling of +// eager-owl-205 on gunbc#12533, 2026-09-30; precedent `app_attest_verifier_enrolment_dead_band_observed_only`). +// The POPULATION's authority is `v2.workflow.floor_enrolment_dead_band` +// `mtcollins1_boot_matrix_enrolment_dead_band_observed_only`, each row carrying its CI-observed CPU. +// +// WHAT IS LOST IS THE ENROLMENT-MARGIN DECISION, AND ONLY THAT. The cases stay test fns and execute on +// every required floor that plans them; a semantic red, a runtime error, a route gap, a wall +// interruption and a missing terminal stay armed, and the eval-step overrun is the sibling drop's. The +// authority is self-staling on both sides: at or under the margin a row blocks as +// enrolment_dead_band_stale, above the line as enrolment_dead_band_wrong_ground. +// +// WHY THE COST IS NOT CUT: it is the subject. Each case runs the real entry, and the CPU above the +// margin is gunbc#12434's own SOL polling route -- watch ticks reading the pid file, /proc and the +// capture -- answered faithfully by the dry realization; an ablation on the merged tree found no model +// hotspot (a stubbed advance only shortened the route). The restoration is the same capability as the +// eval-step drop's, named once in `mtcollins1_boot_matrix_native_witness_capability`. +data mtcollins1_boot_matrix_enrolment_dead_band_observed_only_population: List = mtcollins1_boot_matrix_enrolment_dead_band_observed_only() |> map(o => concat(concat(o.identity, ": "), o.reason as String)) + +data mtcollins1_boot_matrix_enrolment_dead_band_observed_only_drop: RungDrop = RungDrop { + identity: "mtcollins1_boot_matrix_enrolment_dead_band_observed_only" as NonEmptyStr, + + subject: "the enrolment-margin decision over the mtcollins1 boot acceptance matrix cases whose honest CPU lies in (margin, per-subject line]: they execute, and an exact reading inside the band is reported rather than decided", + + declared: "2026-09-30", + + standing: Standing, + + declaration: TypedDeclaration { + previous: MechanicallyPreventable, + temporary: Mitigatable, + reason: ReplacementStaged { replacement: "the matrix cases executing as natively emitted witnesses, the same replacement the eval-step drop mtcollins1_boot_matrix_new_witness_eval_step_cost waits on" }, + population: mtcollins1_boot_matrix_enrolment_dead_band_observed_only_population, + restoration_trigger: concat(concat("THE CAPABILITY: ", mtcollins1_boot_matrix_native_witness_capability), "; WHAT THAT MUST BE SUFFICIENT FOR: each dead-band identity reaches its verdict with stable headroom under the enrolment margin v2.workflow.floor_enrolment_margin derives, with its route and outcome assertions unchanged -- at which point every row stales and deletes. Cutting the polling route the cases assert, or supplying a decided value in place of the entry, satisfies neither."), + } +} diff --git a/dag/gunbc/rung_drop/mtcollins1_boot_matrix_new_witness_eval_step_cost.dag b/dag/gunbc/rung_drop/mtcollins1_boot_matrix_new_witness_eval_step_cost.dag new file mode 100644 index 00000000000..9154e0dcae7 --- /dev/null +++ b/dag/gunbc/rung_drop/mtcollins1_boot_matrix_new_witness_eval_step_cost.dag @@ -0,0 +1,57 @@ +module gunbc.rung_drop.mtcollins1_boot_matrix_new_witness_eval_step_cost + +import std.types { String, List, NonEmptyStr } +import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, ReplacementStaged } +import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } +import v2.workflow.floor_eval_step_cost_drop { floor_eval_step_cost_drop_boot_matrix_rows } + +// DECLARED 4b(3) DROP (gunbc#12533, 2026-09-28; the cost-debt ruling of eager-owl-205 on the #12423 +// matrix, msg_83af891b). The DECLARATION lives here; the POPULATION's authority is +// `v2.workflow.floor_eval_step_cost_drop` `floor_eval_step_cost_drop_boot_matrix_rows`. +// +// WHAT IS LOST IS ONE WALL, AND THE CLAIMS ARE UNTOUCHED. The eleven identities are planned, executed +// and measured on every pull request that edits them; a semantic red and a wall-clock crossing still +// block. Only the eval-step overrun is reported as `EvalStepsOverBudgetUnderDeclaredDrop` rather than +// refusing. The budget is not raised. Their CPU stays under the enrolment margin, so they enrol +// without a cost-debt admission (one would be stale under the per-subject line and block). +// +// WHY THE OVERRUN IS THE SUBJECT'S AND NOT DUPLICATED WORK. Each case asserts the ROUTE the real boot +// entry takes -- which effects, in which order, under which hold -- and its typed outcome, which #12423 +// requires be executed through the real production boundary. The decision folds each case reaches are +// already witnessed at their narrower interfaces with supplied values (the media convergence folds, +// the power selection, the host-capture verdict, the hold store); what only the entry can establish is +// that it reaches them with the state its own earlier steps built. The route prefix up to the hold is +// NOT one computation repeated: each case evaluates the entry over its own world, so the same code runs +// on different inputs, and sharing it would mean resuming every case from one snapshot -- replacing the +// route from the entry that each case exists to assert. What IS shared is the construction of the +// healthy world the cases vary, and it is already the section 3 remedy: a SUPPLIED value, constructed +// directly rather than derived by executing production. MEASURED (claim_batch, 2026-09-29, review +// 72606): building that world with its census console and the frame costs 1,687 to 3,793 eval steps, +// against 73,872 to 170,048 for the member cases (re-measured after #12434's route was bound); with it removed even the cheapest member stays over +// the 72,300 budget. So hoisting it neither retires this drop nor removes a member, and none is owed. +data mtcollins1_boot_matrix_new_witness_eval_step_cost_population: List = floor_eval_step_cost_drop_boot_matrix_rows |> map(m => concat(concat(m.identity, ": over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by "), m.measured_by)) + +// THE ONE CAPABILITY that retires both matrix cost drops -- this one and +// `gunbc.rung_drop.mtcollins1_boot_matrix_enrolment_dead_band_observed_only` -- named once so the two +// cannot drift apart: the cost of both is the seed interpreter running the real entry. +data mtcollins1_boot_matrix_native_witness_capability: String = "witnesses emitted to native code with the emitted runtime realizing v2.std.witness_evaluation evaluate_in_witness_frame and its v2.std.operation_realization modeled realization, EXECUTING ON THE MERGE PATH as a phase of a required lane whose red blocks a merge, running the mtcollins1 boot acceptance matrix with the real mtcollins1_boot_wet_on_srv1 entry" + +data mtcollins1_boot_matrix_new_witness_eval_step_cost: RungDrop = RungDrop { + identity: "mtcollins1_boot_matrix_new_witness_eval_step_cost" as NonEmptyStr, + + subject: "new-witness eval-step cost gate over the eleven mtcollins1 boot acceptance matrix cases that run the real boot entry end to end over the dry operation realization: they still execute, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered", + + declared: "2026-09-28", + + standing: Standing, + + declaration: TypedDeclaration { + previous: MechanicallyPreventable, + temporary: Mitigatable, + reason: ReplacementStaged { + replacement: "the evaluation frame and its modeled operation realization realized by the natively emitted runtime, so the boot entry runs as emitted code rather than in the seed interpreter", + }, + population: mtcollins1_boot_matrix_new_witness_eval_step_cost_population, + restoration_trigger: concat(concat("THE CAPABILITY: ", mtcollins1_boot_matrix_native_witness_capability), "; WHAT THAT MUST BE SUFFICIENT FOR: each of these eleven identities measures under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives, with its route and outcome assertions unchanged. Hoisting the shared world construction or the route prefix lowers the bill and retires nothing on its own; supplying a decided value in place of the entry, or deleting the identities, satisfies neither."), + } +} diff --git a/dag/gunbc/rung_drop/roster.dag b/dag/gunbc/rung_drop/roster.dag index 65152f38e6b..a1ad5cf79dd 100644 --- a/dag/gunbc/rung_drop/roster.dag +++ b/dag/gunbc/rung_drop/roster.dag @@ -92,8 +92,10 @@ import gunbc.rung_drop.live_deploy_dark_install_render_new_witness_eval_step_cos import gunbc.rung_drop.roadmap_live_forecast_new_witness_eval_step_cost { roadmap_live_forecast_new_witness_eval_step_cost } import gunbc.rung_drop.roadmap_page_style_new_witness_eval_step_cost { roadmap_page_style_new_witness_eval_step_cost } import gunbc.rung_drop.app_attest_interpreted_crypto_new_witness_eval_step_cost { app_attest_interpreted_crypto_new_witness_eval_step_cost } +import gunbc.rung_drop.mtcollins1_boot_matrix_new_witness_eval_step_cost { mtcollins1_boot_matrix_new_witness_eval_step_cost } import gunbc.rung_drop.app_attest_verifier_new_witness_eval_step_cost { app_attest_verifier_new_witness_eval_step_cost } import gunbc.rung_drop.app_attest_verifier_enrolment_dead_band_observed_only { app_attest_verifier_enrolment_dead_band_observed_only } +import gunbc.rung_drop.mtcollins1_boot_matrix_enrolment_dead_band_observed_only { mtcollins1_boot_matrix_enrolment_dead_band_observed_only_drop } import gunbc.rung_drop.sha256_span_program_serialize_new_witness_eval_step_cost { sha256_span_program_serialize_new_witness_eval_step_cost } import gunbc.rung_drop.v41_row_store_host_realized_by_sample { v41_row_store_host_realized_by_sample } import gunbc.rung_drop.seam_monolith_control_unmeasured_derived_root { seam_monolith_control_unmeasured_derived_root } @@ -186,8 +188,10 @@ data rung_drop_roster: List = [ roadmap_live_forecast_new_witness_eval_step_cost, roadmap_page_style_new_witness_eval_step_cost, app_attest_interpreted_crypto_new_witness_eval_step_cost, + mtcollins1_boot_matrix_new_witness_eval_step_cost, app_attest_verifier_new_witness_eval_step_cost, app_attest_verifier_enrolment_dead_band_observed_only, + mtcollins1_boot_matrix_enrolment_dead_band_observed_only_drop, sha256_span_program_serialize_new_witness_eval_step_cost, v41_row_store_host_realized_by_sample, seam_monolith_control_unmeasured_derived_root, diff --git a/dag/gunbc/wall_clock_model.dag b/dag/gunbc/wall_clock_model.dag new file mode 100644 index 00000000000..4180a8b828f --- /dev/null +++ b/dag/gunbc/wall_clock_model.dag @@ -0,0 +1,51 @@ +module gunbc.wall_clock_model + +import std.types { EpochSecs, Int, List, String } +import std.measure { Second, second, second_count, SecondDisplacement, second_displacement_count } +import v2.std.operation_argv { OperationRef } +import v2.std.operation_realization { + OperationBinding, OperationCall, OperationStep, OperationObserved, ShellObserved, +} +import extdeps.transports.shell { ShellProcessExited } +import extdeps.units.iso8601_calendar { iso8601_utc_text } + +// A MODELED WALL CLOCK: what the worker's `date` prints, as a function of the realization's virtual +// clock. The virtual clock (v2.std.operation_realization, a Nat-counted Second) is monotonic by +// construction; the WALL clock is not, and a real host's can step backwards (NTP, a VM restored from +// a snapshot). So the model keeps them apart: a reading is the Unix time the scenario assigns to the +// virtual origin, plus the virtual seconds elapsed, plus a signed step the scenario may set -- a +// negative step is a backward clock the consumer must survive, while virtual time, deadlines and +// scheduled events keep moving forward. +// +// It answers extdeps.clock Clock.Now in `date -u +%Y-%m-%dT%H:%M:%SZ` form, and Clock.UnixSecs and +// Clock.UnixMillis in `date +%s` and `date +%s%3N` form; the calendar is extdeps.units.iso8601_calendar's. +type ModeledWallClock { + unix_at_origin: EpochSecs + step: SecondDisplacement +} + +fn wall_clock_unix(clock: ModeledWallClock, now: Second) -> Int { + (clock.unix_at_origin as Int) + (second_count(s: now) as Int) + second_displacement_count(d: clock.step) +} + +data clock_operation_path: String = "dag/extdeps/clock/clock.dag" + +fn clock_operation(operation: String) -> OperationRef { + OperationRef { path: clock_operation_path, service: "Clock", operation: operation } +} + +fn wall_clock_printed(state: S, text: String) -> OperationStep { + OperationObserved { + observation: ShellObserved { observation: ShellProcessExited { exit_code: 0, stdout: concat(text, "\n"), stderr: "" } }, + state: state, + elapsed: second(count: 0), + } +} + +fn wall_clock_bindings(get: fn(S) -> ModeledWallClock) -> List> { + [ + OperationBinding { at: clock_operation(operation: "Now"), handler: fn(state, call) { wall_clock_printed(state: state, text: iso8601_utc_text(unix: wall_clock_unix(clock: get(state), now: call.now))) } }, + OperationBinding { at: clock_operation(operation: "UnixSecs"), handler: fn(state, call) { wall_clock_printed(state: state, text: to_string(wall_clock_unix(clock: get(state), now: call.now))) } }, + OperationBinding { at: clock_operation(operation: "UnixMillis"), handler: fn(state, call) { wall_clock_printed(state: state, text: to_string(wall_clock_unix(clock: get(state), now: call.now) * 1000)) } }, + ] +} diff --git a/dag/std/measure.dag b/dag/std/measure.dag index d114a0fcc3b..05c9b1a6706 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -1609,6 +1609,19 @@ fn second_count(s: Second) -> Nat { measure_count(s) } +// A SIGNED DURATION: a displacement in time that may be negative, as a wall clock stepping backwards +// is. Second is Nat-counted and so cannot carry it; this is the same instant-versus-displacement split +// CelsiusDelta and ArcsecondDisplacement make for their quantities. +type SecondDisplacement = Measure + +fn second_displacement(count: Int) -> SecondDisplacement { + Measure { count: count } +} + +fn second_displacement_count(d: SecondDisplacement) -> Int { + measure_count(d) +} + fn energy_from_power_and_time(power: Watt, time: Second) -> Joule { joule(watt_count(w: power) * second_count(s: time)) } diff --git a/dag/test/claim/bmc_model_web_kvm_witness_test.dag b/dag/test/claim/bmc_model_web_kvm_witness_test.dag index aa7e15b3789..2c51aeac002 100644 --- a/dag/test/claim/bmc_model_web_kvm_witness_test.dag +++ b/dag/test/claim/bmc_model_web_kvm_witness_test.dag @@ -6,7 +6,7 @@ import v2.std.optional { Present, Absent } import std.measure { second } import gunbc.bmc_model { BmcWorld, BmcWebWorld, BmcWebAccount, BmcPowerOn, bmc_web_world_untouched, BmcScheduledEvent, BmcKvmStreamClosed, BmcKvmIdle, BmcKvmStreaming, BmcKvmClosedByController, - BmcWebLoginAccepted, BmcWebLoginRefused, + BmcWebLoginAccepted, BmcWebLoginRefused, bmc_world, bmc_with_web, bmc_with_pending, bmc_with_sol_session, bmc_web_login, bmc_kvm_viewer_count, bmc_kvm_connect, bmc_web_logout, bmc_advance, } import gunbc.bmc_megarac_web_adapter { @@ -28,18 +28,17 @@ fn web(other_viewers: Int, canvas_readable: Bool) -> BmcWebWorld { } fn world(other_viewers: Int, close_at: Int, canvas_readable: Bool) -> BmcWorld { - BmcWorld { - power: BmcPowerOn, + bmc_with_pending( + world: bmc_with_web(world: bmc_world(power: BmcPowerOn), web: web(other_viewers: other_viewers, canvas_readable: canvas_readable)), pending: if close_at < 0 { [] } else { [BmcScheduledEvent { at: second(count: close_at), event: BmcKvmStreamClosed {} }] }, fired: [], - web: web(other_viewers: other_viewers, canvas_readable: canvas_readable), - } + ) } // A WORLD WITH NO ACCOUNT REFUSES EVERY LOGIN, empty credentials included: absence is a constructor, // not a sentinel a guard has to catch. test fn a_world_without_an_account_refuses_every_login() -> Bool { - let untouched = BmcWorld { power: BmcPowerOn, pending: [], fired: [], web: bmc_web_world_untouched } + let untouched = bmc_world(power: BmcPowerOn) let empty = bmc_web_login(world: untouched, username: "", password: "") let named = bmc_web_login(world: untouched, username: "admin", password: "pw") match empty.reply { BmcWebLoginRefused {} => true _ => false } && match named.reply { BmcWebLoginRefused {} => true _ => false } @@ -118,10 +117,9 @@ test fn another_viewer_holding_the_seat_refuses_the_connect() -> Bool { // FIELD BOUNDARIES SURVIVE: two credential pairs whose space-joined forms are equal are different // requests, and each keeps its own row answered by the model. test fn credentials_that_join_alike_stay_distinct_requests() -> Bool { - let w0 = BmcWorld { - power: BmcPowerOn, pending: [], fired: [], + let w0 = bmc_with_web(world: bmc_world(power: BmcPowerOn), web: BmcWebWorld { account: Present { value: BmcWebAccount { username: "admin", password: "pw secret", privilege: 4 } }, sessions: [], next_session_id: 7, other_kvm_viewers: 0, kvm: BmcKvmIdle {}, canvas_readable: true }, - } + ) let table = megarac_web_transition_table( initial: w0, credentials: [MegaRacWebLogin { username: "admin", password: "pw secret" }, MegaRacWebLogin { username: "admin pw", password: "secret" }], @@ -133,7 +131,7 @@ test fn credentials_that_join_alike_stay_distinct_requests() -> Bool { } // A WORLD'S TABLE KEY IS COMPLETE: two worlds that differ only in their pending schedule, or only in -// which events have fired, are different table states. +// which events have fired, or only in the controller's SOL session, are different table states. test fn world_keys_distinguish_pending_and_fired_events() -> Bool { let a = world(other_viewers: 0, close_at: 3, canvas_readable: true) let b = world(other_viewers: 0, close_at: 5, canvas_readable: true) @@ -142,6 +140,7 @@ test fn world_keys_distinguish_pending_and_fired_events() -> Bool { megarac_web_world_text(world: a) != megarac_web_world_text(world: b) && megarac_web_world_text(world: a) != megarac_web_world_text(world: c) && megarac_web_world_text(world: fired) != megarac_web_world_text(world: c) + && megarac_web_world_text(world: c) != megarac_web_world_text(world: bmc_with_sol_session(world: c, open: true)) } // THE TABLE CARRIES THE ABSOLUTE INSTANT: the only advance row is at the event's own second, and at diff --git a/dag/test/claim/boot_world_models_witness_test.dag b/dag/test/claim/boot_world_models_witness_test.dag new file mode 100644 index 00000000000..b1c5b5357bb --- /dev/null +++ b/dag/test/claim/boot_world_models_witness_test.dag @@ -0,0 +1,109 @@ +module test.claim.boot_world_models_witness_test + +import std.types { Bool, List, String } +import std.measure { second } +import gunbc.bmc_model { BmcWorld, BmcPowerOn, bmc_world, bmc_with_sol_session, bmc_with_sol_drop_after_boot, bmc_chassis_control, bmc_advance, bmc_power_is_on, bmc_sol_drop_fired } +import extdeps.bmc.ipmi_chassis_control { IpmiChassisPowerCycle } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import extdeps.transports.shell { ShellProcessExited } +import extdeps.exec.command { argv_words } +import extdeps.tools.gnu_coreutils { cat_command } +import extdeps.crypto.hash { sha256sum_file_command } +import gunbc.wall_clock_model { ModeledWallClock, wall_clock_unix } +import extdeps.units.iso8601_calendar { iso8601_utc_text } +import gunbc.remote_host_model { ModeledRemoteHost, ModeledRemoteFile, remote_request, remote_answer } +import gunbc.filesystem_model { ModeledFilesystem, ModeledFile, fs_parent, fs_write, fs_list, fs_read } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE MODELS' OWN SEMANTICS, checked apart from any orchestrator run, so a matrix case cannot pass +// against a model that is wrong in the same direction as the code under test. Reference values for the +// calendar are independent: Python's datetime.fromtimestamp(t, timezone.utc) for each instant. +test fn the_wall_clock_renders_utc_like_date() -> Bool { + iso8601_utc_text(unix: 0) == "1970-01-01T00:00:00Z" + && iso8601_utc_text(unix: 951782400) == "2000-02-29T00:00:00Z" + && iso8601_utc_text(unix: 1790000000) == "2026-09-21T14:13:20Z" + && iso8601_utc_text(unix: 4102444799) == "2099-12-31T23:59:59Z" + && iso8601_utc_text(unix: 0 - 1) == "1969-12-31T23:59:59Z" +} + +// A NEGATIVE STEP IS A WALL CLOCK THAT WENT BACKWARDS while virtual time moved forward. +test fn a_backward_step_reads_earlier_while_virtual_time_advances() -> Bool { + let clock = ModeledWallClock { unix_at_origin: 1790000000, step: std.measure.second_displacement(count: 0 - 120) } + wall_clock_unix(clock: clock, now: second(count: 60)) == 1789999940 +} + +// THE FAR SIDE OF AN SSH REQUEST is the word before the first `--` and everything after it, so a +// remote command that itself carries `--` keeps it. +test fn a_remote_request_splits_at_the_first_separator() -> Bool { + match remote_request(client_args: ["-o", "BatchMode=yes", "srv2", "--", "sha256sum", "--", "/srv/x"]) { + Present { value: r } => r.endpoint == "srv2" && r.words == ["sha256sum", "--", "/srv/x"] + Absent => false + } + && match remote_request(client_args: ["srv2", "cat", "/srv/x"]) { Present { value: _ } => false Absent => true } +} + +// THE REMOTE HOST ANSWERS ONLY THE PRODUCTION BUILDERS' WORDS, in coreutils' formats. +test fn the_remote_host_answers_production_commands_in_coreutils_format() -> Bool { + let host = ModeledRemoteHost { endpoint: "srv2", files: [ + ModeledRemoteFile { path: "/srv/rec", content: Present { value: "abc\n" }, sha256: none }, + ModeledRemoteFile { path: "/srv/img", content: Present { value: "bytes" }, sha256: Present { value: "ff00" } }, + ModeledRemoteFile { path: "/srv/gone", content: none, sha256: none }, + ] } + let cat_ok = match remote_answer(host: host, words: argv_words(command: cat_command(path: "/srv/rec"))) { + Present { value: ShellProcessExited { exit_code: 0, stdout: "abc\n", stderr: _ } } => true + _ => false + } + let sum_ok = match remote_answer(host: host, words: argv_words(command: sha256sum_file_command(path: "/srv/img"))) { + Present { value: ShellProcessExited { exit_code: 0, stdout: "ff00 /srv/img\n", stderr: _ } } => true + _ => false + } + let gone = match remote_answer(host: host, words: argv_words(command: cat_command(path: "/srv/gone"))) { + Present { value: ShellProcessExited { exit_code: 1, stdout: _, stderr: "cat: /srv/gone: No such file or directory\n" } } => true + _ => false + } + let unlisted = match remote_answer(host: host, words: ["rm", "-rf", "/srv"]) { Present { value: _ } => false Absent => true } + cat_ok && sum_ok && gone && unlisted +} + +// THE FILESYSTEM'S PARENT RULE: a write under a directory the model does not hold is not_found. +test fn a_write_needs_its_parent_directory() -> Bool { + let fs = ModeledFilesystem { directories: ["/", "/run"], files: [] } + fs_parent(path: "/run/sol.pid") == "/run" && fs_parent(path: "/x") == "/" && fs_parent(path: "target/a.pub") == "target" + && match fs_write(fs: fs, path: "/var/x", content: "1", create_new: false).observation { + extdeps.transports.file.FileOperationFailed { kind: extdeps.filesystem.filesystem_io.FilesystemNotFound, error: _ } => true + _ => false + } +} + +// A POWER RESTORE KEEPS THE SOL DROP IT SCHEDULES (#12423 side-chat review 5342387382). An ON host with +// an open SOL session and a 30-second after-boot drop is power-cycled at t=0: the controller drops power +// and schedules the restore at t=5; the restore boots the host and schedules the drop at t=35. A quiet +// advance to t=10 fires only the restore; ONE quiet advance to t=40, spanning both due times, fires both +// -- the drop the restore scheduled is not discarded -- and leaves nothing pending. +fn cycled_on_host() -> BmcWorld { + let on = bmc_with_sol_drop_after_boot(world: bmc_with_sol_session(world: bmc_world(power: BmcPowerOn), open: true), after: second(count: 30)) + bmc_chassis_control(world: on, action: IpmiChassisPowerCycle, now: second(count: 0)).world +} + +test fn a_power_restore_keeps_the_sol_drop_it_schedules() -> Bool { + let at_ten = bmc_advance(world: cycled_on_host(), now: second(count: 10)) + let at_forty = bmc_advance(world: cycled_on_host(), now: second(count: 40)) + bmc_power_is_on(world: at_ten) && at_ten.sol_session_open && count(at_ten.fired) == 1 && count(at_ten.pending) == 1 + && bmc_power_is_on(world: at_forty) && !at_forty.sol_session_open && bmc_sol_drop_fired(world: at_forty) + && count(at_forty.fired) == 2 && count(at_forty.pending) == 0 +} + +// A READ REPORTS UTF-8 BYTES, NOT CODE POINTS (review 72309): the realization's own file read reports +// content.len(), so the model must too. `é` is one code point and two bytes. +fn read_byte_count(fs: ModeledFilesystem, path: String) -> Int { + match fs_read(fs: fs, path: path) { + extdeps.transports.file.FileOperationSucceeded { byte_count: b, content: _ } => extdeps.transports.file.file_observation_byte_count(bytes: b) + _ => 0 - 1 + } +} + +test fn a_modeled_read_counts_utf8_bytes() -> Bool { + let fs = ModeledFilesystem { directories: ["/", "/t"], files: [ModeledFile { path: "/t/a", content: "é" }, ModeledFile { path: "/t/b", content: "abc" }] } + read_byte_count(fs: fs, path: "/t/a") == 2 && read_byte_count(fs: fs, path: "/t/b") == 3 +} diff --git a/dag/test/claim/machine_intake/megarac_media_convergence_witness_test.dag b/dag/test/claim/machine_intake/megarac_media_convergence_witness_test.dag index d47cb01d8a0..1c9f0164869 100644 --- a/dag/test/claim/machine_intake/megarac_media_convergence_witness_test.dag +++ b/dag/test/claim/machine_intake/megarac_media_convergence_witness_test.dag @@ -2,6 +2,7 @@ module test.claim.machine_intake.megarac_media_convergence_witness_test import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.types { Bool, EpochMs, List, NonEmptyStr, String } +import std.process { ProcessExit, ExitSuccess, ExitFailure } import std.content_hash { ContentHash, content_hash_of_value } import extdeps.bmc.megarac { megarac_firmware_0_32 } import extdeps.provisioning.ubuntu_seeded_install_media { ubuntu_seeded_install_media_image_name, ubuntu_seeded_install_media_name_digest_prefix } @@ -106,7 +107,7 @@ import gunbc.machine_intake_megarac_media_attach { SessionReleaseNotAttempted, } import extdeps.bmc.ipmi_chassis_control { ChassisPowerRead } -import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle { media_attach_text, media_attach_outcome_reason, MediaAttachAttempted, MtCollins1MediaAttachRecord, detach_evidence_text, HandoffMediaAttempted, HandoffConfirmed, HandoffAttemptedUnconfirmed, MediaAttachNotAttempted, StalePowerOffNotNeeded, end_media_is_owed, HandoffMediaWithheldAtRecheck, handoff_media_findings } +import gunbc.machine_intake_mtcollins1_boot_diagnostic_bundle { media_attach_text, media_attach_outcome_reason, MediaAttachAttempted, MtCollins1MediaAttachRecord, detach_evidence_text, HandoffMediaAttempted, HandoffConfirmed, HandoffAttemptedUnconfirmed, MediaAttachNotAttempted, StalePowerOffNotNeeded, end_media_is_owed, HandoffMediaWithheldAtRecheck, handoff_media_findings, MtCollins1HandoffMedia, MtCollins1EndMedia, EndMediaObserved, EndMediaNotTaken, media_loss_after_handoff, outcome_attributing_media_loss } import gunbc.machine_intake_mtcollins1_media_attach { MediaGateReady, MediaGateWithheld, mtcollins1_media_gate, mtcollins1_media_share } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -573,6 +574,38 @@ test fn a_withdrawn_row_after_the_handoff_is_an_affirmed_loss() -> Bool { only_finding_contains(findings: handoff_media_findings(h: HandoffMediaAttempted { before: served_look, handoff: HandoffConfirmed, after: observed(general: mtcollins1_media_general_2026_09_27_morning_as_reported, configurations: "[]") }), pattern: "LOST at or after") } +// A LOSS AFFIRMED AFTER A CONFIRMED HANDOFF IS THE ATTEMPT'S CAUSE (gunbc#12533 finding 4): the +// deadline failure is re-attributed to "media presentation lost at ", the earliest affirming +// look is the phase, and the downstream reason is kept. Controls, each on the same failure: a +// served look, an UNOBSERVED look, and an unconfirmed handoff leave the reason as it was; a success +// stands over an affirmed loss. +data withdrawn_look: MegaRacAttachResult = observed(general: mtcollins1_media_general_2026_09_27_morning_as_reported, configurations: "[]") +data deadline_failure: ProcessExit = ExitFailure { code: 1, reason: "mtcollins1 boot: deadline reached without a host-capture terminal" } + +fn attributed_reason(handoff: MtCollins1HandoffMedia, end: MtCollins1EndMedia) -> String { + match outcome_attributing_media_loss(outcome: deadline_failure, loss: media_loss_after_handoff(handoff: handoff, end: end)) { + ExitFailure { code: _, reason: r } => r + ExitSuccess => "" + } +} + +test fn a_presentation_lost_after_a_confirmed_handoff_is_the_named_cause() -> Bool { + let at_after = attributed_reason(handoff: HandoffMediaAttempted { before: served_look, handoff: HandoffConfirmed, after: withdrawn_look }, end: EndMediaObserved { look: withdrawn_look }) + let at_end = attributed_reason(handoff: HandoffMediaAttempted { before: served_look, handoff: HandoffConfirmed, after: served_look }, end: EndMediaObserved { look: withdrawn_look }) + starts_with(s: at_after, prefix: "mtcollins1 boot: media presentation lost at after-handoff (") + && string_contains(s: at_after, pattern: "deadline reached without a host-capture terminal") + && starts_with(s: at_end, prefix: "mtcollins1 boot: media presentation lost at end-of-attempt (") +} + +test fn an_unaffirmed_look_or_an_unconfirmed_handoff_leaves_the_cause_alone() -> Bool { + let failed = MegaRacAttachResult { outcome: MegaRacSessionRefused { detail: "curl: (7)" }, session_release: SessionReleaseNotAttempted, baseline: none } + let unchanged = "mtcollins1 boot: deadline reached without a host-capture terminal" + attributed_reason(handoff: HandoffMediaAttempted { before: served_look, handoff: HandoffConfirmed, after: served_look }, end: EndMediaObserved { look: served_look }) == unchanged + && attributed_reason(handoff: HandoffMediaAttempted { before: served_look, handoff: HandoffConfirmed, after: failed }, end: EndMediaObserved { look: failed }) == unchanged + && attributed_reason(handoff: HandoffMediaAttempted { before: served_look, handoff: HandoffAttemptedUnconfirmed { reason: "no read-back" }, after: withdrawn_look }, end: EndMediaObserved { look: withdrawn_look }) == unchanged + && (match outcome_attributing_media_loss(outcome: ExitSuccess, loss: media_loss_after_handoff(handoff: HandoffMediaAttempted { before: served_look, handoff: HandoffConfirmed, after: withdrawn_look }, end: EndMediaNotTaken { reason: "x" })) { ExitSuccess => true _ => false }) +} + // THE DISCRIMINATING CONTROL: a failed session with the prior good presentation unchanged is // UNOBSERVED, never LOST. test fn a_failed_look_is_indeterminate_not_lost() -> Bool { diff --git a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag new file mode 100644 index 00000000000..c92e01e71bd --- /dev/null +++ b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag @@ -0,0 +1,533 @@ +module test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.measure { Second, second } +import std.materialization_ladder { Frame, SharedStateFrame } +import std.effect_grant { Read, Write, ServiceOpTree, NamespacePosition, ModeledRealization, LifecycleByConstruction, Grant, Envelope } +import v2.std.operation_argv { InputText, InputTextList } +import v2.std.operation_realization { DispatchRecord, virtual_clock_origin } +import v2.std.witness_evaluation { + WitnessEvaluation, WitnessEvaluationFrame, WitnessReturned, WitnessRefused, WitnessInterrupted, + evaluate_in_witness_frame, witness_diagnostic_rendered_reason, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.bmc_model { BmcWorld, BmcPowerOff, bmc_world, bmc_with_sol_session, bmc_with_sol_drop_after_boot, bmc_sol_drop_fired } +import gunbc.filesystem_model { ModeledFilesystem, ModeledFile } +import gunbc.process_environment_model { ModeledVariable } +import gunbc.remote_host_model { ModeledRemoteHost, ModeledRemoteFile } +import gunbc.wall_clock_model { ModeledWallClock } +import gunbc.megarac_media_model { MegaRacMediaWorld, MegaRacShare, MegaRacImage, MegaRacCdRow, megarac_cleared_cd } +import gunbc.machine_intake_mtcollins1_boot_dry_realization { + MtCollins1BootWorld, ModeledSshAgent, ModeledWorker, ModeledHostConsole, TimedConsoleLine, + mtcollins1_boot_dry_realization, with_media, with_bmc, with_notice_watcher, +} +import v2.std.operation_realization { + OperationRealization, OperationBinding, OperationCall, OperationStep, OperationObserved, OperationWorkerKilled, + DispatchWorkerKilled, +} +import gunbc.machine_intake_mtcollins1_boot_run { + MtCollins1BootAttempt, mtcollins1_boot_wet_on_srv1, mtcollins1_boot_exit_reason, + ActuationNotPoweredOn, ActuationPoweredOn, ActuationCensusEnded, +} +import gunbc.machine_intake_mtcollins1_boot_authorization { mtcollins1_boot_medium, mtcollins1_boot_medium_image_name, MtCollins1CensusMedium } +import gunbc.machine_intake_mtcollins1_census_image { mtcollins1_census_image, Mtcollins1CensusImageDerived } +import gunbc.machine_intake_mtcollins1_census_medium_readback { mtcollins1_census_record_path, mtcollins1_census_medium_served_path } +import gunbc.durable_exclusive_hold_file_store { file_hold_acquire } +import gunbc.machine_intake_mtcollins1_maintenance_hold { boot_run_owner, unit_hold_store_root, mtcollins1_unit_hold_key } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE mtcollins1 BOOT ACCEPTANCE MATRIX (gunbc#12423, operator ruling 2026-09-27). Every case runs THE +// REAL ENTRY -- gunbc.machine_intake_mtcollins1_boot_run mtcollins1_boot_wet_on_srv1, unchanged -- over +// a dry realization of its whole effect demand (gunbc.machine_intake_mtcollins1_boot_dry_realization): +// the one BMC model, its virtual-media subsystem, the worker's filesystem, processes, environment and +// clocks, the SSH agent and srv2. Nothing in the orchestrator is replaced. Each case asserts the ROUTE +// the dispatcher logged -- which effects, in what order, under which hold -- and the typed outcome. +// +// EVIDENCE BOUNDARY, for every case here: the deepest real layer is the orchestration and every +// production decoder above the transport observation; the first substituted layer is the transport +// observation. None of these cases is evidence about what the physical controller, the ipmitool or +// curl clients, the SOL collector process or the host firmware do -- those are the companion transport +// controls and live acceptance -- and every modeled answer is grounded where the corpus retains one +// (extdeps.bmc.ipmitool_observed_output, extdeps.bmc.megarac_observed_output). +data realization_identity: NonEmptyStr = "mtcollins1-boot-matrix" as NonEmptyStr + +data credential_path: String = "/run/bmc-credential" + +data sol_capture_path: String = "/run/sol.capture" + +data sol_pid_path: String = "/run/sol.pid" + +fn matrix_grant(service: String, verb: std.effect_grant.Verb) -> Grant { + Grant { verb: verb, root: NamespacePosition { tree: ServiceOpTree { service: service }, path: [] }, binding: ModeledRealization { realization: realization_identity as String }, lifecycle: LifecycleByConstruction } +} + +// The services the entry's effect demand reaches, each granted to the dry realization for reading and +// writing. An operation of any other service refuses as uncovered. +data matrix_services: List = [ + "diagnostic.ipmi.Tool", "megarac.Media", "Filesystem", "shell.Env", "sleep.Delay", + "gunbc.machine_intake.sol_hold", "shell.Exec", "ssh.Session", "Clock", "linux.Procfs", "shell.Move", +] + +fn matrix_frame(world: MtCollins1BootWorld) -> WitnessEvaluationFrame { + matrix_frame_over(realization: mtcollins1_boot_dry_realization(identity: realization_identity, initial: world, epoch: virtual_clock_origin())) +} + +fn matrix_frame_over(realization: OperationRealization) -> WitnessEvaluationFrame { + WitnessEvaluationFrame { + envelope: Envelope { + frame: Frame { name: "mtcollins1-boot-matrix", kind: SharedStateFrame } + grants: concat(map(matrix_services, s => matrix_grant(service: s, verb: Read)), map(matrix_services, s => matrix_grant(service: s, verb: Write))) + } + rest_fixtures: [] + realization: Present { value: realization } + } +} + +fn run_attempt(world: MtCollins1BootWorld) -> WitnessEvaluation { + evaluate_in_witness_frame(frame: matrix_frame(world: world), subject: fn(_scope) { mtcollins1_boot_wet_on_srv1() }) +} + +// ─── THE HEALTHY WORLD, and the facts it is built from ─────────────────────────────────────────── +fn selected_digest() -> String { + match mtcollins1_boot_medium { + MtCollins1CensusMedium { output_digest: d } => d as String + _ => "" + } +} + +fn healthy_srv2() -> ModeledRemoteHost { + ModeledRemoteHost { endpoint: "srv2", files: match mtcollins1_census_image { + Mtcollins1CensusImageDerived { input: input } => [ + ModeledRemoteFile { path: mtcollins1_census_record_path(input: input) as String, content: Present { value: concat(selected_digest(), "\n") }, sha256: none }, + ModeledRemoteFile { path: mtcollins1_census_medium_served_path(medium: mtcollins1_boot_medium) as String, content: Present { value: "" }, sha256: Present { value: selected_digest() } }, + ] + _ => [] + } } +} + +fn healthy_media() -> MegaRacMediaWorld { + MegaRacMediaWorld { + sessions: [], next_session: 1, + share: MegaRacShare { server: "192.168.1.188", source_path: "/srv/bmc", share_type: "nfs" }, + mount_cd: 1, cd_error_code: 0, + images: [MegaRacImage { image_name: mtcollins1_boot_medium_image_name(medium: mtcollins1_boot_medium) as String, image_index: 5 }], + cd: megarac_cleared_cd(), + ready_after: second(count: 12), + withdraw_at: none, + withdraw_after_ready: none, + } +} + +fn worker_filesystem() -> ModeledFilesystem { + ModeledFilesystem { + directories: ["target", "/", "/run", "/proc", "/var", "/var/lib", "/var/lib/gunbc", unit_hold_store_root as String], + files: [ModeledFile { path: credential_path, content: "secret" }], + } +} + +fn world_with_console(lines: List) -> MtCollins1BootWorld { + with_notice_watcher(capture_path: sol_capture_path, token: "matrix-notice-token", w: MtCollins1BootWorld { + bmc: bmc_world(power: BmcPowerOff), + fs: worker_filesystem(), + environment: [ + ModeledVariable { name: "GUNBC_HOST_RESET_BMC_CREDENTIAL_FILE", value: credential_path }, + ModeledVariable { name: "GUNBC_MTCOLLINS1_SOL_CAPTURE", value: sol_capture_path }, + ModeledVariable { name: "GUNBC_MTCOLLINS1_SOL_PID_FILE", value: sol_pid_path }, + ModeledVariable { name: "GITHUB_RUN_ID", value: "4242" }, + ModeledVariable { name: "SSH_AUTH_SOCK", value: "/run/ssh-agent.sock" }, + ModeledVariable { name: "GITHUB_SHA", value: "0123456789abcdef0123456789abcdef01234567" }, + ], + agent: ModeledSshAgent { socket: "/run/ssh-agent.sock", holds_fleet_key: true }, + remote_hosts: [healthy_srv2()], + clock: ModeledWallClock { unix_at_origin: 1790000000, step: std.measure.second_displacement(count: 0) }, + worker: ModeledWorker { next_pid: 4000, processes: [], uptime_at_origin: 86400 }, + console: ModeledHostConsole { lines: lines, emitted: 0, boot: none }, + media: healthy_media(), + }) +} + +// A census image that boots one socket and completes: the capture test.claim.machine_intake.mtcollins1_boot_run_witness_test +// `clean` shows reaching TerminalAccepted, printed a minute into the boot and closed at four minutes. +data one_socket_census_capture: String = "=====GUNBC-HOST-CAPTURE mtcollins1 attempt=1 begin 2026-09-18T00:00:00Z=====\n----SECTION boot-media----\n----ARGV boot-media: ls -l /dev/disk/by-label; blkid\nLABEL=\"GUNBC_MTC1_CENSUS_2404_3\"\n----EXIT boot-media: 0\n----SECTION nproc----\n----ARGV nproc: nproc\n80\n----EXIT nproc: 0\n----SECTION numa----\n----ARGV numa: cat /sys/devices/system/node/online; numactl -H\n0\navailable: 1 nodes (0)\nnode 0 cpus: 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79\nnode 0 size: 255937 MB\nnode 0 free: 250112 MB\n----EXIT numa: 0\n----SECTION edac-before----\n----ARGV edac-before: (counters)\n== /sys/devices/system/edac/mc/mc0/ce_count == 0\n== /sys/devices/system/edac/mc/mc0/ue_count == 0\n----EXIT edac-before: 0\n----SECTION workload----\n----ARGV workload: (the rendered workload command)\nworkload-bytes=4294967296\nworkload-shm-avail-bytes=8373932032\nworkload-mem-available-bytes=15032385536\nworkload-preflight=fits\nworkload-write-rc=0\nworkload-digest-stable=yes\n----EXIT workload: 0\n----SECTION edac-after----\n----ARGV edac-after: (counters)\n== /sys/devices/system/edac/mc/mc0/ce_count == 0\n== /sys/devices/system/edac/mc/mc0/ue_count == 0\n----EXIT edac-after: 0\n=====GUNBC-HOST-CAPTURE mtcollins1 attempt=1 end 2026-09-18T00:04:00Z=====" + +fn console_of(capture: String, begin_after: Int, end_after: Int) -> List { + map(filter(split(s: capture, delimiter: "\n"), l => l != ""), l => TimedConsoleLine { + after: second(count: if starts_with(s: l, prefix: "=====GUNBC-HOST-CAPTURE mtcollins1 attempt=1 end") { end_after } else { begin_after }), + text: l, + }) +} + +// ─── ROUTE READING ───────────────────────────────────────────────────────────────────────────── +fn operation_name(r: DispatchRecord) -> String { + join([r.invocation.at.service, ".", r.invocation.at.operation], "") +} + +fn record_path(r: DispatchRecord) -> String { + fold(r.invocation.bindings, init: "", f: fn(acc, b) { + if acc != "" { acc } else if b.name == "path" { match b.value { InputText { text: t } => t InputTextList { items: _ } => "" } } else { "" } + }) +} + +fn is_hold_write(r: DispatchRecord) -> Bool { + r.invocation.at.service == "Filesystem" && starts_with(s: r.invocation.at.operation, prefix: "WriteCreateNew") + && starts_with(s: record_path(r: r), prefix: unit_hold_store_root as String) +} + +// The effects that change the controller or start a process against it. +data controller_writes: List = [ + "diagnostic.ipmi.Tool.ChassisPowerControl", "diagnostic.ipmi.Tool.ChassisBootDevWithOptions", + "megarac.Media.StartMedia", "megarac.Media.StopMedia", "diagnostic.ipmi.Tool.SolDeactivate", + "gunbc.machine_intake.sol_hold.ActivateHeld", +] + +fn is_controller_write(r: DispatchRecord) -> Bool { + !all(controller_writes, w => w != operation_name(r: r)) +} + +fn ordinals_where(route: List, keep: fn(DispatchRecord) -> Bool) -> List { + map(filter(route, r => keep(r)), r => r.ordinal) +} + +fn count_named(route: List, name: String) -> Int { + count(filter(route, r => operation_name(r: r) == name)) +} + +// EVERY CONTROLLER WRITE HAPPENS UNDER THE UNIT HOLD: after the hold's first commit and before its +// last (the release). The hold writes are the only WriteCreateNew calls under the hold root. +fn controller_writes_are_under_the_hold(route: List) -> Bool { + let holds = ordinals_where(route: route, keep: is_hold_write) + let writes = ordinals_where(route: route, keep: is_controller_write) + match holds.first() { + Absent => count(writes) == 0 + Present { value: acquired } => match holds.last() { + Absent => false + Present { value: released } => count(holds) >= 2 && all(writes, o => o > acquired && o < released) + } + } +} + +fn first_ordinal(route: List, name: String) -> Int { + match ordinals_where(route: route, keep: fn(r) { operation_name(r: r) == name }).first() { Present { value: o } => o Absent => 0 - 1 } +} + +fn outcome_reason(a: MtCollins1BootAttempt) -> String { + mtcollins1_boot_exit_reason(outcome: a.outcome) +} + +fn census_ended(a: MtCollins1BootAttempt) -> Bool { + match a.stage { + ActuationCensusEnded { selection: _, smpro_power_on: _, smpro_census: _ } => true + _ => false + } +} + +// ─── CASES ─────────────────────────────────────────────────────────────────────────────────────── + +// THE HOST NEVER PRINTS A CENSUS. The attempt goes all the way through -- media converged and ready, +// cdrom override set, power on -- and refuses at the terminal deadline with exactly the outcome the +// real attempt of 2026-09-27 recorded (run 36335369059). Route: the collector is started before any +// other controller write; the media start precedes the boot override, which precedes the one power +// action; every controller write is under the hold; the collector is torn down last. +test fn a_host_that_never_prints_a_census_refuses_at_the_deadline() -> Bool { + match run_attempt(world: world_with_console(lines: [])) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "deadline reached without a host-capture terminal") + && count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") == 1 + && count_named(route: route, name: "gunbc.machine_intake.sol_hold.ActivateHeld") == 1 + && first_ordinal(route: route, name: "gunbc.machine_intake.sol_hold.ActivateHeld") < first_ordinal(route: route, name: "megarac.Media.StartMedia") + && first_ordinal(route: route, name: "megarac.Media.StartMedia") < first_ordinal(route: route, name: "diagnostic.ipmi.Tool.ChassisBootDevWithOptions") + && first_ordinal(route: route, name: "diagnostic.ipmi.Tool.ChassisBootDevWithOptions") < first_ordinal(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") + && controller_writes_are_under_the_hold(route: route) + _ => false + } +} + +// A HEALTHY HOST REPORTS SUCCESS, AND THE TEARDOWN RELEASES ONLY WHAT IT OWNS. The census closes and +// is accepted, and the attempt completes. This case was pinned as a defect -- the collector's pid file +// read as stale after the deactivate -- until #12434 made the release identity-checked and retiring; it +// is now the control that the repair holds. Route: the SOL deactivate, then the hold's ReleaseHeld +// of the recorded instance, then the retirement of its pid file and activation receipt; every +// controller write under the unit hold. +test fn a_healthy_census_completes_and_releases_its_collector() -> Bool { + match run_attempt(world: world_with_console(lines: console_of(capture: one_socket_census_capture, begin_after: 60, end_after: 240))) { + WitnessReturned { value, route } => + census_ended(a: value) + && outcome_reason(a: value) == "ok" + && count_named(route: route, name: "diagnostic.ipmi.Tool.SolDeactivate") == 1 + && first_ordinal(route: route, name: "diagnostic.ipmi.Tool.SolDeactivate") < first_ordinal(route: route, name: "gunbc.machine_intake.sol_hold.ReleaseHeld") + && first_ordinal(route: route, name: "gunbc.machine_intake.sol_hold.ReleaseHeld") < first_ordinal(route: route, name: "Filesystem.Delete") + && count_named(route: route, name: "Filesystem.Delete") == 2 + && controller_writes_are_under_the_hold(route: route) + _ => false + } +} + +// THE SAME UNIT HELD BY ANOTHER RUN. Before this attempt starts, a different run's boot holds the +// unit (acquired through the production file_hold_acquire, into the same store). This attempt is +// refused at the hold with the controller untouched: no controller write of any kind appears in its +// route, and it never starts a SOL collector. +test fn a_second_run_for_a_held_unit_writes_nothing_to_the_controller() -> Bool { + let prior = evaluate_in_witness_frame( + frame: matrix_frame(world: world_with_console(lines: [])), + subject: fn(_scope) { file_hold_acquire(root: unit_hold_store_root, slot_key: mtcollins1_unit_hold_key, requested_owner: boot_run_owner(run_id: "4141" as NonEmptyStr)) } + ) + match prior { + WitnessReturned { state } => match state { + Absent => false + Present { value: held } => match run_attempt(world: held) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "is held by 'mtcollins1-boot:4141'") + && count(filter(route, r => is_controller_write(r: r))) == 0 + && count_named(route: route, name: "gunbc.machine_intake.sol_hold.ActivateHeld") == 0 + _ => false + } + } + _ => false + } +} + +// ─── MEDIA VARIATION ─────────────────────────────────────────────────────────────────────────────── +fn media_varied(media: MegaRacMediaWorld) -> MtCollins1BootWorld { + with_media(w: world_with_console(lines: []), media: media) +} + +fn media_with(images: List, share: MegaRacShare, cd: MegaRacCdRow, ready_after: Int, withdraw_after_ready: Second?) -> MegaRacMediaWorld { + MegaRacMediaWorld { + sessions: [], next_session: 1, share: share, mount_cd: 1, cd_error_code: 0, images: images, cd: cd, + ready_after: second(count: ready_after), withdraw_at: none, withdraw_after_ready: withdraw_after_ready, + } +} + +fn no_withdrawal() -> Second? { + none +} + +fn desired_image() -> String { + mtcollins1_boot_medium_image_name(medium: mtcollins1_boot_medium) as String +} + +data real_share: MegaRacShare = MegaRacShare { server: "192.168.1.188", source_path: "/srv/bmc", share_type: "nfs" } + +fn reached_no_power_action(route: List) -> Bool { + count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") == 0 + && count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisBootDevWithOptions") == 0 +} + +// THE IMAGE IS ALREADY PRESENTED AND READY. Convergence has nothing to do: no stop, no start, and the +// attempt proceeds to the boot exactly as from a fresh attach. +test fn an_already_presented_image_is_not_attached_again() -> Bool { + let presented = MegaRacCdRow { image_name: desired_image(), redirection_status: 1, media_index: 0, session_index: 0, ready_at: none } + match run_attempt(world: media_varied(media: media_with(images: [MegaRacImage { image_name: desired_image(), image_index: 5 }], share: real_share, cd: presented, ready_after: 12, withdraw_after_ready: no_withdrawal()))) { + WitnessReturned { value, route } => + count_named(route: route, name: "megarac.Media.StartMedia") == 0 + && count_named(route: route, name: "megarac.Media.StopMedia") == 0 + && count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") == 1 + && controller_writes_are_under_the_hold(route: route) + _ => false + } +} + +// READINESS SLOWER THAN THE WAIT. The controller keeps the row connecting past the readiness budget; +// the attempt refuses without setting the boot override or touching power. +test fn media_that_never_becomes_ready_refuses_before_any_power_action() -> Bool { + match run_attempt(world: media_varied(media: media_with(images: [MegaRacImage { image_name: desired_image(), image_index: 5 }], share: real_share, cd: megarac_cleared_cd(), ready_after: 600, withdraw_after_ready: no_withdrawal()))) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "did not reach Started with a bound session") + && string_contains(s: outcome_reason(a: value), pattern: "No boot-device or power handoff was made") + && count_named(route: route, name: "megarac.Media.StartMedia") == 1 + && reached_no_power_action(route: route) + _ => false + } +} + +// THE SAME FILENAME ON THE WRONG SHARE. The listing offers an image with the desired name, but the +// controller's CD share is bound to another server. It refuses before any power action; a start, if +// one is issued, must not be followed by the boot. +test fn the_right_filename_on_the_wrong_share_refuses_before_any_power_action() -> Bool { + let wrong = MegaRacShare { server: "192.168.1.99", source_path: "/srv/bmc", share_type: "nfs" } + match run_attempt(world: media_varied(media: media_with(images: [MegaRacImage { image_name: desired_image(), image_index: 5 }], share: wrong, cd: megarac_cleared_cd(), ready_after: 12, withdraw_after_ready: no_withdrawal()))) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "remote-media share is not this unit's boot share") + && string_contains(s: outcome_reason(a: value), pattern: "observed 192.168.1.99:/srv/bmc") + && count_named(route: route, name: "megarac.Media.StartMedia") == 0 + && reached_no_power_action(route: route) + _ => false + } +} + +// THE LISTING NAMES THE IMAGE TWICE. Taking either row would let the controller's order choose which +// file is attached, so nothing is started and nothing is powered. +test fn a_listing_that_names_the_image_twice_starts_nothing() -> Bool { + let twice = [MegaRacImage { image_name: desired_image(), image_index: 5 }, MegaRacImage { image_name: desired_image(), image_index: 6 }] + match run_attempt(world: media_varied(media: media_with(images: twice, share: real_share, cd: megarac_cleared_cd(), ready_after: 12, withdraw_after_ready: no_withdrawal()))) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "names the image more than once, so its index is ambiguous") + && count_named(route: route, name: "megarac.Media.StartMedia") == 0 + && reached_no_power_action(route: route) + _ => false + } +} + +// THE PRESENTATION IS LOST FIVE SECONDS AFTER IT BECAME READY: after the attach saw it ready and before +// the handoff. Measured window: a loss 3 to 8 seconds after readiness falls here; 1 second falls between +// two readiness looks (the attach never sees it ready), and 12 seconds or more falls after the handoff. +// The pre-handoff re-observation must see it gone and refuse without the boot override or power. +test fn a_presentation_lost_after_readiness_stops_the_handoff() -> Bool { + match run_attempt(world: media_varied(media: media_with(images: [MegaRacImage { image_name: desired_image(), image_index: 5 }], share: real_share, cd: megarac_cleared_cd(), ready_after: 12, withdraw_after_ready: Present { value: second(count: 5) }))) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "pre-handoff recheck did not admit it") + && count_named(route: route, name: "megarac.Media.StartMedia") == 1 + && reached_no_power_action(route: route) + _ => false + } +} + +// A PRESENTATION LOST AFTER THE HANDOFF IS THE NAMED CAUSE (finding 4, repaired in #12554). Lost +// twenty seconds after readiness -- after the boot override and the power action -- the watch still +// reaches its deadline, but a post-handoff look (after-handoff, or end-of-attempt when the handoff +// finished before the withdrawal) affirmed the loss, so the outcome names it and keeps the deadline +// beside it; which look sees it is the unit witnesses' subject, not this case's (#12423 media: presentation withdrawal). The red is the bare deadline. +test fn a_presentation_lost_after_the_handoff_is_the_reported_cause() -> Bool { + match run_attempt(world: media_varied(media: media_with(images: [MegaRacImage { image_name: desired_image(), image_index: 5 }], share: real_share, cd: megarac_cleared_cd(), ready_after: 12, withdraw_after_ready: Present { value: second(count: 20) }))) { + WitnessReturned { value, route } => + (string_contains(s: outcome_reason(a: value), pattern: "media presentation lost at after-handoff (") + || string_contains(s: outcome_reason(a: value), pattern: "media presentation lost at end-of-attempt (")) + && string_contains(s: outcome_reason(a: value), pattern: "deadline reached without a host-capture terminal") + && count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") == 1 + _ => false + } +} + +// ─── OBSERVATION FAILURES ───────────────────────────────────────────────────────────────────────── + +// ANOTHER CLIENT ALREADY HOLDS THE SOL SESSION. The collector starts and exits at once with the +// controller's refusal on its stderr, and the attempt refuses with that typed cause -- read from the +// client diagnostics, never the host capture -- before any other controller write, and without +// deactivating a session this hold did not establish. +test fn a_sol_session_held_elsewhere_refuses_before_the_attach() -> Bool { + let w = world_with_console(lines: []) + match run_attempt(world: with_bmc(w: w, bmc: bmc_with_sol_session(world: w.bmc, open: true))) { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "SOL collector not established: the SOL payload is already active on another session") + && count_named(route: route, name: "megarac.Media.StartMedia") == 0 + && count_named(route: route, name: "diagnostic.ipmi.Tool.SolDeactivate") == 0 + && reached_no_power_action(route: route) + _ => false + } +} + +// SOL IS LOST THIRTY SECONDS AFTER THE HOST STARTS BOOTING WHILE MANAGEMENT KEEPS ANSWERING, and the +// census would have printed at sixty. The drop is armed by the host's own boot in the model, so it +// follows the route's real power-on. The loss is reported when it is observed, not at the terminal +// deadline (#12423): a typed ObservationChannelLost, the incident frozen, the BMC shown answering, and +// the teardown within sixty seconds of the power action -- before the census could have printed. This +// case was pinned as reporting the loss only at the deadline until #12434's watch detected it. The final +// world shows the drop fired, so the case is not green on a run where the loss never happened. +fn sol_drop_fired_in(w: MtCollins1BootWorld) -> Bool { + bmc_sol_drop_fired(world: w.bmc) +} + +fn first_dispatch_second(route: List, name: String) -> Int? { + match filter(route, r => operation_name(r: r) == name).first() { Present { value: r } => Present { value: std.measure.second_count(s: r.dispatched_at) as Int } Absent => none } +} + +// The teardown's delay after the power action, required to exist on both ends -- an absent deactivate +// or power action is not a zero -- and to be nonnegative and at most `bound` seconds (review of #12533 +// at bd99cbb489: a -1 sentinel let an absent or early teardown pass). +fn teardown_within(route: List, bound: Int) -> Bool { + match first_dispatch_second(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") { + Absent => false + Present { value: power } => match first_dispatch_second(route: route, name: "diagnostic.ipmi.Tool.SolDeactivate") { + Absent => false + Present { value: torn } => torn - power >= 0 && torn - power <= bound + } + } +} + +test fn a_sol_loss_mid_boot_is_reported_before_the_deadline() -> Bool { + let w = world_with_console(lines: console_of(capture: one_socket_census_capture, begin_after: 60, end_after: 240)) + let dropping = with_bmc(w: w, bmc: bmc_with_sol_drop_after_boot(world: w.bmc, after: second(count: 30))) + match evaluate_in_witness_frame(frame: matrix_frame(world: dropping), subject: fn(_scope) { mtcollins1_boot_wet_on_srv1() }) { + WitnessReturned { value, route, state } => + string_contains(s: outcome_reason(a: value), pattern: "ObservationChannelLost while the boot was being watched") + && string_contains(s: outcome_reason(a: value), pattern: "incident frozen to /run/sol.capture.loss") + && string_contains(s: outcome_reason(a: value), pattern: "BMC answered mc info") + && count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") == 1 + && count_named(route: route, name: "diagnostic.ipmi.Tool.SolDeactivate") == 1 + && first_ordinal(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") < first_ordinal(route: route, name: "diagnostic.ipmi.Tool.SolDeactivate") + && teardown_within(route: route, bound: 60) + && match state { Present { value: end } => sol_drop_fired_in(w: end) Absent => false } + _ => false + } +} + +// ─── RESOURCE VARIATION ─────────────────────────────────────────────────────────────────────────── + +// TWO SOCKETS ANSWER. The census reports 160 CPUs over two NUMA nodes; the declared expectation for +// this unit is one socket and 80 CPUs, so the terminal verdict refuses on topology and reports what it +// observed -- the thread count and the per-node placement -- rather than a transport failure. The +// refused terminal is reported at the powered-on stage, not as a census that ended. +data two_socket_census_capture: String = "=====GUNBC-HOST-CAPTURE mtcollins1 attempt=1 begin 2026-09-18T00:00:00Z=====\n----SECTION boot-media----\n----ARGV boot-media: ls -l /dev/disk/by-label; blkid\nLABEL=\"GUNBC_MTC1_CENSUS_2404_3\"\n----EXIT boot-media: 0\n----SECTION nproc----\n----ARGV nproc: nproc\n160\n----EXIT nproc: 0\n----SECTION numa----\n----ARGV numa: cat /sys/devices/system/node/online; numactl -H\n0-1\navailable: 2 nodes (0-1)\nnode 0 cpus: 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79\nnode 1 cpus: 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159\n----EXIT numa: 0\n----SECTION edac-before----\n----ARGV edac-before: (counters)\n== /sys/devices/system/edac/mc/mc0/ce_count == 0\n== /sys/devices/system/edac/mc/mc0/ue_count == 0\n----EXIT edac-before: 0\n----SECTION workload----\n----ARGV workload: (the rendered workload command)\nworkload-bytes=4294967296\nworkload-shm-avail-bytes=8373932032\nworkload-mem-available-bytes=15032385536\nworkload-preflight=fits\nworkload-write-rc=0\nworkload-digest-stable=yes\n----EXIT workload: 0\n----SECTION edac-after----\n----ARGV edac-after: (counters)\n== /sys/devices/system/edac/mc/mc0/ce_count == 0\n== /sys/devices/system/edac/mc/mc0/ue_count == 0\n----EXIT edac-after: 0\n=====GUNBC-HOST-CAPTURE mtcollins1 attempt=1 end 2026-09-18T00:04:00Z=====" + +test fn a_two_socket_answer_is_a_truthful_topology_refusal() -> Bool { + match run_attempt(world: world_with_console(lines: console_of(capture: two_socket_census_capture, begin_after: 60, end_after: 240))) { + WitnessReturned { value, route } => + !census_ended(a: value) + && string_contains(s: outcome_reason(a: value), pattern: "nproc observed 160, qualification expects 80") + && string_contains(s: outcome_reason(a: value), pattern: "node 0=80, node 1=80") + && count_named(route: route, name: "diagnostic.ipmi.Tool.ChassisPowerControl") == 1 + _ => false + } +} + +// ─── INTERRUPTION ───────────────────────────────────────────────────────────────────────────────── + +// THE WORKER DIES RIGHT AFTER THE START-MEDIA WRITE COMMITS, before its reply. The realization is the +// matrix's own with that one handler wrapped: the controller takes the start, and the worker is gone. +fn killed_after_start_media(realization: OperationRealization) -> OperationRealization { + OperationRealization { + identity: realization.identity, initial: realization.initial, epoch: realization.epoch, advance: realization.advance, + bindings: map(realization.bindings, b => if b.at.operation == "StartMedia" { + OperationBinding { at: b.at, handler: fn(state, call) { + let inner = b.handler + match inner(state, call) { + OperationObserved { observation: _, state: after, elapsed: _ } => OperationWorkerKilled { committed: true, state: after } + other => other + } + } } + } else { b }), + } +} + +fn as_another_run(w: MtCollins1BootWorld, run_id: String) -> MtCollins1BootWorld { + let env = map(w.environment, v => if v.name == "GITHUB_RUN_ID" { ModeledVariable { name: v.name, value: run_id } } else { v }) + MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: env, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media } +} + +// PINNED: THE NEXT ATTEMPT IS LOCKED OUT BY THE DEAD RUN'S HOLD. The interrupted run never released the +// unit, so a new run finds it held by the dead one and refuses with the controller untouched -- safe, +// but it cannot reconcile: nothing retires a hold whose owner is gone, so every later attempt refuses +// until an operator intervenes (#12423: interrupted operations must be reconciled without undocumented +// preparation). When dead-owner reconciliation lands this case flips. +test fn pinned_an_interrupted_attempt_locks_out_the_next_one() -> Bool { + let realization = killed_after_start_media(realization: mtcollins1_boot_dry_realization(identity: realization_identity, initial: world_with_console(lines: []), epoch: virtual_clock_origin())) + match evaluate_in_witness_frame(frame: matrix_frame_over(realization: realization), subject: fn(_scope) { mtcollins1_boot_wet_on_srv1() }) { + WitnessInterrupted { at, state, now: interrupted_clock } => { + let next = as_another_run(w: state, run_id: "4243") + let resumed = evaluate_in_witness_frame( + frame: matrix_frame_over(realization: mtcollins1_boot_dry_realization(identity: realization_identity, initial: next, epoch: interrupted_clock)), + subject: fn(_scope) { mtcollins1_boot_wet_on_srv1() } + ) + at.invocation.at.operation == "StartMedia" + && match at.outcome { DispatchWorkerKilled { committed: c } => c _ => false } + && match resumed { + WitnessReturned { value, route } => + string_contains(s: outcome_reason(a: value), pattern: "is held by 'mtcollins1-boot:4242'") + && count(filter(route, r => is_controller_write(r: r))) == 0 + _ => false + } + } + _ => false + } +} diff --git a/dag/test/claim/modeled_filesystem_witness_test.dag b/dag/test/claim/modeled_filesystem_witness_test.dag new file mode 100644 index 00000000000..346e733645a --- /dev/null +++ b/dag/test/claim/modeled_filesystem_witness_test.dag @@ -0,0 +1,191 @@ +module test.claim.modeled_filesystem_witness_test + +import std.types { Bool, List, NonEmptyStr, String } +import std.materialization_ladder { Frame, SharedStateFrame } +import std.effect_grant { + Read, Write, ServiceOpTree, NamespacePosition, + ModeledRealization, LifecycleByConstruction, Grant, Envelope, +} +import v2.std.operation_realization { + OperationRealization, OperationBinding, OperationCall, OperationStep, DispatchRecord, + OperationObserved, ShellObserved, DispatchObserved, + virtual_clock_origin, +} +import v2.std.witness_evaluation { + WitnessEvaluationFrame, WitnessReturned, WitnessRefused, WitnessInterrupted, + evaluate_in_witness_frame, witness_diagnostic_rendered_reason, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.measure { second } +import extdeps.transports.shell { ShellProcessExited } +import extdeps.filesystem.filesystem_io { + Filesystem, FilesystemFailureKindAdmitted, FilesystemAlreadyExists, admit_filesystem_failure_kind, +} +import gunbc.durable_exclusive_hold_file_store { + file_hold_acquire, FileHoldAcquired, FileHoldOccupied, +} +import gunbc.machine_intake_mtcollins1_maintenance_hold { boot_run_owner } +import gunbc.filesystem_model { + ModeledFilesystem, ModeledFile, filesystem_bindings, filesystem_operation, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE FILE ARM OF THE MODELED OPERATION REALIZATION, exercised through the real dispatcher and the +// production durable-hold store. Every subject calls production code -- file_hold_acquire runs the +// real compare-and-set fold (gunbc.durable_cas_file_store), which lists, reads and create-exclusively +// writes its slot through extdeps.filesystem.filesystem_io -- and the model answers only the file +// operations. The hold root is an ordinary path inside the modeled filesystem, so nothing touches +// /var/lib on the host running the witness. +data realization_identity: NonEmptyStr = "modeled-filesystem-witness" as NonEmptyStr + +data hold_root: NonEmptyStr = "/var/lib/gunbc/unit-holds" as NonEmptyStr + +data hold_key: NonEmptyStr = "operator-host-mtcollins1" as NonEmptyStr + +fn filesystem_grant(verb: std.effect_grant.Verb) -> Grant { + Grant { + verb: verb + root: NamespacePosition { tree: ServiceOpTree { service: "Filesystem" }, path: [] } + binding: ModeledRealization { realization: realization_identity as String } + lifecycle: LifecycleByConstruction + } +} + +fn filesystem_frame(initial: ModeledFilesystem) -> WitnessEvaluationFrame { + WitnessEvaluationFrame { + envelope: Envelope { + frame: Frame { name: "modeled-filesystem-witness", kind: SharedStateFrame } + grants: [filesystem_grant(verb: Read), filesystem_grant(verb: Write)] + } + rest_fixtures: [] + realization: Present { value: OperationRealization { + identity: realization_identity, + initial: initial, + epoch: virtual_clock_origin(), + bindings: filesystem_bindings(get: fn(fs) { fs }, put: fn(fs, next) { next }), + advance: fn(fs, now) { fs }, + } } + } +} + +fn empty_hold_store() -> ModeledFilesystem { + ModeledFilesystem { directories: ["/", "/var", "/var/lib", "/var/lib/gunbc", hold_root as String], files: [] } +} + +fn route_operations(route: List) -> List { + map(route, r => r.invocation.at.operation) +} + +fn acquired(o: gunbc.durable_exclusive_hold_file_store.FileHoldAcquireOutcome) -> Bool { + match o { + FileHoldAcquired { slot_key: _, owner: _, generation: _ } => true + _ => false + } +} + +fn occupied_by(o: gunbc.durable_exclusive_hold_file_store.FileHoldAcquireOutcome, owner: String) -> Bool { + match o { + FileHoldOccupied { slot_key: _, holder: h, generation: _ } => (h as String) == owner + _ => false + } +} + +// THE REAL COMPARE-AND-SET, TWO CONTENDERS FOR ONE UNIT. The first acquire commits into the empty +// store; the second, a different run for the SAME key in the SAME store, finds the committed slot and +// is refused as occupied by the first run. Both go through file_hold_acquire unchanged, so the verdict +// is the production fold's reading of what the model's filesystem holds, and the route shows the +// second contender never wrote. +test fn two_contenders_for_one_unit_get_one_hold() -> Bool { + let first_owner = boot_run_owner(run_id: "run-a" as NonEmptyStr) + let second_owner = boot_run_owner(run_id: "run-b" as NonEmptyStr) + let result = evaluate_in_witness_frame( + frame: filesystem_frame(initial: empty_hold_store()), + subject: fn(_scope) { + let first = file_hold_acquire(root: hold_root, slot_key: hold_key, requested_owner: first_owner) + let second = file_hold_acquire(root: hold_root, slot_key: hold_key, requested_owner: second_owner) + acquired(o: first) && occupied_by(o: second, owner: first_owner as String) + } + ) + match result { + WitnessReturned { value, route, state } => + value + && count(filter(route, r => r.invocation.at.service == "Filesystem")) == count(route) + && count(filter(route, r => starts_with(s: r.invocation.at.operation, prefix: "WriteCreateNew"))) == 1 + && match state { Present { value: fs } => store_holds_one_slot(fs: fs) Absent => false } + _ => false + } +} + +fn store_holds_one_slot(fs: ModeledFilesystem) -> Bool { + count(filter(fs.files, f => starts_with(s: f.path, prefix: hold_root as String))) == 1 +} + +// THE FAILURE KIND TRAVELS THE REAL CHANNEL. A create-exclusive write to an existing path answers +// already_exists, and the operation's declared error_kind field, read by the production admission +// admit_filesystem_failure_kind, decodes it to FilesystemAlreadyExists -- the same projection a host +// io::Error reaches. +test fn a_create_exclusive_write_over_an_existing_file_is_already_exists() -> Bool { + let seeded = ModeledFilesystem { directories: ["/", "/tmp"], files: [ModeledFile { path: "/tmp/slot", content: "held" }] } + match evaluate_in_witness_frame( + frame: filesystem_frame(initial: seeded), + subject: fn(_scope) { + let w = Filesystem.WriteCreateNew(path: "/tmp/slot", content: "mine") + !w.success && match admit_filesystem_failure_kind(observed: w.error_kind) { + FilesystemFailureKindAdmitted { kind: k } => match k { FilesystemAlreadyExists => true _ => false } + _ => false + } + } + ) { + WitnessReturned { value, state } => value && match state { Present { value: fs } => untouched(fs: fs) Absent => false } + _ => false + } +} + +fn untouched(fs: ModeledFilesystem) -> Bool { + all(fs.files, f => f.content == "held") +} + +// A LISTING IS THE REALIZATION'S OWN CONTRACT: immediate children, sorted, one per line, files and +// directories alike; a file listed as a directory is not_a_directory. +test fn a_listing_is_sorted_immediate_children() -> Bool { + let fs = ModeledFilesystem { + directories: ["/", "/d", "/d/sub", "/d/sub/deeper"], + files: [ModeledFile { path: "/d/b", content: "" }, ModeledFile { path: "/d/a", content: "" }, ModeledFile { path: "/d/sub/c", content: "" }], + } + match evaluate_in_witness_frame( + frame: filesystem_frame(initial: fs), + subject: fn(_scope) { + let listed = Filesystem.List(path: "/d") + let as_dir = Filesystem.List(path: "/d/a") + listed.success && listed.entries == "a\nb\nsub" && !as_dir.success && as_dir.error_kind == "not_a_directory" + } + ) { + WitnessReturned { value } => value + _ => false + } +} + +// AN OBSERVATION OF THE WRONG TRANSPORT IS A HARNESS FAULT: a file operation answered with a shell +// observation refuses rather than being read through either projection. +test fn a_file_operation_answered_as_a_shell_run_refuses() -> Bool { + let realization = OperationRealization { + identity: realization_identity, + initial: empty_hold_store(), + epoch: virtual_clock_origin(), + bindings: [OperationBinding { + at: filesystem_operation(operation: "Read"), + handler: fn(s, c) { OperationObserved { observation: ShellObserved { observation: ShellProcessExited { exit_code: 0, stdout: "x", stderr: "" } }, state: s, elapsed: second(count: 0) } }, + }], + advance: fn(s, now) { s }, + } + let frame = filesystem_frame(initial: empty_hold_store()) + match evaluate_in_witness_frame( + frame: WitnessEvaluationFrame { envelope: frame.envelope, rest_fixtures: [], realization: Present { value: realization } }, + subject: fn(_scope) { Filesystem.Read(path: "/x").success } + ) { + WitnessRefused { diagnostic } => + string_contains(s: witness_diagnostic_rendered_reason(diagnostic: diagnostic), pattern: "needs FileObserved") + _ => false + } +} diff --git a/dag/test/claim/operation_realization_witness_test.dag b/dag/test/claim/operation_realization_witness_test.dag index a90f4f4cc7d..e0208ee85b4 100644 --- a/dag/test/claim/operation_realization_witness_test.dag +++ b/dag/test/claim/operation_realization_witness_test.dag @@ -30,7 +30,8 @@ import extdeps.bmc.ipmi_chassis_control { } import gunbc.machine_intake_oob_boot_handoff { read_chassis_power } import gunbc.bmc_model { - BmcWorld, BmcPowerOn, BmcPowerOff, BmcScheduledEvent, BmcAcPowerLost, bmc_power_is_on, bmc_web_world_untouched, + BmcWorld, BmcPowerOn, BmcPowerOff, BmcScheduledEvent, BmcAcPowerLost, bmc_power_is_on, + bmc_world, bmc_with_pending, bmc_with_power, } import gunbc.bmc_dry_realization { bmc_dry_realization, bmc_ipmi_operation, bmc_chassis_power_control_handler, @@ -71,7 +72,7 @@ fn modeled_frame(realization: OperationRealization) -> WitnessEvaluati } fn world(power_on: Bool) -> BmcWorld { - BmcWorld { power: if power_on { BmcPowerOn } else { BmcPowerOff }, pending: [], fired: [], web: bmc_web_world_untouched } + bmc_world(power: if power_on { BmcPowerOn } else { BmcPowerOff }) } fn read_power() -> ChassisPowerObservation { @@ -202,7 +203,7 @@ fn loss_fired_and_none_pending(w: BmcWorld) -> Bool { // (t 0 -> 1), sleeps five seconds through the production sleep helper (t 1 -> 6), and reads again. The // loss fired during the sleep with no operation issued at t=3, and the second read observes it. test fn a_scheduled_event_fires_during_a_quiet_wait() -> Bool { - let initial = BmcWorld { power: BmcPowerOn, pending: [BmcScheduledEvent { at: second(count: 3), event: BmcAcPowerLost {} }], fired: [], web: bmc_web_world_untouched } + let initial = bmc_with_pending(world: bmc_world(power: BmcPowerOn), pending: [BmcScheduledEvent { at: second(count: 3), event: BmcAcPowerLost {} }], fired: []) let result = evaluate_in_witness_frame( frame: modeled_frame(realization: bmc_dry_realization(identity: realization_identity, initial: initial, epoch: virtual_clock_origin())), subject: fn(_scope) { @@ -307,7 +308,7 @@ test fn a_binding_to_an_undeclared_identity_refuses_before_the_subject_runs() -> // witness is the supervisor: it resumes a SECOND attempt from that world in a new frame, and the // resumed attempt reads before it writes and finds the host already on. fn killed_after_power_on(state: BmcWorld, call: OperationCall) -> OperationStep { - OperationWorkerKilled { committed: true, state: BmcWorld { power: BmcPowerOn, pending: state.pending, fired: state.fired, web: state.web } } + OperationWorkerKilled { committed: true, state: bmc_with_power(world: state, power: BmcPowerOn) } } test fn a_killed_worker_is_interrupted_and_a_resumed_attempt_reconciles() -> Bool { @@ -523,7 +524,7 @@ test fn frames_are_independent_after_the_outer_scope_ends() -> Bool { // fires) and reads off, exactly as the uninterrupted history does. Had the resume restarted at the // origin its reads would complete at 1 and the loss would not yet have fired. fn loss_at_five() -> BmcWorld { - BmcWorld { power: BmcPowerOn, pending: [BmcScheduledEvent { at: second(count: 5), event: BmcAcPowerLost {} }], fired: [], web: bmc_web_world_untouched } + bmc_with_pending(world: bmc_world(power: BmcPowerOn), pending: [BmcScheduledEvent { at: second(count: 5), event: BmcAcPowerLost {} }], fired: []) } fn killed_without_commit(state: BmcWorld, call: OperationCall) -> OperationStep { diff --git a/dag/test/claim/roadmap/roadmap_launch_deployment_observe_witness_test.dag b/dag/test/claim/roadmap/roadmap_launch_deployment_observe_witness_test.dag index 667ba51f198..5ceaf860afe 100644 --- a/dag/test/claim/roadmap/roadmap_launch_deployment_observe_witness_test.dag +++ b/dag/test/claim/roadmap/roadmap_launch_deployment_observe_witness_test.dag @@ -29,6 +29,7 @@ test fn witness_iso8601_utc_epoch_seconds_matches_known_instants() -> Bool { && (match iso8601_utc_epoch_seconds(text: "2026-02-30T00:00:00Z") { Present { value: _ } => false Absent => true }) && (match iso8601_utc_epoch_seconds(text: "2027-04-31T00:00:00Z") { Present { value: _ } => false Absent => true }) && (match iso8601_utc_epoch_seconds(text: "2024-02-29T00:00:00Z") { Present { value: s } => second_count(s) == 1709164800 Absent => false }) + && (match iso8601_utc_epoch_seconds(text: iso8601_utc_text(unix: 4102444799)) { Present { value: s } => second_count(s) == 4102444799 Absent => false }) } // (2) Freshness: fresh within the cadence bound, stale beyond it, refused before the deploy, and diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 480da2c3c00..3171a24f547 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -342,6 +342,10 @@ new-witness eval-step cost gate over the one roadmap page claim that derives the new-witness eval-step cost gate over the ten interpreted P-256 and P-384 point and group-law checks and SHA-384 FIPS vectors of the App Attest path: they still execute, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: the P-384 and SHA-384 primitives executing as natively emitted code rather than as interpreted bignat and Word64 folds). Population: test.claim.p384_dag_ecdsa_witness_test.the_p384_base_point_is_on_the_curve: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by merge-queue required floor run 35678328407 (gunbc#11981), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, wall under 2000ms, over the new-witness eval-step budget: the billed work is interpreted 384-bit field arithmetic (16 limbs) or a SHA-384 block over Word64 pairs, test.claim.p384_dag_ecdsa_witness_test.a_point_beside_the_base_point_is_off_the_curve: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by merge-queue required floor run 35678328407 (gunbc#11981), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, wall under 2000ms, over the new-witness eval-step budget: the billed work is interpreted 384-bit field arithmetic (16 limbs) or a SHA-384 block over Word64 pairs, test.claim.p384_dag_ecdsa_witness_test.a_point_with_a_coordinate_at_p_is_not_admitted: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by merge-queue required floor run 35678328407 (gunbc#11981), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, wall under 2000ms, over the new-witness eval-step budget: the billed work is interpreted 384-bit field arithmetic (16 limbs) or a SHA-384 block over Word64 pairs, test.claim.p384_dag_ecdsa_witness_test.apples_ca_and_root_keys_are_on_p384: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by merge-queue required floor run 35678328407 (gunbc#11981), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, wall under 2000ms, over the new-witness eval-step budget: the billed work is interpreted 384-bit field arithmetic (16 limbs) or a SHA-384 block over Word64 pairs, test.claim.sha384_fips_witness_test.sha384_of_the_empty_message_is_the_published_value_and_one_octet_discriminates: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by required floor run 35703555837 (gunbc#11981, head 0b0a2dffe), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, over the new-witness eval-step budget and above the per-subject line. The standing figure is whatever this identity's row reads in the artifact named above, never a number copied into this field. The billed work is two single-block SHA-384 compressions, the published empty message and a one-octet message on an interpreter that reifies no machine width; the published positive and its discriminating mutation are one subject, so the cost is caused by the claim's own boundary and not by neighbouring vectors, test.claim.sha384_fips_witness_test.sha384_of_abc_is_the_published_value_and_one_octet_discriminates: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by required floor run 35703555837 (gunbc#11981, head 0b0a2dffe), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, over the new-witness eval-step budget and above the per-subject line. The standing figure is whatever this identity's row reads in the artifact named above, never a number copied into this field. The billed work is two single-block SHA-384 compressions, the published abc vector and abd on an interpreter that reifies no machine width; the published positive and its discriminating mutation are one subject, so the cost is caused by the claim's own boundary and not by neighbouring vectors, test.claim.sha384_fips_witness_test.sha384_of_the_896_bit_message_is_the_published_two_block_value_and_one_octet_discriminates: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by required floor run 35703555837 (gunbc#11981, head 0b0a2dffe), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, over the new-witness eval-step budget and above the per-subject line. The standing figure is whatever this identity's row reads in the artifact named above, never a number copied into this field. The billed work is four SHA-384 block compressions, the published 896-bit two-block vector and a last-block mutation on an interpreter that reifies no machine width; the published positive and its discriminating mutation are one subject, so the cost is caused by the claim's own boundary and not by neighbouring vectors, test.claim.p256_dag_ecdsa_witness_test.the_base_point_is_on_the_curve: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by required floor run 35708011844 (gunbc#11981), artifact required-ci-measurement-receipt; planned_as_changed_witness, verdict pass, well inside the wall deadline and over the new-witness eval-step budget. The billed work is one P-256 curve equation over the published base point as 11-limb bignat folds on an interpreter that reifies no machine width. It is a MEMBER BECAUSE IT WAS SPLIT OUT of a claim that also asserted n*G = infinity: that conjunction crossed the 8000ms wall deadline and was INTERRUPTED BEFORE ANY VERDICT, so both facts were being lost; the scalar multiplication left the floor for the native row the frontier names, and this cheap half now reaches a verdict. The standing figure is whatever this identity's row reads in the artifact named above, never a number copied into this field, test.claim.p384_dag_ecdsa_witness_test.doubling_and_adding_the_base_point_stay_on_the_curve: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by claim_batch --hermetic [witness] receipt on session/nimble-eagle-216-step3 (added for review 69917 after run 35678328407): verdict pass, wall under the 8 s deadline, over the new-witness eval-step budget; the billed work is one Jacobian doubling, one addition and two projective curve-equation checks at 16 limbs, test.claim.p384_dag_ecdsa_witness_test.doubling_an_off_curve_point_stays_off_the_curve: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_interpreted_crypto_rows; measured by claim_batch --hermetic [witness] receipt on session/nimble-eagle-216-step3 (added for review 69917 after run 35678328407): verdict pass, wall under the 8 s deadline, over the new-witness eval-step budget; the billed work is one Jacobian doubling and one projective curve-equation check at 16 limbs. Restored when: THE CAPABILITY: gunbc test //gunbc/instruments:native-crypto-vectors EXECUTING ON THE MERGE PATH, i.e. as a phase of a required lane whose red blocks a merge, running these ten identities natively (its cases p256_the_base_point_is_on_the_curve, p384_the_base_point_is_on_the_curve, p384_red_a_point_beside_the_base_point_is_off_the_curve, p384_red_a_point_with_a_coordinate_at_p_is_not_admitted, p384_doubling_and_adding_the_base_point_stay_on_the_curve, p384_red_doubling_an_off_curve_point_stays_off_the_curve, p384_apples_ca_and_root_keys_are_on_the_curve and the sha384_* FIPS cases with their reds) while each still evaluates the real curve equation or the real hash; WHAT THAT MUST BE SUFFICIENT FOR: the P-384 parameters and SHA-384 are exercised on the acceptance path with no interpreted 16-limb fold inside a claim frame, so the interpreted identities can leave the floor for that row, or they measure under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives. The same row run BY NAME (as it exists since gunbc#12306) executes the facts natively but is NOT the acceptance path and retires nothing. Supplying the curve check's answer or the digest as a fixture, or deleting the identities, satisfies neither. +### new-witness eval-step cost gate over the eleven mtcollins1 boot acceptance matrix cases that run the real boot entry end to end over the dry operation realization: they still execute, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered — declared 2026-09-28 + +new-witness eval-step cost gate over the eleven mtcollins1 boot acceptance matrix cases that run the real boot entry end to end over the dry operation realization: they still execute, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: the evaluation frame and its modeled operation realization realized by the natively emitted runtime, so the boot entry runs as emitted code rather than in the seed interpreter). Population: test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_host_that_never_prints_a_census_refuses_at_the_deadline: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_host_that_never_prints_a_census_refuses_at_the_deadline, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=170048 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_healthy_census_completes_and_releases_its_collector: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_healthy_census_completes_and_releases_its_collector, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=160637 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.an_already_presented_image_is_not_attached_again: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions an_already_presented_image_is_not_attached_again, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=137485 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.media_that_never_becomes_ready_refuses_before_any_power_action: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions media_that_never_becomes_ready_refuses_before_any_power_action, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=92947 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_presentation_lost_after_readiness_stops_the_handoff: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_presentation_lost_after_readiness_stops_the_handoff, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=98794 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_presentation_lost_after_the_handoff_is_the_reported_cause: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_presentation_lost_after_the_handoff_is_the_reported_cause, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=132731 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_sol_loss_mid_boot_is_reported_before_the_deadline: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_sol_loss_mid_boot_is_reported_before_the_deadline, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=129808 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_two_socket_answer_is_a_truthful_topology_refusal: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_two_socket_answer_is_a_truthful_topology_refusal, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=126897 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_listing_that_names_the_image_twice_starts_nothing: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_listing_that_names_the_image_twice_starts_nothing, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=79511 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.the_right_filename_on_the_wrong_share_refuses_before_any_power_action: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions the_right_filename_on_the_wrong_share_refuses_before_any_power_action, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=73872 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.pinned_an_interrupted_attempt_locks_out_the_next_one: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_boot_matrix_rows; measured by PR required floor run 36661418914 of gunbc#12533 at c308d7f3dd5, the COMPLETED-OVER-COST-REQUIREMENT line for this identity: verdict pass, eval_steps=75263 against the 72,300 new-witness budget (a local claim_batch over the same tree read 70,000; the floor's own figure decides membership); the billed work is the real boot entry executed twice in the seed interpreter over the dry realization. Restored when: THE CAPABILITY: witnesses emitted to native code with the emitted runtime realizing v2.std.witness_evaluation evaluate_in_witness_frame and its v2.std.operation_realization modeled realization, EXECUTING ON THE MERGE PATH as a phase of a required lane whose red blocks a merge, running the mtcollins1 boot acceptance matrix with the real mtcollins1_boot_wet_on_srv1 entry; WHAT THAT MUST BE SUFFICIENT FOR: each of these eleven identities measures under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives, with its route and outcome assertions unchanged. Hoisting the shared world construction or the route prefix lowers the bill and retires nothing on its own; supplying a decided value in place of the entry, or deleting the identities, satisfies neither. + ### new-witness eval-step cost gate over six App Attest verifier claims -- the two real-path inhabitance claims over Apple's objects, three single structural steps priced by their own SHA-256s, and the wire-carrier join: they still execute, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered — declared 2026-09-22 new-witness eval-step cost gate over six App Attest verifier claims -- the two real-path inhabitance claims over Apple's objects, three single structural steps priced by their own SHA-256s, and the wire-carrier join: they still execute, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: the CBOR, DER and SHA-256 readers executing as natively emitted code over the sample objects rather than as interpreted octet-list folds). Population: test.claim.app_attest_verifier_witness_test.the_sample_passes_every_step_before_the_extension_steps: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_app_attest_verifier_rows; measured by claim_batch --hermetic [witness] receipt at session/nimble-eagle-216-step3b 4d089af1cb9 (gunbc#11989): verdict pass, wall under the 8 s deadline, eval_steps read from that receipt's own line and over the new-witness budget; the billed work is the real path end to end: Apple's attestation object through decode_attestation (CBOR, two DER certificates, the PEM-pinned root, authenticator data) and the whole structural fold with its SHA-256s. It is the attestation path's one inhabitance claim, so nothing here is supplied, test.claim.app_attest_verifier_witness_test.the_nonce_step_reds_on_other_client_data: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_app_attest_verifier_rows; measured by claim_batch --hermetic [witness] receipt at session/nimble-eagle-216-step3b 4d089af1cb9 (gunbc#11989): verdict pass, wall under the 8 s deadline, eval_steps read from that receipt's own line and over the new-witness budget; the billed work is nonce_step alone over supplied inputs: SHA-256 of the client data and SHA-256 of authData concatenated with it, two interpreted hashes, which is the step and nothing before it, test.claim.app_attest_verifier_witness_test.the_app_id_step_reds_on_another_app_id: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_app_attest_verifier_rows; measured by claim_batch --hermetic [witness] receipt at session/nimble-eagle-216-step3b 4d089af1cb9 (gunbc#11989): verdict pass, wall under the 8 s deadline, eval_steps read from that receipt's own line and over the new-witness budget; the billed work is app_id_step alone over supplied inputs: one interpreted SHA-256 of the App ID, test.claim.app_attest_verifier_witness_test.the_key_id_step_admits_the_real_key_and_reds_on_another_key_id: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_app_attest_verifier_rows; measured by claim_batch --hermetic [witness] receipt at session/nimble-eagle-216-step3b (gunbc#11989), and the required floor's required-ci-measurement-receipt: verdict pass, wall under the 8 s deadline, eval_steps read from that receipt's own line and over the new-witness budget; the billed work is key_id_step alone over supplied inputs, paired over its own subject: one interpreted SHA-256 of the credential certificate's 65-octet public key (the second comparison reuses it), test.claim.app_attest_verifier_witness_test.the_sample_assertion_passes_rp_id_and_refuses_on_absent_extensions: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_app_attest_verifier_rows; measured by claim_batch --hermetic [witness] receipt at session/nimble-eagle-216-step3b (gunbc#11989), and the required floor's required-ci-measurement-receipt: verdict pass, wall under the 8 s deadline, eval_steps read from that receipt's own line and over the new-witness budget; the billed work is the assertion's real path: the assertion object through assertion_parts and the fold's RP ID SHA-256, plus the attestation's leaf certificate read for the credential key (the attestation-to-assertion join). It is the assertion path's one inhabitance claim, paired with a wrong-App-ID refusal over the same subject, test.claim.signature_verify_join_witness_test.malformed_carriers_refuse_before_the_curve: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_app_attest_verifier_rows; measured by claim_batch --hermetic [witness] receipt at session/nimble-eagle-216-step3b 4d089af1cb9 (gunbc#11989): verdict pass, wall under the 8 s deadline, eval_steps read from that receipt's own line and over the new-witness budget. THIS ROW'S BILLED WORK IS NOT THE VERIFIER ROWS': it touches no Apple object, no certificate and no hash. It base64url-decodes two carriers of the RFC 6979 A.2.5 P-256 vectors through extdeps.crypto.signature verify_signature, which asks signature_carrier_refusal FIRST and refuses on size before the implementation is consulted. What the budget prices is the interpreter walking those octet lists byte by byte to decode and size them. Restored when: THE CAPABILITY. MachineWidth reification (gunbc#11819) lets the extdeps.apple.app_attest closure emit, and these six identities execute on the natively emitted route -- the gunbc test instrument row the ecdsa_verification_realization_frontier names -- while each still exercises its own production code over its own inputs -- Apple's objects end to end for the two inhabitance claims, its one named step for the three step claims, the RFC 6979 carriers for the carrier-join claim; WHAT THAT MUST BE SUFFICIENT FOR: the verifier folds are exercised over the real sample on the acceptance path, and the carrier join over its real carriers, with no interpreted octet walk inside a claim frame, and the identities then measure under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives, or leave the floor for that native row. Supplying the two inhabitance claims' inputs as fixtures, precomputing a step's hashes, or deleting the identities satisfies neither. @@ -350,6 +354,10 @@ new-witness eval-step cost gate over six App Attest verifier claims -- the two r the enrolment-margin decision over exactly two App Attest verifier claims whose honest CPU lies in (margin, per-subject line]: they execute, and an exact reading inside the band is reported rather than decided: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: a general dead-band standing in v2.workflow.floor_enrolment_margin, or these two identities executing with stable headroom below the margin). Population: test.claim.app_attest_verifier_witness_test.the_key_id_step_admits_the_real_key_and_reds_on_another_key_id, test.claim.app_attest_verifier_witness_test.the_sample_assertion_passes_rp_id_and_refuses_on_absent_extensions. Restored when: THE CAPABILITY, EITHER OF TWO: (a) these EXACT two identities execute on a named native route (the gunbc test instrument row gunbc.auth.approval_device_redemption ecdsa_verification_realization_frontier names) with stable headroom below the enrolment margin across the envelope floor_enrolment_margin derives; or (b) a general repair of the dead-band policy in v2.workflow.floor_enrolment_margin gives every newly enrolled identity in the band a representable standing (gunbc.recurring_failure_mode enrolment_dead_band_has_no_representable_standing). MachineWidth reification or the native frontier ALONE does not retire this row: what must hold is that the two readings are under the margin with headroom, or that the policy no longer needs an exact-identity authority. v2.workflow.floor_enrolment_dead_band and this row then delete together. +### the enrolment-margin decision over the mtcollins1 boot acceptance matrix cases whose honest CPU lies in (margin, per-subject line]: they execute, and an exact reading inside the band is reported rather than decided — declared 2026-09-30 + +the enrolment-margin decision over the mtcollins1 boot acceptance matrix cases whose honest CPU lies in (margin, per-subject line]: they execute, and an exact reading inside the band is reported rather than decided: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: the matrix cases executing as natively emitted witnesses, the same replacement the eval-step drop mtcollins1_boot_matrix_new_witness_eval_step_cost waits on). Population: test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_host_that_never_prints_a_census_refuses_at_the_deadline: the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 396 ms CPU, strictly above the 302 ms margin and under the 500 ms line, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_healthy_census_completes_and_releases_its_collector: the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 394 ms CPU, strictly above the 302 ms margin and under the 500 ms line, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_presentation_lost_after_the_handoff_is_the_reported_cause: the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648951356 of gunbc#12554 at 1cf19cf8ba observed 303 ms CPU, strictly above the 302 ms margin and under the 500 ms line, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.an_already_presented_image_is_not_attached_again: the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 361 ms CPU, strictly above the 302 ms margin and under the 500 ms line, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_two_socket_answer_is_a_truthful_topology_refusal: the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 339 ms CPU, strictly above the 302 ms margin and under the 500 ms line, test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_sol_loss_mid_boot_is_reported_before_the_deadline: the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 332 ms CPU, strictly above the 302 ms margin and under the 500 ms line. Restored when: THE CAPABILITY: witnesses emitted to native code with the emitted runtime realizing v2.std.witness_evaluation evaluate_in_witness_frame and its v2.std.operation_realization modeled realization, EXECUTING ON THE MERGE PATH as a phase of a required lane whose red blocks a merge, running the mtcollins1 boot acceptance matrix with the real mtcollins1_boot_wet_on_srv1 entry; WHAT THAT MUST BE SUFFICIENT FOR: each dead-band identity reaches its verdict with stable headroom under the enrolment margin v2.workflow.floor_enrolment_margin derives, with its route and outcome assertions unchanged -- at which point every row stales and deletes. Cutting the polling route the cases assert, or supplying a decided value in place of the entry, satisfies neither. + ### new-witness eval-step cost gate over the one claim that inhabits the real byte-span argv with its really-serialized program: it still executes, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered — declared 2026-09-22 new-witness eval-step cost gate over the one claim that inhabits the real byte-span argv with its really-serialized program: it still executes, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: the serialized byte-span program reaching a claim frame as a served value rather than being re-rendered inside it, or a serialization that fits the budget). Population: test.claim.spark.v41_checkpoint_materialize_witness.the_span_read_reads_exactly_its_region: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_span_program_rows; measured by gunbc#12010, claim_batch over dag/test/claim/spark/v41_checkpoint_materialize_witness_test.dag; planned_as_changed_witness, verdict pass, over the new-witness budget. The billed work is the one real serialization of gunbc.sha256sum_byte_span sha256sum_byte_span_program through gunbc.shell_command_text, which this claim is the argv's only inhabitance route for. Restored when: THE CAPABILITY, EITHER CLAUSE SATISFIES IT, AND BOTH ARE STATED BECAUSE THE CAUSE IS NOT YET ESTABLISHED. (i) gunbc.sha256sum_byte_span sha256sum_byte_span_program is served across claim frames by v2.workflow.floor_pure_producer_share on the acceptance path; WHAT THAT MUST BE SUFFICIENT FOR: a required-floor claim asserting the real byte-span argv carries the really-serialized program does not re-render it inside its own frame. A share row not covering this identity's demand does not satisfy this clause. OR (ii) v2.workflow.bash_command_fold_serialize serializes a fourteen-word statement list inside the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives -- whether by repair of a cost-shape defect there or by any other means. IN EITHER CASE this identity must measure under that budget WHILE STILL EXECUTING the real serialization route. Deleting the identity, supplying the program as a fixture, asserting only length(argv), or relocating it to a home that does not execute it satisfies neither clause. diff --git a/src/v1/stage0/src/std_measure.rs b/src/v1/stage0/src/std_measure.rs index adf9528a58d..1d7fd00dcee 100644 --- a/src/v1/stage0/src/std_measure.rs +++ b/src/v1/stage0/src/std_measure.rs @@ -1645,6 +1645,19 @@ pub fn second_count(s: Second) -> Nat { measure_count(s.clone()) } +pub type SecondDisplacement = Rc>; + +pub fn second_displacement(count: i64) -> SecondDisplacement { + Rc::new(Measure { + count: count.clone(), + _phantom: std::marker::PhantomData, + }) +} + +pub fn second_displacement_count(d: SecondDisplacement) -> i64 { + measure_count(d.clone()) +} + pub fn energy_from_power_and_time(power: Watt, time: Second) -> Joule { joule(v1_rt::int_mul( watt_count(power.clone()), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index d276f89973e..4d8a0cae656 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -7858,6 +7858,15 @@ fn current_witness_evaluation_frame() -> Option { struct ModeledRealizationSlot { envelope: Value, realization: Value, + /// The realization's bindings by operation identity (`operation_realization_index`), built + /// once at admission so no dispatch rescans the binding list. + index: Value, + /// Handler selections already decided in this frame, keyed by the COMPLETE input of + /// `operation_handler_selection` that varies: the operation's declaring file, service, + /// operation and whether it is readonly. The envelope, the realization and its index are fixed + /// for the frame's extent and the selection reads nothing else of the invocation, so a hit is + /// the same fact recomputed, never a different one. + selections: HashMap, identity: String, state: Value, /// The virtual clock, an opaque `std.measure` `Second`: the dispatcher never reads its @@ -8084,9 +8093,17 @@ fn admit_modeled_realization( let advance = record_field(ctx, &realization, "advance") .ok_or_else(|| modeled_refused("(frame)", "the realization carries no advance function"))?; let state = apply_modeled_handler(&advance, &[initial, now.clone()], env, ctx)?; + let index = run_in_context_with_args( + ctx, + "operation_realization_index", + &[(Some("realization".to_string()), realization.clone())], + false, + )?; Ok(Some(ModeledRealizationSlot { envelope, realization, + index, + selections: HashMap::new(), identity, state, now, @@ -8121,6 +8138,24 @@ fn bound_operation_invocation_value( continue; }; let bound = match value { + // An argv expansion binds as the words a real spawn receives, expanded by the same + // seed realization of v2.std.compilers.cli_surface ProcessArgvExpansion the shell + // dispatcher uses, never as a rendering of the carrier. + Value::Record { type_name, fields } + if resolve_sym(*type_name).rsplit('.').next() == Some("ProcessArgvExpansion") => + { + let mut words = Vec::new(); + push_process_argv_expansion(&mut words, &fields)?; + variant_value( + ctx, + "OperationInputValue", + "InputTextList", + vec![( + "items", + list_value(words.into_iter().map(str_value).collect::>()), + )], + ) + } Value::List(items) => { let texts: Vec = items.iter().map(|v| str_value(render_input(v))).collect(); variant_value( @@ -8177,6 +8212,7 @@ fn dispatch_modeled_operation( ( s.envelope.clone(), s.realization.clone(), + s.index.clone(), s.identity.clone(), s.state.clone(), s.now.clone(), @@ -8185,7 +8221,7 @@ fn dispatch_modeled_operation( }) }) }); - let Some((envelope, realization, identity, state, now, ordinal)) = snapshot else { + let Some((envelope, realization, index, identity, state, now, ordinal)) = snapshot else { return Ok(None); }; let key = format!("{service_name}.{op_name}"); @@ -8219,20 +8255,41 @@ fn dispatch_modeled_operation( }); record }; - let selection = run_in_context_with_args( - ctx, - "operation_handler_selection", - &[ - (Some("env".to_string()), envelope), - (Some("realization".to_string()), realization.clone()), - (Some("invocation".to_string()), invocation.clone()), - ( - Some("readonly".to_string()), - Value::Bool(op_declared_readonly(op_node, ctx)), - ), - ], - false, - )?; + let readonly = op_declared_readonly(op_node, ctx); + let selection_key = format!( + "{}#{}.{}#{}", + op_node.span.file, service_name, op_name, readonly + ); + let remembered = MODELED_REALIZATION_SLOTS.with(|slots| { + slots.borrow().last().and_then(|slot| { + slot.as_ref() + .and_then(|s| s.selections.get(&selection_key).cloned()) + }) + }); + let selection = match remembered { + Some(v) => v, + None => { + let decided = run_in_context_with_args( + ctx, + "operation_handler_selection", + &[ + (Some("env".to_string()), envelope), + (Some("realization".to_string()), realization.clone()), + (Some("index".to_string()), index), + (Some("invocation".to_string()), invocation.clone()), + (Some("readonly".to_string()), Value::Bool(readonly)), + ], + false, + )?; + MODELED_REALIZATION_SLOTS.with(|slots| { + if let Some(Some(slot)) = slots.borrow_mut().last_mut() { + slot.selections + .insert(selection_key.clone(), decided.clone()); + } + }); + decided + } + }; let (arm, fields) = variant_parts(ctx, &selection) .ok_or_else(|| modeled_refused(&key, "handler selection returned a malformed value"))?; let binding = match arm.as_str() { @@ -8277,9 +8334,10 @@ fn dispatch_modeled_operation( ); modeled_refused(&key, format!("harness fault: {reason}")) }; - if !is_shell_transport(transport.clone()) { + let shell_operation = is_shell_transport(transport.clone()); + if !shell_operation && !is_file_transport(transport.clone(), ctx.si()) { return Err(harness_fault( - "a modeled realization supplies shell transport observations only; this operation's transport is not shell".to_string(), + "a modeled realization supplies shell and file transport observations only; this operation's transport is neither".to_string(), )); } let handler = record_field(ctx, &binding, "handler") @@ -8357,7 +8415,24 @@ fn dispatch_modeled_operation( return Err(error); } }; - let shell = shell_result_of_observation(&observation, ctx).map_err(&harness_fault)?; + let projected = if shell_operation { + shell_result_of_observation(&observation, ctx) + .map_err(&harness_fault) + .map(|shell| shell_result_projection(shell, op_node, ctx)) + } else { + // The path is the transport's own (file_transport_path), resolved exactly as the wet + // dispatch resolves it; one that is missing or empty refuses, never an empty path the + // projection would report as if the operation had named one. + match file_transport_path(transport, param_env, ctx) { + Ok(p) => file_result_of_observation(&observation, &p, ctx), + Err(e) => Err(format!( + "a file operation's transport path did not resolve: {e}" + )), + } + .map_err(&harness_fault) + .map(|file| map_file_outputs(&file, op_node, ctx)) + }; + let projected = projected?; log( variant_value( ctx, @@ -8369,7 +8444,7 @@ fn dispatch_modeled_operation( Some(advanced), false, ); - shell_result_projection(shell, op_node, ctx).map(Some) + projected.map(Some) } "OperationWorkerKilled" => { let committed = ctx @@ -8404,6 +8479,80 @@ fn dispatch_modeled_operation( } } +/// A modeled FileExchangeObservation as the file transport result the real dispatcher produces. +/// The failure kind is named by its closed .dag authority (`filesystem_failure_kind_name`), the same +/// channel a host `io::Error` is projected onto, so a consumer's kind admission reads it unchanged. +fn file_result_of_observation( + observation: &Value, + path: &str, + ctx: &InterpContext, +) -> Result { + let (arm, fields) = variant_parts(ctx, observation).ok_or("the observation is malformed")?; + if arm != "FileObserved" { + return Err(format!( + "a file operation was answered with a {arm} observation; a file operation needs FileObserved" + )); + } + let file = ctx + .field(&fields, "observation") + .ok_or("FileObserved carries no observation")?; + let (file_arm, file_fields) = + variant_parts(ctx, file).ok_or("the file observation is malformed")?; + let text = |name: &str| match ctx.field(&file_fields, name) { + Some(Value::Str(s)) => Ok(s.to_string()), + _ => Err(format!("the file observation carries no {name}")), + }; + match file_arm.as_str() { + "FileOperationSucceeded" => { + let bytes = ctx + .field(&file_fields, "byte_count") + .cloned() + .ok_or("the file observation carries no byte_count")?; + let byte_count = match run_in_context_with_args( + ctx, + "file_observation_byte_count", + &[(Some("bytes".to_string()), bytes)], + false, + ) { + Ok(Value::Int(n)) => n, + _ => return Err("the file observation's byte_count is not a byte size".to_string()), + }; + Ok(FileResult { + success: true, + byte_count, + path: path.to_string(), + error: String::new(), + error_kind: String::new(), + content: text("content")?, + }) + } + "FileOperationFailed" => { + let kind = ctx + .field(&file_fields, "kind") + .cloned() + .ok_or("the file observation carries no kind")?; + let kind_name = match run_in_context_with_args( + ctx, + "filesystem_failure_kind_name", + &[(Some("kind".to_string()), kind)], + false, + ) { + Ok(Value::Str(s)) => s.to_string(), + _ => return Err("the file observation's kind has no name".to_string()), + }; + Ok(FileResult { + success: false, + byte_count: 0, + path: path.to_string(), + error: text("error")?, + error_kind: kind_name, + content: String::new(), + }) + } + other => Err(format!("unrecognized file observation {other}")), + } +} + /// A modeled ShellExchangeObservation as the shell transport result the real dispatcher produces. fn shell_result_of_observation( observation: &Value, @@ -17167,18 +17316,20 @@ fn io_error_kind_name(e: &std::io::Error) -> String { .to_string() } -fn dispatch_file( - op_node: &Rc, +/// THE ONE RESOLUTION OF A FILE OPERATION'S PATH: the transport's own `path` property, evaluated and +/// template-substituted over the operation's inputs. The wet dispatch and the modeled realization both +/// read it here, so a modeled answer is recorded against exactly the path the real transport would +/// touch -- including an operation whose path is a literal in its transport and not an input +/// (linux.Procfs ReadUptime). A missing or empty path refuses. +fn file_transport_path( transport: &Rc, param_env: &Rc, ctx: &InterpContext, -) -> InterpResult { - let si = ctx.si(); - +) -> InterpResult { let path = match find_property( transport.properties.clone(), "base_path".to_string(), - si.clone(), + ctx.si(), ) { Some(path_node) => { let path_val = eval_expr(&path_node, param_env, ctx)?; @@ -17195,6 +17346,18 @@ fn dispatch_file( msg: "file transport resolved to an empty path".to_string(), }); } + Ok(path) +} + +fn dispatch_file( + op_node: &Rc, + transport: &Rc, + param_env: &Rc, + ctx: &InterpContext, +) -> InterpResult { + let si = ctx.si(); + + let path = file_transport_path(transport, param_env, ctx)?; // Optional explicit verb on the transport row (`transport file { path: ..., verb: "delete" }`). // Delete/List are structurally indistinguishable from Read (path-only inputs), so the diff --git a/src/v2/std/operation_realization.dag b/src/v2/std/operation_realization.dag index 97e82210962..225cc431f40 100644 --- a/src/v2/std/operation_realization.dag +++ b/src/v2/std/operation_realization.dag @@ -1,16 +1,18 @@ module v2.std.operation_realization -import std.types { Bool, Int, List, NonEmptyStr, String } +import std.types { Bool, Int, List, Map, NonEmptyStr, String } import std.effect_grant { Envelope, HandlerBinding, CoveredBy, NoCoveringGrant, covering_grant, NamespacePosition, ServiceOpTree, Read, Write, Verb, } import v2.std.operation_argv { OperationRef, BoundOperationInvocation, InputText, InputTextList } import std.list { first_duplicate_by_key } +import v2.std.collection { empty_map, map_insert, map_lookup } import std.measure { Second, second, second_count } import std.checked_arithmetic { checked_int_to_nat } import std.execution_mode { ExecutionMode, Hermetic, Wet, Record } import extdeps.transports.shell { ShellExchangeObservation, ShellProcessExited } +import extdeps.transports.file { FileExchangeObservation } // A MODELED OPERATION REALIZATION: the dry arm of an operation's realization, bound per grant. // @@ -43,6 +45,7 @@ import extdeps.transports.shell { ShellExchangeObservation, ShellProcessExited } // and the dispatch log for the dynamic extent of one witness frame. type TransportObservation = ShellObserved { observation: ShellExchangeObservation } + | FileObserved { observation: FileExchangeObservation } // A step either answers with an observation, or reports that the worker died after the effect was // (or was not) committed and before any reply, or reports that the SCENARIO is malformed. The last @@ -109,7 +112,6 @@ type OperationBindingRefusal | OperationBoundElsewhere { at: OperationRef, binding: HandlerBinding } | OperationRealizationMismatch { at: OperationRef, named: String, active: NonEmptyStr } | OperationNotBound { at: OperationRef } - | OperationBoundTwice { at: OperationRef, count: Int } type OperationHandlerSelection = OperationHandlerSelected { binding: OperationBinding } @@ -127,44 +129,27 @@ fn operation_verb(readonly: Bool) -> Verb { if readonly { Read } else { Write } } -type BindingMatch - = BindingMatchNone - | BindingMatchOne { binding: OperationBinding } - | BindingMatchMany { count: Int } - -fn binding_match(bindings: List>, at: OperationRef) -> BindingMatch { - fold(bindings, init: BindingMatchNone, f: fn(acc, b) { - if operation_ref_eq(a: b.at, b: at) { - match acc { - BindingMatchNone => BindingMatchOne { binding: b } - BindingMatchOne { binding: _ } => BindingMatchMany { count: 2 } - BindingMatchMany { count: n } => BindingMatchMany { count: n + 1 } - } - } else { acc } - }) -} - // THE SINGLE SELECTION DECISION, called by the dispatcher for every operation issued while a modeled // realization is active. Grant coverage first (the same covering_grant REST replay uses), then the -// named realization, then exactly one binding for the resolved identity. +// named realization, then the one binding the admitted index holds for the resolved identity. fn operation_handler_selection( env: Envelope, realization: OperationRealization, + index: Map>, invocation: BoundOperationInvocation, readonly: Bool, ) -> OperationHandlerSelection { let at = invocation.at match covering_grant(env: env, verb: operation_verb(readonly: readonly), target: operation_position(at: at)) { NoCoveringGrant { verb: _, target: _, frame: _ } => OperationHandlerRefused { cause: OperationUncovered { at: at } } - CoveredBy { grant } => match grant.binding { + CoveredBy { grant: covering } => match covering.binding { ModeledRealization { realization: named } => if named != (realization.identity as String) { OperationHandlerRefused { cause: OperationRealizationMismatch { at: at, named: named, active: realization.identity } } } else { - match binding_match(bindings: realization.bindings, at: at) { - BindingMatchNone => OperationHandlerRefused { cause: OperationNotBound { at: at } } - BindingMatchMany { count: n } => OperationHandlerRefused { cause: OperationBoundTwice { at: at, count: n } } - BindingMatchOne { binding: b } => OperationHandlerSelected { binding: b } + match map_lookup(m: index, key: operation_ref_key(at: at)) { + Absent => OperationHandlerRefused { cause: OperationNotBound { at: at } } + Present { value: b } => OperationHandlerSelected { binding: b } } } other => OperationHandlerRefused { cause: OperationBoundElsewhere { at: at, binding: other } } @@ -172,6 +157,14 @@ fn operation_handler_selection( } } +// THE BINDINGS BY IDENTITY, BUILT ONCE WHEN THE FRAME IS ADMITTED. Every dispatch then looks its +// operation up instead of scanning the binding list: the list is fixed for the frame's extent, so a +// per-dispatch scan re-derived the same fact on every call (DESIGN section 2). Admission has already +// refused a realization that binds one identity twice, so each key holds exactly one binding. +fn operation_realization_index(realization: OperationRealization) -> Map> { + fold(realization.bindings, init: empty_map(), f: fn(acc, b) { map_insert(m: acc, key: operation_ref_key(at: b.at), value: b) }) +} + // ADMISSION BEFORE THE SUBJECT RUNS: a realization binding one identity twice is malformed whatever // the subject later issues. Resolution of each binding against the operation registry is the // dispatcher's (it owns the registry); this is the part decidable from the value alone. diff --git a/src/v2/workflow/floor_enrolment_dead_band.dag b/src/v2/workflow/floor_enrolment_dead_band.dag index b5c7fe1e6e7..4d124412d1e 100644 --- a/src/v2/workflow/floor_enrolment_dead_band.dag +++ b/src/v2/workflow/floor_enrolment_dead_band.dag @@ -40,6 +40,38 @@ fn app_attest_verifier_enrolment_dead_band_observed_only() -> List List { + [ + EnrolmentDeadBandObservation { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_host_that_never_prints_a_census_refuses_at_the_deadline", + reason: "the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 396 ms CPU, strictly above the 302 ms margin and under the 500 ms line" as NonEmptyStr, + }, + EnrolmentDeadBandObservation { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_healthy_census_completes_and_releases_its_collector", + reason: "the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 394 ms CPU, strictly above the 302 ms margin and under the 500 ms line" as NonEmptyStr, + }, + EnrolmentDeadBandObservation { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_presentation_lost_after_the_handoff_is_the_reported_cause", + reason: "the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648951356 of gunbc#12554 at 1cf19cf8ba observed 303 ms CPU, strictly above the 302 ms margin and under the 500 ms line" as NonEmptyStr, + }, + EnrolmentDeadBandObservation { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.an_already_presented_image_is_not_attached_again", + reason: "the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 361 ms CPU, strictly above the 302 ms margin and under the 500 ms line" as NonEmptyStr, + }, + EnrolmentDeadBandObservation { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_two_socket_answer_is_a_truthful_topology_refusal", + reason: "the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 339 ms CPU, strictly above the 302 ms margin and under the 500 ms line" as NonEmptyStr, + }, + EnrolmentDeadBandObservation { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_sol_loss_mid_boot_is_reported_before_the_deadline", + reason: "the real boot entry end to end over the dry realization, whose cost is gunbc#12434's own SOL polling route run faithfully (the subject gunbc#12423 requires); PR required floor run 36648847499 of gunbc#12533 at bd99cbb4899 observed 332 ms CPU, strictly above the 302 ms margin and under the 500 ms line" as NonEmptyStr, + }, + ] +} + fn enrolment_dead_band_identities() -> List { - app_attest_verifier_enrolment_dead_band_observed_only() |> map(o => o.identity) + concat(app_attest_verifier_enrolment_dead_band_observed_only(), mtcollins1_boot_matrix_enrolment_dead_band_observed_only()) |> map(o => o.identity) } diff --git a/src/v2/workflow/floor_eval_step_cost_drop.dag b/src/v2/workflow/floor_eval_step_cost_drop.dag index 790f945168a..1f09d789cbb 100644 --- a/src/v2/workflow/floor_eval_step_cost_drop.dag +++ b/src/v2/workflow/floor_eval_step_cost_drop.dag @@ -26,6 +26,8 @@ import std.types { NonEmptyStr } // (`sha256_span_program_serialize_new_witness_eval_step_cost`); // - `floor_eval_step_cost_drop_python_to_typescript_inhabitance_rows`: the python->typescript // compile inhabitance claim (`python_to_typescript_compile_inhabitance_off_the_required_gate`); +// - `floor_eval_step_cost_drop_boot_matrix_rows`: the mtcollins1 boot acceptance matrix +// (`mtcollins1_boot_matrix_new_witness_eval_step_cost`). // - `floor_eval_step_cost_drop_dark_install_render_rows`: the first reader of the broker dark-install // script (`live_deploy_dark_install_render_new_witness_eval_step_cost`). // The loss is a WORKFLOW fact -- which @@ -234,6 +236,59 @@ data floor_eval_step_cost_drop_python_to_typescript_inhabitance_rows: List = [ + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_host_that_never_prints_a_census_refuses_at_the_deadline" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_host_that_never_prints_a_census_refuses_at_the_deadline, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=170048 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_healthy_census_completes_and_releases_its_collector" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_healthy_census_completes_and_releases_its_collector, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=160637 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.an_already_presented_image_is_not_attached_again" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions an_already_presented_image_is_not_attached_again, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=137485 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.media_that_never_becomes_ready_refuses_before_any_power_action" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions media_that_never_becomes_ready_refuses_before_any_power_action, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=92947 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_presentation_lost_after_readiness_stops_the_handoff" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_presentation_lost_after_readiness_stops_the_handoff, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=98794 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_presentation_lost_after_the_handoff_is_the_reported_cause" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_presentation_lost_after_the_handoff_is_the_reported_cause, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=132731 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_sol_loss_mid_boot_is_reported_before_the_deadline" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_sol_loss_mid_boot_is_reported_before_the_deadline, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=129808 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_two_socket_answer_is_a_truthful_topology_refusal" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_two_socket_answer_is_a_truthful_topology_refusal, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=126897 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.a_listing_that_names_the_image_twice_starts_nothing" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions a_listing_that_names_the_image_twice_starts_nothing, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=79511 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.the_right_filename_on_the_wrong_share_refuses_before_any_power_action" as NonEmptyStr, + measured_by: "claim_batch --entry dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag --functions the_right_filename_on_the_wrong_share_refuses_before_any_power_action, over gunbc#12533 merged with main after gunbc#12636 (tree d6c5146bce6 plus the file-transport path resolution), 2026-09-30: PASS, eval_steps=73872 against the 72,300 new-witness budget (eval_steps are host-independent); the billed work is the real boot entry executed end to end in the seed interpreter over the dry realization" as NonEmptyStr, + }, + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test.pinned_an_interrupted_attempt_locks_out_the_next_one" as NonEmptyStr, + measured_by: "PR required floor run 36661418914 of gunbc#12533 at c308d7f3dd5, the COMPLETED-OVER-COST-REQUIREMENT line for this identity: verdict pass, eval_steps=75263 against the 72,300 new-witness budget (a local claim_batch over the same tree read 70,000; the floor's own figure decides membership); the billed work is the real boot entry executed twice in the seed interpreter over the dry realization" as NonEmptyStr, + }, +] + // NINTH DROP, SAME MEMBERSHIP TEST, OPERATOR-ADMITTED (2026-09-29, relayed by proud-deer-538). One // identity: whichever test.claim.live_deploy.emit claim first reads witness_approval_broker_dark_script_text // is billed a marginal the generic bash emit path's per-step overhead causes (bundle lookup, @@ -248,7 +303,7 @@ data floor_eval_step_cost_drop_dark_install_render_rows: List List { - concat(concat(concat(concat(concat(concat(concat(concat(floor_eval_step_cost_drop_rows, floor_eval_step_cost_drop_apply_render_rows), floor_eval_step_cost_drop_live_forecast_rows), floor_eval_step_cost_drop_page_style_rows), floor_eval_step_cost_drop_interpreted_crypto_rows), floor_eval_step_cost_drop_app_attest_verifier_rows), floor_eval_step_cost_drop_span_program_rows), floor_eval_step_cost_drop_python_to_typescript_inhabitance_rows), floor_eval_step_cost_drop_dark_install_render_rows) + concat(concat(concat(concat(concat(concat(concat(concat(concat(floor_eval_step_cost_drop_rows, floor_eval_step_cost_drop_apply_render_rows), floor_eval_step_cost_drop_live_forecast_rows), floor_eval_step_cost_drop_page_style_rows), floor_eval_step_cost_drop_interpreted_crypto_rows), floor_eval_step_cost_drop_app_attest_verifier_rows), floor_eval_step_cost_drop_span_program_rows), floor_eval_step_cost_drop_python_to_typescript_inhabitance_rows), floor_eval_step_cost_drop_boot_matrix_rows), floor_eval_step_cost_drop_dark_install_render_rows) } // THE PROJECTION THE SEED RUNNER READS AND THE MODEL TESTS AGAINST. The runner refuses an empty or