1	import Base
2	import ../math/u64.bend as W
3	import ../math/w64.bend as X
4	import ../math/random/rand.bend as R
5	import ../math/random/chacha8.bend as C8
6	import ../math/random/chacha8/block.bend as B
7	
8	# A cryptographically secure random generator: ChaCha8Rand (C2SP
9	# chacha8rand), the generator behind Go's runtime and math/rand/v2 top-level
10	# functions and its ChaCha8 source, with Go's ChaCha8.Read byte order.
11	#
12	#   new(seed)           Some{g} for a 32-byte seed (32 bytes < 256), None
13	#                       otherwise: deterministic, for tests and reproducible
14	#                       runs; the seed must be secret and uniformly random
15	#   from_os()           IO: a generator keyed with 32 bytes of operating-system
16	#                       entropy (eight IO.random_u32 calls: getrandom /
17	#                       arc4random / crypto.getRandomValues)
18	#   bytes(g, n)         n random bytes (a list of U32 < 256) and the new
19	#                       generator; Go's (*ChaCha8).Read: the little-endian
20	#                       bytes of successive 64-bit outputs, a partly used
21	#                       output's remaining bytes served first by the next call
22	#   uint64(g)           a uniform 64-bit word
23	#   uint_below(g, n)    uniform in [0, n) for n > 0 (Lemire, unbiased)
24	#   shuffle(g, items)   a uniform permutation of items (Fisher-Yates)
25	#   next(g)             the Source step, for every function of
26	#                       src/math/random/rand.bend: R.float64(~Gen, ~next, g)
27	#
28	# Security (the C2SP chacha8rand design; Aumasson, "Too Much Crypto", for
29	# eight rounds): the output is ChaCha8 keyed by the seed, a PRF, so it is
30	# indistinguishable from uniform to anyone who does not know the seed.
31	# Every 992 bytes of output the key is replaced by 32 bytes of the stream
32	# (fast key erasure), so once a key is overwritten the outputs before it
33	# cannot be recomputed from the generator's state: forward secrecy with a
34	# window of at most one iteration (the unread words of the current
35	# iteration and the key it started from are in the state). Callers must:
36	#
37	#   - keep the seed and every generator value secret (a copied generator
38	#     repeats its outputs: Bend values are immutable, so reusing an old g
39	#     replays the same bytes; always continue from the returned generator);
40	#   - seed from_os() for secrets; new(seed) only with a secret uniform seed;
41	#   - not rely on constant-time behaviour: Bend has no timing model, and
42	#     uint_below's rejection loop takes a data-dependent number of draws (as
43	#     in Go), which reveals nothing about the accepted value.
44	#
45	# The stream is proved to be C2SP's for every seed, uint_below < n, the
46	# rejection exactly unbiased and shuffle a permutation
47	# (proofs/crypto/random/); tested against Go's vectors (tools/check_random.py).
48	
49	type Gen is Data:
50	  G{src: C8.ChaCha8, pending: List<&2, U32>}
51	
52	def wrap(m: Maybe<&2, C8.ChaCha8>) -> Maybe<&2, Gen>:
53	  match m:
54	    case None{}:
55	      None{}
56	    case Some{c}:
57	      Some{G{c, []}}
58	
59	def new(+seed: List<&2, U32>) -> Maybe<&2, Gen>:
60	  wrap(C8.new(seed))
61	
62	def of_words(+k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32) -> Gen:
63	  G{C8.of_key(B.K{k0, k1, k2, k3, k4, k5, k6, k7}), []}
64	
65	def os_word() -> IO(U32):
66	  IO.try(U32, IO.random_u32())
67	
68	def from_os() -> IO(Gen):
69	  do IO<Gen>:
70	    k0 : U32 <- os_word()
71	    k1 : U32 <- os_word()
72	    k2 : U32 <- os_word()
73	    k3 : U32 <- os_word()
74	    k4 : U32 <- os_word()
75	    k5 : U32 <- os_word()
76	    k6 : U32 <- os_word()
77	    k7 : U32 <- os_word()
78	    return of_words(k0, k1, k2, k3, k4, k5, k6, k7)
79	
80	def keep_pending(+p: List<&2, U32>, r: W.U64 & C8.ChaCha8) -> W.U64 & Gen:
81	  (x, c) = r
82	  (x, G{c, p})
83	
84	# the Source step: the next 64-bit output (pending bytes are left for bytes)
85	def next(g: Gen) -> W.U64 & Gen:
86	  match g:
87	    case G{c, +p}:
88	      keep_pending(p, C8.next(c))
89	
90	# the eight little-endian bytes of a 64-bit word
91	def le_bytes(+x: W.U64) -> List<&2, U32>:
92	  +l = X.lo(x)
93	  +h = X.hi(x)
94	  [U32.and(l, 255), U32.and(U32.shrn(l, 8n), 255), U32.and(U32.shrn(l, 16n), 255), U32.and(U32.shrn(l, 24n), 255), U32.and(h, 255), U32.and(U32.shrn(h, 8n), 255), U32.and(U32.shrn(h, 16n), 255), U32.and(U32.shrn(h, 24n), 255)]
95	
96	# the bytes read so far (latest first), the generator and its pending bytes
97	type Fill is Data:
98	  FS{acc: List<&2, U32>, src: C8.ChaCha8, pending: List<&2, U32>}
99	
100	def split_bytes(acc: List<&2, U32>, c: C8.ChaCha8, bs: List<&2, U32>) -> Fill:
101	  match bs:
102	    case Con{b, rest}:
103	      FS{Con{b, acc}, c, rest}
104	    case Nil{}:
105	      FS{acc, c, []}
106	
107	def split(acc: List<&2, U32>, r: W.U64 & C8.ChaCha8) -> Fill:
108	  (+x, c) = r
109	  split_bytes(acc, c, le_bytes(x))
110	
111	# one byte: the next pending byte, or the first byte of a fresh word
112	def take1(f: Fill) -> Fill:
113	  match f:
114	    case FS{acc, c, p}:
115	      match p:
116	        case Con{b, rest}:
117	          FS{Con{b, acc}, c, rest}
118	        case Nil{}:
119	          split(acc, C8.next(c))
120	
121	def fill(n: Nat, f: Fill) -> Fill:
122	  match n:
123	    case 0n:
124	      f
125	    case 1n+k:
126	      fill(k, take1(f))
127	
128	def done(f: Fill) -> List<&2, U32> & Gen:
129	  match f:
130	    case FS{acc, c, p}:
131	      (List.reverse(&2, U32, acc), G{c, p})
132	
133	def bytes(g: Gen, n: Nat) -> List<&2, U32> & Gen:
134	  match g:
135	    case G{c, p}:
136	      done(fill(n, FS{[], c, p}))
137	
138	def uint64(g: Gen) -> W.U64 & Gen:
139	  next(g)
140	
141	# uniform in [0, n) for n > 0
142	def uint_below(g: Gen, +n: W.U64) -> W.U64 & Gen:
143	  R.uint64n(~Gen, ~next, g, n)
144	
145	# a uniform permutation of items
146	def shuffle(~A: Data, g: Gen, +items: List<&2, A>) -> List<&2, A> & Gen:
147	  R.shuffle(~A, ~Gen, ~next, g, items)