Theorems about restricting variables and variable renaming.
The function restrict-vars is used, in the Yul dynamic semantics, to model the execution of blocks and the execution of loops. These theorems about restrict-vars apply to these two cases, as explained below.
In the execution of a block,
there are three computation states of interest:
(i) the state before the block;
(ii) the state after executing the statements of the block; and
(iii) the state after the block,
obtained from the second one by restricting it
to the variables present in the first one.
Consider the execution of two blocks related by variable renaming:
then there are corresponding first, second, and third states.
If the first states are related,
and the second states are related,
and the keys of each second state is a superset of
the keys of the first state,
then the third states are related too.
The theorem
In the execution of a loop,
there are four computation states of interest:
(i) the state before the loop;
(ii) the state after executing the initialization block;
(ii) the state after execution the loop iterations; and
(iv) the state after the loop.
The theorem
Theorem:
(defthm lstate-renamevarp-of-restrict-1 (implies (and (lstatep old-lstate) (lstatep new-lstate) (lstate-renamevarp old-lstate new-lstate ren) (lstatep old-lstate1) (lstatep new-lstate1) (lstate-renamevarp old-lstate1 new-lstate1 ren1) (subset (omap::keys old-lstate) (omap::keys old-lstate1)) (subset (omap::keys new-lstate) (omap::keys new-lstate1)) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (b* ((old-lstate2 (omap::restrict (omap::keys old-lstate) old-lstate1)) (new-lstate2 (omap::restrict (omap::keys new-lstate) new-lstate1))) (lstate-renamevarp old-lstate2 new-lstate2 ren))))
Theorem:
(defthm cstate-renamevarp-of-restrict-vars-1 (implies (and (cstate-renamevarp old-cstate new-cstate ren) (cstate-renamevarp old-cstate1 new-cstate1 ren1) (subset (omap::keys (cstate->local old-cstate)) (omap::keys (cstate->local old-cstate1))) (subset (omap::keys (cstate->local new-cstate)) (omap::keys (cstate->local new-cstate1))) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (b* ((old-cstate2 (restrict-vars (omap::keys (cstate->local old-cstate)) old-cstate1)) (new-cstate2 (restrict-vars (omap::keys (cstate->local new-cstate)) new-cstate1))) (cstate-renamevarp old-cstate2 new-cstate2 ren))))
Theorem:
(defthm lstate-renamevarp-of-restrict-2 (implies (and (lstatep old-lstate) (lstatep new-lstate) (lstate-renamevarp old-lstate new-lstate ren) (lstatep old-lstate1) (lstatep new-lstate1) (lstate-renamevarp old-lstate1 new-lstate1 ren1) (lstatep old-lstate2) (lstatep new-lstate2) (lstate-renamevarp old-lstate2 new-lstate2 ren1) (subset (omap::keys old-lstate) (omap::keys old-lstate1)) (subset (omap::keys new-lstate) (omap::keys new-lstate1)) (equal (omap::keys old-lstate2) (omap::keys old-lstate1)) (equal (omap::keys new-lstate2) (omap::keys new-lstate1)) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (b* ((old-lstate3 (omap::restrict (omap::keys old-lstate) old-lstate2)) (new-lstate3 (omap::restrict (omap::keys new-lstate) new-lstate2))) (lstate-renamevarp old-lstate3 new-lstate3 ren))))
Theorem:
(defthm cstate-renamevarp-of-restrict-vars-2 (implies (and (cstate-renamevarp old-cstate new-cstate ren) (cstate-renamevarp old-cstate1 new-cstate1 ren1) (cstate-renamevarp old-cstate2 new-cstate2 ren1) (subset (omap::keys (cstate->local old-cstate)) (omap::keys (cstate->local old-cstate1))) (subset (omap::keys (cstate->local new-cstate)) (omap::keys (cstate->local new-cstate1))) (equal (omap::keys (cstate->local old-cstate2)) (omap::keys (cstate->local old-cstate1))) (equal (omap::keys (cstate->local new-cstate2)) (omap::keys (cstate->local new-cstate1))) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (b* ((old-cstate3 (restrict-vars (omap::keys (cstate->local old-cstate)) old-cstate2)) (new-cstate3 (restrict-vars (omap::keys (cstate->local new-cstate)) new-cstate2))) (cstate-renamevarp old-cstate3 new-cstate3 ren))))