def pow_rv

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/scalarpow.bend:83

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/src/crypto/secp256k1/scalar.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV

83def pow_rv(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, +hb: {BV.all01(bs) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.pow(x, bs, acc)) == True{} : Bool}:
84  %Equal.sym(List<&2, Nat>, S.pow(x, bs, acc), S.pow_go(x, bs, acc), pow_is(one, x, hx, bs, acc)) : {FS.reduced(one, FS.order(one), _) == True{} : Bool}
85  pow_r(one, h1, x, hx, bs, acc, ha, hb)