From 525242ae7bb3ec196151753df04955c30b62d472 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 22 Sep 2026 10:39:19 +0000 Subject: [PATCH] Per-route effect receipt: a route disagreement classifies as RouteEffectDisagreement, not a host defect DifferentialRecord carried one effect_receipt attributed to no route, so the interpreter and the emitted binary disagreeing on effect order could only land on HostRealizationDefect. Each v2 route now carries its own receipt, and the two are joined against each other at identity grain (operation + ordinal) before any authority order is consulted -- no ExpectsEffectOrder is needed or populated. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/semantic_conformance.dag | 99 +++++++++++++------ ...host_semantic_conformance_witness_test.dag | 74 +++++++++++++- 2 files changed, 140 insertions(+), 33 deletions(-) diff --git a/dag/gunbc/semantic_conformance.dag b/dag/gunbc/semantic_conformance.dag index 9baca775d08..bd512d728f2 100644 --- a/dag/gunbc/semantic_conformance.dag +++ b/dag/gunbc/semantic_conformance.dag @@ -183,15 +183,21 @@ type SubjectAuthorityBinding = AuthorityBound { subject: BehaviorSubject } | AuthorityMissing { subject_id: BehaviorSubjectIdentity, area: CoverageArea } +// EACH ROUTE CARRIES ITS OWN EFFECT RECEIPT, because an ordered receipt is an observation OF A ROUTE +// and a receipt attributed to no route cannot say which realization produced it. With one shared +// receipt, the interpreter and the emitted binary disagreeing on effect order had nowhere to land but +// HostRealizationDefect -- an arm naming the host, not the routes that disagree. The split makes that +// observation attributable; it does not decide it: no expected order is consulted to detect it. type DifferentialRecord { binding: SubjectAuthorityBinding native_v2: ObservedResult + native_v2_effects: List v2_evaluator: ObservedResult + v2_evaluator_effects: List legacy_v1: LegacyObservation - effect_receipt: List } -// The nine total dispositions. Every arm names WHICH component is defective, because the remedies +// The ten total dispositions. Every arm names WHICH component is defective, because the remedies // are different and a disposition that collapses them is total at the level examined and blind one // level down. LegacyV1Defect is the arm that makes v1 a probe: v1 diverging from an authority the // v2 routes both satisfy is a fact about v1, and it does not block anything. @@ -200,6 +206,7 @@ type ConformanceDisposition | NativeV2Defect { detail: NonEmptyStr } | V2EvaluatorDefect { detail: NonEmptyStr } | HostRealizationDefect { detail: NonEmptyStr } + | RouteEffectDisagreement { detail: NonEmptyStr } | SemanticAuthorityMissing { subject_id: BehaviorSubjectIdentity } | SemanticAuthorityConflict { subject_id: BehaviorSubjectIdentity, detail: NonEmptyStr } | WitnessDefect { detail: NonEmptyStr } @@ -337,46 +344,52 @@ fn classify_bound_record( detail: "no v2 route was observed: the record carries no measurement of the subject under judgment" as NonEmptyStr } } else { - if !effect_receipt_matches_expected_order( - expected: subject.expected, - receipt: record.effect_receipt - ) { - HostRealizationDefect { - detail: "ordered effect receipt does not match the effect order the authority requires" as NonEmptyStr + if route_effect_receipts_disagree(record: record) { + RouteEffectDisagreement { + detail: "the native v2 route and the v2 evaluator recorded different ordered effect receipts" as NonEmptyStr } } else { - if !observed_was_run(observed: record.native_v2) { - Unclassified { - detail: "the native v2 route was not observed, so no statement about it is available" as NonEmptyStr + if !effect_receipt_matches_expected_order( + expected: subject.expected, + receipt: observed_route_effects(record: record) + ) { + HostRealizationDefect { + detail: "ordered effect receipt does not match the effect order the authority requires" as NonEmptyStr } } else { - if !observed_satisfies_expected( - expected: subject.expected, - observed: record.native_v2 - ) { - NativeV2Defect { - detail: "the native v2 result does not satisfy the subject's primary authority" as NonEmptyStr + if !observed_was_run(observed: record.native_v2) { + Unclassified { + detail: "the native v2 route was not observed, so no statement about it is available" as NonEmptyStr } } else { - if !evaluator_satisfies_or_is_excused(subject: subject, record: record) { - V2EvaluatorDefect { - detail: "the v2 evaluator result does not satisfy the subject's primary authority" as NonEmptyStr + if !observed_satisfies_expected( + expected: subject.expected, + observed: record.native_v2 + ) { + NativeV2Defect { + detail: "the native v2 result does not satisfy the subject's primary authority" as NonEmptyStr } } else { - if !evaluator_observation_is_sufficient(record: record, route: route) { - Unclassified { - detail: "the v2 evaluator was not observed while it is still on the promoted route" as NonEmptyStr + if !evaluator_satisfies_or_is_excused(subject: subject, record: record) { + V2EvaluatorDefect { + detail: "the v2 evaluator result does not satisfy the subject's primary authority" as NonEmptyStr } } else { - if legacy_diverges_from_authority( - expected: subject.expected, - legacy: record.legacy_v1 - ) { - LegacyV1Defect { - detail: "v1 diverges from the authority both v2 routes satisfy" as NonEmptyStr + if !evaluator_observation_is_sufficient(record: record, route: route) { + Unclassified { + detail: "the v2 evaluator was not observed while it is still on the promoted route" as NonEmptyStr } } else { - Conforms + if legacy_diverges_from_authority( + expected: subject.expected, + legacy: record.legacy_v1 + ) { + LegacyV1Defect { + detail: "v1 diverges from the authority both v2 routes satisfy" as NonEmptyStr + } + } else { + Conforms + } } } } @@ -386,6 +399,31 @@ fn classify_bound_record( } } +// ROUTES ARE JOINED AGAINST EACH OTHER, NOT AGAINST AN EXPECTED ORDER. When both v2 routes ran, a +// receipt pair that differs at identity grain (operation and ordinal) is a located disagreement +// between the routes whatever the authority says, and it is decidable without any authored order -- +// which is the point: no row in the corpus says which sibling-effect order is correct, and this arm +// must not need one. A route that was not run recorded nothing, so its empty receipt is not compared. +fn route_effect_receipts_disagree(record: DifferentialRecord) -> Bool { + observed_was_run(observed: record.native_v2) + && observed_was_run(observed: record.v2_evaluator) + && !effect_receipts_agree( + expected: record.native_v2_effects, + receipt: record.v2_evaluator_effects + ) +} + +// The receipt judged against the authority's order: the native route's when it was run, else the +// evaluator's. Only reached once the two routes' receipts agree (or only one route ran), so which +// route supplies it cannot change the answer. +fn observed_route_effects(record: DifferentialRecord) -> List { + if observed_was_run(observed: record.native_v2) { + record.native_v2_effects + } else { + record.v2_evaluator_effects + } +} + fn evaluator_observation_is_sufficient(record: DifferentialRecord, route: PromotedRoute) -> Bool { match route { EvaluatorOffPromotedRoute => true @@ -461,6 +499,7 @@ fn disposition_blocks_cutover( } NativeV2Defect { detail: _ } => true HostRealizationDefect { detail: _ } => true + RouteEffectDisagreement { detail: _ } => true SemanticAuthorityMissing { subject_id: _ } => true SemanticAuthorityConflict { subject_id: _, detail: _ } => true WitnessDefect { detail: _ } => true diff --git a/dag/test/claim/self_host_semantic_conformance_witness_test.dag b/dag/test/claim/self_host_semantic_conformance_witness_test.dag index 4dee68eab80..6e7cbdcc1a6 100644 --- a/dag/test/claim/self_host_semantic_conformance_witness_test.dag +++ b/dag/test/claim/self_host_semantic_conformance_witness_test.dag @@ -18,6 +18,7 @@ import gunbc.semantic_conformance { SubjectAuthorityBinding, AuthorityBound, AuthorityMissing, DifferentialRecord, ConformanceDisposition, Conforms, NativeV2Defect, V2EvaluatorDefect, HostRealizationDefect, + RouteEffectDisagreement, SemanticAuthorityMissing, WitnessDefect, LegacyV1Defect, ContractFacet, ValueResultFacet, RefusalBehaviorFacet, EffectOrderingFacet, BehaviorSubjectIdentity, @@ -91,9 +92,10 @@ fn record( DifferentialRecord { binding: AuthorityBound { subject: fixture_subject() }, native_v2: native, + native_v2_effects: [], v2_evaluator: evaluator, + v2_evaluator_effects: [], legacy_v1: legacy, - effect_receipt: [], } } @@ -266,9 +268,10 @@ test fn a_subject_with_no_primary_authority_is_authority_missing_and_blocks() -> area: CompilerClosureMechanism, }, native_v2: right(), + native_v2_effects: [], v2_evaluator: right(), + v2_evaluator_effects: [], legacy_v1: LegacyNotConsulted, - effect_receipt: [], }, route: EvaluatorOnPromotedRoute ) @@ -301,9 +304,10 @@ fn effect_record(receipt: List) -> DifferentialRecord { DifferentialRecord { binding: AuthorityBound { subject: ordered_effect_subject() }, native_v2: right(), + native_v2_effects: receipt, v2_evaluator: right(), + v2_evaluator_effects: receipt, legacy_v1: LegacyNotConsulted, - effect_receipt: receipt, } } @@ -663,3 +667,67 @@ test fn a_failed_open_omitted_arm_refuses_a_clean_gate() -> Bool { } } } + +fn is_route_effect_disagreement(d: ConformanceDisposition) -> Bool { + match d { + RouteEffectDisagreement { detail: _ } => true + _ => false + } +} + +fn two_route_effect_record( + native: ObservedResult, + native_effects: List, + evaluator_effects: List +) -> DifferentialRecord { + DifferentialRecord { + binding: AuthorityBound { subject: fixture_subject() }, + native_v2: native, + native_v2_effects: native_effects, + v2_evaluator: right(), + v2_evaluator_effects: evaluator_effects, + legacy_v1: LegacyNotConsulted, + } +} + +// THE SUBJECT EXPECTS A VALUE, NOT AN ORDER, deliberately. No row in the corpus says which +// sibling-effect order is correct, so the disagreement must be detectable without one: the two +// routes' receipts are joined against EACH OTHER at identity grain, ordinal included. Both routes +// produce the authority value, so a classifier that only compared a receipt against an expected order +// answers Conforms here -- the disagreement silently absorbed -- and one that read a single unrouted +// receipt answers HostRealizationDefect, naming the wrong subject. +test fn two_routes_disagreeing_on_effect_ordinal_is_a_route_disagreement() -> Bool { + is_route_effect_disagreement( + d: classify_differential_record( + record: two_route_effect_record( + native: right(), + native_effects: [effect(name: "open", ordinal: 0), effect(name: "write", ordinal: 1)], + evaluator_effects: [effect(name: "write", ordinal: 0), effect(name: "open", ordinal: 1)] + ), + route: EvaluatorOnPromotedRoute + ) + ) +} + +// THE CONTROL, shaped as the gunbc#12032 specimen: the routes agree on their (empty) effect receipts +// and disagree on value, native wrong against the law. It must classify NativeV2Defect before and +// after the split -- agreeing receipts contribute nothing to the verdict -- and an agreeing NONEMPTY +// pair must not trip the disagreement arm either. +test fn routes_agreeing_on_effects_classify_by_value_unchanged() -> Bool { + is_native_defect( + d: classify_differential_record( + record: two_route_effect_record(native: wrong(), native_effects: [], evaluator_effects: []), + route: EvaluatorOnPromotedRoute + ) + ) + && is_conforms( + d: classify_differential_record( + record: two_route_effect_record( + native: right(), + native_effects: [effect(name: "open", ordinal: 0), effect(name: "write", ordinal: 1)], + evaluator_effects: [effect(name: "open", ordinal: 0), effect(name: "write", ordinal: 1)] + ), + route: EvaluatorOnPromotedRoute + ) + ) +}