1	import Base
2	import ../src/wide.bend as W
3	import ./division_candidate_bound.bend as Candidate
4	import ./division_remainder.bend as Remainder
5	import ./map_routing.bend as Logic
6	
7	def remainder(-n: Nat, result: W.Division<n>) -> U32:
8	  W.Div{q, r} = result
9	  r
10	
11	def not_ge(c: Cmp, e: {Cmp.is_ge(c) == False{} : Bool}) -> {Cmp.is_lt(c) == True{} : Bool}:
12	  match c:
13	    case LT{}: {==}
14	    case EQ{}: Empty.absurd({False{} == True{} : Bool}, Logic.false_true(Equal.sym(Bool, True{}, False{}, e)))
15	    case GT{}: Empty.absurd({False{} == True{} : Bool}, Logic.false_true(Equal.sym(Bool, True{}, False{}, e)))
16	
17	# Both branches refer to actual wide.digit_result, not a proof-side divider.
18	def result(+p: Nat, q: Word(p), +r: U32, flag: Bool, chosen: {U32.is_ge(r, 1000000) == flag : Bool}, bound: {U32.is_lt(r, 2000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit_result(p, q, r, flag)), 1000000) == True{} : Bool}:
19	  match flag:
20	    case False{}:
21	      not_ge(U32.cmp(r, 1000000), chosen)
22	    case True{}:
23	      Remainder.million(r, chosen, bound)
24	
25	def compare(+p: Nat, +q: Word(p), +r: U32, bound: {U32.is_lt(r, 2000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit_compare(p, q, r)), 1000000) == True{} : Bool}:
26	  result(p, q, r, U32.is_ge(r, 1000000), {==}, bound)
27	
28	def digit(+p: Nat, +bit: Bool, prior: W.Division<p>, bound: {U32.is_lt(remainder(p, prior), 1000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit(p, bit, prior)), 1000000) == True{} : Bool}:
29	  match prior:
30	    case W.Div{q, +r}:
31	      compare(p, q, U32.add(U32.mul(r, 2), W.bit_u32(bit)), Candidate.million(r, bit, bound))
32	
33	# Every recursively reached remainder of the executed divider is strictly below
34	# the divisor, for arbitrary widths and inputs. No reachable-range premise.
35	def bounded(+n: Nat, word: Word(n)) -> {U32.is_lt(remainder(n, W.div_million(n, word)), 1000000) == True{} : Bool}:
36	  match n:
37	    case 0n: {==}
38	    case 1n+ +p:
39	      match word:
40	        case WCon{+bit, +tail}:
41	          digit(p, bit, W.div_million(p, tail), bounded(p, tail))