From 93fd5df1bff8b22b3513a07a765b0a72f1505243 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:26:32 +0200 Subject: some more on builtins --- backend/Selectionproof.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 50ff377a..d839f22a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -854,6 +854,8 @@ Remark find_label_commut: | _, _ => False end. Proof. +Admitted. +(* induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) unfold store. destruct (addressing m (sel_expr e)); simpl; auto. @@ -886,6 +888,7 @@ Proof. (* label *) destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. + *) Definition measure (s: Cminor.state) : nat := match s with @@ -900,6 +903,8 @@ Lemma sel_step_correct: (exists T2, step tge T1 t T2 /\ match_states S2 T2) \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. +Admitted. +(* induction 1; intros T1 ME; inv ME; try (monadInv TS). - (* skip seq *) inv MC. left; econstructor; split. econstructor. econstructor; eauto. @@ -1067,6 +1072,7 @@ Proof. right; split. simpl; omega. split. auto. econstructor; eauto. apply sel_builtin_res_correct; auto. Qed. + *) Lemma sel_initial_states: forall S, Cminor.initial_state prog S -> -- cgit