1 import Base 2 import ../../../spec/lib/common.bend as SC 3 import ../../lib/array.bend as AR 4 import ../../lib/list.bend as LL 5 import ../../lib/nat.bend as N 6 import ../../lib/logic.bend as L 7 import ../../lib/arith.bend as AR2 8 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 9 import ../../math/natural/arith.bend as NR 10 import ../../../src/crypto/blake/blake2b/types.bend as T 11 import ../../../src/crypto/argon2/types.bend as A 12 import ../../../src/crypto/argon2/blamka.bend as G 13 import ../../../src/crypto/argon2/memory.bend as M 14 import ../../../src/crypto/argon2/argon2.bend as I 15 import ../../../spec/crypto/argon2/blamka.bend as SG 16 import ../../../spec/crypto/argon2/argon2.bend as SA 17 import ./blamka.bend as BL 18 import ./memory.bend as MEM 19 import ./hash.bend as HS 20 import ./fill.bend as F 21 22 # Argon2id of the implementation equals Argon2id of the specification for 23 # every input the implementation accepts: the first two blocks of every 24 # lane, the passes (fill.bend), the final XOR and H' of it. 25 26 # ---------------------------------------------------------------- the first blocks 27 28 def init_block_eq(+hh: List<&2, U32>, +i: Nat, +l: Nat) -> {I.block_of(I.hprime(1024n, I.cat(hh, I.cat(I.le32(i), I.le32(l))))) == SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(i), SA.le32(l))))) : A.Block}: 29 +x = SA.cat(hh, SA.cat(SA.le32(i), SA.le32(l))) 30 Equal.trans(A.Block, I.block_of(I.hprime(1024n, x)), I.block_of(SA.hprime(1024n, x)), SA.block_of(SA.hprime(1024n, x)), 31 Equal.cong(List<&2, U32>, A.Block, z => I.block_of(z), I.hprime(1024n, x), SA.hprime(1024n, x), HS.hprime_eq(1024n, x)), 32 HS.block_of_eq(SA.hprime(1024n, x))) 33 34 def init_len(+n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.init_go(n, l, q, hh, mem)) == SC.length(A.Block, mem) : Nat}: 35 match n: 36 case 0n: 37 {==} 38 case 1n+ +rest: 39 +b0 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(0n), SA.le32(l))))) 40 +b1 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(1n), SA.le32(l))))) 41 +m1 = SA.set(mem, Nat.mul(l, q), b0) 42 +m2 = SA.set(m1, Nat.add(Nat.mul(l, q), 1n), b1) 43 Equal.trans(Nat, SC.length(A.Block, SA.init_go(rest, Nat.add(l, 1n), q, hh, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem), 44 init_len(rest, Nat.add(l, 1n), q, hh, m2), 45 Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), SC.length(A.Block, mem), LL.length_update(A.Block, m1, Nat.add(Nat.mul(l, q), 1n), b1), LL.length_update(A.Block, mem, Nat.mul(l, q), b0))) 46 47 def lt_first(+l: Nat, +p: Nat, +q: Nat, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hq2: {Nat.is_le(2n, q) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(l, q), Nat.mul(p, q)) == True{} : Bool}: 48 L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(p, q)) == True{} : Bool}, Nat.add(Nat.mul(l, q), 0n), Nat.mul(l, q), N.add_zero(Nat.mul(l, q)), F.lt_mul_add(l, p, 0n, q, hl, N.lt_le_trans(0n, 2n, q, {==}, hq2))) 49 50 def lt_second(+l: Nat, +p: Nat, +q: Nat, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hq2: {Nat.is_le(2n, q) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(l, q), 1n), Nat.mul(p, q)) == True{} : Bool}: 51 F.lt_mul_add(l, p, 1n, q, hl, N.lt_le_trans(1n, 2n, q, {==}, hq2)) 52 53 # B[l][0] and B[l][1] for the lanes l .. l + n - 1. 54 def init_eq(+d: Nat, +n: Nat, +l: Nat, +p: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq2: {Nat.is_le(2n, q) == True{} : Bool}, +hln: {Nat.is_le(Nat.add(l, n), p) == True{} : Bool}) -> {I.init_go(n, l, q, hh, AR.thaw(U32, MEM.mt(d, mem))) == AR.thaw(U32, MEM.mt(d, SA.init_go(n, l, q, hh, mem))) : Array}: 55 match n: 56 case 0n: 57 {==} 58 case 1n+ +rest: 59 +b0i = I.block_of(I.hprime(1024n, I.cat(hh, I.cat(I.le32(0n), I.le32(l))))) 60 +b1i = I.block_of(I.hprime(1024n, I.cat(hh, I.cat(I.le32(1n), I.le32(l))))) 61 +b0 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(0n), SA.le32(l))))) 62 +b1 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(1n), SA.le32(l))))) 63 +i0 = Nat.mul(l, q) 64 +i1 = Nat.add(Nat.mul(l, q), 1n) 65 +m1 = SA.set(mem, i0, b0) 66 +m2 = SA.set(m1, i1, b1) 67 +hl = F.lt_of_add_succ(l, rest, p, hln) 68 +e1 = LL.length_update(A.Block, mem, i0, b0) 69 +e2 = Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), SC.length(A.Block, mem), LL.length_update(A.Block, m1, i1, b1), e1) 70 -goal = AR.thaw(U32, MEM.mt(d, SA.init_go(rest, Nat.add(l, 1n), q, hh, m2))) 71 %Equal.sym(A.Block, b0i, b0, init_block_eq(hh, 0n, l)) : {I.init_go(rest, Nat.add(l, 1n), q, hh, M.set(i1, b1i, M.set(i0, _, AR.thaw(U32, MEM.mt(d, mem))))) == goal : Array} 72 %Equal.sym(A.Block, b1i, b1, init_block_eq(hh, 1n, l)) : {I.init_go(rest, Nat.add(l, 1n), q, hh, M.set(i1, _, M.set(i0, b0, AR.thaw(U32, MEM.mt(d, mem))))) == goal : Array} 73 %Equal.sym(Array, M.set(i0, b0, AR.thaw(U32, MEM.mt(d, mem))), AR.thaw(U32, MEM.mt(d, m1)), MEM.set_block(d, mem, i0, b0, hd, hc, F.lt_len(i0, mem, p, q, hlen, lt_first(l, p, q, hl, hq2)))) : {I.init_go(rest, Nat.add(l, 1n), q, hh, M.set(i1, b1, _)) == goal : Array} 74 %Equal.sym(Array, M.set(i1, b1, AR.thaw(U32, MEM.mt(d, m1))), AR.thaw(U32, MEM.mt(d, m2)), MEM.set_block(d, m1, i1, b1, hd, F.keep_c(d, mem, m1, e1, hc), F.lt_len(i1, m1, p, q, F.keep_len(mem, m1, Nat.mul(p, q), e1, hlen), lt_second(l, p, q, hl, hq2)))) : {I.init_go(rest, Nat.add(l, 1n), q, hh, _) == goal : Array} 75 init_eq(d, rest, Nat.add(l, 1n), p, q, hh, m2, hd, F.keep_c(d, mem, m2, e2, hc), F.keep_len(mem, m2, Nat.mul(p, q), e2, hlen), hq2, F.le_shift(l, rest, p, hln)) 76 77 # ---------------------------------------------------------------- the final block 78 79 # C = B[l][q-1] XOR .. for the lanes l .. l + n (b is B[l][q-1]). 80 def final_eq(+d: Nat, +n: Nat, +l: Nat, +p: Nat, +q: Nat, +c: A.Block, +b: A.Block, +mem: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, mem) == Nat.mul(p, q) : Nat}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}, +hln: {Nat.is_lt(Nat.add(l, n), p) == True{} : Bool}) -> {I.final_go(n, l, q, c, (AR.thaw(U32, MEM.mt(d, mem)), b)) == SA.final_go(n, l, q, c, b, mem) : A.Block}: 81 match n: 82 case 0n: 83 BL.xor_correct(c, b) 84 case 1n+ +rest: 85 +ix = Nat.add(Nat.mul(Nat.add(l, 1n), q), Nat.sub(q, 1n)) 86 +hl1 = N.le_lt_trans(Nat.add(l, 1n), Nat.add(l, 1n+rest), p, N.le_trans(Nat.add(l, 1n), Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), N.le_add_right(Nat.add(l, 1n), rest), N.eq_le(Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), MEM.add_one_assoc(l, rest))), hln) 87 +hix = F.lt_len(ix, mem, p, q, hlen, F.lt_mul_add(Nat.add(l, 1n), p, Nat.sub(q, 1n), q, hl1, F.sub1_lt(q, hq1))) 88 +hln2 = L.subst(Nat, z => {Nat.is_lt(z, p) == True{} : Bool}, Nat.add(l, 1n+rest), Nat.add(Nat.add(l, 1n), rest), Equal.sym(Nat, Nat.add(Nat.add(l, 1n), rest), Nat.add(l, 1n+rest), MEM.add_one_assoc(l, rest)), hln) 89 -ar = AR.thaw(U32, MEM.mt(d, mem)) 90 -goal = SA.final_go(rest, Nat.add(l, 1n), q, SG.xor(c, b), SA.get(mem, ix), mem) 91 %Equal.sym(Array & A.Block, M.get(ix, ar), (ar, SA.get(mem, ix)), MEM.get_block(d, mem, ix, hd, hc, hix)) : {I.final_go(rest, Nat.add(l, 1n), q, G.xor(c, b), _) == goal : A.Block} 92 %Equal.sym(A.Block, G.xor(c, b), SG.xor(c, b), BL.xor_correct(c, b)) : {I.final_go(rest, Nat.add(l, 1n), q, _, (ar, SA.get(mem, ix))) == goal : A.Block} 93 final_eq(d, rest, Nat.add(l, 1n), p, q, SG.xor(c, b), SA.get(mem, ix), mem, hd, hc, hlen, hq1, hln2)