proofs/lib/u32div.bend
bend-collections-laws-crypto@1.0.0.0 · 228 lines · 28 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as PR
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as DB
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/natural_division.bend as ND
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as WC
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
14
15
16
17
18
19
20
21
22
23def v(+x: U32) -> Nat:
24 U32.to_nat(x)
25
26def dq(-m: Nat, r: Word(m) & U32) -> Word(m):
27 (q, s) = r
28 q
29
30def dr(-m: Nat, r: Word(m) & U32) -> U32:
31 (q, s) = r
32 s
33
34
35def inv(+m: Nat, +a: Word(m), +bn: Nat, r: Word(m) & U32) -> Type:
36 {Nat.add(Nat.mul(S.unsigned(m, dq(m, r)), bn), v(dr(m, r))) == S.unsigned(m, a) : Nat} & {Nat.is_lt(v(dr(m, r)), bn) == True{} : Bool}
37
38
39
40
41def digit_one(+q: Nat, +bn: Nat, +r: Nat, +a: Nat, +d: Nat, +h: {Nat.add(bn, d) == Nat.add(a, Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(q), bn), d) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}:
42 +x = Nat.double(Nat.mul(q, bn))
43 +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r)))
44 %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(Nat.add(bn, _), d) == rhs : Nat}
45 %Equal.sym(Nat, Nat.add(Nat.add(bn, x), d), Nat.add(Nat.add(bn, d), x), A.add_rot(bn, x, d)) : {_ == rhs : Nat}
46 %N.add_comm(x, Nat.add(bn, d)) : {_ == rhs : Nat}
47 %Equal.sym(Nat, Nat.add(bn, d), Nat.add(a, Nat.double(r)), h) : {Nat.add(x, _) == rhs : Nat}
48 %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat}
49 Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(x, Nat.double(r)), Nat.double(Nat.add(Nat.mul(q, bn), r)), N.add_double(Nat.mul(q, bn), r))
50
51
52def digit_zero(+q: Nat, +bn: Nat, +r: Nat, +a: Nat) -> {Nat.add(Nat.mul(Nat.double(q), bn), Nat.add(a, Nat.double(r))) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}:
53 +x = Nat.double(Nat.mul(q, bn))
54 +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r)))
55 %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(_, Nat.add(a, Nat.double(r))) == rhs : Nat}
56 %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat}
57 Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(x, Nat.double(r)), Nat.double(Nat.add(Nat.mul(q, bn), r)), N.add_double(Nat.mul(q, bn), r))
58
59
60
61def vw(+w: Word(32n)) -> {v(U32{w}) == WD.uw(32n, w) : Nat}:
62 U.to_nat_word(w)
63
64def vb(+one: Nat, +h1: {one == 1n : Nat}, +x: U32) -> {Nat.is_lt(v(x), WD.sc(32n, one)) == True{} : Bool}:
65 match x:
66 case U32{+w}:
67 %Equal.sym(Nat, v(U32{w}), WD.uw(32n, w), vw(w)) : {Nat.is_lt(_, WD.sc(32n, one)) == True{} : Bool}
68 WD.wb(32n, one, h1, w)
69
70def sub32(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +b: U32, +d: Nat, +e: {Nat.add(v(x), WD.sc(32n, one)) == Nat.add(d, v(b)) : Nat}, +hd: {Nat.is_lt(d, WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.sub(x, b)) == d : Nat}:
71 match x b:
72 case U32{+xw} U32{+bw}:
73 +e2 = Equal.trans(Nat, Nat.add(WD.uw(32n, xw), WD.sc(32n, one)), Nat.add(v(U32{xw}), WD.sc(32n, one)), Nat.add(d, WD.uw(32n, bw)),
74 Equal.cong(Nat, Nat, z => Nat.add(z, WD.sc(32n, one)), WD.uw(32n, xw), v(U32{xw}), Equal.sym(Nat, v(U32{xw}), WD.uw(32n, xw), vw(xw))),
75 Equal.trans(Nat, Nat.add(v(U32{xw}), WD.sc(32n, one)), Nat.add(d, v(U32{bw})), Nat.add(d, WD.uw(32n, bw)), e, Equal.cong(Nat, Nat, z => Nat.add(d, z), v(U32{bw}), WD.uw(32n, bw), vw(bw))))
76 %Equal.sym(Nat, v(U32{Word.sub(32n, xw, bw)}), WD.uw(32n, Word.sub(32n, xw, bw)), vw(Word.sub(32n, xw, bw))) : {_ == d : Nat}
77 WD.sub_wrap(32n, one, h1, xw, bw, d, e2, hd)
78
79
80
81def fin_true(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : Nat}, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hts: {Nat.add(v(s), WD.sc(32n, one)) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{})):
82 +bn = v(b)
83 +k = WD.sc(32n, one)
84 +t = Nat.add(S.bit_value(a0), Nat.double(r))
85 +hbk = vb(one, h1, b)
86 +hkt = L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, Nat.add(k, v(s)), t, Equal.trans(Nat, Nat.add(k, v(s)), Nat.add(v(s), k), t, N.add_comm(k, v(s)), hts), N.le_add_right(k, v(s)))
87 +hbt = N.lt_le(bn, t, N.lt_le_trans(bn, k, t, hbk, hkt))
88 +d = Nat.sub(t, bn)
89 +hsum = N.sub_add(t, bn, hbt)
90 +htb = L.subst(Nat, z => {Nat.is_lt(t, z) == True{} : Bool}, Nat.double(bn), Nat.add(bn, bn), NA.double_self(bn), N.double_lt_bit(a0, r, bn, hr))
91 +hdb = N.sub_lt(t, bn, bn, hbt, htb)
92 +hdk = N.lt_trans(d, bn, k, hdb, hbk)
93 +e = Equal.trans(Nat, Nat.add(v(s), k), t, Nat.add(d, bn), hts, Equal.trans(Nat, t, Nat.add(bn, d), Nat.add(d, bn), Equal.sym(Nat, Nat.add(bn, d), t, hsum), N.add_comm(bn, d)))
94 +hsub = sub32(one, h1, s, b, d, e, hdk)
95 +eq = Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), v(U32.sub(s, b))), Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))),
96 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), z), v(U32.sub(s, b)), d, hsub),
97 %he : {Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat}
98 digit_one(S.unsigned(p, q), bn, r, S.bit_value(a0), d, hsum))
99 +lt = L.subst(Nat, z => {Nat.is_lt(z, bn) == True{} : Bool}, d, v(U32.sub(s, b)), Equal.sym(Nat, v(U32.sub(s, b)), d, hsub), hdb)
100 (eq, lt)
101
102def fin_ge(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +hge: {Nat.is_ge(v(s), v(b)) == True{} : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{})):
103 +bn = v(b)
104 +t = Nat.add(S.bit_value(a0), Nat.double(r))
105 +htb = L.subst(Nat, z => {Nat.is_lt(t, z) == True{} : Bool}, Nat.double(bn), Nat.add(bn, bn), NA.double_self(bn), N.double_lt_bit(a0, r, bn, hr))
106 +hle = Equal.trans(Bool, Nat.is_le(bn, v(s)), Nat.is_ge(v(s), bn), True{}, Equal.sym(Bool, Nat.is_ge(v(s), bn), Nat.is_le(bn, v(s)), DB.ge_reverse(v(s), bn)), hge)
107 +d = Nat.sub(v(s), bn)
108 +hsub = U.sub_nat(s, b, hle)
109 +hsum = Equal.trans(Nat, Nat.add(bn, d), v(s), t, N.sub_add(v(s), bn, hle), hs)
110 +hsb = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(bn, bn)) == True{} : Bool}, t, v(s), Equal.sym(Nat, v(s), t, hs), htb)
111 +hdb = N.sub_lt(v(s), bn, bn, hle, hsb)
112 +eq = Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), v(U32.sub(s, b))), Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))),
113 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), z), v(U32.sub(s, b)), d, hsub),
114 %he : {Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat}
115 digit_one(S.unsigned(p, q), bn, r, S.bit_value(a0), d, hsum))
116 +lt = L.subst(Nat, z => {Nat.is_lt(z, bn) == True{} : Bool}, d, v(U32.sub(s, b)), Equal.sym(Nat, v(U32.sub(s, b)), d, hsub), hdb)
117 (eq, lt)
118
119def fin_lt(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +hge: {Nat.is_ge(v(s), v(b)) == False{} : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, False{})):
120 +bn = v(b)
121 +t = Nat.add(S.bit_value(a0), Nat.double(r))
122 +lt = DB.not_ge(v(s), bn, hge)
123 +eq = Equal.trans(Nat, Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), v(s)), Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), t), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))),
124 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), z), v(s), t, hs),
125 %he : {Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), t) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat}
126 digit_zero(S.unsigned(p, q), bn, r, S.bit_value(a0)))
127 (eq, lt)
128
129def fin_false(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +g: Bool, +hg: {U32.is_ge(s, b) == g : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, g)):
130 match g:
131 case True{}:
132 fin_ge(p, q, s, b, a0, hi, r, he, hr, hs, Equal.trans(Bool, Nat.is_ge(v(s), v(b)), U32.is_ge(s, b), True{}, Equal.sym(Bool, U32.is_ge(s, b), Nat.is_ge(v(s), v(b)), WC.u32_ge(s, b)), hg))
133 case False{}:
134 fin_lt(p, q, s, b, a0, hi, r, he, hs, Equal.trans(Bool, Nat.is_ge(v(s), v(b)), U32.is_ge(s, b), False{}, Equal.sym(Bool, U32.is_ge(s, b), Nat.is_ge(v(s), v(b)), WC.u32_ge(s, b)), hg))
135
136def shl_ts(+p: Nat, +q: Word(p), +b: U32, +t: Bool, +s: Word(32n), +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : Nat}, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hts: {Nat.add(WD.uw(32n, s), WD.sc(32n, WD.bo(t, one))) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, U32{s}, b, Bool.or(t, U32.is_ge(U32{s}, b)))):
137 match t:
138 case True{}:
139 fin_true(p, q, U32{s}, b, a0, hi, r, one, h1, he, hr, L.subst(Nat, z => {Nat.add(z, WD.sc(32n, one)) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, WD.uw(32n, s), v(U32{s}), Equal.sym(Nat, v(U32{s}), WD.uw(32n, s), vw(s)), hts))
140 case False{}:
141 +hs = Equal.trans(Nat, v(U32{s}), WD.uw(32n, s), Nat.add(S.bit_value(a0), Nat.double(r)), vw(s), Equal.trans(Nat, WD.uw(32n, s), Nat.add(WD.uw(32n, s), 0n), Nat.add(S.bit_value(a0), Nat.double(r)), Equal.sym(Nat, Nat.add(WD.uw(32n, s), 0n), WD.uw(32n, s), N.add_zero(WD.uw(32n, s))), hts))
142 fin_false(p, q, U32{s}, b, a0, hi, r, he, hr, hs, U32.is_ge(U32{s}, b), {==})
143
144def shl_ok(+p: Nat, +q: Word(p), +b: U32, ts: Bool & Word(32n), +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : Nat}, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, hts: {Nat.add(WD.uw(32n, WD.ow(32n, ts)), WD.sc(32n, WD.bo(WD.ob(32n, ts), one))) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.shl(p, q, b, ts)):
145 match ts:
146 case (+t, +s):
147 shl_ts(p, q, b, t, s, a0, hi, r, one, h1, he, hr, hts)
148
149def rec_ok(+p: Nat, +a0: Bool, +b: U32, +hi: Word(p), qr: Word(p) & U32, ih: inv(p, hi, v(b), qr), +one: Nat, +h1: {one == 1n : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.rec(p, a0, b, qr)):
150 match qr:
151 case (+q, +r):
152 match r:
153 case U32{+rw}:
154 (he, hr) = ih
155 +hts = Equal.trans(Nat, Nat.add(WD.uw(32n, WD.ow(32n, Word.shl.out(32n, a0, rw))), WD.sc(32n, WD.bo(WD.ob(32n, Word.shl.out(32n, a0, rw)), one))), Nat.add(S.bit_value(a0), Nat.double(WD.uw(32n, rw))), Nat.add(S.bit_value(a0), Nat.double(v(U32{rw}))),
156 WD.shl_out1(32n, one, h1, a0, rw),
157 Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(a0), Nat.double(z)), WD.uw(32n, rw), v(U32{rw}), Equal.sym(Nat, v(U32{rw}), WD.uw(32n, rw), vw(rw))))
158 shl_ok(p, q, b, Word.shl.out(32n, a0, rw), a0, hi, v(U32{rw}), one, h1, he, hr, hts)
159
160
161def go_ok(+m: Nat, +a: Word(m), +b: U32, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> inv(m, a, v(b), U32.divmod.go(m, a, b)):
162 match m a:
163 case 0n WNil{}:
164 ({==}, hb)
165 case 1n+p WCon{a0, hi}:
166 rec_ok(p, a0, b, hi, U32.divmod.go(p, hi, b), go_ok(p, hi, b, hb, one, h1), one, h1)
167
168
169
170def pos_nat(+x: Nat, +h: {Cmp.is_eq(Nat.cmp(x, 0n)) == False{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}:
171 match x:
172 case 0n:
173 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(h))
174 case 1n+k:
175 {==}
176
177def pos(+b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {Nat.is_lt(0n, v(b)) == True{} : Bool}:
178 pos_nat(v(b), L.subst(Cmp, c => {Cmp.is_eq(c) == False{} : Bool}, U32.cmp(b, 0), Nat.cmp(v(b), 0n), U.u32_cmp(b, 0), hb))
179
180def dm_fin(+aw: Word(32n), +b: U32, qr: Word(32n) & U32, h: inv(32n, aw, v(b), qr)) -> {Nat.add(Nat.mul(v(U32.div.fin(qr)), v(b)), v(U32.mod.fin(qr))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.fin(qr)), v(b)) == True{} : Bool}:
181 match qr:
182 case (+q, +r):
183 (he, hr) = h
184 +eq = Equal.trans(Nat, Nat.add(Nat.mul(v(U32{q}), v(b)), v(r)), Nat.add(Nat.mul(S.unsigned(32n, q), v(b)), v(r)), v(U32{aw}),
185 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, v(b)), v(r)), v(U32{q}), S.unsigned(32n, q), vw(q)),
186 Equal.trans(Nat, Nat.add(Nat.mul(S.unsigned(32n, q), v(b)), v(r)), S.unsigned(32n, aw), v(U32{aw}), he, Equal.sym(Nat, v(U32{aw}), S.unsigned(32n, aw), vw(aw))))
187 (eq, hr)
188
189def dm_if(+aw: Word(32n), +b: U32, +z: Bool, +hz: {z == False{} : Bool}, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(v(U32.div.if(aw, b, z)), v(b)), v(U32.mod.if(aw, b, z))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.if(aw, b, z)), v(b)) == True{} : Bool}:
190 match z:
191 case True{}:
192 Empty.absurd({Nat.add(Nat.mul(v(U32.div.if(aw, b, True{})), v(b)), v(U32.mod.if(aw, b, True{}))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.if(aw, b, True{})), v(b)) == True{} : Bool}, L.true_false(hz))
193 case False{}:
194 dm_fin(aw, b, U32.divmod.go(32n, aw, b), go_ok(32n, aw, b, hb, 1n, {==}))
195
196
197def div_mod(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat} & {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool}:
198 match a b:
199 case U32{+aw} U32{+bw}:
200 dm_if(aw, U32{bw}, U32.is_zero(U32{bw}), hb, pos(U32{bw}, hb))
201
202def mod_identify(+q: Nat, +d: Nat, +r: Nat, +bound: {Nat.is_lt(r, d) == True{} : Bool}) -> {Nat.mod(Nat.add(Nat.mul(q, d), r), d) == r : Nat}:
203 match d:
204 case 0n:
205 Empty.absurd({Nat.mod(Nat.add(Nat.mul(q, 0n), r), 0n) == r : Nat}, N.lt_zero_absurd(r, bound))
206 case 1n+p:
207 ND.remainder(q, p, r, N.lt_succ_le(r, p, bound))
208
209def dm_type(+a: U32, +b: U32) -> Type:
210 {Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat} & {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool}
211
212def div_of(+a: U32, +b: U32, h: dm_type(a, b)) -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}:
213 (e, lt) = h
214 %e : {v(U32.div(a, b)) == Nat.div(_, v(b)) : Nat}
215 Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))), v(b)), v(U32.div(a, b)), DQ.identify(v(U32.div(a, b)), v(b), v(U32.mod(a, b)), lt))
216
217def mod_of(+a: U32, +b: U32, h: dm_type(a, b)) -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}:
218 (e, lt) = h
219 %e : {v(U32.mod(a, b)) == Nat.mod(_, v(b)) : Nat}
220 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))), v(b)), v(U32.mod(a, b)), mod_identify(v(U32.div(a, b)), v(b), v(U32.mod(a, b)), lt))
221
222
223def div_nat(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}:
224 div_of(a, b, div_mod(a, b, hb))
225
226
227def mod_nat(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}:
228 mod_of(a, b, div_mod(a, b, hb))