feat(trace): first-class side_effect record and lane (#465 Phase A, 1/5)

crates/flowproof-cli/src/agent_flow.rs

@@ -26,6 +26,7 @@ use flowproof_adapters::mcp_stdio::{McpCall, McpOut, McpPlan, McpServerEvent};
 use flowproof_agent::{FlowSpec, SpecStep};
 use flowproof_trace::cassette::Cassette;
 use flowproof_trace::egress::EgressEvent;
+use flowproof_trace::side_effect::SideEffect;
 use flowproof_trace::substitution::Mocks;
 use flowproof_trace::toolcalls::{self, ToolCallExpectation};
 
@@ -94,6 +95,12 @@ struct AgentTrace {
     /// authority: enforcement always uses the CURRENT spec's set).
     #[serde(default, skip_serializing_if = "Option::is_none")]
     egress: Option<EgressTrace>,
+    /// The side-effect audit lane, written at record when the run was
+    /// observed. ADDITIVE and OMITTED when the mechanism never ran, so an
+    /// unsupervised flow serializes BYTE-IDENTICAL to today; absence means
+    /// "no observation mechanism", never "nothing happened".
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    side_effects: Option<SideEffectsTrace>,
 }
 
 /// The trace's egress lane: the containment tier the recording ran under, the
@@ -111,6 +118,21 @@ struct EgressTrace {
     blocked: Vec<EgressEvent>,
 }
 
+/// The trace's side-effect lane. The tag speaks OBSERVATION vocabulary
+/// (`observed`, never `enforced`) - nothing here was prevented. `faults`
+/// is kept beside `effects` because an empty effects list under a blind
+/// supervisor is silence, not evidence, and the lane must not launder one
+/// into the other.
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+struct SideEffectsTrace {
+    /// The observation tag, e.g. `observed (linux seccomp)`.
+    observation: String,
+    #[serde(default, skip_serializing_if = "Vec::is_empty")]
+    effects: Vec<SideEffect>,
+    #[serde(default, skip_serializing_if = "Vec::is_empty")]
+    faults: Vec<String>,
+}
+
 /// One MCP server's recorded lane: its mocks, snapshotted (travel-in-trace,
 /// like `AgentTrace.mocks`), and the JSON-RPC calls captured in order.
 #[derive(Debug, Clone, Default, serde::Serialize, serde::Deserialize)]
@@ -1392,6 +1414,9 @@ fn record_inner(
         cassette,
         mcp: mcp_trace,
         egress,
+        // Nothing populates the lane yet: capture lands with the fs and http
+        // hooks, so every trace this version writes omits the key.
+        side_effects: None,
     };
     let json = serde_json::to_string_pretty(&trace).map_err(|e| e.to_string())?;
     std::fs::write(out, json).map_err(|e| format!("writing {}: {e}", out.display()))?;
@@ -1599,6 +1624,7 @@ mod tests {
             cassette,
             mcp: BTreeMap::new(),
             egress: None,
+            side_effects: None,
         };
         std::fs::write(
             &path,
@@ -1761,6 +1787,7 @@ mod tests {
             cassette: neutral_cassette("hi", "there"),
             mcp: BTreeMap::new(),
             egress: None,
+            side_effects: None,
         };
         let json = serde_json::to_string_pretty(&trace).expect("serialize");
         // The `mcp` and `egress` keys are skipped when empty, so the bytes
@@ -1800,6 +1827,7 @@ mod tests {
                     at_ms: 42,
                 }],
             }),
+            side_effects: None,
         };
         let json = serde_json::to_string(&trace).expect("serialize");
         assert!(json.contains("\"egress\""), "egress present: {json}");
@@ -1812,6 +1840,74 @@ mod tests {
         assert_eq!(lane.blocked[0].protocol, "tcp");
     }
 
