~/jendhub

proofs/crypto/argon2/run.bend

bend-collections-laws-crypto@1.0.0.0 · 93 lines · 6 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR2
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
13import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M
14import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
15import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
16import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as BL
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as MEM
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as HS
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/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
28def 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
34def 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
47def 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
50def 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.
54def 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<U32>}:
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<U32>}
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<U32>}
73      %Equal.sym(Array<U32>, 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<U32>}
74      %Equal.sym(Array<U32>, 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<U32>}
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]).
80def 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<U32> & 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)