Update proof

3 files changed, 125 insertions, 37 deletions

diff --git a/flake.nix b/flake.nix
index 563797f..7303d3b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -8,6 +8,9 @@
       pkgs = nixpkgs.legacyPackages.x86_64-linux;
       ncoq = pkgs.coq_8_14;
       ncoqPackages = pkgs.coqPackages_8_14;
+      dpkgs = nixpkgs.legacyPackages.x86_64-darwin;
+      dncoq = dpkgs.coq_8_14;
+      dncoqPackages = dpkgs.coqPackages_8_14;
     in {
       devShell.x86_64-linux = pkgs.mkShell {
         buildInputs = with pkgs;
@@ -29,5 +32,25 @@
             python3Packages.sphinx_rtd_theme
           ];
       };
+      devShell.x86_64-darwin = dpkgs.mkShell {
+        buildInputs = with dpkgs;
+          [ dncoq
+            dune_2
+            gcc
+            dncoq.ocaml
+            dncoq.ocamlPackages.findlib
+            dncoq.ocamlPackages.menhir
+            dncoq.ocamlPackages.ocamlgraph
+            dncoq.ocamlPackages.menhirLib
+
+            dncoq.ocamlPackages.ocp-indent
+            dncoq.ocamlPackages.utop
+
+            dncoqPackages.serapi
+            python3
+            python3Packages.alectryon
+            python3Packages.sphinx_rtd_theme
+          ];
+      };
     };
 }
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 9e2cfc5..2a04a55 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -84,6 +84,11 @@ Lemma step_instr_false :
     ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0).
 Proof. destruct a; unfold not; intros; inv H. Qed.
 
+Lemma step_list_false :
+  forall A B ge sp a i0 s,
+    ~ step_list (@step_instr A B ge) sp s a (Iexec i0).
+Proof. destruct a; unfold not; intros; inv H. Qed.
+
 Lemma step_list2_false :
   forall A B ge l0 sp i c i0',
     ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0').
@@ -125,11 +130,11 @@ Qed.
 #[local] Notation "'mki'" := (mk_instr_state) (at level 1).
 
 Lemma exec_rbexit_truthy :
-  forall A B bb ge sp rs pr m rs' pr' m' pc',
-    @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) ->
+  forall A B bb ge sp rs pr m rs' pr' m' cf,
+    @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
     exists p b1 b2,
       truthy pr' p
