The native side can refuse, and the label that would report it aborts on any real value

src/v2/compiler/self_host/native_agreement_support.dag

@@ -6,19 +6,30 @@ import v2.std.optional {
   Present,
   Absent
 }
-import v2.std.diagnostic { Accepted }
+import v2.std.diagnostic { Accepted, Rejected }
 import v2.std.native_agreement {
   NativeAgreementDivergence,
   runtime_value_octet_label
 }
 import v2.std.runtime { RuntimeValue }
-import v2.std.verdict { Pass, SemanticMismatch, BuildFailed, RunFailed, Deferred }
+import v2.std.verdict { Verdict, Pass, SemanticMismatch, BuildFailed, RunFailed, Deferred }
 
 fn native_agreement_divergence_from_run<Subj>(
   member_id: String,
   run: TestClaimRun<Subj, RuntimeValue>
 ) -> Optional<NativeAgreementDivergence> {
-  match run.verdict {
+  native_agreement_divergence_from_verdict(member_id: member_id, verdict: run.verdict)
+}
+
+// THE SUBJECT OF THIS FOLD IS THE VERDICT, NOT THE RUN. It read `run.verdict` and nothing else,
+// so taking the whole `TestClaimRun` made its only caller a full emit-vs-eval execution: the
+// cache receipt is unreachable input that no witness can supply, which is why the Rejected arm
+// below had no executable evidence until the parameter was narrowed to what the fold reads.
+fn native_agreement_divergence_from_verdict<V>(
+  member_id: String,
+  verdict: Verdict<V, RuntimeValue>
+) -> Optional<NativeAgreementDivergence> {
+  match verdict {
     Pass => Absent
     SemanticMismatch {
       actual: Accepted { value: native_val, diagnostics: _ },
@@ -33,6 +44,19 @@ fn native_agreement_divergence_from_run<Subj>(
           native_value: runtime_value_octet_label(value: native_val)
         }
       }
+    SemanticMismatch {
+      actual: Rejected { diagnostics: _ },
+      falsification: Present {
+        value: receipt
+      }
+    } =>
+      Present {
+        value: NativeAgreementDivergence {
+          member_id: member_id,
+          interpreted_value: runtime_value_octet_label(value: receipt.expected),
+          native_value: "rejected"
+        }
+      }
     SemanticMismatch { actual: _, falsification: Absent } =>
       Present {
         value: NativeAgreementDivergence {

src/v2/std/native_agreement.dag

@@ -11,7 +11,7 @@ import v2.std.optional {
   Absent
 }
 import v2.std.logic { Bool }
-import v2.std.integer { integer_int_to_decimal_string }
+import v2.std.integer { integer_int_to_decimal_string, integer_u8_from_byte }
 import v2.std.runtime { RuntimePrimitive, RuntimePrimitiveValue, RuntimeValue }
 import v2.std.text { String }
 
@@ -34,12 +34,23 @@ fn octet_display(octet: Int) -> String {
   integer_int_to_decimal_string(value: octet)
 }
 
+// THE OCTET IS AN Int AND THE LIST HOLDS Byte. `list_at_optional` over a `List<Byte>` yields
+// `Optional<Byte>`, which this function previously returned under a declared `Optional<Int>`:
+// the record then reached `octet_display`'s Int parameter and every label of a primitive with a
+// second byte aborted with `cannot apply Lt to Record and Int`. It stayed invisible because the
+// only reachable arm in practice was the empty-list one, whose `Absent` answers "?" -- so the
+// formatter that exists to stop a divergence being reported as values-unknown could instead
+// abort exactly when a divergence was being reported. The conversion is named here rather than
+// the declaration widened, because the carrier's octet IS an integer.
 fn runtime_value_discriminant_octet(value: RuntimeValue) -> Optional<Int> {
   match value {
     RuntimePrimitive {
       value: RuntimePrimitiveValue { bytes: bytes, primitive_type: _ }
     } =>
-      list_at_optional(xs: bytes, index: 1)
+      match list_at_optional(xs: bytes, index: 1) {
+        Present { value: octet_byte } => Present { value: integer_u8_from_byte(b: octet_byte) }
+        Absent => Absent
+      }
     _ => Absent
   }
 }

src/v2/test/claim/self_host/native_agreement_label_probe_test.dag

@@ -0,0 +1,37 @@
+module v2.test.claim.self_host.native_agreement_label_probe_test
+
+import v2.std.native_agreement { runtime_value_octet_label }
+import v2.std.node { Node, TypeNode, Atom, OccurrenceSynthetic }
+import v2.std.runtime { RuntimeValue, RuntimePrimitive, RuntimePrimitiveValue }
+import v2.std.machine { Byte }
+
+fn probe_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^label_probe_type } },
+    children: [],
+    occurrence_id: OccurrenceSynthetic
+  }
+}
+
+fn probe_two_bytes() -> RuntimeValue {
+  RuntimePrimitive {
+    value: RuntimePrimitiveValue {
+      primitive_type: probe_node(),
+      bytes: [Byte { bits: [true] }, Byte { bits: [false] }]
+    }
+  }
+}
+
+fn probe_zero_bytes() -> RuntimeValue {
+  RuntimePrimitive {
+    value: RuntimePrimitiveValue { primitive_type: probe_node(), bytes: [] }
+  }
+}
+
+test fn label_of_a_two_byte_primitive() -> Bool {
+  runtime_value_octet_label(value: probe_two_bytes()) != "?"
+}
+
+test fn label_of_an_empty_primitive_is_unknown() -> Bool {
+  runtime_value_octet_label(value: probe_zero_bytes()) == "?"
+}

src/v2/test/claim/self_host/native_agreement_rejected_actual_test.dag

@@ -0,0 +1,106 @@
+module v2.test.claim.self_host.native_agreement_rejected_actual_test
+
+import v2.compiler.self_host.native_agreement_support {
+  native_agreement_divergence_from_verdict
+}
+import v2.std.diagnostic {
+  Diagnostic,
+  Rejected,
+  Textual,
+  WholeFile,
+  Unavailable,
+  AmbiguousIntent,
+  diagnostics_singleton
+}
+import v2.std.node { Node, TypeNode, Atom, OccurrenceSynthetic }
+import v2.std.optional { Optional, Present, Absent }
+import v2.std.runtime { RuntimeValue, RuntimePrimitive, RuntimePrimitiveValue }
+import v2.std.machine { Byte }
+import v2.std.host_run { ValueDiff }
+import v2.std.test_claim_falsification { FalsificationReceipt, EvidenceNone }
+import v2.std.verdict { Verdict, SemanticMismatch }
+import v2.std.native_agreement { NativeAgreementDivergence }
+
+// THE NATIVE SIDE CAN REFUSE, AND A REFUSAL IS NOT AN ABSENT VALUE. `SemanticMismatch` carries
+// `actual: Outcome<RuntimeValue>`, so `Rejected` is one of its two inhabitants; the divergence
+// carrier has three String fields and no channel for a refusal reason, so the native side is
+// named by the sentinel this file's siblings already use for "no value here" while the
+// INTERPRETED side keeps the real value the falsification receipt holds. Reporting "?" for both
+// would discard a value in hand, which is the loss v2.std.native_agreement exists to prevent.
+
+fn rejected_probe_type_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^native_agreement_rejected_probe_type } },
+    children: [],
+    occurrence_id: OccurrenceSynthetic
+  }
+}
+
+fn rejected_probe_value() -> RuntimeValue {
+  RuntimePrimitive {
+    value: RuntimePrimitiveValue {
+      primitive_type: rejected_probe_type_node(),
+      bytes: [Byte { bits: [true] }, Byte { bits: [false] }]
+    }
+  }
+}
+
+fn rejected_probe_diagnostic() -> Diagnostic {
+  Diagnostic {
+    reason: ^native_agreement_native_side_refused,
+    at: Textual { file: ^native_agreement_rejected_actual_test, extent: WholeFile },
+    correction: Unavailable { reason: AmbiguousIntent }
+  }
+}
+
+fn rejected_probe_receipt() -> FalsificationReceipt<String, RuntimeValue> {
+  FalsificationReceipt {
+    subject: "native_agreement_rejected_actual_probe",
+    expected: rejected_probe_value(),
+    actual: rejected_probe_value(),
+    divergence: ValueDiff { expected: rejected_probe_value(), actual: rejected_probe_value() },
+    evidence: EvidenceNone
+  }
+}
+
+fn rejected_actual_verdict(
+  falsification: Optional<FalsificationReceipt<String, RuntimeValue>>
+) -> Verdict<String, RuntimeValue> {
+  SemanticMismatch {
+    actual: Rejected { diagnostics: diagnostics_singleton(d: rejected_probe_diagnostic()) },
+    falsification: falsification
+  }
+}
+
+fn rejected_actual_divergence(
+  falsification: Optional<FalsificationReceipt<String, RuntimeValue>>
+) -> Optional<NativeAgreementDivergence> {
+  native_agreement_divergence_from_verdict(
+    member_id: "rejected_probe",
+    verdict: rejected_actual_verdict(falsification: falsification)
+  )
+}
+
+test fn rejected_native_side_is_named_and_the_interpreted_value_survives() -> Bool {
+  match rejected_actual_divergence(
+    falsification: Present { value: rejected_probe_receipt() }
+  ) {
+    Present { value: d } =>
+      d.member_id == "rejected_probe"
+        && d.native_value == "rejected"
+        && d.interpreted_value != "?"
+    Absent => false
+  }
+}
+
+// THE CONTROL THAT KEEPS THE ARM ABOVE HONEST: the same refused native side WITHOUT a
+// falsification receipt must keep answering "?" on both sides. Without this, an arm that
+// answered "rejected"/"?" for every `Rejected` would satisfy the assertion above while having
+// swallowed the neighbouring case.
+test fn rejected_without_a_receipt_still_reports_both_sides_unknown() -> Bool {
+  match rejected_actual_divergence(falsification: Absent) {
+    Present { value: d } =>
+      d.interpreted_value == "?" && d.native_value == "?"
+    Absent => false
+  }
+}