def long_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:99

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2

99# The long case of H': with Q = (T + 31) / 32, r = Q - 2 digests of 32 bytes and a last one of T - 32 r.
100def long_len(+tl: Nat, +q: Nat, +r: Nat, +v: List<&2, U32>, +e: {Nat.add(tl, 31n) == Nat.add(Nat.mul(q, 32n), r) : Nat}, +hr: {Nat.is_lt(r, 32n) == True{} : Bool}, +ht: {Nat.is_le(65n, tl) == True{} : Bool}, +hv: {len(v) == 64n : Nat}) -> {len(A2.hp_go(Nat.sub(Nat.sub(q, 2n), 1n), v, Nat.sub(tl, Nat.mul(32n, Nat.sub(q, 2n))))) == tl : Nat}:
101  match q:
102    case 0n:
103      Empty.absurd({len(A2.hp_go(0n, v, Nat.sub(tl, 0n))) == tl : Nat}, big(tl, 0n, r, e, hr, ht, {==}))
104    case 1n:
105      Empty.absurd({len(A2.hp_go(0n, v, Nat.sub(tl, 0n))) == tl : Nat}, big(tl, 1n, r, e, hr, ht, {==}))
106    case 2n:
107      Empty.absurd({len(A2.hp_go(0n, v, Nat.sub(tl, 0n))) == tl : Nat}, big(tl, 2n, r, e, hr, ht, {==}))
108    case 3n+ +j:
109      +m = Nat.mul(j, 32n)
110      +et = NR.add_cancel(31n, tl, Nat.add(65n, Nat.add(m, r)), Equal.trans(Nat, Nat.add(31n, tl), Nat.add(tl, 31n), Nat.add(Nat.mul(3n+j, 32n), r), N.add_comm(31n, tl), e))
111      %Equal.sym(Nat, tl, Nat.add(65n, Nat.add(m, r)), et) : {len(A2.hp_go(Nat.sub(j, 0n), v, Nat.sub(_, Nat.mul(32n, 1n+j)))) == _ : Nat}
112      %Equal.sym(Nat, Nat.sub(j, 0n), j, N.sub_zero(j)) : {len(A2.hp_go(_, v, Nat.sub(Nat.add(65n, Nat.add(m, r)), Nat.mul(32n, 1n+j)))) == Nat.add(65n, Nat.add(m, r)) : Nat}
113      %Equal.sym(Nat, Nat.mul(32n, 1n+j), Nat.mul(1n+j, 32n), NA.mul_comm(32n, 1n+j)) : {len(A2.hp_go(j, v, Nat.sub(Nat.add(65n, Nat.add(m, r)), _))) == Nat.add(65n, Nat.add(m, r)) : Nat}
114      %Equal.sym(Nat, Nat.sub(Nat.add(33n, Nat.add(m, r)), m), Nat.add(33n, r), sub_cancel(33n, m, r)) : {len(A2.hp_go(j, v, _)) == Nat.add(65n, Nat.add(m, r)) : Nat}
115      %Equal.sym(Nat, len(A2.hp_go(j, v, Nat.add(33n, r))), Nat.add(Nat.mul(1n+j, 32n), Nat.add(33n, r)), hp_go_len(j, v, Nat.add(33n, r), hv, N.lt_succ_le(r, 31n, hr))) : {_ == Nat.add(65n, Nat.add(m, r)) : Nat}
116      %Equal.sym(Nat, Nat.add(m, Nat.add(33n, r)), Nat.add(33n, Nat.add(m, r)), NA.add_swap(m, 33n, r)) : {Nat.add(32n, _) == Nat.add(65n, Nat.add(m, r)) : Nat}
117      {==}