diff --git a/CHANGELOG.md b/CHANGELOG.md index 9a1cdef..c5f44f9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -72,6 +72,22 @@ together). discrimination. Without the second, "order-tolerant matching" would be indistinguishable from "the request is not checked at all", and a matcher that accepted anything would satisfy the first proof perfectly. +- **The argument matchers had no red path.** `assert_tool_call` could be proven + to fail on the tool NAME — a flow demanding a tool the agent never calls + refuses the trace — but nothing proved the `where ` clauses + can fail at all. Every `where` clause in the suite asserts an argument the + model was always going to produce, so each passes whether the matcher works or + not. + + That is the layer carrying the most weight and the least evidence. + `docs/agent-testing.md` calls argument assertions "usually where the bugs + are", and names chained arguments — threading one tool's result into the next + call — as the behaviour multi-step agents actually get wrong. + + One committed guilty call covers both halves of the vocabulary: the right tool + with the wrong city violates a value matcher (`where city equals Nairobi`) and + a presence matcher (`where city is absent`) at once. Both refuse the record, + and neither mints a trace. - **The guard assertion had no end-to-end test that could fail.** `assert_no_tool_call` is the one the security story leans on — the model diff --git a/crates/flowproof-cli/tests/falsifiability_arg_matchers.rs b/crates/flowproof-cli/tests/falsifiability_arg_matchers.rs new file mode 100644 index 0000000..bee1ff8 --- /dev/null +++ b/crates/flowproof-cli/tests/falsifiability_arg_matchers.rs @@ -0,0 +1,205 @@ +//! Falsifiability proof for `assert_tool_call ... where ` +//! (issue #247). +//! +//! `a_failing_assertion_refuses_the_trace` (`agent_flow_e2e.rs:778`) already +//! proves the TOOL-NAME layer can fail: the flow demands a tool the agent never +//! calls, and record refuses the trace. Nothing proved the ARGUMENT layer can. +//! +//! That is the layer carrying the most weight. `docs/agent-testing.md` says +//! argument assertions are "usually where the bugs are", and names chained +//! arguments -- threading one tool's result into the next call -- as the +//! behaviour multi-step agents actually get wrong. Every existing use of a +//! `where` clause asserts an argument the model was always going to produce, so +//! all of them pass whether the matcher works or not. +//! +//! The violating input is one guilty call, committed as +//! `tests/falsifiability/fixtures/tool-call-wrong-argument.json`: the right +//! tool, the wrong city. It violates two assertions at once -- +//! `where city equals Nairobi` (a value matcher, the value is Mombasa) and +//! `where city is absent` (a presence matcher, the key is there) -- so one +//! fixture covers both halves of the vocabulary. +//! +//! Two layers throughout: the record refuses, and no trace reaches disk. + +use std::io::{Read, Write}; +use std::net::TcpListener; +use std::path::{Path, PathBuf}; + +const FLOWPROOF_BIN: &str = env!("CARGO_BIN_EXE_flowproof"); + +/// An obedient agent: calls whatever the model asks, feeds the result back. +const TOOL_AGENT: &str = r#" +import json, os, urllib.request + +base = os.environ["OPENAI_BASE_URL"] +prompt = os.environ["FLOWPROOF_PROMPT"] +messages = [{"role": "user", "content": prompt}] + +for _ in range(5): + payload = json.dumps({ + "model": "gpt-4o", + "messages": messages, + "tools": [{"type": "function", "function": {"name": "get_weather"}}], + }).encode() + req = urllib.request.Request(base + "/chat/completions", data=payload, + headers={"content-type": "application/json"}) + with urllib.request.urlopen(req) as resp: + msg = json.load(resp)["choices"][0]["message"] + if msg.get("tool_calls"): + messages.append(msg) + for call in msg["tool_calls"]: + messages.append({"role": "tool", "tool_call_id": call["id"], + "content": json.dumps({"sky": "clear"})}) + continue + print(msg.get("content", "")) + break +"#; + +fn fixture() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../tests/falsifiability/fixtures/tool-call-wrong-argument.json") +} + +fn work_dir(name: &str) -> PathBuf { + let dir = std::env::temp_dir().join(format!("flowproof-fals-args-{name}")); + std::fs::remove_dir_all(&dir).ok(); + std::fs::create_dir_all(&dir).expect("work dir"); + dir +} + +fn read_http_request(stream: &mut std::net::TcpStream) -> String { + let mut buf = Vec::new(); + let mut chunk = [0u8; 1024]; + while let Ok(n) = stream.read(&mut chunk) { + if n == 0 { + break; + } + buf.extend_from_slice(&chunk[..n]); + let text = String::from_utf8_lossy(&buf).to_string(); + let Some(head_end) = text.find("\r\n\r\n") else { + continue; + }; + let len = text + .lines() + .find_map(|l| { + let (k, v) = l.split_once(':')?; + k.eq_ignore_ascii_case("content-length") + .then(|| v.trim().parse::().ok())? + }) + .unwrap_or(0); + if buf.len() >= head_end + 4 + len { + break; + } + } + String::from_utf8_lossy(&buf).to_string() +} + +/// Serve the committed guilty tool call, then a plain finish once the agent +/// reports the tool result back. +fn model_with_the_guilty_call() -> String { + let raw = std::fs::read_to_string(fixture()).expect("read fixture"); + let mut value: serde_json::Value = serde_json::from_str(&raw).expect("fixture is JSON"); + value + .as_object_mut() + .expect("fixture is an object") + .remove("_comment"); + let tool_call = value.to_string(); + let finish = serde_json::json!({ + "choices": [{"index": 0, "finish_reason": "stop", + "message": {"role": "assistant", "content": "Reported."}}] + }) + .to_string(); + + let listener = TcpListener::bind("127.0.0.1:0").expect("bind"); + let port = listener.local_addr().expect("addr").port(); + std::thread::spawn(move || { + for stream in listener.incoming().take(8) { + let Ok(mut stream) = stream else { continue }; + let req = read_http_request(&mut stream); + let body = if req.contains("\"role\":\"tool\"") || req.contains("\"role\": \"tool\"") { + finish.clone() + } else { + tool_call.clone() + }; + let _ = stream.write_all( + format!( + "HTTP/1.1 200 OK\r\ncontent-type: application/json\r\n\ + content-length: {}\r\nconnection: close\r\n\r\n{body}", + body.len() + ) + .as_bytes(), + ); + let _ = stream.flush(); + let _ = stream.shutdown(std::net::Shutdown::Write); + } + }); + format!("http://127.0.0.1:{port}/v1") +} + +/// Record the guilty trajectory against `assertion`, and return (success, out). +fn record_with(assertion: &str, tag: &str) -> (bool, String) { + let dir = work_dir(tag); + let agent = dir.join("agent.py"); + std::fs::write(&agent, TOOL_AGENT).expect("agent"); + let spec = dir.join("args.flow.yaml"); + std::fs::write( + &spec, + format!( + "name: Weather for Nairobi\n\ + app: agent\n\ + agent:\n command: python3 {agent}\n\ + tools:\n - name: get_weather\n result: {{ sky: clear }}\n\ + steps:\n\ + \x20 - prompt: What is the weather in Nairobi?\n\ + \x20 - assert_tool_call: {assertion}\n", + agent = agent.display() + ), + ) + .expect("spec"); + + let out = std::process::Command::new(FLOWPROOF_BIN) + .arg("record") + .arg(&spec) + .current_dir(&dir) + .env("FLOWPROOF_AGENT_UPSTREAM", model_with_the_guilty_call()) + .env("FLOWPROOF_AGENT_KEY", "not-a-real-key") + .output() + .expect("record"); + + let text = format!( + "stdout={} stderr={}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + let trace_written = dir.join("args.trace.jsonl").exists(); + assert!( + !trace_written || out.status.success(), + "a refused record must mint no trace: {text}" + ); + std::fs::remove_dir_all(&dir).ok(); + (out.status.success(), text) +} + +/// A value matcher must fail when the recorded argument differs. +#[test] +fn a_wrong_argument_value_fails_the_record() { + let (ok, text) = record_with("get_weather where city equals Nairobi", "equals"); + assert!( + !ok, + "the model called get_weather with city=Mombasa; `where city equals \ + Nairobi` must fail, or the matcher vocabulary proves nothing about the \ + layer the docs call 'usually where the bugs are'. {text}" + ); +} + +/// A presence matcher must fail when the argument is present after all. +#[test] +fn an_argument_asserted_absent_but_present_fails_the_record() { + let (ok, text) = record_with("get_weather where city is absent", "absent"); + assert!( + !ok, + "the call carries a `city` argument; `where city is absent` must fail. \ + A presence matcher that cannot fail would let a flow assert the \ + absence of anything at all. {text}" + ); +} diff --git a/docs/how-flowproof-tests-flowproof.md b/docs/how-flowproof-tests-flowproof.md index b78cc45..eeeb698 100644 --- a/docs/how-flowproof-tests-flowproof.md +++ b/docs/how-flowproof-tests-flowproof.md @@ -43,6 +43,7 @@ check and is exactly the defect worth catching. | `assert_no_tool_call` (the guard path) | [`guard-agent.py`](../tests/falsifiability/fixtures/guard-agent.py) | a guard assertion that cannot fail. Every other end-to-end use sits in a flow where the forbidden tool was never going to be called, so it would pass even if the assertion were an unconditional PASS | | `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`) | ### A note on gates specifically diff --git a/tests/falsifiability/fixtures/tool-call-wrong-argument.json b/tests/falsifiability/fixtures/tool-call-wrong-argument.json new file mode 100644 index 0000000..173e53f --- /dev/null +++ b/tests/falsifiability/fixtures/tool-call-wrong-argument.json @@ -0,0 +1,40 @@ +{ + "_comment": [ + "Falsifiability fixture for assert_tool_call ... where (issue #247).", + "", + "The model calls the RIGHT tool with the WRONG argument. That distinction is the whole point:", + "a_failing_assertion_refuses_the_trace in agent_flow_e2e.rs already proves the TOOL-NAME layer", + "can fail, by demanding a tool the agent never calls. Nothing proved the ARGUMENT layer can fail.", + "", + "docs/agent-testing.md says argument assertions are usually where the bugs are -- chained", + "arguments threaded from one tool result into the next call is named as the behaviour multi-step", + "agents get wrong. So the matcher vocabulary carries the most weight and, until now, the least evidence.", + "", + "Two assertions are violated by this one response:", + " - where city equals Nairobi -- the value is Mombasa;", + " - where city is absent -- the key is present.", + "One value matcher and one presence matcher, from a single guilty call.", + "", + "Do not fix the city. It is evidence, and it is supposed to be wrong." + ], + "choices": [ + { + "index": 0, + "finish_reason": "tool_calls", + "message": { + "role": "assistant", + "content": null, + "tool_calls": [ + { + "id": "call_1", + "type": "function", + "function": { + "name": "get_weather", + "arguments": "{\"city\":\"Mombasa\"}" + } + } + ] + } + } + ] +}