~/bend-docscommunity

proofs/lib/lemmas/proofs/division_value.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend as Division_value

11 imports
import Base
import ../src/wide.bend as W
import ../spec/numeric.bend as S
import ./division_remainder.bend as Rem
import ./division_no_overflow.bend as Overflow
import ./division_invariant.bend as Inv
import ./division_candidate_bound.bend as Bound
import ./natural_products.bend as P
import ./string_compare.bend as Natural
import ./numeric.bend as Numeric
import ./map_index.bend as Index

Definitions

def value source · line 14 · raw

@+n:Nat -> @result:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.Division<n> -> @d:U32 -> Nat

A mathematical observation of the actual returned quotient and remainder.

def selected source · line 18 · raw

@+r:U32 -> @d:U32 -> @flag:Bool -> U32

def selection_value source · line 23 · raw

@+r:U32 -> @+d:U32 -> @flag:Bool -> @chosen:{U32.is_ge(r, d) == flag : Bool} -> {U32.to_nat(r) == Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(flag), U32.to_nat(d)), U32.to_nat(selected(r, d, flag))) : Nat}

def result_form source · line 31 · raw

@+p:Nat -> @+q:Word(p) -> @+r:U32 -> @+d:U32 -> @flag:Bool -> @same:{d == 1000000 : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.digit_result(p, q, r, flag) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.Div{WCon{flag, q}, selected(r, d, flag)} : 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.Division<1n+p>}

Normal form of the actual helper; the denominator identity is explicit.

def weight_step source · line 37 · raw

@+q:Nat -> @+d:Nat -> @+r:Nat -> @flag:Bool -> {Nat.add(Nat.mul(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(flag), Nat.double(q)), d), r) == Nat.add(Nat.mul(Nat.double(q), d), Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(flag), d), r)) : Nat}

def result_value source · line 44 · raw

@+p:Nat -> @+q:Word(p) -> @+r:U32 -> @+d:U32 -> @+flag:Bool -> @+same:{d == 1000000 : U32} -> @chosen:{U32.is_ge(r, 1000000) == flag : Bool} -> {value(1n+p, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.digit_result(p, q, r, flag), d) == Nat.add(Nat.mul(Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(p, q)), U32.to_nat(d)), U32.to_nat(r)) : Nat}

def gather source · line 48 · raw

@+q:Nat -> @+r:Nat -> @bit:Bool -> {Nat.add(Nat.double(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(r))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(Nat.add(q, r))) : Nat}

def digit source · line 55 · raw

@+p:Nat -> @+bit:Bool -> @prior:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.Division<p> -> @+d:U32 -> @same:{d == 1000000 : U32} -> @bound:{U32.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/division_invariant.remainder(p, prior), 1000000) == True{} : Bool} -> {value(1n+p, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.digit(p, bit, prior), d) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(value(p, prior, d))) : Nat}

def conservation source · line 62 · raw

@+n:Nat -> @word:Word(n) -> @+d:U32 -> @+same:{d == 1000000 : U32} -> {value(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.div_million(n, word), d) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word) : Nat}

The denominator is a symbolic U32 identified with the actual fixed divisor; the proof observes the actual execution and discharges each recursive bound.

def actual source · line 71 · raw

@+n:Nat -> @word:Word(n) -> {value(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.div_million(n, word), 1000000) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word) : Nat}

Public native divisor identity is discharged here, with no external premise.