diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-05-19 15:32:02 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-05-19 15:32:02 +0200 |
| commit | 1df2759e91263fb494133e668b6db6f881e2784e (patch) | |
| tree | 7ea468ec13bcb7cec35ac3593a5c49848f61c034 | |
| parent | 8bf7464e0293f514b6a8b4cb7a0d038be6520d1c (diff) | |
| download | compcert-kvx-1df2759e91263fb494133e668b6db6f881e2784e.tar.gz compcert-kvx-1df2759e91263fb494133e668b6db6f881e2784e.zip | |
sistep_correct proved completely
| -rw-r--r-- | mppa_k1c/lib/RTLpathSE_theory.v | 37 |
1 files changed, 16 insertions, 21 deletions
diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index 7fe212ab..2a8c4e3f 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -642,26 +642,21 @@ Proof. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. subst; rewrite Regmap.gss; simpl. erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps. admit. - } { admit. } -(* inversion_SOME a0; intros ADD. - { inversion_SOME v; intros LOAD; simpl. - - explore_destruct; unfold ssem, ssem_local; simpl; intuition. - * exploit REG. try_simplify_someHyps. - * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. - subst; rewrite Regmap.gss; simpl. - erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - - unfold sabort, sabort_local; simpl. - left. right. right. - exists r. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps. } - { unfold sabort, sabort_local; simpl. - left. right. right. - exists r. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite seval_list_sval_inj; simpl; auto. - rewrite ADD; simpl; auto. } *) + try_simplify_someHyps. intros SMEM SEVAL. + rewrite LOAD. reflexivity. + } { rewrite ADD. destruct t. + - simpl. left; eauto. simpl. econstructor; eauto. + right. right. simpl. exists r. destruct (Pos.eq_dec r r); [|contradiction]. + simpl. inversion_SOME args. intro SLS. + eapply seval_list_sval_inj in REG. rewrite REG in SLS. inv SLS. + rewrite ADD. reflexivity. + - simpl. constructor; [|constructor]; simpl; auto. + constructor; simpl; constructor; auto; [congruence|]. + intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst. simpl. rewrite Regmap.gss. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. intro SMEM. rewrite ADD. reflexivity. + } + (* STORE *) inversion_SOME a0; intros ADD. { inversion_SOME m'; intros STORE; simpl. @@ -701,7 +696,7 @@ Proof. unfold seval_condition. erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. } -Admitted. +Qed. Lemma sistep_correct_None ge sp i st rs0 m0 rs m: |