← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/schmaltz-borrione/GeNoC-support/GeNoC.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/2006/schmaltz-borrione/GeNoC-support/GeNoC.lisp
 
1
;; Julien Schmaltz
 
2
;; Generic Routing Module of GeNoC
 
3
;; June 20th 2005
 
4
;; File: GeNoC-routing.lisp
 
5
 
 
6
(in-package "ACL2")
 
7
 
 
8
;; we import the previous books
 
9
(include-book "GeNoC-scheduling") ;; imports GeNoC-misc and GeNoC-nodeset
 
10
(include-book "GeNoC-routing")
 
11
 
 
12
(in-theory (disable mv-nth))
 
13
 
 
14
;;------------------------------------------------------------------------
 
15
;;
 
16
;;                        GeNoC_t
 
17
;;
 
18
;;------------------------------------------------------------------------
 
19
 
 
20
;; Tail definition of GeNoC_t
 
21
;; --------------------------
 
22
(defun GeNoC_t (M NodeSet att TrLst)
 
23
  ;; The composition of Routing and Scheduling is built by function GeNoC_t.
 
24
  ;; It takes as arguments:
 
25
  ;; - a list of missives, M
 
26
  ;; - the set of existing nodes, NodeSet
 
27
  ;; - the list of attempts, att
 
28
  ;; - an accumulator of travels, TrLst
 
29
  ;; 
 
30
  ;; we set the measure to be SumOfAttempts(att)
 
31
  (declare (xargs :measure (SumOfAttempts att)))
 
32
  (if (zp (SumOfAttempts att))
 
33
      ;; if every attempt has been consumed, we return the accumulator
 
34
      ;; TrLst and the remaining missives M
 
35
      (mv TrLst M)
 
36
    ;; else, 
 
37
    (let ((V (Routing M NodeSet)))
 
38
      ;; we compute the routes. This produces the travel list V.
 
39
      (mv-let (Scheduled Delayed newAtt)
 
40
              ;; we call function scheduling
 
41
              (Scheduling V att)
 
42
              ;; we enter the recursive call and accumulate the 
 
43
              ;; scheduled travels
 
44
              (GeNoC_t (ToMissives Delayed) NodeSet newAtt
 
45
                       (append Scheduled TrLst))))))
 
46
 
 
47
 
 
48
;; Correctness of GeNoC_t
 
49
;; ----------------------
 
50
(defun CorrectRoutes-GeNoC_t (routes m-dest)
 
51
  ;; GeNoC_t is correct if every element ctr of the output list
 
52
  ;; is such that (a) FrmV(ctr) = FrmM(m) and (b) forall r in 
 
53
  ;; RoutesV(ctr) Last(r) = DestM(m). For the m such that
 
54
  ;; IdM(m) = IdV(ctr).
 
55
  ;; This function checks that (b) holds.
 
56
  (if (endp routes)
 
57
      t
 
58
    (let ((r (car routes)))
 
59
      (and (equal (car (last r)) m-dest)
 
60
           (CorrectRoutes-GeNoC_t (cdr routes) m-dest)))))
 
61
 
 
62
(defun GeNoC_t-correctness1 (TrLst M/TrLst)
 
63
  ;; we complement the correctness of GeNoC_t
 
64
  (if (endp TrLst)
 
65
      (if (endp M/TrLst)
 
66
          t
 
67
        nil)
 
68
    (let* ((tr (car TrLst))
 
69
           (v-frm (FrmV tr))
 
70
           (routes (RoutesV tr))
 
71
           (m (car M/TrLst))
 
72
           (m-frm (FrmM m))
 
73
           (m-dest (DestM m)))
 
74
      (and (equal v-frm m-frm)
 
75
           (CorrectRoutes-GeNoC_t routes m-dest)
 
76
           (GeNoC_t-correctness1 (cdr TrLst) 
 
77
                                 (cdr M/TrLst))))))  
 
78
 
 
79
(defun GeNoC_t-correctness (TrLst M)
 
80
  ;; before checking correctness we filter M
 
81
  ;; according to the ids of TrLst
 
82
  (let ((M/TrLst (extract-sublst M (V-ids TrLst))))
 
83
    (GeNoC_t-correctness1 TrLst M/TrLst)))
 
84
 
 
85
 
 
86
;; Non tail definition of GeNoC_t
 
87
;; ------------------------------
 
88
(defun GeNoC_t-non-tail-Comp (M NodeSet att)
 
89
  ;; we define a non tail function that computes the 
 
90
  ;; first output of GeNoC_t, i.e the completed transactions
 
91
  (declare (xargs :measure (SumOfAttempts att)))
 
92
  (if (zp (SumOfAttempts att))
 
93
      ;; if every attempt has been consumed, we return the accumulator
 
94
      ;; TrLst and the remaining missives M
 
95
      nil
 
96
    ;; else, 
 
97
    (let ((V (Routing M NodeSet)))
 
98
      ;; we compute the routes. This produces the travel list V.
 
99
      (mv-let (Scheduled Delayed newAtt)
 
100
              ;; we call function scheduling
 
101
              (Scheduling V att)
 
102
              ;; we enter the recursive call and accumulate the 
 
103
              ;; scheduled travels
 
104
              (append (GeNoC_t-non-tail-Comp (ToMissives Delayed) 
 
105
                                             NodeSet newAtt)
 
106
                      Scheduled)))))
 
