~/jendhub

spec/crypto/random.bend

bend-collections-laws-crypto@1.0.0.0 · 101 lines · 14 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
4import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as C8
5import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
6import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as R
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
8import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
9import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
10import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as SC
11import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
12import bend-collections-laws-crypto@1.0.0.0/spec/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)
34def byte_of(+w: U32, +k: Nat) -> U32:
35  U32.and(U32.shrn(w, k), 255)
36
37# Go's binary.LittleEndian.PutUint64
38def 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
43def 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
51def 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
58def 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
67def 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
74def fst_bytes(-G: Data, r: List<&2, U32> & G) -> List<&2, U32>:
75  (bs, g) = r
76  bs
77
78def 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
85def 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
88def 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
91def 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
94def 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
97def 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
100def 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}