1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../src/math/u64.bend as W
4	import ../../../src/math/random/chacha8/block.bend as B
5	import ../../../spec/math/random.bend as SRM
6	import ./chacha8/stream.bend as CS
7	import ./chacha8/seed.bend as SEED
8	import ./lemire.bend as LE
9	import ./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	
20	def ChaCha8.stream(+n: Nat, +k: B.Key) -> SRM.ChaCha8.stream(n, k):
21	  CS.stream(n, k)
22	
23	def ChaCha8.seeded(+n: Nat, +seed: List<&2, U32>) -> SRM.ChaCha8.seeded(n, seed):
24	  SEED.seeded(n, seed)
25	
26	def 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	
29	def 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	
32	def 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)