[abrichr]

Part 1 of the design in #1434 (docs/VERIFICATION_COVERAGE.md): frame conditions for verify-run and the guarded save.

Problem

In #1365's OpenEMR fault run, verify-run reported verified on all 5 saves where another chart was edited in place. #1375 added forbid_collateral_change, but it judges one effect at a time. Two effects on one read set flag each other's targets, a stray added record passes, and it can't tell a legitimate edit by another user from a stray write.

Change

• runtime/effects/frame.py: judge_frame compares the whole read set before and after the save, once per contract. Any record that no effect declares and that was added, removed or changed is a frame change. So is a pre-existing target changed outside the fields the effects name.
• Attribution (optional frame.attribution):
  • audit_read: a second read-only read of the app's audit log. Entries new since the baseline are the window.
  • record_field: a modified-by field plus a version or ETag on each record.
  • A change attributed to another user is a concurrent edit and doesn't count. A change by the bot's own ids (self, literals or params), or one nothing explains, is collateral. With audit_read, a bot log entry on an undeclared record is collateral even if the read shows no change.
• verify-run:
  • The audit read is stored with the baseline.
  • With a baseline, the frame judge replaces the per-effect collateral rules, unless the file sets those rules explicitly. A frame refutation also makes effect_verdict REFUTED, so older readers see what they saw before.
  • Without a baseline the frame is not_checked and the run is not verified.
• Receipt: a new optional signed field, checked: {delta, frame, source}. source is instruction here (the --params); provenance comes in a later PR. verified requires every part, which receipt_problem and countersign verify both enforce. evidence.frame holds counts and field names only, never records or actors.
• countersign verify prints a "Checked" line. qualify ignores frame:, so one verify.yaml still serves both commands.

Safety review: changes to when verified is issued

Coordinator review requested (local_bcd23d2d) before merge.

1. No baseline means no verified. Before, an absolute-count contract could verify without one.

2. A record added to the read set that no effect declares now refutes.

3. A wrong-patient write is reconciliation_required, no longer halted_before_effect. A record was written; test_wrong_patient_is_refuted changed accordingly.

4. Two effects on one read set no longer refute each other's targets.

5. The only loosening, with the review's three conditions (commit 81034b7, a test each):

   • (a) evidence the bot can't write only: the app's audit log, or record fields declared server-set per app (server_set). A field the run writes, or a run parameter names, refuses attribution.
   • (b) the executor's own id is one of the bot's ids, never "another user".
   • (c) another actor's change to a record the save declares blocks verified (target_changed_by_other); only changes outside the declared delta are excused.

   Before the conditions: a change that an audit log or a modified-by field with a new version attributes to a named non-bot user is not collateral. Unattributed changes, and an unreadable log, still refute.

Flow replay's verified is unchanged by this PR; the design doc says so and plans it separately.

Tests

• tests/test_frame_conditions.py (28): the judge, both attribution kinds, verify-run end to end on MockMed, and a SQLite store with its own audit log where another user's edit stays verified and the bot's own edit is refuted.
• Ran locally: 81 receipt, seal, countersign, qualify, guard, verify-run, effect and record-check test files. 1756 passed, 1 failed. The failure (test_qualification_gate_campaign::test_cli_durable_authority_failure_preserves_the_original_failure) fails the same way on a clean origin/main checkout here.
• ruff, and mypy on the changed modules.

The fresh OpenEMR and openIMIS benchmark runs follow in their own PR.

🤖 Generated with Claude Code

[abrichr]

Coordinator safety review: approve at 81034b7.

• Attribution comes only from per-app server-set fields or the audit log. A field the run writes, or a run parameter names, refuses attribution.
• The executor's id counts as the bot's own.
• Another actor's change to a declared record blocks VERIFIED (reconciliation_required, target_changed_by_other).
• Unattributed changes still refute.
  Merge when green.

🤖 Generated with Claude Code