From f940b40ce458d90af93917e103033eb4939fd8a4 Mon Sep 17 00:00:00 2001 From: Amin Chirazi <32016576+AminChirazi@users.noreply.github.com> Date: Sun, 2 Aug 2026 05:21:48 +0400 Subject: [PATCH] feat(grammar): an app that needs asking twice had no way to be asked Repetition and branching were refused on the grounds that a trace must be a recording of what happened, not a program that decides what to do. That reasoning holds. What it did not follow from is that the loop had to be refused - only that it must not survive into the trace. `repeat:` (with `until:` and a required `max:`) and `when:` are blocks, and both expand while RECORDING: the condition is read against the live app, and what lands in the trace is the passes that actually ran. Replay reads a flat list and still decides nothing. If the condition never holds within `max:`, recording fails and names the bound rather than pressing forever. The step-shaped refusals stay, and now name the block that does the job. --- CHANGELOG.md | 18 +++ crates/flowproof-agent/src/recorder.rs | 193 ++++++++++++++++++++++++- crates/flowproof-agent/src/rules.rs | 31 ++-- crates/flowproof-agent/src/spec.rs | 107 +++++++++++++- docs/authoring.md | 50 ++++++- 5 files changed, 382 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3328254..99044d2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,6 +31,24 @@ together). ### Added +- **Some applications will not settle without being asked twice, and the + grammar had no way to ask.** Repetition and branching were refused on the + grounds that a trace must be a recording of what happened, not a program + that decides what to do. That reasoning holds. What it did not follow from + is that the loop had to be refused - only that it must not survive into + the trace. + + `repeat:` (with `until:` and a required `max:`) and `when:` are blocks, + expanded while RECORDING. The condition is read against the live app, and + what lands in the trace is the passes that actually ran: concrete steps, + no loop and no branch. Replay reads a flat list and still decides nothing. + `foreach` already made this bargain at parse time, which it can only do + because its list is known before anything runs. + + If the condition never holds, recording fails and names the bound rather + than pressing forever. The refusals stay, and now name the block that does + the job - a refusal whose alternative is real is the one worth keeping. + - **A contained run could delete your files and the report would not mention it.** `assert_no_egress` can say an agent did not *send* the thing it must not; nothing said anything about *delete*. A run that unlinked the customer diff --git a/crates/flowproof-agent/src/recorder.rs b/crates/flowproof-agent/src/recorder.rs index 1eebe81..b7e54ca 100644 --- a/crates/flowproof-agent/src/recorder.rs +++ b/crates/flowproof-agent/src/recorder.rs @@ -1688,6 +1688,82 @@ fn assert_holds(actual: &str, expected: &str, matcher: TextMatch) -> bool { } } +/// Does this condition hold RIGHT NOW? +/// +/// The predicate language of `repeat.until` and `when` is a deliberate +/// SUBSET of the assertion grammar: the forms that read state without +/// waiting for it. An auto-waiting predicate would turn a branch into a +/// race - `when` would sit for ten seconds deciding whether to take a +/// branch, and `until` could not tell "not yet" from "never". +/// +/// Anything outside the subset is refused at parse time by name, rather +/// than silently evaluating to false and taking the wrong branch. +fn condition_holds( + driver: &mut D, + app: &str, + condition: &str, +) -> Result { + let text = condition.trim(); + // `page [does not] show ` - the whole surface. + for (prefix, positive) in [ + ("page shows ", true), + ("the page shows ", true), + ("page does not show ", false), + ("the page does not show ", false), + ] { + if let Some(rest) = text.strip_prefix(prefix) { + let surface = driver.surface_text()?; + return Ok(flowproof_driver::text_contains(&surface, rest.trim()) == positive); + } + } + // Element forms go through the ordinary resolver, so a condition + // addresses an element exactly the way every other step does. + let resolved = crate::rules::resolve_step( + app, + &crate::spec::SpecStep::Assert { + assert: text.to_string(), + }, + )?; + let Some(action) = resolved.first() else { + return Ok(false); + }; + match action { + ResolvedAction::AssertText { + target, + expected, + matcher, + .. + } => { + let Some(selector) = action_selector(action) else { + return Ok(false); + }; + let _ = target; + if !driver.element_exists(&selector)? { + // A missing element makes a positive `shows` false and a + // negative one true - the same reading replay takes. + return Ok(matches!(matcher, TextMatch::NotContains)); + } + let actual = driver.read_text(&selector)?; + Ok(assert_holds(&actual, expected, *matcher)) + } + ResolvedAction::AssertPresence { present, .. } => { + let Some(selector) = action_selector(action) else { + return Ok(false); + }; + let (_, visible) = flowproof_driver::visible_now(driver, &selector)?; + Ok(visible == *present) + } + _ => Err(RecordError::AssertMismatch { + intent: text.to_string(), + expected: "a condition that reads state without waiting: `page [does not] show \ + `, `the \"\" shows `, or `the \"\" is \ + [not] visible`" + .to_string(), + actual: "this assertion form is not usable as a condition".to_string(), + }), + } +} + /// Record `spec` against the live app via `driver`, writing the trace to /// `out`. Every planned action's target element must exist before it is /// written — recording is a verification pass, not a transcription. @@ -1937,7 +2013,58 @@ pub fn record_with_reuse( // (b) every `assert_api` response body probed. Populated only when the // flow asserts `assert_no_secret_leak`. let mut secret_corpus: Vec<(String, String)> = Vec::new(); - for spec_step in &spec.steps { + // `repeat:` and `when:` are expanded HERE, against the live app, into the + // concrete steps that actually ran - so the trace stays a flat recording + // and replay never re-decides. `foreach` does the same thing at parse + // time; it can, because its list is known statically, and a condition + // cannot be known until something has run. + // Each entry carries how many passes ITS loop has made, so two loops in + // one flow do not share a budget. + let mut queue: std::collections::VecDeque<(crate::spec::SpecStep, u32)> = + spec.steps.iter().cloned().map(|s| (s, 0)).collect(); + while let Some((owned_step, passes)) = queue.pop_front() { + match &owned_step { + crate::spec::SpecStep::When { when } => { + if condition_holds(driver, spec.app.id(), &when.when)? { + for (i, inner) in when.steps.iter().enumerate() { + queue.insert(i, (inner.clone(), 0)); + } + } + continue; + } + crate::spec::SpecStep::Repeat { repeat } => { + // One pass is queued at a time, with the loop re-queued + // behind it, so the condition is re-read against the app + // AFTER each pass rather than against a stale reading. + if condition_holds(driver, spec.app.id(), &repeat.until)? { + continue; + } + if passes >= repeat.max { + return Err(RecordError::AssertMismatch { + intent: owned_step.intent().to_string(), + expected: format!( + "`{}` to hold within {} passes", + repeat.until, repeat.max + ), + actual: format!( + "it never did. The bound is the author saying what they believe \ + about the application - if {} passes is genuinely too few, raise \ + it; if the condition can never hold, the loop is not the bug", + repeat.max + ), + }); + } + let mut at = 0; + for inner in &repeat.steps { + queue.insert(at, (inner.clone(), 0)); + at += 1; + } + queue.insert(at, (owned_step.clone(), passes + 1)); + continue; + } + _ => {} + } + let spec_step = &owned_step; let intent = spec_step.intent().to_string(); let actions = author_actions( spec, @@ -2853,6 +2980,70 @@ steps: std::fs::remove_dir_all(&dir).ok(); } + const LOOP_SPEC: &str = "\ +name: Press until it settles +app: calc +steps: + - repeat: + until: page shows Done + max: 5 + steps: + - Press plus + - when: page shows Error + steps: + - Press equals + - assert: display shows 8 +"; + + fn surface_reads(driver: &mut MockAppDriver, reads: &[&str]) { + driver.text_sequence.insert( + MockAppDriver::SURFACE.to_string(), + reads.iter().map(|s| s.to_string()).collect(), + ); + } + + #[test] + fn a_repeat_records_the_passes_that_actually_ran() { + let spec = FlowSpec::parse(LOOP_SPEC).expect("spec parses"); + let mut driver = + MockAppDriver::new(&CALC_ELEMENTS).with_text("CalculatorResults", "Display is 8"); + // Read before the first pass, then after each: it settles on the + // third. The fourth read is the `when`, which does not hold. + surface_reads( + &mut driver, + &["counting", "counting", "Done", "all is well"], + ); + let out = std::env::temp_dir().join("flowproof-recorder-repeat.trace.jsonl"); + let summary = record(&spec, &mut driver, &out).expect("recording succeeds"); + + // Two passes ran, so two presses - not a loop, not the `max` of five - + // and no equalButton, because the `when` guarding it was false. + assert_eq!(driver.invoked, vec!["plusButton", "plusButton"]); + assert_eq!(summary.steps, 3); + let contents = std::fs::read_to_string(&out).expect("trace written"); + assert!( + !contents.contains("repeat"), + "the trace holds no control flow" + ); + std::fs::remove_file(&out).ok(); + } + + #[test] + fn a_repeat_that_never_settles_names_its_bound() { + let spec = FlowSpec::parse(LOOP_SPEC).expect("spec parses"); + let driver = + MockAppDriver::new(&CALC_ELEMENTS).with_text("CalculatorResults", "Display is 8"); + let mut driver = driver.with_text(MockAppDriver::SURFACE, "counting"); // forever + let out = std::env::temp_dir().join("flowproof-recorder-unbounded.trace.jsonl"); + let err = record(&spec, &mut driver, &out).expect_err("must fail"); + + let msg = err.to_string(); + assert!(msg.contains("within 5 passes"), "names the bound: {msg}"); + // It ran the bound and stopped there rather than pressing forever. + assert_eq!(driver.invoked.len(), 5); + std::fs::remove_file(&out).ok(); + } + #[test] fn missing_element_fails_recording() { let spec = FlowSpec::parse(CALC_SPEC).expect("spec parses"); diff --git a/crates/flowproof-agent/src/rules.rs b/crates/flowproof-agent/src/rules.rs index 96efabf..63a5d10 100644 --- a/crates/flowproof-agent/src/rules.rs +++ b/crates/flowproof-agent/src/rules.rs @@ -642,16 +642,18 @@ fn refused(step: &str, reason: impl Into) -> RulesError { const DECLINED_SHAPES: &[(&str, &str)] = &[ ( "loop", - "repetition is not in the grammar: a step that repeats until the app changes \ - makes the trace a program that decides what to do, rather than a recording of \ - what happened - drive the app to the state you want with the steps that reach \ - it, and assert the result with 'Wait until page shows '", + "repetition is a block, not a step: write `repeat:` with an `until:` condition \ + and a `max:` bound, whose passes are expanded while recording so the trace \ + still holds what happened rather than a program that decides what to do - a \ + loop written inside a step could not be expanded, because by the time the \ + step's own text is parsed there is nothing left to expand it into", ), ( "conditional", - "there are no conditionals: a flow that branches asserts something different on \ - each run, so what it proves cannot be read from the trace - write the branch \ - you mean to test as its own flow", + "a branch is a block, not a step: write `when: ` with `steps:` under \ + it, and the condition is read once while recording so the trace holds the \ + branch that was actually taken - if the two branches are two different things \ + to prove, they are still two flows", ), ( "regex", @@ -5556,20 +5558,23 @@ mod framed_target_tests { #[test] fn declined_shapes_are_refused_and_name_the_alternative() { let cases: &[(&str, &str, &str)] = &[ + // Repetition and branching EXIST, as blocks. The step forms stay + // refused, and now name the block that does the job - a refusal + // whose alternative is real is the one worth keeping. ( r#"Click "Next" until the "Status" shows Done"#, - "repetition", - "Wait until page shows", + "repetition is a block", + "`repeat:`", ), ( r#"While the "Spinner" is visible, press the "Retry" button"#, - "repetition", - "Wait until page shows", + "repetition is a block", + "`repeat:`", ), ( r#"If the "Banner" is visible, click "Dismiss""#, - "conditionals", - "its own flow", + "a branch is a block", + "`when: `", ), ( r#"Remember the "Total" matching /[0-9.]+/ as amount"#, diff --git a/crates/flowproof-agent/src/spec.rs b/crates/flowproof-agent/src/spec.rs index e9a7ff8..3da01f9 100644 --- a/crates/flowproof-agent/src/spec.rs +++ b/crates/flowproof-agent/src/spec.rs @@ -968,9 +968,48 @@ pub enum SpecStep { /// Each is validated at parse to be exactly `${NAME}` syntax. assert_no_secret_leak: Vec, }, + /// Repeat `steps` until `until` holds, at most `max` times. + /// + /// Expanded at RECORD time, not replay: the iterations that actually + /// happened are written into the trace as ordinary steps, so the trace + /// stays a recording of what happened and replay reads a flat list. + /// `foreach` does the same thing one phase earlier - it can expand at + /// parse time because its list is known statically, and this cannot. + Repeat { + repeat: RepeatSpec, + }, + /// Run `steps` only if `when` holds right now. Expanded at record time + /// like `repeat`: the branch that was TAKEN is recorded, and the one + /// that was not leaves nothing behind. + When { + when: WhenSpec, + }, Plain(String), } +/// `repeat: { until, max, steps }`. +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(deny_unknown_fields)] +pub struct RepeatSpec { + /// An ordinary assertion, in the same grammar every `assert:` uses. + pub until: String, + /// The bound. REQUIRED: a loop against a live application with no + /// ceiling is one that can hang a suite, and the number is also the + /// author saying what they believe about the app. + pub max: u32, + pub steps: Vec, +} + +/// `when: ` with its own `steps`. +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(deny_unknown_fields)] +pub struct WhenSpec { + /// An ordinary assertion; the branch runs only if it holds NOW, with no + /// auto-wait - a conditional that waited would be a race, not a branch. + pub when: String, + pub steps: Vec, +} + /// Validate one `assert_no_secret_leak` selector: it must be exactly a /// single `${NAME}` reference, nothing else. Returns the bare variable name. /// A non-`${VAR}` selector is a clear parse error, since the whole point is @@ -999,7 +1038,8 @@ impl SpecStep { `assert_sql: {...}`, `assert_api: {...}`, `assert_screenshot: {...}`, \ `prompt: `, `assert_tool_call: `, \ `assert_no_tool_call: `, `assert_no_egress`, \ - `assert_no_secret_leak: ${VAR}`, or `foreach: {...}`"; + `assert_no_secret_leak: ${VAR}`, `repeat: {...}`, `when: ` with `steps:`, or \ + `foreach: {...}`"; fn from_yaml(value: serde_yaml::Value) -> Result { use serde_yaml::Value; @@ -1017,6 +1057,14 @@ impl SpecStep { None => format!("{k:?}"), }) .collect(); + // `when:` is the one two-key step form: nesting the + // condition a level deeper to satisfy the arity rule would + // buy consistency with unreadable YAML. + if keys.len() == 2 && keys.contains(&"when".to_string()) { + return serde_yaml::from_value(Value::Mapping(map)) + .map(|when| SpecStep::When { when }) + .map_err(|e| format!("in `when` step: {e}")); + } if map.len() != 1 { return Err(format!( "a step mapping must have exactly one key, got {}; \ @@ -1100,6 +1148,9 @@ impl SpecStep { Some("assert_screenshot") => serde_yaml::from_value(inner) .map(|assert_screenshot| SpecStep::AssertScreenshot { assert_screenshot }) .map_err(|e| format!("in `assert_screenshot` step: {e}")), + Some("repeat") => serde_yaml::from_value(inner) + .map(|repeat| SpecStep::Repeat { repeat }) + .map_err(|e| format!("in `repeat` step: {e}")), // A foreach reaching typed parsing means it was not // expanded — it is only valid as a direct entry in a // spec's `steps:` (FlowSpec::parse expands it there). @@ -1173,6 +1224,15 @@ impl Serialize for SpecStep { match self { SpecStep::Plain(text) => serializer.serialize_str(text), SpecStep::AssertNoEgress => serializer.serialize_str("assert_no_egress"), + // Block steps round-trip as their single-key mapping. + SpecStep::Repeat { repeat } => { + use serde::ser::SerializeMap; + let mut m = serializer.serialize_map(Some(1))?; + m.serialize_entry("repeat", repeat)?; + m.end() + } + // Flat, matching the two-key form it was written in. + SpecStep::When { when } => when.serialize(serializer), // A single selector serializes as the string form it was written // in; several serialize as the list form. Both reparse identically. SpecStep::AssertNoSecretLeak { @@ -1335,6 +1395,10 @@ impl SpecStep { match self { SpecStep::Assert { assert } => assert.clone(), SpecStep::Plain(text) => text.clone(), + SpecStep::Repeat { repeat } => { + format!("repeat until {} (max {})", repeat.until, repeat.max) + } + SpecStep::When { when } => format!("when {}", when.when), SpecStep::AssertSql { assert_sql } => { format!("sql {}: {}", assert_sql.connection, assert_sql.query) } @@ -1947,6 +2011,47 @@ steps: assert_eq!(back, spec.steps); } + #[test] + fn repeat_and_when_survive_a_round_trip() { + let spec = FlowSpec::parse( + "name: x\napp: web\nsteps:\n\ + \x20 - repeat:\n until: page shows Done\n max: 3\n\ + \x20 steps:\n - Press go\n\ + \x20 - when: page shows ERROR\n steps:\n - Press reset\n", + ) + .expect("parses"); + let SpecStep::Repeat { repeat } = &spec.steps[0] else { + panic!("expected a repeat, got {:?}", spec.steps[0]); + }; + assert_eq!((repeat.max, repeat.steps.len()), (3, 1)); + // A `when` must serialize back FLAT, not nested a level deeper. + let yaml = serde_yaml::to_string(&spec.steps).expect("serializes"); + let back: Vec = serde_yaml::from_str(&yaml).expect("round-trips"); + assert_eq!(back, spec.steps); + } + + #[test] + fn a_repeat_needs_both_its_bound_and_its_condition() { + let body = "\n steps:\n - Press go\n"; + for (bad, wanted) in [ + ( + format!(" - repeat:\n until: page shows Done{body}"), + "missing field", + ), + (format!(" - repeat:\n max: 3{body}"), "missing field"), + // A `when` with no steps is a one-key mapping, so it reaches the + // unknown-key path - which names the shape it should have had. + ( + " - when: page shows X\n".to_string(), + "`when: ` with `steps:`", + ), + ] { + let err = FlowSpec::parse(&format!("name: x\napp: web\nsteps:\n{bad}")) + .expect_err("must be rejected"); + assert!(err.to_string().contains(wanted), "{err}"); + } + } + #[test] fn version_triples_parse_strictly() { assert_eq!(parse_version_triple("0.2.1").expect("ok"), (0, 2, 1)); diff --git a/docs/authoring.md b/docs/authoring.md index b889290..22850ef 100644 --- a/docs/authoring.md +++ b/docs/authoring.md @@ -91,8 +91,8 @@ records green and means something nobody asked for. | Refused | Why, and what to write | |---|---| -| `Click "Next" until …`, `While … , …` | Repetition would make the trace a program that decides what to do rather than a recording of what happened. Drive the app with the steps that reach the state, and assert with `Wait until page shows ` — which is real grammar, and is not this | -| `If … , …` / `… otherwise …` | A flow that branches asserts something different on each run, so what it proves cannot be read from the trace. Write the branch you mean to test as its own flow | +| `Click "Next" until …`, `While … , …` | Repetition is a block, not a step — write [`repeat:`](#repeating-until-the-app-settles-repeat-and-when). A loop written inside a step could not be expanded at record time, because by the time the step's own text is parsed there is nothing left to expand it into | +| `If … , …` / `… otherwise …` | A branch is a block, not a step — write [`when:`](#repeating-until-the-app-settles-repeat-and-when). If the two branches are two different things to prove, they are still two flows | | `Remember the "" matching /…/ as ` | A regex in the grammar is a second language inside the first. A capture reads an element's whole text; give the value its own element | | `Remember the text between "X" and "Y" as ` | Pattern matching by another name. `Remember the "" as ` reads a whole element, which is the unit a page actually renders | | `${date:…}` / `{Date[…]}` | Against the wall clock a flow means something different every day; against a pinned `browser.clock` it is a constant you can write by hand. Pin the clock and type the literal | @@ -532,6 +532,52 @@ steps: status: 500 ``` +## Repeating until the app settles (`repeat:` and `when:`) + +`foreach` repeats a block as many times as you know when you write it. +Sometimes you do not know — press a button until the label changes, recover +if an error appeared. Those are `repeat:` and `when:`. + +```yaml +steps: + - repeat: + until: the "id:button" shows Enough + max: 15 + steps: + - Press the "id:button" button + - when: the "id:b1" is not visible + steps: + - Press the "id:tech" button +``` + +**Both expand while recording, not while replaying.** The condition is read +against the live app, and what lands in the trace is the passes that +actually ran — ordinary concrete steps, no `repeat` and no `when`. The trace +stays a recording of what happened and replay still decides nothing. Against +a non-deterministic application that recording only replays against the same +behaviour, which for a regression test is the right way round: a flow that +silently re-adapted every run would always pass. + +`until:` is checked **before** the first pass, so a `repeat:` whose +condition already holds runs zero times. `max:` is required: if the +condition never holds within it, recording fails and names the bound. Each +`repeat:` gets its own budget. + +Conditions read state; they never wait: + +| Condition | Holds when | +|---|---| +| `page shows ` / `page does not show ` | the whole surface's text does or does not contain it | +| `the "" shows ` | that element's text contains it | +| `the "" is visible` / `is not visible` | it is on screen, or is missing or hidden | + +A missing element makes a positive `shows` false and a negative one true — +the same reading replay takes. Anything else is refused by name; there is no +numeric comparison, so `until:` cannot express "until this exceeds that". + +Scope conditions tightly: `page shows ERROR` also matches a heading reading +"Errors occur", so name the element instead. + ## Driving an arbitrary Windows app (`app:` mapping, `window:` config) `app:` is normally a registry id (`web`, `calc`, `notepad`, `sap`, `vision`,