fix align_trace tactic and move it to LeakageSemantics

mit-plv · Oct 26, 2024 · 27da714 · 27da714
1 parent 091b043
commit 27da714
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 31 deletions.
diff --git a/bedrock2/src/bedrock2/LeakageProgramLogic.v b/bedrock2/src/bedrock2/LeakageProgramLogic.v
@@ -10,20 +10,6 @@ Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars.
 Definition spec_of (procname:String.string) := Semantics.env -> Prop.
 Existing Class spec_of.
 
-(* not sure where to put these lemmas *)
-Lemma align_trace_cons {T} x xs cont t (H : xs = List.app cont t) : @List.cons T x xs = List.app (cons x cont) t.
-Proof. intros. cbn. congruence. Qed.
-Lemma align_trace_app {T} x xs cont t (H : xs = List.app cont t) : @List.app T x xs = List.app (List.app x cont) t.
-Proof. intros. cbn. subst. rewrite List.app_assoc; trivial. Qed.
-
-Ltac align_trace :=
-    repeat match goal with
-      | t := cons _ _ |- _ => subst t
-      end;
-    repeat (eapply align_trace_app
-            || eapply align_trace_cons
-            || exact (eq_refl (List.app nil _))).
-
 Module Import Coercions.
   Import Map.Interface Word.Interface BinInt.
   Coercion Z.of_nat : nat >-> Z.

diff --git a/bedrock2/src/bedrock2/LeakageSemantics.v b/bedrock2/src/bedrock2/LeakageSemantics.v
@@ -8,6 +8,35 @@ Require Export bedrock2.Memory.
 Require Import bedrock2.Semantics.
 Require Import Coq.Lists.List.
 
