1	import Base
2	import ../../src/math/u64.bend as W
3	import ../../src/math/w64.bend as X
4	import ../../src/math/random/chacha8.bend as C8
5	import ../../src/math/random/chacha8/block.bend as B
6	import ../../src/math/random/rand.bend as R
7	import ../../src/crypto/random.bend as CR
8	import ../math/w64.bend as SW
9	import ../math/random/source.bend as SRC
10	import ../math/random/chacha8rand.bend as SC
11	import ../math/random/rand.bend as SR
12	import ../math/random.bend as SRM
13	
14	# The contract of src/crypto/random.bend: the ChaCha8Rand generator of
15	# math/random (C2SP chacha8rand) with Go's ChaCha8.Read byte order, each
16	# clause proved for every input in proofs/crypto/random/proof.bend.
17	#
18	#   Random.stream       the 64-bit outputs of the generator keyed by eight
19	#                       words are C2SP's stream keyed by them
20	#   Random.seeded       new(seed) is None unless the seed is 32 bytes below
21	#                       256, and otherwise outputs the stream of its words
22	#   Random.bytes        bytes(g, n) are the first n of: the pending bytes,
23	#                       then the little-endian bytes of the next outputs
24	#                       (Go's binary.LittleEndian.PutUint64, as ChaCha8.Read)
25	#   Random.bytes_lt     every byte is below 256 (when the pending ones are)
26	#   Random.uint_below   uint_below(g, n) < n for n > 0
27	#   Random.shuffle      shuffle(g, items) is a permutation of items
28	#
29	# Security properties (indistinguishability from uniform, forward secrecy)
30	# are properties of ChaCha8 and of the C2SP key erasure, not of this code;
31	# see the module header and docs/CRYPTO_CONTRACTS.md.
32	
33	# Go's byte(v >> k)
34	def byte_of(+w: U32, +k: Nat) -> U32:
35	  U32.and(U32.shrn(w, k), 255)
36	
37	# Go's binary.LittleEndian.PutUint64
38	def le_bytes(x: W.U64) -> List<&2, U32>:
39	  match x:
40	    case W.U64{+l, +h}:
41	      [byte_of(l, 0n), byte_of(l, 8n), byte_of(l, 16n), byte_of(l, 24n), byte_of(h, 0n), byte_of(h, 8n), byte_of(h, 16n), byte_of(h, 24n)]
42	
43	def append(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
44	  match xs:
45	    case Nil{}:
46	      ys
47	    case Con{x, rest}:
48	      Con{x, append(rest, ys)}
49	
50	# the bytes of consecutive outputs
51	def flat(xs: List<&2, W.U64>) -> List<&2, U32>:
52	  match xs:
53	    case Nil{}:
54	      []
55	    case Con{x, rest}:
56	      append(le_bytes(x), flat(rest))
57	
58	def take(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
59	  match n xs:
60	    case 0n _:
61	      []
62	    case 1n+p Nil{}:
63	      []
64	    case 1n+p Con{x, rest}:
65	      Con{x, take(p, rest)}
66	
67	def below256(xs: List<&2, U32>) -> Bool:
68	  match xs:
69	    case Nil{}:
70	      True{}
71	    case Con{+x, rest}:
72	      Bool.and(U32.is_lt(x, 256), below256(rest))
73	
74	def fst_bytes(-G: Data, r: List<&2, U32> & G) -> List<&2, U32>:
75	  (bs, g) = r
76	  bs
77	
78	def map_outputs(+n: Nat, m: Maybe<&2, CR.Gen>) -> Maybe<&2, List<&2, W.U64>>:
79	  match m:
80	    case None{}:
81	      None{}
82	    case Some{g}:
83	      Some{SRC.outputs(~CR.Gen, ~CR.next, n, g)}
84	
85	def Random.stream(+n: Nat, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32) -> Type:
86	  {SRC.outputs(~CR.Gen, ~CR.next, n, CR.of_words(k0, k1, k2, k3, k4, k5, k6, k7)) == SC.stream(n, [k0, k1, k2, k3, k4, k5, k6, k7]) : List<&2, W.U64>}
87	
88	def Random.seeded(+n: Nat, +seed: List<&2, U32>) -> Type:
89	  {map_outputs(n, CR.new(seed)) == SRM.map_stream(n, SC.key_of_seed(seed)) : Maybe<&2, List<&2, W.U64>>}
90	
91	def Random.bytes(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> Type:
92	  {fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n)) == take(n, append(p, flat(SRC.outputs(~C8.ChaCha8, ~C8.next, n, c)))) : List<&2, U32>}
93	
94	def Random.bytes_lt(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>, +hp: {below256(p) == True{} : Bool}) -> Type:
95	  {below256(fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n))) == True{} : Bool}
96	
97	def Random.uint_below(+g: CR.Gen, +n: W.U64, +hn: {X.is_zero(n) == False{} : Bool}) -> Type:
98	  {Nat.is_lt(SW.value(R.fst(W.U64, CR.Gen, CR.uint_below(g, n))), SW.value(n)) == True{} : Bool}
99	
100	def Random.shuffle(~A: Data, ~V: Data, ~rel: A -> V -> Bool, +g: CR.Gen, +items: List<&2, A>, +v: V) -> Type:
101	  {SR.occurrences(~A, ~V, ~rel, v, R.fst(List<&2, A>, CR.Gen, CR.shuffle(~A, g, items))) == SR.occurrences(~A, ~V, ~rel, v, items) : Nat}