feat(flow): build a working record check from the app's own reads

packages/flow/benchmark/effect_e2e/prove_check.py

@@ -0,0 +1,74 @@
+"""The effect_e2e record service as a fixture for proving a proposed check.
+
+``openadapt-flow scaffold-verifier --prove effect-e2e`` runs a proposed record
+check through the real replayer against this service, one run per fault in
+:data:`benchmark.effect_e2e.run.SCENARIOS`, judged by this harness's
+independent ground truth (a read-only connection to the SQLite file that never
+sees the check). See :mod:`openadapt_flow.record_check_proof`.
+"""
+
+from __future__ import annotations
+
+import tempfile
+from pathlib import Path
+from typing import Any, Callable, Mapping, Optional
+
+import requests
+
+from benchmark.effect_e2e import ground_truth
+from benchmark.effect_e2e.record_service import TARGET_PATIENT, TARGET_TYPE, serve
+from benchmark.effect_e2e.run import SCENARIOS
+from openadapt_flow.record_check_proof import Fixture
+
+
+class _Handle:
+    def __init__(
+        self, base_url: str, db_path: Path, tmp: tempfile.TemporaryDirectory
+    ) -> None:
+        self.base_url = base_url
+        self.db_path = db_path
+        self.tmp = tmp
+
+
+def _serve() -> tuple[str, Optional[Path], Callable[[], None], Any]:
+    tmp = tempfile.TemporaryDirectory(prefix="record-check-proof-")
+    db_path = Path(tmp.name) / "record.db"
+    service = serve(db_path)
+    handle = _Handle(service.base_url, db_path, tmp)
+
+    def stop() -> None:
+        service.stop()
+        tmp.cleanup()
+
+    return service.base_url, db_path, stop, handle
+
+
+def _reset(handle: _Handle, seed: bool) -> None:
+    requests.post(
+        f"{handle.base_url}/api/reset", json={"seed_concurrent": seed}, timeout=5.0
+    )
+
+
+def _judge(
+    before: ground_truth.Snapshot,
+    after: ground_truth.Snapshot,
+    params: Mapping[str, str],
+) -> tuple[bool, str]:
+    verdict = ground_truth.judge(before, after, intended_note=params.get("note", ""))
+    return verdict.correct, verdict.fault_class
+
+
+FIXTURE = Fixture(
+    name="effect-e2e",
+    serve=_serve,
+    reset=_reset,
+    snapshot=lambda handle: ground_truth.capture(handle.db_path),
+    judge=_judge,
+    scenarios=tuple((sc.name, sc.seed_concurrent) for sc in SCENARIOS),
+    write_path="/api/encounter",
+    default_body={
+        "patient_id": TARGET_PATIENT,
+        "type": TARGET_TYPE,
+        "note": "{note}",
+    },
+)

packages/flow/claims.yaml

@@ -334,6 +334,72 @@ claims:
         additional opt-in live-OpenEMR test. Per-verifier claims are exactly
         as strong as these tests.
 
