Top.valid_p8: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as Top
Lines 168-176 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&start_line=168&end_line=176

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

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}:
  +a1 = Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n))
  +a2 = Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n))
  +b1 = Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n))
  +b2 = Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n))
  +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))))
  +ha = L.and_left(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv)
  +hb = L.and_right(Bool.and(a1, a2), Bool.and(Bool.and(b1, b2), cs), hv)
  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)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=valid