proofs/u32_division.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/u32_division.bend as U32_division

Actual Base.U32 long division -> the proven Nat binary division algorithm.

8 imports

import Base
import ./binary_division.bend as BinaryDivision
import ./u32_comparison.bend as Comparison
import ./nat_to_u32_bounds.bend as Bounds
import ./nat_order.bend as Order
import ./bounded_u32_arithmetic.bend as Arithmetic
import ./u32_shift.bend as U32Shift
import ./word_encoding.bend as WordEncoding

Laws

law step provedsource · line 45 · raw

@+p:Nat -> @+bit:Bool -> @+b:U32 -> @+cap:U32 -> @+cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @+divisor_bound:{Nat.is_le(Nat.double(U32.to_nat(b)), U32.to_nat(cap)) == True{} : Bool} -> @pair:Pair(Word(p), U32) -> @small:{Nat.is_lt(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.remainder(decode(p, pair)), U32.to_nat(b)) == True{} : Bool} -> {decode(1n+p, U32.divmod.go.rec(p, bit, b, pair)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.step(bit, U32.to_nat(b), decode(p, pair)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient}

law go provedsource · line 84 · raw

@+n:Nat -> @+w:Word(n) -> @+b:U32 -> @+cap:U32 -> @+cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @+divisor_bound:{Nat.is_le(Nat.double(U32.to_nat(b)), U32.to_nat(cap)) == True{} : Bool} -> @+positive:{Nat.is_lt(0n, U32.to_nat(b)) == True{} : Bool} -> {decode(n, U32.divmod.go(n, w, b)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.go(n, w, U32.to_nat(b)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient}

Definitions

def decode source · line 11 · raw

@+n:Nat -> @pair:Pair(Word(n), U32) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient

def nat_lt_native source · line 15 · raw

@+a:U32 -> @+b:U32 -> @h:{Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == True{} : Bool} -> {U32.is_lt(a, b) == True{} : Bool}

def nat_le_native source · line 19 · raw

@+a:U32 -> @+b:U32 -> @h:{Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == True{} : Bool} -> {U32.is_le(a, b) == True{} : Bool}

def native_ge_nat source · line 23 · raw

@+a:U32 -> @+b:U32 -> @h:{U32.is_ge(a, b) == True{} : Bool} -> {Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) == True{} : Bool}

def fin source · line 27 · raw

@+p:Nat -> @+q:Word(p) -> @+s:U32 -> @+b:U32 -> @+cap:U32 -> @+g:Bool -> @cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @bound:{Nat.is_le(U32.to_nat(s), U32.to_nat(cap)) == True{} : Bool} -> @guard:{U32.is_ge(s, b) == g : Bool} -> {decode(1n+p, U32.divmod.go.fin(p, q, s, b, g)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.branch(g, Nat.double(Word.to_nat(p, q)), U32.to_nat(s), U32.to_nat(b)) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient}

def shifted_bound source · line 40 · raw

@+s:U32 -> @+value:Nat -> @+cap:U32 -> @e:{U32.to_nat(s) == value : Nat} -> @h:{Nat.is_le(value, U32.to_nat(cap)) == True{} : Bool} -> {Nat.is_le(U32.to_nat(s), U32.to_nat(cap)) == True{} : Bool}

def transfer_bound source · line 79 · raw

@+prev:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient -> @+next:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient -> @+b:Nat -> @e:{prev == next : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient} -> @h:{Nat.is_lt(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.remainder(next), b) == True{} : Bool} -> {Nat.is_lt(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.remainder(prev), b) == True{} : Bool}

def quotient source · line 106 · raw

@result:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient -> Nat

def quotient_decode source · line 110 · raw

@pair:Pair(Word(32n), U32) -> {U32.to_nat(U32.div.fin(pair)) == quotient(decode(32n, pair)) : Nat}

def remainder_decode source · line 114 · raw

@pair:Pair(Word(32n), U32) -> {U32.to_nat(U32.mod.fin(pair)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.remainder(decode(32n, pair)) : Nat}

def quotient_pair source · line 118 · raw

@+result:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient -> {Pair.fst(Nat, Nat, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.pair(result)) == quotient(result) : Nat}

def remainder_pair source · line 122 · raw

@+result:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.Quotient -> {Pair.snd(Nat, Nat, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.pair(result)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.remainder(result) : Nat}

def natural_quotient source · line 126 · raw

@+w:Word(32n) -> @+b:Nat -> @+positive:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.div(Word.to_nat(32n, w), b) == quotient(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.go(32n, w, b)) : Nat}

def natural_remainder source · line 132 · raw

@+w:Word(32n) -> @+b:Nat -> @+positive:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.mod(Word.to_nat(32n, w), b) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.remainder(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.go(32n, w, b)) : Nat}

def nat_nonzero source · line 138 · raw

@+b:Nat -> @h:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.is_eq(b, 0n) == False{} : Bool}

def nonzero source · line 145 · raw

@+b:U32 -> @h:{Nat.is_lt(0n, U32.to_nat(b)) == True{} : Bool} -> {U32.is_zero(b) == False{} : Bool}

def divide source · line 149 · raw

@+a:U32 -> @+b:U32 -> @+cap:U32 -> @+cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @+divisor_bound:{Nat.is_le(Nat.double(U32.to_nat(b)), U32.to_nat(cap)) == True{} : Bool} -> @+positive:{Nat.is_lt(0n, U32.to_nat(b)) == True{} : Bool} -> {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}

def modulo source · line 161 · raw

@+a:U32 -> @+b:U32 -> @+cap:U32 -> @+cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @+divisor_bound:{Nat.is_le(Nat.double(U32.to_nat(b)), U32.to_nat(cap)) == True{} : Bool} -> @+positive:{Nat.is_lt(0n, U32.to_nat(b)) == True{} : Bool} -> {U32.to_nat(U32.mod(a, b)) == Nat.mod(U32.to_nat(a), U32.to_nat(b)) : Nat}