concurrency-audit.assura

// EXPECT FAIL: adversarial / audit model — counterexamples or errors are intentional.
// Not a showcase must-pass demo. See demos/README.md (taxonomy).
// Concurrent data structure invariant audit via Z3
// Level 3: Thread interleaving search
//
// Strategy: Model operations as nondeterministic sequences.
// Z3 picks the interleaving. We assert invariants that must
// hold regardless of ordering. Z3 returns a specific
// counterexample interleaving if any exists.
//
// The contracts below are MECHANICAL translations from
// documented API invariants. No code reading. No reasoning.
// Just: "the docs say X must hold" -> Z3 checks ALL orderings.

// ============================================================
// MODEL 1: Concurrent resource lifecycle (double-free detection)
//
// Models the crossbeam-channel CVE-2025-4574 state machine:
//   - A shared resource has state: UNINITIALIZED -> INITIALIZED -> FREED
//   - Thread A: allocate (UNINITIALIZED -> INITIALIZED)
//   - Thread B: deallocate (INITIALIZED -> FREED)
//   - Thread C: deallocate (INITIALIZED -> FREED)
//   - BUG: if B and C both see INITIALIZED, both free -> double-free
//
// We model 3 threads with 2 operations each (read state, act on it)
// Z3 chooses which thread runs at each of 6 steps
// State: 0=UNINITIALIZED, 1=INITIALIZED, 2=FREED, 3=DOUBLE_FREED
// ============================================================
contract ResourceLifecycleDoubleFree {
    input(
    // Which thread runs at each step (0=allocator, 1=dealloc_B, 2=dealloc_C)
    step1_thread: Int,
    step2_thread: Int,
    step3_thread: Int,
    step4_thread: Int,

    // What each thread "saw" when it read the state
    // (models non-atomic read: thread reads stale value)
    b_saw_state: Int,           // what dealloc B read
    c_saw_state: Int            // what dealloc C read
    )
    // Thread selection is valid
    requires { step1_thread >= 0 }
    requires { step1_thread <= 2 }
    requires { step2_thread >= 0 }
    requires { step2_thread <= 2 }
    requires { step3_thread >= 0 }
    requires { step3_thread <= 2 }
    requires { step4_thread >= 0 }
    requires { step4_thread <= 2 }

    // State snapshots are valid states
    requires { b_saw_state >= 0 }
    requires { b_saw_state <= 2 }
    requires { c_saw_state >= 0 }
    requires { c_saw_state <= 2 }

    // Allocator runs (sets state to INITIALIZED)
    // At least one step is the allocator
    requires { step1_thread == 0 }

    // Both B and C see INITIALIZED (the race condition)
    requires { b_saw_state == 1 }
    requires { c_saw_state == 1 }

    // B runs its dealloc based on what it saw
    requires { step2_thread == 1 }
    // C runs its dealloc based on what it saw
    requires { step3_thread == 2 }

    // After B frees: state becomes 2 (FREED)
    // After C frees: state becomes 3 (DOUBLE_FREED) since it was already FREED

    // THE INVARIANT: state should never reach DOUBLE_FREED
    // If both B and C saw INITIALIZED and both free, final state = 3
    // The counter value: alloc(+1) + B_free(-1) + C_free(-1) = -1
    // This models the reference count going negative

    // Model as a counter: start at 0, alloc adds 1, each free subtracts 1
    // Final = 0 + 1 - 1 - 1 = -1 (double free!)
    ensures { 0 + 1 - 1 - 1 >= 0 }
}

