← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2013/van-gastel-schmaltz/books/GeNoC-misc.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/2013/van-gastel-schmaltz/books/GeNoC-misc.lisp
 
1
#|$ACL2s-Preamble$;
 
2
;; Amr HELMY
 
3
;; Miscelaneous definitions and lemmas
 
4
 
 
5
;;31st october 2007
 
6
;; File: GeNoC-misc.lisp
 
7
(begin-book t :ttags :all);$ACL2s-Preamble$|#
 
8
 
 
9
(in-package "ACL2")
 
10
 
 
11
(include-book "GeNoC-types")
 
12
(include-book "make-event/defspec"  :dir :system)
 
13
 
 
14
;;
 
15
;;  nil_list
 
16
;;
 
17
(defun nil_list (n)
 
18
  (if (zp n)
 
19
    nil
 
20
    (cons nil (nil_list (1- n)))))
 
21
 
 
22
;;|-------------------------------------------------|
 
23
;;|                                                    |
 
24
;;|                    Not-in                            |
 
25
;;|                                                    |
 
26
;;|-------------------------------------------------|        
 
27
(defun not-in-test (x y)
 
28
  (not (member-equal x y)))
 
29
(create-for-all not-in-test :name not-in :extra (y))
 
30
(defcong permp equal (not-in x y) 2)
 
31
(defthm not-in-append-alt
 
32
  (equal (not-in x (append y z))
 
33
         (and (not-in x y)
 
34
              (not-in x z))))
 
35
(defthm not-in-empty-list-always-true
 
36
  (implies (endp y)
 
37
           (not-in x y)))
 
38
(defthm subset-not-in
 
39
  (implies (and (subsetp x y)
 
40
                (not-in a y))
 
41
           (not-in a x)))
 
42
(defcong permp equal (not-in x y) 2)
 
43
(defthm no-dups-append
 
44
  (equal (no-duplicatesp-equal (append x y))
 
45
         (and (no-duplicatesp-equal x)
 
46
              (no-duplicatesp-equal y)
 
47
              (not-in x y))))
 
48
 
 
49
 
 
50
;;|---------------------------------------|
 
51
;;|                                          |
 
52
;;|         Theoremes about Subsetp              |
 
53
;;|                                          |
 
54
;;|---------------------------------------|        
 
55
;; we prove some useful lemmas about subsetp
 
56
(defthm subsetp-expand
 
57
  (implies (subsetp x y)
 
58
           (subsetp x (cons z y))))
 
59
 
 
60
(defthm subsetp-x-x
 
61
  (subsetp x x))
 
62
 
 
63
(defthm subsetp-append
 
64
  (equal (subsetp (append x y) z)
 
65
         (and (subsetp x z)
 
66
              (subsetp y z))))
 
67
 
 
68
(defthm subsetp-trans
 
69
  ;; transitivity of subsetp
 
70
  (implies (and (subsetp x y)
 
71
                (subsetp y z))
 
72
           (subsetp x z)))
 
73
 
 
74
(defthm subsetp-cons-cdr-part
 
75
  (implies (subsetp (cons x xs) y)
 
76
           (subsetp xs y)))
 
77
 
 
78
(defthm subsetp-cons-car-part
 
79
  (implies (subsetp (cons x xs) y)
 
80
           (member-equal x y)))
 
81
 
 
82
;;|---------------------------------|
 
83
;;|                                    |
 
84
;;|             tomissives             |
 
85
;;|                                 |
 
86
;;|---------------------------------|
 
87
(defun ToMissive-TM (tr)
 
88
    (let* ((id (IdTm tr))
 
89
           (org (OrgTm tr))
 
90
           (frm (FrmTm Tr))
 
91
           ;(dest (DestTm tr))
 
92
           (Flit (FlitTM tr))
 
93
           (time (timeTM tr)))
 
94
     (M Id org frm Flit time)))
 
95
(create-map tomissive-TM :name tomissives)
 
96
 
 
97
;; for the proof of the correctness of GeNOC
 
98
;; two important lemmas are needed
 
99
 
 
100
;; the first one rewrites (ToMissives (extract-sublst ..))
 
101
;; to (extract-sublst (tomissives) ... )
 
