Randomness

random gives your app random tokens, codes, whole numbers, shuffles and samples. In production it reads the operating system's cryptographic generator. In a test it gives the same values on every run, as a test's clock is fixed, so a test can name the very values it expects.

random is a generated namespace, like clock, and only actions, tests and fixtures call it. A function is pure, so calling random from one is type.random_context. Every value it hands out is recorded for replay, since randomness is one of the effects a replayed request depends on (What the graph and production evidence add).

A shop gives each order a reference a customer reads out on the phone and a cancel link no one types; a board game throws a die; a quiz asks its rounds in a random order and a prize draw picks its winners:

type OrderReference = Text {}type CancelToken = Text {}type DiceRoll = Int {    min: 1    max: 6}type Entrant = Text {    max_length: 40}type WinnerCount = Int {    min: 0    max: 10}/// An order's reference, which a customer reads out on the phone.action new_order_reference() -> OrderReference {    return OrderReference(random.code(8))}/// The token in a booking's cancel link, which no one types.action new_cancel_token() -> CancelToken {    return CancelToken(random.token())}/// A die's throw in a board game.action throw_die() -> DiceRoll {    return DiceRoll(random.integer(1, 6))}/// The order a quiz asks its rounds in.action round_order(quiz_rounds: List<Entrant>) -> List<Entrant> {    return random.shuffle(quiz_rounds)}/// A prize draw's winners, each entrant at most once.action prize_winners(entrants: List<Entrant>, count: WinnerCount) -> List<Entrant> {    return random.sample(entrants, count)}

test "an order's reference is the same on every run" {    var reference: OrderReference = new_order_reference()    assert reference == "QHSF1J29"    assert text.length(new_cancel_token()) == 43}test "a prize draw picks different entrants" {    var winners: List<Entrant> = prize_winners(["Ada", "Grace", "Alan", "Edsger"], 2)    assert winners == ["Alan", "Edsger"]    assert list.count(round_order(["Ada", "Grace", "Alan"])) == 3}

Every value is as likely as every other

• A token is 32 bytes as Base64url without padding.
• A code's character is the low five bits of its own byte, so each of the 32 characters is as likely.
• A whole number is drawn by rejection: a 64-bit draw below 2^64 mod the count is drawn again, then the remainder is taken, so the low numbers aren't favoured. The whole range of Int is a draw itself.
• A shuffle is Fisher and Yates's. A sample is the first count steps of one, so its items are in random order too.

Where the random bytes come from

Every draw takes its bytes from one source, the invocation's context: a replayed run's recorded bytes first, then the host's generator, then the test's seed. With none of them, the call is a fault (internal_fault), never a weaker value. The native host reads the operating system's generator (getrandom(2), getentropy), and the Workers host reads the Web Crypto API's.

The same values on every test run

A test's seed is its own, made from the test's key alone, not from the run. So every run gives a test the same values, whatever seed orders the run, and a test can name the very code it expects. New identities share the seed, so they don't change with the order seed either. --seed decides only the order tests run in.

Replaying a recorded run

While a run is recorded, every random byte handed out is kept on its tape. A replayed run is given them back in order, so it makes the same tokens, codes and shuffles; when they run out there is no randomness to give. The bytes the runtime makes credentials from are kept off the tape (Recordings for replay).

What the checker proves

random.integer(1, 6) is proved to give 1 to 6 for the type it builds, so DiceRoll(random.integer(1, 6)) needs no attempt arm. The proof comes from the arguments' bounds, not their order: min above max is a defect where it runs, as overflow is. The checker proves a code's length from 4 to 32 and a sample's count not negative, as it does temporal.occurrences' count and list.slice's.

Not built yet: jadpo replay itself (Debugging and review). Since the recorded bytes can hold tokens, nothing writes them out until it is.