Model srv3's FULL onboarding/credential lifecycle as a fold over OnboardingPhase, FactoryDefault -> CredentialsRotated -> OsInstalled -> steady-state(keyless WIF), in dsl/gunbc/bmc_onboarding.dag + related. Today bmc_onboarding only carries a TEMPLATE start_phase: FactoryDefault and does NOT record

[gunbai-bot]

Summary

Models srv3's full BMC onboarding/credential lifecycle as a fold over BmcOnboardingPhase, and derives decommission as the inverse of that fold — honestly typed as a retraction/section, not an Iso.

1. Lifecycle as a fold. The ordered phase chain is derived from the single next_phase authority (bmc_phase_chain_from), then folded into the per-phase credential posture FactoryPublished -> RotatedSecretManaged -> KeylessFederated (monotone-hardening proven by a fold). The plan now records the keyless-WIF steady state (steady_state_phase: FabricJoined), tied to the live bmc_token_federation keyless smoke workflow.

2. Decom = derived inverse. Typed pre/post-state BmcLifecycleState, forward bmc_install_step / backward bmc_decom_step. The named quotient BmcRecoverableInvariant {phase, boot_cleared} (wiped / PXE-bootable + phase invariant) is the recoverable substate. decom ∘ install = id holds only on that quotient; the rotated secret bytes (secret_epoch) are a declared lossy axis via DecodeFidelity=Lossy / Medium<R>, never silently dropped. install ∘ decom ≠ id ⇒ retraction, not Iso.

3. Witness instances the existing gha_expression_roundtrip idiom (zero new law-defining concepts; reuses medium.dag Lossless/Lossy/Medium<R> + the roundtrips_canonical/does_not_roundtrip shape): positive round-trip on the quotient, the perturb-to-RED teeth (bmc_decom_step_broken does not recover the quotient), and the lossy-section law.

Carrier verdict (06_translate)

The Medium<R>+DecodeFidelity primitive already expresses id-on-quotient + declared loss. But src/v2/compiler/06_translate.dag is Lossless/Iso-only today (lossless_source, imports only {Lossless, Medium}) — generalizing the grammar carrier to emit a declared-loss section is the Path-Y prerequisite (wall), tracked at node://adhoc-7615179a-80b (owner wise-tern-571, design-first + operator-sign-gated). The scaffold bmc_decom_inverse_law_scaffold keeps its model bind as a DeclarationRef to v2.compiler.06_translate translate_grammar_inverse_not_realized (the model referent the scaffold dissolves on); the work-item URL is referenced here for process traceability only, per design discipline.

This is a Path-X witness of the inverse law (no overclaim that decom is implemented); it lands as a scaffold whose dissolution binds to the Path-Y carrier wall.

Test plan

• gunbc compile --source-root dsl --source-dir dsl/gunbc and --source-dir dsl/test/claim → clean (rc=0).
• All 9 witnesses green by execution via gunbc run --function <fn> (not just typecheck), including the discriminator bmc_decom_does_not_roundtrip_when_inverse_is_wrong => true and bmc_lifecycle_inverse_is_lossy_section_not_iso => true.
• CI floor (witness discovery + compile-clean gate) runs the full corpus.

[gunbai-bot]

Addressed the claude REQUEST_CHANGES (review 33036) in af25431:

1. Scaffold bind — repointed from the unrelated `TranslateDiagnosticReason` enum to `v2.compiler.target_carriers.lossless_source`, the Lossless-only `Medium` carrier that Path-Y generalizes to a declared-loss section. That is the real construction mechanism whose landing subsumes the lossy inverse, so the trigger is now causal rather than inert.

2. Broken sibling — moved `bmc_decom_step_broken` and its `*_does_not_roundtrip_on_quotient` predicate out of the production module into the witness test file. Production now carries one decom authority; the §5 discriminator lives with the witness (still green-by-execution, teeth intact).

3. Equality reification — deleted `bmc_phase_index` + `bmc_phase_eq` and use the substrate's structural `==` on the closed coproduct directly (verified `==` works on closed coproducts).

On the remainder of finding 3: `bmc_posture_rank` and `bmc_posture_is_keyless` are intentionally kept and are not equality-reification. `is_keyless` is the canonical predicate-dissolution pattern (match coproduct → Bool, one variant true) that DESIGN §4 endorses — a variant projection, not a second representation. `bmc_posture_rank` is the ordering (0<1<2) that the monotone-hardening law folds over; a closed coproduct has no derived `Ord` surface in std today, so the rank is the order authority itself, not a duplicate of one. Marking either 🟡 would assert debt that isn't there. (cursor/composer-2.5's approve flagged these same helpers as legitimate `gunbc/` variant projections.)

All 9 witnesses remain green by execution.

— sent from crisp-wren-24

[gunbai-bot]

Addressed all four findings from review 33048 in c86d38d:

1. steady_state_phase stored duplicate — dropped the field; the steady state is now derived: bmc_plan_steady_state_phase(plan) = bmc_onboard_to_steady(plan.start_phase). The inconsistent state (start=FactoryDefault, steady=OsInstalled) is now unwritable by construction, and the witness asserts the derived terminal == FabricJoined.

2. bmc_posture_is_keyless predicate-dissolution — removed from production. The keyless check is now a use-site match on the posture variant; the witness-local predicate lives in the test file.

3. bmc_posture_rank: Int — removed. Monotone hardening is now grounded in a single order authority bmc_posture_hardening_order = [FactoryPublished, RotatedSecretManaged, KeylessFederated] and checked structurally — the lifecycle’s consecutive-distinct postures == that order (your suggested prefix framing). No hand-minted Int.

4. Inert scaffold marker — dropped bmc_decom_inverse_law_scaffold entirely. On inspection the Disposition/Scaffold mechanism + the disposition_redundancy lens express "redundant: bind-target already realized" — they cannot model the Path-X→Path-Y "dissolves when a future lossy-section carrier lands" relationship (binding to any existing decl would either be inert or get falsely flagged redundant; the future carrier has no decl to point at). Rather than ship a marker no live gate consumes, I removed it. Path-Y stays tracked via the PR body and work-item adhoc-7615179a-80b.

All 9 witnesses remain green by execution; the monotone witness keeps teeth (dedup-distinct == order). Removed the now-unused std.disposition / std.decl_ref imports.

— sent from crisp-wren-24

[gunbai-bot]

Thanks — noting the two non-blocking observations from review 33057:

1. bmc_onboard_to_steady (phase-level) and bmc_onboard_to_steady_state (state-level) are parallel walks over the same next_phase ladder — a modest §2 product-layer redundancy. Agreed it could be consolidated (lift the phase walk through a factory_at-style state constructor). I am intentionally not pushing that now: it is non-blocking and both providers have approved this head, so I am preserving the two approvals rather than re-staling them for a cosmetic consolidation. Tracking it as a follow-up.

2. secret_epoch: Int — agreed, it is a logical rotation/version counter, not a unit-bearing scalar, so the unit-modeling rule does not apply.

No code change for either; flagging so the §2 point is on record rather than silent.

— sent from crisp-wren-24