3
;; top level module of GeNoC
8
;;Edited 3rd march 2008 to add the round robin
9
(begin-book);$ACL2s-Preamble$|#
13
(include-book "GeNoC-scheduling")
14
(include-book "GeNoC-routing")
15
(include-book "GeNoC-departure")
16
(include-book "GeNoC-simulation")
17
(in-theory (disable mv-nth))
19
(defun genoc_t (m nodeset measure trlst accup time ntkstate order)
20
;; the composition of routing and scheduling is built by function genoc_t.
21
;; it takes as arguments:
22
;; - a list of missives, m
23
;; - the set of existing nodes, nodeset
24
;; - the measure provided by the scheduler
25
;; - an accumulator of arrived messages
26
;; - an accumulator of network states for simulation
28
;; - the state of the network
31
;; - the arrived messages
32
;; - the en route messages
33
;; - the network state accumulator
35
;; the measure is set to the measure defined by the scheduler
36
(declare (xargs :measure (acl2-count measure)))
38
;; no more messages to send
41
(mv-let (delayed departing)
42
;; call R4D to determine which missives are ready for departure
43
(readyfordeparture m nil nil time)
44
;; determine set of routes for all departing missives
45
(let ((v (routing departing nodeset)))
46
(cond ((not (legal-measure measure v nodeset ntkstate order))
47
;; illegal measure supplied
49
;; check if it is possible to schedule
50
((scheduling-assumptions v nodeset ntkstate order)
51
;; schedule and recursivily call genoc_t
52
(mv-let (newtrlst arrived newmeasure newntkstate)
53
(scheduling v nodeset ntkstate order)
54
(genoc_t (append newtrlst delayed)
57
(append arrived trlst)
58
(append accup (list (extract-simulation newntkstate)))
61
(get_next_priority order))))
63
;; scheduler has instructed to terminate
64
(mv trlst m accup)))))))
68
;; correctness of genoc_t
69
;; ----------------------
70
(defun correctroutes-genoc_t (routes m-dest)
71
;; genoc_t is correct if every element ctr of the output list
72
;; is such that (a) frmv(ctr) = frmtm(m) and (b) forall r in
73
;; routesv(ctr) last(r) = desttm(m). for the m such that
75
;; this function checks that (b) holds.
78
(let ((r (car routes)))
79
(and (equal (car (last r)) m-dest)
80
(correctroutes-genoc_t (cdr routes) m-dest)))))
82
(defun genoc_t-correctness1 (trlst m/trlst)
83
;; we complement the correctness of genoc_t
88
(let* ((tr (car trlst))
94
(and (equal v-frm m-frm)
95
(correctroutes-genoc_t routes m-dest)
96
(genoc_t-correctness1 (cdr trlst) (cdr m/trlst))))))
98
(defun genoc_t-correctness (trlst m)
99
;; before checking correctness we filter m
100
;; according to the ids of trlst
101
(let ((m/trlst (extract-sublst (tomissives m) (v-ids trlst))))
102
(genoc_t-correctness1 trlst m/trlst)))
105
;; non tail definition of genoc_t
106
;; ------------------------------
107
(defun genoc_t-non-tail-comp (m nodeset measure time ntkstate order)
108
(declare (xargs :measure (acl2-count measure)))
109
;; we define a non tail function that computes the
110
;; first output of genoc_t, i.e the completed transactions
113
(mv-let (delayed departing)
114
(readyfordeparture m nil nil time)
115
(let ((v (routing departing nodeset)))
116
(cond ((not (legal-measure measure v nodeset ntkstate order))
118
((scheduling-assumptions v nodeset ntkstate order)
119
(mv-let (newtrlst arrived newmeasure newntkstate)
120
(scheduling v nodeset ntkstate order)
121
(append (genoc_t-non-tail-comp (append newtrlst delayed)
126
(get_next_priority order))
130
;; we now prove that this function is right
132
(defthm true-listp-genoc_t-non-tail-comp ;; ok
133
(implies (true-listp m)
134
(true-listp (genoc_t-non-tail-comp m nodeset measure time ntkstate order)))
135
:rule-classes :type-prescription)
137
(defthm genoc_t-non-tail-=-tail-comp ;; ok
138
(equal (mv-nth 0 (genoc_t m nodeset measure trlst accup time ntkstate order))
139
(append (genoc_t-non-tail-comp m nodeset measure time ntkstate order)
143
;; proof of genoc_t correctness
144
;; ----------------------------
146
;; first we add a lemma that tells acl2 that
147
;; converting the travels that are routed and delayed
148
;; produced a valid list of missives
149
(defthm tmissivesp-mv-nth-0-scheduling-routing ;; ok
150
(let ((nodeset (nodesetgenerator params)))
151
(implies (and (tmissivesp m nodeset)
152
(validparamsp params))
153
(tmissivesp (mv-nth 0 (scheduling (routing m nodeset)
157
:use ((:instance tmissivesp-mv-nth-0-scheduling
158
(trlst (routing m (nodesetgenerator params)))))
159
:in-theory (disable trlstp tmissivesp))))
162
;; the next three theorems are to be moved in to the file GeNoC-misc
163
;; the recursive call of genoc_t-non-tail-comp calls append
164
;; we put the append at the top.
165
;; to do so we add the two rules below:
168
;; the ids of an append is the append of the ids
169
(equal (v-ids (append a b))
170
(append (v-ids a) (v-ids b))))
172
(defthm tm-ids-append
173
;; the ids of an append is the append of the ids
174
(equal (tm-ids (append a b))
175
(append (tm-ids a) (tm-ids b))))
177
(defthm extract-sublst-append
178
;; filtering according to an append is the append
180
(equal (extract-sublst m (append id1 id2))
181
(append (extract-sublst m id1)
182
(extract-sublst m id2))))
185
;; then to split the proof is two cases, we replace the
186
;; append by a conjunction.
187
;; the rule below allows this decomposition:
189
(defthm correctroutess1-append
190
(implies (and (equal (len a) (len c))
191
(equal (len b) (len d)))
192
(equal (genoc_t-correctness1 (append a b)
194
(and (genoc_t-correctness1 a c)
195
(genoc_t-correctness1 b d)))))
200
;; now we need to prove some lemmas so that previous rules
201
;; (from genoc-misc) about extract-sublst, tomissives, etc could
204
;next thoerem is to prove that the append of the result of the
205
;scheduling to a a list of tmissives will result in a tmissives list
207
(defthm sched-rout-missivesp-append
208
(implies (and (validparamsp params)
209
(not-in (tm-ids x) (tm-ids y))
210
(tmissivesp x (nodesetgenerator params))
211
(tmissivesp y (nodesetgenerator params)))
216
(routing x (nodesetgenerator params))
217
(nodesetgenerator params) ntkstate order)) y)
218
(nodesetgenerator params)))
220
:use ((:instance tmissivesp-append-tmissivesp
230
(:instance tmissivesp-newTrlst
231
(trlst (routing x (nodesetgenerator params))))
232
(:instance trlstp-routing (m x))
233
(:instance subsetp-arrived-newtrlst-ids
234
(trlst (routing x (nodesetgenerator params)))
235
(nodeset (nodesetgenerator params)))
236
(:instance ids-routing (m x))))))
238
(defthm v-ids-genoc_t-non-tail-comp ;; ok
239
;; the ids of the output of genoc_t-non-tail-comp is a
240
;; subset of those of m
241
;; for this theorem the rule ids-routing is useful
242
(let ((nodeset (nodesetgenerator params)))
243
(implies (and (tmissivesp m nodeset)
244
(validparamsp params))
246
(genoc_t-non-tail-comp m nodeset measure time ntkstate order)))
247
(subsetp (v-ids gnt) (tm-ids m)))))
250
(disable mv-nth tmissivesp trlstp))
252
:do-not '(eliminate-destructors generalize)
253
:use ((:instance tmissivesp-append-tmissivesp
254
(nodeset (nodesetgenerator params))
255
(b (mv-nth 0 (readyfordeparture m nil nil time)))
261
(readyfordeparture m nil nil
263
(nodesetgenerator params))
264
(nodesetgenerator params)
267
(:instance subsetp-arrived-newtrlst-ids
268
(trlst (routing (mv-nth 1
273
(nodeset (nodesetgenerator params)))
274
(:instance ids-routing (m (mv-nth 1
278
:in-theory (disable mv-nth ids-routing
279
subsetp-arrived-newtrlst-ids
282
:in-theory (disable TM-IDS-APPEND GENOC_T-NON-TAIL-COMP TMISSIVESP)
283
:use ((:instance ids-routing (m (mv-nth 1
286
(:instance tmissivesp-append-tmissivesp
287
(nodeset (nodesetgenerator params))
288
(b (mv-nth 0 (readyfordeparture m nil nil time)))
289
(a (mv-nth 0 (scheduling
293
(readyfordeparture m nil
296
(nodesetgenerator params))
297
(nodesetgenerator params)
299
("subgoal *1/2''" :in-theory (enable TM-IDS-APPEND GENOC_T-NON-TAIL-COMP TMISSIVESP))))
302
(defthm not-in-v-ids-genoc_t-non-tail-comp ;; ok
303
;; if the ids of a list have no common element with
304
;; another ids then the output of genoc_t-non-tail-comp does
305
;; not introduce any new id
306
(let ((nodeset (nodesetgenerator params)))
307
(implies (and (not-in (tm-ids delayed) sched-ids)
308
(tmissivesp delayed nodeset)
309
(validparamsp params))
310
(not-in (v-ids (genoc_t-non-tail-comp delayed nodeset measure
317
:in-theory (disable tmissivesp))))
319
(defthm v-ids-genoc_t-non-tail-comp-no-dup ;; ok
320
;; the ids of the output of genoc_t-non-tail-comp have no dup
321
(let ((nodeset (nodesetgenerator params)))
322
(implies (and (tmissivesp m nodeset)
323
(validparamsp params))
324
(let ((gnt (genoc_t-non-tail-comp m nodeset measure time
326
(no-duplicatesp-equal (v-ids gnt)))))
329
:do-not '(eliminate-destructors generalize)
331
:induct (genoc_t-non-tail-comp m (nodesetgenerator params)
332
measure time ntkstate order)
333
:in-theory (disable tmissivesp trlstp ))
335
:use ((:instance trlstp-routing
336
(m (mv-nth 1 (readyfordeparture m nil nil time))))
337
(:instance not-in->not-insched
344
(readyfordeparture m nil
347
(nodesetgenerator params))
349
(nodesetgenerator params) ntkstate order))))
351
(mv-nth 1 (readyfordeparture m nil nil time))))
353
(mv-nth 0 (readyfordeparture m nil nil time)))))
354
(:instance not-in-2->not-in-append
360
1 (readyfordeparture m nil
363
(nodesetgenerator params))
365
(nodesetgenerator params)
368
(mv-nth 0 (readyfordeparture m nil nil time))))
374
(readyfordeparture m nil
377
(nodesetgenerator params))
378
(nodesetgenerator params)
380
(:instance not-in-v-ids-genoc_t-non-tail-comp
388
(readyfordeparture m nil nil time))
389
(nodesetgenerator params))
391
(nodesetgenerator params)
394
(readyfordeparture m nil nil time))))
402
(readyfordeparture m nil nil
404
(nodesetgenerator params))
405
(nodesetgenerator params) ntkstate order)))
412
(mv-nth 1 (readyfordeparture m nil
415
(nodesetgenerator params))
416
(nodesetgenerator params)ntkstate order))))
418
(order (get_next_priority order))
425
1 (readyfordeparture m nil nil time))
426
(nodesetgenerator params))
427
(nodesetgenerator params) ntkstate order))))
428
(:instance not-in-1-0-ready-for-dept
429
(nodeset (nodesetgenerator params)))
430
(:instance subsetp-arrived-newtrlst-ids
431
(trlst (routing (mv-nth
433
(readyfordeparture m nil
436
(nodesetgenerator params)))
437
(nodeset (nodesetgenerator params)))
438
(:instance not-in-newtrlst-arrived
439
(trlst (routing (mv-nth
441
(readyfordeparture m nil
444
(nodesetgenerator params)))
445
(nodeset (nodesetgenerator params)))
446
(:instance trlstp-arrived
447
(trlst (routing (mv-nth 1
450
(nodesetgenerator params)))
451
(nodeset (nodesetgenerator params))))
452
:in-theory (e/d (trlstp)
453
(trlstp-arrived mv-nth trlstp
454
not-in-v-ids-genoc_t-non-tail-comp
457
:use ((:instance not-in-1-0-ready-for-dept-reverse
458
(nodeset (nodesetgenerator params)))))))
460
;; move to GeNoC-misc
461
(defthm tmissivesp-extract-sublst
462
(let ((nodeset (nodesetgenerator params)))
463
(implies (and (tmissivesp m nodeset)
464
(validparamsp params)
466
(no-duplicatesp-equal ids)
467
(subsetp ids (tm-ids m)))
468
(tmissivesp (extract-sublst m ids) nodeset)))
470
:in-theory (disable tmissivesp))
472
:in-theory (enable tmissivesp))))
473
;; the following 7 theorems are intermediate lemmas to prove the
475
;; Tomissives-delayed-ultimate which is that too-missives newtrlst is
476
;; equal to tomissive to extract-sublst from the initial M based upon
477
;; the newtrlst's ids
479
(defthm tomissives-delayed/rtg
480
;; we prove that the conversion of the delayed travels
481
;; into a list of missives is equal to the filtering
482
;; of the initial list of missives m according to the ids
483
;; of the delayed travels.
484
(let ((nodeset (nodesetgenerator params)))
485
(mv-let (newtrlst/rtg arrived/rtg newmeasure newntkstate)
486
(scheduling (routing m nodeset) nodeset ntkstate order)
487
(declare (ignore arrived/rtg newmeasure newntkstate))
488
(implies (and (tmissivesp m nodeset)
489
(validparamsp params))
490
(equal (tomissives newtrlst/rtg)
491
(extract-sublst (tomissives m)
492
(tm-ids newtrlst/rtg))))))
496
:do-not '(eliminate-destructors generalize fertilize)
497
:use ((:instance totmissives-extract-sublst
498
(l (routing m (nodesetgenerator params)))
502
(routing m (nodesetgenerator params))
503
(nodesetgenerator params)
505
(:instance newtrlst-travel-correctness
506
(trlst (routing m (nodesetgenerator params)))
507
(nodeset (nodesetgenerator params)))
508
(:instance subsetp-arrived-newtrlst-ids
509
(trlst (routing m (nodesetgenerator params)))
510
(nodeset (nodesetgenerator params))))
511
:in-theory (disable binary-append nth-with-large-index
512
extract-sublst tm-ids
513
member-equal-tm-ids-assoc-equal
514
tomissives m-ids assoc-equal trlstp
515
missivesp totmissives-extract-sublst
516
len subsetp-arrived-newtrlst-ids))))
518
(defthm newtrlst-subsetp-ready-4-dept
519
(let ((nodeset (nodesetgenerator params)))
520
(mv-let (newtrlst/rtg arrived/rtg newmeasure newntkstate)
523
(readyfordeparture m nil nil time))
525
nodeset ntkstate order)
526
(declare (ignore arrived/rtg newmeasure newntkstate))
527
(implies (and (tmissivesp m nodeset)
528
(validparamsp params))
529
(subsetp(tm-ids newtrlst/rtg)
530
(tm-ids (extract-sublst
540
:in-theory (disable tm-orgs extract-sublst m-ids
542
mv-nth-0-scheduling-on-zero-measure
543
id-not-eq-car-member-cdr-missives
545
subset-ready-for-departure-3
546
not-in-1-0-ready-for-dept
548
checkroutes-subsetp-validroute
549
true-listp-mv-nth-1-sched-2
550
subset-ready-for-departure-2
551
true-listp-last last consp-last
552
subsetp-arrived-newtrlst-ids
553
len nth tmissivesp-extract-sublst
554
tmissivesp-extract trlstp-routing
556
leq-position-equal-len
557
member-equal-m-ids-assoc-equal v-ids
560
:use ((:instance subsetp-arrived-newtrlst-ids
564
(readyfordeparture m nil nil
566
(nodesetgenerator params)))
567
(nodeset (nodesetgenerator params)))
568
(:instance trlstp-routing
569
(m (mv-nth 1 (readyfordeparture m nil nil time))))
570
(:instance subset-ready-for-departure-3
571
(nodeset (nodesetgenerator params)))
572
(:instance tmissivesp-ready-4-departure-mv-1
573
(nodeset (nodesetgenerator params)))
574
(:instance subset-ready-for-departure-2
575
(nodeset (nodesetgenerator params)))
576
(:instance tmissivesp-equal-subsetp
577
(nodeset (nodesetgenerator params))
578
(x (mv-nth 1 (readyfordeparture m nil nil
581
(:instance tmissivesp-ready-4-departure-mv-1
582
(nodeset (nodesetgenerator params)))))))
587
(defthm newtrlst-subsetp-M
588
(let ((nodeset (nodesetgenerator params)))
589
(mv-let (newtrlst/rtg arrived/rtg new newntkstate)
590
(scheduling (routing (mv-nth 1 (readyfordeparture m nil nil time)) nodeset) nodeset ntkstate order)
591
(declare (ignore arrived/rtg new newntkstate))
592
(implies (and (tmissivesp m nodeset)
593
(validparamsp params))
594
(subsetp (tm-ids newtrlst/rtg) (tm-ids m)))))
596
:in-theory (disable extract-sublst
598
mv-nth-0-scheduling-on-zero-measure
600
subset-ready-for-departure-3
601
not-in-1-0-ready-for-dept
602
checkroutes-subsetp-validroute
603
true-listp-mv-nth-1-sched-2
604
len nth tmissivesp-extract-sublst
606
leq-position-equal-len
607
member-equal-m-ids-assoc-equal v-ids
610
((:instance tmissivesp-ready-4-departure-mv-1
611
(nodeset (nodesetgenerator params)))
612
(:instance subsetp-arrived-newtrlst-ids
616
(readyfordeparture m nil nil time))
617
(nodesetgenerator params)))
618
(nodeset (nodesetgenerator params)))
619
(:instance trlstp-routing
620
(m (mv-nth 1 (readyfordeparture
622
(:instance subset-ready-for-departure-2
623
(nodeset (nodesetgenerator params)))))))
625
(defthm taking-the-to-missives-out
626
(let ((nodeset (nodesetgenerator params)))
627
(mv-let (newtrlst/rtg arrived/rtg newmeasure newntkstate)
632
(readyfordeparture m nil nil time)) nodeset)
633
nodeset ntkstate order)
634
(declare (ignore arrived/rtg newmeasure newntkstate))
635
(implies (and (tmissivesp m nodeset)
636
(validparamsp params))
644
(readyfordeparture m nil nil time)))))
645
(tm-ids newtrlst/rtg))
650
(tm-ids (mv-nth 1 (readyfordeparture m nil
653
(tm-ids newtrlst/rtg)))))))
655
:in-theory (disable tmissivesp tomissives-extract-sublst)
657
((:instance tomissives-extract-sublst
658
(nodeset (nodesetgenerator params))
664
(mv-nth 1 (readyfordeparture m nil nil time))
665
(nodesetgenerator params))
666
(nodesetgenerator params) ntkstate order))))
671
(readyfordeparture m nil nil time))))))
672
(:instance subset-ready-for-departure-2
673
(nodeset (nodesetgenerator params)))
674
(:instance subset-ready-for-departure-3
675
(nodeset (nodesetgenerator params)))
676
(:instance tmissivesp-extract
678
(mv-nth 1 (readyfordeparture m nil nil time))))
679
(nodeset (nodesetgenerator params)))
680
(:instance tmissivesp-ready-4-departure-mv-1
681
(nodeset (nodesetgenerator params)))))
682
("subgoal 2" :in-theory (disable tmissivesp)
684
((:instance tmissivesp-ready-4-departure-mv-1
685
(nodeset (nodesetgenerator params)))
686
(:instance subset-ready-for-departure-2
687
(nodeset (nodesetgenerator params)))
688
(:instance subset-ready-for-departure-3
689
(nodeset (nodesetgenerator params)))
690
(:instance tmissivesp-extract
693
(mv-nth 1 (readyfordeparture m nil nil time))))
694
(nodeset (nodesetgenerator params)))))
697
((:instance subsetp-arrived-newtrlst-ids
699
(mv-nth 1 (readyfordeparture m nil nil
701
(nodesetgenerator params)))
702
(nodeset (nodesetgenerator params)))
703
(:instance trlstp-routing
704
(m (mv-nth 1 (readyfordeparture m nil nil time))))
705
(:instance ids-routing
706
(m (mv-nth 1 (readyfordeparture m nil nil time))))
707
(:instance tmissivesp-ready-4-departure-mv-1
708
(nodeset (nodesetgenerator params)))))))
710
(defthm tomissives-delayed-intermediate-2
711
(let ((nodeset (nodesetgenerator params)))
712
(mv-let (newtrlst/rtg arrived/rtg newmeasure newntkstate)
713
(scheduling (routing (mv-nth 1 (readyfordeparture m nil
716
nodeset) nodeset ntkstate order)
717
(declare (ignore arrived/rtg newmeasure newntkstate))
718
(implies (and (tmissivesp m nodeset)
719
(validparamsp params))
720
(equal (tomissives newtrlst/rtg)
727
1 (readyfordeparture m nil nil time)))))
728
(tm-ids newtrlst/rtg))))))
730
:in-theory (disable TOMISSIVES LEN NTH-WITH-LARGE-INDEX TM-IDS
731
nth assoc-equal MEMBER-EQUAL-TM-IDS-ASSOC-EQUAL
732
MEMBER-EQUAL-M-IDS-ASSOC-EQUAL M-IDS)
733
:use ((:instance tmissivesp-equal-subsetp
735
(nodeset (nodesetgenerator params))
736
(x (mv-nth 1 (readyfordeparture m nil nil time))))
737
(:instance subset-ready-for-departure-3
738
(nodeset (nodesetgenerator params)))
739
(:instance tmissivesp-ready-4-departure-mv-1
740
(nodeset (nodesetgenerator params)))))))
742
(defthm tomissives-delayed-ultimate
743
(let ((nodeset (nodesetgenerator params)))
744
(mv-let (newtrlst/rtg arrived/rtg newmeasure newntkstate)
745
(scheduling (routing (mv-nth 1 (readyfordeparture m nil
748
nodeset) nodeset ntkstate order)
749
(declare (ignore arrived/rtg newmeasure newntkstate))
750
(implies (and (tmissivesp m nodeset)
751
(validparamsp params))
752
(equal (tomissives newtrlst/rtg)
754
(extract-sublst m (tm-ids newtrlst/rtg)))))))
756
:use ((:instance subsetp-arrived-newtrlst-ids
760
(readyfordeparture m nil nil
762
(nodesetgenerator params)))
763
(nodeset (nodesetgenerator params)))
764
(:instance trlstp-routing
766
(readyfordeparture m nil nil time))))
767
(:instance extract-sublst-cancel-tm
770
1 (readyfordeparture m nil nil time))))
771
(id2 (tm-ids newtrlst/rtg)))
772
(:instance tmissivesp-ready-4-departure-mv-1
773
(nodeset (nodesetgenerator params)))))))
775
(defthm tomissives-delayed-ultimate-bis
776
(let ((nodeset (nodesetgenerator params)))
777
(mv-let (newtrlst/rtg arrived/rtg newmeasure newntkstate)
778
(scheduling (routing (mv-nth 1 (readyfordeparture m nil
781
nodeset) nodeset ntkstate order)
782
(declare (ignore arrived/rtg newmeasure newntkstate))
783
(implies (and (tmissivesp m nodeset)
784
(validparamsp params))
785
(equal (tomissives newtrlst/rtg)
786
(extract-sublst (tomissives m )
787
(tm-ids newtrlst/rtg))))))
789
:in-theory (disable subset-ready-for-departure-2
791
tm-orgs id-not-eq-car-member-cdr
792
leq-position-equal-len default-car
793
mv-nth-0-scheduling-on-zero-measure
794
nth-with-large-index tmissivesp
795
true-listp-mv-nth-1-sched-2
796
validfield-route m-ids nfix
798
tomissives-extract-sublst
799
id-not-eq-car-member-cdr-missives m-ids
800
member-equal-tm-ids-assoc-equal
801
len tomissives-delayed-ultimate len
802
assoc-equal member-equal-m-ids-assoc-equal)
804
((:instance subsetp-arrived-newtrlst-ids
807
(mv-nth 1 (readyfordeparture m nil nil time))
808
(nodesetgenerator params)))
809
(nodeset (nodesetgenerator params)))
810
(:instance subset-ready-for-departure-2
811
(nodeset (nodesetgenerator params)))
812
(:instance trlstp-routing
813
(m (mv-nth 1 (readyfordeparture m nil nil time))))
814
(:instance tomissives-extract-sublst
815
(nodeset (nodesetgenerator params))
823
1 (readyfordeparture m nil nil time))
824
(nodesetgenerator params))
825
(nodesetgenerator params) ntkstate order)))))
826
(:instance tmissivesp-ready-4-departure-mv-1
827
(nodeset (nodesetgenerator params)))))))
829
(defthm v-ids_g_nt_sigma_subsetp-v-ids-newtrlst/rtg ;; ok
830
;; this lemma is used in the subsequent proofs
831
;; it makes a fact "explicit"
832
(let ((nodeset (nodesetgenerator params)))
833
(mv-let (newtrlst arrived newmeasure newntkstate)
834
(scheduling (routing m nodeset) nodeset ntkstate order)
835
(declare (ignore arrived newntkstate))
836
(implies (and (tmissivesp m nodeset)
837
(validparamsp params))
840
(genoc_t-non-tail-comp
841
(extract-sublst m (tm-ids newtrlst))
842
nodeset newmeasure time ntkstate order))
843
(tm-ids newtrlst)))))
847
:use ((:instance subsetp-arrived-newtrlst-ids
848
(trlst (routing m (nodesetgenerator params)))
849
(nodeset (nodesetgenerator params)))
850
(:instance tmissivesp-newTrlst
851
(trlst (routing m (nodesetgenerator params)))
852
(nodeset (nodesetgenerator params)))
853
(:instance tmissivesp-extract-sublst
858
(nodesetgenerator params))
863
(:instance fwd-tmissivesp
864
(nodeset (nodesetgenerator params)))
865
;; the following is required because in the conclusion of the
866
;; rule there is call to extract-sublst
867
(:instance v-ids-genoc_t-non-tail-comp
875
(routing m (nodesetgenerator params))
876
(nodesetgenerator params)
881
(routing m (nodesetgenerator params))
882
(nodesetgenerator params)
884
:in-theory (disable subsetp-arrived-newtrlst-ids
885
mv-nth-0-scheduling-on-zero-measure
886
binary-append len tmissivesp-newtrlst
887
v-ids-genoc_t-non-tail-comp tm-ids nfix
888
trlstp tmissivesp))))
890
;; arrived/rtg does not modify frames
891
;; ---------------------------------------
893
(defthm s/d-travel-v-frms
894
(implies (and (trlstp sd-trlst nodeset)
895
(s/d-travel-correctness sd-trlst trlst/sd-ids))
896
(equal (v-frms sd-trlst) (v-frms trlst/sd-ids))))
898
(defthm arrived-v-frms-m-frms ;; ok
899
;; we prove that the frames of the scheduled travels
900
;; are equal to the frames of the conversion of the initial list of travels
901
;; filtered according to the ids of the scheduled travels
902
(mv-let (newtrlst arrived newmeasure newntkstate)
903
(scheduling trlst nodeset ntkstate order)
904
(declare (ignore newtrlst newmeasure newntkstate))
905
(implies (and (trlstp trlst nodeset)
906
(validparamsp params))
907
(equal (v-frms arrived)
910
(extract-sublst trlst (v-ids arrived)))))))
912
:use ((:instance tm-frms-to-v-frms
919
(:instance s/d-travel-v-frms
920
(sd-trlst (mv-nth 1 (scheduling trlst
924
(trlst/sd-ids (extract-sublst
934
(:instance arrived-travels-correctness))
935
:in-theory (disable trlstp s/d-travel-v-frms mv-nth))))
938
(defthm arrived/rtg_not_modify_frames ;; ok
939
;; we prove the the frames of the arrived travels produced
940
;; by scheduling and routing are equal to the frames
941
;; of the initial list of missives
942
(let ((nodeset (nodesetgenerator params)))
943
(mv-let (newtrlst arrived newmeasure newntkstate)
944
(scheduling (routing m nodeset) nodeset ntkstate order)
945
(declare (ignore newtrlst newmeasure newntkstate))
946
(implies (and (tmissivesp m nodeset)
947
(validparamsp params))
948
(equal (v-frms arrived)
951
m (v-ids arrived)))))))
954
:do-not '(eliminate-destructors generalize )
955
:use ((:instance arrived-v-frms-m-frms
956
(trlst (routing m (nodesetgenerator params)))
957
(nodeset (nodesetgenerator params)))
958
(:instance subsetp-arrived-newtrlst-ids
959
(trlst (routing m (nodesetgenerator params)))
960
(nodeset (nodesetgenerator params))))
961
:in-theory (disable trlstp tmissivesp
962
subsetp-arrived-newtrlst-ids
963
arrived-v-frms-m-frms))
965
:use ((:instance totmissives-extract-sublst
966
(l (routing m (nodesetgenerator params)))
971
(routing m (nodesetgenerator params))
972
(nodesetgenerator params)
974
(nodeset (nodesetgenerator params))))
975
:in-theory (disable trlstp tmissivesp
976
subsetp-arrived-newtrlst-ids
977
arrived-v-frms-m-frms ids-routing))))
980
(defthm correctroutesp-vm-frms-gc1 ;; ok
981
;; the correctness of routes and equality of frames imply
982
;; the main predicate (correctness of genoc_t-non-tail-comp)
983
(implies (and (correctroutesp l (extract-sublst m (v-ids l))
986
(tm-frms (extract-sublst m (v-ids l)))))
987
(genoc_t-correctness1 l
988
(tomissives (extract-sublst m (v-ids l)))))
990
:hints (("Goal" :in-theory (disable len nfix assoc-equal
991
member-equal-tm-ids-assoc-equal
992
member-equal-m-ids-assoc-equal
993
true-listp-member-equal))))
996
(defthm gc1_arrived/rtg ;; ok
997
;; we prove the correctness of the arrived travels
998
(let ((nodeset (nodesetgenerator params)))
999
(implies (and (tmissivesp m nodeset)
1000
(validparamsp params))
1001
(mv-let (newtrlst arrived newmeasure newntkstate)
1002
(scheduling (routing m nodeset) nodeset
1004
(declare (ignore newtrlst newmeasure newntkstate))
1005
(genoc_t-correctness1
1007
(tomissives (extract-sublst m (v-ids arrived)))))))
1011
:do-not '(eliminate-destructors generalize )
1013
((:instance subsetp-arrived-newtrlst-ids
1014
(trlst (routing m (nodesetgenerator params)))
1015
(nodeset (nodesetgenerator params)))
1016
(:instance totmissives-extract-sublst
1017
(l (routing m (nodesetgenerator params)))
1022
(routing m (nodesetgenerator params))
1024
(nodesetgenerator params) ntkstate order))))
1025
(nodeset (nodesetgenerator params)))
1026
(:instance scheduling-preserves-route-correctness
1027
(nodeset (nodesetgenerator params))
1028
(trlst (routing m (nodesetgenerator params))))
1029
(:instance correctroutesp-vm-frms-gc1
1030
(nodeset (nodesetgenerator params))
1034
(routing m (nodesetgenerator params))
1035
(nodesetgenerator params) ntkstate order)))))
1036
:in-theory (disable trlstp tmissivesp
1037
correctroutesp-vm-frms-gc1 len
1038
subsetp-arrived-newtrlst-ids
1039
scheduling-preserves-route-correctness
1040
arrived/rtg_not_modify_frames))))
1042
;;tomissives of scheduling + tomissives of ready 0 ----> tomissives m
1045
(let ((nodeset (nodesetgenerator params))
1049
(routing (mv-nth 1 (readyfordeparture m nil nil
1051
(nodesetgenerator params))
1052
(nodesetgenerator params) ntkstate order)))
1056
(routing (mv-nth 1 (readyfordeparture m nil nil
1058
(nodesetgenerator params))
1059
(nodesetgenerator params) ntkstate order)))
1063
(routing (mv-nth 1 (readyfordeparture m nil nil
1065
(nodesetgenerator params))
1066
(nodesetgenerator params) ntkstate order)))
1067
(mv0-r4d (mv-nth 0 (readyfordeparture m nil nil time)))
1068
(order1 (get_next_priority order)))
1069
(implies (and (tmissivesp m nodeset)
1070
(validparamsp params))
1072
(extract-sublst (append
1073
(extract-sublst (tomissives m)
1075
(extract-sublst (tomissives m)
1078
(genoc_t-non-tail-comp
1079
(append mv0-sched mv0-r4d) nodeset
1081
(+ 1 time) mv4-sched order1)))
1082
(extract-sublst (tomissives m)
1083
(v-ids (genoc_t-non-tail-comp
1084
(append mv0-sched mv0-r4d)
1085
nodeset mv3-sched (+ 1 time)
1089
:hints (("goal" :use
1090
((:instance v-ids-genoc_t-non-tail-comp
1097
(readyfordeparture m nil nil
1099
(nodesetgenerator params))
1100
(nodesetgenerator params)
1104
(readyfordeparture m nil nil time))))
1109
1 (readyfordeparture m nil nil
1111
(nodesetgenerator params))
1112
(nodesetgenerator params) ntkstate order)))
1114
(order (get_next_priority order))
1120
(mv-nth 1 (readyfordeparture m nil nil
1122
(nodesetgenerator params))
1123
(nodesetgenerator params) ntkstate order))))
1124
(:instance equalid-tomissives
1125
(nodeset (nodesetgenerator params)))
1126
(:instance tm-ids-append-invert
1127
(nodeset (nodesetgenerator params))
1133
(readyfordeparture m nil nil
1135
(nodesetgenerator params))
1136
(nodesetgenerator params) ntkstate order)))
1137
(b (mv-nth 0 (readyfordeparture m nil nil time))))
1138
(:instance newtrlst-travel-correctness
1139
(nodeset (nodesetgenerator params))
1142
(readyfordeparture m nil nil
1144
(nodesetgenerator params))))
1145
(:instance subsetp-arrived-newtrlst-ids
1147
(mv-nth 1 (readyfordeparture m nil nil
1149
(nodesetgenerator params)))
1150
(nodeset (nodesetgenerator params)))
1151
(:instance extract-sublst-cancel-m
1153
(id1 (tm-ids (append
1160
(readyfordeparture m nil nil
1162
(nodesetgenerator params))
1163
(nodesetgenerator params)
1167
(readyfordeparture m nil nil time))) ))
1168
(id2 (v-ids (genoc_t-non-tail-comp
1175
(readyfordeparture m
1179
(nodesetgenerator params))
1185
(readyfordeparture m nil
1188
(nodesetgenerator params)
1194
(readyfordeparture m
1198
(nodesetgenerator params))
1209
(readyfordeparture m nil nil
1211
(nodesetgenerator params))
1212
(nodesetgenerator params)
1214
(get_next_priority order )))))
1215
(:instance tmissivesp-ready-4-departure-mv-0
1216
(nodeset (nodesetgenerator params)))
1217
(:instance trlstp-routing
1218
(m (mv-nth 1 (readyfordeparture m nil nil time))))
1219
(:instance tmissivesp-append-tmissivesp
1224
1 (readyfordeparture m nil nil time))
1225
(nodesetgenerator params))
1226
(nodesetgenerator params) ntkstate
1228
(b (mv-nth 0 (readyfordeparture m nil nil time)))
1229
(nodeset (nodesetgenerator params)))
1230
(:instance v-ids_g_nt_sigma_subsetp-v-ids-newtrlst/rtg
1237
1 (readyfordeparture m nil nil time))
1238
(nodesetgenerator params))
1239
(nodesetgenerator params) ntkstate
1241
(mv-nth 0 (readyfordeparture m nil nil time))) ))
1242
(:instance tmissivesp-ready-4-departure-mv-1
1243
(nodeset (nodesetgenerator params)))
1244
(:instance not-in-1-0-ready-for-dept-reverse
1245
(nodeset (nodesetgenerator params)))
1246
(:instance not-in-1-0-ready-for-dept
1247
(nodeset (nodesetgenerator params)))
1248
(:instance tmissivesp-newTrlst
1251
(readyfordeparture m nil nil time))
1252
(nodesetgenerator params)))
1253
(nodeset (nodesetgenerator params)))))))
1256
(defthm lemma12final
1257
(let ((nodeset (nodesetgenerator params))
1264
1 (readyfordeparture m nil nil time))
1265
(nodesetgenerator params))
1266
(nodesetgenerator params) ntkstate order)))
1273
1 (readyfordeparture m nil nil time))
1274
(nodesetgenerator params))
1275
(nodesetgenerator params) ntkstate order)))
1282
1 (readyfordeparture m nil nil time))
1283
(nodesetgenerator params))
1284
(nodesetgenerator params) ntkstate order)))
1285
(mv0-r4d (mv-nth 0 (readyfordeparture m nil nil time))))
1286
(implies (and (tmissivesp m nodeset)
1287
(validparamsp params))
1290
(append (extract-sublst (tomissives m)
1292
(tomissives mv0-r4d))
1294
(genoc_t-non-tail-comp
1295
(append mv0-sched mv0-r4d) nodeset mv3-sched
1296
(+ 1 time) mv4-sched (get_next_priority order))))
1300
(genoc_t-non-tail-comp
1301
(append mv0-sched mv0-r4d) nodeset mv3-sched (+ 1
1303
mv4-sched (get_next_priority order)))))))
1305
:in-theory (e/d () (tmissivesp
1306
checkroutes-subsetp-validroute
1308
nil-r4d-nil-mv0 nil-r4d-nil-mv1 zp
1309
; true-listp-genoc_t-non-tail-comp
1311
member-equal-tm-ids-assoc-equal
1312
member-equal-m-ids-assoc-equal tm-ids
1314
:use ((:instance lemma12)
1315
(:instance subset-ready-for-departure-4
1316
(nodeset (nodesetgenerator params)))
1317
(:instance tmissivesp-ready-4-departure-mv-0
1318
(nodeset (nodesetgenerator params)))
1319
(:instance tmissivesp-equal-subsetp
1320
(nodeset (nodesetgenerator params))
1322
(x (mv-nth 0 (readyfordeparture m nil nil time))))
1323
(:instance tmissives-subset-extract-tomissives-equal
1324
(nodeset (nodesetgenerator params))
1329
(readyfordeparture m nil nil time)))))
1330
(:instance subset-ready-for-departure
1331
(nodeset (nodesetgenerator params)))
1332
(:instance subset-ready-for-departure-4
1333
(nodeset (nodesetgenerator params)))
1334
(:instance tmissivesp-ready-4-departure-mv-0
1335
(nodeset (nodesetgenerator params)))))))
1337
(defthm takingtomissivesout-equal
1338
(let ((nodeset (nodesetgenerator params))
1343
(mv-nth 1 (readyfordeparture m nil nil time))
1344
(nodesetgenerator params))
1345
(nodesetgenerator params) ntkstate order))))
1346
(implies (and (tmissivesp M nodeset)
1347
(validparamsp params))
1350
(extract-sublst (mv-nth 1 (readyfordeparture m nil nil time))
1352
(extract-sublst (tomissives
1353
(mv-nth 1 (readyfordeparture m nil nil time)))
1354
(v-ids mv1-sched)))))
1357
:use ((:instance tmissivesp-equal-subsetp
1358
(x (mv-nth 1 (readyfordeparture m nil nil time)))
1359
(nodeset (nodesetgenerator params))
1361
(:instance ToMissives-extract-sublst
1366
(readyfordeparture m nil nil time)))))
1373
1 (readyfordeparture m nil nil time))
1374
(nodesetgenerator params))
1375
(nodesetgenerator params)
1377
(nodeset (nodesetgenerator params)))
1378
(:instance subsetp-arrived-newtrlst-ids
1382
(readyfordeparture m nil nil
1384
(nodesetgenerator params)))
1385
(nodeset (nodesetgenerator params)))))))
1389
(defthm lemma121final
1390
(let ((nodeset (nodesetgenerator params))
1396
1 (readyfordeparture m nil nil time))
1397
(nodesetgenerator params))
1398
(nodesetgenerator params) ntkstate order))))
1399
(implies (and (tmissivesp M nodeset)
1400
(validparamsp params))
1403
(tomissives (mv-nth 1 (readyfordeparture m nil nil time)))
1405
(tomissives (extract-sublst M (v-ids mv1-sched))))))
1407
:in-theory (disable tmissivesp len)
1409
:use ((:instance extract-sublst-cancel-TM
1412
1 (readyfordeparture m nil nil time))))
1420
(readyfordeparture m nil nil time))
1421
(nodesetgenerator params))
1422
(nodesetgenerator params)
1424
(:instance tmissivesp-ready-4-departure-mv-1
1425
(nodeset (nodesetgenerator params)))
1426
(:instance ToMissives-extract-sublst
1431
(readyfordeparture m nil nil time)))))
1438
1 (readyfordeparture m nil nil time))
1439
(nodesetgenerator params))
1440
(nodesetgenerator params)
1442
(nodeset (nodesetgenerator params)))
1443
(:instance ids-routing
1444
(M (mv-nth 1 (readyfordeparture m nil nil time))))
1445
(:instance tmissivesp-equal-subsetp
1446
(x (mv-nth 1 (readyfordeparture m nil nil time)))
1447
(nodeset (nodesetgenerator params))
1449
(:instance subsetp-arrived-newtrlst-ids
1452
1 (readyfordeparture m nil nil
1454
(nodesetgenerator params)))
1455
(nodeset (nodesetgenerator params)))))))
1458
(defthm subset-arrived-tm-ids-M
1459
(implies (and (tmissivesp M (nodesetgenerator params))
1460
(validparamsp params))
1461
(subsetp (V-ids (mv-nth
1466
(readyfordeparture m nil nil time))
1467
(nodesetgenerator params))
1468
(nodesetgenerator params) ntkstate order)))
1471
:in-theory (disable tmissivesp)
1473
((:instance subset-ready-for-departure-2
1474
(nodeset (nodesetgenerator params)))
1475
(:instance tmissivesp-ready-4-departure-mv-1
1476
(nodeset (nodesetgenerator params)))
1477
(:instance ids-routing
1478
(M (mv-nth 1 (readyfordeparture m nil nil time))))
1479
(:instance subsetp-arrived-newtrlst-ids
1483
(readyfordeparture m nil nil time))
1484
(nodesetgenerator params)))
1485
(nodeset (nodesetgenerator params)))))))
1488
(defthm lasttheorem-lemma1211
1489
(let ((nodeset (nodesetgenerator params))
1494
(routing (mv-nth 1 (readyfordeparture m nil nil time))
1495
(nodesetgenerator params))
1496
(nodesetgenerator params) ntkstate order))))
1497
(implies (and (tmissivesp M nodeset)
1498
(validparamsp params))
1499
(equal (extract-sublst (tomissives m)
1501
(tomissives (extract-sublst
1502
(mv-nth 1 (readyfordeparture m nil nil time))
1503
(v-ids mv1-sched))))))
1505
:in-theory (disable tmissivesp)
1506
:use ((:instance lemma121final)
1507
(:instance takingtomissivesout-equal)))))
1508
(defthm true-listp-r4d
1509
(implies (tmissivesp m nodeset)
1510
(true-listp (mv-nth 0 (readyfordeparture m nil nil time))))
1511
:hints (("Goal" :use (tmissivesp-ready-4-departure-mv-0)
1512
:in-theory (disable tmissivesp-ready-4-departure-mv-0)))
1513
:rule-classes :type-prescription)
1515
(defthm genoc_t-thm ;; ok
1516
;; now we can prove the correctness of genoc_t
1517
(let ((nodeset (nodesetgenerator params)))
1518
(implies (and (tmissivesp m nodeset) ;(goodorder order)
1519
(validparamsp params))
1521
(genoc_t m nodeset measure nil accup time ntkstate order)
1522
(declare (ignore abt))
1523
(genoc_t-correctness cplt m))))
1526
:induct (genoc_t-non-tail-comp m (nodesetgenerator params)
1527
measure time ntkstate order)
1528
:do-not '(eliminate-destructors generalize)
1529
:in-theory (disable trlstp tmissivesp lemma121final)
1532
:in-theory (disable tmissivesp mv-nth
1533
extract-sublst-cancel-m
1534
lemma121final trlstp tmissivesp
1537
((:instance gc1_arrived/rtg
1538
(m (mv-nth 1 (readyfordeparture m nil nil time))))
1539
(:instance lasttheorem-lemma1211)
1540
(:instance v-ids-genoc_t-non-tail-comp
1547
(readyfordeparture m nil nil
1549
(nodesetgenerator params))
1550
(nodesetgenerator params)
1553
0 (readyfordeparture m nil nil time))))
1560
(readyfordeparture m nil nil time))
1561
(nodesetgenerator params))
1562
(nodesetgenerator params)
1571
(readyfordeparture m nil nil
1573
(nodesetgenerator params))
1574
(nodesetgenerator params)
1576
(order (get_next_priority order)))
1577
(:instance gc1_arrived/rtg
1578
(m (mv-nth 1 (readyfordeparture m nil nil time))))))
1581
((:instance v-ids-genoc_t-non-tail-comp
1588
1 (readyfordeparture m nil nil time))
1589
(nodesetgenerator params))
1590
(nodesetgenerator params) ntkstate
1592
(mv-nth 0 (readyfordeparture m nil nil time))))
1597
(mv-nth 1 (readyfordeparture m nil nil
1599
(nodesetgenerator params))
1600
(nodesetgenerator params) ntkstate
1608
1 (readyfordeparture m nil nil
1610
(nodesetgenerator params))
1611
(nodesetgenerator params)
1613
(order (get_next_priority order)))))
1615
:in-theory (disable tmissivesp mv-nth
1616
extract-sublst-cancel-m
1617
lasttheorem-lemma1211 lemma12)
1619
((:instance tmissivesp-ready-4-departure-mv-1
1620
(nodeset (nodesetgenerator Params)))
1621
(:instance gc1_arrived/rtg
1622
(M (mv-nth 1 (readyfordeparture m nil nil time))))))
1624
:in-theory (disable tmissivesp mv-nth
1625
extract-sublst-cancel-m
1626
lemma121final lemma12))))#|ACL2s-ToDo-Line|#
1630
;;------------------------------------------------------------
1631
;; definition and validation of genoc
1632
;;------------------------------------------------------------
1634
;; we load the generic definitions of the interfaces
1635
(include-book "interfaces-computes")
1637
;(include-book "GeNoC-interfaces")
1639
;; ComputetTMissives
1641
;(defun computeTMissives (transactions)
1642
;; apply the function p2psend to build a list of tmissives
1643
;; from a list of transactions
1644
;(if (endp transactions)
1646
; (let* ((trans (car transactions))
1648
; (org (orgt trans))
1649
; (msg (msgt trans))
1650
; (dest (destt trans))
1651
; (flit (flitt trans))
1652
; (time (timet trans)))
1653
; (cons (list id org org (p2psend msg) dest flit time)
1654
; (computetmissives (cdr transactions))))))
1659
;(defun computeresults (trlst)
1660
;; apply the function p2precv to build a list of results
1661
;; from a list of travels
1664
; (let* ((tr (car trlst))
1666
; (r (car (routesv tr)))
1667
; (dest (car (last r)))
1669
; (flit (flitv tr)))
1670
; (cons (list id dest (p2precv frm) flit)
1671
; (computeresults (cdr trlst))))))
1677
(defun genoc (trs params params2 order)
1679
(if (ValidStateParamsp params params2)
1680
(mv-let (responses aborted simu)
1681
(genoc_t (computetmissives trs)
1682
(NodesetGenerator params)
1683
(initial-measure (routing (computetmissives trs) (NodesetGenerator params))
1684
(NodesetGenerator params)
1685
(generate-initial-ntkstate trs (stategenerator params params2))
1690
(generate-initial-ntkstate trs (stategenerator params params2))
1692
(declare(ignore simu))
1693
(mv (computeresults responses) aborted))
1696
;; genoc correctness
1697
;; -----------------
1698
(defun genoc-correctness (results trs/ids)
1699
;; trs/ids is the initial list of transactions filtered according
1700
;; to the ids of the list of results.
1701
;; we check that the messages and the destinations of these two lists
1703
(and (equal (r-msgs results)
1705
(equal (r-dests results)
1706
(t-dests trs/ids))))
1708
(defun all-frms-equal-to-p2psend (trlst trs)
1709
;; check that every frame of trlst is equal to the application
1710
;; of p2psend to the corresponding message in the list of
1716
(let* ((tr (car trlst))
1719
(t-msg (msgt trans)))
1720
(and (equal tr-frm (p2psend2 t-msg))
1721
(all-frms-equal-to-p2psend (cdr trlst) (cdr trs))))))
1723
(defthm gc1-=>-all-frms-equal-to-p2psend ;; ok
1724
(implies (genoc_t-correctness1 trlst (tomissives (computetmissives trs)))
1725
(all-frms-equal-to-p2psend trlst trs))
1727
:in-theory (disable last true-listp leq-position-equal-len
1730
(defthm all-frms-equal-r-msgs-t-msgs
1731
;; if frames have been computed by p2psend then
1732
;; computeresults applies p2precv. we get thus the initial msg.
1733
(implies (and (all-frms-equal-to-p2psend trlst trs)
1734
(validfields-trlst trlst nodeset))
1735
(equal (r-msgs (computeresults trlst))
1738
:in-theory (disable last true-listp leq-position-equal-len
1741
(defthm gc1-r-dest-tm-dests ;; ok
1742
(implies (and (genoc_t-correctness1 trlst m/trlst)
1743
(validfields-trlst trlst nodeset)
1744
(missivesp m/trlst nodeset))
1745
(equal (r-dests (computeresults trlst))
1746
(m-dests m/trlst))))
1749
(in-theory (disable mv-nth))
1751
(defthm validfields-trlst-genoc_nt ;; ok
1752
;; to use the lemma all-frms-equal-to-p2psend we need to establish
1753
;; that genoc_nt contains travels with validfields
1754
;; and that it contains no duplicated ids
1755
(let ((nodeset (nodesetgenerator params)))
1756
(implies (and (tmissivesp m nodeset)
1757
(validparamsp params))
1759
(genoc_t-non-tail-comp m nodeset measure time ntkstate
1765
:induct (genoc_t-non-tail-comp m (nodesetgenerator params)
1766
measure time ntkstate order))
1769
((:instance tmissivesp-newTrlst
1771
(mv-nth 1 (readyfordeparture m nil nil time))
1772
(nodesetgenerator params)))
1773
(nodeset (nodesetgenerator params)))
1774
(:instance trlstp-arrived
1776
(mv-nth 1 (readyfordeparture m nil nil time))
1777
(nodesetgenerator params)))
1778
(nodeset (nodesetgenerator params)))
1779
(:instance tmissivesp-mv-nth-0-scheduling
1781
(mv-nth 1 (readyfordeparture m nil nil time))
1782
(nodesetgenerator params)))))
1783
:in-theory (disable tmissivesp-newTrlst trlstp-arrived
1784
tmissivesp-mv-nth-0-scheduling))))
1787
(defthm tm-orgs-computetmissives ;; ok
1788
(equal (tm-orgs (computetmissives trs))
1791
(defthm tm-dests-computetmissives ;; ok
1792
(equal (tm-dests (computetmissives trs))
1797
(defthm tm-ids-computestmissives ;; ok
1798
;; lemma for the next defthm
1799
(equal (tm-ids (computetmissives trs))
1803
(defthm tmissivesp-computetmissives ;; ok
1804
(implies (transactionsp trs nodeset)
1805
(tmissivesp (computetmissives trs) nodeset)))
1809
(defthm Extract-computemissives-tmissivesp-instance
1810
(implies (and (transactionsp trs (nodesetgenerator params))
1811
(validparamsp params))
1813
(extract-sublst (computetmissives trs)
1815
(genoc_t-non-tail-comp (computetmissives trs)
1816
(nodesetgenerator params)
1817
measure time ntkstate order)))
1818
(nodesetgenerator params)))
1821
((:instance v-ids-genoc_t-non-tail-comp
1822
(m (computetmissives trs)))
1823
(:instance tmissivesp-computetmissives
1824
(nodeset (nodesetgenerator params)))
1825
(:instance subset-arrived-tm-ids-M
1826
(M (computetmissives trs)))
1827
(:instance v-ids-genoc_t-non-tail-comp-no-dup
1828
(M (computetmissives trs)))))))
1831
(defthm computetmissives-assoc-equal ;; ok
1832
;; if (assoc-equal e l) is not nil then we can link
1833
;; assoc-equal and computetmissives as follows:
1834
;; (this lemma is needed to prove the next defthm)
1835
(implies (assoc-equal e l)
1836
(equal (computetmissives (list (assoc-equal e l)))
1837
(list (assoc-equal e (computetmissives l))))))
1840
(defthm computetmissives-append ;; ok
1841
(equal (computetmissives (append a b))
1842
(append (computetmissives a)
1843
(computetmissives b))))
1846
(defthm member-equal-assoc-equal-not-nil-t-ids
1847
;; if e is an id of a travel of l
1848
;; then (assoc-equal e l) is not nil
1849
(implies (and (member-equal e (t-ids trs))
1850
(validfields-t trs))
1851
(assoc-equal e trs)))
1853
(defthm computetmissives-extract-sublst ;; ok
1854
;; calls of computetmissives are moved into calls
1855
;; of extract-sublst
1856
(implies (and (subsetp ids (t-ids trs))
1857
(validfields-t trs))
1858
(equal (computetmissives (extract-sublst trs ids))
1859
(extract-sublst (computetmissives trs) ids)))
1862
:induct (extract-sublst trs ids)
1864
:in-theory (disable computetmissives append))))
1867
(defthm computemissives-Extract-tmissivesp-instance
1868
(implies (and (transactionsp trs (nodesetgenerator params))
1869
(validparamsp params))
1874
(genoc_t-non-tail-comp (computetmissives trs)
1875
(nodesetgenerator params)
1879
(nodesetgenerator params)))
1883
((:instance v-ids-genoc_t-non-tail-comp
1884
(m (computetmissives trs)))
1885
(:instance Extract-computemissives-tmissivesp-instance)
1886
(:instance subset-arrived-tm-ids-M
1887
(M (computetmissives trs)))
1888
(:instance v-ids-genoc_t-non-tail-comp-no-dup
1889
(M (computetmissives trs)))
1890
(:instance computetmissives-extract-sublst
1892
(genoc_t-non-tail-comp (computetmissives trs)
1893
(nodesetgenerator params)
1894
measure time ntkstate
1899
(in-theory (disable fwd-chaining-transactionsp))
1902
(implies (and (transactionsp trs (nodesetgenerator params))
1903
(validparamsp params))
1904
(genoc_t-correctness1
1905
(genoc_t-non-tail-comp
1906
(computetmissives trs)
1907
(nodesetgenerator params) measure '0 ntkstate order)
1908
(tomissives (computetmissives
1912
(genoc_t-non-tail-comp
1913
(computetmissives trs) (nodesetgenerator params)
1914
measure '0 ntkstate order)))))))
1915
:hints (("Goal" :use ((:instance v-ids-genoc_t-non-tail-comp
1917
(m (computetmissives trs)))
1918
(:instance tomissives-extract-sublst
1919
(l (computetmissives trs))
1921
(genoc_t-non-tail-comp
1922
(computetmissives trs)
1923
(nodesetgenerator params)
1925
'0 ntkstate order)))
1926
(nodeset (nodesetgenerator params)))
1927
(:instance genoc_t-thm
1929
(m (computetmissives trs)))))))
1932
(defthm gc1-=>-all-frms-equal-to-p2psend-instance ;; ok
1933
(implies (and (transactionsp trs (nodesetgenerator params))
1934
(validparamsp params))
1935
(all-frms-equal-to-p2psend
1936
(genoc_t-non-tail-comp (computetmissives trs)
1937
(nodesetgenerator params)
1938
measure '0 ntkstate order)
1941
(genoc_t-non-tail-comp
1942
(computetmissives trs) (nodesetgenerator params)
1943
measure '0 ntkstate order))))))
1945
(defthm gc1-gnc-trs-inv
1946
(implies (and (transactionsp Trs (nodesetgenerator params))
1947
(validparamsp params))
1948
(genoc_t-correctness1
1949
(genoc_t-non-tail-comp (computetmissives
1950
trs)(nodesetgenerator params) measure
1953
(extract-sublst (computetmissives trs)
1955
(genoc_t-non-tail-comp
1956
(computetmissives trs)
1957
(nodesetgenerator params)
1958
measure '0 ntkstate order))))))
1960
:in-theory (disable transactionsp)
1962
((:instance v-ids-genoc_t-non-tail-comp
1964
(m (computetmissives trs)))
1965
(:instance subset-arrived-tm-ids-M
1967
(M (computetmissives trs)))
1968
(:instance v-ids-genoc_t-non-tail-comp-no-dup
1970
(M (computetmissives trs)))
1971
(:instance tmissivesp-computetmissives
1972
(nodeset (nodesetgenerator params)))
1973
(:instance computetmissives-extract-sublst
1974
(ids (v-ids (genoc_t-non-tail-comp
1975
(computetmissives trs)
1976
(nodesetgenerator params)
1977
measure '0 ntkstate order))))
1978
(:instance gc1-gnc-trs)))))
1981
(defthm all-frms-equal-r-msgs-t-msgs-instance
1982
;; if frames have been computed by p2psend then
1983
;; computeresults applies p2precv. we get thus the initial msg.
1984
(implies (and (transactionsp trs (nodesetgenerator params))
1985
(validparamsp params))
1986
(equal (r-msgs (computeresults
1987
(genoc_t-non-tail-comp
1988
(computetmissives trs)(nodesetgenerator
1990
measure '0 ntkstate order)))
1991
(t-msgs (extract-sublst
1994
(genoc_t-non-tail-comp
1995
(computetmissives trs) (nodesetgenerator params)
1996
measure '0 ntkstate order))))))
1999
((:instance validfields-trlst-genoc_nt
2001
(m (computetmissives trs)))
2002
(:instance all-frms-equal-r-msgs-t-msgs
2003
(nodeset (nodesetgenerator params))
2004
(trlst (genoc_t-non-tail-comp
2005
(computetmissives trs)
2006
(nodesetgenerator params) measure '0
2008
(trs (extract-sublst
2010
(v-ids (genoc_t-non-tail-comp
2011
(computetmissives trs)
2012
(nodesetgenerator params)
2013
measure '0 ntkstate order)))))))))
2015
(defthm r-ids-computeresults
2016
(equal (r-ids (computeresults x))
2019
(defthm all-frms-equal-r-msgs-t-msgs-instance-use
2020
;; if frames have been computed by p2psend then
2021
;; computeresults applies p2precv. we get thus the initial msg.
2022
(implies (and (transactionsp trs (nodesetgenerator params))
2023
(validparamsp params))
2026
(genoc_t-non-tail-comp (computetmissives trs)
2027
(nodesetgenerator params)
2028
measure '0 ntkstate order)))
2029
(t-msgs (extract-sublst
2031
(r-ids(computeresults
2032
(genoc_t-non-tail-comp
2033
(computetmissives trs)
2034
(nodesetgenerator params)
2035
measure '0 ntkstate order))))))))
2038
(defthm gc1-r-dest-tm-dests-inst ;; ok
2039
(implies (and (and (transactionsp trs (nodesetgenerator params))
2040
(validparamsp params)))
2043
(genoc_t-non-tail-comp (computetmissives trs)
2044
(nodesetgenerator params)
2045
measure '0 ntkstate order)))
2046
(m-dests (tomissives
2047
(extract-sublst (computetmissives trs)
2049
(genoc_t-non-tail-comp
2050
(computetmissives trs)
2051
(nodesetgenerator params)
2052
measure '0 ntkstate order)))))))
2053
:hints (("Goal" :in-theory (disable len nfix nth)
2055
((:instance gc1-gnc-trs)
2056
(:instance gc1-r-dest-tm-dests)
2057
(:instance validfields-trlst-genoc_nt
2059
(m (computetmissives trs)))
2060
(:instance to-missives-missivesp
2062
(computetmissives trs)
2064
(genoc_t-non-tail-comp
2065
(computetmissives trs)
2066
(nodesetgenerator params)measure
2067
'0 ntkstate order))))
2068
(nodeset (nodesetgenerator params) ) )
2069
(:instance tmissivesp-computetmissives
2070
(nodeset (nodesetgenerator params)))
2071
(:instance v-ids-genoc_t-non-tail-comp
2073
(m (computetmissives trs)))
2074
(:instance subset-arrived-tm-ids-M
2076
(M (computetmissives trs)))
2077
(:instance v-ids-genoc_t-non-tail-comp-no-dup
2079
(M (computetmissives trs)))
2080
(:instance computetmissives-extract-sublst
2082
(genoc_t-non-tail-comp
2083
(computetmissives trs)
2084
(nodesetgenerator params)
2085
measure '0 ntkstate order))))
2086
(:instance tm-ids-computestmissives )
2087
(:instance gc1-r-dest-tm-dests
2088
(nodeset (nodesetgenerator params))
2089
(trlst (genoc_t-non-tail-comp
2090
(computetmissives trs)
2091
(nodesetgenerator params)
2092
measure '0 ntkstate order))
2093
(m/trlst (tomissives
2095
(computetmissives trs)
2096
(v-ids (genoc_t-non-tail-comp
2097
(computetmissives trs)
2098
(nodesetgenerator params)
2099
measure '0 ntkstate order))))))))))
2101
(defthm gc1-r-dest-tm-dests-inst-use ;; ok
2102
(implies (and (and (transactionsp trs (nodesetgenerator params))
2103
(validparamsp params)))
2106
(genoc_t-non-tail-comp
2107
(computetmissives trs)
2108
(nodesetgenerator params) measure '0 ntkstate order)))
2112
(computetmissives trs)
2113
(r-ids (computeresults
2114
(genoc_t-non-tail-comp
2115
(computetmissives trs)
2116
(nodesetgenerator params)
2117
measure '0 ntkstate order)))))))))
2119
(defthm m-dest-t-dests-extract-sublst ;; ok
2120
(implies (and (subsetp ids (t-ids trs))
2121
(validfields-t trs))
2122
(equal (tm-dests (extract-sublst (computetmissives trs) ids))
2123
(t-dests (extract-sublst trs ids))))
2126
:use (:instance tm-dests-computetmissives
2127
(trs (extract-sublst trs ids)))
2128
:in-theory (disable tm-dests-computetmissives))))
2132
(defthm tm-dests-compute-missives-extract-sublst-use
2133
(implies (and (subsetp ids (t-ids trs))
2134
(transactionsp trs nodeset))
2135
(equal (t-dests (extract-sublst trs ids))
2136
(tm-dests (extract-sublst (computetmissives trs) ids))))
2139
(defthm m-dests-tm-dests
2140
(equal (m-dests (tomissives x))
2143
(defthm m-dests-to-missives-compute-missives-extract-sublst-use
2144
(implies (and (subsetp ids (t-ids trs))
2145
(transactionsp trs nodeset))
2146
(equal (t-dests (extract-sublst trs ids))
2147
(m-dests (tomissives (extract-sublst
2148
(computetmissives trs)
2152
(defthm m-dests-to-missives-compute-missives-extract-sublst-use-instance
2153
(implies (and (transactionsp trs (nodesetgenerator params))
2154
(validparamsp params))
2160
(genoc_t-non-tail-comp (computetmissives trs)
2161
(nodesetgenerator params)
2162
measure '0 ntkstate order)))))
2164
(tomissives (extract-sublst
2165
(computetmissives trs)
2168
(genoc_t-non-tail-comp
2169
(computetmissives trs)
2170
(nodesetgenerator params)
2171
measure '0 ntkstate order))))))))
2174
((:instance m-dests-to-missives-compute-missives-extract-sublst-use
2175
(nodeset (nodesetgenerator params))
2178
(genoc_t-non-tail-comp (computetmissives trs)
2179
(nodesetgenerator params)
2180
measure '0 ntkstate order)))))
2181
(:instance tmissivesp-computetmissives
2182
(nodeset (nodesetgenerator params)))
2183
(:instance v-ids-genoc_t-non-tail-comp
2185
(m (computetmissives trs)))))))
2187
(defthm equality-to-test
2188
(let ((nodeset (nodesetgenerator params)))
2189
(mv-let (results aborted)
2190
(genoc trs params params2 order)
2191
(declare (ignore aborted))
2192
(implies (and (transactionsp trs nodeset)
2193
(validstateparamsp params params2))
2196
(genoc_t-non-tail-comp (computetmissives trs)
2199
(initial-measure (routing (computetmissives trs) (NodesetGenerator params))
2200
(NodesetGenerator params)
2201
(generate-initial-ntkstate trs (stategenerator params params2))
2204
(generate-initial-ntkstate trs (stategenerator params params2))
2211
m-dests-to-missives-compute-missives-extract-sublst-use-instance
2212
(ntkstate (stategenerator params params2))))))
2215
(defthm genoc-is-correct ;; ok
2216
(let ((nodeset (nodesetgenerator params)))
2217
(mv-let (results aborted)
2218
(genoc trs params params2 order)
2219
(declare (ignore aborted))
2220
(implies (and (transactionsp trs nodeset)
2221
(validstateparamsp params params2))
2224
(extract-sublst trs (r-ids results))))))
2226
:hints (("goal" :do-not-induct t
2227
:in-theory (disable equality-to-test len nfix nth)
2229
((:instance all-frms-equal-r-msgs-t-msgs-instance-use )
2230
(:instance equality-to-test )
2232
m-dests-to-missives-compute-missives-extract-sublst-use-instance
2233
(ntkstate (generate-initial-ntkstate trs (stategenerator params params2)))
2234
(measure (initial-measure (routing (computetmissives trs) (NodesetGenerator params))
2235
(NodesetGenerator params)
2236
(generate-initial-ntkstate trs (stategenerator params params2))
b'\\ No newline at end of file'
added
removed
books/workshops/2009/verbeek-schmaltz/verbeek/generic-modules/GeNoC.lisp