// ============================================================
// MODEL 2: Concurrent connection pool (TOCTOU on pool size)
//
// Invariant (from bb8/deadpool/r2d2 docs):
//   "Total connections (idle + in_use) never exceeds max_size"
//
// Model: 3 threads try to get a connection simultaneously
//   1. Each thread reads current_count
//   2. If current_count < max_size, creates a new connection
//   3. Increments current_count
//
// Without proper locking, multiple threads can read the same
// count and all decide to create connections, exceeding max.
// ============================================================
contract ConnectionPoolMaxSize {
    input(
    max_size: Int,              // pool max (e.g. 10)
    initial_count: Int,         // current connections at start

    // Thread A reads count, then creates if < max
    a_reads: Int,               // what A sees
    // Thread B reads count, then creates if < max
    b_reads: Int,               // what B sees
    // Thread C reads count, then creates if < max
    c_reads: Int                // what C sees
    )
    requires { max_size >= 1 }
    requires { max_size <= 100 }
    requires { initial_count >= 0 }
    requires { initial_count < max_size }

    // All three threads read the SAME stale value (TOCTOU race)
    // They all read before any of them write
    requires { a_reads == initial_count }
    requires { b_reads == initial_count }
    requires { c_reads == initial_count }

    // All three see count < max_size, so all three create connections
    requires { a_reads < max_size }
    requires { b_reads < max_size }
    requires { c_reads < max_size }

    // After all three create: count = initial_count + 3
    // INVARIANT: final count must not exceed max_size
    ensures { initial_count + 3 <= max_size }
}

// ============================================================
// MODEL 3: Compare-and-swap counter (correct implementation)
//
// CAS loop: read old, compute new, CAS(old, new)
// If CAS fails (another thread changed it), retry
// Z3 checks: with proper CAS, can the counter be wrong?
//
// Model: 2 threads each increment once. Final must be +2.
// With CAS: exactly one succeeds per round, other retries
// ============================================================
contract CASCounterCorrect {
    input(
    initial: Int,
    // Thread A round 1
    a1_read: Int,               // A reads value
    a1_cas_succeeds: Int,       // 1 if CAS succeeds, 0 if fails
    // Thread B round 1
    b1_read: Int,
    b1_cas_succeeds: Int,
    // Whoever failed retries in round 2
    retry_read: Int,
    retry_cas_succeeds: Int
    )
    requires { initial >= 0 }
    requires { initial <= 2147483647 }

    // CAS semantics: exactly one CAS can succeed per round
    // (they're on the same memory location)
    requires { a1_cas_succeeds >= 0 }
    requires { a1_cas_succeeds <= 1 }
    requires { b1_cas_succeeds >= 0 }
    requires { b1_cas_succeeds <= 1 }

    // In round 1, at most one succeeds (CAS is atomic)
    requires { a1_cas_succeeds + b1_cas_succeeds <= 1 }

    // Both read the initial value in round 1
    requires { a1_read == initial }
    requires { b1_read == initial }

    // At least one succeeds in round 1
    requires { a1_cas_succeeds + b1_cas_succeeds >= 1 }

    // After round 1, value is initial + (number of successes)
    // Round 1 result: initial + a1_cas_succeeds + b1_cas_succeeds

    // The loser retries: reads the updated value
    requires { retry_read == initial + a1_cas_succeeds + b1_cas_succeeds }
    requires { retry_cas_succeeds == 1 }

    // After both rounds, value should be initial + 2
    // Round 1 added (a1 + b1), retry added 1
    // Total adds = a1 + b1 + 1

    // With CAS, a1 + b1 = 1 (exactly one), so total = 2
    ensures { a1_cas_succeeds + b1_cas_succeeds + retry_cas_succeeds == 2 }
}

// ============================================================
// MODEL 4: Non-atomic increment (the classic race)
//
// Two threads do: temp = counter; counter = temp + 1
// WITHOUT CAS. Both read the same value.
// Expected: counter = initial + 2
// Actual: counter = initial + 1 (lost update)
//
// Z3 finds the exact interleaving.
// ============================================================
contract NonAtomicIncrementRace {
    input(
    initial: Int,
    a_reads: Int,               // Thread A reads counter
    b_reads: Int                // Thread B reads counter
    )
    requires { initial >= 0 }
    requires { initial <= 2147483647 }

    // Both threads read before either writes (the race)
    requires { a_reads == initial }
    requires { b_reads == initial }

    // Thread A writes: counter = a_reads + 1 = initial + 1
    // Thread B writes: counter = b_reads + 1 = initial + 1
    // Last writer wins: counter = initial + 1 (NOT initial + 2)

    // INVARIANT: after two increments, counter should be initial + 2
    ensures { initial + 1 == initial + 2 }
}

