feat(grammar): a count could be asserted but never used

CHANGELOG.md

@@ -6,6 +6,41 @@ together).
 
 ## Unreleased
 
+### Added
+
+- **A count could be asserted but never used.** `the "css:.row" appears 5
+  times` has always worked, and it is the right step when you know the
+  answer. When the app decides the answer — a table built from whatever the
+  backend returned — there was nothing to write. The number existed, the
+  grammar could compare it to a literal, and no literal was available.
+
+  `Remember how many "<target>" appear as <name>` reads it into the same
+  flow-scoped name a text capture uses, so everything captures already do
+  keeps working:
+
+  ```yaml
+  - Remember how many "css:.order-row" appear as rows
+  - Type ${captured.rows} into the "Rowcount" field
+  - assert: the "Total" shows ${captured.rows} + 1
+  ```
+
+  Counting rides the ordinal every adapter already implements, so it means
+  on each adapter exactly what `the 2nd "Row"` means there — no adapter
+  changed to gain it. The number is read at execution time on record and on
+  every replay, so only the reference enters the trace and a page that grew
+  a row does not need it rewritten.
+
+  **Zero fails.** A selector typo matches nothing, and so does an empty
+  table — and `0` is a confident, plausible number to type into an
+  application. A capture that answered `0` to both would be the silent
+  wrong-value class again, so the step refuses and names the one that means
+  zero: `assert: the "<target>" appears 0 times`.
+
+  There is no second definition of what a number is: the computed
+  comparison's normalisation is reused as it stands, which is what lets
+  `shows ${captured.rows} + 1` compose without either side knowing about
+  the other.
+
 ### Fixed
 
 - **The docs never said what a typed capture does with the text around

crates/flowproof-agent/src/recorder.rs

@@ -595,9 +595,20 @@ fn step_for(id: usize, intent: &str, app: &str, action: &ResolvedAction) -> Step
                 selector_ref: Some(0),
             }),
         ),
