← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Equiv-From-M-Corr.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Equiv-From-M-Corr.lisp
 
1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2
;;;
 
3
;;; Section 4: Definition of m-correspondence
 
4
;;;
 
5
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
6
;;;
 
7
;;; 
 
8
;;; Definition of mapping-induced correspondence: 
 
9
;;; 
 
10
;;; In order for a Gem memory and and Rtm memory to be m-correspondent via m,
 
11
;;; the following conditions must hold:
 
12
;;;   
 
13
;;; - Correctness w.r.t. the types of the variables appearing into the memories: 
 
14
;;;   I.e., m must map boolean Gem variables into single Rtm variables, and integer Gem
 
15
;;;   variables into tuples of |*rns*| Rtm variables;
 
16
;;; 
 
17
;;; - Correctness w.r.t. the values and attributes of the variables appearing into the memories: 
 
18
;;;   for each entry of the mapping,
 
19
;;;   the values obtained by direct application of rns to the gem variable of the entry must 
 
20
;;;   match those of the rtm variables, and
 
21
;;;   the attributes of the rtm variables must match that of the rtm variable.
 
22
;;;
 
23
;;; - A mapping must have every Gem variable within the range of the Gem memory it references
 
24
;;;
 
25
;;; - A mapping must contain every variable of the Gem memory it references
 
26
;;;
 
27
;;; 
 
28
;;; Similar properties to the least two will be needed for the Rtm memories (e.g., every Rtm
 
29
;;; variable should be in the range of the Rtm memory), when proving properties about
 
30
;;; programs. We will insert them then. 
 
31
;;;
 
32
 
 
33
 
 
34
 
 
35
(in-package "ACL2")
 
36
 
 
37
(include-book "CRTcorollaries")
 
