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

CHANGELOG.md

@@ -6,6 +6,21 @@ together).
 
 ## Unreleased
 
+### Added
+
+- **What an agent destroys is now evidence, and evidence you can assert
+  on.** A run that deleted a customer file printed the fact to stderr and
+  passed every check there was: the destruction lived in a channel nobody
+  reviews, no diff records, and no assertion could reach. An observed run
+  now records a `side_effects` lane - workspace-relative names only,
+  everything doubtful hash-redacted, scanned by the secret store-guard
+  before the trace is minted - and `assert_no_side_effect` turns it into a
+  verdict with the egress honesty rules: where observation cannot run it
+  fails "cannot certify" rather than passing vacuously, a blind supervisor
+  cannot certify either, and a violating record mints no trace. Observation
+  is still not containment: a run supervised only to watch reports its own
+  tier and never claims `enforced` for a policy nobody declared.
+
 ## 0.19.0
 
 ### Added

crates/flowproof-cli/src/agent_flow.rs

@@ -1281,6 +1281,15 @@ fn check_side_effects(
     Ok(lane)
 }
 
+/// The recorded side-effect lane's records and faults, read off any agent
+/// trace - the `egress_blocked` precedent, and the REAL serde path the
+/// falsifiability harness feeds back through [`side_effect_verdict`].
+pub fn side_effects_of(trace_path: &Path) -> Option<(Vec<SideEffect>, Vec<String>)> {
+    let raw = std::fs::read_to_string(trace_path).ok()?;
+    let trace: AgentTrace = serde_json::from_str(&raw).ok()?;
+    trace.side_effects.map(|lane| (lane.effects, lane.faults))
+}
+
 /// The short containment tag stored in the trace lane (the parenthetical of
 /// the report line): `enforced (linux seccomp)` or `not contained (<reason>)`.
 /// The run record stores the SAME string, so the trace and the artifact an

crates/flowproof-cli/src/lib.rs

@@ -4,6 +4,10 @@
 mod agent_flow;
 mod capture;
 
+// The falsifiability harness feeds committed fixture records through the
+// SAME reader and verdict record and replay execute, so they are public.
+pub use agent_flow::{side_effect_verdict, side_effects_of};
+
 use std::path::{Path, PathBuf};
 use std::time::Instant;
 

crates/flowproof-cli/tests/falsifiability_side_effect.rs

