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