HypreSpectre.Preserve_ct_relaxed
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) := true.
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 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).
Since every state is a barrier, one will always be reached in just one step.
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 a.
- exists (nil, i, p_src), nil.
split.
+ unfold sem_nonspec, nonspec_trace. reflexivity.
+ reflexivity.
- exists (nonspec_step_fun s), nil.
split. 2: reflexivity.
unfold sem_nonspec, nonspec_trace in H |-*.
rewrite <- app_comm_cons, length_cons.
unfold multi_nonspec, multi_step' in H |-*.
rewrite app_nil_l.
rewrite length_cons in *.
rewrite multi_step_S2.
unfold multi_step_hd.
rewrite H.
cbn. 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 a.
- exists (nil, i, p_src), nil.
split.
+ unfold sem_nonspec, nonspec_trace. reflexivity.
+ reflexivity.
- exists (nonspec_step_fun s), nil.
split. 2: reflexivity.
unfold sem_nonspec, nonspec_trace in H |-*.
rewrite <- app_comm_cons, length_cons.
unfold multi_nonspec, multi_step' in H |-*.
rewrite app_nil_l.
rewrite length_cons in *.
rewrite multi_step_S2.
unfold multi_step_hd.
rewrite H.
cbn. reflexivity.
Qed.
There are no non-barrier states.
Lemma forall_not_isB_is_nil:
forall bs, Forall (fun s => is_B s = false) bs -> bs = nil.
Proof.
intros bs Hbs.
rewrite Forall_forall in Hbs.
destruct bs.
- reflexivity.
- specialize (Hbs s).
cbn in Hbs.
specialize (Hbs (or_introl (eq_refl))).
replace (is_B s) with (true) in Hbs.
+ congruence.
+ reflexivity.
Qed.
Lemma cr_sim_eq p i a α0 α1:
sem_spec_am (comp_relaxed' p) i α0 ->
sem_spec_am (comp_relaxed' p) i α1 ->
cr_sim p i a α0 ->
cr_sim p i a α1 ->
α0 = α1.
Proof.
intros Hsem1 Hsem2 H H0.
induction H in α1, H0, Hsem1, Hsem2 |-*.
- inversion H0. reflexivity.
- inversion H0.
+ reflexivity.
+ inversion H8.
rewrite <- H10, app_nil_r in H7. subst. congruence.
- inversion H0.
+ rewrite <- H7 in H4. inversion H4. subst. congruence.
+ subst. fold (cr_sim p i) in *.
apply multi_step_split in Hsem1, Hsem2. do 2 destructH.
specialize (IHlift_state_rel _ Hsem4 Hsem3 H12). subst. f_equal.
inversion H7; subst.
rewrite <- H9 in H2. rewrite H2 in Hsem2. rewrite Hsem2 in Hsem0. easy.
Qed.
Lemma cr_sim_cons p i a al α:
cr_sim p i (a :: al) α ->
exists α0 αs, α = α0 :: αs /\ cr_sim' a α0.
Proof.
inversion 1.
- eexists. eexists.
split.
+ reflexivity.
+ exact H3.
- eexists. eexists.
split.
2: exact H5.
exact H3.
Qed.
forall bs, Forall (fun s => is_B s = false) bs -> bs = nil.
Proof.
intros bs Hbs.
rewrite Forall_forall in Hbs.
destruct bs.
- reflexivity.
- specialize (Hbs s).
cbn in Hbs.
specialize (Hbs (or_introl (eq_refl))).
replace (is_B s) with (true) in Hbs.
+ congruence.
+ reflexivity.
Qed.
Lemma cr_sim_eq p i a α0 α1:
sem_spec_am (comp_relaxed' p) i α0 ->
sem_spec_am (comp_relaxed' p) i α1 ->
cr_sim p i a α0 ->
cr_sim p i a α1 ->
α0 = α1.
Proof.
intros Hsem1 Hsem2 H H0.
induction H in α1, H0, Hsem1, Hsem2 |-*.
- inversion H0. reflexivity.
- inversion H0.
+ reflexivity.
+ inversion H8.
rewrite <- H10, app_nil_r in H7. subst. congruence.
- inversion H0.
+ rewrite <- H7 in H4. inversion H4. subst. congruence.
+ subst. fold (cr_sim p i) in *.
apply multi_step_split in Hsem1, Hsem2. do 2 destructH.
specialize (IHlift_state_rel _ Hsem4 Hsem3 H12). subst. f_equal.
inversion H7; subst.
rewrite <- H9 in H2. rewrite H2 in Hsem2. rewrite Hsem2 in Hsem0. easy.
Qed.
Lemma cr_sim_cons p i a al α:
cr_sim p i (a :: al) α ->
exists α0 αs, α = α0 :: αs /\ cr_sim' a α0.
Proof.
inversion 1.
- eexists. eexists.
split.
+ reflexivity.
+ exact H3.
- eexists. eexists.
split.
2: exact H5.
exact H3.
Qed.
Lemma sim_same_leakage:
forall x y, cr_sim' x y -> leak_ct x = leak_ct' 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.
- unfold comp_relaxed'. simp comp_relaxed.
cbv zeta. destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: reflexivity.
destruct (leak_lookahead sixteen s1); reflexivity.
- unfold comp_relaxed'. simp comp_relaxed.
cbv zeta. destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: reflexivity.
destruct (leak_lookahead sixteen s1); reflexivity.
Qed.
Lemma cons_inv_l {T} (a b : T) l1 l2:
a :: l1 = b :: l2 -> a = b.
Proof.
now inversion 1.
Qed.
forall x y, cr_sim' x y -> leak_ct x = leak_ct' 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.
- unfold comp_relaxed'. simp comp_relaxed.
cbv zeta. destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: reflexivity.
destruct (leak_lookahead sixteen s1); reflexivity.
- unfold comp_relaxed'. simp comp_relaxed.
cbv zeta. destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: reflexivity.
destruct (leak_lookahead sixteen s1); reflexivity.
Qed.
Lemma cons_inv_l {T} (a b : T) l1 l2:
a :: l1 = b :: l2 -> a = b.
Proof.
now inversion 1.
Qed.
The same statement/program produces the same amount of leakage independent of the environment.
Lemma same_stmt_same_leak_amt V V' H H' s:
|rem_None (leak_ct (V, H, s))| = |rem_None (leak_ct (V', H', s))|.
Proof.
destruct s. reflexivity.
destruct s; try reflexivity.
- simpl. destruct (Z_lt_dec (eval_expr_fun a V) 0), (Z_lt_dec (eval_expr_fun a V') 0).
+ reflexivity.
+ destruct (alist_find _ x V'); reflexivity.
+ destruct (alist_find _ x V); reflexivity.
+ destruct (alist_find _ x V), (alist_find _ x V'); reflexivity.
- simpl. destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0); reflexivity.
Qed.
|rem_None (leak_ct (V, H, s))| = |rem_None (leak_ct (V', H', s))|.
Proof.
destruct s. reflexivity.
destruct s; try reflexivity.
- simpl. destruct (Z_lt_dec (eval_expr_fun a V) 0), (Z_lt_dec (eval_expr_fun a V') 0).
+ reflexivity.
+ destruct (alist_find _ x V'); reflexivity.
+ destruct (alist_find _ x V); reflexivity.
+ destruct (alist_find _ x V), (alist_find _ x V'); reflexivity.
- simpl. destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0); reflexivity.
Qed.
If leak_lookahead does not find any leakages, there are none.
Lemma leak_lookahead_nil a V H s1 s' st:
leak_lookahead a s1 = Some nil ->
apply_lf' (rem_None ∘ leak_ct')
(multi_step spec_step_fun
((Some (a), V, H,
comp_relaxed sixteen (s1 ++ s')) :: st) a)
= nil.
Proof.
induction a in s1 |- *.
- simpl. reflexivity.
- intros.
simpl in H0.
destruct s1. congruence.
destruct s; try congruence.
+ destruct (leak_lookahead a s1); congruence.
+ destruct (leak_lookahead a s1); congruence.
+ rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
simpl. simp comp_relaxed.
rewrite Nat.sub_0_r.
rewrite IHa. 2: exact H0.
reflexivity.
Qed.
Lemma leak_lookahead_inv a b s s1' s2' l:
leak_lookahead (S a) (s :: s1') = leak_lookahead (S b) (s :: s2') ->
leak_lookahead (S a) (s :: s1') = Some l ->
leak_lookahead a s1' = leak_lookahead b s2'.
Proof.
intros. simpl in H, H0.
destruct s; try congruence.
all: destruct (leak_lookahead a s1'), (leak_lookahead b s2'); try congruence.
Qed.
leak_lookahead a s1 = Some nil ->
apply_lf' (rem_None ∘ leak_ct')
(multi_step spec_step_fun
((Some (a), V, H,
comp_relaxed sixteen (s1 ++ s')) :: st) a)
= nil.
Proof.
induction a in s1 |- *.
- simpl. reflexivity.
- intros.
simpl in H0.
destruct s1. congruence.
destruct s; try congruence.
+ destruct (leak_lookahead a s1); congruence.
+ destruct (leak_lookahead a s1); congruence.
+ rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
simpl. simp comp_relaxed.
rewrite Nat.sub_0_r.
rewrite IHa. 2: exact H0.
reflexivity.
Qed.
Lemma leak_lookahead_inv a b s s1' s2' l:
leak_lookahead (S a) (s :: s1') = leak_lookahead (S b) (s :: s2') ->
leak_lookahead (S a) (s :: s1') = Some l ->
leak_lookahead a s1' = leak_lookahead b s2'.
Proof.
intros. simpl in H, H0.
destruct s; try congruence.
all: destruct (leak_lookahead a s1'), (leak_lookahead b s2'); try congruence.
Qed.
If no fences were inserted, then the speculative execution will produce the same observations as nonspeculative execution along the proper path.
This allows us to prove the speculative traces will have the same leakages, as we know leakages are equal in the source traces
Lemma leak_lookahead_same_leakage' a b V H s1 s2 s' st l:
leak_lookahead a s1 = leak_lookahead (S b) s2 ->
leak_lookahead a s1 = Some l ->
apply_lf' (rem_None ∘ leak_ct')
(multi_step spec_step_fun
(((Some a, V, H, comp_relaxed sixteen (s1 ++ s')) :: st))
a) =
apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun
((V, H, s2 ++ s'))
b).
Proof.
revert b.
induction a in s1, s2, l, V, H |-*.
- intros. simpl.
unfold compose. cbn.
cbn in H0.
destruct s2. congruence.
destruct s; try congruence.
destruct (leak_lookahead b s2); try congruence.
destruct (leak_lookahead b s2); try congruence.
induction b in s2, H0 |-*.
+ simpl. reflexivity.
+ simpl in H0.
destruct s2. congruence.
destruct s; try congruence.
destruct (leak_lookahead b s2); congruence.
destruct (leak_lookahead b s2); congruence.
rewrite multi_step_S, apply_lf'_app.
simpl.
rewrite app_comm_cons, <- IHb. reflexivity.
exact H0.
- induction b in s2 |- *.
+ intros.
remember H0; clear Heqe.
rewrite H1 in H0.
simpl in H0.
destruct s2. congruence.
destruct s; try congruence.
* inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons.
rewrite multi_step_S, apply_lf'_app.
simpl.
simp comp_relaxed.
cbn. rewrite Nat.sub_0_r.
destruct (alist_find decZ (eval_expr_fun a0 V) H).
rewrite leak_lookahead_nil. reflexivity. assumption.
rewrite leak_lookahead_nil. reflexivity. assumption.
-- destruct (leak_lookahead a s1); congruence.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
change (apply_lf' (rem_None ∘ leak_ct') (((Some (S a), V, H, comp_relaxed sixteen (Skip :: s1 ++ s')) :: st) :: nil)) with (@nil observation).
rewrite app_nil_r.
simpl. simp comp_relaxed.
specialize (IHa V H s1 (Read x a0 :: s2) _ _ e H1).
rewrite Nat.sub_0_r.
rewrite IHa. reflexivity.
* inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1); congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons.
rewrite multi_step_S, apply_lf'_app.
simpl. simp comp_relaxed.
cbn. rewrite Nat.sub_0_r.
destruct (alist_find _ x V).
rewrite leak_lookahead_nil. reflexivity. assumption.
rewrite leak_lookahead_nil. reflexivity. assumption.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
change (apply_lf' (rem_None ∘ leak_ct')(((Some (S a), V, H, comp_relaxed sixteen (Skip :: s1 ++ s')) :: st) :: nil)) with (@nil observation).
rewrite app_nil_r.
simpl. simp comp_relaxed.
specialize (IHa V H s1 (Write x a0 :: s2) _ _ e H1).
rewrite Nat.sub_0_r.
rewrite IHa. reflexivity.
* rewrite leak_lookahead_nil. reflexivity. rewrite H1. rewrite H0. reflexivity.
+ intros.
remember H0; clear Heqe.
rewrite H1 in H0.
simpl in H0.
destruct s2. congruence.
destruct s; try congruence.
* destruct (leak_lookahead (S b) s2) eqn: Hla; simpl in Hla; rewrite Hla in H0. 2: congruence.
inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons, ! multi_step_S, ! apply_lf'_app. rewrite app_inv_tail_iff.
simpl. simp comp_relaxed.
destruct (alist_find decZ (eval_expr_fun a0 V) H).
rewrite Nat.sub_0_r.
eapply IHa.
2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (ReadExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
rewrite Nat.sub_0_r.
eapply IHa. 2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (ReadExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
-- destruct (leak_lookahead a s1); congruence.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
unfold spec_step_fun. fold spec_step_fun. simp comp_relaxed. unfold decr.
rewrite app_nil_r.
assert (S a - 1 = a) as -> by lia.
eapply IHa.
2: exact H1.
rewrite <- e. reflexivity.
* destruct (leak_lookahead (S b) s2) eqn: Hla; simpl in Hla; rewrite Hla in H0. 2: congruence.
inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1); congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons, ! multi_step_S, ! apply_lf'_app. rewrite app_inv_tail_iff.
simpl. simp comp_relaxed.
destruct (alist_find _ x V).
rewrite Nat.sub_0_r.
eapply IHa. 2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (WriteExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
rewrite Nat.sub_0_r.
eapply IHa. 2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (WriteExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
unfold spec_step_fun. fold spec_step_fun. simp comp_relaxed. unfold decr.
rewrite app_nil_r.
assert (S a - 1 = a) as -> by (simpl; apply Nat.sub_0_r).
eapply IHa.
2: exact H1.
rewrite <- e. reflexivity.
* rewrite <- app_comm_cons. symmetry. rewrite multi_step_S, apply_lf'_app.
rewrite app_nil_r. symmetry.
unfold nonspec_step_fun. fold nonspec_step_fun.
eapply IHb.
rewrite e. reflexivity. assumption.
Qed.
leak_lookahead a s1 = leak_lookahead (S b) s2 ->
leak_lookahead a s1 = Some l ->
apply_lf' (rem_None ∘ leak_ct')
(multi_step spec_step_fun
(((Some a, V, H, comp_relaxed sixteen (s1 ++ s')) :: st))
a) =
apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun
((V, H, s2 ++ s'))
b).
Proof.
revert b.
induction a in s1, s2, l, V, H |-*.
- intros. simpl.
unfold compose. cbn.
cbn in H0.
destruct s2. congruence.
destruct s; try congruence.
destruct (leak_lookahead b s2); try congruence.
destruct (leak_lookahead b s2); try congruence.
induction b in s2, H0 |-*.
+ simpl. reflexivity.
+ simpl in H0.
destruct s2. congruence.
destruct s; try congruence.
destruct (leak_lookahead b s2); congruence.
destruct (leak_lookahead b s2); congruence.
rewrite multi_step_S, apply_lf'_app.
simpl.
rewrite app_comm_cons, <- IHb. reflexivity.
exact H0.
- induction b in s2 |- *.
+ intros.
remember H0; clear Heqe.
rewrite H1 in H0.
simpl in H0.
destruct s2. congruence.
destruct s; try congruence.
* inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons.
rewrite multi_step_S, apply_lf'_app.
simpl.
simp comp_relaxed.
cbn. rewrite Nat.sub_0_r.
destruct (alist_find decZ (eval_expr_fun a0 V) H).
rewrite leak_lookahead_nil. reflexivity. assumption.
rewrite leak_lookahead_nil. reflexivity. assumption.
-- destruct (leak_lookahead a s1); congruence.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
change (apply_lf' (rem_None ∘ leak_ct') (((Some (S a), V, H, comp_relaxed sixteen (Skip :: s1 ++ s')) :: st) :: nil)) with (@nil observation).
rewrite app_nil_r.
simpl. simp comp_relaxed.
specialize (IHa V H s1 (Read x a0 :: s2) _ _ e H1).
rewrite Nat.sub_0_r.
rewrite IHa. reflexivity.
* inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1); congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons.
rewrite multi_step_S, apply_lf'_app.
simpl. simp comp_relaxed.
cbn. rewrite Nat.sub_0_r.
destruct (alist_find _ x V).
rewrite leak_lookahead_nil. reflexivity. assumption.
rewrite leak_lookahead_nil. reflexivity. assumption.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
change (apply_lf' (rem_None ∘ leak_ct')(((Some (S a), V, H, comp_relaxed sixteen (Skip :: s1 ++ s')) :: st) :: nil)) with (@nil observation).
rewrite app_nil_r.
simpl. simp comp_relaxed.
specialize (IHa V H s1 (Write x a0 :: s2) _ _ e H1).
rewrite Nat.sub_0_r.
rewrite IHa. reflexivity.
* rewrite leak_lookahead_nil. reflexivity. rewrite H1. rewrite H0. reflexivity.
+ intros.
remember H0; clear Heqe.
rewrite H1 in H0.
simpl in H0.
destruct s2. congruence.
destruct s; try congruence.
* destruct (leak_lookahead (S b) s2) eqn: Hla; simpl in Hla; rewrite Hla in H0. 2: congruence.
inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons, ! multi_step_S, ! apply_lf'_app. rewrite app_inv_tail_iff.
simpl. simp comp_relaxed.
destruct (alist_find decZ (eval_expr_fun a0 V) H).
rewrite Nat.sub_0_r.
eapply IHa.
2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (ReadExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
rewrite Nat.sub_0_r.
eapply IHa. 2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (ReadExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
-- destruct (leak_lookahead a s1); congruence.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
unfold spec_step_fun. fold spec_step_fun. simp comp_relaxed. unfold decr.
rewrite app_nil_r.
assert (S a - 1 = a) as -> by lia.
eapply IHa.
2: exact H1.
rewrite <- e. reflexivity.
* destruct (leak_lookahead (S b) s2) eqn: Hla; simpl in Hla; rewrite Hla in H0. 2: congruence.
inversion H0; subst; clear H0.
simpl in H1.
destruct s1. congruence.
destruct s; try congruence.
-- destruct (leak_lookahead a s1); congruence.
-- destruct (leak_lookahead a s1) eqn: He. 2: congruence.
inversion H1; subst.
rewrite <-! app_comm_cons, ! multi_step_S, ! apply_lf'_app. rewrite app_inv_tail_iff.
simpl. simp comp_relaxed.
destruct (alist_find _ x V).
rewrite Nat.sub_0_r.
eapply IHa. 2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (WriteExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
rewrite Nat.sub_0_r.
eapply IHa. 2: exact He.
apply (leak_lookahead_inv _ _ _ _ _ (WriteExp a0 x :: l0) e).
simpl. rewrite He. reflexivity.
-- rewrite <- app_comm_cons, multi_step_S, apply_lf'_app.
unfold spec_step_fun. fold spec_step_fun. simp comp_relaxed. unfold decr.
rewrite app_nil_r.
assert (S a - 1 = a) as -> by (simpl; apply Nat.sub_0_r).
eapply IHa.
2: exact H1.
rewrite <- e. reflexivity.
* rewrite <- app_comm_cons. symmetry. rewrite multi_step_S, apply_lf'_app.
rewrite app_nil_r. symmetry.
unfold nonspec_step_fun. fold nonspec_step_fun.
eapply IHb.
rewrite e. reflexivity. assumption.
Qed.
Special case for 16 steps of execution
Lemma leak_lookahead_same_leakage V H c s1 s2 s' l:
leak_lookahead sixteen s1 = leak_lookahead sixteen s2 ->
leak_lookahead sixteen s1 = Some l ->
apply_lf' (rem_None ∘ leak_ct')
(multi_step spec_step_fun
(spec_step_fun ((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
sixteen) =
apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun
(nonspec_step_fun (V, H, If c s1 s2 :: s'))
fifteen).
Proof.
intros.
simp comp_relaxed. cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: congruence.
rewrite H1.
unfold spec_step_fun, nonspec_step_fun. fold spec_step_fun. fold nonspec_step_fun.
destruct (Z.eq_dec (eval_expr_fun c V) 0).
- rewrite <-! comp_relaxed_app.
assert (wndw None = Some sixteen) as -> by reflexivity.
pose proof (leak_lookahead_same_leakage' sixteen fifteen V H s1 s2 s' ((decr None, V, H, comp_relaxed sixteen (s2 ++ s')) :: nil) l H0 H1).
exact H2.
- rewrite <-! comp_relaxed_app.
assert (wndw None = Some sixteen) as -> by reflexivity.
pose proof (leak_lookahead_same_leakage' sixteen fifteen V H s2 s1 s' ((decr None, V, H, comp_relaxed sixteen (s1 ++ s')) :: nil) l).
apply H2; eauto. now rewrite <- H0.
Qed.
leak_lookahead sixteen s1 = leak_lookahead sixteen s2 ->
leak_lookahead sixteen s1 = Some l ->
apply_lf' (rem_None ∘ leak_ct')
(multi_step spec_step_fun
(spec_step_fun ((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
sixteen) =
apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun
(nonspec_step_fun (V, H, If c s1 s2 :: s'))
fifteen).
Proof.
intros.
simp comp_relaxed. cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: congruence.
rewrite H1.
unfold spec_step_fun, nonspec_step_fun. fold spec_step_fun. fold nonspec_step_fun.
destruct (Z.eq_dec (eval_expr_fun c V) 0).
- rewrite <-! comp_relaxed_app.
assert (wndw None = Some sixteen) as -> by reflexivity.
pose proof (leak_lookahead_same_leakage' sixteen fifteen V H s1 s2 s' ((decr None, V, H, comp_relaxed sixteen (s2 ++ s')) :: nil) l H0 H1).
exact H2.
- rewrite <-! comp_relaxed_app.
assert (wndw None = Some sixteen) as -> by reflexivity.
pose proof (leak_lookahead_same_leakage' sixteen fifteen V H s2 s1 s' ((decr None, V, H, comp_relaxed sixteen (s1 ++ s')) :: nil) l).
apply H2; eauto. now rewrite <- H0.
Qed.
If we extend two source traces by one step each, the new trace prefixes will still produce the same leakage
Lemma src_leak_step V V' H H' s s' al al0 (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_ct)) a):
(nonspec_trace p_src (iv [[Fin.F1]]) ((V, H, s :: s') :: al)) ->
(nonspec_trace p_src (iv [[Fin.FS Fin.F1]]) ((V', H', s :: s') :: al0)) ->
apply_lf' (rem_None ∘ leak_ct) ((V, H, s :: s') :: al) =
apply_lf' (rem_None ∘ leak_ct) ((V', H', s :: s') :: al0) ->
apply_lf' (rem_None ∘ leak_ct) (nonspec_step_fun (V, H, s :: s') :: (V, H, s :: s') :: al) =
apply_lf' (rem_None ∘ leak_ct) (nonspec_step_fun (V', H', s :: s') ::(V', H', s :: s') :: al0).
Proof.
intros.
specialize (Hsrc_safe (Vector.cons (list state)
(nonspec_step_fun (V, H, s :: s') :: (V, H, s :: s') :: al) 1
(Vector.cons (list state)
(nonspec_step_fun (V', H', s :: s') :: (V', H', s :: s') :: al0) 0
(Vector.nil (list state))))).
eapply vl_ll_pre_len_ll_eq in Hsrc_safe.
- unfold v2 in Hsrc_safe. exact Hsrc_safe.
- exact eqDec_obs.
- rewrite Vec_Forall2_forall2.
intros i. dependent destruction i. 2: dependent destruction i. 3: dependent destruction i.
+ simpl. unfold nonspec_trace, multi_nonspec, multi_step'.
rewrite length_cons.
unfold nonspec_trace, multi_nonspec, multi_step' in H0.
rewrite length_cons in H0. rewrite <- H0.
rewrite multi_step_len. rewrite multi_step_S2.
unfold multi_step_hd.
rewrite H0. simpl. reflexivity.
+ simpl. unfold nonspec_trace, multi_nonspec, multi_step'.
rewrite length_cons.
unfold nonspec_trace, multi_nonspec, multi_step' in H1.
rewrite length_cons in H1. rewrite <- H1.
rewrite multi_step_len. rewrite multi_step_S2.
unfold multi_step_hd.
rewrite H1. simpl. reflexivity.
- unfold v2. simpl.
rewrite apply_lf'_S. rewrite H2.
rewrite app_length. symmetry. rewrite apply_lf'_S. rewrite app_length.
rewrite Nat.add_cancel_r.
destruct s; try eapply same_stmt_same_leak_amt.
+ destruct (alist_find decZ (eval_expr_fun a V')), (alist_find decZ (eval_expr_fun a V)); eapply same_stmt_same_leak_amt.
+ destruct (alist_find _ x V'), (alist_find _ x V); eapply same_stmt_same_leak_amt.
+ rewrite! apply_lf'_S in H2. unfold compose in H2. simpl in H2.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0).
* eapply same_stmt_same_leak_amt.
* simpl in H2. inversion H2.
* simpl in H2. inversion H2.
* eapply same_stmt_same_leak_amt.
Qed.
Lemma nonspec_trace_step {p i V H s s'}:
nonspec_trace p i ((V, H, s) :: s') ->
nonspec_trace p i (nonspec_step_fun (V, H, s) :: (V, H, s) :: s').
Proof.
unfold nonspec_trace, multi_nonspec, multi_step'.
rewrite! length_cons.
intros.
rewrite multi_step_S2.
unfold multi_step_hd. rewrite H0. reflexivity.
Qed.
Lemma src_leak_steps n V V' H H' s al al0 (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_ct)) a):
(nonspec_trace p_src (iv [[Fin.F1]]) ((V, H, s) :: al)) ->
(nonspec_trace p_src (iv [[Fin.FS Fin.F1]]) ((V', H', s) :: al0)) ->
apply_lf' (rem_None ∘ leak_ct) ((V, H, s) :: al) =
apply_lf' (rem_None ∘ leak_ct) ((V', H', s) :: al0) ->
| apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun (nonspec_step_fun (V, H, s))
n ++ (V, H, s) :: al) | =
| apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun
(nonspec_step_fun (V', H', s)) n ++
(V', H', s) :: al0) |.
Proof.
intros.
induction n in V, V', H, H', s, al, al0, H0, H1, H2 |-*.
- simpl.
destruct s as [| s s'].
+ rewrite apply_lf'_S. symmetry. rewrite apply_lf'_S. rewrite H2, ! app_length.
reflexivity.
+ fold (nonspec_step_fun (V, H, s :: s')). fold (nonspec_step_fun (V', H', s :: s')).
erewrite src_leak_step. reflexivity. all: eassumption.
- rewrite! multi_step_S.
rewrite <-! app_assoc.
rewrite <-! cons_app.
unfold nonspec_step_fun at 3.
unfold nonspec_step_fun at 3.
unfold nonspec_step_fun at 6.
unfold nonspec_step_fun at 5.
destruct s as [| s s']. 2: destruct s.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* rewrite (apply_lf'_S). symmetry. rewrite (apply_lf'_S). rewrite H2. reflexivity.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
+ pose proof (nonspec_trace_step H0). pose proof (nonspec_trace_step H1).
pose proof (src_leak_step V V' H H' _ _ _ _ _ _ Hsrc_safe H0 H1 H2).
simpl in H3, H4, H5.
destruct (alist_find decZ (eval_expr_fun a V')), (alist_find decZ (eval_expr_fun a V)).
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
+ pose proof (nonspec_trace_step H0). pose proof (nonspec_trace_step H1).
pose proof (src_leak_step V V' H H' _ _ _ _ _ _ Hsrc_safe H0 H1 H2).
simpl in H3, H4, H5.
destruct (alist_find _ x V'), (alist_find _ x V).
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
+ pose proof (nonspec_trace_step H0). pose proof (nonspec_trace_step H1).
pose proof (src_leak_step V V' H H' _ _ _ _ _ _ Hsrc_safe H0 H1 H2).
simpl in H3, H4, H5.
rewrite! apply_lf'_S in H2. unfold compose in H2. simpl in H2.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0).
* eapply IHn. exact H3. exact H4. exact H5.
* simpl in H2. inversion H2.
* simpl in H2. inversion H2.
* eapply IHn. exact H3. exact H4. exact H5.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
Qed.
(Hsrc_safe: forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre (rem_None ∘ leak_ct)) a):
(nonspec_trace p_src (iv [[Fin.F1]]) ((V, H, s :: s') :: al)) ->
(nonspec_trace p_src (iv [[Fin.FS Fin.F1]]) ((V', H', s :: s') :: al0)) ->
apply_lf' (rem_None ∘ leak_ct) ((V, H, s :: s') :: al) =
apply_lf' (rem_None ∘ leak_ct) ((V', H', s :: s') :: al0) ->
apply_lf' (rem_None ∘ leak_ct) (nonspec_step_fun (V, H, s :: s') :: (V, H, s :: s') :: al) =
apply_lf' (rem_None ∘ leak_ct) (nonspec_step_fun (V', H', s :: s') ::(V', H', s :: s') :: al0).
Proof.
intros.
specialize (Hsrc_safe (Vector.cons (list state)
(nonspec_step_fun (V, H, s :: s') :: (V, H, s :: s') :: al) 1
(Vector.cons (list state)
(nonspec_step_fun (V', H', s :: s') :: (V', H', s :: s') :: al0) 0
(Vector.nil (list state))))).
eapply vl_ll_pre_len_ll_eq in Hsrc_safe.
- unfold v2 in Hsrc_safe. exact Hsrc_safe.
- exact eqDec_obs.
- rewrite Vec_Forall2_forall2.
intros i. dependent destruction i. 2: dependent destruction i. 3: dependent destruction i.
+ simpl. unfold nonspec_trace, multi_nonspec, multi_step'.
rewrite length_cons.
unfold nonspec_trace, multi_nonspec, multi_step' in H0.
rewrite length_cons in H0. rewrite <- H0.
rewrite multi_step_len. rewrite multi_step_S2.
unfold multi_step_hd.
rewrite H0. simpl. reflexivity.
+ simpl. unfold nonspec_trace, multi_nonspec, multi_step'.
rewrite length_cons.
unfold nonspec_trace, multi_nonspec, multi_step' in H1.
rewrite length_cons in H1. rewrite <- H1.
rewrite multi_step_len. rewrite multi_step_S2.
unfold multi_step_hd.
rewrite H1. simpl. reflexivity.
- unfold v2. simpl.
rewrite apply_lf'_S. rewrite H2.
rewrite app_length. symmetry. rewrite apply_lf'_S. rewrite app_length.
rewrite Nat.add_cancel_r.
destruct s; try eapply same_stmt_same_leak_amt.
+ destruct (alist_find decZ (eval_expr_fun a V')), (alist_find decZ (eval_expr_fun a V)); eapply same_stmt_same_leak_amt.
+ destruct (alist_find _ x V'), (alist_find _ x V); eapply same_stmt_same_leak_amt.
+ rewrite! apply_lf'_S in H2. unfold compose in H2. simpl in H2.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0).
* eapply same_stmt_same_leak_amt.
* simpl in H2. inversion H2.
* simpl in H2. inversion H2.
* eapply same_stmt_same_leak_amt.
Qed.
Lemma nonspec_trace_step {p i V H s s'}:
nonspec_trace p i ((V, H, s) :: s') ->
nonspec_trace p i (nonspec_step_fun (V, H, s) :: (V, H, s) :: s').
Proof.
unfold nonspec_trace, multi_nonspec, multi_step'.
rewrite! length_cons.
intros.
rewrite multi_step_S2.
unfold multi_step_hd. rewrite H0. reflexivity.
Qed.
Lemma src_leak_steps n V V' H H' s al al0 (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_ct)) a):
(nonspec_trace p_src (iv [[Fin.F1]]) ((V, H, s) :: al)) ->
(nonspec_trace p_src (iv [[Fin.FS Fin.F1]]) ((V', H', s) :: al0)) ->
apply_lf' (rem_None ∘ leak_ct) ((V, H, s) :: al) =
apply_lf' (rem_None ∘ leak_ct) ((V', H', s) :: al0) ->
| apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun (nonspec_step_fun (V, H, s))
n ++ (V, H, s) :: al) | =
| apply_lf' (rem_None ∘ leak_ct)
(multi_step nonspec_step_fun
(nonspec_step_fun (V', H', s)) n ++
(V', H', s) :: al0) |.
Proof.
intros.
induction n in V, V', H, H', s, al, al0, H0, H1, H2 |-*.
- simpl.
destruct s as [| s s'].
+ rewrite apply_lf'_S. symmetry. rewrite apply_lf'_S. rewrite H2, ! app_length.
reflexivity.
+ fold (nonspec_step_fun (V, H, s :: s')). fold (nonspec_step_fun (V', H', s :: s')).
erewrite src_leak_step. reflexivity. all: eassumption.
- rewrite! multi_step_S.
rewrite <-! app_assoc.
rewrite <-! cons_app.
unfold nonspec_step_fun at 3.
unfold nonspec_step_fun at 3.
unfold nonspec_step_fun at 6.
unfold nonspec_step_fun at 5.
destruct s as [| s s']. 2: destruct s.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* rewrite (apply_lf'_S). symmetry. rewrite (apply_lf'_S). rewrite H2. reflexivity.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
+ pose proof (nonspec_trace_step H0). pose proof (nonspec_trace_step H1).
pose proof (src_leak_step V V' H H' _ _ _ _ _ _ Hsrc_safe H0 H1 H2).
simpl in H3, H4, H5.
destruct (alist_find decZ (eval_expr_fun a V')), (alist_find decZ (eval_expr_fun a V)).
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
+ pose proof (nonspec_trace_step H0). pose proof (nonspec_trace_step H1).
pose proof (src_leak_step V V' H H' _ _ _ _ _ _ Hsrc_safe H0 H1 H2).
simpl in H3, H4, H5.
destruct (alist_find _ x V'), (alist_find _ x V).
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
* eapply IHn. exact H3. exact H4. exact H5.
+ pose proof (nonspec_trace_step H0). pose proof (nonspec_trace_step H1).
pose proof (src_leak_step V V' H H' _ _ _ _ _ _ Hsrc_safe H0 H1 H2).
simpl in H3, H4, H5.
rewrite! apply_lf'_S in H2. unfold compose in H2. simpl in H2.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0).
* eapply IHn. exact H3. exact H4. exact H5.
* simpl in H2. inversion H2.
* simpl in H2. inversion H2.
* eapply IHn. exact H3. exact H4. exact H5.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
+ eapply IHn.
* exact (nonspec_trace_step H0).
* exact (nonspec_trace_step H1).
* eapply src_leak_step. all: eassumption.
Qed.
Definition prog_eq (sl1 sl2: list state) :=
match sl1, sl2 with
| nil, nil => True
| a :: l1, b :: l2 => match a, b with
| (_, _, p1), (_, _, p2) => p1 = p2
end
| _, _ => False
end.
Definition srcrel sl1 sl2 := ll_eq (rem_None ∘ leak_ct) sl1 sl2 /\ prog_eq sl1 sl2.
match sl1, sl2 with
| nil, nil => True
| a :: l1, b :: l2 => match a, b with
| (_, _, p1), (_, _, p2) => p1 = p2
end
| _, _ => False
end.
Definition srcrel sl1 sl2 := ll_eq (rem_None ∘ leak_ct) sl1 sl2 /\ prog_eq sl1 sl2.
One step of the source traces preserves ll_eq.
Lemma src_step_lleq
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(Ha : v2 srcrel a)
(b : Vector.t (list state) 2)
(Hsem : Vector.Forall2 (sem_nonspec p_src) iv (veclist_app b a))
(b0 : Vector.t state 2)
(bs : Vector.t (list state) 2)
(Hbeq : b = veclist_cons b0 bs)
(Hb0 : Vector.Forall (fun x : state => is_B x = true) b0)
(Hbs : Vector.Forall (Forall (fun s : state => is_B s = false)) bs):
prog_eq (veclist_app b a [[Fin.F1]]) (veclist_app b a [[Fin.FS Fin.F1]]) ->
ll_eq (rem_None ∘ leak_ct) (veclist_app b a [[Fin.F1]])
(veclist_app b a [[Fin.FS Fin.F1]]).
Proof.
intros.
eapply vl_ll_pre_len_ll_eq. 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.
++ 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.
rewrite Vec_Forall2_forall2 in Hsem.
specialize (Hsem Fin.F1) as Hsem1.
specialize (Hsem (Fin.FS Fin.F1)) as Hsem2.
rewrite veclist_app_nth in Hsem1, Hsem2.
rewrite Hbeq in Hsem1, Hsem2.
rewrite veclist_cons_nth in Hsem1, Hsem2.
rewrite vec_Forall_forall in Hbs.
specialize (Hbs Fin.F1) as Hbs1.
specialize (Hbs (Fin.FS Fin.F1)) as Hbs2.
apply forall_not_isB_is_nil in Hbs1, Hbs2.
rewrite Hbs1, Hbs2 in *.
simpl in Hsem1, Hsem2.
rewrite! veclist_app_nth in H.
rewrite Hbeq in H.
rewrite! veclist_cons_nth in H.
rewrite Hbs1, Hbs2 in H. simpl in H.
destruct (b0 [[Fin.F1]]), (b0 [[Fin.FS Fin.F1]]).
unfold compose.
destruct p, p0.
subst.
now apply same_stmt_same_leak_amt.
++ 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.
** 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_is_nil (bs [[Fin.F1]])). 2: auto.
rewrite (forall_not_isB_is_nil (bs [[Fin.FS Fin.F1]])). 2: auto.
reflexivity.
** unfold v2 in Ha. destruct Ha.
unfold ll_eq in H.
rewrite H0.
reflexivity.
Qed.
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(Ha : v2 srcrel a)
(b : Vector.t (list state) 2)
(Hsem : Vector.Forall2 (sem_nonspec p_src) iv (veclist_app b a))
(b0 : Vector.t state 2)
(bs : Vector.t (list state) 2)
(Hbeq : b = veclist_cons b0 bs)
(Hb0 : Vector.Forall (fun x : state => is_B x = true) b0)
(Hbs : Vector.Forall (Forall (fun s : state => is_B s = false)) bs):
prog_eq (veclist_app b a [[Fin.F1]]) (veclist_app b a [[Fin.FS Fin.F1]]) ->
ll_eq (rem_None ∘ leak_ct) (veclist_app b a [[Fin.F1]])
(veclist_app b a [[Fin.FS Fin.F1]]).
Proof.
intros.
eapply vl_ll_pre_len_ll_eq. 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.
++ 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.
rewrite Vec_Forall2_forall2 in Hsem.
specialize (Hsem Fin.F1) as Hsem1.
specialize (Hsem (Fin.FS Fin.F1)) as Hsem2.
rewrite veclist_app_nth in Hsem1, Hsem2.
rewrite Hbeq in Hsem1, Hsem2.
rewrite veclist_cons_nth in Hsem1, Hsem2.
rewrite vec_Forall_forall in Hbs.
specialize (Hbs Fin.F1) as Hbs1.
specialize (Hbs (Fin.FS Fin.F1)) as Hbs2.
apply forall_not_isB_is_nil in Hbs1, Hbs2.
rewrite Hbs1, Hbs2 in *.
simpl in Hsem1, Hsem2.
rewrite! veclist_app_nth in H.
rewrite Hbeq in H.
rewrite! veclist_cons_nth in H.
rewrite Hbs1, Hbs2 in H. simpl in H.
destruct (b0 [[Fin.F1]]), (b0 [[Fin.FS Fin.F1]]).
unfold compose.
destruct p, p0.
subst.
now apply same_stmt_same_leak_amt.
++ 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.
** 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_is_nil (bs [[Fin.F1]])). 2: auto.
rewrite (forall_not_isB_is_nil (bs [[Fin.FS Fin.F1]])). 2: auto.
reflexivity.
** unfold v2 in Ha. destruct Ha.
unfold ll_eq in H.
rewrite H0.
reflexivity.
Qed.
Lemma srcrel_step
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(Ha : v2 srcrel a)
(b : Vector.t (list state) 2)
(Hsem : Vector.Forall2 (sem_nonspec p_src) iv (veclist_app b a))
(b0 : Vector.t state 2)
(bs : Vector.t (list state) 2)
(Hbeq : b = veclist_cons b0 bs)
(Hb0 : Vector.Forall (fun x : state => is_B x = true) b0)
(Hbs : Vector.Forall (Forall (fun s : state => is_B s = false)) bs):
v2 srcrel (veclist_app b a).
Proof.
unfold v2, srcrel.
match goal with
|- ?x /\ ?y => let Q := fresh "Q" in enough ((y -> x) /\ y) as Q
end.
{ clear - Q. destruct Q. specialize (H H0). easy. }
split.
{ eapply src_step_lleq; eauto. }
rewrite Hbeq. rewrite! veclist_app_nth. rewrite! veclist_cons_nth.
rewrite vec_Forall_forall in Hbs.
specialize (Hbs Fin.F1) as Hbs1.
specialize (Hbs (Fin.FS Fin.F1)) as Hbs2.
apply forall_not_isB_is_nil in Hbs1, Hbs2.
rewrite Hbs1, Hbs2. simpl.
specialize (Hsrc_safe _ Hsem) as Hsrc_safe'.
rewrite Vec_Forall2_forall2 in Hsem.
specialize (Hsem Fin.F1) as Hsem1.
specialize (Hsem (Fin.FS Fin.F1)) as Hsem2.
rewrite Hbeq in Hsem1, Hsem2.
rewrite veclist_app_nth in Hsem1, Hsem2.
rewrite veclist_cons_nth in Hsem1, Hsem2.
rewrite Hbs1 in Hsem1. rewrite Hbs2 in Hsem2.
simpl in Hsem1, Hsem2.
unfold sem_nonspec, nonspec_trace, multi_nonspec, multi_step' in Hsem1, Hsem2.
rewrite length_cons in Hsem1, Hsem2.
destruct Ha as (Ha0 & Ha2).
unfold v2 in Hsrc_safe'. rewrite Hbeq in Hsrc_safe'.
rewrite! veclist_app_nth in Hsrc_safe'.
rewrite! veclist_cons_nth in Hsrc_safe'.
rewrite Hbs1, Hbs2 in Hsrc_safe'. simpl in Hsrc_safe'.
destruct ( a [[Fin.FS Fin.F1]]), ( a [[Fin.F1]]).
++ simpl in Hsem1, Hsem2. inversion Hsem1. inversion Hsem2. reflexivity.
++ now simpl in Ha2.
++ now simpl in Ha2.
++ rewrite length_cons in Hsem1, Hsem2. rewrite multi_step_S2 in Hsem1, Hsem2. inversion Hsem1. inversion Hsem2.
unfold multi_step_hd in H0, H2. rewrite H1 in H0. rewrite H3 in H2. simpl in H0, H3.
destruct s0 as [ [v h] s0]. destruct s as [ [v' h'] s]. simpl in Ha2. subst.
unfold multi_step_hd. rewrite H1, H3. simpl.
destruct s. reflexivity.
unfold ll_eq in Ha0.
rewrite! apply_lf'_S in Ha0.
destruct s; try reflexivity.
** destruct (alist_find decZ (eval_expr_fun a0 v) h), (alist_find decZ (eval_expr_fun a0 v') h'); reflexivity.
** destruct (alist_find _ x v), (alist_find _ x v'); reflexivity.
** unfold compose in Ha0. simpl in Ha0.
destruct (Z.eq_dec (eval_expr_fun c v) 0), (Z.eq_dec (eval_expr_fun c v') 0).
--- reflexivity.
--- simpl in Ha0. inversion Ha0.
--- simpl in Ha0. inversion Ha0.
--- reflexivity.
Qed.
Lemma srcrel_tgtrel_If_18steps
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(V : varmap)
(H : heap)
(al : list state)
(V' : varmap)
(H' : heap)
(c : Lang.expr)
(s1 s2 s' : list stmt)
(al0 : list state)
(Ha0 : ll_eq (rem_None ∘ leak_ct) ((V, H, If c s1 s2 :: s') :: al)
((V', H', If c s1 s2 :: s') :: al0))
(αs0 αs : list (list specstate))
(b0 : Vector.t state 2)
(Hsrc_ni : rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src)
((V, H, If c s1 s2 :: s') :: al)))) =
rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0)))))
(β1 : list specstate)
(βαl : list (list specstate))
(H2 : a [[Fin.F1]] = (V, H, If c s1 s2 :: s') :: al)
(H3 : multi_step' spec_step_fun
(spec_step_fun
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V, H, If c s1 s2 :: s')) ++
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs0 =
β1 :: βαl)
(H5 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src) ((V, H, If c s1 s2 :: s') :: al)))
β1)
(β3 : list specstate)
(βαl0 : list (list specstate))
(H10 : a [[Fin.FS Fin.F1]] = (V', H', If c s1 s2 :: s') :: al0)
(H11 : multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V', H', If c s1 s2 :: s')) ++
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs =
β3 :: βαl0)
(H13 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0))) β3)
(Hsa1 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
b0 [[Fin.F1]] :: (V, H, If c s1 s2 :: s') :: al)
(Hsa2 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |) =
b0 [[Fin.FS Fin.F1]] :: (V', H', If c s1 s2 :: s') :: al0)
(H7 : multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
(V, H, If c s1 s2 :: s') :: al)
(H9 : multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src) (| al0 |) =
(V', H', If c s1 s2 :: s') :: al0)
(l : list syntObs)
(Hla : leak_lookahead sixteen s1 = Some l)
(e : Some l = leak_lookahead sixteen s2)
(Hdec : dec_syntObsL (Some l) (leak_lookahead sixteen s2) = left e):
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun ((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
eighteen) =
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil)) eighteen).
Proof.
unfold multi_step'.
assert (eighteen = S (S sixteen)) as -> by reflexivity.
rewrite multi_step_S2. rewrite multi_step_S2 with (n := sixteen).
rewrite! apply_lf'_S.
match goal with [|- ?x ++ ?y = ?w ++ ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: rewrite Q3, Q4; reflexivity.
-- rewrite cr_sim_step_unfold in H11.
cbn zeta in H11.
rewrite Hla, Hdec in H11. unfold multi_step' in H11.
replace eighteen with (S (S sixteen)) in H11 by reflexivity.
rewrite multi_step_S2 in H11.
rewrite <- app_comm_cons in H11.
apply cons_inv_l in H11. subst.
rewrite cr_sim_step_unfold in H3.
cbn zeta in H3.
rewrite Hla, Hdec in H3. unfold multi_step' in H3.
replace eighteen with (S (S sixteen)) in H3 by reflexivity.
rewrite multi_step_S2 in H3.
rewrite <- app_comm_cons in H3.
apply cons_inv_l in H3. subst.
unfold compose.
erewrite <- sim_same_leakage. 2: exact H5.
rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity. exact H13.
-- erewrite leak_lookahead_same_leakage. 3: exact Hla. 2: rewrite Hla; exact e.
erewrite leak_lookahead_same_leakage. 3: exact Hla. 2: rewrite Hla; exact e.
pose (Vector.cons _ (multi_step nonspec_step_fun (nonspec_step_fun (V, H, If c s1 s2 :: s')) fifteen) 1 (Vector.cons _ (multi_step nonspec_step_fun (nonspec_step_fun (V', H', If c s1 s2 :: s')) fifteen) 0 (Vector.nil _))) as a'.
specialize (Hsrc_safe (veclist_app a' a)) as Hsrc_safe'.
unfold v2, ll_pre in Hsrc_safe'.
eapply vl_ll_pre_len_ll_eq in Hsrc_safe'. 2: exact eqDec_obs.
2: {
rewrite Vec_Forall2_forall2.
intros i. dependent destruction i. 2: dependent destruction i. 3: dependent destruction i.
- rewrite veclist_app_nth.
unfold nonspec_trace, multi_nonspec.
rewrite app_length.
change (a' [[Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V, H, If c s1 s2 :: s')) fifteen).
rewrite multi_step_len.
change (sixteen + (|a [[Fin.F1]]|)) with (S (fifteen + (|a [[Fin.F1]]|))).
unfold multi_step'.
rewrite H2. rewrite length_cons, <- H7.
assert (S fifteen + S(|al|) = (S (S fifteen + |al|))) as -> by lia_fs.
rewrite multi_step_app.
f_equal.
unfold multi_step_hd. rewrite H7. reflexivity.
- rewrite veclist_app_nth.
unfold nonspec_trace, multi_nonspec.
rewrite app_length.
change (a' [[Fin.FS Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V', H', If c s1 s2 :: s')) fifteen).
rewrite multi_step_len.
change (sixteen + (|a [[Fin.FS Fin.F1]]|)) with (S (fifteen + (|a [[Fin.FS Fin.F1]]|))).
unfold multi_step'.
rewrite H10. rewrite length_cons, <- H9.
assert (S fifteen + S (|al0|) = S (S fifteen + |al0|)) as -> by lia_fs.
rewrite multi_step_app.
f_equal.
unfold multi_step_hd. rewrite H9. reflexivity.
}
2: {
unfold v2.
rewrite! veclist_app_nth, H2, H10.
change (a' [[Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V, H, If c s1 s2 :: s')) fifteen).
change (a' [[Fin.FS Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V', H', If c s1 s2 :: s')) fifteen).
unfold ll_eq in Ha0.
eapply src_leak_steps.
4: assumption.
- exact Hsrc_safe.
- unfold nonspec_trace, multi_nonspec, multi_step'. rewrite length_cons. now inversion Hsa1.
- unfold nonspec_trace, multi_nonspec, multi_step'. rewrite length_cons. now inversion Hsa2.
}
unfold v2, ll_eq in Hsrc_safe'. rewrite! veclist_app_nth in Hsrc_safe'.
rewrite! apply_lf'_app in Hsrc_safe'.
unfold ll_eq in Ha0. rewrite <- H2, <- H10 in Ha0. rewrite Ha0 in Hsrc_safe'.
rewrite app_inv_tail_iff in Hsrc_safe'. exact Hsrc_safe'.
Qed.
Lemma srcrel_tgtrel_If
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(V : varmap)
(H : heap)
(al : list state)
(V' : varmap)
(H' : heap)
(c : Lang.expr)
(s1 s2 s' : list stmt)
(al0 : list state)
(Ha0 : ll_eq (rem_None ∘ leak_ct) ((V, H, If c s1 s2 :: s') :: al)
((V', H', If c s1 s2 :: s') :: al0))
(αs0 αs : list (list specstate))
(b0 : Vector.t state 2)
(Hsrc_ni : rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src)
((V, H, If c s1 s2 :: s') :: al)))) =
rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0)))))
(β1 : list specstate)
(βαl : list (list specstate))
(H2 : a [[Fin.F1]] = (V, H, If c s1 s2 :: s') :: al)
(H3 : multi_step' spec_step_fun
(spec_step_fun
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V, H, If c s1 s2 :: s')) ++
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs0 =
β1 :: βαl)
(H5 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src) ((V, H, If c s1 s2 :: s') :: al)))
β1)
(β3 : list specstate)
(βαl0 : list (list specstate))
(H10 : a [[Fin.FS Fin.F1]] = (V', H', If c s1 s2 :: s') :: al0)
(H11 : multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V', H', If c s1 s2 :: s')) ++
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs =
β3 :: βαl0)
(H13 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0))) β3)
(Hsa1 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
b0 [[Fin.F1]] :: (V, H, If c s1 s2 :: s') :: al)
(Hsa2 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |) =
b0 [[Fin.FS Fin.F1]] :: (V', H', If c s1 s2 :: s') :: al0)
(H7 : multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
(V, H, If c s1 s2 :: s') :: al)
(H9 : multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src) (| al0 |) =
(V', H', If c s1 s2 :: s') :: al0):
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun ((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V, H, If c s1 s2 :: s'))) =
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V', H', If c s1 s2 :: s'))).
Proof.
repeat rewrite cr_sim_step_unfold.
cbn zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)) eqn: Hdec.
destruct (leak_lookahead sixteen s1) eqn: Hla.
* apply srcrel_tgtrel_If_18steps with (iv := iv) (p_src := p_src) (a := a) (al := al) (al0 := al0) (αs0 := αs0) (αs := αs) (b0 := b0) (β1 := β1) (βαl := βαl) (β3 := β3) (βαl0 := βαl0) (l := l) (e := e); assumption.
* unfold multi_step'. rewrite multi_step_S2.
rewrite multi_step_S2 with (n := 2).
rewrite! apply_lf'_S.
match goal with [|- ?x ++ ?y = ?w ++ ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: rewrite Q3, Q4; reflexivity.
-- rewrite cr_sim_step_unfold in H11.
cbn zeta in H11.
rewrite Hla, Hdec in H11. unfold multi_step' in H11. rewrite multi_step_S2 in H11.
rewrite <- app_comm_cons in H11.
apply cons_inv_l in H11. subst.
rewrite cr_sim_step_unfold in H3.
cbn zeta in H3.
rewrite Hla, Hdec in H3. unfold multi_step' in H3. rewrite multi_step_S2 in H3.
rewrite <- app_comm_cons in H3.
apply cons_inv_l in H3. subst.
unfold compose.
erewrite <- sim_same_leakage. 2: exact H5.
rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity. exact H13.
-- simpl. simp comp_relaxed. cbv zeta. rewrite Hla, Hdec.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0); reflexivity.
* unfold multi_step'. rewrite multi_step_S2.
rewrite multi_step_S2 with (n := 2).
rewrite! apply_lf'_S.
match goal with [|- ?x ++ ?y = ?w ++ ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: rewrite Q3, Q4; reflexivity.
-- rewrite cr_sim_step_unfold in H11.
cbn zeta in H11.
rewrite Hdec in H11. unfold multi_step' in H11. rewrite multi_step_S2 in H11.
rewrite <- app_comm_cons in H11.
apply cons_inv_l in H11. subst.
rewrite cr_sim_step_unfold in H3.
cbn zeta in H3.
rewrite Hdec in H3. unfold multi_step' in H3. rewrite multi_step_S2 in H3.
rewrite <- app_comm_cons in H3.
apply cons_inv_l in H3. subst.
unfold compose.
erewrite <- sim_same_leakage. 2: exact H5.
rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity. exact H13.
-- simpl. simp comp_relaxed. cbv zeta. rewrite Hdec.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0); reflexivity.
Qed.
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(Ha : v2 srcrel a)
(b : Vector.t (list state) 2)
(Hsem : Vector.Forall2 (sem_nonspec p_src) iv (veclist_app b a))
(b0 : Vector.t state 2)
(bs : Vector.t (list state) 2)
(Hbeq : b = veclist_cons b0 bs)
(Hb0 : Vector.Forall (fun x : state => is_B x = true) b0)
(Hbs : Vector.Forall (Forall (fun s : state => is_B s = false)) bs):
v2 srcrel (veclist_app b a).
Proof.
unfold v2, srcrel.
match goal with
|- ?x /\ ?y => let Q := fresh "Q" in enough ((y -> x) /\ y) as Q
end.
{ clear - Q. destruct Q. specialize (H H0). easy. }
split.
{ eapply src_step_lleq; eauto. }
rewrite Hbeq. rewrite! veclist_app_nth. rewrite! veclist_cons_nth.
rewrite vec_Forall_forall in Hbs.
specialize (Hbs Fin.F1) as Hbs1.
specialize (Hbs (Fin.FS Fin.F1)) as Hbs2.
apply forall_not_isB_is_nil in Hbs1, Hbs2.
rewrite Hbs1, Hbs2. simpl.
specialize (Hsrc_safe _ Hsem) as Hsrc_safe'.
rewrite Vec_Forall2_forall2 in Hsem.
specialize (Hsem Fin.F1) as Hsem1.
specialize (Hsem (Fin.FS Fin.F1)) as Hsem2.
rewrite Hbeq in Hsem1, Hsem2.
rewrite veclist_app_nth in Hsem1, Hsem2.
rewrite veclist_cons_nth in Hsem1, Hsem2.
rewrite Hbs1 in Hsem1. rewrite Hbs2 in Hsem2.
simpl in Hsem1, Hsem2.
unfold sem_nonspec, nonspec_trace, multi_nonspec, multi_step' in Hsem1, Hsem2.
rewrite length_cons in Hsem1, Hsem2.
destruct Ha as (Ha0 & Ha2).
unfold v2 in Hsrc_safe'. rewrite Hbeq in Hsrc_safe'.
rewrite! veclist_app_nth in Hsrc_safe'.
rewrite! veclist_cons_nth in Hsrc_safe'.
rewrite Hbs1, Hbs2 in Hsrc_safe'. simpl in Hsrc_safe'.
destruct ( a [[Fin.FS Fin.F1]]), ( a [[Fin.F1]]).
++ simpl in Hsem1, Hsem2. inversion Hsem1. inversion Hsem2. reflexivity.
++ now simpl in Ha2.
++ now simpl in Ha2.
++ rewrite length_cons in Hsem1, Hsem2. rewrite multi_step_S2 in Hsem1, Hsem2. inversion Hsem1. inversion Hsem2.
unfold multi_step_hd in H0, H2. rewrite H1 in H0. rewrite H3 in H2. simpl in H0, H3.
destruct s0 as [ [v h] s0]. destruct s as [ [v' h'] s]. simpl in Ha2. subst.
unfold multi_step_hd. rewrite H1, H3. simpl.
destruct s. reflexivity.
unfold ll_eq in Ha0.
rewrite! apply_lf'_S in Ha0.
destruct s; try reflexivity.
** destruct (alist_find decZ (eval_expr_fun a0 v) h), (alist_find decZ (eval_expr_fun a0 v') h'); reflexivity.
** destruct (alist_find _ x v), (alist_find _ x v'); reflexivity.
** unfold compose in Ha0. simpl in Ha0.
destruct (Z.eq_dec (eval_expr_fun c v) 0), (Z.eq_dec (eval_expr_fun c v') 0).
--- reflexivity.
--- simpl in Ha0. inversion Ha0.
--- simpl in Ha0. inversion Ha0.
--- reflexivity.
Qed.
Lemma srcrel_tgtrel_If_18steps
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(V : varmap)
(H : heap)
(al : list state)
(V' : varmap)
(H' : heap)
(c : Lang.expr)
(s1 s2 s' : list stmt)
(al0 : list state)
(Ha0 : ll_eq (rem_None ∘ leak_ct) ((V, H, If c s1 s2 :: s') :: al)
((V', H', If c s1 s2 :: s') :: al0))
(αs0 αs : list (list specstate))
(b0 : Vector.t state 2)
(Hsrc_ni : rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src)
((V, H, If c s1 s2 :: s') :: al)))) =
rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0)))))
(β1 : list specstate)
(βαl : list (list specstate))
(H2 : a [[Fin.F1]] = (V, H, If c s1 s2 :: s') :: al)
(H3 : multi_step' spec_step_fun
(spec_step_fun
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V, H, If c s1 s2 :: s')) ++
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs0 =
β1 :: βαl)
(H5 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src) ((V, H, If c s1 s2 :: s') :: al)))
β1)
(β3 : list specstate)
(βαl0 : list (list specstate))
(H10 : a [[Fin.FS Fin.F1]] = (V', H', If c s1 s2 :: s') :: al0)
(H11 : multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V', H', If c s1 s2 :: s')) ++
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs =
β3 :: βαl0)
(H13 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0))) β3)
(Hsa1 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
b0 [[Fin.F1]] :: (V, H, If c s1 s2 :: s') :: al)
(Hsa2 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |) =
b0 [[Fin.FS Fin.F1]] :: (V', H', If c s1 s2 :: s') :: al0)
(H7 : multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
(V, H, If c s1 s2 :: s') :: al)
(H9 : multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src) (| al0 |) =
(V', H', If c s1 s2 :: s') :: al0)
(l : list syntObs)
(Hla : leak_lookahead sixteen s1 = Some l)
(e : Some l = leak_lookahead sixteen s2)
(Hdec : dec_syntObsL (Some l) (leak_lookahead sixteen s2) = left e):
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun ((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
eighteen) =
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil)) eighteen).
Proof.
unfold multi_step'.
assert (eighteen = S (S sixteen)) as -> by reflexivity.
rewrite multi_step_S2. rewrite multi_step_S2 with (n := sixteen).
rewrite! apply_lf'_S.
match goal with [|- ?x ++ ?y = ?w ++ ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: rewrite Q3, Q4; reflexivity.
-- rewrite cr_sim_step_unfold in H11.
cbn zeta in H11.
rewrite Hla, Hdec in H11. unfold multi_step' in H11.
replace eighteen with (S (S sixteen)) in H11 by reflexivity.
rewrite multi_step_S2 in H11.
rewrite <- app_comm_cons in H11.
apply cons_inv_l in H11. subst.
rewrite cr_sim_step_unfold in H3.
cbn zeta in H3.
rewrite Hla, Hdec in H3. unfold multi_step' in H3.
replace eighteen with (S (S sixteen)) in H3 by reflexivity.
rewrite multi_step_S2 in H3.
rewrite <- app_comm_cons in H3.
apply cons_inv_l in H3. subst.
unfold compose.
erewrite <- sim_same_leakage. 2: exact H5.
rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity. exact H13.
-- erewrite leak_lookahead_same_leakage. 3: exact Hla. 2: rewrite Hla; exact e.
erewrite leak_lookahead_same_leakage. 3: exact Hla. 2: rewrite Hla; exact e.
pose (Vector.cons _ (multi_step nonspec_step_fun (nonspec_step_fun (V, H, If c s1 s2 :: s')) fifteen) 1 (Vector.cons _ (multi_step nonspec_step_fun (nonspec_step_fun (V', H', If c s1 s2 :: s')) fifteen) 0 (Vector.nil _))) as a'.
specialize (Hsrc_safe (veclist_app a' a)) as Hsrc_safe'.
unfold v2, ll_pre in Hsrc_safe'.
eapply vl_ll_pre_len_ll_eq in Hsrc_safe'. 2: exact eqDec_obs.
2: {
rewrite Vec_Forall2_forall2.
intros i. dependent destruction i. 2: dependent destruction i. 3: dependent destruction i.
- rewrite veclist_app_nth.
unfold nonspec_trace, multi_nonspec.
rewrite app_length.
change (a' [[Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V, H, If c s1 s2 :: s')) fifteen).
rewrite multi_step_len.
change (sixteen + (|a [[Fin.F1]]|)) with (S (fifteen + (|a [[Fin.F1]]|))).
unfold multi_step'.
rewrite H2. rewrite length_cons, <- H7.
assert (S fifteen + S(|al|) = (S (S fifteen + |al|))) as -> by lia_fs.
rewrite multi_step_app.
f_equal.
unfold multi_step_hd. rewrite H7. reflexivity.
- rewrite veclist_app_nth.
unfold nonspec_trace, multi_nonspec.
rewrite app_length.
change (a' [[Fin.FS Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V', H', If c s1 s2 :: s')) fifteen).
rewrite multi_step_len.
change (sixteen + (|a [[Fin.FS Fin.F1]]|)) with (S (fifteen + (|a [[Fin.FS Fin.F1]]|))).
unfold multi_step'.
rewrite H10. rewrite length_cons, <- H9.
assert (S fifteen + S (|al0|) = S (S fifteen + |al0|)) as -> by lia_fs.
rewrite multi_step_app.
f_equal.
unfold multi_step_hd. rewrite H9. reflexivity.
}
2: {
unfold v2.
rewrite! veclist_app_nth, H2, H10.
change (a' [[Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V, H, If c s1 s2 :: s')) fifteen).
change (a' [[Fin.FS Fin.F1]]) with (multi_step nonspec_step_fun (nonspec_step_fun (V', H', If c s1 s2 :: s')) fifteen).
unfold ll_eq in Ha0.
eapply src_leak_steps.
4: assumption.
- exact Hsrc_safe.
- unfold nonspec_trace, multi_nonspec, multi_step'. rewrite length_cons. now inversion Hsa1.
- unfold nonspec_trace, multi_nonspec, multi_step'. rewrite length_cons. now inversion Hsa2.
}
unfold v2, ll_eq in Hsrc_safe'. rewrite! veclist_app_nth in Hsrc_safe'.
rewrite! apply_lf'_app in Hsrc_safe'.
unfold ll_eq in Ha0. rewrite <- H2, <- H10 in Ha0. rewrite Ha0 in Hsrc_safe'.
rewrite app_inv_tail_iff in Hsrc_safe'. exact Hsrc_safe'.
Qed.
Lemma srcrel_tgtrel_If
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(V : varmap)
(H : heap)
(al : list state)
(V' : varmap)
(H' : heap)
(c : Lang.expr)
(s1 s2 s' : list stmt)
(al0 : list state)
(Ha0 : ll_eq (rem_None ∘ leak_ct) ((V, H, If c s1 s2 :: s') :: al)
((V', H', If c s1 s2 :: s') :: al0))
(αs0 αs : list (list specstate))
(b0 : Vector.t state 2)
(Hsrc_ni : rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src)
((V, H, If c s1 s2 :: s') :: al)))) =
rem_None
(leak_ct
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0)))))
(β1 : list specstate)
(βαl : list (list specstate))
(H2 : a [[Fin.F1]] = (V, H, If c s1 s2 :: s') :: al)
(H3 : multi_step' spec_step_fun
(spec_step_fun
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V, H, If c s1 s2 :: s')) ++
((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs0 =
β1 :: βαl)
(H5 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.F1]], p_src) ((V, H, If c s1 s2 :: s') :: al)))
β1)
(β3 : list specstate)
(βαl0 : list (list specstate))
(H10 : a [[Fin.FS Fin.F1]] = (V', H', If c s1 s2 :: s') :: al0)
(H11 : multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V', H', If c s1 s2 :: s')) ++
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil) :: αs =
β3 :: βαl0)
(H13 : cr_sim'
(nonspec_step_fun
(hd (nil, iv [[Fin.FS Fin.F1]], p_src)
((V', H', If c s1 s2 :: s') :: al0))) β3)
(Hsa1 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
b0 [[Fin.F1]] :: (V, H, If c s1 s2 :: s') :: al)
(Hsa2 : nonspec_step_fun
(multi_step_hd nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |))
:: multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src)
(| al0 |) =
b0 [[Fin.FS Fin.F1]] :: (V', H', If c s1 s2 :: s') :: al0)
(H7 : multi_step nonspec_step_fun (nil, iv [[Fin.F1]], p_src) (| al |) =
(V, H, If c s1 s2 :: s') :: al)
(H9 : multi_step nonspec_step_fun (nil, iv [[Fin.FS Fin.F1]], p_src) (| al0 |) =
(V', H', If c s1 s2 :: s') :: al0):
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun ((None, V, H, comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V, H, If c s1 s2 :: s'))) =
apply_lf' (rem_None ∘ leak_ct')
(multi_step' spec_step_fun
(spec_step_fun
((None, V', H', comp_relaxed sixteen (If c s1 s2 :: s')) :: nil))
(cr_sim_step (V', H', If c s1 s2 :: s'))).
Proof.
repeat rewrite cr_sim_step_unfold.
cbn zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)) eqn: Hdec.
destruct (leak_lookahead sixteen s1) eqn: Hla.
* apply srcrel_tgtrel_If_18steps with (iv := iv) (p_src := p_src) (a := a) (al := al) (al0 := al0) (αs0 := αs0) (αs := αs) (b0 := b0) (β1 := β1) (βαl := βαl) (β3 := β3) (βαl0 := βαl0) (l := l) (e := e); assumption.
* unfold multi_step'. rewrite multi_step_S2.
rewrite multi_step_S2 with (n := 2).
rewrite! apply_lf'_S.
match goal with [|- ?x ++ ?y = ?w ++ ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: rewrite Q3, Q4; reflexivity.
-- rewrite cr_sim_step_unfold in H11.
cbn zeta in H11.
rewrite Hla, Hdec in H11. unfold multi_step' in H11. rewrite multi_step_S2 in H11.
rewrite <- app_comm_cons in H11.
apply cons_inv_l in H11. subst.
rewrite cr_sim_step_unfold in H3.
cbn zeta in H3.
rewrite Hla, Hdec in H3. unfold multi_step' in H3. rewrite multi_step_S2 in H3.
rewrite <- app_comm_cons in H3.
apply cons_inv_l in H3. subst.
unfold compose.
erewrite <- sim_same_leakage. 2: exact H5.
rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity. exact H13.
-- simpl. simp comp_relaxed. cbv zeta. rewrite Hla, Hdec.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0); reflexivity.
* unfold multi_step'. rewrite multi_step_S2.
rewrite multi_step_S2 with (n := 2).
rewrite! apply_lf'_S.
match goal with [|- ?x ++ ?y = ?w ++ ?z] => assert (x = w) as Q3;[|assert (y = z) as Q4] end.
3: rewrite Q3, Q4; reflexivity.
-- rewrite cr_sim_step_unfold in H11.
cbn zeta in H11.
rewrite Hdec in H11. unfold multi_step' in H11. rewrite multi_step_S2 in H11.
rewrite <- app_comm_cons in H11.
apply cons_inv_l in H11. subst.
rewrite cr_sim_step_unfold in H3.
cbn zeta in H3.
rewrite Hdec in H3. unfold multi_step' in H3. rewrite multi_step_S2 in H3.
rewrite <- app_comm_cons in H3.
apply cons_inv_l in H3. subst.
unfold compose.
erewrite <- sim_same_leakage. 2: exact H5.
rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity. exact H13.
-- simpl. simp comp_relaxed. cbv zeta. rewrite Hdec.
destruct (Z.eq_dec (eval_expr_fun c V) 0), (Z.eq_dec (eval_expr_fun c V') 0); reflexivity.
Qed.
The source relation implies the target relation.
For the complicated case, If, where speculative execution can occur, we use the previous two lemmas.
Lemma srcrel_impl_tgtrel
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(Ha : v2 srcrel a)
(α : Vector.t (list (list specstate)) 2)
(Hα : v2 (ll_eq (rem_None ∘ leak_ct')) α)
(Hsim : Vec_Forall3 (cr_sim p_src) iv a α)
(b : Vector.t (list state) 2)
(Hsem : Vector.Forall2 (sem_nonspec p_src) iv (veclist_app b a))
(β : Vector.t (list (list specstate)) 2)
(Hsem' : Vector.Forall2 (sem_spec_am (comp_relaxed' p_src)) iv
(veclist_app β α))
(Hsim' : Vec_Forall3 (cr_sim p_src) iv (veclist_app b a) (veclist_app β α))
(b0 : Vector.t state 2)
(bs : Vector.t (list state) 2)
(Hbeq : b = veclist_cons b0 bs)
(Hb0 : Vector.Forall (fun x : state => is_B x = true) b0)
(Hbs : Vector.Forall (Forall (fun s : state => is_B s = false)) bs):
v2 srcrel (veclist_app b a) ->
v2 (ll_eq (rem_None ∘ leak_ct')) (veclist_app β α).
Proof.
intros Hsrc_ni. unfold v2.
unfold ll_eq.
unfold v2, ll_eq in Hsrc_ni.
pose proof (vector_forall_nth _ _ _ Hbs Fin.F1) as Hbs1.
pose proof (vector_forall_nth _ _ _ Hbs (Fin.FS Fin.F1)) as Hbs2.
apply forall_not_isB_is_nil in Hbs1, Hbs2.
rewrite Hbeq in Hsim'.
rewrite vec_forall3_forall in Hsim'.
specialize (Hsim' Fin.F1) as Hsim1.
specialize (Hsim' (Fin.FS Fin.F1)) as Hsim2. clear Hsim' Hbs.
rewrite vl_cons_app in Hsim1, Hsim2.
rewrite veclist_cons_nth in Hsim1, Hsim2.
rewrite veclist_app_nth in Hsim1, Hsim2.
rewrite Hbs1 in Hsim1. rewrite Hbs2 in Hsim2.
rewrite app_nil_l in Hsim1, Hsim2.
rewrite! veclist_app_nth in *.
inversion Hsim1; inversion Hsim2; subst.
- destruct p_src.
+ unfold comp_relaxed'. simp comp_relaxed. cbn. reflexivity.
+ unfold comp_relaxed'. destruct s; simp comp_relaxed.
1-3, 6-7: reflexivity.
* cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)).
destruct (leak_lookahead sixteen s1).
all: rewrite! apply_lf'_S; do 5 f_equal.
* cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)).
destruct (leak_lookahead sixteen s1).
all: rewrite! apply_lf'_S; do 5 f_equal.
- clear - Ha H1 H6.
unfold v2, srcrel in Ha. destruct Ha as (_ & Ha).
rewrite <- H1, H6 in Ha. now simpl in Ha.
- clear - Ha H2 H9.
unfold v2, srcrel in Ha. destruct Ha as (_ & Ha).
rewrite H2, <- H9 in Ha. now simpl in Ha.
- assert (α0 = α[[Fin.F1]]) as ->.
{ eapply cr_sim_eq.
3: exact H6.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'. rewrite <- H1 in Hsem'.
apply multi_step_split in Hsem'. destructH.
exact Hsem'1.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'.
apply multi_step_split in Hsem'. destructH.
exact Hsem'1.
- rewrite vec_forall3_forall in Hsim. apply Hsim.
}
assert (α1 = α[[Fin.FS Fin.F1]]) as ->.
{ eapply cr_sim_eq.
3: eassumption.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'. rewrite <- H9 in Hsem'.
apply multi_step_split in Hsem'. destructH.
eassumption.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'.
eapply multi_step_split in Hsem'. destructH.
eassumption.
- rewrite vec_forall3_forall in Hsim. apply Hsim.
}
unfold v2, ll_eq in Hα.
rewrite! apply_lf'_app. rewrite Hα. f_equal.
rewrite app_inv_tail_iff in H1. subst.
rewrite app_inv_tail_iff in H9. subst.
unfold v2, srcrel in Ha.
rewrite H2, H10 in Ha.
destructH.
unfold prog_eq in Ha1.
destruct a1 as [ [V H] s].
destruct a3 as [ [V' H'] s'].
subst.
rewrite! veclist_cons_nth in Hsrc_ni.
rewrite Hbs1, Hbs2 in Hsrc_ni. simpl in Hsrc_ni.
rewrite Vec_Forall2_forall2 in Hsem.
specialize (Hsem Fin.F1) as Hsa1.
specialize (Hsem (Fin.FS Fin.F1)) as Hsa2.
rewrite veclist_app_nth in Hsa1, Hsa2.
rewrite veclist_cons_nth in Hsa1, Hsa2.
rewrite Hbs1 in Hsa1. rewrite Hbs2 in Hsa2.
simpl in Hsa1, Hsa2.
rewrite Vec_Forall2_forall2 in Hsem'.
specialize (Hsem' Fin.F1) as Hsem1.
specialize (Hsem' (Fin.FS Fin.F1)) as Hsem2.
rewrite veclist_app_nth in Hsem1, Hsem2.
rewrite vec_forall3_forall in Hsim.
clear Hsim1 Hsim2.
specialize (Hsim Fin.F1) as Hsim1.
specialize (Hsim (Fin.FS Fin.F1)) as Hsim2.
unfold cr_sim in Hsim1, Hsim2.
rewrite H10 in Hsim2. rewrite H2 in Hsim1.
apply cr_sim_cons in Hsim1, Hsim2.
destructH. destructH.
apply multi_step_split in Hsem1, Hsem2.
destruct Hsem1 as [Hsem1 Hsem1'].
destruct Hsem2 as [Hsem2 Hsem2'].
unfold multi_step_hd in Hsem1, Hsem2.
rewrite Hsim2, Hsim0 in *.
rewrite length_cons in *.
simpl in Hsem1', Hsem2'.
rewrite multi_step_S2 in Hsem1, Hsem2.
unfold multi_step_hd in Hsem1, Hsem2.
rewrite Hsem1' in Hsem1. rewrite Hsem2' in Hsem2.
simpl in Hsem1, Hsem2. clear Hsem1' Hsem2'.
unfold cr_sim' in Hsim4, Hsim3. subst.
rewrite H4 in Hsem1. rewrite H12 in Hsem2.
rewrite <- Hsem1, <- Hsem2.
rewrite H2 in *. rewrite H10 in *.
rewrite <- Hsem2 in H11.
rewrite <- Hsem1 in H3.
unfold sem_nonspec, nonspec_trace, multi_nonspec, multi_step' in Hsa1, Hsa2.
rewrite! length_cons in Hsa1, Hsa2.
rewrite multi_step_S2 in Hsa1, Hsa2.
inversion Hsa1. unfold multi_step_hd in H1. rewrite H7 in H1.
inversion Hsa2. unfold multi_step_hd in H8. rewrite H9 in H8.
rewrite <- H1 in H5. rewrite <- H8 in H13.
rewrite <- H1, <- H8 in Hsrc_ni.
destruct Hsrc_ni as [Hsrc_ni Hsrc_ni'].
unfold ll_eq in Hsrc_ni.
rewrite apply_lf'_S in Hsrc_ni.
rewrite Ha0 in Hsrc_ni.
rewrite! apply_lf'_S in Hsrc_ni.
rewrite app_inv_tail_iff in Hsrc_ni.
unfold compose in Hsrc_ni.
destruct s'. reflexivity.
unfold comp_relaxed' in *.
destruct s.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: simpl; reflexivity.
erewrite sim_same_leakage. 2: reflexivity. reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: simpl; destruct (alist_find decZ (eval_expr_fun a0 V) H); reflexivity.
erewrite sim_same_leakage. reflexivity. simpl. destruct (alist_find decZ (eval_expr_fun a0 V') H'); reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
2: simpl; destruct (alist_find _ x V); reflexivity.
erewrite sim_same_leakage. reflexivity.
simpl. destruct (alist_find _ x V'); reflexivity.
+ apply srcrel_tgtrel_If with (iv := iv) (p_src := p_src) (a := a) (al := al) (al0 := al0) (αs0 := αs0) (αs := αs) (b0 := b0) (β1 := β1) (βαl := βαl) (β3 := β3) (βαl0 := βαl0); assumption.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
cbv zeta in *.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)) eqn: Hdec. destruct (leak_lookahead sixteen s1) eqn: Hla.
* inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
* inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
* inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hdec. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hdec. reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: reflexivity.
erewrite sim_same_leakage. reflexivity. reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: reflexivity.
erewrite sim_same_leakage. reflexivity. reflexivity.
Qed.
(iv : Vector.t heap 2)
(p_src : list stmt)
(Hsrc_safe : forall a : Vector.t (list state) 2,
Vector.Forall2 (nonspec_trace p_src) iv a ->
v2 (ll_pre (rem_None ∘ leak_ct)) a)
(a : Vector.t (list state) 2)
(Ha : v2 srcrel a)
(α : Vector.t (list (list specstate)) 2)
(Hα : v2 (ll_eq (rem_None ∘ leak_ct')) α)
(Hsim : Vec_Forall3 (cr_sim p_src) iv a α)
(b : Vector.t (list state) 2)
(Hsem : Vector.Forall2 (sem_nonspec p_src) iv (veclist_app b a))
(β : Vector.t (list (list specstate)) 2)
(Hsem' : Vector.Forall2 (sem_spec_am (comp_relaxed' p_src)) iv
(veclist_app β α))
(Hsim' : Vec_Forall3 (cr_sim p_src) iv (veclist_app b a) (veclist_app β α))
(b0 : Vector.t state 2)
(bs : Vector.t (list state) 2)
(Hbeq : b = veclist_cons b0 bs)
(Hb0 : Vector.Forall (fun x : state => is_B x = true) b0)
(Hbs : Vector.Forall (Forall (fun s : state => is_B s = false)) bs):
v2 srcrel (veclist_app b a) ->
v2 (ll_eq (rem_None ∘ leak_ct')) (veclist_app β α).
Proof.
intros Hsrc_ni. unfold v2.
unfold ll_eq.
unfold v2, ll_eq in Hsrc_ni.
pose proof (vector_forall_nth _ _ _ Hbs Fin.F1) as Hbs1.
pose proof (vector_forall_nth _ _ _ Hbs (Fin.FS Fin.F1)) as Hbs2.
apply forall_not_isB_is_nil in Hbs1, Hbs2.
rewrite Hbeq in Hsim'.
rewrite vec_forall3_forall in Hsim'.
specialize (Hsim' Fin.F1) as Hsim1.
specialize (Hsim' (Fin.FS Fin.F1)) as Hsim2. clear Hsim' Hbs.
rewrite vl_cons_app in Hsim1, Hsim2.
rewrite veclist_cons_nth in Hsim1, Hsim2.
rewrite veclist_app_nth in Hsim1, Hsim2.
rewrite Hbs1 in Hsim1. rewrite Hbs2 in Hsim2.
rewrite app_nil_l in Hsim1, Hsim2.
rewrite! veclist_app_nth in *.
inversion Hsim1; inversion Hsim2; subst.
- destruct p_src.
+ unfold comp_relaxed'. simp comp_relaxed. cbn. reflexivity.
+ unfold comp_relaxed'. destruct s; simp comp_relaxed.
1-3, 6-7: reflexivity.
* cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)).
destruct (leak_lookahead sixteen s1).
all: rewrite! apply_lf'_S; do 5 f_equal.
* cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)).
destruct (leak_lookahead sixteen s1).
all: rewrite! apply_lf'_S; do 5 f_equal.
- clear - Ha H1 H6.
unfold v2, srcrel in Ha. destruct Ha as (_ & Ha).
rewrite <- H1, H6 in Ha. now simpl in Ha.
- clear - Ha H2 H9.
unfold v2, srcrel in Ha. destruct Ha as (_ & Ha).
rewrite H2, <- H9 in Ha. now simpl in Ha.
- assert (α0 = α[[Fin.F1]]) as ->.
{ eapply cr_sim_eq.
3: exact H6.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'. rewrite <- H1 in Hsem'.
apply multi_step_split in Hsem'. destructH.
exact Hsem'1.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'.
apply multi_step_split in Hsem'. destructH.
exact Hsem'1.
- rewrite vec_forall3_forall in Hsim. apply Hsim.
}
assert (α1 = α[[Fin.FS Fin.F1]]) as ->.
{ eapply cr_sim_eq.
3: eassumption.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'. rewrite <- H9 in Hsem'.
apply multi_step_split in Hsem'. destructH.
eassumption.
- eapply vec_forall2_nth in Hsem'.
rewrite veclist_app_nth in Hsem'.
eapply multi_step_split in Hsem'. destructH.
eassumption.
- rewrite vec_forall3_forall in Hsim. apply Hsim.
}
unfold v2, ll_eq in Hα.
rewrite! apply_lf'_app. rewrite Hα. f_equal.
rewrite app_inv_tail_iff in H1. subst.
rewrite app_inv_tail_iff in H9. subst.
unfold v2, srcrel in Ha.
rewrite H2, H10 in Ha.
destructH.
unfold prog_eq in Ha1.
destruct a1 as [ [V H] s].
destruct a3 as [ [V' H'] s'].
subst.
rewrite! veclist_cons_nth in Hsrc_ni.
rewrite Hbs1, Hbs2 in Hsrc_ni. simpl in Hsrc_ni.
rewrite Vec_Forall2_forall2 in Hsem.
specialize (Hsem Fin.F1) as Hsa1.
specialize (Hsem (Fin.FS Fin.F1)) as Hsa2.
rewrite veclist_app_nth in Hsa1, Hsa2.
rewrite veclist_cons_nth in Hsa1, Hsa2.
rewrite Hbs1 in Hsa1. rewrite Hbs2 in Hsa2.
simpl in Hsa1, Hsa2.
rewrite Vec_Forall2_forall2 in Hsem'.
specialize (Hsem' Fin.F1) as Hsem1.
specialize (Hsem' (Fin.FS Fin.F1)) as Hsem2.
rewrite veclist_app_nth in Hsem1, Hsem2.
rewrite vec_forall3_forall in Hsim.
clear Hsim1 Hsim2.
specialize (Hsim Fin.F1) as Hsim1.
specialize (Hsim (Fin.FS Fin.F1)) as Hsim2.
unfold cr_sim in Hsim1, Hsim2.
rewrite H10 in Hsim2. rewrite H2 in Hsim1.
apply cr_sim_cons in Hsim1, Hsim2.
destructH. destructH.
apply multi_step_split in Hsem1, Hsem2.
destruct Hsem1 as [Hsem1 Hsem1'].
destruct Hsem2 as [Hsem2 Hsem2'].
unfold multi_step_hd in Hsem1, Hsem2.
rewrite Hsim2, Hsim0 in *.
rewrite length_cons in *.
simpl in Hsem1', Hsem2'.
rewrite multi_step_S2 in Hsem1, Hsem2.
unfold multi_step_hd in Hsem1, Hsem2.
rewrite Hsem1' in Hsem1. rewrite Hsem2' in Hsem2.
simpl in Hsem1, Hsem2. clear Hsem1' Hsem2'.
unfold cr_sim' in Hsim4, Hsim3. subst.
rewrite H4 in Hsem1. rewrite H12 in Hsem2.
rewrite <- Hsem1, <- Hsem2.
rewrite H2 in *. rewrite H10 in *.
rewrite <- Hsem2 in H11.
rewrite <- Hsem1 in H3.
unfold sem_nonspec, nonspec_trace, multi_nonspec, multi_step' in Hsa1, Hsa2.
rewrite! length_cons in Hsa1, Hsa2.
rewrite multi_step_S2 in Hsa1, Hsa2.
inversion Hsa1. unfold multi_step_hd in H1. rewrite H7 in H1.
inversion Hsa2. unfold multi_step_hd in H8. rewrite H9 in H8.
rewrite <- H1 in H5. rewrite <- H8 in H13.
rewrite <- H1, <- H8 in Hsrc_ni.
destruct Hsrc_ni as [Hsrc_ni Hsrc_ni'].
unfold ll_eq in Hsrc_ni.
rewrite apply_lf'_S in Hsrc_ni.
rewrite Ha0 in Hsrc_ni.
rewrite! apply_lf'_S in Hsrc_ni.
rewrite app_inv_tail_iff in Hsrc_ni.
unfold compose in Hsrc_ni.
destruct s'. reflexivity.
unfold comp_relaxed' in *.
destruct s.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: simpl; reflexivity.
erewrite sim_same_leakage. 2: reflexivity. reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: simpl; destruct (alist_find decZ (eval_expr_fun a0 V) H); reflexivity.
erewrite sim_same_leakage. reflexivity. simpl. destruct (alist_find decZ (eval_expr_fun a0 V') H'); reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
2: simpl; destruct (alist_find _ x V); reflexivity.
erewrite sim_same_leakage. reflexivity.
simpl. destruct (alist_find _ x V'); reflexivity.
+ apply srcrel_tgtrel_If with (iv := iv) (p_src := p_src) (a := a) (al := al) (al0 := al0) (αs0 := αs0) (αs := αs) (b0 := b0) (β1 := β1) (βαl := βαl) (β3 := β3) (βαl0 := βαl0); assumption.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
cbv zeta in *.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)) eqn: Hdec. destruct (leak_lookahead sixteen s1) eqn: Hla.
* inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
* inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hla. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hla, Hdec. reflexivity.
* inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni.
erewrite sim_same_leakage. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hdec. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite Hdec. rewrite comp_relaxed_app.
simp comp_relaxed. cbv zeta. rewrite Hdec. reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: reflexivity.
erewrite sim_same_leakage. reflexivity. reflexivity.
+ simpl. simp comp_relaxed. cbn in H3, H11. simp comp_relaxed in H3, H11.
inversion H3. inversion H11. subst.
unfold compose. rewrite! apply_lf'_S.
f_equal.
erewrite <- sim_same_leakage. rewrite Hsrc_ni. 2: reflexivity.
erewrite sim_same_leakage. reflexivity. reflexivity.
Qed.
comp_relaxed Preserves Constant-Time Leakage Equivalence
Theorem relaxed_preserve_ct
(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_ct)) a) (*assume termination-insensitive leakage equivalence*)
: forall α, Vector.Forall2 (spec_am_trace (comp_relaxed' p_src)) iv α -> v2 (ll_pre_sens (rem_None ∘ leak_ct') spec_am_trace (comp_relaxed' p_src) iv) α. (*prove termination-sensitive leakage equivalence*)
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.
eapply hpbc_hpb2 with (tgt_sem := sem_spec_am (comp_relaxed' p_src)) (src_rel := v2 srcrel) in Hterm.
- destructH.
eapply hyper_preserve_tgt_safe with (α:=α).
+ 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 preserved by target relation*)
+ eapply Hα.
- exact (nil, nil, nil). (*type is inhabited*)
- exact state_dec.
- econstructor.
+ unfold v2, srcrel. (*intial empty traces are related by all three relations*)
split.
* eapply vl_ll_eq_zero.
* reflexivity.
+ eapply vl_ll_eq_zero.
+ eapply (cr_sim_nil p_src).
+ clear α Hα. (*hyperstep*)
intros a Ha α Hα Hsim b Hsem β Hsem' Hsim' b0 bs Hbeq Hb0 Hbs.
match goal with
|- ?x /\ ?y => let Q := fresh "Q" in enough (x /\ (x -> y)) as Q
end.
{ clear - Q. destruct Q. specialize (H0 H). easy. }
split.
* eapply srcrel_step; eauto.
* eapply srcrel_impl_tgtrel; eauto.
+ eapply cr_sim_sync_correct.
Unshelve.
1: apply nonspec_trace_linear_semantics.
1: apply spec_am_trace_linear_semantics.
2: apply (tsync_cr 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_ct)) a) (*assume termination-insensitive leakage equivalence*)
: forall α, Vector.Forall2 (spec_am_trace (comp_relaxed' p_src)) iv α -> v2 (ll_pre_sens (rem_None ∘ leak_ct') spec_am_trace (comp_relaxed' p_src) iv) α. (*prove termination-sensitive leakage equivalence*)
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.
eapply hpbc_hpb2 with (tgt_sem := sem_spec_am (comp_relaxed' p_src)) (src_rel := v2 srcrel) in Hterm.
- destructH.
eapply hyper_preserve_tgt_safe with (α:=α).
+ 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 preserved by target relation*)
+ eapply Hα.
- exact (nil, nil, nil). (*type is inhabited*)
- exact state_dec.
- econstructor.
+ unfold v2, srcrel. (*intial empty traces are related by all three relations*)
split.
* eapply vl_ll_eq_zero.
* reflexivity.
+ eapply vl_ll_eq_zero.
+ eapply (cr_sim_nil p_src).
+ clear α Hα. (*hyperstep*)
intros a Ha α Hα Hsim b Hsem β Hsem' Hsim' b0 bs Hbeq Hb0 Hbs.
match goal with
|- ?x /\ ?y => let Q := fresh "Q" in enough (x /\ (x -> y)) as Q
end.
{ clear - Q. destruct Q. specialize (H0 H). easy. }
split.
* eapply srcrel_step; eauto.
* eapply srcrel_impl_tgtrel; eauto.
+ eapply cr_sim_sync_correct.
Unshelve.
1: apply nonspec_trace_linear_semantics.
1: apply spec_am_trace_linear_semantics.
2: apply (tsync_cr p_src).
Qed.
The 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)