proofs/math/random/proof.bend

bend-collections-laws-math@1.0.0.0 · 33 lines · 5 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
4import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
5import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SRM
6import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/stream.bend as CS
7import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/seed.bend as SEED
8import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as LE
9import bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend as SH
10
11# Entry point: `bend proofs/math/random/proof.bend` checks the ChaCha8 source,
12# Lemire's counting theorem and the shuffle/perm permutation clauses of
13# spec/math/random.bend, under the clause's name, for every input (and every
14# source, relation and element type where the clause is a template). No holes,
15# no axioms. The other clauses are checked by
16# proofs/math/random/proof_draws.bend, proofs/math/random/proof_pcg.bend,
17# proofs/math/random/proof_float.bend, so each root only re-checks the lemma
18# files it needs.
19
20def ChaCha8.stream(+n: Nat, +k: B.Key) -> SRM.ChaCha8.stream(n, k):
21  CS.stream(n, k)
22
23def ChaCha8.seeded(+n: Nat, +seed: List<&2, U32>) -> SRM.ChaCha8.seeded(n, seed):
24  SEED.seeded(n, seed)
25
26def Lemire.unbiased(+w: Nat, +n: Nat, +k: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hw: {C.fits(w, n) == True{} : Bool}, +hk: {Nat.is_lt(k, n) == True{} : Bool}) -> SRM.Lemire.unbiased(w, n, k, hn, hw, hk):
27  LE.unbiased(w, n, k, hn, hw, hk)
28
29def Shuffle.permutation(~A: Data, ~V: Data, ~rel: A -> V -> Bool, ~S: Data, ~next: S -> W.U64 & S, +s: S, +xs: List<&2, A>, +v: V) -> SRM.Shuffle.permutation(~A, ~V, ~rel, ~S, ~next, s, xs, v):
30  SH.shuffle_perm(~A, ~V, ~rel, ~S, ~next, s, xs, v)
31
32def Perm.permutation(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +i: Nat) -> SRM.Perm.permutation(~S, ~next, s, n, i):
33  SH.perm_perm(~S, ~next, s, n, i)