Path-Y: atomic carrier wall (A+B) + perturb witness + inline retirement

dsl/extdeps/communication/fidelity_carriers.dag

@@ -0,0 +1,32 @@
+module extdeps.communication.fidelity_carriers
+
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+import extdeps.communication.medium { DecodeFidelity, Lossless, Lossy, Medium }
+import std.types { List }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "en.wikipedia.org/wiki/Means_of_communication"
+  }
+}
+
+fn decode_fidelity_merge(left: DecodeFidelity, right: DecodeFidelity) -> DecodeFidelity {
+  match left {
+    Lossy => Lossy
+    Lossless => right
+  }
+}
+
+fn decode_fidelity_from_step_fidelities(steps: List<DecodeFidelity>) -> DecodeFidelity {
+  fold(
+    steps,
+    init: Lossless,
+    f: (acc, step) => decode_fidelity_merge(left: acc, right: step)
+  )
+}
+
+fn source_medium_carried<R>(carried: R, fidelity: DecodeFidelity) -> Medium<R> {
+  Medium { carried: carried, fidelity: fidelity }
+}

dsl/extdeps/github/expressions.dag

@@ -2,7 +2,9 @@ module extdeps.github.expressions
 
 import extdeps.external_authority { ExternalAuthority }
 import extdeps.uri { Uri, Https }
