Add reusable kernel conformance suite - #205
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. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.96
The new conformance suite can certify a program whose targeted transitions reach a marked state but whose normal untargeted control loop cycles indefinitely. This is a concrete test-oracle defect; model-level verification is not required to establish it and is not recommended before fixing this witness.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.97
The runtime implementation is unchanged, but the new reusable conformance API can certify concrete Store implementations that corrupt concurrent state or durable receipts. These deterministic negative fixtures should be added before merge. Model-level verification is not recommended; direct regression tests are sufficient.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.97
The production kernel is unchanged, but the new conformance suite weakens an existing exact objective-revision regression into an objective-identity test, allowing a core freshness defect to pass. No model-level verification is recommended before merge; a focused regression test is sufficient.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.91
The runtime is unchanged, but the new reusable conformance suite falsely rejects valid fixtures containing durable history. Model-level verification is not recommended before merge because the defect is confined to deterministic test accounting.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.91
The new conformance suite can certify a store that partially mutates durable control state on a failed commit, contradicting its atomic-commit claim. Model-level verification is not recommended before merge; a focused torn-commit regression test is sufficient.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.95
The production runtime is unchanged, but the newly advertised conformance verifier can certify false receipt/refusal/recovery behavior and can reject a valid broad-authority fixture. These are deterministic suite defects; model-level verification is not recommended before merge.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.96
The reusable suite can falsely certify invalid verification, non-CAS concurrency, and incomplete executable-program freshness. These are concrete oracle gaps in the primary feature. Model-level verification before merge is not recommended as a substitute; the demonstrable suite defects should be corrected first.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.95
The runtime itself is unchanged, but the newly introduced conformance verifier has two soundness gaps and an error-path deadlock. It can certify stores without commit-stage CAS and operators whose receipt effect facts are false, while asymmetric port failures can hang the suite. Model-level verification is not recommended before merge; these concrete verifier defects should be addressed with focused regression tests.
There was a problem hiding this comment.
Codex automated review
Verdict: patch is incorrect
Confidence: 0.96
The new verifier has concrete soundness gaps around program identity and authority expiry, and the repository contract weakens an existing domain-isolation check. Model-level verification is not recommended before merge; these deterministic verifier defects should be corrected first.
| alternate, err := kernel.NewRuntime(fixture.Scenario.AlternateProgram, fixture.Domain, fixture.Operator, fixture.CapabilityClassifier, fixture.Store, fixture.Locker, fixture.Clock) | ||
| if err != nil { | ||
| t.Fatal(err) | ||
| } | ||
| before := fixture.Scenario.Snapshot() | ||
| _, err = alternate.Apply(context.Background(), kernel.ApplyRequest{ResolveRequest: request, Prescription: prescription}) | ||
| after := fixture.Scenario.Snapshot() | ||
| if unchangedErr := refusedApplyMutationError(before, after, transition); err == nil || unchangedErr != nil { |
There was a problem hiding this comment.
[P1] Program-fingerprint check never isolates prescription freshness
Invariant: conformance must prove that a prescription is bound to the exact executable program fingerprint. Minimal sequence: resolve under program A/state A → create runtime B while durable state remains A → apply the old prescription. Apply can refuse solely because state A does not match runtime B, even if prescription fingerprint validation is completely removed; this test accepts any error. Thus the new suite can certify a kernel that permits old prescriptions after state and runtime are migrated together. The observable impact is execution under changed program semantics. Add a regression that retargets durable state to B at the same revision, applies A's prescription through runtime B, and requires a stale error with zero effects or state mutation.
Confidence: 0.98
| authority := fixture.Scenario.Authority | ||
| authority.Receipts = append([]kernel.AuthorityReceipt(nil), authority.Receipts...) | ||
| authority.Receipts[0].IssuedAt = fixture.Clock.Now().Add(time.Second) | ||
| resolution, err := resolveWithoutMutation(context.Background(), runtime, fixture.Scenario, kernel.ResolveRequest{InstanceID: fixture.Scenario.InstanceID, Objective: &fixture.Scenario.Objective, Authority: authority, Requested: transition}) |
There was a problem hiding this comment.
[P1] Authority conformance omits expiration and apply-time expiry
Invariant: expired authority must be rejected before effects, including when it expires between resolution and apply. The only temporal negative case changes IssuedAt to the future. A kernel that rejects future receipts but accepts ExpiresAt <= now passes the suite; likewise, the fixture cannot resolve with a valid receipt, advance the clock beyond expiry, and prove Apply refuses the historical prescription. This makes the new authority verifier unsound for a concrete credential-expiry bypass. Add expired-at-resolve and resolve-then-expire-before-apply cases, asserting refusal/staleness and an unchanged snapshot.
Confidence: 0.95
| production_files = [ | ||
| path for path in kernel_files if not path.name.endswith("_test.go") | ||
| ] | ||
| source = "\n".join(path.read_text() for path in production_files) |
There was a problem hiding this comment.
[P2] Domain-neutrality guard no longer scans kernel tests
Invariant: reusable general-kernel fixtures must remain domain-neutral. The patch excludes every *_test.go file from the vocabulary scan, while the remaining test-specific checks only reject Git command execution, testRepository, and softwaredelivery. Consequently, adding a compiling kernel test containing a pull-request-, branch-, coding-agent-, or publication-specific fixture now passes this repository contract, whereas the base check rejected it. This allows domain-specific evidence to masquerade as generic kernel coverage. A minimal regression is a temporary kernel test containing const fixtureDomain = "pull request" and an assertion that the contract rejects it; retain the domain-neutral scan for root kernel tests as well as production and conformance files.
Confidence: 0.96
1 participant
Summary
Verification
cd boatstack && go test -race ./kernel/... -count=1 -vpython3 -m unittest discover -s .github/tests -p "test_*.py" -qpython3 .github/scripts/run_go_tests.py(215 tests)cd boatstack && go vet ./... && go build ./...git diff --checkBoundary conformance
The suite imports only the general kernel. It does not use software-delivery packages, Git, repositories, worktrees, filesystem layouts, or subprocesses. Production kernel semantics are unchanged.