Carry explicit selection semantics through the kernel relation

.github/reviews/kernel-explicit-selection-semantics.receipt.json

@@ -0,0 +1,4 @@
+{
+  "reviewed_tree": "f4ff1a7f1becf21742022c0c19114df6bd7366e2",
+  "program_fingerprint": "3ca3397ff275d89bdb6d5c934b86b51d3cbdfab0ee628c47fe94d1d4f5767155"
+}

boatstack/cmd/boatstack-reviewer/program.go

@@ -66,6 +66,8 @@ func compileReviewProgram(policy Policy) (kernel.Program, error) {
 			RequiredCapabilities: []kernel.Capability{capabilitySubmit},
 			OwnedFacets:          []string{facetRound},
 			Operation:            transitionConverge,
+			SelectionRank:        1,
+			Selection:            kernel.SelectionImplicit,
 			Priority:             10,
 		},
 		{
@@ -77,6 +79,8 @@ func compileReviewProgram(policy Policy) (kernel.Program, error) {
 			RequiredCapabilities: []kernel.Capability{capabilitySubmit},
 			OwnedFacets:          []string{facetRound},
 			Operation:            transitionRecord,
+			SelectionRank:        1,
+			Selection:            kernel.SelectionImplicit,
 			Priority:             20,
 		},
 		{
@@ -88,6 +92,8 @@ func compileReviewProgram(policy Policy) (kernel.Program, error) {
 			RequiredCapabilities: []kernel.Capability{capabilitySubmit},
 			OwnedFacets:          []string{facetRound},
 			Operation:            transitionEscalate,
+			SelectionRank:        1,
+			Selection:            kernel.SelectionImplicit,
 			Priority:             30,
 		},
 		{
@@ -99,6 +105,8 @@ func compileReviewProgram(policy Policy) (kernel.Program, error) {
 			RequiredCapabilities: []kernel.Capability{capabilityHuman},
 			OwnedFacets:          []string{facetRound},
 			Operation:            transitionReopen,
+			SelectionRank:        1,
+			Selection:            kernel.SelectionImplicit,
 			Priority:             40,
 		},
 		{
@@ -110,6 +118,8 @@ func compileReviewProgram(policy Policy) (kernel.Program, error) {
 			RequiredCapabilities: []kernel.Capability{capabilityRecover},
 			OwnedFacets:          []string{facetRound},
 			Operation:            transitionRecover,
+			SelectionRank:        1,
+			Selection:            kernel.SelectionImplicit,
 			Priority:             5,
 			Recovers: []string{
 				transitionConverge,

boatstack/conformance/behavior/behavior.go

@@ -159,12 +159,6 @@ func Laws() []Law {
 // Every method operates through the backend's real production resolve and
 // apply path; adapters normalize evidence only at this boundary.
 type Backend interface {
-	// Unsupported reports why a law cannot be expressed through this
-	// backend's production path without changing production semantics. An
-	// empty string means the law runs. A non-empty reason is a recorded,
-	// precisely evidenced semantic mismatch, never a silent skip.
-	Unsupported(law Law) string
-
 	ResolveUntargeted(t testing.TB) Resolution
 	ResolveTargeted(t testing.TB, role TransitionRole) Resolution
 	Apply(t testing.TB, prescription Prescription) ApplyOutcome
@@ -183,8 +177,7 @@ type Backend interface {
 	// explicit-only transition is the only admissible candidate, so an
 	// implementation that ever promoted explicit-only transitions to
 	// implicit progress would be caught, not shadowed by a higher-ranked
-	// candidate. Backends that record LawExplicitOnly as unsupported never
-	// receive this call.
+	// candidate.
 	IsolateExplicitOnly(t testing.TB)
 
 	// Drift operators mutate the plant or control identity after a
@@ -211,10 +204,11 @@ type Backend interface {
 // Factory constructs one isolated backend per law.
 type Factory func(testing.TB) Backend
 
-// RunSharedLaws executes every shared law against the backend factory.
-func RunSharedLaws(t *testing.T, factory Factory) {
-	t.Helper()
-	runners := map[Law]func(*testing.T, Backend){
+// runners is the canonical one-to-one binding between shared laws and their
+// executable bodies. Every registered backend runs every runner; no backend
+// may exempt itself from a shared control law.
+func runners() map[Law]func(*testing.T, Backend) {
+	return map[Law]func(*testing.T, Backend){
 		LawSharedSelection:        lawSharedSelection,
 		LawExplicitOnly:           lawExplicitOnly,
 		LawAuthorityMissing:       lawAuthorityMissing,
@@ -234,14 +228,22 @@ func RunSharedLaws(t *testing.T, factory Factory) {
 		LawReachesTarget:          lawReachesTarget,
 		LawReadOnlyResolution:     lawReadOnlyResolution,
 	}
+}
+
+// RunSharedLaws executes every shared law against the backend factory. There
+// is deliberately no skip or exemption path: a backend that cannot express a
+// shared law fails it.
+func RunSharedLaws(t *testing.T, factory Factory) {
+	t.Helper()
+	bodies := runners()
 	for _, law := range Laws() {
 		law := law
+		body, ok := bodies[law]
+		if !ok {
+			t.Fatalf("shared law %q has no runner", law)
+		}
 		t.Run(string(law), func(t *testing.T) {
-			backend := factory(t)
-			if reason := backend.Unsupported(law); reason != "" {
-				t.Skipf("recorded semantic mismatch, not silent absence: %s", reason)
-			}
-			runners[law](t, backend)
+			body(t, factory(t))
 		})
 	}
 }

boatstack/conformance/behavior/integrity_test.go

@@ -0,0 +1,36 @@
+package behavior
+
+import "testing"
+
+// TestSharedLawRunnerIntegrity proves the harness cannot silently narrow the
+// shared contract: the canonical law list and the runner table are one
+// bijection, and RunSharedLaws executes exactly that list for every
+// registered backend with no skip or exemption path.
+func TestSharedLawRunnerIntegrity(t *testing.T) {
+	laws := Laws()
+	if len(laws) != 18 {
+		t.Fatalf("canonical shared law list has %d laws, want 18", len(laws))
+	}
+	seen := make(map[Law]bool, len(laws))
+	for _, law := range laws {
+		if seen[law] {
+			t.Fatalf("law %q is duplicated in the canonical list", law)
+		}
+		seen[law] = true
+	}
+	bodies := runners()
+	for _, law := range laws {
+		body, ok := bodies[law]
+		if !ok || body == nil {
+			t.Fatalf("law %q has no runner", law)
+		}
+	}
+	for law := range bodies {
+		if !seen[law] {
+			t.Fatalf("runner %q exists outside the canonical law list", law)
+		}
+	}
+	if len(bodies) != len(laws) {
+		t.Fatalf("runner table has %d entries, want exactly one per law (%d)", len(bodies), len(laws))
+	}
+}

boatstack/conformance/behavior/kernel_backend_test.go

@@ -76,17 +76,12 @@ func (b *kernelBackend) newRuntime(t testing.TB, program kernel.Program, classif
 	return runtime
 }
 
-func (b *kernelBackend) Unsupported(law behavior.Law) string {
-	if law == behavior.LawExplicitOnly {
-		return "kernel.Runtime cannot express an explicit-only transition: kernel.Transition declares no selection class and Runtime.resolve marks every admissible candidate selectable; explicit-only selection exists only at the kernel.Relate relation layer and in the software-delivery catalog"
-	}
-	return ""
-}
-
 func (b *kernelBackend) TransitionID(role behavior.TransitionRole) string {
 	switch role {
 	case behavior.RoleAdvance:
 		return b.fixture.Scenario.AdvanceTransitions[0]
+	case behavior.RoleExplicitOnly:
+		return b.fixture.Scenario.ExplicitOnlyTransition
 	case behavior.RoleRecovery:
 		return b.fixture.Scenario.RecoveryTransition
 	default:
@@ -252,10 +247,8 @@ func (b *kernelBackend) DriftObjectiveBinding(testing.TB) {
 	b.objective = b.fixture.Scenario.RevisedObjective
 }
 
-// IsolateExplicitOnly is unreachable: this backend records LawExplicitOnly
-// as an unsupported semantic mismatch, so the law body never runs here.
-func (b *kernelBackend) IsolateExplicitOnly(t testing.TB) {
-	t.Fatalf("kernel.Runtime cannot express an explicit-only transition; LawExplicitOnly is a recorded mismatch")
+func (b *kernelBackend) IsolateExplicitOnly(testing.TB) {
+	b.fixture.Scenario.IsolateExplicitOnly()
 }
 
 func (b *kernelBackend) RetargetInstance(testing.TB) {

boatstack/conformance/behavior/software_backend_test.go

@@ -481,7 +481,7 @@ func softwareRegistryVariant(t testing.TB, advanceEffect catalog.EffectID, advan
 			RequiredEvidence:     []string{"snapshot"}, OwnedResources: []string{"state"}, OwnedFacets: []model.StateFacet{model.StateFacetControl},
 			StateEffect: catalog.StateEffect{Kind: catalog.StateEffectAssignments, Assignments: []catalog.StateAssignment{{Facet: "phase", Value: &activePhase}}},
 			Effect:      effect, LocalEffects: []catalog.EffectID{effect}, Idempotent: true,
-			Prescription: catalog.Prescription{Operation: string(id), ExpectedPostcondition: "active"},
+			Prescription:    catalog.Prescription{Operation: string(id), ExpectedPostcondition: "active"},
 			SourcePredicate: "observed", AdmissionPredicate: "exact-admission", TargetPredicate: "active", Verifier: "fresh-active",
 			SourceConditions: []catalog.FacetCondition{{Facet: softwareStageFacet, Statuses: []model.FactStatus{model.FactKnown}, Values: sourceStages}},
 			TargetConditions: []catalog.FacetCondition{{Facet: softwareStageFacet, Statuses: []model.FactStatus{model.FactKnown}, Values: []string{"terminal"}}},
@@ -501,7 +501,7 @@ func softwareRegistryVariant(t testing.TB, advanceEffect catalog.EffectID, advan
 		RequiredEvidence:     []string{"snapshot"}, OwnedResources: []string{"state"}, OwnedFacets: []model.StateFacet{model.StateFacetControl},
 		StateEffect: catalog.StateEffect{Kind: catalog.StateEffectAssignments, Assignments: []catalog.StateAssignment{{Facet: "phase", Value: &frontierPhase}, {Facet: "recovery", Value: &escalatedRecovery}}},
 		Effect:      catalog.EffectID(softwareRecoverID), LocalEffects: []catalog.EffectID{catalog.EffectID(softwareRecoverID)}, Idempotent: true,
-		Prescription: catalog.Prescription{Operation: string(softwareRecoverID), ExpectedPostcondition: "frontier"},
+		Prescription:    catalog.Prescription{Operation: string(softwareRecoverID), ExpectedPostcondition: "frontier"},
 		SourcePredicate: "recovery", AdmissionPredicate: "exact-recovery-admission", TargetPredicate: "frontier", Verifier: "fresh-frontier",
 		SourceConditions: []catalog.FacetCondition{{Facet: model.FacetRecovery, Statuses: []model.FactStatus{model.FactKnown}, Values: []string{string(model.RecoveryReconcile)}}},
 		TargetConditions: []catalog.FacetCondition{{Facet: model.FacetRecovery, Statuses: []model.FactStatus{model.FactKnown}, Values: []string{string(model.RecoveryEscalated)}}},
@@ -574,8 +574,6 @@ func (b *softwareBackend) newEngine(t testing.TB, program protocol.ProgramIdenti
 	return built
 }
 
-func (b *softwareBackend) Unsupported(behavior.Law) string { return "" }
-
 func (b *softwareBackend) TransitionID(role behavior.TransitionRole) string {
 	switch role {
 	case behavior.RoleAdvance:

boatstack/delivery/control.go

@@ -610,11 +610,15 @@ func compileSupervisoryProgram(runtime ProgramRuntimeManifest, compatibility, do
 			capabilities = append(capabilities, general.Capability("objective.bind"))
 			facets = append(facets, "supervisor.objective")
 		}
+		selection := general.SelectionExplicitOnly
+		if transition.ImplicitlySelectable() {
+			selection = general.SelectionImplicit
+		}
 		projected = append(projected, general.Transition{
 			ID: string(transition.ID), SourceModes: []string{"software-delivery"}, TargetMode: "software-delivery",
 			ObjectiveScope: transition.Policy.ObjectiveScope, ObjectiveMutation: mutation,
 			RequiredCapabilities: capabilities, OwnedFacets: facets,
-			Operation: string(transition.ID), Priority: transition.SelectionClass.Rank()*1000 + transition.Priority,
+			Operation: string(transition.ID), SelectionRank: transition.SelectionClass.Rank(), Selection: selection, Priority: transition.Priority,
 			Recovers: recoveredBy[transition.ID],
 		})
 	}

boatstack/kernel/conformance/conformance.go

@@ -36,30 +36,32 @@ type Snapshot struct {
 // Scenario maps domain-specific fixture operations onto domain-neutral laws.
 // The suite never infers these roles from transition or operation names.
 type Scenario struct {
-	InstanceID            string
-	Objective             kernel.Objective
-	RevisedObjective      kernel.Objective
-	ConflictingObjective  kernel.Objective
-	AlternateProgram      kernel.Program
-	Authority             kernel.Authority
-	BindTransition        string
-	AdvanceTransitions    []string
-	MaintenanceTransition string
-	RecoveryTransition    string
-	RecoveryCapability    kernel.Capability
-	ExtraCapability       kernel.Capability
-	ChangeObservation     func()
-	RebindObjective       func(kernel.Objective)
-	BumpStateRevision     func()
-	RetargetProgram       func(kernel.ProgramIdentity)
-	AdvanceClock          func(time.Duration)
-	IndependentLocker     func() kernel.Locker
-	VerifyCommitted       func(Snapshot, Snapshot, kernel.Receipt) error
-	InterruptNextOperator func()
-	PanicNextOperator     func()
-	FailNextCommit        func()
-	RetargetInstance      func(string)
-	Snapshot              func() Snapshot
+	InstanceID             string
+	Objective              kernel.Objective
+	RevisedObjective       kernel.Objective
+	ConflictingObjective   kernel.Objective
+	AlternateProgram       kernel.Program
+	Authority              kernel.Authority
+	BindTransition         string
+	AdvanceTransitions     []string
+	MaintenanceTransition  string
+	ExplicitOnlyTransition string
+	IsolateExplicitOnly    func()
+	RecoveryTransition     string
+	RecoveryCapability     kernel.Capability
+	ExtraCapability        kernel.Capability
+	ChangeObservation      func()
+	RebindObjective        func(kernel.Objective)
+	BumpStateRevision      func()
+	RetargetProgram        func(kernel.ProgramIdentity)
+	AdvanceClock           func(time.Duration)
+	IndependentLocker      func() kernel.Locker
+	VerifyCommitted        func(Snapshot, Snapshot, kernel.Receipt) error
+	InterruptNextOperator  func()
+	PanicNextOperator      func()
+	FailNextCommit         func()
+	RetargetInstance       func(string)
+	Snapshot               func() Snapshot
 }
 
 // KernelConformance binds kernel ports to explicit scenario roles. New must
@@ -732,7 +734,7 @@ func (suite KernelConformance) fixture(t testing.TB, setup Setup) KernelConforma
 		t.Fatal("kernel conformance requires a fresh fixture factory")
 	}
 	fixture := suite.New(t, setup)
-	if fixture.Domain == nil || fixture.Operator == nil || fixture.CapabilityClassifier == nil || fixture.Store == nil || fixture.Locker == nil || fixture.Clock == nil || fixture.Scenario.Snapshot == nil || fixture.Scenario.ChangeObservation == nil || fixture.Scenario.RebindObjective == nil || fixture.Scenario.BumpStateRevision == nil || fixture.Scenario.RetargetProgram == nil || fixture.Scenario.AdvanceClock == nil || fixture.Scenario.IndependentLocker == nil || fixture.Scenario.VerifyCommitted == nil || fixture.Scenario.InterruptNextOperator == nil || fixture.Scenario.PanicNextOperator == nil || fixture.Scenario.FailNextCommit == nil || fixture.Scenario.RetargetInstance == nil || fixture.Scenario.InstanceID == "" || fixture.Scenario.BindTransition == "" || len(fixture.Scenario.AdvanceTransitions) == 0 || fixture.Scenario.MaintenanceTransition == "" || fixture.Scenario.RecoveryTransition == "" || fixture.Scenario.RecoveryCapability.Validate() != nil || fixture.Scenario.ExtraCapability.Validate() != nil {
+	if fixture.Domain == nil || fixture.Operator == nil || fixture.CapabilityClassifier == nil || fixture.Store == nil || fixture.Locker == nil || fixture.Clock == nil || fixture.Scenario.Snapshot == nil || fixture.Scenario.ChangeObservation == nil || fixture.Scenario.RebindObjective == nil || fixture.Scenario.BumpStateRevision == nil || fixture.Scenario.RetargetProgram == nil || fixture.Scenario.AdvanceClock == nil || fixture.Scenario.IndependentLocker == nil || fixture.Scenario.VerifyCommitted == nil || fixture.Scenario.InterruptNextOperator == nil || fixture.Scenario.PanicNextOperator == nil || fixture.Scenario.FailNextCommit == nil || fixture.Scenario.RetargetInstance == nil || fixture.Scenario.InstanceID == "" || fixture.Scenario.BindTransition == "" || len(fixture.Scenario.AdvanceTransitions) == 0 || fixture.Scenario.MaintenanceTransition == "" || fixture.Scenario.ExplicitOnlyTransition == "" || fixture.Scenario.IsolateExplicitOnly == nil || fixture.Scenario.RecoveryTransition == "" || fixture.Scenario.RecoveryCapability.Validate() != nil || fixture.Scenario.ExtraCapability.Validate() != nil {
 		t.Fatal("kernel conformance fixture is incomplete")
 	}
 	if fixture.Scenario.RevisedObjective.Validate() != nil || fixture.Scenario.RevisedObjective.ID != fixture.Scenario.Objective.ID || fixture.Scenario.RevisedObjective.Revision <= fixture.Scenario.Objective.Revision || fixture.Scenario.RevisedObjective.Fingerprint == fixture.Scenario.Objective.Fingerprint {

boatstack/kernel/conformance/conformance_test.go

@@ -349,7 +349,7 @@ func integerRecoveryCycleFixture() KernelConformance {
 		ID: "counter.recover-cycle", SourceModes: []string{"zero", "one", "two"}, TargetMode: "zero",
 		ObjectiveScope: kernel.ObjectiveOptionalPreserve, ObjectiveMutation: kernel.PreserveObjective,
 		RequiredCapabilities: []kernel.Capability{"counter.reset"}, OwnedFacets: []string{"counter.value"},
-		Operation: "counter.reset", Priority: 1, Recovers: []string{"counter.increment-first", "counter.increment-second", "counter.reset"},
+		Operation: "counter.reset", SelectionRank: 1, Selection: kernel.SelectionImplicit, Priority: 1, Recovers: []string{"counter.increment-first", "counter.increment-second", "counter.reset"},
 	})
 	program, err := kernel.CompileProgram(base.ID, base.Version, base.RuntimeCompatibility, base.InitialMode, base.MarkedModes, transitions)
 	if err != nil {