The randomness paradox.

The program

twoFloatsDistinct reads Random.float twice and compares the results. Its law supplies distinctStub, a deterministic oracle whose result depends on the per-branch call counter.

fn distinctStub(path: BranchPath, n: Int) -> Float
    ? "Stub returning n+1 as a Float — different value per call counter."
    Float.fromInt(n) + 1.0

fn twoFloatsDistinct() -> Bool
    ? "Sample two random floats; return whether they were different."
    ! [Random.float]
    a = Random.float()
    b = Random.float()
    a != b

verify twoFloatsDistinct law alwaysDistinct
    given rnd: Random.float = [distinctStub]
    twoFloatsDistinct() holds

The final holds states that the Boolean result must be true. The given line provides the declared world used by ordinary verification; it is not itself a restriction on the universal oracle type.

Recorded results

These are the current outcomes for examples/formal/randomness_paradox.av. Backend success and proof-gate status are reported separately.

verify distinctStub         2/2
verify twoFloatsDistinct  1/1

Summary: 3/3 cases passed

verify distinctStub         2/2
verify twoFloatsDistinct  1/4
  1/1 declared, 0/3 hostile

Summary: 3/6 passed | 3 failed

build:      passed
sorries:    0
universal:  no

Dafny:      2 verified, 0 errors
omitted:    1 universal obligation
proof gate: failed

Declared verification

Ordinary aver verify executes the law with the stub named in given. The first call receives counter 0 and returns 1.0; the second receives counter 1 and returns 2.0. Their inequality is true, so the law contributes one passing case. Together with the two checks for distinctStub, the file reports 3/3.

Hostile profiles

aver verify --hostile retains the declared case and also runs the law with the three registered Random.float profiles: midrange, always_zero, and always_one. Each profile returns the same value for both calls, so all three hostile cases fail. The complete file therefore reports 3/6.

If distinct oracle results are an intended precondition, the law can state that precondition with when. Hostile mode then skips profiles outside the declared assumption. If the goal is only to record behavior under one concrete stub, the check should remain sample-shaped rather than claim universality.

Proof export

Oracle lifting turns the effect into an explicit proof parameter, addressed by BranchPath and a per-branch counter. A universal form of this law would need to establish that twoFloatsDistinct returns true for every admissible Random.float oracle. A constant oracle is an immediate counterexample.

Lean

The generated Lean project builds with zero sorries. The exporter keeps the available checked-domain evidence without crediting this law as universal, so the gate reports universal: no. A clean build confirms the emitted declarations; the universal field states whether every law in the export received a kernel-genuine universal theorem.

Dafny

Dafny reports 2 verified, 0 errors for the declarations that were emitted. The universal obligation for this law is omitted because the claim cannot be established. Aver counts that omission separately and the strict proof gate fails with 1 omitted. The backend error count covers the declarations that were emitted; the gate accounts for the omitted obligation.

Run the checks

git clone https://github.com/jasisz/aver
cd aver
cargo install --path .

aver verify examples/formal/randomness_paradox.av
aver verify --hostile examples/formal/randomness_paradox.av

aver proof examples/formal/randomness_paradox.av \
    --backend lean --verify-mode auto --check -o out/randomness-lean

aver proof examples/formal/randomness_paradox.av \
    --backend dafny --check -o out/randomness-dafny

Lean checking requires Elan and the pinned Lean toolchain. Dafny checking requires Dafny 4.x with Z3. The Oracle guide documents classified effects, hostile profiles, trace laws, and proof lifting.