From 27da714aa3f00f8b8b62bd8b98d9cdc8d8cbd79e Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Sat, 26 Oct 2024 14:57:43 -0400 Subject: [PATCH] fix align_trace tactic and move it to LeakageSemantics --- bedrock2/src/bedrock2/LeakageProgramLogic.v | 14 ---------- bedrock2/src/bedrock2/LeakageSemantics.v | 29 ++++++++++++++++++++ compiler/src/compiler/DeadCodeElim.v | 30 +++++++++------------ 3 files changed, 42 insertions(+), 31 deletions(-) diff --git a/bedrock2/src/bedrock2/LeakageProgramLogic.v b/bedrock2/src/bedrock2/LeakageProgramLogic.v index bf6112ac..802d6d78 100644 --- 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 index d957e38e..a913deb3 100644 --- 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 index c0bafcbd..b99d85f0 100644 --- 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.