HealthzEffectiveRead becomes the coproduct it always was; the rung is measured, not claimed

dag/gunbc/live_deploy/readiness.dag

@@ -55,7 +55,7 @@ import gunbc.running_release_identity {
   SurfaceBundleIdentityMalformed,
   observe_running_release_identity,
 }
-import gunbc.roadmap_site_surface_types { RoadmapSiteSurfaceBundle, HealthzEffectiveRead }
+import gunbc.roadmap_site_surface_types { RoadmapSiteSurfaceBundle, HealthzEffectiveRead, HealthzBodyRead, HealthzProbeRefused }
 import gunbc.live_deploy.spec {
   DeploymentSpec,
   deployment_spec_srv1,
@@ -111,9 +111,9 @@ fn service_ready_apply_effect_for_deploy(spec: DeploymentSpec) -> ServiceReadyAp
 
 fn healthz_effective_read_from_get(success: Bool, body: String, error: String) -> HealthzEffectiveRead {
   if success {
-    HealthzEffectiveRead { body: body, probe_error: "" }
+    HealthzBodyRead { body: body }
   } else {
-    HealthzEffectiveRead { body: "", probe_error: error }
+    HealthzProbeRefused { probe_error: error }
   }
 }
 
@@ -135,7 +135,7 @@ fn healthz_effective_read_from_outcome(outcome: TypedArgvExecOutcome) -> Healthz
         body: r.stdout,
         error: "http client GET over ssh failed"
       )
-    TypedArgvExecRefused { reason: why } => HealthzEffectiveRead { body: "", probe_error: why }
+    TypedArgvExecRefused { reason: why } => HealthzProbeRefused { probe_error: why }
   }
 }
 
@@ -157,7 +157,7 @@ fn live_deploy_healthz_get_ssh(port: Int, host: NonEmptyStr) -> HealthzEffective
   let url = live_deploy_health_url_for_port(port: port)
   let argv = http_client_get_argv(url: url)
   match typed_argv_shell_safe_refusal_argv(argv: argv) {
-    Present { value: why } => HealthzEffectiveRead { body: "", probe_error: why }
+    Present { value: why } => HealthzProbeRefused { probe_error: why }
     Absent =>
       match typed_argv_exec_over_ssh(host: host, argv: argv) {
         TypedArgvExecConverged { result: r } =>
@@ -167,7 +167,7 @@ fn live_deploy_healthz_get_ssh(port: Int, host: NonEmptyStr) -> HealthzEffective
             error: "http client GET over ssh failed"
           )
         TypedArgvExecRefused { reason: why } =>
-          HealthzEffectiveRead { body: "", probe_error: why }
+          HealthzProbeRefused { probe_error: why }
       }
   }
 }
@@ -178,8 +178,7 @@ fn live_deploy_healthz_get_for_port(port: Int, transport: HostEffectTransport) -
     SshShell { ssh_host: h } => live_deploy_healthz_get_ssh(port: port, host: h)
     FleetSsh { target: t, context: c } => live_deploy_healthz_get_fleet_ssh(port: port, target: t, context: c)
     EmitArtifactThenThinRun { bootstrap: _, invocation: _ } =>
-      HealthzEffectiveRead {
-        body: "",
+      HealthzProbeRefused {
         probe_error: "health probe refused EmitArtifactThenThinRun transport",
       }
   }
