Property invariants across the decision space + crash safety - #376
Merged
Conversation
…h safety
Gold plan steps 3 and 4.
PROPERTIES (AdmissionPropertyTests): 10,000 generated policy/proposal pairs across
five fixed seeds, machine-checking what must hold for EVERY input, not just the
semantic table's rows:
P1 soundness — Admitted only ever means: self-extending mode AND kind inside the
envelope AND every required gate ran-and-passed AND budget remained
P2 sealed always rejects
P3 Held or Admitted implies the envelope and gates held
P4 determinism; P5 course order is irrelevant; P6 budget monotonicity — spending
more budget can never turn a non-admit into an admit
P0 a reason, always
Deliberately dependency-free: seeded Random instead of FsCheck, so no new package
pin rides in on a test change — that supply-chain decision belongs to the
maintainer. Failures print seed + iteration for exact reproduction.
CRASH SAFETY (GateStoreCrashSafetyTests + the sweep): a writer dying between
write and move leaves a stray .json.tmp. It could never be read as a record
(listings enumerate *.json; the four-char extension dodges the Windows legacy
three-char pattern quirk), but it sat forever — now janitored under the store
lock, where no writer can be mid-move. Tests pin: strays never listed, swept on
the next locked operation, a crashed REWRITE leaves the previously committed
record intact (the half-written verdict simply never happened), and sweeping
never touches committed records.
Deliberately absent: chmod-based read-only tests — the container runs as root,
root bypasses DAC, and this repository has learned three separate times that a
mode-000 premise silently evaporates. OS permissions are the OS's test.
Verified: Tests.Kernel 312/312 (9 new: 5 property theories x 2000 iterations, 4 crash).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Gold plan step 5. Stryker over AdmissionGate + both loaders: 555 mutants, 131
tested, initial score 71.33%. TRIAGE FINDING, the important part: the score
under-counts — the scariest survivor (the sealed-check equality flip) was
hand-applied and killed by 15 existing tests, so Stryker's coverage-based test
selection is unreliable in this net10/xunit setup. Where tool and hand-check
conflict, the hand-check wins; nightly mutation config must use
--coverage-analysis off.
The survivors consistent with real test inventory were genuine gaps, now killed:
- PolicyLoader apiVersion/kind mismatch had NO tests (the manifest had them;
the policy did not)
- the parsed-is-null branch ("null"/"~" YAML documents) untested in both loaders
- ManifestLoader wrong-kind untested
- AdmissionGate's ThrowIfNull guards uncovered
Remaining known survivors are message-string mutants on reason text whose
load-bearing substrings are already asserted; blanket exact-message assertions
would make every wording improvement a test change, so they are accepted.
Tests.Kernel 318/318 (6 new).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
IanFrelinger
pushed a commit
that referenced
this pull request
Aug 23, 2026
IanFrelinger
added a commit
that referenced
this pull request
Aug 23, 2026
…nfig, and the protocol (#377) Step 5 of the gold plan closed. The headline is about the TOOL, not the code: both Stryker modes produced false survivors (verified by hand-applying the two scariest mutants — 15 and 7 test failures respectively). By hand-verification AdmissionGate is 35/35 mutation-killed. The run still earned its keep: four survivor clusters were real test-inventory gaps, killed by six tests in #376. stryker-config.json is checked in pinning accurate mode for manual per-release runs; mutation testing is deliberately NOT wired as a CI gate until the false-survivor cause is understood — a gate that cries wolf trains people to ignore gates, which is the one lesson this product cannot afford to teach. Co-authored-by: PlzTouchGrass <130718671+PlzTouchGrass@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Gold plan steps 3 and 4 (sheet 10.2).
Properties: 10,000 generated policy/proposal pairs across five fixed seeds, machine-checking the soundness sentence (Admitted only ever = self-extending ∧ kind in envelope ∧ all required gates ran-and-passed ∧ budget remained) plus sealed-always-rejects, determinism, course-order irrelevance, and budget monotonicity. Dependency-free by design — seeded Random, not FsCheck, so no new package pin rides in on a test change; failures print seed+iteration for exact repro.
Crash safety: stray .json.tmp from a dead writer is never listed, is janitored under the store lock, and a crashed rewrite leaves the committed record intact. No chmod-based tests — root bypasses DAC in the container, a lesson this repo has learned three times.
Tests.Kernel 312/312.
🤖 Generated with Claude Code