Repository navigation
Per-route effect receipt: a route disagreement classifies as a route disagreement, not a host defect - #12059
Merged
Conversation
…ectDisagreement, 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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A route disagreement on effect order is located at the routes, not the host
Closes the one open item from gunbc#12032, at the carrier home
gunbc.semantic_conformance.Defect.
DifferentialRecordcarried ONEeffect_receiptattributed to no route, andclassify_bound_recordread it before either route arm. When the interpreter and the emitted binary disagree on effect order, the verdict wasHostRealizationDefect, which names the host instead of the routes. Worse, for a subject whose authority is a value (every row today), a disagreement was not detected at all: the verdict wasConforms.Fix (carrier, not consumer).
DifferentialRecord.effect_receiptis deleted and replaced bynative_v2_effectsandv2_evaluator_effects. The old field had one consumer, the witness, which is migrated in the same change.RouteEffectDisagreement, which blocks cutover.route_effect_receipts_disagree: when both v2 routes ran, the two receipts are joined against each other at identity grain (operation + ordinal) using the existingeffect_receipts_agree. No expected order is consulted. The subject in the red expects a value.ExpectsEffectOrderis not populated anywhere new, so the split makes the observation attributable without deciding which order is correct (per Sibling-operand effect order: the absence is already declared, so acceptance refuses the programs that depend on it #12034). A route that was not run has recorded nothing, so its empty receipt is never compared.HostRealizationDefect) now reads the observed route's receipt. That check is reached only once the routes agree, so which route supplies the receipt cannot change the answer.Evidence by execution
Run with
gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/self_host_semantic_conformance_witness_test.dag --claim-run:two_routes_disagreeing_on_effect_ordinal_is_a_route_disagreement(red)routes_agreeing_on_effects_classify_by_value_unchanged(control)route_effect_receipts_disagreebranchThe control is shaped like the #12032 specimen: the routes agree on empty receipts and the native route is wrong on value, giving
NativeV2Defect. The control also checks an agreeing nonempty receipt pair, which givesConforms. #12032 itself is not on main. When it rebases it must renameeffect_receiptto the two per-route fields, and that is the entire migration.Frontier (not built)
This makes the route axis on
BehaviorSubjectIdentityconcrete: the receipt is now an observation of a route, as it already is inv2.compiler.effect_demand's key. The identity key itself is unchanged here.🤖 Generated with Claude Code