~/bend-docscommunity

proofs/lib/lemmas/proofs/division_shift.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift

6 imports
import Base
import ../src/wide.bend as W
import ../spec/numeric.bend as S
import ./word_shift.bend as Shift
import ./addition_bounds.bend as Bounds
import ./division_candidate.bend as Candidate

Definitions

def add_zero source · line 9 · raw

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

Adding the incoming bit to an even shifted word changes only its low bit.

def bit_word source · line 21 · raw

@n:Nat -> @bit:Bool -> Word(n)

def add_bit source · line 26 · raw

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

def primitive_bit source · line 36 · raw

@bit:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/wide.bit_u32(bit) == U32{bit_word(32n, bit)} : U32}

def shifted source · line 41 · raw

@r:U32 -> @bit:Bool -> U32

def actual_candidate source · line 46 · raw

@+r:U32 -> @+bit:Bool -> {U32.add(U32.mul(r, 2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/wide.bit_u32(bit)) == shifted(r, bit) : U32}

This is the exact candidate expression executed in wide.digit.

def exact source · line 54 · raw

@+n:Nat -> @+w:Word(n) -> @+bit:Bool -> @bound:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.unsigned(n, w))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.scale_binary(n, 1n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.shl.put(n, bit, w)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.unsigned(n, w))) : Nat}

The range premise concerns the inputs and discharges discarded carry.