def zeros_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pecr.bend:15

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E

15def zeros_v(bs: List<&2, U32>) -> {E.zeros_ok(bs) == ES.all_zero(bs) : Bool}:
16  match bs:
17    case Nil{}:
18      {==}
19    case +b <> t:
20      Equal.cong(Bool, Bool, x => Bool.and(U32.is_eq(b, 0), x), E.zeros_ok(t), ES.all_zero(t), zeros_v(t))