HypreSpectre.Mitigation
From HypreSpectre Require Import Lang.
From HyPre Require Import Sync StateSimulation.
From Equations Require Import Equations.
From HyPre Require Import Sync StateSimulation.
From Equations Require Import Equations.
Equations? comp_fence sl : list stmt by wf (stmt_depth_list sl) :=
comp_fence nil := nil;
comp_fence ((Assign x e) :: l) := Assign x e :: (comp_fence l);
comp_fence ((Read x e) :: l) := Read x e :: (comp_fence l);
comp_fence ((Write x e) :: l) := Write x e :: (comp_fence l);
comp_fence ((If i t e) :: l) := If i (Fence :: (comp_fence t)) (Fence :: (comp_fence e)) :: (comp_fence l);
comp_fence ((While e s1 s2) :: l) := While e (Fence :: (comp_fence s1)) (Fence :: (comp_fence s2)) :: (comp_fence l);
comp_fence ((Skip) :: l) := Skip :: (comp_fence l);
comp_fence ((Fence) :: l) := Fence :: (comp_fence l).
Proof.
all: 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, 4, 6, 8, 10, 12: reflexivity.
all: lia.
Qed.
comp_fence nil := nil;
comp_fence ((Assign x e) :: l) := Assign x e :: (comp_fence l);
comp_fence ((Read x e) :: l) := Read x e :: (comp_fence l);
comp_fence ((Write x e) :: l) := Write x e :: (comp_fence l);
comp_fence ((If i t e) :: l) := If i (Fence :: (comp_fence t)) (Fence :: (comp_fence e)) :: (comp_fence l);
comp_fence ((While e s1 s2) :: l) := While e (Fence :: (comp_fence s1)) (Fence :: (comp_fence s2)) :: (comp_fence l);
comp_fence ((Skip) :: l) := Skip :: (comp_fence l);
comp_fence ((Fence) :: l) := Fence :: (comp_fence l).
Proof.
all: 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, 4, 6, 8, 10, 12: reflexivity.
all: lia.
Qed.
The simulation relation always relates a program in an environment to the compiled program in the same environment.
Definition cf_sim' (p1 : state) (p2 : list specstate) := match p1 with
| (V, H, l) => p2 = (None, V, H, (comp_fence l)) :: nil
end.
| (V, H, l) => p2 = (None, V, H, (comp_fence l)) :: nil
end.
The synchronizer takes 4 steps for If statements, and one otherwise.
Definition cf_sim_step (p : state) := match p with
| (V, H, s :: l) => (fix F s := match s with
| If _ _ _ => 4
| _ => 1
end) s
| _ => 1
end.
| (V, H, s :: l) => (fix F s := match s with
| If _ _ _ => 4
| _ => 1
end) s
| _ => 1
end.
We lift the synchronizer from individual states to trace prefixes.
Definition cf_sim_sync (p_src : list stmt) :=
lift_tsync nonspec_step_fun (fun i => (nil, i, p_src)) cf_sim_step.
Lemma tsync_gt_0 {SrcSt} n (step_fun: SrcSt -> SrcSt) sim_step:
(forall i, sim_step i > 0) ->
forall i, lift_tsync' step_fun sim_step i n > 0.
Proof.
intros Hstep.
induction n.
- intros i. simpl. eapply Hstep.
- intros i. simpl. eapply IHn.
Qed.
lift_tsync nonspec_step_fun (fun i => (nil, i, p_src)) cf_sim_step.
Lemma tsync_gt_0 {SrcSt} n (step_fun: SrcSt -> SrcSt) sim_step:
(forall i, sim_step i > 0) ->
forall i, lift_tsync' step_fun sim_step i n > 0.
Proof.
intros Hstep.
induction n.
- intros i. simpl. eapply Hstep.
- intros i. simpl. eapply IHn.
Qed.
The synchronizer is indeed a proper synchronizer.
For synchronizers that allow target traces to stutter, i.e. not take a step when the source trace takes one, then the second function specifies how often this can at most happen.
We need to prove that this is correct, i.e. that the target trace will have taken more steps after this limit is exceeded.
Our synchronizer does not allow stuttering, so the second function always returns 1, and the proof boils down to proving that cf_sim_step is always greater than 0.
Lemma tsync_cf p_src i:
TotalSynchroniser (cf_sim_sync p_src i) (fun _ => 1).
Proof.
econstructor.
intros.
induction n.
- cbn. lia.
- replace (S n + 1) with (S (S n)) by lia.
do 3 rewrite iter_S.
pattern (let (n0, m) := Init.Nat.iter n (fun nm : nat * nat => let (n0, m) := nm in (S n0, cf_sim_sync p_src i n0 + m)) (0, 0) in (S n0, cf_sim_sync p_src i n0 + m)).
enough (forall p, snd p < snd (let (n0, m) := p in (S n0, cf_sim_sync p_src i n0 + m)) ) by apply H.
destruct p. cbn.
enough (forall n0, cf_sim_sync p_src i n0 > 0).
+ specialize (H n0). lia.
+ intros.
unfold cf_sim_sync.
induction n2.
* unfold lift_tsync. lia.
* unfold lift_tsync. unfold lift_tsync in IHn2.
eapply tsync_gt_0.
clear.
intros [ [V H] p].
unfold cf_sim_step. destruct p. lia. destruct s; lia.
Qed.
TotalSynchroniser (cf_sim_sync p_src i) (fun _ => 1).
Proof.
econstructor.
intros.
induction n.
- cbn. lia.
- replace (S n + 1) with (S (S n)) by lia.
do 3 rewrite iter_S.
pattern (let (n0, m) := Init.Nat.iter n (fun nm : nat * nat => let (n0, m) := nm in (S n0, cf_sim_sync p_src i n0 + m)) (0, 0) in (S n0, cf_sim_sync p_src i n0 + m)).
enough (forall p, snd p < snd (let (n0, m) := p in (S n0, cf_sim_sync p_src i n0 + m)) ) by apply H.
destruct p. cbn.
enough (forall n0, cf_sim_sync p_src i n0 > 0).
+ specialize (H n0). lia.
+ intros.
unfold cf_sim_sync.
induction n2.
* unfold lift_tsync. lia.
* unfold lift_tsync. unfold lift_tsync in IHn2.
eapply tsync_gt_0.
clear.
intros [ [V H] p].
unfold cf_sim_step. destruct p. lia. destruct s; lia.
Qed.
We lift the relation to trace prefixes according to the synchronizer.
Definition cf_sim p : heap -> list state -> list (list specstate) -> Prop := lift_state_rel cf_sim' (fun i => (nil, i, p)) (fun i => (None, nil, i, comp_fence p) :: nil) cf_sim_step.
The relation relates empty traces (due to lift_state_rel). This is needed for hyper-simulations.
Lemma cf_sim_nil p i:
cf_sim p i nil nil.
Proof.
unfold cf_sim.
econstructor.
Qed.
Lemma trace_head_iter p_src i s sl:
nonspec_trace p_src i (s::sl) -> Nat.iter (|sl|) nonspec_step_fun (nil, i, p_src) = s.
Proof.
revert s.
induction sl.
- cbn. intros. inversion H. reflexivity.
- intros.
rewrite length_cons. cbn.
specialize (IHsl a).
unfold nonspec_trace in H.
unfold multi_nonspec, multi_step' in H.
rewrite! length_cons in H.
unfold Nat.iter in IHsl.
rewrite multi_step_S2 in H.
inversion H.
rewrite H1.
specialize (IHsl H2).
rewrite IHsl.
unfold multi_step_hd in H1. rewrite H2 in H1. cbn in H1.
exact H1.
Qed.
Lemma comp_fence_app a b:
comp_fence (a ++ b) = comp_fence a ++ comp_fence b.
Proof.
induction a.
- simp comp_fence. reflexivity.
- rewrite <- app_comm_cons.
destruct a; simp comp_fence; rewrite IHa; rewrite app_comm_cons; reflexivity.
Qed.
cf_sim p i nil nil.
Proof.
unfold cf_sim.
econstructor.
Qed.
Lemma trace_head_iter p_src i s sl:
nonspec_trace p_src i (s::sl) -> Nat.iter (|sl|) nonspec_step_fun (nil, i, p_src) = s.
Proof.
revert s.
induction sl.
- cbn. intros. inversion H. reflexivity.
- intros.
rewrite length_cons. cbn.
specialize (IHsl a).
unfold nonspec_trace in H.
unfold multi_nonspec, multi_step' in H.
rewrite! length_cons in H.
unfold Nat.iter in IHsl.
rewrite multi_step_S2 in H.
inversion H.
rewrite H1.
specialize (IHsl H2).
rewrite IHsl.
unfold multi_step_hd in H1. rewrite H2 in H1. cbn in H1.
exact H1.
Qed.
Lemma comp_fence_app a b:
comp_fence (a ++ b) = comp_fence a ++ comp_fence b.
Proof.
induction a.
- simp comp_fence. reflexivity.
- rewrite <- app_comm_cons.
destruct a; simp comp_fence; rewrite IHa; rewrite app_comm_cons; reflexivity.
Qed.
The simulation relation is correct w.r.t. the synchronizer, i.e. we always end up in related states again:
Lemma cf_sim_sync_correct p_src (i : heap) (a : list state) (α0 : list (list specstate))
(b : state) (β : list (list specstate)):
cf_sim p_src i a α0 ->
nonspec_trace p_src i (b :: a) ->
spec_am_trace (comp_fence p_src) i (β ++ α0) ->
cf_sim_sync p_src i (| a |) = | β | -> cf_sim p_src i (b :: a) (β ++ α0).
Proof.
intros.
unfold cf_sim.
eapply prove_trace_by_tsync.
1-2: auto.
4: exact H0.
4: exact H1.
- simpl. reflexivity.
- intros.
unfold cf_sim' in H3.
destruct a0 as [ [V HH] s]. rewrite H3.
destruct s.
+ simpl. unfold multi_step_hd. simpl. simp comp_fence. reflexivity.
+ destruct s; simpl; unfold multi_step_hd; simp comp_fence; try reflexivity.
* simpl. destruct (alist_find decZ (eval_expr_fun a0 V) HH); easy.
* simpl. destruct (alist_find _ x V); easy.
* simpl. destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; now rewrite comp_fence_app.
* simpl. do 5 f_equal. rewrite comp_fence_app. simp comp_fence. reflexivity.
- exact H.
- exact H2.
Qed.
(b : state) (β : list (list specstate)):
cf_sim p_src i a α0 ->
nonspec_trace p_src i (b :: a) ->
spec_am_trace (comp_fence p_src) i (β ++ α0) ->
cf_sim_sync p_src i (| a |) = | β | -> cf_sim p_src i (b :: a) (β ++ α0).
Proof.
intros.
unfold cf_sim.
eapply prove_trace_by_tsync.
1-2: auto.
4: exact H0.
4: exact H1.
- simpl. reflexivity.
- intros.
unfold cf_sim' in H3.
destruct a0 as [ [V HH] s]. rewrite H3.
destruct s.
+ simpl. unfold multi_step_hd. simpl. simp comp_fence. reflexivity.
+ destruct s; simpl; unfold multi_step_hd; simp comp_fence; try reflexivity.
* simpl. destruct (alist_find decZ (eval_expr_fun a0 V) HH); easy.
* simpl. destruct (alist_find _ x V); easy.
* simpl. destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; now rewrite comp_fence_app.
* simpl. do 5 f_equal. rewrite comp_fence_app. simp comp_fence. reflexivity.
- exact H.
- exact H2.
Qed.
Relaxed Insertion of Fences
Inductive syntObs :=
| ReadExp (e : expr) (v : var) (*We need to know which value was read, to make sure any changes to the environment are the same in both branches*)
| WriteExp (e : expr) (v : var).
| ReadExp (e : expr) (v : var) (*We need to know which value was read, to make sure any changes to the environment are the same in both branches*)
| WriteExp (e : expr) (v : var).
This function determines what leakages will be encountered in a branch.
If it encounters any situation in which we have to place fences anyway, it returns None.
Fixpoint leak_lookahead (n : nat) (sl : list stmt) : option (list syntObs) :=
match n with
| 0 => Some nil
| S n' => match sl with
| nil => None (*branch is too short. without this restriction, comp_relaxed_app would not hold.*)
| s :: l => match s with
| Fence => None (*would require more complex handling to determine how long speculative execution lasts*)
| If _ _ _ => None (*nested speculation would cause problems*)
| While _ _ _ => None
| Assign _ _ => None (*tracking changes to the environment would be much more difficult*)
| Read x e => match leak_lookahead n' l with
| None => None
| Some l => Some (ReadExp e x:: l)
end
| Write x e => match leak_lookahead n' l with
| None => None
| Some l => Some (WriteExp e x :: l)
end
| _ => leak_lookahead n' l
end
end
end.
match n with
| 0 => Some nil
| S n' => match sl with
| nil => None (*branch is too short. without this restriction, comp_relaxed_app would not hold.*)
| s :: l => match s with
| Fence => None (*would require more complex handling to determine how long speculative execution lasts*)
| If _ _ _ => None (*nested speculation would cause problems*)
| While _ _ _ => None
| Assign _ _ => None (*tracking changes to the environment would be much more difficult*)
| Read x e => match leak_lookahead n' l with
| None => None
| Some l => Some (ReadExp e x:: l)
end
| Write x e => match leak_lookahead n' l with
| None => None
| Some l => Some (WriteExp e x :: l)
end
| _ => leak_lookahead n' l
end
end
end.
Our mitigation needs to be able to decide when the produced sequences are the same:
Definition dec_syntObs : forall (a b : syntObs), {a = b} + {a <> b}.
Proof.
intros.
destruct a, b.
- destruct (dec_expr e e0).
+ destruct (string_eqdec v v0).
* left. now rewrite e1, e2.
* right. now inversion 1.
+ right. now inversion 1.
- now right.
- now right.
- destruct (dec_expr e e0).
+ destruct (string_eqdec v v0).
* left. now rewrite e1, e2.
* right. now inversion 1.
+ right. now inversion 1.
Defined.
Definition dec_syntObsL : forall (a b : option (list syntObs)), {a = b} + {a <> b}.
Proof.
intros.
destruct a as [a |], b as [b |].
* induction a in b |-*; destruct b.
- now left.
- now right.
- now right.
- specialize (IHa b).
destruct IHa.
+ inversion e.
destruct (dec_syntObs a s).
++ left. now rewrite e0.
++ right. now inversion 1.
+ right. inversion 1. apply n. now rewrite H2.
* now right.
* now right.
* now left.
Defined.
Proof.
intros.
destruct a, b.
- destruct (dec_expr e e0).
+ destruct (string_eqdec v v0).
* left. now rewrite e1, e2.
* right. now inversion 1.
+ right. now inversion 1.
- now right.
- now right.
- destruct (dec_expr e e0).
+ destruct (string_eqdec v v0).
* left. now rewrite e1, e2.
* right. now inversion 1.
+ right. now inversion 1.
Defined.
Definition dec_syntObsL : forall (a b : option (list syntObs)), {a = b} + {a <> b}.
Proof.
intros.
destruct a as [a |], b as [b |].
* induction a in b |-*; destruct b.
- now left.
- now right.
- now right.
- specialize (IHa b).
destruct IHa.
+ inversion e.
destruct (dec_syntObs a s).
++ left. now rewrite e0.
++ right. now inversion 1.
+ right. inversion 1. apply n. now rewrite H2.
* now right.
* now right.
* now left.
Defined.
We define the mitigation in a section, to obscure the constant 16 (which becomes a parameter). Otherwise, various tactics would unfold to eagerly and slow Coq down too much.
Section with_16.
Context (lahead : nat).
Equations? comp_relaxed sl : list stmt by wf (stmt_depth_list sl) :=
comp_relaxed nil := nil;
comp_relaxed ((Assign x e) :: l) := Assign x e :: (comp_relaxed l);
comp_relaxed ((Read x e) :: l) := Read x e :: (comp_relaxed l);
comp_relaxed ((Write x e) :: l) := Write x e :: (comp_relaxed l);
comp_relaxed ((If i t e) :: l) :=
let l1 := leak_lookahead lahead t in
let l2 := leak_lookahead lahead e in
if (dec_syntObsL l1 l2) then match l1 with
| None => If i (Fence :: (comp_relaxed t)) (Fence :: (comp_relaxed e)) :: comp_relaxed l
|Some _ => (If i (comp_relaxed t) (comp_relaxed e)) :: (comp_relaxed l)
end
else If i (Fence :: (comp_relaxed t)) (Fence :: (comp_relaxed e)) :: (comp_relaxed l);
comp_relaxed ((While e s1 s2) :: l) :=
let l1 := leak_lookahead lahead s1 in
let l2 := leak_lookahead lahead s2 in
if (dec_syntObsL l1 l2) then match l1 with
| None => While e (Fence :: (comp_relaxed s1)) (Fence :: (comp_relaxed s2)) :: (comp_relaxed l)
| Some _ => (While e (comp_relaxed s1) (comp_relaxed s2)) :: (comp_relaxed l)
end
else While e (Fence :: (comp_relaxed s1)) (Fence :: (comp_relaxed s2)) :: (comp_relaxed l);
comp_relaxed ((Skip) :: l) := Skip :: (comp_relaxed l);
comp_relaxed ((Fence) :: l) := Fence :: (comp_relaxed l).
Proof.
all: 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).
all: try reflexivity.
all: lia.
Qed.
End with_16.
Definition eighteen := 18.
Definition seventeen := 17.
Definition sixteen := 16.
Definition fifteen := 15.
Definition four := 4.
Ltac lia_fs := unfold fifteen,sixteen,eighteen; lia.
Context (lahead : nat).
Equations? comp_relaxed sl : list stmt by wf (stmt_depth_list sl) :=
comp_relaxed nil := nil;
comp_relaxed ((Assign x e) :: l) := Assign x e :: (comp_relaxed l);
comp_relaxed ((Read x e) :: l) := Read x e :: (comp_relaxed l);
comp_relaxed ((Write x e) :: l) := Write x e :: (comp_relaxed l);
comp_relaxed ((If i t e) :: l) :=
let l1 := leak_lookahead lahead t in
let l2 := leak_lookahead lahead e in
if (dec_syntObsL l1 l2) then match l1 with
| None => If i (Fence :: (comp_relaxed t)) (Fence :: (comp_relaxed e)) :: comp_relaxed l
|Some _ => (If i (comp_relaxed t) (comp_relaxed e)) :: (comp_relaxed l)
end
else If i (Fence :: (comp_relaxed t)) (Fence :: (comp_relaxed e)) :: (comp_relaxed l);
comp_relaxed ((While e s1 s2) :: l) :=
let l1 := leak_lookahead lahead s1 in
let l2 := leak_lookahead lahead s2 in
if (dec_syntObsL l1 l2) then match l1 with
| None => While e (Fence :: (comp_relaxed s1)) (Fence :: (comp_relaxed s2)) :: (comp_relaxed l)
| Some _ => (While e (comp_relaxed s1) (comp_relaxed s2)) :: (comp_relaxed l)
end
else While e (Fence :: (comp_relaxed s1)) (Fence :: (comp_relaxed s2)) :: (comp_relaxed l);
comp_relaxed ((Skip) :: l) := Skip :: (comp_relaxed l);
comp_relaxed ((Fence) :: l) := Fence :: (comp_relaxed l).
Proof.
all: 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).
all: try reflexivity.
all: lia.
Qed.
End with_16.
Definition eighteen := 18.
Definition seventeen := 17.
Definition sixteen := 16.
Definition fifteen := 15.
Definition four := 4.
Ltac lia_fs := unfold fifteen,sixteen,eighteen; lia.
We only ever use it with 16.
The simulation relation again relates programs in environments to the compiled program in the same environment.
Definition cr_sim' (p1 : state) (p2 : list specstate) := match p1 with
| (V, H, l) => p2 = (None, V, H, (comp_relaxed' l)) :: nil
end.
| (V, H, l) => p2 = (None, V, H, (comp_relaxed' l)) :: nil
end.
The synchronizer performs the same checks as the compilation function
Definition cr_sim_step (p : state) := match p with
| ( _, s :: l) => match s with
| If i t e => let l1 := leak_lookahead sixteen t in
let l2 := leak_lookahead sixteen e in
if (dec_syntObsL l1 l2) then match l1 with
| None => 4
| Some _ => eighteen
end
else 4
| _ => 1
end
| _ => 1
end.
Lemma cr_sim_step_unfold p (l : list stmt)
: cr_sim_step (p,l) = match l with
| s :: l => match s with
| If i t e => let l1 := leak_lookahead sixteen t in
let l2 := leak_lookahead sixteen e in
if (dec_syntObsL l1 l2) then match l1 with
| None => 4
| Some _ => eighteen
end
else 4
| _ => 1
end
| _ => 1
end.
Proof.
reflexivity.
Qed.
| ( _, s :: l) => match s with
| If i t e => let l1 := leak_lookahead sixteen t in
let l2 := leak_lookahead sixteen e in
if (dec_syntObsL l1 l2) then match l1 with
| None => 4
| Some _ => eighteen
end
else 4
| _ => 1
end
| _ => 1
end.
Lemma cr_sim_step_unfold p (l : list stmt)
: cr_sim_step (p,l) = match l with
| s :: l => match s with
| If i t e => let l1 := leak_lookahead sixteen t in
let l2 := leak_lookahead sixteen e in
if (dec_syntObsL l1 l2) then match l1 with
| None => 4
| Some _ => eighteen
end
else 4
| _ => 1
end
| _ => 1
end.
Proof.
reflexivity.
Qed.
We lift the synchronizer from individual states to trace prefixes.
Definition cr_sim_sync (p_src : list stmt) :=
lift_tsync nonspec_step_fun (fun i => (nil, i, p_src)) cr_sim_step.
lift_tsync nonspec_step_fun (fun i => (nil, i, p_src)) cr_sim_step.
Our synchronizer is a proper synchronizer.
Again, our target traces never stutter, so the second function is always 1.
Lemma tsync_cr p_src i:
TotalSynchroniser (cr_sim_sync p_src i) (fun _ => 1).
Proof.
econstructor.
intros.
induction n.
- cbn. lia.
- replace (S n + 1) with (S (S n)) by lia.
do 3 rewrite iter_S.
pattern (let (n0, m) := Init.Nat.iter n (fun nm : nat * nat => let (n0, m) := nm in (S n0, cf_sim_sync p_src i n0 + m)) (0, 0) in (S n0, cf_sim_sync p_src i n0 + m)).
enough (forall p, snd p < snd (let (n0, m) := p in (S n0, cr_sim_sync p_src i n0 + m)) ) by apply H.
destruct p. cbn.
enough (forall n0, cr_sim_sync p_src i n0 > 0).
+ specialize (H n0). lia.
+ intros.
unfold cr_sim_sync.
induction n2.
* unfold lift_tsync. lia.
* unfold lift_tsync.
eapply tsync_gt_0.
clear.
intros [ [V H] p]. unfold cr_sim_step.
destruct p. lia.
destruct s; try lia.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: lia.
destruct (leak_lookahead sixteen s1). unfold eighteen. lia. lia.
Qed.
TotalSynchroniser (cr_sim_sync p_src i) (fun _ => 1).
Proof.
econstructor.
intros.
induction n.
- cbn. lia.
- replace (S n + 1) with (S (S n)) by lia.
do 3 rewrite iter_S.
pattern (let (n0, m) := Init.Nat.iter n (fun nm : nat * nat => let (n0, m) := nm in (S n0, cf_sim_sync p_src i n0 + m)) (0, 0) in (S n0, cf_sim_sync p_src i n0 + m)).
enough (forall p, snd p < snd (let (n0, m) := p in (S n0, cr_sim_sync p_src i n0 + m)) ) by apply H.
destruct p. cbn.
enough (forall n0, cr_sim_sync p_src i n0 > 0).
+ specialize (H n0). lia.
+ intros.
unfold cr_sim_sync.
induction n2.
* unfold lift_tsync. lia.
* unfold lift_tsync.
eapply tsync_gt_0.
clear.
intros [ [V H] p]. unfold cr_sim_step.
destruct p. lia.
destruct s; try lia.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)). 2: lia.
destruct (leak_lookahead sixteen s1). unfold eighteen. lia. lia.
Qed.
We lift the simulation relation to traces.
Definition cr_sim p : heap -> list state -> list (list specstate) -> Prop := lift_state_rel cr_sim' (fun i => (nil, i, p)) (fun i => (None, nil, i, comp_relaxed' p) :: nil) cr_sim_step.
Empty trace prefixes are related.
Lemma cr_sim_nil p i:
cr_sim p i nil nil.
Proof.
unfold cr_sim.
econstructor.
Qed.
Lemma comp_relaxed_app a b:
comp_relaxed sixteen (a ++ b) = comp_relaxed sixteen a ++ comp_relaxed sixteen b.
Proof.
induction a.
- simp comp_relaxed. reflexivity.
- rewrite <- app_comm_cons.
destruct a; simp comp_relaxed; rewrite IHa; try (rewrite app_comm_cons; reflexivity).
+ cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen (s1)) (leak_lookahead sixteen (s2))).
2: rewrite app_comm_cons; reflexivity.
destruct (leak_lookahead sixteen s1); rewrite app_comm_cons; reflexivity.
+ cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)).
2: rewrite app_comm_cons; reflexivity.
destruct (leak_lookahead sixteen s1); rewrite app_comm_cons; reflexivity.
Qed.
Lemma leak_la_extend a b l:
forall n, leak_lookahead n a = Some l -> leak_lookahead n (a ++ b) = Some l.
Proof.
intros.
induction a in l, n, H |-*.
- destruct n; cbn in H. 2: congruence. exact H.
- destruct n.
+ cbn. cbn in H. exact H.
+ cbn in H |-*.
destruct (leak_lookahead n a0) eqn: Hl.
* specialize (IHa _ _ Hl).
rewrite IHa. exact H.
* destruct a; congruence.
Qed.
Lemma leak_la_extend' a b l:
forall n, Some l = leak_lookahead n a -> Some l = leak_lookahead n (a ++ b).
Proof.
intros. symmetry in H. symmetry.
now apply leak_la_extend.
Qed.
Lemma noleak_extend a c s1 s2:
forall n, leak_lookahead n a = None -> leak_lookahead n (a :r: While c s1 s2) = None.
Proof.
intros.
induction a in n, H |-*.
- destruct n; cbn in *. congruence. reflexivity.
- destruct n.
+ cbn in H. congruence.
+ cbn in *.
destruct (leak_lookahead n a0) eqn: Hl.
* destruct a; congruence.
* now specialize (IHa _ Hl) as ->.
Qed.
cr_sim p i nil nil.
Proof.
unfold cr_sim.
econstructor.
Qed.
Lemma comp_relaxed_app a b:
comp_relaxed sixteen (a ++ b) = comp_relaxed sixteen a ++ comp_relaxed sixteen b.
Proof.
induction a.
- simp comp_relaxed. reflexivity.
- rewrite <- app_comm_cons.
destruct a; simp comp_relaxed; rewrite IHa; try (rewrite app_comm_cons; reflexivity).
+ cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen (s1)) (leak_lookahead sixteen (s2))).
2: rewrite app_comm_cons; reflexivity.
destruct (leak_lookahead sixteen s1); rewrite app_comm_cons; reflexivity.
+ cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen s1) (leak_lookahead sixteen s2)).
2: rewrite app_comm_cons; reflexivity.
destruct (leak_lookahead sixteen s1); rewrite app_comm_cons; reflexivity.
Qed.
Lemma leak_la_extend a b l:
forall n, leak_lookahead n a = Some l -> leak_lookahead n (a ++ b) = Some l.
Proof.
intros.
induction a in l, n, H |-*.
- destruct n; cbn in H. 2: congruence. exact H.
- destruct n.
+ cbn. cbn in H. exact H.
+ cbn in H |-*.
destruct (leak_lookahead n a0) eqn: Hl.
* specialize (IHa _ _ Hl).
rewrite IHa. exact H.
* destruct a; congruence.
Qed.
Lemma leak_la_extend' a b l:
forall n, Some l = leak_lookahead n a -> Some l = leak_lookahead n (a ++ b).
Proof.
intros. symmetry in H. symmetry.
now apply leak_la_extend.
Qed.
Lemma noleak_extend a c s1 s2:
forall n, leak_lookahead n a = None -> leak_lookahead n (a :r: While c s1 s2) = None.
Proof.
intros.
induction a in n, H |-*.
- destruct n; cbn in *. congruence. reflexivity.
- destruct n.
+ cbn in H. congruence.
+ cbn in *.
destruct (leak_lookahead n a0) eqn: Hl.
* destruct a; congruence.
* now specialize (IHa _ Hl) as ->.
Qed.
leak_lookahead is unaffected by appending a While statement. This is necessary for our simulation to still be correct when a While statement is translated to an If during execution.
Lemma leak_extend a c s1 s2:
forall n, leak_lookahead n a = leak_lookahead n (a :r: While c s1 s2).
Proof.
intros.
destruct (leak_lookahead n a) eqn: H.
- symmetry. now apply leak_la_extend.
- symmetry. now apply noleak_extend.
Qed.
Lemma match_all_none x:
match x with
| Assign _ _
| _ => None
end = @None (list syntObs).
Proof.
destruct x; reflexivity.
Qed.
forall n, leak_lookahead n a = leak_lookahead n (a :r: While c s1 s2).
Proof.
intros.
destruct (leak_lookahead n a) eqn: H.
- symmetry. now apply leak_la_extend.
- symmetry. now apply noleak_extend.
Qed.
Lemma match_all_none x:
match x with
| Assign _ _
| _ => None
end = @None (list syntObs).
Proof.
destruct x; reflexivity.
Qed.
Lemma spec_x_steps x s1 l V H a b
(Hl: leak_lookahead x s1 = Some l):
multi_step_hd spec_step_fun ((Some x, V, H, (comp_relaxed sixteen s1) ++ a) :: b :: nil) (S x) = b :: nil.
Proof.
induction x in s1, l, Hl, V, H|-*.
- cbn. reflexivity.
- unfold multi_step_hd. cbn.
destruct s1. cbn in Hl. congruence.
cbn in Hl.
destruct s; try congruence.
+ destruct (leak_lookahead x s1) eqn: Hl'.
* simp comp_relaxed.
rewrite <- app_comm_cons.
destruct (alist_find decZ (eval_expr_fun a0 V) H).
-- unfold multi_step_hd in IHx.
assert (x - 0 = x) as -> by lia.
specialize (IHx _ _ (alist_add _ x0 v V) H Hl').
destruct (multi_step spec_step_fun ((Some x, alist_add RelDec_string x0 v V, H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
fold var in *. fold varmap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
fold var in *. fold varmap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl. simpl in IHx. assumption.
-- unfold multi_step_hd in IHx.
assert (x - 0 = x) as -> by lia.
specialize (IHx _ _ (alist_add _ x0 0%Z V) H Hl').
destruct (multi_step spec_step_fun ((Some x, alist_add RelDec_string x0 0%Z V, H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
fold value in *. fold var in *. fold varmap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
fold value in *. fold var in *. fold varmap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl. simpl in IHx. assumption.
* congruence.
+ destruct (leak_lookahead x s1) eqn: Hl'. 2: congruence.
simp comp_relaxed.
rewrite <- app_comm_cons.
assert (x - 0 = x) as -> by lia.
unfold multi_step_hd in IHx.
destruct (alist_find _ x0 V).
* specialize (IHx _ _ V (alist_add decZ (eval_expr_fun a0 V) v H) Hl').
destruct (multi_step spec_step_fun ((Some x, V, alist_add decZ (eval_expr_fun a0 V) v H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl in *. assumption.
* specialize (IHx _ _ V (alist_add decZ (eval_expr_fun a0 V) 0%Z H) Hl').
destruct (multi_step spec_step_fun ((Some x, V, alist_add decZ (eval_expr_fun a0 V) 0%Z H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl in *. assumption.
+ simp comp_relaxed.
rewrite <- app_comm_cons.
specialize (IHx _ _ V H Hl).
unfold multi_step_hd in IHx.
destruct (multi_step spec_step_fun ((Some x, V, H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
* simpl in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
* assert (x - 0 = x) as -> by lia.
unfold multi_step in He. fold (multi_step spec_step_fun) in He. rewrite He. simpl in *. assumption.
Qed.
Lemma exec_no_nested_spec V H c s1 s2 s0 l
(Hl : leak_lookahead sixteen s1 = Some l)
(He : leak_lookahead sixteen s1 = leak_lookahead sixteen s2):
cr_sim' (nonspec_step_fun (V, H, If c s1 s2 :: s0))
(hd ((None, V, H, If c (comp_relaxed sixteen s1) (comp_relaxed sixteen s2) :: comp_relaxed sixteen s0) :: nil)
(multi_step spec_step_fun
((None, V, H, If c (comp_relaxed sixteen s1) (comp_relaxed sixteen s2) :: comp_relaxed sixteen s0) :: nil) eighteen)).
Proof.
cbn.
destruct (Z.eq_dec (eval_expr_fun c V) 0).
- pose proof (spec_x_steps sixteen _ _ V H (comp_relaxed sixteen s0) (None, V, H, (comp_relaxed sixteen s2) ++ comp_relaxed sixteen s0) Hl).
cbn. cbn in H0. rewrite H0. clear H0.
rewrite comp_relaxed_app.
reflexivity.
- rewrite He in Hl.
pose proof (spec_x_steps sixteen _ _ V H (comp_relaxed sixteen s0) (None, V, H, (comp_relaxed sixteen s1) ++ comp_relaxed sixteen s0) Hl).
cbn. cbn in H0. rewrite H0. clear H0.
rewrite comp_relaxed_app. reflexivity.
Qed.
(Hl: leak_lookahead x s1 = Some l):
multi_step_hd spec_step_fun ((Some x, V, H, (comp_relaxed sixteen s1) ++ a) :: b :: nil) (S x) = b :: nil.
Proof.
induction x in s1, l, Hl, V, H|-*.
- cbn. reflexivity.
- unfold multi_step_hd. cbn.
destruct s1. cbn in Hl. congruence.
cbn in Hl.
destruct s; try congruence.
+ destruct (leak_lookahead x s1) eqn: Hl'.
* simp comp_relaxed.
rewrite <- app_comm_cons.
destruct (alist_find decZ (eval_expr_fun a0 V) H).
-- unfold multi_step_hd in IHx.
assert (x - 0 = x) as -> by lia.
specialize (IHx _ _ (alist_add _ x0 v V) H Hl').
destruct (multi_step spec_step_fun ((Some x, alist_add RelDec_string x0 v V, H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
fold var in *. fold varmap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
fold var in *. fold varmap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl. simpl in IHx. assumption.
-- unfold multi_step_hd in IHx.
assert (x - 0 = x) as -> by lia.
specialize (IHx _ _ (alist_add _ x0 0%Z V) H Hl').
destruct (multi_step spec_step_fun ((Some x, alist_add RelDec_string x0 0%Z V, H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
fold value in *. fold var in *. fold varmap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
fold value in *. fold var in *. fold varmap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl. simpl in IHx. assumption.
* congruence.
+ destruct (leak_lookahead x s1) eqn: Hl'. 2: congruence.
simp comp_relaxed.
rewrite <- app_comm_cons.
assert (x - 0 = x) as -> by lia.
unfold multi_step_hd in IHx.
destruct (alist_find _ x0 V).
* specialize (IHx _ _ V (alist_add decZ (eval_expr_fun a0 V) v H) Hl').
destruct (multi_step spec_step_fun ((Some x, V, alist_add decZ (eval_expr_fun a0 V) v H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl in *. assumption.
* specialize (IHx _ _ V (alist_add decZ (eval_expr_fun a0 V) 0%Z H) Hl').
destruct (multi_step spec_step_fun ((Some x, V, alist_add decZ (eval_expr_fun a0 V) 0%Z H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx. cbn in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
-- fold var in *. fold value in *. fold varmap in *. fold heap in *.
rewrite He in IHx.
unfold multi_step in He. fold (multi_step spec_step_fun) in He.
rewrite He. simpl in *. assumption.
+ simp comp_relaxed.
rewrite <- app_comm_cons.
specialize (IHx _ _ V H Hl).
unfold multi_step_hd in IHx.
destruct (multi_step spec_step_fun ((Some x, V, H, comp_relaxed sixteen s1 ++ a) :: b :: nil) (S x)) eqn: He.
* simpl in IHx. symmetry in IHx. now apply list_cons_neq in IHx.
* assert (x - 0 = x) as -> by lia.
unfold multi_step in He. fold (multi_step spec_step_fun) in He. rewrite He. simpl in *. assumption.
Qed.
Lemma exec_no_nested_spec V H c s1 s2 s0 l
(Hl : leak_lookahead sixteen s1 = Some l)
(He : leak_lookahead sixteen s1 = leak_lookahead sixteen s2):
cr_sim' (nonspec_step_fun (V, H, If c s1 s2 :: s0))
(hd ((None, V, H, If c (comp_relaxed sixteen s1) (comp_relaxed sixteen s2) :: comp_relaxed sixteen s0) :: nil)
(multi_step spec_step_fun
((None, V, H, If c (comp_relaxed sixteen s1) (comp_relaxed sixteen s2) :: comp_relaxed sixteen s0) :: nil) eighteen)).
Proof.
cbn.
destruct (Z.eq_dec (eval_expr_fun c V) 0).
- pose proof (spec_x_steps sixteen _ _ V H (comp_relaxed sixteen s0) (None, V, H, (comp_relaxed sixteen s2) ++ comp_relaxed sixteen s0) Hl).
cbn. cbn in H0. rewrite H0. clear H0.
rewrite comp_relaxed_app.
reflexivity.
- rewrite He in Hl.
pose proof (spec_x_steps sixteen _ _ V H (comp_relaxed sixteen s0) (None, V, H, (comp_relaxed sixteen s1) ++ comp_relaxed sixteen s0) Hl).
cbn. cbn in H0. rewrite H0. clear H0.
rewrite comp_relaxed_app. reflexivity.
Qed.
The simulation relation is correct w.r.t. the synchronizer: We always end up in related states.
Lemma cr_sim_sync_correct p_src (i : heap) (a : list state) (α0 : list (list specstate))
(b : state) (β : list (list specstate)):
cr_sim p_src i a α0 ->
nonspec_trace p_src i (b :: a) ->
spec_am_trace (comp_relaxed' p_src) i (β ++ α0) ->
cr_sim_sync p_src i (| a |) = | β | -> cr_sim p_src i (b :: a) (β ++ α0).
Proof.
intros.
unfold cr_sim.
eapply prove_trace_by_tsync.
1-2: auto.
4: exact H0.
4: exact H1.
- simpl. reflexivity.
- intros.
unfold cr_sim' in H3.
destruct a0 as [ [V HH] s]. rewrite H3.
unfold comp_relaxed'.
destruct s.
+ simpl. unfold multi_step_hd. simpl. simp comp_relaxed. reflexivity.
+ destruct s; unfold multi_step_hd.
* simp comp_relaxed. reflexivity.
* simp comp_relaxed. simpl. destruct (alist_find decZ (eval_expr_fun a0 V) HH); reflexivity.
* simp comp_relaxed. simpl. destruct (alist_find _ x V); reflexivity.
* simp comp_relaxed.
cbv zeta. destruct (dec_syntObsL (leak_lookahead sixteen (s1)) (leak_lookahead sixteen (s2))) eqn:He.
-- destruct (leak_lookahead sixteen (s1)) eqn: Hl.
++ unfold cr_sim_step. rewrite Hl, He. eapply exec_no_nested_spec. eauto. now rewrite <- e.
++ unfold cr_sim_step. rewrite Hl, He. cbn. destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; rewrite comp_relaxed_app; reflexivity.
-- unfold cr_sim_step. rewrite He. cbn. destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; rewrite comp_relaxed_app; reflexivity.
* rewrite comp_relaxed_equation_6.
cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen (s1)) (leak_lookahead sixteen (s2))) eqn: He.
-- destruct (leak_lookahead sixteen (s1)) eqn: Hl; simpl.
++ unfold comp_relaxed'. simp comp_relaxed. cbv zeta. apply (leak_la_extend s1 (While c s1 s2 :: nil)) in Hl as Hl'.
rewrite Hl'. rewrite He.
do 4 f_equal. rewrite comp_relaxed_app. f_equal.
simp comp_relaxed. cbv zeta. rewrite Hl, He.
reflexivity.
++ unfold comp_relaxed'. simp comp_relaxed. cbv zeta.
rewrite (noleak_extend _ _ _ _ _ Hl). rewrite He. do 5 f_equal. rewrite comp_relaxed_app. simp comp_relaxed. cbv zeta. rewrite Hl, He. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite He. do 6 f_equal.
rewrite comp_relaxed_app. simp comp_relaxed. cbv zeta. rewrite He. reflexivity.
* simp comp_relaxed. reflexivity.
* simp comp_relaxed. reflexivity.
- exact H.
- exact H2.
Qed.
(b : state) (β : list (list specstate)):
cr_sim p_src i a α0 ->
nonspec_trace p_src i (b :: a) ->
spec_am_trace (comp_relaxed' p_src) i (β ++ α0) ->
cr_sim_sync p_src i (| a |) = | β | -> cr_sim p_src i (b :: a) (β ++ α0).
Proof.
intros.
unfold cr_sim.
eapply prove_trace_by_tsync.
1-2: auto.
4: exact H0.
4: exact H1.
- simpl. reflexivity.
- intros.
unfold cr_sim' in H3.
destruct a0 as [ [V HH] s]. rewrite H3.
unfold comp_relaxed'.
destruct s.
+ simpl. unfold multi_step_hd. simpl. simp comp_relaxed. reflexivity.
+ destruct s; unfold multi_step_hd.
* simp comp_relaxed. reflexivity.
* simp comp_relaxed. simpl. destruct (alist_find decZ (eval_expr_fun a0 V) HH); reflexivity.
* simp comp_relaxed. simpl. destruct (alist_find _ x V); reflexivity.
* simp comp_relaxed.
cbv zeta. destruct (dec_syntObsL (leak_lookahead sixteen (s1)) (leak_lookahead sixteen (s2))) eqn:He.
-- destruct (leak_lookahead sixteen (s1)) eqn: Hl.
++ unfold cr_sim_step. rewrite Hl, He. eapply exec_no_nested_spec. eauto. now rewrite <- e.
++ unfold cr_sim_step. rewrite Hl, He. cbn. destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; rewrite comp_relaxed_app; reflexivity.
-- unfold cr_sim_step. rewrite He. cbn. destruct (Z.eq_dec (eval_expr_fun c V) 0); simpl; rewrite comp_relaxed_app; reflexivity.
* rewrite comp_relaxed_equation_6.
cbv zeta.
destruct (dec_syntObsL (leak_lookahead sixteen (s1)) (leak_lookahead sixteen (s2))) eqn: He.
-- destruct (leak_lookahead sixteen (s1)) eqn: Hl; simpl.
++ unfold comp_relaxed'. simp comp_relaxed. cbv zeta. apply (leak_la_extend s1 (While c s1 s2 :: nil)) in Hl as Hl'.
rewrite Hl'. rewrite He.
do 4 f_equal. rewrite comp_relaxed_app. f_equal.
simp comp_relaxed. cbv zeta. rewrite Hl, He.
reflexivity.
++ unfold comp_relaxed'. simp comp_relaxed. cbv zeta.
rewrite (noleak_extend _ _ _ _ _ Hl). rewrite He. do 5 f_equal. rewrite comp_relaxed_app. simp comp_relaxed. cbv zeta. rewrite Hl, He. reflexivity.
-- simpl. unfold comp_relaxed'. simp comp_relaxed. cbv zeta. rewrite <- leak_extend. rewrite He. do 6 f_equal.
rewrite comp_relaxed_app. simp comp_relaxed. cbv zeta. rewrite He. reflexivity.
* simp comp_relaxed. reflexivity.
* simp comp_relaxed. reflexivity.
- exact H.
- exact H2.
Qed.