+    /// The side-effect lane round-trips, and unset record fields (the
+    /// reserved ones in particular) leave no key.
+    #[test]
+    fn a_side_effect_lane_survives_the_round_trip() {
+        let trace = AgentTrace {
+            app: "agent".into(),
+            mocks: BTreeMap::new(),
+            cassette: neutral_cassette("hi", "there"),
+            mcp: BTreeMap::new(),
+            egress: None,
+            side_effects: Some(SideEffectsTrace {
+                observation: "observed (linux seccomp)".into(),
+                effects: vec![SideEffect {
+                    kind: flowproof_trace::side_effect::KIND_FS_WRITE.into(),
+                    target: None,
+                    target_note: Some("outside workspace (sha256:9f1c22ab04e1)".into()),
+                    op: Some("openat".into()),
+                    flags: Some("O_WRONLY|O_TRUNC".into()),
+                    at_ms: 412,
+                    before: None,
+                    after: None,
+                    diff: None,
+                }],
+                faults: vec!["openat2: could not read open_how: EPERM".into()],
+            }),
+        };
+        let json = serde_json::to_string(&trace).expect("serialize");
+        assert!(json.contains("\"side_effects\""), "lane present: {json}");
+        for absent in ["\"target\"", "\"before\"", "\"after\"", "\"diff\""] {
+            assert!(!json.contains(absent), "no `{absent}` key: {json}");
+        }
+        let back: AgentTrace = serde_json::from_str(&json).expect("deserialize");
+        let lane = back.side_effects.expect("lane present");
+        assert_eq!(lane.observation, "observed (linux seccomp)");
+        assert_eq!(lane.effects.len(), 1);
+        assert_eq!(lane.effects[0].op.as_deref(), Some("openat"));
+        assert_eq!(lane.faults.len(), 1);
+    }
+
+    /// A side-effect-free trace serializes WITHOUT the key, and a trace
+    /// written before the lane existed still deserializes. A NEW sibling
+    /// of the existing byte-identity test rather than an edit to it.
+    #[test]
+    fn a_side_effect_free_trace_serializes_without_the_key() {
+        let trace = AgentTrace {
+            app: "agent".into(),
+            mocks: BTreeMap::new(),
+            cassette: neutral_cassette("hi", "there"),
+            mcp: BTreeMap::new(),
+            egress: None,
+            side_effects: None,
+        };
+        let json = serde_json::to_string_pretty(&trace).expect("serialize");
+        assert!(
+            !json.contains("side_effects"),
+            "no side_effects key on an unobserved trace: {json}"
+        );
+
+        // A hand-built pre-lane trace (no `side_effects` field at all)
+        // deserializes, the field defaulting to None.
+        let old = r#"{"app":"agent","mocks":{},"cassette":{"turns":[]}}"#;
+        let back: AgentTrace = serde_json::from_str(old).expect("pre-lane trace deserializes");
+        assert!(
+            back.side_effects.is_none(),
+            "absent side_effects defaults to None"
+        );
+    }
+
     // ---- egress containment verdict (cross-platform) ----
 
     /// A minimal `command:` Plan for exercising `check_egress` directly.
@@ -2357,6 +2453,7 @@ mod tests {
             cassette: neutral_cassette("hi", "there"),
             mcp,
             egress: None,
+            side_effects: None,
         };
         let json = serde_json::to_string(&trace).expect("serialize");
         assert!(json.contains("\"mcp\""), "mcp present: {json}");
