def to_be_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:298

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
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/proofs/crypto/secp256k1/limbs.bend as LV

298def to_be_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +h: {FS.limbs16(one, 16n, xs) == True{} : Bool}) -> {B.to_be(xs) == CV.i2osp(32n, LV.ev(xs)) : List<&2, U32>}:
299  %Equal.sym(List<&2, U32>, CV.i2osp(32n, LV.ev(xs)), CV.i2osp_go(32n, LV.ev(xs)), i2_is(32n, LV.ev(xs))) : {B.to_be(xs) == _ : List<&2, U32>}
300  %Equal.sym(List<&2, U32>, B.bytes_le(xs), CV.i2osp_le(Nat.double(16n), LV.ev(xs)), bytes_le_v(one, h1, 16n, xs, h)) : {List.reverse(&2, U32, _) == List.reverse(&2, U32, CV.i2osp_le(32n, LV.ev(xs))) : List<&2, U32>}
301  {==}