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

[AminChirazi]

What was wrong

Repetition and branching were refused, on the grounds that a trace must be a
recording of what happened and 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.

What holds now

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 — ordinary concrete steps, no
repeat and no when. Replay reads a flat list and still decides nothing.

- 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

foreach already made this bargain one phase earlier, at parse time — which it
can only do because its list is known before anything runs.

If the condition never holds within max:, recording fails and names the bound
rather than pressing forever. Each repeat: carries its own budget, so two loops
in one flow do not share one.

Conditions read state and never wait: page [does not] show <text>,
the "<target>" shows <text>, the "<target>" is [not] visible. Anything else
is refused by name rather than guessed at.

The step-shaped refusals (Click "Next" until …, If … , …) stay, and now name
the block that does the job — a refusal whose alternative is real is the one
worth keeping.

Proof

Two pages of a public obstacle web page, recorded and replayed green:

• obstacle 81121 — press until the label changes. Recorded 8 passes under a
  pinned seed; replays deterministically. Unpinned it does not replay, and the
  failure is the honest one: the page redraws a fresh random bound, so the extra
  press lands on a modal. Pinning randomness is what makes a recorded loop mean
  something on the next run.
• obstacle 70924 — a counter that resets to zero whenever the button faults,
  which is repeat: with a when: recovery inside it. The trace is 18 presses:
  three faults recovered, then a clean run of ten. Flat, and readable top to
  bottom.

Both conditions had to be scoped to an element rather than the page. page shows Enough and page shows ERROR both matched the page's own description text —
the second one fired the recovery on every pass and drove the loop into its
bound, which is exactly what the bound is for. That trap is documented.

Tests

• a repeat: records the passes that actually ran — two, not a loop and not the
  max of five — and the trace contains no control flow
• a repeat: that never settles stops at its bound and names it
• a when: whose condition is false records nothing
• repeat:/when: survive a YAML round trip; when: serializes back flat
• a repeat: missing until: or max: is rejected; a bare when: is told the
  shape it should have had

cargo fmt --check, cargo clippy --workspace --all-targets -D warnings and
cargo test --workspace (57 suites) are green. Ratchets: rust tests 792 → 796,
diff 399 lines.

Not in this PR

Obstacle 73589 is a hand-driven bubble sort — the decision at each position is
"is the left number greater than the right", and conditions have no numeric
comparison. That predicate, and the corpus status doc it would update, follow
next.

[Copilot]

Pull request overview

This PR extends the flow authoring grammar with recording-time-only control-flow blocks (repeat: and when:) so authors can express “press until it settles” / “run recovery if error is visible” while still emitting a flat, deterministic trace for replay.

Changes:

• Added repeat: and when: step shapes to the YAML spec model, including strict parsing/serialization and round-trip tests.
• Implemented recording-time expansion in the recorder so only the concrete steps that actually ran are written into the trace.
• Updated refusals, docs, and changelog to reflect the new block-level approach (loops/branches remain refused as step-shaped prose).

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
docs/authoring.md	Documents repeat:/when: semantics and updates the “Refused shapes” guidance to point at the new blocks.
crates/flowproof-agent/src/spec.rs	Adds SpecStep::Repeat / SpecStep::When, their structs, YAML parsing/serialization, and spec-level tests.
crates/flowproof-agent/src/rules.rs	Updates declined-shape error messaging and corresponding tests to reference repeat:/when:.
crates/flowproof-agent/src/recorder.rs	Implements recording-time expansion and adds recorder tests proving traces remain flat and bounded.
CHANGELOG.md	Adds a changelog entry explaining the motivation and guarantee (“expanded while recording, trace stays flat”).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.