-      /\ bb = b1 ++ (RBexit p (RBgoto pc')) :: b2
+      /\ bb = b1 ++ (RBexit p cf) :: b2
       /\ step_list2 (Gible.step_instr ge) sp (Iexec (mki rs pr m)) b1 (Iexec (mki rs' pr' m')).
 Proof.
   induction bb; crush.
@@ -184,9 +189,9 @@ Qed.
 
 Lemma append3 :
   forall A B l0 l1 sp ge s1 s2 s3,
-    step_list2 (step_instr ge) sp s1 l0 s2 ->
+    step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
     @SeqBB.step A B ge sp s1 (l0 ++ l1) s3 ->
-    @SeqBB.step A B ge sp s2 l1 s3.
+    @SeqBB.step A B ge sp (Iexec s2) l1 s3.
 Proof.
   induction l0; crush. inv H. auto.
   inv H0. inv H. assert (i1 = (Iexec state')) by (eapply exec_determ; eauto). subst. eauto.
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index de44118..ca4d18b 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -133,6 +133,7 @@ Section CORRECTNESS.
              (* This can be improved with a recursive relation for a more general structure of the
                 if-conversion proof. *)
              (IS_B: f.(fn_code)!pc = Some b)
+             (IS_TB: forall b', f.(fn_code)!pc0 = Some b' -> tf.(fn_code)!pc0 = if_conv_replace)
              (EXTRAP: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b)
              (SIM: step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)),
         match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0)
@@ -282,9 +283,9 @@ Section CORRECTNESS.
   Proof. intros; simplify. do 3 econstructor; eauto. Qed.
 
   Lemma step_instr :
-    forall sp s s' a,
-      step_instr ge sp (Iexec s) a (Iexec s') ->
-      step_instr tge sp (Iexec s) a (Iexec s').
+    forall sp s1 s2 a,
+      step_instr ge sp s1 a s2 ->
+      step_instr tge sp s1 a s2.
   Proof.
     inversion 1; subst; econstructor; eauto.
     - now rewrite <- eval_op_eq.
@@ -292,12 +293,6 @@ Section CORRECTNESS.
     - now rewrite <- eval_addressing_eq.
   Qed.
 
-  Lemma step_instr_term :
-    forall sp s s' a cf,
-      Gible.step_instr ge sp (Iexec s) a (Iterm s' cf) ->
-      Gible.step_instr tge sp (Iexec s) a (Iterm s' cf).
-  Proof. inversion 1; subst; constructor; auto. Qed.
-
   Lemma seqbb_eq :
     forall bb sp rs pr m rs' pr' m' cf,
       SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
@@ -306,7 +301,17 @@ Section CORRECTNESS.
     induction bb; crush; inv H.
     - econstructor; eauto. apply step_instr; eassumption.
       destruct state'. eapply IHbb; eauto.
-    - constructor; apply step_instr_term; auto.
+    - constructor; apply step_instr; auto.
+  Qed.
+
+  Lemma step_list_2_eq :
+    forall bb sp a b,
+      step_list2 (Gible.step_instr ge) sp a bb b ->
+      step_list2 (Gible.step_instr tge) sp a bb b.
+  Proof.
+    induction bb; crush; inv H.
+    - econstructor; eauto.
+    - econstructor; eauto. now apply step_instr.
   Qed.
 
   Lemma fn_all_eq :
@@ -365,16 +370,36 @@ Section CORRECTNESS.
   Qed.
 
   Lemma exec_if_conv :
-    forall bb sp rs pr m rs' pr' m' pc' b' tb,
-      SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) ->
-      if_conv_replace pc' b' bb tb ->
-      exists p b rb,
-        tb = b ++ (map (map_if_convert p) b') ++ rb
-        /\ SeqBB.step ge sp (Iexec (mki rs pr m)) b (Iexec (mki rs' pr' m')).
+    forall A B ge sp pc' b' tb i i' x0 x x1,
+      step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') ->
+      if_conv_replace pc' b' (x0 ++ RBexit x (RBgoto pc') :: x1) tb ->
+      exists b rb,
+        tb = b ++ (map (map_if_convert x) b') ++ rb
+        /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i').
+  Proof.
+    Admitted.
+
+  Lemma exec_if_conv2 :
+    forall A B ge sp pc' b' tb i i' x0 x x1 cf,
+      step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') ->
+      cf <> RBgoto pc' ->
+      if_conv_replace pc' b' (x0 ++ RBexit x cf :: x1) tb ->
+      exists b rb,
+        tb = b ++ RBexit x cf :: rb
+        /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i').
   Proof.
+  Admitted.
+
+  Lemma map_truthy_step:
+    forall sp rs' m' pr' x b' i c,
+      truthy pr' x ->
+      SeqBB.step tge sp (Iexec (mki rs' pr' m')) b' (Iterm i c) ->
+      SeqBB.step tge sp (Iexec (mki rs' pr' m')) (map (map_if_convert x) b') (Iterm i c).
+  Proof.
+    intros * H1 H2.
     Admitted.
 
-  Lemma temp2:
+  Lemma match_none_correct :
     forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk',
       (fn_code f) ! pc = Some bb ->
       SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
@@ -393,19 +418,53 @@ Section CORRECTNESS.
       do 3 econstructor. apply plus_one. econstructor; eauto.
       apply seqbb_eq; eauto. eauto.
     - simplify.
-      destruct (cf_dec cf pc'); subst. inv H1.
-      exploit exec_if_conv; eauto; simplify.
-      exploit exec_rbexit_truthy; eauto; simplify.
-      apply sim_star. exists (Some b'). exists (State stk' (transf_function f) sp pc rs pr m).
-      simplify; try (unfold ltof; auto). apply star_refl.
-      constructor; auto. unfold sem_extrap; simplify.
-
-  Lemma step_cf_matches :
-    forall b s cf t s' ts,
-      step_cf_instr ge s cf t s' ->
-      match_states b s ts ->
-      exists b' ts', step_cf_instr tge ts cf t ts' /\ match_states b' s' ts'.
-  Proof. Admitted.
+      destruct (cf_dec cf pc'); subst.
+      + inv H1.
+        exploit exec_rbexit_truthy; eauto; simplify.
+        exploit exec_if_conv; eauto; simplify.
+        apply sim_star. exists (Some b'). exists (State stk' (transf_function f) sp pc rs pr m).
+        simplify; try (unfold ltof; auto). apply star_refl.
+        constructor; auto. unfold sem_extrap; simplify.
+        destruct out_s. exfalso; eapply step_list_false; eauto.
+        apply append. exists (mki rs' pr' m'). split.
+        eapply step_list_2_eq; eauto.
+        apply append2. eapply map_truthy_step; eauto.
+        econstructor; eauto. constructor; auto.
+      + exploit exec_rbexit_truthy; eauto; simplify.
+        exploit exec_if_conv2; eauto; simplify.
+        exploit step_cf_eq; eauto; simplify.
+        apply sim_plus. exists None. exists x4.
+        split. apply plus_one. econstructor; eauto.
+        apply append. exists (mki rs' pr' m'). split; auto.
+        apply step_list_2_eq; auto.
+        constructor. constructor; auto. auto.
+  Qed.
+
+  Lemma match_some_correct:
+    forall t s1' s f sp pc rs m pr rs' m' bb pr' cf stk' b0 pc1 rs1 p0 m1,
+      step ge (State s f sp pc rs pr m) t s1' ->
+      (fn_code f) ! pc = Some bb ->
+      SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
+      step_cf_instr ge (State s f sp pc rs' pr' m') cf t s1' ->
+      Forall2 match_stackframe s stk' ->
+      (fn_code f) ! pc = Some b0 ->
+      sem_extrap (transf_function f) pc1 sp (Iexec (mki rs pr m)) (Iexec (mki rs1 p0 m1)) b0 ->
+      step ge (State s f sp pc1 rs1 p0 m1) E0 (State s f sp pc rs pr m) ->
+      exists b' s2',
+        (plus step tge (State stk' (transf_function f) sp pc1 rs1 p0 m1) t s2' \/
+           star step tge (State stk' (transf_function f) sp pc1 rs1 p0 m1) t s2' /\
+             ltof (option SeqBB.t) measure b' (Some b0)) /\ match_states b' s1' s2'.
+  Proof.
+    intros * H H0 H1 H2 STK IS_B EXTRAP SIM.
+    rewrite IS_B in H0; simplify.
+    exploit step_cf_eq; eauto; simplify.
+    apply sim_plus.
+    exists None. exists x.
+    split; auto.
+    unfold sem_extrap in *.
+    inv SIM.
+    pose proof (transf_spec_correct f pc1) as X. inv X.
+    eapply plus_two. econstructor; eauto.
 
   Lemma transf_correct:
     forall s1 t s1',
@@ -418,8 +477,9 @@ Section CORRECTNESS.
   Proof using TRANSL.
     inversion 1; subst; simplify;
       match goal with H: context[match_states] |- _ => inv H end.
-    - admit.
-    - eauto using temp2. Admitted.
+    -
+    - eauto using match_none_correct.
+    - Admitted.
 
 
     (* - *)