Random Module

ESBMC models Python’s random module using nondeterministic values constrained by __ESBMC_assume. This replaces true pseudo-randomness with symbolic nondeterminism, allowing ESBMC to explore all values a random call could produce and verify properties that must hold for any outcome.

Supported Functions

random.randint(a, b)

Returns a nondeterministic int N such that a ≤ N ≤ b (inclusive on both ends, matching CPython semantics).

import random
x: int = random.randint(1, 10)
assert x >= 1 and x <= 10  # always holds

random.random()

Returns a nondeterministic float in the half-open interval [0.0, 1.0).

import random
x: float = random.random()
assert x >= 0.0 and x < 1.0  # always holds

random.uniform(a, b)

Returns a nondeterministic float in [min(a,b), max(a,b)]. Handles reversed bounds (a > b) by swapping the constraint direction.

import random
x: float = random.uniform(2.5, 5.0)
assert x >= 2.5 and x <= 5.0  # always holds

random.getrandbits(k)

Returns a nondeterministic non-negative int in [0, 2**k − 1]. Raises ValueError if k < 0; returns 0 when k == 0.

import random
x: int = random.getrandbits(8)
assert x >= 0 and x <= 255  # always holds

random.randrange(stop) / random.randrange(start, stop[, step])

Returns a nondeterministic integer selected from the same range as range(start, stop, step). Raises ValueError for a zero step or an empty range.

import random
x: int = random.randrange(10)          # in [0, 9]
y: int = random.randrange(0, 20, 2)   # one of 0, 2, 4, …, 18
assert x >= 0 and x < 10
assert y % 2 == 0 and y >= 0 and y < 20

random.choice(seq)

Returns a nondeterministic element seq[i] for an index constrained to [0, len(seq) - 1]. Raises IndexError on an empty sequence (matching CPython).

import random
xs = [10, 20, 30]
v: int = random.choice(xs)
assert v == 10 or v == 20 or v == 30   # always holds

random.sample(population, k)

Under-approximation: returns the first k elements of population as a fresh list. Raises ValueError when k < 0 or k > len(population). A precise model would pick k distinct nondeterministic indices; that is out of scope for the current stub.

import random
xs = [1, 2, 3, 4]
s = random.sample(xs, 2)
assert len(s) == 2                     # always holds

random.shuffle(lst)

Under-approximation: leaves lst untouched. A precise model would express the permutation symbolically; the current stub keeps the operation a no-op so callers that only rely on length / membership remain sound. Properties that depend on a specific reshuffled order cannot be verified.

random.seed(a=0)

No-op stub. Because the nondeterminism of nondet_int / nondet_float already ranges over every seed-dependent outcome, seeding the model has no observable effect under verification.

Unsupported Functions

Functions outside the list above (e.g. triangular, gauss, betavariate, …) are not yet modelled.

Modelling Approach

Each supported function calls an ESBMC nondeterministic primitive (nondet_int() or nondet_float()) and immediately constrains the result with __ESBMC_assume(). From the solver’s perspective the return value is a free variable bounded by the assume — equivalent to quantifying over all values in the range.

This means:

• Assertions that must hold for all outcomes are verified soundly.
• random.seed() has no effect — the model is stateless; seeding cannot make results deterministic.
• Distribution is irrelevant — ESBMC considers every value in the range equally, so statistical properties (expected value, variance) cannot be verified with this model.