~/bend-docscommunity

proofs/crypto/secp256k1/scalarpow.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as Scalarpow

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/scalarpow.src; edit the .src

18 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/scalar.bend as S
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WW
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./ineq.bend as I
import ./consts.bend as K
import ./bitsv.bend as BV
import ./modexp.bend as ME
import ./scalarops.bend as SO
import ./lits.bend as LT

Definitions

def m source · line 25 · raw

@+one:Nat -> Nat

def step_e source · line 29 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), acc) == True{} : Bool} -> @+e:Nat -> @+he:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(acc) == Nat.mod(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), e), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat} -> @b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow_step(b, x, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(acc, acc))) == Nat.mod(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), Nat.add(Nat.mul(b, one), Nat.double(e))), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat}

one square-and-multiply step

def step_r source · line 45 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), acc) == True{} : Bool} -> @b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow_step(b, x, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(acc, acc))) == True{} : Bool}

def pow_r source · line 54 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @bs:List<&2, Nat> -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), acc) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow_go(x, bs, acc)) == True{} : Bool}

def pow_e source · line 63 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @bs:List<&2, Nat> -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), acc) == True{} : Bool} -> @+e:Nat -> @+he:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(acc) == Nat.mod(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), e), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow_go(x, bs, acc)) == Nat.mod(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(bs, one, e)), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat}

x^e for the exponent spelled by the bits, from acc = x^e0

def pow_is source · line 72 · raw

@+one:Nat -> @x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+bs:List<&2, Nat> -> @+acc:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow(x, bs, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow_go(x, bs, acc) : List<&2, Nat>}

S.pow looks at x first

def pow_ev source · line 79 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+bs:List<&2, Nat> -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), acc) == True{} : Bool} -> @+e:Nat -> @+he:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(acc) == Nat.mod(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), e), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow(x, bs, acc)) == Nat.mod(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(bs, one, e)), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat}

def pow_rv source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+bs:List<&2, Nat> -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), acc) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.pow(x, bs, acc)) == True{} : Bool}

def one_lt source · line 89 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(1n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)) == True{} : Bool}

def one_r source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.one) == True{} : Bool}

def one_e source · line 95 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.one) == Nat.mod(Nat.pow(x, 0n), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat}

def xn source · line 101 · raw

List<&2, Nat>

def zeros7 source · line 104 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n]) == 0n : Nat}

def zeros_tail source · line 129 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]) : Nat}

the trailing zero limbs add nothing

def xn_digits source · line 136 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, xn) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), one) : Nat}

c_n + 1

def xn_limbs source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, xn) == True{} : Bool}

def xb source · line 151 · raw

List<&2, Nat>

the bits of c_n + 1, most significant first

def bits_xb source · line 161 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(xn) == xb : List<&2, Nat>}

def ib_lit source · line 164 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv_bits == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(xb) : List<&2, Nat>}

def xb01 source · line 167 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(xb) == True{} : Bool}

def xb_len source · line 170 · raw

{List.length(&2, Nat, xb) == 256n : Nat}

def xb_v source · line 174 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(xb, one, 0n) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), one) : Nat}

hv(xb) = c_n + 1

def inv_h2 source · line 182 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv_bits, one, 0n), 2n)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) : Nat}

def exp_inv source · line 197 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv_bits, one, 0n) == Nat.sub(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one), 2n) : Nat}

def inv_bits01 source · line 205 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv_bits) == True{} : Bool}

def inv_v source · line 208 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv(a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.minv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, a)) : Nat}

def inv_r source · line 217 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv(a)) == True{} : Bool}