docs(grammar): a typed capture is interpolated, not evaluated

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} + <number>` 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

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""#,

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")]))

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.<name>}`
+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} + <number>` 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