@@ -275,16 +274,37 @@ fn ground_service_ready_from_healthz_with_bundle(
   expected_revision: CommitSha,
   expected_surface_identity: Fnv1a64Structural,
 ) -> Grounding<ServiceReadyEvidence> {
-  if read.probe_error != "" {
-    DoesNotGround { reason: healthz_refusal_reason(cause: HealthzProbeFailed { detail: read.probe_error }) }
-  } else if !healthz_body_groundable(body: read.body) {
-    DoesNotGround { reason: healthz_refusal_reason(cause: HealthzBodyUnparseable { body: read.body }) }
+  match read {
+    HealthzProbeRefused { probe_error: detail } =>
+      DoesNotGround { reason: healthz_refusal_reason(cause: HealthzProbeFailed { detail: detail }) }
+    HealthzBodyRead { body: observed_body } =>
+      ground_service_ready_from_healthz_body(
+        body: observed_body,
+        bundle: bundle,
+        expected_revision: expected_revision,
+        expected_surface_identity: expected_surface_identity,
+      )
+  }
+}
+
+// The four stages BELOW the probe, split out so the probe arm above is a match rather than the
+// first clause of a chain. This function only ever sees a body, because only HealthzBodyRead can
+// reach it -- which is the climb: the probe stage cannot be forgotten, mis-ordered, or reached
+// past, because a refusal has no body to hand it.
+fn ground_service_ready_from_healthz_body(
+  body: String,
+  bundle: RoadmapSiteSurfaceBundle,
+  expected_revision: CommitSha,
+  expected_surface_identity: Fnv1a64Structural,
+) -> Grounding<ServiceReadyEvidence> {
+  if !healthz_body_groundable(body: body) {
+    DoesNotGround { reason: healthz_refusal_reason(cause: HealthzBodyUnparseable { body: body }) }
   } else {
-    match observe_running_release_identity(healthz_body: read.body) {
+    match observe_running_release_identity(healthz_body: body) {
       RunningReleaseUnidentified { cause: why } =>
         DoesNotGround {
           reason: healthz_refusal_reason(
-            cause: healthz_release_identity_refusal(body: read.body, cause: why)
+            cause: healthz_release_identity_refusal(body: body, cause: why)
           )
         }
       RunningReleaseIdentified { observation: obs } =>
@@ -302,21 +322,21 @@ fn ground_service_ready_from_healthz_with_bundle(
               observed: obs.surface_bundle_identity.digest as String,
             })
           }
-        } else if !roadmap_site_healthz_surface_is_current(bundle: bundle, observed_body: read.body) {
+        } else if !roadmap_site_healthz_surface_is_current(bundle: bundle, observed_body: body) {
           DoesNotGround {
             reason: healthz_refusal_reason(cause: ServedSurfaceStale {
-              observed: read.body,
+              observed: body,
               expected: bundle.healthz_body,
             })
           }
         } else {
-          Grounds { evidence: ServiceReadyEvidence { body: read.body } }
+          Grounds { evidence: ServiceReadyEvidence { body: body } }
         }
     }
   }
 }
 
