		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-stmt-rules

Rules for exec-stmt.

Besides the rules for the large symbolic execution, whose names we put into the constant defined at the end, we also prove rules used in the new modular proofs. The latter rules avoid if in the right side, to avoid unwanted case splits; furthermore, they wrap the if tests into test* to prevent unwanted rewrites (see atc-contextualize).

Definitions and Theorems

Theorem: exec-stmt-when-compound

(defthm exec-stmt-when-compound
 (implies (and (syntaxp (quotep s))
               (equal (stmt-kind s) :compound)
               (not (zp limit))
               (equal sval+compst1
                      (exec-block-item-list (stmt-compound->items s)
                                            (enter-scope compst)
                                            fenv (1- limit)))
               (equal sval (mv-nth 0 sval+compst1))
               (equal compst1 (mv-nth 1 sval+compst1))
               (stmt-valuep sval))
          (equal (exec-stmt s compst fenv limit)
                 (mv sval (exit-scope compst1)))))

Theorem: exec-stmt-when-expr

(defthm exec-stmt-when-expr
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :expr)
                (not (zp limit))
                (equal eval?+compst1
                       (exec-expr (stmt-expr->get s)
                                  compst fenv (1- limit)))
                (equal eval? (mv-nth 0 eval?+compst1))
                (equal compst1 (mv-nth 1 eval?+compst1))
                (expr-value-optionp eval?))
           (equal (exec-stmt s compst fenv limit)
                  (mv (stmt-value-none) compst1))))

Theorem: exec-stmt-when-if

(defthm exec-stmt-when-if
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :if)
                (expr-purep (stmt-if->test s))
                (integerp limit)
                (>= limit
                    (1+ (expr-pure-limit (stmt-if->test s))))
                (compustatep compst)
                (equal arg1
                       (exec-expr-pure (stmt-if->test s)
                                       compst))
                (expr-valuep arg1)
                (equal carg1 (apconvert-expr-value arg1))
                (expr-valuep carg1)
                (equal test
                       (test-value (expr-value->value carg1)))
                (booleanp test))
           (equal (exec-stmt s compst fenv limit)
                  (if test (exec-stmt (stmt-if->then s)
                                      compst fenv (1- limit))
                    (mv (stmt-value-none) compst)))))

Theorem: exec-stmt-when-if-and-true

(defthm exec-stmt-when-if-and-true
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :if)
                (expr-purep (stmt-if->test s))
                (integerp limit)
                (>= limit
                    (1+ (expr-pure-limit (stmt-if->test s))))
                (compustatep compst)
                (equal arg1
                       (exec-expr-pure (stmt-if->test s)
                                       compst))
                (expr-valuep arg1)
                (equal carg1 (apconvert-expr-value arg1))
                (expr-valuep carg1)
                (equal test
                       (test-value (expr-value->value carg1)))
                (booleanp test)
                (test* test))
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt (stmt-if->then s)
                             compst fenv (1- limit)))))

Theorem: exec-stmt-when-if-and-false

(defthm exec-stmt-when-if-and-false
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :if)
                (expr-purep (stmt-if->test s))
                (integerp limit)
                (>= limit
                    (1+ (expr-pure-limit (stmt-if->test s))))
                (compustatep compst)
                (equal arg1
                       (exec-expr-pure (stmt-if->test s)
                                       compst))
                (expr-valuep arg1)
                (equal carg1 (apconvert-expr-value arg1))
                (expr-valuep carg1)
                (equal test
                       (test-value (expr-value->value carg1)))
                (booleanp test)
                (test* (not test)))
           (equal (exec-stmt s compst fenv limit)
                  (mv (stmt-value-none) compst))))

Theorem: exec-stmt-when-ifelse

(defthm exec-stmt-when-ifelse
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :ifelse)
                (expr-purep (stmt-ifelse->test s))
                (integerp limit)
                (>= limit
                    (1+ (expr-pure-limit (stmt-ifelse->test s))))
                (equal arg1
                       (exec-expr-pure (stmt-ifelse->test s)
                                       compst))
                (expr-valuep arg1)
                (equal carg1 (apconvert-expr-value arg1))
                (expr-valuep carg1)
                (equal test
                       (test-value (expr-value->value carg1)))
                (booleanp test))
           (equal (exec-stmt s compst fenv limit)
                  (if test (exec-stmt (stmt-ifelse->then s)
                                      compst fenv (1- limit))
                    (exec-stmt (stmt-ifelse->else s)
                               compst fenv (1- limit))))))

Theorem: exec-stmt-when-ifelse-and-true

(defthm exec-stmt-when-ifelse-and-true
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :ifelse)
                (expr-purep (stmt-ifelse->test s))
                (integerp limit)
                (>= limit
                    (1+ (expr-pure-limit (stmt-ifelse->test s))))
                (equal arg1
                       (exec-expr-pure (stmt-ifelse->test s)
                                       compst))
                (expr-valuep arg1)
                (equal carg1 (apconvert-expr-value arg1))
                (expr-valuep carg1)
                (equal test
                       (test-value (expr-value->value carg1)))
                (booleanp test)
                (test* test))
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt (stmt-ifelse->then s)
                             compst fenv (1- limit)))))

Theorem: exec-stmt-when-ifelse-and-false

(defthm exec-stmt-when-ifelse-and-false
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :ifelse)
                (expr-purep (stmt-ifelse->test s))
                (integerp limit)
                (>= limit
                    (1+ (expr-pure-limit (stmt-ifelse->test s))))
                (equal arg1
                       (exec-expr-pure (stmt-ifelse->test s)
                                       compst))
                (expr-valuep arg1)
                (equal carg1 (apconvert-expr-value arg1))
                (expr-valuep carg1)
                (equal test
                       (test-value (expr-value->value carg1)))
                (booleanp test)
                (test* (not test)))
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt (stmt-ifelse->else s)
                             compst fenv (1- limit)))))

Theorem: exec-stmt-when-while

(defthm exec-stmt-when-while
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :while)
                (not (zp limit)))
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt-while (stmt-while->test s)
                                   (stmt-while->body s)
                                   compst fenv (1- limit)))))

Theorem: exec-stmt-when-return

(defthm exec-stmt-when-return
  (implies (and (syntaxp (quotep s))
                (equal (stmt-kind s) :return)
                (not (zp limit))
                (equal e (stmt-return->value s))
                e
                (equal eval+compst1
                       (exec-expr e compst fenv (1- limit)))
                (equal eval (mv-nth 0 eval+compst1))
                (equal compst1 (mv-nth 1 eval+compst1))
                (expr-valuep eval)
                (equal eval1 (apconvert-expr-value eval))
                (expr-valuep eval1)
                (equal val (expr-value->value eval1)))
           (equal (exec-stmt s compst fenv limit)
                  (mv (stmt-value-return val) compst1))))