Make software-delivery state effects declarative - #208
Conversation
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.98
The declarative state-effect contract is bypassed on protocol-backed production paths, the journal schema bump strands interrupted cross-version updates, and assignment validation admits deterministic apply refusals. Model-level verification is recommended after fixes, focused on whether every new declarative transition reaches its reducer and whether all version-skew recovery states retain progress.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.97
The new declarative-state boundary admits authority and liveness contradictions and gives semantically identical programs different identities. Model-level verification is recommended after these fixes: exhaustively check that every accepted assignment set preserves durable-state validity for all resolver-matching states, and that every native handler is bound to compatible origin, policy, facets, and capabilities.
Findings without inline diff anchors
[P2] Canonicalize unordered state-effect declarations before fingerprinting
Invariant: representation-only ordering must not change executable program identity. Preconditions are ANDed, their values are ORed, and assignments target unique fields, yet normalization skips all three new slices. Reversing two assignments, preconditions, or precondition values therefore produces identical behavior with a different program fingerprint, causing false program drift and unnecessary explicit reconciliation. This is introduced by adding state effects to the fingerprint without canonicalizing them. A regression should compile reordered equivalent manifests and assert identical fingerprints.
Confidence: 0.98
Location: boatstack/delivery/program_manifest.go:475-479 (RIGHT)
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.97
The new declarative state boundary introduces a reachable confused-deputy deletion path and makes recovery authority depend on mutable, unbound journal data. Model-level verification is recommended for whether other declaratively produced durable fields can unlock privileged native transitions or recovery cycles.
Findings without inline diff anchors
[P1] Recovery trusts an unbound journal field as state authority
Invariant: recovery may replay only the interrupted transition's kernel-admitted state-facet grant. AllowedStateFacets is canonicalized but is not included in the admission identity or checked against the admitted transition/program, yet recovery treats it as authority. Modifying a pending control-only journal to add program or installation, and modifying its staged state mutation accordingly, lets resume/rollback commit that cross-domain mutation and issue a successful recovery receipt. Previously recovery derived this envelope from kernel-owned transition rules. Add a regression test with a control-only interrupted admission and a journal claiming an added program facet; recovery must reject even when the claimed list and mutation annotations are canonical.
Confidence: 0.97
Location: boatstack/internal/softwaredelivery/effects/recovery.go:150-151 (RIGHT)
|
Fixed declaration canonicalization before fingerprinting. Preconditions, nested values, and assignments are sorted and deduplicated; reordered equivalent manifests now produce the same fingerprint. |
There was a problem hiding this comment.
Codex automated review
Verdict: patch is correct
Confidence: 0.86
No actionable patch-introduced defect was established. The declarations match prior reducer behavior, and validation closes resolver/apply, facet-ownership, fingerprint, and recovery-envelope relations. Model-level verification is recommended before merge because this broadly changes control-program state semantics; verify that no accepted declarative assignment combination can create a blocking durable state or recovery cycle.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.98
The patch introduces capability under-classification, mutable recovery authority, an unsound state-effect/target compatibility check, and a concrete unrecoverable schema-upgrade crash window. Model-level verification is recommended before merge, particularly to ask whether any newly declarative transition can deterministically miss its target or enter a recovery cycle.
Findings without inline diff anchors
[P1] Do not trust the journal's mutable facet envelope during recovery
Invariant: recovery may replay only the immutable facet authority of the interrupted admitted transition. AllowedStateFacets is stored outside the admission content identity, is merely syntax-checked when read, and is then used here as recovery authority. Starting with a control-only interrupted transition, changing the pending journal's envelope to include installation (and its staged state mutation/annotation accordingly) makes recovery.resume accept and commit runtime-state changes without installation authority. Previously recovery derived the envelope from the kernel transition mapping, so this widening is introduced by the patch. The observable result is cross-domain mutation through an untrusted recovery record. A regression test should tamper a valid control-only pending journal this way and prove recovery refuses before any mutation.
Confidence: 0.98
Location: boatstack/internal/softwaredelivery/effects/recovery.go:145-151 (RIGHT)
|
The remaining review-body finding is fixed in #209. Recovery no longer trusts an allowed-state-facets list stored in mutable journal JSON. It reconstructs the recovery envelope from the admitted transition identity and admission-bound required capabilities, with regression coverage for journal-field injection and authority widening. |
Summary
Boundary
StateEffectis a software-delivery domain primitive (category B), not a new kernel primitive. It uses the kernel transition vocabulary for owned facets and keeps capability and authority admission in the kernel. Repository and extension programs cannot select host-native handlers or own installation state.Native handlers remain only where the existing effect needs cross-field validation, conditional phase derivation, collection updates, or reconciliation: runtime/configuration reconciliation, installation/catalog reconciliation, objective binding, plan approval, abandonment, workspace cleanup/reap/reconciliation, gate evidence, visual evidence, and publication observation.
Verification
go test -race ./... -count=1go vet ./...go build ./...git diff --checkThe end-to-end regression adds a transition unknown to Go, applies its declared assignment, commits durable state, and retains its receipt. A temporary Standard Flow JSON declaration also passed the same test without production Go changes and was removed afterward.