@@ -0,0 +1,292 @@
+//! Falsifiability proof for `assert_no_side_effect` (issue #465).
+//!
+//! The side-effect lane records what an agent destroyed or reached; this
+//! proves the record can be read in anger - a lane nothing can convict from
+//! is reporting, not evidence. Three red paths: the VIOLATION (a committed
+//! guilty trace through the real parse path and the real verdict, the same
+//! code record and replay execute), the CAPABILITY direction ("we could not
+//! observe" must never read as "nothing happened"), and CLASSIFICATION
+//! injection (a target named `./cannot certify.csv` must not relabel a
+//! violation as capability-error).
+//!
+//! Two layers, as everywhere in this suite: the verdict, and the exit code.
+
+use std::path::{Path, PathBuf};
+
+use flowproof_cli::{side_effect_verdict, side_effects_of};
+use flowproof_replay::runrecord::ControlVerdict;
+
+fn fixture(name: &str) -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR"))
+        .join("../../tests/falsifiability/fixtures")
+        .join(name)
+}
+
+fn work_dir(name: &str) -> PathBuf {
+    let dir = std::env::temp_dir().join(format!("flowproof-fals-side-effect-{name}"));
+    std::fs::remove_dir_all(&dir).ok();
+    std::fs::create_dir_all(&dir).expect("work dir");
+    dir
+}
+
+/// A well-behaved agent: exactly the one model call the fixture cassette
+/// recorded, and no filesystem writes at all.
+const CLEAN_AGENT: &str = r#"
+import json, os, urllib.request
+base = os.environ["OPENAI_BASE_URL"]
+payload = json.dumps({"model": "gpt-4o", "messages": [
+    {"role": "user", "content": os.environ["FLOWPROOF_PROMPT"]}]}).encode()
+req = urllib.request.Request(base + "/chat/completions", data=payload,
+                             headers={"content-type": "application/json"})
+urllib.request.urlopen(req).read()
+"#;
+
+/// The spec both halves share: liveness first, then the assertion.
+fn write_spec(dir: &Path, agent: &Path) -> PathBuf {
+    let spec = dir.join("side.flow.yaml");
+    std::fs::write(
+        &spec,
+        format!(
+            "name: no deletions\napp: agent\nagent:\n  command: python3 {}\n\
+             steps:\n\x20 - prompt: Clean up the workspace\n\
+             \x20 - assert_no_side_effect: fs_write\n",
+            agent.display()
+        ),
+    )
+    .expect("spec");
+    spec
+}
+
+/// The committed guilty trace convicts through the real parse path and the
+/// real verdict - on macOS and Linux alike, which is what the pure
+/// factoring of `side_effect_verdict` buys.
+#[test]
+fn a_fixture_trace_with_a_recorded_side_effect_fails_the_assertion() {
+    let (effects, faults) = side_effects_of(&fixture("side-effect-violation.trace.jsonl"))
+        .expect("the fixture carries a side_effects lane");
+    // Self-check the fixture is actually guilty before asking for a verdict.
+    assert!(
+        effects.iter().any(|e| e.op.as_deref() == Some("unlinkat")),
+        "not guilty: {effects:?}"
+    );
+
+    let fs = vec!["fs_write".to_string()];
+    let err = side_effect_verdict(&fs, &effects, &faults, true, None)
+        .expect_err("a recorded fs_write must convict");
+    assert!(
+        err.contains("unlinkat") && err.contains("./exports/2025.csv"),
+        "{err}"
+    );
+    // ...including the record whose target quotes a capability keyword: the
+    // sentinel precedence, proven on the real classification path.
+    assert!(err.contains("./cannot certify.csv"), "{err}");
+    assert!(
+        !err.contains("198.51.100.9"),
+        "only the asserted kind convicts: {err}"
+    );
+    assert_eq!(
+        ControlVerdict::from_outcome(&Err(err)).0,
+        ControlVerdict::Fail,
+        "a violation is a Fail, never a capability error"
+    );
+
+    let http = vec!["http_request".to_string()];
+    let err = side_effect_verdict(&http, &effects, &faults, true, None)
+        .expect_err("a recorded http_request must convict too");
+    assert!(err.contains("198.51.100.9:443"), "{err}");
+    assert_eq!(
+        ControlVerdict::from_outcome(&Err(err)).0,
+        ControlVerdict::Fail
+    );
+}
+
+/// Where observation cannot run, the assertion fails rather than passing
+/// vacuously - the capability red path, at the exit-code layer this host
+/// can honestly provide.
+#[cfg(not(target_os = "linux"))]
+#[test]
+fn an_unobservable_platform_fails_the_assertion_rather_than_passing_vacuously() {
+    let dir = work_dir("capability");
+    let agent = dir.join("agent.py");
+    std::fs::write(&agent, CLEAN_AGENT).expect("agent");
+    std::fs::copy(
+        fixture("side-effect-violation.trace.jsonl"),
+        dir.join("side.trace.jsonl"),
+    )
+    .expect("stage the trace");
+    let spec = write_spec(&dir, &agent);
+
+    let out = std::process::Command::new(env!("CARGO_BIN_EXE_flowproof"))
+        .args(["run", spec.to_str().expect("utf8")])
+        .output()
+        .expect("flowproof run");
+    let text = format!(
+        "{}{}",
+        String::from_utf8_lossy(&out.stdout),
+        String::from_utf8_lossy(&out.stderr)
+    );
+    assert!(!out.status.success(), "must not pass vacuously: {text}");
+    // A JUDGMENT, not a usage error: the capability wording and the named
+    // platform reason distinguish the two.
+    assert!(text.contains("cannot certify"), "{text}");
+    assert!(
+        text.contains("Linux-only"),
+        "the platform reason is named: {text}"
+    );
+    std::fs::remove_dir_all(&dir).ok();
+}
+
+/// The Linux end-to-end pair, the `egress_e2e.rs` shape: kernel-dependent,
+/// so CI runs it with `RUN_EGRESS_E2E=1`.
+#[cfg(target_os = "linux")]
+mod linux_e2e {
+    use super::*;
+
+    /// The seccomp deadlock guard `egress_e2e.rs` carries, for the same
+    /// reason: a future deadlock must fail red, not hang CI.
+    struct Watchdog(std::sync::Arc<std::sync::atomic::AtomicBool>);
+
+    impl Watchdog {
+        fn arm(label: &'static str, secs: u64) -> Self {
+            use std::sync::atomic::Ordering;
+            let disarmed = std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false));
+            let flag = std::sync::Arc::clone(&disarmed);
+            std::thread::spawn(move || {
+                let deadline = std::time::Instant::now() + std::time::Duration::from_secs(secs);
+                while std::time::Instant::now() < deadline {
+                    if flag.load(Ordering::Relaxed) {
+                        return;
+                    }
+                    std::thread::sleep(std::time::Duration::from_millis(100));
+                }
+                eprintln!("side-effect E2E watchdog: `{label}` exceeded {secs}s - aborting");
+                std::process::abort();
+            });
+            Watchdog(disarmed)
+        }
+    }
+
+    impl Drop for Watchdog {
+        fn drop(&mut self) {
+            self.0.store(true, std::sync::atomic::Ordering::Relaxed);
+        }
+    }
+
+    fn enabled() -> bool {
+        std::env::var("RUN_EGRESS_E2E")
+            .map(|v| !v.is_empty())
+            .unwrap_or(false)
+    }
+
+    /// A canned one-reply model on loopback (exempt from observation).
+    fn fake_model(replies: usize) -> String {
+        let server = tiny_http::Server::http("127.0.0.1:0").expect("bind model");
+        let base = format!("http://{}/v1", server.server_addr());
+        std::thread::spawn(move || {
+            for _ in 0..replies {
+                let Ok(request) = server.recv() else { break };
+                let body = serde_json::json!({"choices": [{"index": 0,
+                    "finish_reason": "stop", "message":
+                    {"role": "assistant", "content": "All tidy now."}}]})
+                .to_string();
+                let response = tiny_http::Response::from_string(body).with_header(
+                    "content-type: application/json"
+                        .parse::<tiny_http::Header>()
+                        .expect("header"),
+                );
+                let _ = request.respond(response);
+            }
+        });
+        base
+    }
+
+    fn record(dir: &Path, spec: &Path, model: &str) -> (bool, String) {
+        let out = std::process::Command::new(env!("CARGO_BIN_EXE_flowproof"))
+            .args(["record", spec.to_str().expect("utf8")])
+            .current_dir(dir)
+            .env("FLOWPROOF_AGENT_UPSTREAM", model)
+            .output()
+            .expect("flowproof record");
+        let text = format!(
+            "{}{}",
+            String::from_utf8_lossy(&out.stdout),
+            String::from_utf8_lossy(&out.stderr)
+        );
+        (out.status.success(), text)
+    }
+
+    /// The record-refusal red path: a deleting agent fails, names the
+    /// syscall and the workspace-relative victim, and mints NO trace - a
+    /// refused record must not enshrine a passing cassette.
+    #[test]
+    fn a_deleting_agent_fails_the_record_and_mints_no_trace() {
+        if !enabled() {
+            eprintln!("RUN_EGRESS_E2E not set; skipping the seccomp E2E");
+            return;
+        }
+        let _watchdog = Watchdog::arm("a_deleting_agent_fails_the_record", 90);
+        let dir = work_dir("red");
+        let agent = dir.join("deleting-agent.py");
+        std::fs::copy(fixture("deleting-agent.py"), &agent).expect("stage agent");
+        let spec = write_spec(&dir, &agent);
+
+        let (ok, text) = record(&dir, &spec, &fake_model(4));
+        assert!(!ok, "a deleting agent must fail the record: {text}");
+        assert!(
+            text.contains("unlink") && text.contains("./victim.csv"),
+            "the failure names the syscall and the victim: {text}"
+        );
+        assert!(
+            !dir.join("side.trace.jsonl").exists(),
+            "a refused record mints no trace"
+        );
+        std::fs::remove_dir_all(&dir).ok();
+    }
+
+    /// The green-when-clean discriminator: an assertion that always fires
+    /// is as useless as one that never does. A clean agent records green
+    /// with an observed-and-clean lane, and the ONE tier line printed says
+    /// what was supervised - never `enforced` (the §465 tier pin).
+    #[test]
+    fn a_clean_agent_records_green_with_an_observed_lane() {
+        if !enabled() {
+            eprintln!("RUN_EGRESS_E2E not set; skipping the seccomp E2E");
+            return;
+        }
+        let _watchdog = Watchdog::arm("a_clean_agent_records_green", 90);
+        let dir = work_dir("green");
+        let agent = dir.join("agent.py");
+        std::fs::write(&agent, CLEAN_AGENT).expect("agent");
+        let spec = write_spec(&dir, &agent);
+
+        let (ok, text) = record(&dir, &spec, &fake_model(8));
+        assert!(ok, "a clean agent records green: {text}");
+        let tiers: Vec<&str> = text
+            .lines()
+            .filter(|l| l.contains("egress containment:"))
+            .collect();
+        assert_eq!(tiers.len(), 1, "one tier line, no contradiction: {text}");
+        assert!(
+            tiers[0].contains("not contained (flow engages side-effect observation only"),
+            "{text}"
+        );
+        assert!(!text.contains("enforced"), "{text}");
+        let trace = std::fs::read_to_string(dir.join("side.trace.jsonl")).expect("trace minted");
+        assert!(
+            trace.contains("\"observation\": \"observed (linux seccomp)\""),
+            "observed and clean, not silent: {trace}"
+        );
+        assert!(!trace.contains("\"effects\""), "clean: {trace}");
+
+        // And the machine-readable pin: replay's `--json` says contained: false.
+        let out = std::process::Command::new(env!("CARGO_BIN_EXE_flowproof"))
+            .args(["run", spec.to_str().expect("utf8"), "--json"])
+            .current_dir(&dir)
+            .output()
+            .expect("flowproof run --json");
+        let stdout = String::from_utf8_lossy(&out.stdout);
+        assert!(out.status.success(), "clean replay passes: {stdout}");
+        assert!(stdout.contains("\"contained\":false"), "{stdout}");
+        std::fs::remove_dir_all(&dir).ok();
+    }
+}

