HypreSpectre.Preserve_mem
From HypreSpectre Require Import
Lang
Mitigation
Leak
Prefix_sens.
From Coq Require Import
Program.Basics
Program.Equality.
From HyPre Require Import
BarrierSync
HyperPreserve
HyperPreserveBarrier
NonInterference
StateSimulation.
From Equations Require Import Equations.
Open Scope program_scope.
Lang
Mitigation
Leak
Prefix_sens.
From Coq Require Import
Program.Basics
Program.Equality.
From HyPre Require Import
BarrierSync
HyperPreserve
HyperPreserveBarrier
NonInterference
StateSimulation.
From Equations Require Import Equations.
Open Scope program_scope.
Definition is_B (s : state) := match s with
| (_, _, nil) => true
| (_, _, (Read _ _) :: l) => true
| (_, _, (Write _ _) :: l) => true
| _ => false
end.
Definition sem_nonspec : list stmt -> heap -> list state -> Prop := nonspec_trace.
Definition vsem_nonspec p : Vector.t heap 2 -> Vector.t (list state) 2 -> Prop := Vector.Forall2 (sem_nonspec p).
Definition sem_spec_am : list stmt -> heap -> list (list specstate) -> Prop := spec_am_trace.
Definition vsem_spec_am p : Vector.t heap 2 -> Vector.t (list (list specstate)) 2 -> Prop := Vector.Forall2 (sem_spec_am p).
| (_, _, nil) => true
| (_, _, (Read _ _) :: l) => true
| (_, _, (Write _ _) :: l) => true
| _ => false
end.
Definition sem_nonspec : list stmt -> heap -> list state -> Prop := nonspec_trace.
Definition vsem_nonspec p : Vector.t heap 2 -> Vector.t (list state) 2 -> Prop := Vector.Forall2 (sem_nonspec p).
Definition sem_spec_am : list stmt -> heap -> list (list specstate) -> Prop := spec_am_trace.
Definition vsem_spec_am p : Vector.t heap 2 -> Vector.t (list (list specstate)) 2 -> Prop := Vector.Forall2 (sem_spec_am p).
Barrier states produce leakage, other states do not
Lemma barrier_leak V H s:
is_B (V, H, s) = true -> exists x, leak_mem (V, H, s) = Some x.
Proof with eexists; easy.
intros. destruct s.
- now eexists.
- destruct s; cbn in H0; try congruence.
+ eexists...
+ simpl. destruct (Z_lt_dec (eval_expr_fun a V)). eexists...
destruct (alist_find _ x V)...
Qed.
Lemma no_barrier_no_leak V H s:
is_B (V, H, s) = false -> leak_mem (V, H, s) = None.
Proof.
intros. destruct s.
- simpl in H0. congruence.
- destruct s; cbn; try easy.
Qed.
Lemma forall_not_isB_leak_nil:
forall bs, Forall (fun s => is_B s = false) bs -> apply_lf' (rem_None ∘ leak_mem) bs = nil.
Proof.
intros bs.
induction bs; intros Hbs.
- reflexivity.
- rewrite apply_lf'_S.
eapply Forall_cons_iff in Hbs.
destructH.
enough ((rem_None ∘ leak_mem) a = nil) as Q.
+ rewrite Q. cbn.
eapply IHbs. assumption.
+ unfold compose.
destruct a as [ [V H] s].
rewrite no_barrier_no_leak. 2: easy.
cbn. reflexivity.
Qed.
Lemma Forall2_map_eq2 X X' Y:
forall (f : X -> Y) (f' : X' -> Y) (xl1 : list X) (xl2 : list X'),
Forall2 (fun x0 y0 => f x0 = f' y0) xl1 xl2 ->
map f xl1 = map f' xl2.
Proof.
intros.
induction H;cbn;eauto.
now rewrite H, IHForall2.
Qed.
Lemma vec_forall2_map_eq2 {k} {X X' Y : Type} (f : X -> Y) (f' : X' -> Y) (xl1 : Vector.t X k) (xl2 : Vector.t X' k) :
Vector.Forall2 (fun x y => f x = f' y) xl1 xl2 -> Vector.map f xl1 = Vector.map f' xl2.
Proof.
intros.
dependent induction H; eauto.
setoid_rewrite vec_map_cons.
rewrite H, IHForall2. reflexivity.
Qed.
Lemma list_app_unchanged {T} (a b: list T) :
b = a ++ b -> a = nil.
Proof.
intros.
assert (|b| = |a ++ b|).
- rewrite H at 1. easy.
- rewrite app_length in H0.
assert (|a| = 0) by lia.
now apply length_zero_iff_nil.
Qed.
is_B (V, H, s) = true -> exists x, leak_mem (V, H, s) = Some x.
Proof with eexists; easy.
intros. destruct s.
- now eexists.
- destruct s; cbn in H0; try congruence.
+ eexists...
+ simpl. destruct (Z_lt_dec (eval_expr_fun a V)). eexists...
destruct (alist_find _ x V)...
Qed.
Lemma no_barrier_no_leak V H s:
is_B (V, H, s) = false -> leak_mem (V, H, s) = None.
Proof.
intros. destruct s.
- simpl in H0. congruence.
- destruct s; cbn; try easy.
Qed.
Lemma forall_not_isB_leak_nil:
forall bs, Forall (fun s => is_B s = false) bs -> apply_lf' (rem_None ∘ leak_mem) bs = nil.
Proof.
intros bs.
induction bs; intros Hbs.
- reflexivity.
- rewrite apply_lf'_S.
eapply Forall_cons_iff in Hbs.
destructH.
enough ((rem_None ∘ leak_mem) a = nil) as Q.
+ rewrite Q. cbn.
eapply IHbs. assumption.
+ unfold compose.
destruct a as [ [V H] s].
rewrite no_barrier_no_leak. 2: easy.
cbn. reflexivity.
Qed.
Lemma Forall2_map_eq2 X X' Y:
forall (f : X -> Y) (f' : X' -> Y) (xl1 : list X) (xl2 : list X'),
Forall2 (fun x0 y0 => f x0 = f' y0) xl1 xl2 ->
map f xl1 = map f' xl2.
Proof.
intros.
induction H;cbn;eauto.
now rewrite H, IHForall2.
Qed.
Lemma vec_forall2_map_eq2 {k} {X X' Y : Type} (f : X -> Y) (f' : X' -> Y) (xl1 : Vector.t X k) (xl2 : Vector.t X' k) :
Vector.Forall2 (fun x y => f x = f' y) xl1 xl2 -> Vector.map f xl1 = Vector.map f' xl2.
Proof.
intros.
dependent induction H; eauto.
setoid_rewrite vec_map_cons.
rewrite H, IHForall2. reflexivity.
Qed.
Lemma list_app_unchanged {T} (a b: list T) :
b = a ++ b -> a = nil.
Proof.
intros.
assert (|b| = |a ++ b|).
- rewrite H at 1. easy.
- rewrite app_length in H0.
assert (|a| = 0) by lia.
now apply length_zero_iff_nil.
Qed.
Lemma sim_same_leakage:
forall x y, cf_sim' x y -> leak_mem x = leak_mem' y.
Proof.
intros x y Hsim.
destruct x as [ [V H] s].
unfold cf_sim' in Hsim.
destruct s; rewrite Hsim. auto.
clear Hsim.
destruct s; auto.
Qed.
forall x y, cf_sim' x y -> leak_mem x = leak_mem' y.
Proof.
intros x y Hsim.
destruct x as [ [V H] s].
unfold cf_sim' in Hsim.
destruct s; rewrite Hsim. auto.
clear Hsim.
destruct s; auto.
Qed.
Simulation-related trace prefixes produce the same leakage.
Lemma sim_trace_same_leakage {p_src iv a α}:
nonspec_trace p_src iv a ->
spec_am_trace (comp_fence p_src) iv α ->
cf_sim p_src iv a α ->
apply_lf' (rem_None ∘ leak_mem) (a) = apply_lf' (rem_None ∘ leak_mem') (α).
Proof.
intros Ha Hα Hsim.
unfold cf_sim in Hsim.
induction Hsim.
- reflexivity.
- cbn. unfold compose. f_equal. f_equal. now eapply sim_same_leakage.
- rewrite apply_lf'_S. rewrite apply_lf'_app. rewrite IHHsim.
f_equal.
unfold spec_am_trace, multi_spec_am in Hα. apply multi_step_split in Hα as [Hβ Hα].
unfold multi_step_hd in Hβ.
rewrite H in Hsim. remember Hsim as Hsim'. clear HeqHsim'. apply lift_state_rel_cons_impl_cons in Hsim' as (α0 & αl & ?).
rewrite H3 in *. rewrite length_cons in Hα. unfold multi_step' in Hα.
rewrite length_cons in Hβ. rewrite multi_step_S2 in Hβ. unfold multi_step_hd in Hβ. rewrite Hα in Hβ.
simpl in Hβ. rewrite <- Hβ.
rewrite H1.
unfold nonspec_trace, multi_nonspec, multi_step' in Ha. rewrite H in Ha. rewrite! length_cons in Ha. rewrite multi_step_S2 in Ha.
inversion Ha. unfold multi_step_hd in H5. rewrite H6 in H5. simpl in H5.
unfold multi_step_hd. rewrite H6. simpl.
apply lift_state_rel_cons in Hsim.
clear H. destruct a0 as [ [V H] s].
unfold cf_sim' in Hsim. rewrite Hsim.
destruct s.
+ simpl. simp comp_fence. reflexivity.
+ destruct s; simpl; simp comp_fence; rewrite! apply_lf'_S; rewrite app_nil_r; unfold compose.
* f_equal. now apply sim_same_leakage.
* f_equal. destruct (alist_find decZ (eval_expr_fun a0 V) H); now apply sim_same_leakage.
* f_equal. destruct (alist_find _ x V); now apply sim_same_leakage.
* destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl spec_step_fun; rewrite app_nil_r; f_equal; rewrite <- comp_fence_app; now apply sim_same_leakage.
* f_equal.
* f_equal. now apply sim_same_leakage.
* f_equal. now apply sim_same_leakage.
+ clear - Ha.
unfold nonspec_trace in *. rewrite length_cons in Ha.
unfold multi_nonspec, multi_step' in *.
destruct a. reflexivity.
rewrite length_cons in *. rewrite multi_step_S2 in Ha. now inversion Ha.
+ clear - Hα.
unfold spec_am_trace in *.
now apply multi_step_split in Hα.
Qed.
nonspec_trace p_src iv a ->
spec_am_trace (comp_fence p_src) iv α ->
cf_sim p_src iv a α ->
apply_lf' (rem_None ∘ leak_mem) (a) = apply_lf' (rem_None ∘ leak_mem') (α).
Proof.
intros Ha Hα Hsim.
unfold cf_sim in Hsim.
induction Hsim.
- reflexivity.
- cbn. unfold compose. f_equal. f_equal. now eapply sim_same_leakage.
- rewrite apply_lf'_S. rewrite apply_lf'_app. rewrite IHHsim.
f_equal.
unfold spec_am_trace, multi_spec_am in Hα. apply multi_step_split in Hα as [Hβ Hα].
unfold multi_step_hd in Hβ.
rewrite H in Hsim. remember Hsim as Hsim'. clear HeqHsim'. apply lift_state_rel_cons_impl_cons in Hsim' as (α0 & αl & ?).
rewrite H3 in *. rewrite length_cons in Hα. unfold multi_step' in Hα.
rewrite length_cons in Hβ. rewrite multi_step_S2 in Hβ. unfold multi_step_hd in Hβ. rewrite Hα in Hβ.
simpl in Hβ. rewrite <- Hβ.
rewrite H1.
unfold nonspec_trace, multi_nonspec, multi_step' in Ha. rewrite H in Ha. rewrite! length_cons in Ha. rewrite multi_step_S2 in Ha.
inversion Ha. unfold multi_step_hd in H5. rewrite H6 in H5. simpl in H5.
unfold multi_step_hd. rewrite H6. simpl.
apply lift_state_rel_cons in Hsim.
clear H. destruct a0 as [ [V H] s].
unfold cf_sim' in Hsim. rewrite Hsim.
destruct s.
+ simpl. simp comp_fence. reflexivity.
+ destruct s; simpl; simp comp_fence; rewrite! apply_lf'_S; rewrite app_nil_r; unfold compose.
* f_equal. now apply sim_same_leakage.
* f_equal. destruct (alist_find decZ (eval_expr_fun a0 V) H); now apply sim_same_leakage.
* f_equal. destruct (alist_find _ x V); now apply sim_same_leakage.
* destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl spec_step_fun; rewrite app_nil_r; f_equal; rewrite <- comp_fence_app; now apply sim_same_leakage.
* f_equal.
* f_equal. now apply sim_same_leakage.
* f_equal. now apply sim_same_leakage.
+ clear - Ha.
unfold nonspec_trace in *. rewrite length_cons in Ha.
unfold multi_nonspec, multi_step' in *.
destruct a. reflexivity.
rewrite length_cons in *. rewrite multi_step_S2 in Ha. now inversion Ha.
+ clear - Hα.
unfold spec_am_trace in *.
now apply multi_step_split in Hα.
Qed.
Lemma mem_hypersim iv p_src
(Hsrc_safe: forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre_sens (rem_None ∘ leak_mem) nonspec_trace p_src iv) a) (*assuming termination sensitive leakage equivalence*)
:
hyper_preserve_barrier_c5
iv
(v2 (ll_eq (rem_None ∘ leak_mem))) (*source relation*)
(v2 (ll_eq (rem_None ∘ leak_mem'))) (*target relation*)
(nonspec_trace p_src)
(spec_am_trace (comp_fence p_src))
(nonspec_trace_linear_semantics p_src)
(spec_am_trace_linear_semantics (comp_fence p_src))
(cf_sim p_src)
(cf_sim_sync p_src)
(fun _ _ => 1)
(tsync_cf p_src)
is_B.
Proof.
econstructor.
- eapply vl_ll_eq_zero. (*all relations are satisfied by initial empty trace prefixes*)
- eapply vl_ll_eq_zero.
- eapply cf_sim_nil.
- intros a Ha α Hα Hsim b Hsem β Hsem' Hsim' b0 bs Hbeq Hb0 Hbs.
split1. (*show first for source*)
+ eapply vl_ll_pre_len_ll_eq. (*conclude from Hsrc_safe*)
* exact eqDec_obs.
* eapply Hsrc_safe.
eapply Hsem.
* rewrite Hbeq.
rewrite vl_cons_app.
unfold v2.
do 2 rewrite veclist_cons_nth.
setoid_rewrite apply_lf'_S.
setoid_rewrite app_length.
match goal with [|- ?x + ?y = ?w + ?z] => assert (x = w) as Q1;[|assert (y = z) as Q2] end.
3: lia.
++ clear - Hb0. (*new barrier states both produce 1 leakage*)
eapply vector_forall_nth with (i := Fin.F1) in Hb0 as Hb1.
eapply vector_forall_nth with (i := Fin.FS Fin.F1) in Hb0 as Hb2.
destruct (b0 [[Fin.F1]]), (b0 [[Fin.FS Fin.F1]]).
unfold compose.
destruct p, p0.
destruct (barrier_leak v h l), (barrier_leak v0 h0 l0); try easy.
rewrite H, H0. reflexivity.
++ setoid_rewrite veclist_app_nth.
setoid_rewrite apply_lf'_app.
setoid_rewrite app_length.
match goal with [|- ?x + ?y = ?w + ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: lia.
** (*intermediate states produce no leakage*)
specialize (vector_forall_nth _ _ _ Hbs) as Hnth.
assert (forall i: Fin.t 2, Forall (fun s : state => (is_B s = false)%type) (bs [[i]])) as Hnth'.
{ clear - Hnth.
intros.
eapply Forall_impl.
2: eapply Hnth.
intros.
cbn in H.
destruct (is_B a); congruence.
}
rewrite forall_not_isB_leak_nil. 2: auto.
rewrite forall_not_isB_leak_nil. 2: auto.
reflexivity.
** unfold ll_eq in Ha. (*states from previous step*)
unfold v2 in Ha.
rewrite Ha.
reflexivity.
+ intros Hsrc_ni. unfold v2. (*translate to target using sim_trace_same_leakage*)
unfold ll_eq.
unfold v2, ll_eq in Hsrc_ni.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
exact Hsrc_ni.
- eapply cf_sim_sync_correct.
- (* If one trace does not reach another barrier, the relations are also satisfied *)
intros a i Ha Hnoleak α Hα Hsim b Hsem β Hsem' Hsim'.
split1. (*show for source trace, then transfer to target*)
+ clear Hα Hsim Hsem' Hsim' α β.
unfold v2, ll_eq.
specialize (Hsrc_safe (veclist_app b a) Hsem).
do 3 dependent destruction a.
do 3 dependent destruction b.
unfold v2, ll_pre_sens in Hsrc_safe.
dependent destruction i. (*proof is the same no matter which trace is known to not produce more leakage, but we need to repeat it*)
* simpl in *. (*leakage of h1 must be None by Hnoleak*)
destruct Hsrc_safe as [_ [b1 [b2 Hsrc_safe] ] ].
destruct Hsrc_safe as [Hsrc_safe [Hb1 Hb2] ].
unfold ll_eq in Hsrc_safe.
rewrite app_assoc in Hsrc_safe, Hb1.
rewrite app_assoc in Hsrc_safe, Hb2.
specialize (Hnoleak (b1 ++ h1) Hb1).
apply forall_not_isB_leak_nil in Hnoleak.
unfold v2, ll_eq in Ha. simpl in Ha.
rewrite apply_lf'_app in Hsrc_safe.
rewrite Hnoleak in Hsrc_safe. simpl in Hsrc_safe.
rewrite! apply_lf'_app.
rewrite apply_lf'_app in Hsrc_safe.
rewrite Ha in *.
f_equal.
apply list_app_unchanged in Hsrc_safe. (*No matter how we extend h2, the leakage must be equal to some extension of h1, which must always be nil. Thus, h2 must be nil*)
rewrite apply_lf'_app in Hsrc_safe, Hnoleak.
symmetry in Hsrc_safe, Hnoleak. apply app_nil_eq in Hsrc_safe, Hnoleak.
destruct Hsrc_safe, Hnoleak. now rewrite H2, H0.
* dependent destruction i. 2: dependent destruction i. (*same as above.*)
simpl in *.
destruct Hsrc_safe as [_ [b1 [b2 Hsrc_safe] ] ].
destruct Hsrc_safe as [Hsrc_safe [Hb1 Hb2] ].
unfold ll_eq in Hsrc_safe.
rewrite app_assoc in Hsrc_safe, Hb1.
rewrite app_assoc in Hsrc_safe, Hb2.
specialize (Hnoleak (b2 ++ h2) Hb2).
apply forall_not_isB_leak_nil in Hnoleak.
unfold v2, ll_eq in Ha. simpl in Ha.
rewrite (apply_lf'_app h0 (b2 ++ h2)) in Hsrc_safe.
rewrite Hnoleak in Hsrc_safe. simpl in Hsrc_safe.
rewrite! apply_lf'_app.
rewrite apply_lf'_app in Hsrc_safe.
rewrite Ha in *.
f_equal.
symmetry in Hsrc_safe. apply list_app_unchanged in Hsrc_safe.
rewrite apply_lf'_app in Hsrc_safe, Hnoleak.
symmetry in Hsrc_safe, Hnoleak. apply app_nil_eq in Hsrc_safe, Hnoleak.
destruct Hsrc_safe, Hnoleak. now rewrite H2, H0.
+ intros Hsrc_ni. unfold v2. (*translate to target using sim_trace_same_leakage.*)
unfold ll_eq.
unfold v2, ll_eq in Hsrc_ni.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
exact Hsrc_ni.
Qed.
(Hsrc_safe: forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre_sens (rem_None ∘ leak_mem) nonspec_trace p_src iv) a) (*assuming termination sensitive leakage equivalence*)
:
hyper_preserve_barrier_c5
iv
(v2 (ll_eq (rem_None ∘ leak_mem))) (*source relation*)
(v2 (ll_eq (rem_None ∘ leak_mem'))) (*target relation*)
(nonspec_trace p_src)
(spec_am_trace (comp_fence p_src))
(nonspec_trace_linear_semantics p_src)
(spec_am_trace_linear_semantics (comp_fence p_src))
(cf_sim p_src)
(cf_sim_sync p_src)
(fun _ _ => 1)
(tsync_cf p_src)
is_B.
Proof.
econstructor.
- eapply vl_ll_eq_zero. (*all relations are satisfied by initial empty trace prefixes*)
- eapply vl_ll_eq_zero.
- eapply cf_sim_nil.
- intros a Ha α Hα Hsim b Hsem β Hsem' Hsim' b0 bs Hbeq Hb0 Hbs.
split1. (*show first for source*)
+ eapply vl_ll_pre_len_ll_eq. (*conclude from Hsrc_safe*)
* exact eqDec_obs.
* eapply Hsrc_safe.
eapply Hsem.
* rewrite Hbeq.
rewrite vl_cons_app.
unfold v2.
do 2 rewrite veclist_cons_nth.
setoid_rewrite apply_lf'_S.
setoid_rewrite app_length.
match goal with [|- ?x + ?y = ?w + ?z] => assert (x = w) as Q1;[|assert (y = z) as Q2] end.
3: lia.
++ clear - Hb0. (*new barrier states both produce 1 leakage*)
eapply vector_forall_nth with (i := Fin.F1) in Hb0 as Hb1.
eapply vector_forall_nth with (i := Fin.FS Fin.F1) in Hb0 as Hb2.
destruct (b0 [[Fin.F1]]), (b0 [[Fin.FS Fin.F1]]).
unfold compose.
destruct p, p0.
destruct (barrier_leak v h l), (barrier_leak v0 h0 l0); try easy.
rewrite H, H0. reflexivity.
++ setoid_rewrite veclist_app_nth.
setoid_rewrite apply_lf'_app.
setoid_rewrite app_length.
match goal with [|- ?x + ?y = ?w + ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: lia.
** (*intermediate states produce no leakage*)
specialize (vector_forall_nth _ _ _ Hbs) as Hnth.
assert (forall i: Fin.t 2, Forall (fun s : state => (is_B s = false)%type) (bs [[i]])) as Hnth'.
{ clear - Hnth.
intros.
eapply Forall_impl.
2: eapply Hnth.
intros.
cbn in H.
destruct (is_B a); congruence.
}
rewrite forall_not_isB_leak_nil. 2: auto.
rewrite forall_not_isB_leak_nil. 2: auto.
reflexivity.
** unfold ll_eq in Ha. (*states from previous step*)
unfold v2 in Ha.
rewrite Ha.
reflexivity.
+ intros Hsrc_ni. unfold v2. (*translate to target using sim_trace_same_leakage*)
unfold ll_eq.
unfold v2, ll_eq in Hsrc_ni.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
exact Hsrc_ni.
- eapply cf_sim_sync_correct.
- (* If one trace does not reach another barrier, the relations are also satisfied *)
intros a i Ha Hnoleak α Hα Hsim b Hsem β Hsem' Hsim'.
split1. (*show for source trace, then transfer to target*)
+ clear Hα Hsim Hsem' Hsim' α β.
unfold v2, ll_eq.
specialize (Hsrc_safe (veclist_app b a) Hsem).
do 3 dependent destruction a.
do 3 dependent destruction b.
unfold v2, ll_pre_sens in Hsrc_safe.
dependent destruction i. (*proof is the same no matter which trace is known to not produce more leakage, but we need to repeat it*)
* simpl in *. (*leakage of h1 must be None by Hnoleak*)
destruct Hsrc_safe as [_ [b1 [b2 Hsrc_safe] ] ].
destruct Hsrc_safe as [Hsrc_safe [Hb1 Hb2] ].
unfold ll_eq in Hsrc_safe.
rewrite app_assoc in Hsrc_safe, Hb1.
rewrite app_assoc in Hsrc_safe, Hb2.
specialize (Hnoleak (b1 ++ h1) Hb1).
apply forall_not_isB_leak_nil in Hnoleak.
unfold v2, ll_eq in Ha. simpl in Ha.
rewrite apply_lf'_app in Hsrc_safe.
rewrite Hnoleak in Hsrc_safe. simpl in Hsrc_safe.
rewrite! apply_lf'_app.
rewrite apply_lf'_app in Hsrc_safe.
rewrite Ha in *.
f_equal.
apply list_app_unchanged in Hsrc_safe. (*No matter how we extend h2, the leakage must be equal to some extension of h1, which must always be nil. Thus, h2 must be nil*)
rewrite apply_lf'_app in Hsrc_safe, Hnoleak.
symmetry in Hsrc_safe, Hnoleak. apply app_nil_eq in Hsrc_safe, Hnoleak.
destruct Hsrc_safe, Hnoleak. now rewrite H2, H0.
* dependent destruction i. 2: dependent destruction i. (*same as above.*)
simpl in *.
destruct Hsrc_safe as [_ [b1 [b2 Hsrc_safe] ] ].
destruct Hsrc_safe as [Hsrc_safe [Hb1 Hb2] ].
unfold ll_eq in Hsrc_safe.
rewrite app_assoc in Hsrc_safe, Hb1.
rewrite app_assoc in Hsrc_safe, Hb2.
specialize (Hnoleak (b2 ++ h2) Hb2).
apply forall_not_isB_leak_nil in Hnoleak.
unfold v2, ll_eq in Ha. simpl in Ha.
rewrite (apply_lf'_app h0 (b2 ++ h2)) in Hsrc_safe.
rewrite Hnoleak in Hsrc_safe. simpl in Hsrc_safe.
rewrite! apply_lf'_app.
rewrite apply_lf'_app in Hsrc_safe.
rewrite Ha in *.
f_equal.
symmetry in Hsrc_safe. apply list_app_unchanged in Hsrc_safe.
rewrite apply_lf'_app in Hsrc_safe, Hnoleak.
symmetry in Hsrc_safe, Hnoleak. apply app_nil_eq in Hsrc_safe, Hnoleak.
destruct Hsrc_safe, Hnoleak. now rewrite H2, H0.
+ intros Hsrc_ni. unfold v2. (*translate to target using sim_trace_same_leakage.*)
unfold ll_eq.
unfold v2, ll_eq in Hsrc_ni.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
erewrite sim_trace_same_leakage in Hsrc_ni.
2: eapply vec_forall2_nth; exact Hsem.
2: eapply vec_forall2_nth; exact Hsem'.
2: eapply vec_forall3_forall in Hsim'; exact Hsim'.
exact Hsrc_ni.
Qed.
Now we can conclude that the target traces satisfy termination-sensitive leakage equivalence using hyper_preserve_tgt_safe.
Theorem fence_preserve_mem
(iv: Vector.t heap 2)
(p_src: list stmt)
(Hsrc_safe: forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre_sens (rem_None ∘ leak_mem) nonspec_trace p_src iv) a)
: forall α, Vector.Forall2 (spec_am_trace (comp_fence p_src)) iv α -> v2 (ll_pre_sens (rem_None ∘ leak_mem') spec_am_trace (comp_fence p_src) iv) α.
Proof.
intros α Hα.
pose proof (mem_hypersim iv p_src Hsrc_safe) as Hs.
eapply hpbc_hpb5 in Hs.
2: repeat econstructor.
destructH.
eapply hyper_preserve_tgt_safe in Hs; eauto.
- eapply nonspec_trace_linear_semantics.
- eapply spec_am_trace_linear_semantics.
- eapply vl_ll_pre_sens_safety.
- eapply vl_ll_eq_ll_pre_sens.
- exact state_dec.
Qed.
(iv: Vector.t heap 2)
(p_src: list stmt)
(Hsrc_safe: forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre_sens (rem_None ∘ leak_mem) nonspec_trace p_src iv) a)
: forall α, Vector.Forall2 (spec_am_trace (comp_fence p_src)) iv α -> v2 (ll_pre_sens (rem_None ∘ leak_mem') spec_am_trace (comp_fence p_src) iv) α.
Proof.
intros α Hα.
pose proof (mem_hypersim iv p_src Hsrc_safe) as Hs.
eapply hpbc_hpb5 in Hs.
2: repeat econstructor.
destructH.
eapply hyper_preserve_tgt_safe in Hs; eauto.
- eapply nonspec_trace_linear_semantics.
- eapply spec_am_trace_linear_semantics.
- eapply vl_ll_pre_sens_safety.
- eapply vl_ll_eq_ll_pre_sens.
- exact state_dec.
Qed.
The proof requires the following assumptions:
Axioms:
RelationalChoice.relational_choice
: forall (A B : Type) (R : A -> B -> Prop),
(forall x : A, exists y : B, R x y) ->
exists R' : A -> B -> Prop,
Logic.subrelation R' R /\ (forall x : A, exists ! y : B, R' x y)
functional_extensionality_dep
: forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
(forall x : A, f x = g x) -> f = g
Eqdep.Eq_rect_eq.eq_rect_eq
: forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h
ClassicalUniqueChoice.dependent_unique_choice
: forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
(forall x : A, exists ! y : B x, R x y) ->
exists f : forall x : A, B x, forall x : A, R x (f x)
Classical_Prop.classic : forall P : Prop, P \/ ~ P