~/bend-docscommunity

proofs/crypto/secp256k1/fieldpow.bend checks

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

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/fieldpow.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/field.bend as F
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 ./bounds.bend as B
import ./consts.bend as K
import ./bitsv.bend as BV
import ./modexp.bend as ME
import ./fieldops.bend as FO

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.prime(one), x) == True{} : Bool} -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(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.pp(one)) : Nat} -> @b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.pow_step(b, x, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sq(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.pp(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.prime(one), x) == True{} : Bool} -> @+acc:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(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.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.pow_step(b, x, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sq(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.prime(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.prime(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.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.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.prime(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.prime(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.pp(one)) : Nat} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.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.pp(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.prime(one), x) == True{} : Bool} -> @+bs:List<&2, Nat> -> @+acc:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.pow(x, bs, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.pow_go(x, bs, acc) : List<&2, Nat>}

F.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.prime(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.prime(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.pp(one)) : Nat} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.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.pp(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.prime(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.prime(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.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.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.prime(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.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.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/field.one) == Nat.mod(Nat.pow(x, 0n), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) : Nat}

def xp_lit source · line 101 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([978n, 0n, 1n]) == [978n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n] : List<&2, Nat>}

def zeros13 source · line 104 · raw

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

def xp_digits source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([978n, 0n, 1n])) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), one) : Nat}

978 + 2^32 = c_p + 1

def xp_limbs source · line 171 · raw

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

def inv_h2 source · line 175 · raw

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

hv(bits of p - 2) + 2 = p

def exp_inv source · line 193 · raw

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

def inv_bits01 source · line 201 · raw

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

def inv_v source · line 204 · raw

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

def inv_r source · line 213 · raw

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

def yp_lit source · line 218 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n]) == [975n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n] : List<&2, Nat>}

def yp_digits source · line 222 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n])), one), one) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one) : Nat}

975 + 2^32 + 2 = c_p

def yp_limbs source · line 252 · raw

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

def sq_split source · line 255 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n]))) == List.append(&2, Nat, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sqrt_bits, [0n, 0n]) : List<&2, Nat>}

def sq_four source · line 259 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n]))), one, 0n) == Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sqrt_bits, one, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sqrt_bits, one, 0n)), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sqrt_bits, one, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sqrt_bits, one, 0n))) : Nat}

hv of the bits of p + 1 is 4 hv(sqrt bits)

def yp_hv source · line 272 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n])), one, 0n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n])) : Nat}

def sq_cb source · line 278 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n]))), one, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n]))), one) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat}

hv(bits of p + 1) + d + one = 2^256 with d = (c_p - 2)

def arr3 source · line 284 · raw

@+d:Nat -> @+o:Nat -> @+h:Nat -> {Nat.add(Nat.add(d, o), h) == Nat.add(Nat.add(h, d), o) : Nat}

def arr4 source · line 291 · raw

@+m:Nat -> @+d:Nat -> @+o:Nat -> {Nat.add(m, Nat.add(Nat.add(d, o), o)) == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}

def sq_g source · line 298 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n])), one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n]))), one, 0n)) == Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([975n, 0n, 1n])), one), Nat.add(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one), one)) : Nat}

def four_h source · line 305 · raw

@+h:Nat -> {Nat.add(Nat.add(h, h), Nat.add(h, h)) == Nat.add(Nat.mul(h, 4n), 0n) : Nat}

def exp_sqrt source · line 315 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.sqrt_bits, one, 0n) == Nat.div(Nat.add(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one), 1n), 4n) : Nat}

4 hv(sqrt bits) = p + 1, so hv(sqrt bits) = (p + 1) / 4

def sq01 source · line 325 · raw

@xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(List.append(&2, Nat, xs, ys)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(xs) == True{} : Bool}

def sqrt_bits01 source · line 332 · raw

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

def sqrt_v source · line 336 · raw

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

def sqrt_r source · line 345 · raw

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