107
 
 
108
;; we now prove that this function is right
 
109
 
 
110
(defthm true-listp-GeNoC_t-non-tail-comp
 
111
  (true-listp (GeNoC_t-non-tail-Comp M NodeSet att))
 
112
  :rule-classes :type-prescription)
 
113
 
 
114
(defthm GeNoC_t-non-tail-=-tail-comp
 
115
  (implies (true-listp TrLst)
 
116
           (equal (car (GeNoC_t M NodeSet att TrLst))
 
117
                  (append (GeNoC_t-non-tail-Comp M NodeSet Att)
 
118
                          TrLst))))
 
119
 
 
120
;; Proof of GeNoC_t correctness
 
121
;; ----------------------------
 
122
 
 
123
;; first we add a lemma that tells ACL2 that 
 
124
;; converting the travels that are routed and delayed
 
125
;; produced a valid list of missives
 
126
(defthm missivesp-mv-nth1-scheduling-routing
 
127
  (let ((NodeSet (NodeSetGenerator Params)))
 
128
    (implies (and (Missivesp M NodeSet)
 
129
                  (ValidParamsp Params))
 
130
             (Missivesp 
 
131
              (ToMissives (mv-nth 1 
 
132
                                  (scheduling (routing M NodeSet)
 
133
                                              att)))
 
134
              NodeSet)))
 
135
  :hints (("GOAL"
 
136
           :in-theory (disable
 
137
                       TrLstp Missivesp))))
 
138
 
 
139
 
 
140
 
 
141
;; the recursive call of genoc_t-non-tail-comp calls append
 
142
;; we put the append at the top.
 
143
;; to do so we add the two rules below:
 
144
 
 
145
(defthm v-ids-append
 
146
  ;; the ids of an append is the append of the ids
 
147
  (equal (v-ids (append a b))
 
148
         (append (v-ids a) (v-ids b))))
 
149
 
 
150
(defthm extract-sublst-append
 
151
  ;; filtering according to an append is the append 
 
152
  ;; of the filtering.
 
153
  (equal (extract-sublst M (append id1 id2))
 
154
         (append (extract-sublst M id1)
 
155
                 (extract-sublst M id2))))
 
156
 
 
157
 
 
158
;; then to split the proof is two cases, we replace the 
 
159
;; append by a conjunction. 
 
160
;; the rule below allows this decomposition:
 
161
 
 
162
(defthm correctroutess1-append
 
163
  (implies (and (equal (len a) (len c))
 
164
                (equal (len b) (len d)))
 
165
           (equal (genoc_t-correctness1 (append a b) 
 
166
                                        (append c d))
 
167
                  (and (Genoc_T-Correctness1 a c)
 
168
                       (Genoc_T-Correctness1 b d)))))
 
169
 
 
170
;; To have this lemma used we need to prove some 
 
171
;; additional properties between len and extract-sublst
 
172
;; and len and v-ids (e.g. a is a call to v-ids)
 
173
 
 
174
(defthm len-extract-sublst
 
175
  (equal (len (extract-sublst L ids))
 
176
         (len ids)))
 
177
 
 
178
(defthm len-v-ids
 
179
  (equal (len (v-ids x))
 
180
         (len x)))
 
181
 
 
182
;; now we need to prove some lemmas so that previous rules
 
183
;; (from GeNoC-misc) about extract-sublst, tomissives, etc could
 
184
;; fire.
 
185
 
 
186
(defthm subsetp-trans
 
187
  ;; transitivity of subsetp
 
188
  (implies (and (subsetp x y)
 
189
                (subsetp y z))
 
190
           (subsetp x z)))
 
191
 
 
192
(defthm v-ids-GeNoC_t-non-tail-comp
 
193
  ;; the ids of the output of genoc_t-non-tail-comp is a 
 
194
  ;; subset of those of M
 
195
  ;; for this theorem the rule ids-routing is useful
 
196
  (let ((NodeSet (NodeSetGenerator Params)))
 
197
    (implies (and (Missivesp M NodeSet)
 
198
                  (ValidParamsp Params))
 
199
             (let ((Gnt (Genoc_T-Non-Tail-Comp M NodeSet att)))
 
200
               (subsetp (V-ids Gnt) (M-ids M)))))
 
201
  :hints (("GOAL"
 
202
           :in-theory 
 
203
           (disable missivesp TrLstp))
 
204
          ("Subgoal *1/3"
 
205
           :use 
 
206
           ((:instance subsetp-scheduled-delayed-ids
 
207
                       (TrLst (Routing M (NodeSetGenerator Params)))))
 
208
           :in-theory 
 
209
           (disable subsetp-scheduled-delayed-ids Missivesp TrLstp))))
 