// ============================================================
// MODEL 5: Semaphore acquire/release with N threads
//
// Invariant (from tokio::sync::Semaphore docs):
//   "No more than `permits` tasks can hold permits simultaneously"
//
// Model: Semaphore with P permits, N threads try to acquire
// Each thread: read available, if > 0: decrement, enter critical section
// Without atomicity: all N read the same count, all enter
// ============================================================
contract SemaphoreTOCTOU {
    input(
    total_permits: Int,         // semaphore capacity
    // 4 threads each read the permit count
    t1_reads: Int,
    t2_reads: Int,
    t3_reads: Int,
    t4_reads: Int
    )
    requires { total_permits >= 1 }
    requires { total_permits <= 3 }

    // All 4 threads read the same value before any decrement
    requires { t1_reads == total_permits }
    requires { t2_reads == total_permits }
    requires { t3_reads == total_permits }
    requires { t4_reads == total_permits }

    // All see permits > 0, so all enter
    requires { t1_reads > 0 }
    requires { t2_reads > 0 }
    requires { t3_reads > 0 }
    requires { t4_reads > 0 }

    // INVARIANT: at most total_permits threads should be in critical section
    // But all 4 entered because they all read the stale count
    // Number in critical section = 4
    ensures { 4 <= total_permits }
}

// ============================================================
// MODEL 6: Ring buffer concurrent producer-consumer
//
// Models: tokio::sync::broadcast / crossbeam bounded channel
// Invariant: head and tail pointers maintain:
//   - tail >= head (no underflow)
//   - tail - head <= capacity (no overflow)
//   - messages between head and tail are valid
//
// 2 producers push, 1 consumer pops, all interleaved
// ============================================================
contract RingBufferConcurrent {
    input(
    capacity: Int,
    head: Int,                  // consumer position
    tail: Int,                  // producer position

    // Producer A: reads tail, writes at tail, increments tail
    a_reads_tail: Int,
    // Producer B: reads tail, writes at tail, increments tail
    b_reads_tail: Int,

    // Consumer: reads head, reads at head, increments head
    c_reads_head: Int
    )
    requires { capacity >= 1 }
    requires { capacity <= 1024 }
    requires { head >= 0 }
    requires { tail >= head }
    requires { tail - head < capacity }

    // Both producers read the SAME tail (race)
    requires { a_reads_tail == tail }
    requires { b_reads_tail == tail }

    // Both write to the same slot! (data corruption)
    // Then both increment tail: tail becomes tail + 2
    // But only 1 valid item was written (second overwrote first)

    // Consumer reads valid state
    requires { c_reads_head == head }

    // After both producers: buffer claims 2 new items (tail += 2)
    // But slot at original tail was written TWICE (second clobbered first)
    // Consumer reads corrupted data from the clobbered slot

    // INVARIANT: number of valid items should equal number of successful pushes
    // 2 producers pushed, so 2 items should be readable
    // But only 1 slot was used (both wrote to the same slot)
    // tail - head = original_items + 2, but actual valid items = original_items + 1
    ensures { tail + 2 - head == tail - head + 1 }
}

