Robert Krug, Jan. 2008 I. What is info flow? x := a + b; forward: a and b affect x backward: x is affected by a and b II. Why do we care? Want to make sure that secret information does not leak out. III. General form of theorem. (implies (and (at-entry st1) (at-entry st2) (equal (a st1) (a st2)) (equal (b st1) (b st2))) (equal (x (run st1)) (x (run st2)))) Two states --- if affecting variables are same, affected variables are same. Think of (a st) as a macro, say (access 107 st). IV. Pointers. *p1 := *p1 + 1; *p2 := *p2 + 2; p1 := p2; Dependencies must be in terms of initial values. If final values used, no way to state that the location pointed to by the initial value of p1 was changed. single path: (implies (and (at-entry st1) (at-entry st2) (equal (p1 st1) (p1 st2)) (equal (access (p1 st1) st1) (access (p1 st1) st2)) (equal (access (p1 st1) (run st1)) (access (p1 st1) (run st2)))) or two path: (implies (and (at-entry st1) (at-entry st2) (equal (access (p1 st1) st1) (access (p1 st2) st2))) (equal (access (p1 st1) (run st1)) (access (p1 st2) (run st2)))) Some people like single path --- requires memory layout to be same in both states. Here, *p1 depends on p1 and *p1. Some people like two path --- less restrictive. Here, *p1 depends only on *p1. I believe that the two path version is easier to work with, but preferances may be more a matter of taste than logic. V. Compositional cutpoints --- A method for structuring the proof of a theorem about running a machine. Identify a set of PCs (or cutpoints) --- typically entry, exit, and one for each loop. Attach conditions at each cutpoint --- entry: precondition, exit: postcondition, and loops: loop invariants such that: (implies (and (at-cutpoint-p st) (condition-holds-p (get-condition st) st)) (condition-holds-p (get-condition (run-to-next-cutpoint st)) (run-to-next-cutpoint st))) (We assume termination) After proving the above, we can functionally instantiate (implies (and (at-entry st) (pre-condition st)) (post-condition (run st))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (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 ever depend 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; } int output; main (int high, low, n, flag) { output = 0; if flag < 0 { tricky1(high, low, n); } else { tricky3(high, low, n); } 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. ;;; Exit must go first, so that when we exit we do not consider the ;;; case that we have popped back to the entry or exit again. ;;; ??? 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 entry or exit 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. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; !!! As for 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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; !!! 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))))