docs/agent-testing.md

@@ -912,6 +912,37 @@ having reached whatever it liked. Since 0.11 that run prints a warning naming
 the allow-list, the reason it was not applied, and the step to add - but a
 warning is what it is, and the assertion is what makes it a control.
 
+## Side-effect assertion (`assert_no_side_effect`)
+
+The recorded `side_effects` lane (below) can be asserted on directly, one
+step per kind: `- assert_no_side_effect: fs_write` (and/or `http_request`).
+It certifies what was OBSERVED, on the observation tier the lane names: no
+destructive filesystem syscall was observed attempted, no off-loopback
+network attempt was observed. Attempts, not outcomes - the observation
+punts below apply unchanged. The honesty rules are `assert_no_egress`'s:
+wherever observation cannot run (macOS, Windows, any `url:` service) the
+step fails "cannot certify" with no bypass, and a supervisor fault relevant
+to an asserted kind fails the same way, because an empty effects list under
+a blind supervisor is silence, not evidence.
+
+A flow asserting this WITHOUT engaging egress is supervised on Linux under
+an allow-all policy nobody declared. Its one tier line therefore reads `not
+contained (flow engages side-effect observation only; ...)` - observation is
+not containment, and replay under allow-all still PERFORMS the agent's
+connects before the verdict fails. Engaging observation also buys the
+supervisor's structural refusals, policy or none: fd-passing over trapped
+`sendmsg` is refused `EPERM`, and a non-loopback `listen()` is denied
+`EACCES` - visible to the agent as errno, recorded in no lane.
+
+Two readings to keep straight. `assert_no_side_effect: http_request` in a
+flow that also declares `allow_egress` fails BY CONSTRUCTION - every allowed
+and performed destination is an observed side effect; a flow wanting bounded
+egress wants `allow_egress` + `assert_no_egress` instead. And DNS: on a host
+whose resolver is off-loopback, the resolver's own UDP send is admitted
+under allow-all, observed, and fails the assertion - consistent with
+`assert_no_egress`, which denies the same send. The failure names your
+resolver, not a flowproof bug.
+
 ## Filesystem observation
 
 **The observation itself is not a control.** It prevents nothing, and it