210
 
 
211
(defthm not-in-no-duplicatesp-equal-append
 
212
  ;; if x is not in y and both do not have duplicates then
 
213
  ;; their append has no duplicate too
 
214
  (implies (and (no-duplicatesp-equal x)
 
215
                (not-in x y)
 
216
                (no-duplicatesp-equal y))
 
217
           (no-duplicatesp-equal (append x y))))
 
218
 
 
219
(defthm subsetp-not-in
 
220
  ;; if a list y and no element in common with z
 
221
  ;; then any sublist x of y has no element in z
 
222
  (implies (and (not-in delayed scheduled)
 
223
                (subsetp x delayed))
 
224
           (not-in x scheduled)))
 
225
 
 
226
(defthm not-in-v-ids-genoc_t-non-tail-comp
 
227
  ;; if the ids of a list have no common element with 
 
228
  ;; another ids then the output of genoc_t-non-tail-comp does
 
229
  ;; not introduce any new id
 
230
  (let ((NodeSet (NodeSetGenerator Params)))
 
231
    (implies (and (not-in (m-ids delayed) Sched-ids)
 
232
                  (Missivesp delayed NodeSet)
 
233
                  (ValidParamsp Params))
 
234
             (not-in (v-ids (genoc_t-non-tail-comp delayed NodeSet att))
 
235
                     Sched-ids)))
 
236
  :otf-flg t
 
237
  :hints (("GOAL"
 
238
           :do-not-induct t
 
239
           :in-theory (disable missivesp))))
 
240
 
 
241
(defthm fwd-trlstp
 
242
  ;; because we disable trlstp, this rule adds its content
 
243
  ;; as hypotheses
 
244
  (implies (TrLstp TrLst)
 
245
           (and (validfields-trlst trlst)
 
246
                (true-listp trlst)
 
247
                (no-duplicatesp-equal (v-ids trlst))))
 
248
  :rule-classes :forward-chaining)
 
249
 
 
250
(defthm v-ids-GeNoC_t-non-tail-comp-no-dup
 
251
  ;; the ids of the output of genoc_t-non-tail-comp have no dup
 
252
  (let ((NodeSet (NodeSetGenerator Params)))
 
253
    (implies (and (Missivesp M NodeSet)
 
254
                  (ValidParamsp Params))
 
255
             (let ((Gnt (Genoc_T-Non-Tail-Comp M NodeSet att)))
 
256
               (no-duplicatesp-equal (V-ids Gnt)))))
 
257
  :otf-flg t
 
258
  :hints (("GOAL"
 
259
           :do-not '(eliminate-destructors generalize)
 
260
           :do-not-induct t
 
261
           :induct (genoc_t-non-tail-comp M (nodeSetGenerator Params) att)
 
262
           :in-theory (disable missivesp TrLstp))
 
263
          ("Subgoal *1/2"
 
264
           :use 
 
265
           ((:instance 
 
266
             not-in-v-ids-genoc_t-non-tail-comp
 
267
             (delayed (tomissives 
 
268
                       (mv-nth 1 (scheduling
 
269
                                  (routing M (nodeSetGenerator Params))
 
270
                                  att))))
 
271
             (att (mv-nth 2 (scheduling
 
272
                             (routing M (nodeSetGenerator Params))
 
273
                             att)))
 
274
             (Sched-ids (v-ids (mv-nth 0 (scheduling 
 
275
                                          (routing M (nodeSetGenerator Params))
 
276
                                          att)))))
 
277
            (:instance trlstp-scheduled 
 
278
                       (TrLst (routing M (Nodesetgenerator Params)))))
 
279
           :in-theory 
 
280
           (disable trlstp-scheduled mv-nth trlstp
 
281
                    not-in-v-ids-genoc_t-non-tail-comp Missivesp))))
 
282
 
 
283
(defthm extract-sublst-subsetp-m-ids
 
284
  ;; filtering a list l according to a subset ids of its identifiers
 
285
  ;; produces a list the ident. of which are ids
 
286
  (implies (and (subsetp ids (M-ids l))
 
287
                (true-listp ids)
 
288
                (Validfields-M l))
 
289
           (equal (M-ids (extract-sublst l ids))
 
290
                  ids)))
 
