feat(grammar): an app that needs asking twice had no way to be asked

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

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<D: AppDriver>(
+    driver: &mut D,
+    app: &str,
+    condition: &str,
+) -> Result<bool, RecordError> {
+    let text = condition.trim();
+    // `page [does not] show <text>` - 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 \
+                       <text>`, `the \"<target>\" shows <text>`, or `the \"<target>\" 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<D: AppDriver, C: ModelClient>(
     // (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");

crates/flowproof-agent/src/rules.rs

@@ -642,16 +642,18 @@ fn refused(step: &str, reason: impl Into<String>) -> 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 <text>'",
+        "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: <condition>` 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: <condition>`",
             ),
             (
                 r#"Remember the "Total" matching /[0-9.]+/ as amount"#,