From 20fd86375f814864cafb72a465d956d512ae5877 Mon Sep 17 00:00:00 2001
From: Amin Chirazi <32016576+AminChirazi@users.noreply.github.com>
Date: Sat, 1 Aug 2026 13:32:27 +0400
Subject: [PATCH] fix(adapters): Select typed the option name when the option
 did not exist
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A JS exception inside the driver does not reach Rust as an `Err`, so the
throw on a missing option looked exactly like "this element is not a
<select>" — the one case the code below it exists to handle — and it fell
through to typing the option's name into the dropdown.

Typing into a <select> is itself a prefix search, so the step landed on
whatever option starts with the same letters and reported success. Not a
failure and not the option that was asked for: a plausible wrong answer,
chosen quietly.

The two cases are now different answers rather than the same one. A status
value comes back and is inspected: `not_select` keeps the fall-through to
typing, which is what it was always for, and a name matching nothing fails
naming it. Prefix matching is untouched — value, then exact visible text,
then prefix — so `Audit` selecting `Auditor` stays correct.

Found while building the multi-option form, whose first version had the same
defect and was caught by its own red-path test.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 CHANGELOG.md                                  |  21 ++++
 crates/flowproof-adapters/src/web.rs          |  32 ++++-
 .../tests/select_missing_option_e2e.rs        | 110 ++++++++++++++++++
 docs/authoring.md                             |   2 +-
 4 files changed, 158 insertions(+), 7 deletions(-)
 create mode 100644 crates/flowproof-cli/tests/select_missing_option_e2e.rs

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d46a50..2c753f8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -105,6 +105,27 @@ together).
 
 ### Fixed
 
+- **`Select` typed the option name when the option did not exist.** A JS
+  exception inside the driver does not reach Rust as an `Err`, so the throw
+  on a missing option looked exactly like "this element is not a
+  `<select>`" — the one case the code below it exists to handle — and it
+  fell through to typing the option's name into the dropdown.
+
+  Typing into a `<select>` is itself a prefix search, so the step landed on
+  whatever option starts with the same letters and reported success. Not a
+  failure and not the option that was asked for: a plausible wrong answer,
+  chosen quietly.
+
+  The two cases are now different answers rather than the same one. A status
+  value comes back and is inspected: `not_select` keeps the fall-through to
+  typing, which is what it was always for, and a name matching nothing fails
+  naming it. Prefix matching is untouched — it is the documented ladder
+  (value, then exact visible text, then prefix), and `Audit` selecting
+  `Auditor` is correct.
+
+  Found while building the multi-option form, whose first version had the
+  same defect and was caught by its own red-path test.
+
 - **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
diff --git a/crates/flowproof-adapters/src/web.rs b/crates/flowproof-adapters/src/web.rs
index 47c71fa..b799050 100644
--- a/crates/flowproof-adapters/src/web.rs
+++ b/crates/flowproof-adapters/src/web.rs
@@ -2287,31 +2287,51 @@ impl AppDriver for WebAppDriver {
         let handled =
             self.with_element(&locator, &format!("selecting in [{selector}]"), |element| {
                 element.call_js_fn(
+                    // A STATUS STRING, not a throw and not a bare boolean.
+                    // A JS exception does not reach Rust as an `Err` here,
+                    // so throwing on a missing option looked identical to
+                    // "this is not a <select>" - and fell through to typing
+                    // the option's name into the dropdown, which keyboard-
+                    // selects by prefix and lands on whatever starts with
+                    // the same letters. A wrong option, selected quietly.
+                    //
+                    // The two cases are now different answers: `not_select`
+                    // is the genuine fall-through to typing, `no_option` is
+                    // a failure.
                     r#"function(wanted) {
-                        if (this.tagName !== 'SELECT') { return false; }
+                        if (this.tagName !== 'SELECT') { return 'not_select'; }
                         const w = String(wanted).trim();
                         const options = Array.from(this.options);
                         const match = options.find(o => o.value === w)
                             || options.find(o => o.textContent.trim() === w)
                             || options.find(o => o.textContent.trim().startsWith(w));
-                        if (!match) {
-                            throw new Error('no <option> matches "' + w + '"');
-                        }
+                        if (!match) { return 'no_option:' + w; }
                         const desc = Object.getOwnPropertyDescriptor(
                             HTMLSelectElement.prototype, 'value');
                         if (desc && desc.set) { desc.set.call(this, match.value); }
                         else { this.value = match.value; }
                         this.dispatchEvent(new Event('input', { bubbles: true }));
                         this.dispatchEvent(new Event('change', { bubbles: true }));
-                        return true;
+                        return 'ok';
                     }"#,
                     vec![serde_json::json!(text)],
                     false,
                 )
             })?;
