1 import Base 2 import ../../../src/math/u64.bend as W 3 import ../../../src/math/random/chacha8.bend as C8 4 import ../../../src/crypto/random.bend as CR 5 import ../../../spec/math/random/source.bend as SRC 6 import ../../../spec/crypto/random.bend as SCR 7 import ../../lib/nat.bend as N 8 import ../../lib/logic.bend as L 9 import ../../lib/u32.bend as U 10 import ../../../spec/math/random/rand.bend as SR 11 import ../../math/random/bits.bend as BI 12 import ../../math/random/below.bend as BL 13 14 # bytes(g, n) (Go's ChaCha8.Read) returns the pending bytes, then the 15 # little-endian bytes of the next outputs: its accumulator, read back, is 16 # always the prefix of that byte stream. 17 18 def rev(xs: List<&2, U32>) -> List<&2, U32>: 19 List.reverse(&2, U32, xs) 20 21 def app_nil(+xs: List<&2, U32>) -> {SCR.append(xs, []) == xs : List<&2, U32>}: 22 match xs: 23 case Nil{}: 24 {==} 25 case Con{+x, +rest}: 26 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{x, l}, SCR.append(rest, []), rest, app_nil(rest)) 27 28 def app_assoc(+xs: List<&2, U32>, +ys: List<&2, U32>, +zs: List<&2, U32>) -> {SCR.append(SCR.append(xs, ys), zs) == SCR.append(xs, SCR.append(ys, zs)) : List<&2, U32>}: 29 match xs: 30 case Nil{}: 31 {==} 32 case Con{+x, +rest}: 33 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{x, l}, SCR.append(SCR.append(rest, ys), zs), SCR.append(rest, SCR.append(ys, zs)), app_assoc(rest, ys, zs)) 34 35 # reverse.go(xs, ys) = reverse(xs) ++ ys 36 def rgo(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.reverse.go(&2, U32, xs, ys) == SCR.append(rev(xs), ys) : List<&2, U32>}: 37 match xs: 38 case Nil{}: 39 {==} 40 case Con{+h, +t}: 41 Equal.trans(List<&2, U32>, List.reverse.go(&2, U32, t, Con{h, ys}), SCR.append(rev(t), Con{h, ys}), SCR.append(List.reverse.go(&2, U32, t, [h]), ys), 42 rgo(t, Con{h, ys}), 43 Equal.trans(List<&2, U32>, SCR.append(rev(t), Con{h, ys}), SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(List.reverse.go(&2, U32, t, [h]), ys), 44 Equal.sym(List<&2, U32>, SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(rev(t), SCR.append([h], ys)), app_assoc(rev(t), [h], ys)), 45 Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ys), SCR.append(rev(t), [h]), List.reverse.go(&2, U32, t, [h]), Equal.sym(List<&2, U32>, List.reverse.go(&2, U32, t, [h]), SCR.append(rev(t), [h]), rgo(t, [h]))))) 46 47 # rev(b :: acc) ++ ts = rev(acc) ++ (b :: ts) 48 def rev_cons(+b: U32, +acc: List<&2, U32>, +ts: List<&2, U32>) -> {SCR.append(rev(Con{b, acc}), ts) == SCR.append(rev(acc), Con{b, ts}) : List<&2, U32>}: 49 Equal.trans(List<&2, U32>, SCR.append(List.reverse.go(&2, U32, acc, [b]), ts), SCR.append(SCR.append(rev(acc), [b]), ts), SCR.append(rev(acc), Con{b, ts}), 50 Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ts), List.reverse.go(&2, U32, acc, [b]), SCR.append(rev(acc), [b]), rgo(acc, [b])), 51 app_assoc(rev(acc), [b], ts)) 52 53 # the eight bytes of a word, split at the first 54 def b0(x: W.U64) -> U32: 55 match x: 56 case W.U64{+l, +h}: 57 SCR.byte_of(l, 0n) 58 59 def b7(x: W.U64) -> List<&2, U32>: 60 match x: 61 case W.U64{+l, +h}: 62 [SCR.byte_of(l, 8n), SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)] 63 64 def le_split(+x: W.U64) -> {SCR.le_bytes(x) == Con{b0(x), b7(x)} : List<&2, U32>}: 65 match x: 66 case W.U64{+l, +h}: 67 {==} 68 69 def outs(+k: Nat, +c: C8.ChaCha8) -> List<&2, W.U64>: 70 SRC.outputs(~C8.ChaCha8, ~C8.next, k, c) 71 72 # taking j bytes never looks past the first j outputs 73 def prefix(+j: Nat, +r: List<&2, U32>, +c: C8.ChaCha8, +d: Nat) -> {SCR.take(j, SCR.append(r, SCR.flat(outs(Nat.add(j, d), c)))) == SCR.take(j, SCR.append(r, SCR.flat(outs(j, c)))) : List<&2, U32>}: 74 match j r: 75 case 0n _: 76 {==} 77 case 1n+i Con{+b, +rest}: 78 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{b, l}, SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+Nat.add(i, d), c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+i, c)))), 79 Equal.trans(List<&2, U32>, SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+Nat.add(i, d), c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+i, c)))), 80 %N.add_succ(i, d) : {SCR.take(i, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))) : List<&2, U32>} 81 prefix(i, rest, c, 1n+d), 82 Equal.sym(List<&2, U32>, SCR.take(i, SCR.append(rest, SCR.flat(outs(1n+i, c)))), SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))), 83 %Equal.trans(Nat, Nat.add(i, 1n), 1n+Nat.add(i, 0n), 1n+i, N.add_succ(i, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(i, 0n), i, N.add_zero(i))) : {SCR.take(i, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(i, SCR.append(rest, SCR.flat(outs(i, c)))) : List<&2, U32>} 84 prefix(i, rest, c, 1n)))) 85 case 1n+i Nil{}: 86 +x = SRC.fst64(C8.ChaCha8, C8.next(c)) 87 +c1 = SRC.snd64(C8.ChaCha8, C8.next(c)) 88 %Equal.sym(List<&2, U32>, SCR.le_bytes(x), Con{b0(x), b7(x)}, le_split(x)) : {SCR.take(1n+i, SCR.append(_, SCR.flat(outs(Nat.add(i, d), c1)))) == SCR.take(1n+i, SCR.append(_, SCR.flat(outs(i, c1)))) : List<&2, U32>} 89 Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{b0(x), l}, SCR.take(i, SCR.append(b7(x), SCR.flat(outs(Nat.add(i, d), c1)))), SCR.take(i, SCR.append(b7(x), SCR.flat(outs(i, c1)))), prefix(i, b7(x), c1, d)) 90 91 # ---- the fill loop ---- 92 93 def facc(f: CR.Fill) -> List<&2, U32>: 94 match f: 95 case CR.FS{a, c, p}: 96 a 97 98 def fsrc(f: CR.Fill) -> C8.ChaCha8: 99 match f: 100 case CR.FS{a, c, p}: 101 c 102 103 def fpend(f: CR.Fill) -> List<&2, U32>: 104 match f: 105 case CR.FS{a, c, p}: 106 p 107 108 def step_nil(+j: Nat, +acc: List<&2, U32>, q: W.U64 & C8.ChaCha8) -> {SCR.append(rev(facc(CR.split(acc, q))), SCR.take(j, SCR.append(fpend(CR.split(acc, q)), SCR.flat(outs(j, fsrc(CR.split(acc, q))))))) == SCR.append(rev(acc), SCR.take(1n+j, SCR.flat(Con{SRC.fst64(C8.ChaCha8, q), outs(j, SRC.snd64(C8.ChaCha8, q))}))) : List<&2, U32>}: 109 match q: 110 case Tuple{x, +c1}: 111 match x: 112 case W.U64{+l, +h}: 113 +r7 = {[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)] : List<&2, U32>} 114 rev_cons(U32.and(l, 255), acc, SCR.take(j, SCR.append(r7, SCR.flat(outs(j, c1))))) 115 116 # one byte of the loop against the byte stream 117 def step(+j: Nat, +f: CR.Fill) -> {SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))) == SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))) : List<&2, U32>}: 118 match f: 119 case CR.FS{+acc, +c, +p}: 120 match p: 121 case Con{+b, +rest}: 122 Equal.trans(List<&2, U32>, SCR.append(rev(Con{b, acc}), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))), SCR.append(rev(acc), Con{b, SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))}), SCR.append(rev(acc), Con{b, SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c))))}), 123 rev_cons(b, acc, SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))), 124 Equal.cong(List<&2, U32>, List<&2, U32>, z => SCR.append(rev(acc), Con{b, z}), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))), SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c)))), 125 Equal.sym(List<&2, U32>, SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c)))), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))), 126 %Equal.trans(Nat, Nat.add(j, 1n), 1n+Nat.add(j, 0n), 1n+j, N.add_succ(j, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, 0n), j, N.add_zero(j))) : {SCR.take(j, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))) : List<&2, U32>} 127 prefix(j, rest, c, 1n)))) 128 case Nil{}: 129 step_nil(j, acc, C8.next(c)) 130 131 # THEOREM: after k bytes the accumulator, read back, is the old one followed 132 # by the first k bytes of the pending bytes and the stream 133 def fill_inv(+k: Nat, +f: CR.Fill) -> {rev(facc(CR.fill(k, f))) == SCR.append(rev(facc(f)), SCR.take(k, SCR.append(fpend(f), SCR.flat(outs(k, fsrc(f)))))) : List<&2, U32>}: 134 match k: 135 case 0n: 136 Equal.sym(List<&2, U32>, SCR.append(rev(facc(f)), []), rev(facc(f)), app_nil(rev(facc(f)))) 137 case 1n+j: 138 Equal.trans(List<&2, U32>, rev(facc(CR.fill(j, CR.take1(f)))), SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))), SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))), 139 fill_inv(j, CR.take1(f)), 140 step(j, f)) 141 142 def done_bytes(+f: CR.Fill) -> {SCR.fst_bytes(CR.Gen, CR.done(f)) == rev(facc(f)) : List<&2, U32>}: 143 match f: 144 case CR.FS{a, c, p}: 145 {==} 146 147 # THEOREM (Random.bytes) 148 def bytes(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>) -> SCR.Random.bytes(n, c, p): 149 Equal.trans(List<&2, U32>, SCR.fst_bytes(CR.Gen, CR.done(CR.fill(n, CR.FS{[], c, p}))), rev(facc(CR.fill(n, CR.FS{[], c, p}))), SCR.take(n, SCR.append(p, SCR.flat(outs(n, c)))), 150 done_bytes(CR.fill(n, CR.FS{[], c, p})), 151 fill_inv(n, CR.FS{[], c, p})) 152 153 # ---- every byte is below 256 ---- 154 155 def and_true_r(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}: 156 match b: 157 case True{}: 158 {==} 159 case False{}: 160 {==} 161 162 def below_take(+n: Nat, +xs: List<&2, U32>, +h: {SCR.below256(xs) == True{} : Bool}) -> {SCR.below256(SCR.take(n, xs)) == True{} : Bool}: 163 match n xs: 164 case 0n _: 165 {==} 166 case 1n+p Nil{}: 167 {==} 168 case 1n+p Con{+x, +rest}: 169 %Equal.sym(Bool, U32.is_lt(x, 256), True{}, L.and_left(U32.is_lt(x, 256), SCR.below256(rest), h)) : {Bool.and(_, SCR.below256(SCR.take(p, rest))) == True{} : Bool} 170 below_take(p, rest, L.and_right(U32.is_lt(x, 256), SCR.below256(rest), h)) 171 172 def below_app(+xs: List<&2, U32>, +ys: List<&2, U32>, +hx: {SCR.below256(xs) == True{} : Bool}, +hy: {SCR.below256(ys) == True{} : Bool}) -> {SCR.below256(SCR.append(xs, ys)) == True{} : Bool}: 173 match xs: 174 case Nil{}: 175 hy 176 case Con{+x, +rest}: 177 %Equal.sym(Bool, U32.is_lt(x, 256), True{}, L.and_left(U32.is_lt(x, 256), SCR.below256(rest), hx)) : {Bool.and(_, SCR.below256(SCR.append(rest, ys))) == True{} : Bool} 178 below_app(rest, ys, L.and_right(U32.is_lt(x, 256), SCR.below256(rest), hx), hy) 179 180 # y & 255 < 256 181 def byte_lt(+y: U32) -> {U32.is_lt(U32.and(y, 255), 256) == True{} : Bool}: 182 Equal.trans(Bool, U32.is_lt(U32.and(y, 255), 256), Nat.is_lt(U32.to_nat(U32.and(y, 255)), 256n), True{}, 183 U.is_lt_nat(U32.and(y, 255), 256), 184 %Equal.sym(Nat, U32.to_nat(U32.and(y, 255)), SR.and_bits(32n, U32.to_nat(y), 255n), BI.uand(y, 255)) : {Nat.is_lt(_, 256n) == True{} : Bool} 185 N.le_lt_succ(SR.and_bits(32n, U32.to_nat(y), 255n), 255n, BL.and_le(32n, U32.to_nat(y), 255n))) 186 187 def byte_of_lt(+w: U32, +k: Nat) -> {U32.is_lt(SCR.byte_of(w, k), 256) == True{} : Bool}: 188 byte_lt(U32.shrn(w, k)) 189 190 def le_below(+x: W.U64) -> {SCR.below256(SCR.le_bytes(x)) == True{} : Bool}: 191 match x: 192 case W.U64{+l, +h}: 193 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 0n), 256), True{}, byte_of_lt(l, 0n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 8n), SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool} 194 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 8n), 256), True{}, byte_of_lt(l, 8n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool} 195 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 16n), 256), True{}, byte_of_lt(l, 16n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool} 196 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 24n), 256), True{}, byte_of_lt(l, 24n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool} 197 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 0n), 256), True{}, byte_of_lt(h, 0n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool} 198 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 8n), 256), True{}, byte_of_lt(h, 8n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool} 199 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 16n), 256), True{}, byte_of_lt(h, 16n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 24n)])) == True{} : Bool} 200 %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 24n), 256), True{}, byte_of_lt(h, 24n)) : {Bool.and(_, True{}) == True{} : Bool} 201 {==} 202 203 def flat_below(+os: List<&2, W.U64>) -> {SCR.below256(SCR.flat(os)) == True{} : Bool}: 204 match os: 205 case Nil{}: 206 {==} 207 case Con{+x, +rest}: 208 below_app(SCR.le_bytes(x), SCR.flat(rest), le_below(x), flat_below(rest)) 209 210 # THEOREM (Random.bytes_lt) 211 def bytes_lt(+n: Nat, +c: C8.ChaCha8, +p: List<&2, U32>, +hp: {SCR.below256(p) == True{} : Bool}) -> SCR.Random.bytes_lt(n, c, p, hp): 212 %Equal.sym(List<&2, U32>, SCR.fst_bytes(CR.Gen, CR.bytes(CR.G{c, p}, n)), SCR.take(n, SCR.append(p, SCR.flat(outs(n, c)))), bytes(n, c, p)) : {SCR.below256(_) == True{} : Bool} 213 below_take(n, SCR.append(p, SCR.flat(outs(n, c))), below_app(p, SCR.flat(outs(n, c)), hp, flat_below(outs(n, c))))