291
 
 
292
(defthm ToMissives-Delayed/Rtg
 
293
  ;; we prove that the conversion of the delayed travels
 
294
  ;; into a list of missives is equal to the filtering 
 
295
  ;; of the initial list of missives M according to the ids
 
296
  ;; of the delayed travels.
 
297
  (let ((NodeSet (NodeSetGenerator Params)))
 
298
    (mv-let (Scheduled/Rtg Delayed/Rtg newAtt)
 
299
            (scheduling (Routing M NodeSet) att)
 
300
            (declare (ignore Scheduled/Rtg newAtt))
 
301
            (implies (and (Missivesp M NodeSet)
 
302
                          (ValidParamsp Params))
 
303
                     (equal (ToMissives Delayed/Rtg)
 
304
                            (extract-sublst M (V-ids Delayed/Rtg))))))
 
305
  :otf-flg t
 
306
  :hints (("GOAL"
 
307
           :do-not-induct t
 
308
           :do-not '(eliminate-destructors generalize fertilize)
 
309
           :use ((:instance ToMissives-extract-sublst
 
310
                            (L (Routing M (NodeSetGenerator Params)))
 
311
                            (ids 
 
312
                             (V-ids (mv-nth 1 
 
313
                                            (scheduling 
 
314
                                             (Routing M (NodeSetGenerator Params))
 
315
                                             att)))))
 
316
                 (:instance delayed-travel-correctness
 
317
                            (TrLst (Routing M (NodeSetGenerator Params))))
 
318
                 (:instance subsetp-scheduled-delayed-ids
 
319
                            (TrLst (Routing M (NodeSetGenerator Params)))))
 
320
           :in-theory (disable TrLstp Missivesp
 
321
                               ToMissives-extract-sublst
 
322
                               subsetp-scheduled-delayed-ids))))
 
323
 
 
324
(defthm valid-missive-assoc-equal
 
325
  ;; a list of a member of a valid list of missives 
 
326
  ;; is a valid list of missives
 
327
  (implies (and (Missivesp M NodeSet)
 
328
                (member-equal e (M-ids M)))
 
329
           (Missivesp (list (assoc-equal e M)) NodeSet)))
 
330
 
 
331
(defthm missivesp-cons
 
332
  ;; lemma used in the next defthm
 
333
  ;; if we cons a valid missive to a filtered valid list
 
334
  ;; of missives, we obtain a valid list of missives if the 
 
335
  ;; the id of the consed missive is not in the filter
 
336
  (implies (and (missivesp (extract-sublst M ids) nodeset)
 
337
                (missivesp (list (assoc-equal e M)) nodeset)
 
338
                (not (member-equal e ids)) 
 
339
                (subsetp ids (M-ids M)))
 
340
           (missivesp (cons (assoc-equal e M)
 
341
                            (extract-sublst M ids))
 
342
                      nodeset)))
 
343
 
 
344
 
 
345
(defthm missivesp-extract-sublst
 
346
  (let ((NodeSet (NodeSetGenerator Params)))
 
347
    (implies (and (missivesp M NodeSet)
 
348
                  (ValidParamsp Params)
 
349
                  (true-listp ids)
 
350
                  (no-duplicatesp-equal ids)
 
351
                  (subsetp ids (M-ids M)))
 
352
             (Missivesp (extract-sublst M ids) NodeSet)))
 
353
  :hints (("GOAL"
 
354
           :in-theory (disable missivesp))
 
355
          ("Subgoal *1/1"
 
356
           :in-theory (enable missivesp))))
 
357
 
 
358
 
 
359
(defthm fwd-missivesp
 
360
  ;; as missivesp is disabled we prove this rule to add
 
361
  ;; the content of missivesp as hypotheses
 
362
  (implies (missivesp M NodeSet)
 
363
           (and (Validfields-M M)
 
364
                (subsetp (M-orgs M) NodeSet)
 
365
                (subsetp (M-dests M) NodeSet)
 
366
                (True-listp M)
 
367
                (No-duplicatesp (M-ids M))))
 
368
  :rule-classes :forward-chaining)
 
369
 
 
370
 
 
371
(defthm v-ids_G_nt_sigma_subsetp-v-ids-delayed/rtg
 
372
  ;; this lemma is used in the subsequent proofs
 
373
  ;; it makes a fact "explicit"
 
374
  (let ((NodeSet (NodeSetGenerator Params)))
 
375
    (mv-let (scheduled/rtg delayed/rtg newAtt)
 
376
            (scheduling (routing M NodeSet) att)
 
377
            (declare (ignore scheduled/rtg))
 
378
            (implies (and (Missivesp M NodeSet)
 
379
                          (ValidParamsp Params))
 
380
                     (subsetp 
 
381
                      (V-ids 
 
382
                       (genoc_t-non-tail-comp 
 
383
                        (extract-sublst M (v-ids delayed/rtg))
 
384
                        NodeSet newAtt))
 
385
                      (V-ids delayed/rtg)))))
 
386
  :otf-flg t
 
387
  :hints (("GOAL"
 
388
           :do-not-induct t
 
389
           :use 
 
390
           ((:instance subsetp-scheduled-delayed-ids
 
391
                       (TrLst (Routing M (NodeSetGenerator Params))))
 
392
            (:instance trlstp-delayed
 
393
                       (TrLst (routing M (NodeSetGenerator Params))))
 
394
            ;; the following is required because in the conclusion of the 
 
395
            ;; rule there is no call to extract-sublst
 
396
            (:instance v-ids-GeNoC_t-non-tail-comp
 
397
                       (M (extract-sublst 
 
398
                           M 
 
399
                           (V-ids (mv-nth 1 (scheduling
 
400
                                             (routing M (NodeSetGenerator Params))
 
401
                                             att)))))
 
402
                       (att (mv-nth 2 (scheduling
 
403
                                       (routing M (NodeSetGenerator Params))
 
404
                                       att)))))
 
405
           :in-theory (disable subsetp-scheduled-delayed-ids
 
406
                               trlstp-delayed
 
407
                               v-ids-GeNoC_t-non-tail-comp
 
408
                               trlstp missivesp))))
 