-data readiness_check_order_note: String = "THE ORDER IS PROBE, PARSE, IDENTITY, REVISION, SURFACE, AND IT IS CHOSEN SO THE FIRST REFUSAL IS THE MOST LOCATING ONE. A process at the wrong revision usually also serves the wrong surface, so checking the surface first would report 'stale surface' for what is really 'the pre-restart process is still answering' — true but one inference away from the remedy. Checking the revision first names the process; checking the surface after names the rebind. Identity precedes both because a body with no readable identity cannot be compared on either axis, and reporting a surface verdict about a process we cannot identify would attribute the surface to the wrong party."
+data readiness_check_order_note: String = "THE ORDER IS PARSE, IDENTITY, REVISION, SURFACE, AND IT IS CHOSEN SO THE FIRST REFUSAL IS THE MOST LOCATING ONE. A process at the wrong revision usually also serves the wrong surface, so checking the surface first would report 'stale surface' for what is really 'the pre-restart process is still answering' — true but one inference away from the remedy. Checking the revision first names the process; checking the surface after names the rebind. Identity precedes both because a body with no readable identity cannot be compared on either axis, and reporting a surface verdict about a process we cannot identify would attribute the surface to the wrong party.\\n\\nTHIS ROW USED TO NAME FIVE STAGES AND NOW NAMES FOUR, and the missing one is the point: PROBE is no longer ordered by this note because it is no longer ordered by anything. HealthzEffectiveRead became a coproduct (gunbc.roadmap_site_surface_types), so a refused probe carries no body at all and the parse stage is unreachable from it — not checked-first, but unreachable. The four above remain ordering-by-discipline inside ground_service_ready_from_healthz_body: they are stages over ONE String, and nothing structural stops a future edit from reordering them, so this note is still doing real work for them. It is stated this way rather than deleted wholesale because a note that shrank silently would read as though the whole ordering had been made structural, which is the rung inflation DESIGN §4b calls worse than sitting low."
 
 fn ground_service_ready_from_healthz(
   read: HealthzEffectiveRead,
@@ -340,8 +360,7 @@ fn show_healthz_read_for_deploy(
   match verdict {
     Deny { refusal: _ } =>
       ReadObserved {
-        value: HealthzEffectiveRead {
-          body: "",
+        value: HealthzProbeRefused {
           probe_error: deploy_access_decision_reason(d: verdict),
         }
       }
@@ -362,7 +381,7 @@ fn show_healthz_read_fixture_healthy(
   release_revision: CommitSha,
 ) -> ShowEffectiveRead<HealthzEffectiveRead> {
   ReadObserved {
-    value: HealthzEffectiveRead {
+    value: HealthzBodyRead {
       body: healthz_body_with_release_identity(
         roadmap: bundle.roadmap_md,
         dispatch: bundle.dispatch_json,
@@ -372,7 +391,6 @@ fn show_healthz_read_fixture_healthy(
         release_revision: release_revision,
         surface_bundle_identity: bundle.bundle_identity,
       ),
-      probe_error: "",
     }
   }
 }

dag/gunbc/roadmap_site_surface_expect.dag

@@ -15,7 +15,7 @@ import extdeps.languages.json.parse {
 import v2.std.collection { Absent, Present }
 import extdeps.languages.json.emit { JsonValue, JsonKeyValue, json_kv, json_object, serialize_json }
 import extdeps.http.server { media_type_wire_label, application_json_utf8 }
-import gunbc.roadmap_site_surface_types { RoadmapSiteSurfaceBundle, RoadmapSiteSurfaceArtifact, HealthzEffectiveRead }
+import gunbc.roadmap_site_surface_types { RoadmapSiteSurfaceBundle, RoadmapSiteSurfaceArtifact, HealthzEffectiveRead, HealthzBodyRead, HealthzProbeRefused }
 
 data roadmap_site_surface_expect_note: String = "PURE bundle predicates for roadmap served-surface witnesses. Every function here takes an already-materialized RoadmapSiteSurfaceBundle (or a typed HTTP read) and performs no filesystem, Git, authority, or rendering observation."
 
@@ -107,9 +107,12 @@ fn healthz_round_trip_receipt_holds(bundle: RoadmapSiteSurfaceBundle) -> Bool {
 }
 
 fn healthz_read_grounds(bundle: RoadmapSiteSurfaceBundle, read: HealthzEffectiveRead) -> Bool {
-  read.probe_error == ""
-    && roadmap_site_healthz_json_string_parses(body: read.body)
-    && roadmap_site_healthz_surface_is_current(bundle: bundle, observed_body: read.body)
+  match read {
+    HealthzProbeRefused { probe_error: _ } => false
+    HealthzBodyRead { body: observed_body } =>
+      roadmap_site_healthz_json_string_parses(body: observed_body)
+        && roadmap_site_healthz_surface_is_current(bundle: bundle, observed_body: observed_body)
+  }
 }
 
 fn fresh_surface_read_grounds(bundle: RoadmapSiteSurfaceBundle, read: HealthzEffectiveRead) -> Bool {
@@ -121,7 +124,7 @@ fn stale_surface_read_does_not_ground(bundle: RoadmapSiteSurfaceBundle, stale_bo
     && !roadmap_site_healthz_surface_is_current(bundle: bundle, observed_body: stale_body)
     && !healthz_read_grounds(
       bundle: bundle,
-      read: HealthzEffectiveRead { body: stale_body, probe_error: "" },
+      read: HealthzBodyRead { body: stale_body },
     )
 }
 

dag/gunbc/roadmap_site_surface_types.dag

@@ -4,10 +4,75 @@ import std.types { String, NonEmptyStr }
 import std.content_hash { Fnv1a64Structural }
 import gunbc.roadmap_model { RoadmapNodeId }
 
-type HealthzEffectiveRead {
-  body: String
-  probe_error: String
-}
+// A HEALTHZ READ IS A COPRODUCT AND ALWAYS WAS -- this declaration now says so.
+//
+// It used to be a two-field record whose discriminant was carried as "which field did I leave
+// empty". Every one of its twenty constructions set exactly one field; not one ever set both,
+// because there is no such observation: a probe either landed and produced a body, or it refused
+// and produced a reason. The empty string was doing the work of a tag, in a type that also admits
+// the empty string as a legitimate body.
+//
+// WHAT THE COPRODUCT REMOVES, and both are state-space reductions rather than added checks.
+// A refusal no longer HAS a body field, so reading a body off a failed probe is unwritable rather
+// than merely wrong -- and the consumer that used to guarantee this by checking probe_error first
+// now cannot get it wrong in any order, because the compiler will not let it reach a body it does
+// not have. And { body: "x", probe_error: "y" } -- representable before, meaningless always -- has
+// no legitimate constructor: nothing can produce it through either variant. It can still be SPELLED
+// as a bare record literal, which is the one place this climb stops short; the rung block below
+// measures exactly where, rather than letting this paragraph round it up.
+//
+// THE RUNG, MEASURED IN BOTH DIRECTIONS RATHER THAN ASSERTED -- and it is TWO rungs, because the
+// two ways of writing the invalid state are refused at two different times.
+//
+// FIELD ACCESS IS STRUCTURAL. `read.body` against this carrier is a located resolve-time refusal:
+// `error: no field 'body' on type 'HealthzEffectiveRead'`, reported during strict-preparation with
+// modules_resolved=3729, before a single witness executes. A probe was written to reach a body off
+// a HealthzProbeRefused and the floor refused to prepare at all. So the headline claim -- a refusal
+// has no body to read -- is structurally guaranteed, and it is in fact broader than that: the
+// carrier has no fields at the type level, so every field-access route into it is gone, not just
+// the one on the refusal arm.
+//
+// THE BARE RECORD LITERAL IS NOT. Writing `HealthzEffectiveRead { body: .., probe_error: .. }` --
+// the old shape, tagging no variant -- still RESOLVES and still constructs; it is refused only when
+// something matches on it, at evaluation, as `non-exhaustive pattern match on: HealthzEffectiveRead
+// { body: .., probe_error: .. }`. Measured, not inferred: the pre-change probe passed on the record
+// and the same source became a per-witness runtime FAIL after the coproduct landed, with the corpus
+// fully executed (planned=9784) rather than refused in preparation.
+//
+// So the honest ceiling for the CONSTRUCTION half is mechanically preventable, not structurally
+// impossible: the invalid value is writable, and what stops it is a runtime refusal that has to
+// execute. NEXT-RUNG TRIGGER: a record literal naming a coproduct type with no variant tag should
+// refuse at resolve, where the field-access form already does. SHARPENED after measuring what the
+// compiler already computes, because "a compiler capability" -- how an earlier revision of this
+// line read -- implies infrastructure that has to be built, and that is not what is missing. The
+// predicate exists and is one expression: v1.compiler.types is_coproduct_type answers it as
+// n.connective == Disj. Record-literal inference already resolves the named type and already
+// reasons about coproduct membership on the neighbouring path -- lookup_variant_parent_enum,
+// variant_owner_node, record_lit_variant_from_expected and record_lit_expected_coproduct all sit
+// in v1.compiler.infer. What is absent is the refusal, not the fact. NOTED AT THE REACH MEASURED
+// AND NO FURTHER: those symbols answer the VARIANT-named literal (this name is an arm, whose
+// parent is X), while the case here is the PARENT-named literal, which is a different question,
+// and I have neither built nor tested the refusal. So this is DESIGN section 4b's third category
+// -- can climb now but unbuilt -- rather than its second, and the distinction is the whole reason
+// for correcting the line. ONE TRAP FOR WHOEVER BUILDS IT, named here because a trigger exists to
+// stop a future implementation being wrong: is_coproduct_type is sufficient for the DIRECT,
+// exactly-resolved specimen this row measured. Generalizing it must apply the predicate to the
+// RESOLVED STRUCTURAL declaration, not assume every authored alias node itself carries Disj -- an
+// alias to a coproduct need not, and a check that tested the alias node would silently admit
+// exactly the construction it was written to refuse. Until that lands, saying this carrier makes the state
+// unwritable would be the rung inflation DESIGN §4b calls worse than sitting low -- which is why
+// the paragraph above says what it says, and why the probes that established it are cited here by
+// their measurement rather than left enrolled: both are hard refusals, so neither can survive in
+// the corpus as an executing control.
+//
+// WHAT IT DOES NOT REMOVE, stated so this row is not read as more than it is. Readiness grounds in
+// five ordered stages (probe, parse, identity, revision, surface) and this makes only the FIRST
+// structural. The other four remain ordering-by-discipline inside
+// gunbc.live_deploy.readiness ground_service_ready_from_healthz_with_bundle; see that module's
+// readiness_check_order_note, which now names the four that remain rather than all five.
+type HealthzEffectiveRead
+  = HealthzBodyRead { body: String }
+  | HealthzProbeRefused { probe_error: String }
 
 type RoadmapSiteSurfaceArtifact {
   url_path: NonEmptyStr

dag/gunbc/roadmap_site_surface_witness.dag

@@ -13,6 +13,7 @@ import std.realization_reconcile {
 }
 import gunbc.live_deploy.readiness {
   HealthzEffectiveRead,
+  HealthzBodyRead,
   reconcile_service_ready_read_for_bundle,
   live_deploy_service_ready_once_for_bundle,
   show_healthz_read_fixture_healthy,
@@ -35,7 +36,7 @@ data witness_stale_artifact_digest_hex: String = "0000000000000000"
 fn fresh_surface_read_grounds_for_bundle(bundle: RoadmapSiteSurfaceBundle) -> Bool {
   fresh_surface_read_grounds(
     bundle: bundle,
-    read: HealthzEffectiveRead { body: bundle.healthz_body, probe_error: "" },
+    read: HealthzBodyRead { body: bundle.healthz_body },
   )
 }
 
@@ -86,7 +87,7 @@ fn stale_surface_read_does_not_ground_for_bundle(
   )
   stale_surface_read_does_not_ground(bundle: bundle, stale_body: stale_body)
     && match ground_service_ready_from_healthz_with_bundle(
-      read: HealthzEffectiveRead { body: stale_body, probe_error: "" },
+      read: HealthzBodyRead { body: stale_body },
       bundle: bundle,
       expected_revision: release_revision,
       expected_surface_identity: bundle.bundle_identity,