HypreSpectre.Preserve_lm
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
| (_, _, (While _ _ _) :: l) => 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).
Definition state_depth (s : state) := match s with (V, H, sl) => stmt_depth_list sl end.
| (_, _, nil) => true
| (_, _, (While _ _ _) :: l) => 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).
Definition state_depth (s : state) := match s with (V, H, sl) => stmt_depth_list sl end.
We define this function to compute how many steps are needed to reach a barrier. We then use it to prove we always reach another barrier.
Equations? steps_to_barrier (st : state) : nat by wf (state_depth st) :=
steps_to_barrier (V, H, nil) := 0;
steps_to_barrier (V, H, Read _ _ :: l) := 0;
steps_to_barrier (V, H, Write _ _ :: l) := 0;
steps_to_barrier (V, H, While _ _ _ :: l) := 0;
steps_to_barrier (V, H, s :: l) := S (steps_to_barrier (nonspec_step_fun (V, H, s :: l))).
Proof.
replace ((fix aux (sl : list stmt) : nat :=
match sl with
| nil => 0
| x :: xs => S (stmt_depth x + aux xs)
end)) with (stmt_depth_list). 2: reflexivity.
destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; rewrite stmt_depth_list_app; lia.
Qed.
Fixpoint n_sem_steps n st : list state := match n with
| 0 => st :: nil
| S n' => let l := n_sem_steps n' st in
(nonspec_step_fun (hd st l)) :: l
end.
Definition extend_trace p_src i a := match a with
| nil => (nil, i, p_src) :: nil
| s :: l => (nonspec_step_fun s) :: s :: l
end.
Fixpoint extend_trace_n n p_src i a := match n with
| 0 => a
| S n' => extend_trace p_src i (extend_trace_n n' p_src i a)
end.
Fixpoint extend_trace_n' n p_src i a := match n with
| 0 => a
| S n' => extend_trace_n' n' p_src i (extend_trace p_src i a)
end.
Lemma extend_trace_correct p_src i a :
sem_nonspec p_src i a -> sem_nonspec p_src i (extend_trace p_src i a).
Proof.
unfold sem_nonspec, nonspec_trace, multi_nonspec, multi_step'.
destruct a.
- reflexivity.
- unfold extend_trace. rewrite! length_cons.
intros Hsem.
rewrite <- Hsem.
rewrite multi_step_S2.
f_equal.
unfold multi_step_hd.
rewrite Hsem.
reflexivity.
Qed.
Lemma stb_step_decrease s s' n:
S n = steps_to_barrier s ->
s' = nonspec_step_fun s ->
n = steps_to_barrier s'.
Proof.
destruct s as [ [V H] s].
intros Hs Heq.
destruct s.
{ cbn in Hs. simp steps_to_barrier in Hs. congruence. }
destruct s; simp steps_to_barrier in *; try rewrite <- Heq in Hs; try now inversion Hs.
Qed.
Lemma extend_until_barrier' n:
forall p_src i s a l,
l = s::a ->
sem_nonspec p_src i (l) ->
n = steps_to_barrier (s) ->
sem_nonspec p_src i (extend_trace_n' n p_src i l) /\ is_B (hd (nil, i, p_src) (extend_trace_n' n p_src i l)) = true.
Proof.
destruct s as [ [V H] s].
revert V H s.
induction n.
- intros. unfold extend_trace_n'. split.
+ assumption.
+ unfold is_B, hd. rewrite H0.
destruct s. easy.
destruct s; simp steps_to_barrier in H2; try congruence.
- intros.
cbn.
destruct (nonspec_step_fun (V, H, s)) as [ [V' H'] s'] eqn: Hnsf.
eapply IHn with (a:=l).
+ rewrite H0. unfold extend_trace. f_equal. exact Hnsf.
+ now apply extend_trace_correct.
+ eapply stb_step_decrease. eassumption. now rewrite Hnsf.
Qed.
Lemma extend_trace_cons p_src i a:
exists s, extend_trace p_src i a = s :: a.
Proof.
unfold extend_trace.
destruct a.
+ eexists. reflexivity.
+ eexists. reflexivity.
Qed.
Lemma extend_trace_concat n p_src i a l:
l = extend_trace_n n p_src i a ->
exists b, l = b ++ a.
Proof.
revert l. induction n; intros l.
- cbn. now exists nil.
- cbn. specialize (IHn (extend_trace_n n p_src i a)). destruct IHn. reflexivity.
rewrite H.
intros ->.
destruct (extend_trace_cons p_src i (x++a)).
rewrite H0.
exists (x0 :: x).
apply app_comm_cons.
Qed.
Lemma extend_trace_shift n p_src i a:
extend_trace_n n p_src i (extend_trace p_src i a) = extend_trace p_src i (extend_trace_n n p_src i a).
Proof.
induction n.
- cbn. reflexivity.
- cbn. f_equal. exact IHn.
Qed.
Lemma extend_trace_n_agree n p_src i a:
extend_trace_n' n p_src i a = extend_trace_n n p_src i a.
Proof.
revert a.
induction n.
- reflexivity.
- cbn. intros a. rewrite IHn.
apply extend_trace_shift.
Qed.
Lemma extend_help n:
forall p_src i V H s a l,
l = (V, H, s)::a ->
sem_nonspec p_src i (l) ->
n = steps_to_barrier (V, H, s) ->
exists b bs, sem_nonspec p_src i ((b::bs)++a) /\ is_B b = true.
Proof.
intros.
assert (sem_nonspec p_src i (extend_trace_n' n p_src i l) /\ is_B (hd (nil, i, p_src) (extend_trace_n' n p_src i l)) = true) by (eapply extend_until_barrier'; eassumption).
rewrite (extend_trace_n_agree) in H3.
destruct (extend_trace_concat n p_src i l (extend_trace_n n p_src i l)). reflexivity.
rewrite H0 in H4.
rewrite app_cons_assoc in H4.
rewrite H0 in H3. rewrite H4 in H3.
destruct (x :r: (V, H, s)) eqn:HH.
- contradict HH. apply rcons_not_nil.
- exists s0, l0.
assert (x :r: (V, H, s) ++ a = (s0 :: l0) ++ a).
+ now rewrite HH.
+ Set Printing All.
fold state in *.
rewrite HH in H3.
Unset Printing All.
cbn in H3. exact H3.
Qed.
steps_to_barrier (V, H, nil) := 0;
steps_to_barrier (V, H, Read _ _ :: l) := 0;
steps_to_barrier (V, H, Write _ _ :: l) := 0;
steps_to_barrier (V, H, While _ _ _ :: l) := 0;
steps_to_barrier (V, H, s :: l) := S (steps_to_barrier (nonspec_step_fun (V, H, s :: l))).
Proof.
replace ((fix aux (sl : list stmt) : nat :=
match sl with
| nil => 0
| x :: xs => S (stmt_depth x + aux xs)
end)) with (stmt_depth_list). 2: reflexivity.
destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; rewrite stmt_depth_list_app; lia.
Qed.
Fixpoint n_sem_steps n st : list state := match n with
| 0 => st :: nil
| S n' => let l := n_sem_steps n' st in
(nonspec_step_fun (hd st l)) :: l
end.
Definition extend_trace p_src i a := match a with
| nil => (nil, i, p_src) :: nil
| s :: l => (nonspec_step_fun s) :: s :: l
end.
Fixpoint extend_trace_n n p_src i a := match n with
| 0 => a
| S n' => extend_trace p_src i (extend_trace_n n' p_src i a)
end.
Fixpoint extend_trace_n' n p_src i a := match n with
| 0 => a
| S n' => extend_trace_n' n' p_src i (extend_trace p_src i a)
end.
Lemma extend_trace_correct p_src i a :
sem_nonspec p_src i a -> sem_nonspec p_src i (extend_trace p_src i a).
Proof.
unfold sem_nonspec, nonspec_trace, multi_nonspec, multi_step'.
destruct a.
- reflexivity.
- unfold extend_trace. rewrite! length_cons.
intros Hsem.
rewrite <- Hsem.
rewrite multi_step_S2.
f_equal.
unfold multi_step_hd.
rewrite Hsem.
reflexivity.
Qed.
Lemma stb_step_decrease s s' n:
S n = steps_to_barrier s ->
s' = nonspec_step_fun s ->
n = steps_to_barrier s'.
Proof.
destruct s as [ [V H] s].
intros Hs Heq.
destruct s.
{ cbn in Hs. simp steps_to_barrier in Hs. congruence. }
destruct s; simp steps_to_barrier in *; try rewrite <- Heq in Hs; try now inversion Hs.
Qed.
Lemma extend_until_barrier' n:
forall p_src i s a l,
l = s::a ->
sem_nonspec p_src i (l) ->
n = steps_to_barrier (s) ->
sem_nonspec p_src i (extend_trace_n' n p_src i l) /\ is_B (hd (nil, i, p_src) (extend_trace_n' n p_src i l)) = true.
Proof.
destruct s as [ [V H] s].
revert V H s.
induction n.
- intros. unfold extend_trace_n'. split.
+ assumption.
+ unfold is_B, hd. rewrite H0.
destruct s. easy.
destruct s; simp steps_to_barrier in H2; try congruence.
- intros.
cbn.
destruct (nonspec_step_fun (V, H, s)) as [ [V' H'] s'] eqn: Hnsf.
eapply IHn with (a:=l).
+ rewrite H0. unfold extend_trace. f_equal. exact Hnsf.
+ now apply extend_trace_correct.
+ eapply stb_step_decrease. eassumption. now rewrite Hnsf.
Qed.
Lemma extend_trace_cons p_src i a:
exists s, extend_trace p_src i a = s :: a.
Proof.
unfold extend_trace.
destruct a.
+ eexists. reflexivity.
+ eexists. reflexivity.
Qed.
Lemma extend_trace_concat n p_src i a l:
l = extend_trace_n n p_src i a ->
exists b, l = b ++ a.
Proof.
revert l. induction n; intros l.
- cbn. now exists nil.
- cbn. specialize (IHn (extend_trace_n n p_src i a)). destruct IHn. reflexivity.
rewrite H.
intros ->.
destruct (extend_trace_cons p_src i (x++a)).
rewrite H0.
exists (x0 :: x).
apply app_comm_cons.
Qed.
Lemma extend_trace_shift n p_src i a:
extend_trace_n n p_src i (extend_trace p_src i a) = extend_trace p_src i (extend_trace_n n p_src i a).
Proof.
induction n.
- cbn. reflexivity.
- cbn. f_equal. exact IHn.
Qed.
Lemma extend_trace_n_agree n p_src i a:
extend_trace_n' n p_src i a = extend_trace_n n p_src i a.
Proof.
revert a.
induction n.
- reflexivity.
- cbn. intros a. rewrite IHn.
apply extend_trace_shift.
Qed.
Lemma extend_help n:
forall p_src i V H s a l,
l = (V, H, s)::a ->
sem_nonspec p_src i (l) ->
n = steps_to_barrier (V, H, s) ->
exists b bs, sem_nonspec p_src i ((b::bs)++a) /\ is_B b = true.
Proof.
intros.
assert (sem_nonspec p_src i (extend_trace_n' n p_src i l) /\ is_B (hd (nil, i, p_src) (extend_trace_n' n p_src i l)) = true) by (eapply extend_until_barrier'; eassumption).
rewrite (extend_trace_n_agree) in H3.
destruct (extend_trace_concat n p_src i l (extend_trace_n n p_src i l)). reflexivity.
rewrite H0 in H4.
rewrite app_cons_assoc in H4.
rewrite H0 in H3. rewrite H4 in H3.
destruct (x :r: (V, H, s)) eqn:HH.
- contradict HH. apply rcons_not_nil.
- exists s0, l0.
assert (x :r: (V, H, s) ++ a = (s0 :: l0) ++ a).
+ now rewrite HH.
+ Set Printing All.
fold state in *.
rewrite HH in H3.
Unset Printing All.
cbn in H3. exact H3.
Qed.
Every trace prefix can be extended to reach another barrier.
Lemma src_term p_src :
forall i a, sem_nonspec p_src i a -> exists b0 bs, sem_nonspec p_src i ((b0 :: bs) ++ a) /\ is_B b0 = true.
Proof.
intros.
destruct (extend_trace_cons p_src i a). destruct x as [ [V H'] s].
eapply extend_help with (l := extend_trace p_src i a).
- eassumption.
- now eapply extend_trace_correct.
- reflexivity.
Qed.
forall i a, sem_nonspec p_src i a -> exists b0 bs, sem_nonspec p_src i ((b0 :: bs) ++ a) /\ is_B b0 = true.
Proof.
intros.
destruct (extend_trace_cons p_src i a). destruct x as [ [V H'] s].
eapply extend_help with (l := extend_trace p_src i a).
- eassumption.
- now eapply extend_trace_correct.
- reflexivity.
Qed.
Barrier states produce leakage, other states do not.
Lemma barrier_leak V H s:
is_B (V, H, s) = true -> exists x, leak_lm (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)...
+ now eexists.
Qed.
Lemma no_barrier_no_leak V H s:
is_B (V, H, s) = false -> leak_lm (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_lm) 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_lm) 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.
is_B (V, H, s) = true -> exists x, leak_lm (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)...
+ now eexists.
Qed.
Lemma no_barrier_no_leak V H s:
is_B (V, H, s) = false -> leak_lm (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_lm) 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_lm) 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 sim_same_leakage:
forall x y, cf_sim' x y -> leak_lm x = leak_lm' 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_lm x = leak_lm' 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 traces 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_lm) (a) = apply_lf' (rem_None ∘ leak_lm') (α).
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_lm) (a) = apply_lf' (rem_None ∘ leak_lm') (α).
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.
comp_fence Preserves Leakage Equivalence for Loops+Memory
Theorem fence_preserve_lm
(iv: Vector.t heap 2)
(p_src: list stmt)
(Hsrc_safe: forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre (rem_None ∘ leak_lm)) a) (*assume (termination-insensitive) leakage equivalence on source*)
: forall α, Vector.Forall2 (spec_am_trace (comp_fence p_src)) iv α -> v2 (ll_pre_sens (rem_None ∘ leak_lm') spec_am_trace (comp_fence p_src) iv) α. (*prove (termination-sensitive) leakage equivalence on target*)
Proof.
intros α Hα.
assert (forall i a, sem_nonspec p_src i a -> exists b0 bs, sem_nonspec p_src i ((b0 :: bs) ++ a) /\ is_B b0 = true) as Hterm by apply src_term. (*can always reach barrier*)
eapply hpbc_hpb2 with (tgt_sem := sem_spec_am (comp_fence p_src)) in Hterm.
- destructH.
eapply hyper_preserve_tgt_safe with (α:=α). (*conclude a safety hyperproperty holds on target from a hyper-simulation*)
+ eapply hyper_preserve_barrier_hp. exact Hterm.
+ apply nonspec_trace_linear_semantics.
+ apply spec_am_trace_linear_semantics.
+ eapply vl_ll_pre_sens_safety. (*is a hypersafety*)
+ eapply vl_ll_eq_ll_pre_sens. (*is implied by target relation*)
+ eapply Hα.
- exact (nil, nil, nil). (*type is inhabited*)
- exact state_dec.
- econstructor. (*hyper-simulation*)
+ eapply vl_ll_eq_zero. (*empty trace prefixes satisfy relations*)
+ eapply vl_ll_eq_zero.
+ eapply (cf_sim_nil).
+ clear α Hα. (*hyper-step*)
intros a Ha α Hα Hsim b Hsem β Hsem' Hsim' b0 bs Hbeq Hb0 Hbs.
split1. (*show for source first*)
* eapply vl_ll_pre_len_ll_eq. (*conclude from Hsrc_safe because same length*) 1: 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.
** (*The 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. (*known because this is the 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.
Unshelve.
1: apply nonspec_trace_linear_semantics.
1: apply spec_am_trace_linear_semantics.
2: apply (tsync_cf p_src).
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 (rem_None ∘ leak_lm)) a) (*assume (termination-insensitive) leakage equivalence on source*)
: forall α, Vector.Forall2 (spec_am_trace (comp_fence p_src)) iv α -> v2 (ll_pre_sens (rem_None ∘ leak_lm') spec_am_trace (comp_fence p_src) iv) α. (*prove (termination-sensitive) leakage equivalence on target*)
Proof.
intros α Hα.
assert (forall i a, sem_nonspec p_src i a -> exists b0 bs, sem_nonspec p_src i ((b0 :: bs) ++ a) /\ is_B b0 = true) as Hterm by apply src_term. (*can always reach barrier*)
eapply hpbc_hpb2 with (tgt_sem := sem_spec_am (comp_fence p_src)) in Hterm.
- destructH.
eapply hyper_preserve_tgt_safe with (α:=α). (*conclude a safety hyperproperty holds on target from a hyper-simulation*)
+ eapply hyper_preserve_barrier_hp. exact Hterm.
+ apply nonspec_trace_linear_semantics.
+ apply spec_am_trace_linear_semantics.
+ eapply vl_ll_pre_sens_safety. (*is a hypersafety*)
+ eapply vl_ll_eq_ll_pre_sens. (*is implied by target relation*)
+ eapply Hα.
- exact (nil, nil, nil). (*type is inhabited*)
- exact state_dec.
- econstructor. (*hyper-simulation*)
+ eapply vl_ll_eq_zero. (*empty trace prefixes satisfy relations*)
+ eapply vl_ll_eq_zero.
+ eapply (cf_sim_nil).
+ clear α Hα. (*hyper-step*)
intros a Ha α Hα Hsim b Hsem β Hsem' Hsim' b0 bs Hbeq Hb0 Hbs.
split1. (*show for source first*)
* eapply vl_ll_pre_len_ll_eq. (*conclude from Hsrc_safe because same length*) 1: 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.
** (*The 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. (*known because this is the 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.
Unshelve.
1: apply nonspec_trace_linear_semantics.
1: apply spec_am_trace_linear_semantics.
2: apply (tsync_cf p_src).
Qed.
This proof relies on 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)