Skip to content

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

Merged
gunbai-bot[bot] merged 13 commits into
mainfrom
session/deep-lynx-731
Oct 6, 2026
Merged

gunbai-bot[bot] merged 13 commits into
mainfrom
session/deep-lynx-731

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 5, 2026 •

Copy link
Copy Markdown
Contributor

Managed-host cut O1c-2: the convergence fold's effectful half (dry)

Plan of record: docs/plans/managed-host-untangle.md, Cut O, the fold capability table, row O1c-2. The first effectful consumer of gunbc.fleet.convergence_fold is the PriorLifeBoundary archive. This PR brings an applied step with its own domain receipt, per-leg deadlines, and incomplete-versus-refused.

Brief corrected against the plan. The brief placed "apply plus independent readback" on BmcSecure in this cut. The plan gives BmcSecure, the authorization gate, the principal and the mutation lane to O1c-3. Putting BmcSecure's Apply into the fold here would have admitted an ungated credential-write arm. warm-crane-577 ruled (A): BmcSecure is untouched here, and no ungated write arm enters the fold.

What lands

  • gunbc.fleet.convergence_fold: incomplete as its own arm
    • StepOutcome<R, C, I> gains StepIncomplete { key, cause: I }. The domain's incompleteness type is a third parameter, so a cause meaning "nothing was done" cannot stand for "something was done and not read back".
    • InstanceIncomplete never satisfies a precondition.
    • RunIncomplete { ledger, at } is distinct from RunStopped.
    • ConvergedRun stays mintable only when every instance converged.
    • The arm is not named Pending: re-attach across runs belongs to the Spark arm.
  • gunbc.fleet.convergence_fold: effect legs and their deadlines
    • LegBudget is sealed, holds a PositiveMillisecond duration, and is minted only for each domain's declaring function.
    • LegDeadline and LegCompletedWithinDeadline are sealed.
    • complete_effect_leg judges a leg on the observer clock. Its result is within the deadline, elapsed, finished-before-start, or unobserved.
    • No time-typed scalar formal carries a deadline, because of File product_value_at_a_scalar_formal_is_accepted; enroll its compile-probe reds #13385.
  • gunbc.machine_intake_prior_life_boundary (new): the carriers
    • The eight carriers of machine-intake-design §5 are each captured as content-addressed bytes or recorded as a typed gap, never omitted.
    • The BaselineCursor is derived from the archive: the SEL final id, each log service's final entry, the account-event final entry, and the archive digest.
    • The archive is written to a dry store that realizes the staging ContentAddressedArtifactStore, then read back from the store by digest, independently of what the write returned.
    • Observe, assess and decide go through HostEffectDomainProjection. The write and readback are the domain's own, so C8 stays awaiting: the write is not reconciled through host_effect_apply.
    • Only LogsArchivedWithBaselineCursor has a constructor. LogsArchivedAndCleared has none.
    • The receipt names the dry realization it came from.
  • gunbc.machine_intake_prior_life_boundary: policy rows (warm-crane-577's decision, reported upward for veto)
    • Mt. Collins and Mt. Jade both require all eight carriers and admit only the uncleared baseline-cursor arm.
    • Rows are keyed by the cited upstream subject (extdeps.ampere.mt_collins_product_brief.subject, extdeps.ocp.mt_jade.subject), so neither row claims a controller family.
  • Store divergence, stated (§3b): the archive store does not use std.artifact_store ArtifactStore, because that is an LRU cache provider that evicts, and an evidence archive must never evict.
  • gunbc.bmc_model BmcWorld: record_surfaces
    • Five fields: Manager DateTime, Redfish LogService (new extdeps.bmc.redfish_telemetry RedfishLogService, citing LogService.v1_0_0), account-event LogEntrys, VirtualMedia, and Sensor.
    • All five are unmodeled by default, and the existing transitions are unchanged.
    • The values are generic, with no vendor content.
  • gunbc.machine_intake_arrival_converge:
    • The prefix now runs through PriorLifeBoundary, which has its own census row.
    • The step refuses an identity receipt from another instance.
    • The platform is selected before the step (§3d).
  • Pre-existing O1b defect, fixed as its own commit:
    • observer_clock_modeled admitted test.claim.machine_intake_bmc_secure_state_witness observer_at, which returned a sealed ObserverClockInstant. That was a lesson-1 proxy.
    • It is now confined to the witness's Bool claims, which mint into an open ScheduleInstants record.
    • Known lesson-1 proxy, not fixed here: gunbc.machine_intake_bmc_secure dry_bmc_account_instant is an unsealed fn that takes EpochMs and returns a sealed ObserverClockInstant. It is routed, not left open: Managed-host cut O1a-2: IPMI Set User Access as a second route request shape #13242 has landed, and bright-wolf-485 is sealing it in a separate PR.

No hardware was touched, no live write was made, and no workflow mode or job changed. The fleet-converge.yml generator output equals the committed file body (details below).

Side-chat review 5419442560: both blockers fixed

  1. The minter chain is confined to the checked path.
    • established, write_then_read_back, archive_of, observe_prior_life, dry_write_archive, read_back_archive, effect_leg_deadline and complete_effect_leg each admit only their checked-path callers.
    • Each has an outside-call RED in test.claim.machine_intake_prior_life_boundary_forged_probe_witness every_minter_behind_the_checked_entry_refuses_an_outside_caller.
    • archive_of now captures the world itself, so it no longer takes captures from the caller.
  2. The archive encoding is injective.
    • Captures carry their typed payloads.
    • The bytes are RFC 8259 JSON (extdeps.languages.json.emit serialize_json) over every modeled field: tagged enum arms, framed lists, and media_types/connected_via kept.
    • The cursor positions are read from those payloads and encoded into the same bytes, and the digest is of those bytes.
    • Controls:
      • w_two_log_populations_that_a_delimiter_join_conflated_archive_distinctly is the review's counterexample. The bytes and digests are distinct, B is written rather than held over A's store, and the cursors are 3 and 2.
      • w_virtual_media_connected_via_and_media_types_are_archived
    • Mutants:
      • M11, dropping connected_via: FAIL.
      • M12, a delimiter-joined log encoding with the cursor member removed: FAIL.
      • M13, a cursor that ignores the SEL payload: FAIL on the real-route claim.
  3. Floor cost.
    • The encoder is linear: 31,280 / 44,841 / 88,221 eval steps at 1 / 20 / 80 SEL records.
    • So the two arrival route claims now archive the smallest world that still captures all eight carriers with one real SEL record, and they assert that record's cursor position.
    • Local marginal eval steps are 63,594 and 62,995, against a budget of 72,300.

The 13 KVM Hermetic route gaps, reconciled by identity

These are no-verdict route gaps, not semantic reds. Each measured (claim, operation) pair joins exactly one row of v2.workflow.floor_route_gap floor_route_gap_expectation_chunk_29 (ground NoMockResponse), 13 of 13 both ways. No rung drop, failure-mode row or expected-red enrolment is added.

test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness. … operation in chunk_29
a_busy_viewer_slot_refuses_the_observer_and_the_handoff Dir ✓
a_connection_lost_mid_boot_is_reported_and_no_still_is_claimed_after_it Dir ✓
a_held_observer_is_admitted_and_its_triggered_still_is_hash_bound Dir ✓
a_launch_that_cannot_publish_its_pid_stops_its_child Dir ✓
an_owned_process_is_released_and_observed_gone Dir ✓
an_unreadable_canvas_is_acquisition_failed_with_the_browsers_words Dir ✓
an_unreadable_process_state_never_skips_the_kill_of_an_unpublished_child Dir ✓
a_record_naming_another_process_is_foreign_and_not_released Dir ✓
a_relative_observer_directory_is_resolved_once DirWithTemplate ✓
a_root_page_that_navigates_cannot_destroy_the_login Dir ✓
a_term_ignoring_child_with_an_unpublished_record_is_observed_stopped Dir ✓
a_transport_that_exits_at_once_is_not_serving Dir ✓
a_viewer_without_its_feature_list_never_opens_kvm Dir ✓

Hermetic results (claim_batch --hermetic, --functions regenerated from each file)

Run locally with the release claim_batch built from this branch's base compiler sources. The merge of main since then touched no src/v1 or Cargo.lock. One process ran all 22 entry groups, 322 witnesses:

witness file result
machine_intake_prior_life_boundary_witness (new) 7/7 PASS
machine_intake_prior_life_boundary_forged_probe_witness (new) 4/4 PASS
machine_intake_arrival_converge_witness 23/23 PASS
machine_intake_bmc_secure_state_witness 15/15 PASS (after b8497f0b85)
every other file in the roster (bmc_model_web_kvm, boot_world_models, fleet_health_observe, mtcollins_firmware_converge, host_convergence_census, host_convergence_protocol, arrival_converge_forged_probe, bmc_rotation_route ±forged, bmc_secure_state_forged_probe, bmc_secure, mtcollins1_bmc_secure_standing, mtcollins1_boot_acceptance_matrix, operation_realization, optional_cast_wall, probed_at_word, redfish_telemetry) all PASS
mtcollins1_kvm_observer_protocol_wet_witness (wet) 1 PASS, 13 FAIL as hermetic route gaps ("operation declares no mock_response, not a verdict"); identical PASS/FAIL lines at base 8d39b30a73, so they are not caused by this PR

BuildBuddy run at the exact head: see the comment below.

Terminal receipt

1. Consumer witnesses, run by name. The roster is every test module that directly imports a module this PR changes (bmc_model, bmc_dry_realization, bmc_megarac_web_adapter, bmc_rotation_route, bmc_secure, mtcollins1_boot_dry_realization, clock_read, host_convergence_census, convergence_fold, arrival_converge, redfish_telemetry, prior_life_boundary). It was run with claim_batch --hermetic, with --functions regenerated from each file. Results are in the table below.

2. Same-path REDs. Each mutation was applied alone to the measured head, and only the claims named here were run:

mutation witness that goes red
M10: remove the binding (arrival_step_of_phase PriorLifeBoundary => none) w_mtjade1_converges_the_prefix_through_its_dry_prior_life_archive FAIL
M1: an admitting policy skips the required-carrier check w_only_the_sel_final_record_with_the_other_carriers_absent_is_not_established, w_one_unmodeled_carrier_is_a_typed_gap_that_refuses FAIL
M2: the fold drops RunIncomplete w_a_lost_archive_write_leaves_the_run_incomplete_at_prior_life_boundary, w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplete FAIL
M3: the readback trusts the archive instead of re-reading the store w_a_lost_corrupted_or_late_write_is_incomplete_not_refused, w_a_lost_archive_write_leaves_the_run_incomplete_at_prior_life_boundary FAIL
M4: the deadline ignores its budget w_a_budget_that_differs_only_in_its_duration_flips_completed_to_elapsed, w_a_lost_corrupted_or_late_write_is_incomplete_not_refused FAIL
M5: the platform parameter is ignored (Mt. Jade row always applies) w_a_policy_refusal_writes_nothing FAIL
M6: the identity-instance check is removed w_prior_life_boundary_refuses_an_identity_receipt_from_another_run FAIL
M7: a held archive is written again w_an_archive_already_held_is_a_noop_and_is_not_written_twice FAIL
M8: the cursor is not the archive's w_the_baseline_cursor_is_derived_from_the_archive_it_was_read_from FAIL
M9: the observer_at proxy is restored the bmc_secure_state witness refuses to resolve: constructor call admission refused: 'gunbc.clock_read.observer_clock_modeled' refuses call from '…observer_at'

The seals' outside-call and literal REDs are enrolled in test.claim.machine_intake_prior_life_boundary_forged_probe_witness, covering:

  • LegBudget, leg_budget, LegDeadline, LegCompletedWithinDeadline
  • BaselineCursor, PriorLifeArchive, PriorLifeArchivePlan, ArchiveWriteReceipt, ArchiveReadBack, PriorLifeBoundaryEstablished
  • dry_archive_prior_life, dry_prior_life_instant

It also has a class-scoped clean control. All 4 pass.

3. Corpus sweep. git grep at head across .dag, .rs, .yml, docs/ and artifacts/ for the deleted and renamed symbols returns 0 hits for each: observer_at, w_mtjade1_converges_both_read_only_phases_from_its_committed_captures, w_the_roster_is_the_two_phase_prefix_of_the_authority, w_the_real_two_step_plan_is_admitted. No module was deleted.

4. No aliases. Nothing re-exports, wraps or renames through a removed root.

Lesson 3 (trial merge): main was merged at bc6efca7f7. None of the .dag files main changed since base constructs BmcWorld, names StepOutcome</ConvergenceRunVerdict<, or calls converge_arrival_prefix/converge_mtjade1_arrival_prefix.

fleet-converge.yml: gunbc.fleet_converge_workflow expected_fleet_converge_yml at head was diffed against the committed file. The body is identical. The only differences are the two # Generated by header lines that the artifact layer prepends.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 6 commits October 5, 2026 14:02
…ms (pre-existing O1b proxy)

test.claim.machine_intake_bmc_secure_state_witness observer_at was admitted to
gunbc.clock_read observer_clock_modeled and returned a sealed ObserverClockInstant,
so any function of that module could mint a modeled instant through it: a
sanctioned-constructor proxy. The helpers now take instants, each Bool claim
mints its own into an open ScheduleInstants record, and only those claims are
admitted.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…es, incomplete vs refused (dry)

The convergence fold's first effectful consumer. gunbc.fleet.convergence_fold
gains StepIncomplete / InstanceIncomplete / RunIncomplete, distinct from refused
and stopped and never converged, with the domain's incompleteness type as a
third parameter; and sealed effect-leg carriers: LegBudget (a positive duration,
minted only for the domain's declaring function), LegDeadline and
LegCompletedWithinDeadline, judged on the observer clock.

gunbc.machine_intake_prior_life_boundary archives the eight prior-life carriers
of machine-intake-design §5 as content-addressed evidence, derives the baseline
cursor from that archive, writes it to the (dry) staging store and reads it
back by digest. Observe/assess/decide go through HostEffectDomainProjection;
the write and readback are the domain's (C8 stays awaiting). Only
LogsArchivedWithBaselineCursor has a constructor. Mt. Collins and Mt. Jade
policy rows require all eight carriers and admit only the uncleared arm.

gunbc.bmc_model BmcWorld gains record_surfaces (Manager DateTime, Redfish
LogService, account-event log entries, VirtualMedia, Sensor), all unmodeled by
default; extdeps.bmc.redfish_telemetry gains RedfishLogService. The arrival
prefix now runs through PriorLifeBoundary with its census row.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… (real-path control)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…caught

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… plus a Bool (review 76614)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Review 76614 (stopped_incomplete as an undeclared sum): fixed in 3d7b1f3. LedgerWalk now carries one LineState = LineOpen | LineStoppedAt { at } | LineIncompleteAt { at }, set by line_after(standing). fold_convergence_run matches it directly, so a stop with no key, or a key with no kind, has no constructor, and the Bool match is gone. Re-run, hermetic: arrival_converge_witness 23/23, prior_life_boundary_witness 7/7, arrival_converge_forged_probe 7/7 PASS. The same-path RED still holds: mapping LineIncompleteAt to RunStopped turns w_a_lost_archive_write_leaves_the_run_incomplete_at_prior_life_boundary and w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplete FAIL.

— sent from deep-lynx-731

@gunbai-bot

gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Hermetic on BuildBuddy at the exact head 3d7b1f303b (invocation b133bedb-14ea-41a1-ac2d-244887b29f80).

  • One dispatch: a tree-hash check passed, claim_batch was built at that head, and the cgroup was bound after the build (EstimatedMemory=28GB, GUNBC_BIND_MEMORY_CGROUP_BYTES). No budget variable was used.
  • --functions was regenerated from each file. 22 entry groups, 323 witnesses: 310 PASS, 13 FAIL.
  • All 13 FAILs are hermetic route gaps in mtcollins1_kvm_observer_protocol_wet_witness ("operation declares no mock_response — not a verdict"). They are the same 13 names that fail at base 8d39b30a73, so none is caused by this PR.
  • Every other witness file in the roster passes in full, including prior_life_boundary 7/7, its forged probe 4/4, arrival_converge 23/23, and bmc_secure_state 15/15.

— sent from deep-lynx-731

# Conflicts:
#	dag/gunbc/bmc_model.dag
#	dag/test/claim/machine_intake/machine_intake_bmc_secure_state_witness_test.dag
@gunbai-bot

gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Merged main, including #13242, at 31ef3db. There were two conflicts:

  • gunbc.bmc_model: BmcWorld now carries both main's ipmi_user_access and this PR's record_surfaces on every literal.
  • machine_intake_bmc_secure_state_witness: main rewrote it with new channel-close helpers that still used observer_at. I re-applied the O1b proxy fix over main's version: helpers take instants, the Bool claims mint them, and clock_read's admit list now names the 17 claims that mint instants.

Local hermetic re-run on the merged tree: bmc_secure_state_witness and its forged probe are 24/24. Full roster: 340 witnesses, 327 PASS, plus the same 13 route gaps that fail at base.

dry_bmc_account_instant is routed to bright-wolf-485's PR; the PR body now says so.

— sent from deep-lynx-731

@gunbai-bot

gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Review 76675, the growing admit list on observer_clock_modeled: the list is deliberate. A test-only helper that returns a sealed ObserverClockInstant is the shape this PR removes: observer_at was exactly that, a sanctioned-constructor proxy. The rule this lane runs under is that no admitted test caller returns a sealed carrier; only Bool claims may be admitted. One entry per minting claim is the cost of that rule. If the list's length becomes the problem, the fix is a sealed modeled-clock carrier minted by a sealed schedule, not a helper.

— sent from deep-lynx-731

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

REQUEST_CHANGES at exact requested head 31ef3dbe8c6270bb7fe8599a95c4fa937607e0b0, against DESIGN.md §§3, 4b, 5 and 6b and docs/plans/managed-host-untangle.md O1c-2. Two archive-boundary blockers; neither requires BmcSecure apply/cutover, a live controller write, or restoration of a CI lane.

Accepted scope and composition

Keeping BmcSecure apply/readback, authorization, principals and lanes for O1c-3 is correct. The archive is explicitly a dry realization, not evidence of a live prior-life capture. The platform rows require all eight carriers and do not infer a controller family. Unmodeled record surfaces stay distinct from modeled empty populations.

The incomplete propagation is coherent: StepIncomplete becomes InstanceIncomplete, satisfies no converged precondition, preserves LineIncompleteAt, and produces RunIncomplete rather than RunStopped or ConvergedRun. The duration budget and deadline use their own carriers; completion distinguishes elapsed, reversed and unobserved time. This is a dry elapsed-time judgment, not evidence that a future live I/O operation is cancellable. The ordinary archive path independently looks up and hashes the stored body before establishment. Those improvements are not the findings below.

[P1] The actual archive/receipt minters remain callable around the checked entry

In gunbc.machine_intake_prior_life_boundary, dry_archive_prior_life has an admit list, but established does not. It directly constructs PriorLifeBoundaryEstablished from independently supplied key, consumed identity, subject, policy, archive, application and readback. A caller holding a genuine receipt can reuse its archive/readback, supply another subject/run's keys, choose ArchiveAlreadyHeld, and obtain a new sealed receipt without executing the identity join, policy assessment or a store read. Supplying sealed members does not establish the relationships between those members.

There is also a route that does not need a previously established phase receipt. archive_of is unrestricted and takes a world and captures independently; it can return a sealed archive with empty/gapped or unrelated captures. write_then_read_back is unrestricted too: it constructs the sealed plan, writes, reads back and calls established without running classify_prior_life_policy. Calling this helper on an incomplete archive therefore bypasses the very required-carrier refusal the guarded entry tests.

The enrolled forged probe covers carrier literals and outside calls to dry_archive_prior_life, dry_prior_life_instant and leg_budget. It does not cover these actual minter/helper calls. Its greens do not establish the claimed entry confinement.

Confine the receipt/plan/archive-producing helper chain to its checked production callers, or change those functions to consume sufficient joined evidence rather than independent authorable facts. In particular, close established, write_then_read_back and the independent world/captures construction boundary in archive_of; audit intermediary carrier-returning helpers rather than sealing only the advertised entry. Add callee-specific outside-call REDs and an accepted real-entry control. A receipt for A must not be re-keyed to B, and an incomplete capture population must not become established through a helper. No carrier-returning witness facade is needed.

[P1] The stored archive is lossy, so a valid digest readback can certify the wrong baseline

The earliest faulty boundary is the capture encoding, before hashing or storage. virtual_media_line serializes only locator, inserted and image. The input RedfishVirtualMediaObservation also carries media_types and connected_via, which are discarded. This is not merely omitting an unmodeled upstream property: these fields are present in this exact tree, and redfish_virtual_media_is_detached explicitly consumes connected_via. Varying that observed state can leave the archive body and digest unchanged.

The delimiter encoding is also non-injective. log_entry_line joins id/severity/message with |, and log_service_lines joins records with newlines without escaping or lengths. These two valid two-entry populations of one service produce identical capture bytes:

A: (1, "OK", "a\n2|OK|b"), (3, "OK", "c")
B: (1, "OK", "a"), (2, "OK", "b\n3|OK|c")

Both emit:

1|OK|a
2|OK|b
3|OK|c

The service id and declared entry count are the same. Every other carrier and the subject can remain identical, so the complete archive body and its digest are identical too. But archive_of obtains the cursor separately from world.record_surfaces.log_services: A gets final entry 3 and B gets final entry 2. Thus the alleged archive-derived cursor is not a function of the stored archive. Re-observing B over A's store can take ArchiveAlreadyHeld while producing a different baseline cursor. This is a serialization collision, not a cryptographic-hash collision.

Preserve the complete modeled capture payload through an existing lossless encoding authority, with unambiguous framing. Derive the bytes and baseline cursor from that one archived payload (or derive the cursor from its verified readback), not independent world/capture inputs. Unsupported fidelity must be a typed gap, not a CarrierCaptured that silently discards it. Add controls for the two log populations above, differing connected_via/media_types with other fields held fixed, and a real write/readback positive. Hashing and re-reading a lossy summary cannot satisfy the archive contract.

The 13 KVM Hermetic route gaps: no new declared drop merely for this rerun

These are no-verdict realization gaps, not 13 semantic assertion failures and not newly demonstrated regressions. At this head v2.workflow.floor_route_gap already records this KVM witness family in floor_route_gap_expectation_chunk_29, naming Dir/DirWithTemplate and NoMockResponse; its receipt also names their local-repo-wet route and historical execution. Preserve/reconcile the measured identities with those existing records and cite that standing in this PR's terminal receipt.

Do not invent a previous working Hermetic rung and then declare it lost. DESIGN §4b(3) needs a real loss of a previously held route or guarantee; the reported identical base/head gaps establish no such loss. Do not enroll these as expected semantic reds, or add unconditional success mocks to manufacture a verdict. No duplicate RFM is required merely to repeat an already tracked gap. A genuinely uncovered error class gets an RFM filing/update under §4b; evidence that a formerly executing wet route or gate has been removed would instead require updating/declaring the corresponding bounded drop. Neither is established solely by this Hermetic result.

Evidence

Verified exact-head workflow 37345767503: floor, generated, emit-build and aggregate witnesses all succeeded. The 310/13 BuildBuddy batch belongs to 3d7b1f303b; the later PR comment reports 327 passes and the same 13 route gaps at the requested merged head, including 24/24 for the merged BmcSecure state/probe population. Those batches and ten mutation results remain author-run evidence. I inspected the source and controls; I did not execute the project's claims/mutations or touch hardware. The encoding counterexample above is derived directly from the implemented joins.

The requested SHA was unchanged and mergeable immediately before submission. The two blockers are new archive-authority/fidelity defects, independent of the acknowledged, separately routed dry_bmc_account_instant repair and of the pre-existing KVM route gaps.

…rchive bytes, digest and cursor (review 5419442560)

established, write_then_read_back, archive_of, observe_prior_life, dry_write_archive,
read_back_archive, effect_leg_deadline and complete_effect_leg are admit_callers-sealed to the
checked path, each with an outside-call RED. Captures carry their typed payloads; the archive
bytes are RFC 8259 JSON over every modeled field (tagged enum arms, framed lists), the cursor
positions are read from those payloads and encoded too, and the digest is of those bytes.
Controls: the review's two-log counterexample and connected_via / media_types variation.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbc-ci-auto-heal and others added 3 commits October 5, 2026 23:44
… position (floor cost)

The two arrival route claims went over the 72,300 new-witness budget (83,264 / 82,829 marginal
eval steps) after the archive moved to an injective JSON encoding. The encoder is linear
(about 720 steps per SEL record at 1, 20 and 80), so the route claims archive the smallest
world that still captures all eight carriers with one real SEL record, and assert the cursor's
SEL position as well as its archive digest.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

REQUEST_CHANGES at exact requested head 061696d5b28d44393261d9934758b35a6642ce5d, against DESIGN.md §§3, 4b, 5 and 6b. The previously demonstrated receipt-rekeying and unchecked-write bypasses are closed. The one-SEL real-route pairing is accepted. One archive-fidelity blocker remains: a nested record is still flattened through a non-injective renderer before JSON receives it.

[P1] virtual_media_json still loses the locator's field boundaries

In gunbc.machine_intake_prior_life_boundary::virtual_media_json, v.locator is archived only as:

json_kv(key: "resource", value: json_string(s: redfish_virtual_media_resource_path(locator: v.locator) as String))

But extdeps.bmc.redfish_virtual_media::RedfishVirtualMediaLocator contains a tagged parent and a separate media_id. The manager/system ID and media ID are NonEmptyStr, not sealed path segments. Its resource-path renderer concatenates them around /VirtualMedia/ without escaping or refusing embedded separators.

These two distinct modeled locators therefore produce the same resource string:

// A
RedfishVirtualMediaLocator {
  parent: UnderManager { manager_id: "bmc" },
  media_id: "slot/VirtualMedia/CD1",
}

// B
RedfishVirtualMediaLocator {
  parent: UnderManager { manager_id: "bmc/VirtualMedia/slot" },
  media_id: "CD1",
}

Both render:

/redfish/v1/Managers/bmc/VirtualMedia/slot/VirtualMedia/CD1

Hold the subject, times, other carriers and all other virtual-media fields constant. capture_from_world retains those distinct locator values in memory, but virtual_media_json gives them identical JSON values. Their cursor positions also agree, so the entire stored archive body and its digest agree. B observed over A's store is consequently accepted as ArchiveAlreadyHeld; the independent digest re-read cannot recover the lost parent-ID/media-ID distinction. This is identical input bytes to the hash, not a cryptographic-collision argument.

I am not asserting that a live controller has emitted these IDs. The issue is the currently admitted modeled payload: the IDs have only non-emptiness constraints, and neither capture nor policy assessment establishes a stricter segment domain. The archive's stated contract is preservation of every modeled field. JSON quoting repairs delimiter collisions inside values supplied to JSON; it cannot repair field boundaries already discarded by the upstream path renderer.

The current virtual-media discriminators keep the locator constant while varying connected_via and media_types, so they do not discriminate this remaining loss.

Bounded repair: serialize the locator structurally too: its parent arm, the raw manager/system ID in that arm, and the separate media ID. Reuse the existing JSON constructors; no new identity model or JSON serializer is needed. Alternatively, an established admission boundary could restrict the renderer's domain and prove the crossing injective, but that boundary is absent here and is unnecessary merely to preserve this record. Keep the resource path as a derived display only if a consumer actually needs it.

Add this locator A/B at the encoding boundary, preserving the unchanged-locator positive. The existing production archive/virtual-media pairing may carry the integration obligation; another large arrival-route fixture is not required. A phase-level version can follow the existing two-log control: different stored bytes/digests, and B over A's store must be written rather than held. Replacing the structural locator encoding with the old path-only projection must redden the discriminator.

Accepted repairs and scope

established and write_then_read_back now admit only the checked phase's callers. The archive constructor captures the supplied world itself rather than accepting an independently supplied captures list. The direct observation, store-write, readback and effect-leg mint restrictions are present, and the compiler probe requires blocking ConstructorCallAdmissionRefused separately at all eight named callees; an unrelated refusal or CensusNotRunnable cannot satisfy it. The public arrival step still joins the consumed identity's run and subject before entering the dry phase. I am not retaining the old unchecked receipt/write finding.

The original two-log counterexample is now a meaningful control: it asserts distinct bodies/digests, B written over A's store, and final log cursors 3 versus 2. connected_via and media_types are preserved and discriminated. Tagged choices, framed lists and payload-derived cursor positions are the right repair; the locator is the remaining nested flattening identified here.

The smaller route claim is non-vacuous

Yes: w_mtjade1_converges_the_prefix_through_its_dry_prior_life_archive still invokes converge_mtjade1_arrival_prefix, consumes the real Manager/FRU/SMBIOS-backed access and identity results, reaches the PriorLifeBoundary instance, requires ArchiveWritten, checks the consumed identity's run/subject, and checks both the archive-digest join and Present { value: "1" } from the one SEL record. It is not an empty-cursor equality. The losing-store sibling goes through the same route and requires incomplete rather than converged. The reported route-removal and cursor-ignores-payload mutations are appropriate discriminators. Richer field-fidelity populations belong to the archive's boundary witnesses; shrinking the integration input does not itself erase that obligation or require a budget increase.

KVM gaps and evidence

I checked the current floor_route_gap_expectation_chunk_29: its KVM subset matches the 13 identities and operations in the PR table, including the one DirWithTemplate case; each carries NoMockResponse. The adjacent SOL row is a separate identity. These are already tracked no-verdict gaps, not 13 semantic failures needing new expected-red admissions. No additional drop or duplicate RFM is required for encountering the same population.

Verified requested-SHA workflow 37409003854: floor, generated, emit-build, rust-unit-tests and aggregate witnesses all succeeded. The Hermetic batches, encoder-cost measurements and mutation executions remain author-run evidence; I inspected source and controls but did not run gunbc claims, compiler mutants or hardware actions. The locator counterexample is source-derived. The head remained unchanged and mergeable before submission. No live read/write, O1c-3 implementation, CI-lane restoration or larger route specimen is requested.

gunbc-ci-auto-heal and others added 2 commits October 6, 2026 05:19
…not as rendered strings (review 5424040879)

redfish_virtual_media_resource_path joins a manager/system ID and a media ID around separators the
IDs may contain, so two distinct locators archived to one path. The locator is now its parent arm
with that arm's ID plus the media ID; the image URI is its scheme plus locator. Swept every *_json
encoder: no other field is joined into a string. Control: the review's two locators that render
one path archive to distinct bytes and digests, and B over A's store is written, not held.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

APPROVE at exact requested head f073ddfb81b89b5a71f7afad2e4fc2cfe54f02a2, against DESIGN.md §§3, 4b, 5 and 6b. The remaining archive-fidelity finding in review 5424040879 is resolved. No remaining semantic blocker in this re-review.

The locator's structure reaches the stored bytes

gunbc.machine_intake_prior_life_boundary::virtual_media_json now calls locator_json rather than flattening the locator through redfish_virtual_media_resource_path. The encoded object preserves the parent arm (UnderManager or UnderSystem), that arm's raw manager/system ID, and the separate media_id. An embedded /VirtualMedia/ therefore remains inside its original JSON string; it cannot move the boundary between the two IDs. The previously demonstrated pair can no longer produce identical archive bodies through this projection.

The image URI also retains its two modeled components: uri_json records the scheme using the existing scheme-spelling authority and records the locator separately, inside an explicit Present/Absent choice. No new path-segment restriction or alternate JSON serializer has been introduced. The other payload encoders retain their record fields, tagged alternatives and framed populations; the cursor remains derived from the captured payload and encoded with it. This is a field-preservation argument at the encoding boundary, not a claim that a finite cryptographic digest is mathematically injective.

The new control exercises the archive's actual reuse decision

w_two_locators_that_render_one_resource_path_archive_distinctly holds the subject, other fields and timing constant and calls the checked dry_archive_prior_life entry for A, B over A's resulting store, and A again over its own store. It asserts that the old resource renderer conflates the locators, requires both different archive bytes and different digests, requires B to be written rather than held, and requires the unchanged A to remain ArchiveAlreadyHeld. Its helper requires established outcomes on both sides, so a refusal cannot satisfy the distinctness assertion.

That is the requested RED and positive at the product boundary, not merely a comparison of two designed JSON values. Restoring the path-only projection removes the distinction this claim asserts; the reported M14 failure is the appropriate single-mutation discriminator. The additional admitted caller is this Bool claim, not a carrier-returning helper.

Earlier accepted boundaries remain intact

The comparison with reviewed head 061696d5b28d44393261d9934758b35a6642ce5d limits this repair to the encoder changes and new witness/admission entry; the main merge also brings the separate guarantee-probe ordering change. The previously accepted receipt/write confinement, independent store readback, policy refusals, incomplete propagation and effect-leg checks are not loosened.

The one-SEL arrival pairing and its losing-store sibling are unchanged. The earlier ruling therefore stands: the integration is non-vacuous because it traverses the real arrival prefix, requires the archive write/receipt, and checks the payload-derived nonempty SEL cursor and archive join. Richer field-fidelity cases belong at the archive boundary; no larger arrival specimen or budget increase is required.

The previously reconciled 13 chunk_29 KVM outcomes remain tracked no-verdict route gaps, not newly introduced semantic reds. This correction neither supplies their missing routes nor requires a duplicate RFM or declared drop. BmcSecure apply/cutover, C8 and live archive realization remain outside this dry cut's completed scope.

Evidence

Verified requested-SHA workflow 37419410952: floor, generated, emit-build, rust-unit-tests and aggregate witnesses all completed successfully. The local Hermetic 10/10 archive result, 331-pass consumer roster with the same 13 gaps, and M14 execution remain author-run evidence; I inspected the source, exact-head comparison, control and CI results but did not execute gunbc claims, mutants or hardware actions. The branch still named the requested SHA immediately before submission. This approval does not authorize a live controller write or claim a live prior-life capture.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 6, 2026
@gunbai-bot
gunbai-bot Bot removed this pull request from the merge queue due to a manual request Oct 6, 2026
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 6, 2026
Merged via the queue into main with commit 580f66d Oct 6, 2026
5 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/deep-lynx-731 branch October 6, 2026 20:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant