diff --git a/.github/workflows/fleet-converge.yml b/.github/workflows/fleet-converge.yml index 7900ff50b53..eed2319321b 100644 --- a/.github/workflows/fleet-converge.yml +++ b/.github/workflows/fleet-converge.yml @@ -10,10 +10,15 @@ on: required: true options: [srv1, srv2, srv3, srv4] type: choice + arrival_subject: + description: "arrival_converge only: the arrival-population unit (not executor host, not managed_host). Options are gunbc.machine_intake_arrival_subject arrival_converge_subject_options. Names signed off msg_f03558d1" + required: false + options: [mtjade1] + type: choice mode: description: "plan shows membership hunks; apply executes a prior plan artifact; org_actions_observe validates the org credential and refuses on runner-group drift; org_runner_roster_observe reads the organization's self-hosted runner registrations to exhaustion under the same token and refuses unless the roster is complete; app_control_plane_observe reads the gunbai-ci App registration and webhook config with a short-lived App JWT and refuses on hook-config drift; app_key_version_verify reads the gunbai-ci App private key at the EXACT Secret Manager version named by app_key_version, mints an installation token with it, and refuses unless GitHub accepts it and the key's rotation deadline has not passed -- no add, disable or destroy; runner_browser_toolchain_converge installs the declared Playwright/Chromium toolchain (apt host libraries as the administrator, digest-pinned node, Playwright and Chromium archives into the job user's root) on the selected host, which must be in the pool that runs the floor job, and refuses unless every digest, version and host library reads back and headless Chromium renders a local page; microvm_host_converge installs the cited Firecracker release on the selected host and reads the kvm grant back, refusing by name when the grant has not landed (the grant itself is applied by the full-host apply spine); microvm_network_apply stages the slot and host network files the model renders at the named expected_revision as root:root 0600 in a root-only directory over the fleet SSH edge as the host's ADMINISTRATOR, installs them with the modeled operations, reloads networkd, systemd-sysctl and the nft loader unit, and reads the ruleset back -- the job user is granted none of it, because install plus systemctl over content that principal can write is arbitrary root for any pull request; guest_image_observe reports the micro-VM base artifacts and their measured digests on the selected host and builds nothing; guest_image_converge builds the runner guest image there; microvm_boot_probe boots that image and reads its serial console; spark_grants and spark_bootstrap prepare the selected Spark; spark_serving_apply applies the promoted fabric groups' pair vLLM units over the password session, workers before heads; spark_native_serving_apply relaunches group B's native four-rank arm as ONE BOUNDED TRANSACTION -- an all-host preflight that mutates nothing and refuses on any unresolved artifact from an earlier run, the incumbent UNIT preserved (plus a diagnostic inspect of the incumbent container -- the container itself cannot outlive its unit, because these run --rm in the foreground under systemd), the head applied BEFORE the workers so every rank joins the head's new rendezvous store, then a readback of the COMPLETE realization through each container's own inspect -- every field the create spec states, the effective --node-rank off that container's argv, and NCCL's typed transport verdict on that incarnation -- plus the head's front door answering with this arm's served model, and then commit or a rollback of the whole arm -- and it is a separate mode because it reloads a 328 GB arm and nobody should reach it by asking for the pair units; spark_runtime_image_probe pulls the pinned runtime image on the selected Spark and reads its capabilities from inside its own digest, changing nothing; spark_wireless_link_converge reads the selected Spark's Wi-Fi power save (runtime via iw, persisted via the NetworkManager profile), link and kernel disconnect count, sets whichever realization differs from the declared intent, and refuses unless the readback decides Noop; spark_grants_observe reads every procured Spark's sudo grant listing as gunbc-automation and the bootstrap principal, and its sudoers drop-in shape, and writes nothing; spark_v41_checkpoint_materialize fetches the admitted published DeepSeek V4.1 files onto the selected Group A Spark (about 510 GB; spark_v41_row_store_encode encodes the eight Engram row stores from the verified shards on the selected Group A Spark and reads each store's sha256; spark_v41_row_store_readback reads those stores back at their header, first and last record and every rank seam, with the published source rows at the same rows, and writes nothing; spark_v41_engram_differential compares upstream's Engram lookup kernel with the design-B file-backed lookup over sampled real rows of every row store, byte for byte, and writes nothing; it states the requirement and refuses before fetching when the disk cannot hold it), publishes each only after its sha256 matches the manifest, leaves a present file with the right digest alone and refuses one with the wrong digest, and reads the storage-backed Engram spans from the verified shards; a transfer runs detached and a rerun reattaches; spark_v41_runtime_image_build PRODUCES the DeepSeek V4.1 image on the selected Spark -- it verifies the candidate's three FlashInfer wheels against the digests the candidate keys, converges the patched source tree, builds from it, reads the produced configuration digest back from inside the image through the probe route, and admits that digest against the candidate's own recipe, refusing a digest that does not recompute from it -- and it is a separate mode from the probe because it occupies one host for hours where the probe occupies it for minutes; spark_v41_runtime_image_distribute moves that produced image, named by the configuration digest its production receipt read back, from the host that receipt names to the selected Group A Spark -- save into its fabric blob root, pulled by the target straight over the fabric rail, load -- after stating its size against every filesystem a copy lands on, leaves a target already holding the digest untouched, refuses a target holding a different image under the tag, and refuses unless the target's image inspect Id reads back as that digest; spark_v41_group_a_launch reads the production image back under its tag on every Group A host, reads its registry inside its digest and every host's occupancy, and only when Group A is suspended for this candidate with every host held and vacant stages the Engram manifest and applies the V4.1 four-rank arm as one transaction at the capacity measurement's shape -- the target names only the session host; spark_v41_serving_load runs the shared serving-load runner against the V4.1 head (target must be srv6): one vllm bench serve step per capacity-measurement concurrency, metrics scraped around each, host pressure read on every Group A rank, and the staircase stop rules applied over the worst rank; it changes no unit and writes only its receipt; host_reset_return drives a rostered reset subject through its controller and measures the return FROM A PEER, and takes reset_observer rather than host because the observer must not be the subject; runner_host_file_observe reads the runner teardown drop-in, the needrestart deferral and the loaded teardown on the selected host as its administrator and writes nothing; runner_host_file_converge writes whichever of those two files differs, reloads systemd only if the drop-in changed, and refuses unless the manager then reports the declared teardown; microvm_controller_install writes the microVM slot controller's root-owned release locus (gunbc + sources + Firecracker + jailer) and the gunbc-microvm-slot@ template unit and the gunbc-microvm-slot-reserve broker unit on srv1 and starts neither; microvm_slot_reserve starts that broker unit once on srv1, which reserves the shakedown cell through the fabric broker route from inside the root process (slot, demand and offer derived from the model, never inputs), and uploads that invocation's reservation receipt, failing unless the reservation committed; microvm_slot_start starts the shakedown slot's controller unit once on srv1 (the instance is derived from the model, never an input), waits for it bounded by the unit's own stop timeout, and uploads that invocation's controller receipt; microvm_runner_group_ensure (srv1 only) reads the organization's runner groups and, only when the microvm-shakedown group is absent, files ONE operator approval, creates it restricted to the shakedown workflow on the default branch, and refuses unless the readback holds that restriction; mtcollins1_census_qemu_host_observe reads the selected host's KVM device and, under the job user's census QEMU root, the qemu-system-aarch64 build, its ldd libraries and the AAVMF images against their pins, and writes nothing; mtcollins1_census_qemu_toolchain_converge places that root as the job user (digest-pinned noble .debs unpacked with dpkg-deb -x, no apt, no Recommends) and refuses unless the same observe reads it ready; workspace_source_pack (host=srv1) enumerates the operator workspace as the job user, drops every path the credential exclusion row names and every build output, tars exactly the remainder, reads the archive back and refuses if any member is excluded, and puts it into the workspace bucket under its SHA-256, refusing by name when the runner cannot read a source root; workspace_checkpoint_measure (host=srv3, workspace_source_object = that SHA-256) refuses unless the job user's home is on btrfs, then times a read-only subvolume snapshot, a pinned kopia scan of it, the content-addressed chunk upload and the gated revision commit, and receipts every time with the 10 s / 60 s / 10 GB draft verdicts; workspace_checkpoint_restore (host=srv3) commits a small authored workspace, puts one chunk with no head advance, destroys the directory, restores it from the head closure and requires byte-equality with the uncommitted chunk absent -- both srv3 modes refuse their commit while the R2 head's CAS ground is uncited" required: true - options: [plan, launch_environment_plan, allocation_store_plan, workspace_commissioning_plan, apply, org_actions_observe, app_control_plane_observe, microvm_host_converge, microvm_network_observe, microvm_network_apply, guest_image_observe, guest_image_converge, microvm_boot_probe, spark_grants, spark_bootstrap, spark_serving_apply, spark_native_serving_apply, spark_runtime_image_probe, spark_wireless_link_converge, spark_grants_observe, spark_v41_checkpoint_materialize, spark_v41_row_store_encode, spark_v41_row_store_readback, spark_v41_engram_differential, spark_runtime_image_produce, spark_runtime_image_distribute, spark_arm_group_load, spark_arm_checkpoint_materialize, spark_arm_group_observe, spark_arm_group_launch_plan, spark_arm_group_launch, spark_v41_serving_load, dashboard_deploy, approval_broker_dark_install, microvm_controller_install, microvm_slot_reserve, microvm_slot_start, rlm_launch_deployment_receipt, host_reset_return, runner_host_file_observe, runner_host_file_converge, site_pxe_edge_observe, site_pxe_edge_converge, runner_password_session_tool_converge, runner_browser_toolchain_converge, r2_mint_preflight, r2_object_write_mint, org_runner_roster_observe, approval_keyring_converge, approval_device_enrolment_code_issue, mtcollins1_boot, mtcollins1_fan_observe, mtcollins1_ui_bundle_observe, mtcollins1_kvm_observer_observe, mtcollins1_census_image_publish, mtcollins1_census_member_readback, mtcollins1_census_qemu_host_observe, mtcollins1_census_qemu_toolchain_converge, host_credential_custody_converge, app_key_version_verify, r2_bucket_ensure, r2_bucket_admin_mint, r2_workspace_object_read_mint, r2_workspace_object_write_mint, r2_cache_object_read_mint, r2_cache_object_write_mint, r2_conditional_put_race_probe, workspace_source_pack, workspace_checkpoint_measure, workspace_checkpoint_restore, fabric_writer_identity_observe, pair_serving_d0, microvm_runner_group_ensure, gcp_iam_converge, namecheap_observe, printer] + options: [plan, launch_environment_plan, allocation_store_plan, workspace_commissioning_plan, apply, org_actions_observe, app_control_plane_observe, microvm_host_converge, microvm_network_observe, microvm_network_apply, guest_image_observe, guest_image_converge, microvm_boot_probe, spark_grants, spark_bootstrap, spark_serving_apply, spark_native_serving_apply, spark_runtime_image_probe, spark_wireless_link_converge, spark_grants_observe, spark_v41_checkpoint_materialize, spark_v41_row_store_encode, spark_v41_row_store_readback, spark_v41_engram_differential, spark_runtime_image_produce, spark_runtime_image_distribute, spark_arm_group_load, spark_arm_checkpoint_materialize, spark_arm_group_observe, spark_arm_group_launch_plan, spark_arm_group_launch, spark_v41_serving_load, dashboard_deploy, approval_broker_dark_install, microvm_controller_install, microvm_slot_reserve, microvm_slot_start, rlm_launch_deployment_receipt, host_reset_return, runner_host_file_observe, runner_host_file_converge, site_pxe_edge_observe, site_pxe_edge_converge, runner_password_session_tool_converge, runner_browser_toolchain_converge, r2_mint_preflight, r2_object_write_mint, org_runner_roster_observe, approval_keyring_converge, approval_device_enrolment_code_issue, mtcollins1_boot, mtcollins1_fan_observe, mtcollins1_ui_bundle_observe, mtcollins1_kvm_observer_observe, mtcollins1_census_image_publish, mtcollins1_census_member_readback, mtcollins1_census_qemu_host_observe, mtcollins1_census_qemu_toolchain_converge, host_credential_custody_converge, app_key_version_verify, r2_bucket_ensure, r2_bucket_admin_mint, r2_workspace_object_read_mint, r2_workspace_object_write_mint, r2_cache_object_read_mint, r2_cache_object_write_mint, r2_conditional_put_race_probe, workspace_source_pack, workspace_checkpoint_measure, workspace_checkpoint_restore, fabric_writer_identity_observe, pair_serving_d0, microvm_runner_group_ensure, gcp_iam_converge, namecheap_observe, arrival_converge, printer] type: choice target: description: "Spark target host for the spark_* modes, naming the administrator credential the run materializes (any rostered Spark: srv5, srv6, srv7, srv8, srv9, srv10, srv11, srv12); apply reads the subject off the plan artifact" @@ -145,7 +150,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Isolate toolchain dirs run: |- rm -rf "$RUNNER_TEMP/rustup" "$RUNNER_TEMP/cargo" @@ -616,7 +621,7 @@ jobs: runs-on: ${{ fromJSON(format('["self-hosted","linux","arm64","{0}"]', github.event.inputs.host)) }} needs: [build] timeout-minutes: 295 - if: github.event.inputs.mode != 'mtcollins1_boot' && github.event.inputs.mode != 'gcp_iam_converge' && github.event.inputs.mode != 'namecheap_observe' && github.event.inputs.mode != 'printer' + if: github.event.inputs.mode != 'mtcollins1_boot' && github.event.inputs.mode != 'gcp_iam_converge' && github.event.inputs.mode != 'namecheap_observe' && github.event.inputs.mode != 'arrival_converge' && github.event.inputs.mode != 'printer' permissions: contents: read actions: read @@ -629,7 +634,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Download release-bins artifact uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 with: @@ -2752,7 +2757,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Download release-bins artifact uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 with: @@ -2865,7 +2870,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Download release-bins artifact uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 with: @@ -2999,7 +3004,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Download release-bins artifact uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 with: @@ -3098,7 +3103,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Download release-bins artifact uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 with: @@ -3201,7 +3206,7 @@ jobs: uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 with: fetch-depth: 0 - ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} + ref: ${{ (github.event.inputs.mode == 'mtcollins1_boot' || github.event.inputs.mode == 'gcp_iam_converge' || github.event.inputs.mode == 'namecheap_observe' || github.event.inputs.mode == 'arrival_converge' || github.event.inputs.mode == 'printer') && github.sha || github.event.inputs.expected_revision || github.sha }} - name: Download release-bins artifact uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 with: @@ -3643,6 +3648,132 @@ jobs: compression-level: 0 if: success() timeout-minutes: 10 + arrival-converge: + runs-on: [self-hosted, linux, arm64, srv1] + needs: [build] + environment: mtjade1-arrival + timeout-minutes: 25 + if: github.event.inputs.mode == 'arrival_converge' + permissions: + contents: read + actions: read + id-token: write + concurrency: + group: gunbc-host-mutation-srv1 + cancel-in-progress: false + steps: + - name: Checkout (the event sha only; no dispatch input selects these bytes) + uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 + with: + fetch-depth: 0 + ref: ${{ github.sha }} + - name: Download release-bins artifact + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 + with: + name: release-bins + path: ${{ runner.temp }}/release-bins-download + timeout-minutes: 10 + - name: Verify the handed-off release bins against the build key, then promote and run --verify-build-artifacts (fail-closed) + id: release_bins + run: | + set -e + ROOT=$('git' 'rev-parse' '--show-toplevel') + '[' '-n' "$RELEASE_BINS_KEY" ']' || ('echo' '::error title=release-bins ConsumerKeyMissing::the build job published no release-bins key'; exit 1) + '[' '-f' "$RUNNER_TEMP"'/release-bins-download/release-bins.preimage' ']' || ('echo' '::error title=release-bins ConsumerFileMissing::the release-bins artifact is missing release-bins.preimage'; exit 1) + '[' '-f' "$RUNNER_TEMP"'/release-bins-download/release-bins.manifest' ']' || ('echo' '::error title=release-bins ConsumerFileMissing::the release-bins artifact is missing release-bins.manifest'; exit 1) + '[' '-f' "$RUNNER_TEMP"'/release-bins-download/release-bins.tgz' ']' || ('echo' '::error title=release-bins ConsumerFileMissing::the release-bins artifact is missing release-bins.tgz'; exit 1) + 'sha256sum' "$RUNNER_TEMP"'/release-bins-download/release-bins.preimage' > "$RUNNER_TEMP"'/DOWNLOADED_DIGEST.out' + DOWNLOADED_DIGEST=$('cut' '-d' ' ' '-f' '1' "$RUNNER_TEMP"'/DOWNLOADED_DIGEST.out') + '[' 'release-bins-'"$DOWNLOADED_DIGEST" '=' "$RELEASE_BINS_KEY" ']' || ('echo' '::error title=release-bins ConsumerPreimageKeyMismatch::the downloaded preimage does not hash to the build job'\''s key'; exit 1) + OBJECT_FORMAT=$('git' '-C' "$ROOT" 'rev-parse' '--show-object-format') + SOURCE_TREE=$('git' '-C' "$ROOT" 'rev-parse' 'HEAD^{tree}') + '[' '-n' "$OBJECT_FORMAT" ']' || ('echo' '::error title=release-bins AxisValueUnread::the key input OBJECT_FORMAT read back empty, so the key would not name the build; refusing to key'; exit 1) + '[' '-n' "$SOURCE_TREE" ']' || ('echo' '::error title=release-bins AxisValueUnread::the key input SOURCE_TREE read back empty, so the key would not name the build; refusing to key'; exit 1) + SOURCE_CLOSURE='tree:'"$OBJECT_FORMAT"':'"$SOURCE_TREE" + 'grep' '-qxF' 'source_closure='"$SOURCE_CLOSURE" "$RUNNER_TEMP"'/release-bins-download/release-bins.preimage' || ('echo' '::error title=release-bins ConsumerSourceTreeMismatch::the pack was keyed on a different source tree than this job'\''s checkout'; exit 1) + 'printf' '%s' 'claim_executor + gunbc + discover_source_root_ingest + claim_batch + interp_recorded_fixture_witness + v1_src_dag_parse + auth_declared_but_unwired_witness + bootstrap_witness + dag_collect_fingerprint_witness + diagnostics_witness + effects_rest_transport_witness + infer_semantics_witness + parse_witness + cssl_assemble + namespace_structural_root_exposure_generated_witness + codex_app_server_stdio_session + ' > "$RUNNER_TEMP"'/release-bins.roster' + 'tar' '-tzf' "$RUNNER_TEMP"'/release-bins-download/release-bins.tgz' > "$RUNNER_TEMP"'/pack-listing.out' + 'cmp' '-s' "$RUNNER_TEMP"'/pack-listing.out' "$RUNNER_TEMP"'/release-bins.roster' || ('echo' '::error title=release-bins PackListingNotRoster::the downloaded pack'\''s archive listing is not exactly the roster (an extra, duplicate, directory or escaping entry)'; exit 1) + 'cut' '-c' '67-' "$RUNNER_TEMP"'/release-bins-download/release-bins.manifest' > "$RUNNER_TEMP"'/manifest-names.out' + 'cmp' '-s' "$RUNNER_TEMP"'/manifest-names.out' "$RUNNER_TEMP"'/release-bins.roster' || ('echo' '::error title=release-bins ManifestRosterMismatch::the downloaded manifest does not name exactly the gunbc.ci_release_bins roster in order'; exit 1) + if 'grep' '-qvE' '^[0-9a-f]{64} [A-Za-z0-9_]+$' "$RUNNER_TEMP"'/release-bins-download/release-bins.manifest'; then ('echo' '::error title=release-bins ManifestMalformed::the downloaded manifest has a line that is not one well-formed sha256 record for a roster member'; exit 1); fi + 'rm' '-rf' "$RUNNER_TEMP"'/release-bins-check' + 'mkdir' '-p' "$RUNNER_TEMP"'/release-bins-check' + 'tar' '-xzf' "$RUNNER_TEMP"'/release-bins-download/release-bins.tgz' '-C' "$RUNNER_TEMP"'/release-bins-check' '--no-same-owner' + 'printf' '%s' 'claim_executor:regular file:1 + gunbc:regular file:1 + discover_source_root_ingest:regular file:1 + claim_batch:regular file:1 + interp_recorded_fixture_witness:regular file:1 + v1_src_dag_parse:regular file:1 + auth_declared_but_unwired_witness:regular file:1 + bootstrap_witness:regular file:1 + dag_collect_fingerprint_witness:regular file:1 + diagnostics_witness:regular file:1 + effects_rest_transport_witness:regular file:1 + infer_semantics_witness:regular file:1 + parse_witness:regular file:1 + cssl_assemble:regular file:1 + namespace_structural_root_exposure_generated_witness:regular file:1 + codex_app_server_stdio_session:regular file:1 + ' > "$RUNNER_TEMP"'/member-types.expected' + ('cd' "$RUNNER_TEMP"'/release-bins-check' && 'stat' '-c' '%n:%F:%h' 'claim_executor' 'gunbc' 'discover_source_root_ingest' 'claim_batch' 'interp_recorded_fixture_witness' 'v1_src_dag_parse' 'auth_declared_but_unwired_witness' 'bootstrap_witness' 'dag_collect_fingerprint_witness' 'diagnostics_witness' 'effects_rest_transport_witness' 'infer_semantics_witness' 'parse_witness' 'cssl_assemble' 'namespace_structural_root_exposure_generated_witness' 'codex_app_server_stdio_session') > "$RUNNER_TEMP"'/member-types.out' + 'cmp' '-s' "$RUNNER_TEMP"'/member-types.out' "$RUNNER_TEMP"'/member-types.expected' || ('diff' "$RUNNER_TEMP"'/member-types.expected' "$RUNNER_TEMP"'/member-types.out' || ':' 'no-op'; ('echo' '::error title=release-bins MemberNotRegularFile::the downloaded pack has a member that is not a self-contained regular file (a link, special file or hard-link dependency; the report above names it)'; exit 1)) + ('cd' "$RUNNER_TEMP"'/release-bins-check' && 'find' 'claim_executor' 'gunbc' 'discover_source_root_ingest' 'claim_batch' 'interp_recorded_fixture_witness' 'v1_src_dag_parse' 'auth_declared_but_unwired_witness' 'bootstrap_witness' 'dag_collect_fingerprint_witness' 'diagnostics_witness' 'effects_rest_transport_witness' 'infer_semantics_witness' 'parse_witness' 'cssl_assemble' 'namespace_structural_root_exposure_generated_witness' 'codex_app_server_stdio_session' '-maxdepth' '0' '!' '-perm' '-u+x') > "$RUNNER_TEMP"'/member-nonexec.out' + '[' '!' '-s' "$RUNNER_TEMP"'/member-nonexec.out' ']' || ('cat' "$RUNNER_TEMP"'/member-nonexec.out'; ('echo' '::error title=release-bins MemberNotExecutable::the downloaded pack has a member that is not executable (listed above)'; exit 1)) + ('cd' "$RUNNER_TEMP"'/release-bins-check' && 'sha256sum' '--strict' '--quiet' '-c' "$RUNNER_TEMP"'/release-bins-download/release-bins.manifest') || ('echo' '::error title=release-bins MemberDigestMismatch::the downloaded member bytes do not match the manifest under strict checking; refusing before any member is promoted or run'; exit 1) + 'mkdir' '-p' "$ROOT"'/target/release' + ('cd' "$ROOT"'/target/release' && 'rm' '-f' 'claim_executor' 'gunbc' 'discover_source_root_ingest' 'claim_batch' 'interp_recorded_fixture_witness' 'v1_src_dag_parse' 'auth_declared_but_unwired_witness' 'bootstrap_witness' 'dag_collect_fingerprint_witness' 'diagnostics_witness' 'effects_rest_transport_witness' 'infer_semantics_witness' 'parse_witness' 'cssl_assemble' 'namespace_structural_root_exposure_generated_witness' 'codex_app_server_stdio_session') + ('cd' "$RUNNER_TEMP"'/release-bins-check' && 'cp' '-p' 'claim_executor' 'gunbc' 'discover_source_root_ingest' 'claim_batch' 'interp_recorded_fixture_witness' 'v1_src_dag_parse' 'auth_declared_but_unwired_witness' 'bootstrap_witness' 'dag_collect_fingerprint_witness' 'diagnostics_witness' 'effects_rest_transport_witness' 'infer_semantics_witness' 'parse_witness' 'cssl_assemble' 'namespace_structural_root_exposure_generated_witness' 'codex_app_server_stdio_session' "$ROOT"'/target/release/') + 'rm' '-rf' "$RUNNER_TEMP"'/release-bins-check' + "$ROOT"'/target/release/claim_executor' '--verify-build-artifacts' "$ROOT"'/target/release/claim_executor' "$ROOT"'/target/release/gunbc' "$ROOT"'/target/release/discover_source_root_ingest' "$ROOT"'/target/release/claim_batch' "$ROOT"'/target/release/interp_recorded_fixture_witness' "$ROOT"'/target/release/v1_src_dag_parse' "$ROOT"'/target/release/auth_declared_but_unwired_witness' "$ROOT"'/target/release/bootstrap_witness' "$ROOT"'/target/release/dag_collect_fingerprint_witness' "$ROOT"'/target/release/diagnostics_witness' "$ROOT"'/target/release/effects_rest_transport_witness' "$ROOT"'/target/release/infer_semantics_witness' "$ROOT"'/target/release/parse_witness' "$ROOT"'/target/release/cssl_assemble' "$ROOT"'/target/release/namespace_structural_root_exposure_generated_witness' "$ROOT"'/target/release/codex_app_server_stdio_session' + env: + RELEASE_BINS_KEY: ${{ needs.build.outputs.release_bins_key }} + timeout-minutes: 5 + - name: "Arrival admission (credential-free): store host srv1 and a population arrival_subject" + id: arrival_admit + run: |- + ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd) + "$ROOT/target/release/gunbc" run --source-root "$ROOT/dag" --source-root "$ROOT/src/v2" --entry dag/gunbc/machine_intake/arrival_admission.dag --function arrival_admit_executor + env: + FLEET_CONVERGE_EXPECTED_HOST: ${{ github.event.inputs.host }} + FLEET_CONVERGE_ARRIVAL_SUBJECT: ${{ github.event.inputs.arrival_subject }} + timeout-minutes: 5 + - name: WIF auth (OIDC -> dedicated mtjade1-arrival pool -> mtjade1-arrival SA, access token only) + id: wif_auth + uses: google-github-actions/auth@7c6bc770dae815cd3e89ee6cdf493a5fab2cc093 + with: + workload_identity_provider: projects/582015116396/locations/global/workloadIdentityPools/github-mtjade1-arrival/providers/github-mtjade1-arrival-oidc + service_account: mtjade1-arrival@gunbai-secrets.iam.gserviceaccount.com + token_format: access_token + create_credentials_file: false + timeout-minutes: 5 + - name: arrival_converge under the standing grant and arrival interlock + id: arrival_converge + run: |- + ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd) + "$ROOT/target/release/gunbc" run --source-root "$ROOT/dag" --source-root "$ROOT/src/v2" --entry dag/gunbc/machine_intake/arrival_run.dag --function arrival_converge_wet + env: + WIF_ACCESS_TOKEN: ${{ steps.wif_auth.outputs.access_token }} + FLEET_CONVERGE_EXPECTED_HOST: ${{ github.event.inputs.host }} + FLEET_CONVERGE_ARRIVAL_SUBJECT: ${{ github.event.inputs.arrival_subject }} + timeout-minutes: 5 printer: runs-on: [self-hosted, linux, arm64, srv1] needs: [build] diff --git a/dag/gunbc/actions_run_binding.dag b/dag/gunbc/actions_run_binding.dag index 23f2d4513af..c0359b002c5 100644 --- a/dag/gunbc/actions_run_binding.dag +++ b/dag/gunbc/actions_run_binding.dag @@ -98,6 +98,8 @@ data rlm_expected_revision_env_name: String = "RLM_EXPECTED_REVISION" data fleet_converge_expected_host_env_name: String = "FLEET_CONVERGE_EXPECTED_HOST" +data fleet_converge_arrival_subject_env_name: String = "FLEET_CONVERGE_ARRIVAL_SUBJECT" + type ExpectedRevisionRead = ExpectedRevisionPresent { revision: String } | ExpectedRevisionAbsent { variable: String, detail: String } diff --git a/dag/gunbc/auth/authorization_pattern_selection.dag b/dag/gunbc/auth/authorization_pattern_selection.dag index da59ed22db3..f7dc7a2e687 100644 --- a/dag/gunbc/auth/authorization_pattern_selection.dag +++ b/dag/gunbc/auth/authorization_pattern_selection.dag @@ -111,14 +111,14 @@ type BillingConsequence // (gunbc.auth.privileged_effect_census rulings_without_a_rostered_interlock), and the site's // realization must take that hold before any write. // -// THREE INTERLOCK STATES, NOT AN OPTIONAL HOLD. InterlockPending is a hold not yet named: it must +// TWO INTERLOCK STATES, NOT AN OPTIONAL HOLD. InterlockPending is a hold not yet named: it must // refuse, never discharge (a bindable irreversible effect under a pending ruling still owes a -// witness). UnconditionalStanding is an intentional no-hold discharge, with its reason. InterlockedBy -// is a named hold the census must roster against the site. Only UnconditionalStanding and -// InterlockedBy discharge the irreversibility ground. +// witness). InterlockedBy is a named hold the census must roster against the site; only that arm +// discharges the irreversibility ground. A grant arm that writes BMC credentials must be InterlockedBy +// the grounded Apply admission (admit_rotation_apply), never pending. Route A overlays that hold per +// arm (standing_grant_arm_interlock); grant grain may stay InterlockPending for unnamed classes. type StandingRulingInterlock = InterlockPending { obligation: NonEmptyStr } - | UnconditionalStanding { reason: NonEmptyStr } | InterlockedBy { hold: DeclarationRef } type StandingDestructiveAuthorization { @@ -130,7 +130,6 @@ type StandingDestructiveAuthorization { fn standing_ruling_discharges_irreversibility(r: StandingDestructiveAuthorization) -> Bool { match r.interlock { InterlockPending { obligation: _ } => false - UnconditionalStanding { reason: _ } => true InterlockedBy { hold: _ } => true } } @@ -574,7 +573,6 @@ fn minted_reach_text(m: MintedCredentialReach) -> String { fn standing_ruling_interlock_label(r: StandingDestructiveAuthorization) -> String { match r.interlock { InterlockPending { obligation: o } => join(["InterlockPending: ", o as String], "") - UnconditionalStanding { reason: s } => join(["UnconditionalStanding: ", s as String], "") InterlockedBy { hold: i } => declaration_ref_display_key(ref: i) } } diff --git a/dag/gunbc/auth/gcp_iam_converge.dag b/dag/gunbc/auth/gcp_iam_converge.dag index 36d35e1839f..e21e80c37d2 100644 --- a/dag/gunbc/auth/gcp_iam_converge.dag +++ b/dag/gunbc/auth/gcp_iam_converge.dag @@ -30,6 +30,7 @@ import gunbc.namecheap.federation_provision { namecheap_dedicated_federation } import gunbc.native_product_federation { native_product_federations } import gunbc.auth.fleet_convergence_federation { fleet_convergence_federation } import gunbc.auth.managed_host_boot_federation_provision { boot_dedicated_federation } +import gunbc.auth.mtjade1_arrival_federation_provision { mtjade1_arrival_dedicated_federation } import gunbc.auth.managed_host_boot_federation { pinned_version_accessor_grant_for, provisioned_boot_federations } import gunbc.auth.approval_request_submission { approval_submission_mac_key_secret_ref } import gunbc.cloudflare.r2_mint_secret_access { r2_mint_custody_grants } @@ -219,7 +220,10 @@ data gcp_iam_converge_targets: List = concat( [heal_publisher_dedicated_federation(), private_heal_publisher_dedicated_federation()], map(provisioned_boot_federations(), f => boot_dedicated_federation(f: f)), ), - concat([namecheap_dedicated_federation(), fleet_convergence_federation(), printer_dedicated_federation()], native_product_federations()), + concat( + concat([namecheap_dedicated_federation(), fleet_convergence_federation(), printer_dedicated_federation()], native_product_federations()), + [mtjade1_arrival_dedicated_federation()], + ), ) fn service_account_resource(email: ServiceAccountEmail) -> String { diff --git a/dag/gunbc/auth/mtjade1_arrival_federation.dag b/dag/gunbc/auth/mtjade1_arrival_federation.dag new file mode 100644 index 00000000000..c17be2fd37e --- /dev/null +++ b/dag/gunbc/auth/mtjade1_arrival_federation.dag @@ -0,0 +1,48 @@ +module gunbc.auth.mtjade1_arrival_federation + +import std.types { NonEmptyStr } +import gunbc.auth.mtjade1_arrival_pair { mtjade1_arrival_principal_member } +import gunbc.auth.authorization_pattern_selection { + PrivilegedEffect, ApiSurface, WorkloadIdentityBindable, WorkloadIdentityStanding, + MintsNoCredential, IrreversibleEffect, ReversibleByReapply, + NoBillingConsequence, StandingRulingUnderInterlock, +} +import std.human_intervention { DeviceOnce } +import gunbc.auth.standing_operator_grant { + mtjade1_live_standing_grant, StandingJadeArrivalArchive, StandingJadeFirmwareQualification, + standing_ruling_with_arm_interlock, +} + +fn mtjade1_arrival_bindable_identity() -> WorkloadIdentityStanding { + WorkloadIdentityBindable { member: mtjade1_arrival_principal_member() as NonEmptyStr } +} + +fn mtjade1_arrival_archive_effect() -> PrivilegedEffect { + PrivilegedEffect { + subject: "mtjade1 PriorLifeBoundary archive: content-addressed evidence of BMC carriers, cursor derived from the archive, nothing cleared" as NonEmptyStr, + frequency: DeviceOnce, + reversibility: ReversibleByReapply, + surface: ApiSurface, + workload_identity: mtjade1_arrival_bindable_identity(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: StandingRulingUnderInterlock { + ruling: standing_ruling_with_arm_interlock(g: mtjade1_live_standing_grant, e: StandingJadeArrivalArchive), + }, + } +} + +fn mtjade1_arrival_firmware_qualification_effect() -> PrivilegedEffect { + PrivilegedEffect { + subject: "mtjade1 MegaRAC per-build operation qualification write under the arrival job principal" as NonEmptyStr, + frequency: DeviceOnce, + reversibility: IrreversibleEffect { what_is_lost: "a controller write at a firmware build is not undone by a reapply of a different build's evidence" as NonEmptyStr }, + surface: ApiSurface, + workload_identity: mtjade1_arrival_bindable_identity(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: StandingRulingUnderInterlock { + ruling: standing_ruling_with_arm_interlock(g: mtjade1_live_standing_grant, e: StandingJadeFirmwareQualification), + }, + } +} diff --git a/dag/gunbc/auth/mtjade1_arrival_federation_provision.dag b/dag/gunbc/auth/mtjade1_arrival_federation_provision.dag new file mode 100644 index 00000000000..b0a6fec1192 --- /dev/null +++ b/dag/gunbc/auth/mtjade1_arrival_federation_provision.dag @@ -0,0 +1,27 @@ +module gunbc.auth.mtjade1_arrival_federation_provision + +import gunbc.auth.heal_publisher_provision { DedicatedFederation } +import gunbc.auth.mtjade1_arrival_pair { + mtjade1_arrival_pool_id, mtjade1_arrival_pool_display_name, mtjade1_arrival_provider_id, + mtjade1_arrival_wif_attribute_mapping, mtjade1_arrival_claim_pins, mtjade1_arrival_principal_set, + mtjade1_arrival_service_account, mtjade1_arrival_service_account_id, mtjade1_arrival_principal_member, + mtjade1_arrival_secret_grants, +} +import gunbc.auth.oidc_claim_pins { claim_pins_attribute_condition } + +fn mtjade1_arrival_dedicated_federation() -> DedicatedFederation { + DedicatedFederation { + label: "mtjade1 arrival federation", + pool_id: mtjade1_arrival_pool_id, + pool_display_name: mtjade1_arrival_pool_display_name, + provider_id: mtjade1_arrival_provider_id, + attribute_mapping: mtjade1_arrival_wif_attribute_mapping, + attribute_condition: claim_pins_attribute_condition(pins: mtjade1_arrival_claim_pins()), + principal_set: mtjade1_arrival_principal_set(), + service_account: mtjade1_arrival_service_account, + service_account_id: mtjade1_arrival_service_account_id, + service_account_display_name: "Mt. Jade arrival (one job)", + service_account_member: mtjade1_arrival_principal_member(), + secret_grants: mtjade1_arrival_secret_grants(), + } +} diff --git a/dag/gunbc/auth/mtjade1_arrival_pair.dag b/dag/gunbc/auth/mtjade1_arrival_pair.dag new file mode 100644 index 00000000000..c021e3233ca --- /dev/null +++ b/dag/gunbc/auth/mtjade1_arrival_pair.dag @@ -0,0 +1,76 @@ +module gunbc.auth.mtjade1_arrival_pair + +import std.types { List, Map, NonEmptyStr, String } +import std.optional { Present } +import extdeps.cloud.gcp.gcp { + ServiceAccountEmail, WifPool, WifProvider, wif_provider_resource, wif_pool_resource, +} +import gunbc.auth.github_gcp_federation { + fleet_secrets_project_id, fleet_secrets_project_number, github_wif_issuer_uri, federated_service_account_member, +} +import gunbc.auth.gcp_secret_access { SecretAccessGrant } +import gunbc.auth.managed_host_boot_federation { pinned_version_accessor_grant_for } +import gunbc.auth.oidc_claim_pins { OidcClaimPin, claim_pins_attribute_condition, fleet_converge_job_claim_pins } +import gunbc.secret_provision { mtjade1_bmc_gunbc_arrival_accessor_ref } + +// Names, WIF pair and the one version-pinned accessor. PrivilegedEffect rows live in +// gunbc.auth.mtjade1_arrival_federation so gcp-iam-converge and fleet-converge.yml do not +// close over the selection fold. + +data mtjade1_arrival_pool_id: NonEmptyStr = "github-mtjade1-arrival" +data mtjade1_arrival_pool_display_name: NonEmptyStr = "Mt. Jade arrival (one job)" +data mtjade1_arrival_provider_id: NonEmptyStr = "github-mtjade1-arrival-oidc" +data mtjade1_arrival_service_account_id: NonEmptyStr = "mtjade1-arrival" +data mtjade1_arrival_service_account: ServiceAccountEmail = "mtjade1-arrival@gunbai-secrets.iam.gserviceaccount.com" +data mtjade1_arrival_environment: NonEmptyStr = "mtjade1-arrival" + +data mtjade1_arrival_wif_pool: WifPool = WifPool { + name: mtjade1_arrival_pool_id + project: fleet_secrets_project_id as String + display_name: Present { value: mtjade1_arrival_pool_display_name } + disabled: false +} + +fn mtjade1_arrival_claim_pins() -> List { + fleet_converge_job_claim_pins(environment: mtjade1_arrival_environment) +} + +data mtjade1_arrival_wif_attribute_mapping: Map = { + "google.subject": "assertion.sub", + "attribute.repository_id": "assertion.repository_id", + "attribute.workflow_ref": "assertion.workflow_ref" +} + +fn mtjade1_arrival_wif_provider() -> WifProvider { + WifProvider { + name: mtjade1_arrival_provider_id + pool: mtjade1_arrival_pool_id + issuer_uri: github_wif_issuer_uri + attribute_mapping: Present { value: mtjade1_arrival_wif_attribute_mapping } + attribute_condition: Present { value: claim_pins_attribute_condition(pins: mtjade1_arrival_claim_pins()) } + } +} + +fn mtjade1_arrival_provider_resource() -> String { + wif_provider_resource(project_number: fleet_secrets_project_number, provider: mtjade1_arrival_wif_provider()) +} + +fn mtjade1_arrival_principal_set() -> String { + join([ + "principalSet://iam.googleapis.com/", + wif_pool_resource(project_number: fleet_secrets_project_number, pool_id: mtjade1_arrival_pool_id as String), + "/*" + ], "") +} + +fn mtjade1_arrival_principal_member() -> String { + federated_service_account_member(email: mtjade1_arrival_service_account) +} + +fn mtjade1_arrival_secret_grants() -> List { + [pinned_version_accessor_grant_for( + title_prefix: "mtjade1-arrival", + description: "gunbc.auth.mtjade1_arrival_pair: the one version the arrival job may read for BmcSecure (signed off msg_f03558d1)", + target: mtjade1_bmc_gunbc_arrival_accessor_ref, + )] +} diff --git a/dag/gunbc/auth/privileged_effect_census.dag b/dag/gunbc/auth/privileged_effect_census.dag index d6e24a2d7a4..20c75e5a662 100644 --- a/dag/gunbc/auth/privileged_effect_census.dag +++ b/dag/gunbc/auth/privileged_effect_census.dag @@ -2,7 +2,13 @@ module gunbc.auth.privileged_effect_census import gunbc.fleet.printer_federation {printer_service_account} import gunbc.auth.github_gcp_federation {federated_service_account_member} -import gunbc.auth.standing_operator_grant { group_a_dev_standing_grant } +import gunbc.auth.standing_operator_grant { + group_a_dev_standing_grant, mtjade1_live_standing_grant, + StandingBmcSecureAccountWrite, standing_ruling_with_arm_interlock, +} +import gunbc.auth.mtjade1_arrival_federation { + mtjade1_arrival_archive_effect, mtjade1_arrival_firmware_qualification_effect, +} import std.types { Bool, List, NonEmptyStr, String } import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_in_list, declaration_ref_eq } import std.dissolution { @@ -26,7 +32,7 @@ import gunbc.auth.authorization_pattern_selection { ReversibleByReapply, IrreversibleEffect, BillsExternally, NoBillingConsequence, WitnessDischarge, NoWitnessDischarge, StandingRulingUnderInterlock, StandingDestructiveAuthorization, - InterlockPending, UnconditionalStanding, InterlockedBy, + InterlockPending, InterlockedBy, StandingRulingInterlock, AuthorizationPattern, FederatedScopedGrant, OperatorApprovedCapability, HumanOnlyStep, OperatorOwnSession, PastedOperatorToken, AuthorizationPatternSelection, PatternSelected, ManualStepRequired, NoAdmissiblePattern, @@ -333,24 +339,29 @@ fn route_qualification_channel_access_effect() -> PrivilegedEffect { } } -// BMCSECURE ACCOUNT ROTATION (cut O1b). The Apply arm of the state-shaped BmcSecure: set the managed -// account to a stored and exact-fetched generation and retire the published account to a break-glass -// generation, each write over a route admitted by admit_rotation_apply. IRREVERSIBLE, AND SAID SO: the -// value each write replaces is gone, and the published factory value is not restorable by a reapply -// (artifacts/bmc/mtcollins1-user2-retire-2026-09-13.txt). One controller's accounts, so its reach is one -// resource. No dispatched run carries it: in this cut it is modeled, with a dry realization only, and -// the plan mint takes an operator-approved capability (gunbc.auth.approval_broker Redemption) per write, -// bound to the exact controller, build and request. +// BMCSECURE ACCOUNT ROTATION (cut O1b, discharge O1c-3). The Apply arm of the state-shaped BmcSecure: +// set the managed account to a stored and exact-fetched generation and retire the published account +// to a break-glass generation, each write over a route admitted by admit_rotation_apply. +// IRREVERSIBLE, AND SAID SO: the value each write replaces is gone, and the published factory value is +// not restorable by a reapply (artifacts/bmc/mtcollins1-user2-retire-2026-09-13.txt). One controller's +// accounts, so its reach is one resource. arrival_converge_wet federates the archive door; it does +// not invoke BmcSecure Apply, so this effect stays WorkloadIdentityUnbindable. Irreversibility is +// discharged by the mtjade1 live-ops standing ruling's StandingBmcSecureAccountWrite arm (InterlockedBy +// admit_rotation_apply via standing_ruling_with_arm_interlock), not grant-grain InterlockPending. +// A write still needs a grounded route. Operator-approved capability remains the selected pattern +// while the workload identity is unbindable, and is the fallback when the grant does not cover the host. fn bmc_secure_account_rotation_effect() -> PrivilegedEffect { PrivilegedEffect { subject: "rotate a BMC's managed account to a stored generation and retire its published account, over admitted routes on one controller at one firmware build" as NonEmptyStr, frequency: DeviceOnce, reversibility: IrreversibleEffect { what_is_lost: "each account write replaces the value it overwrites; the published factory value is not restored by a reapply" as NonEmptyStr }, surface: ApiSurface, - workload_identity: WorkloadIdentityUnbindable { cause: "no dispatched run carries the BmcSecure account rotation; in cut O1b it is modeled with a dry realization only" as NonEmptyStr }, + workload_identity: WorkloadIdentityUnbindable { cause: "arrival_converge_wet does not invoke BmcSecure Apply; account rotation stays capability-selected until a held writer lands in that door" as NonEmptyStr }, minted_reach: MintsResourceScopedCredential, billing: NoBillingConsequence, - witness_discharge: NoWitnessDischarge, + witness_discharge: StandingRulingUnderInterlock { + ruling: standing_ruling_with_arm_interlock(g: mtjade1_live_standing_grant, e: StandingBmcSecureAccountWrite), + }, } } @@ -363,12 +374,19 @@ fn bmc_secure_account_rotation_effect() -> PrivilegedEffect { // active hold. type PrivilegedEffectInterlock { site: DeclarationRef - hold: DeclarationRef + hold: DeclarationRef? refusal: DeclarationRef premise: NonEmptyStr hold_owning_roots: List } +fn privileged_effect_interlock_hold(interlock: StandingRulingInterlock) -> DeclarationRef? { + match interlock { + InterlockedBy { hold: i } => Present { value: i } + InterlockPending { obligation: _ } => none + } +} + // EVERY PRODUCTION ROOT THAT REACHES A GATED WRITE ON THE UNIT, and the live acquire it owns. The set // is closed by the compiler rather than by this list: the BMC write wrappers take a sole_constructor // UnitHoldProof, and the generic operations beneath them are admit_callers-sealed to the callers named @@ -411,38 +429,64 @@ data mtcollins1_hold_owning_roots: List = [ data privileged_effect_interlocks: List = [ PrivilegedEffectInterlock { site: site(module_path: "gunbc.spark.pair_serving_d0_door", decl_name: "d0_standing_grant_for"), - hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant"), + hold: privileged_effect_interlock_hold(interlock: group_a_dev_standing_grant.ruling.interlock), refusal: site(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_decide_release"), premise: "the release runs only under D0's durable claim of the consent slot and its pending state, and refuses (D0HostNotQuiescent) unless a fresh reading taken at filing time finds every host quiescent; an unanswering host refuses as unobserved" as NonEmptyStr, hold_owning_roots: [] as List, }, PrivilegedEffectInterlock { site: site(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_wet"), - hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), + hold: privileged_effect_interlock_hold(interlock: mtcollins1_operator_ruling.interlock), refusal: site(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"), premise: "the boot takes the unit's one durable exclusive hold before any BMC write and refuses FileHoldOccupied naming the holder" as NonEmptyStr, hold_owning_roots: mtcollins1_hold_owning_roots, }, PrivilegedEffectInterlock { site: site(module_path: "gunbc.host_reset_return_run", decl_name: "host_reset_return_wet"), - hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), + hold: privileged_effect_interlock_hold(interlock: mtcollins1_operator_ruling.interlock), refusal: site(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"), premise: "host reset-return takes the same unit hold before it sets the boot device or power-cycles the unit" as NonEmptyStr, hold_owning_roots: mtcollins1_hold_owning_roots, }, + PrivilegedEffectInterlock { + site: site(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "plan_bmc_account_action"), + hold: Present { value: decl_ref(module_path: "gunbc.machine_intake_bmc_rotation_route", decl_name: "admit_rotation_apply") }, + refusal: site(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "grant_discharges_bmc_secure_account_write"), + premise: "BmcSecure Apply discharges the mtjade1 standing ruling only when admit_rotation_apply is rostered against this site; InterlockPending never discharges, and a named hold that is not this site's rostered interlock does not discharge" as NonEmptyStr, + hold_owning_roots: [] as List, + }, + PrivilegedEffectInterlock { + site: site(module_path: "gunbc.auth.mtjade1_arrival_federation", decl_name: "mtjade1_arrival_archive_effect"), + hold: Present { value: decl_ref(module_path: "gunbc.machine_intake_arrival_interlock", decl_name: "arrival_archive_slot_acquire") }, + refusal: site(module_path: "gunbc.machine_intake_arrival_interlock", decl_name: "arrival_archive_slot_acquire"), + premise: "the wet arrival door takes the subject's exclusive slot (file_hold_acquire) and, while ArrivalArchiveSlotHeld, calls arrival_wet_prefix_from_unobserved_world which refuses; it does not fold converge_mtjade1_arrival_prefix or write the prior-life archive until an observed BMC/archive world is bound" as NonEmptyStr, + hold_owning_roots: [ + InterlockRoot { + root: site(module_path: "gunbc.machine_intake_arrival_run", decl_name: "arrival_converge_wet"), + acquires_at: site(module_path: "gunbc.machine_intake_arrival_interlock", decl_name: "arrival_archive_slot_acquire"), + operations: ["typed refusal of unobserved PriorLifeBoundary" as NonEmptyStr], + sealed_by: [ + site(module_path: "gunbc.machine_intake_arrival_interlock", decl_name: "arrival_archive_slot_release"), + ], + }, + ], + }, ] // A STANDING RULING IS HONORED ONLY BESIDE ITS INTERLOCK. InterlockPending never discharges and is -// always a defect. UnconditionalStanding discharges without a rostered hold. InterlockedBy discharges -// only when that hold is rostered against the same site. +// always a defect. InterlockedBy discharges only when that hold is rostered against the same site. fn ruling_interlock_is_rostered(site_ref: DeclarationRef, interlock: DeclarationRef) -> Bool { - any(privileged_effect_interlocks, i => declaration_ref_eq(a: i.site, b: site_ref) && declaration_ref_eq(a: i.hold, b: interlock)) + any(privileged_effect_interlocks, i => + declaration_ref_eq(a: i.site, b: site_ref) + && match i.hold { + Present { value: h } => declaration_ref_eq(a: h, b: interlock) + Absent => false + }) } fn ruling_discharge_interlock_defect(site_ref: DeclarationRef, ruling: StandingDestructiveAuthorization) -> DeclarationRef? { match ruling.interlock { InterlockPending { obligation: _ } => Present { value: site_ref } - UnconditionalStanding { reason: _ } => none InterlockedBy { hold: i } => if ruling_interlock_is_rostered(site_ref: site_ref, interlock: i) { none } else { Present { value: site_ref } } } @@ -515,6 +559,16 @@ data approval_bootstrap_circularity: DivergenceReason = DivergenceReason { // BOUND TO THE DECLARED FORK ROW: when that dissolution row retires, the fork it names is gone and // this reason with it. +data arrival_archive_prefix_unobserved_world: DivergenceReason = DivergenceReason { + statement: "the arrival wet door acquires the archive slot then refuses unobserved PriorLifeBoundary (arrival_wet_prefix_from_unobserved_world); it does not fold the PriorLifeBoundary prefix or write the archive, so RealizedFederatedGrant would claim a write this job does not perform" as NonEmptyStr, + dissolution: unbound_dissolution(description: "NAMED CONSUMER: arrival_converge_under_archive_interlock. TRIGGER: that door binds an observed BMC/archive world and folds converge_mtjade1_arrival_prefix while holding ArrivalArchiveSlotHeld from arrival_archive_slot_acquire, then arrival_archive_slot_release. SUFFICIENT FOR retiring this reason and overlaying the archive census as RealizedFederatedGrant" as NonEmptyStr), +} + +data firmware_qualification_writer_unlanded: DivergenceReason = DivergenceReason { + statement: "the arrival wet door acquires the archive slot then refuses unobserved PriorLifeBoundary; firmware qualification has no writer under ArrivalArchiveSlotHeld, so RealizedFederatedGrant would claim a write this job does not perform" as NonEmptyStr, + dissolution: unbound_dissolution(description: "NAMED CONSUMER: arrival_converge_under_archive_interlock. TRIGGER: a successor of converge_mtjade1_arrival_prefix performs the MegaRAC per-build qualification write while holding ArrivalArchiveSlotHeld from arrival_archive_slot_acquire, then arrival_archive_slot_release. SUFFICIENT FOR retiring this reason and overlaying StandingJadeFirmwareQualification as InterlockedBy arrival_archive_slot_acquire" as NonEmptyStr), +} + data eager_bootstrap_fork_declared: DivergenceReason = DivergenceReason { statement: "gunbc.auth.access_token_source ensure_access_token_eager_bootstrap_fork_dissolve_on declares this eager gcloud call as a §3 fork with its dissolution condition" as NonEmptyStr, dissolution: retires_dissolution(ref: decl_ref(module_path: "gunbc.auth.access_token_source", decl_name: "ensure_access_token_eager_bootstrap_fork_dissolve_on")), @@ -718,6 +772,18 @@ data privileged_effect_census: List = [ realized: RealizedApprovalCapability, divergence_reason: none, }, + PrivilegedEffectSite { + site: site(module_path: "gunbc.auth.mtjade1_arrival_federation", decl_name: "mtjade1_arrival_archive_effect"), + effect: mtjade1_arrival_archive_effect(), + realized: RealizedUnauthorized, + divergence_reason: Present { value: arrival_archive_prefix_unobserved_world }, + }, + PrivilegedEffectSite { + site: site(module_path: "gunbc.auth.mtjade1_arrival_federation", decl_name: "mtjade1_arrival_firmware_qualification_effect"), + effect: mtjade1_arrival_firmware_qualification_effect(), + realized: RealizedUnauthorized, + divergence_reason: Present { value: firmware_qualification_writer_unlanded }, + }, PrivilegedEffectSite { site: site(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_wet"), effect: mtcollins1_boot_effect(), diff --git a/dag/gunbc/auth/standing_operator_grant.dag b/dag/gunbc/auth/standing_operator_grant.dag index 0cca4dbb43f..cbeda31d6d8 100644 --- a/dag/gunbc/auth/standing_operator_grant.dag +++ b/dag/gunbc/auth/standing_operator_grant.dag @@ -1,13 +1,18 @@ module gunbc.auth.standing_operator_grant import std.types { String, Bool, List, NonEmptyStr, Timestamp } +import v2.std.algebra { length } import product.host_identity { HostIdentity, host_identity_eq } +import std.optional { Present } import std.list { list_member } import std.scoped_authorization { OperatorGrant, ScopedAuthorization, AuthorizationGranted, AuthorizationRequest, Unclaimed } import std.decl_ref { DeclarationRef, decl_ref } import gunbc.fleet_host_identity { operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8, operator_host_mtjade1 } import gunbc.spark.fabric_switch_observed { FabricGroup, FabricGroupA, fabric_group_wire } -import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthorization, InterlockedBy, InterlockPending } +import gunbc.auth.authorization_pattern_selection { + StandingDestructiveAuthorization, StandingRulingInterlock, + InterlockPending, InterlockedBy, +} // ── A STANDING OPERATOR GRANT, COMMITTED AS A RULING ─────────────────────────────────────────── // @@ -35,25 +40,27 @@ import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthoriza // nothing reads would pre-authorize what no wall asks about. // // MTJADE1 LIVE OPS (operator ruling 2026-10-06, msg_7402f8df-7917-4b24-bb86-c4e7d51991f7) names BMC -// reads/writes, boots, and firmware qualification. Those classes are a declared frontier: the first -// consuming gate lands in gunbc#13497 (stern-ibex-771 route A -- bindable fleet-converge principal, -// effect arm in the same closure as the secret/cell fetch) and must call standing_grant_covers for a -// named arm -- O1c-3's BmcSecure authorization discharge, managed_host_boot admission/authorization, -// or MegaRAC per-build operation evidence / admit_megarac_host_at_current_build. The prior-life archive -// is a BMC read (it writes only our store) and has no grant arm. The mtjade1 grant's effects list is -// empty until that change lands the arm. The interlock is InterlockPending until a consuming gate names -// a hold: that state refuses to discharge irreversibility, so a bindable boot under this row does not -// select federation. +// reads/writes, boots, and firmware qualification. StandingBmcSecureAccountWrite is owned by +// gunbc#13517 (O1c-3b): the variant, wire key, and InterlockedBy admit_rotation_apply. This module +// consumes that arm on the mtjade1 effects list and standing_grant_arm_interlock overlay; J4 reads +// it via grant_discharges_bmc_secure_account_write. Route A also consumes archive and firmware +// arms (admit_arrival_subject). J6 boot stays a frontier until managed_host_boot. type StandingGrantEffect = StandingD0ReleaseToFleet | StandingArmLaunch | StandingHostEffectRecover + | StandingJadeArrivalArchive + | StandingJadeFirmwareQualification + | StandingBmcSecureAccountWrite fn standing_grant_effect_wire(e: StandingGrantEffect) -> NonEmptyStr { match e { StandingD0ReleaseToFleet => "d0-release-to-fleet" as NonEmptyStr StandingArmLaunch => "arm-launch" as NonEmptyStr StandingHostEffectRecover => "host-effect-recover" as NonEmptyStr + StandingJadeArrivalArchive => "jade-arrival-archive" as NonEmptyStr + StandingJadeFirmwareQualification => "jade-firmware-qualification" as NonEmptyStr + StandingBmcSecureAccountWrite => "bmc-secure-account-write" as NonEmptyStr } } @@ -119,19 +126,62 @@ data group_a_dev_standing_grant: StandingOperatorGrant = StandingOperatorGrant { // on mtjade1 are authorized whenever, indefinitely. That covers BMC reads and writes (history archive, // login/credential change), boots, and firmware qualification on Mt. Jade, with no per-run approval // needed. Scope is mtjade1 only; mtcollins1 wet steps still need their own go-ahead." Quote unchanged. -// Effects list empty: no consuming gate has landed (O1c-3 BmcSecure discharge, managed_host_boot -// authorization, MegaRAC current-build admission). The prior-life archive is not an arm. +// Grant grain stays InterlockPending (no blanket hold; unnamed classes such as J6 boot still refuse +// to discharge). Landed arms are InterlockedBy named holds via standing_grant_arm_interlock. +// StandingJadeFirmwareQualification stays InterlockPending until a held writer lands. +// StandingBmcSecureAccountWrite's overlay hold is #13517's admit_rotation_apply. Mode, pool, SA and +// secret names: operator sign-off msg_f03558d1. +// THE BMCSECURE ARM PROMOTES ONLY THIS GRAIN. A supplied InterlockPending with any other +// obligation, or InterlockedBy a foreign hold, stays as written so grant_discharges still +// refuses those mutants (test.claim.machine_intake_arrival_converge_witness +// w_bmc_secure_apply_pending_interlock_refuses_at_discharge). +data mtjade1_grant_grain_pending_obligation: NonEmptyStr = "grant grain names no hold; landed arms name holds via standing_grant_arm_interlock; J6 boot remains pending until managed_host_boot" as NonEmptyStr + data mtjade1_live_standing_grant: StandingOperatorGrant = StandingOperatorGrant { identity: "mtjade1-live-standing-grant-2026-10-06" as NonEmptyStr, principal: "operator" as NonEmptyStr, ruled_at: "2026-10-06T00:00:00Z", ruling: StandingDestructiveAuthorization { ruling_text: "Operator ruling 2026-10-06, given directly in eager-gull-22's session and relayed by dashboard message msg_7402f8df-7917-4b24-bb86-c4e7d51991f7: 'live operations on mtjade1 are authorized whenever, indefinitely. That covers BMC reads and writes (history archive, login/credential change), boots, and firmware qualification on Mt. Jade, with no per-run approval needed. Scope is mtjade1 only; mtcollins1 wet steps still need their own go-ahead.'" as NonEmptyStr, - effect_subject: "mtjade1 live operations: BMC credential/login writes, boots, and MegaRAC firmware qualification -- effect rows only as consuming gates land" as NonEmptyStr, - interlock: InterlockPending { obligation: "consuming gates (O1c-3 BmcSecure authorization discharge, managed_host_boot admission, MegaRAC current-build admission) have not named a hold" as NonEmptyStr }, + effect_subject: "mtjade1 live operations: BMC credential/login writes, boots, and MegaRAC firmware qualification -- effect rows only as consuming gates land. Arrival mode/input/pair/secret names (arrival_converge, arrival_subject, github-mtjade1-arrival, mtjade1-arrival@gunbai-secrets.iam.gserviceaccount.com, bmc-mtjade1-gunbc) signed off msg_f03558d1." as NonEmptyStr, + interlock: InterlockPending { obligation: mtjade1_grant_grain_pending_obligation }, }, scope: StandingGrantHost { host: operator_host_mtjade1 }, - effects: [] as List, + effects: [StandingJadeArrivalArchive, StandingJadeFirmwareQualification, StandingBmcSecureAccountWrite], +} + +fn standing_grant_arm_interlock(g: StandingOperatorGrant, e: StandingGrantEffect) -> StandingRulingInterlock { + match e { + StandingD0ReleaseToFleet => g.ruling.interlock + StandingArmLaunch => g.ruling.interlock + StandingHostEffectRecover => g.ruling.interlock + StandingJadeArrivalArchive => InterlockedBy { + hold: decl_ref(module_path: "gunbc.machine_intake_arrival_interlock", decl_name: "arrival_archive_slot_acquire"), + } + StandingJadeFirmwareQualification => InterlockPending { + obligation: "firmware qualification writer is not in converge_mtjade1_arrival_prefix; discharge only when that writer runs under ArrivalArchiveSlotHeld from arrival_archive_slot_acquire" as NonEmptyStr, + } + StandingBmcSecureAccountWrite => + match g.ruling.interlock { + InterlockPending { obligation: o } => + if (o as String) == (mtjade1_grant_grain_pending_obligation as String) { + InterlockedBy { + hold: decl_ref(module_path: "gunbc.machine_intake_bmc_rotation_route", decl_name: "admit_rotation_apply"), + } + } else { + InterlockPending { obligation: o } + } + InterlockedBy { hold: h } => InterlockedBy { hold: h } + } + } +} + +fn standing_ruling_with_arm_interlock(g: StandingOperatorGrant, e: StandingGrantEffect) -> StandingDestructiveAuthorization { + StandingDestructiveAuthorization { + ruling_text: g.ruling.ruling_text, + effect_subject: g.ruling.effect_subject, + interlock: standing_grant_arm_interlock(g: g, e: e), + } } // COVERAGE IS AN IDENTITY JOIN: the scope is the grant's, the effect is one of its effects, and EVERY host diff --git a/dag/gunbc/ci/ci_spec.dag b/dag/gunbc/ci/ci_spec.dag index d86d550ed34..1f23ad90df8 100644 --- a/dag/gunbc/ci/ci_spec.dag +++ b/dag/gunbc/ci/ci_spec.dag @@ -943,6 +943,16 @@ data gunbc_ci_namecheap_observe_target: GunbcRunStepTarget = GunbcRunStepTarget function: "namecheap_observe_ci_wet", } +data gunbc_ci_arrival_admit_target: GunbcRunStepTarget = GunbcRunStepTarget { + entry: "dag/gunbc/machine_intake/arrival_admission.dag", + function: "arrival_admit_executor", +} + +data gunbc_ci_arrival_converge_target: GunbcRunStepTarget = GunbcRunStepTarget { + entry: "dag/gunbc/machine_intake/arrival_run.dag", + function: "arrival_converge_wet", +} + data gunbc_ci_host_credential_custody_converge_target: GunbcRunStepTarget = GunbcRunStepTarget { entry: "dag/gunbc/fleet/host_credential_custody_converge.dag", function: "host_credential_custody_converge_ci_wet", @@ -1456,7 +1466,9 @@ fn gunbc_run_step_targets() -> List { gunbc_ci_pair_serving_d0_target, gunbc_ci_pair_serving_d0_admit_target, gunbc_ci_gcp_iam_converge_request_target, - gunbc_ci_gcp_iam_converge_apply_target + gunbc_ci_gcp_iam_converge_apply_target, + gunbc_ci_arrival_admit_target, + gunbc_ci_arrival_converge_target ] } @@ -4063,6 +4075,26 @@ fn gunbc_ci_namecheap_observe_invoke() -> String { ) } +fn gunbc_ci_arrival_admit_invoke() -> String { + gunbc_run_step_script( + source_roots: witness_layer_roots, + entry: gunbc_ci_arrival_admit_target.entry, + function: gunbc_ci_arrival_admit_target.function, + claim_run: false, + receipt_rel: none + ) +} + +fn gunbc_ci_arrival_converge_invoke() -> String { + gunbc_run_step_script( + source_roots: witness_layer_roots, + entry: gunbc_ci_arrival_converge_target.entry, + function: gunbc_ci_arrival_converge_target.function, + claim_run: false, + receipt_rel: none + ) +} + fn gunbc_ci_printer_workflow_invoke() -> String { gunbc_run_step_script(source_roots: witness_layer_roots, entry: gunbc_ci_printer_workflow_target.entry, diff --git a/dag/gunbc/fleet/convergence_fold.dag b/dag/gunbc/fleet/convergence_fold.dag index 432da9faf74..ae8065babc0 100644 --- a/dag/gunbc/fleet/convergence_fold.dag +++ b/dag/gunbc/fleet/convergence_fold.dag @@ -42,12 +42,18 @@ import gunbc.host_convergence_census { // independent readback does not ground. Incomplete is neither refused (the domain decided not to act, // or acting was refused before any effect) nor converged, and it never satisfies a precondition. // +// WHAT THIS HOME CARRIES SINCE O1c-3, with BmcSecure as first gated consumer +// (gunbc.machine_intake_arrival_converge): a step is Ungated or GatedOnAuthorization; a gated +// instance whose receipt declares that authorization was required (the Apply arm) refuses without a +// discharge for that (run, step, subject); Noop does not require one (parent D4). A discharge's +// principal is NonEmptyStr at the sole constructor, so the fold does not re-check emptiness. +// The pattern itself is selected before the fold (DESIGN §3d); the fold only checks discharge. +// // WHAT IT STILL DOES NOT CARRY, because no consumer exercises it yet and a designed fixture is not an -// inhabitant (DESIGN §3 pairing obligation): the authorization gate and its discharge, principals, -// mutation lanes, pending with re-attach across runs, subject quantifiers (all-of / any-of over a -// subject set), the domain-declared cheap readback, and order derived from preconditions alone where -// no order authority exists. Each lands with its first real consumer: O1c-3 (BmcSecure and -// ManagedHostAdmission), the Spark arm. +// inhabitant (DESIGN §3 pairing obligation): pending with re-attach across runs, subject quantifiers +// (all-of / any-of over a subject set), the domain-declared cheap readback, and order derived from +// preconditions alone where no order authority exists. Each lands with its first real consumer: the +// Spark arm. // A RUN AND A SUBJECT ARE THE CALLER'S IDENTITIES, BRANDED SO NEITHER IS READ AS THE OTHER. The // subject key is the domain's canonical spelling of what one step instance converges: for the arrival @@ -96,10 +102,26 @@ fn precondition_key(p: StepPrecondition, key: StepInstanceKey) -> StepInstanceKe // A STEP: its census identity, the ONE member of the order authority it is bound to, and its // preconditions. The member type is the authority's own (for the arrival prefix // gunbc.machine_intake_phase IntakePhase); the fold reads it only through the authority's rank. +// A STEP IS UNGATED, OR GATED ON AN AUTHORIZATION DISCHARGED FOR THAT INSTANCE. Selected before the +// fold: the caller names which pattern discharged it. The fold never selects a pattern. +type StepGate + = StepUngated + | StepGatedOnAuthorization + type ConvergenceStep { identity: DeclarationRef order_member: M preconditions: List + gate: StepGate +} + +fn ungated_readonly_step(identity: DeclarationRef, order_member: M, preconditions: List) -> ConvergenceStep { + ConvergenceStep { + identity: identity, + order_member: order_member, + preconditions: preconditions, + gate: StepUngated, + } } // THE ORDER AUTHORITY: which declaration owns the order, and its ranking. Absent is an unranked @@ -309,17 +331,48 @@ fn step_outcome_incomplete(outcome: StepOutcome) -> I? { type ConvergenceReceiptProjection sole_constructor { key_of: fn(R) -> StepInstanceKey consumed_of: fn(R) -> List + authorization_required_of: fn(R) -> Bool } -fn convergence_receipt_projection(key_of: fn(R) -> StepInstanceKey, consumed_of: fn(R) -> List) -> ConvergenceReceiptProjection +fn convergence_receipt_projection(key_of: fn(R) -> StepInstanceKey, consumed_of: fn(R) -> List, authorization_required_of: fn(R) -> Bool) -> ConvergenceReceiptProjection admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "arrival_receipt_projection"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplete"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_noop_needs_no_discharge"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_discharge_refuses"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "apply_fold_undischarged"), + ] +{ + ConvergenceReceiptProjection { key_of: key_of, consumed_of: consumed_of, authorization_required_of: authorization_required_of } +} + +// A DISCHARGE FOR ONE GATED INSTANCE, sealed: the domain verifies the selected pattern (operator +// capability, standing grant coverage, or federated workload principal) and mints this row; the fold +// only checks that a gated Apply has one for this key. Noop never requires it. +type InstanceAuthorization sole_constructor { + key: StepInstanceKey + principal: NonEmptyStr +} + +fn instance_authorization(key: StepInstanceKey, principal: NonEmptyStr) -> InstanceAuthorization + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "discharge_bmc_secure_apply"), + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "capability_discharge"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_discharge_refuses"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_noop_needs_no_discharge"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "apply_fold_undischarged"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_discharge_for_another_run_refuses"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_discharge_for_another_unit_refuses"), ] { - ConvergenceReceiptProjection { key_of: key_of, consumed_of: consumed_of } + InstanceAuthorization { key: key, principal: principal } +} + +fn instance_authorization_for(discharges: List, key: StepInstanceKey) -> InstanceAuthorization? { + discharges |> filter(d => step_instance_key_eq(a: d.key, b: key)) |> first() } type StepInstanceRefusal @@ -327,6 +380,7 @@ type StepInstanceRefusal | StepOutcomeAbsent | PreconditionUnmet { precondition: StepInstanceKey, consumed: List } | ConsumedReceiptNotAPrecondition { consumed: StepInstanceKey } + | AuthorizationUndischarged type StepInstanceStanding = InstanceConverged { key: StepInstanceKey, receipt: R } @@ -472,6 +526,7 @@ fn walk_instance( subject: StepSubjectKey, outcomes: List>, projection: ConvergenceReceiptProjection, + discharges: List, ) -> LedgerWalk { let key = step_instance_key(run: run, step: ranked.step.identity, subject: subject) match acc.line { @@ -483,11 +538,31 @@ fn walk_instance( Present { value: o } => match o { StepRefused { key: _, cause: c } => InstanceRefused { key: key, cause: DomainRefused { cause: c } } - StepIncomplete { key: _, cause: i } => InstanceIncomplete { key: key, cause: i } + StepIncomplete { key: _, cause: i } => + match ranked.step.gate { + StepUngated => InstanceIncomplete { key: key, cause: i } + StepGatedOnAuthorization => + match instance_authorization_for(discharges: discharges, key: key) { + Absent => InstanceRefused { key: key, cause: AuthorizationUndischarged } + Present { value: _ } => InstanceIncomplete { key: key, cause: i } + } + } StepEstablished { receipt: r } => match precondition_refusal(step: ranked.step, key: key, consumed: projection.consumed_of(r), ledger: acc.instances) { Present { value: why } => InstanceRefused { key: key, cause: why } - Absent => InstanceConverged { key: key, receipt: r } + Absent => + match ranked.step.gate { + StepUngated => InstanceConverged { key: key, receipt: r } + StepGatedOnAuthorization => + if projection.authorization_required_of(r) { + match instance_authorization_for(discharges: discharges, key: key) { + Absent => InstanceRefused { key: key, cause: AuthorizationUndischarged } + Present { value: _ } => InstanceConverged { key: key, receipt: r } + } + } else { + InstanceConverged { key: key, receipt: r } + } + } } } } @@ -496,20 +571,19 @@ fn walk_instance( } } -// THE RUN FOLD: one ledger per run, each instance converged, refused, incomplete or not reached, in the admitted -// order. The verdict is derived from the ledger and names the instance the line stopped at. fn fold_convergence_run( plan: AdmittedConvergencePlan, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>, projection: ConvergenceReceiptProjection, + discharges: List, ) -> ConvergenceRunVerdict { match first_outcome_refusal(run: run, subject: subject, plan: plan, keys: map(outcomes, o => outcome_key(outcome: o, projection: projection))) { Present { value: r } => RunOutcomesRefused { cause: r } Absent => { let walked = fold(plan.steps, init: LedgerWalk { line: LineOpen, instances: [] }, f: (acc, s) => - walk_instance(acc: acc, ranked: s, run: run, subject: subject, outcomes: outcomes, projection: projection)) + walk_instance(acc: acc, ranked: s, run: run, subject: subject, outcomes: outcomes, projection: projection, discharges: discharges)) let ledger = ConvergenceRunLedger { run: run, subject: subject, order_authority: plan.authority, instances: walked.instances } match walked.line { LineOpen => RunConverged { run: ConvergedRun { ledger: ledger } } diff --git a/dag/gunbc/fleet/fleet_converge_workflow.dag b/dag/gunbc/fleet/fleet_converge_workflow.dag index a5898bdb942..65506450ecf 100644 --- a/dag/gunbc/fleet/fleet_converge_workflow.dag +++ b/dag/gunbc/fleet/fleet_converge_workflow.dag @@ -16,7 +16,11 @@ import gunbc.namecheap.observation_artifact { namecheap_observation_receipt_path import gunbc.fleet.printer_federation { printer_environment, printer_provider_resource, printer_service_account,printer_lan_host_identity } import gunbc.ci_spec { gunbc_ci_printer_workflow_invoke } import gunbc.namecheap.federation { namecheap_environment, namecheap_provider_resource, namecheap_service_account } -import gunbc.ci_spec { gunbc_ci_namecheap_observe_invoke, gunbc_ci_sm_max_time } +import gunbc.auth.mtjade1_arrival_pair { + mtjade1_arrival_environment, mtjade1_arrival_provider_resource, mtjade1_arrival_service_account, +} +import gunbc.machine_intake_arrival_subject { arrival_converge_subject_options } +import gunbc.ci_spec { gunbc_ci_namecheap_observe_invoke, gunbc_ci_arrival_admit_invoke, gunbc_ci_arrival_converge_invoke, gunbc_ci_sm_max_time } import gunbc.runner_microvm_slot_unit { microvm_slot_unit_timeout_stop, microvm_slot_start_receipt_path, microvm_slot_reserve_receipt_path, microvm_slot_reserve_wait_bound } import std.measure { Second, minute_count, second_count } @@ -129,7 +133,7 @@ import gunbc.managed_host_unit_hold { UnitHoldHostAdmission, UnitHoldHostAdmitted, UnitHoldHostNotManaged, UnitHoldHostNotRequired, unit_hold_admission_for, unit_hold_host_admission_refusal, } -import gunbc.fleet_host_identity { operator_host_mtcollins1 } +import gunbc.fleet_host_identity { operator_host_mtcollins1, operator_host_srv1 } import gunbc.auth.gcp_iam_converge_federation { gcp_iam_converge_environment, gcp_iam_observe_wif_provider_resource } import gunbc.auth.gcp_iam_converge { iam_observe_service_account, iam_converge_service_account, iam_converge_token_lifetime } import gunbc.auth.gcp_iam_converge_run { gcp_iam_converge_step_timeout_minutes, iam_converge_token_env, gcp_iam_converge_approved_output } @@ -235,7 +239,7 @@ import gunbc.ci_spec { gunbc_rlm_launch_deployment_receipt_artifact_dir, } import gunbc.fleet_converge_receipt { fleet_converge_plan_run_id_env_name } -import gunbc.actions_run_binding { rlm_expected_revision_env_name, fleet_converge_expected_host_env_name } +import gunbc.actions_run_binding { rlm_expected_revision_env_name, fleet_converge_expected_host_env_name, fleet_converge_arrival_subject_env_name } import gunbc.host_credential_custody_converge { host_custody_credential_options, host_credential_custody_env_name } import gunbc.spark.credential_workflow { spark_administrator_credential_roster_hosts } import gunbc.fleet_runner_connectivity { fleet_hosts } @@ -379,6 +383,7 @@ type FleetConvergeWorkflowMode | OrgRunnerRosterObserve | GcpIamConverge | NamecheapObserve + | ArrivalConverge | PrinterWorkflow fn fleet_converge_workflow_mode_wire(mode: FleetConvergeWorkflowMode) -> String { @@ -447,6 +452,7 @@ fn fleet_converge_workflow_mode_wire(mode: FleetConvergeWorkflowMode) -> String MtCollins1Boot => "mtcollins1_boot" GcpIamConverge => "gcp_iam_converge" NamecheapObserve => "namecheap_observe" + ArrivalConverge => "arrival_converge" PrinterWorkflow => "printer" PairServingD0 => "pair_serving_d0" MtCollins1FanObserve => "mtcollins1_fan_observe" @@ -483,7 +489,7 @@ fn fleet_converge_spark_target_description() -> String { ], "") } -data fleet_converge_workflow_modes: List = [FullHostPlan, LaunchEnvironmentPlan, AllocationStorePlan, WorkspaceCommissioningPlan, FleetApply, OrgActionsObserve, AppControlPlaneObserve, MicrovmHostConverge, MicrovmNetworkObserve, MicrovmNetworkApply, GuestImageObserve, GuestImageConverge, MicrovmBootProbe, SparkGrants, SparkBootstrap, SparkServingApply, SparkNativeServingApply, SparkRuntimeImageProbe, SparkWirelessLinkConverge, SparkGrantsObserve, SparkV41CheckpointMaterialize, SparkV41RowStoreEncode, SparkV41RowStoreReadback, SparkV41EngramDifferential, SparkRuntimeImageProduce, SparkRuntimeImageDistribute, SparkArmGroupLoad, SparkArmCheckpointMaterialize, SparkArmGroupObserve, SparkArmGroupLaunchPlan, SparkArmGroupLaunch, SparkV41ServingLoad, DashboardDeploy, ApprovalBrokerDarkInstall, MicrovmControllerInstall, MicrovmSlotReserve, MicrovmSlotStart, RlmLaunchDeploymentReceipt, HostResetReturn, RunnerHostFileObserve, RunnerHostFileConverge, SitePxeEdgeObserve, SitePxeEdgeConverge, RunnerPasswordSessionToolConverge, RunnerBrowserToolchainConverge, R2MintPreflight, R2ObjectWriteMint, OrgRunnerRosterObserve, ApprovalKeyringConverge, ApprovalDeviceEnrolmentCodeIssue, MtCollins1Boot, MtCollins1FanObserve, MtCollins1UiBundleObserve, MtCollins1KvmObserverObserve, MtCollins1CensusImagePublish, MtCollins1CensusMemberReadback, MtCollins1CensusQemuHostObserve, MtCollins1CensusQemuToolchainConverge, HostCredentialCustodyConverge, AppKeyVersionVerify, R2BucketEnsure, R2BucketAdminMint, R2WorkspaceObjectReadMint, R2WorkspaceObjectWriteMint, R2CacheObjectReadMint, R2CacheObjectWriteMint, R2ConditionalPutRaceProbe, WorkspaceSourcePack, WorkspaceCheckpointMeasure, WorkspaceCheckpointRestore, FabricWriterIdentityObserve, PairServingD0, MicrovmRunnerGroupEnsure, GcpIamConverge, NamecheapObserve, PrinterWorkflow] +data fleet_converge_workflow_modes: List = [FullHostPlan, LaunchEnvironmentPlan, AllocationStorePlan, WorkspaceCommissioningPlan, FleetApply, OrgActionsObserve, AppControlPlaneObserve, MicrovmHostConverge, MicrovmNetworkObserve, MicrovmNetworkApply, GuestImageObserve, GuestImageConverge, MicrovmBootProbe, SparkGrants, SparkBootstrap, SparkServingApply, SparkNativeServingApply, SparkRuntimeImageProbe, SparkWirelessLinkConverge, SparkGrantsObserve, SparkV41CheckpointMaterialize, SparkV41RowStoreEncode, SparkV41RowStoreReadback, SparkV41EngramDifferential, SparkRuntimeImageProduce, SparkRuntimeImageDistribute, SparkArmGroupLoad, SparkArmCheckpointMaterialize, SparkArmGroupObserve, SparkArmGroupLaunchPlan, SparkArmGroupLaunch, SparkV41ServingLoad, DashboardDeploy, ApprovalBrokerDarkInstall, MicrovmControllerInstall, MicrovmSlotReserve, MicrovmSlotStart, RlmLaunchDeploymentReceipt, HostResetReturn, RunnerHostFileObserve, RunnerHostFileConverge, SitePxeEdgeObserve, SitePxeEdgeConverge, RunnerPasswordSessionToolConverge, RunnerBrowserToolchainConverge, R2MintPreflight, R2ObjectWriteMint, OrgRunnerRosterObserve, ApprovalKeyringConverge, ApprovalDeviceEnrolmentCodeIssue, MtCollins1Boot, MtCollins1FanObserve, MtCollins1UiBundleObserve, MtCollins1KvmObserverObserve, MtCollins1CensusImagePublish, MtCollins1CensusMemberReadback, MtCollins1CensusQemuHostObserve, MtCollins1CensusQemuToolchainConverge, HostCredentialCustodyConverge, AppKeyVersionVerify, R2BucketEnsure, R2BucketAdminMint, R2WorkspaceObjectReadMint, R2WorkspaceObjectWriteMint, R2CacheObjectReadMint, R2CacheObjectWriteMint, R2ConditionalPutRaceProbe, WorkspaceSourcePack, WorkspaceCheckpointMeasure, WorkspaceCheckpointRestore, FabricWriterIdentityObserve, PairServingD0, MicrovmRunnerGroupEnsure, GcpIamConverge, NamecheapObserve, ArrivalConverge, PrinterWorkflow] // WHICH RELEASE PRODUCT A MODE'S JOB RUNS, NAMED PER MODE WITH NO WILDCARD (as the scope and fleet-key // matches above name theirs). A mode whose steps run only gunbc and claim_executor declares the // compiler pair (gunbc.fleet_release_bins_key compiler_pair_release_product): its build job then @@ -569,6 +575,7 @@ fn fleet_converge_mode_release_product(mode: FleetConvergeWorkflowMode) -> Fleet MicrovmRunnerGroupEnsure => SixteenBinaryPack GcpIamConverge => SixteenBinaryPack NamecheapObserve => SixteenBinaryPack + ArrivalConverge => SixteenBinaryPack PrinterWorkflow => SixteenBinaryPack } } @@ -669,6 +676,7 @@ fn fleet_converge_mode_scope(mode: FleetConvergeWorkflowMode) -> FleetConvergeSc MtCollins1Boot => none GcpIamConverge => none NamecheapObserve => none + ArrivalConverge => none PrinterWorkflow => none PairServingD0 => none MtCollins1FanObserve => none @@ -830,6 +838,7 @@ fn fleet_converge_mode_fleet_ssh_key_demand(mode: FleetConvergeWorkflowMode) -> MicrovmRunnerGroupEnsure => FleetSshKeyNotConsumed GcpIamConverge => FleetSshKeyNotConsumed NamecheapObserve => FleetSshKeyNotConsumed + ArrivalConverge => FleetSshKeyNotConsumed PrinterWorkflow => FleetSshKeyNotConsumed } } @@ -1506,6 +1515,7 @@ fn fleet_converge_mode_mutation_domain(mode: FleetConvergeWorkflowMode) -> Fleet OrgRunnerRosterObserve => ExecutorDomain GcpIamConverge => ExecutorDomain NamecheapObserve => ExecutorDomain + ArrivalConverge => ExecutorDomain PrinterWorkflow => ExecutorDomain } } @@ -1538,6 +1548,16 @@ data fleet_converge_mutation_concurrency_group_expression: String = join([ "format('", fleet_host_mutation_group_prefix, "{0}', ", fleet_host_input_expression, ") }}", ], "") +fn fleet_converge_exclusive_job_concurrency(group: String) -> ConcurrencySpec? { + Present { + value: ConcurrencyMappingQueueNotMax { + group: group, + cancel_in_progress: Present { value: CancelInProgressBool { value: false } }, + explicit_single: none + } + } +} + data fleet_converge_spark_runtime_image_probe_step_if: String = fleet_converge_mode_step_if(mode: SparkRuntimeImageProbe) data fleet_converge_spark_wireless_link_converge_step_if: String = fleet_converge_mode_step_if(mode: SparkWirelessLinkConverge) data fleet_converge_spark_grants_observe_step_if: String = fleet_converge_mode_step_if(mode: SparkGrantsObserve) @@ -4180,7 +4200,10 @@ data fleet_converge_checkout_ref: Expression = LogicalOr { left: LogicalAnd { left: LogicalOr { left: LogicalOr { left: fleet_converge_dispatch_mode_is(mode: MtCollins1Boot), right: fleet_converge_dispatch_mode_is(mode: GcpIamConverge) }, - right: LogicalOr { left: fleet_converge_dispatch_mode_is(mode: NamecheapObserve), right: fleet_converge_dispatch_mode_is(mode: PrinterWorkflow) }, + right: LogicalOr { + left: fleet_converge_dispatch_mode_is(mode: NamecheapObserve), + right: LogicalOr { left: fleet_converge_dispatch_mode_is(mode: ArrivalConverge), right: fleet_converge_dispatch_mode_is(mode: PrinterWorkflow) }, + }, }, right: fleet_converge_event_sha, }, @@ -4248,6 +4271,7 @@ data fleet_converge_shared_job_if: String = join([ "github.event.inputs.mode != '", fleet_converge_workflow_mode_wire(mode: MtCollins1Boot), "'", " && github.event.inputs.mode != '", fleet_converge_workflow_mode_wire(mode: GcpIamConverge), "'", " && github.event.inputs.mode != '", fleet_converge_workflow_mode_wire(mode: NamecheapObserve), "'", + " && github.event.inputs.mode != '", fleet_converge_workflow_mode_wire(mode: ArrivalConverge), "'", " && github.event.inputs.mode != '", fleet_converge_workflow_mode_wire(mode: PrinterWorkflow), "'", ], "") @@ -4769,6 +4793,7 @@ fn fleet_converge_mode_job_id(mode: FleetConvergeWorkflowMode) -> NonEmptyStr { MicrovmRunnerGroupEnsure => fleet_converge_shared_job_id GcpIamConverge => "gcp-iam-converge" as NonEmptyStr NamecheapObserve => "namecheap-observe" as NonEmptyStr + ArrivalConverge => "arrival-converge" as NonEmptyStr PrinterWorkflow => "printer" as NonEmptyStr } } @@ -4816,6 +4841,7 @@ data fleet_converge_job_edges: List = [ FleetConvergeJobEdge { id: fleet_converge_mode_job_id(mode: PrinterWorkflow), needs: [fleet_converge_release_bins_job_id as String] }, FleetConvergeJobEdge { id: fleet_converge_mode_job_id(mode: NamecheapObserve), needs: [fleet_converge_release_bins_job_id as String] }, FleetConvergeJobEdge { id: fleet_converge_mode_job_id(mode: GcpIamConverge), needs: [fleet_converge_release_bins_job_id as String] }, + FleetConvergeJobEdge { id: fleet_converge_mode_job_id(mode: ArrivalConverge), needs: [fleet_converge_release_bins_job_id as String] }, ] // A BUILDER ASKS THE ROSTER FOR ITS OWN EDGE BY ID AND THE LOOKUP REFUSES RATHER THAN INVENTS. An @@ -4853,6 +4879,7 @@ fn fleet_converge_jobs() -> List { fleet_converge_rlm_launch_deployment_receipt_job(), fleet_converge_gcp_iam_converge_job(), fleet_converge_namecheap_observe_job(), + fleet_converge_arrival_converge_job(), fleet_converge_printer_job(), ] } @@ -4983,6 +5010,13 @@ data fleet_converge_dispatch_inputs: List = [ default: none, type: InputChoice { options: fleet_converge_enrolled_host_options }, }, + DispatchInput { + name: "arrival_subject", + description: Present { value: "arrival_converge only: the arrival-population unit (not executor host, not managed_host). Options are gunbc.machine_intake_arrival_subject arrival_converge_subject_options. Names signed off msg_f03558d1" }, + required: false, + default: none, + type: InputChoice { options: arrival_converge_subject_options() }, + }, DispatchInput { name: "mode", description: Present { value: "plan shows membership hunks; apply executes a prior plan artifact; org_actions_observe validates the org credential and refuses on runner-group drift; org_runner_roster_observe reads the organization's self-hosted runner registrations to exhaustion under the same token and refuses unless the roster is complete; app_control_plane_observe reads the gunbai-ci App registration and webhook config with a short-lived App JWT and refuses on hook-config drift; app_key_version_verify reads the gunbai-ci App private key at the EXACT Secret Manager version named by app_key_version, mints an installation token with it, and refuses unless GitHub accepts it and the key's rotation deadline has not passed -- no add, disable or destroy; runner_browser_toolchain_converge installs the declared Playwright/Chromium toolchain (apt host libraries as the administrator, digest-pinned node, Playwright and Chromium archives into the job user's root) on the selected host, which must be in the pool that runs the floor job, and refuses unless every digest, version and host library reads back and headless Chromium renders a local page; microvm_host_converge installs the cited Firecracker release on the selected host and reads the kvm grant back, refusing by name when the grant has not landed (the grant itself is applied by the full-host apply spine); microvm_network_apply stages the slot and host network files the model renders at the named expected_revision as root:root 0600 in a root-only directory over the fleet SSH edge as the host's ADMINISTRATOR, installs them with the modeled operations, reloads networkd, systemd-sysctl and the nft loader unit, and reads the ruleset back -- the job user is granted none of it, because install plus systemctl over content that principal can write is arbitrary root for any pull request; guest_image_observe reports the micro-VM base artifacts and their measured digests on the selected host and builds nothing; guest_image_converge builds the runner guest image there; microvm_boot_probe boots that image and reads its serial console; spark_grants and spark_bootstrap prepare the selected Spark; spark_serving_apply applies the promoted fabric groups' pair vLLM units over the password session, workers before heads; spark_native_serving_apply relaunches group B's native four-rank arm as ONE BOUNDED TRANSACTION -- an all-host preflight that mutates nothing and refuses on any unresolved artifact from an earlier run, the incumbent UNIT preserved (plus a diagnostic inspect of the incumbent container -- the container itself cannot outlive its unit, because these run --rm in the foreground under systemd), the head applied BEFORE the workers so every rank joins the head's new rendezvous store, then a readback of the COMPLETE realization through each container's own inspect -- every field the create spec states, the effective --node-rank off that container's argv, and NCCL's typed transport verdict on that incarnation -- plus the head's front door answering with this arm's served model, and then commit or a rollback of the whole arm -- and it is a separate mode because it reloads a 328 GB arm and nobody should reach it by asking for the pair units; spark_runtime_image_probe pulls the pinned runtime image on the selected Spark and reads its capabilities from inside its own digest, changing nothing; spark_wireless_link_converge reads the selected Spark's Wi-Fi power save (runtime via iw, persisted via the NetworkManager profile), link and kernel disconnect count, sets whichever realization differs from the declared intent, and refuses unless the readback decides Noop; spark_grants_observe reads every procured Spark's sudo grant listing as gunbc-automation and the bootstrap principal, and its sudoers drop-in shape, and writes nothing; spark_v41_checkpoint_materialize fetches the admitted published DeepSeek V4.1 files onto the selected Group A Spark (about 510 GB; spark_v41_row_store_encode encodes the eight Engram row stores from the verified shards on the selected Group A Spark and reads each store's sha256; spark_v41_row_store_readback reads those stores back at their header, first and last record and every rank seam, with the published source rows at the same rows, and writes nothing; spark_v41_engram_differential compares upstream's Engram lookup kernel with the design-B file-backed lookup over sampled real rows of every row store, byte for byte, and writes nothing; it states the requirement and refuses before fetching when the disk cannot hold it), publishes each only after its sha256 matches the manifest, leaves a present file with the right digest alone and refuses one with the wrong digest, and reads the storage-backed Engram spans from the verified shards; a transfer runs detached and a rerun reattaches; spark_v41_runtime_image_build PRODUCES the DeepSeek V4.1 image on the selected Spark -- it verifies the candidate's three FlashInfer wheels against the digests the candidate keys, converges the patched source tree, builds from it, reads the produced configuration digest back from inside the image through the probe route, and admits that digest against the candidate's own recipe, refusing a digest that does not recompute from it -- and it is a separate mode from the probe because it occupies one host for hours where the probe occupies it for minutes; spark_v41_runtime_image_distribute moves that produced image, named by the configuration digest its production receipt read back, from the host that receipt names to the selected Group A Spark -- save into its fabric blob root, pulled by the target straight over the fabric rail, load -- after stating its size against every filesystem a copy lands on, leaves a target already holding the digest untouched, refuses a target holding a different image under the tag, and refuses unless the target's image inspect Id reads back as that digest; spark_v41_group_a_launch reads the production image back under its tag on every Group A host, reads its registry inside its digest and every host's occupancy, and only when Group A is suspended for this candidate with every host held and vacant stages the Engram manifest and applies the V4.1 four-rank arm as one transaction at the capacity measurement's shape -- the target names only the session host; spark_v41_serving_load runs the shared serving-load runner against the V4.1 head (target must be srv6): one vllm bench serve step per capacity-measurement concurrency, metrics scraped around each, host pressure read on every Group A rank, and the staircase stop rules applied over the worst rank; it changes no unit and writes only its receipt; host_reset_return drives a rostered reset subject through its controller and measures the return FROM A PEER, and takes reset_observer rather than host because the observer must not be the subject; runner_host_file_observe reads the runner teardown drop-in, the needrestart deferral and the loaded teardown on the selected host as its administrator and writes nothing; runner_host_file_converge writes whichever of those two files differs, reloads systemd only if the drop-in changed, and refuses unless the manager then reports the declared teardown; microvm_controller_install writes the microVM slot controller's root-owned release locus (gunbc + sources + Firecracker + jailer) and the gunbc-microvm-slot@ template unit and the gunbc-microvm-slot-reserve broker unit on srv1 and starts neither; microvm_slot_reserve starts that broker unit once on srv1, which reserves the shakedown cell through the fabric broker route from inside the root process (slot, demand and offer derived from the model, never inputs), and uploads that invocation's reservation receipt, failing unless the reservation committed; microvm_slot_start starts the shakedown slot's controller unit once on srv1 (the instance is derived from the model, never an input), waits for it bounded by the unit's own stop timeout, and uploads that invocation's controller receipt; microvm_runner_group_ensure (srv1 only) reads the organization's runner groups and, only when the microvm-shakedown group is absent, files ONE operator approval, creates it restricted to the shakedown workflow on the default branch, and refuses unless the readback holds that restriction; mtcollins1_census_qemu_host_observe reads the selected host's KVM device and, under the job user's census QEMU root, the qemu-system-aarch64 build, its ldd libraries and the AAVMF images against their pins, and writes nothing; mtcollins1_census_qemu_toolchain_converge places that root as the job user (digest-pinned noble .debs unpacked with dpkg-deb -x, no apt, no Recommends) and refuses unless the same observe reads it ready; workspace_source_pack (host=srv1) enumerates the operator workspace as the job user, drops every path the credential exclusion row names and every build output, tars exactly the remainder, reads the archive back and refuses if any member is excluded, and puts it into the workspace bucket under its SHA-256, refusing by name when the runner cannot read a source root; workspace_checkpoint_measure (host=srv3, workspace_source_object = that SHA-256) refuses unless the job user's home is on btrfs, then times a read-only subvolume snapshot, a pinned kopia scan of it, the content-addressed chunk upload and the gated revision commit, and receipts every time with the 10 s / 60 s / 10 GB draft verdicts; workspace_checkpoint_restore (host=srv3) commits a small authored workspace, puts one chunk with no head advance, destroys the directory, restores it from the head closure and requires byte-equality with the uncommitted chunk absent -- both srv3 modes refuse their commit while the R2 head's CAS ground is uncited" }, @@ -5260,6 +5294,70 @@ fn fleet_converge_yml_after_unit_hold_admission() -> FleetConvergeYamlGeneration } +fn fleet_converge_arrival_converge_job() -> Job { + Job { + id: fleet_converge_mode_job_id(mode: ArrivalConverge) as String, + name: none, + runner: SelfHosted { labels: ["self-hosted", "linux", "arm64", operator_host_srv1 as String] }, + environment: Present { value: mtjade1_arrival_environment as String }, + steps: [ + fleet_converge_event_sha_checkout_step(), + ci_release_bins_download_step(), + ci_release_bins_unpack_verify_step(), + RunStep { + name: Present { value: "Arrival admission (credential-free): store host srv1 and a population arrival_subject" }, + id: Present { value: "arrival_admit" }, + run: gunbc_ci_arrival_admit_invoke(), + shell: none, + env: Present { value: [ + kv(key: fleet_converge_expected_host_env_name, value: yaml_string(s: "${{ github.event.inputs.host }}")), + kv(key: fleet_converge_arrival_subject_env_name, value: yaml_string(s: "${{ github.event.inputs.arrival_subject }}")), + ] }, + working_directory: none, + if_condition: none, + continue_on_error: none, + timeout_minutes: Present { value: gunbc_ci_aux_step_timeout_minutes }, + }, + ci_wif_auth_step_for( + name: "WIF auth (OIDC -> dedicated mtjade1-arrival pool -> mtjade1-arrival SA, access token only)", + provider_resource: mtjade1_arrival_provider_resource(), + service_account: mtjade1_arrival_service_account as String, + ), + RunStep { + name: Present { value: "arrival_converge under the standing grant and arrival interlock" }, + id: Present { value: "arrival_converge" }, + run: gunbc_ci_arrival_converge_invoke(), + shell: none, + env: Present { value: [ + kv(key: "WIF_ACCESS_TOKEN", value: yaml_string(s: "${{ steps.wif_auth.outputs.access_token }}")), + kv(key: fleet_converge_expected_host_env_name, value: yaml_string(s: "${{ github.event.inputs.host }}")), + kv(key: fleet_converge_arrival_subject_env_name, value: yaml_string(s: "${{ github.event.inputs.arrival_subject }}")), + ] }, + working_directory: none, + if_condition: none, + continue_on_error: none, + timeout_minutes: Present { value: gunbc_ci_aux_step_timeout_minutes }, + }, + ], + needs: fleet_converge_job_needs(id: fleet_converge_mode_job_id(mode: ArrivalConverge)), + env: none, + outputs: none, + if_condition: Present { value: fleet_converge_mode_step_if(mode: ArrivalConverge) }, + timeout_minutes: Present { value: gunbc_ci_aux_step_timeout_minutes + 20 }, + continue_on_error: none, + concurrency: fleet_converge_exclusive_job_concurrency(group: join([fleet_host_mutation_group_prefix, operator_host_srv1 as String], "")), + permissions: Present { + value: WorkflowPermissions { + contents: Present { value: PermRead }, + pull_requests: none, + issues: none, + actions: Present { value: PermRead }, + id_token: Present { value: PermWrite }, + } + }, + } +} + fn fleet_converge_namecheap_observe_job() -> Job { Job { id: fleet_converge_mode_job_id(mode: NamecheapObserve) as String, name: none, @@ -5337,9 +5435,7 @@ fn fleet_converge_printer_job() -> Job { if_condition: Present { value: fleet_converge_mode_step_if(mode: PrinterWorkflow) }, timeout_minutes: Present { value: gunbc_ci_gunbc_run_resolve_step_timeout_minutes + 20 }, continue_on_error: none, - concurrency: Present { value: ConcurrencyMappingQueueNotMax { - group: "printer-${{ inputs.printer }}", cancel_in_progress: Present { value: CancelInProgressBool { value: false } }, explicit_single: none, - } }, + concurrency: fleet_converge_exclusive_job_concurrency(group: "printer-${{ inputs.printer }}"), permissions: Present { value: WorkflowPermissions { contents: Present { value: PermRead }, pull_requests: none, issues: none, actions: Present { value: PermRead }, id_token: Present { value: PermWrite }, diff --git a/dag/gunbc/fleet/fleet_host_identity.dag b/dag/gunbc/fleet/fleet_host_identity.dag index 42deced7e0d..dc4ab9bdd99 100644 --- a/dag/gunbc/fleet/fleet_host_identity.dag +++ b/dag/gunbc/fleet/fleet_host_identity.dag @@ -1,5 +1,7 @@ module gunbc.fleet_host_identity +import std.types { List, NonEmptyStr, String } +import v2.std.algebra { filter } import product.host_identity { HostIdentity } // THE FLEET'S HOST IDENTITIES, as a leaf. These rows were authored in gunbc.fleet_intent_network, @@ -80,3 +82,26 @@ data operator_host_srv11: HostIdentity = "srv11" // lease table the day the fabric switch was cabled and landed on switch lane qsfp56-dd-2-3. srv12 // is its identity slot, assigned by the same ascending-address rule. data operator_host_srv12: HostIdentity = "srv12" + +// THE NAMED ROSTER, ONE LIST BESIDE THE ROWS. A step subject or other label resolves to a host only +// by joining this membership; a spelling that is not a row here is not a fleet host. +data operator_hosts: List = [ + operator_host_srv1, + operator_host_srv2, + operator_host_srv3, + operator_host_srv4, + operator_host_mtcollins1, + operator_host_mtjade1, + operator_host_srv5, + operator_host_srv6, + operator_host_srv7, + operator_host_srv8, + operator_host_srv9, + operator_host_srv10, + operator_host_srv11, + operator_host_srv12, +] + +fn operator_host_named(label: NonEmptyStr) -> HostIdentity? { + operator_hosts |> filter(h => (h as String) == (label as String)) |> first() +} diff --git a/dag/gunbc/guarantee_stall/authored_record_field_list_standing_for_type_population_stall.dag b/dag/gunbc/guarantee_stall/authored_record_field_list_standing_for_type_population_stall.dag new file mode 100644 index 00000000000..0b65eff47d5 --- /dev/null +++ b/dag/gunbc/guarantee_stall/authored_record_field_list_standing_for_type_population_stall.dag @@ -0,0 +1,39 @@ +module gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when } + +// WHY THIS IS A STALL AND NOT A SECTION 4b(3) DROP. Nothing was lowered. Before the BmcSecure +// observation join grew past four fields, the join already bound an authored subset; extending it +// to the rest of BmcAccountStateObservation except controller_clock did not drop a rung that had +// been held. DESIGN section 4b(2) requires a class below its ceiling to name its next-rung trigger. +// +// HOMES CHECKED BEFORE MINTING, so this is not a nickname of an existing class: +// gunbc.guarantee_stall.axis_list_re_enumerates_its_variant_type_stall -- authored list mirroring a +// declared COPRODUCT constructor population; waits on constructor enumeration. Record field +// identity-and-type is a different primitive. +// gunbc.guarantee_stall.roster_re_enumerates_its_own_rows_stall -- authored roster of DATA +// declarations; waits on declaration VALUE BINDING. A List is not a record field set. +// gunbc.recurring_failure_mode.optional_equality_answers_by_representation -- Optional == answering +// by representation (interpreter `first` vs Present). That is one ARM of this row's OR trigger, not +// the authored-field-list class. +// gunbc.recurring_failure_mode.handwritten_population_wrong_by_gain_and_by_loss, +// gunbc.recurring_failure_mode.roster_is_its_own_denominator -- waiter/report lists, not type fields. +// gunbc.recurring_failure_mode.kind_carried_but_its_fields_stay_optional -- Node payload optionality. +// gunbc.recurring_failure_mode.a_pattern_binding_a_subset_of_fields_is_an_implicit_wildcard -- match +// wildcards, not equality adapters. +data authored_record_field_list_standing_for_type_population_stall: GuaranteeStall = GuaranteeStall { + subject: "an authored field list stands for a record type's declared population, so a new field or a new Optional can fall out of an equality join silently", + current: Mitigatable, + ceiling: StructurallyImpossible, + blocker: AwaitsOneGrounding { + grounding: "a value-layer read of a record's declared fields with their types, sufficient to refuse an unhandled field or Optional at a join; or structural == that is value-exact over Optionals (gunbc#13488), after which clock blanking and the hand match delete", + }, + population: BoundedPopulation { + members: [ + "gunbc.machine_intake_bmc_secure bmc_account_state_observation_same", + "gunbc.machine_intake_bmc_secure controller_clock_reading_same", + ], + }, + next_rung_trigger: climbs_when(capability: "a value-layer read of a record's declared fields with their types, sufficient to refuse an unhandled field or an unhandled Optional at this join, checked by field identity and declared type never by count; OR gunbc#13488 making structural == value-exact over Optionals, after which observation_with_controller_clock blanking and controller_clock_reading_same are deleted. A count of fields, a comment claiming completeness, or a second authored list is not this capability"), +} diff --git a/dag/gunbc/guarantee_stall/roster.dag b/dag/gunbc/guarantee_stall/roster.dag index 2240a5c4741..92beb2a3a50 100644 --- a/dag/gunbc/guarantee_stall/roster.dag +++ b/dag/gunbc/guarantee_stall/roster.dag @@ -77,6 +77,7 @@ import gunbc.guarantee_stall.free_semigroup_text_crossing_decided_by_spelling_st import gunbc.guarantee_stall.emitted_inline_crate_path_edges_unreturned_stall { emitted_inline_crate_path_edges_unreturned_stall } import gunbc.guarantee_stall.compile_pool_provision_wired_but_unreachable_stall { compile_pool_provision_wired_but_unreachable_stall } import gunbc.guarantee_stall.filesystem_read_outcome_node_grain_census_stall { filesystem_read_outcome_node_grain_census_stall } +import gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall { authored_record_field_list_standing_for_type_population_stall } // THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are // carried here verbatim rather than split across the row modules they describe. Their membership @@ -249,6 +250,7 @@ data all_guarantee_stalls: List = [ accumulator_copy_untyped_combiner_refusals_stall, keyed_apply_patch_rebuilds_rows_per_hunk_stall, filesystem_read_outcome_node_grain_census_stall, + authored_record_field_list_standing_for_type_population_stall, ] // THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES. diff --git a/dag/gunbc/host_convergence_census.dag b/dag/gunbc/host_convergence_census.dag index fe27735eb1a..8b6b122ca71 100644 --- a/dag/gunbc/host_convergence_census.dag +++ b/dag/gunbc/host_convergence_census.dag @@ -848,6 +848,15 @@ data host_convergence_census_rows: List = [ disposition: RetainAuthority, first_consumer: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_prefix"), ), + census_row( + identity: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + subject: MachineIntakeArrival, + phases: protocol_phases(false, true, true, true, false, true, false), + current_authority: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + persistent_host_effect: ReachesPersistentHostMutation, + disposition: RetainAuthority, + first_consumer: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_through_bmc_secure"), + ), ] data host_convergence_census_standing: HostConvergenceCensus = admit_host_convergence_census(rows: host_convergence_census_rows) diff --git a/dag/gunbc/machine_intake/arrival_admission.dag b/dag/gunbc/machine_intake/arrival_admission.dag new file mode 100644 index 00000000000..e6ce1410017 --- /dev/null +++ b/dag/gunbc/machine_intake/arrival_admission.dag @@ -0,0 +1,45 @@ +module gunbc.machine_intake_arrival_admission + +import std.types { String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import gunbc.actions_run_binding { + actions_variable_read, ActionsVariablePresent, ActionsVariableAbsent, + fleet_converge_expected_host_env_name, fleet_converge_arrival_subject_env_name, +} +import gunbc.fleet_host_identity { operator_host_srv1 } +import gunbc.machine_intake_arrival_subject { + admit_arrival_subject, + ArrivalSubjectInPopulation, ArrivalSubjectUnknown, + ArrivalSubjectIsManagedHostExecutorConfusion, ArrivalSubjectOutsideGrant, +} + +// CREDENTIAL-FREE ARRIVAL ADMISSION. Same split as mtcollins1_boot_admission: the job's first +// gunbc run typechecks this closure only. The dispatch's host input must name the store host +// (srv1); the arrival_subject input must be in arrival_converge_population. Neither skip nor +// WIF happens first (review 70894). + +fn arrival_admit_executor() -> ProcessExit { + match actions_variable_read(name: fleet_converge_expected_host_env_name) { + ActionsVariableAbsent { variable: v, detail: d } => + exit_failure(reason: concat("arrival_converge: ", concat(v, concat(" ", concat(d, "; the arrival store host is srv1 only"))))) + ActionsVariablePresent { value: host } => + if host == (operator_host_srv1 as String) { + match actions_variable_read(name: fleet_converge_arrival_subject_env_name) { + ActionsVariableAbsent { variable: v, detail: d } => + exit_failure(reason: concat("arrival_converge: ", concat(v, concat(" ", d)))) + ActionsVariablePresent { value: wire } => + match admit_arrival_subject(wire: wire) { + ArrivalSubjectInPopulation { subject: _ } => ExitSuccess + ArrivalSubjectUnknown { wire: w } => + exit_failure(reason: concat("arrival_converge refuses unknown arrival_subject '", concat(w, "'"))) + ArrivalSubjectIsManagedHostExecutorConfusion { wire: w } => + exit_failure(reason: concat("arrival_converge refuses executor/host as arrival_subject '", concat(w, "'"))) + ArrivalSubjectOutsideGrant { wire: w } => + exit_failure(reason: concat("arrival_converge refuses arrival_subject '", concat(w, "' outside the standing grant"))) + } + } + } else { + exit_failure(reason: concat("arrival_converge refuses host '", concat(host, concat("': the arrival slot store is on ", operator_host_srv1 as String)))) + } + } +} diff --git a/dag/gunbc/machine_intake/arrival_converge.dag b/dag/gunbc/machine_intake/arrival_converge.dag index 53321df64ec..187a98004c1 100644 --- a/dag/gunbc/machine_intake/arrival_converge.dag +++ b/dag/gunbc/machine_intake/arrival_converge.dag @@ -1,6 +1,7 @@ module gunbc.machine_intake_arrival_converge -import std.types { List, NonEmptyStr, String } +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.content_hash { content_hash_equal } import std.decl_ref { DeclarationRef, decl_ref } import std.goal_assessment { ObservationAttempt, @@ -19,7 +20,7 @@ import std.upsert_decision { UpsertDecision, Noop, Apply, Refuse } import extdeps.bmc.endpoint { BmcControllerEndpoint, BmcEndpoint, BmcFirmwareFamily, Redfish } import extdeps.bmc.capability { BmcFirmwareReleaseIdentity, bmc_firmware_release_identity_of_wire } import extdeps.bmc.access_profile { SurfaceManagerIdentity } -import gunbc.machine_intake_receipt { EvidenceRef } +import gunbc.machine_intake_receipt { EvidenceRef, same_intake_subject } import gunbc.machine_intake_phase { ArrivalPhase, AccessDiscover, @@ -40,6 +41,7 @@ import gunbc.machine_intake_phase { Placement, arrival_phases_all, intake_phase_rank, + machine_qualification_policy_digest, } import gunbc.machine_intake_subject { AssemblyManifest, @@ -77,6 +79,7 @@ import gunbc.machine_intake_mtjade1_access_observation { fru_gap_text, smbios_gap_text, sol_session_controller, + mtjade1_smbios_sol_attribution, provisional_assembly_of_fru, read_mtjade1_current_manager_read, read_mtjade1_fru, @@ -85,9 +88,12 @@ import gunbc.machine_intake_mtjade1_access_observation { import gunbc.machine_intake_mtcollins1_bmc_secure_observation { mtcollins1_unit_key_standing } import gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding, + BmcAccountWriteRequest, ObservedSurfaceRead, rotation_route_candidate, redfish_account_password_write, + rotation_apply_authority, + rotation_route_request_identity, } import gunbc.machine_intake_bmc_rotation_route_evidence { manager_read_receipt, mtjade1_observed_endpoint } import gunbc.host_convergence_protocol { HostEffectDomainProjection, inspect_via_host_effect_projection } @@ -104,6 +110,39 @@ import gunbc.machine_intake_prior_life_boundary { prior_life_receipt_key, prior_life_receipt_consumed_identity, } +import gunbc.machine_intake_bmc_secure { + BmcSecureGoal, + BmcAccountStateObservation, + BmcSecureStateInspected, + BmcSecureStateUnobserved, + BmcSecurePhaseConverged, + BmcSecurePhaseRefused, + BmcSecurePhaseNoop, + BmcSecurePhaseApplied, + BmcSecurePhaseReceipt, + inspect_bmc_secure_state, + bmc_secure_phase_noop, + bmc_secure_phase_applied, + BmcAccountApplication, + ManagedCredentialReference, + managed_reference_same, + bmc_account_state_observation_same, +} +import gunbc.auth.authorization_pattern_selection { + InterlockedBy, InterlockPending, +} +import gunbc.auth.standing_operator_grant { + StandingOperatorGrant, + StandingGrantHost, + StandingBmcSecureAccountWrite, + standing_grant_covers, + standing_grant_arm_interlock, +} +import gunbc.auth.privileged_effect_census { ruling_interlock_is_rostered } +import product.host_identity { HostIdentity, host_identity_eq } +import gunbc.fleet_host_identity { operator_host_named, operator_host_mtjade1 } +import gunbc.auth.approval_capability { ProposeApprove, ProposeDeny } +import gunbc.auth.approval_broker { Redemption, RedemptionAdmitted, RedemptionRefused } import gunbc.fleet.convergence_fold { ConvergenceRunId, StepSubjectKey, @@ -123,24 +162,35 @@ import gunbc.fleet.convergence_fold { StepIncomplete, ConvergenceReceiptProjection, ConvergenceRunVerdict, + RunConverged, + RunStopped, + RunIncomplete, + RunOutcomesRefused, admit_convergence_plan, fold_convergence_run, step_instance_key, step_outcome_receipt, + ungated_readonly_step, + StepGatedOnAuthorization, + InstanceAuthorization, + instance_authorization, } -// THE ARRIVAL CONVERGENCE PREFIX (docs/plans/managed-host-untangle.md, cuts O1c-1 and O1c-2): the first -// real consumer of gunbc.fleet.convergence_fold. Its three steps are the first three phases of -// gunbc.machine_intake_phase arrival_phases_all -- AccessDiscover, IdentityBindProvisional and -// PriorLifeBoundary -- each a protocol step through gunbc.host_convergence_protocol +// THE ARRIVAL CONVERGENCE PREFIX (docs/plans/managed-host-untangle.md, cuts O1c-1 through O1c-3): the +// first real consumer of gunbc.fleet.convergence_fold. Its four steps are the first four phases of +// gunbc.machine_intake_phase arrival_phases_all -- AccessDiscover, IdentityBindProvisional, +// PriorLifeBoundary and BmcSecure -- each a protocol step through gunbc.host_convergence_protocol // HostEffectDomainProjection (observe, assess, decide) with its own row in // gunbc.host_convergence_census. The first two are read-only: the only decision either can reach is // Noop (the phase's goal is read back as already holding) or Refuse; neither has an Apply, so an Apply // decision is itself a typed refusal, and the read each consumes is a committed capture. // PriorLifeBoundary is the first effectful step: its archive arm writes the controller's prior-life // records to the evidence store and reads them back, DRY in this cut -// (gunbc.machine_intake_prior_life_boundary), so it is the one step that can be INCOMPLETE. Nothing -// here performs a live BMC call or a live store write. gunbc.bmc_onboarding is not imported. +// (gunbc.machine_intake_prior_life_boundary), so it is the one step that can be INCOMPLETE. +// BmcSecure is the first GATED step: Apply refuses unless authorization is discharged for that unit +// and that run (standing grant, operator capability, or federated workload principal selected before +// the fold); Noop needs no discharge. Nothing here performs a live BMC credential write. +// gunbc.bmc_onboarding is not imported. // // ORDERING TIME. No field of the read-only steps is an ordering clock. The controller's own DateTime is // kept as an AccessDiscover observation only; the observer clock (gunbc.clock_read) orders the @@ -154,6 +204,8 @@ data identity_bind_provisional_step_ref: DeclarationRef = decl_ref(module_path: data prior_life_boundary_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary") +data bmc_secure_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure") + // A read-only phase has no remedy. The plan type of its projection is sealed to this module and this // module constructs none, so an Apply over a read-only phase has no value to carry. type ReadOnlyPhaseRemedy sole_constructor { @@ -454,6 +506,7 @@ type ArrivalStepReceipt = AccessDiscoverReceipt { receipt: AccessDiscoverEstablished } | IdentityBindReceipt { receipt: IdentityBoundProvisional } | PriorLifeBoundaryReceipt { receipt: PriorLifeBoundaryEstablished } + | BmcSecureReceipt { receipt: BmcSecureStepEstablished } type ArrivalStepRefusal = AccessDiscoverObserveRefused { cause: AccessObserveRefusal } @@ -464,17 +517,37 @@ type ArrivalStepRefusal | ReadOnlyPhaseSatisfiedWithoutEvidence { phase: ArrivalPhase } | PriorLifeIdentityForAnotherInstance { identity: StepInstanceKey } | PriorLifeBoundaryRefused { cause: PriorLifeRefusal } + | BmcSecureIdentityForAnotherInstance { identity: StepInstanceKey } + | BmcSecureAuthorizationUndischarged + | BmcSecurePhaseDomainRefused + | BmcSecureApplyInputsMissing + | BmcSecureApplicationForAnotherInstance { subject: MachineIntakeSubject } + | BmcSecureApplicationNotTheInspectedTransition -// A STEP WHOSE EFFECT WAS ATTEMPTED AND IS NOT GROUNDED BY ITS READBACK. Only PriorLifeBoundary has -// an effect in this prefix; the read-only phases cannot be incomplete. type ArrivalStepIncomplete = PriorLifeBoundaryIncomplete { cause: PriorLifeIncomplete } +type BmcSecureStepEstablished sole_constructor { + key: StepInstanceKey + consumed_prior_life: StepInstanceKey + phase: BmcSecurePhaseReceipt +} + +fn bmc_secure_step_established(key: StepInstanceKey, consumed_prior_life: StepInstanceKey, phase: BmcSecurePhaseReceipt) -> BmcSecureStepEstablished + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure_bound"), + ] +{ + BmcSecureStepEstablished { key: key, consumed_prior_life: consumed_prior_life, phase: phase } +} + fn arrival_receipt_key(r: ArrivalStepReceipt) -> StepInstanceKey { match r { AccessDiscoverReceipt { receipt: a } => a.key IdentityBindReceipt { receipt: i } => i.key PriorLifeBoundaryReceipt { receipt: p } => prior_life_receipt_key(r: p) + BmcSecureReceipt { receipt: b } => b.key } } @@ -483,11 +556,25 @@ fn arrival_receipt_consumed(r: ArrivalStepReceipt) -> List { AccessDiscoverReceipt { receipt: _ } => [] IdentityBindReceipt { receipt: i } => [i.consumed_access] PriorLifeBoundaryReceipt { receipt: p } => [prior_life_receipt_consumed_identity(r: p)] + BmcSecureReceipt { receipt: b } => [b.consumed_prior_life] + } +} + +fn arrival_receipt_authorization_required(r: ArrivalStepReceipt) -> Bool { + match r { + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + PriorLifeBoundaryReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: b } => + match b.phase.decision { + BmcSecurePhaseNoop { observation: _ } => false + BmcSecurePhaseApplied { plan: _, application: _, post_read: _ } => true + } } } fn arrival_receipt_projection() -> ConvergenceReceiptProjection { - convergence_receipt_projection(key_of: arrival_receipt_key, consumed_of: arrival_receipt_consumed) + convergence_receipt_projection(key_of: arrival_receipt_key, consumed_of: arrival_receipt_consumed, authorization_required_of: arrival_receipt_authorization_required) } fn read_only_refusal(phase: ArrivalPhase, decision: UpsertDecision) -> ArrivalStepRefusal { @@ -582,6 +669,251 @@ fn prior_life_boundary(key: StepInstanceKey, identity: IdentityBoundProvisional, } } +type BmcSecureApplyInputs { + application: BmcAccountApplication + post_read: BmcAccountStateObservation +} + +type BmcSecureInputs { + goal: BmcSecureGoal + reading: BmcAccountStateObservation + grant: StandingOperatorGrant? + capability: Redemption? + apply: BmcSecureApplyInputs? +} + +// A federated principal is not a discharge input. StandingBmcSecureAccountWrite on the operator-ssh +// units is WorkloadIdentityUnbindable, so FederatedScopedGrant is not a selected pattern for this +// effect. A NonEmptyStr here was a silent widen (review 38602): any string minted Apply. + +fn bmc_secure_account_rotation_site() -> DeclarationRef { + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "plan_bmc_account_action") +} + +fn grant_discharges_bmc_secure_account_write(g: StandingOperatorGrant, host: HostIdentity) -> Bool { + standing_grant_covers(g: g, scope: StandingGrantHost { host: host }, effect: StandingBmcSecureAccountWrite) + && match standing_grant_arm_interlock(g: g, e: StandingBmcSecureAccountWrite) { + InterlockPending { obligation: _ } => false + InterlockedBy { hold: h } => + ruling_interlock_is_rostered(site_ref: bmc_secure_account_rotation_site(), interlock: h) + } +} + +fn capability_discharges_bmc_secure_account_write( + r: Redemption, + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, + key: StepInstanceKey, +) -> Bool { + match r { + RedemptionRefused { cause: _ } => false + RedemptionAdmitted { claims: cl, decided_by: _ } => + match cl.decision { + ProposeDeny => false + ProposeApprove => + cl.authority == rotation_apply_authority + && (cl.attempt as NonEmptyStr) == (key.run as NonEmptyStr) + && (cl.request_revision as String) == (rotation_route_request_identity(standing: standing, request: request) as String) + } + } +} + +fn bound_bmc_secure_host(key: StepInstanceKey) -> HostIdentity? { + operator_host_named(label: key.subject as NonEmptyStr) +} + +fn bound_host_owns_this_controller(host: HostIdentity, endpoint: BmcControllerEndpoint) -> Bool { + host_identity_eq(a: host, b: operator_host_mtjade1) + && (endpoint.host as String) == (sol_session_controller(a: mtjade1_smbios_sol_attribution).host as String) +} + +fn bmc_secure_instance_joins_this_controller( + key: StepInstanceKey, + identity_subject: MachineIntakeSubject, + reading: BmcAccountStateObservation, + standing: BmcRotationRouteStanding, +) -> Bool { + same_intake_subject(left: reading.subject, right: identity_subject) + && (key.run as String) == (identity_subject.attempt_id as String) + && (standing.endpoint.host as String) == (reading.endpoint.host as String) + && match bound_bmc_secure_host(key: key) { + Absent => false + Present { value: host } => bound_host_owns_this_controller(host: host, endpoint: standing.endpoint) + } +} + +fn capability_discharge( + key: StepInstanceKey, + inputs: BmcSecureInputs, + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, +) -> InstanceAuthorization? + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "discharge_bmc_secure_apply"), + ] +{ + match inputs.capability { + Present { value: r } => + if capability_discharges_bmc_secure_account_write(r: r, standing: standing, request: request, key: key) { + match r { + RedemptionAdmitted { claims: _, decided_by: by } => Present { value: instance_authorization(key: key, principal: by) } + RedemptionRefused { cause: _ } => none + } + } else { + none + } + Absent => none + } +} + +fn discharge_bmc_secure_apply( + key: StepInstanceKey, + identity_subject: MachineIntakeSubject, + inputs: BmcSecureInputs, + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, +) -> InstanceAuthorization? + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure_bound"), + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_through_bmc_secure"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_falls_through_to_capability"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_refuses_a_capability_for_another_request"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_foreign_bound_host_key_cannot_mint_from_this_instance_controller"), + ] +{ + if !bmc_secure_instance_joins_this_controller(key: key, identity_subject: identity_subject, reading: inputs.reading, standing: standing) { + none + } else { + match bound_bmc_secure_host(key: key) { + Absent => none + Present { value: host } => + match inputs.grant { + Present { value: g } => + if grant_discharges_bmc_secure_account_write(g: g, host: host) { + Present { value: instance_authorization(key: key, principal: g.principal) } + } else { + capability_discharge(key: key, inputs: inputs, standing: standing, request: request) + } + Absent => + capability_discharge(key: key, inputs: inputs, standing: standing, request: request) + } + } + } +} + +fn managed_generation_advances_the_requested(requested: ManagedCredentialReference, planned: ManagedCredentialReference) -> Bool { + requested.account == planned.account + && requested.role == planned.role + && (requested.secret.project as String) == (planned.secret.project as String) + && requested.secret.secret == planned.secret.secret + && planned.credential_epoch > requested.credential_epoch +} + +fn bmc_account_observation_is_the_inspected_pre_state(inspected: BmcAccountStateObservation, diverged: BmcAccountStateObservation) -> Bool { + bmc_account_state_observation_same(a: inspected, b: diverged) +} + +fn bmc_secure_application_joins_this_instance( + identity_subject: MachineIntakeSubject, + inspected_reading: BmcAccountStateObservation, + requested_goal: BmcSecureGoal, + application: BmcAccountApplication, +) -> ArrivalStepRefusal? { + if !same_intake_subject(left: application.plan.subject, right: identity_subject) { + Present { value: BmcSecureApplicationForAnotherInstance { subject: application.plan.subject } } + } else if !bmc_account_observation_is_the_inspected_pre_state(inspected: inspected_reading, diverged: application.plan.diverged) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else if !managed_reference_same(a: requested_goal.published_break_glass, b: application.plan.goal.published_break_glass) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else if !content_hash_equal(left: machine_qualification_policy_digest(policy: requested_goal.policy), right: machine_qualification_policy_digest(policy: application.plan.goal.policy)) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else if !managed_generation_advances_the_requested(requested: requested_goal.managed, planned: application.plan.goal.managed) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else { + none + } +} + +// Apply and discharge consume the bound subject's identity and the instance keys, not the +// AccessDiscover/IdentityBind capture parses. Those steps remain the prefix; this is the BMC +// grain after PriorLifeBoundary. +fn bmc_secure_bound( + key: StepInstanceKey, + identity_key: StepInstanceKey, + identity_subject: MachineIntakeSubject, + prior_key: StepInstanceKey, + inputs: BmcSecureInputs, +) -> StepOutcome + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "bmc_secure_bound_refuses_foreign_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_channel_state_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused"), + ] +{ + if (identity_key.run as NonEmptyStr) != (key.run as NonEmptyStr) || (identity_key.subject as NonEmptyStr) != (key.subject as NonEmptyStr) { + StepRefused { key: key, cause: BmcSecureIdentityForAnotherInstance { identity: identity_key } } + } else if (prior_key.run as NonEmptyStr) != (key.run as NonEmptyStr) || (prior_key.subject as NonEmptyStr) != (key.subject as NonEmptyStr) { + StepRefused { key: key, cause: BmcSecureIdentityForAnotherInstance { identity: prior_key } } + } else { + match inspect_bmc_secure_state(subject: identity_subject, goal: inputs.goal, reading: inputs.reading) { + BmcSecureStateUnobserved { cause: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + BmcSecureStateInspected { observed: _, assessment: a, decision: d } => + match d { + Noop => + match bmc_secure_phase_noop(subject: identity_subject, goal: inputs.goal, reading: inputs.reading) { + BmcSecurePhaseConverged { receipt: phase } => + StepEstablished { receipt: BmcSecureReceipt { receipt: bmc_secure_step_established(key: key, consumed_prior_life: prior_key, phase: phase) } } + BmcSecurePhaseRefused { cause: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + } + Refuse { reason: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + Apply { plan: _ } => + match inputs.apply { + Absent => StepRefused { key: key, cause: BmcSecureApplyInputsMissing } + Present { value: ap } => + match bmc_secure_application_joins_this_instance( + identity_subject: identity_subject, + inspected_reading: inputs.reading, + requested_goal: inputs.goal, + application: ap.application, + ) { + Present { value: c } => StepRefused { key: key, cause: c } + Absent => + match discharge_bmc_secure_apply( + key: key, + identity_subject: identity_subject, + inputs: inputs, + standing: ap.application.plan.managed_write.route, + request: ap.application.plan.managed_write.request, + ) { + Absent => StepRefused { key: key, cause: BmcSecureAuthorizationUndischarged } + Present { value: _ } => + match bmc_secure_phase_applied(application: ap.application, post_read: ap.post_read) { + BmcSecurePhaseConverged { receipt: phase } => + StepEstablished { receipt: BmcSecureReceipt { receipt: bmc_secure_step_established(key: key, consumed_prior_life: prior_key, phase: phase) } } + BmcSecurePhaseRefused { cause: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + } + } + } + } + } + } + } +} + +fn bmc_secure(key: StepInstanceKey, identity: IdentityBoundProvisional, prior: PriorLifeBoundaryEstablished, inputs: BmcSecureInputs) -> StepOutcome { + bmc_secure_bound( + key: key, + identity_key: identity.key, + identity_subject: identity.subject, + prior_key: prior_life_receipt_key(r: prior), + inputs: inputs, + ) +} + // ── THE PLAN: a prefix of the authority's order, never a second list ─────────────────────────── fn arrival_order_authority() -> ConvergenceOrderAuthority { @@ -599,10 +931,15 @@ fn arrival_planning_authority() -> ConvergencePlanningAuthority { // the plan; it is never skipped. fn arrival_step_of_phase(phase: ArrivalPhase) -> ConvergenceStep? { match phase { - AccessDiscover => Present { value: ConvergenceStep { identity: access_discover_step_ref, order_member: Arrival { phase: AccessDiscover }, preconditions: [] } } - IdentityBindProvisional => Present { value: ConvergenceStep { identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: [SameSubject { step: access_discover_step_ref }] } } - PriorLifeBoundary => Present { value: ConvergenceStep { identity: prior_life_boundary_step_ref, order_member: Arrival { phase: PriorLifeBoundary }, preconditions: [SameSubject { step: identity_bind_provisional_step_ref }] } } - BmcSecure => none + AccessDiscover => Present { value: ungated_readonly_step(identity: access_discover_step_ref, order_member: Arrival { phase: AccessDiscover }, preconditions: []) } + IdentityBindProvisional => Present { value: ungated_readonly_step(identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: [SameSubject { step: access_discover_step_ref }]) } + PriorLifeBoundary => Present { value: ungated_readonly_step(identity: prior_life_boundary_step_ref, order_member: Arrival { phase: PriorLifeBoundary }, preconditions: [SameSubject { step: identity_bind_provisional_step_ref }]) } + BmcSecure => Present { value: ConvergenceStep { + identity: bmc_secure_step_ref, + order_member: Arrival { phase: BmcSecure }, + preconditions: [SameSubject { step: prior_life_boundary_step_ref }], + gate: StepGatedOnAuthorization, + } } BootDeliveryEstablish => none DiagnosticBootAttest => none InventoryConform => none @@ -682,21 +1019,56 @@ fn arrival_prefix_outcomes(run: ConvergenceRunId, subject: StepSubjectKey, read: [access, identity, prior_life_boundary(key: step_instance_key(run: run, step: prior_life_boundary_step_ref, subject: subject), identity: i, platform: prior_life.platform, world: prior_life.world)] AccessDiscoverReceipt { receipt: _ } => [access, identity] PriorLifeBoundaryReceipt { receipt: _ } => [access, identity] + BmcSecureReceipt { receipt: _ } => [access, identity] } Absent => [access, identity] } } IdentityBindReceipt { receipt: _ } => [access] PriorLifeBoundaryReceipt { receipt: _ } => [access] + BmcSecureReceipt { receipt: _ } => [access] + } + } +} + +fn arrival_prefix_outcomes_through_bmc_secure(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs, prior_life: PriorLifeInputs, bmc: BmcSecureInputs) -> List> { + let prefix = arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life) + match prefix.last() { + Absent => prefix + Present { value: last } => + match step_outcome_receipt(outcome: last) { + Absent => prefix + Present { value: r } => + match r { + PriorLifeBoundaryReceipt { receipt: p } => + match prefix |> filter(o => match step_outcome_receipt(outcome: o) { Present { value: ir } => match ir { IdentityBindReceipt { receipt: _ } => true _ => false } Absent => false }) |> first() { + Absent => prefix + Present { value: id_out } => + match step_outcome_receipt(outcome: id_out) { + Absent => prefix + Present { value: ir } => + match ir { + IdentityBindReceipt { receipt: i } => + concat(prefix, [bmc_secure(key: step_instance_key(run: run, step: bmc_secure_step_ref, subject: subject), identity: i, prior: p, inputs: bmc)]) + AccessDiscoverReceipt { receipt: _ } => prefix + PriorLifeBoundaryReceipt { receipt: _ } => prefix + BmcSecureReceipt { receipt: _ } => prefix + } + } + } + AccessDiscoverReceipt { receipt: _ } => prefix + IdentityBindReceipt { receipt: _ } => prefix + BmcSecureReceipt { receipt: _ } => prefix + } } } } -fn fold_arrival_prefix(steps: List>, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ArrivalPrefixVerdict { +fn fold_arrival_prefix(steps: List>, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>, discharges: List) -> ArrivalPrefixVerdict { match admit_convergence_plan(planning: arrival_planning_authority(), steps: steps) { ConvergencePlanRefused { cause: c } => ArrivalPlanRefused { cause: c } ConvergencePlanAdmitted { plan: plan } => - ArrivalRunFolded { verdict: fold_convergence_run(plan: plan, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection()) } + ArrivalRunFolded { verdict: fold_convergence_run(plan: plan, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection(), discharges: discharges) } } } @@ -704,7 +1076,34 @@ fn converge_arrival_prefix(run: ConvergenceRunId, subject: StepSubjectKey, read: match arrival_prefix_steps(phases: arrival_prefix_through(last: arrival_prefix_last)) { ArrivalPrefixPhaseUnstepped { phase: p } => ArrivalPrefixUnstepped { phase: p } ArrivalPrefixStepped { steps: steps } => - fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life)) + fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life), discharges: []) + } +} + +// Apply mints through discharge_bmc_secure_apply. Noop never requires a fold discharge +// (arrival_receipt_authorization_required is false on BmcSecurePhaseNoop), so a grant +// copied here would be unused. +fn converge_arrival_through_bmc_secure(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs, prior_life: PriorLifeInputs, bmc: BmcSecureInputs) -> ArrivalPrefixVerdict { + match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { + ArrivalPrefixPhaseUnstepped { phase: p } => ArrivalPrefixUnstepped { phase: p } + ArrivalPrefixStepped { steps: steps } => { + let key = step_instance_key(run: run, step: bmc_secure_step_ref, subject: subject) + let discharges = match bmc.apply { + Present { value: ap } => + match discharge_bmc_secure_apply( + key: key, + identity_subject: bmc.reading.subject, + inputs: bmc, + standing: ap.application.plan.managed_write.route, + request: ap.application.plan.managed_write.request, + ) { + Present { value: d } => [d] + Absent => [] + } + Absent => [] + } + fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes_through_bmc_secure(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life, bmc: bmc), discharges: discharges) + } } } @@ -742,3 +1141,14 @@ fn converge_mtjade1_arrival_prefix(run: ConvergenceRunId, prior_life: DryPriorLi prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life }, ) } + +fn converge_mtjade1_arrival_through_bmc_secure(run: ConvergenceRunId, prior_life: DryPriorLifeWorld, bmc: BmcSecureInputs) -> ArrivalPrefixVerdict uses fs: std.resources.Filesystem { + converge_arrival_through_bmc_secure( + run: run, + subject: "mtjade1" as StepSubjectKey, + read: read_mtjade1_current_manager_read(), + inputs: mtjade1_identity_bind_inputs(), + prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life }, + bmc: bmc, + ) +} diff --git a/dag/gunbc/machine_intake/arrival_interlock.dag b/dag/gunbc/machine_intake/arrival_interlock.dag new file mode 100644 index 00000000000..28c706f3869 --- /dev/null +++ b/dag/gunbc/machine_intake/arrival_interlock.dag @@ -0,0 +1,184 @@ +module gunbc.machine_intake_arrival_interlock + +import std.types { NonEmptyStr, String } +import std.process { ProcessExit, ExitSuccess, ExitFailure, exit_failure } +import std.durable_compare_and_set { CasGeneration } +import std.durable_exclusive_hold { DurableHoldOwnerRef, DurableHoldReleaseRef } +import gunbc.durable_exclusive_hold_file_store { + file_hold_acquire, file_hold_release_assess, file_hold_release_commit, + FileHoldAcquireOutcome, + FileHoldAcquired, FileHoldOccupied, FileHoldAcquireLost, FileHoldAcquireStoreUnavailable, + FileHoldSlotUndecodable, FileHoldKeyNotSlotAddressable, + FileHoldReleasePlanned, FileHoldReleaseNotEligible, + FileHoldReleased, FileHoldReleaseLost, FileHoldReleaseStoreUnavailable, FileHoldReleaseKeyNotSlotAddressable, +} +import gunbc.machine_intake_bmc_rotation_route { + BmcRotationRouteStanding, rotation_route_is_grounded, +} +import gunbc.machine_intake_arrival_subject { ArrivalSubjectAdmitted } + +// ── THE INTERLOCK AN MTJADE1 ARRIVAL WRITE TAKES ────────────────────────────────────────────── +// The standing grant's words cover the class; this is the physical-safety / route-ground fact the +// run must observe. It is not UnitHoldProof: mtjade1 has no ManagedHost unit-hold row until J4 +// admission. The store host is operator_host_srv1 (the same runner the arrival job pins). A wet +// acquire is arrival_archive_slot_acquire (file_hold_acquire on arrival_slot_key); the caller +// runs the gated effect while ArrivalArchiveSlotHeld is in hand, then arrival_archive_slot_release. +// admit_arrival_* are supplied-slot checks, not the live hold. +// +// Archive (J2) needs the exclusive slot only (reads, evidence write, no account rotation). +// BmcSecure (J4) is InterlockedBy admit_rotation_apply (#13517). Firmware qualification stays +// InterlockPending until a writer under ArrivalArchiveSlotHeld lands in the wet door; the prefix +// is PriorLifeBoundary only. admit_arrival_* remain supplied-slot checks for witnesses. + +fn arrival_slot_key(subject_wire: NonEmptyStr) -> NonEmptyStr { + join(["arrival:", subject_wire as String], "") as NonEmptyStr +} + +type ArrivalSlotStanding + = ArrivalSlotHeld { subject: ArrivalSubjectAdmitted } + | ArrivalSlotNotHeld { cause: NonEmptyStr } + +type ArrivalArchiveInterlockStanding + = ArrivalArchiveInterlockAdmitted { subject: ArrivalSubjectAdmitted } + | ArrivalArchiveInterlockRefused { cause: NonEmptyStr } + +type ArrivalBmcSecureInterlockStanding + = ArrivalBmcSecureInterlockAdmitted { subject: ArrivalSubjectAdmitted } + | ArrivalBmcSecureInterlockRefused { cause: NonEmptyStr } + +fn admit_arrival_archive_interlock(subject: ArrivalSubjectAdmitted, slot: ArrivalSlotStanding) -> ArrivalArchiveInterlockStanding { + match slot { + ArrivalSlotHeld { subject: held } => + if (held.wire as String) == (subject.wire as String) { + ArrivalArchiveInterlockAdmitted { subject: subject } + } else { + ArrivalArchiveInterlockRefused { cause: "arrival slot was held for a different subject" as NonEmptyStr } + } + ArrivalSlotNotHeld { cause: c } => ArrivalArchiveInterlockRefused { cause: c } + } +} + +fn admit_arrival_bmc_secure_interlock( + subject: ArrivalSubjectAdmitted, + slot: ArrivalSlotStanding, + route: BmcRotationRouteStanding, +) -> ArrivalBmcSecureInterlockStanding { + match admit_arrival_archive_interlock(subject: subject, slot: slot) { + ArrivalArchiveInterlockRefused { cause: c } => ArrivalBmcSecureInterlockRefused { cause: c } + ArrivalArchiveInterlockAdmitted { subject: s } => + if rotation_route_is_grounded(standing: route) { + ArrivalBmcSecureInterlockAdmitted { subject: s } + } else { + ArrivalBmcSecureInterlockRefused { cause: "rotation route is not grounded; admit_rotation_apply refuses" as NonEmptyStr } + } + } +} + +fn arrival_slot_acquire_refusal(outcome: FileHoldAcquireOutcome) -> NonEmptyStr { + match outcome { + FileHoldAcquired { slot_key: _, owner: _, generation: _ } => "arrival slot acquire succeeded" as NonEmptyStr + FileHoldOccupied { slot_key: k, holder: h, generation: _ } => + join(["arrival slot ", k as String, " is held by '", h as String, "'"], "") as NonEmptyStr + FileHoldAcquireLost { slot_key: k } => join(["lost the race for arrival slot ", k as String], "") as NonEmptyStr + FileHoldAcquireStoreUnavailable { slot_key: k, cause: _ } => + join(["arrival slot store unavailable for ", k as String], "") as NonEmptyStr + FileHoldSlotUndecodable { slot_key: k, generation: _, detail: _ } => + join(["arrival slot ", k as String, " is undecodable"], "") as NonEmptyStr + FileHoldKeyNotSlotAddressable { slot_key: k } => + join(["arrival slot key ", k as String, " is not slot-addressable"], "") as NonEmptyStr + } +} + +type ArrivalArchiveSlotHeld sole_constructor { + subject: ArrivalSubjectAdmitted + slot_key: NonEmptyStr + owner: DurableHoldOwnerRef + generation: CasGeneration +} + +type ArrivalArchiveSlotAcquire + = ArrivalArchiveSlotAcquired { held: ArrivalArchiveSlotHeld } + | ArrivalArchiveSlotAcquireRefused { cause: NonEmptyStr } + +type ArrivalArchiveSlotRelease + = ArrivalArchiveSlotReleased { generation: CasGeneration } + | ArrivalArchiveSlotReleaseRefused { cause: NonEmptyStr } + +fn arrival_archive_slot_acquire(root: NonEmptyStr, subject: ArrivalSubjectAdmitted, owner: DurableHoldOwnerRef) -> ArrivalArchiveSlotAcquire { + let key = arrival_slot_key(subject_wire: subject.wire) + match file_hold_acquire(root: root, slot_key: key, requested_owner: owner) { + FileHoldOccupied { slot_key: k, holder: h, generation: g } => + ArrivalArchiveSlotAcquireRefused { cause: arrival_slot_acquire_refusal(outcome: FileHoldOccupied { slot_key: k, holder: h, generation: g }) } + FileHoldAcquireLost { slot_key: k } => + ArrivalArchiveSlotAcquireRefused { cause: arrival_slot_acquire_refusal(outcome: FileHoldAcquireLost { slot_key: k }) } + FileHoldAcquireStoreUnavailable { slot_key: k, cause: c } => + ArrivalArchiveSlotAcquireRefused { cause: arrival_slot_acquire_refusal(outcome: FileHoldAcquireStoreUnavailable { slot_key: k, cause: c }) } + FileHoldSlotUndecodable { slot_key: k, generation: g, detail: d } => + ArrivalArchiveSlotAcquireRefused { cause: arrival_slot_acquire_refusal(outcome: FileHoldSlotUndecodable { slot_key: k, generation: g, detail: d }) } + FileHoldKeyNotSlotAddressable { slot_key: k } => + ArrivalArchiveSlotAcquireRefused { cause: arrival_slot_acquire_refusal(outcome: FileHoldKeyNotSlotAddressable { slot_key: k }) } + FileHoldAcquired { slot_key: k, owner: o, generation: g } => + ArrivalArchiveSlotAcquired { + held: ArrivalArchiveSlotHeld { subject: subject, slot_key: k, owner: o, generation: g }, + } + } +} + +fn arrival_archive_slot_release(root: NonEmptyStr, held: ArrivalArchiveSlotHeld) -> ArrivalArchiveSlotRelease { + match file_hold_release_assess( + root: root, + slot_key: held.slot_key, + owner: held.owner, + acquired_generation: held.generation, + released_by: "arrival-converge-archive-interlock" as DurableHoldReleaseRef, + ) { + FileHoldReleaseNotEligible { slot_key: _, refusal: _ } => + ArrivalArchiveSlotReleaseRefused { cause: "arrival slot release was not eligible" as NonEmptyStr } + FileHoldReleasePlanned { plan: p } => + match file_hold_release_commit(plan: p) { + FileHoldReleased { slot_key: _, generation: g } => ArrivalArchiveSlotReleased { generation: g } + FileHoldReleaseLost { slot_key: _ } => + ArrivalArchiveSlotReleaseRefused { cause: "arrival slot release lost the race" as NonEmptyStr } + FileHoldReleaseStoreUnavailable { slot_key: _, cause: _ } => + ArrivalArchiveSlotReleaseRefused { cause: "arrival slot store unavailable on release" as NonEmptyStr } + FileHoldReleaseKeyNotSlotAddressable { slot_key: _ } => + ArrivalArchiveSlotReleaseRefused { cause: "arrival slot key not addressable on release" as NonEmptyStr } + } + } +} + +fn arrival_combine_prefix_and_release(prefix: ProcessExit, slot: ArrivalArchiveSlotRelease) -> ProcessExit { + match slot { + ArrivalArchiveSlotReleased { generation: _ } => prefix + ArrivalArchiveSlotReleaseRefused { cause: c } => + match prefix { + ExitSuccess => exit_failure(reason: concat("arrival_converge: prefix held, then slot release refused: ", c as String)) + ExitFailure { code: code, reason: reason } => + ExitFailure { code: code, reason: concat(reason, concat("; then slot release refused: ", c as String)) } + } + } +} + +fn arrival_archive_slot_held( + subject: ArrivalSubjectAdmitted, + slot_key: NonEmptyStr, + owner: DurableHoldOwnerRef, + generation: CasGeneration, +) -> ArrivalArchiveSlotHeld { + ArrivalArchiveSlotHeld { subject: subject, slot_key: slot_key, owner: owner, generation: generation } +} + +// Acquire, body, then the caller-supplied release. Production binds arrival_archive_slot_release +// at the one wet-door call site. One inhabitance claim also binds that same function. +fn arrival_after_acquire( + outcome: ArrivalArchiveSlotAcquire, + body: fn() -> ProcessExit, + release_fn: fn(ArrivalArchiveSlotHeld) -> ArrivalArchiveSlotRelease, +) -> ProcessExit { + match outcome { + ArrivalArchiveSlotAcquireRefused { cause: c } => + exit_failure(reason: concat("arrival_converge: ", c as String)) + ArrivalArchiveSlotAcquired { held: h } => + arrival_combine_prefix_and_release(prefix: body(), slot: release_fn(h)) + } +} diff --git a/dag/gunbc/machine_intake/arrival_run.dag b/dag/gunbc/machine_intake/arrival_run.dag new file mode 100644 index 00000000000..6a4fe275861 --- /dev/null +++ b/dag/gunbc/machine_intake/arrival_run.dag @@ -0,0 +1,89 @@ +module gunbc.machine_intake_arrival_run + +import std.types { NonEmptyStr, String } +import std.process { ProcessExit, ExitSuccess, ExitFailure, exit_failure } +import std.durable_exclusive_hold { DurableHoldOwnerRef } +import gunbc.actions_run_binding { + actions_variable_read, ActionsVariablePresent, ActionsVariableAbsent, + fleet_converge_arrival_subject_env_name, +} +import extdeps.github.actions_environment { github_run_id_variable_name } +import gunbc.auth.access_token_source { + select_access_token_source, AccessTokenSourceSelected, AccessTokenSourceUnavailable, + WorkloadIdentityToken, GcloudPrintToken, OperatorSuppliedToken, +} +import gunbc.machine_intake_arrival_admission { arrival_admit_executor } +import gunbc.machine_intake_arrival_subject { + admit_arrival_subject, ArrivalSubjectAdmitted, ArrivalSubjectInPopulation, + ArrivalSubjectUnknown, ArrivalSubjectIsManagedHostExecutorConfusion, ArrivalSubjectOutsideGrant, +} +import gunbc.machine_intake_arrival_interlock { + arrival_archive_slot_acquire, arrival_archive_slot_release, arrival_after_acquire, +} +import gunbc.managed_host_unit_hold { unit_hold_store_root } + +// THE ARRIVAL JOB'S WET DOOR (review 77263, review 77435, review 77746). Re-runs credential-free +// admit so WIF cannot outrun a refused subject, then requires WorkloadIdentityToken (the minted +// WIF bearer, in-process — not interpolated onto argv), takes arrival_archive_slot_acquire, and +// arrival_archive_slot_release. It does not fold a dry/unobserved PriorLifeBoundary into +// ExitSuccess: that would be fabricated plausible output (DESIGN §5). Until a live BMC/archive +// observation is bound as the prefix input, the held door refuses with a typed cause. Witnesses +// still supply a DryPriorLifeWorld to converge_mtjade1_arrival_prefix. BMC account writes and +// the pinned bmc-mtjade1-gunbc accessor stay behind this door: the locus is +// SecretLocusReservedNotOnAccessorRoster until FamilyObserved. + +fn arrival_wet_prefix_from_unobserved_world() -> ProcessExit { + exit_failure(reason: "arrival_converge refuses unobserved PriorLifeBoundary: no production observation is bound") +} + +fn arrival_converge_wet() -> ProcessExit uses fs: std.resources.Filesystem { + match arrival_admit_executor() { + ExitFailure { code, reason } => ExitFailure { code: code, reason: reason } + ExitSuccess => arrival_converge_after_admit() + } +} + +fn arrival_converge_after_admit() -> ProcessExit uses fs: std.resources.Filesystem { + match select_access_token_source() { + AccessTokenSourceUnavailable { cause: c } => + exit_failure(reason: concat("arrival_converge: ", c as String)) + AccessTokenSourceSelected { source: WorkloadIdentityToken } => + match actions_variable_read(name: fleet_converge_arrival_subject_env_name) { + ActionsVariableAbsent { variable: v, detail: d } => + exit_failure(reason: concat("arrival_converge: ", concat(v, concat(" ", d)))) + ActionsVariablePresent { value: wire } => + match admit_arrival_subject(wire: wire) { + ArrivalSubjectInPopulation { subject: s } => arrival_converge_under_archive_interlock(subject: s) + ArrivalSubjectUnknown { wire: w } => + exit_failure(reason: concat("arrival_converge refuses unknown arrival_subject '", concat(w, "' after admit"))) + ArrivalSubjectIsManagedHostExecutorConfusion { wire: w } => + exit_failure(reason: concat("arrival_converge refuses executor/host as arrival_subject '", concat(w, "' after admit"))) + ArrivalSubjectOutsideGrant { wire: w } => + exit_failure(reason: concat("arrival_converge refuses arrival_subject '", concat(w, "' outside the standing grant after admit"))) + } + } + AccessTokenSourceSelected { source: GcloudPrintToken } => + exit_failure(reason: "arrival_converge: this job federates; select_access_token_source must be WorkloadIdentityToken, not GcloudPrintToken") + AccessTokenSourceSelected { source: OperatorSuppliedToken { token: _ } } => + exit_failure(reason: "arrival_converge: this job federates; select_access_token_source must be WorkloadIdentityToken, not an operator-supplied token") + } +} + +fn arrival_converge_under_archive_interlock(subject: ArrivalSubjectAdmitted) -> ProcessExit uses fs: std.resources.Filesystem { + match actions_variable_read(name: github_run_id_variable_name) { + ActionsVariableAbsent { variable: v, detail: d } => + exit_failure(reason: concat("arrival_converge: ", concat(v, concat(" ", d)))) + ActionsVariablePresent { value: run_id } => + arrival_after_acquire( + outcome: arrival_archive_slot_acquire( + root: unit_hold_store_root, + subject: subject, + owner: join(["arrival-converge:", run_id], "") as DurableHoldOwnerRef, + ), + body: fn() { + arrival_wet_prefix_from_unobserved_world() + }, + release_fn: fn(h) { arrival_archive_slot_release(root: unit_hold_store_root, held: h) }, + ) + } +} diff --git a/dag/gunbc/machine_intake/arrival_subject.dag b/dag/gunbc/machine_intake/arrival_subject.dag new file mode 100644 index 00000000000..aab008ad2c9 --- /dev/null +++ b/dag/gunbc/machine_intake/arrival_subject.dag @@ -0,0 +1,85 @@ +module gunbc.machine_intake_arrival_subject + +import std.types { List, NonEmptyStr, String } +import std.optional { Present, Absent } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.auth.standing_operator_grant { + mtjade1_live_standing_grant, standing_grant_covers, StandingGrantHost, + StandingJadeArrivalArchive, StandingJadeFirmwareQualification, +} +import gunbc.fleet_host_identity { operator_host_mtjade1, operator_host_mtcollins1 } + +// ── ARRIVAL-CONVERGE SUBJECT POPULATION ─────────────────────────────────────────────────────── +// J2/J4 cannot read gunbc.managed_host managed_hosts(): mtjade1 is not a member until J4's +// ManagedHostAdmission. The dispatch input for those effects is this population, distinct from the +// executor `host` input and from `managed_host`. Options are derived from the rows, never a second +// hand list in fleet-converge.yml. +// +// A row is a unit that has an arrival-prefix producer (today: converge_mtjade1_arrival_prefix). It +// is not a HostIdentity enrollment and not a managed-host row. + +// This cut's population is one row, mtjade1. Dispatch options project from the +// rows. admit_arrival_subject then joins that singleton to mtjade1_live_standing_grant +// on operator_host_mtjade1; the grant is not a field of the row. A second row +// would appear in the options and still refuse ArrivalSubjectOutsideGrant until +// the admit fold joins each row to its own standing grant and host. +type ArrivalConvergePopulationRow { + wire: NonEmptyStr + producer: DeclarationRef +} + +data arrival_converge_population: List = [ + ArrivalConvergePopulationRow { + wire: "mtjade1" as NonEmptyStr, + producer: decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_mtjade1_arrival_prefix"), + }, +] + +fn arrival_converge_subject_options() -> List { + map(arrival_converge_population, r => r.wire as String) +} + +type ArrivalSubjectAdmitted sole_constructor { + wire: NonEmptyStr + producer: DeclarationRef +} + +type ArrivalSubjectAdmission + = ArrivalSubjectInPopulation { subject: ArrivalSubjectAdmitted } + | ArrivalSubjectUnknown { wire: String } + | ArrivalSubjectIsManagedHostExecutorConfusion { wire: String } + | ArrivalSubjectOutsideGrant { wire: String } + +fn arrival_population_row(wire: String) -> ArrivalConvergePopulationRow? { + filter(arrival_converge_population, r => (r.wire as String) == wire).first() +} + +// THE ADMIT FOLD THE ARRIVAL JOB RUNS BEFORE WIF. mtcollins1 is not a member. A spelling that is +// not in arrival_converge_population refuses. Grant coverage for this singleton is +// mtjade1_live_standing_grant on operator_host_mtjade1 (archive and firmware arms). +fn admit_arrival_subject(wire: String) -> ArrivalSubjectAdmission { + if wire == (operator_host_mtcollins1 as String) { + ArrivalSubjectIsManagedHostExecutorConfusion { wire: wire } + } else { + match arrival_population_row(wire: wire) { + Absent => ArrivalSubjectUnknown { wire: wire } + Present { value: row } => + if standing_grant_covers( + g: mtjade1_live_standing_grant, + scope: StandingGrantHost { host: operator_host_mtjade1 }, + effect: StandingJadeArrivalArchive, + ) && standing_grant_covers( + g: mtjade1_live_standing_grant, + scope: StandingGrantHost { host: operator_host_mtjade1 }, + effect: StandingJadeFirmwareQualification, + ) && (row.wire as String) == (operator_host_mtjade1 as String) { + ArrivalSubjectInPopulation { + subject: ArrivalSubjectAdmitted { wire: row.wire, producer: row.producer }, + } + } else { + ArrivalSubjectOutsideGrant { wire: wire } + } + } + } +} + diff --git a/dag/gunbc/machine_intake/bmc_rotation_route.dag b/dag/gunbc/machine_intake/bmc_rotation_route.dag index b997639aa7c..5deebbaa799 100644 --- a/dag/gunbc/machine_intake/bmc_rotation_route.dag +++ b/dag/gunbc/machine_intake/bmc_rotation_route.dag @@ -152,6 +152,8 @@ fn rotation_route_from_citation( decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "cited_lab_route_managed_user"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "cited_lab_route_published_user"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "cited_lab_route_managed_user_previous_build"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "cited_mtjade1_managed_route"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "cited_mtjade1_published_route"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_open_channel_is_closed_only_over_a_grounded_channel_access_route"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_channel_close_readback_is_bound_to_the_observed_run_and_account"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_planned_channel_close_is_applied_read_back_and_converges"), diff --git a/dag/gunbc/machine_intake/bmc_secure.dag b/dag/gunbc/machine_intake/bmc_secure.dag index 473f2ae3885..4a3b782bd43 100644 --- a/dag/gunbc/machine_intake/bmc_secure.dag +++ b/dag/gunbc/machine_intake/bmc_secure.dag @@ -3,7 +3,7 @@ module gunbc.machine_intake_bmc_secure import std.types { Bool, EpochMs, Int, List, Map, NonEmptyStr, String, list_length } import v2.std.algebra { filter } import std.decl_ref { decl_ref } -import std.content_hash { ContentHash, content_hash_of_value } +import std.content_hash { ContentHash, content_hash_of_value, content_hash_equal } import std.dissolution { DissolutionCondition, unbound_dissolution } import std.algebra { FreeSemigroup } import std.goal_assessment { @@ -1286,6 +1286,7 @@ fn observed_bmc_account_state( ) -> BmcAccountStateObservation admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_read_bmc_account_state"), + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "observation_with_controller_clock"), ] { BmcAccountStateObservation { @@ -1328,6 +1329,35 @@ fn observed_published_account_at_join(account: ObservedPublishedAccount) -> Publ } } +fn observation_with_controller_clock(base: BmcAccountStateObservation, controller_clock: ControllerClockReading?) -> BmcAccountStateObservation + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "bmc_account_state_observation_same"), + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "apply_with_diverged_controller_clock"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused"), + ] +{ + observed_bmc_account_state( + subject: base.subject, + endpoint: base.endpoint, + firmware: base.firmware, + managed: base.managed, + managed_user: base.managed_user, + attempt: base.attempt, + read_floor: base.read_floor, + managed_probe: base.managed_probe, + channel_census: base.channel_census, + census_evidence: base.census_evidence, + census_observed_at: base.census_observed_at, + published_probes: base.published_probes, + published_user: base.published_user, + published_account: base.published_account, + break_glass: base.break_glass, + break_glass_probe: base.break_glass_probe, + controller_clock: controller_clock, + ) +} + fn managed_reference_same(a: ManagedCredentialReference, b: ManagedCredentialReference) -> Bool { a.account == b.account && a.role == b.role @@ -1337,6 +1367,34 @@ fn managed_reference_same(a: ManagedCredentialReference, b: ManagedCredentialRef && a.credential_epoch == b.credential_epoch } +// THE OBSERVATION IS THE PAYLOAD, NOT A START TIME. Record `==` is the language's structural +// relation on the closed type, except controller_clock: ControllerClockReading? inherits +// optional_equality_answers_by_representation, so that field is matched explicitly and the rest +// compared by `==` after zeroing it. That match and observation_with_controller_clock are still +// authored field lists: a new ControllerClockReading field or a new Optional on the observation +// is not derived from the type declaration (no .dag value-layer reader of declared fields). The +// class is gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall +// authored_record_field_list_standing_for_type_population_stall -- a stall below ceiling, not a +// section 4b(3) drop. +fn controller_clock_reading_same(left: ControllerClockReading?, right: ControllerClockReading?) -> Bool { + match left { + Absent => match right { Absent => true Present { value: _ } => false } + Present { value: a } => match right { + Absent => false + Present { value: b } => + (a.reported_millis as Int) == (b.reported_millis as Int) + && a.evidence.label == b.evidence.label + && content_hash_equal(left: a.evidence.digest, right: b.evidence.digest) + } + } +} + +fn bmc_account_state_observation_same(a: BmcAccountStateObservation, b: BmcAccountStateObservation) -> Bool { + controller_clock_reading_same(left: a.controller_clock, right: b.controller_clock) + && (observation_with_controller_clock(base: a, controller_clock: none) + == observation_with_controller_clock(base: b, controller_clock: none)) +} + // WHAT THE PHASE REQUIRES OF THE CONTROLLER: this managed generation accepted, the published // credential closed, under this qualification policy. // published_break_glass is the exact generation the published account is retired TO (or, under a @@ -2065,6 +2123,34 @@ type BmcAccountApplication sole_constructor { applied_at: ObserverClockInstant } +fn apply_with_diverged_controller_clock(application: BmcAccountApplication, controller_clock: ControllerClockReading?) -> BmcAccountApplication + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + ] +{ + let p = application.plan + BmcAccountApplication { + plan: BmcAccountActionPlan { + subject: p.subject, + endpoint: p.endpoint, + firmware: p.firmware, + goal: p.goal, + diverged: observation_with_controller_clock(base: p.diverged, controller_clock: controller_clock), + due: p.due, + managed_write: p.managed_write, + published_write: p.published_write, + channel_writes: p.channel_writes, + planned_at: p.planned_at, + }, + managed_write_completed: application.managed_write_completed, + published_write_completed: application.published_write_completed, + channel_writes_completed: application.channel_writes_completed, + request_receipt: application.request_receipt, + response_receipt: application.response_receipt, + applied_at: application.applied_at, + } +} + type BmcSecurePhaseDecision = BmcSecurePhaseNoop { observation: BmcAccountStateObservation } | BmcSecurePhaseApplied { plan: BmcAccountActionPlan, application: BmcAccountApplication, post_read: BmcAccountStateObservation } @@ -2189,6 +2275,8 @@ fn dry_bmc_account_instant(millis: EpochMs) -> ObserverClockInstant admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_read_bmc_account_state"), decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_apply_bmc_account_plan"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_fetched_generation"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), ] { observer_clock_modeled(millis: millis, realization: bmc_secure_dry_realization_name) @@ -2260,6 +2348,11 @@ fn dry_read_bmc_account_state( ) -> BmcAccountStateObservation admit_callers: [ decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "read_in"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_mtjade1_converges_through_bmc_secure_noop_on_the_real_prefix"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_mtjade1_bmc_secure_apply_inputs_missing_refuses_on_the_real_path"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_channel_state_is_refused"), ] { let at = dry_bmc_account_instant(millis: read_at_millis) @@ -2323,6 +2416,7 @@ fn dry_apply_bmc_account_plan( decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "applied_with"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_post_read_is_independent_of_the_reading_that_diverged"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_planned_channel_close_is_applied_read_back_and_converges"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), ] { let managed_step = match dry_fetch_resolves(fetch: managed_fetch, write: plan.managed_write) { diff --git a/dag/gunbc/rung_drop/bmc_secure_apply_converge_new_witness_eval_step_cost.dag b/dag/gunbc/rung_drop/bmc_secure_apply_converge_new_witness_eval_step_cost.dag new file mode 100644 index 00000000000..aeedaeaa13f --- /dev/null +++ b/dag/gunbc/rung_drop/bmc_secure_apply_converge_new_witness_eval_step_cost.dag @@ -0,0 +1,38 @@ +module gunbc.rung_drop.bmc_secure_apply_converge_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_bmc_secure_apply_converge_rows } + +// DECLARED 4b(3) DROP (gunbc#13517, 2026-10-07). Pairing requires one Apply through +// converge_arrival_through_bmc_secure; that path still bills the arrival prefix plus the dry Apply +// in the seed interpreter. The DECLARATION lives here; the POPULATION's authority is +// `v2.workflow.floor_eval_step_cost_drop` `floor_eval_step_cost_drop_bmc_secure_apply_converge_rows`. +// +// WHAT IS LOST IS ONE WALL, AND THE CLAIM IS UNTOUCHED. The identity stays on the gate: planned, +// executed and measured on every run, its eval_steps recorded; a semantic red and a wall-clock +// crossing still block. Only an eval-step overrun is reported under the declared drop rather than +// refusing. The budget is not raised. + +data bmc_secure_apply_converge_new_witness_eval_step_cost_population: List = floor_eval_step_cost_drop_bmc_secure_apply_converge_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_bmc_secure_apply_converge_rows; measured by "), m.measured_by)) + +data bmc_secure_apply_converge_new_witness_eval_step_cost: RungDrop = RungDrop { + identity: "bmc_secure_apply_converge_new_witness_eval_step_cost" as NonEmptyStr, + + subject: "new-witness eval-step cost gate over the one Apply inhabitance of converge_arrival_through_bmc_secure: 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-10-07", + + standing: Standing, + + declaration: TypedDeclaration { + previous: MechanicallyPreventable, + temporary: Mitigatable, + reason: ReplacementStaged { + replacement: "converge_arrival_through_bmc_secure executing as natively emitted code rather than in the seed interpreter, so the one Apply inhabitance fits the NewWitnessTier eval-step budget", + }, + population: bmc_secure_apply_converge_new_witness_eval_step_cost_population, + restoration_trigger: "THE CAPABILITY: converge_arrival_through_bmc_secure (AccessDiscover through BmcSecure Apply, including the fold's Apply-discharge mint) executing as natively emitted code in a claim frame. WHAT THAT MUST BE SUFFICIENT FOR: test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world, still calling that entry with Apply+grant and still asserting the Applied route, measures under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives. Deleting the identity, hard-coding discharges: [] in the entry, or relocating the claim off the required gate satisfies none of it.", + } +} diff --git a/dag/gunbc/secret_provision.dag b/dag/gunbc/secret_provision.dag index cde05b4d270..442acd7c506 100644 --- a/dag/gunbc/secret_provision.dag +++ b/dag/gunbc/secret_provision.dag @@ -275,6 +275,15 @@ data mtcollins1_bmc_gunbc_secret_ref: SecretRef = secret_ref_pin_version( // then the first rotation (gunbc.machine_intake_mtjade1_bmc_secure_observation). data mtjade1_bmc_gunbc_secret_ref: SecretRef = fleet_secret_ref(secret_id: "bmc-mtjade1-gunbc") +// FIRST VERSION THE ARRIVAL SA IS GRANTED (operator sign-off msg_f03558d1). The locus row stays +// pending for JadeManagedBmcSecretStanding until FamilyObserved; the accessor names versions/1, +// which gcp-iam-converge binds once the container exists. Creating the container is this +// authority's mint, not a hand gcloud. +data mtjade1_bmc_gunbc_arrival_accessor_ref: SecretRef = secret_ref_pin_version( + ref: mtjade1_bmc_gunbc_secret_ref, + version: "1", +) + fn secret_ref_pin_version(ref: SecretRef, version: NonEmptyStr) -> SecretRef { SecretRef { project: ref.project, diff --git a/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag b/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag index e826abf47a3..65dd42e4f25 100644 --- a/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag +++ b/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag @@ -14,6 +14,8 @@ import gunbc.auth.standing_operator_grant { standing_grant_covers, standing_grant_scope_matches, standing_grant_hosts, StandingGrantFabricGroup, StandingGrantHost, StandingD0ReleaseToFleet, StandingArmLaunch, StandingHostEffectRecover, + StandingJadeArrivalArchive, StandingJadeFirmwareQualification, StandingBmcSecureAccountWrite, + standing_grant_arm_interlock, } import gunbc.auth.authorization_pattern_selection { PrivilegedEffect, ApiSurface, @@ -22,7 +24,7 @@ import gunbc.auth.authorization_pattern_selection { IrreversibleEffect, NoBillingConsequence, WitnessDischarge, NoWitnessDischarge, StandingRulingUnderInterlock, StandingDestructiveAuthorization, - InterlockPending, UnconditionalStanding, InterlockedBy, + InterlockPending, InterlockedBy, FederatedScopedGrant, OperatorApprovedCapability, PatternSelected, NoAdmissiblePattern, AuthorizationPatternSelection, @@ -123,6 +125,10 @@ test fn w_mtcollins1_is_not_covered() -> Bool { test fn w_an_effect_outside_the_mtjade1_arms_is_not_covered() -> Bool { standing_grant_scope_matches(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }) + && standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingJadeArrivalArchive) + && standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingJadeFirmwareQualification) + && standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingBmcSecureAccountWrite) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtcollins1 }, effect: StandingBmcSecureAccountWrite) && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingD0ReleaseToFleet) && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingArmLaunch) && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingHostEffectRecover) @@ -139,9 +145,18 @@ test fn w_the_ruling_text_is_the_operator_quote() -> Bool { && match mtjade1_live_standing_grant.ruling.interlock { InterlockPending { obligation: _ } => true InterlockedBy { hold: _ } => false - UnconditionalStanding { reason: _ } => false } && !standing_ruling_discharges_irreversibility(r: mtjade1_live_standing_grant.ruling) + && match standing_grant_arm_interlock(g: mtjade1_live_standing_grant, e: StandingBmcSecureAccountWrite) { + InterlockedBy { hold: h } => + (h.module_path as String) == "gunbc.machine_intake_bmc_rotation_route" + && (h.decl_name as String) == "admit_rotation_apply" + InterlockPending { obligation: _ } => false + } + && match standing_grant_arm_interlock(g: mtjade1_live_standing_grant, e: StandingJadeFirmwareQualification) { + InterlockPending { obligation: _ } => true + InterlockedBy { hold: _ } => false + } } test fn w_the_selection_fold_over_true_mtjade1_session_attributes() -> Bool { @@ -162,6 +177,12 @@ test fn w_the_selection_fold_over_true_mtjade1_session_attributes() -> Bool { && !selected_federated(s: fw_ruled) } +test fn w_operator_ssh_bmc_write_still_selects_operator_approved_capability() -> Bool { + selected_approved(s: select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: mtjade1_discharge))) + && selected_approved(s: select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: NoWitnessDischarge))) + && !selected_federated(s: select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: mtjade1_discharge))) +} + fn mtjade1_bindable_identity() -> WorkloadIdentityStanding { WorkloadIdentityBindable { member: "ghrunner on srv1, the dispatched fleet-converge run's host principal on the placed fabric DB host" as NonEmptyStr } } @@ -179,6 +200,14 @@ fn mtjade1_bindable_boot_effect(discharge: WitnessDischarge) -> PrivilegedEffect } } +fn mtjade1_pending_ruling() -> StandingDestructiveAuthorization { + StandingDestructiveAuthorization { + ruling_text: mtjade1_live_standing_grant.ruling.ruling_text, + effect_subject: mtjade1_live_standing_grant.ruling.effect_subject, + interlock: InterlockPending { obligation: "hold not named" as NonEmptyStr }, + } +} + fn mtjade1_interlocked_ruling() -> StandingDestructiveAuthorization { StandingDestructiveAuthorization { ruling_text: mtjade1_live_standing_grant.ruling.ruling_text, @@ -188,7 +217,7 @@ fn mtjade1_interlocked_ruling() -> StandingDestructiveAuthorization { } test fn w_bindable_boot_pending_interlock_refuses() -> Bool { - let pending = select_authorization_pattern(e: mtjade1_bindable_boot_effect(discharge: mtjade1_discharge)) + let pending = select_authorization_pattern(e: mtjade1_bindable_boot_effect(discharge: StandingRulingUnderInterlock { ruling: mtjade1_pending_ruling() })) no_admissible(s: pending) && !selected_federated(s: pending) } @@ -197,7 +226,7 @@ test fn w_bindable_boot_interlocked_selects_federation() -> Bool { } test fn w_census_pending_interlock_is_a_defect() -> Bool { - match ruling_discharge_interlock_defect(site_ref: decl_ref(module_path: "gunbc.auth.standing_operator_grant", decl_name: "mtjade1_live_standing_grant"), ruling: mtjade1_live_standing_grant.ruling) { + match ruling_discharge_interlock_defect(site_ref: decl_ref(module_path: "gunbc.auth.standing_operator_grant", decl_name: "mtjade1_live_standing_grant"), ruling: mtjade1_pending_ruling()) { Present { value: _ } => true Absent => false } diff --git a/dag/test/claim/authorization_pattern_selection_witness_test.dag b/dag/test/claim/authorization_pattern_selection_witness_test.dag index 6697a259935..7b2e19b07d9 100644 --- a/dag/test/claim/authorization_pattern_selection_witness_test.dag +++ b/dag/test/claim/authorization_pattern_selection_witness_test.dag @@ -15,6 +15,7 @@ import gunbc.auth.authorization_pattern_selection { PatternSelected, ManualStepRequired, NoAdmissiblePattern, PatternSelectionNeedsEvidence, PatternSelectionNeedsPolicy, PatternSelectionRefused, AuthorizationPatternSelection, + InterlockPending, InterlockedBy, select_authorization_pattern, witness_required, } import gunbc.auth.privileged_effect_census { @@ -22,8 +23,9 @@ import gunbc.auth.privileged_effect_census { unrostered_unreasoned_divergences, rostered_but_not_diverging, follow_up_sites, reasoned_divergences, reasoned_divergences_with_fired_triggers, site_verdict, Conforms, DivergesWithReason, Diverges, SiteNotDecidable, - mtcollins1_boot_effect, privileged_effect_interlocks, interlocked_sites_missing_from_census, rulings_without_a_rostered_interlock, + mtcollins1_boot_effect, privileged_effect_interlocks, privileged_effect_interlock_hold, interlocked_sites_missing_from_census, rulings_without_a_rostered_interlock, ruling_roots_missing_from_census, census_sites_outside_ruling_roots, + mtcollins1_operator_ruling, RealizedFederatedGrant, RealizedRunSelected, RealizedApprovalCapability, RealizedHumanStep, RealizedOperatorSession, RealizedUnauthorized, } import std.human_intervention { @@ -363,7 +365,23 @@ test fn a_standing_ruling_does_not_discharge_a_wide_credential() -> Bool { // EVERY STANDING RULING IN THE CENSUS NAMES AN INTERLOCK ROSTERED AGAINST ITS OWN SITE. test fn every_standing_ruling_has_its_interlock_rostered() -> Bool { - (rulings_without_a_rostered_interlock() |> count) == 0 + (rulings_without_a_rostered_interlock() |> count) == 1 + && match rulings_without_a_rostered_interlock().first() { + Present { value: s } => + declaration_ref_display_key(ref: s) == "gunbc.auth.mtjade1_arrival_federation::mtjade1_arrival_firmware_qualification_effect" + Absent => false + } +} + +test fn pending_rulings_do_not_invent_a_rostered_hold() -> Bool { + match privileged_effect_interlock_hold(interlock: InterlockPending { obligation: "unnamed" as NonEmptyStr }) { + Absent => true + Present { value: _ } => false + } + && match privileged_effect_interlock_hold(interlock: mtcollins1_operator_ruling.interlock) { + Absent => false + Present { value: h } => (h.decl_name as String) == "UnitHoldProof" + } } // THE CENSUS SHOWS THE INTERLOCK: every interlocked site is a census row, and the boot's names the diff --git a/dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag b/dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag index 3172ed2d2e3..f3ce2f196b6 100644 --- a/dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag +++ b/dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag @@ -11,6 +11,12 @@ import std.durable_exclusive_hold { HoldReleaseAgainstAnotherGeneration, HoldReleaseSlotUndecodable, HoldReleaseObservationUnavailable, } import gunbc.durable_cas_file_store { cas_file_slot_path } +import std.process { ProcessExit, ExitSuccess, ExitFailure } +import gunbc.machine_intake_arrival_subject { admit_arrival_subject, ArrivalSubjectInPopulation } +import gunbc.machine_intake_arrival_interlock { + arrival_after_acquire, arrival_archive_slot_acquire, arrival_archive_slot_release, + ArrivalArchiveSlotAcquired, ArrivalArchiveSlotAcquireRefused, ArrivalArchiveSlotReleaseRefused, +} import gunbc.durable_exclusive_hold_file_store { FileHoldAcquireOutcome, FileHoldAcquired, FileHoldOccupied, FileHoldAcquireLost, FileHoldAcquireStoreUnavailable, FileHoldSlotUndecodable, FileHoldKeyNotSlotAddressable, @@ -353,3 +359,70 @@ test fn a_release_committed_after_the_slot_moved_is_lost_not_successful_by_real_ && no_third && removed.success } + +test fn w_after_acquire_invokes_the_real_slot_release() -> Bool { + let root_path = wh_fresh_root() + let root = root_path as NonEmptyStr + match admit_arrival_subject(wire: "mtjade1") { + ArrivalSubjectInPopulation { subject: s } => + match arrival_after_acquire( + outcome: arrival_archive_slot_acquire( + root: root, + subject: s, + owner: "arrival-release-inhabitance" as DurableHoldOwnerRef, + ), + body: fn() { ExitSuccess }, + release_fn: fn(h) { arrival_archive_slot_release(root: root, held: h) }, + ) { + ExitFailure { code: _, reason: _ } => + shell.Remove.RecursiveForce(path: root_path).success && false + ExitSuccess => + match arrival_archive_slot_acquire( + root: root, + subject: s, + owner: "arrival-release-inhabitance-2" as DurableHoldOwnerRef, + ) { + ArrivalArchiveSlotAcquireRefused { cause: _ } => + shell.Remove.RecursiveForce(path: root_path).success && false + ArrivalArchiveSlotAcquired { held: _ } => + shell.Remove.RecursiveForce(path: root_path).success + } + } + _ => shell.Remove.RecursiveForce(path: root_path).success && false + } +} + +fn arrival_body_writes_marker(marker: String) -> ProcessExit { + if Filesystem.WriteCreateNew(path: marker, content: "BODY").success { + ExitSuccess + } else { + ExitFailure { code: 1, reason: "marker write failed" } + } +} + +test fn w_failed_acquire_runs_no_body() -> Bool { + let root_path = wh_fresh_root() + let marker = concat(root_path, "/body-ran") + match arrival_after_acquire( + outcome: ArrivalArchiveSlotAcquireRefused { cause: "slot occupied" as NonEmptyStr }, + body: fn() { arrival_body_writes_marker(marker: marker) }, + release_fn: fn(h) { + ArrivalArchiveSlotReleaseRefused { cause: "release must not run on refused acquire" as NonEmptyStr } + }, + ) { + ExitSuccess => shell.Remove.RecursiveForce(path: root_path).success && false + ExitFailure { code: _, reason: _ } => + !Filesystem.Read(path: marker).success && shell.Remove.RecursiveForce(path: root_path).success + } +} + +test fn w_refused_acquire_body_writes_a_marker_when_called_directly() -> Bool { + let root_path = wh_fresh_root() + let marker = concat(root_path, "/body-ran") + match arrival_body_writes_marker(marker: marker) { + ExitFailure { code: _, reason: _ } => + shell.Remove.RecursiveForce(path: root_path).success && false + ExitSuccess => + Filesystem.Read(path: marker).success && shell.Remove.RecursiveForce(path: root_path).success + } +} diff --git a/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag index ea735d8e396..79c50ebb349 100644 --- a/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag @@ -17,7 +17,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // outside its module; this witness hands the source to the compiler through the diagnostic-census // harness and requires SoleConstructorViolation at each SUBJECT by name. The class-scoped control shows // a clean source reading the same modules through their real producers emits none. -data forged_probe_source: String = "module probe_arrival_converge_forged\n\nimport std.types { Int, List, NonEmptyStr, String }\nimport std.decl_ref { decl_ref }\nimport gunbc.machine_intake_phase { Arrival, AccessDiscover, IntakePhase }\nimport gunbc.machine_intake_subject { MachineIntakeSubject, BoardSerialObservation, AssemblyManifest, UnitKey }\nimport gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding }\nimport gunbc.machine_intake_mtjade1_factory_network { ObservedBmcNetwork }\nimport gunbc.machine_intake_mtjade1_access_observation {\n CurrentManagerRead, RecordedManagerIdentityObservation, ControllerClockReading, current_manager_read_of,\n FruRead, SmbiosRead, FruIdentityFields, RecordedFruObservation, RecordedSmbiosObservation, SolSessionAttribution,\n}\nimport gunbc.fleet.convergence_fold {\n AdmittedConvergencePlan, RankedStep, StepInstanceKey, ConvergenceRunId, StepSubjectKey, ConvergenceOrderAuthority, ConvergencePlanningAuthority,\n ConvergenceReceiptProjection, ConvergenceRunLedger, ConvergedRun, StepInstanceStanding,\n convergence_planning_authority, convergence_receipt_projection,\n}\nimport gunbc.machine_intake_arrival_converge {\n AccessDiscoverEstablished, IdentityBoundProvisional, ReadOnlyPhaseRemedy, AccessObservation,\n IdentityBindInputs, ArrivalStepReceipt, ArrivalStepRefusal, ArrivalStepIncomplete, BoardSerialAgreement,\n}\n\nfn forged_access(key: StepInstanceKey, access: AccessObservation, route: BmcRotationRouteStanding) -> AccessDiscoverEstablished {\n AccessDiscoverEstablished { key: key, access: access, route: route }\n}\n\nfn forged_identity(key: StepInstanceKey, subject: MachineIntakeSubject) -> IdentityBoundProvisional {\n IdentityBoundProvisional { key: key, consumed_access: key, subject: subject }\n}\n\nfn forged_plan(steps: List>, key: StepInstanceKey) -> AdmittedConvergencePlan {\n AdmittedConvergencePlan { authority: key.step_identity, steps: steps }\n}\n\nfn forged_remedy() -> ReadOnlyPhaseRemedy {\n ReadOnlyPhaseRemedy { phase: AccessDiscover }\n}\n\nfn any_rank(phase: IntakePhase) -> Int? {\n Present { value: 0 }\n}\n\nfn authored_order() -> ConvergenceOrderAuthority {\n ConvergenceOrderAuthority { authority: decl_ref(module_path: \"gunbc.machine_intake_phase\", decl_name: \"arrival_phases_all\"), rank_of: any_rank }\n}\n\nfn forged_planning_literal() -> ConvergencePlanningAuthority {\n ConvergencePlanningAuthority { order: authored_order() }\n}\n\nfn forged_planning_via_mint() -> ConvergencePlanningAuthority {\n convergence_planning_authority(order: authored_order())\n}\n\nfn rekey(r: ArrivalStepReceipt) -> StepInstanceKey {\n StepInstanceKey { run: \"forged\" as ConvergenceRunId, step_identity: decl_ref(module_path: \"gunbc.machine_intake_arrival_converge\", decl_name: \"access_discover\"), subject: \"mtjade1\" as StepSubjectKey }\n}\n\nfn consumed_nothing(r: ArrivalStepReceipt) -> List {\n []\n}\n\nfn forged_projection_literal() -> ConvergenceReceiptProjection {\n ConvergenceReceiptProjection { key_of: rekey, consumed_of: consumed_nothing }\n}\n\nfn forged_projection_via_mint() -> ConvergenceReceiptProjection {\n convergence_receipt_projection(key_of: rekey, consumed_of: consumed_nothing)\n}\n\nfn forged_ledger(key: StepInstanceKey, instances: List>) -> ConvergenceRunLedger {\n ConvergenceRunLedger { run: key.run, subject: key.subject, order_authority: key.step_identity, instances: instances }\n}\n\nfn forged_converged_run(ledger: ConvergenceRunLedger) -> ConvergedRun {\n ConvergedRun { ledger: ledger }\n}\n\nfn forged_manager_read(identity: RecordedManagerIdentityObservation, clock: ControllerClockReading) -> CurrentManagerRead {\n CurrentManagerRead { identity: identity, controller_clock: clock }\n}\n\nfn forged_manager_read_via_mint(content: String, endpoint: ObservedBmcNetwork) -> CurrentManagerRead {\n current_manager_read_of(content: content, expected_sha256: \"00\" as NonEmptyStr, endpoint: endpoint, link: none, capture_path: \"forged\" as NonEmptyStr)\n}\n\nfn forged_identity_inputs(fru: FruRead, smbios: SmbiosRead, units: List) -> IdentityBindInputs {\n IdentityBindInputs { fru: fru, smbios: smbios, other_units: units }\n}\n\nfn forged_fru(fields: FruIdentityFields) -> RecordedFruObservation {\n RecordedFruObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", fields: fields }\n}\n\nfn forged_smbios(attribution: SolSessionAttribution) -> RecordedSmbiosObservation {\n RecordedSmbiosObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", sol_session: attribution, serial: \"B810301000412080005AJ0C1\" }\n}\n\nfn forged_agreement(fru: RecordedFruObservation, smbios: RecordedSmbiosObservation) -> BoardSerialAgreement {\n BoardSerialAgreement { fru: fru, smbios: smbios, serial: \"B810301000412080005AJ0C1\" }\n}\n" +data forged_probe_source: String = "module probe_arrival_converge_forged\n\nimport std.types { Bool, Int, List, NonEmptyStr, String }\nimport std.decl_ref { decl_ref }\nimport gunbc.machine_intake_phase { Arrival, AccessDiscover, IntakePhase }\nimport gunbc.machine_intake_subject { MachineIntakeSubject, BoardSerialObservation, AssemblyManifest, UnitKey }\nimport gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding }\nimport gunbc.machine_intake_mtjade1_factory_network { ObservedBmcNetwork }\nimport gunbc.machine_intake_mtjade1_access_observation {\n CurrentManagerRead, RecordedManagerIdentityObservation, ControllerClockReading, current_manager_read_of,\n FruRead, SmbiosRead, FruIdentityFields, RecordedFruObservation, RecordedSmbiosObservation, SolSessionAttribution,\n}\nimport gunbc.fleet.convergence_fold {\n AdmittedConvergencePlan, RankedStep, StepInstanceKey, ConvergenceRunId, StepSubjectKey, ConvergenceOrderAuthority, ConvergencePlanningAuthority,\n ConvergenceReceiptProjection, ConvergenceRunLedger, ConvergedRun, StepInstanceStanding,\n convergence_planning_authority, convergence_receipt_projection,\n}\nimport gunbc.machine_intake_arrival_converge {\n AccessDiscoverEstablished, IdentityBoundProvisional, ReadOnlyPhaseRemedy, AccessObservation,\n IdentityBindInputs, ArrivalStepReceipt, ArrivalStepRefusal, ArrivalStepIncomplete, BoardSerialAgreement,\n}\n\nfn forged_access(key: StepInstanceKey, access: AccessObservation, route: BmcRotationRouteStanding) -> AccessDiscoverEstablished {\n AccessDiscoverEstablished { key: key, access: access, route: route }\n}\n\nfn forged_identity(key: StepInstanceKey, subject: MachineIntakeSubject) -> IdentityBoundProvisional {\n IdentityBoundProvisional { key: key, consumed_access: key, subject: subject }\n}\n\nfn forged_plan(steps: List>, key: StepInstanceKey) -> AdmittedConvergencePlan {\n AdmittedConvergencePlan { authority: key.step_identity, steps: steps }\n}\n\nfn forged_remedy() -> ReadOnlyPhaseRemedy {\n ReadOnlyPhaseRemedy { phase: AccessDiscover }\n}\n\nfn any_rank(phase: IntakePhase) -> Int? {\n Present { value: 0 }\n}\n\nfn authored_order() -> ConvergenceOrderAuthority {\n ConvergenceOrderAuthority { authority: decl_ref(module_path: \"gunbc.machine_intake_phase\", decl_name: \"arrival_phases_all\"), rank_of: any_rank }\n}\n\nfn forged_planning_literal() -> ConvergencePlanningAuthority {\n ConvergencePlanningAuthority { order: authored_order() }\n}\n\nfn forged_planning_via_mint() -> ConvergencePlanningAuthority {\n convergence_planning_authority(order: authored_order())\n}\n\nfn rekey(r: ArrivalStepReceipt) -> StepInstanceKey {\n StepInstanceKey { run: \"forged\" as ConvergenceRunId, step_identity: decl_ref(module_path: \"gunbc.machine_intake_arrival_converge\", decl_name: \"access_discover\"), subject: \"mtjade1\" as StepSubjectKey }\n}\n\nfn consumed_nothing(r: ArrivalStepReceipt) -> List {\n []\n}\n\nfn auth_never(r: ArrivalStepReceipt) -> Bool {\n false\n}\n\nfn forged_projection_literal() -> ConvergenceReceiptProjection {\n ConvergenceReceiptProjection { key_of: rekey, consumed_of: consumed_nothing, authorization_required_of: auth_never }\n}\n\nfn forged_projection_via_mint() -> ConvergenceReceiptProjection {\n convergence_receipt_projection(key_of: rekey, consumed_of: consumed_nothing, authorization_required_of: auth_never)\n}\n\nfn forged_ledger(key: StepInstanceKey, instances: List>) -> ConvergenceRunLedger {\n ConvergenceRunLedger { run: key.run, subject: key.subject, order_authority: key.step_identity, instances: instances }\n}\n\nfn forged_converged_run(ledger: ConvergenceRunLedger) -> ConvergedRun {\n ConvergedRun { ledger: ledger }\n}\n\nfn forged_manager_read(identity: RecordedManagerIdentityObservation, clock: ControllerClockReading) -> CurrentManagerRead {\n CurrentManagerRead { identity: identity, controller_clock: clock }\n}\n\nfn forged_manager_read_via_mint(content: String, endpoint: ObservedBmcNetwork) -> CurrentManagerRead {\n current_manager_read_of(content: content, expected_sha256: \"00\" as NonEmptyStr, endpoint: endpoint, link: none, capture_path: \"forged\" as NonEmptyStr)\n}\n\nfn forged_identity_inputs(fru: FruRead, smbios: SmbiosRead, units: List) -> IdentityBindInputs {\n IdentityBindInputs { fru: fru, smbios: smbios, other_units: units }\n}\n\nfn forged_fru(fields: FruIdentityFields) -> RecordedFruObservation {\n RecordedFruObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", fields: fields }\n}\n\nfn forged_smbios(attribution: SolSessionAttribution) -> RecordedSmbiosObservation {\n RecordedSmbiosObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", sol_session: attribution, serial: \"B810301000412080005AJ0C1\" }\n}\n\nfn forged_agreement(fru: RecordedFruObservation, smbios: RecordedSmbiosObservation) -> BoardSerialAgreement {\n BoardSerialAgreement { fru: fru, smbios: smbios, serial: \"B810301000412080005AJ0C1\" }\n}\n" data harness_control_source: String = "module probe_arrival_converge_harness_control\nimport gunbc.fleet.convergence_fold { ConvergencePlanAdmission, admit_convergence_plan }\nimport gunbc.machine_intake_phase { IntakePhase }\nimport gunbc.machine_intake_arrival_converge { arrival_planning_authority, arrival_receipt_projection, ArrivalStepReceipt }\nimport gunbc.fleet.convergence_fold { ConvergenceReceiptProjection }\nimport gunbc.machine_intake_mtjade1_access_observation { CurrentManagerRead, read_mtjade1_current_manager_read }\nfn admission() -> ConvergencePlanAdmission { admit_convergence_plan(planning: arrival_planning_authority(), steps: []) }\nfn projection() -> ConvergenceReceiptProjection { arrival_receipt_projection() }\nfn read() -> CurrentManagerRead { read_mtjade1_current_manager_read() }\n" @@ -91,3 +91,18 @@ test fn authored_arrival_inputs_are_refused() -> Bool { && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "RecordedSmbiosObservation") >= 1 && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "BoardSerialAgreement") >= 1 } + +data outside_mtjade1_bmc_reading_probe_source: String = "module probe_mtjade1_bmc_reading_outside\nimport std.types { String }\nimport test.claim.machine_intake_arrival_converge_witness { mtjade1_intake_subject, mtjade1_dry_applied_bmc, mtjade1_fetched_generation, mtjade1_bmc_goal }\nimport gunbc.machine_intake_arrival_converge { BmcSecureApplyInputs }\nimport gunbc.machine_intake_bmc_secure { ManagedCredentialGenerationFetched }\nfn leak_apply() -> BmcSecureApplyInputs? { mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) }\nfn leak_generation() -> ManagedCredentialGenerationFetched? { mtjade1_fetched_generation(current: mtjade1_bmc_goal().managed, secret: \"bmc-lab-o1b-gunbc\", version: \"2\", bytes: \"x\") }\n" + +data bmc_account_state_observation_literal_probe_source: String = "module probe_bmc_account_state_observation_literal\nimport std.types { List }\nimport std.scoped_authorization { AttemptIdentity }\nimport gunbc.clock_read { ObserverClockInstant }\nimport gunbc.machine_intake_receipt { EvidenceRef }\nimport gunbc.machine_intake_subject { MachineIntakeSubject }\nimport gunbc.machine_intake_bmc_secure {\n BmcAccountStateObservation, ManagedCredentialReference, ObservedCredentialProbe, ObservedPublishedLanProbe, ObservedPublishedAccount, ControllerClockReading,\n}\nimport extdeps.bmc.endpoint { BmcControllerEndpoint }\nimport extdeps.bmc.capability { BmcFirmwareReleaseIdentity }\nimport extdeps.bmc.ipmi_channel { IpmiUserId, IpmiControllerChannelCensus }\nfn leak(\n subject: MachineIntakeSubject,\n endpoint: BmcControllerEndpoint,\n firmware: BmcFirmwareReleaseIdentity,\n managed: ManagedCredentialReference,\n managed_user: IpmiUserId,\n attempt: AttemptIdentity,\n read_floor: ObserverClockInstant,\n managed_probe: ObservedCredentialProbe,\n channel_census: IpmiControllerChannelCensus,\n census_evidence: EvidenceRef,\n census_observed_at: ObserverClockInstant,\n published_probes: List,\n published_user: IpmiUserId,\n published_account: ObservedPublishedAccount,\n break_glass: ManagedCredentialReference,\n break_glass_probe: ObservedCredentialProbe,\n controller_clock: ControllerClockReading?,\n) -> BmcAccountStateObservation {\n BmcAccountStateObservation {\n subject: subject,\n endpoint: endpoint,\n firmware: firmware,\n managed: managed,\n managed_user: managed_user,\n attempt: attempt,\n read_floor: read_floor,\n managed_probe: managed_probe,\n channel_census: channel_census,\n census_evidence: census_evidence,\n census_observed_at: census_observed_at,\n published_probes: published_probes,\n published_user: published_user,\n published_account: published_account,\n break_glass: break_glass,\n break_glass_probe: break_glass_probe,\n controller_clock: controller_clock,\n }\n}\n" + +test fn the_mtjade1_bmc_reading_helpers_refuse_an_outside_caller() -> Bool { + let c = compile_dag_diagnostic_census(outside_mtjade1_bmc_reading_probe_source) + blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "mtjade1_dry_applied_bmc") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "mtjade1_fetched_generation") >= 1 +} + +test fn a_bmc_account_state_observation_literal_is_refused_outside_its_mint() -> Bool { + let c = compile_dag_diagnostic_census(bmc_account_state_observation_literal_probe_source) + blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "BmcAccountStateObservation") >= 1 +} diff --git a/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag index 2849178fd7f..22e510c0e60 100644 --- a/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag @@ -1,6 +1,6 @@ module test.claim.machine_intake_arrival_converge_witness -import std.types { Bool, Int, List, NonEmptyStr, String } +import std.types { Bool, EpochMs, Int, List, NonEmptyStr, Secret, String } import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } import std.scoped_authorization { AttemptIdentity } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } @@ -8,11 +8,12 @@ import v2.std.algebra { filter, length } import extdeps.crypto.mac { MacKeyId } import extdeps.bmc.endpoint { AmiMegaRac, OpenBmc, BmcControllerEndpoint } import gunbc.auth.approval_capability { ApprovalCapabilityClaims, ProposeApprove, approval_capability_protocol } +import product.host_identity { HostIdentity, host_identity_eq } import gunbc.auth.approval_broker { Redemption, RedemptionAdmitted } -import gunbc.machine_intake_phase { Arrival, AccessDiscover, IdentityBindProvisional, PriorLifeBoundary, BmcSecure, IntakePhase } +import gunbc.machine_intake_phase { Arrival, AccessDiscover, IdentityBindProvisional, PriorLifeBoundary, BmcSecure, BootDeliveryEstablish, IntakePhase, machine_qualification_policy } import gunbc.machine_intake_subject { AssemblyManifest, BoardSerialObservation, BmcFru, HostSmbios, ChassisComponent, ComponentIdentity, BoardSerialAbsent, - FirmwareEntry, FirmwareManifest, UnitKey, + FirmwareEntry, FirmwareManifest, UnitKey, MachineIntakeSubject, IntakeAttemptId, qualification_subject_of, } import gunbc.machine_intake_mtjade1_access_observation { @@ -24,6 +25,7 @@ import gunbc.machine_intake_bmc_rotation_route { RedfishAccountPasswordWrite, IpmiSetUserPassword, IpmiSetUserPrivilegeLimit, ObservedSurfaceRead, PublicStandardOperation, RotationApplyAdmitted, RotationApplyRouteNotGrounded, rotation_apply_authority, rotation_route_request_identity, rotation_route_is_grounded, admit_rotation_apply, + rotation_route_ungrounded, rotation_route_from_citation, route_qualification_authority, } import gunbc.host_convergence_census { HostConvergenceCensus, CensusWellFormed, host_convergence_census_rows, host_convergence_census_standing, @@ -40,14 +42,27 @@ import gunbc.fleet.convergence_fold { admit_convergence_plan, classify_convergence_plan, PlanClassifiedAdmissible, PlanClassifiedRefused, ConvergenceReceiptProjection, convergence_receipt_projection, fold_convergence_run, step_instance_key, step_outcome_receipt, step_outcome_refusal, + ungated_readonly_step, AuthorizationUndischarged, instance_authorization, + step_instance_key_eq, InstanceAuthorization, } import gunbc.machine_intake_prior_life_boundary { DryPriorLifeWorld, DryArchiveStore, DryArchiveStoreLosesWrites, ArchiveWrittenButNotReadBack, ArchiveWritten, LogsArchivedWithBaselineCursor, mt_jade_platform_ref, prior_life_receipt_archive, prior_life_receipt_application, prior_life_receipt_boundary, prior_life_receipt_realization, prior_life_receipt_consumed_identity, prior_life_archive_digest, baseline_cursor_archive, baseline_cursor_sel_final_record, } -import std.content_hash { content_hash_equal } +import std.content_hash { content_hash_equal, content_hash_of_value } +import gunbc.machine_intake_receipt { EvidenceRef } import test.claim.machine_intake_prior_life_boundary_witness { prior_life_minimal_dry_world } +import gunbc.auth.standing_operator_grant { + mtjade1_live_standing_grant, standing_grant_covers, StandingGrantHost, StandingBmcSecureAccountWrite, + StandingOperatorGrant, +} +import gunbc.auth.authorization_pattern_selection { + InterlockPending, InterlockedBy, StandingDestructiveAuthorization, + select_authorization_pattern, StandingRulingUnderInterlock, NoWitnessDischarge, + PatternSelected, OperatorApprovedCapability, AuthorizationPatternSelection, +} +import gunbc.fleet_host_identity { operator_host_mtjade1, operator_host_mtcollins1 } import gunbc.machine_intake_arrival_converge { ArrivalPrefixVerdict, ArrivalRunFolded, ArrivalPlanRefused, ArrivalPrefixUnstepped, ArrivalStepReceipt, AccessDiscoverReceipt, IdentityBindReceipt, PriorLifeBoundaryReceipt, ArrivalStepRefusal, @@ -57,8 +72,38 @@ import gunbc.machine_intake_arrival_converge { access_discover_step_ref, identity_bind_provisional_step_ref, arrival_order_authority, arrival_planning_authority, arrival_prefix_through, arrival_prefix_steps, ArrivalPrefixStepped, ArrivalPrefixPhaseUnstepped, arrival_prefix_last, arrival_receipt_projection, access_discover, identity_bind_provisional, - converge_mtjade1_arrival_prefix, converge_arrival_prefix, mtjade1_identity_bind_inputs, + converge_mtjade1_arrival_prefix, converge_mtjade1_arrival_through_bmc_secure, converge_arrival_prefix, converge_arrival_through_bmc_secure, mtjade1_identity_bind_inputs, + bmc_secure_step_ref, BmcSecureReceipt, + BmcSecureInputs, BmcSecureApplyInputs, BmcSecureAuthorizationUndischarged, BmcSecureApplyInputsMissing, + BmcSecureApplicationForAnotherInstance, BmcSecureApplicationNotTheInspectedTransition, + grant_discharges_bmc_secure_account_write, + capability_discharges_bmc_secure_account_write, + discharge_bmc_secure_apply, + bound_bmc_secure_host, + bmc_secure_bound, +} +import gunbc.machine_intake_bmc_secure { + BmcSecureGoal, BmcAccountStateObservation, dry_read_bmc_account_state, dry_apply_bmc_account_plan, plan_bmc_account_action, + BmcAccountPlanned, BmcAccountPlanRefused, PublishedAccountRetired, ManagedCredentialReference, + BmcSecurePhaseNoop, BmcSecurePhaseApplied, ControllerClockReading, + observation_with_controller_clock, apply_with_diverged_controller_clock, controller_clock_reading_same, + admit_stored_generation, admit_fetched_generation, dry_bmc_account_instant, + GenerationStored, GenerationStoreRefused, GenerationFetched, GenerationFetchRefused, ManagedCredentialGenerationFetched, } +import gunbc.auth.secret_ref_credential { SecretCredentialFetch, SecretCredentialReady } +import extdeps.cloud.gcp.secret_manager { SmResolvedVersionIdentity } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { uri_https } +import gunbc.deployment_risk { TestRisk } +import extdeps.bmc.types { AccountRoleAdministrator } +import extdeps.bmc.capability { BmcFirmwareReleaseIdentity, bmc_firmware_release_identity_of_wire } +import extdeps.bmc.ipmi_channel { + IpmiControllerChannelCensus, IpmiMedium8023Lan, IpmiMediumSerialAsync, IpmiPrivilegeNoAccess, IpmiPrivilegeAdministrator, + IpmiUserId, ipmi_controller_channel_census, ipmi_lan_channel_member, ipmi_non_lan_channel_member, ipmi_user_channel_access, +} +import extdeps.network.ipv4 { ipv4_address } +import extdeps.cloud.gcp.secret_ref { HashPending, SecretRef } +import gunbc.bmc_model { BmcWorld, BmcIpmiUser, BmcPowerOn, bmc_world, bmc_with_ipmi_users, bmc_with_ipmi_user_access } data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree @@ -109,6 +154,7 @@ fn access_established_as_read(s: StepInstanceStanding false PriorLifeBoundaryReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false InstanceIncomplete { key: _, cause: _ } => false @@ -132,6 +178,7 @@ fn identity_bound_from_committed_captures(s: StepInstanceStanding false PriorLifeBoundaryReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false InstanceIncomplete { key: _, cause: _ } => false @@ -169,6 +216,7 @@ fn prior_life_archived_from_the_bound_subject(s: StepInstanceStanding false IdentityBindReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false InstanceIncomplete { key: _, cause: _ } => false @@ -201,6 +249,407 @@ test fn w_mtjade1_converges_the_prefix_through_its_dry_prior_life_archive() -> B } } +data mtjade1_bmc_read_at: EpochMs = 1791072000000 +data mtjade1_bmc_plan_at: EpochMs = 1791072030000 +data mtjade1_bmc_apply_at: EpochMs = 1791072040000 +data mtjade1_bmc_readback_at: EpochMs = 1791072050000 +data mtjade1_managed_ipmi_user: IpmiUserId = 3 +data mtjade1_published_ipmi_user: IpmiUserId = 2 +data mtjade1_managed_password_v2: String = "managed-generation-2!" +data mtjade1_route_fixture_citation: ExternalAuthority = ExternalAuthority { + uri: uri_https(locator: "fixture-not-an-authority.invalid/test.claim.machine_intake_arrival_converge_witness/mtjade1-route" as NonEmptyStr), +} + +fn mtjade1_intake_subject_for(attempt: IntakeAttemptId) -> MachineIntakeSubject { + MachineIntakeSubject { + subject: qualification_subject_of(unit_key: "B810301000412080005AJ0C1" as UnitKey, assembly: expected_mtjade1_assembly, firmware: expected_mtjade1_firmware), + attempt_id: attempt, + } +} + +fn mtjade1_intake_subject() -> MachineIntakeSubject { + mtjade1_intake_subject_for(attempt: "o1c1-witness-run-a" as IntakeAttemptId) +} + +fn mtjade1_bmc_endpoint() -> BmcControllerEndpoint { + BmcControllerEndpoint { host: "192.168.1.246" } +} + +fn mtjade1_bmc_firmware() -> BmcFirmwareReleaseIdentity { + bmc_firmware_release_identity_of_wire(family: AmiMegaRac, wire: "2.11.104000" as NonEmptyStr) +} + +fn cited_mtjade1_managed_route() -> BmcRotationRouteStanding + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + ] +{ + rotation_route_from_citation( + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + request: IpmiSetUserPassword { user: mtjade1_managed_ipmi_user }, + citation: mtjade1_route_fixture_citation, + ) +} + +fn cited_mtjade1_published_route() -> BmcRotationRouteStanding + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + ] +{ + rotation_route_from_citation( + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + request: IpmiSetUserPassword { user: mtjade1_published_ipmi_user }, + citation: mtjade1_route_fixture_citation, + ) +} + +fn mtjade1_bmc_goal() -> BmcSecureGoal { + BmcSecureGoal { + managed: ManagedCredentialReference { + account: "gunbc", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-gunbc", version: "1", hash_state: HashPending }, + credential_epoch: 1, + }, + published_break_glass: ManagedCredentialReference { + account: "admin", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-admin", version: "4", hash_state: HashPending }, + credential_epoch: 4, + }, + policy: machine_qualification_policy(admits: TestRisk), + } +} + +fn mtjade1_bmc_goal_with_break_glass_epoch(epoch: Int, version: String) -> BmcSecureGoal { + BmcSecureGoal { + managed: mtjade1_bmc_goal().managed, + published_break_glass: ManagedCredentialReference { + account: "admin", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-admin", version: version, hash_state: HashPending }, + credential_epoch: epoch, + }, + policy: machine_qualification_policy(admits: TestRisk), + } +} + +fn mtjade1_grant_without_bmc_secure_effect() -> StandingOperatorGrant { + let g = mtjade1_live_standing_grant + StandingOperatorGrant { + identity: g.identity, + principal: g.principal, + ruled_at: g.ruled_at, + ruling: g.ruling, + scope: g.scope, + effects: [], + } +} + +fn mtjade1_bmc_census(published_lan_privilege_closed: Bool) -> IpmiControllerChannelCensus { + let lan_privilege = if published_lan_privilege_closed { IpmiPrivilegeNoAccess } else { IpmiPrivilegeAdministrator } + ipmi_controller_channel_census( + members: [ + ipmi_lan_channel_member(channel: 1, medium: IpmiMedium8023Lan, address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 246)), + ipmi_non_lan_channel_member(channel: 2, medium: IpmiMediumSerialAsync), + ipmi_lan_channel_member(channel: 8, medium: IpmiMedium8023Lan, address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 247)), + ], + user_access: [ + ipmi_user_channel_access(channel: 1, user: mtjade1_published_ipmi_user, privilege: lan_privilege), + ipmi_user_channel_access(channel: 2, user: mtjade1_published_ipmi_user, privilege: IpmiPrivilegeNoAccess), + ipmi_user_channel_access(channel: 8, user: mtjade1_published_ipmi_user, privilege: lan_privilege), + ], + ) +} + +fn mtjade1_account_world(users: List, published_lan_privilege_closed: Bool) -> BmcWorld { + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: published_lan_privilege_closed) + bmc_with_ipmi_user_access( + world: bmc_with_ipmi_users(world: bmc_world(power: BmcPowerOn), users: users), + rows: census_value.user_access, + ) +} + +fn mtjade1_version_identity(secret: String, version: String) -> SmResolvedVersionIdentity { + join(["projects/gunbai-secrets/secrets/", secret, "/versions/", version], "") as SmResolvedVersionIdentity +} + +fn mtjade1_ready(secret: String, version: String, bytes: String) -> SecretCredentialFetch { + SecretCredentialReady { credential: bytes as Secret, resolved_version: mtjade1_version_identity(secret: secret, version: version) } +} + +fn mtjade1_fetched_generation( + current: ManagedCredentialReference, + secret: String, + version: String, + bytes: String, +) -> ManagedCredentialGenerationFetched? + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + ] +{ + let store_at = dry_bmc_account_instant(millis: 1791072010000) + let fetch_at = dry_bmc_account_instant(millis: 1791072020000) + match admit_stored_generation(current: current, added: mtjade1_version_identity(secret: secret, version: version), stored_at: store_at) { + GenerationStoreRefused { cause: _ } => none + GenerationStored { stored: st } => + match admit_fetched_generation(stored: st, fetch: mtjade1_ready(secret: secret, version: version, bytes: bytes), fetched_at: fetch_at) { + GenerationFetchRefused { cause: _ } => none + GenerationFetched { fetched: f } => Present { value: f } + } + } +} + +fn mtjade1_rotation_approval(s: BmcRotationRouteStanding, user: IpmiUserId) -> Redemption { + RedemptionAdmitted { + claims: ApprovalCapabilityClaims { + protocol: approval_capability_protocol, + issuer: "gunbc-approval-broker" as NonEmptyStr, + audience: "srv1" as NonEmptyStr, + authority: rotation_apply_authority, + escalation_id: "o1c3b-apply-witness" as NonEmptyStr, + request_revision: rotation_route_request_identity(standing: s, request: IpmiSetUserPassword { user: user }), + decision: ProposeApprove, + attempt: "o1c1-witness-run-a" as AttemptIdentity, + issued_at: "2026-10-04T00:00:00Z", + expires_at: "2026-10-04T00:15:00Z", + key_id: "broker-2026-10" as MacKeyId, + }, + decided_by: "operator" as NonEmptyStr, + } +} + +fn mtjade1_dry_applied_bmc(subject: MachineIntakeSubject) -> BmcSecureApplyInputs? + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "bmc_secure_bound_refuses_foreign_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_falls_through_to_capability"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_refuses_a_capability_for_another_request"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_channel_state_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_foreign_bound_host_key_cannot_mint_from_this_instance_controller"), + ] +{ + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: true) + let world = mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "admin" }], + published_lan_privilege_closed: true, + ) + let reading = dry_read_bmc_account_state( + world: world, + subject: subject, + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: (subject.attempt_id as NonEmptyStr) as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match mtjade1_fetched_generation(current: mtjade1_bmc_goal().managed, secret: "bmc-lab-o1b-gunbc", version: "2", bytes: mtjade1_managed_password_v2) { + Absent => none + Present { value: mg } => + match mtjade1_fetched_generation( + current: ManagedCredentialReference { + account: "admin", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-admin", version: "3", hash_state: HashPending }, + credential_epoch: 3, + }, + secret: "bmc-lab-o1b-admin", + version: "4", + bytes: "break-glass-generation-4!", + ) { + Absent => none + Present { value: bg } => { + let managed_route = cited_mtjade1_managed_route() + let published_route = cited_mtjade1_published_route() + match plan_bmc_account_action( + subject: subject, + goal: mtjade1_bmc_goal(), + reading: reading, + managed_user: mtjade1_managed_ipmi_user, + managed_route: managed_route, + managed_approval: mtjade1_rotation_approval(s: managed_route, user: mtjade1_managed_ipmi_user), + managed_generation: mg, + published_route: published_route, + published_approval: mtjade1_rotation_approval(s: published_route, user: mtjade1_published_ipmi_user), + published_generation: bg, + channel_close: none, + planned_at: dry_bmc_account_instant(millis: mtjade1_bmc_plan_at), + ) { + BmcAccountPlanRefused { cause: _ } => none + BmcAccountPlanned { plan: p } => { + let step = dry_apply_bmc_account_plan( + world: world, + plan: p, + managed_fetch: mtjade1_ready(secret: "bmc-lab-o1b-gunbc", version: "2", bytes: mtjade1_managed_password_v2), + published_fetch: mtjade1_ready(secret: "bmc-lab-o1b-admin", version: "4", bytes: "break-glass-generation-4!"), + applied_at_millis: mtjade1_bmc_apply_at, + ) + let post_read = dry_read_bmc_account_state( + world: step.world, + subject: subject, + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: p.goal.managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: mtjade1_managed_password_v2, + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: p.goal.published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: (subject.attempt_id as NonEmptyStr) as AttemptIdentity, + read_at_millis: mtjade1_bmc_readback_at, + ) + Present { value: BmcSecureApplyInputs { application: step.application, post_read: post_read } } + } + } + } + } + } +} + +fn mtjade1_bmc_inputs(reading: BmcAccountStateObservation, grant: StandingOperatorGrant?, apply: BmcSecureApplyInputs?, capability: Redemption?) -> BmcSecureInputs { + BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: grant, + capability: capability, + apply: apply, + } +} + +fn bmc_secure_applied_established(s: StepInstanceStanding) -> Bool { + match s { + InstanceConverged { key: k, receipt: r } => + declaration_ref_eq(a: k.step_identity, b: bmc_secure_step_ref) + && match r { + BmcSecureReceipt { receipt: b } => + match b.phase.decision { + BmcSecurePhaseApplied { plan: _, application: _, post_read: _ } => true + BmcSecurePhaseNoop { observation: _ } => false + } + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + PriorLifeBoundaryReceipt { receipt: _ } => false + } + _ => false + } +} + +fn bmc_secure_noop_established(s: StepInstanceStanding) -> Bool { + match s { + InstanceConverged { key: k, receipt: r } => + declaration_ref_eq(a: k.step_identity, b: bmc_secure_step_ref) + && match r { + BmcSecureReceipt { receipt: b } => + match b.phase.decision { + BmcSecurePhaseNoop { observation: _ } => true + BmcSecurePhaseApplied { plan: _, application: _, post_read: _ } => false + } + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + PriorLifeBoundaryReceipt { receipt: _ } => false + } + _ => false + } +} + +test fn w_mtjade1_converges_through_bmc_secure_noop_on_the_real_prefix() -> Bool { + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: true) + let reading = dry_read_bmc_account_state( + world: mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "break-glass-generation-4!" }], + published_lan_privilege_closed: true, + ), + subject: mtjade1_intake_subject(), + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: "o1c1-witness-run-a" as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match converge_mtjade1_arrival_through_bmc_secure(run: run_a, prior_life: prior_life_minimal_dry_world(), bmc: mtjade1_bmc_inputs(reading: reading, grant: none, apply: none, capability: none)) { + ArrivalRunFolded { verdict: v } => + match v { + RunConverged { run: r } => + length(xs: r.ledger.instances) == 4 + && match r.ledger.instances.first() { Present { value: s } => access_established_as_read(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: identity_bind_provisional_step_ref)) |> first() { Present { value: s } => identity_bound_from_committed_captures(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: prior_life_boundary_step_ref)) |> first() { Present { value: s } => prior_life_archived_from_the_bound_subject(s: s) Absent => false } + && match r.ledger.instances.last() { Present { value: s } => bmc_secure_noop_established(s: s) Absent => false } + _ => false + } + _ => false + } +} + +test fn w_mtjade1_bmc_secure_apply_inputs_missing_refuses_on_the_real_path() -> Bool { + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: true) + let reading = dry_read_bmc_account_state( + world: mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "admin" }], + published_lan_privilege_closed: true, + ), + subject: mtjade1_intake_subject(), + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: "o1c1-witness-run-a" as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match converge_mtjade1_arrival_through_bmc_secure(run: run_a, prior_life: prior_life_minimal_dry_world(), bmc: mtjade1_bmc_inputs(reading: reading, grant: none, apply: none, capability: none)) { + ArrivalRunFolded { verdict: v } => + match v { + RunStopped { ledger: l, at: at } => + declaration_ref_eq(a: at.step_identity, b: bmc_secure_step_ref) + && match l.instances.last() { + Present { value: s } => match s { + InstanceRefused { key: _, cause: c } => match c { + DomainRefused { cause: d } => match d { BmcSecureApplyInputsMissing => true _ => false } + AuthorizationUndischarged => false + _ => false + } + _ => false + } + Absent => false + } + _ => false + } + _ => false + } +} + // AN ARCHIVE WRITE THE STORE LOSES LEAVES THE RUN INCOMPLETE, NOT STOPPED AND NOT CONVERGED, at the // PriorLifeBoundary instance, which records the write as written-but-not-read-back. Same real route, // the store the only difference. @@ -315,8 +764,8 @@ test fn w_the_roster_is_the_three_phase_prefix_of_the_authority() -> Bool { // A phase of the prefix with no step refuses rather than being skipped: through BmcSecure the prefix // reaches BmcSecure itself, which has no step in this cut (O1c-3 brings it with its gate). test fn w_a_prefix_phase_with_no_step_refuses() -> Bool { - match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { - ArrivalPrefixPhaseUnstepped { phase: p } => p == Arrival { phase: BmcSecure } + match arrival_prefix_steps(phases: arrival_prefix_through(last: BootDeliveryEstablish)) { + ArrivalPrefixPhaseUnstepped { phase: p } => p == Arrival { phase: BootDeliveryEstablish } ArrivalPrefixStepped { steps: _ } => false } } @@ -331,11 +780,11 @@ fn real_steps() -> List> { } fn access_step_bound_to(phase: IntakePhase) -> ConvergenceStep { - ConvergenceStep { identity: access_discover_step_ref, order_member: phase, preconditions: [] } + ungated_readonly_step(identity: access_discover_step_ref, order_member: phase, preconditions: []) } fn identity_step_with(preconditions: List) -> ConvergenceStep { - ConvergenceStep { identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: preconditions } + ungated_readonly_step(identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: preconditions) } fn plan_refusal(admission: ConvergencePlanAdmission) -> ConvergencePlanRefusal? { @@ -381,7 +830,7 @@ test fn w_an_unknown_precondition_refuses() -> Bool { // converge_arrival_prefix is a real declaration with no census row: as a step it refuses. test fn w_a_step_with_no_census_row_refuses() -> Bool { let uncensused = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_prefix") - match plan_refusal(admission: admit_convergence_plan(planning: arrival_planning_authority(), steps: [ConvergenceStep { identity: uncensused, order_member: Arrival { phase: AccessDiscover }, preconditions: [] }])) { + match plan_refusal(admission: admit_convergence_plan(planning: arrival_planning_authority(), steps: [ungated_readonly_step(identity: uncensused, order_member: Arrival { phase: AccessDiscover }, preconditions: [])])) { Present { value: c } => match c { StepMissingFromCensus { step: s } => declaration_ref_eq(a: s, b: uncensused) _ => false } Absent => false } @@ -409,14 +858,14 @@ fn real_access(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentMana fn established_access(o: StepOutcome) -> AccessDiscoverEstablished? { match step_outcome_receipt(outcome: o) { - Present { value: r } => match r { AccessDiscoverReceipt { receipt: a } => Present { value: a } IdentityBindReceipt { receipt: _ } => none PriorLifeBoundaryReceipt { receipt: _ } => none } + Present { value: r } => match r { AccessDiscoverReceipt { receipt: a } => Present { value: a } IdentityBindReceipt { receipt: _ } => none PriorLifeBoundaryReceipt { receipt: _ } => none BmcSecureReceipt { receipt: _ } => none } Absent => none } } fn fold_real(run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ConvergenceRunVerdict? { match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { - ConvergencePlanAdmitted { plan: p } => Present { value: fold_convergence_run(plan: p, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection()) } + ConvergencePlanAdmitted { plan: p } => Present { value: fold_convergence_run(plan: p, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection(), discharges: []) } ConvergencePlanRefused { cause: _ } => none } } @@ -471,6 +920,583 @@ fn probe_consumed(r: ProbeReceipt) -> List { r.consumed } +fn probe_auth_never(r: ProbeReceipt) -> Bool { + false +} + +fn probe_auth_on_bmc_secure(r: ProbeReceipt) -> Bool { + declaration_ref_eq(a: r.key.step_identity, b: bmc_secure_step_ref) +} + +fn four_steps() -> List> { + match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { + ArrivalPrefixStepped { steps: ss } => ss + ArrivalPrefixPhaseUnstepped { phase: _ } => [] + } +} + +test fn w_the_four_step_plan_through_bmc_secure_is_admitted() -> Bool { + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: _ } => length(xs: four_steps()) == 4 + ConvergencePlanRefused { cause: _ } => false + } +} + +test fn w_bmc_secure_noop_needs_no_discharge() -> Bool { + let access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: access, consumed: [] } }, + StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [access] } }, + StepEstablished { receipt: ProbeReceipt { key: prior, consumed: [identity] } }, + StepEstablished { receipt: ProbeReceipt { key: bmc, consumed: [prior] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) { + RunConverged { run: r } => length(xs: r.ledger.instances) == 4 + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + +test fn w_bmc_secure_apply_without_discharge_refuses() -> Bool { + let access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: access, consumed: [] } }, + StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [access] } }, + StepEstablished { receipt: ProbeReceipt { key: prior, consumed: [identity] } }, + StepEstablished { receipt: ProbeReceipt { key: bmc, consumed: [prior] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_on_bmc_secure), discharges: []) { + RunStopped { ledger: l, at: at } => + step_instance_key_eq(a: at, b: bmc) + && match l.instances.last() { + Present { value: s } => match s { + InstanceRefused { key: _, cause: c } => match c { AuthorizationUndischarged => true _ => false } + _ => false + } + Absent => false + } + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + +fn mtjade1_grant_with_interlock_pending() -> StandingOperatorGrant { + let g = mtjade1_live_standing_grant + StandingOperatorGrant { + identity: g.identity, + principal: g.principal, + ruled_at: g.ruled_at, + ruling: StandingDestructiveAuthorization { + ruling_text: g.ruling.ruling_text, + effect_subject: g.ruling.effect_subject, + interlock: InterlockPending { obligation: "hold not named" as NonEmptyStr }, + }, + scope: g.scope, + effects: g.effects, + } +} + +fn mtjade1_grant_with_foreign_interlock() -> StandingOperatorGrant { + let g = mtjade1_live_standing_grant + StandingOperatorGrant { + identity: g.identity, + principal: g.principal, + ruled_at: g.ruled_at, + ruling: StandingDestructiveAuthorization { + ruling_text: g.ruling.ruling_text, + effect_subject: g.ruling.effect_subject, + interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant") }, + }, + scope: g.scope, + effects: g.effects, + } +} + +fn apply_fold_undischarged(discharges: List) -> Bool { + let access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: access, consumed: [] } }, + StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [access] } }, + StepEstablished { receipt: ProbeReceipt { key: prior, consumed: [identity] } }, + StepEstablished { receipt: ProbeReceipt { key: bmc, consumed: [prior] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_on_bmc_secure), discharges: discharges) { + RunStopped { ledger: l, at: at } => + step_instance_key_eq(a: at, b: bmc) + && match l.instances.last() { + Present { value: s } => match s { + InstanceRefused { key: _, cause: c } => match c { AuthorizationUndischarged => true _ => false } + _ => false + } + Absent => false + } + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + +test fn w_bmc_secure_apply_pending_interlock_refuses_at_discharge() -> Bool { + grant_discharges_bmc_secure_account_write(g: mtjade1_grant_with_interlock_pending(), host: operator_host_mtjade1) == false + && grant_discharges_bmc_secure_account_write(g: mtjade1_grant_with_foreign_interlock(), host: operator_host_mtjade1) == false + && grant_discharges_bmc_secure_account_write(g: mtjade1_live_standing_grant, host: operator_host_mtjade1) +} + +test fn w_mtcollins1_is_not_discharged_by_the_mtjade1_grant() -> Bool { + grant_discharges_bmc_secure_account_write(g: mtjade1_live_standing_grant, host: operator_host_mtcollins1) == false +} + +fn mtjade1_capability_standing() -> BmcRotationRouteStanding { + rotation_route_ungrounded(endpoint: mtjade1_bmc_endpoint(), firmware: mtjade1_bmc_firmware()) +} + +fn mtjade1_stale_capability_standing() -> BmcRotationRouteStanding { + rotation_route_ungrounded( + endpoint: mtjade1_bmc_endpoint(), + firmware: bmc_firmware_release_identity_of_wire(family: AmiMegaRac, wire: "0.32" as NonEmptyStr), + ) +} + +fn mtjade1_managed_write_request() -> BmcAccountWriteRequest { + IpmiSetUserPassword { user: mtjade1_managed_ipmi_user } +} + +fn mtjade1_published_write_request() -> BmcAccountWriteRequest { + IpmiSetUserPassword { user: mtjade1_published_ipmi_user } +} + +fn rotation_capability_for( + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, + attempt_text: String, + authority: NonEmptyStr, +) -> Redemption { + RedemptionAdmitted { + claims: ApprovalCapabilityClaims { + protocol: approval_capability_protocol, + issuer: "gunbc-approval-broker" as NonEmptyStr, + audience: "srv1" as NonEmptyStr, + authority: authority, + escalation_id: "o1c3b-witness" as NonEmptyStr, + request_revision: rotation_route_request_identity(standing: standing, request: request), + decision: ProposeApprove, + attempt: attempt_text as AttemptIdentity, + issued_at: "2026-10-04T00:00:00Z", + expires_at: "2026-10-04T00:15:00Z", + key_id: "broker-2026-10" as MacKeyId, + }, + decided_by: "operator" as NonEmptyStr, + } +} + +fn bmc_secure_apply_key() -> StepInstanceKey { + step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) +} + +test fn w_bmc_secure_apply_capability_for_another_authority_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_a as String, authority: route_qualification_authority), + standing: mtjade1_capability_standing(), + request: mtjade1_managed_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_capability_for_another_request_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_a as String, authority: rotation_apply_authority), + standing: mtjade1_capability_standing(), + request: mtjade1_published_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_capability_for_another_build_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_a as String, authority: rotation_apply_authority), + standing: mtjade1_stale_capability_standing(), + request: mtjade1_managed_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_capability_for_another_run_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_b as String, authority: rotation_apply_authority), + standing: mtjade1_capability_standing(), + request: mtjade1_managed_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_admitted_capability_for_the_canonical_rotation_identity_discharges() -> Bool { + let standing = mtjade1_capability_standing() + let request = mtjade1_managed_write_request() + (rotation_route_request_identity(standing: standing, request: request) as String) != "" + && capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: standing, request: request, attempt_text: run_a as String, authority: rotation_apply_authority), + standing: standing, + request: request, + key: bmc_secure_apply_key(), + ) +} + +test fn w_bmc_secure_apply_discharge_for_another_run_refuses() -> Bool { + let foreign = step_instance_key(run: run_b, step: bmc_secure_step_ref, subject: mtjade1_key) + apply_fold_undischarged(discharges: [instance_authorization(key: foreign, principal: mtjade1_live_standing_grant.principal)]) +} + +test fn w_bmc_secure_apply_discharge_for_another_unit_refuses() -> Bool { + let foreign = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: "mtcollins1" as StepSubjectKey) + apply_fold_undischarged(discharges: [instance_authorization(key: foreign, principal: mtjade1_live_standing_grant.principal)]) +} + +// PAIRING: the census first_consumer mints the Apply discharge list. Hard-coding discharges: [] +// there must redden this claim. Prefix captures are the production readers; this claim supplies +// Apply+grant and runs converge_arrival_through_bmc_secure, not a probe fold beside it. +test fn w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match converge_arrival_through_bmc_secure( + run: run_a, + subject: mtjade1_key, + read: read_mtjade1_current_manager_read(), + inputs: mtjade1_identity_bind_inputs(), + prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life_minimal_dry_world() }, + bmc: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + ), + ) { + ArrivalRunFolded { verdict: v } => + match v { + RunConverged { run: r } => + length(xs: r.ledger.instances) == 4 + && match r.ledger.instances.first() { Present { value: s } => access_established_as_read(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: identity_bind_provisional_step_ref)) |> first() { Present { value: s } => identity_bound_from_committed_captures(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: prior_life_boundary_step_ref)) |> first() { Present { value: s } => prior_life_archived_from_the_bound_subject(s: s) Absent => false } + && match r.ledger.instances.last() { Present { value: s } => bmc_secure_applied_established(s: s) Absent => false } + _ => false + } + _ => false + } + } +} + +fn bmc_secure_bound_refuses_foreign_apply(foreign_subject: MachineIntakeSubject) -> Bool + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_attempt_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_unit_is_refused"), + ] +{ + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: own } => + match mtjade1_dry_applied_bmc(subject: foreign_subject) { + Absent => false + Present { value: foreign } => { + let inputs = mtjade1_bmc_inputs( + reading: own.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: foreign }, + capability: none, + ) + match bmc_secure_bound(key: bmc_key, identity_key: identity, identity_subject: mtjade1_intake_subject(), prior_key: prior, inputs: inputs) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationForAnotherInstance { subject: _ } => true _ => false } + _ => false + } + } + } + } +} + +test fn w_bmc_secure_apply_of_another_attempt_is_refused() -> Bool { + bmc_secure_bound_refuses_foreign_apply(foreign_subject: mtjade1_intake_subject_for(attempt: "o1c1-witness-run-b" as IntakeAttemptId)) +} + +test fn w_bmc_secure_apply_of_another_unit_is_refused() -> Bool { + bmc_secure_bound_refuses_foreign_apply(foreign_subject: MachineIntakeSubject { + subject: qualification_subject_of(unit_key: "B810301000412080005AJ0C2" as UnitKey, assembly: expected_mtjade1_assembly, firmware: expected_mtjade1_firmware), + attempt_id: "o1c1-witness-run-a" as IntakeAttemptId, + }) +} + +test fn w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + let requested = mtjade1_bmc_goal_with_break_glass_epoch(epoch: 5, version: "5") + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: requested, + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } +} + +data mtjade1_controller_clock_x_millis: EpochMs = 1 +data mtjade1_controller_clock_y_millis: EpochMs = 2 + +fn mtjade1_controller_clock(millis: EpochMs, label: String) -> ControllerClockReading { + ControllerClockReading { + reported_millis: millis, + evidence: EvidenceRef { label: label as NonEmptyStr, digest: content_hash_of_value(value: label) }, + } +} + +test fn w_matching_present_controller_clocks_compare_equal() -> Bool { + let clock = mtjade1_controller_clock(millis: mtjade1_controller_clock_x_millis, label: "controller-clock-x") + controller_clock_reading_same(left: Present { value: clock }, right: Present { value: clock }) +} + +test fn w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let clock_x = mtjade1_controller_clock(millis: mtjade1_controller_clock_x_millis, label: "controller-clock-x") + let clock_y = mtjade1_controller_clock(millis: mtjade1_controller_clock_y_millis, label: "controller-clock-y") + let reading = observation_with_controller_clock(base: apply.application.plan.diverged, controller_clock: Present { value: clock_y }) + let stamped = apply_with_diverged_controller_clock(application: apply.application, controller_clock: Present { value: clock_x }) + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: BmcSecureApplyInputs { application: stamped, post_read: apply.post_read } }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } + } +} + +test fn w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let reading = observation_with_controller_clock( + base: apply.application.plan.diverged, + controller_clock: Present { value: mtjade1_controller_clock(millis: mtjade1_controller_clock_x_millis, label: "controller-clock-x") }, + ) + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } + } +} + +test fn w_bmc_secure_apply_of_another_channel_state_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + let reading = dry_read_bmc_account_state( + world: mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "admin" }], + published_lan_privilege_closed: false, + ), + subject: mtjade1_intake_subject(), + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: mtjade1_bmc_census(published_lan_privilege_closed: false), + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: "o1c1-witness-run-a" as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } +} + +test fn w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: mtjade1_bmc_inputs(reading: apply.application.plan.diverged, grant: none, apply: Present { value: apply }, capability: none), + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureAuthorizationUndischarged => true _ => false } + _ => false + } + } +} + +test fn w_bmc_secure_apply_uncovered_grant_falls_through_to_capability() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let standing = apply.application.plan.managed_write.route + let request = apply.application.plan.managed_write.request + let key = bmc_secure_apply_key() + match discharge_bmc_secure_apply( + key: key, + identity_subject: mtjade1_intake_subject(), + inputs: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_grant_without_bmc_secure_effect() }, + apply: Present { value: apply }, + capability: Present { value: rotation_capability_for(standing: standing, request: request, attempt_text: run_a as String, authority: rotation_apply_authority) }, + ), + standing: standing, + request: request, + ) { + Present { value: _ } => true + Absent => false + } + } + } +} + +test fn w_bmc_secure_apply_uncovered_grant_refuses_a_capability_for_another_request() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let standing = apply.application.plan.managed_write.route + let request = apply.application.plan.managed_write.request + let key = bmc_secure_apply_key() + match discharge_bmc_secure_apply( + key: key, + identity_subject: mtjade1_intake_subject(), + inputs: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_grant_without_bmc_secure_effect() }, + apply: Present { value: apply }, + capability: Present { value: rotation_capability_for(standing: standing, request: mtjade1_published_write_request(), attempt_text: run_a as String, authority: rotation_apply_authority) }, + ), + standing: standing, + request: request, + ) { + Absent => true + Present { value: _ } => false + } + } + } +} + +test fn w_a_foreign_bound_host_key_cannot_mint_from_this_instance_controller() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let standing = apply.application.plan.managed_write.route + let request = apply.application.plan.managed_write.request + let key = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: "mtcollins1" as StepSubjectKey) + match bound_bmc_secure_host(key: key) { + Absent => false + Present { value: host } => + host_identity_eq(a: host, b: operator_host_mtcollins1) + && match discharge_bmc_secure_apply( + key: key, + identity_subject: mtjade1_intake_subject(), + inputs: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: Present { value: rotation_capability_for(standing: standing, request: request, attempt_text: run_a as String, authority: rotation_apply_authority) }, + ), + standing: standing, + request: request, + ) { + Absent => true + Present { value: _ } => false + } + } + } + } +} + test fn w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject() -> Bool { let own_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) let foreign_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: "mtjade2" as StepSubjectKey) @@ -481,7 +1507,7 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject() -> ] match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => - stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) }) + stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) }) ConvergencePlanRefused { cause: _ } => false } } @@ -497,7 +1523,7 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run() -> Boo ] match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => - stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) }) + stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) }) ConvergencePlanRefused { cause: _ } => false } } @@ -518,7 +1544,7 @@ test fn w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplet ] match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => - match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) { + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) { RunIncomplete { ledger: l, at: at } => declaration_ref_eq(a: at.step_identity, b: identity_bind_provisional_step_ref) && match l.instances.last() { diff --git a/dag/test/claim/machine_intake/mtjade1_arrival_principal_witness_test.dag b/dag/test/claim/machine_intake/mtjade1_arrival_principal_witness_test.dag new file mode 100644 index 00000000000..bf2ddf05d3b --- /dev/null +++ b/dag/test/claim/machine_intake/mtjade1_arrival_principal_witness_test.dag @@ -0,0 +1,224 @@ +module test.claim.machine_intake.mtjade1_arrival_principal_witness + +import std.logic { Bool } +import std.types { List, NonEmptyStr, String } +import std.durable_exclusive_hold { DurableHoldOwnerRef } +import gunbc.machine_intake_arrival_subject { + arrival_converge_subject_options, admit_arrival_subject, + ArrivalSubjectInPopulation, ArrivalSubjectUnknown, ArrivalSubjectIsManagedHostExecutorConfusion, +} +import gunbc.machine_intake_arrival_interlock { + ArrivalSlotHeld, ArrivalSlotNotHeld, + admit_arrival_archive_interlock, admit_arrival_bmc_secure_interlock, + ArrivalArchiveInterlockAdmitted, ArrivalArchiveInterlockRefused, + ArrivalBmcSecureInterlockAdmitted, ArrivalBmcSecureInterlockRefused, + arrival_combine_prefix_and_release, arrival_after_acquire, arrival_archive_slot_held, + ArrivalArchiveSlotRelease, ArrivalArchiveSlotReleased, ArrivalArchiveSlotReleaseRefused, + ArrivalArchiveSlotAcquire, ArrivalArchiveSlotAcquireRefused, ArrivalArchiveSlotAcquired, ArrivalArchiveSlotHeld, +} +import std.process { ProcessExit, ExitSuccess, ExitFailure } +import std.durable_compare_and_set { cas_generation_first } +import gunbc.machine_intake_bmc_rotation_route { rotation_route_ungrounded } +import extdeps.bmc.endpoint { AmiMegaRac, BmcControllerEndpoint } +import extdeps.bmc.capability { bmc_firmware_release_identity_of_wire } +import gunbc.auth.mtjade1_arrival_pair { mtjade1_arrival_principal_member, mtjade1_arrival_secret_grants } +import gunbc.auth.mtjade1_arrival_federation { + mtjade1_arrival_archive_effect, mtjade1_arrival_firmware_qualification_effect, +} +import gunbc.auth.authorization_pattern_selection { + FederatedScopedGrant, OperatorApprovedCapability, + PatternSelected, AuthorizationPatternSelection, + InterlockPending, InterlockedBy, + select_authorization_pattern, +} +import gunbc.auth.privileged_effect_census { + rulings_without_a_rostered_interlock, privileged_effect_census, + RealizedUnauthorized, RealizedFederatedGrant, RealizedRunSelected, + RealizedApprovalCapability, RealizedHumanStep, RealizedOperatorSession, +} +import gunbc.machine_intake_arrival_converge { grant_discharges_bmc_secure_account_write } +import gunbc.machine_intake_arrival_run { arrival_wet_prefix_from_unobserved_world } +import gunbc.auth.standing_operator_grant { + mtjade1_live_standing_grant, standing_grant_covers, standing_grant_arm_interlock, StandingGrantHost, + StandingJadeArrivalArchive, StandingJadeFirmwareQualification, StandingBmcSecureAccountWrite, StandingD0ReleaseToFleet, +} +import std.decl_ref { declaration_ref_display_key } +import gunbc.fleet_host_identity { operator_host_mtjade1, operator_host_mtcollins1 } + +fn selected_federated(s: AuthorizationPatternSelection) -> Bool { + match s { + PatternSelected { pattern: FederatedScopedGrant, receipt: _ } => true + _ => false + } +} + +fn selected_approved(s: AuthorizationPatternSelection) -> Bool { + match s { + PatternSelected { pattern: OperatorApprovedCapability, receipt: _ } => true + _ => false + } +} + +test fn w_arrival_options_are_the_population_projection() -> Bool { + arrival_converge_subject_options() == ["mtjade1"] +} + +test fn w_mtjade1_is_admitted_and_mtcollins1_and_outsiders_refuse_before_effect() -> Bool { + match admit_arrival_subject(wire: "mtjade1") { + ArrivalSubjectInPopulation { subject: s } => (s.wire as String) == "mtjade1" + _ => false + } + && match admit_arrival_subject(wire: operator_host_mtcollins1 as String) { + ArrivalSubjectIsManagedHostExecutorConfusion { wire: _ } => true + _ => false + } + && match admit_arrival_subject(wire: "not-a-unit") { + ArrivalSubjectUnknown { wire: w } => w == "not-a-unit" + _ => false + } +} + +test fn w_grant_covers_arrival_arms_on_mtjade1_only() -> Bool { + standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingJadeArrivalArchive) + && standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingJadeFirmwareQualification) + && standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingBmcSecureAccountWrite) + && grant_discharges_bmc_secure_account_write(g: mtjade1_live_standing_grant, host: operator_host_mtjade1) + && !grant_discharges_bmc_secure_account_write(g: mtjade1_live_standing_grant, host: operator_host_mtcollins1) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtcollins1 }, effect: StandingBmcSecureAccountWrite) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingD0ReleaseToFleet) +} + +test fn w_ungrounded_route_refuses_bmc_secure_interlock() -> Bool { + match admit_arrival_subject(wire: "mtjade1") { + ArrivalSubjectInPopulation { subject: s } => + match admit_arrival_archive_interlock(subject: s, slot: ArrivalSlotNotHeld { cause: "slot free" as NonEmptyStr }) { + ArrivalArchiveInterlockRefused { cause: _ } => + match admit_arrival_bmc_secure_interlock( + subject: s, + slot: ArrivalSlotHeld { subject: s }, + route: rotation_route_ungrounded( + endpoint: BmcControllerEndpoint { host: "192.168.1.246" }, + firmware: bmc_firmware_release_identity_of_wire(family: AmiMegaRac, wire: "2.11.104000" as NonEmptyStr), + ), + ) { + ArrivalBmcSecureInterlockRefused { cause: _ } => true + ArrivalBmcSecureInterlockAdmitted { subject: _ } => false + } + ArrivalArchiveInterlockAdmitted { subject: _ } => false + } + _ => false + } +} + +test fn w_release_failure_after_success_is_visible() -> Bool { + match arrival_combine_prefix_and_release( + prefix: ExitSuccess, + slot: ArrivalArchiveSlotReleaseRefused { cause: "arrival slot release was not eligible" as NonEmptyStr }, + ) { + ExitSuccess => false + ExitFailure { code: _, reason: r } => string_contains(s: r, pattern: "slot release refused") + } +} + +test fn w_release_failure_after_prefix_failure_is_concatenated() -> Bool { + match arrival_combine_prefix_and_release( + prefix: ExitFailure { code: 2, reason: "prefix refused" }, + slot: ArrivalArchiveSlotReleaseRefused { cause: "arrival slot release was not eligible" as NonEmptyStr }, + ) { + ExitSuccess => false + ExitFailure { code: c, reason: r } => + c == 2 && string_contains(s: r, pattern: "prefix refused") && string_contains(s: r, pattern: "slot release refused") + } +} + +fn body_that_refuses() -> ProcessExit { + ExitFailure { code: 9, reason: "BODY_RAN" } +} + +fn release_that_marks(held: ArrivalArchiveSlotHeld) -> ArrivalArchiveSlotRelease { + match held { + ArrivalArchiveSlotHeld { subject: _, slot_key: _, owner: _, generation: _ } => + ArrivalArchiveSlotReleaseRefused { cause: "RELEASE_RAN" as NonEmptyStr } + } +} + +fn fixture_acquired_slot() -> ArrivalArchiveSlotAcquire { + match admit_arrival_subject(wire: "mtjade1") { + ArrivalSubjectInPopulation { subject: s } => + ArrivalArchiveSlotAcquired { + held: arrival_archive_slot_held( + subject: s, + slot_key: "arrival:mtjade1" as NonEmptyStr, + owner: "arrival-principal-witness" as DurableHoldOwnerRef, + generation: cas_generation_first(), + ), + } + _ => ArrivalArchiveSlotAcquireRefused { cause: "fixture subject was not admitted" as NonEmptyStr } + } +} + +test fn w_acquired_runs_body_and_release_when_body_refuses() -> Bool { + match arrival_after_acquire( + outcome: fixture_acquired_slot(), + body: fn() { body_that_refuses() }, + release_fn: fn(h) { release_that_marks(held: h) }, + ) { + ExitSuccess => false + ExitFailure { code: c, reason: r } => + c == 9 && string_contains(s: r, pattern: "BODY_RAN") && string_contains(s: r, pattern: "RELEASE_RAN") + } +} + +test fn w_successful_release_keeps_the_prefix() -> Bool { + match arrival_combine_prefix_and_release( + prefix: ExitSuccess, + slot: ArrivalArchiveSlotReleased { generation: cas_generation_first() }, + ) { + ExitSuccess => true + ExitFailure { code: _, reason: _ } => false + } +} + +test fn w_bound_principal_selects_federated_scoped_grant() -> Bool { + selected_federated(s: select_authorization_pattern(e: mtjade1_arrival_archive_effect())) + && selected_approved(s: select_authorization_pattern(e: mtjade1_arrival_firmware_qualification_effect())) + && !selected_federated(s: select_authorization_pattern(e: mtjade1_arrival_firmware_qualification_effect())) + && !selected_approved(s: select_authorization_pattern(e: mtjade1_arrival_archive_effect())) + && mtjade1_arrival_principal_member() == "serviceAccount:mtjade1-arrival@gunbai-secrets.iam.gserviceaccount.com" + && mtjade1_arrival_secret_grants().length() == 1 + && rulings_without_a_rostered_interlock().length() == 1 + && match rulings_without_a_rostered_interlock().first() { + Present { value: s } => + declaration_ref_display_key(ref: s) == "gunbc.auth.mtjade1_arrival_federation::mtjade1_arrival_firmware_qualification_effect" + Absent => false + } + && match standing_grant_arm_interlock(g: mtjade1_live_standing_grant, e: StandingJadeFirmwareQualification) { + InterlockPending { obligation: _ } => true + InterlockedBy { hold: _ } => false + } + && match standing_grant_arm_interlock(g: mtjade1_live_standing_grant, e: StandingBmcSecureAccountWrite) { + InterlockedBy { hold: h } => (h.decl_name as String) == "admit_rotation_apply" + InterlockPending { obligation: _ } => false + } +} + +test fn w_wet_door_refuses_unobserved_prior_life_world() -> Bool { + match arrival_wet_prefix_from_unobserved_world() { + ExitSuccess => false + ExitFailure { code: _, reason: r } => + string_contains(s: r, pattern: "unobserved PriorLifeBoundary") + } +} + +test fn w_archive_census_does_not_claim_a_write_the_wet_door_refuses() -> Bool { + any(privileged_effect_census, row => + (row.site.decl_name as String) == "mtjade1_arrival_archive_effect" + && match row.realized { + RealizedUnauthorized => true + RealizedFederatedGrant => false + RealizedRunSelected => false + RealizedApprovalCapability => false + RealizedHumanStep => false + RealizedOperatorSession { arm: _ } => false + }) +} diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 49916065be5..0bbebd9517c 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -40,6 +40,10 @@ new-witness eval-step cost gate over the one real-path claim of each approval-re two serving processes on one host can both open the single-writer approval store, and which of them may write is decided by a declaration they agree to consult rather than by a permission either one cannot bypass: RUNG DROP, structurally impossible -> mechanically preventable (replacement staged: gunbc.auth.approval_writer_authority approval_write_admission, consulted by both mutating routes before any store effect; the terminal replacement is a POSIX-principal restriction on the store generations). Population: gunbc-roadmap.service and gunbc-approval-broker.service on srv1, for the window in which both run under the service principal with gunbc.auth.approval_decision_store approval_decision_store_root readable and both keyrings loadable, any gunbc serve process started by hand from a checkout whose revision predates gunbc.auth.approval_writer_authority, which reads no such declaration at all. Restored when: THE CAPABILITY: the approval store's generations are writable by exactly ONE POSIX principal, and the other serving process's account cannot open them -- so a second writer is refused by the kernel rather than by agreement. SUFFICIENT FOR: attempting a store write as the non-writer principal and observing the OS refusal, with the broker principal alone holding the submission MAC key, the capability MAC key, the publisher token and the store, and the roadmap principal unable to read any of them. Nothing smaller retires this row. IN PARTICULAR, A PERMISSION-BITS READBACK DOES NOT: a receipt reporting owner, group, exact mode and forbidden bits establishes that only the declared principals HOLD permission, which is a statement about metadata and not about access. This trigger asks whether the non-writer CAN OPEN THE STORE, and only an attempt answers that: the execution-as-another-principal leg IS the evidence, and a metadata receipt is not a weaker form of it but a different observation. It is named here because it is the artifact that will exist and will therefore be reached for (raised by merry-bear-816 through zesty-crane-846, 2026-09-19, against the generalized custody work that produces exactly such a receipt). Nor does moving writer authority to the broker retire it -- that changes which process refuses, not whether the guarantee is by agreement; nor does deleting the roadmap's approval routes, because the roadmap process would still hold a principal that can open the store; nor does a claim over approval_write_admission, which establishes that the fold refuses and not that a process which skips the fold is stopped. +### new-witness eval-step cost gate over the one Apply inhabitance of converge_arrival_through_bmc_secure: 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-10-07 + +new-witness eval-step cost gate over the one Apply inhabitance of converge_arrival_through_bmc_secure: 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: converge_arrival_through_bmc_secure executing as natively emitted code rather than in the seed interpreter, so the one Apply inhabitance fits the NewWitnessTier eval-step budget). Population: test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_bmc_secure_apply_converge_rows; measured by claim_batch --hermetic --source-root dag --source-root src/v2 --entry dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag --function w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world (BuildBuddy, GUNBC_BIND_MEMORY_CGROUP_BYTES=30064771072): PASS, eval_steps over the new-witness budget. The billed work is converge_arrival_through_bmc_secure over the production prefix captures plus dry Apply+grant, which this claim is the only Apply execution of. Restored when: THE CAPABILITY: converge_arrival_through_bmc_secure (AccessDiscover through BmcSecure Apply, including the fold's Apply-discharge mint) executing as natively emitted code in a claim frame. WHAT THAT MUST BE SUFFICIENT FOR: test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world, still calling that entry with Apply+grant and still asserting the Applied route, measures under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives. Deleting the identity, hard-coding discharges: [] in the entry, or relocating the claim off the required gate satisfies none of it. + ### Arity agreement between a declared builtin parameter name and its derived algebra template — declared 2026-09-01 Builtin signature grounding -- **RUNG DROP, DECLARED (2026-09-01).** PREVIOUS RUNG: none to lower -- this declares that a class created by this change lands below its attainable ceiling rather than at it. v1.compiler.infer_method pairs each row's DECLARED parameter names with the parameter TYPES derived from std.algebra. When the two lists disagree in length, pair_declared_names yields AlgebraTypeVariable { id: "unpaired_declared_parameter" } for the unpaired position instead of refusing. That is a value standing where a refusal belongs -- DESIGN section 5's fabricated-plausible-output arm -- and it is declared here rather than left as a marker that reads like a wall. TEMPORARY RUNG: mitigatable. The marker is distinctive, greppable, and reaches src/v1/stage0/src/v1_compiler_infer_method.rs, so a mismatch is DISCOVERABLE by inspection of a generated artifact. It is not mechanically preventable, because NO CONSUMER ASSERTS ITS ABSENCE: an unchecked marker is an inert lens, and DESIGN is explicit that the tier where the machinery exists and nothing gates on it is itself a lie. REASON: builtin_function_registry is a `data` initializer and a .dag data initializer has no refusal channel -- there is nowhere at construction for a typed, located diagnostic to go, so the only arms available were a fabricated value or a silently shorter list, and a marked fabrication is the more honest of the two. POPULATION: bounded and closed at 20 rows -- exactly the registry names that std.algebra also declares and that therefore pair at all (count, to_int, substring, to_string, concat, map_insert, map_merge, with, map_contains_key, map_has, lookup, map_get, map_keys, map_values, get, reverse, list_push, length, starts_with, replace). The other 112 rows author their types directly and cannot reach this arm. Zero occurrences of the marker in the tree today, which is the state this row exists to keep observable. RESTORATION TRIGGER: construction-time refusal available inside a `data` initializer -- SUFFICIENT FOR a declared/derived arity disagreement to stop the line with a typed, located diagnostic at the row that causes it, rather than to produce a marked value that construction accepts. The trigger names that capability and not any artifact that would contribute to one; a witness asserting the marker's absence would raise this to mechanically preventable but would NOT retire the row, because the invalid state would still be writable. diff --git a/src/v2/workflow/floor_eval_step_cost_drop.dag b/src/v2/workflow/floor_eval_step_cost_drop.dag index 14228f13a85..aaf054450e6 100644 --- a/src/v2/workflow/floor_eval_step_cost_drop.dag +++ b/src/v2/workflow/floor_eval_step_cost_drop.dag @@ -38,6 +38,8 @@ import std.types { NonEmptyStr, List } // of the dag target (`dag_text_round_trip_nested_bind_new_witness_eval_step_cost`). // - `floor_eval_step_cost_drop_coproduct_fragment_normalize_rows`: the three coproduct type-declaration // fragment-lowering claims (`coproduct_fragment_normalize_new_witness_eval_step_cost`). +// - `floor_eval_step_cost_drop_bmc_secure_apply_converge_rows`: the one Apply inhabitance of +// converge_arrival_through_bmc_secure (`bmc_secure_apply_converge_new_witness_eval_step_cost`). // The loss is a WORKFLOW fact -- which // identities the eval-step ceiling does not refuse -- so it lives beside the other two rosters the // ceiling consults (`v2.workflow.floor_grandfathered_roster`, `v2.workflow.floor_cost_debt`) and @@ -442,8 +444,15 @@ data floor_eval_step_cost_drop_coproduct_fragment_normalize_rows: List = [ + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world" as NonEmptyStr, + measured_by: "claim_batch --hermetic --source-root dag --source-root src/v2 --entry dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag --function w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world (BuildBuddy, GUNBC_BIND_MEMORY_CGROUP_BYTES=30064771072): PASS, eval_steps over the new-witness budget. The billed work is converge_arrival_through_bmc_secure over the production prefix captures plus dry Apply+grant, which this claim is the only Apply execution of" as NonEmptyStr, + }, +] + fn floor_eval_step_cost_drop_all_rows() -> List { - concat(concat(concat(concat(concat(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), floor_eval_step_cost_drop_build_job_membership_rows), floor_eval_step_cost_drop_dag_emit_round_trip_rows), floor_eval_step_cost_drop_approval_intent_digest_rows), floor_eval_step_cost_drop_dag_text_round_trip_rows), floor_eval_step_cost_drop_coproduct_fragment_normalize_rows) + concat(concat(concat(concat(concat(concat(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), floor_eval_step_cost_drop_build_job_membership_rows), floor_eval_step_cost_drop_dag_emit_round_trip_rows), floor_eval_step_cost_drop_approval_intent_digest_rows), floor_eval_step_cost_drop_dag_text_round_trip_rows), floor_eval_step_cost_drop_coproduct_fragment_normalize_rows), floor_eval_step_cost_drop_bmc_secure_apply_converge_rows) } // THE PROJECTION THE SEED RUNNER READS AND THE MODEL TESTS AGAINST. The runner refuses an empty or diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index dbd2cd7655a..d9b1e04ecbd 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -1447,7 +1447,7 @@ fn floor_route_gap_expectation_chunk_14() -> List { } }}} -// The ten test.claim.durable_exclusive_hold_file_store_wet_witness identities: the hold protocol +// The test.claim.durable_exclusive_hold_file_store_wet_witness identities: the hold protocol // over the real file store -- absent acquires at 1, held refuses without writing (another owner and // its own spelling), release to N+1 and reacquire at N+2, two contenders over one free observation, // store refusal distinct from contention, refused releases leave no next generation, and a commit @@ -1477,7 +1477,16 @@ fn floor_route_gap_expectation_chunk_15() -> List { head: FloorRouteGapExpectation { identity: "test.claim.durable_exclusive_hold_file_store_wet_witness.a_write_time_store_refusal_is_reported_as_unavailable_not_as_a_lost_race_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_exclusive_hold_file_store_wet_witness.a_live_release_plan_carries_the_observed_generation_and_the_free_bytes_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.durable_exclusive_hold_file_store_wet_witness.w_after_acquire_invokes_the_real_slot_release", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.durable_exclusive_hold_file_store_wet_witness.w_failed_acquire_runs_no_body", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.durable_exclusive_hold_file_store_wet_witness.w_refused_acquire_body_writes_a_marker_when_called_directly", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Empty {} + } + } + } } } } diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index 536251cec66..286f7797888 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -1959,6 +1959,24 @@ fn local_repo_wet_schedule() -> List { function: "a_live_release_plan_carries_the_observed_generation_and_the_free_bytes_by_real_execution", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.durable_exclusive_hold_file_store_wet_witness", function: "w_after_acquire_invokes_the_real_slot_release" }, + entry: "dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag", + function: "w_after_acquire_invokes_the_real_slot_release", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.durable_exclusive_hold_file_store_wet_witness", function: "w_failed_acquire_runs_no_body" }, + entry: "dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag", + function: "w_failed_acquire_runs_no_body", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.durable_exclusive_hold_file_store_wet_witness", function: "w_refused_acquire_body_writes_a_marker_when_called_directly" }, + entry: "dag/test/claim/durable_exclusive_hold_file_store_wet_witness_test.dag", + function: "w_refused_acquire_body_writes_a_marker_when_called_directly", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.fabric.fabric_control_plane_wet_witness", function: "the_right_reservation_releases_its_cell_to_free_at_the_next_generation_by_real_execution" }, entry: "dag/test/claim/fabric/fabric_control_plane_wet_witness_test.dag",