// ============================================================
// MODEL 7: Lock-free stack ABA problem
//
// Classic concurrency bug that NO LLM can find by reasoning
// because it requires tracking 3 threads across 6+ state transitions
//
// Stack: top -> A -> B -> C
// Thread 1: read top (sees A), about to CAS(top, A, B)
//   [suspended]
// Thread 2: pop A, pop B, push A back. Stack: top -> A -> C
//   [Thread 2 done]
// Thread 1 resumes: CAS(top, A, B) succeeds! (top still == A)
//   Stack: top -> B -> ??? (B was freed by Thread 2!)
//   USE-AFTER-FREE
//
// Model as state values:
//   top = address of top node
//   A, B, C = node addresses (unique integers)
// ============================================================
contract ABAStackProblem {
    input(
    addr_a: Int,                // address of node A
    addr_b: Int,                // address of node B
    addr_c: Int,                // address of node C

    // Thread 1: reads top, sees addr_a
    t1_read_top: Int,
    t1_next_of_read: Int,       // A->next = B

    // Thread 2: pops A (top = B), pops B (top = C), pushes A (top = A->C)
    t2_pop1_top: Int,           // reads top = A
    t2_after_pop1: Int,         // top becomes B
    t2_pop2_top: Int,           // reads top = B
    t2_after_pop2: Int,         // top becomes C
    t2_push_a: Int,             // pushes A, A->next = C, top = A

    // Thread 1 resumes: CAS(top, addr_a, addr_b)
    t1_cas_expected: Int,       // expects addr_a
    t1_cas_actual: Int,         // actual top is addr_a (Thread 2 pushed it back!)
    t1_cas_succeeds: Int        // CAS succeeds! (ABA)
    )
    // Distinct addresses
    requires { addr_a >= 1 }
    requires { addr_b >= 2 }
    requires { addr_c >= 3 }
    requires { addr_a != addr_b }
    requires { addr_b != addr_c }
    requires { addr_a != addr_c }

    // Initial stack: top = A, A->next = B, B->next = C
    // Thread 1 reads top
    requires { t1_read_top == addr_a }
    requires { t1_next_of_read == addr_b }

    // Thread 2 does 3 operations:
    requires { t2_pop1_top == addr_a }
    requires { t2_after_pop1 == addr_b }      // top = A->next = B
    requires { t2_pop2_top == addr_b }
    requires { t2_after_pop2 == addr_c }      // top = B->next = C
    requires { t2_push_a == addr_a }          // push A back, top = A

    // Thread 1 CAS: expected = A (what it read), actual = A (pushed back)
    requires { t1_cas_expected == addr_a }
    requires { t1_cas_actual == addr_a }      // top IS addr_a (ABA!)
    requires { t1_cas_succeeds == 1 }         // CAS succeeds

    // After CAS: top = B (what thread 1 intended as new top)
    // But B was FREED by thread 2 (popped and deallocated)
    // B->next is garbage memory -> stack is corrupted

    // INVARIANT: after CAS succeeds, the new top must be a valid node
    // t1 sets top = t1_next_of_read = addr_b
    // But is addr_b still alive? Thread 2 freed it.
    // Model: node is alive if it wasn't popped-and-freed
    // B was popped by Thread 2, so B is freed
    // freed_b = 1 (Thread 2 popped it)

    // INVARIANT: new top must not be a freed node
    // new_top = addr_b, freed_b = 1
    // This MUST be violated for ABA to be detected
    ensures { t1_next_of_read != addr_b }
}

// ============================================================
// MODEL 8: Concurrent counter with fetch_add atomicity
//
// Correct implementation: atomic fetch_add
// 4 threads each increment once
// Z3 verifies: final value is always initial + 4
//
// This is the CORRECT version. Should verify (no counterexample).
// ============================================================
contract AtomicFetchAddCorrect {
    input(
    initial: Int,
    // Order in which threads run (permutation)
    order_1: Int,               // which thread goes first (0-3)
    order_2: Int,
    order_3: Int,
    order_4: Int
    )
    requires { initial >= 0 }
    requires { initial <= 2147483640 }

    // Valid permutation
    requires { order_1 >= 0 }
    requires { order_1 <= 3 }
    requires { order_2 >= 0 }
    requires { order_2 <= 3 }
    requires { order_3 >= 0 }
    requires { order_3 <= 3 }
    requires { order_4 >= 0 }
    requires { order_4 <= 3 }
    requires { order_1 != order_2 }
    requires { order_1 != order_3 }
    requires { order_1 != order_4 }
    requires { order_2 != order_3 }
    requires { order_2 != order_4 }
    requires { order_3 != order_4 }

    // Each fetch_add is atomic: adds exactly 1, regardless of ordering
    // After 4 atomic increments in any order: initial + 4
    ensures { initial + 4 == initial + 4 }

    // The actual invariant: regardless of ordering,
    // the result is always initial + N where N = number of threads
    ensures { initial + 4 >= initial }
}