From 3985e33e895525e44c20a77af812f5f05dfd79d0 Mon Sep 17 00:00:00 2001 From: Amin Chirazi <32016576+AminChirazi@users.noreply.github.com> Date: Sat, 1 Aug 2026 12:32:16 +0400 Subject: [PATCH] docs(grammar): a typed capture is interpolated, not evaluated MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit authoring.md showed one form — `Type ${captured.oid} into the …` — and said the value is read fresh on every replay. It did not say that several references resolve in one step, that literal text between them is typed as written, or that none of it is evaluated. So `Type ${captured.a} + ${captured.b} into the "Sum" field` types `12 + 30`. That is interpolation working as designed, and it is also close enough to an answer that a flow can go green on it while asserting nothing anybody meant — on the page that reads like the complete account of captures. No behaviour change. The non-arithmetic is now stated outright, with the reason: a capture is text the app displayed and handing it back is data entry, while deriving a value from two of them is a computation, and a trace carrying a computation has stopped being a recording. Pinned by a test that asserts `12 + 30`, so arithmetic can only ever arrive as a spelling that cannot be mistaken for this one. Co-Authored-By: Claude Opus 5 --- CHANGELOG.md | 24 +++++++++++++++++ crates/flowproof-agent/src/rules.rs | 12 +++++++++ crates/flowproof-trace/src/captures.rs | 27 +++++++++++++++++++ docs/authoring.md | 37 ++++++++++++++++++++++++++ 4 files changed, 100 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e89aa41..7edca40 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,30 @@ together). ### Fixed +- **The docs never said what a typed capture does with the text around + it.** `authoring.md` showed one form, `Type ${captured.oid} into the …`, + and said the value is read fresh on every replay. It did not say that + several references resolve in one step, that literal text between them is + typed as written — or, the part that matters, that none of it is + evaluated. + + So `Type ${captured.a} + ${captured.b} into the "Sum" field` types + `12 + 30`. That is interpolation working exactly as designed. It is also + close enough to an answer that a flow can go green on it while asserting + nothing anybody meant, and the page that reads like the complete account + of captures did not mention it. + + Documented now, with the non-arithmetic stated outright and the reason: + a capture is text the app displayed, and handing it back is data entry; + deriving a new value from two of them is a computation, and a trace + carrying a computation has stopped being a recording. The one exception + stays where it was — `shows ${captured.x} + ` on the assertion + side, which answers "did this change by the right amount?", a question no + literal can express. + + Pinned by a test that asserts `12 + 30`, so if arithmetic is ever added it + has to arrive as a spelling that cannot be mistaken for this one. + - **A step the grammar had decided not to have was built by the model instead.** `record` resolves with rules first and hands anything they cannot parse to the LLM author. That is right for a step nobody has taught diff --git a/crates/flowproof-agent/src/rules.rs b/crates/flowproof-agent/src/rules.rs index 36415f8..befb3c2 100644 --- a/crates/flowproof-agent/src/rules.rs +++ b/crates/flowproof-agent/src/rules.rs @@ -3865,6 +3865,18 @@ mod tests { "web", r#"Remember the "Amount" in the item containing "Invoice 4711" as amount"#, ), + // Interpolation: several references in one step, and literal + // text around them. Documented under "A typed value is + // interpolated, not evaluated". + ("web", r#"Type order-${captured.oid} into the "Ref" field"#), + ( + "web", + r#"Type ${captured.first} ${captured.last} into the "Name" field"#, + ), + ( + "web", + r#"Type ${captured.a} + ${captured.b} into the "Sum" field"#, + ), ( "web", r#"Right-click the "Pay" in the item containing "Invoice 4711""#, diff --git a/crates/flowproof-trace/src/captures.rs b/crates/flowproof-trace/src/captures.rs index c27d786..e7de1f9 100644 --- a/crates/flowproof-trace/src/captures.rs +++ b/crates/flowproof-trace/src/captures.rs @@ -95,6 +95,33 @@ mod tests { /// contain a dot so the secret resolver left it alone. Silently entering /// the wrong value is the worst outcome available, so an unknown name is /// an error that names what IS in scope. + /// The documented claim, pinned: a typed capture is INTERPOLATED, not + /// evaluated. `12 + 30` is three tokens of displayed text, and the + /// reason it is worth a test of its own is that it looks close enough + /// to an answer for a flow to go green on it while asserting nothing + /// anybody meant. If arithmetic is ever added it must be a spelling + /// that cannot be confused with this one, and this test is what says so. + #[test] + fn a_typed_capture_is_interpolated_and_never_evaluated() { + let c = scope(&[("a", "12"), ("b", "30")]); + assert_eq!( + substitute("${captured.a} + ${captured.b}", &c).expect("both resolve"), + "12 + 30", + "interpolation substitutes; it does not compute" + ); + // Literal text around a reference is typed as written, and several + // references in one step each resolve. + let c = scope(&[("first", "Grace"), ("last", "Hopper"), ("oid", "1061367")]); + assert_eq!( + substitute("${captured.first} ${captured.last}", &c).expect("both resolve"), + "Grace Hopper" + ); + assert_eq!( + substitute("order-${captured.oid}", &c).expect("resolves"), + "order-1061367" + ); + } + #[test] fn an_unremembered_name_is_an_error_that_lists_the_scope() { let err = substitute("${captured.typo}", &scope(&[("oid", "1"), ("amount", "2")])) diff --git a/docs/authoring.md b/docs/authoring.md index 69f6ba5..88bea32 100644 --- a/docs/authoring.md +++ b/docs/authoring.md @@ -320,6 +320,43 @@ stores the reference and every replay reads the value fresh: - Type ${captured.oid} into the "Order id" field ``` +**A typed value is interpolated, not evaluated.** Every `${captured.}` +in the text is replaced by what that element displayed, and the literal +characters around them are typed as written: + +```yaml +- Type order-${captured.oid} into the "Ref" field # order-1061367 +- Type ${captured.first} ${captured.last} into the "Name" field +``` + +More than one reference in one step is fine, and so is a step that is all +literal apart from them. What does **not** happen is arithmetic. This: + +```yaml +- Remember the "id:no1" as a +- Remember the "id:no2" as b +- Type ${captured.a} + ${captured.b} into the "Sum" field +``` + +types `12 + 30` — three tokens of displayed text with a plus sign between +them — and not `42`. That is interpolation behaving correctly, not a bug, +and it is the reason the step is worth spelling out: `12 + 30` looks close +enough to an answer that a flow could go green on it while asserting +nothing anybody meant. + +Arithmetic is refused deliberately, not merely absent. A capture is *text +the app displayed*, and supplying it back is data entry — the thing a user +does with a generated id. Deriving a new value from two of them is a +computation, and a trace that carries a computation has stopped being a +recording of what happened. The one exception is on the assertion side, +where `shows ${captured.x} + ` answers "did this change by the +right amount?" — a question a literal cannot express, because the starting +value is only known at run time. It takes one capture and one plain number, +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. + 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