(in-package "ACL2") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (include-book "tiny") (include-book "misc/defpun" :dir :system) (include-book "arithmetic-3/bind-free/top" :dir :system) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Here is the program we will be analyzing. Note that in both loops ;;; --- tricky1 and tricky3 --- we increment output only when i is ;;; even. Further note that temp = low at those times. (Because we ;;; set it so either initially, or on the previous iteration.) Thus, ;;; the value of output does not depend ever on high. #| tricky1 (int high, low, n) { int temp = low; for i = 0 to n do { if even(i) { output = output + temp; temp = high; } else { temp = low; } } output = output + 7; } tricky3 (int high, low, n) { int temp = low; for i = 0 to 3*n do { if even(i) { output = output + temp; temp = high; } else { temp = low; } } output = output + 7; } main (int high, low, n, flag) { int output = 0; if flag < 0 { tricky1(high, low); } else { tricky3(high, low); } output = output - 1; } |# ;;; The two main theorems that we will prove are: ;;; 1) that the final value of output in main depends only on low, n, ;;; and flag ---main-out-pre-post. ;;; 2) that the only values changed at the end of main are output, ;;; temp, i, and the machine register scratch --- main-frame. ;;; Although the proof script is a little more than 1300 lines long, ;;; this is very much a demonstration of feasibility, rather than a ;;; fully worked, production quality example. The vast majority of ;;; what appears in the script is quite routine and automatable, and ;;; should be generated by macros. Very little should have to be ;;; entered by hand. ;;; Those parts which require some level of manual intervention are ;;; marked with !!!. It is likely that the effort required even for ;;; these parts can be eased with the proper tools. It is certainly ;;; the case that the syntax can be improved. ;;; Other important parts are marked with +++. ;;; We skip marking the corresponding pieces for tricky3, since they ;;; are almost identical to those for tricky1. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; We now define the machine code for the above, and some good-state ;;; predicates which ensure the state is well formed and the ;;; appropriate programs loaded. (defconst *high* 0) (defconst *low* 1) (defconst *n* 2) (defconst *flag* 3) (defconst *output* 4) (defconst *temp* 5) (defconst *i* 6) (defconst *scratch* 7) (defun tricky1 () `(;; initialize (100 (loadi ,*temp* 0)) (101 (add ,*temp* ,*low*)) (102 (loadi ,*i* 0)) ;; loop test (103 (ifgt ,*i* ,*n* 114)) ;; branch test (104 (ifodd ,*i* 109)) ;; true branch (105 (add ,*output* ,*temp*)) (106 (loadi ,*temp* 0)) (107 (add ,*temp* ,*high*)) (108 (goto 111)) ;; false branch (109 (loadi ,*temp* 0)) (110 (add ,*temp* ,*low*)) ;; finish off loop (111 (loadi ,*scratch* 1)) (112 (add ,*i* ,*scratch*)) (113 (goto 103)) ;; finish off routine (114 (loadi ,*scratch* 7)) (115 (add ,*output* ,*scratch*)) (116 (ret)))) (defun good-tricky1-state (st h) (and (consp (get-pc-stack st)) (program-loaded-p (tricky1) st) (< 10 (len (get-memory st))) (equal (len (get-pc-stack st)) h))) (defun tricky3 () `(;; initialize (200 (loadi ,*temp* 0)) (201 (add ,*temp* ,*low*)) (202 (loadi ,*i* 0)) ;; loop test (203 (loadi ,*scratch* 3)) (204 (mult ,*scratch* ,*n*)) (205 (ifgt ,*i* ,*scratch* 216)) ;; branch test (206 (ifodd ,*i* 211)) ;; true branch (207 (add ,*output* ,*temp*)) (208 (loadi ,*temp* 0)) (209 (add ,*temp* ,*high*)) (210 (goto 213)) ;; false branch (211 (loadi ,*temp* 0)) (212 (add ,*temp* ,*low*)) ;; finish off loop (213 (loadi ,*scratch* 1)) (214 (add ,*i* ,*scratch*)) (215 (goto 203)) ;; finish off routine (216 (loadi ,*scratch* 7)) (217 (add ,*output* ,*scratch*)) (218 (ret)))) (defun good-tricky3-state (st h) (and (consp (get-pc-stack st)) (program-loaded-p (tricky3) st) (< 10 (len (get-memory st))) (equal (len (get-pc-stack st)) h))) (defun main () `((300 (loadi ,*output* 0)) (301 (loadi ,*scratch* 0)) (302 (ifgt ,*flag* ,*scratch* 305)) (303 (call 100)) (304 (goto 306)) (305 (call 200)) (306 (spin)))) (defun good-main-state (st h) (and (consp (get-pc-stack st)) (program-loaded-p (tricky1) st) (program-loaded-p (tricky3) st) (program-loaded-p (main) st) (< 10 (len (get-memory st))) (equal (len (get-pc-stack st)) h))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; We now specify the cutpoints for tricky1. ;;; Our machine model, tiny, maintains a stack of program-counters. ;;; In good-tricky1-state, we specify that this stack is of height h. ;;; Thus, if the stack height is less than h, we have exited tricky1. (defun sub-routine-exited (st h) (< (len (get-pc-stack st)) h)) ;;; !!! The user must specify (or perhaps merely approve ACL2s choice ;;; of) the cutpoints. The first represents the instruction just ;;; after returning from a call to tricky1, the second tricky1's entry ;;; point, and the third the top of the loop. ;;; ??? Should we be using the beginning of the loop test, or the ;;; first instruction in the loop's body? Does it matter? (defun tricky1-cutpoint-p (st h) (or (sub-routine-exited st h) (equal (get-pc st) 100) (equal (get-pc st) 103))) ;;; Since we will be stepping pairs of states from cutpoint to ;;; cutpoint, we define a predicate to identify when the two states ;;; are standing at the same cutpoint. (defun equal-tricky1-cutpoints-p (st0 h0 st1 h1) (and (tricky1-cutpoint-p st0 h0) (if (sub-routine-exited st0 h0) (sub-routine-exited st1 h1) (and (not (sub-routine-exited st1 h1)) (equal (get-pc st0) (get-pc st1)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; We now define a set of entirely routine stepper functions. ;;; The first of these steps a state to the next cutpoint. We must ;;; use defpun here, so as to avoid the neccessity of proving that we ;;; really do get to one. In particular, if we are not in tricky1's ;;; body, this need not be true. (encapsulate () (local (in-theory (enable nfix))) (defpun run-tricky1-to-next-cutpoint (st h) (if (tricky1-cutpoint-p st h) st (run-tricky1-to-next-cutpoint (next st) h))) ) ;;; And here are a couple of openers for run-tricky1-to-next-cutpoint. (defthm run-tricky1-to-next-cutpoint-base (implies (tricky1-cutpoint-p st h) (equal (run-tricky1-to-next-cutpoint st h) st))) (defthm run-tricky1-to-next-cutpoint-opener (implies (not (tricky1-cutpoint-p st h)) (equal (run-tricky1-to-next-cutpoint st h) (run-tricky1-to-next-cutpoint (next st) h)))) (in-theory (disable run-tricky1-to-next-cutpoint-def)) ;;; Here is another defpun, which steps st all the way to tricky1's ;;; exit. (encapsulate () (local (in-theory (enable nfix))) (defpun run-tricky1-to-exit (st h) (if (< (len (get-pc-stack st)) h) st (run-tricky1-to-exit (run-tricky1-to-next-cutpoint (next st) h) h))) ) (defthm run-tricky1-to-exit-base (implies (< (len (get-pc-stack st)) h) (equal (run-tricky1-to-exit st h) st))) (defthm run-tricky1-to-exit-opener (implies (not (< (len (get-pc-stack st)) h)) (equal (run-tricky1-to-exit st h) (run-tricky1-to-exit (run-tricky1-to-next-cutpoint (next st) h) h)))) (in-theory (disable run-tricky1-to-exit-def)) ;;; We will only be proving partial correctness reults here. ;;; So that we can perform an induction, we define a regular function ;;; which steps through tricky1 either to its exit or a maximum of n ;;; steps. This is a standard trick adopted from Sandip's work on ;;; compositional cutpoints. ;;; We will add a hypothesis to any inductive theorems (or those that ;;; depend on one), that stepping n times is sufficient to exit. The ;;; alternative is to prove that tricky1 really does always terminate ;;; by providing a measure, and proving a total correctness result. (defun run-tricky1-to-exit-bounded (st h n) (declare (xargs :measure (nfix n) :hints (("Goal" :in-theory (enable nfix))))) (if (or (zp n) (< (len (get-pc-stack st)) h)) st (run-tricky1-to-exit-bounded (run-tricky1-to-next-cutpoint (next st) h) h (+ -1 n)))) ;;; In order to justify the use of the above, we prove that if n is ;;; large enough for run-tricky1-to-exit-bounded to run to exit, so ;;; will run-tricky1-to-exit. (defthm run-tricky1-to-exit-exits-if-run-tricky1-to-exit-bounded-does (implies (< (LEN (GET-PC-STACK (RUN-TRICKY1-TO-EXIT-BOUNDED ST0 H0 N))) H0) (< (LEN (GET-PC-STACK (RUN-TRICKY1-TO-EXIT ST0 H0))) H0))) ;;; We now give a couple of induction schemes based on ;;; run-tricky1-to-next-cutpoint. (defun run-tricky1-to-exit-ind-1 (st0 h0 st1 h1 n) (if (zp n) (+ st0 h0 st1 h1) (run-tricky1-to-exit-ind-1 st0 h0 (run-tricky1-to-next-cutpoint (next st1) h1) h1 (+ -1 n)))) (defun run-tricky1-to-exit-ind-2 (st0 h0 st1 h1 n) (if (zp n) (+ st0 h0 st1 h1) (run-tricky1-to-exit-ind-2 (run-tricky1-to-next-cutpoint (next st0) h0) h0 (run-tricky1-to-next-cutpoint (next st1) h1) h1 (+ -1 n)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; !!! The next three events must be specified by the user. (Or ;;; perhaps we can use some external tool in the simple cases to ;;; gather this information. There is no reason to believe that this ;;; can be automated in general, however, without a true artifical ;;; intelligence.) ;;; These three events form the heart of specifying the information ;;; flow. The first lists those variables upon which the final value ;;; of output depends, and the second specifies the loop invariant ;;; which makes the dependency true. ;;; We would need a similar set for each variable (or set of ;;; variables) for which we wish to specify the information flow. We ;;; will see below that the variables which are changed, but for which ;;; we do not care about the information flow, must also be listed. ;;; Certainly a more succinct way of specifying this could be ;;; developed. (defun tricky1-pre-out (st0 h0 st1 h1) (and (good-tricky1-state st0 h0) (good-tricky1-state st1 h1) (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)) (equal (get-addr *output* st0) (get-addr *output* st1)))) (defun tricky1-loop-invariant-out (st0 h0 st1 h1) (and (good-tricky1-state st0 h0) (good-tricky1-state st1 h1) (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)) (equal (get-addr *i* st0) (get-addr *i* st1)) (implies (evenp (get-addr *i* st0)) (equal (get-addr *temp* st0) (get-addr *temp* st1))) (equal (get-addr *output* st0) (get-addr *output* st1)))) (defun tricky1-post-out (st0 h0 st1 h1) (declare (ignore h0 h1)) (equal (get-addr *output* st0) (get-addr *output* st1))) ;;; !!! We define a predicate which says that the appropriate ;;; condition holds at each cutpoint. The user must at least specify ;;; which condition coresponds to which cutpoint. ;;; Exit must go first, so that when we exit we do not consider the ;;; case that we have popped back to the beginning again. (defun tricky1-assertions-out (st0 h0 st1 h1) (cond ((sub-routine-exited st0 h0) (tricky1-post-out st0 h0 st1 h1)) ((equal (get-pc st0) 100) (tricky1-pre-out st0 h0 st1 h1)) ((equal (get-pc st0) 103) (tricky1-loop-invariant-out st0 h0 st1 h1)))) ;;; We prove that if we start at equal cutpoints, stepping to the next ;;; one leaves us at equal cutpoints. This is neccesary for induction ;;; in tricky1-assertion-out-induct to hold. (defthm equal-tricky1-cutpoints-invariant-out (implies (and (equal-tricky1-cutpoints-p st0 h0 st1 h1) (tricky1-assertions-out st0 h0 st1 h1) (not (< (len (get-pc-stack st0)) h0))) (equal-tricky1-cutpoints-p (run-tricky1-to-next-cutpoint (next st0) h0) h0 (run-tricky1-to-next-cutpoint (next st1) h1) h1))) ;;; And we prove that the assertions holding at one cutpoint, implies ;;; that they hold at the next. This is the heart of the proof. (defthm tricky1-assertion-out-invariant (implies (and (tricky1-assertions-out st0 h0 st1 h1) (equal-tricky1-cutpoints-p st0 h0 st1 h1) (not (< (len (get-pc-stack st0)) h0))) (tricky1-assertions-out (run-tricky1-to-next-cutpoint (next st0) h0) h0 (run-tricky1-to-next-cutpoint (next st1) h1) h1))) ;;; This theorem should be proven via functional instantiation. Thus, ;;; all the hints used should be ignored. (defthm tricky1-assertion-out-induct (implies (and (tricky1-assertions-out st0 h0 st1 h1) (equal-tricky1-cutpoints-p st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st0 h0 n))) h0)) (tricky1-assertions-out (run-tricky1-to-exit st0 h0) h0 (run-tricky1-to-exit st1 h1) h1)) :hints (("Goal" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out equal-tricky1-cutpoints-p) :induct (run-tricky1-to-exit-ind-2 st0 h0 st1 h1 n) :do-not '(generalize)) ("Subgoal *1/2.7" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) ("Subgoal *1/2.6" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) ("Subgoal *1/2.5" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) ("Subgoal *1/2.4" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) ("Subgoal *1/2.3" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out) :use (:instance equal-tricky1-cutpoints-invariant-out)) ("Subgoal *1/2.2" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) ("Subgoal *1/2.1" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) ("Subgoal *1/1" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-out)) )) ;;; +++ This is merely an instantiation of ;;; tricky1-assertion-out-induct. Perhaps a clearer and more ;;; desireable version is: #| (implies (and (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)) (equal (get-addr *output* st0) (get-addr *output* st1)) (good-tricky1-state st0 h0) (good-tricky1-state st1 h1) (equal (get-pc st0) 100) (equal (get-pc st1) 100) ) (equal (get-addr *output* (run-tricky1-to-exit st0 h0)) (get-addr *output* (run-tricky1-to-exit st1 h1)))) |# ;;; in which tricky1-pre-out and tricky1-post-out are expanded. ;;; It demonstrates that the final value of output in tricky1 depends ;;; only on the initial values of low, n, and output. (defthm tricky1-assertion-out-pre-post (implies (and (tricky1-pre-out st0 h0 st1 h1) (equal (get-pc st0) 100) (equal-tricky1-cutpoints-p st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st0 h0 n))) h0)) (tricky1-post-out (run-tricky1-to-exit st0 h0) h0 (run-tricky1-to-exit st1 h1) h1)) :hints (("Goal" :in-theory (disable run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next run-tricky1-to-exit-bounded RUN-TRICKY1-TO-EXIT-BASE RUN-TRICKY1-TO-EXIT-OPENER) :use (:instance tricky1-assertion-out-induct) :do-not-induct t)) :otf-flg t) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; !!! The user (or, again, an external tool) must specify those ;;; variables that change, but for which we do not care about the ;;; information flow. In the present example, this is temp, scratch, ;;; and i. The events themselves in this section should be entirely ;;; automaticly generated from this listing. ;;; In order to use the above theorem in the proof about the ;;; information flow of main, some more work is neccesary. We must ;;; specify and ``affect'' function for tricky1, so that we can ;;; compose the call to tricky1 in main with the symbolic simulation ;;; of the regular op-codes. ;;; However, we do not want to have to do any real work to do this, so ;;; we merely state that those variables that change, change in the ;;; way that running the code changes them. (defun tricky1-pre-spec (st0 h0 st1 h1) (and (good-tricky1-state st0 h0) (good-tricky1-state st1 h1) (equal st0 st1))) (defun tricky1-loop-invariant-spec (st0 h0 st1 h1) (and (good-tricky1-state st0 h0) (good-tricky1-state st1 h1) (let ((st-spec (set-pc (get-pc st1) (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st0))))))) (equal st-spec st1)))) (defun tricky1-post-spec (st0 h0 st1 h1) (declare (ignore h0 h1)) (and (let ((st-spec (pop-pc (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st0))))))) (equal st-spec st1)))) ;;; Note that we use st1 for the branch conditions here (since st0 is ;;; static). Should we use st1 throughout for consistency? Does it ;;; matter? Will this work? (defun tricky1-assertions-spec (st0 h0 st1 h1) (cond ((< (len (get-pc-stack st1)) h1) (tricky1-post-spec st0 h0 st1 h1)) ((equal (get-pc st1) 100) (tricky1-pre-spec st0 h0 st1 h1)) ((equal (get-pc st1) 103) (tricky1-loop-invariant-spec st0 h0 st1 h1)))) ;;; no equal-cutpoints hypothesis since st0 is static. (defthm tricky1-assertion-spec-invariant (implies (and (tricky1-assertions-spec st0 h0 st1 h1) (not (< (len (get-pc-stack st1)) h1))) (tricky1-assertions-spec st0 h0 (run-tricky1-to-next-cutpoint (next st1) h1) h1)) :otf-flg t) (defthm tricky1-assertion-spec-induct (implies (and (tricky1-assertions-spec st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st1 h1 n))) h1)) (tricky1-assertions-spec st0 h0 (run-tricky1-to-exit st1 h1) h1)) :hints (("Goal" :in-theory (e/d (run-tricky1-to-exit-def) (run-tricky1-to-next-cutpoint-base run-tricky1-to-next-cutpoint-opener next tricky1-assertions-spec)) :induct (run-tricky1-to-exit-ind-1 st0 h0 st1 h1 n) :do-not '(generalize)))) ;;; +++ Here is our spec function. It is based upon ;;; tricky1-post-spec. Or, rather, tricky1-post-spec is based upon ;;; this. Note that as stated above we merely state that those ;;; variables that change, change in the way that running the code ;;; changes them. (defun tricky1-spec (st h) (let ((st1 (run-tricky1-to-exit st h))) (pop-pc (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st))))))) ;;; We now prove a bunch of theorems about out spec function: (encapsulate () (local (defthm tricky1-spec-thm-temp (implies (and (good-tricky1-state st h) (equal (get-pc st) 100) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st h n))) h)) (equal (tricky1-spec st h) (run-tricky1-to-exit st h))) :hints (("Goal" :use (:instance tricky1-assertion-spec-induct (st0 st) (h0 h) (st1 st) (h1 h)) :in-theory (disable tricky1-assertion-spec-induct program-loaded-p RUN-TRICKY1-TO-EXIT-OPENER) :do-not-induct t)))) ;;; The information flow for output that we proved in ;;; tricky1-assertion-out-pre-post holds for the spec function also. (defthm tricky1-spec-out (implies (and (tricky1-pre-out st0 h0 st1 h1) (equal (get-pc st0) 100) (equal-tricky1-cutpoints-p st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st0 h0 n))) h0) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st1 h1 n))) h1)) (tricky1-post-out (tricky1-spec st0 h0) h0 (tricky1-spec st1 h1) h1)) :hints (("Goal" :in-theory (disable program-loaded-p RUN-TRICKY1-TO-EXIT-OPENER tricky1-post-out tricky1-spec) :do-not-induct t))) ;;; +++ Only output, temp, scratch, and I are changed by tricky-spec, ;;; and therefore by tricky1. Thus we have not missed any channels of ;;; communication. (defthm tricky1-spec-frame (implies (and (not (equal addr *output*)) (not (equal addr *temp*)) (not (equal addr *scratch*)) (not (equal addr *i*))) (equal (get-addr addr (tricky1-spec st h)) (get-addr addr st)))) (defthm tricky1-spec-pc (equal (get-pc (tricky1-spec st h)) (get-pc (pop-pc st)))) (defthm program-loaded-p-tricky1-spec (equal (program-loaded-p prog (tricky1-spec st h)) (program-loaded-p prog st))) (defthm get-program-tricky1-spec (equal (get-program (tricky1-spec st h)) (get-program st))) (defthm consp-get-pc-stack-tricky1-spec (equal (consp (get-pc-stack (tricky1-spec (push-pc pc st) h))) (consp (get-pc-stack st)))) (defthm len-get-pc-stack-tricky1-spec (implies (consp (get-pc-stack st)) (equal (len (get-pc-stack (tricky1-spec st h))) (+ -1 (len (get-pc-stack st)))))) ;;; +++ Tricky1-spec has the same affect as running tricky1. (defthm tricky1-spec-thm (implies (and (good-tricky1-state st h) (equal (get-pc st) 100) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st h n))) h)) (equal (run-tricky1-to-exit st h) (tricky1-spec st h)))) ) (defthm tricky1-frame (implies (and (good-tricky1-state st h) (equal (get-pc st) 100) (not (equal addr *output*)) (not (equal addr *temp*)) (not (equal addr *scratch*)) (not (equal addr *i*)) (< (len (get-pc-stack (run-tricky1-to-exit-bounded st h n))) h)) (equal (get-addr addr (run-tricky1-to-exit st h)) (get-addr addr st))) :rule-classes nil) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; We now repeat the above, but for tricky3. ;;; Same as above except: ;;; tricky1 --> tricky3 ;;; cutpoint 100 --- 200, 103 --> 203 (defun tricky3-cutpoint-p (st h) (or (sub-routine-exited st h) (equal (get-pc st) 200) (equal (get-pc st) 203))) (defun equal-tricky3-cutpoints-p (st0 h0 st1 h1) (and (tricky3-cutpoint-p st0 h0) (if (sub-routine-exited st0 h0) (sub-routine-exited st1 h1) (and (not (sub-routine-exited st1 h1)) (equal (get-pc st0) (get-pc st1)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (encapsulate () (local (in-theory (enable nfix))) (defpun run-tricky3-to-next-cutpoint (st h) (if (tricky3-cutpoint-p st h) st (run-tricky3-to-next-cutpoint (next st) h))) ) (defthm run-tricky3-to-next-cutpoint-base (implies (tricky3-cutpoint-p st h) (equal (run-tricky3-to-next-cutpoint st h) st))) (defthm run-tricky3-to-next-cutpoint-opener (implies (not (tricky3-cutpoint-p st h)) (equal (run-tricky3-to-next-cutpoint st h) (run-tricky3-to-next-cutpoint (next st) h)))) (in-theory (disable run-tricky3-to-next-cutpoint-def)) (encapsulate () (local (in-theory (enable nfix))) (defpun run-tricky3-to-exit (st h) (if (< (len (get-pc-stack st)) h) st (run-tricky3-to-exit (run-tricky3-to-next-cutpoint (next st) h) h))) ) (defthm run-tricky3-to-exit-base (implies (< (len (get-pc-stack st)) h) (equal (run-tricky3-to-exit st h) st))) (defthm run-tricky3-to-exit-opener (implies (not (< (len (get-pc-stack st)) h)) (equal (run-tricky3-to-exit st h) (run-tricky3-to-exit (run-tricky3-to-next-cutpoint (next st) h) h)))) (in-theory (disable run-tricky3-to-exit-def)) (defun run-tricky3-to-exit-bounded (st h n) (declare (xargs :measure (nfix n) :hints (("Goal" :in-theory (enable nfix))))) (if (or (zp n) (< (len (get-pc-stack st)) h)) st (run-tricky3-to-exit-bounded (run-tricky3-to-next-cutpoint (next st) h) h (+ -1 n)))) (defthm run-tricky3-to-exit-exits-if-run-tricky3-to-exit-bounded-does (implies (< (LEN (GET-PC-STACK (RUN-TRICKY3-TO-EXIT-BOUNDED ST0 H0 N))) H0) (< (LEN (GET-PC-STACK (RUN-TRICKY3-TO-EXIT ST0 H0))) H0))) (defun run-tricky3-to-exit-ind-1 (st0 h0 st1 h1 n) (if (zp n) (+ st0 h0 st1 h1) (run-tricky3-to-exit-ind-1 st0 h0 (run-tricky3-to-next-cutpoint (next st1) h1) h1 (+ -1 n)))) (defun run-tricky3-to-exit-ind-2 (st0 h0 st1 h1 n) (if (zp n) (+ st0 h0 st1 h1) (run-tricky3-to-exit-ind-2 (run-tricky3-to-next-cutpoint (next st0) h0) h0 (run-tricky3-to-next-cutpoint (next st1) h1) h1 (+ -1 n)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun tricky3-pre-out (st0 h0 st1 h1) (and (good-tricky3-state st0 h0) (good-tricky3-state st1 h1) (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)) (equal (get-addr *output* st0) (get-addr *output* st1)))) (defun tricky3-loop-invariant-out (st0 h0 st1 h1) (and (good-tricky3-state st0 h0) (good-tricky3-state st1 h1) (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)) (equal (get-addr *i* st0) (get-addr *i* st1)) (implies (evenp (get-addr *i* st0)) (equal (get-addr *temp* st0) (get-addr *temp* st1))) (equal (get-addr *output* st0) (get-addr *output* st1)))) (defun tricky3-post-out (st0 h0 st1 h1) (declare (ignore h0 h1)) (equal (get-addr *output* st0) (get-addr *output* st1))) ;;; Exit must go first, to ensure that we do not pop back to ;;; pre (defun tricky3-assertions-out (st0 h0 st1 h1) (cond ((< (len (get-pc-stack st0)) h0) (tricky3-post-out st0 h0 st1 h1)) ((equal (get-pc st0) 200) (tricky3-pre-out st0 h0 st1 h1)) ((equal (get-pc st0) 203) (tricky3-loop-invariant-out st0 h0 st1 h1)))) (defthm equal-tricky3-cutpoints-invariant-out (implies (and (equal-tricky3-cutpoints-p st0 h0 st1 h1) (tricky3-assertions-out st0 h0 st1 h1) (not (< (len (get-pc-stack st0)) h0))) (equal-tricky3-cutpoints-p (run-tricky3-to-next-cutpoint (next st0) h0) h0 (run-tricky3-to-next-cutpoint (next st1) h1) h1))) (defthm tricky3-assertion-out-invariant (implies (and (tricky3-assertions-out st0 h0 st1 h1) (equal-tricky3-cutpoints-p st0 h0 st1 h1) (not (< (len (get-pc-stack st0)) h0))) (tricky3-assertions-out (run-tricky3-to-next-cutpoint (next st0) h0) h0 (run-tricky3-to-next-cutpoint (next st1) h1) h1))) (defthm tricky3-assertion-out-induct (implies (and (tricky3-assertions-out st0 h0 st1 h1) (equal-tricky3-cutpoints-p st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st0 h0 n))) h0)) (tricky3-assertions-out (run-tricky3-to-exit st0 h0) h0 (run-tricky3-to-exit st1 h1) h1)) :hints (("Goal" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out equal-tricky3-cutpoints-p) :induct (run-tricky3-to-exit-ind-2 st0 h0 st1 h1 n) :do-not '(generalize)) ("Subgoal *1/2.7" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) ("Subgoal *1/2.6" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) ("Subgoal *1/2.5" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) ("Subgoal *1/2.4" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) ("Subgoal *1/2.3" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out) :use (:instance equal-tricky3-cutpoints-invariant-out)) ("Subgoal *1/2.2" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) ("Subgoal *1/2.1" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) ("Subgoal *1/1" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-out)) )) (defthm tricky3-assertion-out-pre-post (implies (and (tricky3-pre-out st0 h0 st1 h1) (equal (get-pc st0) 200) (equal-tricky3-cutpoints-p st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st0 h0 n))) h0)) (tricky3-post-out (run-tricky3-to-exit st0 h0) h0 (run-tricky3-to-exit st1 h1) h1)) :hints (("Goal" :in-theory (disable run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next run-tricky3-to-exit-bounded RUN-TRICKY3-TO-EXIT-BASE RUN-TRICKY3-TO-EXIT-OPENER) :use (:instance tricky3-assertion-out-induct) :do-not-induct t)) :otf-flg t) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun tricky3-pre-spec (st0 h0 st1 h1) (and (good-tricky3-state st0 h0) (good-tricky3-state st1 h1) (equal st0 st1))) (defun tricky3-loop-invariant-spec (st0 h0 st1 h1) (and (good-tricky3-state st0 h0) (good-tricky3-state st1 h1) (let ((st-spec (set-pc (get-pc st1) (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st0))))))) (equal st-spec st1)))) (defun tricky3-post-spec (st0 h0 st1 h1) (declare (ignore h0 h1)) (and (let ((st-spec (pop-pc (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st0))))))) (equal st-spec st1)))) (defun tricky3-assertions-spec (st0 h0 st1 h1) (cond ((< (len (get-pc-stack st1)) h1) (tricky3-post-spec st0 h0 st1 h1)) ((equal (get-pc st1) 200) (tricky3-pre-spec st0 h0 st1 h1)) ((equal (get-pc st1) 203) (tricky3-loop-invariant-spec st0 h0 st1 h1)))) (defthm tricky3-assertion-spec-invariant (implies (and (tricky3-assertions-spec st0 h0 st1 h1) (not (< (len (get-pc-stack st1)) h1))) (tricky3-assertions-spec st0 h0 (run-tricky3-to-next-cutpoint (next st1) h1) h1)) :otf-flg t) (defthm tricky3-assertion-spec-induct (implies (and (tricky3-assertions-spec st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st1 h1 n))) h1)) (tricky3-assertions-spec st0 h0 (run-tricky3-to-exit st1 h1) h1)) :hints (("Goal" :in-theory (e/d (run-tricky3-to-exit-def) (run-tricky3-to-next-cutpoint-base run-tricky3-to-next-cutpoint-opener next tricky3-assertions-spec)) :induct (run-tricky3-to-exit-ind-1 st0 h0 st1 h1 n) :do-not '(generalize)))) (defun tricky3-spec (st h) (let ((st1 (run-tricky3-to-exit st h))) (pop-pc (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st))))))) (encapsulate () (local (defthm tricky3-spec-thm-temp (implies (and (good-tricky3-state st h) (equal (get-pc st) 200) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st h n))) h)) (equal (tricky3-spec st h) (run-tricky3-to-exit st h))) :hints (("Goal" :use (:instance tricky3-assertion-spec-induct (st0 st) (h0 h) (st1 st) (h1 h)) :in-theory (disable tricky3-assertion-spec-induct program-loaded-p RUN-TRICKY3-TO-EXIT-OPENER) :do-not-induct t)))) (defthm tricky3-spec-out (implies (and (tricky3-pre-out st0 h0 st1 h1) (equal (get-pc st0) 200) (equal-tricky3-cutpoints-p st0 h0 st1 h1) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st0 h0 n))) h0) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st1 h1 n))) h1)) (tricky3-post-out (tricky3-spec st0 h0) h0 (tricky3-spec st1 h1) h1)) :hints (("Goal" :in-theory (disable program-loaded-p RUN-TRICKY3-TO-EXIT-OPENER tricky3-post-out tricky3-spec) :do-not-induct t))) (defthm tricky3-spec-frame (implies (and (not (equal addr *output*)) (not (equal addr *temp*)) (not (equal addr *scratch*)) (not (equal addr *i*))) (equal (get-addr addr (tricky3-spec st h)) (get-addr addr st)))) (defthm tricky3-spec-pc (equal (get-pc (tricky3-spec st h)) (get-pc (pop-pc st)))) (defthm program-loaded-p-tricky3-spec (equal (program-loaded-p prog (tricky3-spec st h)) (program-loaded-p prog st))) (defthm get-program-tricky3-spec (equal (get-program (tricky3-spec st h)) (get-program st))) (defthm consp-get-pc-stack-tricky3-spec (equal (consp (get-pc-stack (tricky3-spec (push-pc pc st) h))) (consp (get-pc-stack st)))) (defthm len-get-pc-stack-tricky3-spec (implies (consp (get-pc-stack st)) (equal (len (get-pc-stack (tricky3-spec st h))) (+ -1 (len (get-pc-stack st)))))) (defthm tricky3-spec-thm (implies (and (good-tricky3-state st h) (equal (get-pc st) 200) (< (len (get-pc-stack (run-tricky3-to-exit-bounded st h n))) h)) (equal (run-tricky3-to-exit st h) (tricky3-spec st h)))) ) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; !!! As fo tricky1, we specify the cutpoints for main. (defun main-cutpoint-p (st h) (declare (ignore h)) (or (equal (get-pc st) 300) (equal (get-pc st) 306))) (defun equal-main-cutpoints-p (st0 h0 st1 h1) (declare (ignore h1)) (and (main-cutpoint-p st0 h0) (equal (get-pc st0) (get-pc st1)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Here are our step functions for main (encapsulate () (local (in-theory (enable nfix))) (defpun run-main-to-next-cutpoint (st h) (if (main-cutpoint-p st h) st (run-main-to-next-cutpoint (next st) h))) ) (defthm run-main-to-next-cutpoint-base (implies (main-cutpoint-p st h) (equal (run-main-to-next-cutpoint st h) st))) (defthm run-main-to-next-cutpoint-opener (implies (not (main-cutpoint-p st h)) (equal (run-main-to-next-cutpoint st h) (run-main-to-next-cutpoint (next st) h)))) (in-theory (disable run-main-to-next-cutpoint-def)) (encapsulate () (local (in-theory (enable nfix))) (defpun run-main-to-exit (st h) (if (equal (get-pc st) 306) st (run-main-to-exit (run-main-to-next-cutpoint (next st) h) h))) ) (defthm run-main-to-exit-base (implies (equal (get-pc st) 306) (equal (run-main-to-exit st h) st))) (defthm run-main-to-exit-opener (implies (not (equal (get-pc st) 306)) (equal (run-main-to-exit st h) (run-main-to-exit (run-main-to-next-cutpoint (next st) h) h)))) (in-theory (disable run-main-to-exit-def)) (defun run-main-to-exit-bounded (st h n) (declare (xargs :measure (nfix n) :hints (("Goal" :in-theory (enable nfix))))) (if (or (zp n) (equal (get-pc st) 306)) st (run-main-to-exit-bounded (run-main-to-next-cutpoint (next st) h) h (+ -1 n)))) (defthm run-main-to-exit-exits-if-run-main-to-exit-bounded-does (implies (equal (get-pc (run-main-to-exit-bounded st h n)) 306) (equal (get-pc (run-main-to-exit st h)) 306))) (defun run-main-to-exit-ind-1 (st0 h0 st1 h1 n) (if (zp n) (+ st0 h0 st1 h1) (run-main-to-exit-ind-1 st0 h0 (run-main-to-next-cutpoint (next st1) h1) h1 (+ -1 n)))) (defun run-main-to-exit-ind-2 (st0 h0 st1 h1 n) (if (zp n) (+ st0 h0 st1 h1) (run-main-to-exit-ind-2 (run-main-to-next-cutpoint (next st0) h0) h0 (run-main-to-next-cutpoint (next st1) h1) h1 (+ -1 n)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; !!! As for tricky1, we specify the information flow properties of ;;; main by a set of assertions on the cutpoints. Main, since there ;;; is no loop, requires only a pre-condition listing the dependencies ;;; for output and a post condition stating that the two values of ;;; output are equal. (defun main-pre-out (st0 h0 st1 h1) (and (good-main-state st0 h0) (good-main-state st1 h1) (equal (get-addr *flag* st0) (get-addr *flag* st1)) (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)))) (defun main-post-out (st0 h0 st1 h1) (declare (ignore h0 h1)) (equal (get-addr *output* st0) (get-addr *output* st1))) (defun main-assertions-out (st0 h0 st1 h1) (cond ((equal (get-pc st0) 300) (main-pre-out st0 h0 st1 h1)) ((equal (get-pc st0) 306) (main-post-out st0 h0 st1 h1)))) ;;; We want to keep tricky1 and tricky3 closed up, so that the spec ;;; functions and associated theorems we defined can be used. (in-theory (disable tricky1 (:executable-counterpart tricky1) tricky3 (:executable-counterpart tricky3) tricky1-spec tricky3-spec RUN-TRICKY1-TO-EXIT-OPENER RUN-TRICKY1-TO-EXIT-BASE RUN-TRICKY3-TO-EXIT-OPENER RUN-TRICKY3-TO-EXIT-BASE)) ;;; These two axioms state that tricky1 and tricky3 terminate in the ;;; context of main running to the next cutpoint. They seem pretty ;;; obviously true to me, and Sandip assures me that with a little ;;; rephrasing of some of the above they can be proven. (defaxiom run-main-to-next-cutpoint-tricky1 (implies (and (good-tricky1-state st (+ 1 h)) (equal (get-pc st) 100)) (equal (run-main-to-next-cutpoint st h) (run-main-to-next-cutpoint (run-tricky1-to-exit st (+ 1 h)) h)))) (defaxiom run-main-to-next-cutpoint-tricky3 (implies (and (good-tricky3-state st (+ 1 h)) (equal (get-pc st) 200)) (equal (run-main-to-next-cutpoint st h) (run-main-to-next-cutpoint (run-tricky3-to-exit st (+ 1 h)) h)))) (defmacro tricky1-terminates (st) `(< (LEN (GET-PC-STACK (RUN-TRICKY1-TO-EXIT-BOUNDED (PUSH-PC 100 (SET-PC 304 (SET-ADDR 4 0 (SET-ADDR 7 0 ,ST)))) (+ 1 (LEN (GET-PC-STACK ,ST))) N))) (+ 1 (LEN (GET-PC-STACK ,ST))))) (defmacro tricky3-terminates (st) `(< (LEN (GET-PC-STACK (RUN-TRICKY3-TO-EXIT-BOUNDED (PUSH-PC 200 (SET-PC 306 (SET-ADDR 4 0 (SET-ADDR 7 0 ,ST)))) (+ 1 (LEN (GET-PC-STACK ,ST))) N))) (+ 1 (LEN (GET-PC-STACK ,ST))))) (defmacro main-terminates (st h) `(equal (get-pc (run-main-to-next-cutpoint (next ,st) ,h)) 306)) ;;; The cutpoints for main remain in sync when we step from one to the ;;; next. (defthm equal-main-cutpoints-invariant-out (implies (and (equal-main-cutpoints-p st0 h0 st1 h1) (main-assertions-out st0 h0 st1 h1) (not (equal (get-pc st0) 306)) (tricky1-terminates st0) (tricky1-terminates st1) (tricky3-terminates st0) (tricky3-terminates st1)) (equal-main-cutpoints-p (run-main-to-next-cutpoint (next st0) h0) h0 (run-main-to-next-cutpoint (next st1) h1) h1))) ;;; The assertions hold as we step from one cutpoint to the next. The ;;; hints should be easy to automate with computed hints. (defthm main-assertion-out-invariant (implies (and (main-assertions-out st0 h0 st1 h1) (equal-main-cutpoints-p st0 h0 st1 h1) (not (equal (get-pc st0) 306)) (tricky1-terminates st0) (tricky1-terminates st1) (tricky3-terminates st0) (tricky3-terminates st1)) (main-assertions-out (run-main-to-next-cutpoint (next st0) h0) h0 (run-main-to-next-cutpoint (next st1) h1) h1)) :hints (("Goal" :in-theory (disable tricky1-spec-out tricky3-spec-out) :do-not '(generalize) :do-not-induct t :use ((:instance tricky3-spec-out (st0 (PUSH-PC 200 (SET-PC 306 (SET-ADDR 4 0 (SET-ADDR 7 0 ST0))))) (h0 (+ 1 (LEN (GET-PC-STACK ST0)))) (st1 (PUSH-PC 200 (SET-PC 306 (SET-ADDR 4 0 (SET-ADDR 7 0 ST1))))) (h1 (+ 1 (LEN (GET-PC-STACK ST1))))) (:instance tricky1-spec-out (st0 (PUSH-PC 100 (SET-PC 304 (SET-ADDR 4 0 (SET-ADDR 7 0 ST0))))) (h0 (+ 1 (LEN (GET-PC-STACK ST0)))) (st1 (PUSH-PC 100 (SET-PC 304 (SET-ADDR 4 0 (SET-ADDR 7 0 ST1))))) (h1 (+ 1 (LEN (GET-PC-STACK ST1))))))))) ;;; +++ As for tricky1-assertion-out-pre-post, this theorem states ;;; that the final value of output in main, depends only on the input ;;; values of low, n, and flag. The hypotheses that tricky1 and ;;; tricky3 terminate can be eliminated with a little more work at ;;; setting up the proper framework. This is exactly analogous to the ;;; situation in the more usual functional correctness proofs using ;;; compositional cutpoints which Sandip and Eric Smith have dealt ;;; with. ;;; Here is the more perspicuous version with main-pre-out and ;;; main-post-out expanded: #| (implies (and (equal (get-pc st0) 300) (equal (get-pc st1) 300) (good-main-state st0 h0) (good-main-state st1 h1) (equal (get-addr *flag* st0) (get-addr *flag* st1)) (equal (get-addr *low* st0) (get-addr *low* st1)) (equal (get-addr *n* st0) (get-addr *n* st1)) (tricky1-terminates st0) (tricky1-terminates st1) (tricky3-terminates st0) (tricky3-terminates st1) (main-terminates st0 h0) (main-terminates st1 h1)) (equal (get-addr *output* (run-main-to-exit st0 h0)) (get-addr *output* (run-main-to-exit st1 h1)))) |# (defthm main-out-pre-post (implies (and (equal (get-pc st0) 300) (equal (get-pc st1) 300) (main-pre-out st0 h0 st1 h1) (tricky1-terminates st0) (tricky1-terminates st1) (tricky3-terminates st0) (tricky3-terminates st1) (main-terminates st0 h0) (main-terminates st1 h1)) (main-post-out (run-main-to-exit st0 h0) h0 (run-main-to-exit st1 h1) h1)) :hints (("Goal" :use (:instance main-assertion-out-invariant) :in-theory (disable main-assertion-out-invariant main-pre-out main-post-out run-main-to-next-cutpoint-opener run-main-to-next-cutpoint-base next))) :otf-flg t) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; As for tricky1, we define a spec function for main, and prove some ;;; theorems about it. (defun main-pre-spec (st0 h0 st1 h1) (and (good-main-state st0 h0) (good-main-state st1 h1) (equal st0 st1))) (defun main-post-spec (st0 h0 st1 h1) (declare (ignore h0 h1)) (and (let ((st-spec (set-pc 306 (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st0))))))) (equal st-spec st1)))) (defun main-assertions-spec (st0 h0 st1 h1) (cond ((equal (get-pc st1) 306) (main-post-spec st0 h0 st1 h1)) ((equal (get-pc st1) 300) (main-pre-spec st0 h0 st1 h1)))) (defthm main-assertion-spec-invariant (implies (and (main-assertions-spec st0 h0 st1 h1) (not (equal (get-pc st1) 306)) (tricky1-terminates st0) (tricky1-terminates st1) (tricky3-terminates st0) (tricky3-terminates st1)) (main-assertions-spec st0 h0 (run-main-to-exit st1 h1) h1)) :hints (("Subgoal 15.2'" :in-theory (e/d (tricky1-spec tricky3-spec) (tricky1-spec-thm tricky3-spec-thm))) ("Subgoal 15.1'" :in-theory (e/d (tricky1-spec tricky3-spec) (tricky1-spec-thm tricky3-spec-thm)))) :otf-flg t) (defthm main-assertion-spec-pre-post (implies (and (EQUAL (GET-PC ST1) 300) (main-pre-spec st0 h0 st1 h1) (tricky1-terminates st0) (tricky1-terminates st1) (tricky3-terminates st0) (tricky3-terminates st1) (main-terminates st1 h1)) (main-post-spec st0 h0 (run-main-to-next-cutpoint (next st1) h1) h1)) :hints (("Goal" :use (:instance main-assertion-spec-invariant) :in-theory (disable main-assertion-spec-invariant main-pre-spec main-post-spec run-main-to-next-cutpoint-opener run-main-to-next-cutpoint-base next)))) (defun main-spec (st h) (let ((st1 (run-main-to-next-cutpoint (next st) h))) (set-pc 306 (set-addr *output* (get-addr *output* st1) (set-addr *temp* (get-addr *temp* st1) (set-addr *scratch* (get-addr *scratch* st1) (set-addr *i* (get-addr *i* st1) st))))))) (encapsulate () (local (defthm main-spec-thm-temp (implies (and (good-main-state st h) (equal (get-pc st) 300) (equal (get-pc (run-main-to-next-cutpoint (next st) h)) 306) (tricky1-terminates st) (tricky3-terminates st)) (equal (main-spec st h) (run-main-to-next-cutpoint (next st) h))) :hints (("Goal" :use (:instance main-assertion-spec-pre-post (st0 st) (h0 h) (st1 st) (h1 h)) :in-theory (disable main-assertion-spec-pre-post program-loaded-p run-main-to-next-cutpoint-OPENER) :do-not-induct t)))) (defthm main-spec-frame (implies (and (not (equal addr *output*)) (not (equal addr *temp*)) (not (equal addr *scratch*)) (not (equal addr *i*))) (equal (get-addr addr (main-spec st h)) (get-addr addr st)))) (defthm main-spec-thm (implies (and (good-main-state st h) (equal (get-pc st) 300) (tricky1-terminates st) (tricky3-terminates st) (main-terminates st h)) (equal (run-main-to-exit st h) (main-spec st h)))) ) ;;; +++ Our final theorem. Main changes only the values of output, ;;; temp, scratch. and i. Thus we have not missed any hidden channels ;;; of information flow. (defthm main-frame (implies (and (good-main-state st h) (equal (get-pc st) 300) (not (equal addr *output*)) (not (equal addr *temp*)) (not (equal addr *scratch*)) (not (equal addr *i*)) (tricky1-terminates st) (tricky3-terminates st) (main-terminates st h)) (equal (get-addr addr (run-main-to-exit st h)) (get-addr addr st))))