Main static soundness theorems.
These are about the mutually recursive execution functions. Each theorem says that if the static safety checks succeed, with respect to the variable table for computation state and the function table for the function environment, if the function environment is safe, and if the execution function does not return a limit error, then the execution function does not return an error, and the outcome is consistent with the result of the safety checks: for expressions, the number of values matches the calculated number; for statements (and blocks etc.), the mode is in the calculated set.
We currently have an undesired lemma that is somewhat specific to one of the arising subgoals. We plan to look into avoiding this.
The hints for the main inductive theorem mainly consist in
enabling certain functions and theorems.
We obviously enable the execution and checking functions;
unfortunately we also need an
As is often the case,
the proof also makes implicit use of enabled-by-default rules.
Some are theorems that relate static and dynamic counterparts.
We also remark the use of the
Theorem:
(defthm exec-statement-list-cstate-to-vars-lemma (implies (and (not (reserrp (add-funs (statements-to-fundefs stmts) funenv))) (not (reserrp (exec-statement-list stmts cstate (add-funs (statements-to-fundefs stmts) funenv) limit)))) (equal (intersect (cstate-to-vars cstate) (cstate-to-vars (soutcome->cstate (exec-statement-list stmts cstate (add-funs (statements-to-fundefs stmts) funenv) limit)))) (cstate-to-vars cstate))))
Theorem:
(defthm exec-expression-static-soundness (b* ((results (check-safe-expression expr (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-expression expr cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp results)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)) (equal (len (eoutcome->values outcome)) results)))))
Theorem:
(defthm exec-expression-list-static-soundness (b* ((results (check-safe-expression-list exprs (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-expression-list exprs cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp results)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)) (equal (len (eoutcome->values outcome)) results)))))
Theorem:
(defthm exec-funcall-static-soundness (b* ((results (check-safe-funcall call (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-funcall call cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp results)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)) (equal (len (eoutcome->values outcome)) results)))))
Theorem:
(defthm exec-function-static-soundness (b* ((ftype (get-funtype fun (funenv-to-funtable funenv))) (outcome (exec-function fun args cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp ftype)) (equal (len args) (funtype->in ftype)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (eoutcome->cstate outcome)) (cstate-to-vars cstate)) (equal (len (eoutcome->values outcome)) (funtype->out ftype))))))
Theorem:
(defthm exec-statement-static-soundness (b* ((varsmodes (check-safe-statement stmt (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-statement stmt cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp varsmodes)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (vars+modes->vars varsmodes)) (in (soutcome->mode outcome) (vars+modes->modes varsmodes))))))
Theorem:
(defthm exec-statement-list-static-soundness (b* ((varsmodes (check-safe-statement-list stmts (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-statement-list stmts cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp varsmodes)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (if (equal (soutcome->mode outcome) (mode-regular)) (equal (cstate-to-vars (soutcome->cstate outcome)) (vars+modes->vars varsmodes)) (subset (cstate-to-vars (soutcome->cstate outcome)) (vars+modes->vars varsmodes))) (in (soutcome->mode outcome) (vars+modes->modes varsmodes))))))
Theorem:
(defthm exec-block-static-soundness (b* ((modes (check-safe-block block (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-block block cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp modes)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (cstate-to-vars cstate)) (in (soutcome->mode outcome) modes)))))
Theorem:
(defthm exec-for-iterations-static-soundness (b* ((test-results (check-safe-expression test (cstate-to-vars cstate) (funenv-to-funtable funenv))) (update-modes (check-safe-block update (cstate-to-vars cstate) (funenv-to-funtable funenv))) (body-modes (check-safe-block body (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-for-iterations test update body cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp test-results)) (equal test-results 1) (not (reserrp update-modes)) (not (in (mode-break) update-modes)) (not (in (mode-continue) update-modes)) (not (reserrp body-modes)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (cstate-to-vars cstate)) (in (soutcome->mode outcome) (difference (insert (mode-regular) (union body-modes update-modes)) (insert (mode-break) (insert (mode-continue) nil))))))))
Theorem:
(defthm exec-switch-rest-static-soundness (b* ((cases-modes (check-safe-swcase-list cases (cstate-to-vars cstate) (funenv-to-funtable funenv))) (default-modes (check-safe-block-option default (cstate-to-vars cstate) (funenv-to-funtable funenv))) (outcome (exec-switch-rest cases default target cstate funenv limit))) (implies (and (funenv-safep funenv) (not (reserrp cases-modes)) (not (reserrp default-modes)) (not (reserr-limitp outcome))) (and (not (reserrp outcome)) (equal (cstate-to-vars (soutcome->cstate outcome)) (cstate-to-vars cstate)) (in (soutcome->mode outcome) (union cases-modes default-modes))))))