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).
Theorem:
(defthm exec-stmt-when-compound (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :compound) (not (zp limit)) (equal val?+compst1 (exec-block-item-list (stmt-compound->items s) (enter-scope compst) fenv (1- limit))) (equal val? (mv-nth 0 val?+compst1)) (equal compst1 (mv-nth 1 val?+compst1)) (value-optionp val?)) (equal (exec-stmt s compst fenv limit) (mv val? (exit-scope compst1)))))
Theorem:
(defthm exec-stmt-when-expr (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :expr) (not (zp limit)) (equal compst1 (exec-expr-call-or-asg (stmt-expr->get s) compst fenv (1- limit))) (compustatep compst1)) (equal (exec-stmt s compst fenv limit) (mv nil compst1))))
Theorem:
(defthm exec-stmt-when-if (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :if) (not (zp limit)) (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 nil compst)))))
Theorem:
(defthm exec-stmt-when-if-and-true (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :if) (not (zp limit)) (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:
(defthm exec-stmt-when-if-and-false (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :if) (not (zp limit)) (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 nil compst))))
Theorem:
(defthm exec-stmt-when-ifelse (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :ifelse) (not (zp limit)) (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:
(defthm exec-stmt-when-ifelse-and-true (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :ifelse) (not (zp limit)) (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:
(defthm exec-stmt-when-ifelse-and-false (implies (and (syntaxp (quotep s)) (equal (stmt-kind s) :ifelse) (not (zp limit)) (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:
(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:
(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 val+compst1 (exec-expr-call-or-pure e compst fenv (1- limit))) (equal val (mv-nth 0 val+compst1)) (equal compst1 (mv-nth 1 val+compst1)) (valuep val)) (equal (exec-stmt s compst fenv limit) (mv val compst1))))