def tagged_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:60

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY

60def tagged_len(+tag: List<&2, U32>, +x: List<&2, U32>) -> {B.has_len(32n, SS.tagged(tag, x)) == True{} : Bool}:
61  %Equal.sym(Bool, B.has_len(32n, SS.tagged(tag, x)), Nat.is_eq(List.length(&2, U32, SS.tagged(tag, x)), 32n), BY.has_len_v(32n, SS.tagged(tag, x))) : {_ == True{} : Bool}
62  %Equal.sym(Nat, List.length(&2, U32, SS.tagged(tag, x)), 32n, fips_len(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x)))) : {Nat.is_eq(_, 32n) == True{} : Bool}
63  {==}