-        if handled.value.and_then(|v| v.as_bool()) == Some(true) {
+        let status = handled
+            .value
+            .as_ref()
+            .and_then(|v| v.as_str())
+            .unwrap_or("not_select");
+        if status == "ok" {
             return Ok(());
         }
+        if let Some(wanted) = status.strip_prefix("no_option:") {
+            return Err(DriverError::Browser(format!(
+                "no option matching '{wanted}' in [{selector}] - the options are matched by \
+                 value, then by visible text; nothing was selected"
+            )));
+        }
         self.with_element(&locator, &format!("typing into [{selector}]"), |element| {
             element.click()?.type_into(text).map(|_| ())
         })
diff --git a/crates/flowproof-cli/tests/select_missing_option_e2e.rs b/crates/flowproof-cli/tests/select_missing_option_e2e.rs
new file mode 100644
index 0000000..300898e
--- /dev/null
+++ b/crates/flowproof-cli/tests/select_missing_option_e2e.rs
@@ -0,0 +1,110 @@
+//! `Select` with an option that does not exist must FAIL, not type.
+//!
+//! A JS exception inside the driver does not reach Rust as an `Err`, so
+//! throwing on a missing option was indistinguishable from "this element is
+//! not a `<select>`" — and fell through to typing the option's name into the
+//! dropdown. Typing into a `<select>` keyboard-selects by prefix, so the
+//! step landed on whatever option starts with the same letters and reported
+//! success. A wrong option, selected quietly.
+//!
+//! The green half is here for the same reason: a fix that made every select
+//! fail would pass the red test on its own. Gated on FLOWPROOF_E2E=1.
+
+use flowproof_agent::FlowSpec;
+
+const PAGE: &str = r#"<!doctype html>
+<html><head><meta charset="utf-8"><title>Roles</title></head><body>
+  <select id="role">
+    <option>Admin</option>
+    <option>Auditor</option>
+    <option>Viewer</option>
+  </select>
+  <input id="free" placeholder="free text">
+  <div id="out">none</div>
+  <script>
+    document.getElementById('role').addEventListener('change', function () {
+      document.getElementById('out').textContent = 'SEL:' + this.value;
+    });
+  </script>
+</body></html>
+"#;
+
+fn fixture(dir: &std::path::Path) -> String {
+    std::fs::create_dir_all(dir).expect("temp dir");
+    let page = dir.join("roles.html");
+    std::fs::write(&page, PAGE).expect("page written");
+    format!("file://{}", page.display())
+}
+
+/// The red path: an option that matches NOTHING on the ladder.
+///
+/// Note what is deliberately absent here. `Audit` is not one of these,
+/// because prefix matching is documented behaviour — value, then exact
+/// visible text, then prefix — so `Audit` legitimately selects `Auditor`.
+/// The bug was never about prefixes; it was that a name matching nothing
+/// at all fell through to typing, and typing into a `<select>` is itself a
+/// prefix search, so the step landed on some other option and passed.
+#[test]
+fn selecting_an_option_that_does_not_exist_fails_instead_of_typing() {
+    if std::env::var("FLOWPROOF_E2E").as_deref() != Ok("1") {
+        eprintln!("skipping select E2E: set FLOWPROOF_E2E=1 to run it");
+        return;
+    }
+    let dir = std::env::temp_dir().join("flowproof-select-missing-e2e");
+    let url = fixture(&dir);
+    let trace = dir.join("missing.trace.jsonl");
+
+    for missing in ["Telepathy", "Zzz Nonexistent"] {
+        let spec = FlowSpec::parse(&format!(
+            "name: Missing\napp: web\nurl: {url}\nsteps:\n  \
+             - Select {missing} from the \"id:role\" field\n"
+        ))
+        .expect("spec parses");
+        let mut driver = flowproof_cli::driver_for("web").expect("browser launches");
+        let err = flowproof_agent::record(&spec, &mut driver, &trace)
+            .expect_err("a missing option must fail the recording");
+        let message = err.to_string();
+        assert!(
+            message.contains("no option matching"),
+            "{missing}: the failure must name the missing option: {message}"
+        );
+        drop(driver);
+    }
+
+    std::fs::remove_dir_all(&dir).ok();
+}
+
+/// The other direction, so the fix cannot be "make selecting fail": a real
+/// option still commits and fires `change`, a prefix that IS unambiguous
+/// still resolves, and typing into an ordinary input still falls through to
+/// typing — which is what the `not_select` answer exists to preserve.
+#[test]
+fn a_real_option_still_selects_and_ordinary_typing_still_types() {
+    if std::env::var("FLOWPROOF_E2E").as_deref() != Ok("1") {
+        eprintln!("skipping select E2E: set FLOWPROOF_E2E=1 to run it");
+        return;
+    }
+    let dir = std::env::temp_dir().join("flowproof-select-ok-e2e");
+    let url = fixture(&dir);
+    let trace = dir.join("ok.trace.jsonl");
+
+    let spec = FlowSpec::parse(&format!(
+        "name: Selects\napp: web\nurl: {url}\nsteps:\n  \
+         - Select Auditor from the \"id:role\" field\n  \
+         - assert: page shows SEL:Auditor\n  \
+         - Type hello into the \"id:free\" field\n  \
+         - assert: the \"id:free\" field contains hello\n"
+    ))
+    .expect("spec parses");
+
+    let mut driver = flowproof_cli::driver_for("web").expect("browser launches");
+    let summary = flowproof_agent::record(&spec, &mut driver, &trace).expect("recording succeeds");
+    assert_eq!(summary.steps, 4);
+    drop(driver);
+
+    let mut driver = flowproof_cli::driver_for("web").expect("browser launches");
+    let (report, _) = flowproof_replay::run_trace(&trace, &mut driver).expect("replay runs");
+    assert!(report.passed, "select must replay: {report:#?}");
+
+    std::fs::remove_dir_all(&dir).ok();
+}
diff --git a/docs/authoring.md b/docs/authoring.md
index c516271..dbde00d 100644
--- a/docs/authoring.md
+++ b/docs/authoring.md
@@ -50,7 +50,7 @@ before migrating a suite's setup helpers step by step.
 | `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 |
+| `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. The option is matched by `value`, then exact visible text, then prefix - so `Audit` finds `Auditor`. A name matching NONE of those fails naming it, rather than falling through to typing (typing into a `<select>` is a prefix search of its own, so it would land on some other option and pass) |
 | `Select "<A>", "<B>" and "<C>" from the [2nd ]"<label>" field` | a `<select multiple>`, driven to EXACTLY the named set in one commit with one `input`+`change` - what the app's own handler expects to see is a user finishing a selection, not three of them. Set-a-state like `Check`, not a toggle: what is named becomes selected and what is not named does not, so the step means the same thing however the environment arrived. **Every item is quoted**, because option text is arbitrary app text - `"Rock, Paper and Scissors"` is one option, and an unquoted list could not tell it from three. Names are resolved before anything is selected, so a typo in the third option leaves the control untouched rather than half-applied, and the step then verifies the selection took. Web only |
 | `Press the [2nd ]"<label>" button` / `Press the <id> button` | |
 | `Right-click [the [2nd ]]"<text>"` | opens the element's context menu; `Right click` also accepted |