From 44b2d04414b13811868a134f1eae9eaece506b69 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 2 Feb 2019 08:35:08 +0100
Subject: Disable the generation of jump tables until issues are fixed

---
 common/Switchaux.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'common')

diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 4035e299..06337e7d 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -80,6 +80,10 @@ let compile_switch_as_jumptable default cases minkey maxkey =
               CTaction default)
 
 let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
+  (* FIXME DMonniaux disable jump tables until we can prove them through *)
+  false
+
+(*
   let span = Z.sub maxkey minkey in
   assert (Z.ge span Z.zero);
   let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases)
@@ -87,7 +91,8 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
   numcases >= 7           (* small jump tables are always less efficient *)
   && Z.le table_size tree_size
   && Z.lt span (Z.of_uint Sys.max_array_length)
-
+ *)
+  
 let compile_switch modulus default table =
   let (tbl, keys) = normalize_table table in
   if ZSet.is_empty keys then CTaction default else begin
-- 
cgit 


From 47a4ccade6f73e95be34cd2d55be3655302fff97 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 21 Mar 2019 20:29:57 +0100
Subject: begin jumptables (does not work)

---
 common/Switchaux.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'common')

diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 06337e7d..69300feb 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -80,10 +80,6 @@ let compile_switch_as_jumptable default cases minkey maxkey =
               CTaction default)
 
 let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
-  (* FIXME DMonniaux disable jump tables until we can prove them through *)
-  false
-
-(*
   let span = Z.sub maxkey minkey in
   assert (Z.ge span Z.zero);
   let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases)
@@ -91,7 +87,6 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
   numcases >= 7           (* small jump tables are always less efficient *)
   && Z.le table_size tree_size
   && Z.lt span (Z.of_uint Sys.max_array_length)
- *)
   
 let compile_switch modulus default table =
   let (tbl, keys) = normalize_table table in
-- 
cgit 


From c24042a694b960237827c6255d5d407fb58227dc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 29 Mar 2019 20:23:27 +0100
Subject: FIXME: Jumptables have linking issues.

---
 common/Switchaux.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'common')

diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 69300feb..81d7208f 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -80,6 +80,9 @@ let compile_switch_as_jumptable default cases minkey maxkey =
               CTaction default)
 
 let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
+  false
+
+  (* DM FIXME 2019-03-29 do not use jump tables bug in assembly/link
   let span = Z.sub maxkey minkey in
   assert (Z.ge span Z.zero);
   let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases)
@@ -87,6 +90,7 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
   numcases >= 7           (* small jump tables are always less efficient *)
   && Z.le table_size tree_size
   && Z.lt span (Z.of_uint Sys.max_array_length)
+   *)
   
 let compile_switch modulus default table =
   let (tbl, keys) = normalize_table table in
-- 
cgit 


From 3451ed469864c10b2fc5892d46dab08e57e68416 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 30 Mar 2019 16:20:20 +0100
Subject: fix for jump tables

---
 common/Switchaux.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'common')

diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 81d7208f..1744a932 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -80,9 +80,7 @@ let compile_switch_as_jumptable default cases minkey maxkey =
               CTaction default)
 
 let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
-  false
-
-  (* DM FIXME 2019-03-29 do not use jump tables bug in assembly/link
+  (* DM Settings this to constant false disables jump tables *)
   let span = Z.sub maxkey minkey in
   assert (Z.ge span Z.zero);
   let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases)
@@ -90,7 +88,6 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
   numcases >= 7           (* small jump tables are always less efficient *)
   && Z.le table_size tree_size
   && Z.lt span (Z.of_uint Sys.max_array_length)
-   *)
   
 let compile_switch modulus default table =
   let (tbl, keys) = normalize_table table in
-- 
cgit 


From 59089e5d11428dd224b3239bc7f5db602df9b177 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 24 Apr 2019 22:20:13 +0200
Subject: begin bitfields

---
 common/Values.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index a20dd567..ae8d31f3 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -766,6 +766,21 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
   | _ => Vundef
   end.
 