@@ -3063,6 +3160,7 @@ mod tests {
             cassette: neutral_cassette("hi", "there"),
             mcp,
             egress: None,
+            side_effects: None,
         };
         let json = serde_json::to_string_pretty(&trace).expect("serialize");
         assert!(

crates/flowproof-trace/schema/side-effect-v1.schema.json

@@ -0,0 +1,59 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "https://github.com/automators-com/flowproof/blob/main/crates/flowproof-trace/schema/side-effect-v1.schema.json",
+  "title": "flowproof agent-trace side-effect lane v1",
+  "description": "The `side_effects` lane an `app: agent` trace document may carry, and the records inside it. Deliberately describes the lane only, not the whole agent-trace document.",
+  "oneOf": [
+    { "$ref": "#/$defs/side_effects_lane" },
+    { "$ref": "#/$defs/side_effect" }
+  ],
+  "$defs": {
+    "side_effect": {
+      "type": "object",
+      "description": "One observed side-effect ATTEMPT, never an outcome claim: the fs observation replies CONTINUE before the kernel runs the call.",
+      "required": ["kind", "at_ms"],
+      "additionalProperties": false,
+      "properties": {
+        "kind": {
+          "description": "fs_write and http_request are capturable; db_change and sap_transaction are RESERVED - documented, never emitted in Phase A.",
+          "enum": ["fs_write", "http_request", "db_change", "sap_transaction"]
+        },
+        "target": {
+          "type": "string",
+          "description": "fs: the hygiene-processed workspace-relative path (`./`-prefixed; a rename renders `src -> dst`). http: `ip:port`, or an unresolved `${VAR}` allow-entry spelling."
+        },
+        "target_note": {
+          "type": "string",
+          "description": "Why target is absent or weakened, e.g. `outside workspace (sha256:...)`."
+        },
+        "op": { "type": "string", "description": "fs: the syscall name. http: the transport (tcp/udp)." },
+        "flags": { "type": "string", "description": "fs only: the closed flag renderings, e.g. `O_WRONLY|O_TRUNC`." },
+        "at_ms": { "type": "integer", "minimum": 0, "description": "Monotonic ms since agent spawn, never wall clock." },
+        "before": { "type": "string", "description": "RESERVED, never emitted in Phase A." },
+        "after": { "type": "string", "description": "RESERVED, never emitted in Phase A." },
+        "diff": { "type": "string", "description": "RESERVED, never emitted in Phase A." }
+      }
+    },
+    "side_effects_lane": {
+      "type": "object",
+      "required": ["observation"],
+      "additionalProperties": false,
+      "properties": {
+        "observation": {
+          "type": "string",
+          "description": "The observation tag the recording ran under, e.g. `observed (linux seccomp)`. Observation vocabulary only - never `enforced`."
+        },
+        "effects": {
+          "type": "array",
+          "description": "The observed effects, ordered by at_ms. Absent when empty.",
+          "items": { "$ref": "#/$defs/side_effect" }
+        },
+        "faults": {
+          "type": "array",
+          "description": "Supervisor adjudication failures: an empty effects list under one is silence, not evidence.",
+          "items": { "type": "string" }
+        }
+      }
+    }
+  }
+}

crates/flowproof-trace/src/lib.rs

@@ -13,6 +13,7 @@ pub mod egress;
 pub mod format;
 pub mod secret;
 pub mod secret_scan;
+pub mod side_effect;
 pub mod substitution;
 pub mod toolcalls;
 

crates/flowproof-trace/src/side_effect.rs

@@ -0,0 +1,81 @@
+//! The on-trace side-effect record, shared by the lane builder
+//! (`flowproof-cli`) and the capture side (`flowproof-adapters`) so the
+//! two never drift on what a record means.
+//!
+//! A record is an observed ATTEMPT, never an outcome claim. The fs
+//! observation replies CONTINUE before the kernel runs the call, so an
+//! `unlinkat` of a file that was not there reads identically to one that
+//! destroyed data. An `http_request` record is a connect/send the
+//! supervisor itself performed on the child's behalf - stronger evidence,
+//! but still the destination, not the bytes.
+
+use serde::{Deserialize, Serialize};
+
+/// A destructive filesystem syscall observed by the seccomp supervisor.
+pub const KIND_FS_WRITE: &str = "fs_write";
+
+/// A non-loopback connect/send the supervisor performed for the child.
+pub const KIND_HTTP_REQUEST: &str = "http_request";
+
+/// The kinds the capture mechanism can actually produce. Spec validation
+/// and capture both read THIS list, so grammar and mechanism cannot
+/// drift; the reserved kinds (`db_change`, `sap_transaction` - in the
+/// schema's enum, never emitted in Phase A) are deliberately not in it.
+pub fn capturable_kinds() -> &'static [&'static str] {
+    &[KIND_FS_WRITE, KIND_HTTP_REQUEST]
+}
+
+/// One observed side effect, recorded into the trace's `side_effects`
+/// lane. `at_ms` is monotonic milliseconds since agent spawn - NEVER wall
+/// clock, so a re-record does not churn the lane on timing alone.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct SideEffect {
+    /// [`KIND_FS_WRITE`] or [`KIND_HTTP_REQUEST`]. A `String` rather than
+    /// an enum so a reader tolerates a kind it predates - the forward
+    /// posture a cassette turn's `protocol` takes.
+    pub kind: String,
+    /// fs: the hygiene-processed workspace-relative path, `./`-prefixed
+    /// and byte-for-byte the NAME the syscall used minus the workspace
+    /// prefix - never a resolution claim, since a symlinked intermediate
+    /// component can carry the actual victim elsewhere. A rename renders
+    /// `"<src> -> <dst>"`. http: `ip:port`, or the UNRESOLVED `${VAR}`
+    /// allow-entry spelling. Absent when redacted or unreadable -
+    /// `target_note` says why.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub target: Option<String>,
+    /// Why `target` is absent or weakened: the trap proved the syscall,
+    /// the string naming the victim is weaker evidence.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub target_note: Option<String>,
+    /// fs: the syscall name. http: the transport (`tcp`/`udp`).
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub op: Option<String>,
+    /// fs only: the closed flag renderings, e.g. `O_WRONLY|O_TRUNC`.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub flags: Option<String>,
+    /// Monotonic milliseconds since the agent was spawned.
+    pub at_ms: u64,
+    /// RESERVED, never emitted in Phase A: a before-image would require
+    /// performing or delaying the syscall, which is prevention, not
+    /// observation. Declared now so a later phase adds no format change.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub before: Option<String>,
+    /// RESERVED, same reasoning as `before`.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub after: Option<String>,
+    /// RESERVED, same reasoning as `before`.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub diff: Option<String>,
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn the_capturable_kinds_exclude_the_reserved_ones() {
+        assert_eq!(capturable_kinds(), &[KIND_FS_WRITE, KIND_HTTP_REQUEST]);
+        assert!(!capturable_kinds().contains(&"db_change"));
+        assert!(!capturable_kinds().contains(&"sap_transaction"));
+    }
+}

