From 79c039d7b33878d00f22ad8542dc30a78aa8b70a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 11:34:35 +0100
Subject: CSE3 + conditions proof

---
 backend/CSE3proof.v | 67 +++++++++++++++++++++++++++--------------------------
 1 file changed, 34 insertions(+), 33 deletions(-)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index cc4ab686..50a32d56 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -352,6 +352,23 @@ Qed.
 
 Hint Resolve rel_ge : cse3.
 
+Lemma relb_ge:
+  forall inv inv'
+         (GE : RB.ge inv' inv)
+         ctx sp rs m
+         (REL: sem_rel_b sp ctx inv rs m),
+  sem_rel_b sp ctx inv' rs m.
+Proof.
+  intros.
+  destruct inv; cbn in *.
+  2: contradiction.
+  destruct inv'; cbn in *.
+  2: assumption.
+  eapply rel_ge; eassumption.
+Qed.
+
+Hint Resolve relb_ge : cse3.
+
 Lemma sem_rhs_sop :
   forall sp op rs args m v,
   eval_operation ge sp op rs ## args m = Some v ->
@@ -946,23 +963,15 @@ Proof.
       rewrite andb_true_iff in IND_step_me.
       destruct IND_step_me as [IND_so [IND_not ZOT]].
       clear ZOT.
-      destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *.
-      2: discriminate.
-      destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *.
-      2: discriminate.
-      rewrite rel_leb_correct in IND_so.
-      rewrite rel_leb_correct in IND_not.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
       destruct b.
-      {
-        rewrite INV_so.
-        cbn.
-        eapply rel_ge; eauto.
-      }
-      {
-        rewrite INV_not.
-        cbn.
-        eapply rel_ge; eauto.
-      }
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
       (* END INVARIANT *)
         }
         unfold sem_rel_b in REL.
@@ -1048,23 +1057,15 @@ Proof.
       rewrite andb_true_iff in IND_step_me.
       destruct IND_step_me as [IND_so [IND_not ZOT]].
       clear ZOT.
-      destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *.
-      2: discriminate.
-      destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *.
-      2: discriminate.
-      rewrite rel_leb_correct in IND_so.
-      rewrite rel_leb_correct in IND_not.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
       destruct b.
-      {
-        rewrite INV_so.
-        cbn.
-        eapply rel_ge; eauto.
-      }
-      {
-        rewrite INV_not.
-        cbn.
-        eapply rel_ge; eauto.
-      }
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
       (* END INVARIANT *)
       
   - (* Ijumptable *)
@@ -1171,7 +1172,7 @@ Proof.
       apply wt_regset_assign; trivial.
       rewrite WTRES0.
       exact WTRES.
-Admitted.
+Qed.
 
 Lemma transf_initial_states:
   forall S1, RTL.initial_state prog S1 ->
-- 
cgit