def valid_p8

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:168

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

168def 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)))