-import extdeps.communication.medium { Medium, Lossless }
+import extdeps.communication.medium { Lossless }
+import std.disposition { Disposition, Scaffold, SingleAuthority }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
 
 data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
   uri: Uri {
@@ -303,8 +305,13 @@ fn ingest_template(src: String) -> ExpressionTemplate? {
   ingest_template_with(src: src, sp: default_expression_spellings)
 }
 
-fn gha_expression_medium_lossless(expr: Expression) -> Medium<Expression> {
-  Medium { carried: expr, fidelity: Lossless }
+data gha_expression_roundtrip_canonical_inline_scaffold: Disposition = Scaffold {
+  dissolves_to: SingleAuthority,
+  bind: DeclarationRef {
+    module_path: "v2.compiler.target_carriers",
+    decl_name: "decode_fidelity_from_target",
+    field: WholeDeclaration
+  }
 }
 
 fn runner_os() -> Expression { ContextAccess { context: Runner, path: ["os"] } }

dsl/gunbc/bmc_onboarding.dag

@@ -9,6 +9,9 @@ import extdeps.bmc.types { RedfishBootSourceOverrideTarget, BootTargetPxe, Redfi
 import extdeps.bmc.openbmc { openbmc_factory_login }
 import extdeps.boards.asrock_rack { asrock_altrad8ud_redfish_system_id }
 import extdeps.communication.medium { DecodeFidelity, Lossless, Lossy, Medium }
+import extdeps.communication.fidelity_carriers { decode_fidelity_from_step_fidelities }
+import std.disposition { Disposition, Scaffold, SingleAuthority }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
 
 type BmcOnboardingPhase =
     FactoryDefault
@@ -177,30 +180,30 @@ fn bmc_full_state_is_lossy_after_roundtrip(s: BmcLifecycleState) -> Bool {
   !(recovered == s)
 }
 
-fn bmc_decom_step_fidelity(into_phase: BmcOnboardingPhase) -> DecodeFidelity {
-  match into_phase {
-    FactoryDefault => Lossless
-    CredentialsRotated => Lossy
-    OsInstalled => Lossless
-    FabricJoined => Lossless
-  }
-}
+data bmc_lifecycle_decom_step_fidelities_dissolution_trigger: String = "🟡 parallel-representation: positional List<DecodeFidelity> indexed implicitly by bmc_onboarding_phase_order — phase↔fidelity correspondence is silent; dissolves when bmc lifecycle reads fidelity via decode_fidelity_from_target on a TargetModel fidelity_quotient (same bind as bmc_lifecycle_inverse_fidelity_inline_scaffold)"
 
-fn bmc_lifecycle_inverse_fidelity() -> DecodeFidelity {
-  fold(
-    bmc_onboarding_phase_order,
-    init: Lossless,
-    f: (acc, ph) => match acc {
-      Lossy => Lossy
-      Lossless => bmc_decom_step_fidelity(into_phase: ph)
-    }
-  )
+data bmc_lifecycle_decom_step_fidelities: List<DecodeFidelity> = [
+  Lossless,
+  Lossy,
+  Lossless,
+  Lossless
+]
+
+data bmc_lifecycle_inverse_fidelity_inline_scaffold: Disposition = Scaffold {
+  dissolves_to: SingleAuthority,
+  bind: DeclarationRef {
+    module_path: "v2.compiler.target_carriers",
+    decl_name: "decode_fidelity_from_target",
+    field: WholeDeclaration
+  }
 }
 
 fn bmc_lifecycle_roundtrip(s: BmcLifecycleState) -> Medium<BmcRecoverableInvariant> {
   Medium {
-    carried: bmc_recoverable_quotient(s: bmc_decom_to_factory_state(s: bmc_onboard_to_steady_state(s: s))),
-    fidelity: bmc_lifecycle_inverse_fidelity()
+    carried: bmc_recoverable_quotient(
+      s: bmc_decom_to_factory_state(s: bmc_onboard_to_steady_state(s: s))
+    ),
+    fidelity: decode_fidelity_from_step_fidelities(steps: bmc_lifecycle_decom_step_fidelities)
   }
 }
 

dsl/test/claim/bmc_onboarding_lifecycle_witness_test.dag

@@ -26,7 +26,6 @@ import gunbc.bmc_onboarding {
   bmc_transition_roundtrips_on_quotient,
   bmc_full_state_is_lossy_after_roundtrip,
   bmc_lifecycle_roundtrip,
-  bmc_lifecycle_inverse_fidelity,
   bmc_phase_credential_posture,
   bmc_lifecycle_is_monotone_hardening,
   bmc_lifecycle_length,
@@ -177,14 +176,10 @@ test fn bmc_decom_does_not_roundtrip_when_inverse_is_wrong() -> Bool {
 }
 
 test fn bmc_lifecycle_inverse_is_lossy_section_not_iso() -> Bool {
-  match bmc_lifecycle_inverse_fidelity() {
+  match bmc_lifecycle_roundtrip(s: bmc_factory_state()).fidelity {
     Lossy => true
     Lossless => false
   }
-    && match bmc_lifecycle_roundtrip(s: bmc_factory_state()).fidelity {
-      Lossy => true
-      Lossless => false
-    }
     && bmc_full_state_is_lossy_after_roundtrip(s: factory_at(p: FactoryDefault))
 }
 

dsl/test/claim/gha_expression_roundtrip_test.dag

@@ -19,15 +19,15 @@ import extdeps.github.expressions {
   ingest_expression,
   ingest_expression_with,
   ingest_template,
-  gha_expression_medium_lossless,
   Github,
   Runner,
   HashFiles,
   Contains,
   FromJSON,
   Format,
 }
-import extdeps.communication.medium { Lossless, Lossy }
+import extdeps.communication.fidelity_carriers { source_medium_carried }
+import extdeps.communication.medium { Lossless }
 
 fn core_expr() -> Expression {
   LogicalOr {
@@ -53,24 +53,13 @@ fn core_template() -> ExpressionTemplate {
   }
 }
 
-fn roundtrips_canonical(e: Expression) -> Bool {
-  match ingest_expression(src: serialize_expression(expression: e)) {
-    Present { value: v } => v == e
+fn witness_roundtrip_expression() -> Bool {
+  match ingest_expression(src: serialize_expression(expression: core_expr())) {
+    Present { value: v } => v == core_expr()
     Absent => false
   }
 }
 
-fn does_not_roundtrip(e: Expression) -> Bool {
-  match ingest_expression(src: serialize_expression(expression: e)) {
-    Present { value: v } => !(v == e)
-    Absent => true
-  }
-}
-
-fn witness_roundtrip_expression() -> Bool {
-  roundtrips_canonical(e: core_expr())
-}
-
 fn witness_roundtrip_template() -> Bool {
   match ingest_template(src: serialize_template(template: core_template())) {
     Present { value: v } => v == core_template()
@@ -142,7 +131,14 @@ fn right_nested_or() -> Expression {
 }
 
 fn witness_or_associativity_partition() -> Bool {
-  roundtrips_canonical(e: left_nested_or()) && does_not_roundtrip(e: right_nested_or())
+  match ingest_expression(src: serialize_expression(expression: left_nested_or())) {
+    Present { value: left_v } =>
+      match ingest_expression(src: serialize_expression(expression: right_nested_or())) {
+        Present { value: right_v } => (left_v == left_nested_or()) && !(right_v == right_nested_or())
+        Absent => false
+      }
+    Absent => false
+  }
 }
 
 fn frontier_string_with_or() -> Expression {
@@ -167,15 +163,27 @@ fn frontier_nested_multiarg_call() -> Expression {
 }
 
 fn witness_frontier_not_roundtripped() -> Bool {
-  does_not_roundtrip(e: right_nested_or())
-    && does_not_roundtrip(e: frontier_string_with_or())
-    && does_not_roundtrip(e: frontier_nested_multiarg_call())
+  match ingest_expression(src: serialize_expression(expression: right_nested_or())) {
+    Present { value: v1 } =>
+      match ingest_expression(src: serialize_expression(expression: frontier_string_with_or())) {
+        Present { value: v2 } =>
+          match ingest_expression(src: serialize_expression(expression: frontier_nested_multiarg_call())) {
+            Present { value: v3 } =>
+              !(v1 == right_nested_or())
+                && !(v2 == frontier_string_with_or())
+                && !(v3 == frontier_nested_multiarg_call())
+            Absent => true
+          }
+        Absent => true
+      }
+    Absent => true
+  }
 }
 
 fn witness_core_advertised_lossless() -> Bool {
   match ingest_expression(src: serialize_expression(expression: core_expr())) {
     Present { value: v } => {
-      let m = gha_expression_medium_lossless(expr: v)
+      let m = source_medium_carried(carried: v, fidelity: Lossless)
       match m.fidelity {
         Lossless => m.carried == core_expr()
         Lossy => false

src/v2/compiler/06_translate.dag

@@ -11,7 +11,7 @@ import v2.extdeps.languages.dag {
   ParseSubtreeFound
 }
 import extdeps.communication.medium { Lossless, Medium }
-import v2.compiler.target_carriers { lossless_source }
+import v2.compiler.target_carriers { target_source_medium }
 import v2.std.compilers.target_model {
   CanonicalOperation,
   TargetBodiedArrowStatementScaffold,
@@ -807,7 +807,7 @@ fn serialize_concrete_syntax_tokens_to_source(
   bind_outcome(
     o: serialize_concrete_syntax_tokens_to_source_string(target: target, tokens: tokens),
     f: fn(text) {
-      outcome_accepted(lossless_source(text: text))
+      target_source_medium(text: text, target: target)
     }
   )
 }
@@ -1181,7 +1181,7 @@ fn target_serialize_source_from_model(
       bind_outcome(
         o: target_serialize_source_from_model_bounded(measure, target, emitted),
         f: fn(text) {
-          outcome_accepted(lossless_source(text: text))
+          target_source_medium(text: text, target: target)
         }
       )
     }