diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:50:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:50:12 +0100 |
| commit | b8823bfa481e4322e809d600624c59634447ec4d (patch) | |
| tree | 7fdae9ce92102db321c6a91e15890cf86ea86ce3 /backend/ForwardMovesproof.v | |
| parent | a8dd20cd96a1c8636add5b8b45b6ee5ff5982f9a (diff) | |
| download | compcert-kvx-b8823bfa481e4322e809d600624c59634447ec4d.tar.gz compcert-kvx-b8823bfa481e4322e809d600624c59634447ec4d.zip | |
nearly done
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index b1425401..8c036851 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -468,10 +468,12 @@ Proof. subst args. rewrite MOVE in GE. simpl in H0. - destruct (map # pc') as [mpc' | ] in *; try discriminate. simpl in GE. - admit. - admit. + apply get_rb_sem_ge with (rb2 := Some (move src res mpc)). + assumption. + replace v with (rs # src) by congruence. + apply move_ok. + assumption. } admit. |