From c8c21c205b085ac0e33053e9d84dd678f017eaa6 Mon Sep 17 00:00:00 2001 From: Ilya Sergey Date: Wed, 7 Jun 2017 20:02:57 +0100 Subject: [PATCH 1/3] changed semantics of processes --- Core/Always.v | 50 +-- Core/HoareTriples.v | 28 +- Core/InferenceRules.v | 4 +- Core/Process.v | 134 ++++---- Core/Process1.v | 697 ++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 803 insertions(+), 110 deletions(-) create mode 100644 Core/Process1.v diff --git a/Core/Always.v b/Core/Always.v index f7986a2..77ddda1 100644 --- a/Core/Always.v +++ b/Core/Always.v @@ -17,19 +17,19 @@ Unset Printing Implicit Defensive. Section Always. -Variable this : nid. Variable W : world. +Variable this : nid. Notation coherent := (Coh W). -Implicit Arguments proc [W this]. +Implicit Arguments proc [W]. Fixpoint always_sc A (s1 : state) p scs (P : state -> proc A -> Prop) : Prop := s1 \In coherent /\ if scs is sc :: scs' then forall s2, network_rely W this s1 s2 -> - [/\ safe p sc s2, P s2 p & - forall s3 q, @pstep this W A s2 p sc s3 q -> always_sc s3 q scs' P] + [/\ safe p this sc s2, P s2 p & + forall s3 q, @pstep W A s2 p this sc s3 q -> always_sc s3 q scs' P] else forall s2, network_rely W this s1 s2 -> P s2 p. Definition always A s (p : proc A) P := forall scs, always_sc s p scs P. @@ -45,13 +45,13 @@ Lemma alw_coh A s (p : proc A) P : Proof. by move/(_ [::]); move/alw_coh'. Qed. Lemma alw_safe' A s (p : proc A) sc scs P : - always_sc s p (sc :: scs) P -> safe p sc s. + always_sc s p (sc :: scs) P -> safe p this sc s. Proof. by case: scs=>[|a l][]C/(_ s (rely_refl this C))[]. Qed. Lemma alw_safe A s (p : proc A) P : - always s p P -> forall sc, safe p sc s. + always s p P -> forall sc, safe p this sc s. Proof. by move=>H sc; apply: alw_safe' (H [:: sc]). Qed. Lemma alw_refl' A s (p : proc A) sc P : always_sc s p sc P -> P s p. @@ -76,7 +76,7 @@ Proof. by move=>S E scs; apply: alw_envs' (S scs) E. Qed. (* Always is preserved by this-stepping *) Lemma alw_step A s1 (p : proc A) sc s2 q P : - always s1 p P -> pstep s1 p sc s2 q -> always s2 q P. + always s1 p P -> pstep s1 p this sc s2 q -> always s2 q P. Proof. move=>Ls Ts; move: (Ls [:: sc])=>/= [C]. case/(_ _ (rely_refl this C))=>_ _; move/(_ _ _ Ts)=>_. @@ -139,14 +139,14 @@ Proof. by move=>C H ps; apply: alw_ret'. Qed. Lemma alw_act A s1 (a : action W A this) (P : state -> proc A -> Prop) : s1 \In coherent -> (forall s2, network_rely W this s1 s2 -> exists S : a_safe a s2, - P s2 (Act a) /\ + P s2 (Act this a) /\ forall s3 v s4, a_step S s3 v -> network_rely W this s3 s4 -> P s4 (Ret v)) -> - always s1 (Act a) P. + always s1 (Act this a) P. Proof. move=>C H [|sc scs]; split=>// s2; case/H=>// H1[H2]H3//. split=>//; first by case: sc. -move=>s3 q /stepAct [v][pf][_ -> St]. +move=>s3 q /stepAct [v][pf][_ -> _ St]. rewrite (proof_irrelevance H1 pf) in H3. apply: alw_ret'; last by move=>s4; apply: H3 St. by case: (step_coh (a_step_sem St)). @@ -262,7 +262,7 @@ split=>//; last first. by move/(_ _ _ _ T)/IH; apply; exists k. move/(alw_envs Ls): E=>{Ls} Ls. have Ls': always s2 p1 (fun s2 p2 => - forall sc p v, p2 = Ret v -> p \In pp2 v -> safe p sc s2). + forall sc p v, p2 = Ret v -> p \In pp2 v -> safe p this sc s2). - by apply: alw_imp Ls=>s p _ I sc' q v E; move/(I _ _ E)/alw_safe. case: sc=>//=; first by case: p1 {Ls} Ls'. move=>sc; case: (Ls [:: sc])=>C. @@ -388,11 +388,11 @@ Qed. -Lemma alw_inject (p : proc this V A) - (P : state -> proc this V A -> Prop) i j : +Lemma alw_inject (p : proc V A) + (P : state -> proc V A -> Prop) i j : i \+ j \In Coh W -> - always i p P -> - always (i \+ j) (Inject w p) + always this i p P -> + always this (i \+ j) (Inject w p) (fun m q => exists i' j', [/\ m = i' \+ j', i' \In Coh V, network_rely W2 this j j' & (exists q', q = Inject w q' /\ P i' q') \/ @@ -433,10 +433,10 @@ move=>s p _ [i2][j2][->{s}] Ci2 S2 H; exists i2, j2; split=>//. by apply: rely_trans S1 S2. Qed. -Lemma aft_inject (p : proc this V A) (P : A -> state -> Prop) i j : +Lemma aft_inject (p : proc V A) (P : A -> state -> Prop) i j : i \+ j \In Coh W -> - after i p P -> - after (i \+ j) (Inject w p) + after this i p P -> + after this (i \+ j) (Inject w p) (fun v m => exists i' j', [/\ m = i' \+ j', i' \In Coh V, network_rely W2 this j j' & P v i']). @@ -471,11 +471,11 @@ Variables (A : Type) (this: nid). Notation V := (mkWorld pr). Notation W := (mkWorld (ProtocolWithIndInv ii)). -Lemma alw_ind_inv (p : proc this V A) - (P : state -> proc this V A -> Prop) i : +Lemma alw_ind_inv (p : proc V A) + (P : state -> proc V A -> Prop) i : i \In Coh W -> - always i p P -> - always i (WithInv pr I ii (erefl _) p) + always this i p P -> + always this i (WithInv pr I ii (erefl _) p) (fun m q => m \In Coh W /\ ((exists q', q = WithInv pr I ii (erefl _) q' /\ P m q') \/ (exists v', q = Ret v' /\ P m (Ret v')))). @@ -503,10 +503,10 @@ move/(alw_step Ls'): T=>{Ls'} Ls'. by apply: IH. Qed. -Lemma aft_ind_inv (p : proc this V A) (P : A -> state -> Prop) i : +Lemma aft_ind_inv (p : proc V A) (P : A -> state -> Prop) i : i \In Coh W -> - after i p P -> - after i (WithInv pr I ii (erefl _) p) + after this i p P -> + after this i (WithInv pr I ii (erefl _) p) (fun v m => m \In Coh W /\ P v m). Proof. move=>C /(alw_ind_inv C); apply: alw_imp=>{p i C} s q _. diff --git a/Core/HoareTriples.v b/Core/HoareTriples.v index 38f8f7e..d533c60 100644 --- a/Core/HoareTriples.v +++ b/Core/HoareTriples.v @@ -16,7 +16,7 @@ Unset Printing Implicit Defensive. (* Program is a set of processes *) Structure prog (W : world) A (this : nid) := Prog { - set_of : proc this W A -> Prop; + set_of : proc W A -> Prop; (* Unifinshed is a bottom element that should be present *) _ : set_of Unfinished }. @@ -55,7 +55,7 @@ Definition spec A := prod pre (post A). Definition has_spec (s : spec A) := [Pred T : prog W A this | forall i t, - s.1 i -> i \In Coh W -> t \In T -> after i t (s.2 i)]. + s.1 i -> i \In Coh W -> t \In T -> after this i t (s.2 i)]. End Programs. @@ -128,7 +128,7 @@ This is the main predicate defining what the verification is: Definition verify (W : world) A (i : state) (e : DT W A) r := i \In Coh W -> - forall p, p \In DTbin.prog_of (code_of e) -> after i p r. + forall p, p \In DTbin.prog_of (code_of e) -> after this i p r. End Specs. @@ -160,8 +160,8 @@ by apply/stsepE/progE; apply: poset_asym H1 H2. Qed. -Definition bot_set t := t = @Unfinished this W A. -Definition bot_prg := @Prog _ _ _ bot_set (erefl _). +Definition bot_set t := t = @Unfinished W A. +Definition bot_prg := @Prog _ _ this bot_set (erefl _). (* Bottom satisfies any specification *) Lemma bot_spec : bot_prg \In has_spec this W s. @@ -175,7 +175,7 @@ Proof. by case: e=>[[p U] H] t ->. Qed. Definition sup_set (es : Pred (DTbin s)) t := t = Unfinished \/ exists e : DTbin s, t \In DTbin.prog_of e /\ e \In es. -Definition sup_prog es := @Prog _ _ _ (sup_set es) (or_introl (erefl _)). +Definition sup_prog es := @Prog _ _ this (sup_set es) (or_introl (erefl _)). Lemma sup_spec es : sup_prog es \In has_spec this W s. Proof. @@ -245,10 +245,10 @@ Variable W : world. Variables (A : Type) (x : A). (* Trees inhabiting a return statement *) -Definition ret_set t := t = Unfinished \/ t = @Ret this W A x. +Definition ret_set t := t = Unfinished \/ t = @Ret W A x. (* It naturally has the unfinished statement *) -Definition ret_prog := @Prog _ _ _ ret_set (or_introl (erefl _)). +Definition ret_prog := @Prog _ _ this ret_set (or_introl (erefl _)). Definition ret_s : spec A := (fun i => True, fun i y m => network_rely W this i m /\ y = x). @@ -271,8 +271,8 @@ Variable W : world. Variables (A : Type) (x : A). Variable a : action W A this. -Definition act_set t := t = Unfinished \/ t = @Act this W A a. -Definition act_prog := @Prog _ _ _ act_set (or_introl (erefl _)). +Definition act_set t := t = Unfinished \/ t = @Act W A this a. +Definition act_prog := @Prog _ _ this act_set (or_introl (erefl _)). (* Relaxing the precondition with respect to the rely, via action's safety *) Definition act_s : spec A := @@ -305,7 +305,7 @@ Variables (T : prog W A this) (K : A -> prog W B this). Definition bnd_set t := t = Unfinished \/ exists t', t \In pcat t' K /\ t' \In T. -Definition bnd_prog := @Prog _ _ _ bnd_set (or_introl (erefl _)). +Definition bnd_prog := @Prog _ _ this bnd_set (or_introl (erefl _)). End Prog. @@ -362,7 +362,7 @@ Variable T : prog V A this. Definition inject_set t := t = Unfinished \/ exists t', t' \In T /\ t = Inject w t'. -Definition inject_prog := @Prog _ _ _ inject_set (or_introl (erefl _)). +Definition inject_prog := @Prog _ _ this inject_set (or_introl (erefl _)). End Prog. Definition inject_s : spec A := @@ -375,7 +375,7 @@ Lemma inject_has_spec : inject_prog (code_of e) \In has_spec this W inject_s. Proof. move=>i /= t [i1][j1][->{i}][Ci1 H1] C. case=>[|[t' [H2 ->{t}]]]; first by move=>->; apply: alw_unfin. -have : after i1 t' (s.2 i1) by case: (code_of e) H2=>p /= /(_ _ _ H1); apply. +have : after this i1 t' (s.2 i1) by case: (code_of e) H2=>p /= /(_ _ _ H1); apply. move/(aft_inject w C); apply: aft_imp=>{H1 t' H2} v m _. case=>i2 [j2][->{m} Ci2 S2 H2] i3 j3 E Ci3. suff [E1 E2]: i3 = i1 /\ j3 = j1. @@ -414,7 +414,7 @@ Variable T : prog V A this. Definition with_inv_set t := t = Unfinished \/ exists t', t' \In T /\ t = WithInv pr I ii (erefl _) t'. -Definition with_inv_prog := @Prog _ _ _ with_inv_set (or_introl (erefl _)). +Definition with_inv_prog := @Prog _ _ this with_inv_set (or_introl (erefl _)). End Prog. Notation getS i := (getStatelet i l). diff --git a/Core/InferenceRules.v b/Core/InferenceRules.v index e78feb2..5c8397d 100644 --- a/Core/InferenceRules.v +++ b/Core/InferenceRules.v @@ -149,8 +149,8 @@ Lemma ghC (p : B -> pre) (q : B -> A -> pre) : (forall i x, p x i -> i \In Coh W -> verify i e (q x)) -> conseq e (logvar (fun x => binarify (p x) (q x))). Proof. -move=>H i /= [x Hp] Ci t Ht. -have S : alwsafe i t by apply: alw_imp (H i x Hp Ci Ci t Ht). +move=>H i /= [x Hp] Ci t Ht. +have S: (always this i t (fun _ _ => True)) by apply: alw_imp (H i x Hp Ci Ci t Ht). by apply/aftA=>// y; apply/aftI=>// /H; apply. Qed. diff --git a/Core/Process.v b/Core/Process.v index a5d6b70..35dd567 100644 --- a/Core/Process.v +++ b/Core/Process.v @@ -15,15 +15,13 @@ Unset Printing Implicit Defensive. Section ProcessSyntax. -Variable this : nid. - (* Syntax for process *) Inductive proc (W : world) A := - Unfinished | Ret of A | Act of action W A this | + Unfinished | Ret of A | Act (this : nid) of action W A this | Seq B of proc W B & B -> proc W A | Inject V K of injects V W K & proc V A | WithInv p I (ii : InductiveInv p I) of - W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A. + W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A. Definition pcat W A B (t : proc W A) (k : A -> Pred (proc W B)) := [Pred s | exists q, s = Seq t q /\ forall x, q x \In k x]. @@ -35,21 +33,19 @@ Inductive schedule := End ProcessSyntax. -Implicit Arguments Unfinished [this W A]. -Implicit Arguments Ret [this W A]. -Implicit Arguments Act [this W A]. -Implicit Arguments Seq [this W A B]. -Implicit Arguments WithInv [this W A]. +Implicit Arguments Unfinished [W A]. +Implicit Arguments Ret [W A]. +Implicit Arguments Act [W A]. +Implicit Arguments Seq [W A B]. +Implicit Arguments WithInv [W A]. Section ProcessSemantics. -Variable this : nid. - -Fixpoint step (W : world) A (s1 : state) (p1 : proc this W A) - sc (s2 : state) (p2 : proc this W A) : Prop := +Fixpoint step (W : world) A (s1 : state) (p1 : proc W A) + sc (s2 : state) (p2 : proc W A) : Prop := match sc, p1 with (* Action - make a step *) - | ActStep, Act a => exists v pf, @a_step _ _ _ a s1 pf s2 v /\ p2 = Ret v + | ActStep, Act this a => exists v pf, @a_step _ _ this a s1 pf s2 v /\ p2 = Ret v (* Sequencing - apply a continuation *) | SeqRet, Seq _ (Ret v) k => s2 = s1 /\ p2 = k v | SeqStep sc', Seq _ p' k1 => @@ -70,9 +66,9 @@ Fixpoint step (W : world) A (s1 : state) (p1 : proc this W A) | _, _ => False end. -Fixpoint good (W : world) A (p : proc this W A) sc : Prop := +Fixpoint good (W : world) A (p : proc W A) sc : Prop := match sc, p with - | ActStep, Act _ => True + | ActStep, Act _ _ => True | SeqRet, Seq _ (Ret _) _ => True | SeqStep sc', Seq _ p' _ => good p' sc' | InjectStep sc', Inject _ _ _ p' => good p' sc' @@ -94,29 +90,28 @@ structure. Once it's dropped, this structure is lost. *) -Fixpoint safe (W : world) A (p : proc this W A) sc (s : state) : Prop := +Fixpoint safe (W : world) A (p : proc W A) (this : nid) sc (s : state) : Prop := match sc, p with - | ActStep, Act a => a_safe a s + | ActStep, Act n a => n == this /\ @a_safe _ _ n a s | SeqRet, Seq _ (Ret _) _ => True - | SeqStep sc', Seq _ p' _ => safe p' sc' s + | SeqStep sc', Seq _ p' _ => safe p' this sc' s | InjectStep sc', Inject V K pf p' => - exists s', extends pf s s' /\ safe p' sc' s' + exists s', extends pf s s' /\ safe p' this sc' s' | InjectRet, Inject V K pf (Ret _) => exists s', extends pf s s' - | WithInvStep sc', WithInv _ _ _ _ p' => safe p' sc' s + | WithInvStep sc', WithInv _ _ _ _ p' => safe p' this sc' s | WithInvRet, WithInv _ _ _ _ (Ret _) => True | _, _ => True end. -Definition pstep (W : world) A s1 (p1 : proc this W A) sc s2 p2 := - [/\ s1 \In Coh W, safe p1 sc s1 & step s1 p1 sc s2 p2]. +Definition pstep (W : world) A s1 (p1 : proc W A) this sc s2 p2 := + [/\ s1 \In Coh W, safe p1 this sc s1 & step s1 p1 sc s2 p2]. (* Some sanity lemmas wrt. stepping *) -Lemma pstep_safe (W : world) A s1 (t : proc this W A) sc s2 q : - pstep s1 t sc s2 q -> safe t sc s1. +Lemma pstep_safe (W : world) A s1 (t : proc W A) this sc s2 q : + pstep s1 t this sc s2 q -> safe t this sc s1. Proof. by case. Qed. - (* The following lemma established the operational "progress" property: a @@ -124,27 +119,27 @@ program, which is safe and also the schedule is appropriate. Together, this implies that we can do a step. *) -Lemma proc_progress W A s (p : proc this W A) sc : - s \In Coh W -> safe p sc s -> good p sc -> - exists s' (p' : proc this W A), pstep s p sc s' p'. +Lemma proc_progress W A s (p : proc W A) this sc : + s \In Coh W -> safe p this sc s -> good p sc -> + exists s' (p' : proc W A), pstep s p this sc s' p'. Proof. -move=>C H1 H2; elim: sc W A s p H2 H1 C=>[||sc IH|sc IH||sc IH|]W A s. -- case=>//=a _/= H; move/a_step_total: (H)=>[s'][r]H'. +move=>C H1 H2; elim: sc W A this s p H2 H1 C=>[||sc IH|sc IH||sc IH|]W A this s. +- case=>//=n a _/= [E H]; move/a_step_total: (H)=>[s'][r]H'. by exists s', (Ret r); split=>//=; exists r, H. - by case=>//; move=>B p k/=; case: p=>//b _ _; exists s, (k b). - case=>//B p k/=H1 H2 C. - case: (IH W B s p H1 H2 C)=>s'[p'][G1 G2]. + case: (IH W B this s p H1 H2 C)=>s'[p'][G1 G2]. by exists s', (Seq p' k); split=>//; exists p'. - case=>// V K pf p/=H1 [z][E]H2 C. case: (E)=>s3[Z] C1 C2. - case: (IH V A z p H1 H2 C1) =>s'[p']H3; case: H3=>S St. + case: (IH V A this z p H1 H2 C1) =>s'[p']H3; case: H3=>S St. exists (s' \+ s3), (Inject pf p'); split=>//; first by exists z. by subst s; exists z, s', s3, p'. - case=>//V K pf; case=>// v/=_[s'] E C. by exists s, (Ret v); split=>//=; exists s'. - case=>//pr I ii E p/= H1 H2 C. have C' : s \In Coh (mkWorld pr) by subst W; apply: (with_inv_coh C). - case: (IH (mkWorld pr) A s p H1 H2 C')=>s'[p']H3. + case: (IH (mkWorld pr) A this s p H1 H2 C')=>s'[p']H3. exists s', (WithInv pr I ii E p'); split=>//=. by exists p'; split=>//; case: H3. - case=>//pr I ii E; case=>//v/=_ _ C. @@ -153,29 +148,29 @@ Qed. (* Some view lemmas for processes and corresponding schedules *) -Lemma stepUnfin W A s1 sc s2 (t : proc this W A) : - pstep s1 Unfinished sc s2 t <-> False. +Lemma stepUnfin W A s1 this sc s2 (t : proc W A) : + pstep s1 Unfinished this sc s2 t <-> False. Proof. by split=>//; case; case: sc. Qed. -Lemma stepRet W A s1 sc s2 (t : proc this W A) v : - pstep s1 (Ret v) sc s2 t <-> False. +Lemma stepRet W A s1 this sc s2 (t : proc W A) v : + pstep s1 (Ret v) this sc s2 t <-> False. Proof. by split=>//; case; case: sc. Qed. -Lemma stepAct W A s1 a sc s2 (t : proc this W A) : - pstep s1 (Act a) sc s2 t <-> - exists v pf, [/\ sc = ActStep, t = Ret v & @a_step _ _ _ a s1 pf s2 v]. +Lemma stepAct W A s1 n this a sc s2 (t : proc W A) : + pstep s1 (Act n a) this sc s2 t <-> + exists v pf, [/\ sc = ActStep, t = Ret v, n == this & @a_step _ _ _ a s1 pf s2 v]. Proof. -split; first by case=>C; case: sc=>//= c [v [pf [H ->]]]; exists v, pf. +split; first by case=>C; case: sc=>//= [[G c]][v [pf [H ->]]]; exists v, pf. case=>v[pf] [->-> H]; split=>//; last by exists v, pf. by apply: (a_safe_coh pf). Qed. -Lemma stepSeq W A B s1 (t : proc this W B) k sc s2 (q : proc this W A) : - pstep s1 (Seq t k) sc s2 q <-> +Lemma stepSeq W A B s1 (t : proc W B) k this sc s2 (q : proc W A) : + pstep s1 (Seq t k) this sc s2 q <-> (exists v, [/\ sc = SeqRet, t = Ret v, q = k v, s2 = s1 & s1 \In Coh W]) \/ exists sc' p', - [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t sc' s2 p']. + [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t this sc' s2 p']. Proof. split; last first. - case; first by case=>v [->->->->]. @@ -186,8 +181,8 @@ by move=>G /= [p' [H1 ->]]; right; exists sc, p'. Qed. Lemma stepInject V W K A (em : injects V W K) - s1 (t : proc this V A) sc s2 (q : proc this W A) : - pstep s1 (Inject em t) sc s2 q <-> + s1 (t : proc V A) this sc s2 (q : proc W A) : + pstep s1 (Inject em t) this sc s2 q <-> (* Case 1 : stepped to the final state s1' of the inner program*) (exists s1' v, [/\ sc = InjectRet, t = Ret v, q = Ret v, s2 = s1 & extends em s1 s1']) \/ @@ -195,7 +190,7 @@ Lemma stepInject V W K A (em : injects V W K) exists sc' t' s1' s2' s, [/\ sc = InjectStep sc', q = Inject em t', s1 = s1' \+ s, s2 = s2' \+ s, s1 \In Coh W & - pstep s1' t sc' s2' t']. + pstep s1' t this sc' s2' t']. Proof. split; last first. - case. @@ -213,13 +208,13 @@ by case: X=>t'' [E] Cs' _; rewrite (coh_prec (cohS C) E _ Cs'). Qed. Lemma stepWithInv W A pr I (ii : InductiveInv pr I) s1 - (t : proc this (mkWorld pr) A) sc s2 (q : proc this W A) pf : - pstep s1 (WithInv pr I ii pf t) sc s2 q <-> + (t : proc (mkWorld pr) A) this sc s2 (q : proc W A) pf : + pstep s1 (WithInv pr I ii pf t) this sc s2 q <-> (exists v, [/\ sc = WithInvRet, t = Ret v, q = Ret v, s2 = s1, s1 \In Coh W & W = mkWorld (ProtocolWithIndInv ii)]) \/ exists sc' t' , [/\ sc = WithInvStep sc', q = WithInv pr I ii pf t', W = mkWorld (ProtocolWithIndInv ii), - s1 \In Coh W & pstep s1 t sc' s2 t']. + s1 \In Coh W & pstep s1 t this sc' s2 t']. Proof. split; last first. - case. @@ -240,26 +235,27 @@ programs respect the global network semantics. *) -Lemma pstep_network_sem (W : world) A s1 (t : proc this W A) sc s2 q : - pstep s1 t sc s2 q -> network_step W this s1 s2. +Lemma pstep_network_sem (W : world) A s1 (t : proc W A) this sc s2 q : + pstep s1 t this sc s2 q -> network_step W this s1 s2. Proof. -elim: sc W A s1 s2 t q=>/=. -- move=>W A s1 s2 p q; case: p; do?[by case|by move=>?; case]. - + by move=>a/stepAct [v][pf][Z1]Z2 H; subst q; apply: (a_step_sem H). +elim: sc W A this s1 s2 t q=>/=. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + move=>n a/stepAct[v][pf][Z1]Z2 /eqP Z H; subst n. + by subst q; apply: (a_step_sem H). + by move=>???; case. + by move=>????; case. by move=>?????; case. -- move=>W A s1 s2 p q; case: p; do?[by case|by move=>?; case]. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + move=>B p p0/stepSeq; case=>[[v][_]??? C|[sc'][p'][]]//. by subst p s2; apply: Idle. by move=>????/stepInject; case=>[[?][?][?]|[?][?][?][?][?][?]]//. by move=>?????; case. -- move=>sc HI W A s1 s2 p q; case: p; do?[by case|by move=>?; case]. +- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + move=>B p p0/stepSeq; case=>[[?][?]|[sc'][p'][][]? ?]//. by subst sc' q; apply: HI. by move=>????; case=>? _. by move=>?????; case. -- move=>sc HI W A s1 s2 p q; case: p; do?[by case|by move=>?; case]. +- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + by move=>B p p0; case. move=>V K pf p/stepInject; case=>[[?][?][?]|[sc'][t'][s1'][s2'][s][][]????]//. subst sc' q s1 s2=>C; move/HI=>S; apply: (sem_extend pf)=>//. @@ -267,20 +263,20 @@ elim: sc W A s1 s2 t q=>/=. move/(cohE pf): (C)=>[s1][s2][E]C' H. by move: (coh_prec (cohS C) E C1 C')=>Z; subst s1'; rewrite (joinfK (cohS C) E). by move=>?????; case. -- move=>W A s1 s2 p q; case: p; do?[by case|by move=>?; case]. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + by move=>???; case. + move=>V K i p; case/stepInject=>[[s1'][v][_]??? X|[?][?][?][?][?][?]]//. by subst p q s2; apply: Idle; split=>//; case: X=>x []. by move=>?????; case. - -- move=>sc HI W A s1 s2 p q; case: p; - do?[by case|by move=>?; case|by move=>???; case|by move=>????; case]. +- move=>sc HI W A this s1 s2 p q; case: p; + do?[by case|by move=>?; case| by move=>??; case + |by move=>???; case|by move=>????; case]. move=>pr I ii E p; case/(stepWithInv s1); first by case=>?; case. case=>sc'[t'][][]Z1 Z2 _ C1; subst q sc'. by move/HI=>T; subst W; apply: with_inv_step. -move=>W A s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case]. -case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3. -by subst s1' s2 q; apply: Idle. +- move=>W A this s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case]. + case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3. + by subst s1' s2 q; apply: Idle. Qed. (* @@ -292,10 +288,10 @@ it leverages the proof of the fact that each transition preserves the invariant. *) -Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc - (t t' : proc this (mkWorld pr) A): +Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 this sc + (t t' : proc (mkWorld pr) A): s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) -> - pstep s1 t sc s2 t' -> + pstep s1 t this sc s2 t' -> s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. diff --git a/Core/Process1.v b/Core/Process1.v new file mode 100644 index 0000000..b3e1bff --- /dev/null +++ b/Core/Process1.v @@ -0,0 +1,697 @@ +Require Import Relation_Operators. +Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding. +Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem. +Require Import Actions Injection. +Require Import InductiveInv. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Section ProcessSyntax. + +(* Syntax for process *) +Inductive proc (W : world) A := + Unfinished | Ret of A | Act (this : nid) of action W A this | + Seq B of proc W B & B -> proc W A | + Inject V K of injects V W K & proc V A | + WithInv p I (ii : InductiveInv p I) of + W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A | + (* Top-level parallel composition *) + ParProc of seq (nid * (proc W A)). + +Definition pcat W A B (t : proc W A) (k : A -> Pred (proc W B)) := + [Pred s | exists q, s = Seq t q /\ forall x, q x \In k x]. +Require Import Relation_Operators. +Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding. +Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem. +Require Import Actions Injection. +Require Import InductiveInv. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Section ProcessSyntax. + +(* Syntax for process *) +Inductive proc (W : world) A := + Unfinished | Ret of A | Act (this : nid) of action W A this | + Seq B of proc W B & B -> proc W A | + Inject V K of injects V W K & proc V A | + WithInv p I (ii : InductiveInv p I) of + W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A | + (* Top-level parallel composition *) + ParProc of seq (nid * (proc W A)). + +Definition pcat W A B (t : proc W A) (k : A -> Pred (proc W B)) := + [Pred s | exists q, s = Seq t q /\ forall x, q x \In k x]. + +Inductive schedule := + ActStep | SeqRet | SeqStep of schedule | + InjectStep of schedule | InjectRet | + WithInvStep of schedule | WithInvRet | + (* Step node number n *) + ParStep (n : nid) of schedule. + +End ProcessSyntax. + +Implicit Arguments Unfinished [W A]. +Implicit Arguments Ret [W A]. +Implicit Arguments Act [W A]. +Implicit Arguments Seq [W A B]. +Implicit Arguments WithInv [W A]. +Implicit Arguments ParProc [W A]. + +Section ProcessSemantics. + +Fixpoint step (W : world) A (s1 : state) (p1 : proc W A) + sc (s2 : state) (p2 : proc W A) : Prop := + match sc, p1 with + (* Action - make a step *) + | ActStep, Act this a => exists v pf, @a_step _ _ this a s1 pf s2 v /\ p2 = Ret v + (* Sequencing - apply a continuation *) + | SeqRet, Seq _ (Ret v) k => s2 = s1 /\ p2 = k v + | SeqStep sc', Seq _ p' k1 => + exists p'', step s1 p' sc' s2 p'' /\ p2 = Seq p'' k1 + (* Injection of a non-reduced term *) + | InjectRet, Inject V K pf (Ret v) => + exists s1', [/\ s2 = s1, p2 = Ret v & extends pf s1 s1'] + | InjectStep sc', Inject V K pf t1' => + exists s1' s2' s t2', + [/\ p2 = Inject pf t2', s1 = s1' \+ s, s2 = s2' \+ s, + s1' \In Coh V & step s1' t1' sc' s2' t2'] + (* Imposing an inductive invariant on a non-reduced term *) + | WithInvRet, WithInv p inv ii pf (Ret v) => + exists s1', [/\ s2 = s1, p2 = Ret v & s1 = s1'] + | WithInvStep sc', WithInv p inv ii pf t1' => + exists t2', p2 = WithInv p inv ii pf t2' /\ + step s1 t1' sc' s2 t2' + | ParStep n sc', ParProc ps => + exists p p' ps1 ps2, + [/\ ps = ps1 ++ (n, p) :: ps2, + step s1 p sc' s2 p' & + p2 = ParProc (ps1 ++ (n, p') :: ps2)] + | _, _ => False + end. + +Fixpoint good (W : world) A (p : proc W A) sc : Prop := + match sc, p with + | ActStep, Act _ _ => True + | SeqRet, Seq _ (Ret _) _ => True + | SeqStep sc', Seq _ p' _ => good p' sc' + | InjectStep sc', Inject _ _ _ p' => good p' sc' + | InjectRet, Inject _ _ _ (Ret _) => True + | WithInvStep sc', WithInv _ _ _ _ p' => good p' sc' + | WithInvRet, WithInv _ _ _ _ (Ret _) => True + | ParStep n sc', ParProc ps => + exists p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 /\ good p sc' + | _, _ => False + end. + +(* + +[Safety in small-step semantics] + +The safety (in order to make the following step) with respect to the +schedule is defined inductively on the shape of the program and the +schedule. Omitting the schedule is not a good idea, at it's required +in order to "sequentialize" the execution of the program +structure. Once it's dropped, this structure is lost. + + *) + +Fixpoint safe (W : world) A (p : proc W A) (this : nid) sc (s : state) : Prop := + match sc, p with + | ActStep, Act n a => n == this /\ @a_safe _ _ n a s + | SeqRet, Seq _ (Ret _) _ => True + | SeqStep sc', Seq _ p' _ => safe p' this sc' s + | InjectStep sc', Inject V K pf p' => + exists s', extends pf s s' /\ safe p' this sc' s' + | InjectRet, Inject V K pf (Ret _) => exists s', extends pf s s' + | WithInvStep sc', WithInv _ _ _ _ p' => safe p' this sc' s + | WithInvRet, WithInv _ _ _ _ (Ret _) => True + | ParStep n sc', ParProc ps => + (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2) /\ + (forall p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 -> safe p n sc' s) + | _, _ => True + end. + +Definition pstep (W : world) A s1 (p1 : proc W A) this sc s2 p2 := + [/\ s1 \In Coh W, safe p1 this sc s1 & step s1 p1 sc s2 p2]. + +(* Some sanity lemmas wrt. stepping *) + +Lemma pstep_safe (W : world) A s1 (t : proc W A) this sc s2 q : + pstep s1 t this sc s2 q -> safe t this sc s1. +Proof. by case. Qed. + +(* + +The following lemma established the operational "progress" property: a +program, which is safe and also the schedule is appropriate. Together, +this implies that we can do a step. + *) + +Lemma proc_progress W A s (p : proc W A) this sc : + s \In Coh W -> safe p this sc s -> good p sc -> + exists s' (p' : proc W A), pstep s p this sc s' p'. +Proof. +move=>C H1 H2; elim: sc W A this s p H2 H1 C=>[||sc IH|sc IH||sc IH||n sc IH]W A this s. +- case=>//=n a _/= [E H]; move/a_step_total: (H)=>[s'][r]H'. + by exists s', (Ret r); split=>//=; exists r, H. +- by case=>//; move=>B p k/=; case: p=>//b _ _; exists s, (k b). +- case=>//B p k/=H1 H2 C. + case: (IH W B this s p H1 H2 C)=>s'[p'][G1 G2]. + by exists s', (Seq p' k); split=>//; exists p'. +- case=>// V K pf p/=H1 [z][E]H2 C. + case: (E)=>s3[Z] C1 C2. + case: (IH V A this z p H1 H2 C1) =>s'[p']H3; case: H3=>S St. + exists (s' \+ s3), (Inject pf p'); split=>//; first by exists z. + by subst s; exists z, s', s3, p'. +- case=>//V K pf; case=>// v/=_[s'] E C. + by exists s, (Ret v); split=>//=; exists s'. +- case=>//pr I ii E p/= H1 H2 C. + have C' : s \In Coh (mkWorld pr) by subst W; apply: (with_inv_coh C). + case: (IH (mkWorld pr) A this s p H1 H2 C')=>s'[p']H3. + exists s', (WithInv pr I ii E p'); split=>//=. + by exists p'; split=>//; case: H3. +- case=>//pr I ii E; case=>//v/=_ _ C. + by exists s, (Ret v); split=>//=; exists s. +case=>//ps/=[p][ps1][ps2][Z]G1; subst ps. +case=>[[[[p' ps1'] ps2'] G2]]; case: G2=>E1 E; rewrite E1. +case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps1' ps2'; clear E1. +move/(_ p ps1 ps2 (erefl _))=>S C. +case: (IH W A n s p G1 S C)=>s'[p']H; exists s', (ParProc (ps1 ++ (n, p') :: ps2)). +split=>//=; last by exists p, p', ps1, ps2; split=>//; case: H. +split; last by move=> x1 x2 x3; case/(E (x1, x2, x3))=><-. +by exists (p, ps1, ps2). +Qed. + +(* Some view lemmas for processes and corresponding schedules *) + +Lemma stepUnfin W A s1 this sc s2 (t : proc W A) : + pstep s1 Unfinished this sc s2 t <-> False. +Proof. by split=>//; case; case: sc. Qed. + +Lemma stepRet W A s1 this sc s2 (t : proc W A) v : + pstep s1 (Ret v) this sc s2 t <-> False. +Proof. by split=>//; case; case: sc. Qed. + +Lemma stepAct W A s1 this a sc s2 (t : proc W A) : + pstep s1 (Act this a) this sc s2 t <-> + exists v pf, [/\ sc = ActStep, t = Ret v & @a_step _ _ _ a s1 pf s2 v]. +Proof. +split; first by case=>C; case: sc=>//= c [v [pf [H ->]]]; exists v, pf. +case=>v[pf] [->-> H]; split=>//; last by exists v, pf. +by apply: (a_safe_coh pf). +Qed. + +Lemma stepSeq W A B s1 (t : proc W B) k this sc s2 (q : proc W A) : + pstep s1 (Seq t k) this sc s2 q <-> + (exists v, [/\ sc = SeqRet, t = Ret v, q = k v, s2 = s1 & + s1 \In Coh W]) \/ + exists sc' p', + [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t this sc' s2 p']. +Proof. +split; last first. +- case; first by case=>v [->->->->]. + by case=>sc' [t'][->->][S H]; do !split=>//; exists t'. +case; case: sc=>//[|sc] C. +- by case: t=>//= v _ [->->]; left; exists v. +by move=>G /= [p' [H1 ->]]; right; exists sc, p'. +Qed. + +Lemma stepPar W A s1 ps this sc s2 (q : proc W A) : + pstep s1 (ParProc ps) this sc s2 q <-> + exists n sc', + sc = ParStep n sc' /\ + exists p p' ps1 ps2, + [/\ ps = ps1 ++ (n, p) :: ps2, + q = ParProc (ps1 ++ (n, p') :: ps2), + (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2)& + pstep s1 p n sc' s2 p']. +Proof. +split=>/=; last first. +- case=>n[s'][->{sc}][p][p'][ps1][ps2][->->{ps q}]U[C] H1 H2. + split=>//=; last by exists p, p', ps1, ps2. + split=>//; clear H2 p'; case: U=>[[[p' ps1']] ps2'][Z]E. + case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps2' ps1'. + by move=>x1 x2 x3; case/(E (x1, x2, x3))=><-. +case; case: sc=>//n sc' C/=G1 G2; exists n, sc'; split=>//. +case:G1; case=>[[[p ps1]ps2]]U H; case: U=>Z U; subst ps. +case: G2=>p1[p'][ps1'][ps2'][Z]S->. +case: (U (p1, ps1', ps2') Z)=>Z1 Z2 Z3. subst p1 ps1' ps2'. +move: (H _ _ _ Z)=>{H Z}H. +by exists p, p', ps1, ps2; split=>//; exists (p, ps1, ps2). +Qed. + +Lemma stepInject V W K A (em : injects V W K) + s1 (t : proc V A) this sc s2 (q : proc W A) : + pstep s1 (Inject em t) this sc s2 q <-> + (* Case 1 : stepped to the final state s1' of the inner program*) + (exists s1' v, [/\ sc = InjectRet, t = Ret v, q = Ret v, s2 = s1 & + extends em s1 s1']) \/ + (* Case 2 : stepped to the nextx state s12 of the inner program*) + exists sc' t' s1' s2' s, + [/\ sc = InjectStep sc', q = Inject em t', + s1 = s1' \+ s, s2 = s2' \+ s, s1 \In Coh W & + pstep s1' t this sc' s2' t']. +Proof. +split; last first. +- case. + + case=>s1' [v][->->->->] E. + split=>//=; [by case: E=>x[] | by exists s1'|by exists s1']. + case=>sc' [t'][s1'][s2'][s][->->->-> C][[C' S] T]. + split=>//=; last by exists s1', s2', s, t'. + by exists s1'; split=>//; exists s. +case=>C; case: sc=>//=; last first. +- case: t=>//= v [C1 S][s1'][->->{s2 q}] X. + by left; exists s1'; exists v. +move=>sc /= [s'][X] S [s1'][s2'][t'][t2'][??? C1'] T; subst q s1 s2. +right; exists sc, t2', s1', s2', t'; do !split=>//. +by case: X=>t'' [E] Cs' _; rewrite (coh_prec (cohS C) E _ Cs'). +Qed. + +Lemma stepWithInv W A pr I (ii : InductiveInv pr I) s1 + (t : proc (mkWorld pr) A) this sc s2 (q : proc W A) pf : + pstep s1 (WithInv pr I ii pf t) this sc s2 q <-> + (exists v, [/\ sc = WithInvRet, t = Ret v, q = Ret v, s2 = s1, + s1 \In Coh W & W = mkWorld (ProtocolWithIndInv ii)]) \/ + exists sc' t' , [/\ sc = WithInvStep sc', q = WithInv pr I ii pf t', + W = mkWorld (ProtocolWithIndInv ii), + s1 \In Coh W & pstep s1 t this sc' s2 t']. +Proof. +split; last first. +- case. + + by case=>v[->->->->{s2}]C E; split=>//=; exists s1. + by case=>sc' [t'][->->{sc q}]E C[C' S]T; split=>//=; exists t'. +case=>C; case: sc=>//=; last first. +- by case: t=>//=v _[s1'][Z1]Z2 Z3; subst s2 s1' q; left; exists v. +move=>sc /=S[t'][->{q}T]; right; exists sc, t'; split=>//. +by split=>//; subst W; apply: (with_inv_coh C). +Qed. + +(* + +[Stepping and network semantics] + +The following lemma ensures that the operational semantics of our +programs respect the global network semantics. + + *) + +Lemma pstep_network_sem (W : world) A s1 (t : proc W A) this sc s2 q : + pstep s1 t this sc s2 q -> network_step W this s1 s2. +Proof. +elim: sc W A this s1 s2 t q=>/=. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + (* move=>n a. *) + (* Check (stepAct s1 a ActStep s2 q). *) + (* [v][pf][Z1]Z2 H. subst q; apply: (a_step_sem H). *) + admit. + + by move=>???; case. + + by move=>????; case. + by move=>?????; case. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + move=>B p p0/stepSeq; case=>[[v][_]??? C|[sc'][p'][]]//. + by subst p s2; apply: Idle. + by move=>????/stepInject; case=>[[?][?][?]|[?][?][?][?][?][?]]//. + by move=>?????; case. +- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + move=>B p p0/stepSeq; case=>[[?][?]|[sc'][p'][][]? ?]//. + by subst sc' q; apply: HI. + by move=>????; case=>? _. + by move=>?????; case. +- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + by move=>B p p0; case. + move=>V K pf p/stepInject; case=>[[?][?][?]|[sc'][t'][s1'][s2'][s][][]????]//. + subst sc' q s1 s2=>C; move/HI=>S; apply: (sem_extend pf)=>//. + apply/(cohE pf); exists s2', s; case: (step_coh S)=>C1 C2; split=>//. + move/(cohE pf): (C)=>[s1][s2][E]C' H. + by move: (coh_prec (cohS C) E C1 C')=>Z; subst s1'; rewrite (joinfK (cohS C) E). + by move=>?????; case. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + by move=>???; case. + + move=>V K i p; case/stepInject=>[[s1'][v][_]??? X|[?][?][?][?][?][?]]//. + by subst p q s2; apply: Idle; split=>//; case: X=>x []. + by move=>?????; case. +- move=>sc HI W A this s1 s2 p q; case: p; + do?[by case|by move=>?; case| by move=>??; case + |by move=>???; case|by move=>????; case]. + move=>pr I ii E p; case/(stepWithInv s1); first by case=>?; case. + case=>sc'[t'][][]Z1 Z2 _ C1; subst q sc'. + by move/HI=>T; subst W; apply: with_inv_step. +- move=>W A this s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case]. + case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3. + by subst s1' s2 q; apply: Idle. +move=>n sc HI W A this s1 s2 p q; case: p=>//; +do?[by case|by move=>?; case|by move=>???; case|by move=>????; case + |by move=>?????; case|by move=>??; case]. +move=>ps/stepPar=>[[m]][sc']; case; case=>Z1 Z2; subst n sc'. +case=>p[p'][ps1][ps2]. + + by case=>p[p'][ps1][ps2][_]_ _; apply: HI. +Qed. + +(* + +[Inductive invariants and stepping] + +The following lemma is the crux of wrapping into inductive invariants, as +it leverages the proof of the fact that each transition preserves the invariant. + +*) + +Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc + (t t' : proc this (mkWorld pr) A): + s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) -> + pstep s1 t sc s2 t' -> + s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). +Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. + +End ProcessSemantics. +Inductive schedule := + ActStep | SeqRet | SeqStep of schedule | + InjectStep of schedule | InjectRet | + WithInvStep of schedule | WithInvRet | + (* Step node number n *) + ParStep (n : nid) of schedule. + +End ProcessSyntax. + +Implicit Arguments Unfinished [W A]. +Implicit Arguments Ret [W A]. +Implicit Arguments Act [W A]. +Implicit Arguments Seq [W A B]. +Implicit Arguments WithInv [W A]. +Implicit Arguments ParProc [W A]. + +Section ProcessSemantics. + +Fixpoint step (W : world) A (s1 : state) (p1 : proc W A) + sc (s2 : state) (p2 : proc W A) : Prop := + match sc, p1 with + (* Action - make a step *) + | ActStep, Act this a => exists v pf, @a_step _ _ this a s1 pf s2 v /\ p2 = Ret v + (* Sequencing - apply a continuation *) + | SeqRet, Seq _ (Ret v) k => s2 = s1 /\ p2 = k v + | SeqStep sc', Seq _ p' k1 => + exists p'', step s1 p' sc' s2 p'' /\ p2 = Seq p'' k1 + (* Injection of a non-reduced term *) + | InjectRet, Inject V K pf (Ret v) => + exists s1', [/\ s2 = s1, p2 = Ret v & extends pf s1 s1'] + | InjectStep sc', Inject V K pf t1' => + exists s1' s2' s t2', + [/\ p2 = Inject pf t2', s1 = s1' \+ s, s2 = s2' \+ s, + s1' \In Coh V & step s1' t1' sc' s2' t2'] + (* Imposing an inductive invariant on a non-reduced term *) + | WithInvRet, WithInv p inv ii pf (Ret v) => + exists s1', [/\ s2 = s1, p2 = Ret v & s1 = s1'] + | WithInvStep sc', WithInv p inv ii pf t1' => + exists t2', p2 = WithInv p inv ii pf t2' /\ + step s1 t1' sc' s2 t2' + | ParStep n sc', ParProc ps => + exists p p' ps1 ps2, + [/\ ps = ps1 ++ (n, p) :: ps2, + step s1 p sc' s2 p' & + p2 = ParProc (ps1 ++ (n, p') :: ps2)] + | _, _ => False + end. + +Fixpoint good (W : world) A (p : proc W A) sc : Prop := + match sc, p with + | ActStep, Act _ _ => True + | SeqRet, Seq _ (Ret _) _ => True + | SeqStep sc', Seq _ p' _ => good p' sc' + | InjectStep sc', Inject _ _ _ p' => good p' sc' + | InjectRet, Inject _ _ _ (Ret _) => True + | WithInvStep sc', WithInv _ _ _ _ p' => good p' sc' + | WithInvRet, WithInv _ _ _ _ (Ret _) => True + | ParStep n sc', ParProc ps => + exists p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 /\ good p sc' + | _, _ => False + end. + +(* + +[Safety in small-step semantics] + +The safety (in order to make the following step) with respect to the +schedule is defined inductively on the shape of the program and the +schedule. Omitting the schedule is not a good idea, at it's required +in order to "sequentialize" the execution of the program +structure. Once it's dropped, this structure is lost. + + *) + +Fixpoint safe (W : world) A (p : proc W A) (this : nid) sc (s : state) : Prop := + match sc, p with + | ActStep, Act n a => n == this /\ @a_safe _ _ n a s + | SeqRet, Seq _ (Ret _) _ => True + | SeqStep sc', Seq _ p' _ => safe p' this sc' s + | InjectStep sc', Inject V K pf p' => + exists s', extends pf s s' /\ safe p' this sc' s' + | InjectRet, Inject V K pf (Ret _) => exists s', extends pf s s' + | WithInvStep sc', WithInv _ _ _ _ p' => safe p' this sc' s + | WithInvRet, WithInv _ _ _ _ (Ret _) => True + | ParStep n sc', ParProc ps => + (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2) /\ + (forall p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 -> safe p n sc' s) + | _, _ => True + end. + +Definition pstep (W : world) A s1 (p1 : proc W A) this sc s2 p2 := + [/\ s1 \In Coh W, safe p1 this sc s1 & step s1 p1 sc s2 p2]. + +(* Some sanity lemmas wrt. stepping *) + +Lemma pstep_safe (W : world) A s1 (t : proc W A) this sc s2 q : + pstep s1 t this sc s2 q -> safe t this sc s1. +Proof. by case. Qed. + +(* + +The following lemma established the operational "progress" property: a +program, which is safe and also the schedule is appropriate. Together, +this implies that we can do a step. + *) + +Lemma proc_progress W A s (p : proc W A) this sc : + s \In Coh W -> safe p this sc s -> good p sc -> + exists s' (p' : proc W A), pstep s p this sc s' p'. +Proof. +move=>C H1 H2; elim: sc W A this s p H2 H1 C=>[||sc IH|sc IH||sc IH||n sc IH]W A this s. +- case=>//=n a _/= [E H]; move/a_step_total: (H)=>[s'][r]H'. + by exists s', (Ret r); split=>//=; exists r, H. +- by case=>//; move=>B p k/=; case: p=>//b _ _; exists s, (k b). +- case=>//B p k/=H1 H2 C. + case: (IH W B this s p H1 H2 C)=>s'[p'][G1 G2]. + by exists s', (Seq p' k); split=>//; exists p'. +- case=>// V K pf p/=H1 [z][E]H2 C. + case: (E)=>s3[Z] C1 C2. + case: (IH V A this z p H1 H2 C1) =>s'[p']H3; case: H3=>S St. + exists (s' \+ s3), (Inject pf p'); split=>//; first by exists z. + by subst s; exists z, s', s3, p'. +- case=>//V K pf; case=>// v/=_[s'] E C. + by exists s, (Ret v); split=>//=; exists s'. +- case=>//pr I ii E p/= H1 H2 C. + have C' : s \In Coh (mkWorld pr) by subst W; apply: (with_inv_coh C). + case: (IH (mkWorld pr) A this s p H1 H2 C')=>s'[p']H3. + exists s', (WithInv pr I ii E p'); split=>//=. + by exists p'; split=>//; case: H3. +- case=>//pr I ii E; case=>//v/=_ _ C. + by exists s, (Ret v); split=>//=; exists s. +case=>//ps/=[p][ps1][ps2][Z]G1; subst ps. +case=>[[[[p' ps1'] ps2'] G2]]; case: G2=>E1 E; rewrite E1. +case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps1' ps2'; clear E1. +move/(_ p ps1 ps2 (erefl _))=>S C. +case: (IH W A n s p G1 S C)=>s'[p']H; exists s', (ParProc (ps1 ++ (n, p') :: ps2)). +split=>//=; last by exists p, p', ps1, ps2; split=>//; case: H. +split; last by move=> x1 x2 x3; case/(E (x1, x2, x3))=><-. +by exists (p, ps1, ps2). +Qed. + +(* Some view lemmas for processes and corresponding schedules *) + +Lemma stepUnfin W A s1 this sc s2 (t : proc W A) : + pstep s1 Unfinished this sc s2 t <-> False. +Proof. by split=>//; case; case: sc. Qed. + +Lemma stepRet W A s1 this sc s2 (t : proc W A) v : + pstep s1 (Ret v) this sc s2 t <-> False. +Proof. by split=>//; case; case: sc. Qed. + +Lemma stepAct W A s1 this a sc s2 (t : proc W A) : + pstep s1 (Act this a) this sc s2 t <-> + exists v pf, [/\ sc = ActStep, t = Ret v & @a_step _ _ _ a s1 pf s2 v]. +Proof. +split; first by case=>C; case: sc=>//= c [v [pf [H ->]]]; exists v, pf. +case=>v[pf] [->-> H]; split=>//; last by exists v, pf. +by apply: (a_safe_coh pf). +Qed. + +Lemma stepSeq W A B s1 (t : proc W B) k this sc s2 (q : proc W A) : + pstep s1 (Seq t k) this sc s2 q <-> + (exists v, [/\ sc = SeqRet, t = Ret v, q = k v, s2 = s1 & + s1 \In Coh W]) \/ + exists sc' p', + [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t this sc' s2 p']. +Proof. +split; last first. +- case; first by case=>v [->->->->]. + by case=>sc' [t'][->->][S H]; do !split=>//; exists t'. +case; case: sc=>//[|sc] C. +- by case: t=>//= v _ [->->]; left; exists v. +by move=>G /= [p' [H1 ->]]; right; exists sc, p'. +Qed. + +Lemma stepPar W A s1 ps this sc s2 (q : proc W A) : + pstep s1 (ParProc ps) this sc s2 q <-> + exists n sc', + sc = ParStep n sc' /\ + exists p p' ps1 ps2, + [/\ ps = ps1 ++ (n, p) :: ps2, + q = ParProc (ps1 ++ (n, p') :: ps2), + (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2)& + pstep s1 p n sc' s2 p']. +Proof. +split=>/=; last first. +- case=>n[s'][->{sc}][p][p'][ps1][ps2][->->{ps q}]U[C] H1 H2. + split=>//=; last by exists p, p', ps1, ps2. + split=>//; clear H2 p'; case: U=>[[[p' ps1']] ps2'][Z]E. + case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps2' ps1'. + by move=>x1 x2 x3; case/(E (x1, x2, x3))=><-. +case; case: sc=>//n sc' C/=G1 G2; exists n, sc'; split=>//. +case:G1; case=>[[[p ps1]ps2]]U H; case: U=>Z U; subst ps. +case: G2=>p1[p'][ps1'][ps2'][Z]S->. +case: (U (p1, ps1', ps2') Z)=>Z1 Z2 Z3. subst p1 ps1' ps2'. +move: (H _ _ _ Z)=>{H Z}H. +by exists p, p', ps1, ps2; split=>//; exists (p, ps1, ps2). +Qed. + +Lemma stepInject V W K A (em : injects V W K) + s1 (t : proc V A) this sc s2 (q : proc W A) : + pstep s1 (Inject em t) this sc s2 q <-> + (* Case 1 : stepped to the final state s1' of the inner program*) + (exists s1' v, [/\ sc = InjectRet, t = Ret v, q = Ret v, s2 = s1 & + extends em s1 s1']) \/ + (* Case 2 : stepped to the nextx state s12 of the inner program*) + exists sc' t' s1' s2' s, + [/\ sc = InjectStep sc', q = Inject em t', + s1 = s1' \+ s, s2 = s2' \+ s, s1 \In Coh W & + pstep s1' t this sc' s2' t']. +Proof. +split; last first. +- case. + + case=>s1' [v][->->->->] E. + split=>//=; [by case: E=>x[] | by exists s1'|by exists s1']. + case=>sc' [t'][s1'][s2'][s][->->->-> C][[C' S] T]. + split=>//=; last by exists s1', s2', s, t'. + by exists s1'; split=>//; exists s. +case=>C; case: sc=>//=; last first. +- case: t=>//= v [C1 S][s1'][->->{s2 q}] X. + by left; exists s1'; exists v. +move=>sc /= [s'][X] S [s1'][s2'][t'][t2'][??? C1'] T; subst q s1 s2. +right; exists sc, t2', s1', s2', t'; do !split=>//. +by case: X=>t'' [E] Cs' _; rewrite (coh_prec (cohS C) E _ Cs'). +Qed. + +Lemma stepWithInv W A pr I (ii : InductiveInv pr I) s1 + (t : proc (mkWorld pr) A) this sc s2 (q : proc W A) pf : + pstep s1 (WithInv pr I ii pf t) this sc s2 q <-> + (exists v, [/\ sc = WithInvRet, t = Ret v, q = Ret v, s2 = s1, + s1 \In Coh W & W = mkWorld (ProtocolWithIndInv ii)]) \/ + exists sc' t' , [/\ sc = WithInvStep sc', q = WithInv pr I ii pf t', + W = mkWorld (ProtocolWithIndInv ii), + s1 \In Coh W & pstep s1 t this sc' s2 t']. +Proof. +split; last first. +- case. + + by case=>v[->->->->{s2}]C E; split=>//=; exists s1. + by case=>sc' [t'][->->{sc q}]E C[C' S]T; split=>//=; exists t'. +case=>C; case: sc=>//=; last first. +- by case: t=>//=v _[s1'][Z1]Z2 Z3; subst s2 s1' q; left; exists v. +move=>sc /=S[t'][->{q}T]; right; exists sc, t'; split=>//. +by split=>//; subst W; apply: (with_inv_coh C). +Qed. + +(* + +[Stepping and network semantics] + +The following lemma ensures that the operational semantics of our +programs respect the global network semantics. + + *) + +Lemma pstep_network_sem (W : world) A s1 (t : proc W A) this sc s2 q : + pstep s1 t this sc s2 q -> network_step W this s1 s2. +Proof. +elim: sc W A this s1 s2 t q=>/=. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + (* move=>n a. *) + (* Check (stepAct s1 a ActStep s2 q). *) + (* [v][pf][Z1]Z2 H. subst q; apply: (a_step_sem H). *) + admit. + + by move=>???; case. + + by move=>????; case. + by move=>?????; case. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + move=>B p p0/stepSeq; case=>[[v][_]??? C|[sc'][p'][]]//. + by subst p s2; apply: Idle. + by move=>????/stepInject; case=>[[?][?][?]|[?][?][?][?][?][?]]//. + by move=>?????; case. +- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + move=>B p p0/stepSeq; case=>[[?][?]|[sc'][p'][][]? ?]//. + by subst sc' q; apply: HI. + by move=>????; case=>? _. + by move=>?????; case. +- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + by move=>B p p0; case. + move=>V K pf p/stepInject; case=>[[?][?][?]|[sc'][t'][s1'][s2'][s][][]????]//. + subst sc' q s1 s2=>C; move/HI=>S; apply: (sem_extend pf)=>//. + apply/(cohE pf); exists s2', s; case: (step_coh S)=>C1 C2; split=>//. + move/(cohE pf): (C)=>[s1][s2][E]C' H. + by move: (coh_prec (cohS C) E C1 C')=>Z; subst s1'; rewrite (joinfK (cohS C) E). + by move=>?????; case. +- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. + + by move=>???; case. + + move=>V K i p; case/stepInject=>[[s1'][v][_]??? X|[?][?][?][?][?][?]]//. + by subst p q s2; apply: Idle; split=>//; case: X=>x []. + by move=>?????; case. +- move=>sc HI W A this s1 s2 p q; case: p; + do?[by case|by move=>?; case| by move=>??; case + |by move=>???; case|by move=>????; case]. + move=>pr I ii E p; case/(stepWithInv s1); first by case=>?; case. + case=>sc'[t'][][]Z1 Z2 _ C1; subst q sc'. + by move/HI=>T; subst W; apply: with_inv_step. +- move=>W A this s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case]. + case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3. + by subst s1' s2 q; apply: Idle. +move=>n sc HI W A this s1 s2 p q; case: p=>//; +do?[by case|by move=>?; case|by move=>???; case|by move=>????; case + |by move=>?????; case|by move=>??; case]. +move=>ps/stepPar=>[[m]][sc']; case; case=>Z1 Z2; subst n sc'. +case=>p[p'][ps1][ps2]. + + by case=>p[p'][ps1][ps2][_]_ _; apply: HI. +Qed. + +(* + +[Inductive invariants and stepping] + +The following lemma is the crux of wrapping into inductive invariants, as +it leverages the proof of the fact that each transition preserves the invariant. + +*) + +Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc + (t t' : proc this (mkWorld pr) A): + s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) -> + pstep s1 t sc s2 t' -> + s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). +Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. + +End ProcessSemantics. \ No newline at end of file From d390a57839e02b280073c89c785a5fcec9584ecd Mon Sep 17 00:00:00 2001 From: Ilya Sergey Date: Wed, 7 Jun 2017 20:42:22 +0100 Subject: [PATCH 2/3] added parallel schedules --- Core/Process.v | 76 ++++++ Core/Process1.v | 697 ------------------------------------------------ 2 files changed, 76 insertions(+), 697 deletions(-) delete mode 100644 Core/Process1.v diff --git a/Core/Process.v b/Core/Process.v index 35dd567..0ce1fc5 100644 --- a/Core/Process.v +++ b/Core/Process.v @@ -295,4 +295,80 @@ Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 this sc s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. + +(***********************************************************************) +(******************** Parallel schedule ********************************) +(***********************************************************************) + +Definition par_proc W A := seq (nid * proc W A). + +Inductive par_schedule := + Done | ParStep (n : nid) of schedule. + +Definition par_good (W : world) A (ps : par_proc W A) sc : Prop := + match sc with + | Done => False + | ParStep n sc' => exists p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 /\ good p sc' end. + +Definition par_safe (W : world) A (ps : par_proc W A) sc (s : state) : Prop := + match sc with + | ParStep n sc' => + (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2) /\ + (forall p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 -> safe p n sc' s) + | _ => True + end. + +(* Parallel stepping *) +Definition par_step (W : world) A (s1 : state) (ps : par_proc W A) sc + (s2 : state) (ps' : par_proc W A) : Prop := + match sc with + | ParStep n sc' => + exists p p' ps1 ps2, + [/\ ps = ps1 ++ (n, p) :: ps2, step s1 p sc' s2 p' & ps' = (ps1 ++ (n, p') :: ps2)] + | _ => False + end. + +Definition par_pstep (W : world) A s1 (ps : par_proc W A) sc s2 p2 := + [/\ s1 \In Coh W, par_safe ps sc s1 & par_step s1 ps sc s2 p2]. + +(* Some sanity lemmas wrt. stepping *) + +Lemma par_pstep_safe (W : world) A s1 (t : par_proc W A) sc s2 q : + par_pstep s1 t sc s2 q -> par_safe t sc s1. +Proof. by case. Qed. + +Lemma par_pstep_network_sem (W : world) A s1 (t : par_proc W A) sc s2 q : + par_pstep s1 t sc s2 q -> exists n p, (n, p) \In t /\ network_step W n s1 s2. +Proof. +case: sc =>//=; first by case=>//. +move=>n sc; case=>/= C; case; case=>[[[p ps1] ps2]][E]H1 H2; subst t. +case=>x[p'][ps3][ps4][E]S Z; subst q. +case/(H1 (x, ps3, ps4)): E=> Z1 Z2 Z3; subst x ps3 ps4. +exists n, p; split; first by apply/Mem_cat; right; apply/In_cons; left. +apply: (@pstep_network_sem W A s1 p n sc s2 p'). +by split=>//; apply: (H2 p ps1 ps2 (erefl _)). +Qed. + +Lemma par_pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc + (t t' : par_proc (mkWorld pr) A): + s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) -> + par_pstep s1 t sc s2 t' -> + s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). +Proof. +by move=>C1; case/par_pstep_network_sem=> n [p][_]/(with_inv_step C1)/step_coh; case. +Qed. + +Lemma par_proc_progress W A s (t : par_proc W A) sc : + s \In Coh W -> par_safe t sc s -> par_good t sc -> + exists s' (q : par_proc W A), par_pstep s t sc s' q. +Proof. +move=>C; case: sc=>// n sc/=. +case; case=>[[[p ps1] ps2]][E]H1 H2; subst t. +case=>x[ps3][ps4][E]G; case/(H1 (x, ps3, ps4)): E=> Z1 Z2 Z3; subst x ps3 ps4. +move: (H2 p ps1 ps2 (erefl _))=>S. +case: (proc_progress C S G)=>s'[p'][_]_ H; exists s'. +exists (ps1 ++ (n, p') :: ps2); split=>//=; last by exists p, p', ps1, ps2. +by split=>//; exists (p, ps1, ps2). +Qed. + End ProcessSemantics. \ No newline at end of file diff --git a/Core/Process1.v b/Core/Process1.v deleted file mode 100644 index b3e1bff..0000000 --- a/Core/Process1.v +++ /dev/null @@ -1,697 +0,0 @@ -Require Import Relation_Operators. -Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding. -Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem. -Require Import Actions Injection. -Require Import InductiveInv. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Section ProcessSyntax. - -(* Syntax for process *) -Inductive proc (W : world) A := - Unfinished | Ret of A | Act (this : nid) of action W A this | - Seq B of proc W B & B -> proc W A | - Inject V K of injects V W K & proc V A | - WithInv p I (ii : InductiveInv p I) of - W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A | - (* Top-level parallel composition *) - ParProc of seq (nid * (proc W A)). - -Definition pcat W A B (t : proc W A) (k : A -> Pred (proc W B)) := - [Pred s | exists q, s = Seq t q /\ forall x, q x \In k x]. -Require Import Relation_Operators. -Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding. -Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem. -Require Import Actions Injection. -Require Import InductiveInv. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Section ProcessSyntax. - -(* Syntax for process *) -Inductive proc (W : world) A := - Unfinished | Ret of A | Act (this : nid) of action W A this | - Seq B of proc W B & B -> proc W A | - Inject V K of injects V W K & proc V A | - WithInv p I (ii : InductiveInv p I) of - W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A | - (* Top-level parallel composition *) - ParProc of seq (nid * (proc W A)). - -Definition pcat W A B (t : proc W A) (k : A -> Pred (proc W B)) := - [Pred s | exists q, s = Seq t q /\ forall x, q x \In k x]. - -Inductive schedule := - ActStep | SeqRet | SeqStep of schedule | - InjectStep of schedule | InjectRet | - WithInvStep of schedule | WithInvRet | - (* Step node number n *) - ParStep (n : nid) of schedule. - -End ProcessSyntax. - -Implicit Arguments Unfinished [W A]. -Implicit Arguments Ret [W A]. -Implicit Arguments Act [W A]. -Implicit Arguments Seq [W A B]. -Implicit Arguments WithInv [W A]. -Implicit Arguments ParProc [W A]. - -Section ProcessSemantics. - -Fixpoint step (W : world) A (s1 : state) (p1 : proc W A) - sc (s2 : state) (p2 : proc W A) : Prop := - match sc, p1 with - (* Action - make a step *) - | ActStep, Act this a => exists v pf, @a_step _ _ this a s1 pf s2 v /\ p2 = Ret v - (* Sequencing - apply a continuation *) - | SeqRet, Seq _ (Ret v) k => s2 = s1 /\ p2 = k v - | SeqStep sc', Seq _ p' k1 => - exists p'', step s1 p' sc' s2 p'' /\ p2 = Seq p'' k1 - (* Injection of a non-reduced term *) - | InjectRet, Inject V K pf (Ret v) => - exists s1', [/\ s2 = s1, p2 = Ret v & extends pf s1 s1'] - | InjectStep sc', Inject V K pf t1' => - exists s1' s2' s t2', - [/\ p2 = Inject pf t2', s1 = s1' \+ s, s2 = s2' \+ s, - s1' \In Coh V & step s1' t1' sc' s2' t2'] - (* Imposing an inductive invariant on a non-reduced term *) - | WithInvRet, WithInv p inv ii pf (Ret v) => - exists s1', [/\ s2 = s1, p2 = Ret v & s1 = s1'] - | WithInvStep sc', WithInv p inv ii pf t1' => - exists t2', p2 = WithInv p inv ii pf t2' /\ - step s1 t1' sc' s2 t2' - | ParStep n sc', ParProc ps => - exists p p' ps1 ps2, - [/\ ps = ps1 ++ (n, p) :: ps2, - step s1 p sc' s2 p' & - p2 = ParProc (ps1 ++ (n, p') :: ps2)] - | _, _ => False - end. - -Fixpoint good (W : world) A (p : proc W A) sc : Prop := - match sc, p with - | ActStep, Act _ _ => True - | SeqRet, Seq _ (Ret _) _ => True - | SeqStep sc', Seq _ p' _ => good p' sc' - | InjectStep sc', Inject _ _ _ p' => good p' sc' - | InjectRet, Inject _ _ _ (Ret _) => True - | WithInvStep sc', WithInv _ _ _ _ p' => good p' sc' - | WithInvRet, WithInv _ _ _ _ (Ret _) => True - | ParStep n sc', ParProc ps => - exists p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 /\ good p sc' - | _, _ => False - end. - -(* - -[Safety in small-step semantics] - -The safety (in order to make the following step) with respect to the -schedule is defined inductively on the shape of the program and the -schedule. Omitting the schedule is not a good idea, at it's required -in order to "sequentialize" the execution of the program -structure. Once it's dropped, this structure is lost. - - *) - -Fixpoint safe (W : world) A (p : proc W A) (this : nid) sc (s : state) : Prop := - match sc, p with - | ActStep, Act n a => n == this /\ @a_safe _ _ n a s - | SeqRet, Seq _ (Ret _) _ => True - | SeqStep sc', Seq _ p' _ => safe p' this sc' s - | InjectStep sc', Inject V K pf p' => - exists s', extends pf s s' /\ safe p' this sc' s' - | InjectRet, Inject V K pf (Ret _) => exists s', extends pf s s' - | WithInvStep sc', WithInv _ _ _ _ p' => safe p' this sc' s - | WithInvRet, WithInv _ _ _ _ (Ret _) => True - | ParStep n sc', ParProc ps => - (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2) /\ - (forall p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 -> safe p n sc' s) - | _, _ => True - end. - -Definition pstep (W : world) A s1 (p1 : proc W A) this sc s2 p2 := - [/\ s1 \In Coh W, safe p1 this sc s1 & step s1 p1 sc s2 p2]. - -(* Some sanity lemmas wrt. stepping *) - -Lemma pstep_safe (W : world) A s1 (t : proc W A) this sc s2 q : - pstep s1 t this sc s2 q -> safe t this sc s1. -Proof. by case. Qed. - -(* - -The following lemma established the operational "progress" property: a -program, which is safe and also the schedule is appropriate. Together, -this implies that we can do a step. - *) - -Lemma proc_progress W A s (p : proc W A) this sc : - s \In Coh W -> safe p this sc s -> good p sc -> - exists s' (p' : proc W A), pstep s p this sc s' p'. -Proof. -move=>C H1 H2; elim: sc W A this s p H2 H1 C=>[||sc IH|sc IH||sc IH||n sc IH]W A this s. -- case=>//=n a _/= [E H]; move/a_step_total: (H)=>[s'][r]H'. - by exists s', (Ret r); split=>//=; exists r, H. -- by case=>//; move=>B p k/=; case: p=>//b _ _; exists s, (k b). -- case=>//B p k/=H1 H2 C. - case: (IH W B this s p H1 H2 C)=>s'[p'][G1 G2]. - by exists s', (Seq p' k); split=>//; exists p'. -- case=>// V K pf p/=H1 [z][E]H2 C. - case: (E)=>s3[Z] C1 C2. - case: (IH V A this z p H1 H2 C1) =>s'[p']H3; case: H3=>S St. - exists (s' \+ s3), (Inject pf p'); split=>//; first by exists z. - by subst s; exists z, s', s3, p'. -- case=>//V K pf; case=>// v/=_[s'] E C. - by exists s, (Ret v); split=>//=; exists s'. -- case=>//pr I ii E p/= H1 H2 C. - have C' : s \In Coh (mkWorld pr) by subst W; apply: (with_inv_coh C). - case: (IH (mkWorld pr) A this s p H1 H2 C')=>s'[p']H3. - exists s', (WithInv pr I ii E p'); split=>//=. - by exists p'; split=>//; case: H3. -- case=>//pr I ii E; case=>//v/=_ _ C. - by exists s, (Ret v); split=>//=; exists s. -case=>//ps/=[p][ps1][ps2][Z]G1; subst ps. -case=>[[[[p' ps1'] ps2'] G2]]; case: G2=>E1 E; rewrite E1. -case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps1' ps2'; clear E1. -move/(_ p ps1 ps2 (erefl _))=>S C. -case: (IH W A n s p G1 S C)=>s'[p']H; exists s', (ParProc (ps1 ++ (n, p') :: ps2)). -split=>//=; last by exists p, p', ps1, ps2; split=>//; case: H. -split; last by move=> x1 x2 x3; case/(E (x1, x2, x3))=><-. -by exists (p, ps1, ps2). -Qed. - -(* Some view lemmas for processes and corresponding schedules *) - -Lemma stepUnfin W A s1 this sc s2 (t : proc W A) : - pstep s1 Unfinished this sc s2 t <-> False. -Proof. by split=>//; case; case: sc. Qed. - -Lemma stepRet W A s1 this sc s2 (t : proc W A) v : - pstep s1 (Ret v) this sc s2 t <-> False. -Proof. by split=>//; case; case: sc. Qed. - -Lemma stepAct W A s1 this a sc s2 (t : proc W A) : - pstep s1 (Act this a) this sc s2 t <-> - exists v pf, [/\ sc = ActStep, t = Ret v & @a_step _ _ _ a s1 pf s2 v]. -Proof. -split; first by case=>C; case: sc=>//= c [v [pf [H ->]]]; exists v, pf. -case=>v[pf] [->-> H]; split=>//; last by exists v, pf. -by apply: (a_safe_coh pf). -Qed. - -Lemma stepSeq W A B s1 (t : proc W B) k this sc s2 (q : proc W A) : - pstep s1 (Seq t k) this sc s2 q <-> - (exists v, [/\ sc = SeqRet, t = Ret v, q = k v, s2 = s1 & - s1 \In Coh W]) \/ - exists sc' p', - [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t this sc' s2 p']. -Proof. -split; last first. -- case; first by case=>v [->->->->]. - by case=>sc' [t'][->->][S H]; do !split=>//; exists t'. -case; case: sc=>//[|sc] C. -- by case: t=>//= v _ [->->]; left; exists v. -by move=>G /= [p' [H1 ->]]; right; exists sc, p'. -Qed. - -Lemma stepPar W A s1 ps this sc s2 (q : proc W A) : - pstep s1 (ParProc ps) this sc s2 q <-> - exists n sc', - sc = ParStep n sc' /\ - exists p p' ps1 ps2, - [/\ ps = ps1 ++ (n, p) :: ps2, - q = ParProc (ps1 ++ (n, p') :: ps2), - (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2)& - pstep s1 p n sc' s2 p']. -Proof. -split=>/=; last first. -- case=>n[s'][->{sc}][p][p'][ps1][ps2][->->{ps q}]U[C] H1 H2. - split=>//=; last by exists p, p', ps1, ps2. - split=>//; clear H2 p'; case: U=>[[[p' ps1']] ps2'][Z]E. - case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps2' ps1'. - by move=>x1 x2 x3; case/(E (x1, x2, x3))=><-. -case; case: sc=>//n sc' C/=G1 G2; exists n, sc'; split=>//. -case:G1; case=>[[[p ps1]ps2]]U H; case: U=>Z U; subst ps. -case: G2=>p1[p'][ps1'][ps2'][Z]S->. -case: (U (p1, ps1', ps2') Z)=>Z1 Z2 Z3. subst p1 ps1' ps2'. -move: (H _ _ _ Z)=>{H Z}H. -by exists p, p', ps1, ps2; split=>//; exists (p, ps1, ps2). -Qed. - -Lemma stepInject V W K A (em : injects V W K) - s1 (t : proc V A) this sc s2 (q : proc W A) : - pstep s1 (Inject em t) this sc s2 q <-> - (* Case 1 : stepped to the final state s1' of the inner program*) - (exists s1' v, [/\ sc = InjectRet, t = Ret v, q = Ret v, s2 = s1 & - extends em s1 s1']) \/ - (* Case 2 : stepped to the nextx state s12 of the inner program*) - exists sc' t' s1' s2' s, - [/\ sc = InjectStep sc', q = Inject em t', - s1 = s1' \+ s, s2 = s2' \+ s, s1 \In Coh W & - pstep s1' t this sc' s2' t']. -Proof. -split; last first. -- case. - + case=>s1' [v][->->->->] E. - split=>//=; [by case: E=>x[] | by exists s1'|by exists s1']. - case=>sc' [t'][s1'][s2'][s][->->->-> C][[C' S] T]. - split=>//=; last by exists s1', s2', s, t'. - by exists s1'; split=>//; exists s. -case=>C; case: sc=>//=; last first. -- case: t=>//= v [C1 S][s1'][->->{s2 q}] X. - by left; exists s1'; exists v. -move=>sc /= [s'][X] S [s1'][s2'][t'][t2'][??? C1'] T; subst q s1 s2. -right; exists sc, t2', s1', s2', t'; do !split=>//. -by case: X=>t'' [E] Cs' _; rewrite (coh_prec (cohS C) E _ Cs'). -Qed. - -Lemma stepWithInv W A pr I (ii : InductiveInv pr I) s1 - (t : proc (mkWorld pr) A) this sc s2 (q : proc W A) pf : - pstep s1 (WithInv pr I ii pf t) this sc s2 q <-> - (exists v, [/\ sc = WithInvRet, t = Ret v, q = Ret v, s2 = s1, - s1 \In Coh W & W = mkWorld (ProtocolWithIndInv ii)]) \/ - exists sc' t' , [/\ sc = WithInvStep sc', q = WithInv pr I ii pf t', - W = mkWorld (ProtocolWithIndInv ii), - s1 \In Coh W & pstep s1 t this sc' s2 t']. -Proof. -split; last first. -- case. - + by case=>v[->->->->{s2}]C E; split=>//=; exists s1. - by case=>sc' [t'][->->{sc q}]E C[C' S]T; split=>//=; exists t'. -case=>C; case: sc=>//=; last first. -- by case: t=>//=v _[s1'][Z1]Z2 Z3; subst s2 s1' q; left; exists v. -move=>sc /=S[t'][->{q}T]; right; exists sc, t'; split=>//. -by split=>//; subst W; apply: (with_inv_coh C). -Qed. - -(* - -[Stepping and network semantics] - -The following lemma ensures that the operational semantics of our -programs respect the global network semantics. - - *) - -Lemma pstep_network_sem (W : world) A s1 (t : proc W A) this sc s2 q : - pstep s1 t this sc s2 q -> network_step W this s1 s2. -Proof. -elim: sc W A this s1 s2 t q=>/=. -- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + (* move=>n a. *) - (* Check (stepAct s1 a ActStep s2 q). *) - (* [v][pf][Z1]Z2 H. subst q; apply: (a_step_sem H). *) - admit. - + by move=>???; case. - + by move=>????; case. - by move=>?????; case. -- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + move=>B p p0/stepSeq; case=>[[v][_]??? C|[sc'][p'][]]//. - by subst p s2; apply: Idle. - by move=>????/stepInject; case=>[[?][?][?]|[?][?][?][?][?][?]]//. - by move=>?????; case. -- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + move=>B p p0/stepSeq; case=>[[?][?]|[sc'][p'][][]? ?]//. - by subst sc' q; apply: HI. - by move=>????; case=>? _. - by move=>?????; case. -- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + by move=>B p p0; case. - move=>V K pf p/stepInject; case=>[[?][?][?]|[sc'][t'][s1'][s2'][s][][]????]//. - subst sc' q s1 s2=>C; move/HI=>S; apply: (sem_extend pf)=>//. - apply/(cohE pf); exists s2', s; case: (step_coh S)=>C1 C2; split=>//. - move/(cohE pf): (C)=>[s1][s2][E]C' H. - by move: (coh_prec (cohS C) E C1 C')=>Z; subst s1'; rewrite (joinfK (cohS C) E). - by move=>?????; case. -- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + by move=>???; case. - + move=>V K i p; case/stepInject=>[[s1'][v][_]??? X|[?][?][?][?][?][?]]//. - by subst p q s2; apply: Idle; split=>//; case: X=>x []. - by move=>?????; case. -- move=>sc HI W A this s1 s2 p q; case: p; - do?[by case|by move=>?; case| by move=>??; case - |by move=>???; case|by move=>????; case]. - move=>pr I ii E p; case/(stepWithInv s1); first by case=>?; case. - case=>sc'[t'][][]Z1 Z2 _ C1; subst q sc'. - by move/HI=>T; subst W; apply: with_inv_step. -- move=>W A this s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case]. - case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3. - by subst s1' s2 q; apply: Idle. -move=>n sc HI W A this s1 s2 p q; case: p=>//; -do?[by case|by move=>?; case|by move=>???; case|by move=>????; case - |by move=>?????; case|by move=>??; case]. -move=>ps/stepPar=>[[m]][sc']; case; case=>Z1 Z2; subst n sc'. -case=>p[p'][ps1][ps2]. - - by case=>p[p'][ps1][ps2][_]_ _; apply: HI. -Qed. - -(* - -[Inductive invariants and stepping] - -The following lemma is the crux of wrapping into inductive invariants, as -it leverages the proof of the fact that each transition preserves the invariant. - -*) - -Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc - (t t' : proc this (mkWorld pr) A): - s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) -> - pstep s1 t sc s2 t' -> - s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). -Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. - -End ProcessSemantics. -Inductive schedule := - ActStep | SeqRet | SeqStep of schedule | - InjectStep of schedule | InjectRet | - WithInvStep of schedule | WithInvRet | - (* Step node number n *) - ParStep (n : nid) of schedule. - -End ProcessSyntax. - -Implicit Arguments Unfinished [W A]. -Implicit Arguments Ret [W A]. -Implicit Arguments Act [W A]. -Implicit Arguments Seq [W A B]. -Implicit Arguments WithInv [W A]. -Implicit Arguments ParProc [W A]. - -Section ProcessSemantics. - -Fixpoint step (W : world) A (s1 : state) (p1 : proc W A) - sc (s2 : state) (p2 : proc W A) : Prop := - match sc, p1 with - (* Action - make a step *) - | ActStep, Act this a => exists v pf, @a_step _ _ this a s1 pf s2 v /\ p2 = Ret v - (* Sequencing - apply a continuation *) - | SeqRet, Seq _ (Ret v) k => s2 = s1 /\ p2 = k v - | SeqStep sc', Seq _ p' k1 => - exists p'', step s1 p' sc' s2 p'' /\ p2 = Seq p'' k1 - (* Injection of a non-reduced term *) - | InjectRet, Inject V K pf (Ret v) => - exists s1', [/\ s2 = s1, p2 = Ret v & extends pf s1 s1'] - | InjectStep sc', Inject V K pf t1' => - exists s1' s2' s t2', - [/\ p2 = Inject pf t2', s1 = s1' \+ s, s2 = s2' \+ s, - s1' \In Coh V & step s1' t1' sc' s2' t2'] - (* Imposing an inductive invariant on a non-reduced term *) - | WithInvRet, WithInv p inv ii pf (Ret v) => - exists s1', [/\ s2 = s1, p2 = Ret v & s1 = s1'] - | WithInvStep sc', WithInv p inv ii pf t1' => - exists t2', p2 = WithInv p inv ii pf t2' /\ - step s1 t1' sc' s2 t2' - | ParStep n sc', ParProc ps => - exists p p' ps1 ps2, - [/\ ps = ps1 ++ (n, p) :: ps2, - step s1 p sc' s2 p' & - p2 = ParProc (ps1 ++ (n, p') :: ps2)] - | _, _ => False - end. - -Fixpoint good (W : world) A (p : proc W A) sc : Prop := - match sc, p with - | ActStep, Act _ _ => True - | SeqRet, Seq _ (Ret _) _ => True - | SeqStep sc', Seq _ p' _ => good p' sc' - | InjectStep sc', Inject _ _ _ p' => good p' sc' - | InjectRet, Inject _ _ _ (Ret _) => True - | WithInvStep sc', WithInv _ _ _ _ p' => good p' sc' - | WithInvRet, WithInv _ _ _ _ (Ret _) => True - | ParStep n sc', ParProc ps => - exists p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 /\ good p sc' - | _, _ => False - end. - -(* - -[Safety in small-step semantics] - -The safety (in order to make the following step) with respect to the -schedule is defined inductively on the shape of the program and the -schedule. Omitting the schedule is not a good idea, at it's required -in order to "sequentialize" the execution of the program -structure. Once it's dropped, this structure is lost. - - *) - -Fixpoint safe (W : world) A (p : proc W A) (this : nid) sc (s : state) : Prop := - match sc, p with - | ActStep, Act n a => n == this /\ @a_safe _ _ n a s - | SeqRet, Seq _ (Ret _) _ => True - | SeqStep sc', Seq _ p' _ => safe p' this sc' s - | InjectStep sc', Inject V K pf p' => - exists s', extends pf s s' /\ safe p' this sc' s' - | InjectRet, Inject V K pf (Ret _) => exists s', extends pf s s' - | WithInvStep sc', WithInv _ _ _ _ p' => safe p' this sc' s - | WithInvRet, WithInv _ _ _ _ (Ret _) => True - | ParStep n sc', ParProc ps => - (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2) /\ - (forall p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 -> safe p n sc' s) - | _, _ => True - end. - -Definition pstep (W : world) A s1 (p1 : proc W A) this sc s2 p2 := - [/\ s1 \In Coh W, safe p1 this sc s1 & step s1 p1 sc s2 p2]. - -(* Some sanity lemmas wrt. stepping *) - -Lemma pstep_safe (W : world) A s1 (t : proc W A) this sc s2 q : - pstep s1 t this sc s2 q -> safe t this sc s1. -Proof. by case. Qed. - -(* - -The following lemma established the operational "progress" property: a -program, which is safe and also the schedule is appropriate. Together, -this implies that we can do a step. - *) - -Lemma proc_progress W A s (p : proc W A) this sc : - s \In Coh W -> safe p this sc s -> good p sc -> - exists s' (p' : proc W A), pstep s p this sc s' p'. -Proof. -move=>C H1 H2; elim: sc W A this s p H2 H1 C=>[||sc IH|sc IH||sc IH||n sc IH]W A this s. -- case=>//=n a _/= [E H]; move/a_step_total: (H)=>[s'][r]H'. - by exists s', (Ret r); split=>//=; exists r, H. -- by case=>//; move=>B p k/=; case: p=>//b _ _; exists s, (k b). -- case=>//B p k/=H1 H2 C. - case: (IH W B this s p H1 H2 C)=>s'[p'][G1 G2]. - by exists s', (Seq p' k); split=>//; exists p'. -- case=>// V K pf p/=H1 [z][E]H2 C. - case: (E)=>s3[Z] C1 C2. - case: (IH V A this z p H1 H2 C1) =>s'[p']H3; case: H3=>S St. - exists (s' \+ s3), (Inject pf p'); split=>//; first by exists z. - by subst s; exists z, s', s3, p'. -- case=>//V K pf; case=>// v/=_[s'] E C. - by exists s, (Ret v); split=>//=; exists s'. -- case=>//pr I ii E p/= H1 H2 C. - have C' : s \In Coh (mkWorld pr) by subst W; apply: (with_inv_coh C). - case: (IH (mkWorld pr) A this s p H1 H2 C')=>s'[p']H3. - exists s', (WithInv pr I ii E p'); split=>//=. - by exists p'; split=>//; case: H3. -- case=>//pr I ii E; case=>//v/=_ _ C. - by exists s, (Ret v); split=>//=; exists s. -case=>//ps/=[p][ps1][ps2][Z]G1; subst ps. -case=>[[[[p' ps1'] ps2'] G2]]; case: G2=>E1 E; rewrite E1. -case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps1' ps2'; clear E1. -move/(_ p ps1 ps2 (erefl _))=>S C. -case: (IH W A n s p G1 S C)=>s'[p']H; exists s', (ParProc (ps1 ++ (n, p') :: ps2)). -split=>//=; last by exists p, p', ps1, ps2; split=>//; case: H. -split; last by move=> x1 x2 x3; case/(E (x1, x2, x3))=><-. -by exists (p, ps1, ps2). -Qed. - -(* Some view lemmas for processes and corresponding schedules *) - -Lemma stepUnfin W A s1 this sc s2 (t : proc W A) : - pstep s1 Unfinished this sc s2 t <-> False. -Proof. by split=>//; case; case: sc. Qed. - -Lemma stepRet W A s1 this sc s2 (t : proc W A) v : - pstep s1 (Ret v) this sc s2 t <-> False. -Proof. by split=>//; case; case: sc. Qed. - -Lemma stepAct W A s1 this a sc s2 (t : proc W A) : - pstep s1 (Act this a) this sc s2 t <-> - exists v pf, [/\ sc = ActStep, t = Ret v & @a_step _ _ _ a s1 pf s2 v]. -Proof. -split; first by case=>C; case: sc=>//= c [v [pf [H ->]]]; exists v, pf. -case=>v[pf] [->-> H]; split=>//; last by exists v, pf. -by apply: (a_safe_coh pf). -Qed. - -Lemma stepSeq W A B s1 (t : proc W B) k this sc s2 (q : proc W A) : - pstep s1 (Seq t k) this sc s2 q <-> - (exists v, [/\ sc = SeqRet, t = Ret v, q = k v, s2 = s1 & - s1 \In Coh W]) \/ - exists sc' p', - [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t this sc' s2 p']. -Proof. -split; last first. -- case; first by case=>v [->->->->]. - by case=>sc' [t'][->->][S H]; do !split=>//; exists t'. -case; case: sc=>//[|sc] C. -- by case: t=>//= v _ [->->]; left; exists v. -by move=>G /= [p' [H1 ->]]; right; exists sc, p'. -Qed. - -Lemma stepPar W A s1 ps this sc s2 (q : proc W A) : - pstep s1 (ParProc ps) this sc s2 q <-> - exists n sc', - sc = ParStep n sc' /\ - exists p p' ps1 ps2, - [/\ ps = ps1 ++ (n, p) :: ps2, - q = ParProc (ps1 ++ (n, p') :: ps2), - (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2)& - pstep s1 p n sc' s2 p']. -Proof. -split=>/=; last first. -- case=>n[s'][->{sc}][p][p'][ps1][ps2][->->{ps q}]U[C] H1 H2. - split=>//=; last by exists p, p', ps1, ps2. - split=>//; clear H2 p'; case: U=>[[[p' ps1']] ps2'][Z]E. - case: (E (p, ps1, ps2) (erefl _))=>Z1 Z2 Z3; subst p' ps2' ps1'. - by move=>x1 x2 x3; case/(E (x1, x2, x3))=><-. -case; case: sc=>//n sc' C/=G1 G2; exists n, sc'; split=>//. -case:G1; case=>[[[p ps1]ps2]]U H; case: U=>Z U; subst ps. -case: G2=>p1[p'][ps1'][ps2'][Z]S->. -case: (U (p1, ps1', ps2') Z)=>Z1 Z2 Z3. subst p1 ps1' ps2'. -move: (H _ _ _ Z)=>{H Z}H. -by exists p, p', ps1, ps2; split=>//; exists (p, ps1, ps2). -Qed. - -Lemma stepInject V W K A (em : injects V W K) - s1 (t : proc V A) this sc s2 (q : proc W A) : - pstep s1 (Inject em t) this sc s2 q <-> - (* Case 1 : stepped to the final state s1' of the inner program*) - (exists s1' v, [/\ sc = InjectRet, t = Ret v, q = Ret v, s2 = s1 & - extends em s1 s1']) \/ - (* Case 2 : stepped to the nextx state s12 of the inner program*) - exists sc' t' s1' s2' s, - [/\ sc = InjectStep sc', q = Inject em t', - s1 = s1' \+ s, s2 = s2' \+ s, s1 \In Coh W & - pstep s1' t this sc' s2' t']. -Proof. -split; last first. -- case. - + case=>s1' [v][->->->->] E. - split=>//=; [by case: E=>x[] | by exists s1'|by exists s1']. - case=>sc' [t'][s1'][s2'][s][->->->-> C][[C' S] T]. - split=>//=; last by exists s1', s2', s, t'. - by exists s1'; split=>//; exists s. -case=>C; case: sc=>//=; last first. -- case: t=>//= v [C1 S][s1'][->->{s2 q}] X. - by left; exists s1'; exists v. -move=>sc /= [s'][X] S [s1'][s2'][t'][t2'][??? C1'] T; subst q s1 s2. -right; exists sc, t2', s1', s2', t'; do !split=>//. -by case: X=>t'' [E] Cs' _; rewrite (coh_prec (cohS C) E _ Cs'). -Qed. - -Lemma stepWithInv W A pr I (ii : InductiveInv pr I) s1 - (t : proc (mkWorld pr) A) this sc s2 (q : proc W A) pf : - pstep s1 (WithInv pr I ii pf t) this sc s2 q <-> - (exists v, [/\ sc = WithInvRet, t = Ret v, q = Ret v, s2 = s1, - s1 \In Coh W & W = mkWorld (ProtocolWithIndInv ii)]) \/ - exists sc' t' , [/\ sc = WithInvStep sc', q = WithInv pr I ii pf t', - W = mkWorld (ProtocolWithIndInv ii), - s1 \In Coh W & pstep s1 t this sc' s2 t']. -Proof. -split; last first. -- case. - + by case=>v[->->->->{s2}]C E; split=>//=; exists s1. - by case=>sc' [t'][->->{sc q}]E C[C' S]T; split=>//=; exists t'. -case=>C; case: sc=>//=; last first. -- by case: t=>//=v _[s1'][Z1]Z2 Z3; subst s2 s1' q; left; exists v. -move=>sc /=S[t'][->{q}T]; right; exists sc, t'; split=>//. -by split=>//; subst W; apply: (with_inv_coh C). -Qed. - -(* - -[Stepping and network semantics] - -The following lemma ensures that the operational semantics of our -programs respect the global network semantics. - - *) - -Lemma pstep_network_sem (W : world) A s1 (t : proc W A) this sc s2 q : - pstep s1 t this sc s2 q -> network_step W this s1 s2. -Proof. -elim: sc W A this s1 s2 t q=>/=. -- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + (* move=>n a. *) - (* Check (stepAct s1 a ActStep s2 q). *) - (* [v][pf][Z1]Z2 H. subst q; apply: (a_step_sem H). *) - admit. - + by move=>???; case. - + by move=>????; case. - by move=>?????; case. -- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + move=>B p p0/stepSeq; case=>[[v][_]??? C|[sc'][p'][]]//. - by subst p s2; apply: Idle. - by move=>????/stepInject; case=>[[?][?][?]|[?][?][?][?][?][?]]//. - by move=>?????; case. -- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + move=>B p p0/stepSeq; case=>[[?][?]|[sc'][p'][][]? ?]//. - by subst sc' q; apply: HI. - by move=>????; case=>? _. - by move=>?????; case. -- move=>sc HI W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + by move=>B p p0; case. - move=>V K pf p/stepInject; case=>[[?][?][?]|[sc'][t'][s1'][s2'][s][][]????]//. - subst sc' q s1 s2=>C; move/HI=>S; apply: (sem_extend pf)=>//. - apply/(cohE pf); exists s2', s; case: (step_coh S)=>C1 C2; split=>//. - move/(cohE pf): (C)=>[s1][s2][E]C' H. - by move: (coh_prec (cohS C) E C1 C')=>Z; subst s1'; rewrite (joinfK (cohS C) E). - by move=>?????; case. -- move=>W A this s1 s2 p q; case: p; do?[by case|by move=>?; case| by move=>??; case]. - + by move=>???; case. - + move=>V K i p; case/stepInject=>[[s1'][v][_]??? X|[?][?][?][?][?][?]]//. - by subst p q s2; apply: Idle; split=>//; case: X=>x []. - by move=>?????; case. -- move=>sc HI W A this s1 s2 p q; case: p; - do?[by case|by move=>?; case| by move=>??; case - |by move=>???; case|by move=>????; case]. - move=>pr I ii E p; case/(stepWithInv s1); first by case=>?; case. - case=>sc'[t'][][]Z1 Z2 _ C1; subst q sc'. - by move/HI=>T; subst W; apply: with_inv_step. -- move=>W A this s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case]. - case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3. - by subst s1' s2 q; apply: Idle. -move=>n sc HI W A this s1 s2 p q; case: p=>//; -do?[by case|by move=>?; case|by move=>???; case|by move=>????; case - |by move=>?????; case|by move=>??; case]. -move=>ps/stepPar=>[[m]][sc']; case; case=>Z1 Z2; subst n sc'. -case=>p[p'][ps1][ps2]. - - by case=>p[p'][ps1][ps2][_]_ _; apply: HI. -Qed. - -(* - -[Inductive invariants and stepping] - -The following lemma is the crux of wrapping into inductive invariants, as -it leverages the proof of the fact that each transition preserves the invariant. - -*) - -Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc - (t t' : proc this (mkWorld pr) A): - s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) -> - pstep s1 t sc s2 t' -> - s2 \In Coh (mkWorld (ProtocolWithIndInv ii)). -Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. - -End ProcessSemantics. \ No newline at end of file From 6e0ca9c0a979383162d738410cb26acda4b03eb0 Mon Sep 17 00:00:00 2001 From: Ilya Sergey Date: Wed, 7 Jun 2017 21:01:34 +0100 Subject: [PATCH 3/3] more into parallel semantics --- Core/Always.v | 7 +++++++ Core/Process.v | 8 ++------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/Core/Always.v b/Core/Always.v index 77ddda1..84a6984 100644 --- a/Core/Always.v +++ b/Core/Always.v @@ -34,6 +34,13 @@ Fixpoint always_sc A (s1 : state) p scs (P : state -> proc A -> Prop) : Prop := Definition always A s (p : proc A) P := forall scs, always_sc s p scs P. +Fixpoint par_always_sc A (s1 : state) ps scs (P : state -> par_proc W A -> Prop) : Prop := + s1 \In coherent /\ + if scs is sc :: scs' then + [/\ par_safe ps sc s1, P s1 ps & + forall s2 qs, @par_pstep W A s1 ps sc s2 qs -> par_always_sc s2 qs scs' P] + else P s1 ps. + (* Some basic properties of the alwas predicate *) Lemma alw_coh' A s (p : proc A) scs P : diff --git a/Core/Process.v b/Core/Process.v index 0ce1fc5..86df04b 100644 --- a/Core/Process.v +++ b/Core/Process.v @@ -302,12 +302,10 @@ Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed. Definition par_proc W A := seq (nid * proc W A). -Inductive par_schedule := - Done | ParStep (n : nid) of schedule. +Inductive par_schedule := ParStep (n : nid) of schedule. Definition par_good (W : world) A (ps : par_proc W A) sc : Prop := match sc with - | Done => False | ParStep n sc' => exists p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 /\ good p sc' end. Definition par_safe (W : world) A (ps : par_proc W A) sc (s : state) : Prop := @@ -315,7 +313,6 @@ Definition par_safe (W : world) A (ps : par_proc W A) sc (s : state) : Prop := | ParStep n sc' => (exists! pp, let: (p, ps1, ps2) := pp in ps = ps1 ++ (n, p) :: ps2) /\ (forall p ps1 ps2, ps = ps1 ++ (n, p) :: ps2 -> safe p n sc' s) - | _ => True end. (* Parallel stepping *) @@ -325,7 +322,6 @@ Definition par_step (W : world) A (s1 : state) (ps : par_proc W A) sc | ParStep n sc' => exists p p' ps1 ps2, [/\ ps = ps1 ++ (n, p) :: ps2, step s1 p sc' s2 p' & ps' = (ps1 ++ (n, p') :: ps2)] - | _ => False end. Definition par_pstep (W : world) A s1 (ps : par_proc W A) sc s2 p2 := @@ -340,7 +336,7 @@ Proof. by case. Qed. Lemma par_pstep_network_sem (W : world) A s1 (t : par_proc W A) sc s2 q : par_pstep s1 t sc s2 q -> exists n p, (n, p) \In t /\ network_step W n s1 s2. Proof. -case: sc =>//=; first by case=>//. +case: sc =>//=. move=>n sc; case=>/= C; case; case=>[[[p ps1] ps2]][E]H1 H2; subst t. case=>x[p'][ps3][ps4][E]S Z; subst q. case/(H1 (x, ps3, ps4)): E=> Z1 Z2 Z3; subst x ps3 ps4.