Work on CondElim proof

6 files changed, 111 insertions, 24 deletions

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index ab0511f..9992b1c 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -728,11 +728,11 @@ Definition beq_pred_expr (pe1 pe2: pred_expr) : bool :=
 
 Definition check := Rtree.beq beq_pred_expr.
 
-Compute (check (empty # (Reg 2) <-
-                ((((Pand (Plit (true, 4)) (¬ (Plit (true, 4))))), (Ebase (Reg 9))) ::|
-                                                                      (NE.singleton (((Plit (true, 2))), (Ebase (Reg 3))))))
-               (empty # (Reg 2) <- (NE.singleton (((Por (Plit (true, 2)) (Pand (Plit (true, 3)) (¬ (Plit (true, 3)))))),
-                                                  (Ebase (Reg 3)))))).
+(* Compute (check (empty # (Reg 2) <- *)
+(*                 ((((Pand (Plit (true, 4)) (¬ (Plit (true, 4))))), (Ebase (Reg 9))) ::| *)
+(*                                                                       (NE.singleton (((Plit (true, 2))), (Ebase (Reg 3)))))) *)
+(*                (empty # (Reg 2) <- (NE.singleton (((Por (Plit (true, 2)) (Pand (Plit (true, 3)) (¬ (Plit (true, 3)))))), *)
+(*                                                   (Ebase (Reg 3)))))). *)
 
 Lemma inj_asgn_eg : forall a b, (a =? b)%nat = (a =? a)%nat -> a = b.
 Proof.
diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v
index f16a710..cdd3298 100644
--- a/src/hls/CondElimproof.v
+++ b/src/hls/CondElimproof.v
@@ -61,13 +61,80 @@ Lemma random1 :
 Proof.
 Admitted.
 
