(* Network Calculus *)
(**)
(* Hax, trix and required modules *)
(* (module systems are hard, let's go proving) *)
Require Export Coq.Strings.String.
Require Export Coq.Bool.Bool.
Require Export Coq.Program.Equality.
Require Export Coq.Logic.Classical.
Require Export Coq.Arith.Max.
Require Import Omega.
(* Is this really not importable from somewhere? *)
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
(* Nice hack! http://www.cis.upenn.edu/~bcpierce/sf/Basics.html,
originally by Aaron Bohannon *)
Require String. Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
 H : _  _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
 assert_eq x name; move_to_top x
 fail 1 "because we are working on a different case" ].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
(* Hack done *)
(**)
(* Generalpurpose lemmas *)
Lemma forall_cons_cons_forall :
forall A p x0 xs,
(forall x : A, List.In x (x0 :: xs) > p x = true) <>
(p x0 = true /\ (forall x : A, List.In x xs > p x = true)).
Proof.
firstorder. subst. assumption.
Qed.
Lemma in_app_either :
forall A, forall x : A, forall xs ys, List.In x (app xs ys) <> List.In x xs \/ List.In x ys.
Proof.
firstorder.
Qed.
Fixpoint list_max (xs : list nat) : nat :=
match xs with
 [] => 0
 x :: xs' => let m := list_max xs' in if Compare_dec.gt_dec x m then x else m
end.
Example list_max0 : list_max [1; 4; 1; 6] = 6. auto. Qed.
Lemma element_of_list_max_le :
forall xs x, List.In x xs > x <= list_max xs.
Proof.
intro xs.
induction xs.
intros x H; inversion H.
intros x H.
simpl.
simpl in H; inversion H.
Case "a = x".
rewrite H0.
destruct (gt_dec x (list_max xs)).
auto.
omega.
Case "x in xs".
destruct (gt_dec a (list_max xs)).
assert (x <= list_max xs); [ apply IHxs; assumption  ]; omega.
apply IHxs; assumption.
Qed.
(**)
(* Network Calculus Syntax *)
Inductive leaf_st : Type :=
 no_state : leaf_st
 int_state : nat > leaf_st. (* spurious, but helps Coq generalize appropriately *)
Inductive val : Type :=
 vbase : leaf_st > val
 vatom : string > val
 vpair : val > val > val .
Inductive pat : Type :=
 pbase : leaf_st > pat
 patom : string > pat
 ppair : pat > pat > pat
 pwild : pat .
Inductive route : Type :=
 pub : pat > nat > route
 sub : pat > nat > route
 rmeta : route > route .
Inductive msgevent : Type :=
 send : val > msgevent
 feedback : val > msgevent
 mmeta : msgevent > msgevent .
Inductive event : Type :=
 msg : msgevent > event
 newtable : list route > event .
Inductive action : Type :=
 evt : event > action
 spawn : spawnable > action
(* TODO: make a real spawnableactor refinement of actor type, to avoid instantiate_spec etc. *)
with spawnable : Type :=
 spawnLeaf : list route > list action > leaf_beh > leaf_st > spawnable
 spawnConfig : list spawnable > spawnable
with leaf_beh : Type :=
 primordial : leaf_beh
 fn_b : (event > leaf_st > list action * leaf_st) > leaf_beh
with beh : Type :=
 leaf : leaf_beh > leaf_st > beh
 config : config_st > beh
with config_st : Type :=
 cfg : list event > list route > list actor > config_st
with actor : Type :=
 act : list route > sigma > actor
with sigma : Type :=
 st : list action > beh > sigma.
(**)
(* Network Calculus metafunctions *)
Definition table_actor (a : actor) : list route :=
match a with
 act rs _ => rs
end.
Definition table (actors : list actor) : list route := List.flat_map table_actor actors.
Definition lift (rs : list route) : list route := List.map rmeta rs.
Fixpoint keep_somes {X : Type} (xs : list (option X)) : list X :=
match xs with
 [] => []
 Some x :: xs' => x :: keep_somes xs'
 None :: xs' => keep_somes xs'
end.
Definition drop_route (r : route) : option route :=
match r with
 rmeta r' => Some r'
 _ => None
end.
Definition drop (rs : list route) : list route := keep_somes (List.map drop_route rs).
Fixpoint vmatch (v : val) (p : pat) : Prop :=
match v, p with
 _, pwild => True
 vbase u, pbase u' => u = u'
 vatom x, patom x' => x = x'
 vpair v1 v2, ppair p1 p2 => vmatch v1 p1 /\ vmatch v2 p2
 _, _ => False
end.
Definition leaf_st_dec : forall u u' : leaf_st, { u = u' } + { u <> u' }.
decide equality; auto with arith.
Defined.
Definition vmatch_dec : forall v p, { vmatch v p } + { ~ vmatch v p }.
induction v; destruct p; simpl; try solve [apply leaf_st_dec  apply string_dec  tauto].
(* Pair/Pair is the only tricky case. *)
elim IHv1 with (p := p1); elim IHv2 with (p := p2); firstorder.
Defined.
Fixpoint pmatch (p1 : pat) (p2 : pat) : option pat :=
match p1, p2 with
 p1, pwild => Some p1
 pwild, p2 => Some p2
 pbase u1, pbase u2 => if leaf_st_dec u1 u2 then Some p1 else None
 patom x1, patom x2 => if string_dec x1 x2 then Some p1 else None
 ppair p11 p12, ppair p21 p22 =>
match pmatch p11 p21, pmatch p12 p22 with
 Some p1', Some p2' => Some (ppair p1' p2')
 _, _ => None
end
 _, _ => None
end.
Theorem pmatch_refl: forall p, pmatch p p = Some p.
Proof.
intros.
induction p; simpl.
Case "Base". destruct leaf_st_dec; firstorder.
Case "Atom". destruct string_dec; firstorder.
Case "Pair". rewrite IHp1; rewrite IHp2; reflexivity.
Case "Wild". reflexivity.
Qed.
Theorem pmatch_comm: forall p q, pmatch p q = pmatch q p.
Proof.
double induction p q; try solve [auto].
Case "Base/Base".
simpl. intros. do 2 destruct leaf_st_dec; firstorder; rewrite e; reflexivity.
Case "Atom/Atom".
simpl. intros. do 2 destruct string_dec; firstorder; rewrite e; reflexivity.
Case "Pair/Pair".
intros. simpl.
rewrite H2. destruct (pmatch p0 p3).
rewrite H1. reflexivity.
reflexivity.
Qed.
Fixpoint rmatch (r1 : route) (r2 : route) : option route :=
match r1, r2 with
 sub p1 n, pub p2 m => if Compare_dec.ge_dec n m then None else
match pmatch p1 p2 with
 Some p => Some (sub p n)
 None => None
end
 pub p1 n, sub p2 m => if Compare_dec.ge_dec n m then None else
match pmatch p1 p2 with
 Some p => Some (pub p n)
 None => None
end
 rmeta r1', rmeta r2' => match rmatch r1' r2' with
 Some r => Some (rmeta r)
 None => None
end
 _, _ => None
end.
Definition intersect_routes' (rr : route * route) : option route :=
rmatch (fst rr) (snd rr).
Definition intersect_routes (rs1 : list route) (rs2 : list route) : list route :=
keep_somes (List.map intersect_routes' (List.list_prod rs1 rs2)).
Fixpoint sub_matches (v : val) (r : route) : bool :=
match r with
 sub p n => if vmatch_dec v p then true else false
 _ => false
end.
Fixpoint pub_matches (v : val) (r : route) : bool :=
match r with
 pub p n => if vmatch_dec v p then true else false
 _ => false
end.
Fixpoint filter_msgevent (m : msgevent) (rs : list route) : bool :=
match m with
 feedback v => List.existsb (pub_matches v) rs
 send v => List.existsb (sub_matches v) rs
 mmeta m' => filter_msgevent m' (drop rs)
end.
Definition filter_event (e : event) (rs : list route) : option event :=
match e with
 msg m => if filter_msgevent m rs then Some (msg m) else None
 newtable new_rs => Some (newtable (intersect_routes new_rs rs))
end.
(**)
(* Evaluation functions and reduction relations *)
Definition interp0 (f : leaf_beh) (e : event) (u : leaf_st) : list action * leaf_st :=
match f, e, u with
 primordial, _, _ => ([], u)
 fn_b f, e, u => let '(acs, u') := f e u in (acs, u')
end.
Definition quiescent_actor (a : actor) : bool :=
match a with
 act _ (st [] _) => true
 act _ (st _ _) => false
end.
Definition quiescent_actor_dec :
forall a,
{ quiescent_actor a = true } + { quiescent_actor a = false }.
intro.
induction quiescent_actor. left. reflexivity. right. reflexivity.
Defined.
Definition quiescent_config (C : config_st) : bool :=
match C with
 cfg [] _ actors => List.forallb quiescent_actor actors
 _ => false
end.
Fixpoint inert_config (C : config_st) : bool :=
match C with
 cfg [] _ actors => List.forallb inert_actor actors
 _ => false
end
with inert_actor (a : actor) : bool :=
match a with
 act _ (st [] b) => inert_behavior b
 act _ (st _ _) => false
end
with inert_behavior (b : beh) : bool :=
match b with
 leaf _ _ => true
 config C => inert_config C
end.
Definition inert_actor_dec :
forall a,
{ inert_actor a = true } + { inert_actor a = false }.
intro.
induction inert_actor. left. reflexivity. right. reflexivity.
Defined.
Inductive partition_actors : list actor > list actor > list actor > Prop :=
 pa_nil : partition_actors [] [] []
 pa_quiescent :
forall a actors qs ns,
quiescent_actor a = true >
partition_actors actors qs ns >
partition_actors (a :: actors) (a :: qs) ns
 pa_nonquiescent :
forall a actors,
quiescent_actor a = false >
partition_actors (a :: actors) [] (a :: actors).
Inductive partition_inerts : list actor > list actor > list actor > Prop :=
 pi_nil : partition_inerts [] [] []
 pi_inert :
forall a actors is qs,
inert_actor a = true >
partition_inerts actors is qs >
partition_inerts (a :: actors) (a :: is) qs
 pi_quiescent :
forall a actors,
inert_actor a = false >
List.forallb quiescent_actor (a :: actors) = true >
partition_inerts (a :: actors) [] (a :: actors).
Definition instantiate_spec (spec : spawnable) : actor :=
match spec with
 spawnLeaf rs acs f u => act rs (st acs (leaf f u))
 spawnConfig specs =>
act [] (st [] (config (cfg [] [] [act [] (st (List.map spawn specs)
(leaf primordial no_state))])))
end.
Definition inject (e : event) (C : config_st) : config_st :=
match C with
 cfg es rs actors =>
match e with
 msg m => cfg (app es [msg (mmeta m)]) rs actors
 newtable rs' => cfg (app es [newtable (app (table actors) (lift rs'))]) (lift rs') actors
end
end.
Inductive dispatch_arrow : actor > event > actor > Prop :=
 da_handle0 :
forall e rs e' f u acs' u',
filter_event e rs = Some e' >
interp0 f e' u = (acs', u') >
dispatch_arrow (act rs (st [] (leaf f u)))
e
(act rs (st acs' (leaf f u')))
 da_handleC :
