~/bend-docscommunity

proofs/crypto/secp256k1/fwrap.bend checks

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

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

14 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 ../../../src/crypto/secp256k1/scalar.bend as S
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./fprot.bend as FR
import ./consts.bend as K
import ./listops.bend as LO

Definitions

def is_zero_f source · line 23 · raw

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

def eq_f source · line 28 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.eq(a, b) == Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, b)) : Bool}

def parity_f source · line 35 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.parity(a) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, a), 2n) : Nat}

def lt_p_f source · line 40 · raw

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

def is_zero_s source · line 48 · raw

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

def eq_s source · line 53 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.eq(a, b) == Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, b)) : Bool}

def lt_n_s source · line 60 · raw

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

def dig1 source · line 67 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+r:Nat -> {Nat.add(Nat.mul(one, 1n+d), r) == 1n+Nat.add(Nat.mul(one, d), r) : Nat}

a leading digit one larger

def hm_n1 source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(2n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.cm1)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat}

n + 1 + (2^256 - n - 1) = 2^256

def nlt source · line 101 · raw

@x:Nat -> @m:Nat -> {Bool.not(Nat.is_lt(x, 1n+m)) == Nat.is_lt(m, x) : Bool}

not (x < m + 1) is m < x

def is_high_s source · line 111 · raw

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