		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Exec-of-dead

Correctness theorems of the execution functions.

As mentioned earlier, the main theorems are proved by mutual execution, using the flag approach.

The current proof uses some :use and :expand hints for certain cases of the induction proof. For robustness and efficiency, we prefer to apply these hints only to those cases. (In earlier version of this proof, which was more complex at the time, attempting to apply these hints to all cases uniformly caused the proof to be too slow, if it worked at all, presumably due to many unnecessary case splits.) There may be actually ways to avoid the :use hints, by proving and enabling suitable rules. It is less clear whether the :expand hints could be avoided, given that the functions in question are already enabled, but ACL2's heuristics prevent their expansion, even though forcing the expand with the :expand hints leads to a successful proof in the end. Perhaps they might be applied uniformly to all subgoals, but this may cause proof brittleness or inefficiency. Thus, limiting these :use and :expand hints to the needed cases seems to be the right thing at this moment.

To avoid the brittleness and unreadability of subgoal hints, we use computed hints to robustly and readably designate the proof cases to which specific hints must apply. We do that with the function below, which uses two macros for conciseness. The proof cases are denoted based on the flag value and possibly the kind of statement; these are expressed in terms of occurrences of terms in the clauses.

We locally enable, for all subgoals, the execution functions, the transformation functions, and the no-function-definition predicates. We also enable the equivalence relations, since we always want to expand them in the proofs. And we enable some additional rules, motivated by the arising subgoals. Note that, if we put these enablements into a goal hint, they would not apply to subgoals where computed hints apply; this is why we locally enable them instead.

Definitions and Theorems

Function: exec-of-dead-hints

(defun exec-of-dead-hints (id clause world)
 (declare (ignore id world))
 (cond
  ((exec-of-dead-flag-is exec-statement)
   (and (or (exec-of-dead-stmt-kind-is :if)
            (exec-of-dead-stmt-kind-is :for)
            (exec-of-dead-stmt-kind-is :switch))
        '(:expand ((exec-statement stmt cstate funenv limit)
                   (statement-dead stmt)))))
  ((exec-of-dead-flag-is exec-statement-list)
   '(:in-theory
         (disable statement-kind-when-mode-regular)
         :use (:instance statement-kind-when-mode-regular
                         (stmt (car stmts))
                         (limit (1- limit)))
         :expand (exec-statement-list (statement-list-dead stmts)
                                      cstate (funenv-dead funenv)
                                      limit)))
  ((exec-of-dead-flag-is exec-block)
   '(:expand (exec-block block cstate funenv limit)))
  ((exec-of-dead-flag-is exec-switch-rest)
   '(:expand
         ((block-option-dead default)
          (block-option-nofunp default)
          (exec-switch-rest cases
                            default target cstate funenv limit))))))

Theorem: exec-expression-of-dead

(defthm exec-expression-of-dead
  (implies (funenv-nofunp funenv)
           (eoutcome-result-okeq
                (exec-expression expr cstate (funenv-dead funenv)
                                 limit)
                (exec-expression expr cstate funenv limit))))

Theorem: exec-expression-list-of-dead

(defthm exec-expression-list-of-dead
  (implies
       (funenv-nofunp funenv)
       (eoutcome-result-okeq
            (exec-expression-list exprs cstate (funenv-dead funenv)
                                  limit)
            (exec-expression-list exprs cstate funenv limit))))

Theorem: exec-funcall-of-dead

(defthm exec-funcall-of-dead
  (implies (funenv-nofunp funenv)
           (eoutcome-result-okeq
                (exec-funcall call cstate (funenv-dead funenv)
                              limit)
                (exec-funcall call cstate funenv limit))))

Theorem: exec-function-of-dead

(defthm exec-function-of-dead
  (implies (funenv-nofunp funenv)
           (eoutcome-result-okeq
                (exec-function fun args cstate (funenv-dead funenv)
                               limit)
                (exec-function fun args cstate funenv limit))))

Theorem: exec-statement-of-dead

(defthm exec-statement-of-dead
 (implies
  (and (statement-nofunp stmt)
       (funenv-nofunp funenv))
  (soutcome-result-okeq (exec-statement (statement-dead stmt)
                                        cstate (funenv-dead funenv)
                                        limit)
                        (exec-statement stmt cstate funenv limit))))

Theorem: exec-statement-list-of-dead

(defthm exec-statement-list-of-dead
  (implies (and (statement-list-nofunp stmts)
                (funenv-nofunp funenv))
           (soutcome-result-okeq
                (exec-statement-list (statement-list-dead stmts)
                                     cstate (funenv-dead funenv)
                                     limit)
                (exec-statement-list stmts cstate funenv limit))))

Theorem: exec-block-of-dead

(defthm exec-block-of-dead
 (implies
     (and (block-nofunp block)
          (funenv-nofunp funenv))
     (soutcome-result-okeq (exec-block (block-dead block)
                                       cstate (funenv-dead funenv)
                                       limit)
                           (exec-block block cstate funenv limit))))

Theorem: exec-for-iterations-of-dead

(defthm exec-for-iterations-of-dead
 (implies
  (and (block-nofunp update)
       (block-nofunp body)
       (funenv-nofunp funenv))
  (soutcome-result-okeq
       (exec-for-iterations test (block-dead update)
                            (block-dead body)
                            cstate (funenv-dead funenv)
                            limit)
       (exec-for-iterations test update body cstate funenv limit))))

Theorem: exec-switch-rest-of-dead

(defthm exec-switch-rest-of-dead
  (implies
       (and (swcase-list-nofunp cases)
            (block-option-nofunp default)
            (funenv-nofunp funenv))
       (soutcome-result-okeq
            (exec-switch-rest (swcase-list-dead cases)
                              (block-option-dead default)
                              target cstate (funenv-dead funenv)
                              limit)
            (exec-switch-rest cases
                              default target cstate funenv limit))))