-        ResolvedAction::Capture { target, name } => {
+        ResolvedAction::Capture {
+            target,
+            name,
+            count,
+        } => {
             let mut params = serde_json::Map::new();
             params.insert("name".into(), name.clone().into());
+            // A new PARAM KEY, not a new action: the payload is free-form,
+            // so a trace written before counting existed still loads, and
+            // an old reader meeting this simply does not understand the
+            // step rather than misreading it as a text capture.
+            if *count {
+                params.insert("count".into(), true.into());
+            }
             (selectors_for(app, target, None), Action::Capture(params))
         }
         ResolvedAction::AssertCaptured {
@@ -1900,7 +1911,15 @@ pub fn record_with_reuse<D: AppDriver, C: ModelClient>(
                     | ResolvedAction::AssertChecked { .. }
                     | ResolvedAction::AssertCaptured { .. }
             );
-            if !is_assert {
+            // A COUNTING capture asks "how many", which is a question with
+            // a valid answer of none. The generic precheck would answer it
+            // with `ElementNotFound` - true, but it names a selector rather
+            // than the step that means zero, and this reading has its own
+            // account of why zero is refused. A TEXT capture keeps the
+            // precheck: it must read some element.
+            let is_counting_capture =
+                matches!(&action, ResolvedAction::Capture { count: true, .. });
+            if !is_assert && !is_counting_capture {
                 if let Some(selector) = &selector {
                     if !driver.element_exists(selector)? {
                         return Err(RecordError::ElementNotFound {
@@ -1945,8 +1964,33 @@ pub fn record_with_reuse<D: AppDriver, C: ModelClient>(
                 ResolvedAction::SetChecked { checked, .. } => {
                     driver.set_checked(targeted(), *checked)?
                 }
-                ResolvedAction::Capture { name, .. } => {
-                    let value = driver.read_text(targeted())?;
+                ResolvedAction::Capture { name, count, .. } => {
+                    let value = if *count {
+                        let found = flowproof_driver::count_matching(
+                            driver,
+                            targeted(),
+                            flowproof_driver::COUNT_DIAGNOSTIC_CAP,
+                        )?;
+                        // Zero FAILS rather than remembering "0". A
+                        // selector typo matches nothing, and so does an
+                        // empty table - and a capture that answered `0` to
+                        // both would type a confident wrong number into the
+                        // app. The step that MEANS zero is an assertion,
+                        // and the error says so.
+                        if found == 0 {
+                            return Err(RecordError::AssertMismatch {
+                                intent: spec_step.intent().to_string(),
+                                expected: "at least one matching element to count".to_string(),
+                                actual: "nothing matched, so the count would be a guess - \
+                                         to assert emptiness write 'assert: the \"<target>\" \
+                                         appears 0 times'"
+                                    .to_string(),
+                            });
+                        }
+                        found.to_string()
+                    } else {
+                        driver.read_text(targeted())?
+                    };
                     captures.insert(name.clone(), value);
                 }
                 ResolvedAction::AssertCaptured {
@@ -3322,6 +3366,65 @@ steps:
     /// step - `Click "Next" until the label changes` becomes ONE click -
     /// record green, and fail one replay in five. The decline has to
     /// outrank the fallback, and `calls == 0` is what proves it does.
+    /// A count is a READING, like any capture: taken at execution time on
+    /// record and on every replay, so a page that grew a row does not need
+    /// the trace rewritten. The number therefore never enters the trace -
+    /// only the reference does, exactly as a text capture works.
+    #[test]
+    fn a_counted_capture_records_the_reference_and_not_the_number() {
+        let spec = FlowSpec::parse(
+            "name: Rows\napp: web\nurl: https://e.test/x\nsteps:\n  \
+             - Remember how many \"css:.row\" appear as rows\n  \
+             - Type ${captured.rows} into the \"Count\" field\n",
+        )
+        .expect("parses");
+        let mut driver = MockAppDriver::new(&[".row", "Count"]).with_occurrences(".row", 7);
+        let out = std::env::temp_dir().join("flowproof-count-capture.trace.jsonl");
+        record(&spec, &mut driver, &out).expect("records");
+
+        // The app was handed the count, not the reference.
+        assert!(
+            driver.typed.iter().any(|(_, text)| text == "7"),
+            "the resolved count must be typed: {:?}",
+            driver.typed
+        );
+        let trace = std::fs::read_to_string(&out).expect("trace readable");
+        assert!(trace.contains("\"count\":true"), "the reading is recorded");
+        assert!(
+            trace.contains("${captured.rows}"),
+            "the typed step stores the REFERENCE"
+        );
+        assert!(
+            !trace.contains("\"text\":\"7\""),
+            "the number itself must never enter the trace: {trace}"
+        );
+        std::fs::remove_file(&out).ok();
+    }
+
+    /// The red path, and the reason this capture is not allowed to answer
+    /// `0`. A selector typo matches nothing and so does an empty table -
+    /// and `0` is a confident, plausible number to type into an app. The
+    /// step that MEANS zero is an assertion, and the error says so.
+    #[test]
+    fn a_count_of_zero_fails_instead_of_remembering_zero() {
+        let spec = FlowSpec::parse(
+            "name: Rows\napp: web\nurl: https://e.test/x\nsteps:\n  \
+             - Remember how many \"css:.typo\" appear as rows\n",
+        )
+        .expect("parses");
+        // `.typo` is not on the page - the shape of a selector mistake.
+        let mut driver = MockAppDriver::new(&[".row"]);
+        let out = std::env::temp_dir().join("flowproof-count-zero.trace.jsonl");
+        let err =
+            record(&spec, &mut driver, &out).expect_err("a count of zero must fail the recording");
+        let message = err.to_string();
+        assert!(
+            message.contains("appears 0 times"),
+            "the failure must point at the step that MEANS zero: {message}"
+        );
+        std::fs::remove_file(&out).ok();
+    }
+
     #[test]
     fn a_declined_shape_never_reaches_the_model_author() {
         for step in [

crates/flowproof-agent/src/rules.rs

@@ -201,7 +201,18 @@ pub enum ResolvedAction {
     /// Read a target's text into a flow-scoped name for later comparison
     /// (`Remember the "Balance" as balance`). The VALUE never enters the
     /// trace - only the name does, exactly like a `${VAR}` secret.
-    Capture { target: Target, name: String },
+    /// Remember something about the target under `name`, for a later
+    /// assertion or a later `Type` to use. `count` picks WHICH reading:
+    /// false is the element's text, true is how many elements match.
+    ///
+    /// Either way the value is taken at execution time on record and on
+    /// every replay, so it never enters the trace - the same indirection
+    /// `${VAR}` secrets use.
+    Capture {
+        target: Target,
+        name: String,
+        count: bool,
+    },
     /// Drive a checkbox-like control to a STATE (`Check`/`Uncheck`).
     /// Set-state rather than toggle, so the step means the same thing
     /// however the environment arrives: idempotent by design.
@@ -2586,6 +2597,44 @@ mod web {
         // `Remember the [Nth ]"<target>" as <name>` - read a value now so a
         // later assertion can compare against it. The value is read at
         // execution time on record AND replay, so it never enters the trace.
+        // `Remember how many "<target>" appear as <name>` - the COUNT, not
+        // the text. Same family and the same indirection: the number is
+        // taken at execution time on record and on every replay, so a page
+        // that grew a row does not need the trace rewritten.
+        //
+        // Checked before `remember the` because "how many" is not a target.
+        if let Some(rest) = strip_prefix_ci(trimmed, "remember how many ") {
+            let tail = rest.trim();
+            if let Some(quoted) = tail.strip_prefix('"') {
+                if let Some((label, after)) = quoted_label(quoted) {
+                    let after = after.trim();
+                    // `appear` reads correctly for a plural count; `appears`
+                    // is accepted because the singular slips out when the
+                    // author is thinking of one row.
+                    let after = strip_prefix_ci(after, "appear as ")
+                        .or_else(|| strip_prefix_ci(after, "appears as "));
+                    if let Some(name) = after.map(str::trim) {
+                        if !valid_capture_name(name) {
+                            return Err(unresolvable(
+                                trimmed,
+                                "a capture name must start with a lowercase letter and \
+                                 contain only lowercase letters, digits, and underscores",
+                            ));
+                        }
+                        return Ok(vec![ResolvedAction::Capture {
+                            target: target_from_label(label),
+                            name: name.to_string(),
+                            count: true,
+                        }]);
+                    }
+                }
+            }
+            return Err(unresolvable(
+                trimmed,
+                "expected 'Remember how many \"<target>\" appear as <name>'",
+            ));
+        }
+
         if let Some(rest) = strip_prefix_ci(trimmed, "remember the ") {
             let (nth, tail) = split_ordinal(rest.trim());
             if let Some(quoted) = tail.strip_prefix('"') {
@@ -2602,6 +2651,7 @@ mod web {
                         return Ok(vec![ResolvedAction::Capture {
                             target: scoped_target(trimmed, nth, label, scope)?,
                             name: name.to_string(),
+                            count: false,
                         }]);
                     }
                 }
@@ -3868,6 +3918,10 @@ mod tests {
             // Interpolation: several references in one step, and literal
             // text around them. Documented under "A typed value is
             // interpolated, not evaluated".
+            (
+                "web",
+                r#"Remember how many "css:.order-row" appear as rows"#,
+            ),
             ("web", r#"Type order-${captured.oid} into the "Ref" field"#),
             (
                 "web",
@@ -3983,6 +4037,7 @@ mod tests {
                 "web",
                 r#"the "Amount" in the "css:[data-test=transaction]" containing "Invoice 4711" shows 50"#,
             ),
+            ("web", r#"the "Total" shows ${captured.rows} + 1"#),
             ("calc", "display shows 8"),
             ("notepad", "document contains hello"),
         ];
@@ -5376,7 +5431,8 @@ mod scoped_target_tests {
                 .expect("parses"),
             vec![ResolvedAction::Capture {
                 target: wanted.clone(),
-                name: "total".into()
+                name: "total".into(),
+                count: false
             }]
         );
         assert_eq!(

crates/flowproof-replay/src/lib.rs

@@ -1781,7 +1781,31 @@ fn execute_step<D: AppDriver>(
                 };
                 // Read at execution time, on replay exactly as on record -
                 // which is why the value never needs to be in the trace.
-                let value = driver.read_text(&target)?;
+                // `count` picks the reading; the indirection is the same.
+                let value = if params.get("count").and_then(|v| v.as_bool()) == Some(true) {
+                    let found = flowproof_driver::count_matching(
+                        driver,
+                        &target,
+                        flowproof_driver::COUNT_DIAGNOSTIC_CAP,
+                    )?;
+                    // Unreachable while the target resolved, since a
+                    // resolved element is a first match - but stated
+                    // rather than assumed, because "0" is the one value
+                    // this capture must never quietly hand on.
+                    if found == 0 {
+                        return Ok((
+                            Err(
+                                "nothing matched, so the count would be a guess - to assert \
+                                 emptiness use 'the \"<target>\" appears 0 times'"
+                                    .to_string(),
+                            ),
+                            matched,
+                        ));
+                    }
+                    found.to_string()
+                } else {
+                    driver.read_text(&target)?
+                };
                 captures.insert(name.to_string(), value);
                 (Ok(()), matched)
             }

docs/authoring.md

@@ -48,6 +48,7 @@ before migrating a suite's setup helpers step by step.
 | `Replace the <id> field with <text>` | |
 | `Clear the [2nd ]"<label>" field` / `Clear the <id> field` | fill-with-empty semantics |
 | `Remember the [2nd ]"<target>" as <name>` | read the target's text into a flow-scoped name (`[a-z][a-z0-9_]*`) for a later assertion to compare against. The VALUE is read at execution time on record and on every replay, so it never enters the trace - the same indirection `${VAR}` secrets use. Re-using a name overwrites it |
+| `Remember how many "<target>" appear as <name>` | the COUNT of matching elements, not their text. Same family and the same indirection as the reading above: taken at execution time on record and on every replay, so a page that grew a row does not need the trace rewritten. Counting rides the ordinal every adapter implements, so it means on each adapter exactly what `the 2nd "Row"` means there. **Zero fails** - a selector typo matches nothing and so does an empty table, and `0` is a confident wrong number to hand to an app; the step that MEANS zero is `assert: the "<target>" appears 0 times`. `appears` is accepted for `appear` |
 | `Check the [2nd ]"<label>" checkbox` / `Uncheck the …` | drives a checkbox, radio, or `role=switch` to a STATE, not a toggle: `Check` on an already-checked box is a no-op, so the step means the same thing however the environment arrives. Resolves the control inside a wrapper too (the common pattern of a visually hidden `input` inside a styled label), performs a real click so the app's own handlers fire, then verifies the state took |
 | `Select <option> from the [2nd ]"<label>" field` | native `<select>`: committed via the value setter, fires `input`+`change` (React-safe). `in the` and `… dropdown` also accepted |
 | `Press the [2nd ]"<label>" button` / `Press the <id> button` | |
@@ -357,6 +358,17 @@ and it does not compose.
 A name that was never remembered fails closed, naming what was in scope,
 rather than typing the reference or an empty string.
 
+A **counted** capture is the same value with a different reading, so it
+composes with everything a captured value already does — including the
+computed comparison, which needs no second definition of what a number is:
+
+```yaml
+- Remember how many "css:.order-row" appear as rows
+- Type ${captured.rows} into the "Rowcount" field
+- Press the "Add row" button
+- assert: the "Total" shows ${captured.rows} + 1
+```
+
 Typing is where it stops. A capture may not choose an element or a
 destination - `Click "${captured.x}"`, `Go to ${captured.x}`, or a capture
 in a target label are all parse errors, because that would let the app under

docs/trace-format.md

@@ -132,6 +132,17 @@ these fields existed) is byte-identical:
   was in scope. Captures resolve before secrets, because a `${VAR}` name may
   not contain a dot.
 
+  A `capture` step carries `{"name": "<name>"}` and, for the **counted**
+  reading, `"count": true` — how many elements match, rather than one
+  element's text. A new param key rather than a new action type, so a trace
+  written before counting existed still loads and an old reader meeting one
+  does not misread it as a text capture. Either way the trace holds only the
+  name: the number is taken at execution time on record and on every replay,
+  so a page that grew a row does not need the trace rewritten. A counted
+  capture of **zero** fails rather than remembering `0` — a selector typo
+  matches nothing and so does an empty table, and the step that means zero
+  is an `assert` with `element_count: 0`.
+
   `type_text` variants: an **empty `selectors` array** means "type into the
   element that currently has keyboard focus"; `params.replace: true` marks
   fill semantics — the input's current value is cleared before typing (a