~/bend-docscommunity

proofs/binary_division.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/binary_division.bend as Binary_division

Natural-number binary long division, proved against the frozen Base.divmod.

9 imports
import Base
import ./natural_addition.bend as Addition
import ./binary_digit.bend as BinaryDigit
import ./u32_comparison.bend as Comparison
import ./nat_order.bend as Order
import ./nat_division.bend as Division
import ./word_multiplication.bend as Multiplication
import ./word_subtraction.bend as Subtraction
import ./word_encoding.bend as WordEncoding

Laws

law go_total provedsource · line 115 · raw

@+n:Nat -> @+w:Word(n) -> @+b:Nat -> {total(go(n, w, b), b) == Word.to_nat(n, w) : Nat}

law go_bound provedsource · line 131 · raw

@+n:Nat -> @+w:Word(n) -> @+b:Nat -> @positive:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.is_lt(remainder(go(n, w, b)), b) == True{} : Bool}

Types

type Quotient source · line 12 · raw

Data

Definitions

def total source · line 15 · raw

@result:Quotient -> @b:Nat -> Nat

def remainder source · line 19 · raw

@result:Quotient -> Nat

def pair source · line 23 · raw

@result:Quotient -> Pair(Nat, Nat)

def branch source · line 27 · raw

@g:Bool -> @+q:Nat -> @s:Nat -> @b:Nat -> Quotient

def step source · line 34 · raw

@bit:Bool -> @+b:Nat -> @prev:Quotient -> Quotient

def go source · line 39 · raw

@n:Nat -> @w:Word(n) -> @+b:Nat -> Quotient

def rotate source · line 47 · raw

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

def product_right source · line 51 · raw

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

def product_double source · line 61 · raw

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

def even_total source · line 65 · raw

@+q:Nat -> @+r:Nat -> @+b:Nat -> {Nat.add(Nat.mul(Nat.double(q), b), Nat.double(r)) == Nat.double(Nat.add(Nat.mul(q, b), r)) : Nat}

def digit_total source · line 70 · raw

@+bit:Bool -> @+q:Nat -> @+r:Nat -> @+b:Nat -> {Nat.add(Nat.mul(Nat.double(q), b), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(bit, r)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(bit, Nat.add(Nat.mul(q, b), r)) : Nat}

def branch_total source · line 81 · raw

@+g:Bool -> @+q:Nat -> @+s:Nat -> @+b:Nat -> @guard:{Nat.is_ge(s, b) == g : Bool} -> {total(branch(g, q, s, b), b) == Nat.add(Nat.mul(q, b), s) : Nat}

def step_total source · line 91 · raw

@+bit:Bool -> @+b:Nat -> @+prev:Quotient -> {total(step(bit, b, prev), b) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(bit, total(prev, b)) : Nat}

def sum_bound source · line 98 · raw

@+s:Nat -> @+b:Nat -> @h:{Nat.is_lt(s, Nat.double(b)) == True{} : Bool} -> {Nat.is_lt(s, Nat.add(b, b)) == True{} : Bool}

def branch_bound source · line 102 · raw

@+g:Bool -> @+q:Nat -> @+s:Nat -> @+b:Nat -> @guard:{Nat.is_ge(s, b) == g : Bool} -> @bound:{Nat.is_lt(s, Nat.double(b)) == True{} : Bool} -> {Nat.is_lt(remainder(branch(g, q, s, b)), b) == True{} : Bool}

def step_bound source · line 110 · raw

@+bit:Bool -> @+b:Nat -> @+prev:Quotient -> @h:{Nat.is_lt(remainder(prev), b) == True{} : Bool} -> {Nat.is_lt(remainder(step(bit, b, prev)), b) == True{} : Bool}

def finish source · line 145 · raw

@+a:Nat -> @+b:Nat -> @+result:Quotient -> @e:{total(result, b) == a : Nat} -> @positive:{Nat.is_lt(0n, b) == True{} : Bool} -> @bounded:{Nat.is_lt(remainder(result), b) == True{} : Bool} -> {Nat.divmod(a, b) == pair(result) : Pair(Nat, Nat)}

def natural source · line 150 · raw

@+n:Nat -> @+w:Word(n) -> @+b:Nat -> @+positive:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.divmod(Word.to_nat(n, w), b) == pair(go(n, w, b)) : Pair(Nat, Nat)}