102
(defthm m-ids-tomissives
 
103
  (equal (M-ids (ToMissives m)) (Tm-ids m))
 
104
    :hints (("Goal" :in-theory (e/d (v-id M)()) ))
 
105
)
 
106
 
 
107
(defthm fwd-missivesp
 
108
  ;; as missivesp is disabled we prove this rule to add
 
109
  ;; the content of missivesp as hypotheses
 
110
  (implies (missivesp M NodeSet)
 
111
           (and (Validfields-M M )
 
112
                (subsetp (M-orgs M) NodeSet)
 
113
                ;(subsetp (M-dests M) NodeSet)
 
114
                (True-listp M)
 
115
                (No-duplicatesp-equal (M-ids M))))
 
116
  :rule-classes :forward-chaining)        
 
117
 
 
118
 
 
119
(defthm tomissives-truelistp
 
120
  (implies (Tmissivesp M nodeset)
 
121
           (true-listp (tomissives m))))
 
122
 
 
123
(defthm to-missives-missivesp
 
124
  (implies (TMissivesp tmissives nodeset)
 
125
           (Missivesp (ToMissives tmissives) NodeSet))
 
126
      :hints (("Goal" :in-theory (e/d (v-id m-_id M M-p weak-M-p M-frame TM-frame M-flit M-time M-org)()) ))
 
127
)
 
128
 
 
129
(defthm rewrite-missivesp-append
 
130
  (implies (true-listp x)
 
131
           (equal (missivesp (append x y) nodeset)
 
132
                  (and (missivesp x nodeset)
 
133
                       (missivesp y nodeset)
 
134
                       (not-in (m-ids x) (m-ids y))))))
 
135
 
 
136
(defthm missivesy-missives-cdry
 
137
  ;; missivesp y then missivesp cdr y                
 
138
  (implies (missivesp y nodeset) 
 
139
           (missivesp (cdr y) nodeset)))
 
140
 
 
141
;;|------------------------------|
 
142
;;|                              |
 
143
;;|            toTmissives                 |
 
144
;;|                                 |
 
145
;;|------------------------------|                         
 
146
 
 
147
(defun ToTMissive-V (tr)
 
148
    (let ((frm (FrmV tr))
 
149
           (org (OrgV tr))
 
150
           (curr (CurV tr))
 
151
           ;(dest (DestV tr))
 
152
           (id (IdV tr))
 
153
           (Flit (FlitV tr))
 
154
           (Time (TimeV tr))
 
155
           (Loc (LocV tr)))
 
156
      (TM id org curr frm Flit time loc)))
 
157
 
 
158
(create-map ToTMissive-V :name ToTMissives)
 
159
 
 
160
(defun tomissive-V (v)
 
161
  (M (IdV v) (OrgV v) (FrmV v) (FlitV v) (TimeV v)))
 
162
 
 
163
(defun equal-locs (trlst TM)
 
164
  (if (endp TrLst)
 
165
      (if (endp TM)
 
166
          t
 
167
        nil)
 
168
      (and (equal (LocV (car trlst)) (LocTM (car TM)))
 
169
           (equal-locs (cdr trlst) (cdr TM)))))
 
170
(defthm TM-ids-ToMissives-V-ids    ;; OK
 
171
  (equal (TM-ids (ToTMissives x)) (V-ids x))
 
172
      :hints (("Goal" :in-theory (e/d (v-id TM)()) ))
 
173
)
 
174
 
 
175
 
 
176
;; for the proof of the correctness of GeNOC
 
177
;; two important lemmas are needed
 
178
 
 
179
;; the first one rewrites (ToMissives (extract-sublst ..))
 
180
;; to (extract-sublst (tomissives) ... )                 
 
181
(defthm TMissivesp-ToMissives-bis
 
182
  (implies (trlstp trlst nodeset)
 
183
           (TMissivesp (ToTMissives TrLst) NodeSet))
 
184
        :hints (("Goal" :in-theory (e/d (v-id TM TM-p weak-TM-p TM-frame TM-flit TM-time TM-org TM-cur TM-loc)()) ))
 
185
        )
 
