Property-based and differential testing across Awa #562

Why

The property tests added for staged follow-ups in #557 found three classes of bug in one pass that the example-based tests had missed:

• A completion that could never commit. A staged run_at outside Postgres's timestamp range was accepted, and then rolled back every completion attempt. Proptest shrank it to one second before 4714 BC.
• Six differences between the Python HandlerJob test stand-in and the runtime: NUL characters, non-string JSON keys, float integers, a bare string as tags, None meaning the default, and a 64-bit overflow.
• Queue storage: inserts fail for queue names longer than 59 bytes (pg_notify channel limit) #560, a bug that predates the staging work. Queue storage cannot insert into a queue whose name is longer than 59 bytes, on any insert path.

All three sit where several inputs interact at their limits, or where two implementations of the same contract drift apart. Awa has many such places: two storage engines, Rust and Python front ends, test harnesses that imitate the runtime, and TLA+ models whose invariants are never checked against the real system. This issue proposes applying the approach across the codebase.

Approach

• Properties run against Postgres wherever the invariant involves SQL. Pure functions get fast in-process properties.

• Differential testing is the main oracle:

  • canonical against queue storage;
  • Rust against Python;
  • test harness and stand-in against the runtime;
  • single insert against batch insert and COPY.

  Where two implementations promise the same contract, a generated input that separates them is a bug in one of them.

• Model-based (stateful) tests apply random sequences of operations to the system and to an in-memory reference model, compare the observable state, and check invariants after every step.

• TLA+ invariants serve as runtime oracles. The invariants the models prove, such as AtMostOneCompletion, CompletionByCurrentLease and UniqueKeyExclusive, become SQL assertions after random concurrent schedules. That checks the code, not just the model.

• Reproducible and shrinking. Rust uses proptest, with proptest-state-machine for the stateful tests. Python uses hypothesis, with RuleBasedStateMachine for the stateful tests. A failure must print its seed and a minimal case.

Targets

P0

1. Insert parity across engines. For any args and InsertOpts, both engines either reject the request with the same error class, or accept it and store equal rows (kind, queue, priority, run_at, metadata, tags, unique key, ordering key). The property covers insert, insert_many, Rust COPY, Python bulk insert and inserts inside a transaction. It would have found Queue storage: inserts fail for queue names longer than 59 bytes (pg_notify channel limit) #560 directly.
2. Lifecycle state machine. Random sequences drawn from these operations: insert, claim, complete, retryable and terminal failure, snooze, cancel (handler and admin), heartbeat, deadline and callback rescue (with simulated time), callback register, resume and resolve, DLQ retry and purge, and admin retry. They run against a reference model on both engines. Invariants:
   • only legal transitions occur;
   • attempts are counted correctly, with snooze not spending one and rescues bounded by max_attempts;
   • at most one live lease per job;
   • conservation: every job is in exactly one state or in the DLQ;
   • unique claims are exclusive;
   • both engines show the same observable state.
3. Concurrent schedules checked against the TLA+ invariants. Run several workers, inject connection drops, lose responses after a commit, and race rescue against completion. Afterwards, assert the model invariants in SQL.

P1

4. Unique keys (awa-model/src/unique.rs).
   • A key is deterministic and does not depend on the order of keys in a JSON object.
   • The semantics of by_queue, by_args, by_period and the state bitmask hold.
   • Rust and Python compute the same key for the same request.
5. Cron (awa-model/src/cron.rs, correctness/cron-compat).
   • Next and latest fire times are monotonic.
   • No fire is missed or duplicated across DST transitions and arbitrary time zones.
   • The evaluator enqueues each fire at most once, including under concurrent evaluators.
6. Ordering keys and partitioned queues.
   • Routing by key is deterministic and identical in Rust and Python.
   • FIFO order is preserved per key under random enqueue and claim when enqueue_shards > 1.
7. Backoff and priority aging. Backoff stays within the 24 h cap and its jitter range and is monotonic in the attempt number. Aging never escapes its bounds.
8. Callback CEL.
   • Precedence (filter, then on_fail, then on_complete, then the default action) matches a reference interpreter.
   • Behaviour on evaluation errors and transform fallback are as documented.
   • No payload or expression makes the evaluator panic.
9. Batch operations (ADR-030). For random filters and data, the preview count equals the affected rows, pagination is stable, and resuming after an interruption is idempotent.
10. Round trips and merges.
    • JobRow survives the admin API as JSON.
    • Args convert between Rust and Python (dataclass, pydantic, dict).
    • update_metadata and progress merges agree with a model.
11. Rate limiting. The token bucket never exceeds its configured rate over any window of simulated time.
12. Harness parity, beyond staging. awa-testing::TestClient and the Python AwaTestClient and HandlerJob agree with the runtime for random handler outcomes and options.

P2

13. Admin and HTTP API fuzzing (awa-ui): random query parameters and bodies produce validation errors, never 500s.
14. Migration preservation. A random job population created at the oldest supported schema shows the same observable state after migrate, including the 0.6 → 0.7 queue-storage transition.
15. Operator skip rules (ADR-047, ADR-047: operator skip rules #561), once they exist: the preview count agrees with what enforcement matches, and an evaluation error never matches.

Infrastructure

• Shared generators. Valid and hostile names, JSON, timestamps, InsertOpts and unique options in one place, for example awa-testing::arb and a Python awa.testing.strategies module. Start from awa/tests/staged_follow_up_props.rs and awa-python/tests/test_staged_follow_up_fuzz.py.
• Budgets.
  • PRs: small case counts so the rest shard stays fast.
  • Nightly: a workflow with large counts and random seeds that opens an issue on failure, with the seed and the minimal case.
  • Knobs: PROPTEST_CASES, a Hypothesis profile, AWA_FUZZ_SEED and AWA_FUZZ_CASES.
• Regressions. Commit proptest-regressions/ files and Hypothesis examples, so a shrunk case found once runs forever after.
• CI dependencies. hypothesis (and proptest-state-machine) must be added to the Python install lines in ci.yml. CI installs those packages explicitly, not from the dev group.
• Known limits to keep in generators until they're fixed: Queue storage: inserts fail for queue names longer than 59 bytes (pg_notify channel limit) #560 (queue names longer than 59 bytes under queue storage).

Acceptance

• Each P0 target lands with a mutation check: a deliberately seeded bug that the property catches, as Handler-staged follow-up jobs (ADR-046) #557 did for the staging properties.
• Every bug a property finds is either fixed in the same PR or filed and linked from the generator that works around it.
• The nightly job has run for two weeks without unexplained failures.