forall e rs e' C C',
filter_event e rs = Some e' >
inject e' C = C' >
dispatch_arrow (act rs (st [] (config C)))
e
(act rs (st [] (config C')))
 da_ignore :
forall e rs Σ,
filter_event e rs = None >
dispatch_arrow (act rs Σ)
e
(act rs Σ).
Inductive dispatch_arrow_all : list actor > event > list actor > Prop :=
 daa_nil : forall e, dispatch_arrow_all [] e []
 daa_cons :
forall e a a' actors actors',
dispatch_arrow a e a' >
dispatch_arrow_all actors e actors' >
dispatch_arrow_all (a :: actors) e (a' :: actors').
Inductive arrow : sigma > sigma > Prop :=
 a_dispatch :
forall actors e actors' es acs0 rs1,
List.forallb quiescent_actor actors = true >
dispatch_arrow_all actors e actors' >
arrow (st acs0 (config (cfg (e :: es) rs1 actors)))
(st acs0 (config (cfg es rs1 actors')))
 a_send :
forall actors qs rs v acs b ns acs0 es rs1,
partition_actors actors qs (act rs (st (evt (msg (send v)) :: acs) b) :: ns) >
arrow (st acs0 (config (cfg es rs1 actors)))
(st acs0 (config (cfg (app es [msg (send v)]) rs1 (app qs (act rs (st acs b)
:: ns)))))
 a_feedback :
forall actors qs rs v acs b ns acs0 es rs1,
partition_actors actors qs (act rs (st (evt (msg (feedback v)) :: acs) b) :: ns) >
arrow (st acs0 (config (cfg es rs1 actors)))
(st acs0 (config (cfg (app es [msg (feedback v)]) rs1 (app qs (act rs (st acs b)
:: ns)))))
 a_relay_out :
forall actors qs rs m acs b ns acs0 es rs1,
partition_actors actors qs (act rs (st (evt (msg (mmeta m)) :: acs) b) :: ns) >
arrow (st acs0 (config (cfg es rs1 actors)))
(st (app acs0 [evt (msg m)]) (config (cfg es rs1 (app qs (act rs (st acs b)
:: ns)))))
 a_routes_out :
forall actors qs rs rs' acs b ns rs'' acs0 es rs1,
rs'' = app (table qs) (app rs' (table ns)) >
partition_actors actors qs (act rs (st (evt (newtable rs') :: acs) b) :: ns) >
arrow (st acs0
(config (cfg es rs1 actors)))
(st (app acs0 [evt (newtable (drop rs''))])
(config (cfg (app es [newtable (app rs'' rs1)])
rs1
(app qs (act rs' (st acs b) :: ns)))))
 a_spawn :
forall actors qs rs spec acs b ns acs0 rs' es rs1,
rs' = app (table qs) (app rs (app (table ns) (table_actor (instantiate_spec spec)))) >
partition_actors actors qs (act rs (st (spawn spec :: acs) b) :: ns) >
arrow (st acs0
(config (cfg es rs1 actors)))
(st (app acs0 [evt (newtable (drop rs'))])
(config (cfg (app es [newtable (app rs' rs1)])
rs1
(app qs (app (act rs (st acs b) :: ns) [instantiate_spec spec])))))
 a_schedule :
forall actors is rs Σq qs Σ' acs0 rs1,
partition_inerts actors is (act rs Σq :: qs) >
arrow Σq Σ' >
arrow (st acs0 (config (cfg [] rs1 actors)))
(st acs0 (config (cfg [] rs1 (app qs (app is [act rs Σ']))))).
(**)
(* Proofs about the system *)
Lemma partition_actors_properties :
forall actors qs ns,
partition_actors actors qs ns <>
((forall a, List.In a qs > quiescent_actor a = true) /\
(ns = [] \/ (forall a, a = List.hd a ns > quiescent_actor a = false)) /\
actors = app qs ns).
Proof.
intros.
split.
Case "forward".
intro.
induction H.
SCase "pa_nil".
simpl. tauto.
SCase "pa_quiescent".
split.
SSCase "qs quiescent".
apply forall_cons_cons_forall.
rewrite H. split. reflexivity.
apply IHpartition_actors.
split.
SSCase "ns head nonquiescent".
apply IHpartition_actors.
SSCase "actors = app qs ns".
simpl.
inversion IHpartition_actors. inversion H2. rewrite H4. reflexivity.
SCase "pa_nonquiescent".
split.
SSCase "qs quiescent".
simpl. tauto.
split.
SSCase "ns head nonquiescent".
right. simpl. intros. rewrite H0. assumption.
SSCase "actors = app qs ns".
simpl. reflexivity.
Case "backward".
intro.
inversion H as [Hqs]. inversion H0 as [Hnsn1 Hactorseq]. clear H H0.
dependent induction actors.
SCase "no actors".
destruct qs as [ q0 qs'].
destruct ns as [ n0 qs'].
(* only leaves us with three easy cases  the cons/cons case seems automatically proven *)
apply pa_nil.
simpl in Hactorseq. inversion Hactorseq.
simpl in Hactorseq. inversion Hactorseq.
SCase "some actors".
destruct qs.
SSCase "no qs".
simpl in Hactorseq. rewrite < Hactorseq.
apply pa_nonquiescent.
inversion Hnsn1.
rewrite H in Hactorseq. inversion Hactorseq.
rewrite < Hactorseq in H.
simpl in H. apply H. reflexivity.
SSCase "some qs".
simpl in Hactorseq. inversion Hactorseq.
apply pa_quiescent.
apply Hqs. simpl. left. reflexivity.
rewrite < H1.
apply IHactors.
SSSCase "qs quiescent". apply forall_cons_cons_forall in Hqs. apply Hqs.
SSSCase "ns head nonquiescent". assumption.
SSSCase "actors = app qs ns". assumption.
Qed.
Lemma partition_ns_head_nonquiescent :
forall actors qs n ns,
partition_actors actors qs (n :: ns) > quiescent_actor n = false.
Proof.
intros.
apply partition_actors_properties in H.
inversion H as [Hqs]. inversion H0 as [Hnsn1 Hactorseq]. clear H H0.
inversion Hnsn1.
inversion H.
simpl in H. apply H. reflexivity.
Qed.
Lemma partition_inerts_properties :
forall actors is qs,
partition_inerts actors is qs <>
((forall a, List.In a is > inert_actor a = true) /\
(qs = [] \/ (forall a, a = List.hd a qs > inert_actor a = false)) /\
(forall a, List.In a qs > quiescent_actor a = true) /\
actors = app is qs).
Proof.
intros.
split.
Case "forward".
intro.
induction H.
SCase "pi_nil".
simpl. tauto.
SCase "pi_inert".
split.
SSCase "Hisi".
apply forall_cons_cons_forall.
rewrite H. split. reflexivity.
apply IHpartition_inerts.
split.
SSCase "Hqsq".
apply IHpartition_inerts.
SSCase "Hactorseq".
simpl.
inversion IHpartition_inerts.
inversion H2. inversion H4. clear H2 H4.
split.
assumption.
rewrite H6. reflexivity.
SCase "pi_quiescent".
split.
SSCase "Hisi".
simpl. tauto.
split.
SSCase "Hqsq".
right. simpl. intros. rewrite H1. assumption.
SSCase "Hactorseq".
split. rewrite < List.forallb_forall. assumption.
simpl. reflexivity.
Case "backward".
intro.
inversion H as [Hisi]. inversion H0 as [Hqs1ni]. inversion H1 as [Hqsq Hactorseq].
clear H H0 H1.
dependent induction actors.
SCase "no actors".
destruct is as [ i0 is'].
destruct qs as [ q0 qs'].
apply pi_nil.
simpl in Hactorseq. inversion Hactorseq.
simpl in Hactorseq. inversion Hactorseq.
SCase "some actors".
destruct is as [ i0 is'].
SSCase "no is".
simpl in Hactorseq. rewrite < Hactorseq. apply pi_quiescent.
inversion Hqs1ni.
rewrite < Hactorseq in H. inversion H.
apply H. rewrite < Hactorseq. simpl. reflexivity.
rewrite Hactorseq. rewrite List.forallb_forall. assumption.
SSCase "some is".
simpl in Hactorseq. inversion Hactorseq.
apply pi_inert.
apply Hisi. simpl. left. reflexivity.
rewrite < H1.
apply IHactors.
SSSCase "Hisi". apply forall_cons_cons_forall in Hisi. inversion Hisi. assumption.
SSSCase "Hqs1ni". assumption.
SSSCase "Hqsq". assumption.
SSSCase "Hactorseq". assumption.
Qed.
Lemma partition_inerts_actorseq :
forall actors is qs, partition_inerts actors is qs > actors = (app is qs).
Proof.
intros. apply partition_inerts_properties in H. inversion H. inversion H1. inversion H3.
assumption.
Qed.
Lemma partition_qs_head_properties :
forall actors is q qs,
partition_inerts actors is (q :: qs) > (inert_actor q = false /\ quiescent_actor q = true).
Proof.
intros.
apply partition_inerts_properties in H.
inversion H as [His]. inversion H0 as [Hqs1ni]. inversion H1 as [Hqsq Hactorseq]. clear H H0 H1.
split.
Case "noninert".
inversion Hqs1ni.
inversion H.
simpl in H. apply H. reflexivity.
Case "quiescent".
apply Hqsq. simpl. left. reflexivity.
Qed.
Lemma some_nonquiescent_actor_implies_config_nonquiescent :
forall actors qs n ns es rs1,
partition_actors actors qs (n :: ns) > quiescent_config (cfg es rs1 actors) = false.
Proof.
intros.
destruct es.
Case "no events".
apply partition_actors_properties in H.
inversion H as [Hqs]. inversion H0 as [Hnsn1 Hactorseq]. clear H H0.
inversion Hnsn1. inversion H. clear Hnsn1.
simpl. rewrite Hactorseq.
rewrite List.forallb_app. apply andb_false_iff. right.
simpl. rewrite H. reflexivity. simpl. reflexivity.
Case "some events".
reflexivity.
Qed.
Lemma some_nonquiescent_actor_implies_partitioning :
forall actors,
List.forallb quiescent_actor actors = false >
(exists qs n ns, partition_actors actors qs (n :: ns)).
Proof.
intros.
induction actors.
Case "no actors". inversion H.
Case "some actors".
simpl in H.
destruct (quiescent_actor_dec a).
SCase "quiescent".
rewrite e in H. simpl in H.
apply IHactors in H.
clear IHactors.
inversion H as [qs']. inversion H0 as [n']. inversion H1 as [ns']. clear H H0 H1.
exists (a :: qs'). exists n'. exists ns'. apply pa_quiescent. assumption. assumption.
SCase "nonquiescent".
exists []. exists a. exists actors.
apply pa_nonquiescent. assumption.
Qed.
Lemma inert_actors_are_quiescent :
forall actors,
List.forallb inert_actor actors = true > List.forallb quiescent_actor actors = true.
Proof.
induction actors; auto.
simpl. do 2 rewrite andb_true_iff.
destruct a as [rs [[ ac acs] b]]; firstorder.
Qed.
Lemma nonquiescent_actors_are_noninert :
forall actors,
List.forallb quiescent_actor actors = false > List.forallb inert_actor actors = false.
Proof.
induction actors; auto.
simpl. do 2 rewrite andb_false_iff.
destruct a as [rs [[ ac acs] b]]; firstorder.
Qed.
Lemma some_noninert_quiescent_actor_implies_partitioning :
forall actors,
List.forallb inert_actor actors = false >
List.forallb quiescent_actor actors = true >
(exists is q qs, partition_inerts actors is (q :: qs)).
Proof.
intros.
induction actors.
Case "no actors". inversion H.
Case "some actors".
simpl in H.
destruct (inert_actor_dec a).
SCase "inert".
rewrite e in H. simpl in H.
apply IHactors in H.
clear IHactors.
inversion H as [is']. inversion H1 as [q']. inversion H2 as [qs']. clear H H1 H2.
exists (a :: is'). exists q'. exists qs'. apply pi_inert.
assumption.
assumption.
simpl in H0. apply andb_true_iff in H0. inversion H0. assumption.
SCase "noninert".
exists []. exists a. exists actors.
apply pi_quiescent. assumption. assumption.
Qed.
Lemma inert_config_implies_quiescent :
forall C, inert_config C = true > quiescent_config C = true.
Proof.
intros.
destruct C as [[ e es] rs actors].
Case "no events".
simpl in H. simpl.
apply inert_actors_are_quiescent.
assumption.
Case "some events".
simpl in H. simpl. assumption.
Qed.
Lemma nonquiescent_config_implies_noninert :
forall C, quiescent_config C = false > inert_config C = false.
Proof.
intros.
destruct C as [[ e es] rs actors]; simpl in H; simpl;
[ apply nonquiescent_actors_are_noninert  ]; auto.
Qed.
Lemma steppable_is_noninert :
forall acs C,
(exists Σ', arrow (st acs (config C)) Σ') >
inert_config C = false.
Proof.
intros.
inversion H as [Σ' Hstep].
dependent induction Hstep; auto;
try ( apply some_nonquiescent_actor_implies_config_nonquiescent
with (es := es) (rs1 := rs1) in H0;
apply nonquiescent_config_implies_noninert in H0;
assumption ).
(* a_context is the only remaining case (a_dispatch was taken care
of by "auto") *)
simpl.
apply partition_inerts_properties in H0.
inversion_clear H0 as [Hisi [Hqs1ni [Hqsq Hactorseq]]].
rewrite Hactorseq.
rewrite List.forallb_app. apply andb_false_iff.
right. unfold List.forallb. apply andb_false_iff.
left.
inversion Hqs1ni.
inversion H0.
apply H0. simpl. reflexivity.
Qed.
Lemma dispatch_arrow_functionlike :
forall a e, quiescent_actor a = true > exists a', dispatch_arrow a e a'.
Proof.
intro a. intros.
destruct a as [rs [[ ac acs] [f u  C]]].
Case "no actions".
SCase "leaf".
remember (filter_event e rs) as filter_result.
destruct filter_result as [e' ].
SSCase "matches".
remember (interp0 f e' u) as interp_result.
destruct interp_result as [acs' u'].
exists (act rs (st acs' (leaf f u'))).
apply da_handle0 with (e' := e'); auto.
SSCase "doesn't match".
exists (act rs (st [] (leaf f u))).
apply da_ignore; auto.
SCase "config".
remember (filter_event e rs) as filter_result.
destruct filter_result as [e' ].
SSCase "matches".
remember (inject e' C) as C'.
exists (act rs (st [] (config C'))).
apply da_handleC with (e' := e'); auto.
SSCase "doesn't match".
exists (act rs (st [] (config C))).
apply da_ignore; auto.
Case "some actions".
SCase "leaf". inversion H.
SCase "config". inversion H.
Qed.
Lemma dispatch_arrow_all_functionlike :
forall actors e,
List.forallb quiescent_actor actors = true >
exists actors', dispatch_arrow_all actors e actors'.
Proof.
intro actors. intros.
induction actors.
exists []. apply daa_nil.
simpl in H. apply andb_true_iff in H. inversion_clear H.
apply IHactors in H1.
assert (exists a', dispatch_arrow a e a').
Case "assertion".
apply dispatch_arrow_functionlike.
assumption.
inversion H as [a'].
inversion H1 as [actors'].
exists (a' :: actors').
apply daa_cons; trivial.
Qed.
Fixpoint actor_size (a : actor) : nat :=
match a with
 act _ (st _ (leaf _ _)) => 0
 act _ (st _ (config C)) => config_size C
end
with config_size (C : config_st) : nat :=
match C with
 cfg _ _ actors => 1 + list_max (List.map actor_size actors)
end.
Lemma child_size_smaller_than_container_size :
forall es rs1 actors rs acs C,
List.In (act rs (st acs (config C))) actors >
config_size C < config_size (cfg es rs1 actors).
Proof.
intros.
destruct actors as [ a actors'].
Case "nil".
inversion H.
Case "cons".
remember (config_size C) as Csize.
unfold config_size. fold actor_size.
remember (List.map actor_size (a :: actors')) as actor_sizes.
apply le_lt_n_Sm.
apply element_of_list_max_le.
rewrite Heqactor_sizes.
assert (Csize = actor_size (act rs (st acs (config C)))); auto.
rewrite H0.
apply List.in_map.
assumption.
Qed.
(* Paper section 4, lemma 1 *)
Lemma progress_lemma:
forall Csize acs C,
config_size C <= Csize >
inert_config C = false >
exists Sigma', arrow (st acs (config C)) Sigma'.
Proof.
intro Csize.
induction Csize as [ Csize'].
Case "no size".
intros.
destruct C as [es rs actors].
unfold config_size in H. simpl in H. inversion H.
intros acs C Hsizebound H.
remember C as C1.
destruct C1 as [es rs1 actors].
remember (List.forallb inert_actor actors) as actors_i. symmetry in Heqactors_i.
destruct actors_i.
Case "actors inert".
destruct es as [ e es'].
SCase "no events".
simpl in H. contradict Heqactors_i. rewrite H. congruence.
SCase "some events".
assert (exists actors', dispatch_arrow_all actors e actors').
apply dispatch_arrow_all_functionlike.
apply inert_actors_are_quiescent.
assumption.
inversion H0 as [actors'].
exists (st acs (config (cfg es' rs1 actors'))).
apply a_dispatch; intuition (apply inert_actors_are_quiescent; assumption).
Case "some noninert actor".
remember actors as actors1.
destruct actors1 as [ a actors'].
SCase "no actors".
inversion Heqactors_i.
SCase "some actors".
remember (List.forallb quiescent_actor (a :: actors')) as actors_q. symmetry in Heqactors_q.
destruct actors_q.
SSCase "actors quiescent".
(* schedule *)
assert (Hpartitioning_exists := Heqactors_i).
apply some_noninert_quiescent_actor_implies_partitioning in Hpartitioning_exists; auto.
inversion_clear Hpartitioning_exists as [is [q [qs Hpartition]]].
destruct es as [ e es'].
SSSCase "no events".
destruct q as [rs [[ ac acs'] b]].
SSSSCase "no actions".
destruct b as [f u  Cq].
SSSSSCase "leaf".
apply partition_qs_head_properties in Hpartition.
inversion Hpartition. inversion H0.
SSSSSCase "config".
assert (exists Σ', arrow (st [] (config Cq)) Σ').
SSSSSSCase "assertion".
apply IHCsize'.
apply lt_n_Sm_le.
assert (config_size Cq < config_size (cfg [] rs1 (a :: actors'))).
apply child_size_smaller_than_container_size with (rs := rs) (acs := []).
apply partition_inerts_actorseq in Hpartition. rewrite Hpartition.
apply in_app_either; firstorder.
omega.
apply partition_qs_head_properties in Hpartition.
inversion Hpartition. apply H0.
inversion_clear H0 as [Σ'].
exists (st acs (config (cfg [] rs1 (app qs (app is [act rs Σ']))))).
apply a_schedule with (Σq := (st [] (config Cq))); assumption.
SSSSCase "some actions".
apply partition_qs_head_properties in Hpartition.
inversion Hpartition. inversion H1.
SSSCase "some event queued".
assert (exists actors'', dispatch_arrow_all (a :: actors') e actors'').
apply dispatch_arrow_all_functionlike; assumption.
inversion H0 as [actors''].
exists (st acs (config (cfg es' rs1 actors''))).
apply a_dispatch; assumption.
SSCase "some actor nonquiescent and noninert".
(* action pending *)
assert (Hpartitioning_exists := Heqactors_q).
apply some_nonquiescent_actor_implies_partitioning in Hpartitioning_exists.
inversion_clear Hpartitioning_exists as [qs [n [ns Hpartition]]].
remember n as n1.
destruct n1 as [x [[ ac acs'] b]].
SSSCase "no actions".
apply partition_ns_head_nonquiescent in Hpartition. inversion Hpartition.
SSSCase "some actions".
destruct ac as [[[v  v  m]  rs']  spec]; [
exists (st acs (config (cfg (app es [msg (send v)])
rs1
(app qs (act x (st acs' b) :: ns)))));
apply a_send

exists (st acs (config (cfg (app es [msg (feedback v)])
rs1
(app qs (act x (st acs' b) :: ns)))));
apply a_feedback

exists (st (app acs [evt (msg m)]) (config (cfg es
rs1
(app qs (act x (st acs' b) :: ns)))));
apply a_relay_out

remember (app (table qs) (app rs' (table ns))) as rs'';
exists (st (app acs [evt (newtable (drop rs''))])
(config (cfg (app es [newtable (app rs'' rs1)])
rs1
(app qs (act rs' (st acs' b) :: ns)))));
apply a_routes_out with (rs := x)

remember spec as spec0;
remember (app (table qs)
(app x (app (table ns) (table_actor (instantiate_spec spec)))))
as rs';
exists (st (app acs [evt (newtable (drop rs'))])
(config (cfg (app es [newtable (app rs' rs1)])
rs1
(app qs (app (act x (st acs' b) :: ns)
[instantiate_spec spec])))));
apply a_spawn; [  rewrite < Heqspec0 ]
]; auto.
Qed.
(* Paper section 4, theorem 3 *)
Theorem soundness :
forall b,
inert_behavior b = false <> (exists Sigma', arrow (st [] b) Sigma').
Proof.
split.
Case "forward".
intros.
destruct b as [f u  C].
SCase "leaf".
inversion H.
SCase "config".
apply progress_lemma with (Csize := config_size C); auto.
Case "backward".
intros.
destruct b as [f u  C].
SCase "leaf".
inversion H as [Sigma' Hstep].
dependent induction Hstep; auto.
SCase "config".
apply steppable_is_noninert in H; assumption.
Qed.
Lemma dispatch_arrow_deterministic :
forall a e a', dispatch_arrow a e a' > forall a'', dispatch_arrow a e a'' > a' = a''.
Proof.
intros a e a' H' a'' H''.
dependent induction H'; inversion H''; subst; auto;
try solve [ contradict H5; rewrite H; congruence (* filter can't be both some and none *)
 contradict H2; rewrite H; congruence (* filter can't be both some and none *) ].
Case "interp0 deterministic".
rewrite H in H6; inversion H6; subst; clear H6. (* ensure e' = e'0 *)
rewrite H7 in H0; inversion H0; reflexivity. (* interp0 equivalent *)
Case "inject deterministic".
rewrite H in H3; inversion H3; subst; clear H3. (* ensure e' = e'0 *)
reflexivity.
Qed.
Lemma dispatch_arrow_all_deterministic :
forall actors e actors',
List.forallb quiescent_actor actors = true >
dispatch_arrow_all actors e actors' >
forall actors'',
dispatch_arrow_all actors e actors'' > actors' = actors''.
Proof.
intros actors e actors' Hactorsq H' actors'' H''.
dependent induction actors; inversion H'; inversion H''; auto; subst.
simpl in Hactorsq. apply andb_true_iff in Hactorsq.
inversion_clear Hactorsq as [Haq Hactorsq0]. rename Hactorsq0 into Hactorsq.
apply dispatch_arrow_deterministic with (a' := a'0) in H1.
assert (actors'0 = actors'1).
apply IHactors with (e := e) (actors' := actors'0) (actors'' := actors'1); assumption.
subst. reflexivity.
assumption.
Qed.
Fixpoint partition_actors_fn (actors : list actor) : (list actor * list actor) :=
match actors with
 [] => ([], [])
 a :: actors' => if quiescent_actor a
then let '(qs, ns) := partition_actors_fn actors' in (a :: qs, ns)
else ([], actors)
end.
Lemma partition_actors_fn_refines_partition_actors :
forall actors qs ns, partition_actors actors qs ns <> partition_actors_fn actors = (qs, ns).
Proof.
intro actors.
induction actors.
Case "nil".
split; intro; inversion H; [ reflexivity  apply pa_nil ].
Case "cons".
split; intro.
SCase "forward".
inversion H.
SSCase "pa_quiescent".
simpl. rewrite H2.
assert (partition_actors_fn actors = (qs0, ns)).
SSSCase "assertion".
apply IHactors. assumption.
rewrite H6. reflexivity.
SSCase "pa_nonquiescent".
simpl. rewrite H4. reflexivity.
SCase "backward".
simpl in H.
remember (quiescent_actor a) as aq. symmetry in Heqaq.
destruct aq.
SSCase "quiescent".
destruct qs; destruct (partition_actors_fn actors) as [qs' ns']; inversion H.
(* cons case remains *)
apply pa_quiescent. rewrite < H1. assumption.
apply IHactors. subst. reflexivity.
SSCase "nonquiescent".
inversion H.
apply pa_nonquiescent; assumption.
Qed.
Lemma partition_actors_unique :
forall actors qs ns,
partition_actors actors qs ns >
forall qs' ns',
partition_actors actors qs' ns' > qs = qs' /\ ns = ns'.
Proof.
intros actors qs ns H qs' ns' H'.
apply partition_actors_fn_refines_partition_actors in H.
apply partition_actors_fn_refines_partition_actors in H'.
rewrite H in H'.
inversion H'.
auto.
Qed.
Fixpoint partition_inerts_fn (actors : list actor) : option (list actor * list actor) :=
match actors with
 [] => Some ([], [])
 a :: actors' => if inert_actor a
then match partition_inerts_fn actors' with
 None => None
 Some (is, qs) => Some (a :: is, qs)
end
else if List.forallb quiescent_actor actors
then Some ([], actors)
else None
end.
Lemma partition_inerts_fn_refines_partition_inerts :
forall actors is qs, partition_inerts actors is qs <> partition_inerts_fn actors = Some (is, qs).
Proof.
intro actors.
induction actors.
Case "nil".
split; intro; inversion H; [ reflexivity  apply pi_nil ].
Case "cons".
split; intro.
SCase "forward".
inversion H; subst; simpl; rewrite H2.
SSCase "pi_inert".
assert (partition_inerts_fn actors = Some (is0, qs)).
apply IHactors. assumption.
rewrite H0. reflexivity.
SSCase "pi_quiescent".
simpl in H5; apply andb_true_iff in H5; inversion_clear H5.
rewrite H0. rewrite H1. reflexivity.
SCase "backward".
simpl in H.
remember (inert_actor a) as ai; symmetry in Heqai.
destruct ai.
SSCase "inert".
destruct is; destruct (partition_inerts_fn actors) as [[is' ns']  ]; inversion H.
subst; apply pi_inert. assumption.
apply IHactors. reflexivity.
SSCase "noninert".
remember (quiescent_actor a && List.forallb quiescent_actor actors) as allq;
symmetry in Heqallq.
destruct allq.
inversion H; apply pi_quiescent. assumption.
simpl; assumption.
inversion H.
Qed.
Lemma partition_inerts_unique :
forall actors is qs,
partition_inerts actors is qs >
forall is' qs',
partition_inerts actors is' qs' > is = is' /\ qs = qs'.
Proof.
intros actors is qs H is' qs' H'.
apply partition_inerts_fn_refines_partition_inerts in H.
apply partition_inerts_fn_refines_partition_inerts in H'.
rewrite H in H'.
inversion H'.
auto.
Qed.
Lemma partition_ns_head_nonquiescent_all :
forall actors qs n ns,
partition_actors actors qs (n :: ns) > List.forallb quiescent_actor actors = false.
Proof.
intros.
apply some_nonquiescent_actor_implies_config_nonquiescent with (es := []) (rs1 := []) in H.
simpl in H.
assumption.
Qed.
Lemma partition_inerts_implies_partition_actors_all_quiescent :
forall actors is qs,
partition_inerts actors is qs > partition_actors actors actors [].
Proof.
intros.
apply partition_inerts_properties in H.
inversion_clear H as [Hisi [Hqs1ni [Hqsq Hactorseq]]].
rewrite < List.forallb_forall in Hisi.
apply inert_actors_are_quiescent in Hisi.
rewrite < List.forallb_forall in Hqsq.
assert (List.forallb quiescent_actor actors = true).
rewrite Hactorseq. rewrite List.forallb_app. rewrite Hisi. rewrite Hqsq. reflexivity.
rewrite List.forallb_forall in H.
apply partition_actors_properties.
split.
assumption.
split.
left; reflexivity.
rewrite List.app_nil_r; reflexivity.
Qed.
Ltac contradict_dispatch_and_action :=
match goal with
 hp1:(partition_actors ?actors _ _),
hp2:(List.forallb quiescent_actor ?actors = true)  _ =>
apply partition_ns_head_nonquiescent_all in hp1; rewrite hp2 in hp1; inversion hp1
end.
Ltac contradict_conflicting_action_choices :=
match goal with
 hp1:(partition_actors _ ?qqs ?nns), hp2:(partition_actors _ _ _)  _ =>
let Heqqs := fresh in
let Heqa := fresh in
(apply partition_actors_unique with (qs := qqs) (ns := nns) in hp2 as [Heqqs Heqa];
[ inversion Heqqs; inversion Heqa; auto  assumption ])
end.
Ltac contradict_schedule_and_action :=
match goal with
 hp1:(partition_inerts _ _ _), hp2:(partition_actors ?actors _ _)  _ =>
let Hqseq := fresh in
let Hnseq := fresh in
(apply partition_inerts_implies_partition_actors_all_quiescent in hp1;
apply partition_actors_unique with (qs := actors) (ns := []) in hp2 as [Hqseq Hnseq];
[ inversion Hnseq  assumption ])
end.
(* Paper section 4, theorem 4 *)
Theorem arrow_deterministic :
forall Σ Σ', arrow Σ Σ' > forall Σ'', arrow Σ Σ'' > Σ' = Σ''.
Proof.
intros Σ Σ' H'.
induction H'; intros Σ'' H''; dependent induction H'';
try solve [ contradict_dispatch_and_action
 contradict_conflicting_action_choices
 contradict_schedule_and_action ].
(* Dispatch/Dispatch *)
assert (actors' = actors'0); [
apply dispatch_arrow_all_deterministic with (actors := actors) (e := e); assumption  ];
subst; reflexivity.
(* Schedule/Schedule *)
apply partition_inerts_unique with (is := is) (qs := (act rs Σq :: qs)) in H0.
inversion H0. inversion H1. inversion H2.
rewrite < H6 in H''. apply IHH' in H''. rewrite H''. reflexivity. assumption.
Qed.
(**)
Definition spawnA (f : leaf_beh) (u : leaf_st) (acs : list action) : action :=
spawn (spawnLeaf [] acs f u).
Definition bootSigma (acs : list action) : sigma :=
st [] (config (cfg [] [] [act [] (st acs (leaf primordial no_state))])).
Definition spawnVM (ss : list spawnable) : action :=
spawn (spawnConfig ss).
(* Eval simpl in *)
(* match (bootSigma [evt (msg (send (vatom "hi"))); evt (msg (send (vatom "there")))]) with *)
(*  st acs (config C) => until_quiescent 100 (acs, C) *)
(*  st acs s => exhausted ([], cfg [] [] []) *)
(* end. *)