# Negative testing: rejected transfer, committed debit

This original instructional fixture runs real SQLite statements through the exact
`transfer_baseline` and `transfer_corrected` functions in `transfer.py`. It is not a
customer incident or an abstract arithmetic model. No Proof service, credential,
package installation, or network access is required.

## Run

Use Python 3.10 or newer with its standard-library `sqlite3` module. From this
directory:

```sh
python3 reproduce.py
```

The output directory `rerun-output/` must be absent or empty. To preserve a
previous run, choose a fresh directory:

```sh
python3 reproduce.py --output-dir another-run
```

The wrapper exits **0 only when the complete experiment is reproduced**. This
includes two children that must fail. Wrapper success does not accept the buggy
implementation. Inspect `reproduction-summary.json` and the raw child stdout and
stderr files in the chosen output directory.

For individual gates:

```sh
python3 run_cases.py --implementation baseline --gate response
python3 run_cases.py --implementation baseline --gate effects
python3 run_cases.py --implementation corrected --gate effects
python3 run_cases.py --implementation reject-all --gate effects --cases positive
```

Expected results:

| Child gate | Passed cases | Failed cases | Exit code |
| --- | ---: | ---: | ---: |
| Baseline, response only | 7 | 0 | 0 |
| Baseline, response plus effects | 5 | 2 | 1 |
| Corrected, response plus effects | 7 | 0 | 0 |
| Reject-all stub, two positive controls | 0 | 2 | 1 |

## Contract and oracle

Money is integer cents. Every case starts with Alice at 10,000 cents, Bob at
2,500 cents, no transfer records, and no active transaction. The exact admitted
scenario set, expected responses and literal expected poststates are in
`cases.json`; full scope and exclusions are in `contract.json`.

There are **five rejection scenarios**: missing destination, insufficient balance,
zero amount, negative amount, and an injected database failure after debit. There
are **two successful controls**: a 2,000-cent transfer and a full 10,000-cent
transfer. Each case uses a fresh on-disk SQLite database and calls the exact
selected implementation once. Case invocations are not unique production inputs,
customer transactions or coverage of a wider domain.

The response-only gate checks the exact returned result but ignores side effects
when deciding acceptance. It still records those effects. The strengthened gate
uses its own SQL observer and the independent literal expectations to compare
both account rows and **all transfer rows after closing and reopening the
database**, and verifies that the function left no transaction open. It does not
merely compare a total or reimplement the transfer calculation.

## The observed defect

The connection explicitly pins `autocommit=LEGACY_TRANSACTION_CONTROL` on Python
3.12 and newer; Python 3.10/3.11 use their existing legacy behavior. With this mode,
`isolation_level=None` prevents implicit Python-managed transactions. It is not
the same setting as `Connection.autocommit=True`.

The baseline uses that connection and never issues `BEGIN`, so its debit
statement is committed before it checks whether the destination exists. It returns
`unknown_destination` but persists Alice at 8,000 cents and Bob at 2,500 cents,
with no transfer record. The promised rejected state was 10,000 / 2,500 cents and
no record.

The test-only `fail_after_debit` seam causes a real zero-amount transfer-record
INSERT immediately after the actual debit. SQLite raises `IntegrityError` from
the `CHECK` constraint. In the baseline, that failed statement does not undo the
earlier autocommitted debit; the same 8,000 / 2,500 partial state persists. The
fault seam is not a public request parameter and does not establish external
attacker reachability.

The corrected implementation issues `BEGIN IMMEDIATE`, checks destination before
writing, and explicitly rolls back any caught SQL error. Its trace shows the
temporary debit while `in_transaction` is true, followed by the actual constraint
error and explicit rollback. Reconnecting observes the original 10,000 / 2,500
state. Normal successful cases commit the exact expected balances and one exact
transfer record.

The reject-all stub is deliberately useless. Both positive controls fail against
it, demonstrating that a handler cannot satisfy the full gate just by refusing
every operation.

## Retained evidence and limits

The published kit's `observed/` directory contains the original raw stdout,
stderr, UTC start/finish timestamps, commands, source hashes, Python/SQLite
versions, connection settings, immediate and reconnected states, and event traces.
`PROVENANCE.json` identifies this observation. `SHA256SUMS` covers all other
retained files in the kit. A new local run preserves the same categories in its
chosen output directory and may have different timestamps or runtime versions.

This checks seven scenarios from one starting state, not all inputs or possible
failures. It does not test concurrent callers, lock contention, crash or power
loss, full disks, corrupt databases, authorization or repeated-request semantics.
`BEGIN IMMEDIATE` is outside the corrected function's protected write body; a
failure to acquire a transaction can propagate. That path is outside this fixture's
single-connection, uncontended preconditions and has not been accepted by this run.
It makes no idempotency or at-most-once claim. There are no notifications, emails,
or external calls, so no cross-system atomicity or delivery is claimed. Temporary
databases are deleted after their reconnected states have been captured.