def dlr

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pdec.bend:131

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
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/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL

131def dlr(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, c33: Bool, c65: Bool, +h33: {B.has_len(33n, bs) == c33 : Bool}, +h65: {B.has_len(65n, bs) == c65 : Bool}) -> {PE.mpred(one, P.decode_len(bs, c33, c65)) == True{} : Bool}:
132  match c33 c65:
133    case True{} _:
134      %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {PE.mpred(one, P.decode_33(B.head(bs), _)) == True{} : Bool}
135      d33r(one, h1, B.head(bs), CV.after(1n, bs), BL.len_tail(32n, bs, h33))
136    case False{} True{}:
137      %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {PE.mpred(one, P.decode_65(B.head(bs), _)) == True{} : Bool}
138      d65r(one, h1, B.head(bs), CV.after(1n, bs), BL.len_tail(64n, bs, h65))
139    case False{} False{}:
140      {==}