def lane_ok

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
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/proofs/crypto/argon2/phc.bend as PP

164def lane_ok(+l: T.Lane) -> {PP.ok(H.lane_bytes(l)) == True{} : Bool}:
165  match l:
166    case T.W{+a, +b}:
167      ok_append(H.le(a), H.le(b), le_ok(a), le_ok(b))