~/bend-docscommunity

proofs/crypto/secp256k1/semiring.bend checks

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

4 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW

Definitions

def zero_add source · line 9 · raw

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

def zero_mul source · line 12 · raw

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

def one_mul source · line 15 · raw

@+x:Nat -> {Nat.mul(1n, x) == x : Nat}

def shift0 source · line 18 · raw

@+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(0n, x) == x : Nat}

def mul_swap source · line 21 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}

def shift_shift source · line 27 · raw

@+j:Nat -> @+k:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(j, k), x) : Nat}

def succ_add source · line 30 · raw

@+k:Nat -> @+x:Nat -> {Nat.add(k, x) == Nat.add(x, k) : Nat}