flow: an unknown versions target_surface is not_checked; QUESTIONS.md shows a missing version check

packages/flow/docs/GENERATE_CONTRACTS.md

@@ -347,7 +347,8 @@ saves. Only the main record is a target (`target_surface`). A target
 the read before the write doesn't show as new is treated as existing, and
 with no version before the write it stops as `missing` (a record saved
 before the trail began, or outside the app). With neither, the update has no
-version check, and `report.json` shows `versions: null`. If the app stops
+version check: `report.json` shows `versions: null`, and `QUESTIONS.md`
+says so under the kind. If the app stops
 writing the trail (an agenda setting turned off), the agent's own save has
 no new version, and the verifier stops the write rather than pass it.
 

packages/flow/docs/VERIFY_RUN.md

@@ -533,9 +533,11 @@ only a whole-number version's value is kept, to count steps. The receipt's
 `evidence.frame.versions` holds counts and a problem code (`another_author`,
 `extra_steps`, `went_back`, `no_author`, `not_a_number`, `null_version`,
 `duplicate_version`, `no_new_version`, `history_changed`, `missing`,
-`no_target_id`, `unreadable`, `self_unresolved`), never ids or values. A
-refuted check refutes the frame (`checked.frame: refuted`); one that can't be
-judged leaves the frame `not_checked`.
+`no_target_id`, `unreadable`, `self_unresolved`, `unknown_surface`), never
+ids or values. A refuted check refutes the frame (`checked.frame: refuted`);
+one that can't be judged leaves the frame `not_checked`. A `target_surface`
+that no write effect reads is `unknown_surface`: with no target there is
+nothing to hold.
 
 ## What the receipt says was checked
 

packages/flow/openadapt_flow/generate/verify_contract.py

@@ -3900,6 +3900,19 @@ def _questions_md(
                 + ". A task that gives one is stopped: record a demonstration "
                 "that gives it now, before tasks need it."
             )
+        if (
+            rep["mode"] == "update"
+            and "versions" in rep
+            and rep["versions"] is None
+            and not rep["refused"]
+        ):
+            lines.append(
+                "  - No version check: the main table has no version column and "
+                "no audit trail names the record and the acting user in every "
+                "demonstration, so another user's save to the same record in the "
+                "window (a lost update) is not seen. Write `frame.versions` by "
+                "hand if the app keeps versions somewhere else."
+            )
         for r in rep["refused"]:
             lines.append(f"  - Refused: {r}")
         for r in rep["rejected"][:5]:

packages/flow/openadapt_flow/runtime/effects/versions.py

@@ -58,6 +58,7 @@
     "duplicate_version",
     "no_new_version",
     "history_changed",
+    "unknown_surface",
 )
 
 _WHOLE = re.compile(r"^(0|[1-9][0-9]*)$")

packages/flow/openadapt_flow/verify_run.py

