~/jendhub

proofs/crypto/argon2/gb.bend

bend-collections-laws-crypto@1.0.0.0 · 125 lines · 17 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/src/math/w64.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
8import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/lane.bend as L
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as I
12import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as B
13import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as S
14
15# GB of the implementation (src/crypto/argon2/blamka.bend) equals GB of the
16# specification (spec/crypto/argon2/blamka.bend) for every four lanes.
17#
18# The only step that is not a computation on the lanes' bits is the product
19# of the multiplication-hardened fBlaMka: the implementation's 64-bit product
20# of two U32 (src/math/w64.bend's mul32, by 16-bit halves) is the lane of the
21# Nat product (mul32's proved value, proofs/math/typed/w64mul.bend, and the
22# two-limb round trip). GB is then rewritten one fBlaMka at a time.
23
24# ---------------------------------------------------------------- the product
25
26# Every U64 is the U64 of its value.
27def rt(+x: WU.U64) -> {SW.of_nat(SW.value(x)) == x : WU.U64}:
28  match x:
29    case WU.U64{+l, +h}:
30      +el = WW.low_u(32n, LW.v(l), LW.v(h), LW.vb(l))
31      +eh = WW.high_u(32n, LW.v(l), LW.v(h), LW.vb(l))
32      +e1 = Equal.trans(U32, U32.from_nat(C.low(32n, SW.value(WU.U64{l, h}))), U32.from_nat(LW.v(l)), l, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, SW.value(WU.U64{l, h})), LW.v(l), el), LW.rt(l))
33      +e2 = Equal.trans(U32, U32.from_nat(C.high(32n, SW.value(WU.U64{l, h}))), U32.from_nat(LW.v(h)), h, Equal.cong(Nat, U32, z => U32.from_nat(z), C.high(32n, SW.value(WU.U64{l, h})), LW.v(h), eh), LW.rt(h))
34      Equal.trans(WU.U64, WU.U64{U32.from_nat(C.low(32n, SW.value(WU.U64{l, h}))), U32.from_nat(C.high(32n, SW.value(WU.U64{l, h})))}, WU.U64{l, U32.from_nat(C.high(32n, SW.value(WU.U64{l, h})))}, WU.U64{l, h}, Equal.cong(U32, WU.U64, z => WU.U64{z, U32.from_nat(C.high(32n, SW.value(WU.U64{l, h})))}, U32.from_nat(C.low(32n, SW.value(WU.U64{l, h}))), l, e1), Equal.cong(U32, WU.U64, z => WU.U64{l, z}, U32.from_nat(C.high(32n, SW.value(WU.U64{l, h}))), h, e2))
35
36# mul32(a, b) is the U64 of a * b.
37def mul32_of(+a: U32, +b: U32) -> {X.mul32(a, b) == SW.of_nat(Nat.mul(U32.to_nat(a), U32.to_nat(b))) : WU.U64}:
38  Equal.trans(WU.U64, X.mul32(a, b), SW.of_nat(SW.value(X.mul32(a, b))), SW.of_nat(Nat.mul(U32.to_nat(a), U32.to_nat(b))),
39    Equal.sym(WU.U64, SW.of_nat(SW.value(X.mul32(a, b))), X.mul32(a, b), rt(X.mul32(a, b))),
40    Equal.cong(Nat, WU.U64, z => SW.of_nat(z), SW.value(X.mul32(a, b)), Nat.mul(U32.to_nat(a), U32.to_nat(b)), W64M.mul32_value(a, b)))
41
42# The implementation's product lane is the specification's.
43def prod_correct(+a: U32, +b: U32) -> {I.prod(a, b) == S.lane_of(Nat.mul(U32.to_nat(a), U32.to_nat(b))) : T.Lane}:
44  Equal.cong(WU.U64, T.Lane, +z => T.W{X.lo(z), X.hi(z)}, X.mul32(a, b), SW.of_nat(Nat.mul(U32.to_nat(a), U32.to_nat(b))), mul32_of(a, b))
45
46# fBlaMka
47def bla_correct(+x: T.Lane, +y: T.Lane) -> {I.bla(x, y) == S.fBlaMka(x, y) : T.Lane}:
48  match x y:
49    case T.W{+xl, +xh} T.W{+yl, +yh}:
50      Equal.cong(T.Lane, T.Lane, +z => L.add(L.add(T.W{xl, xh}, T.W{yl, yh}), L.add(z, z)), I.prod(xl, yl), S.lane_of(Nat.mul(U32.to_nat(xl), U32.to_nat(yl))), prod_correct(xl, yl))
51
52# ---------------------------------------------------------------- GB
53
54# The rotations of XORs, lane by lane.
55def rx32(+d: T.Lane, +a: T.Lane) -> {L.rot32(L.xor(d, a)) == B.rotr(B.xor(d, a), 32n) : T.Lane}:
56  match d a:
57    case T.W{dl, dh} T.W{al, ah}:
58      {==}
59
60def rx24(+d: T.Lane, +a: T.Lane) -> {L.rot24(L.xor(d, a)) == B.rotr(B.xor(d, a), 24n) : T.Lane}:
61  match d a:
62    case T.W{dl, dh} T.W{al, ah}:
63      {==}
64
65def rx16(+d: T.Lane, +a: T.Lane) -> {L.rot16(L.xor(d, a)) == B.rotr(B.xor(d, a), 16n) : T.Lane}:
66  match d a:
67    case T.W{dl, dh} T.W{al, ah}:
68      {==}
69
70def rx63(+d: T.Lane, +a: T.Lane) -> {L.rot63(L.xor(d, a)) == B.rotr(B.xor(d, a), 63n) : T.Lane}:
71  match d a:
72    case T.W{dl, dh} T.W{al, ah}:
73      {==}
74
75# The specification's GB after its first k assignment pairs.
76def m4(+a2: T.Lane, +b1: T.Lane, +c2: T.Lane, +d2: T.Lane) -> T.Quad:
77  T.Q{a2, B.rotr(B.xor(b1, c2), 63n), c2, d2}
78
79def m3(+a2: T.Lane, +b1: T.Lane, +c1: T.Lane, +d1: T.Lane) -> T.Quad:
80  +d2 = B.rotr(B.xor(d1, a2), 16n)
81  m4(a2, b1, S.fBlaMka(c1, d2), d2)
82
83def m2(+a1: T.Lane, +b: T.Lane, +c1: T.Lane, +d1: T.Lane) -> T.Quad:
84  +b1 = B.rotr(B.xor(b, c1), 24n)
85  m3(S.fBlaMka(a1, b1), b1, c1, d1)
86
87def m1(+a1: T.Lane, +b: T.Lane, +c: T.Lane, +d: T.Lane) -> T.Quad:
88  +d1 = B.rotr(B.xor(d, a1), 32n)
89  m2(a1, b, S.fBlaMka(c, d1), d1)
90
91def gb4_correct(+a2: T.Lane, +b1: T.Lane, +c2: T.Lane, +d2: T.Lane) -> {I.gb4(a2, b1, c2, d2) == m4(a2, b1, c2, d2) : T.Quad}:
92  Equal.cong(T.Lane, T.Quad, z => T.Q{a2, z, c2, d2}, L.rot63(L.xor(b1, c2)), B.rotr(B.xor(b1, c2), 63n), rx63(b1, c2))
93
94def gb3_correct(+a2: T.Lane, +b1: T.Lane, +c1: T.Lane, +d1: T.Lane) -> {I.gb3(a2, b1, c1, d1) == m3(a2, b1, c1, d1) : T.Quad}:
95  +di = L.rot16(L.xor(d1, a2))
96  +ds = B.rotr(B.xor(d1, a2), 16n)
97  Equal.trans(T.Quad, I.gb4(a2, b1, I.bla(c1, di), di), I.gb4(a2, b1, I.bla(c1, ds), ds), m4(a2, b1, S.fBlaMka(c1, ds), ds),
98    Equal.cong(T.Lane, T.Quad, +z => I.gb4(a2, b1, I.bla(c1, z), z), di, ds, rx16(d1, a2)),
99    Equal.trans(T.Quad, I.gb4(a2, b1, I.bla(c1, ds), ds), I.gb4(a2, b1, S.fBlaMka(c1, ds), ds), m4(a2, b1, S.fBlaMka(c1, ds), ds),
100      Equal.cong(T.Lane, T.Quad, z => I.gb4(a2, b1, z, ds), I.bla(c1, ds), S.fBlaMka(c1, ds), bla_correct(c1, ds)),
101      gb4_correct(a2, b1, S.fBlaMka(c1, ds), ds)))
102
103def gb2_correct(+a1: T.Lane, +b: T.Lane, +c1: T.Lane, +d1: T.Lane) -> {I.gb2(a1, b, c1, d1) == m2(a1, b, c1, d1) : T.Quad}:
104  +bi = L.rot24(L.xor(b, c1))
105  +bs = B.rotr(B.xor(b, c1), 24n)
106  Equal.trans(T.Quad, I.gb3(I.bla(a1, bi), bi, c1, d1), I.gb3(I.bla(a1, bs), bs, c1, d1), m3(S.fBlaMka(a1, bs), bs, c1, d1),
107    Equal.cong(T.Lane, T.Quad, +z => I.gb3(I.bla(a1, z), z, c1, d1), bi, bs, rx24(b, c1)),
108    Equal.trans(T.Quad, I.gb3(I.bla(a1, bs), bs, c1, d1), I.gb3(S.fBlaMka(a1, bs), bs, c1, d1), m3(S.fBlaMka(a1, bs), bs, c1, d1),
109      Equal.cong(T.Lane, T.Quad, z => I.gb3(z, bs, c1, d1), I.bla(a1, bs), S.fBlaMka(a1, bs), bla_correct(a1, bs)),
110      gb3_correct(S.fBlaMka(a1, bs), bs, c1, d1)))
111
112def gb1_correct(+a1: T.Lane, +b: T.Lane, +c: T.Lane, +d: T.Lane) -> {I.gb1(a1, b, c, d) == m1(a1, b, c, d) : T.Quad}:
113  +di = L.rot32(L.xor(d, a1))
114  +ds = B.rotr(B.xor(d, a1), 32n)
115  Equal.trans(T.Quad, I.gb2(a1, b, I.bla(c, di), di), I.gb2(a1, b, I.bla(c, ds), ds), m2(a1, b, S.fBlaMka(c, ds), ds),
116    Equal.cong(T.Lane, T.Quad, +z => I.gb2(a1, b, I.bla(c, z), z), di, ds, rx32(d, a1)),
117    Equal.trans(T.Quad, I.gb2(a1, b, I.bla(c, ds), ds), I.gb2(a1, b, S.fBlaMka(c, ds), ds), m2(a1, b, S.fBlaMka(c, ds), ds),
118      Equal.cong(T.Lane, T.Quad, z => I.gb2(a1, b, z, ds), I.bla(c, ds), S.fBlaMka(c, ds), bla_correct(c, ds)),
119      gb2_correct(a1, b, S.fBlaMka(c, ds), ds)))
120
121# GB: the implementation's equals the specification's.
122def gb_correct(+a: T.Lane, +b: T.Lane, +c: T.Lane, +d: T.Lane) -> {I.gb(a, b, c, d) == S.GB(a, b, c, d) : T.Quad}:
123  Equal.trans(T.Quad, I.gb1(I.bla(a, b), b, c, d), I.gb1(S.fBlaMka(a, b), b, c, d), m1(S.fBlaMka(a, b), b, c, d),
124    Equal.cong(T.Lane, T.Quad, z => I.gb1(z, b, c, d), I.bla(a, b), S.fBlaMka(a, b), bla_correct(a, b)),
125    gb1_correct(S.fBlaMka(a, b), b, c, d))