Generate the theorem saying that looking up a certain C function in the function environment yields the information for that function.
(atc-gen-cfun-fun-env-thm fn thm-name prog-const finfo init-fun-env-thm) → event
This serves to speed up the proofs when there is a large number of functions involved. A previous version of ATC was generating proofs that were executing function lookups, which worked fine for small C programs, but was slow for larger C programs.
Function:
(defun atc-gen-cfun-fun-env-thm (fn thm-name prog-const finfo init-fun-env-thm) (declare (xargs :guard (and (symbolp fn) (symbolp thm-name) (symbolp prog-const) (fun-infop finfo) (symbolp init-fun-env-thm)))) (let ((__function__ 'atc-gen-cfun-fun-env-thm)) (declare (ignorable __function__)) (b* ((fn-name (symbol-name fn)) (formula (cons 'equal (cons (cons 'fun-env-lookup (cons (cons 'ident (cons fn-name 'nil)) (cons (cons 'init-fun-env (cons (cons 'preprocess (cons prog-const 'nil)) 'nil)) 'nil))) (cons (cons 'quote (cons finfo 'nil)) 'nil)))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons '(:e fun-env-lookup) (cons '(:e ident) (cons init-fun-env-thm 'nil))) 'nil)) 'nil))) 'nil)) ((mv event &) (evmac-generate-defthm thm-name :formula formula :hints hints :enable nil))) event)))
Theorem:
(defthm pseudo-event-formp-of-atc-gen-cfun-fun-env-thm (b* ((event (atc-gen-cfun-fun-env-thm fn thm-name prog-const finfo init-fun-env-thm))) (pseudo-event-formp event)) :rule-classes :rewrite)