test(falsifiability): the side-effect assertion proven able to fail (#465 Phase A, 5/5) - #472
Open
AminChirazi wants to merge 1 commit into
Open
Conversation
11 tasks
AminChirazi
force-pushed
the
feat/465a-5-falsifiability
branch
from
August 11, 2026 19:10
6b1bec7 to
4285e96
Compare
AminChirazi
force-pushed
the
feat/465a-4-side-effect-assertion
branch
from
August 11, 2026 19:10
08ec605 to
2ddc5e8
Compare
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
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.
Part 5/5 of #465 Phase A. Stacked on 4/5; completes the split described there.
What
The red-path proof per CHARTER's falsifiability rules (add-only): the committed guilty fixture
side-effect-violation.trace.jsonlis fed through the REAL serde reader (side_effects_of, exported here withside_effect_verdict— their only consumer) and the real verdict; the test proves conviction namesunlinkatand the target,ControlVerdictmaps to Fail including for the./cannot certify.csvrecord (sentinel precedence on the real classification path), and on macOS a CLI subprocess run proves the capability direction fails with non-zero exit and "cannot certify" naming the platform. The Linux e2e pair (deleting-agent.py: record refused with no trace minted; a clean agent records green with an observed-and-clean lane) is compile-checked here and runtime-proven on the Linux CI runner. Also: theagent-testing.md"Side-effect assertion" section (allow-all/DNS/replay-performs-connects caveats), thehow-flowproof-tests-flowproof.mdtable row, and the CHANGELOG entry.Non-vacuity was verified adversarially before opening: with
side_effect_verdictgutted toOk(()), both harness tests FAIL (the gutted binary prints the exact false-green PASS the harness convicts); restored, they pass.Evidence
fmt 0 · clippy 0 ·
cargo test --workspace0 (harness runs 2/2 on macOS) · Linux cross-check 0 · ratchets.sh exit 0, diff 370/400.🤖 Generated with Claude Code