feat(trace): assert_no_side_effect turns side-effect observation into a verdict (#465 Phase A, 4/5)

crates/flowproof-agent/src/spec.rs

@@ -619,6 +619,7 @@ impl FlowSpec {
                     | SpecStep::AssertToolCall { .. }
                     | SpecStep::AssertNoToolCall { .. }
                     | SpecStep::AssertNoEgress
+                    | SpecStep::AssertNoSideEffect { .. }
             )
         });
 
@@ -1463,6 +1464,13 @@ pub enum SpecStep {
     /// phase, and a capability error on any platform where containment is
     /// not enforced.
     AssertNoEgress,
+    /// `app: agent`: assert the run OBSERVED no side effect of the named
+    /// kind (`fs_write` | `http_request`). Judged against the live
+    /// observation log of each phase, and a capability error on any
+    /// platform or driver where observation cannot run.
+    AssertNoSideEffect {
+        assert_no_side_effect: String,
+    },
     /// `app: agent`: assert NO declared secret appeared in the run's output
     /// corpus. The named-selector form: one or more `${VAR}` names, each a
     /// secret that must never surface. The `${VAR}` values resolve at
@@ -1570,6 +1578,7 @@ impl SpecStep {
          `assert_sql: {...}`, `assert_api: {...}`, `assert_screenshot: {...}`, \
          `prompt: <text>`, `assert_tool_call: <text>`, \
          `assert_no_tool_call: <text>`, `assert_no_egress`, \
+         `assert_no_side_effect: <kind>`, \
          `assert_no_secret_leak: ${VAR}`, `repeat: {...}`, `when: <cond>` with `steps:`, \
          `in: <surface>` with `steps:`, or `foreach: {...}`";
 
@@ -1639,6 +1648,39 @@ impl SpecStep {
                         }),
                         _ => Err("`assert_no_tool_call:` takes a string (a tool name)".into()),
                     },
+                    // `assert_no_side_effect:` takes ONE capturable kind,
+                    // read off the same list the capture mechanism emits, so
+                    // grammar and mechanism cannot drift; the schema's
+                    // reserved kinds earn their own message.
+                    Some("assert_no_side_effect") => {
+                        let kind = match inner {
+                            Value::String(s) => s.trim().to_string(),
+                            _ => {
+                                return Err(
+                                    "`assert_no_side_effect:` takes one kind (`fs_write` or \
+                                     `http_request`)"
+                                        .into(),
+                                )
+                            }
+                        };
+                        if ["db_change", "sap_transaction"].contains(&kind.as_str()) {
+                            return Err(format!(
+                                "`{kind}` is reserved for a later phase, not yet capturable; \
+                                 `assert_no_side_effect:` takes `fs_write` or `http_request`"
+                            ));
+                        }
+                        if !flowproof_trace::side_effect::capturable_kinds()
+                            .contains(&kind.as_str())
+                        {
+                            return Err(format!(
+                                "`{kind}` is not a capturable side-effect kind; \
+                                 `assert_no_side_effect:` takes `fs_write` or `http_request`"
+                            ));
+                        }
+                        Ok(SpecStep::AssertNoSideEffect {
+                            assert_no_side_effect: kind,
+                        })
+                    }
                     // `assert_no_secret_leak:` takes a single `${VAR}`
                     // selector or a LIST of them. Each is validated to be
                     // `${VAR}` syntax here, so a literal or a predicate is a
@@ -1797,6 +1839,9 @@ impl Serialize for SpecStep {
             SpecStep::AssertNoToolCall {
                 assert_no_tool_call,
             } => single(serializer, "assert_no_tool_call", assert_no_tool_call),
+            SpecStep::AssertNoSideEffect {
+                assert_no_side_effect,
+            } => single(serializer, "assert_no_side_effect", assert_no_side_effect),
             SpecStep::AssertSql { assert_sql } => single(serializer, "assert_sql", assert_sql),
             SpecStep::AssertApi { assert_api } => single(serializer, "assert_api", assert_api),
             SpecStep::AssertScreenshot { assert_screenshot } => {
@@ -1978,6 +2023,9 @@ impl SpecStep {
                 format!("assert_no_tool_call: {assert_no_tool_call}")
             }
             SpecStep::AssertNoEgress => "assert_no_egress".to_string(),
+            SpecStep::AssertNoSideEffect {
+                assert_no_side_effect,
+            } => format!("assert_no_side_effect: {assert_no_side_effect}"),
             SpecStep::AssertNoSecretLeak {
                 assert_no_secret_leak,
             } => {
@@ -3164,6 +3212,37 @@ steps:
         assert!(err.to_string().contains("assert_no_egress"), "{err}");
     }
 
+    /// `assert_no_side_effect` takes only the CAPTURABLE kinds and
+    /// round-trips as its keyed mapping. A reserved kind is refused with
+    /// its own message - "reserved", never "unknown" - and the step is
+    /// agent-only like the rest of the agent vocabulary.
+    #[test]
+    fn assert_no_side_effect_takes_only_capturable_kinds() {
+        let flow = spec(
+            "name: n\napp: agent\nagent:\n  command: x\nsteps:\n  - prompt: hi\n  - assert_no_side_effect: fs_write\n  - assert_no_side_effect: http_request\n",
+        )
+        .expect("parses");
+        let yaml = serde_yaml::to_string(&flow.steps).expect("serializes");
+        let back: Vec<SpecStep> = serde_yaml::from_str(&yaml).expect("round-trips");
+        assert_eq!(back, flow.steps);
+
+        for (kind, why) in [
+            ("db_change", "reserved for a later phase"),
+            ("exec", "not a capturable"),
+        ] {
+            let err = spec(&format!(
+                "name: n\napp: agent\nagent:\n  command: x\nsteps:\n  - prompt: hi\n  - assert_no_side_effect: {kind}\n"
+            ))
+            .expect_err(why);
+            assert!(err.to_string().contains(why), "{err}");
+        }
+
+        let err =
+            spec("name: n\napp: calc\nsteps:\n  - Type 5\n  - assert_no_side_effect: fs_write\n")
+                .expect_err("assert_no_side_effect on calc");
+        assert!(err.to_string().contains("agent step"), "{err}");
+    }
+
     /// A full `mcp:` block parses: servers, commands, and per-server tool
     /// mocks all land where the trace and stand-in expect them.
     #[test]