~/bend-docscommunity

proofs/crypto/secp256k1/fprot.bend checks

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

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

4 imports
import Base
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/scalar.bend as S

Definitions

def f_add_a source · line 11 · raw

@a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.add(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.add_b(a, b) : List<&2, Nat>}

def f_add_b source · line 18 · raw

@+a:List<&2, Nat> -> @b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.add_b(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.add_u(a, b) : List<&2, Nat>}

def f_add source · line 25 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.add(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.add_u(a, b) : List<&2, Nat>}

def f_mul_a source · line 28 · raw

@a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul_b(a, b) : List<&2, Nat>}

def f_mul_b source · line 35 · raw

@+a:List<&2, Nat> -> @b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul_b(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul_u(a, b) : List<&2, Nat>}

def f_mul source · line 42 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul_u(a, b) : List<&2, Nat>}

def f_eq_a source · line 45 · raw

@a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.eq(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.eq_b(a, b) : Bool}

def f_eq_b source · line 52 · raw

@+a:List<&2, Nat> -> @b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.eq_b(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.eq(a, b) : Bool}

def f_eq source · line 59 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.eq(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.eq(a, b) : Bool}

def s_add_a source · line 62 · raw

@a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add_b(a, b) : List<&2, Nat>}

def s_add_b source · line 69 · raw

@+a:List<&2, Nat> -> @b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add_b(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add_u(a, b) : List<&2, Nat>}

def s_add source · line 76 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add_u(a, b) : List<&2, Nat>}

def s_mul_a source · line 79 · raw

@a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul_b(a, b) : List<&2, Nat>}

def s_mul_b source · line 86 · raw

@+a:List<&2, Nat> -> @b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul_b(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul_u(a, b) : List<&2, Nat>}

def s_mul source · line 93 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul_u(a, b) : List<&2, Nat>}

def s_eq_a source · line 96 · raw

@a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.eq(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.eq_b(a, b) : Bool}

def s_eq_b source · line 103 · raw

@+a:List<&2, Nat> -> @b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.eq_b(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.eq(a, b) : Bool}

def s_eq source · line 110 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.eq(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.eq(a, b) : Bool}

def f_neg source · line 113 · raw

@a:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.neg(a) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.neg_u(a) : List<&2, Nat>}

def s_neg source · line 116 · raw

@a:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(a) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg_u(a) : List<&2, Nat>}

def s_reduce source · line 119 · raw

@xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce_u(xs) : List<&2, Nat>}

def lred source · line 122 · raw

@+c:List<&2, Nat> -> @+k:Nat -> @xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, k, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce_go(c, k, xs) : List<&2, Nat>}