409
 
 
410
 
 
411
;; Scheduled/Rtg does not modify frames
 
412
;; ---------------------------------------
 
413
 
 
414
(defthm s/d-travel-v-frms
 
415
  (implies (and (TrLstp sd-trlst)
 
416
                (s/d-travel-correctness sd-trlst TrLst/sd-ids))
 
417
           (equal (V-frms sd-trlst) (V-frms TrLst/sd-ids))))
 
418
 
 
419
(defthm m-frms-to-v-frms
 
420
  ;; this rule is only used to rewrite the next theorem to 
 
421
  ;; the previous one.
 
422
  (equal (m-frms (toMissives x))
 
423
         (v-frms x)))
 
424
 
 
425
(defthm Scheduled-v-frms-m-frms
 
426
  ;; we prove that the frames of the scheduled travels
 
427
  ;; are equal to the frames of the conversion of the initial list of travels
 
428
  ;; filtered according to the ids of the scheduled travels
 
429
  (mv-let (Scheduled Delayed newAtt)
 
430
          (scheduling TrLst att)
 
431
          (declare (ignore Delayed newAtt))
 
432
          (implies (and (TrLstp TrLst) 
 
433
                        (ValidParamsp Params))
 
434
                   (equal 
 
435
                    (V-frms scheduled)
 
436
                    (M-frms 
 
437
                     (ToMissives (extract-sublst TrLst
 
438
                                                 (v-ids scheduled)))))))
 
439
  :hints (("GOAL"
 
440
           :use ((:instance s/d-travel-v-frms
 
441
                            (sd-trlst 
 
442
                             (mv-nth 0 (scheduling TrLst att)))
 
443
                            (TrLst/sd-ids
 
444
                           (extract-sublst 
 
445
                            TrLst 
 
446
                            (v-ids 
 
447
                             (mv-nth 0 (scheduling TrLst att))))))
 
448
               (:instance scheduled-travels-correctness))
 
449
           :in-theory (disable TrLstp s/d-travel-v-frms mv-nth))))
 
450
 
 
451
(in-theory (disable m-frms-to-v-frms))
 
452
 
 
453
(defthm Scheduled/Rtg_not_modify_frames
 
454
  ;; we prove the the frames of the scheduled travels produced
 
455
  ;; by scheduling and routing are equal to the frames 
 
456
  ;; of the initial list of missives
 
457
  (let ((NodeSet (NodeSetGenerator Params)))
 
458
  (mv-let (Scheduled/Rtg Delayed/Rtg newAtt)
 
459
          (scheduling (routing M NodeSet) att)
 
460
          (declare (ignore Delayed/Rtg newAtt))
 
461
          (implies (and (Missivesp M NodeSet)
 
462
                        (ValidParamsp Params))
 
463
                   (equal (V-frms Scheduled/Rtg)
 
464
                          (M-frms 
 
465
                           (extract-sublst 
 
466
                            M (v-ids Scheduled/Rtg)))))))
 
467
  :hints (("GOAL"
 
468
           :do-not-induct t
 
469
           :do-not '(eliminate-destructors generalize fertilize)
 
470
           :use ((:instance Scheduled-v-frms-m-frms
 
471
                            (TrLst (routing M (NodeSetGenerator Params))))
 
472
                 (:instance subsetp-scheduled-delayed-ids
 
473
                            (TrLst (routing M (NodeSetGenerator Params)))))
 
474
           :in-theory (disable TrLstp Missivesp
 
475
                               subsetp-scheduled-delayed-ids
 
476
                               scheduled-v-frms-m-frms))))
 
477
 
 
478
(defthm correctroutesp-vm-frms-gc1
 
479
  ;; the correctness of routes and equality of frames imply
 
480
  ;; the main predicate (correctness of genoc_t-non-tail-comp)
 
481
  (implies (and (correctroutesp L (extract-sublst M (v-ids L))
 
482
                                NodeSet)
 
483
                (equal (V-frms L)
 
484
                       (m-frms (extract-sublst M (v-ids L)))))
 
485
           (Genoc_T-Correctness1 L 
 
486
                                 (extract-sublst m (v-ids L)))))
 
