From 82ecfc692b0f84b52162e5f0972fbcc6a9f7f51e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 29 Oct 2020 23:15:49 +0100
Subject: reinstated previous forward_move function

---
 backend/CSE3analysisproof.v | 78 ++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 70 insertions(+), 8 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 12048010..29254a4f 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -500,9 +500,9 @@ Section SOUNDNESS.
     destruct (reg_min_sound bef a); auto.
   Qed.
     
-  Lemma pick_source_sound :
+  Lemma pick_min_source_sound :
     forall (l : list reg),
-      match pick_source l with
+      match pick_min_source l with
       | Some x => In x l
       | None => True
       end.
@@ -511,7 +511,7 @@ Section SOUNDNESS.
     destruct (reg_min_rec_sound l r); auto.
   Qed.
 
-  Hint Resolve pick_source_sound : cse3.
+  Hint Resolve pick_min_source_sound : cse3.
 
   Theorem get_sources_sound :
     forall l src rs m x,
@@ -551,15 +551,15 @@ Section SOUNDNESS.
     assumption.
   Qed.
     
-  Theorem forward_move_sound :
+  Theorem forward_move2_sound :
     forall rel rs m x,
       (sem_rel rel rs m) ->
-      rs # (forward_move (ctx := ctx) rel x) = rs # x.
+      rs # (forward_move2 (ctx := ctx) rel x) = rs # x.
   Proof.
-    unfold forward_move.
+    unfold forward_move2.
     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.
+    pose proof (pick_min_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK.
+    destruct pick_min_source.
     2: reflexivity.
     apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m).
     2: assumption.
@@ -572,6 +572,68 @@ Section SOUNDNESS.
     apply REL with (i:=i); assumption.
   Qed.
   
+  Hint Resolve forward_move2_sound : cse3.
+
+    
+  Lemma pick_source_sound :
+    forall (l : list reg),
+      match pick_source l with
+      | Some x => In x l
+      | None => True
+      end.
+  Proof.
+    unfold pick_source.
+    destruct l; simpl; trivial.
+    left; trivial.
+  Qed.
+    
+  Hint Resolve pick_source_sound : cse3.
+
+  Theorem forward_move1_sound :
+    forall rel rs m x,
+      (sem_rel rel rs m) ->
+      rs # (forward_move1 (ctx := ctx) rel x) = rs # x.
+  Proof.
+    unfold sem_rel, forward_move1.
+    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)).
+    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.
+  Qed.
+
+  Hint Resolve forward_move1_sound : cse3.
+
+  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 forward_move.
+    apply forward_move1_sound.
+  Qed.
+  
   Hint Resolve forward_move_sound : cse3.
 
   Theorem forward_move_l_sound :
-- 
cgit