@@ -524,7 +524,7 @@ def _judge_versions(
     window that isn't the agent's own refutes it; one that can't be read or
     attributed leaves it not checked."""
 
-    from openadapt_flow.runtime.effects.versions import judge_versions
+    from openadapt_flow.runtime.effects.versions import VersionVerdict, judge_versions
 
     spec = cfg.frame.versions if cfg.frame is not None else None
     if spec is None:
@@ -557,13 +557,21 @@ def before_rows(effect: Effect) -> Optional[dict[str, dict[str, Any]]]:
             return index(rows) if isinstance(rows, list) else None
         return index(before.records) if before.reachable else None
 
+    def writes_a_target(effect: Effect) -> bool:
+        """A write effect whose records can be targets. A guard ("nothing
+        here", ``record_written`` with ``expected_count`` 0) never is."""
+
+        if effect.kind not in (EffectKind.RECORD_WRITTEN, EffectKind.FIELD_EQUALS):
+            return False
+        return not (
+            effect.kind is EffectKind.RECORD_WRITTEN and effect.expected_count == 0
+        )
+
     ignored = set(cfg.frame.ignore_fields)  # type: ignore[union-attr]
     targets: list[tuple[Optional[str], bool, bool]] = []
     for effect, verdict in zip(effects, verdicts):
-        if effect.kind not in (EffectKind.RECORD_WRITTEN, EffectKind.FIELD_EQUALS):
+        if not writes_a_target(effect):
             continue
-        if effect.kind is EffectKind.RECORD_WRITTEN and effect.expected_count == 0:
-            continue  # a guard: "nothing here"
         if not verdict.confirmed:
             continue
         if (
@@ -588,14 +596,27 @@ def before_rows(effect: Effect) -> Optional[dict[str, dict[str, Any]]]:
             )
             targets.append((text, existed, changed))
     stored = (before.detail or {}).get(FRAME_VERSIONS_DETAIL)
-    result = judge_versions(
-        spec,
-        stored if isinstance(stored, Mapping) else {},
-        _read_versions(cfg, params),
-        targets,
-        _mac_key(salt),
-        params,
-    )
+    if spec.target_surface is not None and not any(
+        writes_a_target(e) and surface_of(e) == spec.target_surface for e in effects
+    ):
+        # A surface no write target is read from (a typo in a hand-written
+        # contract, or a surface only a guard reads) would leave no target,
+        # and no target holds.
+        result = VersionVerdict(
+            "not_checked",
+            "unknown_surface",
+            reason="frame.versions.target_surface names a surface no write "
+            "target is read from, so no target's versions can be judged",
+        )
+    else:
+        result = judge_versions(
+            spec,
+            stored if isinstance(stored, Mapping) else {},
+            _read_versions(cfg, params),
+            targets,
+            _mac_key(salt),
+            params,
+        )
     frame.versions = result
     if result.status == "refuted":
         frame.status = "refuted"

packages/flow/tests/test_frame_versions.py

@@ -345,3 +345,89 @@ def test_r2_i2_a_target_field_the_write_changes_is_not_a_new_record(
     )
     assert result["receipt"]["outcome"] != "verified"
     assert _versions(result)["problem"] == "missing"
+
+
+@pytest.mark.parametrize("window", [_correct, _lost_update], ids=["correct", "lost"])
+def test_a_target_surface_no_effect_reads_is_not_checked(
+    tmp_path: Path, window: Callable[[sqlite3.Connection], None]
+) -> None:
+    # A misspelt surface would leave no target, and zero targets held: a
+    # lost update was verified.
+    result = _run(tmp_path, window, {"target_surface": "recrod"})
+    assert _versions(result)["status"] == "not_checked"
+    assert _versions(result)["problem"] == "unknown_surface"
+    assert result["receipt"]["checked"]["frame"] == "not_checked"
+    assert result["receipt"]["outcome"] != "verified"
+
+
+def _guarded(doc: dict[str, Any], db: Path) -> dict[str, Any]:
+    """``doc`` read through two surfaces: the target write on ``record``, and
+    a guard ("no row has the bot's phone twice") alone on ``guard``."""
+
+    sql = {"kind": "sql", "sqlite_database": str(db)}
+    doc["verifier"] = {
+        "kind": "surfaces",
+        "surfaces": {
+            "record": {**sql, "sql_query": "SELECT * FROM person"},
+            "guard": {**sql, "sql_query": "SELECT * FROM person WHERE id = 2"},
+        },
+    }
+    [write] = doc["effects"]
+    doc["effects"] = [
+        {**write, "probe": "surface=record|the phone is saved"},
+        {
+            "kind": "record_written",
+            "probe": "surface=guard|the other record keeps its phone",
+            "match": {"id": "2", "phone": {"param": "phone"}},
+            "expected_count": 0,
+        },
+    ]
+    return doc
+
+
+def _run_guarded(
+    tmp_path: Path,
+    window: Callable[[sqlite3.Connection], None],
+    target_surface: str,
+) -> dict[str, Any]:
+    tmp_path.mkdir(parents=True, exist_ok=True)
+    db = tmp_path / "app.sqlite"
+    con = sqlite3.connect(db)
+    con.executescript(SCHEMA)
+    con.commit()
+    doc = _guarded(_doc(db, {"target_surface": target_surface, **AUTHORS}), db)
+    cfg = parse_verify_config(doc)
+    capture_baseline(cfg, PARAMS, tmp_path / "baseline.json")
+    window(con)
+    con.commit()
+    con.close()
+    return verify_run(
+        cfg,
+        params=PARAMS,
+        run_record={"executor_kind": "agent", "executor_id": "bot"},
+        authorization_ref="test",
+        baseline_path=tmp_path / "baseline.json",
+    )
+
+
+@pytest.mark.parametrize("window", [_correct, _lost_update], ids=["correct", "lost"])
+def test_a_target_surface_only_a_guard_reads_is_not_checked(
+    tmp_path: Path, window: Callable[[sqlite3.Connection], None]
+) -> None:
+    # A guard's records are never targets, so its surface leaves no target,
+    # and zero targets held: a lost update was verified.
+    result = _run_guarded(tmp_path, window, "guard")
+    assert _versions(result)["status"] == "not_checked"
+    assert _versions(result)["problem"] == "unknown_surface"
+    assert result["receipt"]["checked"]["frame"] == "not_checked"
+    assert result["receipt"]["outcome"] != "verified"
+
+
+def test_the_write_surface_beside_a_guard_is_still_judged(tmp_path: Path) -> None:
+    # Control: the same contract aimed at the write's surface judges the
+    # target, and the other user's save in the window refutes it.
+    lost = _run_guarded(tmp_path / "lost", _lost_update, "record")
+    assert _versions(lost)["status"] == "refuted"
+    assert lost["receipt"]["outcome"] != "verified"
+    correct = _run_guarded(tmp_path / "correct", _correct, "record")
+    assert _versions(correct)["status"] == "held"

packages/flow/tests/test_generate_verify_contract_attacks_r3.py

@@ -318,3 +318,30 @@ def check(role: str) -> list[str]:
     ro4 = check("ro4")
     assert any("has UPDATE on table public.t" in p for p in ro4), ro4
     assert check("ro6") == []
+
+
+def test_an_update_with_no_version_check_says_so_in_questions() -> None:
+    from openadapt_flow.generate.verify_contract import _questions_md
+
+    def kind(mode: str, versions: Any, refused: list[str]) -> dict[str, Any]:
+        return {
+            "mode": mode,
+            "main_table": "t",
+            "emitted": 1,
+            "versions": versions,
+            "refused": refused,
+            "rejected": [],
+        }
+
+    report = {
+        "kinds": {
+            "bare": kind("update", None, []),
+            "stepped": kind("update", {"kind": "step"}, []),
+            "made": kind("create", None, []),
+            "stopped": kind("update", None, ["no identity"]),
+        }
+    }
+    text = _questions_md([], {}, report)
+    sections = text.split("- `")[1:]
+    said = {s.split("`", 1)[0]: "No version check" in s for s in sections}
+    assert said == {"bare": True, "stepped": False, "made": False, "stopped": False}