def hp_go_ok

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as H
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP

185def hp_go_ok(+n: Nat, +v: List<&2, U32>, +last: Nat, +hv: {PP.ok(v) == True{} : Bool}) -> {PP.ok(A2.hp_go(n, v, last)) == True{} : Bool}:
186  match n v:
187    case _ Nil{}:
188      {==}
189    case 0n +x <> +r:
190      ok_append(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r), ok_take(x <> r, 32n, hv), hash_ok(last, x <> r))
191    case 1n+ +p +x <> +r:
192      ok_append(List.take(&2, U32, x <> r, 32n), A2.hp_go(p, H.hash(64n, x <> r), last), ok_take(x <> r, 32n, hv), hp_go_ok(p, H.hash(64n, x <> r), last, hash_ok(64n, x <> r)))