+
+Definition extfz stop start v :=
+  if (Int.cmp Cle start stop)
+       && (Int.cmp Cge start Int.zero)
+       && (Int.cmp Clt stop Int.iwordsize)
+  then
+    let stop' := Int.add stop Int.one in
+    match v with
+    | Vint w =>
+      Vint (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start)))
+    | _ => Vundef
+    end
+  else Vundef.
+
+
 (** Comparisons *)
 
 Section COMPARISONS.
-- 
cgit 


From bb185aa85ddf32feed61d7888c1b199fffdd821f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 25 Apr 2019 10:32:38 +0200
Subject: IT COMPILES

---
 common/Values.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index ae8d31f3..837ed799 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -768,14 +768,14 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
 
 
 Definition extfz stop start v :=
-  if (Int.cmp Cle start stop)
-       && (Int.cmp Cge start Int.zero)
-       && (Int.cmp Clt stop Int.iwordsize)
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int.zwordsize)
   then
-    let stop' := Int.add stop Int.one in
+    let stop' := Z.add stop Z.one in
     match v with
     | Vint w =>
-      Vint (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start)))
+      Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
     | _ => Vundef
     end
   else Vundef.
-- 
cgit 


From 5809fa295f23952a2d8b043f6da69d61da3568de Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 25 Apr 2019 11:17:19 +0200
Subject: progress

---
 common/Values.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index 837ed799..059a72d9 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -768,6 +768,20 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
 
 
 Definition extfz stop start v :=
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int.zwordsize)
+  then
+    let stop' := Z.add stop Z.one in
+    match v with
+    | Vint w =>
+      Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
+    | _ => Vundef
+    end
+  else Vundef.
+
+
+Definition extfs stop start v :=
   if (Z.leb start stop)
        && (Z.geb start Z.zero)
        && (Z.ltb stop Int.zwordsize)
-- 
cgit 


From ff1e531a3f2a58b6fbdc4a5a29f2520d5367c01c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 25 Apr 2019 16:24:10 +0200
Subject: start of extfzl/extfsl

---
 common/Values.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index 059a72d9..45774913 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -794,6 +794,33 @@ Definition extfs stop start v :=
     end
   else Vundef.
 
