benchmark: verification coverage against an independent spec (stand-in results; live run pending)

packages/flow/benchmark/scoreboard/tasks/openimis.py

@@ -111,7 +111,10 @@
 
 
 def fixture() -> OpenIMISFixture:
-    return OpenIMISFixture()
+    # A second copy runs on its own ports (OPENIMIS_HTTP_PORT, OPENIMIS_DB_PORT)
+    # and compose project (OPENIMIS_COMPOSE_PROJECT); the defaults are unchanged.
+    port = os.environ.get("OPENIMIS_HTTP_PORT")
+    return OpenIMISFixture(http_port=int(port)) if port else OpenIMISFixture()
 
 
 def claim_form_url(fx: Optional[OpenIMISFixture] = None) -> str:

packages/flow/benchmark/verification_coverage/README.md

@@ -0,0 +1,87 @@
+# Verification coverage: fresh runs, per fault class
+
+Measures the design in
+[`docs/VERIFICATION_COVERAGE.md`](../../docs/VERIFICATION_COVERAGE.md): frame
+conditions, the fault gate, and provenance. It reruns the OpenEMR fault
+experiment of OpenAdaptAI/OpenAdapt#1365 as fresh agent runs, not rebuilt
+database states, and runs the same suite on openIMIS. The results are in
+[`RESULTS.md`](RESULTS.md).
+
+## Protocol
+
+For each item, a computer-use agent (Claude Sonnet 5.5, the scoreboard's
+agent) enters one record through the app's own UI, on a local fixture with
+synthetic data. A fault is injected only in the fixture's database, by a
+trigger installed before the agent starts or a poller that acts once the new
+record lands. The app itself is unchanged.
+
+Three `verify-run` engines judge the same save. Each runs from its own
+checkout and takes its own baseline before the agent starts:
+
+| Engine | Commit | What it checks |
+|---|---|---|
+| `e1365` | the engine #1365 measured with | the declared record; another record removed |
+| `main` | main before this work | the same, plus #1375: another record changed, per effect |
+| `after` | this work | the frame with the app's own attribution, and the round trip against the source document |
+
+Ground truth is read from the fixture's database after the run. A bad save
+is caught when the engine's outcome is anything but `verified`. A clean save
+that is refused is a false alarm.
+
+## Fault classes
+
+| Class | What happens | The save is |
+|---|---|---|
+| `ok` | nothing | clean |
+| `partial` | a trigger blanks a field of the new record | bad |
+| `wrong_value` | a trigger changes a field of the new record | bad |
+| `duplicate` | the poller copies the new record | bad |
+| `no_persist` | the poller removes the new record after it lands | bad |
+| `collateral_loss` | the poller removes another, pre-existing record | bad |
+| `collateral_edit` | the poller edits another record, with no audit trail | bad |
+| `collateral_edit_bot` | the same edit, attributed to the bot's own user | bad |
+| `concurrent_edit_other` | the same edit, attributed to another user | clean: a legitimate concurrent edit |
+| `misread_source` | the source document holds one value; the agent is told another (a misread before the save) and saves it faithfully | bad |
+
+Attribution comes from the app. OpenEMR writes each patient-record change to
+its audit log (`log`, with the user and `patient_id`); the `after` engine
+reads it with a SELECT-only database user (`audit_read`). openIMIS stamps
+each claim row with its last writer and time (`AuditUserID`,
+`ValidityFrom`); the `after` engine reads those (`record_field`). For the two
+attributed edits, the poller writes what the app would have written: a
+`patient-record-update` log row in OpenEMR, the writer and time on the
+openIMIS row.
+
+For every item the `after` engine also gets the source document (a synthetic
+referral or claim form) and the provenance a first reader would produce. The
+"Held before the save" column is the pre-save cross-check: a deterministic
+second reading of the document disagreeing with what the agent was told.
+
+## The fault gate
+
+`openemr_gate.py` runs the fault gate (`openadapt_flow/fault_gate.py`) on the
+OpenEMR fixture with no model calls, for two reads of the same contract: the
+full patient list (the #1365 check) and a search for the run's email (the
+kind of read a synthesized check picks).
+
+## Running
+
+The fixtures run as their own compose projects under the shared-machine
+rules for this workspace (a lease, at most two fixture sessions, a disk and
+load floor). With a fixture up and the three engines checked out:
+
+```bash
+PYTHONPATH=packages/flow/benchmark python -m verification_coverage.openemr_run \
+  --run-id <id> --per-fault 5 \
+  --engine-e1365 <checkout> --engine-main <checkout> --engine-after <checkout>
+```
+
+```bash
+python -m verification_coverage.summarize --write
+```
+
+## What is public
+
+The harness, the fault classes and these rows are public: synthetic data
+only. Coverage floors a deployment chooses and any grown fault corpus are
+not part of this directory.

