proofs/u32_division.bend
stelliferous@0.0.3.0 · 177 lines · 0 definitions
1# Actual Base.U32 long division -> the proven Nat binary division algorithm.
2import Base
3import stelliferous@0.0.3.0/proofs/binary_division.bend as BinaryDivision
4import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
5import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
6import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
7import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
8import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
9import stelliferous@0.0.3.0/proofs/u32_shift.bend as U32Shift
10import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
11
12def 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
16def 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
20def 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
24def 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
28def 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
41def 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
46law 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}
56def 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
80def 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
85law 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}
94def 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
107def quotient(result: BinaryDivision.Quotient) -> Nat:
108 BinaryDivision.Quotient{q,r} = result
109 q
110
111def quotient_decode(pair: Word(32n) & U32) -> {U32.to_nat(U32.div.fin(pair)) == quotient(decode(32n,pair)) : Nat}:
112 (q,r) = pair
113 {==}
114
115def 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
119def quotient_pair(+result: BinaryDivision.Quotient) -> {Pair.fst(Nat,Nat,BinaryDivision.pair(result)) == quotient(result) : Nat}:
120 BinaryDivision.Quotient{q,r} = result
121 {==}
122
123def remainder_pair(+result: BinaryDivision.Quotient) -> {Pair.snd(Nat,Nat,BinaryDivision.pair(result)) == BinaryDivision.remainder(result) : Nat}:
124 BinaryDivision.Quotient{q,r} = result
125 {==}
126
127def 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
133def 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
139def 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
146def 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
150def 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
162def 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
174def 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,{==}))