~/bend-docscommunity

proofs/crypto/secp256k1/peth.bend checks

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

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/peth.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 ../keccak/laws.bend as KL
import ../keccak/proof.bend as KPF
import ./blist.bend as BL

Definitions

def words_v source · line 17 · raw

@n:Nat -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.words(n, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.words(n, bs) : List<&2, U32>}

def pack_v source · line 33 · raw

@ws:List<&2, U32> -> @+i:U32 -> @a:Array<U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.pack(ws, i, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.pack(ws, i, a) : Array<U32>}

def unpack_v source · line 40 · raw

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

def digest_v source · line 47 · raw

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

def k64_v source · line 54 · raw

@+h1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Hash -> @+h2:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Hash -> @e:(@a:Array<U32> -> @l:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.hash(h1, a, l) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.hash(h2, a, l) : Maybe<&1, Array<U32>>}) -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.keccak64(h1, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.keccak64(h2, bs) : List<&2, U32>}

def eth_if_v source · line 60 · raw

@b:Bool -> @+dg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.eth_if(b, dg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.eth_if(b, dg) : Maybe<&2, List<&2, U32>>}

def ew_is source · line 67 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Hash -> @pk:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.eth_with(h, pk) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.eth_go(h, pk) : Maybe<&2, List<&2, U32>>}

def sw_is source · line 74 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Hash -> @pk:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.eth_with(h, pk) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.eth_go(h, pk) : Maybe<&2, List<&2, U32>>}

def eth_with_v source · line 81 · raw

@+h1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Hash -> @+h2:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Hash -> @e:(@a:Array<U32> -> @l:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.hash(h1, a, l) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.hash(h2, a, l) : Maybe<&1, Array<U32>>}) -> @+pk:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.eth_with(h1, pk) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.eth_with(h2, pk) : Maybe<&2, List<&2, U32>>}

def kk source · line 91 · raw

@a:Array<U32> -> @+l:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.hash(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Keccak256{}, a, l) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.hash(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Keccak256{}, a, l) : Maybe<&1, Array<U32>>}

the Keccak-256 implementation is its specification

def eth_address_v source · line 94 · raw

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