+  # ------------------- record checks built from the app's own reads
+  - id: record-check-from-app-reads
+    claim: >-
+      scaffold-verifier builds a record check from the reads the app made
+      after the save (the recording's network capture, a SQLite database read
+      path, or a reviewed verifier section), binds the recorded values to run
+      parameters, guards every other table when a database path is given (no
+      row added, changed or removed), and tests the check against injected
+      bad writes before anyone reviews it. A check that misses one is written as a draft
+      with the misses listed. Every effect stays unconfirmed until a person
+      removes the flag.
+    surfaces: [docs]
+    tier: supported
+    evidence:
+      - path: tests/test_record_check_synthesis.py
+        node: test_database_read_path_covers_every_table_and_passes_the_suite
+        proves: >-
+          On the benchmark/effect_e2e record service, a check built from a
+          database read path catches every injected bad write end to end
+          through the real replayer (including the stray billing write) and
+          passes the clean save.
+      - path: tests/test_record_check_synthesis.py
+        node: test_one_rest_read_misses_the_billing_write_and_stays_a_draft
+        proves: >-
+          A check built from one REST read misses the stray billing write,
+          both in the recorded-state fault test and end to end, and is
+          written as a draft with that miss listed.
+      - path: tests/test_record_check_synthesis.py
+        node: test_mockmed_needs_a_declared_complete_read
+        proves: >-
+          On the MockMed --break-it fault server, the check built from the
+          app's /api/db read catches every fault end to end once a person
+          declares the read complete, and stays a draft until then.
+      - path: tests/test_record_check_synthesis.py
+        node: test_openemr_fhir_check_refutes_store_level_faults
+        proves: >-
+          On the OpenEMR-shaped FHIR R4 fake, the check found from the
+          Observation search refutes partial, duplicate, phantom,
+          wrong-patient and lost-update faults and confirms the clean save.
+      - path: tests/test_record_check_synthesis.py
+        node: test_guards_catch_a_changed_or_deleted_row_through_the_real_read
+        proves: >-
+          The generated SQL reads, run against a real SQLite file, refute a
+          save that also changed or deleted a row in another table.
+      - path: tests/test_record_check_synthesis.py
+        node: test_verify_run_refuses_until_a_person_removes_the_flags
+        proves: >-
+          verify-run refuses the proposed check until every
+          needs_operator_confirmation line is removed.
+      - path: docs/EFFECT_KIT.md
+        proves: >-
+          The operator guide: inputs, outputs, the fault classes, and what
+          the proof does not cover.
+    caveats:
+      - >-
+        Proven on synthetic fixtures only (MockMed, the effect_e2e SQLite
+        record service, an OpenEMR-shaped FHIR fake). A check built from API
+        reads alone cannot see writes to tables it does not read, so it stays
+        a draft unless a database path covers them or a person declares the
+        read complete. The fault classes are the effect_e2e taxonomy, not a
+        measured field incident rate.
+      - >-
+        Saves that update an existing record are not handled yet: the check
+        expects one new record. The read's credential is the operator's job;
+        the recording's reads used the browser's sign-in.
+
   - id: ui-readback-separate-session
     claim: >-
       With no API or database access, a save can be checked through the
@@ -410,6 +476,10 @@ claims:
         MINORITY of clicks (4 of 12 on a recent live OpenEMR bundle); an
         UNARMED click proceeds with no identity check whatsoever. Coverage is
         an auditable per-step metric, but disclosure does not close the gap.
+        `scaffold-verifier --bundle` reports coverage before and after
+        evidence from the recording's DOM / accessibility text at each
+        unarmed click; it proposes only evidence the runtime checks on that
+        surface, and a person applies it.
 
   # -------------------------- compiler-emitted identifier crops (pixel tier)
   - id: identifier-crop-compile-emission

packages/flow/docs/EFFECT_KIT.md

@@ -262,6 +262,151 @@ Both reads are kept in `sor_snapshots.json` (mode 0600, raw records). The
 proposed file is also mode 0600 and copies `verifier:` as written, with
 `${NAME}` references unexpanded. Without `--verify`, `record` is unchanged.
 
