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 + ) + ) +}