~/jendhub

proofs/math/random/bits.bend

bend-collections-laws-crypto@1.0.0.0 · 125 lines · 9 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/spec/math/w64.bend as SW
4import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
5import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as R
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
12
13# Bitwise and on words against SR.and_bits on their values: bit by bit on
14# U32 words, then a 64-bit word as two 32-bit limbs.
15
16def bv(b: Bool) -> Nat:
17  match b:
18    case True{}:
19      1n
20    case False{}:
21      0n
22
23# one bit and the rest: (b + 2a) & (c + 2d) = b c + 2 (a & d)
24def and_step(+p: Nat, +b: Nat, +a: Nat, +c: Nat, +d: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +hc: {Nat.is_le(c, 1n) == True{} : Bool}) -> {SR.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(b, c), Nat.double(SR.and_bits(p, a, d))) : Nat}:
25  match b c:
26    case 0n 0n:
27      %Equal.sym(Nat, C.bit(Nat.double(a)), 0n, WI.bit_dbl(0n, a)) : {Nat.add(Nat.mul(_, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, C.half(Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
28      %Equal.sym(Nat, C.half(Nat.double(a)), a, WI.half_dbl(0n, a)) : {Nat.add(Nat.mul(0n, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, _, C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
29      %Equal.sym(Nat, C.half(Nat.double(d)), d, WI.half_dbl(0n, d)) : {Nat.add(Nat.mul(0n, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
30      {==}
31    case 0n 1n:
32      %Equal.sym(Nat, C.bit(Nat.double(a)), 0n, WI.bit_dbl(0n, a)) : {Nat.add(Nat.mul(_, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, C.half(Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
33      %Equal.sym(Nat, C.half(Nat.double(a)), a, WI.half_dbl(0n, a)) : {Nat.add(Nat.mul(0n, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, _, C.half(1n+Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
34      %Equal.sym(Nat, C.half(1n+Nat.double(d)), d, WI.half_dbl(1n, d)) : {Nat.add(Nat.mul(0n, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
35      {==}
36    case 1n 0n:
37      %Equal.sym(Nat, C.bit(1n+Nat.double(a)), 1n, WI.bit_dbl(1n, a)) : {Nat.add(Nat.mul(_, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
38      %Equal.sym(Nat, C.bit(Nat.double(d)), 0n, WI.bit_dbl(0n, d)) : {Nat.add(Nat.mul(1n, _), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
39      %Equal.sym(Nat, C.half(1n+Nat.double(a)), a, WI.half_dbl(1n, a)) : {Nat.add(Nat.mul(1n, 0n), Nat.double(SR.and_bits(p, _, C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
40      %Equal.sym(Nat, C.half(Nat.double(d)), d, WI.half_dbl(0n, d)) : {Nat.add(Nat.mul(1n, 0n), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
41      {==}
42    case 1n 1n:
43      %Equal.sym(Nat, C.bit(1n+Nat.double(a)), 1n, WI.bit_dbl(1n, a)) : {Nat.add(Nat.mul(_, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
44      %Equal.sym(Nat, C.bit(1n+Nat.double(d)), 1n, WI.bit_dbl(1n, d)) : {Nat.add(Nat.mul(1n, _), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
45      %Equal.sym(Nat, C.half(1n+Nat.double(a)), a, WI.half_dbl(1n, a)) : {Nat.add(Nat.mul(1n, 1n), Nat.double(SR.and_bits(p, _, C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
46      %Equal.sym(Nat, C.half(1n+Nat.double(d)), d, WI.half_dbl(1n, d)) : {Nat.add(Nat.mul(1n, 1n), Nat.double(SR.and_bits(p, a, _))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
47      {==}
48    case 2n+q _:
49      Empty.absurd({SR.and_bits(1n+p, Nat.add(2n+q, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(2n+q, c), Nat.double(SR.and_bits(p, a, d))) : Nat}, L.false_true(hb))
50    case _ 2n+q:
51      Empty.absurd({SR.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(2n+q, Nat.double(d))) == Nat.add(Nat.mul(b, 2n+q), Nat.double(SR.and_bits(p, a, d))) : Nat}, L.false_true(hc))
52
53def bv_le(+b: Bool) -> {Nat.is_le(bv(b), 1n) == True{} : Bool}:
54  match b:
55    case True{}:
56      {==}
57    case False{}:
58      {==}
59
60def bv_and(+x: Bool, +y: Bool) -> {bv(Bool.and(x, y)) == Nat.mul(bv(x), bv(y)) : Nat}:
61  match x y:
62    case True{} True{}:
63      {==}
64    case True{} False{}:
65      {==}
66    case False{} _:
67      {==}
68
69# a word's value, its low bit first
70def to_nat_con(+p: Nat, +x: Bool, +t: Word(p)) -> {Word.to_nat(1n+p, WCon{x, t}) == Nat.add(bv(x), Nat.double(Word.to_nat(p, t))) : Nat}:
71  match x:
72    case True{}:
73      {==}
74    case False{}:
75      {==}
76
77# THEOREM: Word.and is and_bits on the values
78def wand(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.to_nat(n, Word.and(n, a, b)) == SR.and_bits(n, Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}:
79  match n a b:
80    case 0n WNil{} WNil{}:
81      {==}
82    case 1n+p WCon{+x, +t} WCon{+y, +u}:
83      +e1 = to_nat_con(p, Bool.and(x, y), Word.and(p, t, u))
84      +e2 = Equal.cong(Nat, Nat, z => Nat.add(bv(Bool.and(x, y)), Nat.double(z)), Word.to_nat(p, Word.and(p, t, u)), SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)), wand(p, t, u))
85      +e3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), bv(Bool.and(x, y)), Nat.mul(bv(x), bv(y)), bv_and(x, y))
86      +e4 = Equal.sym(Nat, SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), Nat.add(Nat.mul(bv(x), bv(y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), and_step(p, bv(x), Word.to_nat(p, t), bv(y), Word.to_nat(p, u), bv_le(x), bv_le(y)))
87      %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, t}), Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), to_nat_con(p, x, t)) : {Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}) == SR.and_bits(1n+p, _, Word.to_nat(1n+p, WCon{y, u})) : Nat}
88      %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, u}), Nat.add(bv(y), Nat.double(Word.to_nat(p, u))), to_nat_con(p, y, u)) : {Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}) == SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), _) : Nat}
89      Equal.trans(Nat, Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}), Nat.add(bv(Bool.and(x, y)), Nat.double(Word.to_nat(p, Word.and(p, t, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e1,
90        Equal.trans(Nat, Nat.add(bv(Bool.and(x, y)), Nat.double(Word.to_nat(p, Word.and(p, t, u)))), Nat.add(bv(Bool.and(x, y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e2,
91          Equal.trans(Nat, Nat.add(bv(Bool.and(x, y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), Nat.add(Nat.mul(bv(x), bv(y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e3, e4)))
92
93def uand(+x: U32, +y: U32) -> {U32.to_nat(U32.and(x, y)) == SR.and_bits(32n, U32.to_nat(x), U32.to_nat(y)) : Nat}:
94  match x y:
95    case U32{+a} U32{+b}:
96      wand(32n, a, b)
97
98# THEOREM: and on two limbs, (a1 + 2^k b1) & (a2 + 2^k b2) = a1 & a2 + 2^k (b1 & b2)
99def and_join(+k: Nat, +j: Nat, +a1: Nat, +b1: Nat, +a2: Nat, +b2: Nat, +h1: {C.fits(k, a1) == True{} : Bool}, +h2: {C.fits(k, a2) == True{} : Bool}) -> {SR.and_bits(Nat.add(k, j), Nat.add(a1, C.shift(k, b1)), Nat.add(a2, C.shift(k, b2))) == Nat.add(SR.and_bits(k, a1, a2), C.shift(k, SR.and_bits(j, b1, b2))) : Nat}:
100  match k:
101    case 0n:
102      %Equal.sym(Nat, a1, 0n, N.eq_from_is_eq(a1, 0n, h1)) : {SR.and_bits(j, Nat.add(_, b1), Nat.add(a2, b2)) == Nat.add(SR.and_bits(0n, _, a2), SR.and_bits(j, b1, b2)) : Nat}
103      %Equal.sym(Nat, a2, 0n, N.eq_from_is_eq(a2, 0n, h2)) : {SR.and_bits(j, b1, Nat.add(_, b2)) == Nat.add(SR.and_bits(0n, 0n, _), SR.and_bits(j, b1, b2)) : Nat}
104      {==}
105    case 1n+p:
106      +S1 = C.shift(p, b1)
107      +S2 = C.shift(p, b2)
108      +X = SR.and_bits(j, b1, b2)
109      +B = Nat.mul(C.bit(a1), C.bit(a2))
110      +Ih = and_join(p, j, C.half(a1), b1, C.half(a2), b2, h1, h2)
111      %Equal.sym(Nat, C.bit(Nat.add(a1, Nat.double(S1))), C.bit(a1), WI.bit_dbl(a1, S1)) : {Nat.add(Nat.mul(_, C.bit(Nat.add(a2, Nat.double(S2)))), Nat.double(SR.and_bits(Nat.add(p, j), C.half(Nat.add(a1, Nat.double(S1))), C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
112      %Equal.sym(Nat, C.bit(Nat.add(a2, Nat.double(S2))), C.bit(a2), WI.bit_dbl(a2, S2)) : {Nat.add(Nat.mul(C.bit(a1), _), Nat.double(SR.and_bits(Nat.add(p, j), C.half(Nat.add(a1, Nat.double(S1))), C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
113      %Equal.sym(Nat, C.half(Nat.add(a1, Nat.double(S1))), Nat.add(C.half(a1), S1), WI.half_dbl(a1, S1)) : {Nat.add(B, Nat.double(SR.and_bits(Nat.add(p, j), _, C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
114      %Equal.sym(Nat, C.half(Nat.add(a2, Nat.double(S2))), Nat.add(C.half(a2), S2), WI.half_dbl(a2, S2)) : {Nat.add(B, Nat.double(SR.and_bits(Nat.add(p, j), Nat.add(C.half(a1), S1), _))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
115      %Equal.sym(Nat, SR.and_bits(Nat.add(p, j), Nat.add(C.half(a1), S1), Nat.add(C.half(a2), S2)), Nat.add(SR.and_bits(p, C.half(a1), C.half(a2)), C.shift(p, X)), Ih) : {Nat.add(B, Nat.double(_)) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
116      %N.add_double(SR.and_bits(p, C.half(a1), C.half(a2)), C.shift(p, X)) : {Nat.add(B, _) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
117      Equal.sym(Nat, Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))), Nat.add(B, Nat.add(Nat.double(SR.and_bits(p, C.half(a1), C.half(a2))), Nat.double(C.shift(p, X)))), N.add_assoc(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2))), Nat.double(C.shift(p, X))))
118
119# THEOREM: the 64-bit and of rand.bend is and_bits on the values
120def and64_value(+a: WU.U64, +b: WU.U64) -> {SW.value(R.and64(a, b)) == SR.and_bits(64n, SW.value(a), SW.value(b)) : Nat}:
121  match a b:
122    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
123      %Equal.sym(Nat, U32.to_nat(U32.and(al, bl)), SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), uand(al, bl)) : {Nat.add(_, C.shift(32n, U32.to_nat(U32.and(ah, bh)))) == SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}
124      %Equal.sym(Nat, U32.to_nat(U32.and(ah, bh)), SR.and_bits(32n, U32.to_nat(ah), U32.to_nat(bh)), uand(ah, bh)) : {Nat.add(SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), C.shift(32n, _)) == SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}
125      Equal.sym(Nat, SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), Nat.add(SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), C.shift(32n, SR.and_bits(32n, U32.to_nat(ah), U32.to_nat(bh)))), and_join(32n, 32n, U32.to_nat(al), U32.to_nat(ah), U32.to_nat(bl), U32.to_nat(bh), WA.vb(al), WA.vb(bl)))