487
 
 
488
(defthm GC1_scheduled/Rtg
 
489
  ;; we prove the correctness of the scheduled travels
 
490
  (let ((NodeSet (NodeSetGenerator Params)))
 
491
    (implies (And (missivesp M NodeSet)
 
492
                  (ValidParamsp Params))
 
493
             (mv-let (scheduled/rtg delayed/rtg newAtt)
 
494
                     (scheduling (routing M NodeSet) att)
 
495
                     (declare (ignore delayed/rtg newAtt))
 
496
                     (genoc_t-correctness1 
 
497
                      scheduled/rtg
 
498
                      (extract-sublst M (v-ids scheduled/rtg))))))
 
499
  :otf-flg t
 
500
  :hints (("GOAL"
 
501
           :do-not-induct t
 
502
           :do-not '(eliminate-destructors generalize fertilize)
 
503
           :use 
 
504
           ((:instance Scheduled/Rtg_not_modify_frames)
 
505
            (:instance subsetp-scheduled-delayed-ids
 
506
                       (TrLst (Routing M (NodeSetGenerator Params))))
 
507
            (:instance 
 
508
             scheduling-preserves-route-correctness
 
509
             (NodeSet (NodeSetGenerator Params))
 
510
             (TrLst (routing M (NodeSetGenerator Params))))
 
511
            (:instance correctroutesp-vm-frms-gc1
 
512
                       (NodeSet (NodeSetGenerator Params))
 
513
                       (L (mv-nth 0 (scheduling
 
514
                                     (routing m (NodeSetGenerator Params))
 
515
                                     att)))))
 
516
           :in-theory (disable TrLstp Missivesp 
 
517
                               Correctroutesp-Vm-Frms-Gc1        
 
518
                               subsetp-scheduled-delayed-ids
 
519
                               Scheduling-Preserves-Route-Correctness
 
520
                               Scheduled/Rtg_not_modify_frames))))
 
521
 
 
522
(defthm GeNoC_t-thm 
 
523
  ;; now we can prove the correctness of GeNoC_t
 
524
  (let ((NodeSet (NodeSetGenerator Params)))
 
525
    (implies (and (Missivesp M NodeSet)
 
526
                  (ValidParamsp Params))
 
527
             (mv-let (Cplt Abt)
 
528
                     (GeNoC_t M NodeSet att nil)
 
529
                     (declare (ignore Abt))
 
530
                     (GeNoC_t-correctness Cplt M))))
 
531
  :otf-flg t
 
532
  :hints (("GOAL"
 
533
           :induct (GeNoC_t-non-tail-comp M (NodeSetGenerator Params) Att)
 
534
           :do-not '(eliminate-destructors generalize)
 
535
           :in-theory (disable TrLstp Missivesp)
 
536
           :do-not-induct t)
 
537
          ("Subgoal *1/2"
 
538
           :use 
 
539
           ((:instance trlstp-delayed
 
540
                       (TrLst (routing M (NodeSetGenerator Params))))
 
541
            (:instance subsetp-scheduled-delayed-ids
 
542
                       (TrLst (Routing M (NodeSetGenerator Params))))
 
543
            (:instance GC1_scheduled/Rtg))
 
544
           :in-theory (e/d (mv-nth) 
 
545
                           (TrLstp missivesp trlstp-delayed
 
546
                                   subsetp-scheduled-delayed-ids
 
547
                                   GC1_scheduled/Rtg)))))
 
548
                               
 
549
;;------------------------------------------------------------
 
550
;;      Definition and Validation of GeNoC
 
551
;;------------------------------------------------------------
 
552
 
 
553
;; we load the generic definitions of the interfaces
 
554
(include-book "GeNoC-interfaces")
 
555
 
 
556
;; ComputeMissives
 
557
;; --------------
 
558
(defun ComputeMissives (Transactions)
 
559
  ;; apply the function p2psend to build a list of missives
 
560
  ;; from a list of transactions
 
561
  (if (endp Transactions)
 
562
      nil
 
563
    (let* ((trans (car Transactions))
 
564
           (id (IdT trans))
 
565
           (org (OrgT trans))
 
566
           (msg (MsgT trans))
 
567
           (dest (DestT trans)))
 
568
      (cons (list id org (p2psend msg) dest)
 
569
            (ComputeMissives (cdr Transactions))))))
 
570
 
 
571
;; ComputeResults
 
572
;; -------------
 
573
(defun ComputeResults (TrLst)
 
574
  ;; apply the function p2precv to build a list of results
 
575
  ;; from a list of travels
 
576
  (if (endp TrLst)
 
577
      nil
 
578
    (let* ((tr (car TrLst))
 
579
           (id (IdV tr))
 
580
           (r (car (routesV tr)))
 
581
           (dest (car (last r)))
 
582
           (frm (FrmV tr)))
 
583
      (cons (list id dest (p2precv frm))
 
584
            (ComputeResults (cdr TrLst))))))
 
585
 
 
586
;; GeNoC
 
587
;; -----
 
588
(defun GeNoC (Trs NodeSet att)
 
589
  ;; main function
 
590
  (mv-let (Responses Aborted)
 
591
          (GeNoC_t (ComputeMissives Trs) NodeSet att nil)
 
592
          (mv (ComputeResults Responses) Aborted)))
 
