Carry explicit selection semantics through the kernel relation - #241
Merged
Conversation
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.
Boundary
This change crosses the transition-selection boundary between compiled domain programs and the generic kernel relation. A program declares, per transition, how the canonical relation may choose it — a selection rank and whether it competes for untargeted progress or waits for an explicit request. Until now that declaration existed only in the software-delivery catalog and was flattened into a single priority number on its way into the kernel, so the kernel could not represent explicit-only transitions and the shared conformance harness let backends exempt themselves from the law that proves it. Selection semantics are control law, so they must survive projection exactly and be enforced by the kernel, not reconstructed by each backend.
Transition
Before: every transition admitted by kernel.Runtime was marked selectable, so an explicit-only transition could be prescribed as untargeted progress; the software-delivery projection encoded selection rank as rank*1000+priority, collapsing two independent ordering dimensions into one; and a backend could declare a shared behavioral law unsupported, converting it into a passing skip — the explicit-only law was skipped for the kernel backend. After: every kernel transition must declare a positive selection rank and an explicit selection mode (implicit or explicit-only) or the program fails validation; untargeted resolution never prescribes an explicit-only transition while a targeted request still reaches it and applies normally; rank and priority order candidates independently with ties still producing a frontier; changing either field changes the program fingerprint, staling prior prescriptions before any effect; and the shared harness has no exemption path — all 18 shared laws execute for every registered backend.
Evidence
The full sharded Go suite passes (634 tests), including the shared behavioral laws run against both registered backends — kernel.Runtime on the extended integer fixture and the production software-delivery engine — with the explicit-only law passing verbosely on both and zero skips. A new harness integrity test proves the law list and runner table are a bijection so no future backend can narrow the shared contract. New kernel tests prove validation rejects a missing rank or selection mode and that the program fingerprint binds both fields. The race-enabled conformance suite, delivery, engine, flow, controlprogram (frontend-required), effects, and surfaces suites pass; go build and go vet are clean; the flow SDK tests and docs check pass. PR #239 and #240 regression contracts remain green.
Commits
Self-review attestation
f4ff1a7f1becf21742022c0c19114df6bd7366e23ca3397ff275d89bdb6d5c934b86b51d3cbdfab0ee628c47fe94d1d4f5767155