Rules for exec-fun.
The proofs generated by ATC are modularized so that there is one theorem per non-recursive target function. So we generally do not expand calls of exec-fun, except in the theorem for the function in question. We rely on the fact that the correctness theorems for the functions called by the function in question come after the following rule in the ACL2 history (because they are generated by ATC as part of the generated events), and thus take precedence over this rule: in other words, given theorems for the called functions, this rule is expected to apply only on the function in question, i.e. the one whose correctness theorem is being proved. Note that these theorems are generated only for non-recursive functions; the recursive functions represent loops, and their correctness theorems do not involve exec-fun.
Theorem:
(defthm exec-fun-open (implies (and (not (zp limit)) (equal info (fun-env-lookup fun fenv)) info (equal scope (init-scope (fun-info->params info) args)) (scopep scope) (equal val?+compst1 (exec-block-item-list (fun-info->body info) (push-frame (make-frame :function fun :scopes (list scope)) compst) fenv (1- limit))) (equal val? (mv-nth 0 val?+compst1)) (equal compst1 (mv-nth 1 val?+compst1)) (value-optionp val?) (equal (type-of-value-option val?) (tyname-to-type (fun-info->result info)))) (equal (exec-fun fun args compst fenv limit) (mv val? (pop-frame compst1)))))