Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
8ef49ab
Board identity: a bound host's FRU board reaches its per-board author…
Oct 6, 2026
c425c92
Board authority witness: a WIWYNN FRU naming another product refuses
Oct 6, 2026
4267d8a
Board FRU receipt has one home; the committed Collins observation is …
Oct 6, 2026
5dd7fc9
BoardFruReceipt carries a Sha256Digest: no empty-digest default arm
Oct 6, 2026
64776b4
Retire the dynatron ampere_lga4926_cooling_mount unimported-bare-prov…
Oct 6, 2026
557a2be
board_fru_observation_of_text: enumerate FruCaptureGap arms, no wildc…
Oct 7, 2026
55b0e83
w_unread_compatibility: resolve against the single-socket recipe (the…
Oct 7, 2026
1668f4e
FRU gap grains: a field read can only be Absent|Repeated|Empty; captu…
Oct 7, 2026
baf59fa
Merge origin/main into session/sleek-carp-686
Oct 7, 2026
102950f
Make five latent T? == T sites explicit (Present) so the floor subjec…
Oct 7, 2026
1e44343
Merge origin/main into session/sleek-carp-686
Oct 7, 2026
2844bf5
grounded_principal witness: grant/step counts follow the ci_runner_su…
Oct 8, 2026
d927e67
witnesses: compare first() through an explicit match (the Present-lit…
Oct 8, 2026
de18f22
One carrier for FRU capture failures: board lookup wraps gunbc.ipmito…
Oct 8, 2026
e4b25be
Fallout from #13179: latent T? == T sites and a stale roster count on…
Oct 8, 2026
4a499e1
grounded_principal witness: counts join ci_runner_sudo_binaries (revi…
Oct 8, 2026
6a3838c
Merge fallout-13179-optional-equality into session/sleek-carp-686
Oct 8, 2026
04f939b
tailscale credential + design witness: unwrap bindings.first() once v…
Oct 8, 2026
3c8558c
Merge fallout-13179-optional-equality into session/sleek-carp-686
Oct 8, 2026
69e8654
Merge origin/main into session/sleek-carp-686
Oct 8, 2026
a32a233
gigabyte: carry the candidate-board dissolution trigger onto the surv…
Oct 8, 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
43 changes: 43 additions & 0 deletions dag/extdeps/ampere/mt_collins_board.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
module extdeps.ampere.mt_collins_board

import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.board_authority { BoardAuthorityRef }
import extdeps.ampere.mt_collins_getting_started_guide.subject { mt_collins_gsg_authority }
import extdeps.ampere.mt_collins_product_brief.subject { MtCollinsPublicProductBrief, mt_collins_public_product_brief }

data extdeps_external_authority_anchor: ExternalAuthority = mt_collins_gsg_authority

data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.ampere.mt_collins_board",
decl_name: "mt_collins_board",
field: WholeDeclaration
}
},
first_citation: extdeps_external_authority_anchor,
further_citations: []
}

// THE MT. COLLINS BOARD AS A SUBJECT, joining the two Ampere documents that already own its facts
// rather than restating either: the Getting Started Guide (figures, orientation) and the public
// product brief. A board-grain subject exists so a bound host's board can reach its per-board
// authority by reference instead of through a closed enum.
type MtCollinsBoard {
getting_started_guide: ExternalAuthority
product_brief: MtCollinsPublicProductBrief
}

data mt_collins_board: MtCollinsBoard = MtCollinsBoard {
getting_started_guide: mt_collins_gsg_authority,
product_brief: mt_collins_public_product_brief,
}

data mt_collins_board_authority: BoardAuthorityRef = BoardAuthorityRef {
subject: DeclarationRef {
module_path: "extdeps.ampere.mt_collins_board",
decl_name: "mt_collins_board",
field: WholeDeclaration
}
}
10 changes: 5 additions & 5 deletions dag/extdeps/ampere/mt_collins_firmware_release.dag
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
module extdeps.ampere.mt_collins_firmware_release

import extdeps.ampere.mt_collins_board { mt_collins_board_authority }
import std.types { Int, NonEmptyStr, List }
import std.measure { ByteSize, byte_size, Second, second }
import extdeps.crypto.hash { sha256_digest }
import std.optional { Present }
import extdeps.boards.types { AmpereMtCollins }
import extdeps.firmware.types {
FirmwareReleaseRow, FirmwareTarget, FirmwareSemanticVersion,
BmcController, HostBios, ScpFirmware, MainboardCpld,
Expand Down Expand Up @@ -42,7 +42,7 @@ data mt_collins_firmware_delivery_authority: ExternalAuthority = ExternalAuthori
}

