def divide

stelliferous@0.0.2.0 · proofs/u32_division.bend:149

import Base
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision

149def divide(+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)),
150      U32.to_nat(cap)) == True{} : Bool},+positive: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}) -> {U32.to_nat(U32.div(a,
151      b)) == Nat.div(U32.to_nat(a),U32.to_nat(b)) : Nat}:
152  U32{+w} = a
153  U32{+bw} = b
154  +b = {U32{bw} : U32}
155  %Equal.sym(Bool,U32.is_zero(b),False{},nonzero(b,positive)) : {U32.to_nat(U32.div.if(w,b,_)) == Nat.div(Word.to_nat(32n,w),U32.to_nat(b)) : Nat}
156  %Equal.sym(Nat,Nat.div(Word.to_nat(32n,w),U32.to_nat(b)),quotient(BinaryDivision.go(32n,w,U32.to_nat(b))),natural_quotient(w,U32.to_nat(b),
157      positive)) : {U32.to_nat(U32.div.fin(U32.divmod.go(32n,w,b))) == _ : Nat}
158  %go(32n,w,b,cap,cap_ok,divisor_bound,positive) : {U32.to_nat(U32.div.fin(U32.divmod.go(32n,w,b))) == quotient(_) : Nat}
159  quotient_decode(U32.divmod.go(32n,w,b))