fix(transaction): require positive evidence of absence for HALTED_BEFORE_EFFECT - #280
Conversation
be10e7b to
83e1e08
Compare
|
Safety review: the central fix is necessary, but this head is not merge-ready yet because three absence assertions remain unsound.
Please preserve the valuable empty-evidence/commit-timeout fix, but close these three cases before merge. I am holding this PR out of the current #278 -> #275 exact-SHA train until the revised head and full matrix are green. |
…ORE_EFFECT `classify_transaction_outcome` fell through to `HALTED_BEFORE_EFFECT` whenever the coarse outcome was `HALTED`, no policy rejection applied, and `_has_unresolved_uncertainty` was False. That last check iterates `result.effect_evidence`, so when a run aborts before verification runs the list is empty, the loop body never executes, and it returns False. Absence of evidence was read as evidence of absence, in the one place where that is most dangerous. `HALTED_BEFORE_EFFECT` is documented to mean the verifier established that NO business effect occurred; a customer receiving it reconciles nothing. When the backend commits a row and then hangs past the client deadline, the run reported `HALTED_BEFORE_EFFECT` while the store held the write -- an unreconciled mutation in a system of record with no signal it exists. Measured by the committed openadapt-evals probe (PR #272, release 0.90.0) against MockMed's independent store: 7 of 16 applicable runs made a false absence claim, and 14 of 23 claimed proven absence for a consequential step that reached actuation with no verification performed at all. The rule now enforced: no outcome may assert absence while any consequential step's effect is UNKNOWN. For each consequential step the runtime requires either that a verifier settled every declared effect (observed `absent`, or `confirmed` and journaled) or that the step positively stopped before delivery was attempted. This guards `HALTED_BEFORE_EFFECT`, `REJECTED_POLICY`, `CANCELED`, and `FAILED_PLATFORM` alike, since all four assert an absence. Anything else fails toward `RECONCILIATION_REQUIRED`. `_attempt_state` is made fail-closed for the same reason: `not_actuated` is itself an absence claim, so it now requires positive evidence of a pre-delivery stop (a skipped step, a pre-execution gate pseudo-step, or a typed `safety_halt` / `governed_refusal` / unverified pre-click identity check). A step whose delivery was never recorded either way is `delivery_uncertain`. A failed postcondition now counts as proof of delivery -- postconditions are checked after the click, so an over-halt on one shows the write already went out. Same pattern, second instance: `build_effect_journal` read a workflow-step lookup miss as "not consequential" and dropped the step from the journal. An absent lookup is unknown, not a negative, so the report-side mirror now keeps such a step whenever its own typed fields say it could write. `_has_unresolved_uncertainty` is unchanged in behavior but its docstring now states that it reads conflicting evidence only and says nothing about a step with no evidence. Benchmark expectations updated where they pinned the defect. In `ap_invoice` (`missing_po`, `duplicate_invoice`) and `o2c_recon` (`ambiguous_duplicate`, `stale_snapshot`) the API gateway refuses the write and the direct state oracle confirms zero deltas -- but the runtime cannot prove that. `ActuationStatus.HALT` is documented in-tree as "the request WAS sent ... the write may have landed", and no verifier read the system of record afterwards, so these are unverified actuations and now report `RECONCILIATION_REQUIRED`. `missing_in_ledger` (an explicit halt terminal, never actuated) and `phantom_writeback` (the governed arm re-reads the file and establishes absence) correctly REMAIN `HALTED_BEFORE_EFFECT`, which is the discrimination that shows this is not an over-correction. Published `results.json` regenerated and both READMEs updated; the headline claims are unchanged (governed silent-wrong 0, over-halts 0, model calls 0, healthy path VERIFIED). Preserved: a halt genuinely before actuation, and a verifier-established absence, both remain `HALTED_BEFORE_EFFECT`. `COMPLETED_UNVERIFIED` is still never a production success and never billable, only `VERIFIED` is billable, and there is still no blind retry after an uncertain delivery. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NyCHrzA1psrKMFfroYbzaM
622508c to
51a7004
Compare
…tics `paper/check_artifacts.py` pinned four benchmark cells to HALTED_BEFORE_EFFECT that this PR correctly reclassifies as RECONCILIATION_REQUIRED: ap_invoice missing_po and duplicate_invoice, and o2c_recon ambiguous_duplicate and stale_snapshot. All four reach the gateway and are refused or time out, so `ActuationStatus.HALT` applies -- documented in-tree as "the request WAS sent but its outcome is unknown or a rejection" -- and the write may have landed. Claiming proven absence there was the defect. The two cells that keep HALTED_BEFORE_EFFECT are unchanged and are the ones that earn it: `missing_in_ledger` never actuates, and `phantom_writeback` has a verifier that reads the record and finds it absent. That the check still passes for those two is the evidence that the new rule discriminates rather than blanket-downgrades. No paper prose states these per-scenario outcomes, so only the constants moved. `python paper/check_artifacts.py` returns OK. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NyCHrzA1psrKMFfroYbzaM
The adapter-result table already qualifies the `confirmed` row ("run-level
`VERIFIED` is decided by the run classifier") but not the `refuted` row,
so the table reads as though one refuted effect settles the run outcome.
It does not, and has not since #280: run-level `HALTED_BEFORE_EFFECT`
requires absence for every declared effect of every consequential step. The
tutorial's own `?fault=optimistic` probe is exactly this case -- one
refuted effect beside one unverified effect -- and terminates
`RECONCILIATION_REQUIRED`.
Adds the symmetric caveat.
…ly reports `docs/EXECUTION_PROFILES.md` told readers that the tutorial's `?fault=optimistic` probe terminates `HALTED` / `HALTED_BEFORE_EFFECT` "with nothing persisted", and cited `tests/e2e/test_free_path_e2e.py` as the pin. That test pins `RECONCILIATION_REQUIRED`, and has since #280. The prose is what is wrong; the code is right, and deliberately so. #281 wrote the paragraph, #280 then made `HALTED_BEFORE_EFFECT` require positively established absence for every declared effect of every consequential step, flipped the test, and rewrote the taxonomy table in this same file -- but not this paragraph. The document has been self-contradictory since: line 77 claimed `HALTED_BEFORE_EFFECT` for a step that reached actuation, while line 99 said such a step "does not qualify". Measured on the real probe: the save declares 2 mined effects, the retained verifier returns evidence for 1 (`refuted`), and the store is in fact empty -- but only the test's out-of-band `GET /api/db` snapshot knows that. The runtime never held absence evidence for the second effect, so it reports `RECONCILIATION_REQUIRED`. This matters more than a stale line. `HALTED_BEFORE_EFFECT` tells an operator there is nothing to reconcile. Documenting it for a run that cannot support the claim is exactly the failure the transaction taxonomy exists to prevent, described in the file that defines the taxonomy. Rewrites the paragraph to state both probes' real outcome, why the optimistic case cannot claim absence, and that this is the taxonomy working rather than a gap in it.
The adapter-result table already qualifies the `confirmed` row ("run-level
`VERIFIED` is decided by the run classifier") but not the `refuted` row,
so the table reads as though one refuted effect settles the run outcome.
It does not, and has not since #280: run-level `HALTED_BEFORE_EFFECT`
requires absence for every declared effect of every consequential step. The
tutorial's own `?fault=optimistic` probe is exactly this case -- one
refuted effect beside one unverified effect -- and terminates
`RECONCILIATION_REQUIRED`.
Adds the symmetric caveat.
…VERIFIED (#298) * fix(docs): correct the halt outcome the tutorial's fault probe actually reports `docs/EXECUTION_PROFILES.md` told readers that the tutorial's `?fault=optimistic` probe terminates `HALTED` / `HALTED_BEFORE_EFFECT` "with nothing persisted", and cited `tests/e2e/test_free_path_e2e.py` as the pin. That test pins `RECONCILIATION_REQUIRED`, and has since #280. The prose is what is wrong; the code is right, and deliberately so. #281 wrote the paragraph, #280 then made `HALTED_BEFORE_EFFECT` require positively established absence for every declared effect of every consequential step, flipped the test, and rewrote the taxonomy table in this same file -- but not this paragraph. The document has been self-contradictory since: line 77 claimed `HALTED_BEFORE_EFFECT` for a step that reached actuation, while line 99 said such a step "does not qualify". Measured on the real probe: the save declares 2 mined effects, the retained verifier returns evidence for 1 (`refuted`), and the store is in fact empty -- but only the test's out-of-band `GET /api/db` snapshot knows that. The runtime never held absence evidence for the second effect, so it reports `RECONCILIATION_REQUIRED`. This matters more than a stale line. `HALTED_BEFORE_EFFECT` tells an operator there is nothing to reconcile. Documenting it for a run that cannot support the claim is exactly the failure the transaction taxonomy exists to prevent, described in the file that defines the taxonomy. Rewrites the paragraph to state both probes' real outcome, why the optimistic case cannot claim absence, and that this is the taxonomy working rather than a gap in it. * test(e2e): pin HOW the free path reaches VERIFIED, not only that it does `VERIFIED` is one bit, and one bit is a weak release gate. A run can end `VERIFIED` for the wrong reason and every existing assertion in `tests/e2e/test_free_path_e2e.py` stays green: - the structural rung stops resolving and the ladder falls to OCR or geometry -- weaker evidence, same verdict; - an actuation path leaves the DOM for synthesised pointer events; - the save loses its `irreversible` classification, and with it the armed identity gate; - a heal fires on an undrifted screen; - the mined effect contract changes shape, so `VERIFIED` is asserted against a different promise than the one that was reviewed. Adds `tests/golden/tutorial_run.json`: the whole free path projected onto a closed-vocabulary shape -- per step the resolution rung, actuation, delivery status, identity status/mode, risk class, postcondition verdict, heal flag and effect evidence; plus step count, `rung_counts`, identity armed/applicable counts, required/passed contract counts, the mined effect-contract hashes, model calls, cost, and the outcome fields. The comparison walks both documents leaf by leaf and names the exact field that moved rather than dumping two blobs. Determinism: every pinned field was byte-identical across 8 local runs under widely varying machine load. `TutorialResult.bundle_digest` is the one unstable field (the bundle carries retained frames) and is deliberately excluded. Nothing here is a timing, a path, or a temp dir. Mutation proof. Drop the `field_equals` effect from `compiler/effect_mining.py` -- the partial-save catch -- and the free path still reaches `VERIFIED`, `test_free_path_terminates_verified_with_- independent_effect_evidence` still passes, and this is what fails: changed effects_confirmed: golden=2 now=1 changed required_contracts.effect: golden=2 now=1 the run no longer emits steps[5].effect_evidence[1].verdict the run no longer emits effect_journal[0].intended_effect_contract_hashes[1] Cost. Zero additional runner minutes. The assertion reads the report the module-scoped `free_path` fixture already produces, so it adds a comparison, not a run. The `e2e-browser` job now runs that module as its FIRST step and `--ignore`s it from the directory run below, so the core loop answers in the first ~2 minutes of a ~21-minute job instead of the last -- ordering, not spend. No new workflow, no new job, no new required context, and no change to any trigger. Regenerate deliberately, never as a reflex: OPENADAPT_UPDATE_GOLDEN=1 pytest tests/e2e/test_free_path_e2e.py python scripts/check_release_consistency.py --write-public-artifact-inventory Boundary: the artifact is enum names, key names, counts, and contract hashes. No values, no record content, no screen text, no paths, no tuning. Mechanism, not data -- the public side of AGENTS.md 4.2. * docs(effect-kit): note that a refuted STEP is not a refuted RUN The adapter-result table already qualifies the `confirmed` row ("run-level `VERIFIED` is decided by the run classifier") but not the `refuted` row, so the table reads as though one refuted effect settles the run outcome. It does not, and has not since #280: run-level `HALTED_BEFORE_EFFECT` requires absence for every declared effect of every consequential step. The tutorial's own `?fault=optimistic` probe is exactly this case -- one refuted effect beside one unverified effect -- and terminates `RECONCILIATION_REQUIRED`. Adds the symmetric caveat.
The defect (P0 soundness)
classify_transaction_outcome()fell through toTransactionOutcome.HALTED_BEFORE_EFFECTwhenever the coarse outcome wasHALTED, no policy rejection applied, and_has_unresolved_uncertainty(report)was False. Its inline comment asserted "a governed halt with the verifier having established no effect" — but nothing on that path established any such thing._has_unresolved_uncertainty()iteratesresult.effect_evidence. When a run aborts before verification runs, that list is empty, the loop body never executes, and the function returns False. Absence of evidence was read as evidence of absence, in the one place where that is most dangerous.HALTED_BEFORE_EFFECTis documented to mean the verifier established that NO effect occurred. A customer receiving it reconciles nothing. If a write landed, they hold an unreconciled mutation in a system of record with no signal it exists — the exact silent-wrong-effect failure this product is sold against, pointing the other way.Measured consequence
The committed reproduction in
openadapt-evals(merged PR #272, released 0.90.0) judges the taxonomy against MockMed's independent store atGET /api/db, never against the runtime's own report:RECONCILIATION_REQUIREDWhen the backend commits the row then hangs past the client timeout, the run reported
HALTED_BEFORE_EFFECTwhile the store held the write.RECONCILIATION_REQUIREDwas reached only when a configured verifier returned a conflicting reading.The rule implemented
No outcome may assert absence while any consequential step's effect is UNKNOWN.
For each consequential step, one of these must hold:
absent, orconfirmedand journaled; or_attempt_state→not_actuated).Otherwise the run is
RECONCILIATION_REQUIRED. This guardsHALTED_BEFORE_EFFECT,REJECTED_POLICY,CANCELED, andFAILED_PLATFORMalike — all four assert an absence and all four tell the operator to reconcile nothing.Why "settled" rather than "absent": the failure mode being fixed is an unaccounted write. A verifier-confirmed effect is known, journaled, and needs no reconciliation, so it does not by itself flip a later governed halt. Whether a partially-completed run deserves its own label is a separate taxonomy question, flagged in-code and pinned by a test rather than silently decided here.
_attempt_statemade fail-closednot_actuatedis itself an absence claim, so it now requires positive evidence of a pre-delivery stop: a skipped step, a pre-execution gate pseudo-step, or a typedsafety_halt/governed_refusal/ unverified pre-click identity check. A step whose delivery was never recorded either way is nowdelivery_uncertain, notnot_actuated.A failed postcondition now counts as proof of delivery — postconditions are checked after the click, so an over-halt on one shows the write already went out. This is what makes the premature-abort case classify correctly.
Other instances of the same pattern
build_effect_journalread a workflow-step lookup miss as "not consequential" and dropped the step from the journal entirely. An absent lookup is unknown, not a negative; the report-side mirror now retains such a step whenever its own typed fields say it could write._has_unresolved_uncertaintyis unchanged in behavior, but its docstring now states that it reads conflicting evidence only and says nothing about a step with no evidence — so no future caller reads itsFalseas "no effect occurred"._worst_observed_effectwas already correct (no evidence →unknown) and is untouched.Noted but not changed (out of scope, different failure direction — false presence, not false absence):
execution_profiles.classify_execution_outcomedoesif step is None: continue, skipping a result whose step is missing from the workflow rather than failing towardCOMPLETED_UNVERIFIED.Benchmark expectations that pinned the defect
In
ap_invoice(missing_po,duplicate_invoice) ando2c_recon(ambiguous_duplicate,stale_snapshot) the API gateway refuses the write and the direct state oracle confirms zero deltas — but the runtime cannot prove that.ActuationStatus.HALTis documented in-tree as "The request WAS sent but its outcome is unknown or a rejection -> the write may have landed", and no verifier read the system of record afterwards. These are unverified actuations and now reportRECONCILIATION_REQUIRED.That this is not an over-correction is shown by what did not move:
missing_in_ledger— an explicit halt terminal, never actuated → stillHALTED_BEFORE_EFFECTphantom_writeback(governed) — re-reads the file and establishes absence → stillHALTED_BEFORE_EFFECTPublished
results.jsonregenerated and both READMEs updated. The safety headlines are unchanged — governed silent-incorrect-success 0, healthy-path over-halts 0, model calls 0, healthy pathVERIFIED. The only headline number that moves isap_invoice'sgoverned_reconciliation_required, 6 -> 12, which is exactly the 6 runs (2 scenarios x 3) that stopped making an unproven absence claim.Tests
tests/test_transaction_outcome.py25 → 42. 8 of the new tests fail on unmodifiedorigin/mainand pass here (verified in a detached baseline worktree), so none is vacuous.Coverage:
RECONCILIATION_REQUIRED, explicitly notHALTED_BEFORE_EFFECTruntime_failureon a consequential step → fails closedActuationStatus.HALT→RECONCILIATION_REQUIREDREJECTED_POLICY,CANCELED,FAILED_PLATFORMHALTED_BEFORE_EFFECTHALTED_BEFORE_EFFECTHALTED_BEFORE_EFFECT(scope boundary, pinned deliberately)duplicateconflicting-reading case → stillRECONCILIATION_REQUIREDTwo of these run end-to-end through the real
Replayer, using the backend's recorded actions as independent proof of whether the click went out:RECONCILIATION_REQUIRED(this one reproduces the defect onorigin/main)backend.actions == []→HALTED_BEFORE_EFFECTInvariants preserved and re-asserted:
COMPLETED_UNVERIFIEDnever a production success and never billable; onlyVERIFIEDbillable; no blind retry after uncertain delivery.Verification
uvx ruff==0.15.22 check openadapt_flow— passuvx ruff==0.15.22 format --check openadapt_flow tests— pass (428 files)mypy openadapt_flow/transaction.py— passpytest tests/test_transaction_outcome.py tests/test_uncertain_delivery.py tests/test_replayer.py tests/test_run_gate.py tests/test_ap_invoice_benchmark.py tests/test_o2c_recon_benchmark.py tests/test_execution_profiles.py— passOverlap note
PR #279 (
feat: bind PHI-free qualified identity signals) merged as3f34200while this was in flight. This branch is rebased on top of it; #279 did not touchtransaction.py, so there is no conflict. The diff here is deliberately surgical —transaction.py, its tests, the two benchmark suites whose expectations pinned the defect, and theHALTED_BEFORE_EFFECTdocs. Nopaper/**, nobenchmark/effectbench/**.🤖 Generated with Claude Code
https://claude.ai/code/session_01NyCHrzA1psrKMFfroYbzaM