diff --git a/.github/reviews/behavioral-conformance-harness.receipt.json b/.github/reviews/behavioral-conformance-harness.receipt.json new file mode 100644 index 0000000..08d7424 --- /dev/null +++ b/.github/reviews/behavioral-conformance-harness.receipt.json @@ -0,0 +1,4 @@ +{ + "reviewed_tree": "c6774b140f7793d9a31cc0978d6cd90f583dc31f", + "program_fingerprint": "2277c979a06ee984c09aa32b2ed3d8886f1ae685a647274185a71a75a1a3961c" +} diff --git a/boatstack/conformance/behavior/behavior.go b/boatstack/conformance/behavior/behavior.go new file mode 100644 index 0000000..4e37393 --- /dev/null +++ b/boatstack/conformance/behavior/behavior.go @@ -0,0 +1,610 @@ +// Package behavior defines backend-neutral supervisory control laws. +// +// The laws are expressed once, against normalized behavioral observations, +// and run unchanged against every registered backend. A backend adapter owns +// the mechanics of its runtime (how state drifts, how failures are injected, +// how concurrency is raced) but never reinterprets a law: each law body in +// this package is the single semantic assertion for that law. +// +// This package intentionally imports no runtime. Adapters live with their +// runtimes and depend on this package, never the reverse. +package behavior + +import ( + "reflect" + "testing" +) + +// DecisionKind is the normalized resolution outcome shared by all backends. +type DecisionKind string + +const ( + // DecisionPrescribed means the backend selected exactly one transition + // and minted a prescription for it. + DecisionPrescribed DecisionKind = "prescribed" + // DecisionSatisfied means the control instance is at its marked or + // accepted target and no further progress is prescribed. + DecisionSatisfied DecisionKind = "satisfied" + // DecisionFrontier means candidates exist but required authority or + // capability evidence is missing. + DecisionFrontier DecisionKind = "frontier" + // DecisionRefused means the request was rejected outright. + DecisionRefused DecisionKind = "refused" + // DecisionBlocked means no candidate is admissible and explicit + // intervention is required. + DecisionBlocked DecisionKind = "blocked" + // DecisionUnresolved means the backend could not resolve a decision. + DecisionUnresolved DecisionKind = "unresolved" +) + +// TransitionRole names the fixture transitions every backend must map. +type TransitionRole string + +const ( + // RoleAdvance is the deterministic forward transition the untargeted + // relation selects from the fixture's initial state. + RoleAdvance TransitionRole = "advance" + // RoleExplicitOnly is a transition that must never be selected without + // an explicit request. + RoleExplicitOnly TransitionRole = "explicit-only" + // RoleRecovery is the transition that settles an open recovery + // obligation. + RoleRecovery TransitionRole = "recovery" +) + +// Prescription is a normalized, backend-opaque prescription reference. +type Prescription struct { + ID string + TransitionID string + // Handle carries the backend's exact production prescription and request + // context. Laws never inspect it. + Handle any +} + +// Resolution is the normalized outcome of one resolve call. +type Resolution struct { + Kind DecisionKind + TransitionID string + Prescription *Prescription + Reason string +} + +// FailureKind classifies why an apply did not commit. +type FailureKind string + +const ( + FailureNone FailureKind = "none" + FailureStale FailureKind = "stale" + FailureRecoveryRequired FailureKind = "recovery-required" + FailureRefused FailureKind = "refused" + FailureOther FailureKind = "other" +) + +// ApplyOutcome is the normalized result of one apply call. +type ApplyOutcome struct { + Committed bool + ReceiptID string + Failure FailureKind + Reason string +} + +// Observation is the normalized behavioral evidence a backend exposes. It is +// deterministic test evidence, never runtime state. +type Observation struct { + StateRevision uint64 + Mode string + ObservationFingerprint string + ObjectiveBound bool + ObjectiveIdentity string + RecoveryPending bool + // AdvanceEffectExecutions counts real executions of the advance effect. + AdvanceEffectExecutions int + CommittedFacts int + ReceiptIDs []string + AtTarget bool +} + +// Event is one normalized durability-ordering fact recorded by the backend's +// instrumented ports. +type Event string + +const ( + // EventAttemptDurable is recorded when the effect attempt becomes + // durable (journal begin / durable attempt state), before execution. + EventAttemptDurable Event = "attempt-durable" + // EventEffectExecuted is recorded when the effect actually executes. + EventEffectExecuted Event = "effect-executed" + // EventCommitted is recorded when the transition fact commits. + EventCommitted Event = "committed" +) + +// Law identifies one shared behavioral law. +type Law string + +const ( + LawSharedSelection Law = "targeted_and_untargeted_share_one_selection" + LawExplicitOnly Law = "explicit_only_never_becomes_implicit_progress" + LawAuthorityMissing Law = "missing_authority_fails_before_journal_or_effects" + LawStateRevisionDrift Law = "state_revision_drift_invalidates_before_effects" + LawProgramDrift Law = "program_drift_invalidates_before_effects" + LawObjectiveDrift Law = "objective_binding_drift_invalidates_before_effects" + LawObservationDrift Law = "observation_drift_invalidates_before_effects" + LawAuthorityExpiry Law = "authority_expiry_invalidates_before_effects" + LawCapabilityFloor Law = "declared_capabilities_cannot_weaken_trusted_minimum" + LawAttemptDurableFirst Law = "effect_attempt_durable_before_execution" + LawVerificationNoCommit Law = "verification_failure_cannot_commit" + LawCommitFailureRecovery Law = "commit_failure_requires_explicit_recovery" + LawRecoveryNoDuplicate Law = "recovery_cannot_duplicate_executed_effect" + LawNoCrossInstanceReplay Law = "prescription_cannot_replay_across_instances" + LawConcurrentSingleCommit Law = "concurrent_applies_commit_at_most_once" + LawStateReceiptConsistent Law = "state_advancement_and_committed_fact_remain_consistent" + LawReachesTarget Law = "valid_sequence_reaches_marked_target" + LawReadOnlyResolution Law = "readonly_resolution_and_tracing_do_not_mutate" +) + +// Laws lists every shared law in execution order. +func Laws() []Law { + return []Law{ + LawSharedSelection, LawExplicitOnly, LawAuthorityMissing, + LawStateRevisionDrift, LawProgramDrift, LawObjectiveDrift, + LawObservationDrift, LawAuthorityExpiry, LawCapabilityFloor, + LawAttemptDurableFirst, LawVerificationNoCommit, + LawCommitFailureRecovery, LawRecoveryNoDuplicate, + LawNoCrossInstanceReplay, LawConcurrentSingleCommit, + LawStateReceiptConsistent, LawReachesTarget, LawReadOnlyResolution, + } +} + +// Backend is the minimal operator surface a runtime adapter must expose. +// 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 + // ConcurrentApply races exactly two applications of one prescription + // from one base revision through the production apply path. + ConcurrentApply(t testing.TB, prescription Prescription) [2]ApplyOutcome + + Inspect(t testing.TB) Observation + Events() []Event + + // TransitionID reports the backend transition identity for a role so + // laws can compare selected transitions without raw runtime types. + TransitionID(role TransitionRole) string + + // IsolateExplicitOnly moves the plant to a state from which the + // 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. + IsolateExplicitOnly(t testing.TB) + + // Drift operators mutate the plant or control identity after a + // prescription has been minted. + DriftStateRevision(t testing.TB) + DriftObservation(t testing.TB) + DriftObjectiveBinding(t testing.TB) + RetargetInstance(t testing.TB) + ExpireAuthority(t testing.TB) + DropAuthority(t testing.TB) + // WithholdMinimumCapability keeps authority otherwise valid while + // removing the trusted minimum capability the backend's floor demands. + WithholdMinimumCapability(t testing.TB) + + // Failure injection at the backend's real boundaries. + FailNextVerification(t testing.TB) + FailNextCommit(t testing.TB) + + // ProgramDrifted returns a backend over the same plant whose program + // identity fingerprint differs from the one that minted prescriptions. + ProgramDrifted(t testing.TB) Backend +} + +// 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){ + LawSharedSelection: lawSharedSelection, + LawExplicitOnly: lawExplicitOnly, + LawAuthorityMissing: lawAuthorityMissing, + LawStateRevisionDrift: driftLaw(func(t testing.TB, b Backend) { b.DriftStateRevision(t) }, true), + LawProgramDrift: lawProgramDrift, + LawObjectiveDrift: driftLaw(func(t testing.TB, b Backend) { b.DriftObjectiveBinding(t) }, true), + LawObservationDrift: driftLaw(func(t testing.TB, b Backend) { b.DriftObservation(t) }, true), + LawAuthorityExpiry: driftLaw(func(t testing.TB, b Backend) { b.ExpireAuthority(t) }, false), + LawCapabilityFloor: lawCapabilityFloor, + LawAttemptDurableFirst: lawAttemptDurableFirst, + LawVerificationNoCommit: lawVerificationNoCommit, + LawCommitFailureRecovery: lawCommitFailureRecovery, + LawRecoveryNoDuplicate: lawRecoveryNoDuplicate, + LawNoCrossInstanceReplay: lawNoCrossInstanceReplay, + LawConcurrentSingleCommit: lawConcurrentSingleCommit, + LawStateReceiptConsistent: lawStateReceiptConsistent, + LawReachesTarget: lawReachesTarget, + LawReadOnlyResolution: lawReadOnlyResolution, + } + for _, law := range Laws() { + law := 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) + }) + } +} + +// lawSharedSelection: targeted and untargeted resolution derive one canonical +// selection with one prescription identity, and that prescription commits. +func lawSharedSelection(t *testing.T, b Backend) { + untargeted := b.ResolveUntargeted(t) + if untargeted.Kind != DecisionPrescribed || untargeted.Prescription == nil { + t.Fatalf("untargeted resolution did not prescribe: %+v", untargeted) + } + if untargeted.TransitionID != b.TransitionID(RoleAdvance) { + t.Fatalf("untargeted resolution selected %q, want advance %q", untargeted.TransitionID, b.TransitionID(RoleAdvance)) + } + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Kind != DecisionPrescribed || targeted.Prescription == nil { + t.Fatalf("targeted resolution did not prescribe: %+v", targeted) + } + if targeted.Prescription.ID != untargeted.Prescription.ID { + t.Fatalf("targeted prescription %q differs from untargeted %q: relation is not canonical", targeted.Prescription.ID, untargeted.Prescription.ID) + } + outcome := b.Apply(t, *targeted.Prescription) + if !outcome.Committed || outcome.ReceiptID == "" { + t.Fatalf("canonical prescription did not commit: %+v", outcome) + } +} + +// lawExplicitOnly: an explicit-only transition is never selected by +// untargeted resolution — even from a state where it is the only admissible +// candidate — yet an explicit request prescribes and commits it. The +// isolation step is what makes the forbidden direction falsifiable: with a +// higher-ranked sibling always admissible, an implementation that promoted +// explicit-only transitions to implicit progress would stay shadowed. +func lawExplicitOnly(t *testing.T, b Backend) { + untargeted := b.ResolveUntargeted(t) + if untargeted.Kind == DecisionPrescribed && untargeted.TransitionID == b.TransitionID(RoleExplicitOnly) { + t.Fatalf("untargeted resolution implicitly selected the explicit-only transition %q from a shared source state", untargeted.TransitionID) + } + b.IsolateExplicitOnly(t) + isolated := b.ResolveUntargeted(t) + if isolated.Kind == DecisionPrescribed { + t.Fatalf("untargeted resolution prescribed %q although the only admissible candidate is explicit-only", isolated.TransitionID) + } + explicit := b.ResolveTargeted(t, RoleExplicitOnly) + if explicit.Kind != DecisionPrescribed || explicit.Prescription == nil { + t.Fatalf("explicit request did not prescribe the explicit-only transition: %+v", explicit) + } + outcome := b.Apply(t, *explicit.Prescription) + if !outcome.Committed { + t.Fatalf("explicitly requested transition did not commit: %+v", outcome) + } +} + +// lawAuthorityMissing: with authority absent, resolution does not prescribe +// and a previously minted prescription fails before any journal or effect. +func lawAuthorityMissing(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + b.DropAuthority(t) + resolution := b.ResolveUntargeted(t) + if resolution.Kind == DecisionPrescribed { + t.Fatalf("resolution prescribed without authority: %+v", resolution) + } + before := b.Inspect(t) + outcome := b.Apply(t, *targeted.Prescription) + after := b.Inspect(t) + assertRefusedBeforeEffects(t, b, outcome, before, after, FailureNone) +} + +// driftLaw builds the shared drift-invalidation law body: a minted +// prescription must fail before effects once the named facet drifts. +func driftLaw(drift func(testing.TB, Backend), requireStale bool) func(*testing.T, Backend) { + return func(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + drift(t, b) + before := b.Inspect(t) + outcome := b.Apply(t, *targeted.Prescription) + after := b.Inspect(t) + want := FailureNone + if requireStale { + want = FailureStale + } + assertRefusedBeforeEffects(t, b, outcome, before, after, want) + } +} + +// lawProgramDrift: a prescription minted under one program identity fails +// before effects when applied under a drifted program identity. +func lawProgramDrift(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + drifted := b.ProgramDrifted(t) + before := b.Inspect(t) + outcome := drifted.Apply(t, *targeted.Prescription) + after := b.Inspect(t) + assertRefusedBeforeEffects(t, b, outcome, before, after, FailureNone) +} + +// lawCapabilityFloor: when the trusted minimum capability is withheld, the +// backend must not prescribe and nothing mutates. The semantic assertion is +// one: declared capabilities cannot weaken the kernel-owned minimum. The +// decision surface differs by backend mechanics — the kernel models the +// withheld floor as a capability frontier, while the software engine's +// capability projection denies at admission and surfaces a refusal — so the +// law accepts exactly that evidence-denial family and nothing else. +func lawCapabilityFloor(t *testing.T, b Backend) { + b.WithholdMinimumCapability(t) + before := b.Inspect(t) + resolution := b.ResolveTargeted(t, RoleAdvance) + after := b.Inspect(t) + if resolution.Kind != DecisionFrontier && resolution.Kind != DecisionRefused { + t.Fatalf("withheld trusted minimum capability produced %q, want frontier or refused", resolution.Kind) + } + if resolution.Prescription != nil { + t.Fatalf("capability-denied decision carried a prescription: %+v", resolution) + } + if !reflect.DeepEqual(before, after) { + t.Fatalf("capability-denied resolution mutated evidence: before=%+v after=%+v", before, after) + } +} + +// lawAttemptDurableFirst: the effect attempt becomes durable strictly before +// the effect executes, and the commit follows execution. +func lawAttemptDurableFirst(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + outcome := b.Apply(t, *targeted.Prescription) + if !outcome.Committed { + t.Fatalf("apply did not commit: %+v", outcome) + } + events := b.Events() + durable, executed, committed := eventIndex(events, EventAttemptDurable), eventIndex(events, EventEffectExecuted), eventIndex(events, EventCommitted) + if durable < 0 || executed < 0 || committed < 0 { + t.Fatalf("apply did not record durable/executed/committed events: %v", events) + } + if durable >= executed || executed >= committed { + t.Fatalf("effect attempt was not durable before execution and commit: %v", events) + } +} + +// lawVerificationNoCommit: a failed verification cannot produce a committed +// accepted fact or receipt. +func lawVerificationNoCommit(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + before := b.Inspect(t) + b.FailNextVerification(t) + outcome := b.Apply(t, *targeted.Prescription) + after := b.Inspect(t) + if outcome.Committed { + t.Fatalf("verification failure still committed: %+v", outcome) + } + if after.CommittedFacts != before.CommittedFacts || len(after.ReceiptIDs) != len(before.ReceiptIDs) { + t.Fatalf("verification failure changed committed facts: before=%+v after=%+v", before, after) + } + if eventIndex(b.Events(), EventCommitted) >= 0 { + t.Fatalf("verification failure recorded a commit event: %v", b.Events()) + } +} + +// lawCommitFailureRecovery: a commit failure after a verified effect yields +// an explicit recovery obligation and untargeted resolution selects recovery. +func lawCommitFailureRecovery(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + b.FailNextCommit(t) + outcome := b.Apply(t, *targeted.Prescription) + if outcome.Committed || outcome.Failure != FailureRecoveryRequired { + t.Fatalf("commit failure outcome is not an explicit recovery obligation: %+v", outcome) + } + observation := b.Inspect(t) + if !observation.RecoveryPending { + t.Fatalf("commit failure left no pending recovery obligation: %+v", observation) + } + resolution := b.ResolveUntargeted(t) + if resolution.Kind != DecisionPrescribed || resolution.TransitionID != b.TransitionID(RoleRecovery) { + t.Fatalf("untargeted resolution after commit failure selected %+v, want recovery %q", resolution, b.TransitionID(RoleRecovery)) + } +} + +// lawRecoveryNoDuplicate: neither retry nor recovery re-executes an already +// executed effect. +func lawRecoveryNoDuplicate(t *testing.T, b Backend) { + base := b.Inspect(t).AdvanceEffectExecutions + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + b.FailNextCommit(t) + if outcome := b.Apply(t, *targeted.Prescription); outcome.Committed { + t.Fatalf("setup: commit failure still committed: %+v", outcome) + } + interrupted := b.Inspect(t) + if interrupted.AdvanceEffectExecutions != base+1 { + t.Fatalf("setup: advance effect executed %d extra times, want 1", interrupted.AdvanceEffectExecutions-base) + } + retry := b.Apply(t, *targeted.Prescription) + if retry.Committed { + t.Fatalf("retry of the failed prescription committed: %+v", retry) + } + if executions := b.Inspect(t).AdvanceEffectExecutions; executions != base+1 { + t.Fatalf("retry duplicated the executed effect: %d extra executions", executions-base) + } + recovery := b.ResolveUntargeted(t) + if recovery.Kind != DecisionPrescribed || recovery.Prescription == nil || recovery.TransitionID != b.TransitionID(RoleRecovery) { + t.Fatalf("recovery was not prescribed after commit failure: %+v", recovery) + } + settled := b.Apply(t, *recovery.Prescription) + if !settled.Committed { + t.Fatalf("recovery transition did not commit: %+v", settled) + } + after := b.Inspect(t) + if after.AdvanceEffectExecutions != base+1 || after.RecoveryPending { + t.Fatalf("recovery duplicated the effect or left the obligation open: %+v", after) + } +} + +// lawNoCrossInstanceReplay: a prescription minted for one control instance +// fails before effects when replayed against another instance identity. +func lawNoCrossInstanceReplay(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + b.RetargetInstance(t) + before := b.Inspect(t) + outcome := b.Apply(t, *targeted.Prescription) + after := b.Inspect(t) + assertRefusedBeforeEffects(t, b, outcome, before, after, FailureStale) +} + +// lawConcurrentSingleCommit: two concurrent applications from one base +// revision commit at most one transition with exactly one effect execution. +func lawConcurrentSingleCommit(t *testing.T, b Backend) { + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + before := b.Inspect(t) + outcomes := b.ConcurrentApply(t, *targeted.Prescription) + commits := 0 + for _, outcome := range outcomes { + if outcome.Committed { + commits++ + } + } + after := b.Inspect(t) + if commits != 1 { + t.Fatalf("concurrent applications committed %d times, want exactly 1: %+v", commits, outcomes) + } + if after.CommittedFacts != before.CommittedFacts+1 || len(after.ReceiptIDs) != len(before.ReceiptIDs)+1 { + t.Fatalf("concurrent race changed committed evidence by more than one: before=%+v after=%+v", before, after) + } + if after.AdvanceEffectExecutions != before.AdvanceEffectExecutions+1 { + t.Fatalf("concurrent race executed the effect %d extra times, want 1", after.AdvanceEffectExecutions-before.AdvanceEffectExecutions) + } +} + +// lawStateReceiptConsistent: one committed transition advances state and +// commits exactly one fact and one receipt whose identity the apply returned. +func lawStateReceiptConsistent(t *testing.T, b Backend) { + before := b.Inspect(t) + targeted := b.ResolveTargeted(t, RoleAdvance) + if targeted.Prescription == nil { + t.Fatalf("setup: advance transition did not prescribe: %+v", targeted) + } + outcome := b.Apply(t, *targeted.Prescription) + if !outcome.Committed || outcome.ReceiptID == "" { + t.Fatalf("apply did not commit a receipted transition: %+v", outcome) + } + after := b.Inspect(t) + if after.CommittedFacts != before.CommittedFacts+1 || len(after.ReceiptIDs) != len(before.ReceiptIDs)+1 { + t.Fatalf("committed facts and receipts did not advance exactly once: before=%+v after=%+v", before, after) + } + if after.CommittedFacts != len(after.ReceiptIDs) { + t.Fatalf("committed fact count %d diverged from durable receipts %d", after.CommittedFacts, len(after.ReceiptIDs)) + } + if after.StateRevision <= before.StateRevision { + t.Fatalf("committed transition did not advance state revision: before=%d after=%d", before.StateRevision, after.StateRevision) + } + if latest := after.ReceiptIDs[len(after.ReceiptIDs)-1]; latest != outcome.ReceiptID { + t.Fatalf("returned receipt %q differs from durable receipt %q", outcome.ReceiptID, latest) + } +} + +// lawReachesTarget: repeated untargeted resolution and application reaches +// the marked or accepted target within a bounded number of transitions. +func lawReachesTarget(t *testing.T, b Backend) { + const maxTransitions = 4 + for step := 0; ; step++ { + resolution := b.ResolveUntargeted(t) + if resolution.Kind == DecisionSatisfied { + break + } + if resolution.Kind != DecisionPrescribed || resolution.Prescription == nil { + t.Fatalf("step %d: untargeted resolution returned %+v before target", step, resolution) + } + if step >= maxTransitions { + t.Fatalf("target not reached within %d transitions", maxTransitions) + } + if outcome := b.Apply(t, *resolution.Prescription); !outcome.Committed { + t.Fatalf("step %d: prescribed transition did not commit: %+v", step, outcome) + } + } + if observation := b.Inspect(t); !observation.AtTarget { + t.Fatalf("satisfied decision disagrees with target evidence: %+v", observation) + } +} + +// lawReadOnlyResolution: resolution and tracing never mutate state, effects, +// or committed history. +func lawReadOnlyResolution(t *testing.T, b Backend) { + before := b.Inspect(t) + b.ResolveUntargeted(t) + b.ResolveTargeted(t, RoleAdvance) + after := b.Inspect(t) + if !reflect.DeepEqual(before, after) { + t.Fatalf("read-only resolution mutated evidence: before=%+v after=%+v", before, after) + } + if events := b.Events(); len(events) != 0 { + t.Fatalf("read-only resolution recorded effect events: %v", events) + } +} + +// assertRefusedBeforeEffects is the shared post-condition for every +// invalidation law: no commit, no mutation, no effect, no durability event. +func assertRefusedBeforeEffects(t testing.TB, b Backend, outcome ApplyOutcome, before, after Observation, requiredFailure FailureKind) { + t.Helper() + if outcome.Committed { + t.Fatalf("apply committed despite invalidation: %+v", outcome) + } + if outcome.Failure == FailureNone { + t.Fatalf("apply reported no failure despite invalidation: %+v", outcome) + } + if requiredFailure != FailureNone && outcome.Failure != requiredFailure { + t.Fatalf("apply failure %q, want %q (%s)", outcome.Failure, requiredFailure, outcome.Reason) + } + if !reflect.DeepEqual(before, after) { + t.Fatalf("refused apply mutated evidence: before=%+v after=%+v", before, after) + } + if events := b.Events(); len(events) != 0 { + t.Fatalf("refused apply crossed the durability or effect boundary: %v", events) + } +} + +func eventIndex(events []Event, target Event) int { + for index, event := range events { + if event == target { + return index + } + } + return -1 +} diff --git a/boatstack/conformance/behavior/kernel_backend_test.go b/boatstack/conformance/behavior/kernel_backend_test.go new file mode 100644 index 0000000..07f2caf --- /dev/null +++ b/boatstack/conformance/behavior/kernel_backend_test.go @@ -0,0 +1,466 @@ +package behavior_test + +import ( + "context" + "fmt" + "strings" + "sync" + "testing" + "time" + + "github.com/operatorstack/boatstack/boatstack/conformance/behavior" + "github.com/operatorstack/boatstack/boatstack/kernel" + kernelconformance "github.com/operatorstack/boatstack/boatstack/kernel/conformance" +) + +// TestKernelRuntimeSharedBehavioralLaws runs the shared behavioral laws +// against the real kernel.Runtime over the deterministic integer fixture. +func TestKernelRuntimeSharedBehavioralLaws(t *testing.T) { + behavior.RunSharedLaws(t, newKernelBackend) +} + +// eventLog records normalized durability-ordering events for both adapters. +type eventLog struct { + mu sync.Mutex + events []behavior.Event +} + +func (l *eventLog) append(event behavior.Event) { + l.mu.Lock() + defer l.mu.Unlock() + l.events = append(l.events, event) +} + +func (l *eventLog) snapshot() []behavior.Event { + l.mu.Lock() + defer l.mu.Unlock() + return append([]behavior.Event(nil), l.events...) +} + +type kernelBackend struct { + fixture kernelconformance.KernelConformance + domain *kernelInstrumentedDomain + operator kernelInstrumentedOperator + store *kernelInstrumentedStore + runtime kernel.Runtime + events *eventLog + instanceID string + objective kernel.Objective + authority kernel.Authority +} + +func newKernelBackend(t testing.TB) behavior.Backend { + t.Helper() + fixture := kernelconformance.IntegerFixture().New(t, kernelconformance.SetupBound) + events := &eventLog{} + backend := &kernelBackend{ + fixture: fixture, + domain: &kernelInstrumentedDomain{Domain: fixture.Domain}, + store: &kernelInstrumentedStore{Store: fixture.Store, events: events}, + events: events, + instanceID: fixture.Scenario.InstanceID, + objective: fixture.Scenario.Objective, + authority: fixture.Scenario.Authority, + } + backend.operator = kernelInstrumentedOperator{Operator: fixture.Operator, events: events} + backend.runtime = backend.newRuntime(t, fixture.Program, fixture.CapabilityClassifier) + return backend +} + +func (b *kernelBackend) newRuntime(t testing.TB, program kernel.Program, classifier kernel.CapabilityClassifier) kernel.Runtime { + t.Helper() + runtime, err := kernel.NewRuntime(program, b.domain, b.operator, classifier, b.store, b.fixture.Locker, b.fixture.Clock) + if err != nil { + t.Fatalf("construct kernel runtime: %v", err) + } + 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.RoleRecovery: + return b.fixture.Scenario.RecoveryTransition + default: + return "" + } +} + +func (b *kernelBackend) resolve(t testing.TB, requested string) behavior.Resolution { + t.Helper() + request := kernel.ResolveRequest{InstanceID: b.instanceID, Objective: &b.objective, Authority: b.authority, Requested: requested, Trace: true} + resolution, err := b.runtime.Resolve(context.Background(), request) + if err != nil { + return behavior.Resolution{Kind: behavior.DecisionRefused, Reason: err.Error()} + } + normalized := behavior.Resolution{ + Kind: normalizeKernelDecision(resolution.Decision.Kind), + TransitionID: resolution.Decision.Transition, + Reason: resolution.Decision.Reason, + } + if resolution.Prescription != nil { + normalized.Prescription = &behavior.Prescription{ID: resolution.Prescription.ID, TransitionID: resolution.Prescription.TransitionID, Handle: *resolution.Prescription} + } + return normalized +} + +func normalizeKernelDecision(kind kernel.DecisionKind) behavior.DecisionKind { + switch kind { + case kernel.Prescribed: + return behavior.DecisionPrescribed + case kernel.Marked: + return behavior.DecisionSatisfied + case kernel.Frontier: + return behavior.DecisionFrontier + case kernel.Blocked: + return behavior.DecisionBlocked + case kernel.Refused: + return behavior.DecisionRefused + default: + return behavior.DecisionUnresolved + } +} + +func (b *kernelBackend) ResolveUntargeted(t testing.TB) behavior.Resolution { + return b.resolve(t, "") +} + +func (b *kernelBackend) ResolveTargeted(t testing.TB, role behavior.TransitionRole) behavior.Resolution { + return b.resolve(t, b.TransitionID(role)) +} + +func (b *kernelBackend) Apply(t testing.TB, prescription behavior.Prescription) behavior.ApplyOutcome { + t.Helper() + return b.applyThrough(t, b.runtime, prescription) +} + +func (b *kernelBackend) applyThrough(t testing.TB, runtime kernel.Runtime, prescription behavior.Prescription) behavior.ApplyOutcome { + t.Helper() + handle, ok := prescription.Handle.(kernel.Prescription) + if !ok { + t.Fatalf("prescription handle is not a kernel prescription: %T", prescription.Handle) + } + request := kernel.ResolveRequest{InstanceID: b.instanceID, Objective: &b.objective, Authority: b.authority, Requested: prescription.TransitionID} + receipt, err := runtime.Apply(context.Background(), kernel.ApplyRequest{ResolveRequest: request, Prescription: handle}) + return normalizeKernelApply(receipt, err) +} + +func normalizeKernelApply(receipt kernel.Receipt, err error) behavior.ApplyOutcome { + switch { + case err == nil: + return behavior.ApplyOutcome{Committed: true, ReceiptID: receipt.ID, Failure: behavior.FailureNone} + case kernel.IsStale(err): + return behavior.ApplyOutcome{Failure: behavior.FailureStale, Reason: err.Error()} + case kernel.IsRecoveryRequired(err): + return behavior.ApplyOutcome{Failure: behavior.FailureRecoveryRequired, Reason: err.Error()} + case strings.Contains(err.Error(), "apply refused"): + return behavior.ApplyOutcome{Failure: behavior.FailureRefused, Reason: err.Error()} + default: + return behavior.ApplyOutcome{Failure: behavior.FailureOther, Reason: err.Error()} + } +} + +func (b *kernelBackend) ConcurrentApply(t testing.TB, prescription behavior.Prescription) [2]behavior.ApplyOutcome { + t.Helper() + handle, ok := prescription.Handle.(kernel.Prescription) + if !ok { + t.Fatalf("prescription handle is not a kernel prescription: %T", prescription.Handle) + } + storeBarrier, domainBarrier := newTwoPartyBarrier(), newTwoPartyBarrier() + store := &sameBaseStore{Store: b.store, barrier: storeBarrier} + domain := &sameBaseDomain{Domain: b.domain, barrier: domainBarrier} + request := kernel.ResolveRequest{InstanceID: b.instanceID, Objective: &b.objective, Authority: b.authority, Requested: prescription.TransitionID} + runtimes := make([]kernel.Runtime, 0, 2) + for range 2 { + runtime, err := kernel.NewRuntime(b.fixture.Program, domain, b.operator, b.fixture.CapabilityClassifier, store, b.fixture.Scenario.IndependentLocker(), b.fixture.Clock) + if err != nil { + t.Fatalf("construct concurrent kernel runtime: %v", err) + } + runtimes = append(runtimes, runtime) + } + start := make(chan struct{}) + results := make(chan behavior.ApplyOutcome, 2) + for _, runtime := range runtimes { + runtime := runtime + go func() { + <-start + outcome := behavior.ApplyOutcome{Failure: behavior.FailureOther} + defer func() { + if recovered := recover(); recovered != nil { + storeBarrier.cancel() + domainBarrier.cancel() + outcome = behavior.ApplyOutcome{Failure: behavior.FailureOther, Reason: fmt.Sprintf("concurrent apply panicked: %v", recovered)} + } + results <- outcome + }() + receipt, err := runtime.Apply(context.Background(), kernel.ApplyRequest{ResolveRequest: request, Prescription: handle}) + if err != nil { + storeBarrier.cancel() + domainBarrier.cancel() + } + outcome = normalizeKernelApply(receipt, err) + }() + } + close(start) + var outcomes [2]behavior.ApplyOutcome + for index := range outcomes { + outcomes[index] = <-results + } + return outcomes +} + +func (b *kernelBackend) Inspect(t testing.TB) behavior.Observation { + t.Helper() + snapshot := b.fixture.Scenario.Snapshot() + receiptIDs := make([]string, 0, len(snapshot.Receipts)) + for _, receipt := range snapshot.Receipts { + receiptIDs = append(receiptIDs, receipt.ID) + } + observation := behavior.Observation{ + StateRevision: snapshot.State.Revision, + Mode: snapshot.State.Mode, + ObservationFingerprint: snapshot.Observation.Fingerprint, + ObjectiveBound: snapshot.State.ObjectiveBinding != nil, + RecoveryPending: snapshot.State.Recovery != nil, + AdvanceEffectExecutions: snapshot.Effects[b.TransitionID(behavior.RoleAdvance)], + CommittedFacts: snapshot.CommitCount, + ReceiptIDs: receiptIDs, + AtTarget: b.fixture.Program.Marked(snapshot.State.Mode), + } + if snapshot.State.ObjectiveBinding != nil { + observation.ObjectiveIdentity = snapshot.State.ObjectiveBinding.ObjectiveFingerprint + } + return observation +} + +func (b *kernelBackend) Events() []behavior.Event { return b.events.snapshot() } + +func (b *kernelBackend) DriftStateRevision(testing.TB) { b.fixture.Scenario.BumpStateRevision() } + +func (b *kernelBackend) DriftObservation(testing.TB) { b.fixture.Scenario.ChangeObservation() } + +func (b *kernelBackend) DriftObjectiveBinding(testing.TB) { + b.fixture.Scenario.RebindObjective(b.fixture.Scenario.RevisedObjective) + 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) RetargetInstance(testing.TB) { + other := b.instanceID + "-other" + b.fixture.Scenario.RetargetInstance(other) + b.instanceID = other +} + +func (b *kernelBackend) ExpireAuthority(testing.TB) { + // The fixture authority expires 24h after the fixed clock seed. + b.fixture.Scenario.AdvanceClock(25 * time.Hour) +} + +func (b *kernelBackend) DropAuthority(testing.TB) { b.authority = kernel.Authority{} } + +func (b *kernelBackend) WithholdMinimumCapability(t testing.TB) { + t.Helper() + classifier := kernelFloorClassifier{ + base: b.fixture.CapabilityClassifier, + transitionID: b.TransitionID(behavior.RoleAdvance), + capability: b.fixture.Scenario.ExtraCapability, + } + b.runtime = b.newRuntime(t, b.fixture.Program, classifier) + b.authority = kernelAuthorityWithout(b.authority, b.fixture.Scenario.ExtraCapability) +} + +func (b *kernelBackend) FailNextVerification(testing.TB) { b.domain.failNextVerification() } + +func (b *kernelBackend) FailNextCommit(testing.TB) { b.fixture.Scenario.FailNextCommit() } + +func (b *kernelBackend) ProgramDrifted(t testing.TB) behavior.Backend { + t.Helper() + drifted := *b + drifted.runtime = b.newRuntime(t, b.fixture.Scenario.AlternateProgram, b.fixture.CapabilityClassifier) + return &drifted +} + +// kernelInstrumentedStore records normalized durability events at the real +// kernel store boundary. +type kernelInstrumentedStore struct { + kernel.Store + events *eventLog +} + +func (s *kernelInstrumentedStore) BeginEffect(ctx context.Context, revision uint64, target kernel.ControlState) error { + if err := s.Store.BeginEffect(ctx, revision, target); err != nil { + return err + } + s.events.append(behavior.EventAttemptDurable) + return nil +} + +func (s *kernelInstrumentedStore) CommitTransition(ctx context.Context, revision uint64, target kernel.ControlState, receipt kernel.Receipt) error { + if err := s.Store.CommitTransition(ctx, revision, target, receipt); err != nil { + return err + } + s.events.append(behavior.EventCommitted) + return nil +} + +// kernelInstrumentedOperator records effect executions at the real operator +// boundary. +type kernelInstrumentedOperator struct { + kernel.Operator + events *eventLog +} + +func (o kernelInstrumentedOperator) Execute(ctx context.Context, operation kernel.Operation) (kernel.Effect, error) { + o.events.append(behavior.EventEffectExecuted) + return o.Operator.Execute(ctx, operation) +} + +// kernelInstrumentedDomain injects a one-shot verification failure at the +// real domain verification boundary. +type kernelInstrumentedDomain struct { + kernel.Domain + mu sync.Mutex + failVerify bool +} + +func (d *kernelInstrumentedDomain) failNextVerification() { + d.mu.Lock() + defer d.mu.Unlock() + d.failVerify = true +} + +func (d *kernelInstrumentedDomain) Verify(ctx context.Context, evaluation kernel.Evaluation, effect kernel.Effect, target kernel.Observation) error { + d.mu.Lock() + armed := d.failVerify + d.failVerify = false + d.mu.Unlock() + if armed { + return fmt.Errorf("injected verification failure") + } + return d.Domain.Verify(ctx, evaluation, effect, target) +} + +// kernelFloorClassifier strengthens the trusted capability floor for one +// transition, mirroring a trusted minimum the program cannot weaken. +type kernelFloorClassifier struct { + base kernel.CapabilityClassifier + transitionID string + capability kernel.Capability +} + +func (c kernelFloorClassifier) RequiredCapabilities(transition kernel.Transition) ([]kernel.Capability, error) { + required, err := c.base.RequiredCapabilities(transition) + if err != nil { + return nil, err + } + if transition.ID == c.transitionID { + required = append(required, c.capability) + } + return required, nil +} + +func kernelAuthorityWithout(authority kernel.Authority, removed kernel.Capability) kernel.Authority { + filtered := kernel.Authority{Receipts: make([]kernel.AuthorityReceipt, 0, len(authority.Receipts))} + for _, receipt := range authority.Receipts { + clone := receipt + clone.Capabilities = make([]kernel.Capability, 0, len(receipt.Capabilities)) + for _, capability := range receipt.Capabilities { + if capability != removed { + clone.Capabilities = append(clone.Capabilities, capability) + } + } + if len(clone.Capabilities) != 0 { + filtered.Receipts = append(filtered.Receipts, clone) + } + } + return filtered +} + +// twoPartyBarrier forces two concurrent applies to share one base revision. +type twoPartyBarrier struct { + mu sync.Mutex + arrivals int + ready chan struct{} + canceled chan struct{} + once sync.Once +} + +func newTwoPartyBarrier() *twoPartyBarrier { + return &twoPartyBarrier{ready: make(chan struct{}), canceled: make(chan struct{})} +} + +func (b *twoPartyBarrier) wait() error { + b.mu.Lock() + b.arrivals++ + if b.arrivals == 2 { + close(b.ready) + } + complete := b.arrivals >= 2 + b.mu.Unlock() + if complete { + return nil + } + select { + case <-b.ready: + return nil + case <-b.canceled: + b.mu.Lock() + complete = b.arrivals >= 2 + b.mu.Unlock() + if complete { + return nil + } + return fmt.Errorf("concurrent admission was canceled") + } +} + +func (b *twoPartyBarrier) cancel() { + b.once.Do(func() { close(b.canceled) }) +} + +type sameBaseStore struct { + kernel.Store + barrier *twoPartyBarrier +} + +func (s *sameBaseStore) Load(ctx context.Context, instanceID string) (kernel.ControlState, error) { + state, err := s.Store.Load(ctx, instanceID) + barrierErr := s.barrier.wait() + if err != nil { + return kernel.ControlState{}, err + } + if barrierErr != nil { + return kernel.ControlState{}, barrierErr + } + return state, nil +} + +type sameBaseDomain struct { + kernel.Domain + barrier *twoPartyBarrier +} + +func (d *sameBaseDomain) Observe(ctx context.Context, instanceID string) (kernel.Observation, error) { + observation, err := d.Domain.Observe(ctx, instanceID) + barrierErr := d.barrier.wait() + if err != nil { + return kernel.Observation{}, err + } + if barrierErr != nil { + return kernel.Observation{}, barrierErr + } + return observation, nil +} diff --git a/boatstack/conformance/behavior/software_backend_test.go b/boatstack/conformance/behavior/software_backend_test.go new file mode 100644 index 0000000..f9977f0 --- /dev/null +++ b/boatstack/conformance/behavior/software_backend_test.go @@ -0,0 +1,796 @@ +package behavior_test + +import ( + "context" + "errors" + "fmt" + "path/filepath" + "sync" + "testing" + "time" + + "github.com/operatorstack/boatstack/boatstack/conformance/behavior" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/catalog" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/engine" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/model" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/ports" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/protocol" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/supervisor" +) + +// TestSoftwareDeliveryEngineSharedBehavioralLaws runs the shared behavioral +// laws against the production software-delivery engine through its public +// Resolve/Apply boundary, over the smallest deterministic software fixture. +func TestSoftwareDeliveryEngineSharedBehavioralLaws(t *testing.T) { + behavior.RunSharedLaws(t, newSoftwareBackend) +} + +const ( + softwareProgramFingerprint = "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + driftedProgramFingerprint = "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc" + softwareStageFacet = model.FacetName("fixture.program.stage") + softwareNonceFacet = model.FacetName("fixture.program.nonce") + softwareAdvanceID = catalog.TransitionID("fixture.advance") + softwareExplicitID = catalog.TransitionID("fixture.explicit") + softwareRecoverID = catalog.TransitionID("fixture.recover") + // softwareExplicitGateStage is the plant stage from which the + // explicit-only transition is the only admissible candidate. + softwareExplicitGateStage = "explicit-gate" +) + +var softwareObservedAt = time.Date(2026, 8, 12, 10, 0, 0, 0, time.UTC) + +// softwarePlant is the deterministic in-memory plant the engine controls. The +// observer reads it and the effect driver mutates it; nothing else touches it. +type softwarePlant struct { + mu sync.Mutex + stage string + nonce string + revision uint64 + phase model.ProtocolPhase + recovery model.RecoveryState + transaction model.TransactionState + transactionID string + objectiveID string + repositoryID string + worktreeID string + executions map[catalog.TransitionID]int +} + +func newSoftwarePlant() *softwarePlant { + return &softwarePlant{ + stage: "start", nonce: "steady", revision: 1, + phase: model.PhaseObserved, recovery: model.RecoveryNone, transaction: model.TransactionNone, + objectiveID: "objective", repositoryID: "repo", worktreeID: "wt", + executions: map[catalog.TransitionID]int{}, + } +} + +func (p *softwarePlant) invocation() model.InvocationContext { + p.mu.Lock() + defer p.mu.Unlock() + return p.invocationLocked() +} + +func (p *softwarePlant) invocationLocked() model.InvocationContext { + return model.InvocationContext{ + RepositoryID: p.repositoryID, GitCommonID: "git", WorktreeID: p.worktreeID, Ref: "refs/heads/f", + ControllerID: "ctl", InvokingPath: softwareAbsolutePath("test-fixture", "repo"), + RuntimeVersion: "runtime-version", RuntimePath: softwareAbsolutePath("test-fixture", "runtime"), + RuntimeFingerprint: "runtime", Topology: model.TopologyEmbedded, Host: "cli", Correlation: "corr", + } +} + +func softwareAbsolutePath(parts ...string) string { + path, err := filepath.Abs(filepath.Join(parts...)) + if err != nil { + panic(err) + } + return path +} + +// observation projects the current plant into a valid domain observation. +func (p *softwarePlant) observation() model.Observation { + p.mu.Lock() + defer p.mu.Unlock() + evidence := model.Evidence{Source: "fixture", Fingerprint: "fixture-evidence", ObservedAt: softwareObservedAt} + configurationEvidence := model.Evidence{Source: "configuration:/repo/.boatstack/project.json", Fingerprint: "config-fingerprint", ObservedAt: softwareObservedAt} + observation := model.Observation{ + SchemaVersion: model.SnapshotSchemaVersion, StateRevision: p.revision, + Invocation: p.invocationLocked(), + Phase: model.Known(p.phase, evidence), Engagement: model.Known(model.EngagementActive, evidence), + Delivery: model.Known(model.DeliveryActive, evidence), Workspace: model.Known(model.WorkspaceActive, evidence), + Plan: model.Known(model.PlanApproved, evidence), Configuration: model.Known(model.ConfigurationVerified, configurationEvidence), + Runtime: model.Known(model.RuntimeVerified, evidence), + ConfigurationPolicy: model.Known(model.ConfigurationPolicy{ + PlanApproval: "human", VisualEvidence: "optional", ExternalEffectAuthority: "human-or-autonomy-plus-provider", Hosts: []string{"cli"}, + }, configurationEvidence), + Publication: model.Known(model.PublicationNone, evidence), Verification: model.Known(model.VerificationUnverified, evidence), + Recovery: model.Known(p.recovery, evidence), Transaction: model.Known(p.transaction, evidence), + RecoveryInfo: model.Absent[model.RecoveryContext]("none", evidence), + TransactionInfo: model.Absent[model.TransactionContext]("none", evidence), + Terminal: model.Known(model.TerminalNonterminal, evidence), + Objective: model.Known(model.Objective{ID: p.objectiveID, TargetID: model.ObjectiveVerified, DeliveryID: "delivery"}, evidence), + ObservedAt: softwareObservedAt, + ProgramFacts: map[string]model.Fact[string]{ + string(softwareStageFacet): model.Known(p.stage, evidence), + string(softwareNonceFacet): model.Known(p.nonce, evidence), + }, + } + if p.phase == model.PhaseRecovery { + observation.Terminal = model.Known(model.TerminalStale, evidence) + } + if p.recovery != model.RecoveryNone { + observation.RecoveryInfo = model.Known(model.RecoveryContext{ + TransactionID: p.transactionID, Cause: "transition fact commit interrupted", SourcePhase: model.PhaseObserved, + Permitted: []string{string(softwareRecoverID)}, BudgetRemaining: 1, Resumption: model.PhaseObserved, + }, evidence) + } + if p.transaction != model.TransactionNone { + observation.TransactionInfo = model.Known(model.TransactionContext{ + ID: p.transactionID, TransitionID: string(softwareAdvanceID), Status: "recovery-required", + }, evidence) + } + return observation +} + +func (p *softwarePlant) enterRecovery(transactionID string) { + p.mu.Lock() + defer p.mu.Unlock() + p.phase, p.recovery, p.transaction, p.transactionID = model.PhaseRecovery, model.RecoveryReconcile, model.TransactionLocalApplied, transactionID +} + +// observerGate lets ConcurrentApply force both racing applies to observe the +// same base snapshot before either proceeds toward the effect lock. Disarmed, +// it is a pass-through; armed, the first two observations rendezvous and +// every later observation passes straight through (the barrier is one-shot). +type observerGate struct { + mu sync.Mutex + barrier *twoPartyBarrier +} + +func (g *observerGate) arm(barrier *twoPartyBarrier) { + g.mu.Lock() + g.barrier = barrier + g.mu.Unlock() +} + +func (g *observerGate) wait() error { + g.mu.Lock() + barrier := g.barrier + g.mu.Unlock() + if barrier == nil { + return nil + } + return barrier.wait() +} + +// softwareObserver reads the plant through the engine's observer port. +type softwareObserver struct { + plant *softwarePlant + gate *observerGate +} + +func (o softwareObserver) Observe(context.Context, ports.ObservationRequest) (model.Observation, error) { + observation := o.plant.observation() + if err := o.gate.wait(); err != nil { + return model.Observation{}, err + } + return observation, nil +} + +// softwareClock is a mutable deterministic clock. +type softwareClock struct { + mu sync.Mutex + now time.Time +} + +func (c *softwareClock) Now() time.Time { + c.mu.Lock() + defer c.mu.Unlock() + return c.now +} + +func (c *softwareClock) advance(duration time.Duration) { + c.mu.Lock() + defer c.mu.Unlock() + c.now = c.now.Add(duration) +} + +// softwareLocker serializes the effect region with a real mutex. +type softwareLocker struct{ mu sync.Mutex } + +func (l *softwareLocker) Acquire(context.Context, model.InvocationContext, []string) (ports.Lock, error) { + l.mu.Lock() + return softwareLock{mu: &l.mu}, nil +} + +type softwareLock struct{ mu *sync.Mutex } + +func (l softwareLock) Release() error { + l.mu.Unlock() + return nil +} + +// softwareJournal is the transaction boundary: it records durability events, +// injects one-shot commit failures, and projects recovery obligations into +// the plant exactly as the production journal projects them into state. +type softwareJournal struct { + mu sync.Mutex + plant *softwarePlant + events *eventLog + committed int + recoveryMarks int + commitErr error +} + +func (j *softwareJournal) Begin(context.Context, protocol.Admission, catalog.Transition) error { + j.events.append(behavior.EventAttemptDurable) + return nil +} + +func (j *softwareJournal) Stage(context.Context, string, []ports.ResourceMutation) error { return nil } + +func (j *softwareJournal) Mark(context.Context, string, string) error { return nil } + +func (j *softwareJournal) Commit(context.Context, protocol.TransitionReceipt) error { + j.mu.Lock() + defer j.mu.Unlock() + if j.commitErr != nil { + err := j.commitErr + j.commitErr = nil + return err + } + j.committed++ + j.events.append(behavior.EventCommitted) + return nil +} + +func (j *softwareJournal) Abort(context.Context, string, string) error { return nil } + +func (j *softwareJournal) RequireRecovery(_ context.Context, admissionID string, _ string) error { + j.mu.Lock() + j.recoveryMarks++ + j.mu.Unlock() + j.plant.enterRecovery(admissionID) + return nil +} + +func (j *softwareJournal) failNextCommit() { + j.mu.Lock() + defer j.mu.Unlock() + j.commitErr = errors.New("injected transition fact commit failure") +} + +func (j *softwareJournal) snapshot() (int, int) { + j.mu.Lock() + defer j.mu.Unlock() + return j.committed, j.recoveryMarks +} + +// softwareEffects drives real plant mutations through the effect port. +type softwareEffects struct { + mu sync.Mutex + plant *softwarePlant + events *eventLog + failNextVerification bool +} + +func (e *softwareEffects) Prepare(_ context.Context, _ protocol.Admission, transition catalog.Transition) (ports.PreparedEffect, error) { + return &softwarePreparedEffect{driver: e, transition: transition}, nil +} + +func (e *softwareEffects) consumeVerificationFailure() bool { + e.mu.Lock() + defer e.mu.Unlock() + armed := e.failNextVerification + e.failNextVerification = false + return armed +} + +func (e *softwareEffects) armVerificationFailure() { + e.mu.Lock() + defer e.mu.Unlock() + e.failNextVerification = true +} + +// softwarePlantState is the rollback capture of the mutable plant facets. +type softwarePlantState struct { + stage string + nonce string + revision uint64 + phase model.ProtocolPhase + recovery model.RecoveryState + transaction model.TransactionState +} + +type softwarePreparedEffect struct { + driver *softwareEffects + transition catalog.Transition + prior *softwarePlantState +} + +func (p *softwarePreparedEffect) Manifest() []ports.ResourceMutation { return nil } + +func (p *softwarePreparedEffect) ChangedStateFacets() []model.StateFacet { + return []model.StateFacet{model.StateFacetControl} +} + +func (p *softwarePreparedEffect) CommittedEffects() []protocol.EffectFact { + resource := "state" + if len(p.transition.OwnedResources) != 0 { + resource = p.transition.OwnedResources[0] + } + return []protocol.EffectFact{{ + Kind: protocol.EffectResourceMutation, EffectID: p.transition.Effect, Owner: p.transition.Owner, Resource: resource, + Target: "/test/state.json", Operation: "update", + PriorFingerprint: "1111111111111111111111111111111111111111111111111111111111111111", + ResultingFingerprint: "2222222222222222222222222222222222222222222222222222222222222222", + }} +} + +func (p *softwarePreparedEffect) VerificationInvocation() (model.InvocationContext, bool) { + return model.InvocationContext{}, false +} + +func (p *softwarePreparedEffect) Execute(context.Context) (ports.EffectResult, error) { + plant := p.driver.plant + plant.mu.Lock() + p.prior = &softwarePlantState{ + stage: plant.stage, nonce: plant.nonce, revision: plant.revision, + phase: plant.phase, recovery: plant.recovery, transaction: plant.transaction, + } + switch p.transition.ID { + case softwareAdvanceID: + plant.stage = "terminal" + if p.driver.consumeVerificationFailureLocked(plant) { + plant.stage = "botched" + } + plant.phase = model.PhaseActive + plant.revision++ + case softwareExplicitID: + plant.stage, plant.phase = "terminal", model.PhaseActive + plant.revision++ + case softwareRecoverID: + plant.recovery, plant.phase, plant.transaction = model.RecoveryEscalated, model.PhaseFrontier, model.TransactionNone + plant.revision++ + } + plant.executions[p.transition.ID]++ + plant.mu.Unlock() + p.driver.events.append(behavior.EventEffectExecuted) + return ports.EffectResult{Settlement: ports.EffectSettled}, nil +} + +// consumeVerificationFailureLocked exists because Execute already holds the +// plant lock; the armed flag lives on the driver, not the plant. +func (e *softwareEffects) consumeVerificationFailureLocked(*softwarePlant) bool { + return e.consumeVerificationFailure() +} + +func (p *softwarePreparedEffect) Rollback(context.Context) error { + if p.prior == nil { + return fmt.Errorf("rollback without an executed effect") + } + plant := p.driver.plant + plant.mu.Lock() + plant.stage, plant.nonce, plant.revision = p.prior.stage, p.prior.nonce, p.prior.revision + plant.phase, plant.recovery, plant.transaction = p.prior.phase, p.prior.recovery, p.prior.transaction + plant.mu.Unlock() + return nil +} + +// softwareReceipts is the in-memory receipt projection store. +type softwareReceipts struct { + mu sync.Mutex + next uint64 + values []protocol.TransitionReceipt +} + +func (s *softwareReceipts) Bind(context.Context, string, protocol.Admission) error { return nil } + +func (s *softwareReceipts) Unbind(string) {} + +func (s *softwareReceipts) NextSequence(context.Context, string) (uint64, error) { + s.mu.Lock() + defer s.mu.Unlock() + s.next++ + return s.next, nil +} + +func (s *softwareReceipts) FindByIdempotency(_ context.Context, _ model.InvocationContext, key string) (protocol.TransitionReceipt, bool, error) { + s.mu.Lock() + defer s.mu.Unlock() + for _, receipt := range s.values { + if receipt.IdempotencyKey == key { + return receipt, true, nil + } + } + return protocol.TransitionReceipt{}, false, nil +} + +func (s *softwareReceipts) Project(_ context.Context, receipt protocol.TransitionReceipt) error { + s.mu.Lock() + defer s.mu.Unlock() + s.values = append(s.values, receipt) + return nil +} + +func (s *softwareReceipts) ids() []string { + s.mu.Lock() + defer s.mu.Unlock() + ids := make([]string, 0, len(s.values)) + for _, receipt := range s.values { + ids = append(ids, receipt.ID) + } + return ids +} + +func softwareObjectiveContracts(t testing.TB) catalog.ObjectiveContracts { + t.Helper() + contracts, err := catalog.NewObjectiveContracts([]catalog.ObjectiveContract{{ + TargetID: model.ObjectiveVerified, + Conditions: []catalog.FacetCondition{ + {Facet: softwareStageFacet, Statuses: []model.FactStatus{model.FactKnown}, Values: []string{"terminal"}}, + {Facet: model.FacetRecovery, Statuses: []model.FactStatus{model.FactKnown}, Values: []string{string(model.RecoveryNone)}}, + }, + }}, nil) + if err != nil { + t.Fatal(err) + } + return contracts +} + +func softwareRegistry(t testing.TB) catalog.Registry { + t.Helper() + return softwareRegistryVariant(t, catalog.EffectID(softwareAdvanceID), nil) +} + +// softwareCapabilityFloorRegistry compiles the advance transition to the +// publication.execute effect. The kernel-owned effect classification +// (catalog.KernelEffectCapabilities) then demands publication.publish — a +// capability no repository-class authority grants — while the transition's +// declared authority class stays satisfied. Resolving advance must therefore +// be denied by the production capability floor itself, not by the +// authority-class relation gate. +func softwareCapabilityFloorRegistry(t testing.TB) catalog.Registry { + t.Helper() + return softwareRegistryVariant(t, "publication.execute", []catalog.Capability{catalog.CapabilityPublicationPublish}) +} + +func softwareRegistryVariant(t testing.TB, advanceEffect catalog.EffectID, advanceExtraDeclared []catalog.Capability) catalog.Registry { + t.Helper() + identity := []string{"repository-id", "git-common-id", "worktree-id"} + interruption := catalog.InterruptionContract{ + Points: []string{"after-effect"}, PartialState: []string{"effect-possibly-installed"}, Detection: "test-observation", + ResumeContract: "test-resume", RollbackContract: "test-rollback", CompensationContract: "not-required", + Recovery: softwareRecoverID, RecoveryAuthority: "test-authority", ResumptionPredicate: "test-resumption", + } + activePhase := string(model.PhaseActive) + frontierPhase := string(model.PhaseFrontier) + escalatedRecovery := string(model.RecoveryEscalated) + forward := func(id catalog.TransitionID, selection catalog.SelectionClass, priority int, sourceStages []string, effect catalog.EffectID, extraDeclared []catalog.Capability) catalog.Transition { + declared := append([]catalog.Capability{catalog.CapabilityRepositoryWrite, catalog.CapabilityCommandExecute}, extraDeclared...) + return catalog.Transition{ + ID: id, Version: 1, Class: catalog.EventOwnedLocal, + Origin: catalog.TransitionOrigin{Kind: catalog.OriginControlProgram, ID: "fixture.program", Version: "1.0.0", ManifestFingerprint: softwareProgramFingerprint}, + Owner: "fixture.program", SelectionClass: selection, + SourcePhases: []model.ProtocolPhase{model.PhaseObserved}, TargetPhases: []model.ProtocolPhase{model.PhaseActive}, + RequiredIdentity: identity, Authority: []catalog.AuthorityClass{catalog.AuthorityRepository}, + RequiredCapabilities: []catalog.Capability{catalog.CapabilityRepositoryWrite}, + DeclaredCapabilities: declared, + 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"}, + 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"}}}, + Interruption: interruption, Reversibility: catalog.Reversible, TerminalEffect: "none", + PrivacyClassification: "metadata-only", TelemetryClassification: "transition-receipt", CostClass: "test", + Policy: catalog.PolicyContract{ObjectiveScope: catalog.ObjectiveScopeBoundExact}, Priority: priority, + } + } + recover := catalog.Transition{ + ID: softwareRecoverID, Version: 1, Class: catalog.EventRecovery, + Origin: catalog.TransitionOrigin{Kind: catalog.OriginControlProgram, ID: "fixture.program", Version: "1.0.0", ManifestFingerprint: softwareProgramFingerprint}, + Owner: "fixture.program", SelectionClass: catalog.SelectionProgramRecovery, + SourcePhases: []model.ProtocolPhase{model.PhaseRecovery}, TargetPhases: []model.ProtocolPhase{model.PhaseFrontier}, + RequiredIdentity: identity, Authority: []catalog.AuthorityClass{catalog.AuthorityRepository}, + RequiredCapabilities: []catalog.Capability{catalog.CapabilityRepositoryWrite}, + DeclaredCapabilities: []catalog.Capability{catalog.CapabilityRepositoryWrite, catalog.CapabilityCommandExecute}, + 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"}, + 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)}}}, + Interruption: interruption, Reversibility: catalog.Reversible, TerminalEffect: "none", + PrivacyClassification: "metadata-only", TelemetryClassification: "transition-receipt", CostClass: "test", + Policy: catalog.PolicyContract{ObjectiveScope: catalog.ObjectiveScopeBoundExact}, Priority: 2, + } + registry, err := catalog.New([]catalog.Transition{ + forward(softwareAdvanceID, catalog.SelectionProgramProgress, 1, []string{"start"}, advanceEffect, advanceExtraDeclared), + // The explicit-only transition is admissible both from the shared + // start stage (where a program-progress sibling shadows it) and from + // the isolation stage where it is the only admissible candidate. + forward(softwareExplicitID, catalog.SelectionExplicitOnly, 1, []string{"start", softwareExplicitGateStage}, catalog.EffectID(softwareExplicitID), nil), + recover, + }) + if err != nil { + t.Fatal(err) + } + return registry +} + +type softwareBackend struct { + plant *softwarePlant + events *eventLog + journal *softwareJournal + effects *softwareEffects + receipts *softwareReceipts + clock *softwareClock + observerGate *observerGate + registry catalog.Registry + contracts catalog.ObjectiveContracts + program protocol.ProgramIdentity + engine engine.Engine + authority protocol.AuthorityBundle + objective model.Objective +} + +func newSoftwareBackend(t testing.TB) behavior.Backend { + t.Helper() + plant := newSoftwarePlant() + events := &eventLog{} + clock := &softwareClock{now: softwareObservedAt} + backend := &softwareBackend{ + plant: plant, + events: events, + journal: &softwareJournal{plant: plant, events: events}, + effects: &softwareEffects{plant: plant, events: events}, + receipts: &softwareReceipts{}, + clock: clock, + observerGate: &observerGate{}, + registry: softwareRegistry(t), + contracts: softwareObjectiveContracts(t), + program: protocol.ProgramIdentity{ID: "fixture.program", Version: "1.0.0", Fingerprint: softwareProgramFingerprint}, + objective: model.Objective{ID: "objective", TargetID: model.ObjectiveVerified, DeliveryID: "delivery"}, + } + backend.authority = protocol.AuthorityBundle{Receipts: []protocol.AuthorityReceipt{{ + ID: "repository", Class: catalog.AuthorityRepository, Subject: "repo", Fingerprint: "config-fingerprint", + IssuedAt: clock.Now().Add(-time.Minute), ExpiresAt: clock.Now().Add(time.Hour), + }}} + backend.engine = backend.newEngine(t, backend.program) + return backend +} + +func (b *softwareBackend) newEngine(t testing.TB, program protocol.ProgramIdentity) engine.Engine { + t.Helper() + built, err := engine.New(b.registry, b.contracts, program, softwareObserver{plant: b.plant, gate: b.observerGate}, b.clock, &softwareLocker{}, b.journal, b.effects, b.receipts) + if err != nil { + t.Fatalf("construct software-delivery engine: %v", err) + } + return built +} + +func (b *softwareBackend) Unsupported(behavior.Law) string { return "" } + +func (b *softwareBackend) TransitionID(role behavior.TransitionRole) string { + switch role { + case behavior.RoleAdvance: + return string(softwareAdvanceID) + case behavior.RoleExplicitOnly: + return string(softwareExplicitID) + case behavior.RoleRecovery: + return string(softwareRecoverID) + default: + return "" + } +} + +func (b *softwareBackend) resolveRequest(requested catalog.TransitionID) engine.ResolveRequest { + return engine.ResolveRequest{ + Invocation: b.plant.invocation(), Objective: b.objective, Authority: b.authority, + Requested: requested, Trace: true, + } +} + +func (b *softwareBackend) resolve(t testing.TB, requested catalog.TransitionID) behavior.Resolution { + t.Helper() + resolution, err := b.engine.Resolve(context.Background(), b.resolveRequest(requested)) + if err != nil { + return behavior.Resolution{Kind: behavior.DecisionRefused, Reason: err.Error()} + } + normalized := behavior.Resolution{Kind: normalizeSoftwareDecision(resolution.Decision.Kind), Reason: resolution.Decision.Reason} + if resolution.Decision.Transition != nil { + normalized.TransitionID = string(resolution.Decision.Transition.ID) + } + if normalized.Kind == behavior.DecisionPrescribed { + normalized.Prescription = &behavior.Prescription{ + ID: resolution.Prescription.ID, TransitionID: string(resolution.Prescription.TransitionID), Handle: resolution.Prescription, + } + } + return normalized +} + +func normalizeSoftwareDecision(kind supervisor.DecisionKind) behavior.DecisionKind { + switch kind { + case supervisor.DecisionPrescribed: + return behavior.DecisionPrescribed + case supervisor.DecisionTerminal: + return behavior.DecisionSatisfied + case supervisor.DecisionFrontier: + return behavior.DecisionFrontier + case supervisor.DecisionBlocked: + return behavior.DecisionBlocked + case supervisor.DecisionRefused: + return behavior.DecisionRefused + default: + return behavior.DecisionUnresolved + } +} + +func (b *softwareBackend) ResolveUntargeted(t testing.TB) behavior.Resolution { + return b.resolve(t, "") +} + +func (b *softwareBackend) ResolveTargeted(t testing.TB, role behavior.TransitionRole) behavior.Resolution { + return b.resolve(t, catalog.TransitionID(b.TransitionID(role))) +} + +func (b *softwareBackend) Apply(t testing.TB, prescription behavior.Prescription) behavior.ApplyOutcome { + t.Helper() + handle, ok := prescription.Handle.(protocol.Prescription) + if !ok { + t.Fatalf("prescription handle is not a software prescription: %T", prescription.Handle) + } + _, recoveryBefore := b.journal.snapshot() + result, err := b.engine.Apply(context.Background(), engine.ApplyRequest{ + ResolveRequest: b.resolveRequest(catalog.TransitionID(prescription.TransitionID)), + FlowID: "flow", Prescription: handle, AdmissionLifetime: time.Minute, + }) + _, recoveryAfter := b.journal.snapshot() + return normalizeSoftwareApply(result, err, recoveryAfter > recoveryBefore) +} + +func normalizeSoftwareApply(result engine.ApplyResult, err error, recoveryMarked bool) behavior.ApplyOutcome { + var stalePrescription engine.StalePrescriptionError + var staleAdmission engine.StaleAdmissionError + var decisionErr engine.DecisionError + switch { + case err == nil: + return behavior.ApplyOutcome{Committed: true, ReceiptID: result.Receipt.ID, Failure: behavior.FailureNone} + case errors.As(err, &stalePrescription), errors.As(err, &staleAdmission): + return behavior.ApplyOutcome{Failure: behavior.FailureStale, Reason: err.Error()} + case recoveryMarked: + return behavior.ApplyOutcome{Failure: behavior.FailureRecoveryRequired, Reason: err.Error()} + case errors.As(err, &decisionErr): + return behavior.ApplyOutcome{Failure: behavior.FailureRefused, Reason: err.Error()} + default: + return behavior.ApplyOutcome{Failure: behavior.FailureOther, Reason: err.Error()} + } +} + +func (b *softwareBackend) ConcurrentApply(t testing.TB, prescription behavior.Prescription) [2]behavior.ApplyOutcome { + t.Helper() + handle, ok := prescription.Handle.(protocol.Prescription) + if !ok { + t.Fatalf("prescription handle is not a software prescription: %T", prescription.Handle) + } + // Force both applies onto one base revision: each apply's first (pre-lock) + // observation blocks until the other's has completed, so both pass their + // unlocked freshness checks against the same base and the loser can only + // be rejected by the engine's in-lock revalidation. + barrier := newTwoPartyBarrier() + b.observerGate.arm(barrier) + defer b.observerGate.arm(nil) + defer barrier.cancel() + start := make(chan struct{}) + results := make(chan behavior.ApplyOutcome, 2) + for range 2 { + go func() { + <-start + result, err := b.engine.Apply(context.Background(), engine.ApplyRequest{ + ResolveRequest: b.resolveRequest(catalog.TransitionID(prescription.TransitionID)), + FlowID: "flow", Prescription: handle, AdmissionLifetime: time.Minute, + }) + results <- normalizeSoftwareApply(result, err, false) + }() + } + close(start) + var outcomes [2]behavior.ApplyOutcome + for index := range outcomes { + outcomes[index] = <-results + } + return outcomes +} + +func (b *softwareBackend) Inspect(t testing.TB) behavior.Observation { + t.Helper() + snapshot, err := model.CanonicalizeForProgram(b.plant.observation(), b.program.Fingerprint) + if err != nil { + t.Fatalf("canonicalize plant observation: %v", err) + } + b.plant.mu.Lock() + stage, phase, recovery := b.plant.stage, b.plant.phase, b.plant.recovery + revision, objectiveID := b.plant.revision, b.plant.objectiveID + executions := b.plant.executions[softwareAdvanceID] + b.plant.mu.Unlock() + committed, _ := b.journal.snapshot() + return behavior.Observation{ + StateRevision: revision, + Mode: stage, + ObservationFingerprint: snapshot.Fingerprint, + ObjectiveBound: true, + ObjectiveIdentity: objectiveID, + RecoveryPending: phase == model.PhaseRecovery, + AdvanceEffectExecutions: executions, + CommittedFacts: committed, + ReceiptIDs: b.receipts.ids(), + AtTarget: stage == "terminal" && recovery == model.RecoveryNone && phase != model.PhaseRecovery, + } +} + +func (b *softwareBackend) Events() []behavior.Event { return b.events.snapshot() } + +func (b *softwareBackend) DriftStateRevision(testing.TB) { + b.plant.mu.Lock() + b.plant.revision++ + b.plant.mu.Unlock() +} + +func (b *softwareBackend) DriftObservation(testing.TB) { + b.plant.mu.Lock() + b.plant.nonce = "drifted" + b.plant.mu.Unlock() +} + +func (b *softwareBackend) DriftObjectiveBinding(testing.TB) { + b.plant.mu.Lock() + b.plant.objectiveID = "objective-drifted" + b.plant.mu.Unlock() + b.objective.ID = "objective-drifted" +} + +func (b *softwareBackend) IsolateExplicitOnly(testing.TB) { + b.plant.mu.Lock() + b.plant.stage = softwareExplicitGateStage + b.plant.mu.Unlock() +} + +func (b *softwareBackend) RetargetInstance(testing.TB) { + b.plant.mu.Lock() + b.plant.repositoryID, b.plant.worktreeID = "repo-other", "wt-other" + b.plant.mu.Unlock() +} + +func (b *softwareBackend) ExpireAuthority(testing.TB) { + // The fixture authority expires one hour after the fixed clock seed. + b.clock.advance(2 * time.Hour) +} + +func (b *softwareBackend) DropAuthority(testing.TB) { b.authority = protocol.AuthorityBundle{} } + +func (b *softwareBackend) WithholdMinimumCapability(t testing.TB) { + t.Helper() + // Keep the repository-class authority valid and its authority-class gate + // satisfied, but rebuild the engine over a registry whose advance effect + // the kernel-owned floor classifies as requiring publication.publish — a + // trusted minimum the repository class cannot grant. The denial must come + // from the production capability projection, not the relation gate. + b.registry = softwareCapabilityFloorRegistry(t) + b.engine = b.newEngine(t, b.program) +} + +func (b *softwareBackend) FailNextVerification(testing.TB) { b.effects.armVerificationFailure() } + +func (b *softwareBackend) FailNextCommit(testing.TB) { b.journal.failNextCommit() } + +func (b *softwareBackend) ProgramDrifted(t testing.TB) behavior.Backend { + t.Helper() + drifted := *b + drifted.program = protocol.ProgramIdentity{ID: b.program.ID, Version: b.program.Version, Fingerprint: driftedProgramFingerprint} + drifted.engine = b.newEngine(t, drifted.program) + return &drifted +} diff --git a/boatstack/flow/standard/completeness_test.go b/boatstack/flow/standard/completeness_test.go index 0cccc02..6f29c28 100644 --- a/boatstack/flow/standard/completeness_test.go +++ b/boatstack/flow/standard/completeness_test.go @@ -472,7 +472,7 @@ func classifiedProductionFile(relative string) bool { strings.HasPrefix(relative, "internal/hostprojection/") || strings.HasPrefix(relative, "internal/buildinfo/") || strings.HasPrefix(relative, "internal/runtime/") || strings.HasPrefix(relative, "internal/retromine/") || strings.HasPrefix(relative, "internal/testprogram/") || strings.HasPrefix(relative, "kernel/") || strings.HasPrefix(relative, "sdk/") || - strings.HasPrefix(relative, "analysis/") + strings.HasPrefix(relative, "analysis/") || strings.HasPrefix(relative, "conformance/") } func lifecycleSelector(name string) bool { diff --git a/boatstack/internal/softwaredelivery/engine/program_reconciliation_test.go b/boatstack/internal/softwaredelivery/engine/program_reconciliation_test.go new file mode 100644 index 0000000..00ca1ca --- /dev/null +++ b/boatstack/internal/softwaredelivery/engine/program_reconciliation_test.go @@ -0,0 +1,79 @@ +package engine + +import ( + "strings" + "testing" + + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/catalog" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/model" + "github.com/operatorstack/boatstack/boatstack/internal/softwaredelivery/supervisor" +) + +// TestProgramDriftSuspendsProgressUntilExplicitReconciliation proves the +// program-change suspension law: compiled control-program drift suspends both +// untargeted progress and explicitly requested ordinary transitions, while a +// core-system transition that declares program reconciliation remains +// explicitly resolvable through the same canonical relation. +func TestProgramDriftSuspendsProgressUntilExplicitReconciliation(t *testing.T) { + // control-law: program-drift-suspends-progress-until-explicit-reconciliation + observed := observation(model.PhaseObserved, "source") + observed.RecordedProgramFingerprint = strings.Repeat("a", 64) + snapshot, err := model.CanonicalizeForProgram(observed, syntheticProgramFingerprint) + if err != nil { + t.Fatal(err) + } + if snapshot.Program.Value != model.ProgramDrift { + t.Fatalf("program state = %s, want drift", snapshot.Program.Value) + } + control := supervisor.New(reconciliationRegistry(t), syntheticObjectiveContracts(t)) + authority := catalog.AuthoritySet{catalog.AuthorityRepository: true} + + untargeted := control.Resolve(snapshot, snapshot.Objective.Value, authority, "") + if untargeted.Kind != supervisor.DecisionUnresolved || untargeted.Reason != supervisor.ReasonProgramDrift { + t.Fatalf("untargeted progress crossed program drift: %+v", untargeted) + } + progress := control.Resolve(snapshot, snapshot.Objective.Value, authority, "test.advance") + if progress.Kind != supervisor.DecisionUnresolved || progress.Reason != supervisor.ReasonProgramDrift || progress.Transition != nil { + t.Fatalf("ordinary progress crossed program drift: %+v", progress) + } + reconcile := control.Resolve(snapshot, snapshot.Objective.Value, authority, "test.reconcile") + if reconcile.Kind != supervisor.DecisionPrescribed || reconcile.Transition == nil || reconcile.Transition.ID != "test.reconcile" { + t.Fatalf("explicit program reconciliation was not resolvable under drift: %+v", reconcile) + } +} + +func reconciliationRegistry(t *testing.T) catalog.Registry { + t.Helper() + base := testRegistry(t).All() + activePhase := string(model.PhaseActive) + reconcile := catalog.Transition{ + ID: "test.reconcile", Version: 1, Class: catalog.EventOwnedLocal, + Origin: catalog.TransitionOrigin{Kind: catalog.OriginCoreSystem, ID: "test.synthetic", Version: "1.0.0", ManifestFingerprint: syntheticProgramFingerprint}, + Owner: "test.synthetic", SelectionClass: catalog.SelectionExplicitOnly, + SourcePhases: []model.ProtocolPhase{model.PhaseObserved}, TargetPhases: []model.ProtocolPhase{model.PhaseActive}, + RequiredIdentity: []string{"repository-id", "git-common-id", "worktree-id"}, + Authority: []catalog.AuthorityClass{catalog.AuthorityRepository}, + RequiredCapabilities: []catalog.Capability{catalog.CapabilityRepositoryWrite}, + DeclaredCapabilities: []catalog.Capability{catalog.CapabilityRepositoryWrite, catalog.CapabilityCommandExecute}, + 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: "test.reconcile", LocalEffects: []catalog.EffectID{"test.reconcile"}, Idempotent: true, + Prescription: catalog.Prescription{Operation: "test.reconcile", ExpectedPostcondition: "reconciled"}, + SourcePredicate: "observed", AdmissionPredicate: "exact-admission", TargetPredicate: "reconciled", Verifier: "fresh-program", + SourceConditions: []catalog.FacetCondition{{Facet: model.FacetName("test.synthetic.stage"), Statuses: []model.FactStatus{model.FactKnown}, Values: []string{"start"}}}, + TargetConditions: []catalog.FacetCondition{{Facet: model.FacetProgram, Statuses: []model.FactStatus{model.FactKnown}, Values: []string{string(model.ProgramCurrent)}}}, + Interruption: catalog.InterruptionContract{ + Points: []string{"after-effect"}, PartialState: []string{"effect-possibly-installed"}, Detection: "test-observation", + ResumeContract: "test-resume", RollbackContract: "test-rollback", CompensationContract: "not-required", + Recovery: "test.recover", RecoveryAuthority: "test-authority", ResumptionPredicate: "test-resumption", + }, + Reversibility: catalog.Reversible, TerminalEffect: "none", + PrivacyClassification: "metadata-only", TelemetryClassification: "transition-receipt", CostClass: "test", + Policy: catalog.PolicyContract{ObjectiveScope: catalog.ObjectiveScopeBoundExact, ReconcilesProgram: true}, Priority: 3, + } + registry, err := catalog.New(append(base, reconcile)) + if err != nil { + t.Fatal(err) + } + return registry +} diff --git a/release-notes/2026-08-23-backend-neutral-behavioral-conformance-harness.md b/release-notes/2026-08-23-backend-neutral-behavioral-conformance-harness.md new file mode 100644 index 0000000..bac703e --- /dev/null +++ b/release-notes/2026-08-23-backend-neutral-behavioral-conformance-harness.md @@ -0,0 +1,18 @@ +### Backend-neutral behavioral conformance harness proves shared control laws on both runtimes + +Boatstack now verifies one set of supervisory control laws against both of its +real execution paths. A new backend-neutral harness expresses eighteen shared +behavioral laws once — canonical selection, explicit-only progress, authority +and freshness fail-closed behavior, durable-before-execution effects, +verification and commit failure handling, recovery non-duplication, +cross-instance replay refusal, concurrency single-commit, and target +reachability — and runs them unchanged through the generic kernel runtime +(integer fixture) and through the production software-delivery engine's public +Resolve/Apply boundary (deterministic in-memory software fixture). One genuine +gap is now recorded as executable evidence instead of an assumption: the +generic kernel runtime cannot yet express explicit-only transitions, which the +software-delivery catalog supports. A new regression test also freezes the +program-change suspension law: compiled control-program drift suspends +ordinary progress until an explicitly requested core-system reconciliation +transition resolves it. Users get a stronger guarantee that both runtimes +enforce the same supervisory behavior before any kernel contract changes.