v1_rt decouple — Witness/Diagnostic carrier architecture (design-note-first)

dag/gunbc/doc_graph_roots.dag

@@ -185,6 +185,12 @@ data hand_authored_doc_binds: List<HandAuthoredDocBind> = [
     work: DeclarationRef { module_path: "v2.lens.extdeps_shape_transport_policy", decl_name: "extdeps_shape_transport_policy_clean_holds", field: WholeDeclaration },
     dissolution: HasTrigger { text: "the extdeps positioning restructure PR (pure git mv + import repoint: os/ de-grab-bag + findings 1-4 hub-loose, all under the §3 extdeps discipline this lens enforces) lands and the extdeps directories are §3-congruent — the brief's scope is discharged; delete this row and the doc together" },
   },
+  HandAuthoredDocBind {
+    home: PlanDoc,
+    slug: "v1rt-witness-diagnostic-carrier-decouple-design",
+    work: DeclarationRef { module_path: "v2.std.witness", decl_name: "witness_from_optional", field: WholeDeclaration },
+    dissolution: HasTrigger { text: "Stage-4 Gate-1 E0308 burn-down probe receipt lands (design note §3 — measurement only); doc archives or registers as a gunbc.plan.Plan row" },
+  },
 ]
 
 fn hand_authored_doc_graph_roots() -> List<String> {

dag/gunbc/host_toolchain_ensure.dag

@@ -45,7 +45,7 @@ data host_toolchain_ensure_apply_dispatch_scaffold: Disposition = Scaffold {
 
 data host_toolchain_reach_pairing_note: String = "Access is DERIVED FROM THE TARGET HOST, never looked up independently from the requested host. Before 2026-07-24 these were two parallel decisions: host_toolchain_ensure_target_host was kind-aware (srv3 + OsInstallActuator resolves to the SELECTED actuator host) while the access lookup keyed on the requested host alone and pinned srv3 to ci_deploy_srv1_operator_access. Two defects followed, both silent. (1) A BuildCache request for srv3 targeted srv3 but authenticated to srv1, so the provisioning effect would have landed on the WRONG MACHINE and reported success — a §5 fail-open, and the exact kind this lane adds. (2) The srv1 pin is only correct in the actuator selector's UNSATISFIABLE FALLBACK arm; whenever ActuatorSelected names a different host the access still pointed at srv1. Pairing target and access in one return value makes the disagreement unwritable (§5 construction over validation) rather than a check that could flag it afterwards. Consequence: this module no longer consumes ci_deploy_srv1_operator_access, which is construction-identical to host_identity_srv1_access (same principal, host, transport, privileged commands — witnessed by host_toolchain_srv1_access_rows_are_one_concept); that §3 nickname still has consumers elsewhere and its corpus-wide dissolution is a separate lane, not smuggled in here."
 
-type HostToolchainReach = HostToolchainReach {
+type HostToolchainReach = ResolvedHostToolchainReach {
   target: ComputeHost,
   access: DeployAccess,
 }
@@ -75,7 +75,7 @@ fn host_toolchain_ensure_reach(
     Present { value: target } =>
       match host_toolchain_direct_access(host: target.identity) {
         Present { value: access } =>
-          ReachResolved { reach: HostToolchainReach { target: target, access: access } }
+          ReachResolved { reach: ResolvedHostToolchainReach { target: target, access: access } }
         Absent => ReachAccessAbsent { target_identity: target.identity }
       }
     Absent => ReachTargetAbsent {}

dag/std/algebra.dag

@@ -117,7 +117,7 @@ type FreeMonoid<T>
   | Cons { head: T, tail: FreeMonoid<T> }
 
 type PartialFunction<K, V> {
-  lookup: fn(K) -> Witness<V>
+  lookup: fn(K) -> V?
   empty: PartialFunction<K, V>
   get: fn(K) -> V?
   insert: fn(K, V) -> PartialFunction<K, V>
@@ -309,7 +309,7 @@ fn partial_function_templates() -> List<AlgebraFieldTemplate> {
   [
     { name: "get", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none },
     { name: "map_get", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none },
-    { name: "lookup", param_types: [ReceiverSelf, ReceiverKey], return_type: WitnessOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none },
+    { name: "lookup", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none },
     { name: "map_insert", param_types: [ReceiverSelf, ReceiverKey, ReceiverValue], return_type: ReceiverSelf, size_effect: none, cost_shape: none, callback_element_position: none },
     { name: "map_merge", param_types: [ReceiverSelf, ReceiverSelf], return_type: ReceiverSelf, size_effect: none, cost_shape: none, callback_element_position: none },
     { name: "has", param_types: [ReceiverSelf, ReceiverKey], return_type: NamedTemplate { name: "Bool" }, size_effect: none, cost_shape: none, callback_element_position: none },

dag/test/claim/floor_discovery_hand_rust_equivalence_witness_test.dag

@@ -37,7 +37,15 @@ import v2.workflow.floor_naming_hygiene {
 }
 import v2.std.algebra { length, list_head, HeadFound, HeadAbsent }
 import std.disposition { Disposition, Scaffold, SingleAuthority }
-import v2.std.collection { Absent, List, Optional, Present, fold_list }
+import v2.std.collection {
+  List,
+  fold_list
+}
+import v2.std.optional {
+  Absent,
+  Optional,
+  Present
+}
 import std.types { Bool, String }
 import std.disposition { Scaffold, SingleAuthority }
 import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

dag/test/claim/map_lookup_dual_dispatch_witness_test.dag

@@ -16,12 +16,12 @@ test fn map_index_routes_through_dual_dispatch_chokepoint() -> Bool {
 test fn lookup_builtin_routes_through_dual_dispatch_chokepoint() -> Bool {
   let m = empty_map() |> map_insert("k", 7)
   match lookup(m, "k") {
-    Holds { value: v } => v == 7
-    _ => false
+    Present { value: v } => v == 7
+    Absent => false
   }
 }
 
-data lookup_witness_contract_note: String = "lookup routes through the dual-dispatch chokepoint, which wraps the hit in the Witness coproduct (Holds { value } | Violates) — proven by execution 2026-07-12. The earlier bare `lookup(m, k) == 7` compared the Holds wrapper against a native Int, which the cross-representation equality guard refuses by design (DESIGN §5); matching Holds is the discriminating form — a raw 7 here would mean the bare builtin BYPASSED the chokepoint."
+data lookup_witness_contract_note: String = "lookup routes through the dual-dispatch chokepoint, which wraps the hit in the Optional coproduct (Present { value } | Absent) — the v1_rt Witness<V> carrier was deleted (v1_rt-witness-diagnostic-carrier-decouple-design.md); lookup now returns Option<V> natively. Matching Present is still the discriminating form — a raw 7 here would mean the bare builtin BYPASSED the chokepoint, and Present/Absent proves the modeled dispatch runs."
 
 test fn std_graph_build_adjacency_views_evaluates() -> Bool {
   let names = ["a", "b"]

dag/test/claim/srv3_subsumption_witness_test.dag

@@ -179,7 +179,7 @@ fn reach_pair_agrees_for(reach: HostToolchainReach) -> Bool {
 }
 
 test fn reach_wrong_machine_pairing_is_unwritable() -> Bool {
-  let old_shape = HostToolchainReach {
+  let old_shape = ResolvedHostToolchainReach {
     target: srv3_host,
     access: host_identity_srv1_access,
   }

dag/tools/self_host_module_behavioral_transport_roster.dag

@@ -6,7 +6,16 @@ import tools.self_host_curated_seed_linked_harness {
   cssl_seed_linked_behavioral_receipt
 }
 import v2.std.algebra { fold_list }
-import v2.std.collection { List, Optional, Absent, Present, optional_absent, optional_present }
+import v2.std.collection {
+  List
+}
+import v2.std.optional {
+  Optional,
+  Absent,
+  Present,
+  optional_absent,
+  optional_present
+}
 import v2.std.logic { Bool }
 import v2.std.text { String }