verify-run: frame conditions (nothing outside the declared delta changed)

CAPABILITIES.md

@@ -136,6 +136,7 @@ improvising or retrying when something is off.
 | Never retry an uncertain save (`RECONCILIATION_REQUIRED`) | Released | Synthetic (fault server) | [VERIFICATION.md](packages/flow/docs/VERIFICATION.md) |
 | One check-level scale, 0 to 5, from "unchecked" to "counterparty confirmed" | Released | Unit tests | `openadapt_flow/check_level.py` |
 | Judge any executor's write, including an agent's or a script's, from the system of record | Released | Synthetic | `openadapt-flow verify-run`, [VERIFY_RUN.md](packages/flow/docs/VERIFY_RUN.md) |
+| Prove that nothing outside the declared change moved (frame conditions), and attribute concurrent edits by other users through the app's audit log or a modified-by field; the receipt signs which parts were checked | On main | Synthetic (MockMed, SQLite audit log) | `verify-run`, [VERIFICATION_COVERAGE.md](packages/flow/docs/VERIFICATION_COVERAGE.md) |
 | Guarded save: a safety layer any agent wraps around one write (check the record, hold for approval, read back) | On main ([#1258](https://github.com/OpenAdaptAI/OpenAdapt/pull/1258)) | Synthetic | `GUARDED_SAVE.md` |
 | Draft a record check from the demonstration's write steps (`scaffold-verifier`) | Released | Synthetic | `openadapt-flow scaffold-verifier` (a person fills in the draft) |
 | Build a working record check from the reads the app made while the person viewed the saved record, and test it against injected bad writes before anyone reviews it | On main ([#1284](https://github.com/OpenAdaptAI/OpenAdapt/pull/1284)) | Synthetic (MockMed, OpenEMR fixture) | `openadapt-flow scaffold-verifier` |

llms-full.txt

@@ -533,6 +533,7 @@ improvising or retrying when something is off.
 | Never retry an uncertain save (`RECONCILIATION_REQUIRED`) | Released | Synthetic (fault server) | [VERIFICATION.md](https://github.com/OpenAdaptAI/OpenAdapt/blob/main/packages/flow/docs/VERIFICATION.md) |
 | One check-level scale, 0 to 5, from "unchecked" to "counterparty confirmed" | Released | Unit tests | `openadapt_flow/check_level.py` |
 | Judge any executor's write, including an agent's or a script's, from the system of record | Released | Synthetic | `openadapt-flow verify-run`, [VERIFY_RUN.md](https://github.com/OpenAdaptAI/OpenAdapt/blob/main/packages/flow/docs/VERIFY_RUN.md) |
+| Prove that nothing outside the declared change moved (frame conditions), and attribute concurrent edits by other users through the app's audit log or a modified-by field; the receipt signs which parts were checked | On main | Synthetic (MockMed, SQLite audit log) | `verify-run`, [VERIFICATION_COVERAGE.md](https://github.com/OpenAdaptAI/OpenAdapt/blob/main/packages/flow/docs/VERIFICATION_COVERAGE.md) |
 | Guarded save: a safety layer any agent wraps around one write (check the record, hold for approval, read back) | On main ([#1258](https://github.com/OpenAdaptAI/OpenAdapt/pull/1258)) | Synthetic | `GUARDED_SAVE.md` |
 | Draft a record check from the demonstration's write steps (`scaffold-verifier`) | Released | Synthetic | `openadapt-flow scaffold-verifier` (a person fills in the draft) |
 | Build a working record check from the reads the app made while the person viewed the saved record, and test it against injected bad writes before anyone reviews it | On main ([#1284](https://github.com/OpenAdaptAI/OpenAdapt/pull/1284)) | Synthetic (MockMed, OpenEMR fixture) | `openadapt-flow scaffold-verifier` |

packages/flow/docs/VERIFY_RUN.md

@@ -80,34 +80,104 @@ unless given, and when present they are signed with the rest of the receipt.
 
 ## Records outside the target
 
-With a baseline, a `record_written` check also refutes when a record that
-was there before the agent started and is not the target has changed
-(`forbid_collateral_change`), not only when it is gone
-(`forbid_collateral_loss`). The agent's write can be right while it also
-edited another patient's record in place, and only the baseline shows that.
-verify-run turns this on for every `record_written` effect when it judges.
-The contract in the file is unchanged, so its digest is still the one qualify
-reports, and `evidence.readback.effects[].collateral_change_checked` says the
-check ran. To skip it for one effect, for example when the read covers a
-table other people edit during the run, set `forbid_collateral_change: false`
-on that effect in `effects:`. Fields that change on their own, such as a
-modification time, belong in the verifier's `records_drop_fields`.
-
-A changed record is not proof that the executor changed it: another user may
-have edited it during the run. The verdict says so, and the outcome is
-`reconciliation_required`, so a person checks the record before anything is
+With a baseline, verify-run also proves that nothing outside the declared
+delta changed: no record that the effects don't name was added, removed or
+edited, and a pre-existing target changed only in the fields the effects
+name. This is the frame check ([`VERIFICATION_COVERAGE.md`](VERIFICATION_COVERAGE.md)).
+It reads the same read set the effects use, once after the save, and judges
+the whole contract at once, so two effects on one read set never flag each
+other's targets. The agent's write can be right while it also edited another
+patient's record in place, and only the baseline shows that.
+
+Without a baseline the frame can't be checked, and the run is not
+`verified`.
+
+A `frame:` section says how records are compared and who may change them:
+
+```yaml
+frame:
+  identity_field: pid        # default: id, else the whole record
+  ignore_fields: [date]      # fields that change on their own
+  target_fields: [phone_home]  # default: the fields the effects name
+  attribution:               # optional
+    kind: audit_read         # or record_field, with server_set: [...]
+    actor_field: user
+    record_field: patient_id
+    self: [{param: bot_user}]  # the bot's own user or session ids
+    read:                    # a second read-only read: the app's audit log
+      kind: sql
+      sql_driver: pymysql
+      sql_query: SELECT id, user, patient_id FROM log WHERE event LIKE 'patient-record-%'
+```
+
+Each change outside the declared delta is attributed. A change that the
+audit log (`audit_read`) or the record's own modified-by field with a new
+version (`record_field`) attributes to another user is a concurrent edit: it
+is listed in `evidence.frame.concurrent_count` and does not count against the
+save. A change by one of the bot's own ids, or one nothing explains, is
+collateral, and the outcome is `reconciliation_required`. With `audit_read`,
+a log entry by the bot for a record no effect names is collateral too, even
+when the read shows no change.
+
+Only evidence the bot can't write counts:
+
+- `audit_read` reads the app's own audit log or change feed.
+- `record_field` reads fields the app sets on the server. List them in
+  `server_set` (they must include `actor_field` and any `version_field`);
+  that list is the per-app statement that no user or API client can write
+  them. A field the run itself writes, or that a run parameter names, is
+  never evidence: attribution that uses one is refused, and every change
+  stays unattributed (`evidence.frame.attribution: attribution_refused`).
+- The run's own ids (`self`, and the executor's id from the run record) are
+  never "another user".
+- Another user's change to a record the save declares is never excused. The
+  saved value may no longer stand, so the outcome is
+  `reconciliation_required` (`evidence.frame.target_changed_by_other`). Only
+  changes outside the declared delta can be concurrent edits.
+
+Without `attribution`, every change outside the delta is collateral. A
+change is not proof that the executor made it: another user may have edited
+the record during the run. A person checks the record before anything is
 retried or undone. Values compare by type. A `Decimal` or `datetime` read
 from a database equals the JSON form the baseline stored it in, while two
 strings compare exactly, so `"02139"` changed to `"2139"` is a change.
 
+When the frame is judged, the per-effect collateral rules
+(`forbid_collateral_loss`, `forbid_collateral_change`) apply only where the
+file sets them explicitly; the frame covers the rest. Without a baseline,
+`forbid_collateral_change` is turned on as before, though it can't refute
+without a baseline either.
+
+## What the receipt says was checked
+
+The receipt's `checked` field names each part of the claim behind
+`verified` and how it came out:
+
+```json
+"checked": {"delta": "held", "frame": "held", "source": "instruction"}
+```
+
+- `delta`: the declared records, read from the system of record.
+- `frame`: nothing else in the read set changed.
+- `source`: the inputs match their source. `instruction` means the inputs
+  were the task's own parameters (`--params`), with no document behind them.
+
+Each part is `held`, `refuted` or `not_checked`. `verified` requires `delta`
+and `frame` to be `held` and `source` to be `held` or `instruction`. The
+field is inside `receipt_sha256`, so a Seal signs it. `evidence.frame` holds
+the counts behind the frame part (records compared, collateral, concurrent)
+and the digest of the `frame:` section. A receipt issued before the field
+existed has neither and still checks.
+
 ## Verdicts
 
 | What the store shows | `effect_verdict` | `outcome` |
 |---|---|---|
-| The declared record, exactly once, through a system-of-record read | `CONFIRMED` | `verified` |
+| The declared record, exactly once, through a system-of-record read, and nothing else in the read set changed | `CONFIRMED` | `verified` |
+| The declared record, but no baseline, so the frame can't be checked | `CONFIRMED` | `reconciliation_required` |
 | The same, but the executor approved its own write | `CONFIRMED` | `rejected_policy` |
-| Nothing that matches | `REFUTED` | `halted_before_effect` |
-| A duplicate, a wrong value, only some of the effects, or another record that vanished or changed | `REFUTED` | `reconciliation_required` |
+| Nothing that matches, and nothing else in the read set moved | `REFUTED` | `halted_before_effect` |
+| A duplicate, a wrong value, only some of the effects, or a record outside the delta that was added, vanished or changed | `REFUTED` | `reconciliation_required` |
 | The store could not be read, no baseline, or a separate-session read | `INDETERMINATE` or `CONFIRMED` | `reconciliation_required` |
 
 Only a read through the system of record produces `verified`. A screen

packages/flow/openadapt_flow/countersign/document.py

@@ -497,6 +497,9 @@ class CountersignReport:
     #: The check level the receipt states, or None on a receipt
     #: issued before ``checked_how`` existed.
     checked_how: Optional[str] = None
+    #: Which parts of the claim behind ``verified`` were checked (delta,
+    #: frame, source), or None on a receipt issued before ``checked``.
+    checked: Optional[dict[str, Any]] = None
     seal: dict[str, Any] = field(default_factory=dict)
     evidence: dict[str, Any] = field(default_factory=dict)
     statement: dict[str, Any] = field(default_factory=dict)
@@ -620,6 +623,11 @@ def verify_countersigned(
         outcome=receipt.get("outcome"),
         oracle_tier=receipt.get("oracle_tier"),
         checked_how=receipt.get("checked_how"),
+        checked=(
+            dict(receipt["checked"])
+            if isinstance(receipt.get("checked"), dict)
+            else None
+        ),
         accept_non_flow=accept_non_flow,
     )
     if schema not in (EXECUTE_RECEIPT_SCHEMA, EFFECT_RECEIPT_SCHEMA):
@@ -641,6 +649,16 @@ def verify_countersigned(
         )
         if stated_tier is None or stated_tier != receipt.get("verification_tier"):
             report.problems.append("checked_how_mismatch")
+    if schema == EFFECT_RECEIPT_SCHEMA and "checked" in receipt:
+        parts = receipt.get("checked")
+        if not isinstance(parts, dict) or set(parts) != {"delta", "frame", "source"}:
+            report.problems.append("checked_malformed")
+        elif receipt.get("outcome") in _SEALABLE and (
+            parts.get("delta") != "held"
+            or parts.get("frame") != "held"
+            or parts.get("source") not in ("held", "instruction")
+        ):
+            report.problems.append("verified_without_every_part")
     # Seal signature: openadapt_types.seal, unchanged.
     try:
         keys = parse_key_registry(list(registry))
@@ -677,6 +695,7 @@ def verify_countersigned(
                 != receipt.get("verification_tier")
                 or (ev.get("readback") or {}).get("checked_how")
                 != receipt.get("checked_how")
+                or ev.get("checked") != receipt.get("checked")
             )
         report.evidence = {
             "status": "evidence_mismatch" if mismatch else "bound",

packages/flow/openadapt_flow/countersign/render.py

@@ -81,6 +81,26 @@ def executor_line(report: CountersignReport) -> str:
 }
 
 
+_PART_TEXT = {
+    "delta": "the declared change",
+    "frame": "nothing else in the slice changed",
+    "source": "the inputs match their source",
+}
+
+
+def checked_line(checked: dict[str, Any]) -> str:
+    """One clause per part of the claim, in the receipt's own words."""
+
+    out = []
+    for part in ("delta", "frame", "source"):
+        state = str(checked.get(part))
+        if part == "source" and state == "instruction":
+            out.append("source: the inputs were the authorized instruction")
+        else:
+            out.append(f"{part} ({_PART_TEXT[part]}): {state}")
+    return "; ".join(out)
+
+
 def tier_line(report: CountersignReport) -> str:
     if report.receipt_schema == EXECUTE_RECEIPT_SCHEMA:
         return f"not stated by Execute v1 (oracle_tier {report.oracle_tier})"
@@ -163,6 +183,11 @@ def render_report(report: CountersignReport, *, show_names: bool = True) -> str:
             if report.checked_how is not None
             else []
         ),
+        *(
+            [("Checked", checked_line(report.checked))]
+            if report.checked is not None
+            else []
+        ),
         ("Effect verdict", str(report.effect_verdict or "not stated (Execute v1)")),
         ("Outcome", str(report.outcome)),
         ("Receipt schema", str(report.receipt_schema)),

packages/flow/openadapt_flow/qualify/config.py

@@ -400,6 +400,12 @@ def sub(match: re.Match[str]) -> str:
     return value
 
 
+#: ``openadapt.verify/v1`` sections only ``verify-run`` reads. Qualify accepts
+#: and ignores them, so one file serves both (the mirror of verify-run's
+#: ``QUALIFY_ONLY_SECTIONS``).
+VERIFY_RUN_ONLY_SECTIONS: tuple[str, ...] = ("frame",)
+
+
 def parse_verify_config(
     data: Any,
     *,
@@ -410,6 +416,7 @@ def parse_verify_config(
 
     if not isinstance(data, dict):
         raise QualifyConfigError("verify.yaml must be a YAML mapping")
+    data = {k: v for k, v in data.items() if k not in VERIFY_RUN_ONLY_SECTIONS}
     missing: list[str] = []
     data = _expand(data, missing, env)
     if missing: