1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
|
<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<title>Value.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" />
<script type="text/javascript" src="alectryon.js"></script>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" />
</head>
<body>
<div class="alectryon-root alectryon-floating"><div class="document">
<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-wsp"><span class="highlight"><span class="c">(*(*</span>
<span class="c"> * Vericert: Verified high-level synthesis.</span>
<span class="c"> * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com></span>
<span class="c"> *</span>
<span class="c"> * This program is free software: you can redistribute it and/or modify</span>
<span class="c"> * it under the terms of the GNU General Public License as published by</span>
<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span>
<span class="c"> * (at your option) any later version.</span>
<span class="c"> *</span>
<span class="c"> * This program is distributed in the hope that it will be useful,</span>
<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span>
<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span>
<span class="c"> * GNU General Public License for more details.</span>
<span class="c"> *</span>
<span class="c"> * You should have received a copy of the GNU General Public License</span>
<span class="c"> * along with this program. If not, see <https://www.gnu.org/licenses/>.</span>
<span class="c"> *)</span>
<span class="c">(* begin hide *)</span>
<span class="c">From bbv Require Import Word.</span>
<span class="c">From bbv Require HexNotation WordScope.</span>
<span class="c">From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.</span>
<span class="c">From compcert Require Import lib.Integers common.Values.</span>
<span class="c">From vericert Require Import Vericertlib.</span>
<span class="c">(* end hide *)</span>
<span class="c">(** * Value</span>
<span class="c">A [value] is a bitvector with a specific size. We are using the implementation</span>
<span class="c">of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.</span>
<span class="c">However, we need to wrap it with an [Inductive] so that we can specify and match</span>
<span class="c">on the size of the [value]. This is necessary so that we can easily store</span>
<span class="c">[value]s of different sizes in a list or in a map.</span>
<span class="c">Using the default [word], this would not be possible, as the size is part of the type. *)</span>
<span class="c">Record value : Type :=</span>
<span class="c"> mkvalue {</span>
<span class="c"> vsize: nat;</span>
<span class="c"> vword: word vsize</span>
<span class="c"> }.</span>
<span class="c">(** ** Value conversions</span>
<span class="c">Various conversions to different number types such as [N], [Z], [positive] and</span>
<span class="c">[int], where the last one is a theory of integers of powers of 2 in CompCert. *)</span>
<span class="c">Definition wordToValue : forall sz : nat, word sz -> value := mkvalue.</span>
<span class="c">Definition valueToWord : forall v : value, word (vsize v) := vword.</span>
<span class="c">Definition valueToNat (v :value) : nat :=</span>
<span class="c"> wordToNat (vword v).</span>
<span class="c">Definition natToValue sz (n : nat) : value :=</span>
<span class="c"> mkvalue sz (natToWord sz n).</span>
<span class="c">Definition valueToN (v : value) : N :=</span>
<span class="c"> wordToN (vword v).</span>
<span class="c">Definition NToValue sz (n : N) : value :=</span>
<span class="c"> mkvalue sz (NToWord sz n).</span>
<span class="c">Definition ZToValue (s : nat) (z : Z) : value :=</span>
<span class="c"> mkvalue s (ZToWord s z).</span>
<span class="c">Definition valueToZ (v : value) : Z :=</span>
<span class="c"> wordToZ (vword v).</span>
<span class="c">Definition uvalueToZ (v : value) : Z :=</span>
<span class="c"> uwordToZ (vword v).</span>
<span class="c">Definition posToValue sz (p : positive) : value :=</span>
<span class="c"> ZToValue sz (Zpos p).</span>
<span class="c">Definition posToValueAuto (p : positive) : value :=</span>
<span class="c"> let size := Pos.to_nat (Pos.size p) in</span>
<span class="c"> ZToValue size (Zpos p).</span>
<span class="c">Definition valueToPos (v : value) : positive :=</span>
<span class="c"> Z.to_pos (uvalueToZ v).</span>
<span class="c">Definition intToValue (i : Integers.int) : value :=</span>
<span class="c"> ZToValue Int.wordsize (Int.unsigned i).</span>
<span class="c">Definition valueToInt (i : value) : Integers.int :=</span>
<span class="c"> Int.repr (uvalueToZ i).</span>
<span class="c">Definition ptrToValue (i : Integers.ptrofs) : value :=</span>
<span class="c"> ZToValue Ptrofs.wordsize (Ptrofs.unsigned i).</span>
<span class="c">Definition valueToPtr (i : value) : Integers.ptrofs :=</span>
<span class="c"> Ptrofs.repr (uvalueToZ i).</span>
<span class="c">Definition valToValue (v : Values.val) : option value :=</span>
<span class="c"> match v with</span>
<span class="c"> | Values.Vint i => Some (intToValue i)</span>
<span class="c"> | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z</span>
<span class="c"> then Some (ptrToValue off)</span>
<span class="c"> else None</span>
<span class="c"> | Values.Vundef => Some (ZToValue 32 0%Z)</span>
<span class="c"> | _ => None</span>
<span class="c"> end.</span>
<span class="c">(** Convert a [value] to a [bool], so that choices can be made based on the</span>
<span class="c">result. This is also because comparison operators will give back [value] instead</span>
<span class="c">of [bool], so if they are in a condition, they will have to be converted before</span>
<span class="c">they can be used. *)</span>
<span class="c">Definition valueToBool (v : value) : bool :=</span>
<span class="c"> negb (weqb (@wzero (vsize v)) (vword v)).</span>
<span class="c">Definition boolToValue (sz : nat) (b : bool) : value :=</span>
<span class="c"> natToValue sz (if b then 1 else 0).</span>
<span class="c">(** ** Arithmetic operations *)</span>
<span class="c">Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.</span>
<span class="c">intros; subst; assumption. Defined.</span>
<span class="c">Lemma unify_word_unfold :</span>
<span class="c"> forall sz w,</span>
<span class="c"> unify_word sz sz w eq_refl = w.</span>
<span class="c">Proof. auto. Qed.</span>
<span class="c">Definition value_eq_size:</span>
<span class="c"> forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.</span>
<span class="c">Proof.</span>
<span class="c"> intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?.</span>
<span class="c"> left; apply Nat.eqb_eq in Heqb; assumption.</span>
<span class="c"> right; trivial.</span>
<span class="c">Defined.</span>
<span class="c">Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A)</span>
<span class="c"> (EQ : vsize v1 = vsize v2) : A :=</span>
<span class="c"> let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in</span>
<span class="c"> f (vword v1) w2.</span>
<span class="c">Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A)</span>
<span class="c"> : option A :=</span>
<span class="c"> match value_eq_size v1 v2 with</span>
<span class="c"> | left EQ =></span>
<span class="c"> Some (map_any v1 v2 f EQ)</span>
<span class="c"> | _ => None</span>
<span class="c"> end.</span>
<span class="c">Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value :=</span>
<span class="c"> mkvalue (vsize v) (f (vsize v) (vword v)).</span>
<span class="c">Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value)</span>
<span class="c"> (EQ : (vsize v1 = vsize v2)) : value :=</span>
<span class="c"> let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in</span>
<span class="c"> mkvalue (vsize v1) (f (vsize v1) (vword v1) w2).</span>
<span class="c">Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value)</span>
<span class="c"> : option value :=</span>
<span class="c"> match value_eq_size v1 v2 with</span>
<span class="c"> | left EQ => Some (map_word2 f v1 v2 EQ)</span>
<span class="c"> | _ => None</span>
<span class="c"> end.</span>
<span class="c">Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value)</span>
<span class="c"> : option value :=</span>
<span class="c"> match value_eq_size v1 v2 with</span>
<span class="c"> | left EQ => Some (f EQ)</span>
<span class="c"> | _ => None</span>
<span class="c"> end.</span>
<span class="c">Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y.</span>
<span class="c">Proof.</span>
<span class="c"> split; intros.</span>
<span class="c"> subst. reflexivity. inversion H. apply existT_wordToZ in H1.</span>
<span class="c"> apply wordToZ_inj. assumption.</span>
<span class="c">Qed.</span>
<span class="c">Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y.</span>
<span class="c">Proof. apply eqvalue. Qed.</span>
<span class="c">Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y.</span>
<span class="c">Proof. split; intros; intuition. apply H. apply eqvalue. assumption.</span>
<span class="c"> apply H. rewrite H0. trivial.</span>
<span class="c">Qed.</span>
<span class="c">Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y.</span>
<span class="c">Proof. apply nevalue. Qed.</span>
<span class="c">(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz)</span>
<span class="c"> : option (word finalsz) :=</span>
<span class="c"> match Nat.eqb initsz finalsz return option (word finalsz) with</span>
<span class="c"> | true => Some _</span>
<span class="c"> | false => None</span>
<span class="c"> end.*)</span>
<span class="c">Definition valueeq (sz : nat) (x y : word sz) :</span>
<span class="c"> {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} :=</span>
<span class="c"> match weq x y with</span>
<span class="c"> | left eq => left (eqvaluef x y eq)</span>
<span class="c"> | right ne => right (nevaluef x y ne)</span>
<span class="c"> end.</span>
<span class="c">Definition valueeqb (x y : value) : bool :=</span>
<span class="c"> match value_eq_size x y with</span>
<span class="c"> | left EQ =></span>
<span class="c"> weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ)</span>
<span class="c"> | right _ => false</span>
<span class="c"> end.</span>
<span class="c">Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2).</span>
<span class="c">Theorem value_projZ_eqb_true :</span>
<span class="c"> forall v1 v2,</span>
<span class="c"> v1 = v2 -> value_projZ_eqb v1 v2 = true.</span>
<span class="c">Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed.</span>
<span class="c">Theorem valueeqb_true_iff :</span>
<span class="c"> forall v1 v2,</span>
<span class="c"> valueeqb v1 v2 = true <-> v1 = v2.</span>
<span class="c">Proof.</span>
<span class="c"> split; intros.</span>
<span class="c"> unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?.</span>
<span class="c"> - destruct v1, v2. simpl in H.</span>
<span class="c">Abort.</span>
<span class="c">Definition value_int_eqb (v : value) (i : int) : bool :=</span>
<span class="c"> Z.eqb (valueToZ v) (Int.unsigned i).</span>
<span class="c">(** Arithmetic operations over [value], interpreting them as signed or unsigned</span>
<span class="c">depending on the operation.</span>
<span class="c">The arithmetic operations over [word] are over [N] by default, however, can also</span>
<span class="c">be called over [Z] explicitly, which is where the bits are interpreted in a</span>
<span class="c">signed manner. *)</span>
<span class="c">Definition vplus v1 v2 := map_word2 wplus v1 v2.</span>
<span class="c">Definition vplus_opt v1 v2 := map_word2_opt wplus v1 v2.</span>
<span class="c">Definition vminus v1 v2 := map_word2 wminus v1 v2.</span>
<span class="c">Definition vmul v1 v2 := map_word2 wmult v1 v2.</span>
<span class="c">Definition vdiv v1 v2 := map_word2 wdiv v1 v2.</span>
<span class="c">Definition vmod v1 v2 := map_word2 wmod v1 v2.</span>
<span class="c">Definition vmuls v1 v2 := map_word2 wmultZ v1 v2.</span>
<span class="c">Definition vdivs v1 v2 := map_word2 wdivZ v1 v2.</span>
<span class="c">Definition vmods v1 v2 := map_word2 wremZ v1 v2.</span>
<span class="c">(** ** Bitwise operations</span>
<span class="c">Bitwise operations over [value], which is independent of whether the number is</span>
<span class="c">signed or unsigned. *)</span>
<span class="c">Definition vnot v := map_word wnot v.</span>
<span class="c">Definition vneg v := map_word wneg v.</span>
<span class="c">Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)).</span>
<span class="c">Definition vor v1 v2 := map_word2 wor v1 v2.</span>
<span class="c">Definition vand v1 v2 := map_word2 wand v1 v2.</span>
<span class="c">Definition vxor v1 v2 := map_word2 wxor v1 v2.</span>
<span class="c">(** ** Comparison operators</span>
<span class="c">Comparison operators that return a bool, there should probably be an equivalent</span>
<span class="c">which returns another number, however I might just add that as an explicit</span>
<span class="c">conversion. *)</span>
<span class="c">Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)).</span>
<span class="c">Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ).</span>
<span class="c">Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ).</span>
<span class="c">Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ).</span>
<span class="c">Definition vltb v1 v2 := map_any v1 v2 wltb.</span>
<span class="c">Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)).</span>
<span class="c">Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ).</span>
<span class="c">Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ).</span>
<span class="c">Definition vltsb v1 v2 := map_any v1 v2 wsltb.</span>
<span class="c">Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)).</span>
<span class="c">Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ).</span>
<span class="c">Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ).</span>
<span class="c">Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ).</span>
<span class="c">Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ).</span>
<span class="c">Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ).</span>
<span class="c">Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ).</span>
<span class="c">Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ).</span>
<span class="c">Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ).</span>
<span class="c">Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ).</span>
<span class="c">Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ).</span>
<span class="c">(** ** Shift operators</span>
<span class="c">Shift operators on values. *)</span>
<span class="c">Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) :=</span>
<span class="c"> f w1 (wordToNat w2).</span>
<span class="c">Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2.</span>
<span class="c">Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2.</span>
<span class="c">Module HexNotationValue.</span>
<span class="c"> Export HexNotation.</span>
<span class="c"> Import WordScope.</span>
<span class="c"> Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50).</span>
<span class="c">End HexNotationValue.</span>
<span class="c">Inductive val_value_lessdef: val -> value -> Prop :=</span>
<span class="c">| val_value_lessdef_int:</span>
<span class="c"> forall i v',</span>
<span class="c"> i = valueToInt v' -></span>
<span class="c"> val_value_lessdef (Vint i) v'</span>
<span class="c">| val_value_lessdef_ptr:</span>
<span class="c"> forall b off v',</span>
<span class="c"> off = valueToPtr v' -></span>
<span class="c"> (Z.modulo (uvalueToZ v') 4) = 0%Z -></span>
<span class="c"> val_value_lessdef (Vptr b off) v'</span>
<span class="c">| lessdef_undef: forall v, val_value_lessdef Vundef v.</span>
<span class="c">Inductive opt_val_value_lessdef: option val -> value -> Prop :=</span>
<span class="c">| opt_lessdef_some:</span>
<span class="c"> forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'</span>
<span class="c">| opt_lessdef_none: forall v, opt_val_value_lessdef None v.</span>
<span class="c">Lemma valueToZ_ZToValue :</span>
<span class="c"> forall n z,</span>
<span class="c"> (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -></span>
<span class="c"> valueToZ (ZToValue (S n) z) = z.</span>
<span class="c">Proof.</span>
<span class="c"> unfold valueToZ, ZToValue. simpl.</span>
<span class="c"> auto using wordToZ_ZToWord.</span>
<span class="c">Qed.</span>
<span class="c">Lemma uvalueToZ_ZToValue :</span>
<span class="c"> forall n z,</span>
<span class="c"> (0 <= z < 2 ^ Z.of_nat n)%Z -></span>
<span class="c"> uvalueToZ (ZToValue n z) = z.</span>
<span class="c">Proof.</span>
<span class="c"> unfold uvalueToZ, ZToValue. simpl.</span>
<span class="c"> auto using uwordToZ_ZToWord.</span>
<span class="c">Qed.</span>
<span class="c">Lemma uvalueToZ_ZToValue_full :</span>
<span class="c"> forall sz : nat,</span>
<span class="c"> (0 < sz)%nat -></span>
<span class="c"> forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z.</span>
<span class="c">Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed.</span>
<span class="c">Lemma ZToValue_uvalueToZ :</span>
<span class="c"> forall v,</span>
<span class="c"> ZToValue (vsize v) (uvalueToZ v) = v.</span>
<span class="c">Proof.</span>
<span class="c"> intros.</span>
<span class="c"> unfold ZToValue, uvalueToZ.</span>
<span class="c"> rewrite ZToWord_uwordToZ. destruct v; auto.</span>
<span class="c">Qed.</span>
<span class="c">Lemma valueToPos_posToValueAuto :</span>
<span class="c"> forall p, valueToPos (posToValueAuto p) = p.</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold valueToPos, posToValueAuto.</span>
<span class="c"> rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.</span>
<span class="c"> split. apply Zle_0_pos.</span>
<span class="c"> assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.</span>
<span class="c"> inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.</span>
<span class="c"> simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.</span>
<span class="c">Qed.</span>
<span class="c">Lemma valueToPos_posToValue :</span>
<span class="c"> forall p, valueToPos (posToValueAuto p) = p.</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold valueToPos, posToValueAuto.</span>
<span class="c"> rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.</span>
<span class="c"> split. apply Zle_0_pos.</span>
<span class="c"> assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.</span>
<span class="c"> inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.</span>
<span class="c"> simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.</span>
<span class="c">Qed.</span>
<span class="c">Lemma valueToInt_intToValue :</span>
<span class="c"> forall v,</span>
<span class="c"> valueToInt (intToValue v) = v.</span>
<span class="c">Proof.</span>
<span class="c"> intros.</span>
<span class="c"> unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned.</span>
<span class="c"> split. apply Int.unsigned_range_2.</span>
<span class="c"> assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2.</span>
<span class="c"> apply Z.lt_le_pred in H. apply H.</span>
<span class="c">Qed.</span>
<span class="c">Lemma valueToPtr_ptrToValue :</span>
<span class="c"> forall v,</span>
<span class="c"> valueToPtr (ptrToValue v) = v.</span>
<span class="c">Proof.</span>
<span class="c"> intros.</span>
<span class="c"> unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned.</span>
<span class="c"> split. apply Ptrofs.unsigned_range_2.</span>
<span class="c"> assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2.</span>
<span class="c"> apply Z.lt_le_pred in H. apply H.</span>
<span class="c">Qed.</span>
<span class="c">Lemma intToValue_valueToInt :</span>
<span class="c"> forall v,</span>
<span class="c"> vsize v = 32%nat -></span>
<span class="c"> intToValue (valueToInt v) = v.</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq.</span>
<span class="c"> unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize.</span>
<span class="c"> pose proof (uwordToZ_bound (vword v)).</span>
<span class="c"> rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto.</span>
<span class="c"> rewrite <- H. rewrite two_power_nat_equiv. apply H0.</span>
<span class="c">Qed.</span>
<span class="c">Lemma ptrToValue_valueToPtr :</span>
<span class="c"> forall v,</span>
<span class="c"> vsize v = 32%nat -></span>
<span class="c"> ptrToValue (valueToPtr v) = v.</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq.</span>
<span class="c"> unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize.</span>
<span class="c"> pose proof (uwordToZ_bound (vword v)).</span>
<span class="c"> rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto.</span>
<span class="c"> rewrite <- H. rewrite two_power_nat_equiv. apply H0.</span>
<span class="c">Qed.</span>
<span class="c">Lemma valToValue_lessdef :</span>
<span class="c"> forall v v',</span>
<span class="c"> valToValue v = Some v' -></span>
<span class="c"> val_value_lessdef v v'.</span>
<span class="c">Proof.</span>
<span class="c"> intros.</span>
<span class="c"> destruct v; try discriminate; constructor.</span>
<span class="c"> unfold valToValue in H. inversion H.</span>
<span class="c"> symmetry. apply valueToInt_intToValue.</span>
<span class="c"> inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate.</span>
<span class="c"> inv H1. symmetry. apply valueToPtr_ptrToValue.</span>
<span class="c"> inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate.</span>
<span class="c"> inv H1. apply Z.eqb_eq. apply Heqb0.</span>
<span class="c">Qed.</span>
<span class="c">Lemma boolToValue_ValueToBool :</span>
<span class="c"> forall b,</span>
<span class="c"> valueToBool (boolToValue 32 b) = b.</span>
<span class="c">Proof. destruct b; auto. Qed.</span>
<span class="c">Local Open Scope Z.</span>
<span class="c">Ltac word_op_value H :=</span>
<span class="c"> intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;</span>
<span class="c"> rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.</span>
<span class="c">Lemma zadd_vplus :</span>
<span class="c"> forall sz z1 z2,</span>
<span class="c"> (sz > 0)%nat -></span>
<span class="c"> uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz.</span>
<span class="c">Proof. word_op_value ZToWord_plus. Qed.</span>
<span class="c">Lemma zadd_vplus2 :</span>
<span class="c"> forall z1 z2,</span>
<span class="c"> vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2).</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl.</span>
<span class="c"> rewrite ZToWord_plus; auto.</span>
<span class="c">Qed.</span>
<span class="c">Lemma ZToValue_eq :</span>
<span class="c"> forall w1,</span>
<span class="c"> (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort.</span>
<span class="c">Lemma wordsize_32 :</span>
<span class="c"> Int.wordsize = 32%nat.</span>
<span class="c">Proof. auto. Qed.</span>
<span class="c">Lemma intadd_vplus :</span>
<span class="c"> forall i1 i2,</span>
<span class="c"> valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2.</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus.</span>
<span class="c"> rewrite <- Int.unsigned_repr_eq.</span>
<span class="c"> rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.</span>
<span class="c">Qed.</span>
<span class="c">(*Lemma intadd_vplus2 :</span>
<span class="c"> forall v1 v2 EQ,</span>
<span class="c"> vsize v1 = 32%nat -></span>
<span class="c"> Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ).</span>
<span class="c">Proof.</span>
<span class="c"> intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr).</span>
<span class="c"> rewrite (@vadd_vplus v1 v2 EQ). trivial.</span>
<span class="c"> unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)).</span>
<span class="c"> rewrite H in EQ. rewrite <- EQ in H0 at 3.*)</span>
<span class="c"> (*rewrite zadd_vplus3. trivia*)</span>
<span class="c">Lemma valadd_vplus :</span>
<span class="c"> forall v1 v2 v1' v2' v v' EQ,</span>
<span class="c"> val_value_lessdef v1 v1' -></span>
<span class="c"> val_value_lessdef v2 v2' -></span>
<span class="c"> Val.add v1 v2 = v -></span>
<span class="c"> vplus v1' v2' EQ = v' -></span>
<span class="c"> val_value_lessdef v v'.</span>
<span class="c">Proof.</span>
<span class="c"> intros. inv H; inv H0; constructor; simplify.</span>
<span class="c"> Abort.</span>
<span class="c">Lemma zsub_vminus :</span>
<span class="c"> forall sz z1 z2,</span>
<span class="c"> (sz > 0)%nat -></span>
<span class="c"> uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz.</span>
<span class="c">Proof. word_op_value ZToWord_minus. Qed.</span>
<span class="c">Lemma zmul_vmul :</span>
<span class="c"> forall sz z1 z2,</span>
<span class="c"> (sz > 0)%nat -></span>
<span class="c"> uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz.</span>
<span class="c">Proof. word_op_value ZToWord_mult. Qed.</span>
<span class="c">Local Open Scope N.</span>
<span class="c">Lemma zdiv_vdiv :</span>
<span class="c"> forall n1 n2,</span>
<span class="c"> n1 < 2 ^ 32 -></span>
<span class="c"> n2 < 2 ^ 32 -></span>
<span class="c"> n1 / n2 < 2 ^ 32 -></span>
<span class="c"> valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2.</span>
<span class="c">Proof.</span>
<span class="c"> intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv.</span>
<span class="c"> unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.</span>
<span class="c">Qed.</span>
<span class="c">Lemma ZToValue_valueToNat :</span>
<span class="c"> forall x sz,</span>
<span class="c"> (sz > 0)%nat -></span>
<span class="c"> (0 <= x < 2^(Z.of_nat sz))%Z -></span>
<span class="c"> valueToNat (ZToValue sz x) = Z.to_nat x.</span>
<span class="c">Proof.</span>
<span class="c"> destruct x; intros; unfold ZToValue, valueToNat; crush.</span>
<span class="c"> - rewrite wzero'_def. apply wordToNat_wzero.</span>
<span class="c"> - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial.</span>
<span class="c"> clear H1.</span>
<span class="c"> lazymatch goal with</span>
<span class="c"> | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H</span>
<span class="c"> end.</span>
<span class="c"> 2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. }</span>
<span class="c"> rewrite Z2Nat.inj_pow in H2; crush.</span>
<span class="c"> replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity.</span>
<span class="c"> rewrite Nat2Z.id in H2.</span>
<span class="c"> rewrite <- positive_nat_Z in H2.</span>
<span class="c"> apply Nat2Z.inj_lt in H2.</span>
<span class="c"> assumption.</span>
<span class="c">Qed.</span>
<span class="c">*)</span></span></span></pre>
</div>
</div></body>
</html>
|
