def unpack_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/peth.bend:40

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

40def unpack_v(ws: List<&1, U32>) -> {E.unpack(ws) == ES.unpack(ws) : List<&2, U32>}:
41  match ws:
42    case Nil{}:
43      {==}
44    case +w <> t:
45      Equal.cong(List<&2, U32>, List<&2, U32>, l => U32.and(w, 255) <> U32.and(U32.shrn(w, 8n), 255) <> U32.and(U32.shrn(w, 16n), 255) <> U32.shrn(w, 24n) <> l, E.unpack(t), ES.unpack(t), unpack_v(t))