+(*list lemmas and tactics that are useful for proving equality of leakage traces*)
+Lemma align_trace_cons {T} x xs cont t (H : xs = List.app cont t) : @List.cons T x xs = List.app (cons x cont) t.
+Proof. intros. cbn. congruence. Qed.
+
+Lemma align_trace_app {T} x xs cont t (H : xs = List.app cont t) : @List.app T x xs = List.app (List.app x cont) t.
+Proof. intros. cbn. subst. rewrite List.app_assoc; trivial. Qed.
+
+Lemma align_trace_nil {A : Type} (l : list A) : l = nil ++ l. Proof. reflexivity. Qed.
+
+Ltac align_trace_bad :=
+  repeat match goal with
+    | t:=_ :: _:_ |- _ => subst t
+    end;
+  repeat eapply align_trace_app || eapply align_trace_cons || eapply align_trace_nil || reflexivity.
+
+Goal exists (x y z : list nat), x ++ y = z. do 3 eexists. Fail Timeout 1 align_trace_bad. Abort.
+
+Ltac align_trace :=
+  repeat match goal with
+    | t:=_ :: _:_ |- _ => subst t
+    end;
+  repeat exact eq_refl || eapply align_trace_app || eapply align_trace_cons || eapply align_trace_nil.
+
+Goal exists (x y z : list nat), x ++ y = z. do 3 eexists. align_trace. Abort.
+
+Lemma associate_one_left {A : Type} (x : A) l1 l2 :
+  l1 ++ x :: l2 = (l1 ++ (x :: nil)) ++ l2.
+Proof. rewrite <- app_assoc. reflexivity. Qed.
+
 Inductive leakage_event {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
 | leak_unit
 | leak_bool (b : bool)

diff --git a/compiler/src/compiler/DeadCodeElim.v b/compiler/src/compiler/DeadCodeElim.v
@@ -1,5 +1,4 @@
 Require Import bedrock2.LeakageSemantics.
-Require Import bedrock2.LeakageProgramLogic. (*just for align_trace tactic, probbaly should move it to leakageSemantics...*)
 Require Import compiler.FlatImp.
 Require Import Coq.Lists.List. Import ListNotations.
 Require Import bedrock2.Syntax.
@@ -111,16 +110,13 @@ Section WithArguments1.
         rewrite ListSet.of_list_removeb
     end.
 
-  Ltac solve_compile_post' align_trace' :=
-    do 5 eexists; ssplit; [eauto | repeat listset_to_set; agree_on_solve | scost_hammer | align_trace' | align_trace' | intros; rewrite dfix_step; repeat (match goal with
-             | |- context[rev (?a ++ ?b)] => rewrite (rev_app_distr a b)
-                                                                                                                                                           end || cbn [List.app List.rev]); cbv beta; try reflexivity ].
-  (*TODO: this thing doesn't fail properly, it hangs instead, getting stuck in align_trace.  need some way to make align_trace stop when everything is evars*)
-  Ltac solve_compile_post := solve_compile_post' align_trace.
-
-  Lemma associate_left {A : Type} (x : A) l1 l2 :
-    l1 ++ x :: l2 = (l1 ++ [x]) ++ l2.
-  Proof. rewrite <- app_assoc. reflexivity. Qed.
+  Ltac solve_compile_post :=
+    do 5 eexists; ssplit;
+    [eauto | repeat listset_to_set; agree_on_solve | scost_hammer | align_trace | align_trace |
+      intros; rewrite dfix_step;
+      repeat (match goal with
+              | |- context[rev (?a ++ ?b)] => rewrite (rev_app_distr a b)
+              end || cbn [List.app List.rev]); cbv beta; try reflexivity ].
 
   Lemma dce_correct_aux :
     forall eH eL pick_spL,
@@ -165,7 +161,7 @@ Section WithArguments1.
         * listset_to_set. agree_on_solve.
       + eapply IHexec.
         -- eapply agree_on_refl.
-        -- intros. rewrite associate_left. rewrite H6. rewrite dfix_step.
+        -- intros. rewrite associate_one_left. rewrite H6. rewrite dfix_step.
            simpl. rewrite rev_app_distr. simpl. rewrite H0.
            rewrite <- app_assoc. reflexivity. 
       + intros.
@@ -223,7 +219,7 @@ Section WithArguments1.
            split; [eassumption|]. split; [eassumption|].
            solve_compile_post. simpl. rewrite H7p5. reflexivity.
         -- agree_on_solve.
-        -- intros. rewrite associate_left. rewrite H4. rewrite dfix_step. simpl.
+        -- intros. rewrite associate_one_left. rewrite H4. rewrite dfix_step. simpl.
            rewrite rev_app_distr. simpl. repeat Tactics.destruct_one_match.
            repeat rewrite <- app_assoc. reflexivity.
     - intros. destr (existsb (eqb x) used_after).
@@ -274,7 +270,7 @@ Section WithArguments1.
       + erewrite agree_on_eval_bcond; [ eassumption | ].
         pose agree_on_comm; eauto.
       + eapply @exec.weaken.
-        -- eapply IHexec; eauto. intros. rewrite associate_left. rewrite H3.
+        -- eapply IHexec; eauto. intros. rewrite associate_one_left. rewrite H3.
            rewrite dfix_step. rewrite rev_app_distr. simpl.
            repeat Tactics.destruct_one_match. rewrite <- app_assoc. reflexivity.
         -- unfold compile_post. intros. fwd. solve_compile_post.
@@ -287,7 +283,7 @@ Section WithArguments1.
       + erewrite agree_on_eval_bcond; [ eassumption | ].
         pose agree_on_comm; eauto.
       + eapply @exec.weaken.
-        -- eapply IHexec; eauto. intros. rewrite associate_left. rewrite H3.
+        -- eapply IHexec; eauto. intros. rewrite associate_one_left. rewrite H3.
            rewrite dfix_step. rewrite rev_app_distr. simpl.
            repeat rewrite <- app_assoc. repeat Tactics.destruct_one_match.
            reflexivity.
@@ -333,7 +329,7 @@ Section WithArguments1.
           - repeat listset_to_set.
             eapply agree_on_subset; [ | eapply H4p1 ].
             subset_union_solve.
-          - intros. rewrite associate_left. rewrite app_assoc. rewrite H8.
+          - intros. rewrite associate_one_left. rewrite app_assoc. rewrite H8.
             repeat (rewrite rev_app_distr || cbn [rev List.app] || rewrite <- app_assoc).
             rewrite dfix_step. cbn [stmt_leakage_body]. rewrite H4p5.
             cbv [CustomFix.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.
@@ -342,7 +338,7 @@ Section WithArguments1.
         cbv beta. intros. fwd.
         eapply exec.weaken.
         { eapply IH12; [eassumption|eassumption|].
-          intros. rewrite associate_left. repeat rewrite app_assoc. rewrite H8.
+          intros. rewrite associate_one_left. repeat rewrite app_assoc. rewrite H8.
           repeat (rewrite rev_app_distr || cbn [rev List.app] || rewrite <- app_assoc).
           f_equal. f_equal. rewrite dfix_step. cbn [stmt_leakage_body]. rewrite H4p5.
           cbv [CustomFix.Let_In_pf_nd]. rewrite List.skipn_app_r by reflexivity.