1	# Actual Base.U32 long division -> the proven Nat binary division algorithm.
2	import Base
3	import ./binary_division.bend as BinaryDivision
4	import ./u32_comparison.bend as Comparison
5	import ./nat_to_u32_bounds.bend as Bounds
6	import ./nat_order.bend as Order
7	import ./nat_division.bend as Division
8	import ./bounded_u32_arithmetic.bend as Arithmetic
9	import ./u32_shift.bend as U32Shift
10	import ./word_encoding.bend as WordEncoding
11	
12	def decode(+n: Nat,pair: Word(n) & U32) -> BinaryDivision.Quotient:
13	  (q,r) = pair
14	  BinaryDivision.Quotient{Word.to_nat(n,q),U32.to_nat(r)}
15	
16	def nat_lt_native(+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}:
17	  %Equal.sym(Bool,U32.is_lt(a,b),Nat.is_lt(U32.to_nat(a),U32.to_nat(b)),Comparison.lt(a,b)) : {_ == True{} : Bool}
18	  h
19	
20	def nat_le_native(+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}:
21	  %Equal.sym(Bool,U32.is_le(a,b),Nat.is_le(U32.to_nat(a),U32.to_nat(b)),Comparison.le(a,b)) : {_ == True{} : Bool}
22	  h
23	
24	def native_ge_nat(+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}:
25	  %Comparison.ge(a,b) : {_ == True{} : Bool}
26	  h
27	
28	def fin(+p: Nat,+q: Word(p),+s: U32,+b: U32,+cap: U32,+g: Bool,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},
29	  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,
30	      s,b,g)) == BinaryDivision.branch(g,Nat.double(Word.to_nat(p,q)),U32.to_nat(s),U32.to_nat(b)) : BinaryDivision.Quotient}:
31	  match g:
32	    case False{}:
33	      {==}
34	    case True{}:
35	      %Arithmetic.subtract(s,b,cap,cap_ok,Order.ge_true(U32.to_nat(s),U32.to_nat(b),native_ge_nat(s,b,guard)),
36	        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)),
37	          bound)) : {BinaryDivision.Quotient{1n+Nat.double(Word.to_nat(p,q)),U32.to_nat(U32.sub(s,
38	              b))} == BinaryDivision.Quotient{1n+Nat.double(Word.to_nat(p,q)),_} : BinaryDivision.Quotient}
39	      {==}
40	
41	def shifted_bound(+s: U32,+value: Nat,+cap: U32,e: {U32.to_nat(s) == value : Nat},h: {Nat.is_le(value,
42	      U32.to_nat(cap)) == True{} : Bool}) -> {Nat.is_le(U32.to_nat(s),U32.to_nat(cap)) == True{} : Bool}:
43	  %Equal.sym(Nat,U32.to_nat(s),value,e) : {Nat.is_le(_,U32.to_nat(cap)) == True{} : Bool}
44	  h
45	
46	law step:
47	  for +p: Nat
48	  for +bit: Bool
49	  for +b: U32
50	  for +cap: U32
51	  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
52	  for +divisor_bound: {Nat.is_le(Nat.double(U32.to_nat(b)),U32.to_nat(cap)) == True{} : Bool}
53	  for pair: Word(p) & U32
54	  for small: {Nat.is_lt(BinaryDivision.remainder(decode(p,pair)),U32.to_nat(b)) == True{} : Bool}
55	  {decode(1n+p,U32.divmod.go.rec(p,bit,b,pair)) == BinaryDivision.step(bit,U32.to_nat(b),decode(p,pair)) : BinaryDivision.Quotient}
56	def step(p,bit,b,cap,cap_ok,divisor_bound,pair,small):
57	  (+q,r) = pair
58	  U32{+rw} = r
59	  +small = small
60	  +s = {U32{Word.shl.put(32n,bit,rw)} : U32}
61	  +value = Comparison.digit(bit,Word.to_nat(32n,rw))
62	  +bound = Order.digit_bounded(Word.to_nat(32n,rw),U32.to_nat(b),bit,U32.to_nat(cap),small,divisor_bound)
63	  +numeric = U32Shift.bounded_put(bit,rw,cap,cap_ok,bound)
64	  +bcap = nat_le_native(b,cap,Order.transitive(U32.to_nat(b),Nat.double(U32.to_nat(b)),U32.to_nat(cap),Order.le_double(U32.to_nat(b)),
65	      divisor_bound))
66	  +rcap = Bounds.uint_trans(U32{rw},b,cap,nat_lt_native(U32{rw},b,small),bcap)
67	  %Equal.sym(Bool & Word(32n),Word.shl.out(32n,bit,rw),(False{},Word.shl.put(32n,bit,rw)),U32Shift.no_carry(rw,
68	      bit)(Bounds.uint_trans(U32{rw},cap,2147483648,rcap,cap_ok))) : {decode(1n+p,U32.divmod.go.shl(p,q,b,_)) == BinaryDivision.step(bit,
69	      U32.to_nat(b),BinaryDivision.Quotient{Word.to_nat(p,q),Word.to_nat(32n,rw)}) : BinaryDivision.Quotient}
70	  %Equal.sym(BinaryDivision.Quotient,decode(1n+p,U32.divmod.go.fin(p,q,s,b,U32.is_ge(s,b))),BinaryDivision.branch(U32.is_ge(s,b),
71	      Nat.double(Word.to_nat(p,q)),U32.to_nat(s),U32.to_nat(b)),fin(p,q,s,b,cap,U32.is_ge(s,b),cap_ok,shifted_bound(s,value,cap,numeric,bound),
72	      {==})) : {_ == BinaryDivision.step(bit,U32.to_nat(b),BinaryDivision.Quotient{Word.to_nat(p,q),Word.to_nat(32n,rw)}) : BinaryDivision.Quotient}
73	  %Equal.sym(Bool,U32.is_ge(s,b),Nat.is_ge(U32.to_nat(s),U32.to_nat(b)),Comparison.ge(s,b)) : {BinaryDivision.branch(_,
74	      Nat.double(Word.to_nat(p,q)),U32.to_nat(s),U32.to_nat(b)) == BinaryDivision.step(bit,U32.to_nat(b),BinaryDivision.Quotient{Word.to_nat(p,q),
75	        Word.to_nat(32n,rw)}) : BinaryDivision.Quotient}
76	  %Equal.sym(Nat,U32.to_nat(s),value,numeric) : {BinaryDivision.branch(Nat.is_ge(_,U32.to_nat(b)),Nat.double(Word.to_nat(p,q)),_,
77	      U32.to_nat(b)) == BinaryDivision.step(bit,U32.to_nat(b),BinaryDivision.Quotient{Word.to_nat(p,q),Word.to_nat(32n,rw)}) : BinaryDivision.Quotient}
78	  {==}
79	
80	def transfer_bound(+prev: BinaryDivision.Quotient,+next: BinaryDivision.Quotient,+b: Nat,e: {prev == next : BinaryDivision.Quotient},
81	  h: {Nat.is_lt(BinaryDivision.remainder(next),b) == True{} : Bool}) -> {Nat.is_lt(BinaryDivision.remainder(prev),b) == True{} : Bool}:
82	  %Equal.sym(BinaryDivision.Quotient,prev,next,e) : {Nat.is_lt(BinaryDivision.remainder(_),b) == True{} : Bool}
83	  h
84	
85	law go:
86	  for +n: Nat
87	  for +w: Word(n)
88	  for +b: U32
89	  for +cap: U32
90	  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
91	  for +divisor_bound: {Nat.is_le(Nat.double(U32.to_nat(b)),U32.to_nat(cap)) == True{} : Bool}
92	  for +positive: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}
93	  {decode(n,U32.divmod.go(n,w,b)) == BinaryDivision.go(n,w,U32.to_nat(b)) : BinaryDivision.Quotient}
94	def go(n,w,b,cap,cap_ok,divisor_bound,positive):
95	  match n:
96	    case 0n:
97	      WNil{} = w
98	      {==}
99	    case 1n+ +p:
100	      WCon{+bit,+tail} = w
101	      +previous = go(p,tail,b,cap,cap_ok,divisor_bound,positive)
102	      %previous : {decode(1n+p,U32.divmod.go.rec(p,bit,b,U32.divmod.go(p,tail,b))) == BinaryDivision.step(bit,U32.to_nat(b),
103	          _) : BinaryDivision.Quotient}
104	      step(p,bit,b,cap,cap_ok,divisor_bound,U32.divmod.go(p,tail,b),transfer_bound(decode(p,U32.divmod.go(p,tail,b)),BinaryDivision.go(p,tail,
105	            U32.to_nat(b)),U32.to_nat(b),previous,BinaryDivision.go_bound(p,tail,U32.to_nat(b),positive)))
106	
107	def quotient(result: BinaryDivision.Quotient) -> Nat:
108	  BinaryDivision.Quotient{q,r} = result
109	  q
110	
111	def quotient_decode(pair: Word(32n) & U32) -> {U32.to_nat(U32.div.fin(pair)) == quotient(decode(32n,pair)) : Nat}:
112	  (q,r) = pair
113	  {==}
114	
115	def remainder_decode(pair: Word(32n) & U32) -> {U32.to_nat(U32.mod.fin(pair)) == BinaryDivision.remainder(decode(32n,pair)) : Nat}:
116	  (q,r) = pair
117	  {==}
118	
119	def quotient_pair(+result: BinaryDivision.Quotient) -> {Pair.fst(Nat,Nat,BinaryDivision.pair(result)) == quotient(result) : Nat}:
120	  BinaryDivision.Quotient{q,r} = result
121	  {==}
122	
123	def remainder_pair(+result: BinaryDivision.Quotient) -> {Pair.snd(Nat,Nat,BinaryDivision.pair(result)) == BinaryDivision.remainder(result) : Nat}:
124	  BinaryDivision.Quotient{q,r} = result
125	  {==}
126	
127	def natural_quotient(+w: Word(32n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.div(Word.to_nat(32n,w),
128	    b) == quotient(BinaryDivision.go(32n,w,b)) : Nat}:
129	  %Equal.sym(Nat & Nat,Nat.divmod(Word.to_nat(32n,w),b),BinaryDivision.pair(BinaryDivision.go(32n,w,b)),BinaryDivision.natural(32n,w,b,
130	      positive)) : {Pair.fst(Nat,Nat,_) == quotient(BinaryDivision.go(32n,w,b)) : Nat}
131	  quotient_pair(BinaryDivision.go(32n,w,b))
132	
133	def natural_remainder(+w: Word(32n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.mod(Word.to_nat(32n,w),
134	    b) == BinaryDivision.remainder(BinaryDivision.go(32n,w,b)) : Nat}:
135	  %Equal.sym(Nat & Nat,Nat.divmod(Word.to_nat(32n,w),b),BinaryDivision.pair(BinaryDivision.go(32n,w,b)),BinaryDivision.natural(32n,w,b,
136	      positive)) : {Pair.snd(Nat,Nat,_) == BinaryDivision.remainder(BinaryDivision.go(32n,w,b)) : Nat}
137	  remainder_pair(BinaryDivision.go(32n,w,b))
138	
139	def nat_nonzero(+b: Nat,h: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.is_eq(b,0n) == False{} : Bool}:
140	  match b:
141	    case 0n:
142	      Empty.absurd({Nat.is_eq(0n,0n) == False{} : Bool},WordEncoding.false_true(h))
143	    case 1n+p:
144	      {==}
145	
146	def nonzero(+b: U32,h: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}) -> {U32.is_zero(b) == False{} : Bool}:
147	  %Equal.sym(Bool,U32.is_eq(b,0),Nat.is_eq(U32.to_nat(b),U32.to_nat(0)),Comparison.eq(b,0)) : {_ == False{} : Bool}
148	  nat_nonzero(U32.to_nat(b),h)
149	
150	def 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)),
151	      U32.to_nat(cap)) == True{} : Bool},+positive: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}) -> {U32.to_nat(U32.div(a,
152	      b)) == Nat.div(U32.to_nat(a),U32.to_nat(b)) : Nat}:
153	  U32{+w} = a
154	  U32{+bw} = b
155	  +b = {U32{bw} : U32}
156	  %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}
157	  %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),
158	      positive)) : {U32.to_nat(U32.div.fin(U32.divmod.go(32n,w,b))) == _ : Nat}
159	  %go(32n,w,b,cap,cap_ok,divisor_bound,positive) : {U32.to_nat(U32.div.fin(U32.divmod.go(32n,w,b))) == quotient(_) : Nat}
160	  quotient_decode(U32.divmod.go(32n,w,b))
161	
162	def modulo(+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)),
163	      U32.to_nat(cap)) == True{} : Bool},+positive: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}) -> {U32.to_nat(U32.mod(a,
164	      b)) == Nat.mod(U32.to_nat(a),U32.to_nat(b)) : Nat}:
165	  U32{+w} = a
166	  U32{+bw} = b
167	  +b = {U32{bw} : U32}
168	  %Equal.sym(Bool,U32.is_zero(b),False{},nonzero(b,positive)) : {U32.to_nat(U32.mod.if(w,b,_)) == Nat.mod(Word.to_nat(32n,w),U32.to_nat(b)) : Nat}
169	  %Equal.sym(Nat,Nat.mod(Word.to_nat(32n,w),U32.to_nat(b)),BinaryDivision.remainder(BinaryDivision.go(32n,w,U32.to_nat(b))),natural_remainder(w,
170	      U32.to_nat(b),positive)) : {U32.to_nat(U32.mod.fin(U32.divmod.go(32n,w,b))) == _ : Nat}
171	  %go(32n,w,b,cap,cap_ok,divisor_bound,positive) : {U32.to_nat(U32.mod.fin(U32.divmod.go(32n,w,b))) == BinaryDivision.remainder(_) : Nat}
172	  remainder_decode(U32.divmod.go(32n,w,b))
173	
174	def divided_by_one(+value: U32) -> {U32.to_nat((value / 1 : U32)) == U32.to_nat(value) : Nat}:
175	  Equal.trans(Nat,U32.to_nat((value / 1 : U32)),Nat.div(U32.to_nat(value),1n),U32.to_nat(value),divide(value,1,2,{==},{==},{==}),
176	    %Order.times_one(U32.to_nat(value)) : {Nat.div(_,1n) == U32.to_nat(value) : Nat}
177	    Division.exact_quotient(U32.to_nat(value),1n,{==}))