HyPre.pred.HyperPreserveBarrier
(* CLN B *)
From Coq Require Import
Program.Equality.
From HyPre Require Export
ListExtra
NatExtra
Tac.
From HyPre Require Export
HyperPreserve
BarrierSync.
Import ListNotations.
Import VecNatNotations.
Import VectorListNotations.
Section with_k_st.
Context {k : nat}.
Context {Input SrcSt TgtSt : Type}.
Lemma sim_step_to_reach
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
src_sem tgt_sem t_sync_i t_next_i
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(TSi : forall i : Input, TotalSynchroniser (t_sync_i i) (t_next_i i))
(Hunit : forall i, sim_rel i [] [])
(Hstep : forall (i : Input) (a : list SrcSt) (α : list TgtSt) (b : SrcSt) (β : list TgtSt),
sim_rel i a α ->
src_sem i (b :: a) ->
tgt_sem i (β ++ α) -> t_sync_i i (| a |) = | β | -> sim_rel i (b :: a) (β ++ α))
: forall (i : Input) (a : list SrcSt) (α : list TgtSt),
(t_reachable (TotalSynchroniser:=TSi i)) (| a |, | α |) -> src_sem i a -> tgt_sem i α -> sim_rel i a α.
Proof.
intros i a α Hreach.
remember (|a|) as m.
remember (|α|) as n.
revert a α Heqm Heqn.
eapply tsync_ind with (a:=m) (α:=n).
- intros.
destruct a,α; cbn in Heqm,Heqn; try congruence.
eapply Hunit.
- intros.
eapply firstn_lastn in Heqn as Heqn2.
rewrite Heqn2.
destruct a0;cbn in Heqm;[congruence|].
eapply Hstep.
+ eapply H;eauto.
* rewrite lastn_length_le;eauto.
lia.
* eapply safe;eauto.
* eapply sem_safe_app;eauto.
rewrite Heqn2 in H1.
eapply H1.
+ assumption.
+ rewrite Heqn2 in H1.
eapply H1.
+ rewrite firstn_length_le.
* inversion Heqm.
reflexivity.
* lia.
- eapply Hreach.
Qed.
(*
sync will be defined implicitly by barriers, so the user has to give:
- a barrier predicate list SrcSt -> bool
- a liveness guarantee of the barrier.
t_sync is given parametrised over inputs as a function Input -> list SrcSt -> nat (tgt steps on next src step)
t_next is given parametrised over inputs as a function Input -> list SrcSt -> nat (src steps till step on tgt)
*)
Definition reachable' (s : Vector.t nat k -> Vector.t nat k)
:= VecNatO Nat.add s.
Class hyper_preserve_barrier
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(P_barrier : (SrcSt * list SrcSt) -> Prop)
(steps_to_barrier : Input -> list SrcSt -> (SrcSt * list SrcSt))
: Prop
:=
{
src_rel_unit : src_rel vl_zero;
tgt_rel_unit : tgt_rel vl_zero;
t_reach := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
hpb_step : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> reachable' (bl_sync steps_to_barrier i_vec) (vl_len a)
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall bp,
bp = Vector.map2 (fun i a => steps_to_barrier i a) i_vec a
-> b = (let (b0,bs) := vec_unzip bp in b0 :vl: bs)
-> Vector.Forall P_barrier bp
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
barrier_prop : forall i a, src_sem i a -> P_barrier (steps_to_barrier i a);
stb_sem : forall i a, src_sem i a -> src_sem i (bl_cons steps_to_barrier i a ++ a);
}.
Section with_hpb.
Context `(HPB : hyper_preserve_barrier).
Set Nested Proofs Allowed.
Lemma vec_map2_map_arg2 {W X Y Z : Type} (f : X -> Y -> Z) (g : W -> Y) (xt wt : Vector.t _ k)
: Vector.map2 f xt (Vector.map g wt) = Vector.map2 (fun x w => f x (g w)) xt wt.
Proof.
clear.
setoid_rewrite vec_map2_fun_app.
setoid_rewrite Vector.map_id.
reflexivity.
Qed.
Instance hyper_preserve_barrier_hp
: hyper_preserve i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
TSi
(bl_Sync steps_to_barrier i_vec).
Proof.
econstructor.
- eapply src_rel_unit.
- eapply tgt_rel_unit.
- intros a Hsrc Hreach α Htgt Hsim b Hsrc_sem β Htgt_sem Hsim' Hsync.
eapply hpb_step;eauto.
+ eapply vec_forall3_forall.
intros.
rewrite vec_forall3_forall in Hsim.
eapply sim_step.
* unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
* eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
+ eapply vec_forall3_forall.
intros.
rewrite vec_forall3_forall in Hsim'.
eapply sim_step.
* unfold vl_len in Hsim'.
specialize (Hsim' i).
setoid_rewrite Vector.nth_map in Hsim'. 2,3:reflexivity.
eapply Hsim'.
* eapply Vec_Forall2_forall2;eauto.
* eapply Vec_Forall2_forall2;eauto.
+ eapply bl_sync_cons_eq.
* eapply Vec_Forall2_forall2;intros.
eapply stb_sem;eauto.
* eassumption.
* assumption.
+ eapply vec_Forall_forall.
intros.
rewrite Vec_nth_map2.
eapply barrier_prop.
eapply Vec_Forall2_forall2 in Hsrc_sem.
setoid_rewrite Vec_nth_map2 in Hsrc_sem.
eapply sem_safe_app;eauto.
Qed.
End with_hpb.
Class hyper_preserve_barrier_c
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c : src_rel vl_zero;
tgt_rel_unit_c : tgt_rel vl_zero;
t_reach_c := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
hpb_step_c : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach_c i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
}.
(*
Why would I ever need leakage functions on the state before the simulation?
This would only make sens if I would try to get from different language inputs to the same
simulation state. But there are many hurdles: To do this I have to make sure that the trace
stays infinite...
But there is a very good reason to let the semantics start with :
This way we can factor out the program, and let it be deterministic just on the Input.
In a more abstract vision on the other hand one would see Input and Program as dual objects,
This is circumvented here by just stating everything once for Src and once for Tgt,
as we always have exactly 2 Programs.
There could be some generalisation that would work on several "Programs"
- the same way we argue about several traces (on different Inputs) right now.
But this is currently waaaaay out of scope.
It would also come with new pitfalls:
in particular the TotalSynchroniser breaks the duality currently.
And just using two Synchroniser doesn't work without a further requirement of
always-eventually-in-sync.
*)
Class hyper_preserve_barrier_c2
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c2 : src_rel vl_zero;
tgt_rel_unit_c2 : tgt_rel vl_zero;
sim_rel_unit_c2 : forall i, sim_rel i [] [];
hpb_step_c2 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c2 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α)
}.
Section with_hpbc.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context (is_B : SrcSt -> bool).
Context (stb_live_B : forall i a, src_sem i a -> exists b0 bs, src_sem i (b0 :: bs ++ a) /\ is_B b0 = true).
Context `(HPBC : hyper_preserve_barrier_c (src_sem:=src_sem) (is_B:=is_B)).
(* Context `(HPBC : hyper_preserve_barrier_c).*)
Definition P_barrier (b : SrcSt * list SrcSt)
:= let (b0,bs) := b in
is_B b0 = true /\ Forall (fun x => is_B x = false) bs.
Lemma hpbc_hpb
: exists (bl_step : Input -> list SrcSt -> SrcSt * list SrcSt),
hyper_preserve_barrier i_vec
src_rel
tgt_rel
src_sem
tgt_sem
Rsrc
Rtgt
sim_rel
t_sync_i
t_next_i
TSi
P_barrier
bl_step.
Proof.
specialize (@bl_ex_step0 Input SrcSt _ _ state0 dec_SrcSt is_B) as Hex.
exploit' Hex.
specialize (stb_live_B) as Hlive.
destructH.
exists bl_step.
econstructor.
1,2,4: now destruct HPBC; eauto.
- intros.
eapply hpb_step_c with (b0:=fst (vec_unzip bp))
(bs:=snd (vec_unzip bp));eauto.
+ setoid_rewrite H7.
setoid_rewrite surjective_pairing at 1.
reflexivity.
+ eapply vec_Forall_forall.
rewrite vec_Forall_forall in H8.
intros.
rewrite vec_unzip_fst.
unfold P_barrier in H8.
setoid_rewrite Vector.nth_map. 2:reflexivity.
specialize (H8 i).
destruct (bp[[i]]). cbn.
firstorder.
+ rewrite vec_unzip_snd.
eapply vec_Forall_forall.
intros.
rewrite vec_Forall_forall in H8.
setoid_rewrite Vector.nth_map. 2:reflexivity.
specialize (H8 i). unfold P_barrier in H8.
destruct (bp[[i]]). cbn.
firstorder.
- intros.
unfold live_B_minimal_def' in Hex.
specialize (Hex i a).
destruct (bl_step i a).
unfold P_barrier.
firstorder.
- intros.
unfold live_B_minimal_def' in Hex.
specialize (Hex i a).
unfold bl_cons.
destruct (bl_step i a).
firstorder.
Qed.
End with_hpbc.
Class hyper_preserve_barrier_c3
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c3 : src_rel vl_zero;
tgt_rel_unit_c3 : tgt_rel vl_zero;
t_reach_c3 := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
sim_rel_unit_c3 : forall i, sim_rel i [] [];
hpb_step_c3 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c3 : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach_c3 i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
src_rel_div3 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
src_rel a
-> (forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
Class hyper_preserve_barrier_c5
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c5 : src_rel vl_zero;
tgt_rel_unit_c5 : tgt_rel vl_zero;
sim_rel_unit_c5 : forall i, sim_rel i [] [];
hpb_step_c5 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c5 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α);
src_rel_div5 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
src_rel a
-> (forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
Class hyper_preserve_barrier_c7
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c7 : src_rel vl_zero;
tgt_rel_unit_c7 : tgt_rel vl_zero;
sim_rel_unit_c7 : forall i, sim_rel i [] [];
t_reach_c7 := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
hpb_step_c7 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> (forall j, is_B j a (b0[[j]]) = true)
-> (forall j, Forall (fun y => is_B j a y = false) (bs[[j]]))
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c7 : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach_c7 i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
(* sim_step_c7 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α);*)
src_rel_div7 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
(forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B i a s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
Class hyper_preserve_barrier_c9
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c9 : src_rel vl_zero;
tgt_rel_unit_c9 : tgt_rel vl_zero;
sim_rel_unit_c9 : forall i, sim_rel i [] [];
hpb_step_c9 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> (forall j, is_B j a (b0[[j]]) = true)
-> (forall j, Forall (fun y => is_B j a y = false) (bs[[j]]))
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c9 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α);
src_rel_div9 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
(forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B i a s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
(* It might work afterall! ex_bl_Sync' gives me the Synchroniser (non-constructively).
Thus it is possible to instantiate HyperPreserve with this Synchroniser
The idea was to show that this is an instance of HyperPreserve withouth the live_B assumption.
the instantiation would set src_rel' := src_rel \/ no_barrier_ever etc.
I will *not* be able to show that this is an instance of HyperPreserve,
because I would have to construct a Synchroniser that declines from using is_B
when we are at point where no barrier is visited anymore.
But this is not decidable and Synchronisers reside in Type!
I can only decide on this point using classical reasoning
and I think there is a way to prove an analogon to hyper_preserve_AE
based on hyper_preserve_barrier_c3.
Which is all I need for Termination-Sensitive / "concurrent" Non-Interference.
But it will be a considerable effort and I am not sure if this should be the priority right now.
Alternatively, I could focus on termination-insensitive NI for now.
The approach sketched out here is actually quite general,
thus if successful, it should be fairly easy to adopt the proofs and get the sensitive results.
One could even argue that termination-insensitive NI is more practically relevant,
because termination-sensitive NI requires some reasoning about termination, which is hard.
I should check the literature how common which variant is.
On the other hand one could very much argue against it,
since we are observing traces and ideally we would want to argue about "concurrent" NI,
i.e. treating termination as an effect but also have a result for non-terminating programs.
In particular the whole development is made in a way to support infinite traces.
Another - rather ugly - fix would be to make my language terminate
after some arbitrary but finite "k".
This would make the synchroniser definable and we would argue that we may do this for any "k",
i.e. every finite prefix of "k"-step execution is safe, thus the whole program is kinda safe.
*)
Section with_hbpc3.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(hyper_preserve_barrier_c3 (src_sem:=src_sem) (is_B:=is_B)).
Lemma forall_or_fe_or (P Q : Fin.t k -> Prop)
(Hforall : forall x, P x \/ Q x)
: (forall x, P x) \/ exists x, Q x.
Proof.
clear - Hforall.
dependent induction k.
- left.
intros.
inversion x.
- specialize (Hforall (@Fin.F1 n)) as R.
destruct R.
+ specialize (IHn (fun x => P (Fin.FS x)) (fun x => Q (Fin.FS x))).
exploit' IHn.
destruct IHn.
* left.
intros.
dependent destruction x;eauto.
* right.
destructH.
eexists;eauto.
+ right.
eexists;eauto.
Qed.
Lemma vec_Forall2_or {j : nat} {X Y : Type} (P Q : X -> Y -> Prop) (xt yt : Vector.t _ j)
(Hor : forall x y, P x y \/ Q x y)
: Vector.Forall2 P xt yt \/ exists i, Q (xt[[i]]) (yt[[i]]).
clear - Hor.
Proof.
dependent induction xt; dependent destruction yt.
- left.
rewrite <-x.
econstructor.
- subst n0.
subst yt0.
eapply IHxt in Hor as R.
destruct R.
+ specialize (Hor h h0) as T.
destruct T.
* left.
econstructor;eauto.
* right.
exists (Fin.F1).
cbn.
assumption.
+ right.
destruct H as [i H'].
exists (Fin.FS i).
cbn.
assumption.
Qed.
Lemma hpbc_hpb3
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
specialize (@bl_ex_step_or0 _ _ _ _ state0 dec_SrcSt is_B) as Q.
destructH.
specialize (ex_bl_sync' (k:=k) bl_step' (fun i a => exists b0 bs, src_sem i (b0 :: bs ++ (construct_trace src_sem a i)) /\ is_B b0 = true)) as T.
destructH.
exists bl_sync'.
exists (T1 i_vec).
econstructor.
- eapply src_rel_unit_c3.
- eapply tgt_rel_unit_c3.
- intros.
eapply vec_Forall2_or with (xt:=i_vec) (yt:=a) in Q.
destruct Q as [Q|Q].
+ unfold live_B_minimal_def' in Q.
pose (b0:=fst (vec_unzip (Vector.map2 (fun (i : Input) (a : list SrcSt) => bl_step' i a) i_vec a))).
pose (bs:=snd (vec_unzip (Vector.map2 (fun (i : Input) (a : list SrcSt) => bl_step' i a) i_vec a))).
eapply hpb_step_c3 with (b0:=b0) (bs:=bs);eauto.
* eapply vec_forall3_forall.
intros.
rename H3 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c3.
-- unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply vec_forall3_forall.
intros.
rename H6 into Hsim'.
rewrite vec_forall3_forall in Hsim'.
eapply sim_step_c3.
-- unfold vl_len in Hsim'.
specialize (Hsim' i).
setoid_rewrite Vector.nth_map in Hsim'. 2,3:reflexivity.
eapply Hsim'.
-- eapply Vec_Forall2_forall2;eauto.
-- eapply Vec_Forall2_forall2;eauto.
* eapply bl_sync_cons_eq with (bl_step:=bl_step') in H4;eauto.
-- rewrite H4.
subst b0 bs.
destruct (vec_unzip (Vector.map2 (fun (i : Input) (a0 : list SrcSt) => bl_step' i a0)
i_vec a)).
cbn.
reflexivity.
-- eapply Vec_Forall2_forall2;intros.
eapply Vec_Forall2_forall2 with (i:=i) in Q.
unfold bl_cons.
destruct (bl_step' (i_vec [[i]]) (a[[i]])).
eapply Q in H8.
destruct H8.
assumption.
-- rewrite H7.
specialize (T0 i_vec (vl_len a)).
eapply Vector.eq_nth_iff.
intros.
subst p2.
eapply vec_forall3_forall with (i:=p1) in T0.
destruct T0 as [T0 _].
rewrite T0.
++ unfold bl_sync.
rewrite Vec_nth_map2.
reflexivity.
++ eapply Vec_Forall2_forall2 with (i:=p1) in Q.
destruct (bl_step' (i_vec [[p1]]) (a [[p1]])) as [b1 bs0].
exists b1, bs0.
eapply Vec_Forall2_forall2 with (i:=p1) in H4.
setoid_rewrite Vec_nth_map2 in H4.
eapply sem_safe_app in H4;eauto.
eapply Q in H4 as H4'.
split.
** setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite construct_trace_length.
eapply H4';eauto.
eapply H4.
** eapply H4'.
* eapply vec_Forall_forall.
intros.
subst b0.
rewrite vec_unzip_fst.
setoid_rewrite Vector.nth_map with (p1:=i). 2:reflexivity.
setoid_rewrite Vec_nth_map2.
eapply Vec_Forall2_forall2 with (i:=i) in Q.
destruct (bl_step' (i_vec [[i]]) (a[[i]])).
cbn.
eapply Vec_Forall2_forall2 with (i:=i) in H4.
setoid_rewrite Vec_nth_map2 in H4.
eapply sem_safe_app in H4;eauto.
eapply Q in H4.
eapply H4.
* eapply vec_Forall_forall.
intros.
subst bs.
setoid_rewrite vec_unzip_snd.
setoid_rewrite Vector.nth_map with (p1:=i). 2:reflexivity.
setoid_rewrite Vec_nth_map2.
eapply Vec_Forall2_forall2 with (i:=i) in Q.
destruct (bl_step' (i_vec [[i]]) (a[[i]])).
cbn.
eapply Vec_Forall2_forall2 with (i:=i) in H4.
setoid_rewrite Vec_nth_map2 in H4.
eapply sem_safe_app in H4;eauto.
eapply Q in H4.
eapply H4.
+ destructH.
eapply src_rel_div3;eauto.
* eapply vec_forall3_forall.
intros.
rename H3 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c3.
-- unfold vl_len in Hsim.
specialize (Hsim i0).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply vec_forall3_forall.
intros.
rename H6 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c3.
-- unfold vl_len in Hsim.
specialize (Hsim i0).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2;eauto.
-- eapply Vec_Forall2_forall2;eauto.
Qed. (* TODO tidy up this ugly mess *)
End with_hbpc3.
Section with_hpbc2.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context (stb_live_B : forall i a, src_sem i a -> exists b0 bs, src_sem i (b0 :: bs ++ a) /\ is_B b0 = true).
Context `(HPBC : hyper_preserve_barrier_c2 (src_sem:=src_sem) (is_B:=is_B)).
Definition P_barrier2 (b : SrcSt * list SrcSt)
:= let (b0,bs) := b in
is_B b0 = true /\ Forall (fun x => is_B x = false) bs.
Lemma hpbc_hpb2
: exists (bl_step : Input -> list SrcSt -> SrcSt * list SrcSt),
hyper_preserve_barrier i_vec
src_rel
tgt_rel
src_sem
tgt_sem
Rsrc
Rtgt
sim_rel
t_sync_i
t_next_i
TSi
P_barrier2
bl_step.
Proof.
eapply hpbc_hpb;eauto.
destruct HPBC.
econstructor;eauto.
clear - Rsrc Rtgt sim_step_c4 sim_rel_unit_c4.
eapply sim_step_to_reach;eauto.
Qed.
End with_hpbc2.
Section with_hpbc7.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(HPBC : hyper_preserve_barrier_c7 (src_sem:=src_sem) (is_B:=is_B)).
Lemma hpbc_hpb7
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
specialize (@bl_ex_step_or2 _ _ _ _ _ is_B state0 dec_SrcSt) as Q.
destructH.
pose (vbl_step' := (fun iv a => vec_mapi (fun j i => bl_step' j i a) iv)).
specialize (@vex_bl_sync' k Input SrcSt src_sem Rsrc vbl_step'
(fun i (vn : vecnat k) =>
let a := (Vector.map2 (construct_trace src_sem) vn i) in
exists b0 bs, Vector.Forall2 src_sem i (b0 :vl: bs +vl+ a)
/\ forall j, is_B j a (b0[[j]]) = true)) as T.
destructH.
exists bl_sync'.
exists (T1 i_vec).
econstructor.
- eapply src_rel_unit_c7.
- eapply tgt_rel_unit_c7.
- intros.
unfold live_or_not in Q.
specialize (Q i_vec a).
eapply forall_or_fe_or in Q.
destruct Q as [Q|Q].
+ unfold live_B_minimal_def' in Q.
eapply Forall2_vl_app22 in H3 as H3';eauto.
2:eapply sem_prefix_containing;eauto.
pose (b0:=fst (vec_unzip (vbl_step' i_vec a))).
pose (bs:=snd (vec_unzip (vbl_step' i_vec a))).
eapply hpb_step_c7 with (b0:=b0) (bs:=bs);eauto.
* eapply vec_forall3_forall.
intros.
rename H2 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c7.
-- unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply vec_forall3_forall.
intros.
rename H5 into Hsim'.
rewrite vec_forall3_forall in Hsim'.
eapply sim_step_c7.
-- unfold vl_len in Hsim'.
specialize (Hsim' i).
setoid_rewrite Vector.nth_map in Hsim'. 2,3:reflexivity.
eapply Hsim'.
-- eapply Vec_Forall2_forall2;eauto.
-- eapply Vec_Forall2_forall2;eauto.
* setoid_rewrite vbl_sync_cons_eq with (bl_step:=vbl_step') at 1.
2,4:eauto.
-- setoid_rewrite surjective_pairing.
subst b0 bs.
reflexivity.
-- eapply Vec_Forall2_forall2;intros.
unfold vbl_cons.
setoid_rewrite Vector.nth_map2 with (p2:=i) (p3:=i). 2,3:reflexivity.
setoid_rewrite Vector.nth_map. 2:reflexivity.
specialize (Q i).
subst vbl_step'.
setoid_rewrite vec_mapi_nth.
destruct (bl_step' i (i_vec[[i]]) a).
exploit Q.
++ eapply Vec_Forall2_forall2;eauto.
++ cbn.
eapply Q.
-- rewrite H6.
specialize (T0 i_vec (vl_len a)).
destructH.
cbn in *.
eapply T2.
exists b0, bs.
split.
++ eapply Vec_Forall2_forall2;eauto.
intros.
specialize (Q i).
subst b0 bs.
unfold vbl_step'.
setoid_rewrite Vector.nth_map2. 2,3:reflexivity.
setoid_rewrite Vector.nth_map2. 2-5:reflexivity.
setoid_rewrite vec_unzip_fst.
setoid_rewrite vec_unzip_snd.
setoid_rewrite Vector.nth_map. 2-4:reflexivity.
setoid_rewrite vec_mapi_nth.
destruct (bl_step' i (i_vec[[i]]) a).
cbn.
setoid_rewrite construct_trace_length.
eapply Q.
all: eapply Vec_Forall2_forall2;eauto.
++ intros.
specialize (Q j).
subst b0.
unfold vbl_step'.
rewrite vec_unzip_fst.
setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite vec_mapi_nth.
destruct (bl_step' j (i_vec[[j]]) a).
cbn.
replace (Vector.map2 (construct_trace src_sem) (vl_len a) i_vec)
with a;cycle 1.
{
eapply Vector.eq_nth_iff.
intros.
subst p2.
setoid_rewrite Vector.nth_map2. 2,3:reflexivity.
setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite construct_trace_length;eauto.
eapply Vec_Forall2_forall2;eauto.
}
eapply Q.
eapply Vec_Forall2_forall2;eauto.
-- eauto.
* intros.
subst b0.
rewrite vec_unzip_fst.
setoid_rewrite Vector.nth_map with (p1:=j). 2:reflexivity.
unfold vbl_step'.
setoid_rewrite vec_mapi_nth.
specialize (Q j).
destruct (bl_step' j (i_vec[[j]]) a).
cbn.
eapply Q.
eapply Vec_Forall2_forall2;eauto.
* intros.
subst bs.
setoid_rewrite vec_unzip_snd.
setoid_rewrite Vector.nth_map with (p1:=j). 2:reflexivity.
unfold vbl_step'.
rewrite vec_mapi_nth.
specialize (Q j).
destruct (bl_step' j (i_vec [[j]]) a).
cbn.
eapply Q.
eapply Vec_Forall2_forall2;eauto.
+ destructH.
eapply src_rel_div7;eauto.
eapply vec_forall3_forall.
intros.
rename H2 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c7.
-- unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
Qed.
End with_hpbc7.
Section with_hpbc9.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(HPBC : hyper_preserve_barrier_c9 (src_sem:=src_sem) (is_B:=is_B)).
Lemma hpbc_hpb9
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
eapply hpbc_hpb7;eauto.
destruct HPBC.
econstructor;eauto.
clear - Rsrc Rtgt sim_step_c10 sim_rel_unit_c10.
eapply sim_step_to_reach;eauto.
Qed.
End with_hpbc9.
Section with_hpbc5.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(HPBC : hyper_preserve_barrier_c5 (src_sem:=src_sem) (is_B:=is_B)).
Lemma hpbc_hpb5
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
eapply hpbc_hpb3;eauto.
destruct HPBC.
econstructor;eauto.
clear - Rsrc Rtgt sim_step_c6 sim_rel_unit_c6.
eapply sim_step_to_reach;eauto.
Qed.
End with_hpbc5.
End with_k_st.
(*
Goal forall a, forall i, exists n, d (n_steps (S n) a [i]).
Abort.
Goal forall a, (forall i, exists n, d (n_steps n a[i])) \/ (forall i n, ~ d (n_steps n a[i])).
Abort.
Goal forall a, forall i, (exists n, d (n_steps n a[i])) \/ (forall n, ~ d (n_steps n a[i])).
Abort.
Goal forall a, exists vn, vd (n_steps n a). (* Problem: which one is the next ? the vecnats are not sorted in general *)
Abort.
Goal forall a, (exists vn, vd (n_steps n a)) \/ (forall vn, ~ vd (n_steps n a)).
Abort.
*)
From Coq Require Import
Program.Equality.
From HyPre Require Export
ListExtra
NatExtra
Tac.
From HyPre Require Export
HyperPreserve
BarrierSync.
Import ListNotations.
Import VecNatNotations.
Import VectorListNotations.
Section with_k_st.
Context {k : nat}.
Context {Input SrcSt TgtSt : Type}.
Lemma sim_step_to_reach
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
src_sem tgt_sem t_sync_i t_next_i
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(TSi : forall i : Input, TotalSynchroniser (t_sync_i i) (t_next_i i))
(Hunit : forall i, sim_rel i [] [])
(Hstep : forall (i : Input) (a : list SrcSt) (α : list TgtSt) (b : SrcSt) (β : list TgtSt),
sim_rel i a α ->
src_sem i (b :: a) ->
tgt_sem i (β ++ α) -> t_sync_i i (| a |) = | β | -> sim_rel i (b :: a) (β ++ α))
: forall (i : Input) (a : list SrcSt) (α : list TgtSt),
(t_reachable (TotalSynchroniser:=TSi i)) (| a |, | α |) -> src_sem i a -> tgt_sem i α -> sim_rel i a α.
Proof.
intros i a α Hreach.
remember (|a|) as m.
remember (|α|) as n.
revert a α Heqm Heqn.
eapply tsync_ind with (a:=m) (α:=n).
- intros.
destruct a,α; cbn in Heqm,Heqn; try congruence.
eapply Hunit.
- intros.
eapply firstn_lastn in Heqn as Heqn2.
rewrite Heqn2.
destruct a0;cbn in Heqm;[congruence|].
eapply Hstep.
+ eapply H;eauto.
* rewrite lastn_length_le;eauto.
lia.
* eapply safe;eauto.
* eapply sem_safe_app;eauto.
rewrite Heqn2 in H1.
eapply H1.
+ assumption.
+ rewrite Heqn2 in H1.
eapply H1.
+ rewrite firstn_length_le.
* inversion Heqm.
reflexivity.
* lia.
- eapply Hreach.
Qed.
(*
sync will be defined implicitly by barriers, so the user has to give:
- a barrier predicate list SrcSt -> bool
- a liveness guarantee of the barrier.
t_sync is given parametrised over inputs as a function Input -> list SrcSt -> nat (tgt steps on next src step)
t_next is given parametrised over inputs as a function Input -> list SrcSt -> nat (src steps till step on tgt)
*)
Definition reachable' (s : Vector.t nat k -> Vector.t nat k)
:= VecNatO Nat.add s.
Class hyper_preserve_barrier
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(P_barrier : (SrcSt * list SrcSt) -> Prop)
(steps_to_barrier : Input -> list SrcSt -> (SrcSt * list SrcSt))
: Prop
:=
{
src_rel_unit : src_rel vl_zero;
tgt_rel_unit : tgt_rel vl_zero;
t_reach := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
hpb_step : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> reachable' (bl_sync steps_to_barrier i_vec) (vl_len a)
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall bp,
bp = Vector.map2 (fun i a => steps_to_barrier i a) i_vec a
-> b = (let (b0,bs) := vec_unzip bp in b0 :vl: bs)
-> Vector.Forall P_barrier bp
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
barrier_prop : forall i a, src_sem i a -> P_barrier (steps_to_barrier i a);
stb_sem : forall i a, src_sem i a -> src_sem i (bl_cons steps_to_barrier i a ++ a);
}.
Section with_hpb.
Context `(HPB : hyper_preserve_barrier).
Set Nested Proofs Allowed.
Lemma vec_map2_map_arg2 {W X Y Z : Type} (f : X -> Y -> Z) (g : W -> Y) (xt wt : Vector.t _ k)
: Vector.map2 f xt (Vector.map g wt) = Vector.map2 (fun x w => f x (g w)) xt wt.
Proof.
clear.
setoid_rewrite vec_map2_fun_app.
setoid_rewrite Vector.map_id.
reflexivity.
Qed.
Instance hyper_preserve_barrier_hp
: hyper_preserve i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
TSi
(bl_Sync steps_to_barrier i_vec).
Proof.
econstructor.
- eapply src_rel_unit.
- eapply tgt_rel_unit.
- intros a Hsrc Hreach α Htgt Hsim b Hsrc_sem β Htgt_sem Hsim' Hsync.
eapply hpb_step;eauto.
+ eapply vec_forall3_forall.
intros.
rewrite vec_forall3_forall in Hsim.
eapply sim_step.
* unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
* eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
+ eapply vec_forall3_forall.
intros.
rewrite vec_forall3_forall in Hsim'.
eapply sim_step.
* unfold vl_len in Hsim'.
specialize (Hsim' i).
setoid_rewrite Vector.nth_map in Hsim'. 2,3:reflexivity.
eapply Hsim'.
* eapply Vec_Forall2_forall2;eauto.
* eapply Vec_Forall2_forall2;eauto.
+ eapply bl_sync_cons_eq.
* eapply Vec_Forall2_forall2;intros.
eapply stb_sem;eauto.
* eassumption.
* assumption.
+ eapply vec_Forall_forall.
intros.
rewrite Vec_nth_map2.
eapply barrier_prop.
eapply Vec_Forall2_forall2 in Hsrc_sem.
setoid_rewrite Vec_nth_map2 in Hsrc_sem.
eapply sem_safe_app;eauto.
Qed.
End with_hpb.
Class hyper_preserve_barrier_c
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c : src_rel vl_zero;
tgt_rel_unit_c : tgt_rel vl_zero;
t_reach_c := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
hpb_step_c : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach_c i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
}.
(*
Why would I ever need leakage functions on the state before the simulation?
This would only make sens if I would try to get from different language inputs to the same
simulation state. But there are many hurdles: To do this I have to make sure that the trace
stays infinite...
But there is a very good reason to let the semantics start with :
This way we can factor out the program, and let it be deterministic just on the Input.
In a more abstract vision on the other hand one would see Input and Program as dual objects,
This is circumvented here by just stating everything once for Src and once for Tgt,
as we always have exactly 2 Programs.
There could be some generalisation that would work on several "Programs"
- the same way we argue about several traces (on different Inputs) right now.
But this is currently waaaaay out of scope.
It would also come with new pitfalls:
in particular the TotalSynchroniser breaks the duality currently.
And just using two Synchroniser doesn't work without a further requirement of
always-eventually-in-sync.
*)
Class hyper_preserve_barrier_c2
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c2 : src_rel vl_zero;
tgt_rel_unit_c2 : tgt_rel vl_zero;
sim_rel_unit_c2 : forall i, sim_rel i [] [];
hpb_step_c2 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c2 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α)
}.
Section with_hpbc.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context (is_B : SrcSt -> bool).
Context (stb_live_B : forall i a, src_sem i a -> exists b0 bs, src_sem i (b0 :: bs ++ a) /\ is_B b0 = true).
Context `(HPBC : hyper_preserve_barrier_c (src_sem:=src_sem) (is_B:=is_B)).
(* Context `(HPBC : hyper_preserve_barrier_c).*)
Definition P_barrier (b : SrcSt * list SrcSt)
:= let (b0,bs) := b in
is_B b0 = true /\ Forall (fun x => is_B x = false) bs.
Lemma hpbc_hpb
: exists (bl_step : Input -> list SrcSt -> SrcSt * list SrcSt),
hyper_preserve_barrier i_vec
src_rel
tgt_rel
src_sem
tgt_sem
Rsrc
Rtgt
sim_rel
t_sync_i
t_next_i
TSi
P_barrier
bl_step.
Proof.
specialize (@bl_ex_step0 Input SrcSt _ _ state0 dec_SrcSt is_B) as Hex.
exploit' Hex.
specialize (stb_live_B) as Hlive.
destructH.
exists bl_step.
econstructor.
1,2,4: now destruct HPBC; eauto.
- intros.
eapply hpb_step_c with (b0:=fst (vec_unzip bp))
(bs:=snd (vec_unzip bp));eauto.
+ setoid_rewrite H7.
setoid_rewrite surjective_pairing at 1.
reflexivity.
+ eapply vec_Forall_forall.
rewrite vec_Forall_forall in H8.
intros.
rewrite vec_unzip_fst.
unfold P_barrier in H8.
setoid_rewrite Vector.nth_map. 2:reflexivity.
specialize (H8 i).
destruct (bp[[i]]). cbn.
firstorder.
+ rewrite vec_unzip_snd.
eapply vec_Forall_forall.
intros.
rewrite vec_Forall_forall in H8.
setoid_rewrite Vector.nth_map. 2:reflexivity.
specialize (H8 i). unfold P_barrier in H8.
destruct (bp[[i]]). cbn.
firstorder.
- intros.
unfold live_B_minimal_def' in Hex.
specialize (Hex i a).
destruct (bl_step i a).
unfold P_barrier.
firstorder.
- intros.
unfold live_B_minimal_def' in Hex.
specialize (Hex i a).
unfold bl_cons.
destruct (bl_step i a).
firstorder.
Qed.
End with_hpbc.
Class hyper_preserve_barrier_c3
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c3 : src_rel vl_zero;
tgt_rel_unit_c3 : tgt_rel vl_zero;
t_reach_c3 := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
sim_rel_unit_c3 : forall i, sim_rel i [] [];
hpb_step_c3 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c3 : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach_c3 i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
src_rel_div3 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
src_rel a
-> (forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
Class hyper_preserve_barrier_c5
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c5 : src_rel vl_zero;
tgt_rel_unit_c5 : tgt_rel vl_zero;
sim_rel_unit_c5 : forall i, sim_rel i [] [];
hpb_step_c5 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> Vector.Forall (fun x => is_B x = true) b0
-> Vector.Forall (Forall (fun s => is_B s = false)) bs
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c5 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α);
src_rel_div5 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
src_rel a
-> (forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
Class hyper_preserve_barrier_c7
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c7 : src_rel vl_zero;
tgt_rel_unit_c7 : tgt_rel vl_zero;
sim_rel_unit_c7 : forall i, sim_rel i [] [];
t_reach_c7 := fun (i : Input) (a α : list _) =>
@t_reachable _ _ (TSi i) (length a, length α);
hpb_step_c7 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> (forall j, is_B j a (b0[[j]]) = true)
-> (forall j, Forall (fun y => is_B j a y = false) (bs[[j]]))
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c7 : forall (i : Input) (a : list SrcSt) (α : list TgtSt),
t_reach_c7 i a α
-> src_sem i a
-> tgt_sem i α
-> sim_rel i a α;
(* sim_step_c7 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α);*)
src_rel_div7 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
(forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B i a s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
Class hyper_preserve_barrier_c9
(i_vec : Vector.t Input k)
(src_rel : Vector.t (list SrcSt) k -> Prop)
(tgt_rel : Vector.t (list TgtSt) k -> Prop)
(src_sem : Input -> list SrcSt -> Prop)
(tgt_sem : Input -> list TgtSt -> Prop)
(Rsrc : rad_semantics src_sem)
(Rtgt : rad_semantics tgt_sem)
(sim_rel : Input -> list SrcSt -> list TgtSt -> Prop)
(t_sync_i : Input -> nat -> nat)
(t_next_i : Input -> nat -> nat)
(TSi : forall (i : Input), TotalSynchroniser (t_sync_i i) (t_next_i i))
(is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool)
: Prop
:=
{
src_rel_unit_c9 : src_rel vl_zero;
tgt_rel_unit_c9 : tgt_rel vl_zero;
sim_rel_unit_c9 : forall i, sim_rel i [] [];
hpb_step_c9 : forall a : Vector.t (list SrcSt) k,
src_rel a
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> Vec_Forall3 sim_rel i_vec (b +vl+ a) (β +vl+ α)
-> forall b0 bs,
b = b0 :vl: bs
-> (forall j, is_B j a (b0[[j]]) = true)
-> (forall j, Forall (fun y => is_B j a y = false) (bs[[j]]))
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α);
sim_step_c9 : forall (i : Input) (a : list SrcSt) (α : list TgtSt) b β,
sim_rel i a α
-> src_sem i (b :: a)
-> tgt_sem i (β ++ α)
-> t_sync_i i (length a) = length β
-> sim_rel i (b :: a) (β ++ α);
src_rel_div9 : forall (a : Vector.t (list SrcSt) k) i,
(* if there is *one* trace that never visits a barrier again,
then this must be enough to show that the relation is fulfilled for all extensions *)
(forall b, src_sem (i_vec [[i]]) (b ++ a[[i]])
-> Forall (fun s => is_B i a s = false) b)
-> forall α : Vector.t (list TgtSt) k,
tgt_rel α
-> Vec_Forall3 sim_rel i_vec a α
-> forall b : Vector.t (list SrcSt) k,
Vector.Forall2 src_sem i_vec (b +vl+ a)
-> forall β : Vector.t (list TgtSt) k,
Vector.Forall2 tgt_sem i_vec (β +vl+ α)
-> src_rel (b +vl+ a) /\ tgt_rel (β +vl+ α)
}.
(* It might work afterall! ex_bl_Sync' gives me the Synchroniser (non-constructively).
Thus it is possible to instantiate HyperPreserve with this Synchroniser
The idea was to show that this is an instance of HyperPreserve withouth the live_B assumption.
the instantiation would set src_rel' := src_rel \/ no_barrier_ever etc.
I will *not* be able to show that this is an instance of HyperPreserve,
because I would have to construct a Synchroniser that declines from using is_B
when we are at point where no barrier is visited anymore.
But this is not decidable and Synchronisers reside in Type!
I can only decide on this point using classical reasoning
and I think there is a way to prove an analogon to hyper_preserve_AE
based on hyper_preserve_barrier_c3.
Which is all I need for Termination-Sensitive / "concurrent" Non-Interference.
But it will be a considerable effort and I am not sure if this should be the priority right now.
Alternatively, I could focus on termination-insensitive NI for now.
The approach sketched out here is actually quite general,
thus if successful, it should be fairly easy to adopt the proofs and get the sensitive results.
One could even argue that termination-insensitive NI is more practically relevant,
because termination-sensitive NI requires some reasoning about termination, which is hard.
I should check the literature how common which variant is.
On the other hand one could very much argue against it,
since we are observing traces and ideally we would want to argue about "concurrent" NI,
i.e. treating termination as an effect but also have a result for non-terminating programs.
In particular the whole development is made in a way to support infinite traces.
Another - rather ugly - fix would be to make my language terminate
after some arbitrary but finite "k".
This would make the synchroniser definable and we would argue that we may do this for any "k",
i.e. every finite prefix of "k"-step execution is safe, thus the whole program is kinda safe.
*)
Section with_hbpc3.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(hyper_preserve_barrier_c3 (src_sem:=src_sem) (is_B:=is_B)).
Lemma forall_or_fe_or (P Q : Fin.t k -> Prop)
(Hforall : forall x, P x \/ Q x)
: (forall x, P x) \/ exists x, Q x.
Proof.
clear - Hforall.
dependent induction k.
- left.
intros.
inversion x.
- specialize (Hforall (@Fin.F1 n)) as R.
destruct R.
+ specialize (IHn (fun x => P (Fin.FS x)) (fun x => Q (Fin.FS x))).
exploit' IHn.
destruct IHn.
* left.
intros.
dependent destruction x;eauto.
* right.
destructH.
eexists;eauto.
+ right.
eexists;eauto.
Qed.
Lemma vec_Forall2_or {j : nat} {X Y : Type} (P Q : X -> Y -> Prop) (xt yt : Vector.t _ j)
(Hor : forall x y, P x y \/ Q x y)
: Vector.Forall2 P xt yt \/ exists i, Q (xt[[i]]) (yt[[i]]).
clear - Hor.
Proof.
dependent induction xt; dependent destruction yt.
- left.
rewrite <-x.
econstructor.
- subst n0.
subst yt0.
eapply IHxt in Hor as R.
destruct R.
+ specialize (Hor h h0) as T.
destruct T.
* left.
econstructor;eauto.
* right.
exists (Fin.F1).
cbn.
assumption.
+ right.
destruct H as [i H'].
exists (Fin.FS i).
cbn.
assumption.
Qed.
Lemma hpbc_hpb3
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
specialize (@bl_ex_step_or0 _ _ _ _ state0 dec_SrcSt is_B) as Q.
destructH.
specialize (ex_bl_sync' (k:=k) bl_step' (fun i a => exists b0 bs, src_sem i (b0 :: bs ++ (construct_trace src_sem a i)) /\ is_B b0 = true)) as T.
destructH.
exists bl_sync'.
exists (T1 i_vec).
econstructor.
- eapply src_rel_unit_c3.
- eapply tgt_rel_unit_c3.
- intros.
eapply vec_Forall2_or with (xt:=i_vec) (yt:=a) in Q.
destruct Q as [Q|Q].
+ unfold live_B_minimal_def' in Q.
pose (b0:=fst (vec_unzip (Vector.map2 (fun (i : Input) (a : list SrcSt) => bl_step' i a) i_vec a))).
pose (bs:=snd (vec_unzip (Vector.map2 (fun (i : Input) (a : list SrcSt) => bl_step' i a) i_vec a))).
eapply hpb_step_c3 with (b0:=b0) (bs:=bs);eauto.
* eapply vec_forall3_forall.
intros.
rename H3 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c3.
-- unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply vec_forall3_forall.
intros.
rename H6 into Hsim'.
rewrite vec_forall3_forall in Hsim'.
eapply sim_step_c3.
-- unfold vl_len in Hsim'.
specialize (Hsim' i).
setoid_rewrite Vector.nth_map in Hsim'. 2,3:reflexivity.
eapply Hsim'.
-- eapply Vec_Forall2_forall2;eauto.
-- eapply Vec_Forall2_forall2;eauto.
* eapply bl_sync_cons_eq with (bl_step:=bl_step') in H4;eauto.
-- rewrite H4.
subst b0 bs.
destruct (vec_unzip (Vector.map2 (fun (i : Input) (a0 : list SrcSt) => bl_step' i a0)
i_vec a)).
cbn.
reflexivity.
-- eapply Vec_Forall2_forall2;intros.
eapply Vec_Forall2_forall2 with (i:=i) in Q.
unfold bl_cons.
destruct (bl_step' (i_vec [[i]]) (a[[i]])).
eapply Q in H8.
destruct H8.
assumption.
-- rewrite H7.
specialize (T0 i_vec (vl_len a)).
eapply Vector.eq_nth_iff.
intros.
subst p2.
eapply vec_forall3_forall with (i:=p1) in T0.
destruct T0 as [T0 _].
rewrite T0.
++ unfold bl_sync.
rewrite Vec_nth_map2.
reflexivity.
++ eapply Vec_Forall2_forall2 with (i:=p1) in Q.
destruct (bl_step' (i_vec [[p1]]) (a [[p1]])) as [b1 bs0].
exists b1, bs0.
eapply Vec_Forall2_forall2 with (i:=p1) in H4.
setoid_rewrite Vec_nth_map2 in H4.
eapply sem_safe_app in H4;eauto.
eapply Q in H4 as H4'.
split.
** setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite construct_trace_length.
eapply H4';eauto.
eapply H4.
** eapply H4'.
* eapply vec_Forall_forall.
intros.
subst b0.
rewrite vec_unzip_fst.
setoid_rewrite Vector.nth_map with (p1:=i). 2:reflexivity.
setoid_rewrite Vec_nth_map2.
eapply Vec_Forall2_forall2 with (i:=i) in Q.
destruct (bl_step' (i_vec [[i]]) (a[[i]])).
cbn.
eapply Vec_Forall2_forall2 with (i:=i) in H4.
setoid_rewrite Vec_nth_map2 in H4.
eapply sem_safe_app in H4;eauto.
eapply Q in H4.
eapply H4.
* eapply vec_Forall_forall.
intros.
subst bs.
setoid_rewrite vec_unzip_snd.
setoid_rewrite Vector.nth_map with (p1:=i). 2:reflexivity.
setoid_rewrite Vec_nth_map2.
eapply Vec_Forall2_forall2 with (i:=i) in Q.
destruct (bl_step' (i_vec [[i]]) (a[[i]])).
cbn.
eapply Vec_Forall2_forall2 with (i:=i) in H4.
setoid_rewrite Vec_nth_map2 in H4.
eapply sem_safe_app in H4;eauto.
eapply Q in H4.
eapply H4.
+ destructH.
eapply src_rel_div3;eauto.
* eapply vec_forall3_forall.
intros.
rename H3 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c3.
-- unfold vl_len in Hsim.
specialize (Hsim i0).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply vec_forall3_forall.
intros.
rename H6 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c3.
-- unfold vl_len in Hsim.
specialize (Hsim i0).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2;eauto.
-- eapply Vec_Forall2_forall2;eauto.
Qed. (* TODO tidy up this ugly mess *)
End with_hbpc3.
Section with_hpbc2.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context (stb_live_B : forall i a, src_sem i a -> exists b0 bs, src_sem i (b0 :: bs ++ a) /\ is_B b0 = true).
Context `(HPBC : hyper_preserve_barrier_c2 (src_sem:=src_sem) (is_B:=is_B)).
Definition P_barrier2 (b : SrcSt * list SrcSt)
:= let (b0,bs) := b in
is_B b0 = true /\ Forall (fun x => is_B x = false) bs.
Lemma hpbc_hpb2
: exists (bl_step : Input -> list SrcSt -> SrcSt * list SrcSt),
hyper_preserve_barrier i_vec
src_rel
tgt_rel
src_sem
tgt_sem
Rsrc
Rtgt
sim_rel
t_sync_i
t_next_i
TSi
P_barrier2
bl_step.
Proof.
eapply hpbc_hpb;eauto.
destruct HPBC.
econstructor;eauto.
clear - Rsrc Rtgt sim_step_c4 sim_rel_unit_c4.
eapply sim_step_to_reach;eauto.
Qed.
End with_hpbc2.
Section with_hpbc7.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(HPBC : hyper_preserve_barrier_c7 (src_sem:=src_sem) (is_B:=is_B)).
Lemma hpbc_hpb7
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
specialize (@bl_ex_step_or2 _ _ _ _ _ is_B state0 dec_SrcSt) as Q.
destructH.
pose (vbl_step' := (fun iv a => vec_mapi (fun j i => bl_step' j i a) iv)).
specialize (@vex_bl_sync' k Input SrcSt src_sem Rsrc vbl_step'
(fun i (vn : vecnat k) =>
let a := (Vector.map2 (construct_trace src_sem) vn i) in
exists b0 bs, Vector.Forall2 src_sem i (b0 :vl: bs +vl+ a)
/\ forall j, is_B j a (b0[[j]]) = true)) as T.
destructH.
exists bl_sync'.
exists (T1 i_vec).
econstructor.
- eapply src_rel_unit_c7.
- eapply tgt_rel_unit_c7.
- intros.
unfold live_or_not in Q.
specialize (Q i_vec a).
eapply forall_or_fe_or in Q.
destruct Q as [Q|Q].
+ unfold live_B_minimal_def' in Q.
eapply Forall2_vl_app22 in H3 as H3';eauto.
2:eapply sem_prefix_containing;eauto.
pose (b0:=fst (vec_unzip (vbl_step' i_vec a))).
pose (bs:=snd (vec_unzip (vbl_step' i_vec a))).
eapply hpb_step_c7 with (b0:=b0) (bs:=bs);eauto.
* eapply vec_forall3_forall.
intros.
rename H2 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c7.
-- unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
* eapply vec_forall3_forall.
intros.
rename H5 into Hsim'.
rewrite vec_forall3_forall in Hsim'.
eapply sim_step_c7.
-- unfold vl_len in Hsim'.
specialize (Hsim' i).
setoid_rewrite Vector.nth_map in Hsim'. 2,3:reflexivity.
eapply Hsim'.
-- eapply Vec_Forall2_forall2;eauto.
-- eapply Vec_Forall2_forall2;eauto.
* setoid_rewrite vbl_sync_cons_eq with (bl_step:=vbl_step') at 1.
2,4:eauto.
-- setoid_rewrite surjective_pairing.
subst b0 bs.
reflexivity.
-- eapply Vec_Forall2_forall2;intros.
unfold vbl_cons.
setoid_rewrite Vector.nth_map2 with (p2:=i) (p3:=i). 2,3:reflexivity.
setoid_rewrite Vector.nth_map. 2:reflexivity.
specialize (Q i).
subst vbl_step'.
setoid_rewrite vec_mapi_nth.
destruct (bl_step' i (i_vec[[i]]) a).
exploit Q.
++ eapply Vec_Forall2_forall2;eauto.
++ cbn.
eapply Q.
-- rewrite H6.
specialize (T0 i_vec (vl_len a)).
destructH.
cbn in *.
eapply T2.
exists b0, bs.
split.
++ eapply Vec_Forall2_forall2;eauto.
intros.
specialize (Q i).
subst b0 bs.
unfold vbl_step'.
setoid_rewrite Vector.nth_map2. 2,3:reflexivity.
setoid_rewrite Vector.nth_map2. 2-5:reflexivity.
setoid_rewrite vec_unzip_fst.
setoid_rewrite vec_unzip_snd.
setoid_rewrite Vector.nth_map. 2-4:reflexivity.
setoid_rewrite vec_mapi_nth.
destruct (bl_step' i (i_vec[[i]]) a).
cbn.
setoid_rewrite construct_trace_length.
eapply Q.
all: eapply Vec_Forall2_forall2;eauto.
++ intros.
specialize (Q j).
subst b0.
unfold vbl_step'.
rewrite vec_unzip_fst.
setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite vec_mapi_nth.
destruct (bl_step' j (i_vec[[j]]) a).
cbn.
replace (Vector.map2 (construct_trace src_sem) (vl_len a) i_vec)
with a;cycle 1.
{
eapply Vector.eq_nth_iff.
intros.
subst p2.
setoid_rewrite Vector.nth_map2. 2,3:reflexivity.
setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite construct_trace_length;eauto.
eapply Vec_Forall2_forall2;eauto.
}
eapply Q.
eapply Vec_Forall2_forall2;eauto.
-- eauto.
* intros.
subst b0.
rewrite vec_unzip_fst.
setoid_rewrite Vector.nth_map with (p1:=j). 2:reflexivity.
unfold vbl_step'.
setoid_rewrite vec_mapi_nth.
specialize (Q j).
destruct (bl_step' j (i_vec[[j]]) a).
cbn.
eapply Q.
eapply Vec_Forall2_forall2;eauto.
* intros.
subst bs.
setoid_rewrite vec_unzip_snd.
setoid_rewrite Vector.nth_map with (p1:=j). 2:reflexivity.
unfold vbl_step'.
rewrite vec_mapi_nth.
specialize (Q j).
destruct (bl_step' j (i_vec [[j]]) a).
cbn.
eapply Q.
eapply Vec_Forall2_forall2;eauto.
+ destructH.
eapply src_rel_div7;eauto.
eapply vec_forall3_forall.
intros.
rename H2 into Hsim.
rewrite vec_forall3_forall in Hsim.
eapply sim_step_c7.
-- unfold vl_len in Hsim.
specialize (Hsim i).
setoid_rewrite Vector.nth_map in Hsim. 2,3:reflexivity.
eapply Hsim.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
-- eapply Vec_Forall2_forall2.
eapply Forall2_vl_app22;eauto.
eapply sem_prefix_containing;eauto.
Qed.
End with_hpbc7.
Section with_hpbc9.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : Fin.t k -> Vector.t (list SrcSt) k -> SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(HPBC : hyper_preserve_barrier_c9 (src_sem:=src_sem) (is_B:=is_B)).
Lemma hpbc_hpb9
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
eapply hpbc_hpb7;eauto.
destruct HPBC.
econstructor;eauto.
clear - Rsrc Rtgt sim_step_c10 sim_rel_unit_c10.
eapply sim_step_to_reach;eauto.
Qed.
End with_hpbc9.
Section with_hpbc5.
Import BarrierSyncChoice.
Context (src_sem : Input -> list SrcSt -> Prop).
Context (is_B : SrcSt -> bool).
Context (state0 : SrcSt).
Context (dec_SrcSt : forall x y : SrcSt, {x = y} + {x <> y}).
Context `(HPBC : hyper_preserve_barrier_c5 (src_sem:=src_sem) (is_B:=is_B)).
Lemma hpbc_hpb5
: exists (bl_sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
syn,
hyper_preserve
i_vec
src_rel
tgt_rel
src_sem
tgt_sem
t_sync_i
t_next_i
_
(sync:=bl_sync i_vec)
(next:=fun _ _ => 1)
syn.
Proof.
eapply hpbc_hpb3;eauto.
destruct HPBC.
econstructor;eauto.
clear - Rsrc Rtgt sim_step_c6 sim_rel_unit_c6.
eapply sim_step_to_reach;eauto.
Qed.
End with_hpbc5.
End with_k_st.
(*
Goal forall a, forall i, exists n, d (n_steps (S n) a [i]).
Abort.
Goal forall a, (forall i, exists n, d (n_steps n a[i])) \/ (forall i n, ~ d (n_steps n a[i])).
Abort.
Goal forall a, forall i, (exists n, d (n_steps n a[i])) \/ (forall n, ~ d (n_steps n a[i])).
Abort.
Goal forall a, exists vn, vd (n_steps n a). (* Problem: which one is the next ? the vecnats are not sorted in general *)
Abort.
Goal forall a, (exists vn, vd (n_steps n a)) \/ (forall vn, ~ vd (n_steps n a)).
Abort.
*)