+Lemma append :
+  forall A B cf i0 i1 l0 l1 sp ge,
+      (exists i0', @SeqBB.step A B ge sp (Iexec i0) l0 (Iexec i0') /\
+                    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
+    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
+Proof. Admitted.
+
+Lemma append2 :
+  forall A B cf i0 i1 l0 l1 sp ge,
+    @SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) ->
+    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
+Proof. Admitted.
+
+Definition to_state stk f sp pc c :=
+  match c with
+  | Iexec (mk_instr_state rs ps m)
+  | Iterm (mk_instr_state rs ps m) _ =>
+      State stk f sp pc rs ps m
+  end.
+
+Definition to_cf c :=
+  match c with | Iterm _ cf => Some cf | _ => None end.
+
+#[local] Notation "'mki'" := (mk_instr_state) (at level 1).
+
+Definition max_predset (ps: predset) :=
+  fold_left Pos.max (map fst (PTree.elements (snd ps))) 1.
+
+Variant match_ps : positive -> predset -> predset -> Prop :=
+| match_ps_intro :
+  forall ps ps' m,
+    (forall x, x <= m -> ps !! x = ps' !! x) ->
+    match_ps m ps ps'.
+
+Lemma elim_cond_s_spec :
+  forall A B ge sp rs m rs' m' ps tps ps' p a p0 l v,
+    step_instr ge sp (Iexec (mki rs ps m)) a (Iexec (mki rs' ps' m')) ->
+    max_pred_instr v a <= v ->
+    match_ps v ps tps ->
+    elim_cond_s p a = (p0, l) ->
+    exists tps',
+      step_list2 (@step_instr A B ge) sp (Iexec (mki rs tps m)) l (Iexec (mki rs' tps' m'))
+      /\ match_ps v ps' tps'.
+Proof.
+  inversion 1; subst; simplify; inv H.
+  - inv H2. econstructor. split; eauto; econstructor; econstructor.
+  - inv H2. econstructor. split; eauto; econstructor; econstructor. eauto.
+
+
 Lemma replace_section_spec :
-  forall A B ge sp is_ is_' bb cf,
-    @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) ->
-    exists p,
-      @SeqBB.step A B ge sp (Iexec is_)
-                  (snd (replace_section elim_cond_s p bb))
-                  (Iterm is_' cf). Admitted.
+  forall ge sp bb rs ps m rs' ps' m' stk f t cf pc pc' rs'' ps'' m'' tps,
+    SeqBB.step ge sp (Iexec (mki rs ps m)) bb (Iterm (mki rs' ps' m') cf) ->
+    step_cf_instr ge (State stk f sp pc rs' ps' m') cf t (State stk f sp pc' rs'' ps'' m'') ->
+    match_ps ps tps ->
+    exists p tps' tps'',
+      SeqBB.step ge sp (Iexec (mki rs tps m)) (snd (replace_section elim_cond_s p bb))
+                 (Iterm (mki rs' tps' m') cf)
+      /\ match_ps ps' tps'
+      /\ step_cf_instr ge (State stk f sp pc rs' tps' m') cf t (State stk f sp pc' rs'' tps'' m'')
+      /\ match_ps ps'' tps''.
+Proof.
+  induction bb; simplify; inv H.
+  - destruct state'.
+    econstructor; simplify; repeat destruct_match; simplify.
+    exploit IHbb; eauto; simplify.
+    eapply append. econstructor; simplify.
+    eapply F_correct; eauto. rewrite Heqp in H. eauto.
+    eauto.
+  - econstructor; simplify; repeat destruct_match; simplify.
+    eapply append2. eapply F_correct; eauto. eauto.
+    Unshelve. exact default.
+Qed.
+
+End REPLACE.
 
 Lemma transf_block_spec :
   forall f pc b,
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index 0ab8c1f..ea6bece 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -140,6 +140,16 @@ Definition max_reg_instr (m: positive) (i: instr) :=
   | RBexit _ c => max_reg_cfi m c
   end.
 
+Definition max_pred_instr (m: positive) (i: instr) :=
+  match i with
+  | RBop (Some p) op args res => Pos.max m (max_predicate p)
+  | RBload (Some p) chunk addr args dst => Pos.max m (max_predicate p)
+  | RBstore (Some p) chunk addr args src => Pos.max m (max_predicate p)
+  | RBsetpred (Some p') c args p => Pos.max m (Pos.max p (max_predicate p'))
+  | RBexit (Some p) c => Pos.max m (max_predicate p)
+  | _ => m
+  end.
+
 Definition regset := Regmap.t val.
 Definition predset := PMap.t bool.
 
@@ -293,6 +303,16 @@ Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop):
     step_i sp (Iexec state) i (Iterm state' cf) ->
     step_list step_i sp (Iexec state) (i :: instrs) (Iterm state' cf).
 
+Inductive step_list2 {A} (step_i: val -> istate -> A -> istate -> Prop):
+  val -> istate -> list A -> istate -> Prop :=
+| exec_RBcons2 :
+  forall i0 i1 i2 i instrs sp,
+    step_i sp i0 i i1 ->
+    step_list2 step_i sp i1 instrs i2 ->
+    step_list2 step_i sp i0 (i :: instrs) i2
+| exec_RBnil2 :
+  forall sp i, step_list2 step_i sp i nil i.
+
 (*|
 Top-Level Type Definitions
 ==========================
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 30eb250..e66451d 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -32,7 +32,7 @@ Require Import vericert.hls.Gible.
 
 (*|
 ========
-RTLBlock
+GibleSeq
 ========
 |*)
 
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index c6fe853..087b119 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -566,8 +566,8 @@ Defined.
 
 #[local] Open Scope positive.
 
-Compute tseytin_simple (Por (negate (Pand (Por (Plit (true, 1)) (Plit (true, 2))) (Plit (true, 3)))) (Plit (false, 4))).
-Compute sat_pred_simple (Por Pfalse (Pand (Plit (true, 1)) (Plit (false, 1)))).
+(* Compute tseytin_simple (Por (negate (Pand (Por (Plit (true, 1)) (Plit (true, 2))) (Plit (true, 3)))) (Plit (false, 4))). *)
+(* Compute sat_pred_simple (Por Pfalse (Pand (Plit (true, 1)) (Plit (false, 1)))). *)
 
 Lemma sat_dec a: {sat a} + {unsat a}.
 Proof.
@@ -584,7 +584,7 @@ Definition equiv_check p1 p2 :=
   | _ => false
   end.
 
-Compute equiv_check Pfalse (Pand (Plit (true, 1%positive)) (Plit (false, 1%positive))).
+(* Compute equiv_check Pfalse (Pand (Plit (true, 1%positive)) (Plit (false, 1%positive))). *)
 
 Lemma equiv_check_correct :
   forall p1 p2, equiv_check p1 p2 = true -> p1 == p2.
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 428c176..ae0a05c 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -246,13 +246,13 @@ Definition setFormulaSimple (fm : formula) (l : lit) :=
   | inright _ => None
   end.
 
-Eval compute in setFormulaSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil) (true, 1%nat).
-Eval compute in setFormulaSimple nil (true, 0).
-Eval compute in setFormulaSimple (((true, 0) :: nil) :: nil) (true, 0).
-Eval compute in setFormulaSimple (((false, 0) :: nil) :: nil) (true, 0).
-Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0).
-Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0).
-Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0).
+(* Eval compute in setFormulaSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil) (true, 1%nat). *)
+(* Eval compute in setFormulaSimple nil (true, 0). *)
+(* Eval compute in setFormulaSimple (((true, 0) :: nil) :: nil) (true, 0). *)
+(* Eval compute in setFormulaSimple (((false, 0) :: nil) :: nil) (true, 0). *)
+(* Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0). *)
+(* Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0). *)
+(* Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0). *)
 
 #[local] Hint Extern 1 False => discriminate : core.
 
@@ -483,7 +483,7 @@ Definition lit_set_cl (cl: clause) :=
 Definition lit_set (fm: formula) :=
   fold_right NSet.union NSet.empty (map lit_set_cl fm).
 
-Compute NSet.cardinal (lit_set (((true, 1)::(true, 1)::(true, 1)::nil)::nil)).
+(* Compute NSet.cardinal (lit_set (((true, 1)::(true, 1)::(true, 1)::nil)::nil)). *)
 
 Definition sat_measure (fm: formula) := NSet.cardinal (lit_set fm).
 
@@ -658,4 +658,4 @@ Definition satSolveSimple (fm : formula) :=
   | inright _ => None
   end.
 
-Eval compute in satSolveSimple nil.
+(* Eval compute in satSolveSimple nil. *)