~/jendhub

spec/math/random.bend

bend-collections-laws-crypto@1.0.0.0 · 150 lines · 23 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
4import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F
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/math/random/chacha8.bend as C8
8import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
9import bend-collections-laws-crypto@1.0.0.0/src/math/random/pcg.bend as P
10import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
11import bend-collections-laws-crypto@1.0.0.0/spec/math/f64.bend as SF
12import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
13import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as SC
14import bend-collections-laws-crypto@1.0.0.0/spec/math/random/pcg.bend as SP
15import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
16
17# The contract of src/math/random.bend (Go's math/rand/v2): one
18# <Function>.<clause> proposition per guarantee, each proved for every
19# input under its name in proofs/math/random/proof.bend, proof_draws.bend,
20# proof_pcg.bend or proof_float.bend. The executable
21# specifications are spec/math/random/{chacha8rand,pcg,rand,source}.bend;
22# docs/MATH_CONTRACTS.md has the table.
23#
24#   ChaCha8 (C2SP chacha8rand)
25#     ChaCha8.stream        the outputs of the generator keyed by k are
26#                           C2SP's stream keyed by k's eight words
27#     ChaCha8.seeded        new(seed) is None unless the seed is 32 bytes
28#                           below 256, and otherwise outputs the stream keyed
29#                           by the seed's little-endian words
30#   PCG (Go's PCG-DXSM)
31#     PCG.step              one step is s * mul + inc mod 2^128, for every
32#                           multiplier and increment
33#     PCG.output            the output is DXSM of the new state, for every
34#                           DXSM multiplier: dxsm3 of the first half's
35#                           value dxsm1
36#     PCG.constants         next uses Go's constants
37#   Bounded integers (Lemire, as Go's uint64n)
38#     Uint64n.value         uint64n(n) is the first accepted draw of the
39#                           specification's draw among at most 128 draws
40#     Uint64n.lt            uint64n(n) < n for n > 0, for every source
41#     Lemire.unbiased       for every width w, bound 0 < n < 2^w and k < n,
42#                           exactly floor(2^w / n) of the 2^w source outputs
43#                           draw k: a uniform source gives a uniform result
44#   Permutations (Fisher-Yates, as Go's Shuffle and Perm)
45#     Shuffle.permutation   shuffle(xs) has as many elements related to v as
46#                           xs, for every relation and v (with an equality:
47#                           the same multiset)
48#     Perm.permutation      perm(n) holds every i < n exactly once and
49#                           nothing else
50#   Words and bounded wrappers
51#     Uint32.value, Int64.value, Int32.value   the top 32, low 63 and top
52#                           31 bits of the source output (Go's Uint32, Int64,
53#                           Int32)
54#     Uint32n.lt            uint32n(n) < n for n > 0
55#     Intn.lt               intn(n) < n for 0 < n < 2^64 (a run-time Nat is
56#                           below 2^48)
57#     IntRange.bounds       lo <= int_range(lo, hi) < hi for lo < hi
58#   Floats
59#     Float64.value         float64 is the double m * 2^-53, m the low 53
60#                           bits of the source output (exact, as Go)
61#     Float64.lt_one        float64 < 1.0
62
63def map_outputs(+n: Nat, m: Maybe<&2, C8.ChaCha8>) -> Maybe<&2, List<&2, W.U64>>:
64  match m:
65    case None{}:
66      None{}
67    case Some{g}:
68      Some{SRC.outputs(~C8.ChaCha8, ~C8.next, n, g)}
69
70def map_stream(+n: Nat, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, W.U64>>:
71  match m:
72    case None{}:
73      None{}
74    case Some{kl}:
75      Some{SC.stream(n, kl)}
76
77def ChaCha8.stream(+n: Nat, +k: B.Key) -> Type:
78  {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)) == SC.stream(n, SC.key_list(k)) : List<&2, W.U64>}
79
80def ChaCha8.seeded(+n: Nat, +seed: List<&2, U32>) -> Type:
81  {map_outputs(n, C8.new(seed)) == map_stream(n, SC.key_of_seed(seed)) : Maybe<&2, List<&2, W.U64>>}
82
83def value128(p: P.PCG) -> Nat:
84  match p:
85    case P.P{hi, lo}:
86      Nat.add(SW.value(lo), C.shift(64n, SW.value(hi)))
87
88def PCG.step(+mh: W.U64, +ml: W.U64, +ih: W.U64, +il: W.U64, +p: P.PCG) -> Type:
89  {value128(P.step_with(mh, ml, ih, il, p)) == SP.lcg(value128(P.P{mh, ml}), value128(P.P{ih, il}), value128(p)) : Nat}
90
91# stated through the intermediate value t of the first half (so the
92# checker never compares two copies of the nested 64-bit recursion);
93# t = dxsm1(cm, hi) gives output == dxsm(cm, hi, lo)
94def PCG.output(+cm: W.U64, +hi: W.U64, +lo: W.U64, +t: Nat, +ht: {t == SP.dxsm1(SW.value(cm), SW.value(hi)) : Nat}) -> Type:
95  {SW.value(P.dxsm_with(cm, hi, lo)) == SP.dxsm3(t, SW.value(lo)) : Nat}
96
97def PCG.constants(+p: P.PCG) -> Type:
98  {P.next(p) == P.out(P.step_with(P.mul_hi(), P.mul_lo(), P.inc_hi(), P.inc_lo(), p)) : W.U64 & P.PCG}
99
100def val_pair(-S: Data, r: W.U64 & S) -> Nat & S:
101  (x, s) = r
102  (SW.value(x), s)
103
104def Uint64n.value(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: W.U64) -> Type:
105  {val_pair(S, R.uint64n(~S, ~next, s, n)) == SR.below(~S, ~next, 127n, SW.value(n), s) : Nat & S}
106
107def Uint64n.lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: W.U64, +hn: {X.is_zero(n) == False{} : Bool}) -> Type:
108  {Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, n))), SW.value(n)) == True{} : Bool}
109
110def 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}) -> Type:
111  {SR.count(w, n, k, C.shift(w, 1n)) == Nat.div(C.shift(w, 1n), n) : Nat}
112
113def 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) -> Type:
114  {SR.occurrences(~A, ~V, ~rel, v, R.fst(List<&2, A>, S, R.shuffle(~A, ~S, ~next, s, xs))) == SR.occurrences(~A, ~V, ~rel, v, xs) : Nat}
115
116def Perm.permutation(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +i: Nat) -> Type:
117  {SR.occurrences(~Nat, ~Nat, ~Nat.is_eq, i, R.fst(List<&2, Nat>, S, R.perm(~S, ~next, s, n))) == SR.b2n(Nat.is_lt(i, n)) : Nat}
118
119# the exact double m * 2^-53 for m = the low 53 bits of x (m and the
120# exponent zb - 53 given as variables n, xv with their equations, so the
121# checker never compares two expansions of the rounding)
122def Float64.value(+x: W.U64, +n: Nat, +hn: {C.low(53n, SW.value(x)) == n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}) -> Type:
123  {R.to_float(x) == SF.round(False{}, n, xv) : F.F64}
124
125def Float64.lt_one(+x: W.U64) -> Type:
126  {F.lt(R.to_float(x), F.one()) == True{} : Bool}
127
128# ---- the word slices and the bounded wrappers (Go's Uint32, Int64, Int32,
129# Uint32N, IntN and lo + IntN(hi - lo)) ----
130
131def x0(~S: Data, ~next: S -> W.U64 & S, +s: S) -> Nat:
132  SW.value(SRC.fst64(S, next(s)))
133
134def Uint32.value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> Type:
135  {U32.to_nat(R.fst(U32, S, R.uint32(~S, ~next, s))) == C.high(32n, x0(~S, ~next, s)) : Nat}
136
137def Int64.value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> Type:
138  {SW.value(R.fst(W.U64, S, R.int64(~S, ~next, s))) == C.low(63n, x0(~S, ~next, s)) : Nat}
139
140def Int32.value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> Type:
141  {U32.to_nat(R.fst(U32, S, R.int32(~S, ~next, s))) == C.high(33n, x0(~S, ~next, s)) : Nat}
142
143def Uint32n.lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: U32, +hn: {U32.is_zero(n) == False{} : Bool}) -> Type:
144  {Nat.is_lt(U32.to_nat(R.fst(U32, S, R.uint32n(~S, ~next, s, n))), U32.to_nat(n)) == True{} : Bool}
145
146def Intn.lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hw: {C.fits(64n, n) == True{} : Bool}) -> Type:
147  {Nat.is_lt(R.fst(Nat, S, R.intn(~S, ~next, s, n)), n) == True{} : Bool}
148
149def IntRange.bounds(~S: Data, ~next: S -> W.U64 & S, +s: S, +lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}, +hw: {C.fits(64n, Nat.sub(hi, lo)) == True{} : Bool}) -> Type:
150  {Bool.and(Nat.is_le(lo, R.fst(Nat, S, R.int_range(~S, ~next, s, lo, hi))), Nat.is_lt(R.fst(Nat, S, R.int_range(~S, ~next, s, lo, hi)), hi)) == True{} : Bool}