From 4d79ef052cc05240d6613bb22ef1ec547b17d3e1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 29 Oct 2020 15:54:41 +0100
Subject: in CSE3 choose lowest variable as representative for moves

---
 backend/CSE3analysisproof.v | 107 +++++++++++++++++++++++++++++++-------------
 1 file changed, 76 insertions(+), 31 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index ea4d37ca..12048010 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -478,6 +478,27 @@ Section SOUNDNESS.
     rewrite negb_true_iff in H.
     intuition.
   Qed.
+
+  Lemma reg_min_sound:
+    forall x y, (reg_min x y) = x \/ (reg_min x y) = y.
+  Proof.
+    intros; unfold reg_min.
+    destruct plt; auto.
+  Qed.
+  
+  Lemma reg_min_rec_sound :
+    forall (l : list reg) (before : reg),
+      In (reg_min_rec l before) l \/
+      reg_min_rec l before = before.
+  Proof.
+    induction l; cbn.
+    { auto. }
+    intro bef.
+    destruct (IHl (reg_min bef a)).
+    { auto. }
+    rewrite H.
+    destruct (reg_min_sound bef a); auto.
+  Qed.
     
   Lemma pick_source_sound :
     forall (l : list reg),
@@ -486,47 +507,71 @@ Section SOUNDNESS.
       | None => True
       end.
   Proof.
-    unfold pick_source.
-    destruct l; simpl; trivial.
-    left; trivial.
+    destruct l; cbn; trivial.
+    destruct (reg_min_rec_sound l r); auto.
   Qed.
-    
+
   Hint Resolve pick_source_sound : cse3.
 
+  Theorem get_sources_sound :
+    forall l src rs m x,
+    (forall i eq,
+      In i l ->
+      eq_catalog ctx i = Some eq ->
+      sem_eq eq rs m) ->
+      (In src (get_sources (ctx := ctx) x l)) ->
+      rs # src = rs # x.
+  Proof.
+    induction l; cbn; intros until x; intros SEM IN.
+    contradiction.
+    destruct (eq_catalog ctx a) eqn:CATALOG.
+    2: eauto using IHl; fail.
+    pose proof (SEM a e) as SEMeq.
+    destruct e; cbn in *.
+    destruct (is_smove eq_op && peq x eq_lhs) eqn:CORRECT.
+    2: eauto using IHl; fail.
+    destruct eq_args.
+    eauto using IHl; fail.
+    destruct eq_args.
+    2: eauto using IHl; fail.
+    cbn in IN.
+    destruct IN.
+    2: eauto using IHl; fail.
+    rewrite andb_true_iff in CORRECT.
+    intuition.
+    destruct (peq x eq_lhs).
+    2: discriminate.
+    subst eq_lhs.
+    destruct (is_smove eq_op).
+    2: discriminate.
+    subst eq_op.
+    subst src.
+    cbn in H2.
+    symmetry.
+    assumption.
+  Qed.
+    
   Theorem forward_move_sound :
     forall rel rs m x,
       (sem_rel rel rs m) ->
       rs # (forward_move (ctx := ctx) rel x) = rs # x.
   Proof.
-    unfold sem_rel, forward_move.
-    intros until x.
-    intro REL.
-    pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT.
-    destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))).
-    2: reflexivity.
-    destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG.
-    2: reflexivity.
-    specialize REL with (i := r) (eq0 := eq).
-    destruct (is_smove (eq_op eq)) as [MOVE | ].
-    2: reflexivity.
-    destruct (peq x (eq_lhs eq)).
+    unfold forward_move.
+    intros until x; intros REL.
+    pose proof (pick_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK.
+    destruct pick_source.
     2: reflexivity.
-    simpl.
-    subst x.
-    rewrite PSet.elements_spec in ELEMENT.
-    rewrite PSet.ginter in ELEMENT.
-    rewrite andb_true_iff in ELEMENT.
-    unfold sem_eq in REL.
-    rewrite MOVE in REL.
-    simpl in REL.
-    destruct (eq_args eq) as [ | h t].
-    reflexivity.
-    destruct t.
-    2: reflexivity.
-    simpl in REL.
-    intuition congruence.
+    apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m).
+    2: assumption.
+    intros i eq IN CATALOG.
+    rewrite PSet.elements_spec in IN.
+    rewrite PSet.ginter in IN.
+    rewrite andb_true_iff in IN.
+    destruct IN.
+    unfold sem_rel in REL.
+    apply REL with (i:=i); assumption.
   Qed.
-
+  
   Hint Resolve forward_move_sound : cse3.
 
   Theorem forward_move_l_sound :
-- 
cgit