+Definition extfzl stop start v :=
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int64.zwordsize)
+  then
+    let stop' := Z.add stop Z.one in
+    match v with
+    | Vlong w =>
+      Vlong (Int64.shru (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+    | _ => Vundef
+    end
+  else Vundef.
+
+
+Definition extfsl stop start v :=
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int64.zwordsize)
+  then
+    let stop' := Z.add stop Z.one in
+    match v with
+    | Vlong w =>
+      Vlong (Int64.shr (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+    | _ => Vundef
+    end
+  else Vundef.
+
 
 (** Comparisons *)
 
-- 
cgit 


From beb1cf4f6b56ee739e3a763de93663a875224402 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 25 Apr 2019 17:45:44 +0200
Subject: added code for extfzl/extfsl (not very useful since bitfields are
 limited to 32 bits)

---
 common/Values.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index 45774913..ecc1c458 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -802,7 +802,7 @@ Definition extfzl stop start v :=
     let stop' := Z.add stop Z.one in
     match v with
     | Vlong w =>
-      Vlong (Int64.shru (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+      Vlong (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
     | _ => Vundef
     end
   else Vundef.
@@ -816,7 +816,7 @@ Definition extfsl stop start v :=
     let stop' := Z.add stop Z.one in
     match v with
     | Vlong w =>
-      Vlong (Int64.shr (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+      Vlong (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
     | _ => Vundef
     end
   else Vundef.
-- 
cgit 


From 28e66eb4b60c485bebb1e217bc8f50bdc2cc6ddb Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 27 Apr 2019 18:18:24 +0200
Subject: moved operators to specific file instead of common file

---
 common/Values.v | 55 -------------------------------------------------------
 1 file changed, 55 deletions(-)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index ecc1c458..127d1085 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -767,61 +767,6 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
   end.
 
 
-Definition extfz stop start v :=
-  if (Z.leb start stop)
-       && (Z.geb start Z.zero)
-       && (Z.ltb stop Int.zwordsize)
-  then
-    let stop' := Z.add stop Z.one in
-    match v with
-    | Vint w =>
-      Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
-    | _ => Vundef
-    end
-  else Vundef.
-
-
-Definition extfs stop start v :=
-  if (Z.leb start stop)
-       && (Z.geb start Z.zero)
-       && (Z.ltb stop Int.zwordsize)
-  then
-    let stop' := Z.add stop Z.one in
-    match v with
-    | Vint w =>
-      Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
-    | _ => Vundef
-    end
-  else Vundef.
-
-Definition extfzl stop start v :=
-  if (Z.leb start stop)
-       && (Z.geb start Z.zero)
-       && (Z.ltb stop Int64.zwordsize)
-  then
-    let stop' := Z.add stop Z.one in
-    match v with
-    | Vlong w =>
-      Vlong (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
-    | _ => Vundef
-    end
-  else Vundef.
-
-
-Definition extfsl stop start v :=
-  if (Z.leb start stop)
-       && (Z.geb start Z.zero)
-       && (Z.ltb stop Int64.zwordsize)
-  then
-    let stop' := Z.add stop Z.one in
-    match v with
-    | Vlong w =>
-      Vlong (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
-    | _ => Vundef
-    end
-  else Vundef.
-
-
 (** Comparisons *)
 
 Section COMPARISONS.
-- 
cgit 


From e10870c3da5b28a76c0c0d283c1a0beb09cd7950 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 31 May 2019 19:07:47 +0200
Subject: Additional simulation diagrams for determinate source languages

If the source language is determinate, it can take several steps
(not just one) before the "match_state" invariant is reinstated.
---
 common/Smallstep.v | 173 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 173 insertions(+)

(limited to 'common')

diff --git a/common/Smallstep.v b/common/Smallstep.v
index c269013b..27ad0a2d 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -872,6 +872,14 @@ Proof.
   intros. eapply sd_determ; eauto.
 Qed.
 
+Lemma sd_determ_3:
+  forall s t s1 s2,
+  Step L s t s1 -> Step L s E0 s2 -> t = E0 /\ s1 = s2.
+Proof.
+  intros. exploit (sd_determ DET). eexact H. eexact H0.
+  intros [A B]. inv A. auto.
+Qed.
+
 Lemma star_determinacy:
   forall s t s', Star L s t s' ->
   forall s'', Star L s t s'' -> Star L s' E0 s'' \/ Star L s'' E0 s'.
@@ -895,6 +903,171 @@ Qed.
 
 End DETERMINACY.
 
+(** Extra simulation diagrams for determinate languages. *)
+
+Section FORWARD_SIMU_DETERM.
+
+Variable L1: semantics.
+Variable L2: semantics.
+
+Hypothesis L1det: determinate L1.
+
+Variable index: Type.
+Variable order: index -> index -> Prop.
+Hypothesis wf_order: well_founded order.
+
+Variable match_states: index -> state L1 -> state L2 -> Prop.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 ->
+  exists i s2, initial_state L2 s2 /\ match_states i s1 s2.
+
+Hypothesis match_final_states:
+  forall i s1 s2 r,
+  match_states i s1 s2 ->
+  final_state L1 s1 r ->
+  final_state L2 s2 r.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall i s2, match_states i s1 s2 ->
+  exists s1'' i' s2',
+      Star L1 s1' E0 s1''
+   /\ (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i))
+   /\ match_states i' s1'' s2'.
+
+Hypothesis public_preserved:
+  forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
+
+Inductive match_states_later: index * nat -> state L1 -> state L2 -> Prop :=
+| msl_now: forall i s1 s2,
+    match_states i s1 s2 -> match_states_later (i, O) s1 s2
+| msl_later: forall i n s1 s1' s2,
+    Step L1 s1 E0 s1' -> match_states_later (i, n) s1' s2 -> match_states_later (i, S n) s1 s2.
+
+Lemma star_match_states_later:
+  forall s1 s1', Star L1 s1 E0 s1' ->
+  forall i s2, match_states i s1' s2 ->
+  exists n, match_states_later (i, n) s1 s2.
+Proof.
+  intros s10 s10' STAR0. pattern s10, s10'; eapply star_E0_ind; eauto.
+  - intros s1 i s2 M. exists O; constructor; auto.
+  - intros s1 s1' s1'' STEP IH i s2 M.
+    destruct (IH i s2 M) as (n & MS).
+    exists (S n); econstructor; eauto.
+Qed.
+
+Lemma forward_simulation_determ: forward_simulation L1 L2.
+Proof.
+  apply Forward_simulation with (order0 := lex_ord order lt) (match_states0 := match_states_later);
+  constructor.
+- apply wf_lex_ord. apply wf_order. apply lt_wf.
+- intros. exploit match_initial_states; eauto. intros (i & s2 & A & B).
+  exists (i, O), s2; auto using msl_now.
+- intros. inv H.
+  + eapply match_final_states; eauto.
+  + eelim (sd_final_nostep L1det); eauto.
+- intros s1 t s1' A; destruct 1.
+  + exploit simulation; eauto. intros (s1'' & i' & s2' & B & C & D).
+    exploit star_match_states_later; eauto. intros (n & E).
+    exists (i', n), s2'; split; auto.
+    destruct C as [P | [P Q]]; auto using lex_ord_left.
+  + exploit sd_determ_3. eauto. eexact A. eauto. intros [P Q]; subst t s1'0.
+    exists (i, n), s2; split; auto.
+    right; split. apply star_refl. apply lex_ord_right. omega.
+- exact public_preserved.
+Qed.
+
+End FORWARD_SIMU_DETERM.
+
+(** A few useful special cases. *)
+
+Section FORWARD_SIMU_DETERM_DIAGRAMS.
+
+Variable L1: semantics.
+Variable L2: semantics.
+
+Hypothesis L1det: determinate L1.
+
+Variable match_states: state L1 -> state L2 -> Prop.
+
+Hypothesis public_preserved:
+  forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 ->
+  exists s2, initial_state L2 s2 /\ match_states s1 s2.
+
+Hypothesis match_final_states:
+  forall s1 s2 r,
+  match_states s1 s2 ->
+  final_state L1 s1 r ->
+  final_state L2 s2 r.
+
+Section SIMU_DETERM_STAR.
+
+Variable measure: state L1 -> nat.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s1'' s2',
+      Star L1 s1' E0 s1''
+   /\ (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ measure s1'' < measure s1))%nat
+   /\ match_states s1'' s2'.
+
+Lemma forward_simulation_determ_star: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_determ with
+    (match_states := fun i s1 s2 => i = s1 /\ match_states s1 s2)
+    (order := ltof _ measure).
+- assumption.
+- apply well_founded_ltof.
+- intros. exploit match_initial_states; eauto. intros (s2 & A & B). 
+  exists s1, s2; auto.
+- intros. destruct H. eapply match_final_states; eauto.
+- intros. destruct H0; subst i. 
+  exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s1'', s2'. auto.
+- assumption.
+Qed.
+
+End SIMU_DETERM_STAR.
+
+Section SIMU_DETERM_PLUS.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s1'' s2', Star L1 s1' E0 s1'' /\ Plus L2 s2 t s2' /\ match_states s1'' s2'.
+
+Lemma forward_simulation_determ_plus: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_determ_star with (measure := fun _ => O).
+  intros. exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s2'; auto.
+Qed.
+
+End SIMU_DETERM_PLUS.
+
+Section SIMU_DETERM_ONE.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s1'' s2', Star L1 s1' E0 s1'' /\ Step L2 s2 t s2' /\ match_states s1'' s2'.
+
+Lemma forward_simulation_determ_one: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_determ_plus.
+  intros. exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s2'; auto using plus_one.
+Qed.
+
+End SIMU_DETERM_ONE.
+
+End FORWARD_SIMU_DETERM_DIAGRAMS.
+
 (** * Backward simulations between two transition semantics. *)
 
 Definition safe (L: semantics) (s: state L) : Prop :=
-- 
cgit 


From 1d90fa730df7d1cb2ee726d3b41b9915ae4e4e2e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 23:02:06 +0200
Subject: moved trapping_mode to a more appropriate place

---
 common/AST.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index a91138c9..d98f954a 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -193,6 +193,15 @@ Definition chunk_of_type (ty: typ) :=
 Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr.
 Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
 
+(** Trapping mode: does undefined behavior result in a trap or an undefined value (e.g. for loads) *)
+Inductive trapping_mode : Type := TRAP | NOTRAP.
+
+Definition trapping_mode_eq : forall x y : trapping_mode,
+    { x=y } + { x <> y}.
+Proof.
+  decide equality.
+Defined.
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
-- 
cgit 


From c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 11:19:22 +0200
Subject: more proofs going through

---
 common/AST.v    | 1 +
 common/Memory.v | 3 +++
 2 files changed, 4 insertions(+)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index d98f954a..bb8508b7 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -202,6 +202,7 @@ Proof.
   decide equality.
 Defined.
 
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
diff --git a/common/Memory.v b/common/Memory.v
index b68a5049..cfd13601 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -39,6 +39,9 @@ Require Import Values.
 Require Export Memdata.
 Require Export Memtype.
 
+Definition default_notrap_load_value (chunk : memory_chunk) := Vundef.
+
+
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
-- 
cgit 


From e64b9464fb6662bf63ac255eca94d17d572c9d81 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 6 Sep 2019 22:33:46 +0200
Subject: ONE "admitted" and things compile

---
 common/PrintAST.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'common')

diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index e477957a..baddb722 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -90,3 +90,7 @@ let rec print_builtin_res px oc = function
       fprintf oc "splitlong(%a, %a)"
                  (print_builtin_res px) hi (print_builtin_res px) lo
 
+let print_trapping_mode oc = function
+  | TRAP -> ()
+  | NOTRAP -> output_string oc " [notrap]"
+                
-- 
cgit 


From 7b4e6a522bcf1f247ef9b3517af328b5da670a98 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@univ-grenoble-alpes.fr>
Date: Fri, 4 Oct 2019 17:57:25 +0200
Subject: Ibuiltin proof

---
 common/AST.v | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index a91138c9..7ffe355d 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -17,7 +17,7 @@
   the abstract syntax trees of many of the intermediate languages. *)
 
 Require Import String.
-Require Import Coqlib Maps Errors Integers Floats.
+Require Import Coqlib Maps Errors Integers Floats BinPos.
 Require Archi.
 
 Set Implicit Arguments.
@@ -630,11 +630,28 @@ Inductive builtin_arg (A: Type) : Type :=
   | BA_splitlong (hi lo: builtin_arg A)
   | BA_addptr (a1 a2: builtin_arg A).
 
+Definition builtin_arg_eq {A: Type}:
+  (forall x y : A, {x = y} + {x <> y}) ->
+  forall (ba1 ba2: (builtin_arg A)), {ba1=ba2} + {ba1<>ba2}.
+Proof.
+  intro. generalize Integers.int_eq int64_eq float_eq float32_eq chunk_eq ptrofs_eq ident_eq.
+  decide equality.
+Defined.
+Global Opaque builtin_arg_eq.
+
 Inductive builtin_res (A: Type) : Type :=
   | BR (x: A)
   | BR_none
   | BR_splitlong (hi lo: builtin_res A).
 
+Definition builtin_res_eq {A: Type}:
+  (forall x y : A, {x = y} + {x <> y}) ->
+  forall (a b: builtin_res A), {a=b} + {a<>b}.
+Proof.
+  intro. decide equality.
+Defined.
+Global Opaque builtin_res_eq.
+
 Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
   match a with
   | BA_loadglobal chunk id ofs => id :: nil
-- 
cgit 


From 452f2fcb343fc5b579aa3fa122c8b97c170b14af Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 13 Dec 2019 13:01:59 +0100
Subject: swap writes in memory

---
 common/Memory.v | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

(limited to 'common')

diff --git a/common/Memory.v b/common/Memory.v
index cfd13601..f14a19d7 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -38,6 +38,7 @@ Require Import Floats.
 Require Import Values.
 Require Export Memdata.
 Require Export Memtype.
+Require Import Lia.
 
 Definition default_notrap_load_value (chunk : memory_chunk) := Vundef.
 
@@ -541,6 +542,48 @@ Proof.
   induction vl; simpl; intros. auto. rewrite IHvl. auto.
 Qed.
 
+Remark set_setN_swap_disjoint:
+  forall vl: list memval,
+  forall v: memval,
+  forall m : ZMap.t memval,
+  forall p pl: Z,
+    ~ (Intv.In p (pl, pl + Z.of_nat (length vl))) ->
+    (setN vl pl (ZMap.set p v m)) = (ZMap.set p v (setN vl pl m)).
+Proof.
+  induction vl; simpl; trivial.
+  intros.
+  unfold Intv.In in *; simpl in *.
+  rewrite ZMap.set_disjoint by lia.
+  apply IHvl.
+  lia.
+Qed.
+
+Lemma set_swap_disjoint:
+  forall vl1 vl2: list memval,
+  forall m : ZMap.t memval,
+  forall p1 p2: Z,
+    Intv.disjoint (p1, p1 + Z.of_nat (length vl1))
+                  (p2, p2 + Z.of_nat (length vl2)) ->
+    (setN vl1 p1 (setN vl2 p2 m)) = (setN vl2 p2 (setN vl1 p1 m)).
+Proof.
+  induction vl1; simpl; trivial.
+  intros until p2. intro DISJOINT.
+  rewrite <- set_setN_swap_disjoint.
+  { rewrite IHvl1.
+    reflexivity.
+    unfold Intv.disjoint, Intv.In in *.
+    simpl in *.
+    intro.
+    intro BOUNDS.
+    apply DISJOINT.
+    lia.
+  }
+  unfold Intv.disjoint, Intv.In in *.
+  simpl in *.
+  apply DISJOINT.
+  lia.
+Qed.
+    
 (** [store chunk m b ofs v] perform a write in memory state [m].
   Value [v] is stored at address [b] and offset [ofs].
   Return the updated memory store, or [None] if the accessed bytes
-- 
cgit 


From 70bd68aabcbf27ce525bb565b85fb41e3db4ded3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 13 Dec 2019 19:06:56 +0100
Subject: store_store_other

---
 common/Memory.v | 85 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 84 insertions(+), 1 deletion(-)

(limited to 'common')

diff --git a/common/Memory.v b/common/Memory.v
index f14a19d7..50e339e1 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -558,7 +558,7 @@ Proof.
   lia.
 Qed.
 
-Lemma set_swap_disjoint:
+Lemma setN_swap_disjoint:
   forall vl1 vl2: list memval,
   forall m : ZMap.t memval,
   forall p1 p2: Z,
@@ -1215,6 +1215,89 @@ Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
 Local Hint Resolve store_valid_access_1 store_valid_access_2
              store_valid_access_3: mem.
 
+Remark mem_same_proof_irr :
+  forall m1 m2 : mem,
+    (mem_contents m1) = (mem_contents m2) ->
+    (mem_access m1) = (mem_access m2) ->
+    (nextblock m1) = (nextblock m2) ->
+    m1 = m2.
+Proof.
+  destruct m1 as [contents1 access1 nextblock1 access_max1 nextblock_noaccess1 default1].
+  destruct m2 as [contents2 access2 nextblock2 access_max2 nextblock_noaccess2 default2].
+  simpl.
+  intros.
+  subst contents2.
+  subst access2.
+  subst nextblock2.
+  f_equal; apply proof_irr.
+Qed.
+
+Theorem store_store_other:
+  forall chunk b ofs v chunk' b' ofs' v' m0 m1 m1',
+     b' <> b
+  \/ ofs' + size_chunk chunk' <= ofs
+  \/ ofs  + size_chunk chunk  <= ofs' ->
+     store chunk m0 b ofs v = Some m1 ->
+     store chunk' m0 b' ofs' v' = Some m1' ->
+     store chunk' m1 b' ofs' v' =
+     store chunk m1' b ofs v.
+Proof.
+  intros until m1'.
+  intro DISJOINT.
+  intros W0 W0'.
+  assert (valid_access m1' chunk b ofs Writable) as WRITEABLE1' by eauto with mem.
+  (* {
+    eapply store_valid_access_1.
+    apply W0'.
+    eapply store_valid_access_3.
+    apply W0.
+  } *)
+  assert (valid_access m1 chunk' b' ofs' Writable) as WRITABLE1 by eauto with mem.
+  (* {
+    eapply store_valid_access_1.
+    apply W0.
+    eapply store_valid_access_3.
+    apply W0'.
+  } *)
+  unfold store in *.
+  destruct (valid_access_dec m0 chunk b ofs Writable).
+  2: congruence.
+  destruct (valid_access_dec m1 chunk' b' ofs' Writable).
+  2: contradiction.
+  destruct (valid_access_dec m0 chunk' b' ofs' Writable).
+  2: congruence.
+  destruct (valid_access_dec m1' chunk b ofs Writable).
+  2: contradiction.
+  f_equal.
+  inv W0; simpl in *.
+  inv W0'; simpl in *.
+  apply mem_same_proof_irr; simpl; trivial.
+  destruct (eq_block b b').
+  { subst b'.
+    rewrite PMap.gss.
+    rewrite PMap.gss.
+    rewrite PMap.set2.
+    rewrite PMap.set2.
+    f_equal.
+    apply setN_swap_disjoint.
+    unfold Intv.disjoint.
+    rewrite encode_val_length.
+    rewrite <- size_chunk_conv.
+    rewrite encode_val_length.
+    rewrite <- size_chunk_conv.
+    unfold Intv.In; simpl.
+    intros.
+    destruct DISJOINT. contradiction.
+    lia.
+  }
+  {
+    rewrite PMap.set_disjoint by congruence.
+    rewrite PMap.gso by congruence.
+    rewrite PMap.gso by congruence.
+    reflexivity.
+  }
+Qed.
+    
 Lemma load_store_overlap:
   forall chunk m1 b ofs v m2 chunk' ofs' v',
   store chunk m1 b ofs v = Some m2 ->
-- 
cgit 


From 804e8174a944e3d8983c077502e57113ecdda6dd Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 14 Jan 2020 10:13:57 +0100
Subject: shrx_shr_3

---
 common/Values.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index de317734..01724c99 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1439,6 +1439,60 @@ Proof.
   assert (32 < Int.max_unsigned) by reflexivity. omega.
 Qed.
 
+Theorem shrx1_shr:
+  forall x z,
+  shrx x (Vint (Int.repr 1)) = Some z ->
+  z = shr (add x (shru x (Vint (Int.repr 31)))) (Vint (Int.repr 1)).
+Proof.
+  intros. destruct x; simpl in H; try discriminate.
+  change (Int.ltu (Int.repr 1) (Int.repr 31)) with true in H; simpl in H.
+  inversion_clear H.
+  simpl.
+  change (Int.ltu (Int.repr 31) Int.iwordsize) with true; simpl.
+  change (Int.ltu (Int.repr 1) Int.iwordsize) with true; simpl.
+  f_equal.
+  rewrite Int.shrx1_shr by reflexivity.
+  reflexivity.
+Qed.
+
+Theorem shrx_shr_3:
+  forall n x z,
+  shrx x (Vint n) = Some z ->
+  z = (if Int.eq n Int.zero then x else
+         if Int.eq n Int.one
+         then shr (add x (shru x (Vint (Int.repr 31)))) (Vint Int.one)
+         else shr (add x (shru (shr x (Vint (Int.repr 31)))
+                    (Vint (Int.sub (Int.repr 32) n))))
+             (Vint n)).
+Proof.
+  intros. destruct x; simpl in H; try discriminate.
+  destruct (Int.ltu n (Int.repr 31)) eqn:LT; inv H.
+  exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31; intros LT'.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1.
+  rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+- predSpec Int.eq Int.eq_spec n Int.one.
+  * subst n. simpl.
+    change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl.
+    change (Int.ltu Int.one Int.iwordsize) with true. simpl.
+    f_equal.
+    apply Int.shrx1_shr.
+    reflexivity.
+  * clear H0.
+    simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl.
+    replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl.
+    replace (Int.ltu n Int.iwordsize) with true.
+    f_equal; apply Int.shrx_shr_2; assumption.
+    symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
+    symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
+    assert (Int.unsigned n <> 0).
+    { red; intros; elim H.
+      rewrite <- (Int.repr_unsigned n), H0. auto. }
+    rewrite Int.unsigned_repr.
+    change (Int.unsigned Int.iwordsize) with 32; omega.
+    assert (32 < Int.max_unsigned) by reflexivity. omega.
+Qed.
+
 Theorem or_rolm:
   forall x n m1 m2,
   or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).
-- 
cgit 


From d7c9c729ba52ae926238ab97650104117e488c05 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 14 Jan 2020 15:42:56 +0100
Subject: shrxl_shrl_3

---
 common/Values.v | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index 01724c99..84030123 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1752,6 +1752,58 @@ Proof.
   assert (64 < Int.max_unsigned) by reflexivity. omega.
 Qed.
 
+Theorem shrxl1_shrl:
+  forall x z,
+  shrxl x (Vint (Int.repr 1)) = Some z ->
+  z = shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint (Int.repr 1)).
+Proof.
+  intros. destruct x; simpl in H; try discriminate.
+  change (Int.ltu (Int.repr 1) (Int.repr 63)) with true in H; simpl in H.
+  inversion_clear H.
+  simpl.
+  change (Int.ltu (Int.repr 63) Int64.iwordsize') with true; simpl.
+  change (Int.ltu (Int.repr 1) Int64.iwordsize') with true; simpl.
+  f_equal.
+  rewrite Int64.shrx'1_shr' by reflexivity.
+  reflexivity.
+Qed.
+
+Theorem shrxl_shrl_3:
+  forall n x z,
+  shrxl x (Vint n) = Some z ->
+  z = (if Int.eq n Int.zero then x else
+         if Int.eq n Int.one
+         then shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint Int.one)
+         else shrl (addl x (shrlu (shrl x (Vint (Int.repr 63)))
+                    (Vint (Int.sub (Int.repr 64) n))))
+             (Vint n)).
+Proof.
+  intros. destruct x; simpl in H; try discriminate.
+  destruct (Int.ltu n (Int.repr 63)) eqn:LT; inv H.
+  exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63; intros LT'.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. unfold Int64.shrx'. rewrite Int64.shl'_zero. unfold Int64.divs. change (Int64.signed Int64.one) with 1.
+  rewrite Z.quot_1_r. rewrite Int64.repr_signed; auto.
+- predSpec Int.eq Int.eq_spec n Int.one.
+  * subst n. simpl.
+    change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl.
+    change (Int.ltu Int.one Int64.iwordsize') with true. simpl.
+    f_equal.
+    apply Int64.shrx'1_shr'.
+    reflexivity.
+  * clear H0.
+simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl.
+  replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl.
+  replace (Int.ltu n Int64.iwordsize') with true.
+  f_equal; apply Int64.shrx'_shr_2; assumption.
+  symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
+  symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
+  assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
+  rewrite Int.unsigned_repr.
+  change (Int.unsigned Int64.iwordsize') with 64; omega.
+  assert (64 < Int.max_unsigned) by reflexivity. omega.
+Qed.
+
 Theorem negate_cmp_bool:
   forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y).
 Proof.
-- 
cgit