Theorems about modes for the static soundness proof.
Values of rnumeration fixtype like mode are usually compared via their kinds (i.e. mode-kind), rather than directly; the fixtype definition macros in fact generate theorems to this effect, along with useful theorems such as the forward chaining rule that mode-kind is one of four known possibilities.
However, our ACL2 static safety checking functions return sets of modes (for statements, blocks, and other constructs), and the static soundness theorems say that the mode returned by the ACL2 execution functions are in those sets. This set membership formulation does not blend well with the kind-centric treatment of modes. Thus, here we introduce theorems that turn kind comparisons into mode comparisons. Because some of the theorems about kinds no longer apply, we also need to add some similar theorems for modes, and certain explicit non-equality theorems.
This is not very satisfactory. There may be a way to avoid all of this, and somehow handle mode kinds with set membership well.
Theorem:
(defthm equal-of-mode-kind-continue (implies (modep mode) (equal (equal (mode-kind mode) :continue) (equal mode (mode-continue)))))
Theorem:
(defthm equal-of-mode-kind-break (implies (modep mode) (equal (equal (mode-kind mode) :break) (equal mode (mode-break)))))
Theorem:
(defthm equal-of-mode-kind-regular (implies (modep mode) (equal (equal (mode-kind mode) :regular) (equal mode (mode-regular)))))
Theorem:
(defthm equal-of-mode-kind-leave (implies (modep mode) (equal (equal (mode-kind mode) :leave) (equal mode (mode-leave)))))
Theorem:
(defthm mode-regular-not-continue (not (equal (mode-regular) (mode-continue))))
Theorem:
(defthm mode-regular-not-break (not (equal (mode-regular) (mode-break))))
Theorem:
(defthm mode-leave-not-continue (not (equal (mode-leave) (mode-continue))))
Theorem:
(defthm mode-leave-not-break (not (equal (mode-leave) (mode-break))))
Theorem:
(defthm mode-leave-if-not-regular/continue/break (implies (and (modep mode) (not (equal mode (mode-regular))) (not (equal mode (mode-continue))) (not (equal mode (mode-break)))) (equal (equal mode (mode-leave)) t)))
Theorem:
(defthm mode-possibilities (implies (modep x) (or (equal x (mode-regular)) (equal x (mode-leave)) (equal x (mode-break)) (equal x (mode-continue)))))
Theorem:
(defthm soutcome->mode-regular-lemma (implies (and (in (soutcome->mode outcome) modes) (not (equal (soutcome->mode outcome) (mode-break))) (not (equal (soutcome->mode outcome) (mode-continue))) (not (in (mode-leave) modes))) (equal (soutcome->mode outcome) (mode-regular))))