38
 
 
39
(in-theory (current-theory 'ground-zero))
 
40
 
 
41
(include-book "Mapping")
 
42
 
 
43
 
 
44
;;;
 
45
;;; Subsection 4.1: 
 
46
;;;
 
47
;;; Memories must be correspondent via m in terms of types
 
48
;;;
 
49
 
 
50
 
 
51
 
 
52
(defun correct-wrt-arity (m gem-typed-mem)
 
53
  (if (endp m)
 
54
      (null m) 
 
55
    (and
 
56
     (correct-type (type-0 m))
 
57
     (equal 
 
58
      (type-0 m) 
 
59
      (var-type (get-cell (gemvar-0 m) gem-typed-mem)))
 
60
     (correct-wrt-arity (cdr m) gem-typed-mem))))
 
61
 
 
62
(defthm correct-arity-all-i-need
 
63
 (implies
 
64
  (and
 
65
   (not (endp m))
 
66
   (correct-wrt-arity m gem-typed-mem))
 
67
  (and
 
68
   (correct-type (type-0 m))
 
69
   (equal
 
70
    (type-0 m) 
 
71
    (var-type (get-cell (gemvar-0 m) gem-typed-mem)))
 
72
   (not (null (var-attributes (rtmintvars-0 m) rtm-typed-mem)))
 
73
   (correct-wrt-arity (cdr m) gem-typed-mem))))
 
74
 
 
75
 
 
76
 
 
77
;;
 
78
;; Section 4.5:
 
79
;;
 
80
;; Every entry of the mapping must point to a coherent set of rtm variables, i.e. to a set of of rtm 
 
81
;; variables which share the same attribute.
 
82
;;
 
83
 
 
84
(defun get-common-value (l)
 
85
  (if (equal-elements (car l) (cdr l)) 
 
86
      (car l)
 
87
    'error-value))
 
88
 
 
89
(defthm if-every-element-matches-val-then-get-common-value-amounts-to-val
 
90
 (implies 
 
91
  (and 
 
92
   (true-listp l) 
 
93
   (not (null l)) 
 
94
   (equal-elements v l))  
 
95
  (equal (get-common-value l) v)))
 
96
 
 
97
(in-theory (disable if-every-element-matches-val-then-get-common-value-amounts-to-val))
 
98
 
 
99
 
 
100
(defun m-entries-point-to-good-rtm-var-sets (m rtm-typed-mem)
 
101
  (if (endp m)
 
102
      (null m)
 
103
    (and
 
104
     (not (endp (rtmintvars-0 m)))
 
105
     (true-listp (rtmintvars-0 m))
 
106
     (not (equal 'error-value (get-common-value (var-attributes (rtmintvars-0 m) rtm-typed-mem))))
 
107
     (m-entries-point-to-good-rtm-var-sets (cdr m) rtm-typed-mem))))
 
108
 
 
109
(in-theory (disable m-entries-point-to-good-rtm-var-sets))
 
110
 
 
111
 
 
112
 
 
113
;;;
 
114
;;; Subsection 4.6:
 
115
;;;
 
116
;;; Values and attributes must be correspondent via the mapping.
 
117
;;;
 
118
;;; In order to allow this definition, we first provide
 
119
;;; definitions of transformations of gem values into tuples of rtm values (by *rns*) and
 
120
;;; viceversa (by inverse application of *rns*).
 
121
;;;
 
122
;;; Notice that these transformations are actually just ``stubs'', since we provide a
 
123
;;; simplified form of axiomatization of the chinese remainder inversion theorem. 
 
124
;;; Additional hypothesis (e.g., boundedness of Gem and Rtm integers, and relations between such
 
125
;;; bounds) shall (and will) be added and taken into account when proving properties of programs.
 
126
;;; In the cureent state of the proof, however, we can limit ourselves to consider 'generic'
 
127
;;; transformations of Gem vars into tuples of Rtm vars, and their corresponding generic inverse.
 
128
;;; 
 
129
;;; However, since memories could contain nil cells, we have to lift our transformations, and
 
130
;;; the 'simplified axiomatization of CRT', to deal with nils. 
 
131
;;;
 
132
;;; We extend transformations so that nils transform into sequences of nils and viceversa.
 
133
;;; We lift the simplified CRT axiomatization to such extended version.
 
134
;;;
 
135
;;;
 
136
 
 
137
 
 
138
 
 
139
 
 
140
(defun make-null-list (l)
 
141
 (if (endp l)
 
142
     nil
 
143
     (cons nil (make-null-list (cdr l)))))
 
144
 
 
145
(defthm make-null-list-is-invariant-on-value-slicing (equal (make-null-list rtmvars) (make-null-list (var-values rtmvars rm))))
 
146
 
 
147
(in-theory (disable make-null-list-is-invariant-on-value-slicing))
 
148
 
 
149
(defun equal-values (val-list-1 val-list-2)
 
150
 (equal val-list-1 val-list-2))
 
151
 
 
152
(defun build-values-by-rns (gem-value rns)
 
153
 (if (endp rns)
 
154
     nil
 
155
     (cons (mod gem-value (car rns))
 
156
           (build-values-by-rns gem-value (cdr rns)))))
 
157
 
 
158
(in-theory (enable build-values-by-rns))
 
159
 
 
160
(defun mod-extended-for-nil (val1 val2)
 
161
 (if (null val1) 
 
162
     nil
 
163
     (mod val1 val2)))
 
164
 
 
165
(defun build-values-by-rns-extended-for-nil (gem-value rns)
 
166
 (if (endp rns)
 
167
     nil
 
168
     (cons (mod-extended-for-nil gem-value (car rns))
 
169
           (build-values-by-rns-extended-for-nil gem-value (cdr rns)))))
 
170
 
 
171
(defthm build-values-by-rns-extended-behaves-standardly-on-non-nils
 
172
 (implies 
 
173
  (not (null gem-value))
 
174
  (equal
 
175
    (build-values-by-rns-extended-for-nil gem-value rns) 
 
176
    (build-values-by-rns gem-value rns))))
 
177
 
 
178
(defthm build-values-by-rns-extended-for-nils-provides-integers-from-integer
 
179
 (implies
 
180
  (and
 
181
   (integerp val)
 
182
   (not (null rns))
 
183
   (integer-listp rns))
 
184
  (and
 
185
   (not (null (build-values-by-rns-extended-for-nil val rns)))
 
186
   (integer-listp (build-values-by-rns-extended-for-nil val rns)))))
 
187
 
 
188
 
 
189
 
 
190
 
 
191
(defun build-value-by-inverse-rns (rtm-values rns)
 
192
 (crtmod rtm-values rns))
 
193
 
 
194
 
 
195
(defun build-value-by-inverse-rns-extended-for-nil (rtm-values rns)
 
196
 (if   
 
197
     (integer-listp rtm-values)
 
198
     (crtmod rtm-values rns)
 
199
   nil))
 
200
 
 
201
 
 
202
(defthm build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
 
203
 (implies 
 
204
  (integer-listp rtm-values)
 
205
  (equal
 
206
    (build-value-by-inverse-rns-extended-for-nil rtm-values rns)
 
207
    (build-value-by-inverse-rns rtm-values rns))))
 
208
 
 
209
 
 
210
 
 
211
 
 
212
(defthm crt-inversion-inst
 
213
 (implies
 
214
  (and
 
215
   (rel-prime-moduli rns)
 
216
   (natp gem-value)
 
217
   (< gem-value (prod rns)))
 
218
 (equal 
 
219
  (build-value-by-inverse-rns (build-values-by-rns gem-value rns) rns) 
 
220
  gem-value))
 
221
 :hints (("Goal" :in-theory (enable crt-inversion))))
 
222
 
 
223
 
 
224
(in-theory (enable natp))
 
225
 
 
226
 
 
227
(defthm crt-inversion-extended-to-nils-in-integer-case
 
228
 (implies
 
229
  (and
 
230
   (rel-prime-moduli rns)
 
231
   (< gem-value (prod rns))
 
232
   (not (null rns))
 
233
   (integer-listp rns)
 
234
   (natp gem-value)) 
 
235
 (equal 
 
236
  (build-value-by-inverse-rns-extended-for-nil (build-values-by-rns-extended-for-nil gem-value rns) rns) 
 
237
  gem-value))
 
238
 :hints (("goal"
 
239
          :use (
 
240
                crt-inversion-inst
 
241
                build-values-by-rns-extended-behaves-standardly-on-non-nils 
 
242
                (:instance build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists 
 
243
                           (rtm-values (build-values-by-rns gem-value rns)))
 
244
                (:instance build-values-by-rns-extended-for-nils-provides-integers-from-integer 
 
245
                           (val gem-value))))))
 
246
 
 
247
(defthm crt-inversion-extended-to-nils-in-nil-case
 
248
 (implies
 
249
  (and
 
250
   (rel-prime-moduli rns)
 
251
   (not (null rns))
 
252
   (integer-listp rns)
 
253
   (null gem-value)) 
 
254
 (equal 
 
255
  (build-value-by-inverse-rns-extended-for-nil (build-values-by-rns-extended-for-nil gem-value rns) rns) 
 
256
  gem-value)))
 
257
 
 
258
(defthm crt-inversion-extended-to-nils
 
259
 (implies
 
260
  (and
 
261
   (rel-prime-moduli rns)
 
262
   (integer-listp rns)
 
263
   (not (null rns))
 
264
  (or 
 
265
   (null gem-value)
 
266
   (and
 
267
    (natp gem-value)
 
268
    (< gem-value (prod rns)))))
 
269
 (equal 
 
270
  (build-value-by-inverse-rns-extended-for-nil (build-values-by-rns-extended-for-nil gem-value rns) rns) 
 
271
  gem-value))
 
272
 :hints (("goal" 
 
273
          :cases ( 
 
274
                  (and (not (null gem-value)) (not (and (natp gem-value) (< gem-value (prod rns)))))
 
275
                  (null gem-value) 
 
276
                  (and (natp gem-value) (< gem-value (prod rns)))))
 
277
         ("Subgoal 2" :use crt-inversion-extended-to-nils-in-nil-case)
 
278
         ("subgoal 1" :use (:instance crt-inversion-extended-to-nils-in-integer-case))))
 
279
 
 
280
 
 
281
(in-theory (disable build-values-by-rns-extended-for-nil
 
282
                    build-values-by-rns
 
283
                    build-value-by-inverse-rns-extended-for-nil
 
284
                    build-value-by-inverse-rns
 
285
                    build-values-by-rns-extended-behaves-standardly-on-non-nils 
 
286
                    build-values-by-rns-extended-for-nils-provides-integers-from-integer
 
287
                    build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
 
288
                    crt-inversion-extended-to-nils-in-integer-case
 
289
                    crt-inversion-extended-to-nils-in-nil-case))
 
290
 
 
291
 
 
292
 
 
293
 
 
294
 
 
295
 
 
296
 
 
297
;;
 
298
;; m-correspondence definition w.r.t. values and attributes of memories
 
299
;;
 
300
 
 
301
 
 
302
 
 
303
 
 
304
(defun apply-direct-rns-to-value-according-to-type (gem-cell type)
 
305
 (cond
 
306
  ( (equal type 'bool)
 
307
    (list (var-value gem-cell)))
 
308
  ( (equal type 'int)
 
309
    (build-values-by-rns-extended-for-nil (var-value gem-cell) *rns*))
 
310
  ( t nil)))
 
311
 
 
312
 
 
313
 
 
314
(defun apply-invers-rns-to-values-according-to-type (vals type)
 
315
 (cond
 
316
  ( (equal type 'bool)
 
317
    (car vals) )
 
318
  ( (equal type 'int)
 
319
    (build-value-by-inverse-rns-extended-for-nil vals *rns*))
 
320
  ( t nil )))
 
321
 
 
322
 
 
323
 
 
324
 
 
325
(defun invert-cell (rtmvars rtm-typed-mem type)
 
326
  (if
 
327
     (equal-values
 
328
       (var-values     rtmvars rtm-typed-mem)
 
329
       (make-null-list rtmvars))
 
330
      (apply-invers-rns-to-values-according-to-type 
 
331
       (var-values rtmvars rtm-typed-mem)
 
332
       type)
 
333
    (make-cell
 
334
     (apply-invers-rns-to-values-according-to-type 
 
335
      (var-values rtmvars rtm-typed-mem)
 
336
      type)
 
337
     (get-common-value (var-attributes rtmvars rtm-typed-mem))
 
338
     type)))
 
339
 
 
340
(defun equal-values-and-attributes (gem-cell rtmvars rtm-typed-mem type)
 
341
(and
 
342
 (equal-values
 
343
  (var-values rtmvars rtm-typed-mem)
 
344
  (apply-direct-rns-to-value-according-to-type gem-cell type))
 
345
 (equal-elements 
 
346
  (var-attribute gem-cell)
 
347
  (var-attributes rtmvars rtm-typed-mem))))
 
348
 
 
349
 
 
350
 
 
351
(defthm apply-direct-rns-unfolding-for-integer-case
 
352
 (implies
 
353
  (equal type 'int)
 
354
  (equal 
 
355
   (apply-direct-rns-to-value-according-to-type gem-cell type) 
 
356
   (build-values-by-rns-extended-for-nil (var-value gem-cell) *rns*))))
 
357
 
 
358
(defthm apply-direct-rns-unfolding-for-boolean-case
 
359
 (implies
 
360
  (equal type 'bool)
 
361
  (equal 
 
362
   (apply-direct-rns-to-value-according-to-type gem-cell type) 
 
363
   (list (var-value gem-cell)))))
 
364
 
 
365
 
 
366
 
 
367
(defthm apply-inverse-rns-unfolding-for-integer-case
 
368
 (implies
 
369
  (equal type 'int)
 
370
  (equal (apply-invers-rns-to-values-according-to-type values type) 
 
371
         (build-value-by-inverse-rns-extended-for-nil values *rns*))))
 
372
 
 
373
 
 
374
(defthm apply-inverse-direct-retrieves-same-value-for-typed-cells
 
375
 (implies
 
376
  (and
 
377
  (rel-prime-moduli *rns*)
 
378
  (integer-listp *rns*)
 
379
  (not (null *rns*))
 
380
   (or
 
381
    (equal type 'int)
 
382
    (equal type 'bool))
 
383
   (or
 
384
    (and
 
385
     (natp (var-value gem-cell))
 
386
     (< (var-value gem-cell) (prod *rns*)))
 
387
    (null (var-value gem-cell))))
 
388
  (equal 
 
389
   (apply-invers-rns-to-values-according-to-type 
 
390
    (apply-direct-rns-to-value-according-to-type gem-cell type) type) 
 
391
   (var-value gem-cell)))
 
392
 :hints (("goal" :cases ( (equal type 'bool)
 
393
                          (equal type 'int)))
 
394
         ("subgoal 1"  
 
395
          :in-theory (disable null 
 
396
                              apply-inverse-rns-unfolding-for-integer-case
 
397
                              crt-inversion-extended-to-nils
 
398
                              apply-direct-rns-unfolding-for-integer-case
 
399
                              apply-direct-rns-to-value-according-to-type
 
400
                              var-value
 
401
                              apply-invers-rns-to-values-according-to-type
 
402
                              build-value-by-inverse-rns-extended-for-nil
 
403
                              build-values-by-rns-extended-for-nil)
 
404
          :use ((:instance apply-direct-rns-unfolding-for-integer-case)
 
405
                (:instance apply-inverse-rns-unfolding-for-integer-case (values (build-values-by-rns-extended-for-nil (var-value gem-cell) *rns*)))
 
406
                (:instance crt-inversion-extended-to-nils (rns *rns*) (gem-value (var-value gem-cell)))))))
 
407
 
 
408
 
 
409
 
 
410
 
 
411
(defthm inversion-for-empty-cell
 
412
 (implies
 
413
  (and
 
414
   (null cell)
 
415
   (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
 
416
   (correct-type type))
 
417
  (and
 
418
   (equal-values (var-values rtmvars rm) (make-null-list rtmvars))
 
419
   (equal (apply-invers-rns-to-values-according-to-type (var-values rtmvars rm) type) cell)))
 
420
 :hints (("goal" 
 
421
          :in-theory (enable make-null-list-is-invariant-on-value-slicing)
 
422
          :cases ( (equal type 'bool) (equal type 'int)))))
 
423
 
 
424
 
 
425
(in-theory (disable  make-cell))
 
426
 
 
427
 
 
428
(defthm ad-hoc-2-for-inversion-of-one-nonempty-cell-by-decode
 
429
  (implies 
 
430
   (and (not (null bui)) (integer-listp bui)) 
 
431
   (not (equal (make-null-list l) bui))))
 
432
 
 
433
 
 
434
(defthm ad-hoc-3-for-inversion-of-one-nonempty-cell-by-decode
 
435
  (implies 
 
436
   (integerp (var-value cell)) 
 
437
   (not (equal (make-null-list l) (build-values-by-rns-extended-for-nil (var-value cell) *rns*))))
 
438
  :hints (("goal" :use ((:instance build-values-by-rns-extended-for-nils-provides-integers-from-integer 
 
439
                                   (val (var-value cell)) (rns *rns*))
 
440
                        (:instance ad-hoc-2-for-inversion-of-one-nonempty-cell-by-decode 
 
441
                                   (l l) 
 
442
                                   (bui (build-values-by-rns-extended-for-nil (var-value cell) *rns*)))))))
 
443
 
 
444
(defthm nonempty-cell-is-not-mapped-into-nils-by-rns
 
445
  (implies
 
446
   (and
 
447
    (true-listp (var-attributes rtmvars rm))  
 
448
    (not (null (var-attributes rtmvars rm)))  
 
449
    (is-mem-cell-p cell)
 
450
    (not (null cell))
 
451
    (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
 
452
    (equal-elements (var-attribute cell) (var-attributes rtmvars rm)) 
 
453
    (equal type (var-type cell)))
 
454
    (not (equal-values (var-values rtmvars rm) (make-null-list rtmvars))))
 
455
 :hints (("goal" :cases ( (equal type 'bool) (equal type 'int)))))
 
456
 
 
457
 
 
458
 
 
459
(in-theory (disable my-or-2 my-or-3))
 
460
 
 
461
(defthm silly00
 
462
  (IMPLIES (AND (TRUE-LISTP CELL6)
 
463
                (EQUAL (+ 3 (LEN CELL6)) 3))
 
464
           (NOT CELL6))
 
465
  :rule-classes nil)
 
466
 
 
467
(defthm reconstruction-of-cell
 
468
 (implies
 
469
  (is-mem-cell-p cell)
 
470
  (equal
 
471
   (make-cell
 
472
    (var-value cell)
 
473
    (var-attribute cell)
 
474
    (var-type cell))
 
475
   cell))
 
476
  :hints (("Subgoal 1.1" :use silly00)
 
477
          ("Subgoal 2.1" :use silly00)
 
478
          ("goal" 
 
479
           :in-theory                   
 
480
           (union-theories (current-theory 'ground-zero)
 
481
           '((:definition is-mem-cell-p)
 
482
             (:definition make-cell)
 
483
             (:definition var-type)
 
484
             (:definition var-value)
 
485
             (:definition var-attribute)))))
 
486
  :rule-classes nil)
 
487
 
 
488
 
 
489
 
 
490
(defthm nonempty-rtm-vars-which-correspond-to-gem-var-by-values-and-atributes-map-back-to-gem-var
 
491
  (implies
 
492
   (and
 
493
    (rel-prime-moduli *rns*)
 
494
    (integer-listp *rns*)
 
495
    (not (null *rns*))
 
496
    (true-listp (var-attributes rtmvars rm)) 
 
497
    (not (null (var-attributes rtmvars rm)))  
 
498
    (is-mem-cell-p cell)
 
499
    (not (null cell))
 
500
    (natp (var-value cell))
 
501
    (< (var-value cell) (prod *rns*))
 
502
    (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
 
503
    (equal-elements (var-attribute cell) (var-attributes rtmvars rm)) 
 
504
    (equal type (var-type cell)))
 
505
    (equal 
 
506
     (make-cell
 
507
      (apply-invers-rns-to-values-according-to-type (var-values rtmvars rm) type)
 
508
      (get-common-value (var-attributes rtmvars rm))
 
509
      type)
 
510
     cell))
 
511
  :hints (("goal" :in-theory '((:definition my-or-2)
 
512
                               (:definition is-mem-cell-p)
 
513
                               (:definition natp)
 
514
                               (:definition equal-values)
 
515
                               (:definition is-mem-cell-p))
 
516
                  :use (reconstruction-of-cell
 
517
                        (:instance if-every-element-matches-val-then-get-common-value-amounts-to-val
 
518
                                  (l (var-attributes rtmvars rm)) (v (var-attribute cell)))
 
519
                        (:instance apply-inverse-direct-retrieves-same-value-for-typed-cells
 
520
                                   (type type) (gem-cell cell))))))
 
521
 
 
522
 
 
523
 
 
524
 
 
525
        
 
526
 
 
527
 
 
528
 
 
529
 
 
530
 
 
531
(defthm decode-inversion-for-nonempty-gem-cell
 
532
  (implies
 
533
   (and
 
534
    (rel-prime-moduli *rns*)
 
535
    (integer-listp *rns*)
 
536
    (not (null *rns*))
 
537
    (true-listp (var-attributes rtmvars rm)) 
 
538
    (not (null (var-attributes rtmvars rm)))  
 
539
    (is-mem-cell-p cell)
 
540
    (not (null cell))
 
541
    (natp (var-value cell))
 
542
    (< (var-value cell) (prod *rns*))
 
543
    (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
 
544
    (equal-elements (var-attribute cell) (var-attributes rtmvars rm)) 
 
545
    (equal type (var-type cell)))
 
546
   (and
 
547
    (not (equal-values (var-values rtmvars rm) (make-null-list rtmvars)))
 
548
    (equal 
 
549
     (make-cell
 
550
      (apply-invers-rns-to-values-according-to-type (var-values rtmvars rm) type)
 
551
      (get-common-value (var-attributes rtmvars rm))
 
552
      type)
 
553
     cell)))
 
554
  :hints (("goal" :use (nonempty-cell-is-not-mapped-into-nils-by-rns 
 
555
                        nonempty-rtm-vars-which-correspond-to-gem-var-by-values-and-atributes-map-back-to-gem-var))))
 
556
 
 
557
 
 
558
 
 
559
 
 
560
 
 
561
 
 
562
(defthm var-attributes-always-true-listp
 
563
 (true-listp (var-attributes rtmvars rtm-typed-mem)))
 
564
 
 
565
(defun bounded-value (cell)
 
566
  (if (null cell) 
 
567
      t
 
568
    (and (natp (var-value cell)) (< (var-value cell) (prod *rns*)))))
 
569
 
 
570
(defthm invert-cell-inverts-for-m-correspondents
 
571
 (implies
 
572
  (and
 
573
   (rel-prime-moduli *rns*)
 
574
   (integer-listp *rns*)
 
575
   (not (null *rns*))
 
576
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
577
   (equal type (var-type gem-cell))
 
578
   (correct-type type)
 
579
   (or (null gem-cell) (is-mem-cell-p gem-cell))
 
580
   (bounded-value gem-cell)
 
581
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
582
  (equal 
 
583
   (invert-cell rtmvars rtm-typed-mem type)
 
584
   gem-cell))
 
585
 :hints (("Goal" 
 
586
          :in-theory (disable equal-values)
 
587
          :use ( var-attributes-always-true-listp
 
588
                 (:instance decode-inversion-for-nonempty-gem-cell 
 
589
                            (cell gem-cell)
 
590
                            (rm rtm-typed-mem))
 
591
                 (:instance inversion-for-empty-cell 
 
592
                            (cell gem-cell)
 
593
                            (rm rtm-typed-mem))))))
 
594
 
 
595
 
 
596
(defun is-typed-amem-p (mem)
 
597
  (if (endp mem)
 
598
      (null mem)
 
599
    (and
 
600
     (consp (car mem))
 
601
     (is-mem-cell-p (cdr (car mem)))
 
602
     (is-typed-amem-p (cdr mem)))))
 
603
 
 
604
(in-theory (enable get-cell))
 
605
 
 
606
(defthm any-cell-of-a-typed-mem-is-nil-or-a-typed-cell
 
607
 (implies
 
608
  (is-typed-amem-p gem-typed-mem)
 
609
  (or
 
610
   (and
 
611
    (null (assoc-equal v gem-typed-mem))
 
612
    (null (get-cell v gem-typed-mem)))
 
613
   (is-mem-cell-p (get-cell v gem-typed-mem))))
 
614
 :rule-classes nil)
 
615
 
 
616
 
 
617
 
 
618
 
 
619
 
 
620
 
 
621
 
 
622
 
 
623
(defun m-correspondent-values-p (m gem-typed-mem rtm-typed-mem)
 
624
 (cond
 
625
  ( (endp m)
 
626
    (null m) )
 
627
  ( t
 
628
    (and
 
629
     (equal-values-and-attributes 
 
630
      (get-cell (gemvar-0 m) gem-typed-mem) 
 
631
      (rtmintvars-0 m) 
 
632
      rtm-typed-mem (type-0 m))
 
633
     (m-correspondent-values-p (cdr m)  gem-typed-mem rtm-typed-mem)))))
 
634
 
 
635
(defun decode (m rtm-typed-mem)
 
636
 (if
 
637
  (endp m)
 
638
    nil 
 
639
    (put-cell
 
640
     (gemvar-0 m)
 
641
     (invert-cell (rtmintvars-0 m) rtm-typed-mem (type-0 m))
 
642
     (decode (cdr m) rtm-typed-mem))))
 
643
 
 
644
 
 
645
(defthm silly1 
 
646
     (equal (caar m) (gemvar-0 m)))
 
647
 
 
648
(in-theory (disable silly1))
 
649
 
 
650
(defthm silly2
 
651
  (implies
 
652
   (correct-wrt-arity m gem-typed-mem)
 
653
   (correct-wrt-arity (cdr m) gem-typed-mem)))
 
654
 
 
655
(in-theory (disable silly1 silly2))
 
656
 
 
657
(defun bounded-amem-p (mem)
 
658
  (if
 
659
      (endp mem)
 
660
      (null mem)
 
661
    (and (bounded-value (cdr (car mem)))
 
662
         (bounded-amem-p (cdr mem)))))
 
663
   
 
664
(defthm any-cell-of-bounded-mem-is-bounded
 
665
 (implies
 
666
  (bounded-amem-p gem-typed-mem)
 
667
  (bounded-value (get-cell v gem-typed-mem)))
 
668
 :rule-classes nil)
 
669
 
 
670
(defthm decode-equals-retrieve-vars
 
671
 (implies
 
672
  (and
 
673
   (rel-prime-moduli *rns*)
 
674
   (integer-listp *rns*)
 
675
   (not (null *rns*))
 
676
   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem)
 
677
   (is-typed-amem-p gem-typed-mem)
 
678
   (bounded-amem-p gem-typed-mem)
 
679
   (correct-wrt-arity m gem-typed-mem))
 
680
  (equal
 
681
   (decode m rtm-typed-mem)
 
682
   (retrieve-vars m gem-typed-mem)))
 
683
 :hints (("Goal" :induct (len m))
 
684
         ("Subgoal *1/1"
 
685
          :in-theory nil 
 
686
          :use (silly1
 
687
                silly2
 
688
                decode
 
689
                (:instance retrieve-vars (vars m) (mem gem-typed-mem))
 
690
                m-correspondent-values-p
 
691
                (:instance any-cell-of-a-typed-mem-is-nil-or-a-typed-cell (v (gemvar-0 m)))
 
692
                (:instance any-cell-of-bounded-mem-is-bounded (v (gemvar-0 m)))
 
693
                correct-arity-all-i-need
 
694
                (:instance invert-cell-inverts-for-m-correspondents
 
695
                           (rtmvars (rtmintvars-0 m))
 
696
                           (gem-cell (get-cell (gemvar-0 m) gem-typed-mem))
 
697
                           (type (type-0 m)))))))
 
698
 
 
699
 
 
700
(defthm decode-retrieves-gem-memory
 
701
 (implies
 
702
  (and
 
703
   (rel-prime-moduli *rns*)
 
704
   (integer-listp *rns*)
 
705
   (not (null *rns*))
 
706
   (vars-inclusion gem-typed-mem m)
 
707
   (vars-inclusion m gem-typed-mem)
 
708
   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem)
 
709
   (is-typed-amem-p gem-typed-mem)
 
710
   (bounded-amem-p gem-typed-mem)
 
711
   (correct-wrt-arity m gem-typed-mem))
 
712
  (equal-memories (decode m rtm-typed-mem) gem-typed-mem))
 
713
 :hints (("Goal" :in-theory (enable retrieving-keeps-equality))))
 
714
 
 
715
 
 
716
(defun projectiocell (cell attr)
 
717
 (if (null cell)
 
718
     cell   
 
719
     (if (equal (var-attribute cell) attr)
 
720
         cell
 
721
         nil )))
 
722
 
 
723
(defun projectio (mem attr)
 
724
  (if (endp mem)
 
725
      nil
 
726
      (put-cell (caar mem) 
 
727
                (projectiocell (cdr (car mem))  attr) 
 
728
                (projectio (cdr mem) attr))))
 
729
 
 
730
 
 
731
 
 
732
(defthm cell-of-projected-mem-is-projected-cell
 
733
 (equal 
 
734
  (get-cell cell (projectio mem attr))
 
735
  (projectiocell (get-cell cell mem) attr)))
 
736
 
 
737
 
 
738
 
 
739
 
 
740
(defthm projection-of-null-list-is-null-list
 
741
 (implies
 
742
   (equal-values (var-values l rtm-typed-mem) (make-null-list l))
 
743
   (equal-values (var-values l (projectio rtm-typed-mem attr)) (make-null-list l))))
 
744
 
 
745
 
 
746
(defthm null-cell-corresponds-to-null-lists-of-values
 
747
 (implies
 
748
  (and
 
749
   (null gem-cell)
 
750
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
751
  (equal-values (var-values rtmvars rtm-typed-mem) (make-null-list rtmvars)))
 
752
 :hints (("Goal" :in-theory (disable get-cell var-value var-attribute ))))
 
753
 
 
754
 
 
755
 
 
756
(defthm project-invert-commute-for-empty-cell
 
757
 (implies
 
758
  (and
 
759
   (null gem-cell)
 
760
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
761
 (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
 
762
        (invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
 
763
 :hints (("Goal" :use (null-cell-corresponds-to-null-lists-of-values
 
764
                       (:instance projection-of-null-list-is-null-list (l rtmvars))))))
 
765
 
 
766
 
 
767
 
 
768
(defthm rtmvars-correspondent-to-nonemptycell-is-not-emptylist
 
769
 (implies
 
770
  (and
 
771
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
772
   (equal type (var-type gem-cell))
 
773
   (correct-type type)
 
774
   (not (null gem-cell))
 
775
   (equal (var-attribute gem-cell) attr)
 
776
   (is-mem-cell-p gem-cell)
 
777
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
778
  (not
 
779
   (equal-values
 
780
    (var-values rtmvars rtm-typed-mem)
 
781
    (make-null-list rtmvars)))))
 
782
 
 
783
 
 
784
 
 
785
 
 
786
(defthm values-remain-the-same-if-correspondent-attrs
 
787
 (implies
 
788
  (and
 
789
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
790
   (equal type (var-type gem-cell))
 
791
   (correct-type type)
 
792
   (not (null gem-cell))
 
793
   (equal (var-attribute gem-cell) attr)
 
794
   (is-mem-cell-p gem-cell)
 
795
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
796
 (equal
 
797
  (var-values rtmvars (projectio rtm-typed-mem attr))
 
798
  (var-values rtmvars rtm-typed-mem)))
 
799
 :hints (("Goal" :do-not '(generalize))))
 
800
 
 
801
 
 
802
 
 
803
(defthm attributes-same-1
 
804
 (implies
 
805
  (equal-elements attr (var-attributes rtmvars rtm-typed-mem))
 
806
     (equal
 
807
      (var-attributes rtmvars (projectio rtm-typed-mem attr))
 
808
      (var-attributes rtmvars rtm-typed-mem))))
 
809
 
 
810
 
 
811
 
 
812
 
 
813
(defthm inversion-2-for-nonempty-projected-on-same-attr
 
814
 (implies
 
815
  (and
 
816
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
817
   (equal type (var-type gem-cell))
 
818
   (correct-type type)
 
819
   (not (null gem-cell))
 
820
   (equal (var-attribute gem-cell) attr)
 
821
   (is-mem-cell-p gem-cell)
 
822
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
823
 (equal (invert-cell rtmvars (projectio rtm-typed-mem attr) type) 
 
824
        (invert-cell rtmvars rtm-typed-mem type)))
 
825
 :hints (("Goal" :in-theory nil
 
826
          ;; modified for Version  2.7 fertilization
 
827
          :use (
 
828
                (:instance invert-cell (rtm-typed-mem (projectio rtm-typed-mem attr)))
 
829
                invert-cell
 
830
                equal-values-and-attributes
 
831
                (:instance attributes-same-1 (attr (var-attribute gem-cell)))
 
832
                rtmvars-correspondent-to-nonemptycell-is-not-emptylist
 
833
                values-remain-the-same-if-correspondent-attrs)
 
834
          :expand ((:free (x) (hide x))))))
 
835
 
 
836
 
 
837
(defthm inversion-1-for-nonempty-projected-on-different-attr
 
838
 (implies
 
839
  (and
 
840
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
841
   (equal type (var-type gem-cell))
 
842
   (correct-type type)
 
843
   (not (null gem-cell))
 
844
   (not (equal (var-attribute gem-cell) attr))
 
845
   (is-mem-cell-p gem-cell)
 
846
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
847
 (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
 
848
        nil)))
 
849
 
 
850
 
 
851
(defthm projecting-on-different-attr-gets-nils
 
852
 (implies
 
853
  (and
 
854
   (not (equal (var-attribute gem-cell) attr))
 
855
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
856
  (equal-values
 
857
   (var-values rtmvars (projectio rtm-typed-mem attr))
 
858
   (make-null-list rtmvars))))
 
859
   
 
860
 
 
861
 
 
862
(defthm decode-one-entry-of-null-list-is-nil
 
863
(implies
 
864
 (and
 
865
  (true-listp l)
 
866
  (not (endp l))
 
867
  (equal-values (var-values l rtm-typed-mem) (make-null-list l)))
 
868
 (equal (apply-invers-rns-to-values-according-to-type (var-values l rtm-typed-mem) ty) nil))
 
869
 :hints(("goal" :in-theory (enable build-value-by-inverse-rns-extended-for-nil))))
 
870
 
 
871
 
 
872
(defthm inversion-2-for-nonempty-projected-on-different-attr
 
873
 (implies
 
874
  (and
 
875
   (true-listp rtmvars)
 
876
   (not (null rtmvars))
 
877
   (not (equal (var-attribute gem-cell) attr))
 
878
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
879
 (equal (invert-cell rtmvars (projectio rtm-typed-mem attr) type) 
 
880
        nil))
 
881
 :hints (("Goal" :use
 
882
          ((:instance decode-one-entry-of-null-list-is-nil
 
883
                      (l rtmvars)
 
884
                      (rtm-typed-mem  (projectio rtm-typed-mem attr))
 
885
                      (ty type))
 
886
           (:instance invert-cell (rtm-typed-mem (projectio rtm-typed-mem attr)))
 
887
           projecting-on-different-attr-gets-nils))))
 
888
 
 
889
 
 
890
 
 
891
 
 
892
(defthm inversion-for-nonempty-projected-on-different-attr
 
893
 (implies
 
894
  (and
 
895
   (true-listp rtmvars)
 
896
   (not (null rtmvars))
 
897
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
898
   (equal type (var-type gem-cell))
 
899
   (correct-type type)
 
900
   (not (null gem-cell))
 
901
   (not (equal (var-attribute gem-cell) attr))
 
902
   (is-mem-cell-p gem-cell)
 
903
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
904
 (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
 
905
        (invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
 
906
 :hints (("Goal"
 
907
          :in-theory nil
 
908
          :use 
 
909
          (inversion-1-for-nonempty-projected-on-different-attr
 
910
           inversion-2-for-nonempty-projected-on-different-attr))))
 
911
 
 
912
 
 
913
 
 
914
 
 
915
 
 
916
(defthm project-invert-commuting
 
917
 (implies
 
918
  (and
 
919
   (true-listp rtmvars)
 
920
   (not (null rtmvars))
 
921
   (not (null (var-attributes rtmvars rtm-typed-mem)))
 
922
   (or
 
923
    (null gem-cell)
 
924
    (equal type (var-type gem-cell)))
 
925
   (correct-type type)
 
926
   (or (null gem-cell) (is-mem-cell-p gem-cell))
 
927
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
928
 (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
 
929
        (invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
 
930
 :hints (("Goal" :cases
 
931
          ( (and (not (null gem-cell)) (not (equal (var-attribute gem-cell) attr)))
 
932
            (and (not (null gem-cell)) (equal (var-attribute gem-cell) attr))))
 
933
         ("Subgoal 3" :use project-invert-commute-for-empty-cell)
 
934
         ("Subgoal 2" :use inversion-for-nonempty-projected-on-different-attr)))
 
935
 
 
936
(defthm letssimplify
 
937
  (implies
 
938
  (and
 
939
   (true-listp rtmvars)
 
940
   (not (null rtmvars)))
 
941
   (not (null (var-attributes rtmvars rtm-typed-mem)))))
 
942
 
 
943
  
 
944
(defthm project-invert-commuting-better
 
945
 (implies
 
946
  (and
 
947
   (true-listp rtmvars)
 
948
   (not (null rtmvars))
 
949
   (or
 
950
    (null gem-cell)
 
951
    (equal type (var-type gem-cell)))
 
952
   (correct-type type)
 
953
   (or (null gem-cell) (is-mem-cell-p gem-cell))
 
954
   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
 
955
 (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
 
956
        (invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
 
957
 :hints (("Goal" :use (letssimplify project-invert-commuting))))
 
958
 
 
959
 
 
960
 
 
961
(in-theory (enable
 
962
                   m-entries-point-to-good-rtm-var-sets
 
963
                   m-correspondent-values-p))
 
964
 
 
965
(in-theory (disable gemvar-0 rtmintvars-0))
 
966
 
 
967
(defthm lil-helper
 
968
 (implies
 
969
  (and
 
970
   (not (endp m))
 
971
   (is-typed-amem-p gem-typed-mem)
 
972
   (correct-wrt-arity m gem-typed-mem)
 
973
   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
 
974
   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem))
 
975
  (and
 
976
   (or
 
977
    (null (get-cell (gemvar-0 m) gem-typed-mem))
 
978
    (is-mem-cell-p (get-cell (gemvar-0 m) gem-typed-mem)))
 
979
   (true-listp (rtmintvars-0 m))
 
980
   (not (null (rtmintvars-0 m)))
 
981
   (correct-type (type-0 m))
 
982
   (or
 
983
    (null (get-cell (gemvar-0 m) gem-typed-mem))
 
984
    (equal (type-0 m) (var-type (get-cell (gemvar-0 m) gem-typed-mem))))
 
985
   (equal-values-and-attributes 
 
986
    (get-cell (gemvar-0 m) gem-typed-mem)
 
987
    (rtmintvars-0 m)
 
988
    rtm-typed-mem
 
989
    (type-0 m))
 
990
   (correct-wrt-arity (cdr m) gem-typed-mem)
 
991
   (m-entries-point-to-good-rtm-var-sets (cdr m) rtm-typed-mem)
 
992
   (m-correspondent-values-p (cdr m) gem-typed-mem rtm-typed-mem)))
 
993
 :hints (("Goal" :use (:instance any-cell-of-a-typed-mem-is-nil-or-a-typed-cell
 
994
                                 (v (gemvar-0 m)))))
 
995
 :rule-classes nil)
 
996
 
 
997
 
 
998
 
 
999
(defun decode-projection (m rtm-typed-mem attr)
 
1000
  (if (endp m)
 
1001
      nil
 
1002
    (put-cell (gemvar-0 m)
 
1003
              (projectiocell
 
1004
               (invert-cell 
 
1005
                (rtmintvars-0 m) 
 
1006
                rtm-typed-mem
 
1007
                (type-0 m))
 
1008
               attr)
 
1009
              (decode-projection (cdr m) rtm-typed-mem attr))))
 
1010
 
 
1011
 
 
1012
(in-theory (enable m-entries-point-to-good-rtm-var-sets))
 
1013
 
 
1014
(defthm project-of-decode-is-decode-projection
 
1015
  (equal 
 
1016
   (projectio (decode m rtm-typed-mem) attr) 
 
1017
   (decode-projection m rtm-typed-mem attr)))
 
1018
 
 
1019
 
 
1020
(defthm decode-projection-is-decode-of-projection
 
1021
 (implies
 
1022
  (and
 
1023
   (is-typed-amem-p gem-typed-mem)
 
1024
   (correct-wrt-arity m gem-typed-mem)
 
1025
   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
 
1026
   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem))
 
1027
 (equal
 
1028
  (decode-projection  m rtm-typed-mem attr)
 
1029
  (decode m (projectio rtm-typed-mem attr))))
 
1030
 :hints (("Goal"  :induct (len m))
 
1031
         ("Subgoal *1/1" :in-theory nil
 
1032
          :use (lil-helper
 
1033
                (:instance decode (rtm-typed-mem  (projectio rtm-typed-mem attr)))
 
1034
                decode-projection
 
1035
                               (:instance project-invert-commuting-better
 
1036
                                 (type (type-0 m))
 
1037
                                 (gem-cell (get-cell (gemvar-0 m) gem-typed-mem))
 
1038
                                 (rtmvars (rtmintvars-0 m)))))))
 
1039
 
 
1040
 
 
1041
 
 
1042
(defthm decode-project-commuting
 
1043
 (implies
 
1044
  (and
 
1045
   (is-typed-amem-p gem-typed-mem)
 
1046
   (correct-wrt-arity m gem-typed-mem)
 
1047
   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
 
1048
   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem))
 
1049
 (equal
 
1050
  (projectio (decode m rtm-typed-mem) attr)
 
1051
  (decode m (projectio rtm-typed-mem attr)))))
 
1052
 
 
1053
 
 
1054
 
 
1055
(in-theory (disable get-cell put-cell))
 
1056
 
 
1057
(defthm equalwrt-holds-on-project
 
1058
 (implies
 
1059
  (equal-wrt-vars m0 m1 m2)
 
1060
  (equal-wrt-vars m0 (projectio m1 attr) (projectio m2 attr))))
 
1061
 
 
1062
(defthm projectio-keeps-caars
 
1063
  (same-caars-p m0 (projectio m0 attr))
 
1064
 :hints (("Goal" :in-theory (enable put-cell))))
 
1065
 
 
1066
 
 
1067
(defthm equalwrt-holds-on-project-all
 
1068
 (implies
 
1069
  (equal-wrt-vars m0 m1 m2)
 
1070
  (equal-wrt-vars (projectio m0 attr) m1 m2))
 
1071
 :hints (("Goal" :use (:instance if-same-caars-same-equality-wrt-vars
 
1072
                                 (vars1 m0)
 
1073
                                 (vars2 (projectio m0 attr))
 
1074
                                 (mem1 m1)
 
1075
                                 (mem2 m2)))))
 
1076
 
 
1077
(defthm equalwrt-holds-on-project-all-all
 
1078
 (implies
 
1079
  (equal-wrt-vars m0 m1 m2)
 
1080
  (equal-wrt-vars (projectio m0 attr) (projectio m1 attr) (projectio m2 attr)))
 
1081
 :hints (("Goal" :use (:instance if-same-caars-same-equality-wrt-vars
 
1082
                                 (vars1 m0)
 
1083
                                 (vars2 (projectio m0 attr))
 
1084
                                 (mem1 m1)
 
1085
                                 (mem2 m2)))))
 
1086
 
 
1087
(defthm equal-memories-holds-by-projection
 
1088
 (implies
 
1089
  (equal-memories m1 m2)
 
1090
  (equal-memories (projectio m1 attr) (projectio m2 attr))))
 
1091
 
 
1092
 
 
1093
 
 
1094
 
 
1095
(defthm equalities-on-io
 
1096
 (implies
 
1097
  (and
 
1098
   (rel-prime-moduli *rns*)
 
1099
   (integer-listp *rns*)
 
1100
   (not (null *rns*))
 
1101
   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
 
1102
   (vars-inclusion gem-typed-mem m)
 
1103
   (vars-inclusion m gem-typed-mem)
 
1104
   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem)
 
1105
   (is-typed-amem-p gem-typed-mem)
 
1106
   (bounded-amem-p gem-typed-mem)
 
1107
   (correct-wrt-arity m gem-typed-mem))
 
1108
  (equal-memories (decode m (projectio rtm-typed-mem attr)) (projectio gem-typed-mem attr)))
 
1109
 :hints (("Goal"
 
1110
          :in-theory (enable
 
1111
                      equal-memories-commutative
 
1112
                      retrieving-keeps-equality
 
1113
                      decode-equals-retrieve-vars
 
1114
                      equal-wrt-vars-reflexive
 
1115
                      equal-wrt-vars-transitive
 
1116
                      equalwrt-holds-on-project-all)
 
1117
          :use ( (:instance equal-memories-holds-by-projection
 
1118
                            (m1 (decode m rtm-typed-mem))
 
1119
                            (m2 gem-typed-mem))))))
 
1120
 
 
1121
 
 
1122
(defthm fact-bout-rns-v0
 
1123
  (and
 
1124
   (integer-listp *rns*)
 
1125
   (rel-prime-moduli *rns*)
 
1126
   (posp-all *rns*)
 
1127
   (not (null *rns*))
 
1128
   (natp (prod *rns*))
 
1129
   (> (prod *rns*) 1))
 
1130
  :hints (("Goal" :in-theory (enable prod posp rel-prime-moduli rel-prime-all rel-prime g-c-d
 
1131
  posp-all
 
1132
  (:executable-counterpart nonneg-int-gcd))))
 
1133
  :rule-classes nil)
 
1134
 
 
1135
(defun append-lists (list-of-lists)
 
1136
 (if (endp list-of-lists)
 
1137
     nil
 
1138
     (append (car list-of-lists)
 
1139
             (append-lists (cdr list-of-lists)))))
 
1140
 
 
1141
(defun retrieve-gemvars (m)
 
1142
  (if
 
1143
      (endp m)
 
1144
      nil
 
1145
    (cons (gemvar-0 m) (retrieve-gemvars (cdr m)))))
 
1146
 
 
1147
(defun retrieve-rtmvars (m)
 
1148
  (if (endp m)
 
1149
      nil
 
1150
    (cons (cdr (car m))
 
1151
          (retrieve-rtmvars (cdr m)))))
 
1152
 
 
1153
(defun gem-variables (m) (retrieve-gemvars m))
 
1154
(defun rtm-variables (m) (append-lists (retrieve-rtmvars m)))
 
1155
 
 
1156
(defun same-vars (m1 m2) 
 
1157
 (and 
 
1158
  (vars-inclusion m1 m2) 
 
1159
  (vars-inclusion m2 m1)))
 
1160
 
 
1161
(defun member-equal-bool (el l)
 
1162
 (declare (xargs :guard (true-listp l)))
 
1163
 (cond ((endp l) nil)
 
1164
       ((equal el (car l)) t)
 
1165
       (t (member-equal-bool el (cdr l)))))
 
1166
 
 
1167
(defun no-tmp-into-mapping (m)
 
1168
  (if (endp m)
 
1169
      t
 
1170
    (and
 
1171
     (not (member-equal-bool 'tmp (rtmintvars-0 m)))
 
1172
     (no-tmp-into-mapping (cdr m)))))
 
1173
 
 
1174
(defun no-duplicates-p (l)
 
1175
 (if (endp l)
 
1176
     t
 
1177
     (and (not (member-equal-bool (car l) (cdr l)))
 
1178
          (no-duplicates-p (cdr l)))))
 
1179
 
 
1180
 
 
1181
(defun apply-direct-rns-to-value-depending-on-type (gemvalue type)
 
1182
 (cond ( (equal type 'bool) (list gemvalue) )
 
1183
       ( (equal type 'int)  (build-values-by-rns-extended-for-nil gemvalue *rns*) )
 
1184
       ( t nil )))
 
1185
 
 
1186
(defun represent-same-values-p (gemvalue rtmvalues type)
 
1187
 (equal-values
 
1188
  rtmvalues
 
1189
  (apply-direct-rns-to-value-depending-on-type gemvalue type)))
 
1190
 
 
1191
 
 
1192
(defun m-correspondent-vals-p (m gem-typed-mem rtm-typed-mem)
 
1193
 (cond
 
1194
  ( (endp m)
 
1195
    (null m) )
 
1196
  ( t
 
1197
    (and
 
1198
     (represent-same-values-p
 
1199
      (var-value (get-cell (gemvar-0 m) gem-typed-mem))
 
1200
      (var-values (rtmintvars-0 m) rtm-typed-mem)
 
1201
      (type-0 m))
 
1202
     (m-correspondent-vals-p (cdr m)  gem-typed-mem rtm-typed-mem)))))
 
1203
 
 
1204
 
 
1205
(defun attributes-correspondence (m gem-typed-mem rtm-typed-mem)
 
1206
  (if (endp m)
 
1207
      (null m)
 
1208
    (and
 
1209
     (not (endp (rtmintvars-0 m)))
 
1210
     (true-listp (rtmintvars-0 m))
 
1211
     (not (equal 'error-value (get-common-value (var-attributes (rtmintvars-0 m) rtm-typed-mem))))
 
1212
     (equal-elements 
 
1213
      (var-attribute (get-cell (gemvar-0 m) gem-typed-mem))
 
1214
      (var-attributes (rtmintvars-0 m) rtm-typed-mem))
 
1215
    (attributes-correspondence (cdr m) gem-typed-mem rtm-typed-mem))))
 
1216
 
 
1217
 
 
1218
(defthm redefinition-of-m-corr
 
1219
 (equal
 
1220
  (and
 
1221
   (m-entries-point-to-good-rtm-var-sets m rtm-vars)
 
1222
   (m-correspondent-values-p m gem-vars rtm-vars))
 
1223
  (and
 
1224
   (attributes-correspondence m gem-vars rtm-vars)
 
1225
   (m-correspondent-vals-p m gem-vars rtm-vars)))
 
1226
 :rule-classes nil)
 
1227
 
 
1228
 
 
1229
 
 
1230
(defun is-variable-mapping (m gem-vars rtm-vars)
 
1231
  (and
 
1232
   (alistp m)
 
1233
   (no-tmp-into-mapping m)
 
1234
   (no-duplicates-p (gem-variables m))
 
1235
   (no-duplicates-p (rtm-variables m))
 
1236
   (correct-wrt-arity m gem-vars)
 
1237
   (same-vars gem-vars m)
 
1238
   (attributes-correspondence m gem-vars rtm-vars)
 
1239
   (m-correspondent-vals-p m gem-vars rtm-vars)))
 
1240
 
 
1241
(defun output (mem) (projectio mem 'Output))
 
1242
 
 
1243
(defun is-gem-mem-p (mem) 
 
1244
 (and (is-typed-amem-p mem)
 
1245
      (bounded-amem-p mem)))
 
1246
 
 
1247
(defthm mapping-correspondence-implies-same-outputs
 
1248
 (implies
 
1249
  (and
 
1250
   (is-variable-mapping m gem-mem rtm-mem)
 
1251
   (is-gem-mem-p gem-mem))
 
1252
  (equal-memories 
 
1253
   (output gem-mem)
 
1254
   (decode m (output rtm-mem))))
 
1255
 :hints (("Goal" :use 
 
1256
          (fact-bout-rns-v0 
 
1257
           (:instance redefinition-of-m-corr
 
1258
                      (gem-vars gem-mem)
 
1259
                      (rtm-vars rtm-mem))
 
1260
           (:instance equalities-on-io
 
1261
                      (gem-typed-mem gem-mem)
 
1262
                      (rtm-typed-mem rtm-mem))
 
1263
           (:instance equal-memories-commutative
 
1264
                      (mem1 (output gem-mem))
 
1265
                      (mem2 (decode m (output rtm-mem)))))))
 
1266
 :rule-classes nil)
 
1267
 
 
1268
 
 
1269
 
 
1270
(in-theory (disable correct-arity-all-i-need
 
1271
                    if-every-element-matches-val-then-get-common-value-amounts-to-val
 
1272
                    make-null-list-is-invariant-on-value-slicing
 
1273
                    build-values-by-rns-extended-for-nils-provides-integers-from-integer
 
1274
                    build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
 
1275
                    crt-inversion-extended-to-nils-in-integer-case
 
1276
                    apply-direct-rns-unfolding-for-integer-case
 
1277
                    apply-direct-rns-unfolding-for-boolean-case
 
1278
                    apply-inverse-direct-retrieves-same-value-for-typed-cells
 
1279
                    inversion-for-empty-cell
 
1280
                    ad-hoc-2-for-inversion-of-one-nonempty-cell-by-decode
 
1281
                    ad-hoc-3-for-inversion-of-one-nonempty-cell-by-decode
 
1282
                    nonempty-cell-is-not-mapped-into-nils-by-rns
 
1283
                    nonempty-rtm-vars-which-correspond-to-gem-var-by-values-and-atributes-map-back-to-gem-var
 
1284
                    decode-inversion-for-nonempty-gem-cell
 
1285
                    invert-cell-inverts-for-m-correspondents
 
1286
                    ;any-cell-of-a-typed-mem-is-nil-or-a-typed-cell
 
1287
                    silly1
 
1288
                    silly2
 
1289
                    decode-equals-retrieve-vars
 
1290
                    decode-retrieves-gem-memory
 
1291
                    cell-of-projected-mem-is-projected-cell
 
1292
                    projection-of-null-list-is-null-list
 
1293
                    null-cell-corresponds-to-null-lists-of-values
 
1294
                    project-invert-commute-for-empty-cell
 
1295
                    rtmvars-correspondent-to-nonemptycell-is-not-emptylist
 
1296
                    values-remain-the-same-if-correspondent-attrs
 
1297
                    attributes-same-1
 
1298
                    inversion-2-for-nonempty-projected-on-different-attr
 
1299
                    inversion-1-for-nonempty-projected-on-different-attr
 
1300
                    projecting-on-different-attr-gets-nils
 
1301
                    decode-one-entry-of-null-list-is-nil
 
1302
                    inversion-2-for-nonempty-projected-on-different-attr
 
1303
                    inversion-for-nonempty-projected-on-different-attr
 
1304
                    project-invert-commuting
 
1305
                    letssimplify
 
1306
                    project-invert-commuting-better
 
1307
                    decode-projection-is-decode-of-projection
 
1308
                    decode-project-commuting
 
1309
                    equalwrt-holds-on-project-all
 
1310
                    equalwrt-holds-on-project-all-all
 
1311
                    equal-memories-holds-by-projection
 
1312
                    equalities-on-io))
 
1313
 
 
1314
                    
 
1315
                    
 
1316
                    
 
1317
                    
 
1318
                    
 
1319
                    
 
1320
                    
 
1321
                    
 
 
b'\\ No newline at end of file'