~/bend-docscommunity

proofs/crypto/secp256k1/u32and.bend checks

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

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

7 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/logic.bend as L
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/u32.bend as U
import ../../lib/word.bend as WD
import ../../math/typed/width.bend as WW

Definitions

def v source · line 14 · raw

@+x:U32 -> Nat

def sb source · line 19 · raw

@+k:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.scale_binary(k, x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x) : Nat}

def andw source · line 27 · raw

@+n:Nat -> @+k:Nat -> @+w:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.and(n, w, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(n, k))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.unsigned(n, w)) : Nat}

the low k bits of a word

def andm0 source · line 36 · raw

@+x:U32 -> @+k:Nat -> {v(U32.and(x, U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)})) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, v(x)) : Nat}

def andm source · line 43 · raw

@+x:U32 -> @+k:Nat -> @+c:U32 -> @+hc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)} : U32} -> {v(U32.and(x, c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, v(x)) : Nat}

x and c for a mask constant c = 2^k - 1