def fin

stelliferous@0.0.2.0 · proofs/u32_division.bend:27

import Base
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

27def fin(+p: Nat,+q: Word(p),+s: U32,+b: U32,+cap: U32,+g: Bool,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},
28  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,
29      s,b,g)) == BinaryDivision.branch(g,Nat.double(Word.to_nat(p,q)),U32.to_nat(s),U32.to_nat(b)) : BinaryDivision.Quotient}:
30  match g:
31    case False{}:
32      {==}
33    case True{}:
34      %Arithmetic.subtract(s,b,cap,cap_ok,Order.ge_true(U32.to_nat(s),U32.to_nat(b),native_ge_nat(s,b,guard)),
35        Order.transitive(Nat.sub(U32.to_nat(s),U32.to_nat(b)),U32.to_nat(s),U32.to_nat(cap),Order.sub_le(U32.to_nat(s),U32.to_nat(b)),
36          bound)) : {BinaryDivision.Quotient{1n+Nat.double(Word.to_nat(p,q)),U32.to_nat(U32.sub(s,
37              b))} == BinaryDivision.Quotient{1n+Nat.double(Word.to_nat(p,q)),_} : BinaryDivision.Quotient}
38      {==}