data mt_collins_bmc_0_45_3_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
board: AmpereMtCollins,
board: mt_collins_board_authority,
target: BmcController,
version: firmware_semantic_version(major: 0, minor: 45, patch: 3),
released_on: 1703635200000,
Expand All @@ -56,7 +56,7 @@ data mt_collins_bmc_0_45_3_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
}

data mt_collins_bios_0acod014_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
board: AmpereMtCollins,
board: mt_collins_board_authority,
target: HostBios,
version: firmware_semantic_version(major: 0, minor: 14, patch: 0),
released_on: 1702339200000,
Expand All @@ -70,7 +70,7 @@ data mt_collins_bios_0acod014_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
}

data mt_collins_scp_2_10_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
board: AmpereMtCollins,
board: mt_collins_board_authority,
target: ScpFirmware,
version: firmware_semantic_version(major: 2, minor: 10, patch: 0),
released_on: 1674691200000,
Expand All @@ -84,7 +84,7 @@ data mt_collins_scp_2_10_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
}

data mt_collins_mb_cpld_v06_hpm: FirmwareReleaseRow = FirmwareReleaseRow {
board: AmpereMtCollins,
board: mt_collins_board_authority,
target: MainboardCpld,
version: firmware_semantic_version(major: 6, minor: 0, patch: 0),
released_on: 1654560000000,
Expand Down
35 changes: 27 additions & 8 deletions dag/extdeps/bmc/access_profile.dag
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,11 @@ import extdeps.external_authority { ExternalAuthority, ExternalModelScope, Exter
import extdeps.uri { Uri, Https }
import std.credentials { FactoryLogin }
import extdeps.bmc.endpoint { BmcControllerEndpoint }
import extdeps.boards.types { BaseboardModel }
import extdeps.board_authority {
BoardAuthorityRef, BoardAuthorityBinding, BoardAuthorityLookup, BoardFruObservation,
board_authority_for, board_facts_authority, board_authority_ref_eq
}
import std.optional { Present, Absent }
import extdeps.bmc.capability { BmcFirmwareReleaseCapabilityRow, BmcFirmwareReleaseIdentity, bmc_firmware_release_identity_eq }
import extdeps.bmc.megarac { MegaRacImageRedirection }
import extdeps.bmc.redfish_virtual_media { RedfishVirtualMediaProbeReceipt }
Expand Down Expand Up @@ -82,7 +86,7 @@ type ChassisApplicability
| AllChassisVariants

type BmcAccessProfileKey {
baseboard: BaseboardModel
board: BoardAuthorityRef
chassis: ChassisApplicability
firmware: BmcFirmwareReleaseIdentity
}
Expand Down Expand Up @@ -147,7 +151,7 @@ fn bmc_access_profile_catalog_row_standing(row: BmcAccessProfileCatalogRow) -> B
// alone, so a same-version endpoint cannot be paired with an unrelated board's
// profile. The firmware is carried ONCE, here.
type BmcObservedIdentity {
baseboard: BaseboardModel
board: BoardFruObservation
chassis_part_number: NonEmptyStr?
firmware: BmcFirmwareReleaseIdentity
}
Expand Down Expand Up @@ -200,8 +204,17 @@ fn chassis_applicability_admits(applicability: ChassisApplicability, observed: N

// The profile key binds baseboard, chassis applicability, and exact release
// (family and raw vendor string). Equal firmware alone is not a binding.
fn bmc_access_profile_key_matches(key: BmcAccessProfileKey, identity: BmcObservedIdentity) -> Bool {
key.baseboard == identity.baseboard
// The board is the authority the host's OWN FRU reaches through the supplied bindings, and a profile
// imports board FACTS, so only an evidence-bound board matches.
fn bmc_observed_board_facts_authority(identity: BmcObservedIdentity, bindings: List<BoardAuthorityBinding>) -> BoardAuthorityRef? {
board_facts_authority(lookup: board_authority_for(observation: identity.board, bindings: bindings))
}

fn bmc_access_profile_key_matches(key: BmcAccessProfileKey, identity: BmcObservedIdentity, bindings: List<BoardAuthorityBinding>) -> Bool {
(match bmc_observed_board_facts_authority(identity: identity, bindings: bindings) {
Present { value: a } => board_authority_ref_eq(a: key.board, b: a)
Absent => false
})
&& chassis_applicability_admits(applicability: key.chassis, observed: identity.chassis_part_number)
&& bmc_firmware_release_identity_eq(a: key.firmware, b: identity.firmware)
}
Expand All @@ -211,6 +224,7 @@ fn bmc_access_profile_key_matches(key: BmcAccessProfileKey, identity: BmcObserve
// standings (gunbc.machine_intake_access), not arms here.
type BmcAccessProfileLookup
= AccessProfileKnown { profile: BmcAccessProfile, provenance: BmcAccessProfileProvenance }
| AccessProfileBoardNotFactsBound { observed_identity: BmcObservedIdentity, board: BoardAuthorityLookup }
| AccessProfileUncatalogued { observed_identity: BmcObservedIdentity }
| AccessProfileAmbiguous { observed_identity: BmcObservedIdentity, count: Int }
| AccessProfileCatalogRowRefused { standing: BmcAccessProfileCatalogRowStanding }
Expand Down Expand Up @@ -238,11 +252,14 @@ fn catalog_first_refused(catalog: List<BmcAccessProfileCatalogRow>) -> BmcAccess
fn bmc_access_profile_for(
identity: BmcObservedIdentity,
catalog: List<BmcAccessProfileCatalogRow>,
bindings: List<BoardAuthorityBinding>,
) -> BmcAccessProfileLookup {
match catalog_first_refused(catalog: catalog) {
Present { value: refused } => AccessProfileCatalogRowRefused { standing: refused }
Absent => {
let hits = catalog |> filter(row => bmc_access_profile_key_matches(key: row.profile.key, identity: identity))
Absent => match bmc_observed_board_facts_authority(identity: identity, bindings: bindings) {
Absent => AccessProfileBoardNotFactsBound { observed_identity: identity, board: board_authority_for(observation: identity.board, bindings: bindings) }
Present { value: _ } => {
let hits = catalog |> filter(row => bmc_access_profile_key_matches(key: row.profile.key, identity: identity, bindings: bindings))
let n = count(hits)
if n == 0 {
AccessProfileUncatalogued { observed_identity: identity }
Expand All @@ -255,6 +272,7 @@ fn bmc_access_profile_for(
} else {
AccessProfileAmbiguous { observed_identity: identity, count: n }
}
}
}
}
}
Expand All @@ -276,8 +294,9 @@ fn bmc_surface_eligibility(
profile: BmcAccessProfile,
observation: BmcAccessObservation,
surface: BmcAccessSurface,
bindings: List<BoardAuthorityBinding>,
) -> BmcSurfaceEligibility {
if bmc_access_profile_key_matches(key: profile.key, identity: observation.identity) == false {
if bmc_access_profile_key_matches(key: profile.key, identity: observation.identity, bindings: bindings) == false {
SurfaceProfileObservationIdentityMismatch { profile: profile.key, observed: observation.identity }
} else if bmc_surface_in(surfaces: profile.candidate_surfaces, surface: surface) == false {
SurfaceAbsentFromProfile
Expand Down
146 changes: 146 additions & 0 deletions dag/extdeps/board_authority.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,146 @@
module extdeps.board_authority

import std.decl_ref { DeclarationRef, WholeDeclaration, declaration_ref_eq }
import std.types { Bool, Int, List, NonEmptyStr }
import std.content_hash { Sha256Digest }
import v2.std.algebra { filter }
import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import extdeps.uri { Uri, Https }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.intel.com/content/dam/www/public/us/en/documents/specification-updates/ipmi-platform-mgt-fru-info-storage-def-v1-0-rev-1-3-spec-update.pdf"
}
}

data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.board_authority",
decl_name: "BoardFruIdentity",
field: WholeDeclaration
}
},
first_citation: extdeps_external_authority_anchor,
further_citations: []
}

// THE AGNOSTIC SHAPES OF "WHICH BOARD IS THIS HOST", and nothing else. This module enumerates no
// product (DESIGN section 3, External upstream decomposition): the board a host reports is the
// Board Area of its own FRU (Platform Management FRU Information Storage Definition, Board Area:
// manufacturer, product name, part number), and the board a consumer reasons about is an
// authority REFERENCE to the per-board subject module that owns that board's facts. Adding a board
// is a per-board module plus one binding row in the consumer layer, never an edit here. The rows
// and the table live in gunbc.board_authority_binding; this module owns only the shapes and the one
// fold that reads a table.
type BoardFruIdentity {
manufacturer: NonEmptyStr
product: NonEmptyStr
part_number: NonEmptyStr?
}

// WHY NO FRU BOARD AREA WAS READ. Never defaulted: a host whose board was not read is a different
// fact from a host whose board is read and unbound.
type BoardFruUnreadCause
= BoardAreaAbsent
| BoardAreaFieldsUnreadable

type BoardFruObservation
= BoardFruRead { fru: BoardFruIdentity }
| BoardFruNotRead { cause: BoardFruUnreadCause }

// A BOARD'S AUTHORITY IS THE DECLARATION OF ITS OWN SUBJECT. Equality is declaration_ref_eq, so two
// references agree exactly when they name the same declaration. Each per-board module exports its
// own reference; no consumer spells one.
type BoardAuthorityRef {
subject: DeclarationRef
}

fn board_authority_ref_eq(a: BoardAuthorityRef, b: BoardAuthorityRef) -> Bool {
declaration_ref_eq(a: a.subject, b: b.subject)
}

// WHAT JUSTIFIES THE EDGE, in the type so a consumer cannot read the strong standing off prose.
// BoundByNameOnly: the FRU's names agree with the subject's name and nothing else does; that is an
// inference from a name, typed as a bet with the discriminator that would settle it.
// BoundByObservedEvidence: an observation beyond the name (cited receipts) agrees with the
// subject's own cited facts.
type BoardBindingStanding
= BoundByNameOnly { discriminator_obligation: NonEmptyStr }
| BoundByObservedEvidence { first: DeclarationRef, further: List<DeclarationRef> }

// THE COMMITTED FRU READ the row was authored from: path and sha256 of the bytes.
type BoardFruReceipt {
artifact_path: NonEmptyStr
sha256: Sha256Digest
}

type BoardAuthorityBinding {
manufacturer: NonEmptyStr
product: NonEmptyStr
authority: BoardAuthorityRef
standing: BoardBindingStanding
fru_receipt: BoardFruReceipt
}

// IDENTITY-GRADE USES (keying a reading, pairing a reading with a board) accept either bound arm;
// USES THAT IMPORT BOARD FACTS (figures, profile routes) accept BoardEvidenceBound only.
type BoardAuthorityLookup
= BoardIdentityBound { authority: BoardAuthorityRef, discriminator_obligation: NonEmptyStr }
| BoardEvidenceBound { authority: BoardAuthorityRef, first: DeclarationRef, further: List<DeclarationRef> }
| BoardUnbound { fru: BoardFruIdentity }
| BoardAmbiguous { fru: BoardFruIdentity, count: Int }
| BoardNotRead { cause: BoardFruUnreadCause }

fn binding_names_fru(binding: BoardAuthorityBinding, fru: BoardFruIdentity) -> Bool {
binding.manufacturer == fru.manufacturer && binding.product == fru.product
}

fn bound_lookup_of(binding: BoardAuthorityBinding) -> BoardAuthorityLookup {
match binding.standing {
BoundByNameOnly { discriminator_obligation: o } => BoardIdentityBound { authority: binding.authority, discriminator_obligation: o }
BoundByObservedEvidence { first: f, further: r } => BoardEvidenceBound { authority: binding.authority, first: f, further: r }
}
}

// THE ONE TOTAL FOLD. Exact manufacturer and product; the part number is carried, not matched.
// Refuses on both sides of uniqueness; an unread board is never read as unbound.
fn board_authority_for(observation: BoardFruObservation, bindings: List<BoardAuthorityBinding>) -> BoardAuthorityLookup {
match observation {
BoardFruNotRead { cause: c } => BoardNotRead { cause: c }
BoardFruRead { fru: f } => {
let hits = bindings |> filter(b => binding_names_fru(binding: b, fru: f))
let n = count(hits)
if n == 0 {
BoardUnbound { fru: f }
} else if n == 1 {
fold(hits, init: BoardUnbound { fru: f }, f: (_acc, b) => bound_lookup_of(binding: b))
} else {
BoardAmbiguous { fru: f, count: n }
}
}
}
}

// The authority a lookup reached for an IDENTITY-GRADE use, absent when the board is not bound.
fn board_identity_authority(lookup: BoardAuthorityLookup) -> BoardAuthorityRef? {
match lookup {
BoardIdentityBound { authority: a, discriminator_obligation: _ } => Present { value: a }
BoardEvidenceBound { authority: a, first: _, further: _ } => Present { value: a }
BoardUnbound { fru: _ } => none
BoardAmbiguous { fru: _, count: _ } => none
BoardNotRead { cause: _ } => none
}
}

// The authority a lookup reached for a FACTS use: only the evidence-bound arm.
fn board_facts_authority(lookup: BoardAuthorityLookup) -> BoardAuthorityRef? {
match lookup {
BoardEvidenceBound { authority: a, first: _, further: _ } => Present { value: a }
BoardIdentityBound { authority: _, discriminator_obligation: _ } => none
BoardUnbound { fru: _ } => none
BoardAmbiguous { fru: _, count: _ } => none
BoardNotRead { cause: _ } => none
}
}
Loading
Loading