diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
| commit | 9cf4ca7760982b40e5721b2d6510eae0ced248a8 (patch) | |
| tree | 78bb00e9705d690f4b567268330c8f47f0a2751d /backend/CSE3analysisproof.v | |
| parent | 33c7fc589ebbbd0ebda9739c479bbd9ee7e526db (diff) | |
| download | compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.tar.gz compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.zip | |
forward_move_l
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b14f3964..027a874a 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -277,6 +277,8 @@ Section SOUNDNESS. assumption. Qed. + Hint Resolve kill_reg_sound : cse3. + Lemma pick_source_sound : forall (l : list reg), match pick_source l with @@ -289,6 +291,8 @@ Section SOUNDNESS. left; trivial. Qed. + Hint Resolve pick_source_sound : cse3. + Theorem forward_move_sound : forall rel rs m x, (sem_rel rel rs m) -> @@ -323,6 +327,20 @@ Section SOUNDNESS. intuition congruence. Qed. + Hint Resolve forward_move_sound : cse3. + + Theorem forward_move_l_sound : + forall rel rs m l, + (sem_rel rel rs m) -> + rs ## (forward_move_l (ctx := ctx) rel l) = rs ## l. + Proof. + induction l; simpl; intros; trivial. + erewrite forward_move_sound by eassumption. + intuition congruence. + Qed. + + Hint Resolve forward_move_l_sound : cse3. + Theorem kill_mem_sound : forall rel rs m m', (sem_rel rel rs m) -> @@ -353,4 +371,6 @@ Section SOUNDNESS. intuition. congruence. Qed. + + Hint Resolve kill_mem_sound : cse3. End SOUNDNESS. |