(* Basic Actor Model *)
(*---------------------------------------------------------------------------*)
(* 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.
(* 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 *)
(*---------------------------------------------------------------------------*)
(* General-purpose 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.
(*---------------------------------------------------------------------------*)
(* Basic Actor Model Syntax *)
Inductive leaf_st : Type :=
| no_state : leaf_st
| int_state : nat -> leaf_st.
Inductive val : Type :=
| vbase : leaf_st -> val
| vatom : string -> val
| vpair : val -> val -> val .
Inductive event : Type :=
| send : string -> val -> event .
Inductive 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
with actor : Type :=
| act : string -> sigma -> actor
with sigma : Type :=
| st : list action -> beh -> sigma
with action : Type :=
| evt : event -> action
| spawn : actor -> action .
Inductive config_st : Type :=
| cfg : list event -> list actor -> config_st .
(*---------------------------------------------------------------------------*)
(* 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 [] b) => true
| act _ (st _ _) => false
end.
Definition quiescent_config (C : config_st) : bool :=
match C with
| cfg [] actors => List.forallb quiescent_actor actors
| _ => 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.
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 dispatch_arrow : actor -> event -> actor -> Prop :=
| da_handle :
forall f x v u acs u',
interp0 f (send x v) u = (acs, u') ->
dispatch_arrow (act x (st [] (leaf f u)))
(send x v)
(act x (st acs (leaf f u')))
| da_ignore :
forall x y v Σ,
x <> y ->
dispatch_arrow (act x Σ) (send y v) (act x Σ) .
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 : config_st -> config_st -> Prop :=
| a_dispatch :
forall actors qs e actors' es,
partition_actors actors qs [] ->
dispatch_arrow_all actors e actors' ->
arrow (cfg (e :: es) actors)
(cfg es actors')
| a_send :
forall actors qs x y v acs b ns es,
partition_actors actors qs (act x (st (evt (send y v) :: acs) b) :: ns) ->
arrow (cfg es actors)
(cfg (app es [send y v]) (app qs (act x (st acs b) :: ns)))
| a_spawn :
forall actors qs x y Σ acs b ns actors' es,
partition_actors actors qs (act x (st (spawn (act y Σ) :: acs) b) :: ns) ->
actors' = (app qs (act x (st acs b) :: ns)) ->
arrow (cfg es actors)
(cfg es (app actors' [act y Σ])).
Inductive arrowstar : config_st -> config_st -> Prop :=
| as_zero : forall C, arrowstar C C
| as_succ : forall C C' C'', arrowstar C C' -> arrow C' C'' -> arrowstar C C''.
(*---------------------------------------------------------------------------*)
(* 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_clear H as [Hqs [Hnsn1 Hactorseq]].
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_clear H as [Hqsq [Hnsn1 Hactorseq]].
inversion Hnsn1.
inversion H.
simpl in H. apply H. reflexivity.
Qed.
Lemma quiescent_actors_partition :
forall actors qs,
List.forallb quiescent_actor actors = true /\ qs = actors <-> partition_actors actors qs [].
Proof.
split.
Case "forward".
intros. inversion H. clear H.
apply partition_actors_properties.
split.
SCase "Hqsq".
apply List.forallb_forall. rewrite H1. assumption.
split.
SCase "Hns1n".
left. reflexivity.
SCase "Hactorseq".
rewrite List.app_nil_r. symmetry. assumption.
Case "backward".
intro.
apply partition_actors_properties in H.
inversion_clear H as [Hqsq [Hns1n Hactorseq]].
rewrite List.app_nil_r in Hactorseq.
rewrite Hactorseq.
split.
rewrite List.forallb_forall. assumption.
reflexivity.
Qed.
Lemma some_nonquiescent_actor_implies_config_nonquiescent :
forall actors qs n ns es,
partition_actors actors qs (n :: ns) -> quiescent_config (cfg es actors) = false.
Proof.
intros.
destruct es.
Case "no events".
apply partition_actors_properties in H.
inversion_clear H as [Hqs [Hnsn1 Hactorseq]].
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_clear H as [qs' [n' [ns' Hpartition]]].
exists (a :: qs'). exists n'. exists ns'. apply pa_quiescent; assumption.
SCase "nonquiescent".
exists []. exists a. exists actors.
apply pa_nonquiescent; 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.
SCase "forward".
intro.
inversion H.
reflexivity.
SCase "backward".
intro.
inversion H.
apply pa_nil.
Case "cons".
split.
SCase "forward".
intro.
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".
intro.
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. rewrite H2. rewrite H3. 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.
Lemma steppable_is_nonquiescent :
forall C, (exists C', arrow C C') -> quiescent_config C = false.
Proof.
intros.
inversion_clear H as [C' Hstep].
induction Hstep;
try (apply some_nonquiescent_actor_implies_config_nonquiescent
with (es := es) in H); auto.
Qed.
Lemma dispatch_arrow_functionlike :
forall a e, quiescent_actor a = true -> exists a', dispatch_arrow a e a'.
Proof.
intros.
destruct e as [y v].
destruct a as [x [acs [f u]]].
destruct (string_dec x y).
Case "handle".
rewrite <- e.
remember (interp0 f (send x v) u) as interp_result.
destruct interp_result as [acs' u'].
exists (act x (st acs' (leaf f u'))).
destruct acs.
SCase "no queued actions".
apply da_handle. symmetry. assumption.
SCase "some queued actions".
contradict H. simpl. congruence.
Case "ignore".
exists (act x (st acs (leaf f u))).
apply da_ignore. assumption.
Qed.
Lemma dispatch_arrow_all_functionlike :
forall actors e,
List.forallb quiescent_actor actors = true -> exists actors', dispatch_arrow_all actors e actors'.
Proof.
intros.
induction actors.
exists []. apply daa_nil.
simpl in H. apply andb_true_iff in H. inversion H as [Haq Hactorsq]. clear H.
apply IHactors in Hactorsq. rename Hactorsq into IHactors'.
inversion IHactors' as [actors'].
assert (exists a', dispatch_arrow a e a'). apply dispatch_arrow_functionlike; assumption.
inversion H0 as [a'].
exists (a' :: actors').
apply daa_cons; assumption.
Qed.
Lemma nonquiescent_is_steppable :
forall C, quiescent_config C = false -> (exists C', arrow C C').
Proof.
intros.
destruct C as [es actors].
remember (List.forallb quiescent_actor actors) as actors_q. symmetry in Heqactors_q.
destruct actors_q.
Case "actors quiescent".
destruct es as [| e es'].
SCase "no events".
simpl in H. contradict Heqactors_q. rewrite H. congruence.
SCase "some events".
assert (exists actors', dispatch_arrow_all actors e actors').
apply dispatch_arrow_all_functionlike; assumption.
inversion H0 as [actors'].
exists (cfg es' actors').
apply a_dispatch with (qs := actors).
apply quiescent_actors_partition; auto.
assumption.
Case "some nonquiescent actor".
destruct actors as [| a actors'].
SCase "no actors".
inversion Heqactors_q.
SCase "some actors".
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]].
SSCase "no actions".
apply partition_ns_head_nonquiescent in Hpartition. inversion Hpartition.
SSCase "some actions".
destruct ac as [[y v] | [y Σ]].
SSSCase "send".
exists (cfg (app es [send y v]) (app qs (act x (st acs b) :: ns))).
apply a_send. assumption.
SSSCase "spawn".
exists (cfg es (app (app qs (act x (st acs b) :: ns)) [act y Σ])).
apply a_spawn with (qs := qs) (x := x) (acs := acs) (b := b) (ns := ns).
assumption.
reflexivity.
Qed.
(* Paper section 2, theorem 1 *)
Theorem soundness :
forall C,
((quiescent_config C = false) <-> (exists C', arrow C C')).
Proof.
split.
Case "forward".
intros. apply nonquiescent_is_steppable; assumption.
Case "backward".
intros. apply steppable_is_nonquiescent 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''.
induction H'.
Case "da_handle".
inversion H''.
SCase "da_handle".
rewrite H5 in H; inversion H; reflexivity.
SCase "da_ignore".
contradict H5. reflexivity.
Case "da_ignore".
inversion H''.
SCase "da_handle".
contradict H. assumption.
SCase "da_ignore".
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.
Case "nil".
inversion H'.
inversion H''.
reflexivity.
Case "cons".
simpl in Hactorsq. apply andb_true_iff in Hactorsq.
inversion_clear Hactorsq as [Haq Hactorsq0]. rename Hactorsq0 into Hactorsq.
inversion H'.
inversion H''.
apply dispatch_arrow_deterministic with (a' := a'0) in H1.
rewrite H1.
assert (actors'0 = actors'1).
SCase "assertion".
apply IHactors with (e := e) (actors' := actors'0) (actors'' := actors'1); assumption.
rewrite H11. reflexivity.
assumption.
Qed.
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; subst; auto | assumption ])
end.
(* Paper section 2, theorem 2 *)
Theorem arrow_deterministic :
forall C C', arrow C C' -> forall C'', arrow C C'' -> C' = C''.
Proof.
intros C C' H' C'' H''.
destruct H'; dependent destruction H'';
try solve [ contradict_conflicting_action_choices ].
(* Dispatch/Dispatch *)
apply dispatch_arrow_all_deterministic with (actors' := actors'0) in H0; subst;
[ | apply quiescent_actors_partition in H; inversion H | ]; auto.
Qed.
(*---------------------------------------------------------------------------*)
Definition spawnA (x : string) (f : leaf_beh) (u : leaf_st) (acs : list action) : action :=
spawn (act x (st acs (leaf f u))).
Definition boot (acs : list action) : config_st :=
cfg [] [act "INIT" (st acs (leaf primordial no_state))].
(* Eval simpl in *)
(* let C := (boot [evt (send "a" (vatom "hi")); evt (send "b" (vatom "there"))]) in *)
(* until_quiescent 100 C. *)