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