diff options
| author | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
|---|---|---|
| committer | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
| commit | 092176848cbfd27b96c323cc30c54dff4c4a6872 (patch) | |
| tree | 91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/2007/schmaltz/genoc-v1.0 | |
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/2007/schmaltz/genoc-v1.0')
22 files changed, 6447 insertions, 0 deletions
diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/Readme.lsp b/books/workshops/2007/schmaltz/genoc-v1.0/Readme.lsp new file mode 100644 index 0000000..d8902c4 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/Readme.lsp @@ -0,0 +1,98 @@ +((:FILES " +.: +Makefile +Readme.lsp +generic-modules +instantiations + +./generic-modules: +GeNoC-interfaces.lisp +GeNoC-misc.lisp +GeNoC-nodeset.lisp +GeNoC-routing.lisp +GeNoC-scheduling.lisp +GeNoC-types.lisp +GeNoC.lisp +Makefile +readme + +./instantiations: +Makefile +interfaces +nodeset +routing +scheduling + +./instantiations/interfaces: +Makefile +bi-phi-m.lisp + +./instantiations/nodeset: +2D-mesh-nodeset.lisp +Makefile +octagon-nodeset.lisp + +./instantiations/routing: +Makefile +doubleY-routing +octagon-routing +xy-routing + +./instantiations/routing/doubleY-routing: +Makefile +doubleY-routing.lisp + +./instantiations/routing/octagon-routing: +Makefile +getting_rid_of_mod.lisp +mod_lemmas.lisp +routing_defuns.lisp +routing_local_lemmas.lisp +routing_main.lisp + +./instantiations/routing/xy-routing: +Makefile +xy-routing.lisp + +./instantiations/scheduling: +Makefile +circuit-scheduling.lisp +intersect.lisp +packet-scheduling.lisp + +" +) + (:TITLE "GeNoC: A Generic Network On Chip") + (:AUTHOR/S "J. Schmaltz") ; non-empty list of author strings + (:KEYWORDS ; non-empty list of keywords, case-insensitive + "networks on chip" "formal methods" "system design" + ) + (:ABSTRACT +"GeNoC is a generic network model intended to serve as a reference for +the validation of high-level descriptions of networks on chip (NoCs). It formalizes +the interaction between three key components: interfaces, routing algorithms, +and scheduling policies. It also defines a global correctness property: messages reach their expected destination +without modification of their content. To abstract from particular implementations, +GeNoC's components are not explicitly defined. They are constrained to satisfy a +set of properties. Using encapsulation and functional-instantiation, the constrained +for particular components of a given NoC are automatically generated. Their proof is sufficient +to guarantee the overall correctness of this given NoC. +") + (:PERMISSION ; author/s permission for distribution and copying: +"GeNoC v1.0 +Copyright (C) 2007 J. Schmaltz + +This program is free software; you can redistribute it and/or +modify it under the terms of the GNU General Public License +as published by the Free Software Foundation; either version 2 +of the License, or (at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software +Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA +02110-1301, USA.")) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-interfaces.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-interfaces.lisp new file mode 100644 index 0000000..fa962a7 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-interfaces.lisp @@ -0,0 +1,42 @@ +;; Julien Schmaltz +;; Interface Module of GeNoC +;; June 17th +;; File: GeNoC-interfaces.lisp +(in-package "ACL2") + +;;------------------------------------------------------------ +;; +;; INTERFACES +;; +;;------------------------------------------------------------ +(encapsulate + + ( + ;; Any peer has an interface that can send and receive messages + ;; Function p2psend + ;; argument: a message msg and [options] + ;; output: a frame frm + ((p2psend *) => *) + ;; Function p2precv + ;; argument: a frame frm and [options] + ;; output: a message msg + ((p2precv *) => *) + ) + + (local (defun p2psend (msg) msg)) + (local (defun p2precv (frm) frm)) + + (defthm p2p-Correctness + ;; the composition of p2precv and p2psend + ;; is the identity function + (equal (p2precv (p2psend msg)) msg)) + + (defthm p2psend-nil + ;; if msg is nil then p2psend is nil too + (not (p2psend nil))) + +(defthm p2psend-not-nil + ;; if msg is not nil then p2psend is not nil too + (implies msg + (p2psend msg))) +) ;; end of interfaces diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-misc.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-misc.lisp new file mode 100644 index 0000000..22b2593 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-misc.lisp @@ -0,0 +1,251 @@ +;; Julien Schmaltz +;; Misceaneous definitions and lemmas +;; June 20th 2005 +;; File: GeNoC-misc.lisp + +(in-package "ACL2") + +(include-book "GeNoC-types") + +;; ROUTING + +;; The predicates associated with the routing part are: +;; - ValidRoutep +;; - CorrectRoutesp + +(defun ValidRoutep (r m) + ;; a route r is valid according to a missive m if: + ;; a/ the origin of the r is the source node of m + ;; b/ the destination of r is the destination node of m + ;; c/ r is a subset of NodeSet + ;; d/ a route r has a len >= 2 + (and (equal (car r) (OrgM m)) + (equal (car (last r)) (DestM m)) + (not (equal (car R) (car (last R)))))) + +(defun CheckRoutes (routes m NodeSet) + ;; checks that a list of routes is correct according to a missive m + (if (endp routes) + t + (let ((r (car routes))) + (and (ValidRoutep r m) + (subsetp r NodeSet) + (CheckRoutes (cdr routes) m NodeSet))))) + +(defun CorrectRoutesp (TrLst M NodeSet) + (if (endp TrLst) + (if (endp M) + t + nil) + (let* ((tr (car TrLst)) + (msv (car M)) + (routes (RoutesV tr))) + (and (CheckRoutes routes msv NodeSet) + (equal (IdV tr) (IdM msv)) + (equal (FrmV tr) (FrmM msv)) + (CorrectRoutesp (cdr TrLst) (cdr M) NodeSet))))) + +;; TO MISSIVES + +(defun ToMissives (TrLst) + ;; convert a Travel List to a Missive + (if (endp TrLst) + nil + (let* ((tr (car TrLst)) + (frm (FrmV Tr)) + (routes (RoutesV Tr)) + (id (IdV tr))) + (cons (list Id (caar routes) frm (car (last (car routes)))) + (ToMissives (cdr TrLst)))))) + +(defthm correctroutesp-=>-tomissives + (implies (and (CorrectRoutesp TrLst M NodeSet) + (Missivesp M NodeSet) + (TrLstp TrLst)) + (equal (ToMissives TrLst) M))) + +(defthm M-ids-ToMissives-V-ids + (equal (M-ids (ToMissives x)) (V-ids x))) + +(defthm CorrectRoutesp-member-equal + (implies (and (correctRoutesp TrLst (ToMissives TrLst) NodeSet) + (TrLstp TrLst) + (member-equal e (v-ids TrLst))) + (checkroutes (nth 2 (assoc-equal e TrLst)) + (assoc-equal e (ToMissives TrLst)) + NodeSet))) + +;; EXTRACT SUBLIST + +(defun extract-sublst (Lst Ids) + ;; extracts the element with the Id in Ids + ;; the output is ordered according to Ids + (if (endp Ids) + nil + (append (list (assoc-equal (car Ids) Lst)) + (extract-sublst Lst (cdr Ids))))) + + +;; for the proof of the correctness of GeNOC +;; two important lemmas are needed + +;; the first one rewrites (ToMissives (extract-sublst ..)) +;; to (extract-sublst (tomissives) ... ) + +(defthm ToMissives-append + ;; we first link ToMissives and append + (equal (ToMissives (append A B)) + (append (ToMissives A) (ToMissives B)))) + +(defthm member-equal-assoc-equal-not-nil + ;; if e is an Id of a travel of L + ;; then (assoc-equal e L) is not nil + (implies (and (member-equal e (V-ids L)) + (TrLstp L)) + (assoc-equal e L))) + +(defthm ToMissives-assoc-equal + ;; if (assoc-equal e L) is not nil then we can link + ;; assoc-equal and ToMissives as follows: + ;; (this lemma is needed to prove the next defthm) + (implies (assoc-equal e L) + (equal (ToMissives (list (assoc-equal e L))) + (list (assoc-equal e (ToMissives L)))))) + +(defthm ToMissives-extract-sublst + ;; now we prove our main lemma + (implies (and (subsetp ids (V-ids L)) + (TrLstp L)) + (equal (ToMissives (extract-sublst L ids)) + (extract-sublst (ToMissives L) ids))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize) + :induct (extract-sublst L ids) + :do-not-induct t + :in-theory (disable ToMissives append)))) + +;; the second lemma we need, allow us to cancel +;; one successive call of extract-sublst + +(defthm member-equal-assoc-equal-not-nil-m-ids + ;; if a is ain the ids of L then (assoc-equal e L) + ;; is not nil + (implies (and (member-equal e (M-ids L)) + (validfields-m L)) + (assoc-equal e L))) + +(defthm member-equal-M-ids-assoc-equal + ;; obviously if e in not in the ids of L + ;; then (assoc-equal e L) is nil + (implies (not (member-equal e (M-ids L))) + (not (assoc-equal e L)))) + +(defthm Missivesp-not-assoc-equal + ;; if M is Missivesp then nil is not a key in L + (implies (ValidFields-M M) + (not (assoc-equal nil M)))) + +(defthm assoc-equal-not-nil + ;; if (assoc-equal e L) is not nil, then + ;; its car is e !! + (implies (assoc-equal e L) + (equal (car (assoc-equal e L)) + e))) + +(defthm assoc-equal-extract-sublst-M-lemma + ;; if e is not in id1 there is no key equal to e + ;; after filtering according to id1 + (implies (and (not (member-equal e id1)) + (ValidFields-M M)) + (not (assoc-equal e (extract-sublst M id1))))) + +(defthm assoc-equal-extract-sublst-M + ;; if e is a key in id1 then e is still a key + ;; after filtering according to id1 + (implies (and (member-equal e id1) + (ValidFields-M M)) + (equal (assoc-equal e (extract-sublst M id1)) + (assoc-equal e M))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :induct (extract-sublst M id1)) + ("Subgoal *1/2" + :cases ((member-equal (car id1) (M-ids M)))))) + +(defthm extract-sublst-cancel-M + ;; and now we can prove our second main lemma + (implies (and (subsetp id2 id1) + (ValidFields-M M)) + (equal (extract-sublst (extract-sublst M id1) id2) + (extract-sublst M id2)))) + +;; Finally, we prove that the correctness of the routes +;; is preserved by extract-sublst + +(defthm extract-sublst-identity + (implies (TrLstp TrLst) + (equal (extract-sublst TrLst (V-ids TrLst)) + TrLst))) + +(defthm assoc-equal-tomissives-not-nil + ;; if e is in the ids of L then there is a key equal to + ;; e in (ToMissives L) + (implies (and (TrLstp L) (member-equal e (V-ids L))) + (assoc-equal e (ToMissives L)))) + +(defthm ToMissives-CorrectRoutesp-Extract-sublst + ;; we prove the current lemma + (implies (and (subsetp ids (V-ids TrLst)) + (TrLstp TrLst) + (CorrectRoutesp TrLst (ToMissives TrLst) NodeSet)) + (CorrectRoutesp (extract-sublst TrLst ids) + (ToMissives (extract-sublst TrLst ids)) + NodeSet))) + +;; NOT IN + +(defun not-in (x y) + (if (or (endp x) (endp y)) + t + (and (not (member (car x) y)) + (not-in (cdr x) y)))) + + +;; SUBSETP +;; we prove some useful lemmas about subsetp +(defthm subsetp-expand + (implies (subsetp x y) + (subsetp x (cons z y)))) + +(defthm subsetp-x-x + (subsetp x x)) + +(defthm subsetp-append + (implies (and (subsetp x S) + (subsetp y S)) + (subsetp (append x y) S))) + +(defthm member-equal-subsetp-last + (implies (and (subsetp x NodeSet) (consp x)) + (member-equal (car (last x)) NodeSet))) + +;; Finally, we prove that converting a list of travels +;; to a list of missives gives something that is recoginized +;; by Missivesp +(defthm checkroutes-caar + (implies (and (checkroutes Routes M NodeSet) + (validfield-route Routes) (consp routes)) + (member-equal (caar routes) NodeSet))) + +(defthm checkroutes-car-last-car + (implies (and (checkroutes Routes M NodeSet) + (validfield-route Routes) (consp routes)) + (member-equal (car (last (car routes))) NodeSet))) + +(defthm Missivesp-ToMissives + (implies (and (correctroutesp TrLst (ToMissives TrLst) NodeSet) + (TrLstp TrLst)) + (Missivesp (ToMissives TrLst) NodeSet))) + diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-nodeset.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-nodeset.lisp new file mode 100644 index 0000000..35698c6 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-nodeset.lisp @@ -0,0 +1,39 @@ +;; Julien Schmaltz +;; Generic Set of Nodes +;; June 17th 2005 +;; File: GeNoC-nodeset.lisp + +(in-package "ACL2") + +(encapsulate ;; GenericNodeSet + ;; abstract set of nodes + ;; the set is generated by the following function + ;; its argument is the parameters + (((NodesetGenerator *) => *) + ;; the following predicate recognizes valid parameters + ((ValidParamsp *) => *) + ;; the following predicate recognizes a valid node + ((NodeSetp *) => *)) + + ;; local witnesses + (local (defun ValidParamsp (x) (declare (ignore x)) t)) + (local (defun NodesetGenerator (x) + (if (zp x) nil + (cons x (NodesetGenerator (1- x)))))) + + (local (defun NodeSetp (l) + (if (endp l) t + (and (natp (car l)) + (NodeSetp (cdr l)))))) + + (defthm nodeset-generates-valid-nodes + (implies (ValidParamsp params) + (NodeSetp (NodesetGenerator params)))) + + ;; we add a generic lemma + (defthm subsets-are-valid + ;; this lemma is used to prove that routes are made of valid nodes + (implies (and (NodeSetp x) + (subsetp y x)) + (NodeSetp y))) +) ;; end GenericNodeSet diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-routing.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-routing.lisp new file mode 100644 index 0000000..799e4f7 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-routing.lisp @@ -0,0 +1,116 @@ +;; Julien Schmaltz +;; Generic Routing Module of GeNoC +;; June 20th 2005 +;; File: GeNoC-routing.lisp + +(in-package "ACL2") + +;; we import the books for the set of nodes and about the data-types +(include-book "GeNoC-nodeset") + +(include-book "GeNoC-misc") ;; import also GeNoC-types + +(encapsulate + ;; Routing computes the route of each message within the network + ;; It takes as arguments: M and NodeSet + ;; It outputs a list of travel TrLst = (... (Id frm Route) ...) + ;; Constraints: + ;; 1/ If the input is a list of valid missives, the output must be + ;; a list of valid travels (Ids are still unique) + ;; 2/ Every route of every travel must be correct + ;; 3/ Frms of the output must be equal to the frms of the input + (((Routing * *) => *)) + + ;; local witnesses + (local (defun route (M) + ;; this would be the routing in a bus + (if (endp M) + nil + (let* ((msv (car M)) + (Id (IdM msv)) + (frm (FrmM msv)) + (origin (OrgM msv)) + (destination (DestM msv))) + (cons (list Id frm (list (list origin destination))) + (route (cdr M))))))) + + (local (defun routing (M NodeSet) + (declare (ignore NodeSet)) + (route M))) + + ;; 1/ If the input is a list of valid missives, the output must be + ;; a list of valid travels (Ids are still unique) + + ;; local lemmas + (local (defthm route-ids + ;; ids of the output TrLst are equal to the ids of + ;; the initital missives + (equal (V-Ids (route M)) (M-Ids M)))) + + (local (defthm validfields-route + (implies (Validfields-M M) + (validfields-TrLst (route M))))) + + (local (defthm TrLstp-route + (implies (and (Validfields-M M) + (No-duplicatesp (M-ids M))) + (TrLstp (route M))))) + + (defthm TrLstp-routing + ;; 1st constraint + ;; the travel list is recognized by TrLst + ;; Params is a free variable + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (TrLstp (routing M NodeSet))))) + + ;; 2/ Routes must satisfy the predicate CorrectRoutesp + (local + (defthm correctroutesp-route + (implies (Missivesp M NodeSet) + (CorrectRoutesp (route M) M NodeSet)))) + + (defthm Routing-CorrectRoutesp + ;; 2nd constraint + ;; The routes produced by routing are correct + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (CorrectRoutesp (Routing M NodeSet) M NodeSet)))) + + ;; some additional constraints + (defthm true-listp-routing + (true-listp (routing M NodeSet)) + :rule-classes :type-prescription) + + (defthm routing-nil + ;; the routing has to return nil if the list of missives is nil + (not (routing nil NodeSet))) + ) ;; end of routing + +(defthm tomissives-routing + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (equal (ToMissives (routing M NodeSet)) M))) + :hints (("GOAL" + :use (:instance correctroutesp-=>-tomissives + (TrLst (Routing M (NodeSetGenerator Params))) + (NodeSet (NodeSetGenerator Params))) + :in-theory (disable Missivesp + correctroutesp-=>-tomissives) + :do-not-induct t))) + +;; A useful theorem. +(defthm ids-routing + ;; the ids of the output of routing are equal to the ids + ;; of the initial list of missives + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (equal (V-ids (routing M NodeSet)) + (M-ids M)))) + :hints (("GOAL" + :use ((:instance ToMissives-Routing)) + :in-theory (disable ToMissives-Routing)))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-scheduling.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-scheduling.lisp new file mode 100644 index 0000000..599feb8 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-scheduling.lisp @@ -0,0 +1,310 @@ +; Julien Schmaltz +;; Generic Scheduling Module of GeNoC +;; Feb 16th 2005 +;; File: GeNoC-scheduling.lisp +;; Rev. Nov. 22nd 2005 +;; JS: NodeSet is not necessary in practice and fundamentally +;; so I remove it from the scheduling definition +(in-package "ACL2") +(include-book "GeNoC-nodeset") +(include-book "GeNoC-misc") ;; imports also GeNoC-types + +;; Inputs: TrLst = ( ... (Id frm route) ...) +;; outputs: Scheduled and Delayed (which are both TrLst) +(encapsulate + ;; Function Scheduling represents the scheduling policy of the + ;; network. + ;; arguments: TrLst att + ;; outputs: Scheduled Delayed newatt + (((scheduling * *) => (mv * * *))) + + (local (defun consume-attempts (att) + ;; function that consumes one attempt for each node + ;; which has still at least one left + (if (zp (SumOfAttempts att)) + att + (let* ((top (car att)) + (node (car top)) + (atti (cadr top))) + (if (zp atti) + (cons top + (consume-attempts (cdr att))) + (cons (list node (1- atti)) + (consume-attempts (cdr att)))))))) + + (local (defun scheduling (TrLst att) + ;; local witness + (mv + ;; scheduled frames + (if (zp (SumOfAttempts att)) + nil ;; no attempt left -> nothing is scheduled + TrLst) ;; otherwise everything is scheduled + ;; delayed frames + (if (zp (SumOfAttempts att)) + TrLst ;; no attempt left -> everything is delayed + nil) ;; otherwise nothing is delayed + (if (zp (SumOfAttempts att)) + att ;; no attempt left -> no modification on att + (consume-attempts att))))) ;; newatt has less attempts than att + + ;; Proof obligations (also named constraints) + ;; ----------------------------------------- + + ;; 1/Type of Scheduled and Delayed travels + ;; --------------------------------------- + ;; The list of scheduled travels is a valid travel list + (defthm trlstp-scheduled + (implies (trlstp TrLst) + (trlstp (mv-nth 0 (scheduling TrLst att))))) + + ;; so is the list of delayed travels + (defthm trlstp-delayed + (implies (trlstp TrLst) + (trlstp (mv-nth 1 (scheduling TrLst att))))) + + ;; 2/ consume at least one attempt to ensure termination. + ;; ------------------------------------------------------ + (defthm consume-at-least-one-attempt + ;; the scheduling policy should consume at least one attempt + ;; this is a sufficient condition to prove that + ;; the full network function terminates + (mv-let (Scheduled Delayed newatt) + (scheduling TrLst att) + (declare (ignore Scheduled Delayed)) + (implies (not (zp (SumOfAttempts att))) + (< (SumOfAttempts newatt) (SumOfAttempts att))))) + + ;; 3/ Correctness of the scheduled travels + ;; ------------------------------------------------------------------ + ;; For any scheduled travel sched-tr, there exists a unique travel + ;; tr in the initial TrLst, such that IdV(sched-tr) = IdV(tr) + ;; and FrmV(sched-tr) = FrmV(tr) and RoutesV(sched-tr) is a + ;; sublist of RoutesV(tr). + ;; In ACL2, the uniqueness of the ids is given by the predicate + ;; TrLstp. + ;; ------------------------------------------------------------------- + + ;; First, let us define this correctness + (defun s/d-travel-correctness (sd-TrLst TrLst/sd-ids) + ;; sd-TrLst is the list of scheduled or delayed travels + ;; TrLst/sd-ids is the filtering of the initial TrLst + ;; according to the ids of the scheduled or delayed travels + (if (endp sd-TrLst) + (if (endp TrLst/sd-ids) + t + nil) + (let* ((sd-tr (car sd-TrLst)) + (tr (car TrLst/sd-ids))) + (and (equal (FrmV sd-tr) (FrmV tr)) + (equal (IdV sd-tr) (IdV tr)) + (subsetp (RoutesV sd-tr) (RoutesV tr)) + (s/d-travel-correctness (cdr sd-TrLst) + (cdr TrLst/sd-ids)))))) + + (defthm scheduled-travels-correctness + (mv-let (Scheduled Delayed newatt) + (scheduling TrLst att) + (declare (ignore Delayed newatt)) + (implies (TrLstp TrLst) + (s/d-travel-correctness + scheduled + (extract-sublst TrLst (V-ids Scheduled)))))) + + (defthm subsetp-scheduled-delayed-ids + ;; this should be provable from the two lemmas above + ;; but it will always be trivial to prove, and it is + ;; useful in subsequent proofs. + (mv-let (scheduled delayed newatt) + (scheduling TrLst att) + (declare (ignore newatt)) + (implies (TrLstp TrLst) + (and (subsetp (v-ids scheduled) (v-ids Trlst)) + (subsetp (v-ids delayed) (v-ids TrLst)))))) + + ;; 4. Correctness of the delayed travels + ;; ------------------------------------- + ;; the correctness of the delayed travels differs from + ;; the correctness of the scheduled travels because, + ;; for the scheduled travels we will generally keep only + ;; one route, but for the delayed travels we will not modify + ;; the travels and keep all the routes. In fact, by + ;; converting a travel back to a missive we will remove the + ;; routes. + ;; --------------------------------------------------------- + + ;; the list Delayed is equal to filtering the initial + ;; TrLst according to the Ids of Delayed + + (defthm delayed-travel-correctness + ;; this is a looping rule !!! should be disabled and used + ;; at the right time + (mv-let (Scheduled Delayed newatt) + (scheduling TrLst att) + (declare (ignore newatt scheduled)) + (implies (TrLstp TrLst) + (equal Delayed + (extract-sublst TrLst (V-ids Delayed))))) + :rule-classes nil) + + + ;; 6/ if the initial AttLst contains only 0, we do not modify it + (defthm mv-nth-2-scheduling-on-zero-attlst + ;; if every attempt has been consumed + ;; the new att is equal to the initial one + (implies (and (zp (SumOfAttempts att)) + (TrLstp trlst)) + (equal + (mv-nth 2 (scheduling TrLst att));; new att + att))) + + (defthm mv-nth-1-scheduling-on-zero-attlst + ;; if every attempt has been consumed + ;; the set of delayed orders is equal to the initial TrLst + (implies (zp (SumOfAttempts att)) + (equal + (mv-nth 1 ;; delayed travels + (scheduling TrLst att)) + TrLst))) + + ;; 7/ The intersection of the ids of the scheduled travels and those + ;; of the delayed travels is empty + ;; ----------------------------------------------------------------- + + (defthm not-in-delayed-scheduled + (mv-let (scheduled delayed newatt) + (scheduling TrLst att) + (declare (ignore newatt)) + (implies (TrLstp TrLst) + (not-in (v-ids delayed) (v-ids scheduled))))) + + ;; some constraints required because we do not have a definition + ;; for scheduling + (defthm consp-scheduling + ;; for the mv-nth + (consp (scheduling TrLst att)) + :rule-classes :type-prescription) + + (defthm true-listp-car-scheduling + (implies (true-listp TrLst) + (true-listp (mv-nth 0 (scheduling TrLst att)))) + :rule-classes :type-prescription) + + (defthm true-listp-mv-nth-1-sched + (implies (TrLstp TrLst) + (true-listp (mv-nth 1 (scheduling TrLst att)))) + :rule-classes :type-prescription) +) ;; end of scheduling + +(defthm checkroutes-member-equal + (implies (and (checkroutes routes m NodeSet) + (member-equal r Routes)) + (validroutep r m))) + +(defthm checkroutes-subsetp-validroute + (implies (and (checkroutes routes m NodeSet) + (consp r) + (subsetp r routes)) + (and (validroutep (car r) m) + (subsetp (car r) NodeSet)))) + +(defthm checkroutes-subsetp + (implies (and (checkroutes routes m NodeSet) + (subsetp routes1 routes)) + (checkroutes routes1 m NodeSet))) + +(defthm correctroutesp-s/d-travel-correctness + (implies (and (CorrectRoutesp TrLst/ids (ToMissives TrLst/ids) NodeSet) + (s/d-travel-correctness TrLst1 TrLst/ids)) + (CorrectRoutesp TrLst1 + (ToMissives TrLst/ids) NodeSet))) + + +(defthm scheduling-preserves-route-correctness + (mv-let (Scheduled Delayed newatt) + (scheduling TrLst att) + (declare (ignore Delayed newatt)) + (implies (and (CorrectRoutesp TrLst (ToMissives TrLst) NodeSet) + (TrLstp TrLst)) + (CorrectRoutesp Scheduled + (ToMissives + (extract-sublst + TrLst + (V-ids scheduled))) + NodeSet))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize) + :do-not-induct t + :in-theory + (disable mv-nth ;; to have my rules used + tomissives-extract-sublst TrLstp)))) + +(defthm scheduling-preserves-route-correctness-delayed + (mv-let (Scheduled Delayed newatt) + (scheduling TrLst att) + (declare (ignore scheduled newatt)) + (implies (and (CorrectRoutesp TrLst (ToMissives TrLst) NodeSet) + (TrLstp TrLst)) + (CorrectRoutesp Delayed + (ToMissives Delayed) + NodeSet))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize) + :do-not-induct t + :use + ((:instance delayed-travel-correctness)) + :in-theory (disable tomissives-extract-sublst TrLstp)))) + +;; the three defthms are similar to the three used to prove +;; missivesp-extract-sublst in GeNoC.lisp ... (proof by analogy) + +(defthm valid-trlstp-assoc-equal + (implies (and (TrLstp L) + (member-equal e (V-ids L))) + (TrLstp (list (assoc-equal e L))))) + +(defthm TrLstp-cons + ;; lemma used in the next defthm + ;; if we cons a valid travel to a filtered valid list + ;; of travel, we obtain a valid list of travel if the + ;; consed travel has an id less than the first of the filter + ;; and this id is not in the filter + (implies (and (trlstp (extract-sublst L ids)) + (trlstp (list (assoc-equal e L))) + (not (member-equal e ids)) + (subsetp ids (V-ids L))) + (trlstp (cons (assoc-equal e L) + (extract-sublst L ids))))) + +(defthm trlstp-extract-sublst + (implies (and (TrLstp TrLst) (subsetp ids (v-ids TrLst)) + (no-duplicatesp ids) (true-listp ids)) + (trlstp (extract-sublst TrLst ids))) + :hints (("GOAL" + :in-theory (disable TrLstp)))) + +(defthm extract-sublst-subsetp-v-ids + (implies (and (subsetp ids (V-ids l)) + (true-listp ids) + (TrLstp l)) + (equal (v-ids (extract-sublst l ids)) + ids))) + +(defthm Missivesp-mv-nth-1-scheduling + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (CorrectRoutesp TrLst (ToMissives TrLst) NodeSet) + (ValidParamsp Params) + (TrLstp TrLst)) + (Missivesp (ToMissives + (mv-nth 1 + (scheduling TrLst att))) + NodeSet))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use ((:instance delayed-travel-correctness) + (:instance trlstp-delayed)) + :in-theory (disable Missivesp trlstp-delayed + TOMISSIVES-EXTRACT-SUBLST + TrLstp mv-nth)))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-types.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-types.lisp new file mode 100644 index 0000000..ad8721e --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC-types.lisp @@ -0,0 +1,315 @@ +;; Julien Schmaltz +;; Definition of the data-types used in GeNoC: +;; Transactions, missives, travels, results and attempts +;; June 20th 2005 +;; File: GeNoC-types.lisp +;; rev. July 14th 2007 +;; js: adding guards + +(in-package "ACL2") + +;; book paths on my laptop +(include-book "data-structures/list-defuns" :dir :system) +(include-book "data-structures/list-defthms" :dir :system) +(include-book "textbook/chap11/qsort" :dir :system) + +;;-------------------------------------------------------------------------- +;; +;; TRANSACTIONS +;; +;;-------------------------------------------------------------------------- +;; A transaction is a tuple t = (id A msg B) +;; Accessors are IdT, OrgT, MsgT and DestT +(defun Idt (trans) (car trans)) +(defun OrgT (trans) (nth 1 trans)) +(defun MsgT (trans) (nth 2 trans)) +(defun DestT (trans) (nth 3 trans)) + +(defun T-ids (Transts) + ;; function that grabs the ids of a list of trans. + (if (endp Transts) + nil + (append (list (caar Transts)) (T-ids (cdr Transts))))) + +(defun T-dests (Trs) + ;; function that grabs the destinatiions of a list of trans. + (if (endp Trs) + nil + (cons (DestT (car trs)) + (T-dests (cdr Trs))))) + +(defun T-msgs (Trs) + ;; function that grabs the messages of a list of trans. + (if (endp Trs) + nil + (cons (MsgT (car trs)) + (T-msgs (cdr Trs))))) + +(defun T-orgs (Trs) + ;; function that grabs the origins of a list of trans + (if (endp Trs) + nil + (cons (OrgT (car trs)) + (T-orgs (cdr Trs))))) + +;; The following predicate checks that each transaction has +;; the right number of arguments +(defun validfield-transactionp (trans) + ;; trans = (id A msg B) + (and (consp trans) + (consp (cdr trans)) ;; (A msg B) + (consp (cddr trans)) ;; (msg B) + (consp (cdddr trans)) ;; (B) + (null (cddddr trans)))) + + +;; The following predicate recognizes a valid list of transactions +(defun Validfields-T (Transts) + (if (endp Transts) + t + (let ((trans (car Transts))) + (and (validfield-transactionp trans) + (natp (Idt trans)) ;; id is a natural + (MsgT trans) ;; msg /= nil + (eqlablep (OrgT trans)) ;; needed to prove guard of Transactionsp + (eqlablep (DestT trans)) + (not (equal (OrgT trans) (DestT trans))) ;; A /= B + (Validfields-T (cdr Transts)))))) + + +;; now we define the predicate that recognizes a valid list of +;; transactions +(defun Transactionsp (Transts NodeSet) + (let ((T-ids (T-ids Transts))) + (and (Validfields-T Transts) + (true-listp Transts) + (subsetp (T-orgs Transts) NodeSet) + (subsetp (T-dests Transts) NodeSet) + (No-Duplicatesp T-ids)))) +;;------------------ end of Transactions ---------------------------------- + +;;-------------------------------------------------------------------------- +;; +;; MISSIVES +;; +;;-------------------------------------------------------------------------- + + +;; A missive is a tuple m = (id A frm B) +;; Accessors are IdM, OrgM, FrmM and DestM +(defun IdM (m) (car m)) +(defun OrgM (m) (nth 1 m)) +(defun FrmM (m) (nth 2 m)) +(defun DestM (m) (nth 3 m)) + +;; We need a function that grabs the ids of a list of missives +(defun M-ids (M) + (if (endp M) + nil + (append (list (caar M)) (M-ids (cdr M))))) + +;; We need a function that grabs the origins of Missives +(defun M-orgs (M) + (if (endp M) + nil + (append (list (OrgM (car M))) (M-orgs (cdr M))))) + +;; The same for the destinations +(defun M-dests (M) + (if (endp M) + nil + (append (list (DestM (car M))) (M-dests (cdr M))))) + +;; We also need a function that grabs the frames of +;; a list of missives +(defun M-frms (M) + ;; grabs the frames of M + (if (endp M) + nil + (let* ((msv (car M)) + (m-frm (FrmM msv))) + (append (list m-frm) (M-frms (cdr M)))))) + + +;; The following predicate checks that each missive has +;; the right number of arguments +(defun validfield-missivep (m) + ;; m = (id A frm B) + (and (consp m) + (consp (cdr m)) ;; (A frm B) + (consp (cddr m)) ;; (frm B) + (consp (cdddr m)) ;; (B) + (null (cddddr m)))) + +;; The following predicate recognizes a valid list of missives (partially) +(defun Validfields-M (M) + (if (endp M) + t + (let ((msv (car M))) + (and (validfield-missivep msv) + (natp (IdM msv)) ;; id is a natural + (FrmM msv) ;; frm /= nil + (not (equal (OrgM msv) (DestM msv))) ;; A /= B + (Validfields-M (cdr M)))))) + +;; now we define the predicate that recognizes a valid list of +;; transactions +(defun Missivesp (M NodeSet) + (let ((M-ids (M-ids M))) + (and (Validfields-M M) + (subsetp (M-orgs M) NodeSet) + (subsetp (M-dests M) NodeSet) + (true-listp M) + (No-Duplicatesp M-ids)))) +;;-------------------- end of Missives ------------------------------------- + +;;-------------------------------------------------------------------------- +;; +;; TRAVELS +;; +;;-------------------------------------------------------------------------- + +;; A travel is a tuple tr = (id frm Routes) +;; Accessors are IdV, FrmV and RoutesV +;; (JS: V comes from the french word for travel, voyage :-) +(defun IdV (tr) (car tr)) +(defun FrmV (tr) (nth 1 tr)) +(defun RoutesV (tr) (nth 2 tr)) + +;; We need a function that grabs the ids of a list of travels +(defun V-ids (TrLst) + (if (endp TrLst) + nil + (append (list (caar TrLst)) (V-ids (cdr TrLst))))) + +;; The following predicate checks that each route of routes +;; has at least two elements +(defun validfield-route (routes) + ;; checks that every route has at least two elements + (if (endp routes) + t + (let ((r (car routes))) + (and (consp r) + (consp (cdr r)) + (validfield-route (cdr routes)))))) + +;; The following predicate checks that each travel has +;; the right number of arguments +(defun validfield-travelp (tr) + ;; tr = (id frm Routes) + (and (consp tr) + (consp (cdr tr)) ;; (frm Routes) + (consp (cddr tr)) ;; (Routes) = ( ((R1) (R2) ...)) + (consp (caddr tr)) ;; ((R1) (R2) ...) + (validfield-route (caddr tr)) + (null (cdddr tr)))) + +;; The following predicate recognizes a valid list of missives (partially) +(defun Validfields-TrLst (TrLst) + (if (endp TrLst) + t + (let ((tr (car TrLst))) + (and (validfield-travelp tr) + (natp (IdV tr)) ;; id is a natural + (FrmV tr) ;; frm /= nil + (true-listp (RoutesV tr)) + (Validfields-TrLst (cdr TrLst)))))) + +;; now we define the predicate that recognizes a valid list of +;; transactions +(defun TrLstp (TrLst ) + (let ((V-ids (V-ids TrLst))) + (and (Validfields-TrLst TrLst) + (true-listp TrLst) + (No-Duplicatesp V-ids)))) + +(defun V-frms (TrLst) + ;; grabs the frames of TrLst + (if (endp TrLst) + nil + (let* ((tr (car Trlst)) + (v-frm (FrmV tr))) + (append (list v-frm) (V-frms (cdr TrLst)))))) +;;-------------------- end of Travels ------------------------------------- + +;;-------------------------------------------------------------------------- +;; +;; RESULTS +;; +;;-------------------------------------------------------------------------- + +;; A result is a tuple rst = (Id Dest Msg) +;; Accessors are IdR, DestR and MsgR +(defun IdR (rst) (car rst)) +(defun DestR (rst) (nth 1 rst)) +(defun MsgR (rst) (nth 2 rst)) + +(defun R-ids (R) + ;; function that grabs the ids of a list of results + (if (endp R) + nil + (append (list (caar R)) (R-ids (cdr R))))) + +(defun R-dests (Results) + ;; function that grabs the destinations of a list of results + (if (endp Results) + nil + (cons (DestR (car Results)) + (R-dests (cdr Results))))) + +(defun R-msgs (Results) + ;; function that grabs the messages of a list of results + (if (endp Results) + nil + (cons (MsgR (car results)) + (R-msgs (cdr Results))))) + + +;; The following predicate checks that each result has +;; the right number of arguments +(defun validfield-resultp (rst) + ;; tr = (Id Dest Msg) + (and (consp rst) + (consp (cdr rst)) ;; (Dest Msg) + (consp (cddr rst)) ;; (Msg) + (null (cdddr rst)))) + +;; The following predicate recognizes a valid list of results (partially) +(defun Validfields-R (R NodeSet) + (if (endp R) + t + (let ((rst (car R))) + (and (validfield-resultp rst) + (natp (IdR rst)) ;; id is a natural + (MsgR rst) ;; msg /= nil + (member (DestR rst) NodeSet) + (Validfields-R (cdr R) NodeSet))))) + +;; now we define the predicate that recognizes a valid list of +;; results +(defun Resultsp (R NodeSet) + (let ((R-ids (R-ids R))) + (and (Validfields-R R NodeSet) + (true-listp R) + (No-Duplicatesp R-ids)))) +;;-------------------- end of Results ------------------------------------- + +;;-------------------------------------------------------------------------- +;; +;; ATTEMPTS +;; +;;-------------------------------------------------------------------------- + +;; we just need to define the sum of the attempts +(defun SumOfAttempts (att) + ;; this is the measure for sigma-t + ;; att has the following form: + ;; ( ... (i RemAtt) ...) + (if (endp att) + 0 + (let* ((top (car att)) + (rem-att (cadr top))) + (+ (nfix rem-att) + (SumOfAttempts (cdr att)))))) + +;;-------------------- end of Attempts ------------------------------------- diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC.lisp new file mode 100644 index 0000000..37072b9 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/GeNoC.lisp @@ -0,0 +1,787 @@ +;; Julien Schmaltz +;; Generic Routing Module of GeNoC +;; June 20th 2005 +;; File: GeNoC-routing.lisp + +(in-package "ACL2") + +;; we import the previous books +(include-book "GeNoC-scheduling") ;; imports GeNoC-misc and GeNoC-nodeset +(include-book "GeNoC-routing") + +(in-theory (disable mv-nth)) + +;;------------------------------------------------------------------------ +;; +;; GeNoC_t +;; +;;------------------------------------------------------------------------ + +;; Tail definition of GeNoC_t +;; -------------------------- +(defun GeNoC_t (M NodeSet att TrLst) + ;; The composition of Routing and Scheduling is built by function GeNoC_t. + ;; It takes as arguments: + ;; - a list of missives, M + ;; - the set of existing nodes, NodeSet + ;; - the list of attempts, att + ;; - an accumulator of travels, TrLst + ;; + ;; we set the measure to be SumOfAttempts(att) + (declare (xargs :measure (SumOfAttempts att))) + (if (zp (SumOfAttempts att)) + ;; if every attempt has been consumed, we return the accumulator + ;; TrLst and the remaining missives M + (mv TrLst M) + ;; else, + (let ((V (Routing M NodeSet))) + ;; we compute the routes. This produces the travel list V. + (mv-let (Scheduled Delayed newAtt) + ;; we call function scheduling + (Scheduling V att) + ;; we enter the recursive call and accumulate the + ;; scheduled travels + (GeNoC_t (ToMissives Delayed) NodeSet newAtt + (append Scheduled TrLst)))))) + + +;; Correctness of GeNoC_t +;; ---------------------- +(defun CorrectRoutes-GeNoC_t (routes m-dest) + ;; GeNoC_t is correct if every element ctr of the output list + ;; is such that (a) FrmV(ctr) = FrmM(m) and (b) forall r in + ;; RoutesV(ctr) Last(r) = DestM(m). For the m such that + ;; IdM(m) = IdV(ctr). + ;; This function checks that (b) holds. + (if (endp routes) + t + (let ((r (car routes))) + (and (equal (car (last r)) m-dest) + (CorrectRoutes-GeNoC_t (cdr routes) m-dest))))) + +(defun GeNoC_t-correctness1 (TrLst M/TrLst) + ;; we complement the correctness of GeNoC_t + (if (endp TrLst) + (if (endp M/TrLst) + t + nil) + (let* ((tr (car TrLst)) + (v-frm (FrmV tr)) + (routes (RoutesV tr)) + (m (car M/TrLst)) + (m-frm (FrmM m)) + (m-dest (DestM m))) + (and (equal v-frm m-frm) + (CorrectRoutes-GeNoC_t routes m-dest) + (GeNoC_t-correctness1 (cdr TrLst) + (cdr M/TrLst)))))) + +(defun GeNoC_t-correctness (TrLst M) + ;; before checking correctness we filter M + ;; according to the ids of TrLst + (let ((M/TrLst (extract-sublst M (V-ids TrLst)))) + (GeNoC_t-correctness1 TrLst M/TrLst))) + + +;; Non tail definition of GeNoC_t +;; ------------------------------ +(defun GeNoC_t-non-tail-Comp (M NodeSet att) + ;; we define a non tail function that computes the + ;; first output of GeNoC_t, i.e the completed transactions + (declare (xargs :measure (SumOfAttempts att))) + (if (zp (SumOfAttempts att)) + ;; if every attempt has been consumed, we return the accumulator + ;; TrLst and the remaining missives M + nil + ;; else, + (let ((V (Routing M NodeSet))) + ;; we compute the routes. This produces the travel list V. + (mv-let (Scheduled Delayed newAtt) + ;; we call function scheduling + (Scheduling V att) + ;; we enter the recursive call and accumulate the + ;; scheduled travels + (append (GeNoC_t-non-tail-Comp (ToMissives Delayed) + NodeSet newAtt) + Scheduled))))) + +;; we now prove that this function is right + +(defthm true-listp-GeNoC_t-non-tail-comp + (true-listp (GeNoC_t-non-tail-Comp M NodeSet att)) + :rule-classes :type-prescription) + +(defthm GeNoC_t-non-tail-=-tail-comp + (implies (true-listp TrLst) + (equal (car (GeNoC_t M NodeSet att TrLst)) + (append (GeNoC_t-non-tail-Comp M NodeSet Att) + TrLst)))) + +;; Proof of GeNoC_t correctness +;; ---------------------------- + +;; first we add a lemma that tells ACL2 that +;; converting the travels that are routed and delayed +;; produced a valid list of missives +(defthm missivesp-mv-nth1-scheduling-routing + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (Missivesp + (ToMissives (mv-nth 1 + (scheduling (routing M NodeSet) + att))) + NodeSet))) + :hints (("GOAL" + :in-theory (disable + TrLstp Missivesp)))) + + + +;; the recursive call of genoc_t-non-tail-comp calls append +;; we put the append at the top. +;; to do so we add the two rules below: + +(defthm v-ids-append + ;; the ids of an append is the append of the ids + (equal (v-ids (append a b)) + (append (v-ids a) (v-ids b)))) + +(defthm extract-sublst-append + ;; filtering according to an append is the append + ;; of the filtering. + (equal (extract-sublst M (append id1 id2)) + (append (extract-sublst M id1) + (extract-sublst M id2)))) + + +;; then to split the proof is two cases, we replace the +;; append by a conjunction. +;; the rule below allows this decomposition: + +(defthm correctroutess1-append + (implies (and (equal (len a) (len c)) + (equal (len b) (len d))) + (equal (genoc_t-correctness1 (append a b) + (append c d)) + (and (Genoc_T-Correctness1 a c) + (Genoc_T-Correctness1 b d))))) + +;; To have this lemma used we need to prove some +;; additional properties between len and extract-sublst +;; and len and v-ids (e.g. a is a call to v-ids) + +(defthm len-extract-sublst + (equal (len (extract-sublst L ids)) + (len ids))) + +(defthm len-v-ids + (equal (len (v-ids x)) + (len x))) + +;; now we need to prove some lemmas so that previous rules +;; (from GeNoC-misc) about extract-sublst, tomissives, etc could +;; fire. + +(defthm subsetp-trans + ;; transitivity of subsetp + (implies (and (subsetp x y) + (subsetp y z)) + (subsetp x z))) + +(defthm v-ids-GeNoC_t-non-tail-comp + ;; the ids of the output of genoc_t-non-tail-comp is a + ;; subset of those of M + ;; for this theorem the rule ids-routing is useful + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (let ((Gnt (Genoc_T-Non-Tail-Comp M NodeSet att))) + (subsetp (V-ids Gnt) (M-ids M))))) + :hints (("GOAL" + :in-theory + (disable missivesp TrLstp)) + ("Subgoal *1/3" + :use + ((:instance subsetp-scheduled-delayed-ids + (TrLst (Routing M (NodeSetGenerator Params))))) + :in-theory + (disable subsetp-scheduled-delayed-ids Missivesp TrLstp)))) + +(defthm not-in-no-duplicatesp-equal-append + ;; if x is not in y and both do not have duplicates then + ;; their append has no duplicate too + (implies (and (no-duplicatesp-equal x) + (not-in x y) + (no-duplicatesp-equal y)) + (no-duplicatesp-equal (append x y)))) + +(defthm subsetp-not-in + ;; if a list y and no element in common with z + ;; then any sublist x of y has no element in z + (implies (and (not-in delayed scheduled) + (subsetp x delayed)) + (not-in x scheduled))) + +(defthm not-in-v-ids-genoc_t-non-tail-comp + ;; if the ids of a list have no common element with + ;; another ids then the output of genoc_t-non-tail-comp does + ;; not introduce any new id + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (not-in (m-ids delayed) Sched-ids) + (Missivesp delayed NodeSet) + (ValidParamsp Params)) + (not-in (v-ids (genoc_t-non-tail-comp delayed NodeSet att)) + Sched-ids))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :in-theory (disable missivesp)))) + +(defthm fwd-trlstp + ;; because we disable trlstp, this rule adds its content + ;; as hypotheses + (implies (TrLstp TrLst) + (and (validfields-trlst trlst) + (true-listp trlst) + (no-duplicatesp-equal (v-ids trlst)))) + :rule-classes :forward-chaining) + +(defthm v-ids-GeNoC_t-non-tail-comp-no-dup + ;; the ids of the output of genoc_t-non-tail-comp have no dup + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (let ((Gnt (Genoc_T-Non-Tail-Comp M NodeSet att))) + (no-duplicatesp-equal (V-ids Gnt))))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize) + :do-not-induct t + :induct (genoc_t-non-tail-comp M (nodeSetGenerator Params) att) + :in-theory (disable missivesp TrLstp)) + ("Subgoal *1/2" + :use + ((:instance + not-in-v-ids-genoc_t-non-tail-comp + (delayed (tomissives + (mv-nth 1 (scheduling + (routing M (nodeSetGenerator Params)) + att)))) + (att (mv-nth 2 (scheduling + (routing M (nodeSetGenerator Params)) + att))) + (Sched-ids (v-ids (mv-nth 0 (scheduling + (routing M (nodeSetGenerator Params)) + att))))) + (:instance trlstp-scheduled + (TrLst (routing M (Nodesetgenerator Params))))) + :in-theory + (disable trlstp-scheduled mv-nth trlstp + not-in-v-ids-genoc_t-non-tail-comp Missivesp)))) + +(defthm extract-sublst-subsetp-m-ids + ;; filtering a list l according to a subset ids of its identifiers + ;; produces a list the ident. of which are ids + (implies (and (subsetp ids (M-ids l)) + (true-listp ids) + (Validfields-M l)) + (equal (M-ids (extract-sublst l ids)) + ids))) + +(defthm ToMissives-Delayed/Rtg + ;; we prove that the conversion of the delayed travels + ;; into a list of missives is equal to the filtering + ;; of the initial list of missives M according to the ids + ;; of the delayed travels. + (let ((NodeSet (NodeSetGenerator Params))) + (mv-let (Scheduled/Rtg Delayed/Rtg newAtt) + (scheduling (Routing M NodeSet) att) + (declare (ignore Scheduled/Rtg newAtt)) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (equal (ToMissives Delayed/Rtg) + (extract-sublst M (V-ids Delayed/Rtg)))))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :do-not '(eliminate-destructors generalize fertilize) + :use ((:instance ToMissives-extract-sublst + (L (Routing M (NodeSetGenerator Params))) + (ids + (V-ids (mv-nth 1 + (scheduling + (Routing M (NodeSetGenerator Params)) + att))))) + (:instance delayed-travel-correctness + (TrLst (Routing M (NodeSetGenerator Params)))) + (:instance subsetp-scheduled-delayed-ids + (TrLst (Routing M (NodeSetGenerator Params))))) + :in-theory (disable TrLstp Missivesp + ToMissives-extract-sublst + subsetp-scheduled-delayed-ids)))) + +(defthm valid-missive-assoc-equal + ;; a list of a member of a valid list of missives + ;; is a valid list of missives + (implies (and (Missivesp M NodeSet) + (member-equal e (M-ids M))) + (Missivesp (list (assoc-equal e M)) NodeSet))) + +(defthm missivesp-cons + ;; lemma used in the next defthm + ;; if we cons a valid missive to a filtered valid list + ;; of missives, we obtain a valid list of missives if the + ;; the id of the consed missive is not in the filter + (implies (and (missivesp (extract-sublst M ids) nodeset) + (missivesp (list (assoc-equal e M)) nodeset) + (not (member-equal e ids)) + (subsetp ids (M-ids M))) + (missivesp (cons (assoc-equal e M) + (extract-sublst M ids)) + nodeset))) + + +(defthm missivesp-extract-sublst + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (missivesp M NodeSet) + (ValidParamsp Params) + (true-listp ids) + (no-duplicatesp-equal ids) + (subsetp ids (M-ids M))) + (Missivesp (extract-sublst M ids) NodeSet))) + :hints (("GOAL" + :in-theory (disable missivesp)) + ("Subgoal *1/1" + :in-theory (enable missivesp)))) + + +(defthm fwd-missivesp + ;; as missivesp is disabled we prove this rule to add + ;; the content of missivesp as hypotheses + (implies (missivesp M NodeSet) + (and (Validfields-M M) + (subsetp (M-orgs M) NodeSet) + (subsetp (M-dests M) NodeSet) + (True-listp M) + (No-duplicatesp (M-ids M)))) + :rule-classes :forward-chaining) + + +(defthm v-ids_G_nt_sigma_subsetp-v-ids-delayed/rtg + ;; this lemma is used in the subsequent proofs + ;; it makes a fact "explicit" + (let ((NodeSet (NodeSetGenerator Params))) + (mv-let (scheduled/rtg delayed/rtg newAtt) + (scheduling (routing M NodeSet) att) + (declare (ignore scheduled/rtg)) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (subsetp + (V-ids + (genoc_t-non-tail-comp + (extract-sublst M (v-ids delayed/rtg)) + NodeSet newAtt)) + (V-ids delayed/rtg))))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use + ((:instance subsetp-scheduled-delayed-ids + (TrLst (Routing M (NodeSetGenerator Params)))) + (:instance trlstp-delayed + (TrLst (routing M (NodeSetGenerator Params)))) + ;; the following is required because in the conclusion of the + ;; rule there is no call to extract-sublst + (:instance v-ids-GeNoC_t-non-tail-comp + (M (extract-sublst + M + (V-ids (mv-nth 1 (scheduling + (routing M (NodeSetGenerator Params)) + att))))) + (att (mv-nth 2 (scheduling + (routing M (NodeSetGenerator Params)) + att))))) + :in-theory (disable subsetp-scheduled-delayed-ids + trlstp-delayed + v-ids-GeNoC_t-non-tail-comp + trlstp missivesp)))) + + +;; Scheduled/Rtg does not modify frames +;; --------------------------------------- + +(defthm s/d-travel-v-frms + (implies (and (TrLstp sd-trlst) + (s/d-travel-correctness sd-trlst TrLst/sd-ids)) + (equal (V-frms sd-trlst) (V-frms TrLst/sd-ids)))) + +(defthm m-frms-to-v-frms + ;; this rule is only used to rewrite the next theorem to + ;; the previous one. + (equal (m-frms (toMissives x)) + (v-frms x))) + +(defthm Scheduled-v-frms-m-frms + ;; we prove that the frames of the scheduled travels + ;; are equal to the frames of the conversion of the initial list of travels + ;; filtered according to the ids of the scheduled travels + (mv-let (Scheduled Delayed newAtt) + (scheduling TrLst att) + (declare (ignore Delayed newAtt)) + (implies (and (TrLstp TrLst) + (ValidParamsp Params)) + (equal + (V-frms scheduled) + (M-frms + (ToMissives (extract-sublst TrLst + (v-ids scheduled))))))) + :hints (("GOAL" + :use ((:instance s/d-travel-v-frms + (sd-trlst + (mv-nth 0 (scheduling TrLst att))) + (TrLst/sd-ids + (extract-sublst + TrLst + (v-ids + (mv-nth 0 (scheduling TrLst att)))))) + (:instance scheduled-travels-correctness)) + :in-theory (disable TrLstp s/d-travel-v-frms mv-nth)))) + +(in-theory (disable m-frms-to-v-frms)) + +(defthm Scheduled/Rtg_not_modify_frames + ;; we prove the the frames of the scheduled travels produced + ;; by scheduling and routing are equal to the frames + ;; of the initial list of missives + (let ((NodeSet (NodeSetGenerator Params))) + (mv-let (Scheduled/Rtg Delayed/Rtg newAtt) + (scheduling (routing M NodeSet) att) + (declare (ignore Delayed/Rtg newAtt)) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (equal (V-frms Scheduled/Rtg) + (M-frms + (extract-sublst + M (v-ids Scheduled/Rtg))))))) + :hints (("GOAL" + :do-not-induct t + :do-not '(eliminate-destructors generalize fertilize) + :use ((:instance Scheduled-v-frms-m-frms + (TrLst (routing M (NodeSetGenerator Params)))) + (:instance subsetp-scheduled-delayed-ids + (TrLst (routing M (NodeSetGenerator Params))))) + :in-theory (disable TrLstp Missivesp + subsetp-scheduled-delayed-ids + scheduled-v-frms-m-frms)))) + +(defthm correctroutesp-vm-frms-gc1 + ;; the correctness of routes and equality of frames imply + ;; the main predicate (correctness of genoc_t-non-tail-comp) + (implies (and (correctroutesp L (extract-sublst M (v-ids L)) + NodeSet) + (equal (V-frms L) + (m-frms (extract-sublst M (v-ids L))))) + (Genoc_T-Correctness1 L + (extract-sublst m (v-ids L))))) + +(defthm GC1_scheduled/Rtg + ;; we prove the correctness of the scheduled travels + (let ((NodeSet (NodeSetGenerator Params))) + (implies (And (missivesp M NodeSet) + (ValidParamsp Params)) + (mv-let (scheduled/rtg delayed/rtg newAtt) + (scheduling (routing M NodeSet) att) + (declare (ignore delayed/rtg newAtt)) + (genoc_t-correctness1 + scheduled/rtg + (extract-sublst M (v-ids scheduled/rtg)))))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :do-not '(eliminate-destructors generalize fertilize) + :use + ((:instance Scheduled/Rtg_not_modify_frames) + (:instance subsetp-scheduled-delayed-ids + (TrLst (Routing M (NodeSetGenerator Params)))) + (:instance + scheduling-preserves-route-correctness + (NodeSet (NodeSetGenerator Params)) + (TrLst (routing M (NodeSetGenerator Params)))) + (:instance correctroutesp-vm-frms-gc1 + (NodeSet (NodeSetGenerator Params)) + (L (mv-nth 0 (scheduling + (routing m (NodeSetGenerator Params)) + att))))) + :in-theory (disable TrLstp Missivesp + Correctroutesp-Vm-Frms-Gc1 + subsetp-scheduled-delayed-ids + Scheduling-Preserves-Route-Correctness + Scheduled/Rtg_not_modify_frames)))) + +(defthm GeNoC_t-thm + ;; now we can prove the correctness of GeNoC_t + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (mv-let (Cplt Abt) + (GeNoC_t M NodeSet att nil) + (declare (ignore Abt)) + (GeNoC_t-correctness Cplt M)))) + :otf-flg t + :hints (("GOAL" + :induct (GeNoC_t-non-tail-comp M (NodeSetGenerator Params) Att) + :do-not '(eliminate-destructors generalize) + :in-theory (disable TrLstp Missivesp) + :do-not-induct t) + ("Subgoal *1/2" + :use + ((:instance trlstp-delayed + (TrLst (routing M (NodeSetGenerator Params)))) + (:instance subsetp-scheduled-delayed-ids + (TrLst (Routing M (NodeSetGenerator Params)))) + (:instance GC1_scheduled/Rtg)) + :in-theory (e/d (mv-nth) + (TrLstp missivesp trlstp-delayed + subsetp-scheduled-delayed-ids + GC1_scheduled/Rtg))))) + +;;------------------------------------------------------------ +;; Definition and Validation of GeNoC +;;------------------------------------------------------------ + +;; we load the generic definitions of the interfaces +(include-book "GeNoC-interfaces") + +;; ComputeMissives +;; -------------- +(defun ComputeMissives (Transactions) + ;; apply the function p2psend to build a list of missives + ;; from a list of transactions + (if (endp Transactions) + nil + (let* ((trans (car Transactions)) + (id (IdT trans)) + (org (OrgT trans)) + (msg (MsgT trans)) + (dest (DestT trans))) + (cons (list id org (p2psend msg) dest) + (ComputeMissives (cdr Transactions)))))) + +;; ComputeResults +;; ------------- +(defun ComputeResults (TrLst) + ;; apply the function p2precv to build a list of results + ;; from a list of travels + (if (endp TrLst) + nil + (let* ((tr (car TrLst)) + (id (IdV tr)) + (r (car (routesV tr))) + (dest (car (last r))) + (frm (FrmV tr))) + (cons (list id dest (p2precv frm)) + (ComputeResults (cdr TrLst)))))) + +;; GeNoC +;; ----- +(defun GeNoC (Trs NodeSet att) + ;; main function + (mv-let (Responses Aborted) + (GeNoC_t (ComputeMissives Trs) NodeSet att nil) + (mv (ComputeResults Responses) Aborted))) + +;; GeNoC Correctness +;; ----------------- +(defun genoc-correctness (Results Trs/ids) + ;; Trs/ids is the initial list of transactions filtered according + ;; to the ids of the list of results. + ;; We check that the messages and the destinations of these two lists + ;; are equal. + (and (equal (R-msgs Results) + (T-msgs Trs/ids)) + (equal (R-dests Results) + (T-dests Trs/ids)))) + +(defthm M-ids-computesmissives + ;; lemma for the next defthm + (equal (M-ids (computemissives Trs)) + (T-ids trs))) + +(defthm missivesp-computemissives + (implies (transactionsp trs NodeSet) + (missivesp (ComputeMissives trs) NodeSet))) + + +(defun all-frms-equal-to-p2psend (TrLst Trs) + ;; check that every frame of TrLst is equal to the application + ;; of p2psend to the corresponding message in the list of + ;; transactions Trs + (if (endp TrLst) + (if (endp Trs) + t + nil) + (let* ((tr (car TrLst)) + (trans (car Trs)) + (tr-frm (FrmV tr)) + (t-msg (MsgT trans))) + (and (equal tr-frm (p2psend t-msg)) + (all-frms-equal-to-p2psend (cdr TrLst) (cdr Trs)))))) + +(defthm GC1-=>-all-frms-equal-to-p2psend + (implies (GeNoC_t-correctness1 TrLst (ComputeMissives Trs)) + (all-frms-equal-to-p2psend TrLst Trs))) + +(defthm all-frms-equal-r-msgs-t-msgs + ;; if frames have been computed by p2psend then + ;; computeresults applies p2precv. We get thus the initial msg. + (implies (and (all-frms-equal-to-p2psend TrLst Trs) + (validfields-trlst TrLst)) + (equal (R-msgs (ComputeResults TrLst)) + (T-msgs Trs)))) + +(defthm R-ids-computeresults + (equal (R-ids (computeresults x)) + (V-ids x))) + +(defthm m-dests-computemissives + (equal (M-dests (computeMissives trs)) + (T-dests trs))) + + +(defthm GC1-r-dest-m-dests + (implies (and (GeNoC_t-correctness1 TrLst M/TrLst) + (validfields-trlst TrLst) + (Missivesp M/TrLst NodeSet)) + (equal (R-dests (ComputeResults TrLst)) + (M-dests M/TrLst)))) + +(defthm validfields-append + ;; lemma for the next defthm + (implies (and (validfields-trlst l1) + (validfields-trlst l2)) + (validfields-trlst (append l1 l2)))) + + +(defthm validfields-trlst-GeNoC_nt + ;; to use the lemma all-frms-equal-to-p2psend we need to establish + ;; that GeNoC_nt contains travels with validfields + ;; and that it contains no duplicated ids + (let ((NodeSet (NodeSetGenerator Params))) + (implies (and (Missivesp M NodeSet) + (ValidParamsp Params)) + (validfields-trlst (genoc_t-non-tail-comp M NodeSet att)))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :induct (Genoc_T-Non-Tail-Comp M (NodeSetGenerator Params) att)) + ("Subgoal *1/2" + :use ((:instance trlstp-delayed + (TrLst (Routing M (NodeSetGenerator Params)))) + (:instance trlstp-scheduled + (TrLst (Routing M (NodeSetGenerator Params)))) + (:instance Missivesp-mv-nth-1-scheduling + (TrLst (routing M (NodeSetGenerator Params))))) + :in-theory (disable trlstp-delayed trlstp-scheduled + Missivesp-mv-nth-1-scheduling)))) + +;; the next four lemmas are similar to those used to prove +;; the lemma tomissives-extract-sublst .... (proof by analogy) + +(defthm computemissives-append + (equal (computemissives (append a b)) + (append (computemissives a) (computemissives b)))) + +(defthm member-equal-assoc-equal-not-nil-t-ids + ;; if e is an Id of a travel of L + ;; then (assoc-equal e L) is not nil + (implies (and (member-equal e (T-ids Trs)) + (Validfields-T Trs)) + (assoc-equal e Trs))) + +(defthm computemissives-assoc-equal + ;; if (assoc-equal e L) is not nil then we can link + ;; assoc-equal and computemissives as follows: + ;; (this lemma is needed to prove the next defthm) + (implies (assoc-equal e L) + (equal (computemissives (list (assoc-equal e L))) + (list (assoc-equal e (computemissives L)))))) + +(defthm computemissives-extract-sublst + ;; calls of computemissives are moved into calls + ;; of extract-sublst + (implies (and (subsetp ids (t-ids trs)) + (validfields-t trs)) + (equal (ComputeMissives (extract-sublst trs ids)) + (extract-sublst (ComputeMissives trs) ids))) + :otf-flg t + :hints (("GOAL" + :induct (extract-sublst Trs ids) + :do-not-induct t + :in-theory (disable computemissives append)))) + + +(defthm m-dest-t-dests-extract-sublst + (implies (and (subsetp ids (t-ids trs)) + (validfields-t trs)) + (equal (m-dests (extract-sublst (computemissives Trs) ids)) + (t-dests (extract-sublst trs ids)))) + :hints (("GOAL" + :do-not-induct t + :use (:instance m-dests-computemissives + (Trs (extract-sublst Trs ids))) + :in-theory (disable m-dests-computemissives)))) + +(defthm fwd-chaining-transactionsp + (implies (Transactionsp Trs NodeSet) + (and (validfields-t Trs) + (true-listp trs) + (subsetp (t-orgs trs) nodeset) + (subsetp (t-dests trs) nodeset) + (no-duplicatesp-equal (t-ids trs)))) + :rule-classes :forward-chaining) + +(defthm GeNoC-is-correct + (let ((NodeSet (NodeSetGenerator Params))) + (mv-let (results aborted) + (GeNoC Trs NodeSet att) + (declare (ignore aborted)) + (implies (and (Transactionsp Trs NodeSet) + (equal NodeSet (NodeSetGenerator Params)) + (ValidParamsp Params)) + (GeNoC-correctness + results + (extract-sublst Trs (R-ids results)))))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use ((:instance GeNoC_t-thm + (M (ComputeMissives Trs))) + (:instance v-ids-GeNoC_t-non-tail-comp + (M (computemissives trs))) + (:instance all-frms-equal-r-msgs-t-msgs + (TrLst (genoc_t-non-tail-comp + (computeMissives trs) + (Nodesetgenerator params) att)) + (Trs (extract-sublst Trs + (v-ids + (genoc_t-non-tail-comp + (computeMissives trs) + (nodesetgenerator params) + att))))) + (:instance GC1-r-dest-m-dests + (TrLst (genoc_t-non-tail-comp + (computeMissives trs) + (nodesetgenerator params) att)) + (M/TrLst + (extract-sublst (ComputeMissives Trs) + (V-ids (genoc_t-non-tail-comp + (computeMissives trs) + (nodesetgenerator params) + att)))) + (NodeSet (Nodesetgenerator params)))) + :in-theory (e/d (mv-nth) + (GeNoC_t-thm missivesp trlstp + all-frms-equal-r-msgs-t-msgs + v-ids-GeNoC_t-non-tail-comp + transactionsp GC1-r-dest-m-dests))))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/readme b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/readme new file mode 100755 index 0000000..60c7232 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/readme @@ -0,0 +1,80 @@ +***************************************************************************** +* * +* * +* GeNoC ACL2 scripts * +* * +* Julien Schmaltz * +* * +* TIMA-VDS * +* * +* 29/01/06 * +***************************************************************************** + + +1 Structure of the books for GeNoC +----------------------------------- + +1.1 GeNoC-types +-------------- + + This book defines the data types used in GeNoC: transactions, +missives, travels, etc. It contains basic functions used to manipulate +these datatypes. + It does not import any book. + +1.2 GeNoC-misc +-------------- + + This book imports GeNoC-types. + This book contains miscellaneous definitions. For instance, it +defines predicates like CorrectRoutep, the filtering operator extrac-sublst, +some lemmas about subsetp, etc. + +1.3 GeNoC-nodeset +----------------- + + This book contains functions about the definition and the validation +of the set of the existing nodes of a particular network. + It does not import any book. + +1.4 GeNoC-routing +----------------- + + This book imports GeNoC-nodeset and GeNoC-misc. + It contains functions about the definition and the validation +of the routing algorithm. + +1.5 GeNoC-scheduling +-------------------- + + This book imports GeNoC-misc and GeNoC-nodeset. + It contains functions about the scheduling policy of GeNoC. It +also adds some lemmas used in the final proof. These lemmas link +functions like extract-sublst, missivesp, etc. They are about NodeSet +and this is why we need the corresponding book. + +1.7 GeNoC-interfaces +-------------------- + + This book contains functions about the definition and the validation +of the interfaces. + It does not import any book. + +1.7 GeNoC +--------- + This book imports the previous books. It contains the definition +of GeNoC and its proof of correctness. + +1.8 Global Structure +-------------------- + + The global "book tree" is the following: + + GeNoC + / | \ + GeNoC-scheduling GeNoC-routing GeNoC-interfaces + | | | | + GeNoC-nodeset GeNoC-misc GeNoC-nodeset + | + GeNoC-types + diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/interfaces/bi-phi-m.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/interfaces/bi-phi-m.lisp new file mode 100644 index 0000000..673ef95 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/interfaces/bi-phi-m.lisp @@ -0,0 +1,310 @@ +;; Julien Schmaltz +;; definition of the send side of the biphase mark protocol +;; definition taken from Moore's paper + + +(in-package "ACL2") + + +(defun listn (n x) + ;; makes a list of n copies of x + (if (zp n) + nil + (cons x (listn (1- n) x)))) + + +;; Sending +;; ------- + +;; Moore wrote: +;; "A cell encodes one bit, b, of the message, but the encoding depends +;; upon the signal, x, output immediately before the cell. +;; Let csig be x if b is t and not(x) otherwise. +;; Then a cell is defined as the concatenation of a "mark" subcell containing n +;; repetitions of not(x), followed by a "code" subcell containing k repetitions +;; of csig." + +(defun csig (x b) + (if b x (not x))) + +(defun cell (x n k bit) + ;; encodes bit in a cell of size n+k + (append (listn n (not x)) + (listn k (csig x bit)))) + +;; "To encode a bit vector, msg, with cell size n+k, assuming +;; that the previously otput signal is x we merely concatenate +;; successive cells, being careful to pass the correct value +;; for the "previous signal"." +(defun cells (x n k msg) + (if (endp msg) + nil + (append (cell x n k (car msg)) + (cells (csig x (car msg)) n k (cdr msg))))) + +;; "We adopt the convention that the sender holds the line high +;; before and after the message is sent. Thus, on either side +;; of the encoded cells we include "pads" of t, of arbitrary +;; lengths p1 and p2. +;(defun send (msg p1 n k p2) +; (append (listn p1 t) +; (append (cells t n k msg) (listn p2 t)))) + +(defun send (msg p1 n k flg) + ;; I consider a more general function, that takes the initial + ;; signal as a parameter + (append (listn p1 flg) + (cells flg n k msg))) + + +;; Receiving +;; --------- + +;; "Scan takes a signal x, and a list of signals, lst, and +;; scans lst until it finds the first signal different from x. +;; If lst happens to begin with a string of xs, scan finds the +;; first edge." +(defun scan (x lst) + (if (endp lst) + nil + (if (xor x (car lst)) + lst + (scan x (cdr lst))))) + +;; "Recv-bit is the function that recovers the bit encoded in a +;; cell. It takes two arguments. The first is the 0-based sampling +;; distance, j, at which it is supposed to sample [...]. +;; The second argument is the list of signals, starting with the +;; first signal in the mark subcell of the cell." +(defun recv-bit (k lst) + ;; "The bit received is t if the first signal of the mark is + ;; different from the signal sampled in the code subcell; + ;; otherwise the bit received is f." + (if (xor (car lst) (nth k lst)) + t + nil)) + +;; The receive function receives i bits. +;; "The list of signals on which recv operates should be thought +;; of as starting with the signal, x, sampled in the code subcell +;; of previous cell. If i is 0, the empty message is recovered. +;; Otherwise, recv scans to the next edge (i.e., it scans past the +;; initial xs to get past the code subcell of the previous cell +;; and to the mark of the next cell). Recv then used recv-bit +;; to recover the bit in that cell and conses it to the result +;; of recursively recovering i - 1 more bits." + +(defun recv (i x k lst) + (if (zp i) + nil + (cons (recv-bit k (scan x lst)) + (recv (1- i) (nth k (scan x lst)) + k (nthcdr k (scan x lst)))))) +;; Correctness +;; ----------- + +(defun bvp (x) + (if (endp x) + t + (and (booleanp (car x)) + (bvp (cdr x))))) + + +;; I remove the end of the line .... does not seem to be necessary + +;; I load books on lists +(include-book "data-structures/list-defuns" :dir :system) +(include-book "data-structures/list-defthms" :dir :system) + +;; I load the book for arithmetic +(include-book "arithmetic-3/bind-free/top" :dir :system) + +;; we want to prove that the composition of send and recv +;; is an identity. + +(defthm car-cells + ;; if the size of the cells is properly set up and + ;; if there is at least one bit in the message + ;; the first bit of the cell is the opposite of the previous + ;; signal on the line. + (implies (and (booleanp flg) (integerp n) (integerp k) + (< 0 n) (< 0 k) (consp msg)) + (xor flg (car (cells flg n k msg))))) + +(defthm scan-cells-cancel + ;; if scan works properly then if applied to a list of cells + ;; it returns this list of cells + (implies (and (booleanp flg) (integerp n) (integerp k) + (< 0 n) (< 0 k) (consp msg)) + (equal (scan flg (cells flg n k msg)) + (cells flg n k msg)))) + +;; using this rule we could prove theorems on cells only + +(defthm true-listp-cells + ;; cells returns a true-listp + (true-listp (cells flg n k msg)) + :rule-classes :type-prescription) + +(defthm bvp-cells + ;; if flg is a Boolean and lst a list of Booleans, then + ;; cells is still a list of Booleans. + (implies (and (bvp msg) (booleanp flg)) + (bvp (cells flg n k msg)))) + +(defthm consp-cells + (implies (and (consp msg) (integerp n) (integerp k) + (< 0 n) (<= 0 k)) + (consp (cells flg n k msg)))) + +(defthm len-listn + (implies (and (integerp n) (<= 0 n)) + (equal (len (listn n x)) n))) + +(defun induct-i-k (i k) + (if (or (zp i) (zp k)) + 0 + (induct-i-k (1- i) (1- k)))) + +(defthm car-listn + (implies (and (integerp k) (< 0 k)) + (equal (car (listn k x)) x)) + :hints (("Subgoal *1/3" + :expand (listn 1 x)))) + +(defthm consp-listn + (implies (and (integerp k) (< 0 k)) + (consp (listn k x))) + :hints (("GOAL" + :expand (listn 1 x)))) + +(defthm nth-listn + (implies (and (integerp i) (<= 0 i) (< i k) (integerp k)) + (equal (nth i (listn k x)) x)) + :hints (("GOAL" + :do-not-induct t + :induct (induct-i-k i k)))) + +(defthm scan-cells-nth + ;; if rclock is in the code cell (n <= rclock < k) then + ;; the rclock'th bit of scan is the first coded bit + (implies (and (integerp rclock) (<= n rclock) + (< rclock (+ n k)) + (integerp n) (< 0 n) (integerp k) (< 0 k) + (booleanp flg) (bvp msg) (consp msg)) + (equal (nth rclock (cells flg n k msg)) + (csig flg (car msg)))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :do-not '(eliminate-destructors generalize fertilize) + :in-theory (disable REMOVE-WEAK-INEQUALITIES-ONE) + :induct (cells flg n k msg)))) + +(defthm car-append + (implies (consp a) + (equal (car (append a b)) + (car a)))) + +(defthm recv-bit-first-cell + (implies (and (integerp rclock) (<= n rclock) + (< rclock (+ n k)) + (integerp n) (< 0 n) (integerp k) (< 0 k) + (booleanp flg) (bvp msg) (consp msg)) + (equal (recv-bit rclock (cells flg n k msg)) + (car msg))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t))) + +(in-theory (disable recv-bit)) + +(defthm nthcdr-listn + (implies (and (integerp i) (integerp k) (< 0 k) (<= 0 i) + (<= i k)) + (equal (nthcdr i (listn k bit)) + (listn (- k i) bit)))) + +(defthm scan-cells-nthcdr + ;; if rclock is in the code cell (n <= rclock < k) then + ;; the msg after rclock is an append of n+k-rclock coded + ;; signals and the next cell. + (implies (and (integerp rclock) (<= n rclock) + (< rclock (+ n k)) + (integerp n) (< 0 n) (integerp k) (< 0 k) + (booleanp flg) (bvp msg) (consp msg)) + (equal (nthcdr rclock (cells flg n k msg)) + (append (listn (- (+ n k) rclock) + (csig flg (car msg))) + (cells (csig flg (car msg)) n k + (cdr msg))))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize fertilize) + :do-not-induct t + :induct (cells flg n k msg)))) + + +(defthm recv-cells-base-case-1 + (implies (and (not (consp msg)) (true-listp msg)) + (equal (recv (len msg) flg rclock (cells flg n k msg)) + msg))) + +(defthm true-listp-scan + (implies (true-listp msg) + (true-listp (scan flg msg))) + :rule-classes :type-prescription) + +(defthm bvp-scan + (implies (bvp msg) + (bvp (scan flg msg)))) + +(defthm bvp-nthcdr + (implies (bvp msg) + (bvp (nthcdr n msg))) + :hints (("GOAL" + :in-theory (disable prefer-positive-addends-<)))) + + +(defthm scan-append + (equal (scan flg (append (listn n flg) lst)) + (scan flg lst))) + +(defthm recv-append + (equal (recv i flg rclock (append (listn n flg) msg)) + (recv i flg rclock msg))) + +(defthm recv-cells + (implies (and (integerp rclock) (<= n rclock) + (< rclock (+ n k)) + (true-listp msg) + (integerp n) (< 0 n) (integerp k) (< 0 k) + (booleanp flg) (bvp msg) (consp msg)) + (equal (recv (len msg) flg rclock (cells flg n k msg)) + msg)) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :expand (recv 1 flg rclock (cells flg n k msg)) + :do-not '(eliminate-destructors generalize fertilize) + :in-theory (disable (:definition cells)) + :induct (cells flg n k msg)))) + +(defthm recv-send-is-id + (implies (and (integerp rclock) (<= n rclock) + (< rclock (+ n k)) + (true-listp msg) (natp p1) + (integerp n) (< 0 n) (integerp k) (< 0 k) + (booleanp flg) (bvp msg) (consp msg)) + (equal (recv (len msg) flg rclock + (send msg p1 n k flg)) + msg)) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize fertilize) + :cases ((and (consp msg) (consp (cdr msg)))) + :expand (recv 1 flg rclock (cells flg n k msg)) + :in-theory (disable recv len) + :do-not-induct t) + ("Subgoal 2" + :in-theory (enable len)))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/nodeset/2D-mesh-nodeset.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/nodeset/2D-mesh-nodeset.lisp new file mode 100644 index 0000000..55e2934 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/nodeset/2D-mesh-nodeset.lisp @@ -0,0 +1,133 @@ +;; Julien Schmaltz +;; July 28th 2005 +;; File: 2D-mesh-nodeset.lisp +;; We define here the coordinates of the nodes in +;; a 2D mesh. +;; We show that it is a valid instance of the +;; generic nodeset definition. + +(in-package "ACL2") + +(include-book "../../generic-modules/GeNoC-nodeset") + +;; functions to put elsewhere +(defun rev (x) + ;; reverse a true-list + (if (endp x) + nil + (append (rev (cdr x)) (list (car x))))) + + +;; 1 type of nodes (NodeSetp) +;; ------------------------------ +;; in the mesh topology, nodes are coordinates +(defun coordinatep (x) + (and (consp x) + (consp (cdr x)) + (null (cddr x)) + (natp (car x)) (natp (cadr x)))) + +(defun 2D-mesh-NodeSetp (x) + (if (endp x) + t + (and (coordinatep (car x)) + (2D-mesh-NodeSetp (cdr x))))) + +;; this function will be mapped to NodeSetp in +;; the functional instanciation + +;; 2 nodeset generator (NodeSetGenerator) +;; --------------------------------------- + +(defun x-dim-gen (X y) + ;; generate the nodes along the x-dim, y is a constant + (declare (xargs :guard (and (natp X) (natp y)))) + (if (zp X) + nil + (cons (list (1- X) y) (x-dim-gen (1- X) y)))) + +(defthm all-coordinatep-x-dim-gen + ;; x-dim-gen produces valid coordinates + (implies (and (natp x) (natp y)) + (2D-mesh-NodeSetp (x-dim-gen x y)))) + + +(defun coord-generator-1 (X Y) + ;; generate a list of coordinates + (if (zp Y) + nil + (append (x-dim-gen X (1- y)) + (coord-generator-1 X (1- Y))))) + +(defthm valid-coordinates-coord-gen-1 + (implies (and (natp x) (natp y)) + (2D-mesh-NodeSetp (coord-generator-1 x y)))) + +(defun coord-gen (X Y) + (rev (coord-generator-1 X Y))) + +(defthm valid-coordinates-coord-gen + (implies (and (natp x) (natp y)) + (2D-mesh-NodeSetp (coord-gen x y)))) + +;; as coord-gen is non-recursive function, we disable it +(in-theory (disable coord-gen)) + + +;; 3. Parameters +;; ------------ + +(defun mesh-hyps (Params) + ;; hyps on the parameters + ;; Params is a consp as well as its cdr + ;; each element of the cons is a natural + (and (consp Params) (consp (cdr Params)) (null (cddr Params)) + (natp (car Params)) (natp (cadr Params)))) + +(defun mesh-nodeset-gen (P) + ;; NODE SET GENERATOR + (coord-gen (car P) (cadr P))) + +;; this function will be mapped to +;; NodeSetGenerator + +;; 4. Prove the last constraint (subsetp) +;; -------------------------------------- +(defthm subsets-are-valid-mesh-nodesetp + (implies (and (2D-mesh-NodeSetp x) + (subsetp y x)) + (2D-mesh-NodeSetp y))) + + +;; the next lemma is needed for the instances (like XY Routing) +;(defthm 2d-mesh-nodesetgenerator +; (implies (mesh-hyps params) +; (2d-mesh-nodesetp (mesh-nodeset-gen params)))) + +;; 5. check that these definitions are compliant +;; with the generic encapsulate +;; --------------------------------------------- + +(defthm check-2D-mesh-nodeset +; (implies (true-listp x) (equal (rev (rev x)) x)) + t + :rule-classes nil +; :otf-flg t + :hints (("GOAL" + :use + (:functional-instance nodeset-generates-valid-nodes + (NodeSetp 2D-mesh-NodeSetp) + (NodeSetGenerator mesh-nodeset-gen) + (ValidParamsp mesh-hyps)) + :in-theory (disable nodeset-generates-valid-nodes)))) + + +;; end of file +;; time on my laptop (MAC) 0.00 prove + +;Summary +;Form: (CERTIFY-BOOK "2D-mesh-nodeset" ...) +;Rules: NIL +;Warnings: Free and Non-rec +;Time: 1.22 seconds (prove: 0.74, print: 0.36, other: 0.12) +; "/Users/julien/research/genoc/genoc_v0/2dmesh-nodeset/2D-mesh-nodeset.lisp"
\ No newline at end of file diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/nodeset/octagon-nodeset.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/nodeset/octagon-nodeset.lisp new file mode 100644 index 0000000..3eef082 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/nodeset/octagon-nodeset.lisp @@ -0,0 +1,63 @@ +;; Julien Schmaltz +;; File: octagon-nodeset.lisp +;; August 15th +;; definition and validation of the nodes of the Octagon +(in-package "ACL2") +;; we import the book containing the generic definition of NodeSet +(include-book "../../generic-modules/GeNoC-nodeset") + +;; 1. OctagonNodeSetGenerator +;; ------------------------- +(defun naturals (bound) + ;; define the naturals up to bound + ;; they are the nodes of the Octagon + (if (zp bound) + (list 0) + (cons bound (naturals (1- bound))))) + +(defun OctagonNodeSetGenerator (bound) + ;; more precisely we choose the bound to be the + ;; number of nodes in one quarter of the Octagon + (naturals (+ -1 (* 4 bound)))) + +(defun OctagonValidParamsp (x) + ;; the parameter is a positive integer and not zero + (and (integerp x) (< 0 x))) + +;; 2. OctagonNodeSetp +;; ----------------- +(defun OctagonValidNodep (x) + ;; a valid node is simply a natural + (natp x)) + +(defun OctagonNodeSetp (x) + ;; corresponds to the predicate NodeSetp + (if (endp x) + t + (and (OctagonValidNodep (car x)) + (OctagonNodeSetp (cdr x))))) + +;; 3. Validation of the nodes of the Octagon +;; ----------------------------------------- +;; we need to prove + +(defthm octagon-subsets-are-valid + (implies (and (OctagonNodeSetp x) + (subsetp y x)) + (OctagonNodeSetp y))) + +(defthm OctagonNodeSetp-naturals + ;; lemma needed for the next theorem + (implies (and (integerp bound) (< 0 bound)) + (OctagonNodeSetp (naturals bound)))) + +(defthm check-compliance-octagon-nodeset + t + :rule-classes nil + :hints (("GOAL" + :use (:functional-instance + nodeset-generates-valid-nodes + (ValidParamsp OctagonValidParamsp) + (NodeSetp OctagonNodeSetp) + (Nodesetgenerator OctagonNodeSetGenerator)) + :in-theory (disable nodeset-generates-valid-nodes)))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/doubleY-routing/doubleY-routing.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/doubleY-routing/doubleY-routing.lisp new file mode 100644 index 0000000..84f01c7 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/doubleY-routing/doubleY-routing.lisp @@ -0,0 +1,1223 @@ +;; Julien Schmaltz +;; Sept. 19th 2005 +;; File: doubleY-routing.lisp +;; modeling of an adaptive routing algorithm +;; we consider a 2D-mesh. We compute all possible minimal paths +;; between two nodes. +;; The algorithm is an interleaving of XY and YX. + +(in-package "ACL2") +;;; we need the xy routing algorithm +(include-book "../xy-routing/xy-routing") + +;;------------------------------------------------------------- +;; +;; I. Definition of the YX routing algorithm +;; +;;------------------------------------------------------------- + +;; the distance between two nodes is the sum of the absolute values of the difference of +;; the coordinates + +(defun yx-routing (from to) + (declare (xargs :measure (dist from to))) + ;; from = (x_o y_o) dest = (x_d y_d) + (if (or (not (coordinatep from)) + (not (coordinatep to))) + nil + (let ((x_d (car to)) + (y_d (cadr to)) + (x_o (car from)) + (y_o (cadr from))) + (if (and (equal x_d x_o) ;; x_d = x_o + (equal y_d y_o)) ;; y_d = y_o + ;; if the destination is equal to the current node, we stop + (cons from nil) + (if (not (equal y_d y_o)) ;; y_d /= y_o + (if (< y_d y_o) + ;; the y-destination is on the descending y + (cons from (yx-routing (list x_o (- y_o 1)) to)) + ;; y_d > x_o + (cons from (yx-routing (list x_o (+ 1 y_o)) to))) + ;; otherwise we test the y-direction + ;; y_d = y_o + ;; x_d /= x_o + (if (< x_d x_o) + (cons from (yx-routing (list (- x_o 1) y_o) to)) + ;; x_d > x_o + (cons from (yx-routing (list (+ 1 x_o) y_o) to)))))))) + +(defthm first-YX-routing + ;; the first element the origin + (implies (and (coordinatep from) + (coordinatep to)) + (equal (car (YX-routing from to)) + from))) + +(defthm consp-yx-routing + ;; should be systematically added + (implies (and (coordinatep from) + (coordinatep to)) + (consp (yx-routing from to)))) + + +(defun CloserListp (r d) + ;; recognizes a list r of nodes such that any higher position + ;; of the list gives a nodes that is closer to d than lower + ;; positions. More extactly, the distance decreases by 1 + ;; if the position increases by 1, + (if (or (endp r) (endp (cdr r))) + t + (and (equal (dist (cadr r) d) (1- (dist (car r) d))) + (closerlistp (cdr r) d)))) + +(defthm closertlistp-yx-routing + (closerlistp (yx-routing from to) to)) + +;; we now prove that it is a valid instance of GeNoC +;; most of the lemmas are deduced from theorems proven for the xy algorithm using +;; basic facts about rev + + +;; I.1. Validation of the basic routing function +;; ------------------------------------------- +;; we prove first some lemmas on the basic function + +;; I.1.a/ some trivial properties +;; -------------------------- + + +(defthm last-YX-routing + ;; the last element is the destination + (implies (and (coordinatep from) + (coordinatep to)) + (equal (car (last (YX-routing from to))) + to))) + +(defthm last-cdr-YX-routing + (implies (and (coordinatep from) (not (equal from to)) + (coordinatep to)) + (equal (car (last (cdr (YX-routing from to)))) to))) + +(defthm YX-routing-len->=-2 + ;; a route has at least two elements + (implies (and (coordinatep from) (coordinatep to) + (not (equal from to))) + (<= 2 (len (yx-routing from to))))) + + +;; 3.b A route is a subset of nodeset + +;; now we prove that a route is a subsetp of the set of existing nodes +;; NodeSet + +;; we reuse the strategy + +(defthm 2D-mesh-nodesetp-yx-routing + (2D-mesh-nodesetp (yx-routing from to))) + +;; First, every x-coord of any nodes produced by function yx-routing2 +;; is strictly less than 1 + Max(from_x, to_x) +(defthm yx-routing-all-x-less + (all-x-<-max (yx-routing from to) + (1+ (max (car from) (car to))))) + + +;; and every y-coord is strictly less than 1 + Max(from_y, to_y) +(defthm yx-routing-all-y-less + (all-y-<-max (yx-routing from to) + (1+ (max (cadr from) (cadr to))))) + +(defthm yx-routing-subsetp-coord-max + (implies (and (coordinatep from) (coordinatep to)) + (subsetp (yx-routing from to) + (coord-gen (1+ (max (car from) (car to))) + (1+ (max (cadr from) (cadr to)))))) + :hints (("GOAL" + :in-theory (disable max)))) + +(defthm yx-routing-subsetp-nodeset + ;; now we want to prove that if NodeSet = coord-gen x y, then + ;; route is a subsetp of NodeSet. + ;; from and to must be members of NodeSet + ;; from and to must not be equal + (implies (and (not (equal from to)) + (coordinatep from) (coordinatep to) + (natp X) (natp Y) + ;; it should be member-equal + (member-equal from (coord-gen X Y)) + (member-equal to (coord-gen X Y))) + (subsetp (yx-routing from to) (coord-gen X Y))) + :otf-flg t + :hints (("GOAL" + :use ((:instance all-max-member-equal + (L (coord-gen X Y)) + (x from) (y to) + (x-max X) (y-max Y)) + (:instance yx-routing-subsetp-coord-max)) + :do-not '(eliminate-destructors generalize fertilize) + :in-theory (disable coord-gen coordinatep natp subsetp + all-max-member-equal + yx-routing-subsetp-coord-max) + :do-not-induct t) + ("Subgoal 4" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car from))) (x2 x) + (y1 (+ 1 (cadr from))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)) + ("Subgoal 3" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car from))) (x2 x) + (y1 (+ 1 (cadr to))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)) + ("Subgoal 2" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car to))) (x2 x) + (y1 (+ 1 (cadr from))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)) + ("Subgoal 1" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car to))) (x2 x) + (y1 (+ 1 (cadr to))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)))) + + +;; Definition compatible with GeNoC +;; ----------------------------------- + +;; a Definition of the function +(defun yx-routing-top (Missives) + (if (endp Missives) + nil + (let* ((miss (car Missives)) + (from (OrgM miss)) + (to (DestM miss)) + (id (IdM miss)) + (frm (FrmM miss))) + (cons (list id frm (list (yx-routing from to))) + (yx-routing-top (cdr Missives)))))) + +(defun YXRouting (Missives NodeSet) + (declare (ignore NodeSet)) + (yx-routing-top Missives)) + + + +;; Proof of compliance +;; ------------------------ + +;; need to prove CorrectRoutesp and TrLstp and ToMissives +;; 1. ToMissives seems to be simple + +(defthm YXRouting-Missives + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (Missivesp Missives NodeSet) + (mesh-hyps Params)) + (equal (ToMissives (yx-routing-top Missives)) + Missives))) + :otf-flg t + :hints (("GOAL" + :induct (yx-routing-top Missives) + :do-not '(eliminate-destructors generalize) + :in-theory (disable coordinatep) + :do-not-induct t) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + +;; 2. TrLstp + +(defthm consp-yx-routing-cdr + ;; should be systematically added + (implies (and (coordinatep from) (not (equal from to)) + (coordinatep to)) + (consp (cdr (yx-routing from to))))) + +(defthm V-ids-yx-routing-=-M-ids + ;; this one too ... + (equal (V-ids (yx-routing-top Missives)) + (M-ids Missives))) + +(defthm TrLstp-YXRouting + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (Missivesp Missives NodeSet) + (mesh-hyps Params)) + (TrLstp (yx-routing-top Missives)))) + :hints (("GOAL" + :induct (yx-routing-top missives)) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + +;; 3. CorrectRoutesp +(defthm CorrectRoutesp-YXRouting + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (mesh-hyps Params) + (Missivesp Missives NodeSet)) + (CorrectRoutesp (yx-routing-top Missives) + Missives NodeSet))) + :hints (("GOAL" + :induct (yx-routing-top Missives) + :do-not-induct t) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + + +;; now we can prove that the XY-routing algorithm is compliant +;; to the GeNoC-routing. +(defthm check-compliance-YXRouting + t + :rule-classes nil + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use (:functional-instance + ToMissives-Routing + (NodeSetGenerator mesh-nodeset-gen) + (NodeSetp 2D-mesh-nodesetp) + (ValidParamsp mesh-hyps) + (Routing YXRouting)) + :in-theory (disable ToMissives-Routing + mesh-nodeset-gen + trlstp mesh-hyps + Missivesp)) + ("Subgoal 3" ; changed after v4-3 from "Subgoal 4", for tau system + :in-theory (enable mesh-hyps)))) + +;; this concludes the verification of the YX algorithm. +;; ---------------------------------------------------- + +;;------------------------------------------------------------- +;; +;; II. Definition of the Double-Y routing algorithm +;; +;;------------------------------------------------------------- + +;; in this algorithm, at each node two paths are possible, along the X or the Y axis. +;; We model it as the alternative application of the xy and the yx algorithms. +;; We compute all possible minimal paths between any pair of nodes. +;; Note that for all nodes that share one coordinate with a destination, +;; there is no choice: the shortest path is to travel along the opposite axis. +;; For a given source node s, all possible routes obtained by first +;; applying the xy algorithm are computed by (a) r = xy(s,d), +;; (b) applying yx for all nodes of r that do not share +;; a coordinate with d, (c) for all such routes, applying the xy algorithm to +;; each node that do not share a coordinate with d, ... + + +;; II.1. Basic definitions +;; ----------------------- + +;; we will need to append an element to every list of a list of lists. +(defun append-e-all (e L) + ;; L is a list of list + ;; we append e to every list of L + (if (endp L) + nil + (cons (cons e (car L)) + (append-e-all e (cdr L))))) + +;; we can easily prove that the length of L is not modified +(defthm len-append-e-all + (equal (len (append-e-all e L)) + (len L))) + +;; we will also need to append a list l to every list of a list of lists +(defun append-l-all (l Lst) + ;; l is a list and we append it to every list in Lst + (if (endp Lst) + nil + (cons (append l (car lst)) + (append-l-all l (cdr Lst))))) + +;; again, the length of L is not modified by this operation +(defthm len-append-l-all + (equal (len (append-l-all l Lst)) + (len Lst))) + + +;; II.2. Prefix computation +;; ------------------------ + +;; A subroute of a route from s to d, consists of a route from s to some +;; intermediate node. +;; Prefixes of a route r w.r.t. a destination d, are all the subroutes +;; where each node does not share a coordinate with d. + +(defun extract-prefixes (r d) + ;; compute all the possible prefixes suggested by the route + ;; r for the destination d + (if (or (not (coordinatep d)) (not (2D-mesh-nodesetp r))) + nil + (if (endp r) + nil + (let* ((n1 (car r)) ;; n1 is the first node of r + (n1_x (car n1)) + (n1_y (cadr n1)) + (d_x (car d)) + (d_y (cadr d))) + (if (or (equal n1_x d_x) (equal n1_y d_y)) + ;; nodes with one common coordinate with the destination + ;; do not allow any choice. + nil + (cons (list n1) ;; n1 is a prefix + (append-e-all n1 ;; all other prefixes start with n1 and the recursive call + (extract-prefixes (cdr r) d)))))))) + +;(extract-prefixes (xy-routing '(0 0) '(3 3)) '(3 3)) +;(((0 0)) +; ((0 0) (1 0)) +; ((0 0) (1 0) (2 0))) + +;; II.3. Get Sources +;; -------------------- +;; For a route r, the "sources" w.r.t. a destination d, are the nodes that do not +;; share a coordinate with destination d. + +(defun GetSources1 (r d) + (if (or (endp r) (not (coordinatep d)) + (not (2d-mesh-nodesetp r))) + nil + (let* ((n1 (car r)) + (n1_x (car n1)) + (n1_y (cadr n1)) + (d_x (car d)) + (d_y (cadr d))) + (if (or (equal n1_x d_x) (equal n1_y d_y)) + nil ;; n1 shares a coordinate with d + (cons n1 (GetSources1 (cdr r) d)))))) + +(defun GetSources (r d) + ;; we remove the first node because it has already been computed. + ;; (it is already in the prefix) + (GetSources1 (cdr r) d)) + + + +;; II.4 Double Y Routing +;; --------------------- + + +;; We need some lemmas to prove that the main function (dy1) terminates + +;; the next three defthm's are used to prove that the distance from s to d decreases +;; also from the successor of s. These lemmas consider the application +;; of the xy algorithm + + +(defthm cadr-xy-routing + (implies (and (coordinatep s) (coordinatep d) + (< (car d) (car s))) + (equal (cadr (xy-routing s d)) + (list (+ -1 (car s)) (cadr s))))) + +(defthm dist-cadr-dx-<-sx + (implies (and (coordinatep s) (coordinatep d) + (< (car d) (car s))) + (equal (dist (cadr (xy-routing s d)) d) + (1- (dist s d))))) + +(defthm dist-cadr-xy + ;; now we prove the main theorem for xy-routing and the distance + (implies (and (coordinatep s) (coordinatep d) + (or (not (equal (car s) (car d))) + (not (equal (cadr s) (cadr d))))) + (equal (dist (cadr (xy-routing s d)) d) + (1- (dist s d)))) + :hints (("Subgoal *1/1" + :use dist-cadr-dx-<-sx + :in-theory (disable dist-cadr-dx-<-sx)))) + +;; we need to prove an equivalent theorem for the application of the yx algorithm + +; lemmas for the other definition +(defthm cadr-yx-routing + (implies (and (coordinatep s) (coordinatep d) + (< (cadr d) (cadr s))) + (equal (cadr (yx-routing s d)) + (list (car s) (- (cadr s) 1))))) + +(defthm dist-cadr-dx-<-sx-yx + (implies (and (coordinatep s) (coordinatep d) + (< (cadr d) (cadr s))) + (equal (dist (cadr (yx-routing s d)) d) + (1- (dist s d))))) + +(defthm dist-cadr-yx-routing + ;; now we prove the main theorem for xy-routing and the distance + (implies (and (coordinatep s) (coordinatep d) + (or (not (equal (car s) (car d))) + (not (equal (cadr s) (cadr d))))) + (equal (dist (cadr (yx-routing s d)) d) + (1- (dist s d)))) + :hints (("Subgoal *1/1" + :use dist-cadr-dx-<-sx-yx + :in-theory (disable dist-cadr-dx-<-sx-yx)))) + +;; ------------------- + + +;; to prove termination, we need to know what is the first candidate +(defthm car-getsources1 + (let ((c (getsources1 r d))) + (implies (consp (getsources1 r d)) + (equal (car c) (car r))))) + + +(defun dy1 (sources d flg prefixes) + (declare (xargs :measure + (dist (car sources) d) + :hints (("GOAL" + :in-theory (disable reduce-integerp-+) + :do-not '(eliminate-destructors generalize)) + ("Subgoal 3" + :cases + ((consp (getsources1 + (cdr (yx-routing (car sources) d)) + d)))) + ("Subgoal 2" + :cases + ((consp (getsources1 + (cdr (xy-routing (car sources) d)) + d)))) + ("[1]Subgoal 2" + :in-theory (disable prefer-positive-addends-equal)) + ("[1]Subgoal 1" + :in-theory (disable prefer-positive-addends-equal))))) + ;; sources = a list of nodes, on which xy and yx are applied + ;; d = destination + ;; flg = t means "apply xy", nil means "apply yx" + ;; prefixes = a list of prefixes that are appended to the routes + ;; obtained by xy or yx on the nodes of sources. + ;; The function works as follows. First, sources contains + ;; only one node. We apply either xy or yx to get one route. + ;; From this route we extract a list of nodes (of "sources") + ;; that constitutes the new sources. On each of these nodes + ;; we apply either yx or xy, und so weiter .... + ;; We stop when the first node in list sources shares one coordinate + ;; with the destination. + ;; The first test gets rid of bad inputs. + ;; To prove that this function terminates, the nodes in + ;; sources must be such that nodes with a higher position in + ;; sources are closer to the destination d. + (if (or (endp sources) (not (CloserListp sources d)) + (not (2d-mesh-nodesetp sources)) + (not (coordinatep d))) + nil + (let* ((prefix (car prefixes)) + (s (car sources)) + (s_x (car s)) + (s_y (cadr s)) + (d_x (car d)) + (d_y (cadr d))) + (cond ((or (equal s_x d_x) (equal s_y d_y)) + ;; if one of the coordinate has been reached, + ;; we stop + nil) + (t + (let ((routes + (cond (flg ;; last was yx-routing, next is xy-routing + (let ((suffix (xy-routing s d))) + ;; the new route is made of the prefix and + ;; the new suffix of the route. + (cons + (append prefix suffix) + (dy1 + (getSources suffix d) + d nil ;; next is YX + (append-l-all + prefix + (extract-prefixes suffix d)))))) + (t ;; last was xy-routing, next is yx + (let ((suffix (yx-routing s d))) + (cons (append prefix suffix) + (dy1 + (getSources suffix d) + d t ;;next is XY + (append-l-all + prefix + (extract-prefixes suffix d))))))))) + (append routes + (dy1 (cdr sources) + d flg prefixes)))))))) + + + +(defun dy (s d) + ;; if s and d share a coordinate, we have a "border" case. No minimal adaptive path + ;; is available, thus we have apply either xy or yx. But, in that case, they both + ;; return the same path. + + ;; Note: it is not possible to add this special case in the previous function, because + ;; this would add routes in the computation. + + (if (and (coordinatep s) (coordinatep d) + (or (equal (car s) (car d)) + (equal (cadr s) (cadr d)))) + (list (xy-routing s d)) + + ;; when calling the "full" algorithm, we know that adapative behaviors are possible + ;; note: this is required as an invariant in the proof + + (append (dy1 (list s) d t nil) ;; flag is true,we start with xy + (dy1 (list s) d nil nil)))) ;; flag is false, we start with yx + + +;; we define the last functions to match the signature of the generic routing function + +(defun DoubleYRouting1 (Missives) + (if (endp Missives) + nil + (let* ((miss (car Missives)) + (org (OrgM miss)) + (dest (DestM miss)) + (Id (IdM miss)) + (frm (FrmM miss))) + (cons (list id frm (dy org dest)) + (DoubleYRouting1 (cdr Missives)))))) + +(defun DoubleYRouting (Missives NodeSet) + (declare (ignore NodeSet)) + (DoubleYRouting1 Missives)) + +;; this concludes the definition of the doube Y algorithm +;; --------------------------------------------------------------------------------------------- + + +;;------------------------------------------------------------- +;; +;; III. Validation of the Double-Y routing algorithm +;; +;;------------------------------------------------------------- + +;; now, we want to prove that this algorithms is a valid instance of the +;; generic routing function. + +;; The function here at the same level as xy-routing is dy. +;; The function at the same leval as xy-routing-top is doubleyRouting1. + +;; the final theorem we want to prove is: +;(defthm compliance-dbleYrouting +; t +; :rule-classes nil +; :otf-flg t +; :hints (("GOAL" +; :do-not-induct t +; :use (:functional-instance +; ToMissives-Routing +; (NodeSetGenerator mesh-nodeset-gen) +; (NodeSetp 2D-mesh-nodesetp) +; (ValidParamsp mesh-hyps) +; (Routing DoubleYRouting)) +; :in-theory (disable ToMissives-Routing +; mesh-nodeset-gen +; trlstp mesh-hyps +; Missivesp)))) +;; we can submit this theorem to see which properties have to be proven. +;; the two remaining goals are correctroutesp (routes are correct) and trlstp (travels are +;; well-formed) + +;; III.1. Proving Correctroutesp of DoubleYRouting1 +;; ------------------------------------------------ + +;; the constraint we need to relieve is the following: +;(IMPLIES (AND (MISSIVESP M (MESH-NODESET-GEN PARAMS)) +; (MESH-HYPS PARAMS)) +; (CORRECTROUTESP (DOUBLEYROUTING1 M) +; M (MESH-NODESET-GEN PARAMS))) + + + +;; the strategy is to prove validroutes and subsetp + + +(defun all-validroutep (routes s d) + ;; this predicate recognizes a list of routes where every route r starts in s and ends with d + (if (endp routes) t + (let ((r (car routes))) + (and (equal (car r) s) + (equal (car (last r)) d) + (not (equal (car r) (car (last r)))) + (all-validroutep (cdr routes) s d))))) + +(defun all-subsetp (routes nodeset) + ;; checks that all elements of routes is a subset of nodeset + (if (endp routes) + t + (let ((r (car routes))) + (and (subsetp r nodeset) + (all-subsetp (cdr routes) nodeset))))) + +(defthm tactic-is-good + (implies (and (all-subsetp routes nodeset) + (all-validroutep routes (orgm msv) (destm msv))) + (checkroutes routes msv nodeset))) + + +;; III.1.a/ all-validroutep +;; -------------------- + +;; we want to prove that dy1 satisfies this property + +(defthm all-validroutep-append + ;; removing append's by conjunctions + (equal (all-validroutep (append l1 l2) s d) + (and (all-validroutep l1 s d) + (all-validroutep l2 s d)))) + +(defun all-2d-mesh-nodesetp (lst) + ;; checks that all lists in lst are lists of valid nodes + (if (endp lst) + t + (let ((r (car lst))) + (and (and (consp r) (2d-mesh-nodesetp r)) + ;; we check that if lst is not empty, then + ;; its elements are not empty either + (all-2d-mesh-nodesetp (cdr lst)))))) + +(defthm all-2d-mesh-nodesetp-extract-prefixes + (implies (2d-mesh-nodesetp lst) + (all-2d-mesh-nodesetp (extract-prefixes lst d)))) + +(defthm all-2d-mesh-nodesetp-append-l-all + (implies (and (2d-mesh-nodesetp l) + (all-2d-mesh-nodesetp LST)) + (all-2d-mesh-nodesetp (append-l-all l LST)))) + +(defthm all-2d-mesh-append-l-all-xy-routing + ;; this lemma might not be useful to prove validroutep-apply-DoubleY-all-nodeset + ;; also s is free ... s is now (car sources) ... + (implies (all-2d-mesh-nodesetp prefixes) + (all-2d-mesh-nodesetp (append-l-all (car prefixes) + (extract-prefixes + (xy-routing (car sources) d) d))))) + +(defthm all-2d-mesh-append-l-all-yx-routing2 + (implies (all-2d-mesh-nodesetp prefixes) + (all-2d-mesh-nodesetp (append-l-all (car prefixes) + (extract-prefixes + (yx-routing (car sources) d) d))))) + + +(defthm car-last-append + (implies (consp l2) + (equal (car (last (append l1 l2))) + (car (last l2))))) + +(defthm not-member-equal-getSources + (not (member-equal d (getSources1 L d)))) + +(defthm not-member-equal-with-car + (implies (and (not (member-equal d sources)) (consp sources)) + (not (equal (car sources) d))) + :rule-classes :forward-chaining) + +(defthm 2d-mesh-coordinatep-forward + (implies (and (2d-mesh-nodesetp lst) (consp lst)) + (coordinatep (car lst))) + :rule-classes :forward-chaining) + +(defthm 2d-mesh-nodesetp-cdr + (implies (2d-mesh-nodesetp lst) + (2d-mesh-nodesetp (cdr lst))) + :rule-classes :forward-chaining) + +(defthm 2d-mesh-nodesetp-getSources1 + (implies (and (2d-mesh-nodesetp r) (coordinatep d)) + (2d-mesh-nodesetp (getSources1 r d)))) + +(defthm 2D-nodesetp-cdr-yx-routing + (2d-mesh-nodesetp (getSources1 (cdr (yx-routing from to)) to))) + +(defthm true-list-getSources1 + (true-listp (getSources1 lst d)) + :rule-classes :type-prescription) + +(defun no-common-coordinate (lst d) + ;; check that nodes of lst do not share a coordinate with d + ;; this holds in case of "adaptiveness" + (if (endp lst) + t + (let ((n (car lst))) + (and (not (equal (car n) (car d))) + (not (equal (cadr n) (cadr d))) + (no-common-coordinate (cdr lst) d))))) + +(defthm no-common-coordinate-cdr-fwd + (implies (no-common-coordinate lst d) + (no-common-coordinate (cdr lst) d)) + :rule-classes :forward-chaining) + +(defthm all-2d-mesh-cdr + (implies (all-2d-mesh-nodesetp lst) + (all-2d-mesh-nodesetp (cdr lst))) + :rule-classes :forward-chaining) + +(defthm no-common-coordinate-getSources1 + (no-common-coordinate (getSources1 lst d) d)) + +(defthm no-common-not-equal + (implies (and (no-common-coordinate sources d) + (2d-mesh-nodesetp sources) + (consp sources)) + (not (equal (car sources) d))) + :rule-classes :forward-chaining) + +(defthm last-cdr-xy-routing + (implies (and (coordinatep from) (coordinatep to) + (not (equal from to))) + (equal (car (last (cdr (xy-routing from to)))) to))) + +(defun inv-sources (sources s) + (if (endp sources) + t + (and (equal (car sources) s) + (inv-sources (cdr sources) s)))) + +(defun inv-prefixes (prefixes s) + (if (endp prefixes) + t + (and (equal (caar prefixes) s) + (inv-prefixes (cdr prefixes) s)))) + +(defun inv (prefixes sources s) + (if (endp prefixes) + (inv-sources sources s) + (inv-prefixes prefixes s))) + +(defthm inv-cdr + (implies (inv prefixes sources s) + (inv prefixes (cdr sources) s)) + :rule-classes :forward-chaining) + +(defthm car-xy-routing-append-prefixes + (implies (and (inv prefixes sources s) + (consp sources) + (2d-mesh-nodesetp sources) + (all-2d-mesh-nodesetp prefixes) + (coordinatep d) + ) + (equal (car (append (car prefixes) + (xy-routing (car sources) d))) + s))) + +(defthm car-yx-routing-append-prefixes + (implies (and (inv prefixes sources s) (consp sources) + (2d-mesh-nodesetp sources) + (all-2d-mesh-nodesetp prefixes) + (coordinatep d)) + (equal (car (append (car prefixes) + (yx-routing (car sources) d))) + s))) + + +(defthm consp-car-all-2d-mesh + (implies (and (consp lst) (all-2d-mesh-nodesetp lst)) + (consp (car lst))) + :rule-classes :forward-chaining) + + +(defthm append-l-all-nil + (implies (true-listp lst) + (equal (append-l-all nil lst) + lst))) + +(defthm inv-append-e-all-s + (implies (consp lst) + (inv (append-e-all s lst) sources s))) + +(defthm inv-prefixes-append-e-all + (implies (consp lst) + (inv-prefixes (append-e-all s lst) s))) + +(defthm inv-prefixes-append-l-all + (implies (and (consp lst) (inv-prefixes prefixes s) (consp prefixes) + (all-2d-mesh-nodesetp prefixes)) + (inv-prefixes (append-l-all (car prefixes) lst) s))) + +(defthm consp-append-e-all + (implies (consp lst) + (consp (append-e-all e lst)))) + + +;; we first link car and append +(defthm car-append + (implies (consp a) + (equal (car (append a b)) + (car a)))) + +(defthm inv-append-l-all-xy-routing + (implies (and (inv prefixes sources s) + (no-common-coordinate sources d) + (coordinatep s) (coordinatep d) (consp sources) + (all-2d-mesh-nodesetp prefixes) + (2d-mesh-nodesetp sources)) + (INV (APPEND-L-ALL (CAR PREFIXES) + (EXTRACT-PREFIXES (XY-ROUTING (CAR SOURCES) D) + D)) + (GETSOURCES1 (CDR (XY-ROUTING (CAR SOURCES) D)) + D) + S)) + :otf-flg t + :hints (("GOAL" + :cases ((consp prefixes)) + :do-not-induct t + :do-not '(eliminate-destructors generalize)) + ("Subgoal 2.2.1" + :cases ((consp (extract-prefixes (cdr (xy-routing s d)) d)))) + ("Subgoal 1.2.1" + :cases ((consp (extract-prefixes (cdr (xy-routing (car sources) d)) d)))))) + + +(defthm inv-append-l-all-comprefix-getcand-yx-routing + (implies (and (inv prefixes sources s) + (no-common-coordinate sources d) + (coordinatep s) (coordinatep d) (consp sources) + (all-2d-mesh-nodesetp prefixes) + (2d-mesh-nodesetp sources)) + (INV (APPEND-L-ALL (CAR PREFIXES) + (EXTRACT-PREFIXES (YX-ROUTING (CAR SOURCES) D) + D)) + (GETSOURCES1 (CDR (YX-ROUTING (CAR SOURCES) D)) + D) + S)) + :otf-flg t + :hints (("GOAL" + :cases ((consp prefixes)) + :do-not '(eliminate-destructors generalize) + :do-not-induct t) + ("Subgoal 2.2.1" + :cases ((consp (extract-prefixes (cdr (yx-routing s d)) d)))) + ("Subgoal 1.2.1" + :cases ((consp (extract-prefixes (cdr (yx-routing (car sources) d)) d)))))) + + +(defthm validroutep-apply-DoubleY-all-nodeset + (implies (and (all-2d-mesh-nodesetp prefixes) ;; this true even if prefixes is empty + (coordinatep d) (coordinatep s) + (not (equal s d)) + (no-common-coordinate sources d) + (consp sources) + (2d-mesh-nodesetp sources) + (inv prefixes sources s) + ) + (all-validroutep (dy1 sources d flg prefixes) + s d)) + :hints (("GOAL" + :in-theory (e/d () + (all-2d-mesh-nodesetp member-equal 2d-mesh-nodesetp coordinatep + no-common-coordinate xy-routing yx-routing extract-prefixes + getSources1 append-e-all append-l-all closerlistp inv)) + :do-not '(eliminate-destructors generalize)))) + + +;; III.1.b/ all-subsetp +;; -------------------- + +;; we now prove that the routes produced by the double Y routing algorithm use only existing +;; nodes + +;; we need to prove that the routes computed by apply-doubleY-all are +;; subsets of NodeSet = coord-gen(X,Y), i.e. the following theorem: +;;(defthm subsetp-apply-DoubleY-all-nodeset +;; (implies (and (2d-mesh-nodesetp sources) (coordinatep d) +;; (member-equal d (coord-gen X Y)) +;; (not (member-equal d sources)) +;; (natp X) (natp Y) +;; (subsetp sources (coord-gen X Y)) +;; (all-subsetp prefixes (coord-gen X Y))) +;; (all-subsetp (dy1 sources d flg prefixes) +;; (coord-gen X Y))) +;; + +(defthm subsetp-cdr-fwd + (implies (subsetp l lst) + (subsetp (cdr l) lst)) + :rule-classes :forward-chaining) + +(defthm all-subsetp-append + (equal (all-subsetp (append l1 l2) S) + (and (all-subsetp l1 S) + (all-subsetp l2 S)))) + +(defthm subsetp-append-better + (equal (subsetp (append l1 l2) S) + (and (subsetp l1 S) + (subsetp l2 S)))) + +(defthm subsetp-member-equal + (implies (and (subsetp sources S) + (consp sources)) + (member-equal (car sources) S)) + :rule-classes :forward-chaining) + +(defthm subsetp-append-l-all + (equal (all-subsetp (append-l-all l l1) s) + (if (consp l1) + (and (subsetp l s) (all-subsetp l1 s)) + t))) + +(defthm all-subsetp-subsetp-extract-prefixes + (implies (subsetp l s) + (all-subsetp (extract-prefixes l d) s))) + + +(defthm subsetp-trans + (implies (and (subsetp s1 s2) + (subsetp s2 s3)) + (subsetp s1 s3))) + +(defthm subsetp-getSources + (subsetp (getSources1 lst d) lst)) + + +(defthm subsetp-cdr-rev + (implies (subsetp l s) + (subsetp (cdr l) s))) + +(defthm subsetp-getSources1-xy-routing + (implies (and (not (equal s d)) + (coordinatep s) (coordinatep d) + (natp X) (natp Y) + (member-equal s (coord-gen X Y)) + (member-equal d (coord-gen X Y))) + (subsetp (getSources1 (cdr (xy-routing s d)) d) + (coord-gen x y))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use (:instance subsetp-trans + (s1 (getSources1 (cdr (xy-routing s d)) d)) + (s2 (cdr (xy-routing s d))) + (s3 (coord-gen x y))) + :in-theory (disable coordinatep natp subsetp-trans) + :do-not '(eliminate-destructors generalize fertilize)))) + + +(defthm subsetp-getSources1-yx-routing + (implies (and (not (equal s d)) + (coordinatep s) (coordinatep d) + (natp X) (natp Y) + (member-equal s (coord-gen X Y)) + (member-equal d (coord-gen X Y))) + (subsetp (getSources1 (cdr (yx-routing s d)) d) + (coord-gen x y))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use (:instance subsetp-trans + (s1 (getSources1 (cdr (yx-routing s d)) d)) + (s2 (cdr (yx-routing s d))) + (s3 (coord-gen x y))) + :in-theory (disable coordinatep natp subsetp-trans) + :do-not '(eliminate-destructors generalize fertilize)))) + +(defthm subsetp-apply-DoubleY-all-nodeset + (implies (and (all-2d-mesh-nodesetp prefixes) + (coordinatep d) (member-equal d (coord-gen X Y)) + (consp sources) + (2d-mesh-nodesetp sources) + (no-common-coordinate sources d) + (natp X) (natp Y) + (subsetp sources (coord-gen X Y)) + (all-subsetp prefixes (coord-gen X Y))) + (all-subsetp (dy1 sources d flg prefixes) + (coord-gen X Y))) + :hints (("GOAL" + :in-theory (e/d () + (all-2d-mesh-nodesetp member-equal 2d-mesh-nodesetp coordinatep + no-common-coordinate xy-routing yx-routing extract-prefixes + getSources1 append-e-all append-l-all closerlistp subsetp)) + :do-not '(eliminate-destructors generalize)))) + + + +;; III.1 c/ checkroutes of dy1 +;; ------------------------------------------- + +;; now we put all-validroutep and all-subsetp together to prove checkroutes + +(defthm checkroutes-apply-doubleY + (implies (and (all-2d-mesh-nodesetp prefixes) + (coordinatep (destm msv)) (member-equal (destm msv) (coord-gen X Y)) + (consp sources) + (2d-mesh-nodesetp sources) + (no-common-coordinate sources (destm msv)) + (natp X) (natp Y) + (subsetp sources (coord-gen X Y)) + (all-subsetp prefixes (coord-gen X Y)) + (not (equal (orgm msv) (destm msv))) + (coordinatep (orgm msv)) + (inv prefixes sources (orgm msv))) + (checkroutes (dy1 sources (destm msv) flg prefixes) + msv + (coord-gen X Y))) + :otf-flg t + :hints (("GOAL" + :use (:instance tactic-is-good + (routes (dy1 sources (destm msv) flg prefixes)) + (nodeset (coord-gen X Y))) + :do-not '(eliminate-destructors generalize) + :in-theory (e/d () (coordinatep natp dy1 inv checkroutes + tactic-is-good)) + :do-not-induct t))) + + + +;; III.1 d/ correctroutesp of dy1 +;; --------------------------------------------- + +;; we can now conclude III.1 + +(defthm checkroutes-append + (equal (checkroutes (append l1 l2) nodes S) + (and (checkroutes l1 nodes s) + (checkroutes l2 nodes s)))) + +(defthm nth3-cdddr + (implies (and (consp x) (consp (cdr x)) (consp (cddr x)) (consp (cdddr x))) + (equal (nth 3 x) + (car (cdddr x))))) + +(defthm CorrectRoutesp-DoubleYRouting1 + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (mesh-hyps Params) + (Missivesp Missives NodeSet)) + (CorrectRoutesp (DoubleYRouting1 Missives) + Missives NodeSet))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize) + :in-theory (e/d () (all-2d-mesh-nodesetp coordinatep coord-gen + all-subsetp)) + :induct (DoubleYRouting1 Missives) + :do-not-induct t) + ("Subgoal *1/2.3.2" + :use (:instance checkroutes-apply-doubleY + (sources (list (cadar missives))) + (msv (car missives)) (flg T) (prefixes nil) + (x (car params)) (y (cadr params))) + :in-theory (e/d (coordinatep) (checkroutes-apply-doubleY))) + ("Subgoal *1/2.3.1" + :use (:instance checkroutes-apply-doubleY + (sources (list (cadar missives))) + (msv (car missives)) (flg nil) (prefixes nil) + (x (car params)) (y (cadr params))) + :in-theory (e/d (coordinatep) (checkroutes-apply-doubleY))))) + + +;; III.2. Proving TrLstp of DoubleYRouting1 +;; ------------------------------------------------ + +(defthm V-ids-dy-=-M-ids + (equal (V-ids (DoubleYRouting1 Missives)) + (M-ids Missives))) + +(defthm consp-dy1 + (implies (and (consp sources) + (closerlistp sources d) + (no-common-coordinate sources d) + (2d-mesh-nodesetp sources) + (coordinatep d)) + (consp (dy1 sources d flg prefixes))) + :hints (("GOAL" + :in-theory (e/d () + (all-2d-mesh-nodesetp member-equal 2d-mesh-nodesetp coordinatep + xy-routing yx-routing extract-prefixes + getSources1 append-e-all append-l-all closerlistp subsetp)) + :do-not '(eliminate-destructors generalize)))) + +(defthm validfield-route-append + (equal (validfield-route (append l1 l2)) + (and (validfield-route l1) + (validfield-route l2)))) + + +(defthm consp-cdr-append + (implies (consp (cdr x)) + (consp (cdr (append y x))))) + +(defthm validfield-route-apply-doubleY-all + (implies (and (consp sources) + (closerlistp sources d) + (no-common-coordinate sources d) + (2d-mesh-nodesetp sources) + (coordinatep d)) + (validfield-route (dy1 sources d flg prefixes))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize) + :in-theory (e/d () (2d-mesh-nodesetp coordinatep xy-routing yx-routing + coordinatep extract-prefixes getSources1 closerlistp + no-common-coordinate)))) + ) + +(defthm TrLstp-DoubleYRouting1 + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (Missivesp Missives NodeSet) + (mesh-hyps Params)) + (TrLstp (DoubleYRouting1 Missives)))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :do-not '(eliminate-destructors generalize) + :induct (doubleYRouting1 missives)) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + + + +;; III.3. Checking Compliance with GeNoC +;; ------------------------------------- + + +(defthm check-compliance-DoubleYRouting + t + :rule-classes nil + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use (:functional-instance + ToMissives-Routing + (NodeSetGenerator mesh-nodeset-gen) + (NodeSetp 2D-mesh-nodesetp) + (ValidParamsp mesh-hyps) + (Routing DoubleYRouting)) + :in-theory (disable ToMissives-Routing + mesh-nodeset-gen + trlstp mesh-hyps + Missivesp)) + ("Subgoal 4" ; changed after v4-3 from "Subgoal 5", for tau system + :in-theory (enable mesh-hyps)))) + +;; Q.E.D. !
\ No newline at end of file diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/getting_rid_of_mod.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/getting_rid_of_mod.lisp new file mode 100644 index 0000000..73e1a17 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/getting_rid_of_mod.lisp @@ -0,0 +1,405 @@ +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- +;; +;; +;; Functional Specification and Validation of the Octagon Network on +;; Chip using the ACL2 Theorem Prover +;; +;; +;; Proof Script +;; +;; +;; Julien Schmaltz +;; Joseph Fourier University +;; 46, av. Felix Viallet 38031 Grenoble Cedex +;; FRANCE +;; Julien.Schmaltz@imag.fr +;; +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- + +;; File: getting_rid_of_mod.lisp +;; Implements a strategy to rewrite the function Route to functions that +;; create lists and do not use the function mod + +(in-package "ACL2") + +;; we import the definition of the functio Route +(include-book "routing_defuns") + +(set-non-linearp t) + +;;---------------------------------------------------------------------- +;;---------------------------------------------------------------------- +;; +;; GETTING RID OF MOD +;; +;;---------------------------------------------------------------------- +;;---------------------------------------------------------------------- + + +;; To reason about function "route", I define, for each possible case of +;; (mod (+ dest (- from)) n) a function that computes a list of nodes and +;; that does not use function mod. Then, the properties are generally +;; trivial on these small functions and the properties on route are +;; proved by a simple case split. + +;; We divide the Octagon in quarters and bound, according to the value +;; of (- dest from). + +;;----------------------------------------------------------------------- +;; +;; Quarter 1 +;; (and (<= (- to from) n) +;; (<= 0 (- to from)))) +;; +;;----------------------------------------------------------------------- + + +(defun quarter_1_list (from to) + (declare (xargs :measure (nfix (+ to (- from))) + :hints + (("GOAL" + :in-theory (disable prefer-positive-addends-< + simplify-sums-< + prefer-positive-addends-equal))))) + (if (zp (- to from)) + (cons from nil) + (cons from (quarter_1_list (+ 1 from) to)))) + + +;; I prove that route is equal to this function in this quarter + +(defthm route_=_quarter_1 + (implies (and (natp from) (natp to) + (< to (* 4 n)) (< from (* 4 n)) + (integerp n) (< 0 n) + (and (<= (- to from) n) + (<= 0 (- to from)))) + (equal (route from to n) + (quarter_1_list from to))) + :hints (("GOAL" + :in-theory (disable + (:REWRITE MOD-POSITIVE . 1) + prefer-positive-addends-< + prefer-positive-addends-equal) + :do-not '(eliminate-destructors generalize)))) + +;;----------------------------------------------------------------------- +;; +;; Quarter -4 +;; (and (<= (- to from) (* -3 n)) +;; (< (- (* 4 n)) (- to from)))) +;; +;;----------------------------------------------------------------------- + +;; comes next because defined using quarter_1_list + +(defun quarter_minus_4_list (from to n) + (declare (xargs :measure (nfix (- (+ -1 (* 4 n)) from)) + :hints + (("GOAL" + :in-theory (disable prefer-positive-addends-< + simplify-sums-< + prefer-positive-addends-equal))))) + (cond ((equal (- to from) 0) (cons from nil)) + ((zp (- (+ (* 4 n) -1) from)) + (cons from (quarter_1_list 0 to))) + (t + (cons from (quarter_minus_4_list (+ 1 from) to n))))) + +(defthm route_=_quarter_minus_4_list + (implies (and (integerp from) + (integerp to) + (<= 0 to) + (<= 0 from) + (< to (* 4 n)) + (< from (* 4 n)) + (integerp n) + (and (<= (- to from) (* -3 n)) + (< (- (* 4 n)) (- to from)))) + (equal (route from to n) + (quarter_minus_4_list from to n))) + :hints (("GOAL" + :in-theory (disable (:REWRITE MOD-POSITIVE . 1))))) + +;;----------------------------------------------------------------------- +;; +;; Quarter 3 +;; (and (< (- to from) (* 3 n)) +;; (< (* 2 n) (- to from)))) +;; +;;----------------------------------------------------------------------- + + +(defun quarter_3_list (from to n) + (cons from + (cons (+ from (* 2 n)) + (quarter_1_list (+ from (* 2 n) 1) to)))) + +(defthm route_=_quarter_3 + (implies (and (integerp from) + (integerp to) + (<= 0 to) + (<= 0 from) + (< to (* 4 n)) + (< from (* 4 n)) + (integerp n) + (and (< (- to from) (* 3 n)) + (< (* 2 n) (- to from)))) + (equal (route from to n) + (quarter_3_list from to n))) + :hints (("GOAL" :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal)))) + +;;----------------------------------------------------------------------- +;; +;; Quarter -2 +;; (and (< (- to from) (- n)) +;; (< (* -2 n) (- to from)))) +;; +;;----------------------------------------------------------------------- + + +(defun quarter_minus_2_list (from to n) + (if (<= (* 2 n) from) + (cons from + (cons (+ from (* -2 n)) + (quarter_1_list (+ 1 from (* -2 n)) to))) + (cons from + (quarter_minus_4_list (+ from (* 2 n)) to n)))) + +(defthm route_=_quarter_minus_2_list + (implies (and (integerp from) + (integerp to) + (<= 0 to) + (<= 0 from) + (< to (* 4 n)) + (< from (* 4 n)) + (integerp n) + (and (< (- to from) (- n)) + (< (* -2 n) (- to from)))) + (equal (route from to n) + (quarter_minus_2_list from to n))) + :hints (("GOAL" + :in-theory (disable + prefer-positive-addends-equal + prefer-positive-addends-<)))) + +;;----------------------------------------------------------------------- +;; +;; Quarter -1 +;; (and (< (- to from) 0) +;; (<= (- n) (- to from)))) +;; +;;----------------------------------------------------------------------- + + +(defun quarter_minus_1_list (from to) + (declare (xargs :measure (nfix (- from to)) + :hints + (("GOAL" + :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal))))) + (if (zp (- from to)) + (cons from nil) + (cons from (quarter_minus_1_list (+ -1 from) to)))) + + +(defthm route_=_quarter_minus_1_list + (implies (and (integerp from) + (integerp to) + (<= 0 to) + (integerp n) + (< from (* 4 n)) + (< to (* 4 n)) + (and (< (- to from) 0) + (<= (- n) (- to from)))) + (equal (route from to n) + (quarter_minus_1_list from to))) + :hints (("GOAL" :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal)))) + +;;----------------------------------------------------------------------- +;; +;; Quarter -3 +;; (and (< (* -3 n) (- to from)) +;; (< (- to from) (* -2 n)))) +;; +;;----------------------------------------------------------------------- + +(defun quarter_minus_3_list (from to n) + (cons from + (cons (+ from (* -2 n)) + (quarter_minus_1_list (+ -1 from (* -2 n)) to)))) + +(defthm route_=_quarter_minus_3_list + (implies (and (integerp from) + (<= 0 from) + (< from (* 4 n)) + (integerp to) + (<= 0 to) + (< to (* 4 n)) + (integerp n) + (< 0 n) + (and (< (* -3 n) (- to from)) + (< (- to from) (* -2 n)))) + (equal (route from to n) + (quarter_minus_3_list from to n))) + :hints (("GOAL" :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal)))) + +;;----------------------------------------------------------------------- +;; +;; Quarter 4 +;; (and (<= (* 3 n) (- to from)) +;; (< (- to from) (* 4 n)))) +;; +;;----------------------------------------------------------------------- + +(defun quarter_4_list (from to n) + (declare (xargs :hints (("GOAL" + :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal + simplify-sums-<))))) + (cond ((zp from) + (cons from (quarter_minus_1_list (+ -1 (* 4 n)) to))) + ((equal (- to from) 0) + (cons from nil)) + (t + (cons from (quarter_4_list (+ -1 from) to n))))) + +(defthm route_=_quarter_4_list_lemma_1 + (implies (and (integerp from) + (integerp to) + (<= 0 to) + (integerp n) + (< 0 n) + (< from (* 4 n)) + (< to (* 4 n)) + (<= 0 from) + (and (< (- to from) 1) + (<= (+ 1 (- n)) (- to from)))) + (equal (route from to n) + (quarter_minus_1_list from to))) + :hints (("GOAL" :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal)))) + +(defthm route_=_quarter_4_list + (implies (and (integerp from) + (<= 0 from) + (< from (* 4 n)) + (integerp to) + (<= 0 to) + (< to (* 4 n)) + (< 0 n) + (integerp n) + (< 0 n) + (and (<= (* 3 n) (- to from)) + (< (- to from) (* 4 n)))) + (equal (route from to n) + (quarter_4_list from to n))) + :hints (("GOAL" :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal)))) + +;;----------------------------------------------------------------------- +;; +;; Quarter -2 +;; (and (< n (- to from)) +;; (< (- to from) (* 2 n)))) +;; +;;----------------------------------------------------------------------- + +(defun quarter_2_list (from to n) + (if (< from (* 2 n)) + (cons from + (cons (+ from (* 2 n)) + (quarter_minus_1_list (+ -1 from (* 2 n)) to))) + (cons from + (quarter_4_list (+ from (* -2 n)) to n)))) + + +(defthm route_=_quarter_2_list + (implies (and (integerp from) + (<= 0 from) + (< from (* 4 n)) + (integerp to) + (<= 0 to) + (< to (* 4 n)) + (integerp n) + (< 0 n) + (and (< n (- to from)) + (< (- to from) (* 2 n)))) + (equal (route from to n) + (quarter_2_list from to n))) + :hints (("GOAL" + :in-theory (disable prefer-positive-addends-< + prefer-positive-addends-equal)))) + +;;----------------------------------------------------------------------- +;; +;; BOUNDS +;; +/- (* 2 n) +;; +;;----------------------------------------------------------------------- + + +(defun bounds (from n) + (if (<= (* 2 n) from) + (cons from (cons (+ from (* -2 n)) nil)) + (cons from + (cons (+ from (* 2 n)) nil)))) + +(defthm route_=_bounds + (implies (and (integerp from) + (<= 0 from) + (< from (* 4 n)) + (integerp to) + (<= 0 to) + (< to (* 4 n)) + (integerp n) + (< 0 n) + (or (equal (+ to (- from)) (* 2 n)) + (equal (+ to (- from)) (* -2 n)))) + (equal (route from to n) + (bounds from n)))) + +;; End of the "splitting" +;;----------------------- + +;; now we have rules for all the possible cases, we can disable route + +(in-theory (disable route)) + +;;------------------------ + +;; A useful computed hint + + +;; and for all theorem we will split into all these cases +;; To help, we define the following computed hint: + +(defun computed_hint_route (id clause world) + (declare (ignore clause world)) + (if (equal id '((0) NIL . 0)) + '(:cases ((and (<= (- to from) n) + (<= 0 (- to from))) + (and (<= (- to from) (* -3 n)) + (< (- (* 4 n)) (- to from))) + (and (< (- to from) (* 3 n)) + (< (* 2 n) (- to from))) + (and (< (- to from) (- n)) + (< (* -2 n) (- to from))) + (and (< (- to from) 0) + (<= (- n) (- to from))) + (and (< (* -3 n) (- to from)) + (< (- to from) (* -2 n))) + (and (<= (* 3 n) (- to from)) + (< (- to from) (* 4 n))) + (and (< n (- to from)) + (< (- to from) (* 2 n))) + (equal (+ to (- from)) (* 2 n)) + (equal (+ to (- from)) (* -2 n)))) + nil)) + + diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/mod_lemmas.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/mod_lemmas.lisp new file mode 100644 index 0000000..d41c057 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/mod_lemmas.lisp @@ -0,0 +1,133 @@ +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- +;; +;; +;; Functional Specification and Validation of the Octagon Network on +;; Chip using the ACL2 Theorem Prover +;; +;; +;; Proof Script +;; +;; +;; Julien Schmaltz +;; Joseph Fourier University +;; 46, av. Felix Viallet 38031 Grenoble Cedex +;; FRANCE +;; Julien.Schmaltz@imag.fr +;; +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- + +;; File: mod_lemmas.lisp +;; all the lemmas about mod needed to prove that the routing algorithm +;; terminates + +(in-package "ACL2") + +(include-book "arithmetic-3/bind-free/top" :dir :system) + +(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp + hist pspv))) +(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system) + +(defthm mod-x-=-x + (implies (and (rationalp x) + (integerp n) + (<= 0 x) + (< 0 n) + (< x n)) + (equal (mod x n) x))) + +(local + (defthm lemma_for_next_theorem + (implies (and (rationalp x) + (< 0 x) + (< x n) + (integerp n) + (< 0 n)) + (equal (mod (- x) n) + (+ (- x) n)))) +) + +(defthm mod-x-=-x-+-n + (implies (and (rationalp x) + (< x 0) + (< (- x) n) + (integerp n) + (< 0 n)) + (equal (mod x n) + (+ x n))) + :hints (("GOAL" + :use (:instance lemma_for_next_theorem + (x (- x)))))) + + +(defthm abs-<-1-imp-not-int + (implies (and (< (abs x) 1) + (not (equal x 0))) + (not (integerp x)))) + +(defthm mod-x-=-minusx-pos + (implies (and (rationalp x) + (integerp n) + (< 0 n) + (<= n x) + (< x (* 2 n))) + (equal (mod x n) + (- x n)))) + +(defthm mod-+-n/2-pos + (implies (and (< x n) + (rationalp x) + (integerp n) + (<= (* 1/2 n) x) + (< 2 n) + ) + (< (mod (+ x (* 1/2 n)) n) + (mod x n)))) + +(defthm mod-+-n/2-neg + (implies (and (< x 0) + (< (- x) n) + (rationalp x) + (<= (- x) (* 1/2 n)) + (integerp n) + (< 0 n)) + (< (mod (+ x (* 1/2 n)) n) + (mod x n)))) + +(defthm mod-+-1/2-=-mod-minus-1/2 + (implies (and (integerp n) + (< 0 n) + (rationalp x) + (< (abs x) n)) + (equal (mod (+ x (* -1/2 n)) n) + (mod (+ x (* 1/2 n)) n))) + :hints (("GOAL" :in-theory (enable mod)))) + +(defthm mod-n/2-pos + (implies (and (< 0 x) + (< x n) + (rationalp x) + (integerp n) + (<= (* 1/2 n) x) + (< 0 n) + ) + (< (mod (+ x (* -1/2 n)) n) + (mod x n)))) + +(defthm mod-n/2-neg + (implies (and (< x 0) + (< (- x) n) + (rationalp x) + (<= (- x) (* 1/2 n)) + (integerp n) + (< 0 n)) + (< (mod (+ x (* -1/2 n)) n) + (mod x n)))) + +;;Summary +;;Form: (CERTIFY-BOOK "mod_lemmas" ...) +;;Rules: NIL +;;Warnings: Guards +;;Time: 2.91 seconds (prove: 0.84, print: 0.04, other: 2.03) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_defuns.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_defuns.lisp new file mode 100644 index 0000000..8bf1dee --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_defuns.lisp @@ -0,0 +1,142 @@ +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- +;; +;; +;; Functional Specification and Validation of the Octagon Network on +;; Chip using the ACL2 Theorem Prover +;; +;; +;; Proof Script +;; +;; +;; Julien Schmaltz +;; Joseph Fourier University +;; 46, av. Felix Viallet 38031 Grenoble Cedex +;; FRANCE +;; Julien.Schmaltz@imag.fr +;; +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- + +;; File: routing.lisp +;; Proof of the Routing Algorithm + +(in-package "ACL2") + + +;;---------------------------------------------------------------------- +;;---------------------------------------------------------------------- +;; +;; DEFINITION OF THE AVAILABLE MOVES IN THE NETWORK +;; +;;---------------------------------------------------------------------- +;;---------------------------------------------------------------------- + +;; we define the three possible moves in the Octagon +(defun n_clockwise (from n) + (mod (+ from 1) (* 4 n))) + +(defun n_counter_clockwise (from n) + (mod (- from 1) (* 4 n))) + +(defun n_across (from n) + (mod (+ from (* 2 n)) (* 4 n))) + +;;-------------------------------------------------------------------- +;; IMPORTING LEMMAS ABOUT MOD +;;-------------------------------------------------------------------- +(include-book "mod_lemmas") + +;; this book also import the books on Arithmetic + +;;-------------------------------------------------------------------- +;; USEFUL LOCAL LEMMAS +;;------------------------------------------------------------------- + +;; the following lemmas are used to force some behavior of ACL2 + +(local +(defthm force_case_split + (implies (and (integerp dest) + (integerp from) + (<= 0 dest) + (<= 0 from)) + (iff (not (equal dest from)) + (or (< (+ dest (- from)) 0) + (< 0 (+ dest (- from)))))) + :rule-classes nil) +) + +(local +(defthm <=_=_<_or_= + (implies (and (acl2-numberp a) + (acl2-numberp b) + ) + (equal (<= a b) + (or (< a b) + (= a b)))) + :rule-classes nil) +) + + +;;---------------------------------------------------------------------- +;;---------------------------------------------------------------------- +;; +;; DEFINITION OF THE ROUTING ALGORITHM +;; +;;---------------------------------------------------------------------- +;;---------------------------------------------------------------------- + +;; to simplify a little the ACL2 proof, n represents the number of nodes +;; in one quarter of the Octagon. So, there are 4*n nodes in the network! + +(defun route (from dest n) + (declare (xargs :measure (min (nfix (mod (- dest from) (* 4 n))) + (nfix (mod (- from dest) (* 4 n)))) + :hints + (("GOAL" + :use ((:instance force_case_split) + (:instance <=_=_<_or_= + (a dest) (b (+ -1 (* 4 n)))) + (:instance <=_=_<_or_= + (a from) (b (+ -1 (* 4 n)))) + (:instance mod-+-n/2-pos + (n (* 4 n)) + (x (+ (- dest) from)))) + :in-theory (disable PREFER-POSITIVE-ADDENDS-< + prefer-positive-addends-equal + reduce-integerp-+ + mod-+-n/2-pos)) + ("Subgoal 330.4" :cases ((<= 0 (+ -1 from)) + (< (+ -1 from) 0)))))) + (cond ((or + (not (integerp dest)) ;; dest must be an integer + (< dest 0) ;; dest must be positive + (< (- (* 4 n) 1) dest) ;; dest must be lower than the number of nodes + (not (integerp from)) ;; from must be an integer + (< from 0) ;; from must be positive + (< (- (* 4 n) 1) from) ;; from must be lower than the number of nodes + (not (integerp n)) ;; the number of nodes must be an integer + (<= n 0)) ;; n must be positive + nil) ;; if all the conditions are not OK then we return nil + ((equal (- dest from) 0) (cons from nil));; process at node + ((and (< 0 (mod (- dest from) (* 4 n))) + (<= (mod (- dest from) (* 4 n)) n)) + ;;If we go clock wise the dest is the next of the next next + ;;but dest is in the same quarter + (cons from (route (n_clockwise from n) dest n))) + (;(and (<= (* 3 n) (mod (- dest from) (* 4 n))) + ; (< (mod (- dest from) (* 4 n)) (* 4 n))) + (<= (* 3 n) (mod (- dest from) (* 4 n))) + ;;If we go cc dest is in the same quarter too + (cons from (route (n_counter_clockwise from n) dest n))) + (t + ;; else we cross and then the dest will be in the same quarter + (cons from (route (n_across from n) dest n))))) + +;; ACL2 finds the :type-prescription (TRUE-LISTP (N_GO_TO_NODE FROM DEST N)) + +;;Warnings: None +;;Time: 85.04 seconds (prove: 80.95, print: 4.02, other: 0.07) +;; ROUTE + diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_local_lemmas.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_local_lemmas.lisp new file mode 100644 index 0000000..2dded6e --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_local_lemmas.lisp @@ -0,0 +1,414 @@ +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- +;; +;; +;; Functional Specification and Validation of the Octagon Network on +;; Chip using the ACL2 Theorem Prover +;; +;; +;; Proof Script +;; +;; +;; Julien Schmaltz +;; Joseph Fourier University +;; 46, av. Felix Viallet 38031 Grenoble Cedex +;; FRANCE +;; Julien.Schmaltz@imag.fr +;; +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- + + +;; File: routing_local_lemmas.lisp +;; Contains lemmas needed to prove the main theorem on Route. +;; This book will be included locally in the next one, so that we do +;; not export the lemmas herein in the main proof about Octagon. + +;; August 15th +;; JS: I update this file to match the last version of GeNoC +;; I remove the proof that there is no duplicate and everything +;; in relation with the predicate availablemovep, which is no +;; longer present in GeNoC. +(in-package "ACL2") +;; we import definitions and theorems to work on lists +(include-book "data-structures/list-defuns" :dir :system) +(include-book "data-structures/list-defthms" :dir :system) + +;; To reason about function "route", I define, for each possible case of +;; (mod (+ dest (- from)) n) a function that computes a list of nodes and +;; that does not use function mod. Then, the properties are generally +;; trivial on these small functions and the properties on route are +;; proved by a simple case split. +;; We divide the Octagon in quarters and bound, according to the value +;; of (- dest from). +;; this strategy is embedded inside a book. +(include-book "getting_rid_of_mod") + +;;----------------------------------------------------------------------- +;;----------------------------------------------------------------------- +;; +;; CORRECTNESS OF FUNCTION ROUTE +;; +;;----------------------------------------------------------------------- +;;----------------------------------------------------------------------- + +;; we first prove some useful lemmas about the different moves +(defthm natp_n_across + (implies (and (natp x) (integerp n) (< 0 n)) + (natp (n_across x n)))) + +(defthm n_across_<_n + (implies (and (natp x) (integerp n) (< 0 n)) + (< (n_across x n) (* 4 n)))) + +(defthm natp_counterclockwise + (implies (and (natp x) (integerp n) (< 0 n)) + (natp (n_counter_clockwise x n)))) + +(defthm n_counter_clockwise_<_n + (implies (and (natp x) (integerp n) (< 0 n)) + (< (n_counter_clockwise x n) (* 4 n)))) + +;;------------------------------------------------------------------------ +;; 1. true-listp, consp, len +;;------------------------------------------------------------------------ + +(defthm true-listp_route + ;; route produces a true-listp + (true-listp (route from to n)) + :rule-classes :type-prescription) + +(defthm consp_route + ;; route is a consp + (implies (and (natp from) (natp to) (integerp n) (< 0 n) + (< to (* 4 n)) (< from (* 4 n))) + (consp (route from to n))) + :hints (("GOAL" + :in-theory (enable route) + :induct (route from to n)))) + +(defthm len_route_>=_2 + ;; if from /= to, then route produces a path with at least + ;; two nodes + (implies (and (natp from) (natp to) + (integerp n) (< 0 n) + (< to (* 4 n)) (< from (* 4 n)) + (not (equal from to))) + (<= 2 (len (route from to n)))) + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :in-theory (e/d (route) (n_across n_counter_clockwise)) + :do-not '(eliminate-destructors generalize fertilize) + :induct (route from to n)))) + +;------------------------------------------------------------------------ +; 2. Last of route(from,to) is to +;------------------------------------------------------------------------ +(defthm lemma1_last_route_is_to + ;; any route ends with the correct destination + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (< 0 n) (integerp n)) + (equal (car (last (route from to n))) + to)) + :hints (("GOAL" + :in-theory (e/d (route) + (route_=_QUARTER_4_LIST_LEMMA_1 + route_=_QUARTER_1 + PREFER-POSITIVE-ADDENDS-< + PREFER-POSITIVE-ADDENDS-EQUAL))))) + +;;------------------------------------------------------------------------ +;; 3. First of route(from,to) is from +;;------------------------------------------------------------------------ +(defthm lemma2_first_of_route_is_from + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (< 0 n) (integerp n)) + (equal (car (route from to n)) + from)) + :hints (("GOAL" + :in-theory (e/d (route) + (route_=_QUARTER_4_LIST_LEMMA_1 + route_=_QUARTER_1 + PREFER-POSITIVE-ADDENDS-< + PREFER-POSITIVE-ADDENDS-EQUAL))))) + +;;------------------------------------------------------------------------ +;; 4. Every node is less that 4*n +;;------------------------------------------------------------------------ +(defun all_inf_np (l n) + ;; recognizes a list in which every element is less than n + (if (endp l) + t + (and (< (car l) n) + (all_inf_np (cdr l) n)))) + +(defthm lemma3_all_inf_n_route + ;; we prove that each node is less than the number of nodes + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (< 0 n) (integerp n)) + (all_inf_np (route from to n) + (* 4 n))) + :hints (("GOAL" + :in-theory (e/d (route) + (route_=_QUARTER_4_LIST_LEMMA_1 + route_=_QUARTER_1 + PREFER-POSITIVE-ADDENDS-< + PREFER-POSITIVE-ADDENDS-EQUAL))))) + +;;------------------------------------------------------------------------ +;; 5. every node is recognized by OctagonNodeSetp +;;------------------------------------------------------------------------ + +(include-book "../../nodeset/octagon-nodeset") + +;; to prove this we use the strategy that considers +;; the problem quarter by quarter. +;; We first prove that each quarter is OK. + +(defthm OctagonNodeSetp_quarter_1_list + (implies (and (natp from) (natp to)) + (OctagonNodeSetp (quarter_1_list from to)))) + +(defthm OctagonNodeSetp_quarter_minus_4_list + (implies (and (natp from) (natp to) + (integerp n)) + (OctagonNodeSetp (quarter_minus_4_list from to n)))) + +(defthm OctagonNodeSetp_quarter-3-list + (implies (and (natp from) (natp to) + (integerp n) (< 0 n)) + (OctagonNodeSetp (quarter_3_list from to n)))) + +(defthm OctagonNodeSetp_quarter-minus-2-list + (implies (and (natp from) (natp to) (integerp n)) + (OctagonNodeSetp (quarter_minus_2_list from to n)))) + +(defthm OctagonNodeSetp_quarter-minus-1-list + (implies (and (natp from) (natp to)) + (OctagonNodeSetp (quarter_minus_1_list from to)))) + +(defthm OctagonNodeSetp_quarter-minus-3-list + (implies (and (natp from) (natp to) (integerp n) (< 0 n)) + (OctagonNodeSetp (quarter_3_list from to n)))) + +(defthm OctagonNodeSetp_quarter-4-list + (implies (and (natp from) (natp to) (integerp n) (< 0 n)) + (OctagonNodeSetp (quarter_4_list from to n)))) + +(defthm OctagonNodeSetp_quarter-2-list + (implies (and (natp from) (natp to) (integerp n) (< 0 n)) + (OctagonNodeSetp (quarter_2_list from to n)))) + +(defthm lemma5_OctagonNodeSetp_n-go-to-node-top + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (integerp n) (< 0 n)) + (OctagonNodeSetp (route from to n))) + :hints (computed_hint_route)) + +;;------------------------------------------------------------------------ +;; 6. Routing terminates in N steps +;;------------------------------------------------------------------------ + +;; we prove it for every quarter +;; and we first prove what is the exact length of +;; the route for each quarter +;; each lemma is proven in less than 1 second + +(defthm len_quarter_1_list + (implies (and (natp from) + (natp to) + (<= 0 (- to from))) + (equal (len (quarter_1_list from to)) + (+ 1 (+ to (- from)))))) + +(defthm len_quarter_minus_4_list + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (integerp n) + (and (<= (- to from) (* -3 n)) + (< (- (* 4 n)) (- to from)))) + (equal (len (quarter_minus_4_list from to n)) + (+ 1 (* 4 n) to (- from))))) + +;; for some lemma we will need to disable prefer-blah-blah-blah +;; so we do a computed hint, and we want it inherited to children! +;; So, we use the :computed-hint-replacement feature. +(defun computed_hint_prefer_positive_addends (id clause world) + (declare (ignore clause world)) + (if (equal id '((0) NIL . 0)) + '(:computed-hint-replacement t + :in-theory (disable prefer-positive-addends-equal + reduce-integerp-+ + prefer-positive-addends-<)) + nil)) + +(defthm len_quarter_minus_1_list + (implies (and (integerp from) + (integerp to)) + (equal (len (quarter_minus_1_list from to)) + (if (< to from) + (+ 1 from (- to)) + 1))) + :hints (computed_hint_prefer_positive_addends)) + +(defthm len_quarter_minus_3_list + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (integerp n) + (< 0 n) + (and (< (* -3 n) (- to from)) + (< (- to from) (* -2 n)))) + (equal (len (quarter_minus_3_list from to n)) + (+ 1 1 (* -2 n) (- to) from)))) + +(defthm len_quarter_4_list + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (< 0 n) (integerp n) + (and (<= (* 3 n) (- to from)) + (< (- to from) (* 4 n)))) + (equal (len (quarter_4_list from to n)) + (+ 1 (* 4 n) from (- to))))) + +(defthm len_quarter_2_list + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (< 0 n) (integerp n) + (and (< n (- to from)) + (< (- to from) (* 2 n)))) + (equal (len (quarter_2_list from to n)) + (+ 1 1 (* 2 n) from (- to))))) + +;; we prove the exact value of the length of the route, +;; for every possible + + +;; we merge the previous computed hints into one +;;---------------------------------------------- + +(defun merged_computed_hints_1 (id clause world) + (declare (ignore clause world)) + (if (equal id '((0) NIL . 0)) + '(:computed-hint-replacement t ;; to have the theory inherited + :cases ((and (<= (- to from) n) + (<= 0 (- to from))) + (and (<= (- to from) (* -3 n)) + (< (- (* 4 n)) (- to from))) + (and (< (- to from) (* 3 n)) + (< (* 2 n) (- to from))) + (and (< (- to from) (- n)) + (< (* -2 n) (- to from))) + (and (< (- to from) 0) + (<= (- n) (- to from))) + (and (< (* -3 n) (- to from)) + (< (- to from) (* -2 n))) + (and (<= (* 3 n) (- to from)) + (< (- to from) (* 4 n))) + (and (< n (- to from)) + (< (- to from) (* 2 n))) + (equal (+ to (- from)) (* 2 n)) + (equal (+ to (- from)) (* -2 n))) + :in-theory (disable prefer-positive-addends-equal + prefer-positive-addends-<)) + nil)) + + +(defthm len_route_lemma1 + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (< 0 n) (integerp n)) + (equal (len (route from to n)) + (cond ((and (<= (- to from) N) + (<= 0 (- to from))) ;; Q 1 + (+ 1 to (- from))) + ((AND (<= (- TO FROM) (* -3 N)) + (< (- (* 4 N)) (- TO FROM))) ;; Q -4 + (+ 1 (* 4 n) to (- from))) + ((AND (< (- TO FROM) (* 3 N)) + (< (* 2 N) (- TO FROM))) ;; Q 3 + (+ 1 1 (* -2 n) to (- from))) + ((AND (< (- TO FROM) (- N)) + (< (* -2 N) (- TO FROM))) ;; Q -2 + (+ 1 1 (* 2 n) to (- from))) + ((AND (< (- TO FROM) 0) + (<= (- N) (- TO FROM))) ;;Q -1 + (+ 1 from (- to))) + ((AND (< (* -3 N) (- TO FROM)) + (< (- TO FROM) (* -2 N))) ;; Q -3 + (+ 1 1 (* -2 n) (- to) from)) + ((AND (<= (* 3 N) (- TO FROM)) + (< (- TO FROM) (* 4 N))) ;; Q 4 + (+ 1 (* 4 n) from (- to))) + ((AND (< N (- TO FROM)) + (< (- TO FROM) (* 2 N))) ;; Q 2 + (+ 1 1 (* 2 n) from (- to))) + ((EQUAL (+ TO (- FROM)) (* 2 N)) + 2) + ((EQUAL (+ TO (- FROM)) (* -2 N)) + 2) + (t 0)))) + :otf-flg t + :hints (merged_computed_hints_1 + ("Subgoal 5" + :in-theory (disable quarter_minus_3_list)) + ("Subgoal 3" + :in-theory (disable quarter_2_list)))) + +;;----------------------------------------------------------- +;; Now we can consider we have enough properties on route +;; So, we disable all the rules that map route to lists + +(in-theory (disable ROUTE_=_QUARTER_1 + ROUTE_=_QUARTER_2_LIST + ROUTE_=_QUARTER_3 + ROUTE_=_QUARTER_4_LIST + ROUTE_=_QUARTER_MINUS_1_LIST + ROUTE_=_QUARTER_MINUS_2_LIST + ROUTE_=_QUARTER_MINUS_3_LIST + ROUTE_=_QUARTER_MINUS_4_LIST + ROUTE_=_BOUNDS)) +;;------------------------------------------------------------ + +;; For the last theorem we want is that the length is +;; less than 1+N + +(defthm bound_route_lemma + (implies (and (integerp from) + (<= 0 from) + (< from (* 4 n)) + (integerp to) + (<= 0 to) + (< to (* 4 n)) + (integerp n) + (< 0 n)) + (< (len (route from to n)) + (+ 1 1 n))) + :hints (merged_computed_hints_1) + :rule-classes :linear) + +;; This rule is fine to export but does not state the theorem we want. +;; The final directly follows but is not stored as a rule + +;; Moreover we need to disable the rule LEN_ROUTE_LEMMA1, because +;; it will remove (len ...) and the rule above will never be applied. + +(in-theory (disable LEN_ROUTE_LEMMA1)) + +(defthm bound_route-main + (implies (and (integerp from) + (<= 0 from) + (< from (* 4 n)) + (integerp to) + (<= 0 to) + (< to (* 4 n)) + (integerp n) + (< 0 n)) + (<= (len (route from to n)) + (+ 1 N))) + :rule-classes nil) + diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_main.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_main.lisp new file mode 100644 index 0000000..9c27b61 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_main.lisp @@ -0,0 +1,201 @@ +;; File: routing_main.lisp +;; Proof of the main theorem of Route +;; August 15th 2005 +;; proof of compliance with GeNoC +(in-package "ACL2") + +;; we import the definition of route and lemmas that prove its +;; correctness +(include-book "routing_local_lemmas") + +;; 1. Correction of function Route +;; ------------------------------ + +;; we group the main properties of Route in one theorem + +(local + (defthm consp_len_>_0 + (implies (consp x) + (< 0 (len x))))) + +(defthm CORRECTNESS_OF_ROUTE + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (not (equal from to)) + (< 0 n) (integerp n)) + (and ;; Route contains at least two nodes + (<= 2 (len (route from to n))) + ;; it is a consp + (consp (route from to n)) + ;; every node is an integer + (OctagonNodeSetp (route from to n)) + ;; every node is less than the maximum of nodes + (all_inf_np (route from to n) (* 4 n)) + ;; the first node is the starting node + (equal (car (route from to n)) from) + ;; the last node is the final node + (equal (car (last (route from to n))) to)))) + + +;; we load the book about the generic routing +;; it also imports the types and misc. of GeNoC +(include-book "../../../generic-modules/GeNoC-routing") + +;; 2. Definition of OctagonRouting +;; ------------------------------- +(defun octagon-routing (Missives Bound) + (if (endp Missives) + nil + (let* ((miss (car Missives)) + (Id (IdM miss)) + (frm (FrmM miss)) + (origin (OrgM miss)) + (destination (DestM miss))) + (cons (list Id frm (list + (route origin destination + (/ Bound 4)))) + (octagon-routing (cdr Missives) Bound))))) + +;; 3. Matching the hyps +;; -------------------- +;; in order to use the theorem CORRECTNESS_OF_ROUTE +;; we need to go from GeNoC hyps to the Octagon hyps +(defthm member-of-naturals-hyp + (implies (and (member-equal e (naturals N)) + (natp N)) + (and (natp e) (< e (+ 1 N))))) + + +(defthm len-naturalsp + (implies (natp N) + (equal (len (naturals N)) (+ 1 N)))) + + +(defthm V-ids-M-ids-octagon-routing + ;; this is the same lemma as for the witness + (equal (V-ids (octagon-routing Missives NodeSet)) + (M-ids Missives))) + + +(defthm len->=-2-=>-consp-cdr + (implies (<= 2 (len x)) + (consp (cdr x)))) + +;; the next theorem does not go through ... but should !! +;; check what's wrong ... + +(defthm trlstp-octagon-routing + ;; octagon-routing returns a TrLstp + ;; the hints are very ugly. + ;; They are all the same, but the proof does not go through + ;; if I put the :use at the goal Subgoal *1/2. + (let ((NodeSet (OctagonNodeSetGenerator Bound))) + (implies (and (Missivesp M NodeSet) +; (equal NodeSet (Octagonnodesetgenerator Bound)) + (OctagonValidParamsp Bound)) + (TrLstp (octagon-routing M (* 4 bound))))) + :otf-flg t + :hints (("GOAL" + :induct (octagon-routing M (len (OctagonNodeSetGenerator Bound))) + :do-not-induct t + :in-theory (disable len)) + ("Subgoal *1/2.2" + :use ((:instance member-of-naturals-hyp + (e (cadar M)) + (N (+ -1 (* 4 Bound)))) + (:instance member-of-naturals-hyp + (e (cadddr (car M))) + (N (+ -1 (* 4 Bound))))) + :in-theory (disable member-of-naturals-hyp)) + ("Subgoal *1/2.1" + :use ((:instance member-of-naturals-hyp + (e (cadar M)) + (N (+ -1 (* 4 Bound)))) + (:instance member-of-naturals-hyp + (e (cadddr (car M))) + (N (+ -1 (* 4 Bound))))) + :in-theory (disable member-of-naturals-hyp)))) + + +(defthm naturals_member + (implies (and (<= a b) (natp a) (natp b)) + (member-equal a (naturals b)))) + +(defthm naturals_subset_all_inf + (implies (and (all_inf_np L n1) + (natp n1) (OctagonNodeSetp L)) + (subsetp L (naturals (1- n1))))) + +(defthm subsetp-route-valid-nodes + (implies (and (natp from) (< from (* 4 n)) + (natp to) (< to (* 4 n)) + (not (equal from to)) + (integerp n) (< 0 n)) + (let ((route (route from to n))) + (subsetp route (naturals (1- (* 4 n))))))) + +(defthm CorrectRoutesp-Octagon-Routing + (let ((NodeSet (Naturals (+ -1 (* 4 N))))) + (implies (and (Missivesp M NodeSet) +; (equal NodeSet (Naturals (+ -1 (* 4 N)))) + (OctagonValidParamsp N)) + (CorrectRoutesp (octagon-routing M (* 4 n)) + M NodeSet))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize fertilize) + :induct (true-listp M) + :do-not-induct t) + ("Subgoal *1/1" + :use ((:instance member-of-naturals-hyp + (N (+ -1 (* 4 N))) + (e (nth 1 (car M)))) + (:instance member-of-naturals-hyp + (N (+ -1 (* 4 N))) + (e (nth 3 (car M))))) + :in-theory (disable member-of-naturals-hyp)))) + +(defthm ToMissives-octagon-routing + (let ((NodeSet (Naturals (+ -1 (* 4 N))))) + (implies (and (Missivesp M NodeSet) + (OctagonValidParamsp N)) +; (equal NodeSet (Naturals (+ -1 (* 4 N))))) + (equal (ToMissives (octagon-routing M + (* 4 N))) + M))) + :otf-flg t + :hints (("GOAL" + :do-not '(eliminate-destructors generalize fertilize) + :induct (true-listp M) +; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.] +; :in-theory (disable no-duplicatesp->no-duplicatesp-equal) + :do-not-induct t) + ("Subgoal *1/1" + :use ((:instance member-of-naturals-hyp + (N (+ -1 (* 4 N))) + (e (nth 1 (car M)))) + (:instance member-of-naturals-hyp + (N (+ -1 (* 4 N))) + (e (nth 3 (car M))))) + :in-theory (disable member-of-naturals-hyp)))) + + +(defun OctagonRouting (M NodeSet) + ;; definition that is conform to GeNoC-routing + (octagon-routing M (len NodeSet))) + +(defthm check-octagonrouting-compliance + t + :rule-classes nil + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use (:instance + (:functional-instance + trlstp-routing + (NodeSetGenerator OctagonNodeSetGenerator) + (NodeSetp OctagonNodeSetp) + (ValidParamsp OctagonValidParamsp) + (routing OctagonRouting))) + :in-theory (disable trlstp-routing + trlstp missivesp)))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/xy-routing/xy-routing.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/xy-routing/xy-routing.lisp new file mode 100644 index 0000000..59503a4 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/xy-routing/xy-routing.lisp @@ -0,0 +1,527 @@ +;; Julien Schmaltz +;; August 1st 2005 +;; File: xy-routing.lisp +;; Application of GeNoC-routing to an XY-routing algorithm + +(in-package "ACL2") +;; we import the generic definition +(include-book "../../../generic-modules/GeNoC-routing") +;; we import the book with node definition for a 2D-mesh +(include-book "../../nodeset/2D-mesh-nodeset") + +;; we load the arithmetic books +(include-book "arithmetic-3/bind-free/top" :dir :system) + +;(set-non-linearp t) +(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system) + +;;------------------------------------------------------------------------ +;; +;; Definition of the Routing Algorithm +;; +;;------------------------------------------------------------------------ +;; ALGORITHM +;; from = (x_o y_o) +;; dest = (x_d y_d) +;; if x_o = x_d and y_o = y_d +;; then we stop +;; else +;; if x_o /= x_d then +;; if x_d < x_o then we go one step west +;; else we go one step east +;; endif +;; else +;; if y_d < y_o then we go one step south +;; else we go one step north +;; endif +;; endif +;; endif + + +;; 1 Measure +;; ------------ +;; measure = | x_d - x_o | + | y_d - y_o | +;; The measure is just the sum of the absolute value of the difference of the +;; coordinates. We force the result to be a natural. + + +(defun dist (s d) + (if (or (not (coordinatep s)) (not (coordinatep d))) + 0 + (let ((s_x (car s)) + (s_y (cadr s)) + (d_x (car d)) + (d_y (cadr d))) + (+ (abs (- d_x s_x)) (abs (- d_y s_y)))))) + +(defthm O-P-dist + ;; the measure must be an ordinal + (O-P (dist from to))) + +;; 2 Routing function +;; --------------------- +;; we define here the basic routing function +(defun xy-routing (from to) + (declare (xargs :measure (dist from to))) + ;; from = (x_o y_o) dest = (x_d y_d) + (if (or (not (coordinatep from)) + (not (coordinatep to))) + nil + (let ((x_d (car to)) + (y_d (cadr to)) + (x_o (car from)) + (y_o (cadr from))) + (if (and (equal x_d x_o) ;; x_d = x_o + (equal y_d y_o)) ;; y_d = y_o + ;; if the destination is equal to the current node, we stop + (cons from nil) + (if (not (equal x_d x_o)) ;; x_d /= x_o + (if (< x_d x_o) + ;; the x-destination is on the descending x + (cons from (xy-routing (list (- x_o 1) y_o) to)) + ;; x_d > x_o + (cons from (xy-routing (list (+ x_o 1) y_o) to))) + ;; otherwise we test the y-direction + ;; y_d /= y_o + ;; x_d = x_o + (if (< y_d y_o) + (cons from (xy-routing (list x_o (- y_o 1)) to)) + ;; y_d > y_o + (cons from (xy-routing (list x_o (+ y_o 1)) to)))))))) + +;; 3 Validation of the basic routing function +;; ------------------------------------------- +;; we prove first some lemmas on the basic function + +;; 3.a some trivial properties +(defthm first-XY-routing + ;; the first element is the origin + (implies (and (coordinatep from) + (coordinatep to)) + (equal (car (XY-routing from to)) + from))) + +(defthm last-XY-routing + ;; the last element is the destination + (implies (and (coordinatep from) + (coordinatep to)) + (equal (car (last (XY-routing from to))) + to))) + +(defthm XY-routing-len->=-2 + ;; a route has at least two elements + (implies (and (coordinatep from) (coordinatep to) + (not (equal from to))) + (<= 2 (len (xy-routing from to))))) + + +;; 3.b A route is a subset of nodeset + +;; now we prove that a route is a subsetp of the set of existing nodes +;; NodeSet + +;; the tactic is the following: +;; a/ we prove that a list of valid coordinates with every x less than +;; x-dim and every y less than y-dim is a subset of coord-gen(x-dim, y-dim) +;; b/ we prove that routing satisfies the above properties + +(defun all-x-<-max (L x-max) + ;; we define a function that checks that every x-coordinate is less than x-max + (if (endp L) + t + (and (< (caar L) x-max) ;; x_i < x-max + (all-x-<-max (cdr L) x-max)))) + +(defun all-y-<-max (L y-max) + ;; we define a function that checks that every y-coordinate is less than y-max + (if (endp L) + t + (and (< (cadar L) y-max) ;; y_i < y-max + (all-y-<-max (cdr L) y-max)))) + +(defthm member-equal-x-dim-gen + ;; we prove that if x is a coordinate with its first part less than x-dim + ;; and its second part equal to y-dim then x is a member of x-dim-gen. + (implies (and (coordinatep x) (< (car x) x-dim) + (natp x-dim) + (natp y-dim) + (equal (cadr x) y-dim)) + (member-equal x (x-dim-gen x-dim y-dim)))) + +(defthm member-coord-generator-1 + ;; we prove something similar for the function coord-generator-1 + ;; both parts of x are less than x-dim and y-dim implies that x + ;; is a member of coord-generator-1 + (implies (and (coordinatep x) (natp y-dim) + (natp x-dim) + (< (car x) x-dim) (< (cadr x) y-dim)) + (member-equal x (coord-generator-1 x-dim y-dim)))) + +(defthm tactic1 + ;; we prove that our tactic is valid for membership + (implies (and (2D-mesh-nodesetp L) (consp L) + (all-x-<-max L x-dim) (natp x-dim) + (all-y-<-max L y-dim) (natp y-dim)) + (member-equal (car L) (coord-generator-1 x-dim y-dim)))) + +(defthm member-equal-rev + ;; this should go elsewhere + (implies (member-equal x S) + (member-equal x (rev S)))) + +(defthm tactic1-top + ;; we now prove that our tactic is valid + (implies (and (2D-mesh-nodesetp L) + (all-x-<-max L x-dim) (natp x-dim) + (all-y-<-max L y-dim) (natp y-dim)) + (subsetp L (coord-gen x-dim y-dim))) + :hints (("GOAL" + :in-theory (enable coord-gen)))) + +;; Then the strategy is to prove that xy-routing satisfies +;; the hypotheses of this theorem + +(defthm 2D-mesh-nodesetp-xy-routing + ;; 1st hyp is trivial + ;; a route is a list of valid coordinates + (2D-mesh-nodesetp (xy-routing from to))) + +;; let's go to the more tricky part. +;; First, every x-coord of any nodes produced by function xy-routing +;; is strictly less than 1 + Max(from_x, to_x) +(defthm all-x-<-max-+ + ;; lemma added for compability between 3.1 and 3.2.1 + (implies (all-x-<-max x y) + (all-x-<-max x (+ 1 y)))) + +(defthm routing-all-x-less + (all-x-<-max (xy-routing from to) + (1+ (max (car from) (car to))))) + +;; and every y-coord is strictly less than 1 + Max(from_y, to_y) +(defthm routing-all-y-less + (all-y-<-max (xy-routing from to) + (1+ (max (cadr from) (cadr to))))) + +(defthm xy-routing-subsetp-coord-max + (implies (and (coordinatep from) (coordinatep to)) + (subsetp (xy-routing from to) + (coord-gen (1+ (max (car from) (car to))) + (1+ (max (cadr from) (cadr to)))))) + :hints (("GOAL" + :in-theory (disable max)))) + + +;; then our goal is to prove that coor-gen(NX,NY) produces nodes +;; with x-coord < NX and y-coord < NY + +(defthm all-x-<-max-minus-1 + ;; lemma needed to be able to enlarge the majoration + (implies (all-x-<-max L (1- x)) + (all-x-<-max L x))) + +(defthm all-x-<-max-x-dim-gen + ;; we prove that x-dim-gen generates nodes with x-coord < x + (all-x-<-max (x-dim-gen x y) x)) + +(defthm all-x-<-max-coord-gen + ;; we propagate this property to coord-generator-1 which calls x-dim-gen + (all-x-<-max (coord-generator-1 x y) x)) + +(defthm all-x-<-max-member-equal + (implies (and (all-x-<-max L x) + (member-equal y L)) + (< (car y) x))) + +(defthm all-x-<-max-rev + ;; all-x-<-max is preserved if we reverse its arguments + (implies (all-x-<-max L x) + (all-x-<-max (rev L) x))) + +(defthm all-y-<-max-x-dim-gen + (all-y-<-max (x-dim-gen x y) (+ 1 y))) + +(defthm all-y-<-max-minus-1 + (implies (all-y-<-max L (+ -1 x)) + (all-y-<-max L x))) + +(defthm all-y-<-max-append + (implies (and (all-y-<-max L1 x) + (all-y-<-max L2 x)) + (all-y-<-max (append L1 L2) x))) + +(defthm all-y-<-max-coord-gen-1 + (all-y-<-max (coord-generator-1 x y) y) + :hints (("SubGoal *1/2" + :cases ((all-y-<-max (x-dim-gen x (+ -1 y)) y))) + ("SubGoal *1/2.2" + :use (:instance all-y-<-max-x-dim-gen (y (+ -1 y))) + :in-theory (disable all-y-<-max-x-dim-gen)))) + +(defthm rev-append + ;; should be put elsewhere + (equal (rev (append x y)) + (append (rev y) (rev x)))) + +(defthm all-y-<-max-rev + (implies (all-y-<-max L x) + (all-y-<-max (rev L) x))) + +(defthm all-max-coord-gen + (and (all-x-<-max (coord-gen X Y) X) + (all-y-<-max (coord-gen X Y) Y)) + :hints (("GOAL" + :in-theory (enable coord-gen)))) + +;; now we prove that if (x1 y1) and (x2 y2) belong to (coord-gen NX NY) +;; then Max(x1, x2) < NX and Max(y1, y2) < NY + +(defthm member-equal-x-dim-gen-plus + (implies (and (<= x1 x2) (natp x1) (< 0 x1) (natp x2)) + (member-equal (list (+ -1 x1) y) + (x-dim-gen x2 y)))) + +(defthm subsetp-x-dim-gen-plus + (implies (and (natp x1) (natp x2) (<= x1 x2)) + (subsetp (x-dim-gen x1 y) + (x-dim-gen x2 y)))) + +(defthm subsetp-append-2 + ;; should be put elsewhere + (implies (and (subsetp x L) + (subsetp y L)) + (subsetp (append x y) L))) + +(defthm all-y-<-max-member-equal + (implies (and (all-y-<-max L y) + (member-equal e L)) + (< (cadr e) y))) + +(defthm all-max-member-equal + (implies (and (member-equal x L) + (all-x-<-max L x-max) + (all-y-<-max L y-max) + (member-equal y L)) + (and (< (max (car x) (car y)) x-max) + (< (max (cadr x) (cadr y)) y-max)))) + +;; then we prove that if x < NX and y < NY then +;; (coord-gen x y) is a subset of (coord-gen NX NY) + +(defthm subsetp-x-dim-gen-coord-gen-1 + (implies (and (natp x1) (natp x2) (natp y1) (natp y2) + (<= x1 x2) (< y1 y2)) + (subsetp (x-dim-gen x1 y1) + (coord-generator-1 x2 y2)))) + +(defthm subsetp-coord-gen-1 + (implies (and (<= x1 x2) (<= y1 y2) + (natp x1) (natp x2) (natp y1) (natp y2)) + (subsetp (coord-generator-1 x1 y1) + (coord-generator-1 x2 y2)))) + +(defthm subsetp-rev-2 + ;; should go elsewhere + (implies (subsetp x y) + (subsetp (rev x) (rev y)))) + +;; here comes our main lemma: +(defthm subsetp-coord-plus + (implies (and (<= x1 x2) (<= y1 y2) + (natp x1) (natp x2) (natp y1) (natp y2)) + (subsetp (coord-gen x1 y1) + (coord-gen x2 y2))) + :hints (("GOAL" + :in-theory (enable coord-gen)))) + +;; and now using the transitivity of subsetp we conclude: +(defthm trans-subsetp + ;; should be put elsewhere + (implies (and (subsetp x y) (subsetp y z)) + (subsetp x z))) + + +(defthm xy-routing-subsetp-nodeset + ;; now we want to prove that if NodeSet = coord-gen x y, then + ;; route is a subsetp of NodeSet. + ;; from and to must be members of NodeSet + ;; from and to must not be equal + (implies (and (not (equal from to)) + (coordinatep from) (coordinatep to) + (natp X) (natp Y) + ;; it should be member-equal + (member-equal from (coord-gen X Y)) + (member-equal to (coord-gen X Y))) + (subsetp (xy-routing from to) (coord-gen X Y))) + :otf-flg t + :hints (("GOAL" + :use ((:instance all-max-member-equal + (L (coord-gen X Y)) + (x from) (y to) + (x-max X) (y-max Y)) + (:instance xy-routing-subsetp-coord-max)) + :do-not '(eliminate-destructors generalize fertilize) + :in-theory (disable coord-gen coordinatep natp subsetp + all-max-member-equal + xy-routing-subsetp-coord-max) + :do-not-induct t) + ("Subgoal 4" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car from))) (x2 x) + (y1 (+ 1 (cadr from))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)) + ("Subgoal 3" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car from))) (x2 x) + (y1 (+ 1 (cadr to))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)) + ("Subgoal 2" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car to))) (x2 x) + (y1 (+ 1 (cadr from))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)) + ("Subgoal 1" + :use (:instance subsetp-coord-plus + (x1 (+ 1 (car to))) (x2 x) + (y1 (+ 1 (cadr to))) (y2 y)) + :in-theory (disable subsetp-coord-plus + coord-gen subsetp)))) + + + +;; 4 Definition compatible with GeNoC +;; ----------------------------------- + +;; 4.a Definition of the function +(defun xy-routing-top (Missives) + (if (endp Missives) + nil + (let* ((miss (car Missives)) + (from (OrgM miss)) + (to (DestM miss)) + (id (IdM miss)) + (frm (FrmM miss))) + (cons (list id frm (list (xy-routing from to))) + (xy-routing-top (cdr Missives)))))) + +(defun XYRouting (Missives NodeSet) + (declare (ignore NodeSet)) + (xy-routing-top Missives)) + +;; 4.b Proof of compliance +;; ------------------------ + +;(defun bind-to-itself (x) +; (list (cons x x))) + +;; need to prove CorrectRoutesp and TrLstp and ToMissives +;; 1. ToMissives seems to be simple +(defthm 2D-mesh-nodesetp-member-equal + (implies (and ;(bind-free (bind-to-itself x)) + ;; ask matt why it does not work + (2D-mesh-nodesetp x) + (member-equal e x)) + (Coordinatep e))) + +(defthm XYRouting-Missives + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (Missivesp Missives NodeSet) + (mesh-hyps Params)) + (equal (ToMissives (xy-routing-top Missives)) + Missives))) + :otf-flg t + :hints (("GOAL" + :induct (xy-routing-top Missives) + :do-not '(eliminate-destructors generalize) + :in-theory (disable coordinatep) + :do-not-induct t) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + +;; 2. TrLstp +(defthm consp-xy-routing + ;; should be systematically added + (implies (and (coordinatep from) + (coordinatep to)) + (consp (xy-routing from to)))) + +(defthm consp-xy-routing-cdr + ;; should be systematically added + (implies (and (coordinatep from) (not (equal from to)) + (coordinatep to)) + (consp (cdr (xy-routing from to))))) + +(defthm V-ids-xy-routing-=-M-ids + ;; this one too ... + (equal (V-ids (xy-routing-top Missives)) + (M-ids Missives))) + +(defthm TrLstp-XYRouting + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (Missivesp Missives NodeSet) + (mesh-hyps Params)) +; (equal NodeSet (mesh-nodeset-gen Params))) + (TrLstp (xy-routing-top Missives)))) + :hints (("GOAL" + :induct (xy-routing-top missives)) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + +;; 3. CorrectRoutesp +(defthm CorrectRoutesp-XYRouting + (let ((NodeSet (mesh-nodeset-gen Params))) + (implies (and (mesh-hyps Params) + (Missivesp Missives NodeSet)) + (CorrectRoutesp (xy-routing-top Missives) + Missives NodeSet))) + :hints (("GOAL" + :induct (xy-routing-top Missives) + :do-not-induct t) + ("Subgoal *1/2" + :use ((:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (OrgM (car Missives)))) + (:instance 2D-mesh-nodesetp-member-equal + (x (mesh-nodeset-gen Params)) + (e (DestM (car Missives))))) + :in-theory (disable 2D-mesh-nodesetp-member-equal + coordinatep)))) + + +;; now we can prove that the XY-routing algorithm is compliant +;; to the GeNoC-routing. +(defthm check-compliance-XY-routing + t + :rule-classes nil + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use (:functional-instance + ToMissives-Routing + (NodeSetGenerator mesh-nodeset-gen) + (NodeSetp 2D-mesh-nodesetp) + (ValidParamsp mesh-hyps) + (Routing XYRouting)) + :in-theory (disable ToMissives-Routing + mesh-nodeset-gen + trlstp mesh-hyps + Missivesp)) + ("Subgoal 3" ; changed after v4-3 from "Subgoal 4", for tau system + :in-theory (enable mesh-hyps)))) diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/circuit-scheduling.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/circuit-scheduling.lisp new file mode 100644 index 0000000..407cfdf --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/circuit-scheduling.lisp @@ -0,0 +1,358 @@ +;; Julien Schmaltz +;; File: circuit-scheduling.lisp +;; here we define a function that realises a circuit switching +;; technique, we prove it correct and we prove that it is a valid +;; instance of the scheduling function of GeNoC. +;; Revised: Nov 13th 2005, JS + + +(in-package "ACL2") +(include-book "../../generic-modules/GeNoC-scheduling") +(include-book "intersect") + +;;----------------------------------------------------- +;; +;; DEFINITION OF THE CIRCUIT SWITCHED SCHEDULING POLICY +;; +;;----------------------------------------------------- + +(defun rev (x) + ;; put this definition in a book !! + (if (endp x) + nil + (append (rev (cdr x)) (list (car x))))) + +(defun consume-attempts (AttLst) + ;; any node that has a attempt, consumes one + (if (zp (SumOfAttempts AttLst)) + AttLst + (let* ((top (car AttLst)) + (node (car top)) + (att (cadr top))) + (if (zp att) + (cons top + (consume-attempts (cdr AttLst))) + (cons (list node (1- att)) + (consume-attempts (cdr AttLst))))))) + +(defun test_prev_routes (routes prev) + ;; function that returns a route that uses nodes + ;; that are not in prev or returns nil if there is no + ;; such route. + (if (endp routes) + nil + (let ((r (car routes))) + (if (no_intersectp r prev) + r + (test_prev_routes (cdr routes) prev))))) + +(defun update_route (tr route) + ;; updates the route of tr to be a list containing + ;; only route + (list (IdV tr) (FrmV tr) (list route))) + +(defun ct-scheduler (TrLst Scheduled Delayed prev) + (if (endp TrLst) + (mv (rev scheduled) (rev delayed)) + (let* ((tr (car TrLst)) + (routes (RoutesV tr)) + (r? (test_prev_routes routes prev))) + (if r? + ;; if there is a good route in routes + ;; we update prev and schedule the transaction + (ct-scheduler (cdr TrLst) + (cons (update_route tr r?) Scheduled) + Delayed (append r? prev)) + ;; otherwise the transaction is delayed + (ct-scheduler (cdr TrLst) scheduled + (cons tr Delayed) prev))))) + +(defun circuit-scheduling (TrLst att) + ;; definition compatible with GeNoC-scheduling + (if (zp (SumOfAttempts att)) + ;; nothing is scheduled if there is no attempt left + ;; so everything is delayed + (mv nil TrLst att) + ;; otherwise we call ct-scheduler and consume attempts + (mv-let (scheduled delayed) + (ct-scheduler TrLst nil nil nil) + (mv Scheduled Delayed (consume-attempts att))))) + +(defun ct-sched-nt-sched (TrLst prev) + ;; to simplify proofs we define a non-tail version of + ;; ct-scheduler that computes the scheduled transactions + (if (endp TrLst) + nil + (let* ((tr (car TrLst)) + (routes (RoutesV tr)) + (r? (test_prev_routes routes prev))) + (if r? + (cons (update_route tr r?) + (ct-sched-nt-sched (cdr TrLst) + (append r? prev))) + (ct-sched-nt-sched (cdr TrLst) prev))))) + +(defthm scheduler-=-non-tail-scheduled + ;; we prove that our non-tail definition is correct + (equal (car (ct-scheduler TrLst scheduled delayed prev)) + (append (rev scheduled) + (ct-sched-nt-sched TrLst prev)))) + +(defun ct-sched-nt-del (TrLst prev) + ;; we proceed similarly for the delayed transfers + (if (endp TrLst) + nil + (let* ((tr (car TrLst)) + (routes (RoutesV tr)) + (r? (test_prev_routes routes prev))) + (if r? + (ct-sched-nt-del (cdr TrLst) + (append r? prev)) + (cons tr + (ct-sched-nt-del (cdr TrLst) prev)))))) + +(defthm scheduler-=-non-tail-delayed + (equal (mv-nth 1 (ct-scheduler TrLst scheduled delayed prev)) + (append (rev delayed) + (ct-sched-nt-del TrLst prev)))) +;;----------------------------------------------------------------- + +;;------------------------------------------------------------------------- +;; +;; Compliance with GeNoC SCHEDULING +;; +;;------------------------------------------------------------------------- + +;; 1/ consume at least one attempt to ensure termination +;; ----------------------------------------------------- + (defthm consume-at-least-one-attempt-circuit-scheduling + ;; the scheduling policy should consume at least one attempt + ;; this is a sufficient condition to prove that + ;; the full network function terminates + (mv-let (Scheduled Delayed newAtt) + (circuit-scheduling TrLst att) + (declare (ignore Scheduled Delayed)) + (implies (not (zp (SumOfAttempts att))) + (< (SumOfAttempts newAtt) + (SumOfAttempts att))))) +;;---------------------------------------------------------- + +;; 2/ we prove that the ids of the delayed and scheduled travels +;; are part of the initial travel list +;; ----------------------------------- +(defthm subsetp-scheduled-ct + (implies (TrLstp TrLst) + (subsetp (V-ids (ct-sched-nt-sched TrLst prev)) + (V-ids TrLst)))) + +(defthm subsetp-delayed-ct + (implies (TrLstp TrLst) + (subsetp (V-ids (ct-sched-nt-del TrLst prev)) + (V-ids TrLst)))) +;------------------------------------------------------------------ + +;; 3/ we prove that the list of scheduled travels is a +;; valid travel list +;; -------------------------------------------------- + + +(defthm validfield-route-test_prev_routes + (let ((r? (test_prev_routes routes prev))) + (implies (and (validfield-route routes) + r?) + (and (consp r?) (consp (cdr r?)))))) + + +;; proof for the scheduled travels +;; ------------------------------- +(local + (defthm validfields-trlst-ct-sched + (implies (ValidFields-TrLst TrLst) + (ValidFields-TrLst + (ct-sched-nt-sched TrLst prev))))) + +(local + (defthm not-member-V-ids-ct-sched + (implies (not (member-equal e (V-ids TrLst))) + (not + (member-equal + e + (V-ids + (ct-sched-nt-sched TrLst prev))))))) + +(local (defthm no-duplicatesp-ct-sched + (implies (no-duplicatesp-equal (V-ids TrLst)) + (no-duplicatesp-equal + (V-ids (ct-sched-nt-sched TrLst prev)))))) + +(defthm cons-v-ids + (equal (consp (v-ids TrLst)) + (consp TrLst))) + +(defthm TrLstp-scheduled-ct + (implies (TrLstp TrLst) + (TrLstp (ct-sched-nt-sched TrLst prev)))) + +;; proof for the delayed travels +;; ----------------------------- +(local + (defthm validfields-trlst-ct-del + (implies (ValidFields-TrLst TrLst) + (ValidFields-TrLst + (ct-sched-nt-del TrLst prev))))) + +(local + (defthm not-member-V-ids-ct-del + (implies (not (member-equal e (V-ids TrLst))) + (not + (member-equal + e + (V-ids + (ct-sched-nt-del TrLst prev))))))) + +(local (defthm no-duplicatesp-ct-del + (implies (no-duplicatesp-equal (V-ids TrLst)) + (no-duplicatesp-equal + (V-ids (ct-sched-nt-del TrLst prev)))))) + +(defthm TrLstp-delayed-ct + (implies (TrLstp TrLst) + (TrLstp (ct-sched-nt-del TrLst prev)))) +;;-------------------------------------------------------------------- + +;; 4/ correctness of the scheduled travels +;; ------------------------------------------------------ + +(defthm extract-sublst-cons + (implies (not (member-equal id Ids)) + (equal (extract-sublst (cons (list id frm routes) L) + Ids) + (extract-sublst L Ids)))) + +(defthm test_prev_routes-member-equal + (let ((r? (test_prev_routes routes prev))) + (implies r? + (member-equal r? routes)))) + +(defthm ct-scheduled-correctness + (let ((Scheduled (ct-sched-nt-sched TrLst prev))) + (implies (TrLstp TrLst) + (s/d-travel-correctness + scheduled + (extract-sublst TrLst (V-ids Scheduled)))))) + +;; 5/ We prove that Delayed is equal to filtering TrLst +;; according to the ids of Delayed +;; ---------------------------------------------------- +(defthm ct-delayed-correctness + (let ((delayed (ct-sched-nt-del TrLst prev))) + (implies (TrLstp TrLst) + (equal delayed + (extract-sublst TrLst (V-ids delayed))))) + :rule-classes nil) + +; ----------------------------------------------------------- + +;; 6/ we prove that the ids of the delayed travels are distinct +;; from those of the scheduled travels +;; ------------------------------------------------------------ + +(defthm not-in-cons + ;; same lemma as in the packet scheduling + (implies (and (not-in x y) (not (member-equal e x))) + (not-in x (cons e y)))) + +(defthm not-in-v-ids-ct + (implies (TrLstp trlst) + (not-in (v-ids (ct-sched-nt-del trlst prev)) + (v-ids (ct-sched-nt-sched trlst prev))))) + + +;; Finally, we check that our circuit scheduling function +;; is a valid instance of GeNoC-scheduling +;; ------------------------------------------------------ +(defthm check-compliance-circuit-scheduling + t + :rule-classes nil + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use + ((:functional-instance + consume-at-least-one-attempt + (scheduling circuit-scheduling))) + :in-theory (disable consume-at-least-one-attempt + missivesp)) + ("Subgoal 6" + :use (:instance ct-delayed-correctness + (prev nil))) + ("Subgoal 3" + :in-theory (disable circuit-scheduling)))) + +;;----------------------------------------------------------------- +;; +;; Validation of function circuit-scheduling +;; +;;----------------------------------------------------------------- + +(defun all_no_intersectp (route TrLst) + ;; return t if route has an empty intersection with every + ;; route of TrLst. + (if (endp TrLst) + t + (let* ((tr (car TrLst)) + (r (RoutesV tr))) + (and (no_intersectp route (car r)) + (all_no_intersectp route (cdr TrLst)))))) + +(defun FullNoIntersectp (TrLst) + ;; this function checks that every route in TrLst + ;; has at least one attempt left and it has an empty + ;; intersection with every following route. + ;; This defines the correctness of the circuit scheduling + ;; policy. + ;; JS Nov 13th. Checking that every node of a route has at least + ;; one attempt is stupid ! + (if (or (endp TrLst) (endp (cdr TrLst))) + t + (let* ((tr (car TrLst)) + (r (RoutesV tr))) + (and (all_no_intersectp (car r) (cdr TrLst)) +; (check_attempt (car r) att) + (FullNoIntersectp (cdr TrLst)))))) + +(defthm test_prev_routes-check-no_intersectp + (let ((r? (test_prev_routes routes prev))) + (implies r? +; (and (check_attempt r? att) + (no_intersectp prev r?)))) + + +(defthm all_no_intersectp-append + (implies (all_no_intersectp (append l1 l2) l) + (and (all_no_intersectp l1 l) + (all_no_intersectp l2 l)))) + +(defthm FullNoIntersectp-All_no_intersectp + (implies (FullNoIntersectp (ct-sched-nt-sched l prev)) + (all_no_intersectp prev + (ct-sched-nt-sched l prev)))) + +(defthm FullNoIntersectp-ct-scheduler + (implies (TrLstp TrLst) + (FullNoIntersectp (ct-sched-nt-sched TrLst prev))) + :hints (("Subgoal *1/5" + :use + (:instance + FullNoIntersectp-All_no_intersectp + (l (cdr TrLst)) + (prev (append (test_prev_routes (nth 2 (car trlst)) + prev) + prev))) + :in-theory (disable FullNoIntersectp-All_no_intersectp)))) + +;;----------------------------------------------------------------- +;; end of circuit scheduling +;;----------------------------------------------------------------- + + diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/intersect.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/intersect.lisp new file mode 100644 index 0000000..e99b7ed --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/intersect.lisp @@ -0,0 +1,129 @@ +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- +;; +;; +;; Functional Specification and Validation of the Octagon Network on +;; Chip using the ACL2 Theorem Prover +;; +;; +;; Proof Script +;; +;; +;; Julien Schmaltz +;; Joseph Fourier University +;; 46, av. Felix Viallet 38031 Grenoble Cedex +;; FRANCE +;; Julien.Schmaltz@imag.fr +;; +;;------------------------------------------------------------------------- +;;------------------------------------------------------------------------- +;; we reuse the book developed for the study of the +;; Octagon and presented at the ACL2 workshop 2004 + +;; File: intersect.lisp +;; Contains definitions and lemmas about the intersection of routes +;; Link this concept to other functions, e.g. no-duplicatesp +(in-package "ACL2") +(include-book "data-structures/list-defuns" :dir :system) +(include-book "data-structures/list-defthms" :dir :system) + + +;;------------------------------------------------------------- +;; EMPTY INTERSECTION +;;------------------------------------------------------------ +(defun no_intersectp (l1 l2) + ;; returns t if every element of l1 is not in l2 + ;; i.e. if l1 and l2 have an empty intersection + (if (endp l1) + t + (and (not (member (car l1) l2)) + (no_intersectp (cdr l1) l2)))) + +;; we prove some properties of this predicate +(defthm commutativity_no_intersectp + ;; it is commutative + (equal (no_intersectp l1 l2) + (no_intersectp l2 l1))) + +(defthm no_intersectp_append + ;; we link this concept with APPEND + (equal (no_intersectp l1 (append l2 l3)) + (and (no_intersectp l1 l2) + (no_intersectp l1 l3)))) + +(defthm no_intersectp_append-1 + ;; it should be better to have some kind of normalization + ;; but the proof of rules to go to the normal form is + ;; not automatic in ACL2, but this rule is automatic. + (equal (no_intersectp (append l1 l2) l3) + (and (no_intersectp l1 l3) + (no_intersectp l2 l3)))) + +#| + +;;--------------------------------------------------------- +;; NODE COLLECTION +;;-------------------------------------------------------- + (i-am-here) +(defun grab_nodes (travel_list) + ;; collects all the nodes of all the routes of the travel list + ;; Pb: in the new version of GeNoC there are several routes + ;; not just one :-) + (if (endp travel_list) + nil + (append (RoutesV (car travel_list)) + (grab_nodes (cdr travel_list))))) + +(defthm no-duplicatesp-append + (implies (and (no-duplicatesp l1) + (no-duplicatesp l2) + (no_intersectp l1 l2)) + (no-duplicatesp (append l1 l2)))) + +(defthm no-duplicatesp-append-nil + (implies (no-duplicatesp l) + (no-duplicatesp (append l nil)))) + +(defun all_no_intersectp (route travel_list) + ;; returns t if route does not intersect with all the routes + ;; of the travel list + (if (endp travel_list) + t + (and (no_intersectp route (cdr (car travel_list))) + (all_no_intersectp route (cdr travel_list))))) + +(defthm all_no_intersectp_append + ;; we link this concept with append + (equal (all_no_intersectp l1 (append l2 l3)) + (and (all_no_intersectp l1 l2) + (all_no_intersectp l1 l3)))) + + +(defthm all_no_intersectp_grab_nodes + ;; we also link it with grab_nodes + (equal (all_no_intersectp r tl) + (no_intersectp r (grab_nodes tl)))) + +(defun all_no_intersectp_routep (travel_list) + ;; returns t if every route of the travel list has no intersection with + ;; every other route + (if (endp (cdr travel_list)) + t + (and (all_no_intersectp (cdr (car travel_list)) + (cdr travel_list)) + (all_no_intersectp_routep (cdr travel_list))))) +|# + +#| + +(defthm all_no_duplicates_and_all_no_intersectp_route_=>_no_dupli_grab_nodes + ;; we prove that this concept and if every route has no duplicate, + ;; then grab_nodes of this travel list has no duplicate + (implies (and (all_no_intersectp_routep l) + (all_no_duplicatesp l)) + (no-duplicatesp (grab_nodes l))) +; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.] +; :hints (("GOAL" +; :in-theory (disable NO-DUPLICATESP->NO-DUPLICATESP-EQUAL))) + ) +|#
\ No newline at end of file diff --git a/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/packet-scheduling.lisp b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/packet-scheduling.lisp new file mode 100644 index 0000000..03b16e2 --- /dev/null +++ b/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/scheduling/packet-scheduling.lisp @@ -0,0 +1,371 @@ +;; Julien Schmaltz +;; File: packet-scheduling.lisp +;; Modeling of a packet switching algorithm +;; Jan. 4th 2005 +;; Updated August 17th, 2005 + +(in-package "ACL2") + +(include-book "../../generic-modules/GeNoC-scheduling") +(include-book "intersect") + +;;--------------------------------------------------------------------- +;; +;; PACKET ALGORITHM +;; +;;--------------------------------------------------------------------- + +;; Our packet algorithm works as follows. For each step of the routes, +;; it extracts a set of non-overlapping travels. +;; for instance, if the routes are ( (0 4 5) (1 5 6) (2 1) (5 4)) +;; the first three routes do not overlap, the last one is thrown out. +;; At each step in a route, a node must not be used by other routes. + +(defun rev (x) + ;; we need this definition again :-) + (if (endp x) + nil + (append (rev (cdr x)) (list (car x))))) + +(defun consume-attempts (att) + ;; this function substracts one attempt to every node + ;; in the current model at each call of the scheduler + ;; (function packet-scheduling) each node consumes one attempt, + ;; i.e. each node tries to send a message. + (if (zp (SumOfAttempts att)) + att + (let* ((top (car att)) + (node (car top)) + (att-i (cadr top))) + (if (zp att-i) + (cons top + (consume-attempts (cdr att))) + (cons (list node (1- att-i)) + (consume-attempts (cdr att))))))) + +(defun no_intersectp_packet (route prev) + ;; In the packet mode, prev is the list of the nodes used + ;; for each step. + ;; This function checks that every node of a route + ;; is not already used at the corresponding step. + (if (endp route) + t + (and (not (member (car route) (car prev))) + (no_intersectp_packet (cdr route) (cdr prev))))) + +(defun test_prev_routes (routes prev) + ;; returns a route that does not overlap previous + ;; travels if such a route exists in routes. returns + ;; nil otherwise. + (if (endp routes) + nil + (let ((r (car routes))) + (if (no_intersectp_packet r prev) + r + (test_prev_routes (cdr routes) prev))))) + +(defun update-prev (prev route) + ;; update prev properly with route + (if (endp route) + prev + (cons (cons (car route) (car prev)) + (update-prev (cdr prev) (cdr route))))) + +(defun update_route (tr route) + ;; updates the route of tr to be a list containing + ;; only route + (list (IdV tr) (FrmV tr) (list route))) + +(defun pkt-scheduler (TrLst Scheduled Delayed prev) + ;; core function for the packet scheduler. + (if (endp TrLst) + ;; we use prev to keep the ordering of the ids + (mv (rev scheduled) (rev delayed)) + (let* ((tr (car TrLst)) + (routes (RoutesV tr)) + (r? (test_prev_routes routes prev))) + ;; if there is a good route in routes + ;; we update prev properly and schedule the travel + (if r? + (pkt-scheduler (cdr TrLst) + (cons (update_route tr r?) scheduled) + delayed (update-prev prev r?)) + ;; otherwise the travel is delayed + (pkt-scheduler (cdr TrLst) + scheduled (cons tr delayed) prev))))) + +(defun packet-scheduling (TrLst att) + ;; Function that matches the generic definition + ;; TrLst is the travel list, att is the list of attempts + (if (zp (SumOfAttempts att)) + (mv nil ;; nothing is scheduled if there is no attempt left + TrLst ;; everything is delayed + Att) + ;; otherwise we call pkt-scheduler and consume attempts + (mv-let (scheduled delayed) + (pkt-scheduler TrLst nil nil nil) + (mv Scheduled Delayed (consume-attempts att))))) + + +(defun pkt-sched-nt-sched (TrLst prev) + ;; to simplify proofs we define a non-tail version of + ;; pkt-scheduler that computes the scheduled travels + (if (endp TrLst) + nil + (let* ((tr (car TrLst)) + (routes (RoutesV tr)) + (r? (test_prev_routes routes prev))) + (if r? + (cons (update_route tr r?) + (pkt-sched-nt-sched (cdr TrLst) + (update-prev prev r?))) + (pkt-sched-nt-sched (cdr TrLst) prev))))) + + +(defthm pkt-scheduler-=-non-tail-scheduled + ;; we prove that our non-tail definition is correct + (equal (car (pkt-scheduler TrLst scheduled delayed prev)) + (append (rev scheduled) + (pkt-sched-nt-sched TrLst prev)))) + +(defun pkt-sched-nt-del (TrLst prev) + ;; we proceed similarly for the delayed transfers + (if (endp TrLst) + nil + (let* ((tr (car TrLst)) + (routes (RoutesV tr)) + (r? (test_prev_routes routes prev))) + (if r? + (pkt-sched-nt-del (cdr TrLst) + (update-prev prev r?)) + (cons tr + (pkt-sched-nt-del (cdr TrLst) prev)))))) + +(defthm pkt-scheduler-=-non-tail-delayed + (equal (mv-nth 1 (pkt-scheduler TrLst scheduled delayed prev)) + (append (rev delayed) + (pkt-sched-nt-del TrLst prev)))) +;;----------------------------------------------------------------- + + + +;;--------------------------------------------------------------------- +;; +;; PROOF OF GeNoC CONSTRAINTS +;; +;;--------------------------------------------------------------------- + + +;; 1/ consume at least one attempt to ensure termination + +(defthm consume-at-least-one-attempt-packet-scheduling + ;; the scheduling policy should consume at least one attempt + ;; this is a sufficient condition to prove that + ;; the full network function terminates + (mv-let (Scheduled Delayed newatt) + (packet-scheduling TrLst att) + (declare (ignore Scheduled Delayed)) + (implies (not (zp (SumOfAttempts att))) + (< (SumOfAttempts newatt) + (SumOfAttempts att))))) +;;---------------------------------------------------------- + +;; 2/ we prove that the ids of the delayed and scheduled travels +;; are part of the initial travel list +;; ----------------------------------- +(defthm subsetp-scheduled-pkt + (implies (TrLstp TrLst) + (subsetp (V-ids (pkt-sched-nt-sched TrLst prev)) + (V-ids TrLst)))) + +(defthm subsetp-delayed-pkt + (implies (TrLstp TrLst) + (subsetp (V-ids (pkt-sched-nt-del TrLst prev)) + (V-ids TrLst)))) +;------------------------------------------------------------------ + +;; 3/ we prove that the list of scheduled travels is a +;; valid travel list +;; -------------------------------------------------- + + +(defthm validfield-route-test_prev_routes + (let ((r? (test_prev_routes routes prev))) + (implies (and (validfield-route routes) + r?) + (and (consp r?) (consp (cdr r?)))))) + + +;; proof for the scheduled travels +;; ------------------------------- +(local + (defthm validfields-trlst-pkt-sched + (implies (ValidFields-TrLst TrLst) + (ValidFields-TrLst + (pkt-sched-nt-sched TrLst prev))))) + +(local + (defthm not-member-V-ids-pkt-sched + (implies (not (member-equal e (V-ids TrLst))) + (not + (member-equal + e + (V-ids + (pkt-sched-nt-sched TrLst prev))))))) + +(local (defthm no-duplicatesp-pkt-sched + (implies (no-duplicatesp-equal (V-ids TrLst)) + (no-duplicatesp-equal + (V-ids (pkt-sched-nt-sched TrLst prev)))))) + +(defthm cons-v-ids + (equal (consp (v-ids TrLst)) + (consp TrLst))) + +(defthm TrLstp-scheduled-ct + (implies (TrLstp TrLst) + (TrLstp (pkt-sched-nt-sched TrLst prev)))) + +;; proof for the delayed travels +;; ----------------------------- +(local + (defthm validfields-trlst-pkt-del + (implies (ValidFields-TrLst TrLst) + (ValidFields-TrLst + (pkt-sched-nt-del TrLst prev))))) + +(local + (defthm not-member-V-ids-pkt-del + (implies (not (member-equal e (V-ids TrLst))) + (not + (member-equal + e + (V-ids + (pkt-sched-nt-del TrLst prev))))))) + +(local (defthm no-duplicatesp-pkt-del + (implies (no-duplicatesp-equal (V-ids TrLst)) + (no-duplicatesp-equal + (V-ids (pkt-sched-nt-del TrLst prev)))))) + +(defthm TrLstp-delayed-pkt + (implies (TrLstp TrLst) + (TrLstp (pkt-sched-nt-del TrLst prev)))) +;;-------------------------------------------------------------------- + + +;; 4/ correctness of the scheduled travels +;; ------------------------------------------------------ + +(defthm extract-sublst-cons + (implies (not (member-equal id Ids)) + (equal (extract-sublst (cons (list id frm routes) L) + Ids) + (extract-sublst L Ids)))) + + +(defthm test_prev_routes-member-equal + (let ((r? (test_prev_routes routes prev))) + (implies r? + (member-equal r? routes)))) + +(defthm pkt-scheduled-correctness + (let ((Scheduled (pkt-sched-nt-sched TrLst prev))) + (implies (TrLstp TrLst) + (s/d-travel-correctness + scheduled + (extract-sublst TrLst (V-ids Scheduled)))))) + +;; 5/ We prove that Delayed is equal to filtering TrLst +;; according to the ids of Delayed +;; ---------------------------------------------------- +(defthm pkt-delayed-correctness + (let ((delayed (pkt-sched-nt-del TrLst prev))) + (implies (TrLstp TrLst) + (equal delayed + (extract-sublst TrLst (V-ids delayed))))) + :rule-classes nil) +; ----------------------------------------------------------- + +;; 6/ we prove that the ids of the delayed travels are distinct +;; from those of the scheduled travels +;; ------------------------------------------------------------ + +(defthm not-in-cons + ;; same lemma as in the packet scheduling + (implies (and (not-in x y) (not (member-equal e x))) + (not-in x (cons e y)))) + +(defthm not-in-v-ids-ct + (implies (TrLstp trlst) + (not-in (v-ids (pkt-sched-nt-del trlst prev)) + (v-ids (pkt-sched-nt-sched trlst prev))))) + + +;; Finally, we check that our circuit scheduling function +;; is a valid instance of GeNoC-scheduling +;; ------------------------------------------------------ +(defthm check-compliance-packet-scheduling + t + :rule-classes nil + :otf-flg t + :hints (("GOAL" + :do-not-induct t + :use + ((:functional-instance + consume-at-least-one-attempt + (scheduling packet-scheduling))) + :in-theory (disable consume-at-least-one-attempt + missivesp)) + ("Subgoal 6" + :use (:instance pkt-delayed-correctness + (prev nil))) + ("Subgoal 3" + :in-theory (disable packet-scheduling)))) + +;;--------------------------------------------------------------------- +;; +;; CORRECTNESS OF THE PACKET ALGORITHM +;; +;;--------------------------------------------------------------------- +(defun create_steps (TrLst steps) + ;; creates the lists of the nodes used at every step + ;; by the routes in TrLst (the only route kept by the scheduler) + ;; steps is nil at function call and contains the lists of + ;; the step-nodes. steps = ( (r0[0] r1[0] ...) (r0[1] r1[1] ...) ...) + (if (endp TrLst) + steps + (let* ((tr (car TrLst)) + (r (car (RoutesV tr)))) + (create_steps (cdr TrLst) (update-prev steps r))))) + +(defun all_no_duplicates-steps (steps) + ;; the packet policy is correct is a node is used only once + ;; at a given step. + (if (endp steps) + t + (let ((step-i (car steps))) + (and (no-duplicatesp-equal step-i) + (all_no_duplicates-steps (cdr steps)))))) + +(defthm test_prev_routes-all_no-dup + (let ((r? (test_prev_routes r prev))) + (implies (and r? + (all_no_duplicates-steps prev)) + (all_no_duplicates-steps (update-prev prev r?))))) + +(defthm pkt-scheduling-correctness + (implies (and (TrLstp TrLst) + (all_no_duplicates-steps prev)) + (all_no_duplicates-steps + (create_steps (pkt-sched-nt-sched TrLst prev) + prev))) + :otf-flg t + :hints (("GOAL" + :induct (pkt-sched-nt-sched trlst prev) + :do-not-induct t + :do-not '(eliminate-destructors generalize)))) + +;;----------------------------------------------------------------- +;; end of packet scheduling +;;----------------------------------------------------------------- |