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 import ./run.bend as R 22 23 # Argon2id of the implementation equals Argon2id of the specification for 24 # every input the implementation accepts. 25 26 # ---------------------------------------------------------------- the memory geometry 27 28 def X(+m: Nat, +p: Nat) -> Nat: 29 Nat.div(m, Nat.mul(4n, p)) 30 31 def mm_swap(+p: Nat, +x: Nat) -> {Nat.mul(Nat.mul(4n, p), x) == Nat.mul(Nat.mul(4n, x), p) : Nat}: 32 Equal.trans(Nat, Nat.mul(Nat.mul(4n, p), x), Nat.mul(4n, Nat.mul(p, x)), Nat.mul(Nat.mul(4n, x), p), 33 NA.mul_assoc(4n, p, x), 34 Equal.trans(Nat, Nat.mul(4n, Nat.mul(p, x)), Nat.mul(4n, Nat.mul(x, p)), Nat.mul(Nat.mul(4n, x), p), 35 Equal.cong(Nat, Nat, z => Nat.mul(4n, z), Nat.mul(p, x), Nat.mul(x, p), NA.mul_comm(p, x)), 36 Equal.sym(Nat, Nat.mul(Nat.mul(4n, x), p), Nat.mul(4n, Nat.mul(x, p)), NA.mul_assoc(4n, x, p)))) 37 38 # Exact division: y * d / d = y for d >= 1. 39 def div_exact(+y: Nat, +d: Nat, +hd: {Nat.is_le(1n, d) == True{} : Bool}) -> {Nat.div(Nat.mul(y, d), d) == y : Nat}: 40 match d: 41 case 0n: 42 Empty.absurd({Nat.div(Nat.mul(y, 0n), 0n) == y : Nat}, L.false_true(hd)) 43 case 1n+ +b: 44 %NA.add_zero(Nat.mul(y, 1n+b)) : {Nat.div(_, 1n+b) == y : Nat} 45 NR.div_of(y, b, 0n, {==}) 46 47 # q = m' / p = 4 X. 48 def q_eq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, X(m, p)) : Nat}: 49 %Equal.sym(Nat, Nat.mul(Nat.mul(4n, p), X(m, p)), Nat.mul(Nat.mul(4n, X(m, p)), p), mm_swap(p, X(m, p))) : {Nat.div(_, p) == Nat.mul(4n, X(m, p)) : Nat} 50 div_exact(Nat.mul(4n, X(m, p)), p, hp) 51 52 # sl = q / 4 = X. 53 def div4(+x: Nat) -> {Nat.div(Nat.mul(4n, x), 4n) == x : Nat}: 54 %Equal.sym(Nat, Nat.mul(4n, x), Nat.mul(x, 4n), NA.mul_comm(4n, x)) : {Nat.div(_, 4n) == x : Nat} 55 div_exact(x, 4n, {==}) 56 57 def sl_eq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(Nat.div(I.blocks(m, p), p), 4n) == X(m, p) : Nat}: 58 %Equal.sym(Nat, Nat.div(I.blocks(m, p), p), Nat.mul(4n, X(m, p)), q_eq(m, p, hp)) : {Nat.div(_, 4n) == X(m, p) : Nat} 59 div4(X(m, p)) 60 61 # q = 4 sl 62 def hq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, Nat.div(Nat.div(I.blocks(m, p), p), 4n)) : Nat}: 63 %Equal.sym(Nat, Nat.div(Nat.div(I.blocks(m, p), p), 4n), X(m, p), sl_eq(m, p, hp)) : {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, _) : Nat} 64 q_eq(m, p, hp) 65 66 # m' = p q 67 def hlen(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {I.blocks(m, p) == Nat.mul(p, Nat.div(I.blocks(m, p), p)) : Nat}: 68 %Equal.sym(Nat, Nat.div(I.blocks(m, p), p), Nat.mul(4n, X(m, p)), q_eq(m, p, hp)) : {I.blocks(m, p) == Nat.mul(p, _) : Nat} 69 Equal.trans(Nat, Nat.mul(Nat.mul(4n, p), X(m, p)), Nat.mul(Nat.mul(p, 4n), X(m, p)), Nat.mul(p, Nat.mul(4n, X(m, p))), 70 Equal.cong(Nat, Nat, z => Nat.mul(z, X(m, p)), Nat.mul(4n, p), Nat.mul(p, 4n), NA.mul_comm(4n, p)), 71 NA.mul_assoc(p, 4n, X(m, p))) 72 73 # 8p <= m gives X >= 2. 74 def x_ge2(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +h8: {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}) -> {Nat.is_le(2n, X(m, p)) == True{} : Bool}: 75 match p: 76 case 0n: 77 Empty.absurd({Nat.is_le(2n, X(m, 0n)) == True{} : Bool}, L.false_true(hp)) 78 case 1n+ +b: 79 +e = NR.le_div(Nat.add(b, Nat.mul(3n, 1n+b)), 2n, m) 80 +h2 = L.subst(Nat, z => {Nat.is_le(z, m) == True{} : Bool}, Nat.mul(8n, 1n+b), Nat.mul(2n, Nat.mul(4n, 1n+b)), NA.mul_assoc(2n, 4n, 1n+b), h8) 81 Equal.trans(Bool, Nat.is_le(2n, X(m, 1n+b)), Nat.is_le(Nat.mul(2n, Nat.mul(4n, 1n+b)), m), True{}, e, h2) 82 83 # ---------------------------------------------------------------- the memory size 84 85 def pw_eq(+k: Nat) -> {M.pw(k) == SC.pow2(k) : Nat}: 86 match k: 87 case 0n: 88 {==} 89 case 1n+ +j: 90 Equal.cong(Nat, Nat, z => Nat.double(z), M.pw(j), SC.pow2(j), pw_eq(j)) 91 92 def d8(+b: Nat) -> {Nat.mul(b, 256n) == Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(b)))))))) : Nat}: 93 match b: 94 case 0n: 95 {==} 96 case 1n+ +c: 97 %Equal.sym(Nat, Nat.mul(c, 256n), Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(c)))))))), d8(c)) : {Nat.add(256n, _) == Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(1n+c)))))))) : Nat} 98 {==} 99 100 # levels(n) = k with k <= 23 gives n <= 2^k. 101 def levels_go_ok(+f: Nat, +n: Nat, +k: Nat, +done: Bool, +hd: {done == Nat.is_le(n, M.pw(k)) : Bool}, +hr: {Nat.is_lt(M.levels_go(f, n, k, done), Nat.add(k, f)) == True{} : Bool}) -> {Nat.is_le(n, M.pw(M.levels_go(f, n, k, done))) == True{} : Bool}: 102 match f done: 103 case _ True{}: 104 Equal.sym(Bool, True{}, Nat.is_le(n, M.pw(k)), hd) 105 case 0n False{}: 106 Empty.absurd({Nat.is_le(n, M.pw(k)) == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(k, Nat.add(k, 0n)), True{}, Equal.trans(Bool, False{}, Nat.is_lt(k, k), Nat.is_lt(k, Nat.add(k, 0n)), Equal.sym(Bool, Nat.is_lt(k, k), False{}, N.lt_irrefl(k)), Equal.cong(Nat, Bool, z => Nat.is_lt(k, z), k, Nat.add(k, 0n), Equal.sym(Nat, Nat.add(k, 0n), k, N.add_zero(k)))), hr))) 107 case 1n+ +g False{}: 108 +r = M.levels_go(g, n, 1n+k, Nat.is_le(n, M.pw(1n+k))) 109 levels_go_ok(g, n, 1n+k, Nat.is_le(n, M.pw(1n+k)), {==}, L.subst(Nat, z => {Nat.is_lt(r, z) == True{} : Bool}, Nat.add(k, 1n+g), 1n+Nat.add(k, g), N.add_succ(k, g), hr)) 110 111 def levels_ok(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_le(n, SC.pow2(M.levels(n))) == True{} : Bool}: 112 +hr = N.le_lt_trans(M.levels(n), 23n, 32n, h, {==}) 113 L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, M.pw(M.levels(n)), SC.pow2(M.levels(n)), pw_eq(M.levels(n)), levels_go_ok(32n, n, 0n, Nat.is_le(n, 1n), {==}, hr)) 114 115 # 256 m' <= 2^(8 + k). 116 def cap(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_le(Nat.mul(SC.length(A.Block, SC.replicate(A.Block, n, SG.zero())), 256n), SC.pow2(Nat.add(8n, M.levels(n)))) == True{} : Bool}: 117 +k = M.levels(n) 118 %Equal.sym(Nat, SC.length(A.Block, SC.replicate(A.Block, n, SG.zero())), n, LL.length_replicate(A.Block, n, SG.zero())) : {Nat.is_le(Nat.mul(_, 256n), SC.pow2(Nat.add(8n, k))) == True{} : Bool} 119 %d8(SC.pow2(k)) : {Nat.is_le(Nat.mul(n, 256n), _) == True{} : Bool} 120 AR2.mul_le(n, SC.pow2(k), 256n, levels_ok(n, h)) 121 122 def depth_lt(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(8n, M.levels(n)), 32n) == True{} : Bool}: 123 N.le_lt_succ(M.levels(n), 23n, h) 124 125 # ---------------------------------------------------------------- the passes on the first blocks 126 127 def q2(+q: Nat, +sl: Nat, +hq: {q == Nat.mul(4n, sl) : Nat}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}) -> {Nat.is_le(2n, q) == True{} : Bool}: 128 L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.mul(4n, sl), q, Equal.sym(Nat, q, Nat.mul(4n, sl), hq), N.le_trans(2n, sl, Nat.mul(4n, sl), hsl, N.le_add_right(sl, Nat.mul(3n, sl)))) 129 130 def fill_eq(+d: Nat, +t: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +hh: List<&2, U32>, +z: List<&2, A.Block>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, z), 256n), SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(A.Block, z) == Nat.mul(p, q) : Nat}, +hq: {q == Nat.mul(4n, sl) : Nat}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hsl: {Nat.is_le(2n, sl) == True{} : Bool}) -> {I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, hh, AR.thaw(U32, MEM.mt(d, z)))) == AR.thaw(U32, MEM.mt(d, SA.passes_go(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hh, z)))) : Array}: 131 +m1 = SA.init_go(p, 0n, q, hh, z) 132 +e = R.init_len(p, 0n, q, hh, z) 133 %Equal.sym(Array, I.init_go(p, 0n, q, hh, AR.thaw(U32, MEM.mt(d, z))), AR.thaw(U32, MEM.mt(d, m1)), R.init_eq(d, p, 0n, p, q, hh, z, hd, hc, hlen, q2(q, sl, hq, hsl), N.le_refl(p))) : {I.passes_go(t, 0n, p, q, sl, mm, t, _) == AR.thaw(U32, MEM.mt(d, SA.passes_go(t, 0n, p, q, sl, mm, t, m1))) : Array} 134 F.passes_eq(d, t, 0n, p, q, sl, mm, t, m1, hd, F.keep_c(d, z, m1, e, hc), F.keep_len(z, m1, Nat.mul(p, q), e, hlen), hq, hp, hsl) 135 136 # ---------------------------------------------------------------- the tag 137 138 def tail_i(+tl: Nat, +p: Nat, +q: Nat, a: Array) -> List<&2, U32>: 139 I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, G.zero(), M.get(Nat.sub(q, 1n), a)))) 140 141 def tail_s(+tl: Nat, +p: Nat, +q: Nat, +mem: List<&2, A.Block>) -> List<&2, U32>: 142 SA.hprime(tl, SA.block_bytes(SA.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), SA.get(mem, Nat.sub(q, 1n)), mem))) 143 144 def tail_eq(+d: Nat, +tl: Nat, +p: Nat, +q: Nat, +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}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {tail_i(tl, p, q, AR.thaw(U32, MEM.mt(d, mem))) == tail_s(tl, p, q, mem) : List<&2, U32>}: 145 +b = SA.get(mem, Nat.sub(q, 1n)) 146 +c = SA.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), b, mem) 147 +hb = F.lt_len(Nat.sub(q, 1n), mem, p, q, hlen, N.lt_le_trans(Nat.sub(q, 1n), q, Nat.mul(p, q), F.sub1_lt(q, hq1), F.le_mul_left(p, q, hp))) 148 -ar = AR.thaw(U32, MEM.mt(d, mem)) 149 %Equal.sym(Array & A.Block, M.get(Nat.sub(q, 1n), ar), (ar, b), MEM.get_block(d, mem, Nat.sub(q, 1n), hd, hc, hb)) : {I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, G.zero(), _))) == tail_s(tl, p, q, mem) : List<&2, U32>} 150 %Equal.sym(A.Block, G.zero(), SG.zero(), BL.zero_correct()) : {I.hprime(tl, I.block_bytes(I.final_go(Nat.sub(p, 1n), 0n, q, _, (ar, b)))) == tail_s(tl, p, q, mem) : List<&2, U32>} 151 %Equal.sym(A.Block, I.final_go(Nat.sub(p, 1n), 0n, q, SG.zero(), (ar, b)), c, R.final_eq(d, Nat.sub(p, 1n), 0n, p, q, SG.zero(), b, mem, hd, hc, hlen, hq1, F.sub1_lt(p, hp))) : {I.hprime(tl, I.block_bytes(_)) == tail_s(tl, p, q, mem) : List<&2, U32>} 152 Equal.trans(List<&2, U32>, I.hprime(tl, I.block_bytes(c)), I.hprime(tl, SA.block_bytes(c)), SA.hprime(tl, SA.block_bytes(c)), 153 Equal.cong(List<&2, U32>, List<&2, U32>, x => I.hprime(tl, x), I.block_bytes(c), SA.block_bytes(c), HS.block_bytes_eq(c)), 154 HS.hprime_eq(tl, SA.block_bytes(c))) 155 156 # ---------------------------------------------------------------- Argon2id 157 158 def valid_p1(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hv: {SA.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool}) -> {Nat.is_le(1n, p) == True{} : Bool}: 159 +a1 = Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n)) 160 +a2 = Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n)) 161 +b1 = Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n)) 162 +b2 = Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n)) 163 +cs = Bool.and(Bool.and(Nat.is_le(8n, SA.len(salt)), Nat.is_le(SA.len(salt), 4294967295n)), Bool.and(Nat.is_le(SA.len(pw), 4294967295n), Bool.and(Nat.is_le(SA.len(key), 4294967295n), Nat.is_le(SA.len(ad), 4294967295n)))) 164 +ha = L.and_left(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv) 165 +hb = L.and_right(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv) 166 L.and_left(Nat.is_le(1n, p), Nat.is_le(p, 16777215n), L.and_left(a1, a2, ha)) 167 168 def valid_p8(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hv: {SA.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool}) -> {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}: 169 +a1 = Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n)) 170 +a2 = Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n)) 171 +b1 = Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n)) 172 +b2 = Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n)) 173 +cs = Bool.and(Bool.and(Nat.is_le(8n, SA.len(salt)), Nat.is_le(SA.len(salt), 4294967295n)), Bool.and(Nat.is_le(SA.len(pw), 4294967295n), Bool.and(Nat.is_le(SA.len(key), 4294967295n), Nat.is_le(SA.len(ad), 4294967295n)))) 174 +ha = L.and_left(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv) 175 +hb = L.and_right(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv) 176 L.and_left(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n), L.and_left(b1, b2, L.and_left(Bool.and(b1, b2), cs, hb))) 177 178 def run_body(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +h8: {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.run(pw, salt, key, ad, t, m, p, tl) == SA.run(pw, salt, key, ad, t, m, p, tl) : List<&2, U32>}: 179 +mm = I.blocks(m, p) 180 +q = Nat.div(mm, p) 181 +sl = Nat.div(q, 4n) 182 +k = M.levels(mm) 183 +d = Nat.add(8n, k) 184 +z = SC.replicate(A.Block, mm, SG.zero()) 185 +hi = I.h0(p, tl, m, t, pw, salt, key, ad) 186 +hs = SA.h0(p, tl, m, t, pw, salt, key, ad) 187 +hd = depth_lt(mm, hf) 188 +hc = cap(mm, hf) 189 +hlz = LL.length_replicate(A.Block, mm, SG.zero()) 190 +hc0 = L.subst(Nat, x => {Nat.is_le(Nat.mul(x, 256n), SC.pow2(d)) == True{} : Bool}, SC.length(A.Block, z), mm, hlz, hc) 191 +hlen0 = Equal.trans(Nat, SC.length(A.Block, z), mm, Nat.mul(p, q), hlz, hlen(m, p, hp)) 192 +hq0 = hq(m, p, hp) 193 +hsl = L.subst(Nat, x => {Nat.is_le(2n, x) == True{} : Bool}, X(m, p), sl, Equal.sym(Nat, sl, X(m, p), sl_eq(m, p, hp)), x_ge2(m, p, hp, h8)) 194 +hq1 = N.le_trans(1n, 2n, q, {==}, q2(q, sl, hq0, hsl)) 195 +m2 = SA.passes_go(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hs, z)) 196 +e2 = Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, SA.init_go(p, 0n, q, hs, z)), SC.length(A.Block, z), F.passes_len(t, 0n, p, q, sl, mm, t, SA.init_go(p, 0n, q, hs, z)), R.init_len(p, 0n, q, hs, z)) 197 -goal = SA.run(pw, salt, key, ad, t, m, p, tl) 198 %Equal.sym(Array, Array.new(U32, d, 0), AR.thaw(U32, MEM.mt(d, z)), MEM.new_mem(d, mm, hc0)) : {tail_i(tl, p, q, I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, hi, _))) == goal : List<&2, U32>} 199 %Equal.sym(List<&2, U32>, hi, hs, HS.h0_eq(p, tl, m, t, pw, salt, key, ad)) : {tail_i(tl, p, q, I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, _, AR.thaw(U32, MEM.mt(d, z))))) == goal : List<&2, U32>} 200 %Equal.sym(Array, I.passes_go(t, 0n, p, q, sl, mm, t, I.init_go(p, 0n, q, hs, AR.thaw(U32, MEM.mt(d, z)))), AR.thaw(U32, MEM.mt(d, m2)), fill_eq(d, t, p, q, sl, mm, hs, z, hd, hc, hlen0, hq0, hp, hsl)) : {tail_i(tl, p, q, _) == goal : List<&2, U32>} 201 tail_eq(d, tl, p, q, m2, hd, F.keep_c(d, z, m2, e2, hc), F.keep_len(z, m2, Nat.mul(p, q), e2, hlen0), hp, hq1) 202 203 def run_eq(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hv: {SA.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool}, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.run(pw, salt, key, ad, t, m, p, tl) == SA.run(pw, salt, key, ad, t, m, p, tl) : List<&2, U32>}: 204 run_body(pw, salt, key, ad, t, m, p, tl, valid_p1(pw, salt, key, ad, t, m, p, tl, hv), valid_p8(pw, salt, key, ad, t, m, p, tl, hv), hf) 205 206 def checked_eq(+ok: Bool, +pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +e: {SA.valid(pw, salt, key, ad, t, m, p, tl) == ok : Bool}, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.checked(ok, pw, salt, key, ad, t, m, p, tl) == SA.checked(ok, pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}: 207 match ok: 208 case False{}: 209 {==} 210 case True{}: 211 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, x => Some{x}, I.run(pw, salt, key, ad, t, m, p, tl), SA.run(pw, salt, key, ad, t, m, p, tl), run_eq(pw, salt, key, ad, t, m, p, tl, e, hf)) 212 213 def valid_eq(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> {I.valid(pw, salt, key, ad, t, m, p, tl) == SA.valid(pw, salt, key, ad, t, m, p, tl) : Bool}: 214 {==} 215 216 def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}: 217 match b: 218 case True{}: 219 {==} 220 case False{}: 221 {==} 222 223 # Argon2id: for every password, salt, secret, associated data and parameters 224 # whose memory fits this implementation (m' <= 2^23 blocks), the 225 # implementation's tag (or None) is the specification's. 226 def argon2id_correct(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +hf: {I.fits(m, p) == True{} : Bool}) -> {I.argon2id(pw, salt, key, ad, t, m, p, tl) == SA.argon2id(pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}: 227 +v = SA.valid(pw, salt, key, ad, t, m, p, tl) 228 -goal = SA.argon2id(pw, salt, key, ad, t, m, p, tl) 229 %Equal.sym(Bool, I.fits(m, p), True{}, hf) : {I.checked(Bool.and(I.valid(pw, salt, key, ad, t, m, p, tl), _), pw, salt, key, ad, t, m, p, tl) == goal : Maybe<&2, List<&2, U32>>} 230 %Equal.sym(Bool, I.valid(pw, salt, key, ad, t, m, p, tl), v, valid_eq(pw, salt, key, ad, t, m, p, tl)) : {I.checked(Bool.and(_, True{}), pw, salt, key, ad, t, m, p, tl) == goal : Maybe<&2, List<&2, U32>>} 231 %Equal.sym(Bool, Bool.and(v, True{}), v, and_true(v)) : {I.checked(_, pw, salt, key, ad, t, m, p, tl) == goal : Maybe<&2, List<&2, U32>>} 232 checked_eq(v, pw, salt, key, ad, t, m, p, tl, {==}, hf)