# 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](what-the-graph-and-production-evidence-add.md)).

| Operation | Gives | Fails | SQL form |
|---|---|---|---|
| `random.token()` | `Text`, 32 random bytes as Base64url, 43 characters: for links and keys a person never types | | none |
| `random.code(length)` | `Text` of `length` characters from Crockford's Base32 (digits and capitals without `I`, `L`, `O`, `U`): booking and order references a person reads out; `length` 4 to 32 | | none |
| `random.integer(min, max)` | `Int`, uniformly from `min` to `max`, both included; `min` at most `max` | | none |
| `random.shuffle(items)` | `List<T>`, the items in random order | | none |
| `random.sample(items, count)` | `List<T>`, `count` items from different positions, in random order; all of them when `count` is larger | | none |

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:

```jadpo
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)
}
```

```jadpo
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](secret-values.md#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](debugging-and-review.md)). Since the
> recorded bytes can hold tokens, nothing writes them out until it is.