TOCTOU race synthesizer

Four check-then-act race detectors that cover the highest-impact shapes outside the file-race surface the existing detector already handles. Each rule emits when the check and the act sit in the same function body without an atomic guard between them.

Rule	Shape	Severity
TOCTOU-DB-001	SELECT ... FROM x WHERE id = ? followed by UPDATE x SET ... WHERE id = ? with no FOR UPDATE, with_lock, version stamp, or transaction-level isolation between them	High
TOCTOU-BALANCE-001	balance >= amount check followed by balance -= amount / UPDATE wallets SET balance = balance - ? WHERE id = ? without the check folded into the same UPDATE's WHERE	Critical
TOCTOU-QUEUE-001	SELECT * FROM jobs WHERE status = 'pending' followed by UPDATE jobs SET status = 'running' WHERE id = ? without a WHERE status = 'pending' predicate	High
TOCTOU-IDOR-ACL-001	can_access(user, resource_id) / is_owner(...) / has_permission(...) followed by a mutation on the same id without a refetch + recheck under transaction	Medium

TOCTOU-BALANCE-001: the double-spend shape

This is the classic gift-card / wallet / credit-pool race:

async def pay(user_id, amount):
    if balance >= amount:        # check
        balance -= amount        # act
        db.execute("UPDATE wallets SET balance = ? WHERE id = ?", (balance, user_id))

Two concurrent requests both pass the check. Both subtract the amount. The wallet goes negative by amount while the user gets two purchases.

Fix. Fold the check into the act:

async def pay(user_id, amount):
    result = db.execute(
        "UPDATE wallets SET balance = balance - $1 WHERE id = $2 AND balance >= $1",
        (amount, user_id),
    )
    if result.rowcount != 1:
        raise InsufficientBalance()

The database's row-level locking now guarantees the check and the act are atomic.

Pairs with

• toctou_file_race.rs (existing detector) for the filesystem-shaped race.
• Reverse-reach to find every entry point that can race a flagged check-then-act pair.