~/bend-docscommunity

proofs/crypto/secp256k1/pecr.bend checks

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

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

8 imports
import Base
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/ecdsa.bend as E
import ./prec.bend as PR
import ./peth.bend as PET
import ./blist.bend as BL

Definitions

def zeros_v source · line 15 · raw

@bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.zeros_ok(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.all_zero(bs) : Bool}

def ew_v source · line 22 · raw

@m:Maybe<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.eth_word(m) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.word_of(m) : Maybe<&2, List<&2, U32>>}

def aw_v source · line 29 · raw

@m:Maybe<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.addr_word(m) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.addr_word(m) : Maybe<&2, List<&2, U32>>}

def ecv source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+rs:List<&2, U32> -> @+v:U32 -> @ok:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.ecrecover_v(h, rs, v, ok) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.ecrecover_v(one, h, rs, v, ok) : Maybe<&2, List<&2, U32>>}

def ecin source · line 45 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.ecrecover_in(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.ecrecover_in(one, x) : Maybe<&2, List<&2, U32>>}

def ecrecover_v source · line 67 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+input:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.ecrecover(input) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.ecrecover(one, input) : Maybe<&2, List<&2, U32>>}

the ECRECOVER precompile