1	import Base
2	import ./word_comparison.bend as Comparison
3	import ../src/wide.bend as W
4	import ../spec/numeric.bend as S
5	import ./word_multiplication.bend as Mul
6	import ./word_shift.bend as Shift
7	import ./numeric.bend as N
8	
9	def times_two(a: Nat) -> {Nat.mul(a, 2n) == Nat.double(a) : Nat}:
10	  match a:
11	    case 0n: {==}
12	    case 1n+ +p:
13	      Equal.cong(Nat, Nat, x => 2n+x, Nat.mul(p, 2n), Nat.double(p), times_two(p))
14	
15	# The actual U32 multiplication in wide.digit computes low bits of 2*r.
16	def doubling(+r: U32) -> {U32.mul(r, 2) == U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))} : U32}:
17	  Equal.trans(U32, U32.mul(r, 2), U32{S.from_nat(32n, Nat.mul(U32.to_nat(r), 2n))}, U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))}, Mul.u32_refines(r, 2), Equal.cong(Nat, U32, x => U32{S.from_nat(32n, x)}, Nat.mul(U32.to_nat(r), 2n), Nat.double(U32.to_nat(r)), times_two(U32.to_nat(r))))
18	
19	def shift_value(r: U32) -> {U32.shl(r) == U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))} : U32}:
20	  U32{+bits} = r
21	  %Equal.sym(Nat, Word.to_nat(32n, bits), S.unsigned(32n, bits), N.primitive_word_interpretation(32n, bits)) : {U32.shl(U32{bits}) == U32{S.from_nat(32n, Nat.double(_))} : U32}
22	  Equal.cong(Word(32n), U32, w => U32{w}, Word.shl(32n, bits), S.from_nat(32n, Nat.double(S.unsigned(32n, bits))), Shift.refines(32n, bits))
23	
24	def multiplication_is_shift(+r: U32) -> {U32.mul(r, 2) == U32.shl(r) : U32}:
25	  Equal.trans(U32, U32.mul(r, 2), U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))}, U32.shl(r), doubling(r), Equal.sym(U32, U32.shl(r), U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))}, shift_value(r)))
26	
27	# Link directly to the recurrence used by actual div_million. This equation is
28	# still modular; the reachable remainder range must be discharged separately.
29	def digit(+p: Nat, +bit: Bool, +q: Word(p), +r: U32) -> {W.digit(p, bit, W.Div{q, r}) == W.digit_compare(p, q, U32.add(U32.shl(r), W.bit_u32(bit))) : W.Division<1n+p>}:
30	  Equal.cong(U32, W.Division<1n+p>, x => W.digit_compare(p, q, U32.add(x, W.bit_u32(bit))), U32.mul(r, 2), U32.shl(r), multiplication_is_shift(r))