+## A record check built from the app's own reads (`scaffold-verifier`)
+
+After a save, the app usually reads the saved record back to show it. That
+read is the record check, already written by the app. `openadapt-flow
+scaffold-verifier <recording>` finds it, builds the check, and tries to break
+it before a person reviews it.
+
+```bash
+openadapt-flow scaffold-verifier rec/                      # network capture only
+openadapt-flow scaffold-verifier rec/ --db app.sqlite      # plus every table
+openadapt-flow scaffold-verifier rec/ --verifier verify.yaml --bundle bundle/
+openadapt-flow scaffold-verifier rec/ --db app.sqlite --prove effect-e2e
+```
+
+### Finding the read
+
+The recording's parameter values (`meta.json`) identify the saved record.
+The command looks for a read that returns a record holding them:
+
+- **Network capture.** `network.jsonl` in the `openadapt.network-capture/1`
+  format that `record --capture-network` writes. Each `GET` after the save
+  (by the recording's timeline) whose JSON response holds a record list is a
+  candidate: a REST list (`{"records": [...]}`, `{"data": [...]}`, a bare
+  list) or a FHIR `Bundle`. The read whose record holds the most recorded
+  values wins; a persisted record (one with an `id`) beats an echo of the
+  form. A read whose URL carries a session token, or whose values sit only in
+  nested fields, is rejected and reported.
+- **A database read path** (`--db`, SQLite). Every table is scanned. A table
+  with a row holding the recorded values is read, scoped by the recorded
+  identifiers (`WHERE patient_id = :patient_id`). Every other table gets a
+  no-new-rows guard.
+- **A verifier section** (`--verifier verify.yaml`). The `verifier:` section
+  is read once. With `sor_snapshots.json` from `record --verify`, its
+  before read becomes the baseline.
+
+### What the check holds
+
+- The `verifier:` section is `kind: surfaces`: one read per table or
+  resource. Each effect names its read in `probe` (`surface=<name>`), and a
+  bad write is judged only against the read that can see it.
+- For each read that holds the saved record: a `record_written` effect for
+  exactly one NEW record (`count_new_only`), matched on every field equal to
+  a recorded value (bound as `{param: NAME}`, so each run is checked against
+  its own values) and on fields the save sent with a fixed value under the
+  same name (`type: Triage`). `forbid_collateral_loss` stops the run if a
+  record that was there before is gone.
+- Recorded values in the read's URL become placeholders (`path_params`,
+  FHIR `search_param_exprs`), so the read is scoped to the run's record. A
+  path segment that looks like one record's id (an MRN, a number, a UUID)
+  and is not a recorded value keeps the check a draft: it would read the
+  demonstration's record every run. Such segments show as `*` in names and
+  messages.
+- For each other table (database path only): a guard that no row is added.
+- A read whose records carry an `id` gets a second read, `<name>.content`,
+  with `records_drop_fields: [id]`. The first read counts new records by id,
+  so a stray row identical to an existing one still counts. The content read
+  compares records by their fields, so a save that changes or deletes another
+  record (same id, new content) stops the run.
+
+### Proving it before review
+
+Two tests, both written to `record_check.proof.json`:
+
+1. **Recorded-state faults** (always). The fault classes of
+   `benchmark/effect_e2e` are applied to the records the recording saw:
+   nothing saved, a field dropped, saved twice, saved on another record,
+   another record of the same subject destroyed, and a stray row in another
+   table, plus another record changed or deleted. The check must stop each
+   one and pass the clean save. A fault the check can't be tested on counts
+   as a miss: if every checked field identifies the subject, another record
+   of the same subject looks like the saved one, so "destroyed" is a miss.
+   Every generated read is built, and each `--db` read is run and compared
+   with the scan, so a read that can't work is a miss too.
+2. **End to end** (`--prove mockmed` or `--prove effect-e2e`). On a fixture
+   that injects bad writes at the persistence boundary, each fault runs
+   through the real replayer and API actuator with the proposed check as the
+   effect verifier, judged by the fixture's own ground truth. Free-text values
+   change on every run, so a check that froze the demonstration's values fails
+   the clean save.
+
+A check that misses any fault, or stops the clean save, is written as a
+draft: the file starts with `# DRAFT`, lists each `MISS:`, and the command
+exits 1. So does a check with a write request no read covers, or a table
+`--db` couldn't read (an irregular name, more than 20,000 rows). A working
+check exits 0.
+
+The save is timed from its own write request. The recorder stamps a step
+after the screen settles, so the save's request and the app's read-back come
+before the Save step's time. Reads before the first save request are the
+baseline; reads after the last one are candidates.
+
+On the effect_e2e service, a check built from one REST read (`/api/records`)
+misses the stray billing write, the same blind spot as the REST arm in
+[`EFFECT_E2E.md`](../benchmark/effect_e2e/EFFECT_E2E.md), so it stays a
+draft. With `--db`, the billing guard catches it and every fault is stopped.
+
+A check built from API reads alone can't see tables it doesn't read. If one
+store really holds everything the save can change (MockMed's `/api/db`), a
+person can say so with `--complete-read`. The proof records that as
+`closed_world: declared`, not as proven.
+
+### What a person still does
+
+Every effect carries `needs_operator_confirmation: true`. `verify-run`
+refuses the file and `qualify` reports a problem until a person:
+
+- confirms each read is the system of record and gives it its own read-only
+  credential (`auth`, `access_token_env`, `sql_password_env`); the
+  recording's reads used the browser's sign-in;
+- checks each `{param: ...}` and removes match fields that change on every
+  save;
+- decides whether a guarded table is shared by other users (a guard stops a
+  run when anyone else writes there) and removes that guard if so;
+- deletes every `needs_operator_confirmation: true` line.
+
+### Identity evidence for unarmed clicks
+
+With `--bundle` (or `--recording` when the source is a bundle) the command
+also reports identity coverage: how many clicks have a right-record check
+armed now, and how many would with evidence from the recording's DOM or
+accessibility text at each unarmed click (the clicked row's structured text,
+or the accessible name of a clicked `row`, `listitem`, `option` or
+`treeitem`). It proposes only evidence the runtime checks on the bundle's
+surface; on RDP or Citrix nothing is proposed. A record named elsewhere on the
+page (title, URL) is listed but not counted, because the runtime checks
+identity at the click point. The evidence text goes to `identity.proposed.json`
+(mode 0600); the proof holds counts and parameter names only. Nothing is
+applied to the bundle.
+
+### Limits
+
+- Saves that update an existing record are not handled yet; the check
+  expects one new record.
+- A REST read must return its records at the top level of the response, or
+  under one key; nested record lists are rejected.
+- `--db` reads SQLite files. Other databases go through `--verifier` with a
+  `kind: sql` section.
+- The fault classes are a hand-written taxonomy. Passing them is coverage of
+  that taxonomy, not a field rate.
+- No model calls. The only network read is the `--verifier` read you name.
+- The end-to-end proof changes free-text values on every run, but keeps
+  identifiers (the fixture's patient must exist). Recorded identifiers are
+  always bound as `{param: ...}`, never written as literals.
+- A demonstration with no write step is refused, as before.
+
 ## A read-back taught by demonstration ("Now show how you'd check it saved")
 
 For an application with no API, database or export (a legacy desktop app,
@@ -582,14 +727,20 @@ Per-kind required fields:
 |---|---|---|
 | `onscreen` | (none — auto-derived from the demo) | `readback_region`, `readback_min_ratio` (hand-config fallback) |
 | `ui_readback` | `ui_readback` section: `record_url`, `sign_in` (env-var names for the read-back account), `ready_selector`, `row_selector`, `fields`, `identity` | `url_params`, `empty_selector`, `not_found_selector`, `read_post_paths`, per-field `attribute` / `date_format` / `casefold`, `truncation_markers`, `navigation_timeout_s` |
-| `rest` | `base_url` | `records_path` (may contain `{placeholder}`s), `records_key`, `path_params`, `auth` |
+| `rest` | `base_url` | `records_path` (may contain `{placeholder}`s), `records_key`, `path_params`, `auth`, `records_drop_fields` |
 | `graphql` | `base_url` + `graphql_query` | `graphql_variables` (`{param: ...}` entity binding), `graphql_records_path`, `graphql_freshness_field` + `graphql_freshness_window_s`, `auth` |
-| `fhir` | `base_url` | `resource_type`, `search_params`, `search_param_exprs`, `field_paths`, `access_token_env` or `smart_backend`, `verify_tls` |
-| `sql` | `sql_query` + (`sqlite_database` or `sql_driver`) | `sql_query_params`, `sql_connect_args`, `sql_password_env` |
+| `fhir` | `base_url` | `resource_type`, `search_params`, `search_param_exprs`, `field_paths`, `access_token_env` or `smart_backend`, `verify_tls`, `records_drop_fields` |
+| `sql` | `sql_query` + (`sqlite_database` or `sql_driver`) | `sql_query_params`, `sql_connect_args`, `sql_password_env`, `records_drop_fields` |
 | `file` | `root` | `file_pattern`, `file_min_size`, `file_mtime_window_s`, `file_content_probe` |
 | `email` | `root` | `mail_pattern`, `file_mtime_window_s` (freshness), `file_content_probe` (body regex) |
 | `document` | `root` | `file_pattern`, `document_format` (`json` \| `text`), `document_field_paths`, `document_text_pattern`, `file_mtime_window_s` |
 | `document-hash` | `root` | `glob` |
+| `surfaces` | `surfaces`: name -> one plain verifier config (any kind above) | each effect's `probe` names its surface (`surface=<name>`); an effect naming none, or an unknown one, halts |
+
+`records_drop_fields` (`rest`, `sql`, `fhir`) removes fields from every record
+before judging. `[id]` compares records by content: a record whose id stayed
+the same but whose fields changed reads as one record removed and one added,
+so `forbid_collateral_loss` catches it.
 
 Any kind additionally accepts the evidence-minimization fields
 `evidence_redact_fields` / `evidence_keep_fields` (see "Evidence minimization"