593
 
 
594
;; GeNoC Correctness
 
595
;; -----------------
 
596
(defun genoc-correctness (Results Trs/ids)
 
597
  ;; Trs/ids is the initial list of transactions filtered according
 
598
  ;; to the ids of the list of results. 
 
599
  ;; We check that the messages and the destinations of these two lists
 
600
  ;; are equal.
 
601
  (and (equal (R-msgs Results)
 
602
              (T-msgs Trs/ids))
 
603
       (equal (R-dests Results)
 
604
              (T-dests Trs/ids))))
 
605
 
 
606
(defthm M-ids-computesmissives
 
607
  ;; lemma for the next defthm
 
608
  (equal (M-ids (computemissives Trs))
 
609
         (T-ids trs)))
 
610
 
 
611
(defthm missivesp-computemissives
 
612
  (implies (transactionsp trs NodeSet)
 
613
           (missivesp (ComputeMissives trs) NodeSet)))
 
614
 
 
615
 
 
616
(defun all-frms-equal-to-p2psend (TrLst Trs)
 
617
  ;; check that every frame of TrLst is equal to the application
 
618
  ;; of p2psend to the corresponding message in the list of 
 
619
  ;; transactions Trs
 
620
  (if (endp TrLst)
 
621
      (if (endp Trs) 
 
622
          t
 
623
        nil)
 
624
    (let* ((tr (car TrLst))
 
625
           (trans (car Trs))
 
626
           (tr-frm (FrmV tr))
 
627
           (t-msg (MsgT trans)))
 
628
      (and (equal tr-frm (p2psend t-msg))
 
629
           (all-frms-equal-to-p2psend (cdr TrLst) (cdr Trs))))))
 
630
 
 
631
(defthm GC1-=>-all-frms-equal-to-p2psend
 
632
  (implies (GeNoC_t-correctness1 TrLst (ComputeMissives Trs))
 
633
           (all-frms-equal-to-p2psend TrLst Trs)))
 
634
 
 
635
(defthm all-frms-equal-r-msgs-t-msgs
 
636
  ;; if frames have been computed by p2psend then
 
637
  ;; computeresults applies p2precv. We get thus the initial msg.
 
638
  (implies (and (all-frms-equal-to-p2psend TrLst Trs)
 
639
                (validfields-trlst TrLst))
 
640
           (equal (R-msgs (ComputeResults TrLst))
 
641
                  (T-msgs Trs))))
 
642
 
 
643
(defthm R-ids-computeresults
 
644
  (equal (R-ids (computeresults x))
 
645
         (V-ids x)))
 
646
 
 
647
(defthm m-dests-computemissives
 
648
  (equal (M-dests (computeMissives trs))
 
649
         (T-dests trs)))
 
650
 
 
651
 
 
652
(defthm GC1-r-dest-m-dests
 
653
  (implies (and (GeNoC_t-correctness1 TrLst M/TrLst)
 
654
                (validfields-trlst TrLst)
 
655
                (Missivesp M/TrLst NodeSet))
 
656
           (equal (R-dests (ComputeResults TrLst))
 
657
                  (M-dests M/TrLst))))
 
658
 
 
659
(defthm validfields-append
 
660
  ;; lemma for the next defthm
 
661
  (implies (and (validfields-trlst l1)
 
662
                (validfields-trlst l2))
 
663
           (validfields-trlst (append l1 l2))))
 
664
 
 
665
 
 
666
(defthm validfields-trlst-GeNoC_nt
 
667
  ;; to use the lemma all-frms-equal-to-p2psend we need to establish
 
668
  ;; that GeNoC_nt contains travels with validfields
 
669
  ;; and that it contains no duplicated ids
 
670
  (let ((NodeSet (NodeSetGenerator Params)))
 
671
    (implies (and (Missivesp M NodeSet)
 
672
                  (ValidParamsp Params))
 
673
             (validfields-trlst (genoc_t-non-tail-comp M NodeSet att))))
 
674
  :otf-flg t
 
675
  :hints (("GOAL"
 
676
           :do-not-induct t
 
677
           :induct (Genoc_T-Non-Tail-Comp M (NodeSetGenerator Params) att))
 
678
          ("Subgoal *1/2"
 
679
           :use ((:instance trlstp-delayed
 
680
                            (TrLst (Routing M (NodeSetGenerator Params))))
 
681
                 (:instance trlstp-scheduled
 
682
                            (TrLst (Routing M (NodeSetGenerator Params))))
 
683
                 (:instance Missivesp-mv-nth-1-scheduling
 
684
                            (TrLst (routing M (NodeSetGenerator Params)))))
 
685
           :in-theory (disable trlstp-delayed trlstp-scheduled
 
686
                               Missivesp-mv-nth-1-scheduling))))
 
687
 
 
688
;; the next four lemmas are similar to those used to prove
 
689
;; the lemma tomissives-extract-sublst .... (proof by analogy)
 