packages/flow/benchmark/verification_coverage/exec_mariadb.py

@@ -0,0 +1,80 @@
+"""A minimal DB-API connection to a fixture's MariaDB through ``docker exec``.
+
+The OpenEMR fixture publishes no database port. This lets a ``kind: sql``
+verifier (``sql_driver: verification_coverage.exec_mariadb``) read it as a
+SELECT-only user, the way a deployment would read through its own driver.
+Benchmark plumbing only: one statement, no parameters, rows as text.
+"""
+
+from __future__ import annotations
+
+import os
+import subprocess
+from typing import Any, Optional
+
+
+class _Cursor:
+    def __init__(self, conn: "Connection") -> None:
+        self._conn = conn
+        self.description: Optional[list[tuple[str, ...]]] = None
+        self._rows: list[tuple[Any, ...]] = []
+
+    def execute(self, sql: str, params: Any = None) -> None:
+        if params:
+            raise ValueError("exec_mariadb takes no query parameters")
+        out = subprocess.run(
+            [
+                "docker",
+                "exec",
+                "-i",
+                "-e",
+                "MYSQL_PWD",
+                self._conn.container,
+                "mariadb",
+                "-u",
+                self._conn.user,
+                "--batch",
+                "--raw",
+                self._conn.database,
+                "-e",
+                sql,
+            ],
+            capture_output=True,
+            text=True,
+            timeout=60,
+            env={**os.environ, "MYSQL_PWD": self._conn.password},
+            check=True,
+        ).stdout
+        lines = out.splitlines()
+        if not lines:
+            self.description, self._rows = [], []
+            return
+        header = lines[0].split("\t")
+        self.description = [(name,) for name in header]
+        self._rows = [
+            tuple(None if cell == "NULL" else cell for cell in line.split("\t"))
+            for line in lines[1:]
+        ]
+
+    def fetchall(self) -> list[tuple[Any, ...]]:
+        return list(self._rows)
+
+
+class Connection:
+    def __init__(self, container: str, user: str, password: str, database: str):
+        self.container = container
+        self.user = user
+        self.password = password
+        self.database = database
+
+    def cursor(self) -> _Cursor:
+        return _Cursor(self)
+
+    def close(self) -> None:
+        return None
+
+
+def connect(
+    container: str, user: str, password: str = "", database: str = "openemr"
+) -> Connection:
+    return Connection(container, user, password, database)

packages/flow/benchmark/verification_coverage/independent/README.md

