~/bend-docscommunity

proofs/word_arithmetic.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as Word_arithmetic

Modular arithmetic identities used before applying bounded Nat conversion.

3 imports
import Base
import ./natural_addition.bend as Addition
import ./u32_successor.bend as U32Successor

Laws

law carry provedsource · line 6 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.adc(n, a, b, False{}, True{}) == Word.inc(n, Word.add(n, a, b)) : Word(n)}

law inc_left provedsource · line 28 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.add(n, Word.inc(n, a), b) == Word.inc(n, Word.add(n, a, b)) : Word(n)}

law encode_add provedsource · line 60 · raw

@+a:Nat -> @+b:Nat -> @+width:Nat -> {Word.add(width, encode(a, width), encode(b, width)) == encode(Nat.add(a, b), width) : Word(width)}

law double_carry provedsource · line 77 · raw

@+n:Nat -> @+w:Word(n) -> @+c:Bool -> {Word.adc(n, w, w, False{}, c) == Word.shl.put(n, c, w) : Word(n)}

law native_encoding provedsource · line 118 · raw

@+a:Nat -> {U32.from_nat(a) == U32{encode(a, 32n)} : U32}

Definitions

def encode source · line 53 · raw

@a:Nat -> @+width:Nat -> Word(width)

def shift_put source · line 101 · raw

@+n:Nat -> @+w:Word(n) -> {Word.shl(n, w) == Word.shl.put(n, False{}, w) : Word(n)}

def double_word source · line 109 · raw

@+n:Nat -> @+w:Word(n) -> {Word.add(n, w, w) == Word.shl(n, w) : Word(n)}

def encode_double source · line 113 · raw

@+a:Nat -> @+width:Nat -> {encode(Nat.double(a), width) == Word.shl(width, encode(a, width)) : Word(width)}

def native_add source · line 129 · raw

@+a:Nat -> @+b:Nat -> {U32.add(U32.from_nat(a), U32.from_nat(b)) == U32.from_nat(Nat.add(a, b)) : U32}