diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-08 22:00:23 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-08 22:00:23 +0100 |
| commit | 5be5afc63935c9dc534fe153026ff1ac4326e7c5 (patch) | |
| tree | a25abbd0d3642210aa24e5fcbfffdaa766e64bae /backend/ForwardMovesproof.v | |
| parent | 2e8e84aea389d41332ebd5a569b474d3c1de23d6 (diff) | |
| download | compcert-kvx-5be5afc63935c9dc534fe153026ff1ac4326e7c5.tar.gz compcert-kvx-5be5afc63935c9dc534fe153026ff1ac4326e7c5.zip | |
moving forward in proofs
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 4e24dab6..34c3c688 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -156,12 +156,29 @@ Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. -Admitted. -(* +Proof. induction 1; intros S1' MS; inv MS; try TR_AT. - (* nop *) econstructor; split. eapply exec_Inop; eauto. constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. +Admitted. +(* - (* op *) econstructor; split. eapply exec_Iop with (v := v); eauto. |