docs/authoring.md

@@ -1244,7 +1244,7 @@ LLM author. The step forms:
 | `prompt: <text>` | the task handed to the agent; several `prompt:` steps are joined into one turn |
 | `assert_tool_call: <tool> [where <path> <matcher> <value> [and …]]` | a tool call the agent must make. Matchers: `equals` (alias `is`), `contains`, `matches` (regex), `exists`, `is absent` |
 | `assert_no_tool_call: <tool> [where …]` | a tool the agent must NOT call anywhere in the trajectory |
-| `assert_no_side_effect: <kind>` | the run OBSERVED no side effect of the kind (`fs_write` or `http_request`); anywhere observation cannot run it fails "cannot certify" rather than passing vacuously |
+| `assert_no_side_effect: <kind>` | the run OBSERVED no side effect of the kind (`fs_write` or `http_request`); anywhere observation cannot run it fails "cannot certify" rather than passing vacuously. See [agent-testing.md](agent-testing.md#side-effect-assertion-assert_no_side_effect) |
 | `assert: reply contains <text>` | the final assistant message contains `<text>` |
 
 `agent:` (command/env), `tools:` (the boundary mocks), and `strict:` are

docs/how-flowproof-tests-flowproof.md

@@ -44,6 +44,7 @@ check and is exactly the defect worth catching.
 | `assert: reply contains` | [`reply-missing-text.json`](../tests/falsifiability/fixtures/reply-missing-text.json) | the same shape of hole in the assertion that has already hosted one false green: every existing use asserts text the model was always going to produce, so none of them would notice the assertion ceasing to work |
 | cassette call-order tolerance | [`two-call-agent.py`](../tests/falsifiability/fixtures/two-call-agent.py) | a tolerance that quietly became "the request is never checked". Reordering two INDEPENDENT calls must not diverge; changing what one of them SENDS still must |
 | `assert_tool_call` argument matchers | [`tool-call-wrong-argument.json`](../tests/falsifiability/fixtures/tool-call-wrong-argument.json) | a matcher vocabulary that cannot fail. The tool-NAME layer is proven; every `where` clause in the suite asserts an argument the model was always going to produce. One guilty call violates both a value matcher (`equals`) and a presence matcher (`is absent`) |
+| `assert_no_side_effect` | [`side-effect-violation.trace.jsonl`](../tests/falsifiability/fixtures/side-effect-violation.trace.jsonl) | a side-effect record that can be written but never read in anger — a lane nothing can convict from is reporting, not evidence; the capability direction, so "we could not observe" never reads as "nothing happened"; and verdict-class injection, so a target named after a capability keyword cannot relabel a violation |
 
 ### A note on gates specifically