186
 
 
187
 
 
188
(defthm fwd-tmissivesp
 
189
  ;; as Tmissivesp is disabled we prove this rule to add
 
190
  ;; the content of Tmissivesp as hypotheses
 
191
  (implies (Tmissivesp M NodeSet)
 
192
           (and (Validfields-TM M nodeset)
 
193
                (subsetp (TM-orgs M) NodeSet)
 
194
                (subsetp (TM-curs M) NodeSet)
 
195
                ;(subsetp (TM-dests M) NodeSet)
 
196
                (True-listp M)
 
197
                (No-duplicatesp-equal (TM-ids M))))
 
198
  :rule-classes :forward-chaining)    
 
199
 
 
200
(defthm tmissivesy-tmissives-cdry
 
201
  (implies (tmissivesp y nodeset) 
 
202
           (tmissivesp (cdr y) nodeset)))
 
203
 
 
204
(defthm rewrite-nodups-tm-ids-append
 
205
  (equal (no-duplicatesp-equal (tm-ids (append x y)))
 
206
         (and (no-duplicatesp-equal (tm-ids x))
 
207
              (no-duplicatesp-equal (tm-ids y))
 
208
              (not-in (tm-ids x) (tm-ids y)))))
 
209
(defthm rewrite-validfields-tm-append
 
210
  (equal (validfields-tm (append x y) nodeset)
 
211
         (and (validfields-tm x nodeset)
 
212
              (validfields-tm y nodeset))))
 
213
(defthm rewrite-tmissivesp-append
 
214
  (implies (true-listp tmissives1)
 
215
           (equal (tmissivesp (append tmissives1 tmissives2) nodeset)
 
216
                  (and (tmissivesp tmissives1 nodeset)
 
217
                       (tmissivesp tmissives2 nodeset)
 
218
                       (not-in (tm-ids tmissives1) (tm-ids tmissives2))))))
 
219
;;|------------------------------|
 
220
;;|                                 |
 
221
;;|              Travels            |
 
222
;;|                                 |
 
223
;;|------------------------------|
 
224
(defthm rewrite-trlstp-append
 
225
  (implies (true-listp x)
 
226
           (equal (trlstp (append x y) nodeset)
 
227
                  (and (trlstp x nodeset)
 
228
                       (trlstp y nodeset)
 
229
                       (not-in (v-ids x) (v-ids y)))))
 
230
  :otf-flg t)
 
231
 
 
232
(defthm fwd-trlstp
 
233
  ;; because we disable trlstp, this rule adds its content
 
234
  ;; as hypotheses
 
235
  (implies (TrLstp TrLst nodeset)
 
236
           (and (validfields-trlst trlst nodeset)
 
237
                (true-listp trlst)
 
238
                (no-duplicatesp-equal (v-ids trlst))))
 
239
  :rule-classes :forward-chaining) 
 
240
 
 
241
;;|------------------------------|
 
242
;;|                                 |
 
243
;;|                 rev                 |
 
244
;;|------------------------------|  
 
245
(defun rev (x)
 
246
  (declare (xargs :guard (true-listp x)))
 
247
  (if (endp x)
 
248
      nil
 
249
    (append (rev (cdr x)) (list (car x)))))
 
250
 
 
251
(defthm subsetp-rev-l
 
252
  (equal (subsetp (rev x) y)
 
253
         (subsetp x y)))
 
254
(defthm member-rev
 
255
  (iff (member-equal a (rev x))
 
256
       (member-equal a x)))
 
257
(defthm subsetp-rev-r
 
258
  (equal (subsetp x (rev y))
 
259
         (subsetp x y)))
 
260
 
 
261
 
 
262
 
 
263
;;|------------------------------|
 
264
;;|                                 |
 
265
;;|            ntkstate                 |
 
266
;;|                                 |
 
267
;;|------------------------------| 
 
268
 
 
269
;; valid ntkstate
 
270
(defthm validstate-entry-implies-coord-and-buffer
 
271
  (implies (and (validstate-entryp x)
 
272
                (consp x))
 
273
           (and (validcoord (car x))
 
274
                (validbuffer (cadr x)))))#|ACL2s-ToDo-Line|#
 
275
 
 
276