Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
911abc4
Modeled operation realization: file transport arm + gunbc.filesystem_…
Sep 28, 2026
cd5bdd5
Boot dry realization: environment, local/remote exact-invocation, rem…
Sep 28, 2026
3967705
Witness the boot-world models' own semantics (calendar, backward step…
Sep 28, 2026
96ba551
Boot world: expanded BMC model (override, SEL, SOL session, cycle res…
Sep 28, 2026
a712a75
MegaRAC media model + adapter; mtcollins1 boot acceptance matrix over…
Sep 28, 2026
cb2f3b1
Matrix: media, observation, resource and interruption cases asserting…
Sep 28, 2026
1574a97
Floor: rename the covering-grant binder and the matrix grant helper (…
Sep 28, 2026
41b5730
Matrix floor pricing (cost-debt admissions + declared eval-step drop)…
Sep 28, 2026
c116346
chore: regenerate drifted generated artifacts (ci auto-heal)
gunbai-bot[bot] Sep 28, 2026
a0e46d8
Matrix cost: bindings indexed once at admission, SOL drop armed by th…
Sep 28, 2026
ef2c744
Merge auto-heal regeneration; keep the projection regenerated from th…
Sep 28, 2026
52b2850
Floor: import the map operations from v2.std.collection (map_lookup, …
Sep 28, 2026
53c1ce6
Matrix cost: remember each frame's handler selections; advance does n…
Sep 28, 2026
cfe9618
mtcollins1 boot: a presentation affirmed lost after a confirmed hando…
Sep 28, 2026
e25a17d
BMC model: an event a transition schedules is kept (power restore kee…
Sep 28, 2026
63919b6
Merge #12533 (session/swift-deer-358-pr2) so the matrix case flips in…
Sep 28, 2026
5b8e3bf
Matrix: a presentation lost after the handoff is the reported cause (…
Sep 28, 2026
e597579
File arm refuses a pathless dispatch; modeled byte_count is a ByteSiz…
Sep 28, 2026
5ccd728
Matrix: the lost-presentation case asserts the named cause wherever i…
Sep 28, 2026
020149f
Merge branch 'main' into session/swift-deer-358-pr2
briansrls Sep 29, 2026
72b84eb
Regenerate the std.measure stage0 mirror for SecondDisplacement
Sep 29, 2026
108c033
Merge #12533 (with its std_measure.rs regeneration and main)
Sep 29, 2026
376798f
Merge main: one BmcWorld carries both the boot state and #12490's web…
Sep 29, 2026
a10c0b6
Merge remote-tracking branch 'origin/session/swift-deer-358-pr2' into…
Sep 29, 2026
c2ab8ad
One Gregorian calendar: extdeps.units.iso8601 owns both directions (r…
Sep 29, 2026
7c60c3d
wall_clock_model: name the reading helper wall_clock_printed (the flo…
Sep 29, 2026
f96ba04
Name String's declarer: extdeps.systemd.journalctl and extdeps.units.…
Sep 29, 2026
0227a71
iso8601 keeps String through std.types: it is in the stage0 closure (…
Sep 29, 2026
2c5d045
Calendar in extdeps.units.iso8601_calendar, off the compiler seed's c…
Sep 29, 2026
6e9568a
journalctl names the declarers of String and Unit (floor AmbiguousBar…
Sep 29, 2026
826011d
Rung-drop row: the route prefix is per-world, not a repeated computat…
Sep 29, 2026
d75894e
roadmap_served_observation names Filesystem's declarer (floor Ambiguo…
Sep 29, 2026
e43e6cb
Merge main (#12517, #12482, #12586): both eval-step drop lists; rung-…
Sep 29, 2026
02727b3
Merge #12533 (main at e43e6cbdacd)
Sep 29, 2026
b7c671c
Rung-drop row: the shared world construction is measured, and owes no…
Sep 29, 2026
66f58d5
Merge main; the host-command model renders words through argv_words (…
Sep 29, 2026
680e3da
Merge main (#12434 and others)
Sep 30, 2026
bd99cbb
Matrix: bind #12434's SOL route; the two pinned SOL cases flip to con…
Sep 30, 2026
1cf19cf
Merge #12533 at bd99cbb4899 (main with #12434): keep #12434's clean-r…
Sep 30, 2026
45d967d
Matrix: the SOL-loss case requires exactly one teardown, after the po…
Sep 30, 2026
a67a3dc
Matrix: six cases admitted to the enrolment dead band under one decla…
Sep 30, 2026
d6c5146
Merge remote-tracking branch 'origin/main' into session/swift-deer-35…
Sep 30, 2026
82ec7d4
Integrate #12636: uptime answers over the file transport; one path re…
Sep 30, 2026
eb1bbe4
Merge #12533 at 82ec7d4d605 (enrolment dead band, #12636): the rename…
Sep 30, 2026
c308d7f
Retire dag/std/measure.dag#Time from the unimported-bare-provider ros…
Sep 30, 2026
a94b82e
Eval-step drop: the interrupted-attempt case is back, at CI's 75,263
Sep 30, 2026
4171e87
Merge remote-tracking branch 'origin/main' into session/swift-deer-35…
Sep 30, 2026
707ac6a
Merge #12533 at 4171e87289; the rung-drop doc carries this PR's own d…
Sep 30, 2026
7f95460
Merge main: std_measure.rs takes both sides' additions
Sep 30, 2026
e500734
Merge main: the media-loss witness imports join main's StalePowerOffN…
Sep 30, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 67 additions & 0 deletions dag/extdeps/bmc/ipmitool_observed_output.dag
Original file line number Diff line number Diff line change
@@ -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 <bus> <addr> 2 <reg-lo> <reg-hi>` 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 `<name> : <value>` 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"
73 changes: 73 additions & 0 deletions dag/extdeps/bmc/megarac_observed_output.dag
Original file line number Diff line number Diff line change
@@ -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":"<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 = "{}"
21 changes: 20 additions & 1 deletion dag/extdeps/transports/file.dag
Original file line number Diff line number Diff line change
@@ -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 }
Expand All @@ -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
}
80 changes: 80 additions & 0 deletions dag/extdeps/units/iso8601_calendar.dag
Original file line number Diff line number Diff line change
@@ -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",
], "")
}
Loading
Loading