diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:54:40 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:54:40 +0100 |
| commit | 7d3ac44ff5b909a6d00a94e6d30748e15054daf5 (patch) | |
| tree | 622ad729db551e1a5d2485e23220bfd7dc1154f8 /backend/ForwardMovesproof.v | |
| parent | b8823bfa481e4322e809d600624c59634447ec4d (diff) | |
| download | compcert-kvx-7d3ac44ff5b909a6d00a94e6d30748e15054daf5.tar.gz compcert-kvx-7d3ac44ff5b909a6d00a94e6d30748e15054daf5.zip | |
FINISHED the forward-moves pass
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 8c036851..826d4250 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -475,7 +475,11 @@ Proof. apply move_ok. assumption. } - admit. + rewrite KILL in GE. + apply get_rb_sem_ge with (rb2 := Some (kill res mpc)). + assumption. + apply kill_ok. + assumption. (* load *) - econstructor; split. @@ -762,7 +766,7 @@ Proof. destruct (map # pc) as [mpc |] in *; try contradiction. destruct H8 as [rel' RGE]. eapply get_rb_killed; eauto. -Admitted. +Qed. Lemma transf_initial_states: |