diff --git a/packages/flow/docs/VERIFICATION_COVERAGE.md b/packages/flow/docs/VERIFICATION_COVERAGE.md new file mode 100644 index 000000000..8d485f113 --- /dev/null +++ b/packages/flow/docs/VERIFICATION_COVERAGE.md @@ -0,0 +1,350 @@ +# Record checks that cover their own blind spots + +Design. Status: proposed, with an implementation in small pull requests. Any +change to when a run is `verified` waits for a safety review. + +## The problem + +A record check reads the system of record after a save and compares what it +finds with a contract. The contract comes from the same place as the save: +the demonstration, the task's parameters, or a synthesized check built from +the reads the app made. So the check is blind wherever the contract is blind. +Three blind spots have been measured or are easy to construct: + +1. **Changes the contract never mentions.** In the OpenEMR fault run of + OpenAdaptAI/OpenAdapt#1365, `verify-run` caught 25 of 30 bad saves and + reported `verified` on all 5 saves where another chart was edited in place. + The contract described the new chart, and nothing in it said "and no other + chart changes". OpenAdaptAI/OpenAdapt#1375 added + `forbid_collateral_change`, measured only on rebuilt database states. It + judges one effect at a time, so two effects on one read set flag each + other's targets, and it can't tell a legitimate edit by another user from + a stray write. +2. **Checks that were never shown to fail.** A synthesized check is built + from observed values and available reads. If the read is scoped to one + patient, an edit to another patient can't be seen, however the judge is + written. `scaffold-verifier` tests the check by mutating the records the + check already reads, so it can't find this either. +3. **The wrong input, saved correctly.** A check confirms that the database + holds the parameters it was given. If the referral said `02139` and the + extraction read `02193`, the save of `02193` passes every check. The error + happened before the save, and the read-back can't see it. + +## One claim, three parts + +`verified` means exactly this, and nothing more: + +> The declared delta happened, nothing else in the declared slice changed, +> and the inputs match their source. + +Each part is checked by its own mechanism, and the receipt says which parts +were checked and how. The parts are: + +| Part | Name in the receipt | What it rules out | Mechanism | +|---|---|---|---| +| Delta | `delta` | missing, partial, wrong-value, duplicate and delayed writes | the existing effect judge (`record_written`, `field_equals`, `exact_new_set`) | +| Frame | `frame` | edits, deletions and additions outside the declared records and fields | frame conditions (section 1) | +| Source | `source` | a misread or mistyped input saved correctly | provenance, second extraction, round trip (section 3) | + +A check is admitted only after it is shown to catch the faults it claims to +catch (section 2). Its coverage travels with it into the receipt. + +The name "frame condition" comes from program verification: a procedure's +specification says what it may modify, and everything else is unchanged. +The same idea applies to a save. + +## 1. Frame conditions + +### The contract declares what may change + +The save's contract already names its target records: every `record_written` +and `field_equals` selector, and every `exact_new_set` member. A new `frame:` +section names the slice that must otherwise stay unchanged, and the fields on +the target records that the save may change. + +```yaml +frame: + # Records are compared by this field. Default: id (stable_id). + identity_field: pid + # Fields that change on their own on every record, such as a last-seen time. + ignore_fields: [date] + # Fields of a target record that the save may change. Default: the fields + # the effects name. Any other field of a pre-existing target must not move. + target_fields: [phone_home, street] + # Who changed what, from the app's own audit log or change feed. + attribution: + kind: audit_read + read: {kind: sql, ...} # the same verifier kinds, read-only + record_field: patient_id # the audit entry's record reference + actor_field: user + self: [{param: bot_user}] # the bot's own user or session ids +``` + +The slice is the verifier's read set: the records it returns before and after +the save, through the same read-only channel the delta check uses. No new +connection is needed when there is no attribution read. + +### The judgment + +The frame judge compares the baseline with the read after the save, once for +the whole contract, not once per effect: + +- A record is **declared** when any effect's selector matches it before or + after the save. Declared records are judged by the delta check, except that + a pre-existing declared record may change only in its target fields. +- Every other record that was **added, removed or changed** is a frame + change. Each change is then attributed: + - **another actor**: the audit log names a different user for that record + in the window, or the record's own modified-by field names one and its + version moved. This is a concurrent edit. It is listed in the evidence and + does not count against the save. + - **this run**: the audit log or modified-by field names one of the bot's + own ids. This is collateral. + - **unattributed**: nothing names an actor. This is collateral too. A change + nobody can explain is never assumed to be someone else's. +- An audit entry by the bot for a record that no effect declares is + collateral, even if the record looks unchanged in the read. The log shows a + write the contract does not cover. + +Collateral refutes the frame. The outcome is `reconciliation_required`, the +same as a wrong value, and the reason names the records and fields. + +Without a baseline, or when the baseline is outside the execution window, the +frame is `not_checked`. Without attribution, every frame change is +unattributed, which is the behavior of OpenAdaptAI/OpenAdapt#1375 extended to +additions and to multi-effect contracts. + +### Where attribution comes from + +| App offers | Attribution | Example | +|---|---|---| +| An audit log | `audit_read`: a second read-only read of log entries in the window | OpenEMR's `log` table records `patient-record-update` with the user and `patient_id` | +| A change feed or history | `audit_read` over the feed | FHIR `_history`, `AuditEvent` | +| A modified-by field and a version or ETag on each record | `record_field` | `meta.versionId` plus a last-modified-by extension | +| Nothing | none: every frame change is unattributed | MockMed | + +### What this replaces + +`Effect.forbid_collateral_loss` and `forbid_collateral_change` stay as they +are for contracts without a `frame:` section, so every existing contract hash +holds. When `frame:` is present, the frame judge replaces the per-effect +collateral rules for that contract. `verify-run` applies a default frame (the +read set, compared by `stable_id`, no attribution) to any contract with a +baseline. That keeps #1375's behavior, adds unexplained additions, and stops +two effects on one read set from refuting each other. + +## 2. Mutation-qualified checks + +### The gate + +Before a record check can be admitted, an automatic fault suite runs it +against a test copy of the system of record. The faults are applied to the +**test copy's store**, and the check reads them through **its own read**, so +a read that can't see a fault fails the gate. Mutating only the records the +check already reads would test the judge, not the read. + +Each case resets the copy, takes the check's baseline, applies the clean save, +applies one fault, and runs the check. The clean save must pass. Each fault +must be refuted or ruled indeterminate. + +| Fault class | What the copy holds after the save | Applies when the check claims | +|---|---|---| +| `wrong_value` (one per declared field) | the target with that field changed | delta | +| `wrong_record` | the values written to a look-alike record instead | delta | +| `unrelated_edit` | the clean save, plus another record in the slice edited | frame | +| `partial` | the target with its later fields blank | delta | +| `duplicate` | the target twice | delta | +| `missing` | no target | delta | +| `delayed` | no target until after the check's timeout, then the target | delta | + +`delayed` passes when the check does not confirm before the write lands. A +check that confirms from a cache or a stale read fails it. + +### Coverage + +Coverage is faults killed over faults applicable. A fault is applicable when +the check claims the part it targets: a check with no frame claims no +`unrelated_edit`. The gate writes `check_coverage.json`: + +```json +{ + "schema_version": "openadapt.check-coverage/v1", + "check_sha256": "sha256:...", + "suite": {"id": "openadapt.fault-suite/public", "version": "1.0.0"}, + "test_copy": "sqlite", + "claims": ["delta", "frame"], + "classes": {"wrong_value": {"applicable": 9, "killed": 9}, "...": {}}, + "killed": 15, + "applicable": 15, + "clean_pass": true +} +``` + +`check_sha256` is the check's contract digest (`verify_config_sha256`). A +changed check needs a new coverage record. The record goes in the bundle next +to the check, and its digest and totals go into the receipt. + +### Admission policy + +A check is admitted only when the clean save passes and it kills every +applicable fault. A policy can also require a minimum: a coverage floor over +the whole suite, or named classes that must be applicable (for example, +"every check must claim a frame"). `verify-run` reads the policy from the +`admission:` section and never issues `verified` for a check whose coverage +record is missing, stale or below the policy. + +`scaffold-verifier`'s fault test becomes a call to this gate. With `--db` or a +fixture it runs on a store copy. Without one it falls back to recorded +states and says so in the coverage record (`test_copy: recorded_states`), +and a policy can refuse that kind. + +### What is public + +The gate, the seven operators, the coverage format and a small sample suite +are public. A grown fault corpus and deployment coverage floors are private +under `source-policy.yaml` (`grown_corpus`, `deployment_thresholds`). The +public default policy is the rule above, "catch every fault you claim", not a +tuned number. + +## 3. Intent and provenance + +### Every written value names its source + +A run parameter can carry its provenance: + +```json +{ + "postal_code": { + "value": "02139", + "source": {"kind": "document", "sha256": "sha256:...", "line": 14, "label": "Postal code"}, + "extractor": "intake:agent" + } +} +``` + +The source is one of: + +- `document`: a line (and the label before the value) in a referral, an + invoice or another file, identified by the digest of the file. Intake + (`openadapt_flow/intake`) already finds this line for every field and then + drops it; it now keeps it; +- `worklist_cell`: a row and a column in a worklist file, identified by its + digest; +- `instruction`: the authorized task itself. The value is the instruction, so + it matches its source by construction, and the receipt says so. + +A parameter without provenance is treated as `instruction`. That keeps every +existing run honest about what was checked: its source part reads +`instruction`, not `document`. + +### A second extraction must agree before the save + +Before the save, an independent extractor reads the same source with a +different method: a deterministic parse of labeled fields, a second model, +or OCR on an image. Intake has two methods today: `intake:local` matches +labels, and `intake:agent` asks a model for the line and reads the value +locally. Each serves as the other's second extraction. Values compare by kind (text, code, date, currency), the +same comparison the screen read-back uses. A disagreement, or a value the +second extractor can't find, routes the item to a person, and the save does +not start. The extractor's method must differ from the first one's: two runs +of the same model don't count. + +### A round trip after the save + +After the save, the round trip compares the record as read back with the +source document, not with the parameters. For each declared field it takes +the value the read returned and the value the independent extractor read from +the cited span. A mismatch refutes the source part. This catches a correctly +persisted wrong entry even when the pre-save check was skipped or the +parameters changed between the check and the save. + +### What it doesn't catch + +A source document that is itself wrong is out of scope. So is a span both +extractors misread the same way. The receipt names the extractors, so a +reviewer can judge how independent they were. + +## 4. What the receipt says + +The receipt gets one optional field, `checked`. Like `checked_how`, it is +inside `receipt_sha256`, so the Seal signs it. A receipt issued before it +existed still checks. + +```json +"checked": { + "delta": "held", + "frame": "held", + "source": "instruction", + "coverage": {"killed": 15, "applicable": 15, "sha256": "sha256:..."} +} +``` + +Each part is `held`, `refuted` or `not_checked`. The source part can also be +`instruction`, which means the inputs were the authorized instruction itself +and no document was involved. The evidence lists the attributed concurrent +edits, the extractors and the per-class coverage. + +`verified` requires `delta` and `frame` to be `held`, `source` to be `held` or +`instruction`, and coverage to meet the admission policy when one is set. +Anything else is `reconciliation_required` (or `halted_before_effect` when +nothing landed). The report repeats the `checked` field in words, one line per +part, with no other wording about confidence. + +### Where the rule applies + +Two code paths issue `verified`: + +- the effect receipt from `verify-run` and the guarded save + (`verify_run.verify_run`), which judges a save something else made; +- Flow replay (`execution_profiles.classify_execution_outcome`), whose + `report.json` the offline Seal signs. + +The first implementation applies the rule to the effect receipt, where the +OpenEMR experiment was measured. Flow replay gets the same `checked` block and +the same rule in a separate pull request, through the same frame judge and +provenance functions. Until it lands, a Flow replay report does not carry +`checked`, and nothing on a public surface may say that its `verified` covers +the frame or the source. + +### What changes for existing runs + +These are the changes the safety review must approve: + +- `verify-run` without a baseline can no longer issue `verified`, because the + frame can't be checked. Today it can, for a contract that counts records + absolutely. +- A record added to the read set that no effect declares now refutes the + frame. Today only `exact_new_set` catches it. +- A contract with two effects on one read set no longer refutes itself when + `forbid_collateral_change` is on. +- An admission policy can block `verified` on coverage. + +Nothing in this design turns a refusal into a confirmation, except +attribution, which lets a concurrent edit by another user stop counting as +collateral. That exception is confined to edits an audit log or a +modified-by field attributes to a named actor other than the bot. + +## Measurement + +The benchmark lives in `benchmark/verification_coverage/`. It reruns the +OpenEMR fault experiment of OpenAdaptAI/OpenAdapt#1365 as fresh agent runs, +not rebuilt states, and adds three classes: a concurrent edit by another user +(must stay `verified`), a collateral edit by the bot's own user (must be +caught), and a misread source (must be caught before the save, and by the +round trip if the save happens anyway). The same suite runs on openIMIS. +Results are reported per fault class, before and after, with each run's +engine commit. + +## Implementation plan + +1. This document. +2. Frame conditions: `runtime/effects/frame.py`, the `frame:` section, + attribution reads, and the `checked` field in the receipt. +3. The fault gate: `openadapt_flow/fault_gate.py`, store test copies (SQLite, + an in-memory REST store, and fixture adapters in the benchmark), coverage + records, the admission policy, and `scaffold-verifier` on the gate. +4. Provenance: parameter sources, the deterministic label extractor, the + pre-save cross-check and hold, and the round trip in `verify-run`. +5. The benchmark runs and results. +6. Flow replay: the frame judge and provenance in the replayer, and + `checked` in `report.json`.