def tbv

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/psign.bend:54

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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY

54def tbv(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {B.to_be(x) == CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}:
55  %Equal.sym(List<&2, U32>, B.to_be(x), CV.i2osp(32n, LV.ev(x)), BY.to_be_v(one, h1, x, hx)) : {_ == CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}
56  %Equal.sym(Nat, FS.value(one, x), LV.ev(x), LV.ev_value(one, h1, x)) : {CV.i2osp(32n, LV.ev(x)) == CV.i2osp(32n, _) : List<&2, U32>}
57  {==}