| blob | db8feb487ecb894aeb1f4b87bc3cdac520cfc031 |
1 module Set_str
3 use int.Int
4 use int.Power
5 use array.Array
6 use map.Map
7 use mach.int.Int32
8 use mach.int.UInt32
9 use mach.c.UChar
10 use import mach.int.UInt64GMP as Limb
11 use mach.c.C
12 use types.Types
13 use types.Int32Eq
14 use types.UInt64Eq
15 use lemmas.Lemmas
16 use powm.Powm
17 use stringlemmas.String_lemmas
18 use logical.Logical
19 use util.Util
20 use int.ComputerDivision as CD
21 use int.EuclideanDivision
22 use base_info.BaseInfo
24 let wmpn_set_str_bits (rp: ptr limb) (ghost sz: int32)
25 (sp: ptr uchar) (sn: uint32)
26 (bits: uint32) : int32
27 requires { 0 < sn <= max_int32 }
28 requires { 0 < sz }
29 requires { valid rp sz }
30 requires { valid sp sn }
31 requires { 1 <= bits <= 8 }
32 requires { power 2 (bits * sn) <= power radix sz }
33 requires { writable rp }
34 requires { in_base (power 2 bits) (pelts sp)
35 (offset sp) (offset sp + sn) }
36 ensures { 0 <= result <= sz }
37 ensures { value rp result = svalue (power 2 bits) sp sn }
38 ensures { result > 0 -> (pelts rp)[offset rp + result - 1] > 0 }
39 =
40 let ref rn = 0 in
41 let ref shift = 0 in
42 let ghost ref rdone : int = 0 in
43 let ref j = UInt32.to_int32 sn in
44 let ghost b = power 2 (uint32'int bits) in
45 assert { bits * sn <= 64 * sz
46 by power 2 (bits * sn) <= power radix sz
47 = power (power 2 64) sz
48 = power 2 (64 * sz) };
49 assert { 2 <= b <= 256
50 by 1 <= bits <= 8
51 so power 2 5 = 32
52 so power 2 6 = 64
53 so power 2 7 = 128
54 so power 2 8 = 256 };
55 while j > 0 do
56 invariant { 0 <= j <= sn }
57 invariant { 0 <= rn <= sz }
58 invariant { (sn - j) * bits = rdone }
59 invariant { j > 0 -> if shift = 0 then rdone = 64 * rn
60 else rdone = 64 * rn - 64 + shift }
61 invariant { 0 <= shift < 64 }
62 invariant { shift > 0 ->
63 (pelts rp)[offset rp + rn - 1] < power 2 shift }
64 invariant { rn = 0 -> shift = 0 }
65 invariant { value rp rn
66 = svalue_sub b (pelts sp) (offset sp + j)
67 (offset sp + sn) }
68 variant { j }
69 label StartLoop in
70 let ghost orp = pure { rp } in
71 j <- j-1;
72 let sj = UChar.to_uint64 (C.get_ofs sp j) in
73 svalue_sub_tail b (pelts sp) (offset sp + int32'int j + 1)
74 (offset sp + uint32'int sn);
75 assert { svalue_sub b (pelts sp) (offset sp + j) (offset sp + sn)
76 = svalue_sub b (pelts sp) (offset sp + j + 1)
77 (offset sp + sn)
78 + power b (sn - (j+1)) * sj
79 = svalue_sub b (pelts sp) (offset sp + j + 1)
80 (offset sp + sn)
81 + power 2 rdone * sj
82 by power b (sn - (j+1))
83 = power (power 2 bits) (sn - (j+1))
84 = power 2 (bits * (sn - (j+1)))
85 = power 2 rdone };
86 if shift = 0
87 then begin
88 assert { rn < sz
89 by (sn - (j+1)) * bits = 64 * rn + shift
90 so (sn - (j+1)) * bits
91 = bits * sn - (j+1) * bits
92 <= 64 * sz - (j+1) * bits
93 < 64 * sz
94 so 64 * rn < 64 * sz };
95 C.set_ofs rp rn sj;
96 value_sub_frame (pelts rp) (pelts orp)
97 (offset rp) (offset rp + int32'int rn);
98 assert { value rp rn = value rp rn at StartLoop };
99 value_tail rp rn;
100 rn <- rn + 1;
101 shift <- bits;
102 assert { (pelts rp)[offset rp + rn - 1]
103 = sj
104 < power 2 bits };
105 assert { power b (sn - (j+1)) = power radix (rn-1)
106 by power b (sn - (j+1))
107 = power 2 (bits * (sn - (j+1)))
108 = power 2 rdone
109 = power 2 (64 * (rn-1))
110 = power radix (rn-1) };
111 assert { value rp rn = svalue_sub b (pelts sp) (offset sp + j)
112 (offset sp + sn)
113 by value rp rn
114 = value rp (rn - 1) + power radix (rn - 1) * sj
115 = value orp (rn - 1) + power radix (rn - 1) * sj
116 = svalue_sub b (pelts sp) (offset sp + j + 1)
117 (offset sp + sn)
118 + power radix (rn - 1) * sj
119 = svalue_sub b (pelts sp) (offset sp + j)
120 (offset sp + sn) };
121 end
122 else begin
123 let rlow = C.get_ofs rp (rn - 1) in
124 assert { rlow < power 2 shift };
125 assert { radix = power 2 (64 - shift) * power 2 shift };
126 let slow = lsl_mod sj (Limb.of_uint32 shift) in
127 assert { slow = power 2 shift * mod sj (power 2 (64 - shift))
128 by slow = mod (sj * power 2 shift) radix
129 = mod (sj * power 2 shift)
130 (power 2 (64 - shift) * power 2 shift)
131 = power 2 shift * mod sj (power 2 (64 - shift)) };
132 assert { rlow + slow < radix
133 by slow = power 2 shift * mod sj (power 2 (64 - shift))
134 <= power 2 shift * (power 2 (64 - shift) - 1)
135 = power 2 shift * power 2 (64 - shift)
136 - power 2 shift
137 = radix - power 2 shift };
138 let nr = rlow + slow in
139 C.set_ofs rp (rn-1) nr;
140 let ghost oshift = pure { shift } in
141 shift <- shift + bits;
142 assert { power radix (rn - 1) * power 2 oshift
143 = power b (sn - (j+1))
144 by power radix (rn - 1) = power 2 (64 * (rn - 1))
145 so power radix (rn - 1) * power 2 oshift
146 = power 2 (64 * (rn - 1) + oshift)
147 = power 2 (bits * (sn - (j+1)))
148 = power b (sn - (j+1)) };
149 if shift >= 64
150 then begin
151 shift <- shift - 64;
152 if shift > 0
153 then begin
154 assert { rdone = 64 * rn + shift - bits };
155 assert { rn < sz
156 by (sn - (j+1)) * bits = rdone
157 = 64 * rn + shift - bits
158 so bits * sn <= 64 * sz
159 so 64 * rn + shift - bits
160 = sn * bits - (j+1) * bits
161 <= 64 * sz - (j+1) * bits
162 <= 64 * sz - bits
163 so 64 * rn + shift <= 64 * sz
164 so 64 * rn < 64 * rn + shift };
165 let shigh = lsr_mod sj (Limb.of_uint32 (bits - shift)) in
166 assert { shigh < power 2 shift
167 by shigh = div sj (power 2 (bits - shift))
168 so sj = (power 2 (bits - shift))
169 * div sj (power 2 (bits - shift))
170 + mod sj (power 2 (bits - shift))
171 so power 2 (bits - shift) * shigh
172 = sj - mod sj (power 2 (bits - shift))
173 <= sj < power 2 bits
174 = power 2 (bits - shift) * power 2 shift
175 so shigh < power 2 shift };
176 assert { slow + radix * shigh = power 2 oshift * sj
177 by slow = mod (power 2 oshift * sj) radix
178 so shigh = div sj (power 2 (bits - shift))
179 so shift = oshift + bits - 64
180 so shigh = div sj (power 2 (64 - oshift))
181 so let m = mod sj (power 2 (64 - oshift)) in
182 sj = power 2 (64 - oshift) * shigh + m
183 so power 2 oshift * sj
184 = power 2 oshift * power 2 (64 - oshift) * shigh
185 + power 2 oshift * m
186 = radix * shigh + power 2 oshift * m
187 so 0 <= m < power 2 (64 - oshift)
188 so 0 <= power 2 oshift * m
189 < power 2 oshift * power 2 (64 - oshift)
190 = radix
191 so mod (power 2 oshift * sj) radix
192 = mod (radix * shigh + power 2 oshift * m) radix
193 = mod (power 2 oshift * m) radix
194 = power 2 oshift * m
195 so power 2 oshift * m = slow
196 so power 2 oshift * sj = radix * shigh + slow };
197 C.set_ofs rp rn shigh;
198 value_tail rp (rn - 1);
199 value_sub_frame (pelts rp) (pelts orp)
200 (offset rp) (offset rp + int32'int rn - 1);
201 assert { value rp rn
202 = value orp (rn - 1) + power radix (rn - 1) * nr
203 by (pelts rp)[offset rp + rn - 1] = nr
204 so value rp rn
205 = value rp (rn - 1) + power radix (rn - 1) * nr };
206 value_tail orp (rn - 1);
207 value_tail rp rn;
208 assert { value rp (rn + 1)
209 = svalue_sub b (pelts sp) (offset sp + j) (offset sp + sn)
210 by value rp (rn + 1)
211 = value rp rn + power radix rn * shigh
212 = value orp (rn - 1) + power radix (rn - 1) * nr
213 + power radix rn * shigh
214 = value orp (rn - 1) + power radix (rn - 1) * rlow
215 + power radix (rn - 1) * slow
216 + power radix rn * shigh
217 = value orp rn
218 + power radix (rn - 1) * slow
219 + power radix rn * shigh
220 = value orp rn
221 + power radix (rn - 1) * (slow + radix * shigh)
222 = value orp rn
223 + power radix (rn - 1) * power 2 oshift * sj
224 = value orp rn + power b (sn - (j+1)) * sj
225 = svalue_sub b (pelts sp)
226 (offset sp + j) (offset sp + sn) };
227 rn <- rn + 1;
228 end else begin
229 value_tail rp (rn - 1);
230 value_tail orp (rn - 1);
231 assert { slow = power 2 oshift * sj
232 by slow = power 2 oshift * mod sj (power 2 (64 - oshift))
233 so 64 - oshift = bits
234 so 0 <= sj < power 2 bits
235 so mod sj (power 2 (64 - oshift))
236 = mod sj (power 2 bits)
237 = sj };
238 assert { value rp rn
239 = svalue_sub b (pelts sp) (offset sp + j) (offset sp + sn)
240 by value rp rn
241 = value rp (rn - 1) + power radix (rn - 1) * nr
242 = value rp (rn - 1) + power radix (rn - 1) * rlow
243 + power radix (rn - 1) * slow
244 = value orp (rn - 1) + power radix (rn - 1) * rlow
245 + power radix (rn - 1) * slow
246 = value orp rn + power radix (rn - 1) * slow
247 = value orp rn
248 + power radix (rn - 1) * power 2 oshift * sj
249 = value orp rn + power b (sn - (j+1)) * sj
250 = svalue_sub b (pelts sp) (offset sp + j)
251 (offset sp + sn) };
252 end;
253 end else begin
254 assert { slow = power 2 oshift * sj
255 by slow = power 2 oshift * mod sj (power 2 (64 - oshift))
256 so oshift + bits < 64
257 so sj < power 2 bits <= power 2 (64 - oshift)
258 so mod sj (power 2 (64 - oshift)) = sj };
259 assert { nr < power 2 shift
260 by nr = rlow + slow
261 so rlow < power 2 oshift
262 so rlow + slow < power 2 oshift + power 2 oshift * sj
263 = power 2 oshift * (1 + sj)
264 <= power 2 oshift * power 2 bits
265 = power 2 shift };
266 value_tail rp (rn - 1);
267 value_tail orp (rn - 1);
268 assert { value rp rn
269 = svalue_sub b (pelts sp) (offset sp + j) (offset sp + sn)
270 by value rp rn
271 = value rp (rn - 1) + power radix (rn - 1) * nr
272 = value rp (rn - 1) + power radix (rn - 1) * rlow
273 + power radix (rn - 1) * slow
274 = value orp (rn - 1) + power radix (rn - 1) * rlow
275 + power radix (rn - 1) * slow
276 = value orp rn + power radix (rn - 1) * slow
277 = value orp rn
278 + power radix (rn - 1) * power 2 oshift * sj
279 = value orp rn + power b (sn - (j+1)) * sj
280 = svalue_sub b (pelts sp) (offset sp + j)
281 (offset sp + sn) };
282 end
283 end;
284 rdone <- rdone + uint32'int bits;
285 done;
286 normalize rp rn;
287 rn
289 use mul.Mul
290 use add_1.Add_1
292 let wmpn_set_str_other (rp: ptr limb) (ghost sz: int32)
293 (sp: ptr uchar) (sn: uint32) (b:limb)
294 (info: wmpn_base_info) : int32
295 requires { 0 < sn <= max_int32 }
296 requires { 0 < sz }
297 requires { valid rp sz }
298 requires { valid sp sn }
299 requires { 2 <= b <= 256 }
300 requires { power b sn <= power radix sz }
301 requires { writable rp }
302 requires { in_base b (pelts sp) (offset sp) (offset sp + sn) }
303 requires { info.b = b }
304 ensures { svalue b sp sn > 0 -> 1 <= result <= sz }
305 ensures { value rp result = svalue b sp sn }
306 ensures { svalue b sp sn > 0 -> (pelts rp)[offset rp + result - 1] > 0 }
307 ensures { svalue b sp sn = 0 -> result = 1 }
308 ensures { 0 < result }
309 =
310 let ref k = 1 + (sn - 1) % info.exp in
311 label Start in
312 let ref w = UChar.to_uint64 (C.get sp) in
313 let ref j = 1 in
314 while (k <- k - 1; k) > 0 do
315 variant { k }
316 invariant { 1 <= k <= sn }
317 invariant { 1 <= j <= sn }
318 invariant { w = svalue_sub b (pelts sp) (offset sp) (offset sp + j) }
319 invariant { 0 <= w < power b j }
320 invariant { j + k - 1 = 1 + mod (sn - 1) info.exp }
321 invariant { int32'int j = uint32'int sn -> k = 1 }
322 label Loop in
323 assert { k > 0 };
324 assert { j < info.exp };
325 let sj = UChar.to_uint64 (C.get_ofs sp j) in
326 svalue_sub_head (uint64'int b) (pelts sp)
327 (offset sp) (offset sp + int32'int j + 1);
328 assert { w * b + sj
329 = svalue_sub b (pelts sp) (offset sp) (offset sp + j + 1) };
330 assert { w * b + sj < radix
331 by w * b + sj
332 = svalue_sub b (pelts sp) (offset sp) (offset sp + j + 1)
333 < power b (j+1)
334 so j+1 <= info.exp
335 so power b (j+1) <= power b (info.exp) < radix };
336 w <- w * b + sj;
337 j <- j + 1;
338 done;
339 C.set rp w;
340 let ref rn = 1 in
341 assert { value rp 1
342 = w
343 = svalue_sub b (pelts sp) (offset sp) (offset sp + j) };
344 assert { j = 1 + mod (sn - 1) info.exp };
345 assert { mod (sn - j) info.exp = 0
346 by info.exp > 1
347 so mod 1 info.exp = 1
348 so mod j info.exp
349 = mod (mod 1 info.exp + mod (sn - 1) info.exp) info.exp
350 = mod sn info.exp
351 so let ds = div sn info.exp in
352 let dj = div j info.exp in
353 sn = ds * info.exp + mod sn info.exp
354 so j = dj * info.exp + mod j info.exp
355 so sn - j = (ds - dj) * info.exp
356 so mod (sn - j) info.exp = 0 };
357 while j < UInt32.to_int32 sn do
358 variant { sn - j }
359 invariant { 0 <= j <= sn }
360 invariant { value rp rn
361 = svalue_sub b (pelts sp) (offset sp)
362 (offset sp + int32'int j) }
363 invariant { j <= sn }
364 invariant { 0 <= rn <= sz }
365 invariant { svalue b sp j > 0 -> (pelts rp)[offset rp + rn - 1] > 0 }
366 invariant { svalue b sp j = 0 -> rn = 1 }
367 invariant { mod (sn - j) info.exp = 0 }
368 w <- UChar.to_uint64 (C.get_ofs sp j);
369 let oj = pure { j } in
370 assert { j + info.exp <= sn };
371 j <- j+1;
372 for k = 1 to info.exp - 1 do
373 invariant { w = svalue_sub b (pelts sp) (offset sp + oj)
374 (offset sp + j) }
375 invariant { 1 <= k <= info.exp }
376 invariant { j = oj + k }
377 let sj = UChar.to_uint64 (C.get_ofs sp j) in
378 svalue_sub_head (uint64'int b) (pelts sp) (offset sp + int32'int oj)
379 (offset sp + int32'int j + 1);
380 assert { w * b + sj = svalue_sub b (pelts sp) (offset sp + oj)
381 (offset sp + j + 1) };
382 assert { w * b + sj < radix
383 by svalue_sub b (pelts sp) (offset sp + oj) (offset sp + j + 1)
384 < power b (j + 1 - oj)
385 = power b (k+1) <= power b info.exp < radix };
386 w <- w * b + sj;
387 j <- j + 1;
388 done;
389 assert { mod (sn - j) info.exp = 0
390 by j = oj + info.exp
391 so mod (sn - j) info.exp
392 = mod (sn - oj - info.exp) info.exp
393 = mod (mod (sn - oj) info.exp
394 + mod (- info.exp) info.exp) info.exp
395 = mod (0 + 0) info.exp = 0 };
396 svalue_sub_concat (uint64'int b) (pelts sp) (offset sp)
397 (offset sp + int32'int oj) (offset sp + int32'int j);
398 assert { svalue b sp j
399 = svalue b sp oj * power b (j - oj) + w
400 = value rp rn * power b info.exp + w
401 = value rp rn * info.bb + w };
402 let ghost orp = pure { rp } in
403 let ref cy = wmpn_mul_1_in_place rp rn info.bb in
404 assert { cy < radix - 1
405 by value rp rn <= (power radix rn - 1)
406 so info.bb <= radix - 1
407 so info.bb * value orp rn <= (radix - 1) * (power radix rn - 1)
408 < (radix - 1) * (power radix rn)
409 so value orp rn * info.bb = value rp rn + power radix rn * cy
410 >= power radix rn * cy
411 so power radix rn * cy < power radix rn * (radix - 1) };
412 let cy1 = wmpn_add_1_in_place rp rn w in
413 cy <- cy + cy1;
414 assert { value rp rn + power radix rn * cy
415 = svalue_sub b (pelts sp) (offset sp) (offset sp + j) };
416 if cy > 0 then begin
417 value_sub_update_no_change (pelts rp) (offset rp + int32'int rn)
418 (offset rp) (offset rp + int32'int rn)
419 cy;
420 value_tail orp (rn - 1);
421 assert { rn < sz
422 by power b sn <= power radix sz
423 so value rp rn + power radix rn * cy
424 = svalue_sub b (pelts sp) (offset sp) (offset sp + j)
425 < power b j <= power b sn <= power radix sz
426 so power radix rn * cy >= power radix rn
427 so value rp rn >= 0
428 so power radix rn < power radix sz };
429 C.set_ofs rp rn cy;
430 value_tail rp rn;
431 rn <- rn + 1;
432 end
433 else begin
434 value_tail rp (rn - 1);
435 value_tail orp (rn - 1);
436 assert { svalue b sp j > 0 -> (pelts rp)[offset rp + rn - 1] > 0
437 by info.bb >= 1
438 so value rp rn = value orp rn * info.bb + w
439 >= value orp rn * info.bb
440 >= value orp rn
441 so if svalue b sp oj > 0
442 then (pelts orp)[offset rp + rn - 1] > 0
443 so value orp rn
444 = value orp (rn - 1)
445 + power radix (rn - 1)
446 * (pelts orp)[offset rp + rn - 1]
447 >= power radix (rn - 1) * (pelts orp)[offset rp + rn - 1]
448 >= power radix (rn - 1)
449 so value rp rn >= value orp rn
450 so power radix (rn - 1) * 1
451 = power radix (rn - 1) <= value rp rn
452 = value rp (rn - 1)
453 + power radix (rn - 1) * (pelts rp)[offset rp + rn - 1]
454 < power radix (rn - 1)
455 + power radix (rn - 1) * (pelts rp)[offset rp + rn - 1]
456 = power radix (rn - 1)
457 * (1 + (pelts rp)[offset rp + rn - 1])
458 so 1 < 1 + (pelts rp)[offset rp + rn - 1]
459 else rn = 1 /\ value rp rn = svalue b sp j = w
460 so w > 0
461 so (pelts rp)[offset rp + rn - 1] > 0 };
462 end
463 done;
464 value_tail rp (rn - 1);
465 rn
467 let wmpn_set_str (rp: ptr limb) (ghost sz: int32) (sp: ptr uchar) (sn:uint32)
468 (base: int32) : int32
469 requires { valid sp sn }
470 requires { valid rp sz }
471 requires { sz > 0 }
472 requires { sn >= 0 }
473 requires { power base sn <= power radix (sz - 1) }
474 requires { 2 <= base <= 256 }
475 requires { writable rp }
476 requires { in_base base (pelts sp) (offset sp) (offset sp + sn) }
477 writes { rp.data.elts }
478 ensures { result <= sz - 1 }
479 ensures { value rp result = svalue base sp sn }
480 ensures { sn > 0 -> (pelts sp)[offset sp] > 0
481 -> (pelts rp)[offset rp + result - 1] > 0 }
482 =
483 ghost (if sn > 0 then
484 svalue_sub_tail (int32'int base) (pelts sp) (offset sp + 1)
485 (offset sp + uint32'int sn));
486 assert { sn > 0 -> (pelts sp)[offset sp] > 0 -> svalue base sp sn > 0
487 by svalue base sp sn
488 = svalue_sub base (pelts sp) (offset sp + 1) (offset sp + sn)
489 + power base (sn - 1) * (pelts sp)[offset sp]
490 >= power base (sn - 1) * (pelts sp)[offset sp]
491 > 0 };
492 if sn = 0 then return 0;
493 let bits = wmpn_base_power_of_two_p (Limb.of_int32 base) in
494 if (bits <> 0)
495 then return wmpn_set_str_bits rp (sz-1) sp sn bits
496 else begin
497 let info = wmpn_get_base_info (Limb.of_int32 base) in
498 return wmpn_set_str_other rp (sz-1) sp sn (Limb.of_int32 base) info
499 end
501 end