690
 
 
691
(defthm computemissives-append
 
692
  (equal (computemissives (append a b))
 
693
         (append (computemissives a) (computemissives b))))
 
694
 
 
695
(defthm member-equal-assoc-equal-not-nil-t-ids
 
696
  ;; if e is an Id of a travel of L
 
697
  ;; then (assoc-equal e L) is not nil
 
698
  (implies (and (member-equal e (T-ids Trs))
 
699
                (Validfields-T Trs))
 
700
           (assoc-equal e Trs)))
 
701
 
 
702
(defthm computemissives-assoc-equal
 
703
  ;; if (assoc-equal e L) is not nil then we can link
 
704
  ;; assoc-equal and computemissives as follows:
 
705
  ;; (this lemma is needed to prove the next defthm)
 
706
  (implies (assoc-equal e L)
 
707
           (equal (computemissives (list (assoc-equal e L)))
 
708
                  (list (assoc-equal e (computemissives L))))))
 
709
 
 
710
(defthm computemissives-extract-sublst
 
711
  ;; calls of computemissives are moved into calls
 
712
  ;; of extract-sublst
 
713
  (implies (and (subsetp ids (t-ids trs))
 
714
                (validfields-t trs))
 
715
           (equal (ComputeMissives (extract-sublst trs ids))
 
716
                  (extract-sublst (ComputeMissives trs) ids)))
 
717
  :otf-flg t
 
718
  :hints (("GOAL"
 
719
           :induct (extract-sublst Trs ids)
 
720
           :do-not-induct t
 
721
           :in-theory (disable computemissives append))))
 
722
 
 
723
 
 
724
(defthm m-dest-t-dests-extract-sublst
 
725
  (implies (and (subsetp ids (t-ids trs))
 
726
                (validfields-t trs))
 
727
           (equal (m-dests (extract-sublst (computemissives Trs) ids))
 
728
                  (t-dests (extract-sublst trs ids))))
 
729
  :hints (("GOAL"
 
730
           :do-not-induct t
 
731
           :use (:instance m-dests-computemissives
 
732
                           (Trs (extract-sublst Trs ids)))
 
733
           :in-theory (disable m-dests-computemissives))))
 
734
 
 
735
(defthm fwd-chaining-transactionsp
 
736
  (implies (Transactionsp Trs NodeSet)
 
737
           (and (validfields-t Trs)
 
738
                (true-listp trs)
 
739
                (subsetp (t-orgs trs) nodeset)
 
740
                (subsetp (t-dests trs) nodeset)
 
741
                (no-duplicatesp-equal (t-ids trs))))
 
742
  :rule-classes :forward-chaining)
 
743
 
 
744
(defthm GeNoC-is-correct
 
745
  (let ((NodeSet (NodeSetGenerator Params)))
 
746
    (mv-let (results aborted)
 
747
            (GeNoC Trs NodeSet att)
 
748
            (declare (ignore aborted))
 
749
            (implies (and (Transactionsp Trs NodeSet)
 
750
                          (equal NodeSet (NodeSetGenerator Params))
 
751
                          (ValidParamsp Params))
 
752
                     (GeNoC-correctness
 
753
                      results
 
754
                      (extract-sublst Trs (R-ids results))))))
 
755
  :otf-flg t
 
756
  :hints (("GOAL"
 
757
           :do-not-induct t
 
758
           :use ((:instance GeNoC_t-thm 
 
759
                            (M (ComputeMissives Trs)))
 
760
                 (:instance v-ids-GeNoC_t-non-tail-comp
 
761
                            (M (computemissives trs)))
 
762
                 (:instance all-frms-equal-r-msgs-t-msgs
 
763
                            (TrLst (genoc_t-non-tail-comp
 
764
                                    (computeMissives trs)
 
765
                                    (Nodesetgenerator params) att))
 
766
                            (Trs (extract-sublst Trs 
 
767
                                                 (v-ids 
 
768
                                                  (genoc_t-non-tail-comp
 
769
                                                   (computeMissives trs)
 
770
                                                   (nodesetgenerator params)
 
771
                                                   att)))))
 
772
                 (:instance GC1-r-dest-m-dests
 
773
                            (TrLst (genoc_t-non-tail-comp
 
774
                                    (computeMissives trs)
 
775
                                    (nodesetgenerator params) att))
 
776
                            (M/TrLst 
 
777
                             (extract-sublst (ComputeMissives Trs)
 
778
                                             (V-ids (genoc_t-non-tail-comp
 
779
                                                     (computeMissives trs)
 
780
                                                     (nodesetgenerator params) 
 
781
                                                     att))))
 
782
                            (NodeSet (Nodesetgenerator params))))
 
783
           :in-theory (e/d (mv-nth)
 
784
                           (GeNoC_t-thm missivesp trlstp
 
785
                            all-frms-equal-r-msgs-t-msgs
 
786
                            v-ids-GeNoC_t-non-tail-comp
 
787
                            transactionsp GC1-r-dest-m-dests)))))