@@ -0,0 +1,139 @@
+# Verification coverage against an independent specification
+
+What OpenAdapt's record checks actually catch, measured against a
+specification and faults written without looking at those checks.
+
+An external review said that a check built from the same contract as the save
+inherits the contract's blind spots. This suite tests that claim: write down,
+independently, everything that must and must not be true after one correct
+referral intake in OpenEMR; derive faults from that; run them through
+OpenAdapt's checks; count what each check catches, misses and flags wrongly.
+
+## How it was made
+
+1. `SPEC.md`, the specification, was committed first (ad4bdbfe2), before any
+   run and without reading `verify.yaml` files, synthesized checks or
+   `fault_gate.py`'s fault classes. Sources: the task definition, the referral
+   format and OpenEMR's schema and behavior.
+2. `faults.yaml`, 17 cases derived from the spec, was committed next
+   (40a474bc1): wrong record (2), unrelated changes by the bot to another
+   chart or table (7), wrong values saved faithfully from a misread source
+   (3), a missing side record, a duplicate save, and two legitimate concurrent
+   updates by another user that must not be flagged.
+3. `WITNESS.md` records what OpenEMR's own save path writes, as amendments,
+   without editing the spec.
+
+## The checks under test
+
+| name | what it is |
+|---|---|
+| `shipped` | the OpenEMR referral task's record contract (`scoreboard/claims_openemr.py` `VERIFY_YAML`): the whole patient table, `verify-run`'s default frame |
+| `framed` | the same, plus a frame with OpenEMR's audit log for attribution (as `verification_coverage/openemr_run.py` declares it) and provenance with the referral document, so `verify-run` does the round trip (#1446) |
+| `synthesized` | what `scaffold-verifier --db --fault-gate` proposes from a demonstration on its own copy |
+| pre-save | `provenance.cross_check`: a second extraction of every labeled referral field, compared before the save (scored only for the misread cases) |
+
+The fault gate (#1445) also runs on each check, so its own coverage claim can
+be set beside the independent result.
+
+## Where it runs
+
+- **Stand-in** (`run.py`, `standin.py`): an SQLite copy of the pinned OpenEMR
+  fixture's real baseline dump. Every table, column, default and installer
+  row is OpenEMR's (283 tables, 256,044 rows). The writes are emulated: the
+  New Patient save writes the rows `WITNESS.md` lists, and each named user's
+  write adds the audit row OpenEMR's `EventAuditLogger` writes. `--slice`
+  keeps only the 24 tables the spec names plus bookkeeping.
+- **Live** (`live.py`): the same cases on the pinned OpenEMR fixture. The bot's
+  New Patient save goes through OpenEMR's form in a browser. The bot's other
+  writes and clinician2's go through the REST API with each user's own token,
+  so OpenEMR writes its own audit rows. **Not run yet:** it waits for the
+  shared fixture slot.
+
+## Results: stand-in, clinical slice (2026-10-24)
+
+Per class, for a fault: caught or missed. For a clean case: ok or false alarm.
+`results/standin-slice/` has every row, receipt part and gate record.
+
+| class | cases | shipped | framed | synthesized |
+|---|---|---|---|---|
+| clean | 1 | ok | ok | **false alarm** |
+| concurrent update by another user | 2 | **2 false alarms** | 2/2 ok | **2 false alarms** |
+| wrong record | 2 | 2/2 caught | 2/2 caught | (2/2) |
+| unrelated change by the bot | 7 | 3/7, **4 missed** | 6/7, **1 missed** | (7/7) |
+| misread source, saved faithfully | 3 | 0/3, **3 missed** | 2/3, **1 missed** | (3/3) |
+| missing side record | 1 | **missed** | **missed** | (1/1) |
+| duplicate save | 1 | caught | caught | (1/1) |
+
+The pre-save cross-check held all 3 misread cases.
+
+The synthesized check's catches are in parentheses because they carry no
+information: it refuted the clean save too, so it refutes everything.
+
+What the fault gate said about the same checks:
+
+| check | gate claims | gate result |
+|---|---|---|
+| `shipped` | delta, frame | 18/18 killed, clean passes (admitted) |
+| `framed` | delta, frame | 18/18 killed, clean passes (admitted) |
+| `synthesized` | delta, frame | 7/7 killed, **clean fails** (not admitted) |
+
+## What it found
+
+Fail-open (a bad save reported `verified`), ranked by risk:
+
+1. **A frame with audit attribution excuses any write the bot makes for the
+   saved patient, in any table.** An extra insurance row on the new chart
+   verified under `framed`. #1505
+2. **The gate's "frame" coverage is the one table the check reads.** It
+   admitted `shipped` at 18/18 while the independent cases show 9 of 15
+   faults missed: edits to another chart's history, a note and an allergy on
+   another patient, the extra insurance row, the missing history row, and
+   three faithful saves of misread inputs. #1506
+3. **Provenance checks only the task's parameters.** The referral names a
+   provider; the task has no provider parameter, so a wrong provider verified
+   under `framed`. A coded field (provider id, state code) can't be
+   round-tripped by value. #1507
+4. **Required side records are never checked.** A chart whose `history_data`
+   row is missing verified under both contracts. OpenEMR's own REST save
+   writes no such row. #1508
+
+Fail-closed (no wrong `verified`, but the check can't be used):
+
+5. **`verify-run` crashed on any SQL read with a binary column** (OpenEMR's
+   `uuid binary(16)`), so no `SELECT *` check on OpenEMR could run. Fixed in
+   #1503 (merged into this branch for these measurements).
+6. **`scaffold-verifier --db` can't produce a working check on the real
+   schema.** It takes coincidental value matches in 21 reference tables as
+   the saved row, the gate then fails on the wrong table, and the default
+   frame flags OpenEMR's own log rows on every correct save. On the full
+   schema, synthesis and the gate ran for more than 30 minutes. #1509
+7. **The shipped contract flags every legitimate concurrent update** (no
+   attribution). `framed` handles both concurrent cases correctly.
+
+What held: wrong record and duplicate saves were caught by every check. Edits
+to another chart's own row were caught by every check. A stray edit by the bot
+was still caught when another user's legitimate edit happened in the same
+window. The round trip caught the misread DOB and the swapped names.
+
+## Limits
+
+- The stand-in's audit rows are emulated. `framed` catches 3 of its 6
+  unrelated-change catches only through the bot's audit entries naming another
+  patient. Whether OpenEMR writes `patient_id` on those entries for API writes
+  is what the live run checks.
+- One referral, one app, one run per case. The counts are cases, not rates.
+- The full-schema stand-in run is slower (about 10 minutes a case, mostly
+  `verify-run` polling the synthesized check's 580 effects). Its rows are added
+  to `results/standin-full/` when it finishes.
+
+## Run it
+
+```bash
+python -m verification_coverage.independent.run \
+  --baseline-sql "$OPENEMR_FIXTURE_STATE/baseline.sql" --work WORKDIR --out OUT [--slice]
+python -m verification_coverage.independent.summarize OUT/rows.json
+# with the fixture lease held:
+python -m verification_coverage.independent.live --out OUT
+```
+
+No model calls in any of these.