diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 12:41:28 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 12:41:28 +0100 |
| commit | 935dcae6384e718d26d29377e4c50e53151809e4 (patch) | |
| tree | 7f01f1f8f03101c8e99f0fc68becd183d7d54378 /backend/CSE3analysisproof.v | |
| parent | a3be6358778bb02b03b62486a60b9fd9ef1f1c04 (diff) | |
| download | compcert-kvx-935dcae6384e718d26d29377e4c50e53151809e4.tar.gz compcert-kvx-935dcae6384e718d26d29377e4c50e53151809e4.zip | |
store sound
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f5dd7bf9..05c7a8f3 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -689,5 +689,23 @@ Section SOUNDNESS. eauto. Qed. - Hint Resolve store2_sound : cse3. + Hint Resolve store1_sound : cse3. + + Theorem store_sound: + forall no chunk addr args a src rel tenv rs m m', + sem_rel rel rs m -> + wt_regset tenv rs -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs#src) = Some m' -> + sem_rel (store (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store. + intros until m'. + intros REL WT ADDR STORE. + rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + apply store1_sound with (a := a) (m := m); trivial. + rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + assumption. + Qed. End SOUNDNESS. |