Summary

Vera has no random number generation capability. This blocks games, simulations, shuffling algorithms, Monte Carlo methods, and randomized initial states (e.g., Conway's Game of Life).

Proposed API

New Random effect with three operations:

effect Random {
    random_int(@Int, @Int) -> @Int        // inclusive range [low, high]
    random_float() -> @Float64            // uniform [0.0, 1.0)
    random_bool() -> @Bool                // coin flip
}

Functions using randomness must declare effects(<Random>), making non-determinism visible in the type signature.

Implementation

• environment.py: Register Random effect with three operations
• codegen/api.py: Host imports using Python's random module (random.randint, random.random(), random.choice([True, False]))
• wasm/calls.py: Wire effect operations to host imports
• Browser runtime: Math.random() for float, derive int and bool from it
• Verification: Random operations return unconstrained values in Z3 (no useful axioms to assert)

Why an effect, not a built-in function?

Randomness is a side effect — the same call returns different values each time. Modelling it as an effect:

1. Makes non-determinism visible in function signatures
2. Enables deterministic testing via handle[Random] with seeded/fixed values
3. Follows Vera's design principle that all side effects are tracked

Future work

• random_seed(@Nat) -> Unit operation for reproducible sequences
• array_shuffle built-in that requires effects(<Random>)