crates/flowproof-trace/tests/side_effect_conformance.rs

@@ -0,0 +1,58 @@
+//! Keeps the `SideEffect` serde type, the side-effect JSON Schema, and the
+//! committed falsifiability fixture in agreement: the fixture's lane must
+//! validate, every record must parse into the typed model, and a serialize
+//! round-trip must reproduce the record and still validate.
+
+use flowproof_trace::side_effect::{capturable_kinds, SideEffect};
+
+const SCHEMA: &str = include_str!("../schema/side-effect-v1.schema.json");
+const FIXTURE: &str =
+    include_str!("../../../tests/falsifiability/fixtures/side-effect-violation.trace.jsonl");
+
+fn validator() -> jsonschema::Validator {
+    let schema: serde_json::Value = serde_json::from_str(SCHEMA).expect("schema is valid JSON");
+    jsonschema::validator_for(&schema).expect("schema compiles")
+}
+
+#[test]
+fn the_fixture_lane_validates_and_its_records_round_trip() {
+    let validator = validator();
+    let doc: serde_json::Value = serde_json::from_str(FIXTURE).expect("fixture is JSON");
+    let lane = doc
+        .get("side_effects")
+        .expect("fixture carries a side_effects lane");
+    assert!(
+        validator.validate(lane).is_ok(),
+        "fixture lane failed schema validation: {:?}",
+        validator.iter_errors(lane).next()
+    );
+
+    let effects = lane["effects"].as_array().expect("lane carries effects");
+    assert!(!effects.is_empty(), "the fixture is guilty by construction");
+    for raw in effects {
+        let parsed: SideEffect =
+            serde_json::from_value(raw.clone()).expect("record parses into the typed model");
+        // Only capturable kinds are ever emitted; the reserved kinds live in
+        // the schema's enum, not in a committed lane.
+        assert!(
+            capturable_kinds().contains(&parsed.kind.as_str()),
+            "fixture carries a non-capturable kind: {}",
+            parsed.kind
+        );
+        // Round-trip: what we serialize must reproduce the record exactly
+        // and still satisfy the schema.
+        let reserialized = serde_json::to_value(&parsed).expect("typed model serializes");
+        assert_eq!(reserialized, *raw, "round-trip reproduces the record");
+        assert!(
+            validator.validate(&reserialized).is_ok(),
+            "round-tripped record failed schema validation: {:?}",
+            validator.iter_errors(&reserialized).next()
+        );
+    }
+    // The schema is an instrument, not documentation: a kind outside the
+    // enum, or an unknown key, is refused.
+    let bad_kind = serde_json::json!({"kind": "exec", "at_ms": 1});
+    assert!(validator.validate(&bad_kind).is_err());
+    let bad_key = serde_json::json!({"kind": "fs_write", "at_ms": 1, "resolved_path": "/etc"});
+    assert!(validator.validate(&bad_key).is_err());
+}