Skip to content

test(falsifiability): the side-effect assertion proven able to fail (#465 Phase A, 5/5) - #472

Open
AminChirazi wants to merge 1 commit into
feat/465a-4-side-effect-assertionfrom
feat/465a-5-falsifiability
Open

test(falsifiability): the side-effect assertion proven able to fail (#465 Phase A, 5/5)#472
AminChirazi wants to merge 1 commit into
feat/465a-4-side-effect-assertionfrom
feat/465a-5-falsifiability

Conversation

@AminChirazi

Copy link
Copy Markdown
Contributor

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.jsonl is fed through the REAL serde reader (side_effects_of, exported here with side_effect_verdict — their only consumer) and the real verdict; the test proves conviction names unlinkat and the target, ControlVerdict maps to Fail including for the ./cannot certify.csv record (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: the agent-testing.md "Side-effect assertion" section (allow-all/DNS/replay-performs-connects caveats), the how-flowproof-tests-flowproof.md table row, and the CHANGELOG entry.

Non-vacuity was verified adversarially before opening: with side_effect_verdict gutted to Ok(()), 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 --workspace 0 (harness runs 2/2 on macOS) · Linux cross-check 0 · ratchets.sh exit 0, diff 370/400.

🤖 Generated with Claude Code

@AminChirazi AminChirazi added the needs-human A loop escalated this: it needs a decision or a protected-path change label Aug 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs-human A loop escalated this: it needs a decision or a protected-path change

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant