1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/w64.bend as SW 4 import ../../../src/math/w64.bend as X 5 import ../../../src/math/u64.bend as WU 6 import ../../math/typed/w64mul.bend as W64M 7 import ./words.bend as LW 8 import ../../math/typed/width.bend as WW 9 import ../../../src/crypto/blake/blake2b/types.bend as T 10 import ../../../src/crypto/blake/blake2b/lane.bend as L 11 import ../../../src/crypto/argon2/blamka.bend as I 12 import ../../../spec/crypto/blake/blake2b.bend as B 13 import ../../../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. 27 def 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. 37 def 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. 43 def 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 47 def 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. 55 def 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 60 def 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 65 def 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 70 def 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. 76 def 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 79 def 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 83 def 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 87 def 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 91 def 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 94 def 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 103 def 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 112 def 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. 122 def 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))