From cb6e8938fc2ccdcb762ef1aa5d98a05dcf3c33de Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Tue, 12 Dec 2023 15:17:12 +0200 Subject: [PATCH] Showed that the constrained state property is decidable for ELMO --- theories/Core/Equivocation.v | 6 + theories/Core/ReachableThreshold.v | 5 + theories/Examples/ELMO/ELMO.v | 353 +++++++++++++++++++++++++++++ 3 files changed, 364 insertions(+) diff --git a/theories/Core/Equivocation.v b/theories/Core/Equivocation.v index a0a5c1cc..652553eb 100644 --- a/theories/Core/Equivocation.v +++ b/theories/Core/Equivocation.v @@ -79,6 +79,12 @@ Proof. by apply sum_weights_subseteq. Qed. +#[export] Instance not_heavy_dec + `{BasicEquivocation st validator Cv threshold} + `{!DecidableReachableThreshold validator Cv threshold} : + forall (s : st), Decision (not_heavy s). +Proof. by intros s; apply rt_dec. Qed. + (** *** State-message oracles and endowing states with history Our first step is to define some useful concepts in the context of a single VLSM. diff --git a/theories/Core/ReachableThreshold.v b/theories/Core/ReachableThreshold.v index 10a0a989..bf4f33da 100644 --- a/theories/Core/ReachableThreshold.v +++ b/theories/Core/ReachableThreshold.v @@ -20,6 +20,11 @@ Class ReachableThreshold V Cv (threshold : R) `{Hm : Measurable V} `{FinSet V Cv #[global] Hint Mode ReachableThreshold - - - ! ! ! ! ! ! ! ! ! ! : typeclass_instances. +Class DecidableReachableThreshold V Cv (threshold : R) `{ReachableThreshold V Cv threshold} := + rt_dec :> forall (vs : Cv), Decision (sum_weights vs <= threshold)%R. + +#[global] Hint Mode DecidableReachableThreshold - - - ! ! ! ! ! ! ! ! ! ! ! : typeclass_instances. + Section sec_reachable_threshold_props. Context diff --git a/theories/Examples/ELMO/ELMO.v b/theories/Examples/ELMO/ELMO.v index 2b939703..9765ee70 100644 --- a/theories/Examples/ELMO/ELMO.v +++ b/theories/Examples/ELMO/ELMO.v @@ -74,6 +74,9 @@ Qed. Definition full_node (s : State) (m : Message) : Prop := messages (state m) ⊆+ messages s. +#[export] Instance full_node_dec : RelDecision full_node. +Proof. by intros ? ?; apply submseteq_dec. Qed. + Lemma full_node_reachable_messages_ind (P : State -> Message -> Prop) (Hnew : forall s l msg @@ -229,9 +232,31 @@ Definition local_equivocators_full (s : State) : Address -> Prop := Definition no_self_equiv (s : State) (m : Message) : Prop := adr s = adr (state m) -> m ∈ sentMessages s. +#[export] Instance no_self_equiv_dec : RelDecision no_self_equiv. +Proof. + intros s m. + destruct (decide (m ∈ sentMessages s)) as [| Hnin]; [by left; intro |]. + destruct (decide (adr s = adr (state m))); [| by left; intro]. + by right; contradict Hnin; apply Hnin. +Qed. + Inductive MessageHasSender (m : Message) : Prop := | message_has_sender : forall i, adr (state m) = idx i -> MessageHasSender m. +#[export] Instance MessageHasSender_dec : + forall (m : Message), Decision (MessageHasSender m). +Proof. + intro m. + assert (Decision (Exists (fun i => adr (state m) = idx i) (enum index))) + as [Hex | Hnex] by typeclasses eauto. + - left. + apply Exists_exists in Hex as (i & _ & Hi). + by econstructor. + - right; contradict Hnex; inversion Hnex. + apply Exists_exists; eexists; split; [| done]. + by apply elem_of_enum. +Qed. + Inductive ELMO_msg_valid_full : Message -> Prop := | MVF_nil : forall m : Message, @@ -247,6 +272,33 @@ Inductive ELMO_msg_valid_full : Message -> Prop := ELMO_msg_valid_full m -> ELMO_msg_valid_full (m <*> MkObservation Receive mo). +#[export] Instance ELMO_msg_valid_full_dec : + forall (m : Message), Decision (ELMO_msg_valid_full m). +Proof. + assert (Hwf := well_founded_lt_compat _ (fun m => @sizeMessage Address m) + (fun m1 m2 => sizeMessage m1 < sizeMessage m2) (fun _ _ H => H)). + apply (@well_founded_induction _ (fun m1 m2 => sizeMessage m1 < sizeMessage m2) Hwf). + intros [[[| [[] m'] obs'] adr']] IH. + - destruct (decide (MessageHasSender (MkMessage (MkState [] adr')))) as [| Hnmhs]; + [by left; constructor |]. + by right; contradict Hnmhs; inversion Hnmhs. + - pose (m := (MkMessage (MkState obs' adr'))). + destruct (decide (full_node (state m) m')) as [| Hnf]; + [| by right; contradict Hnf; inversion Hnf; [| destruct m0, state; cbn in *; subst]]. + destruct (decide (no_self_equiv (state m) m')) as [| Hnse]; + [| by right; contradict Hnse; inversion Hnse; [| destruct m0, state; cbn in *; subst]]. + destruct (IH (MkMessage (MkState obs' adr'))) as [| Hnv]; + [..| by right; contradict Hnv; inversion Hnv; [| destruct m0, state; cbn in *; subst]]. + + by cbn; lia. + + by left; apply (MVF_recv m m'). + - destruct (IH (MkMessage (MkState obs' adr'))) as [| Hnv]; + [by cbn; lia |..]. + + destruct (decide (m' = (MkMessage (MkState obs' adr')))) as [-> | Hneq]; + [by left; constructor 2 |]. + by right; contradict Hneq; inversion Hneq; [| destruct m', state]. + + by right; contradict Hnv; inversion Hnv; [done | destruct m', state]. +Qed. + Lemma ELMO_msg_valid_full_to_reach (m : Message) : ELMO_msg_valid_full m -> UMO_reachable (fun s m => full_node s m /\ no_self_equiv s m) (state m). @@ -280,6 +332,22 @@ Record ELMO_recv_valid (s : State) (m : Message) : Prop := local_equivocation_limit_ok (s <+> MkObservation Receive m); }. +#[export] Instance ELMO_recv_valid_dec + `{!DecidableReachableThreshold Address Ca threshold} : + RelDecision ELMO_recv_valid. +Proof. + intros s m. + destruct (decide (full_node s m)) as [| Hno]; + [| by right; contradict Hno; inversion Hno]. + destruct (decide (no_self_equiv s m)) as [| Hno]; + [| by right; contradict Hno; inversion Hno]. + destruct (decide (ELMO_msg_valid_full m)) as [| Hno]; + [| by right; contradict Hno; inversion Hno]. + destruct (decide (not_heavy (s <+> MkObservation Receive m))) as [| Hno]; + [| by right; contradict Hno; inversion Hno]. + by left; constructor. +Qed. + Inductive ELMO_component_valid : Label -> State -> option Message -> Prop := | ELMOCV_Receive : forall (s : State) (m : Message), @@ -289,6 +357,16 @@ Inductive ELMO_component_valid : Label -> State -> option Message -> Prop := forall s : State, ELMO_component_valid Send s None. +#[export] Instance ELMO_component_valid_dec + `{!DecidableReachableThreshold Address Ca threshold} : + forall l : Label, RelDecision (ELMO_component_valid l). +Proof. + intros [] s [m |]; + [| by right; inversion 1 | by right; inversion 1 | by left; constructor]. + by destruct (decide (ELMO_recv_valid s m)) as [| Hno]; + [left; constructor | right; contradict Hno; inversion Hno]. +Qed. + (** This definition is closer to the way the validity condition might be defined by hand, but is probably less convenient than @@ -1426,6 +1504,281 @@ Definition composite_constrained_state_prop (IM : index -> VLSM message) (s : composite_state IM) : Prop := constrained_state_prop (free_composite_vlsm IM) s. +Section sec_ELMO_state_replayable. + +Context + `{!DecidableReachableThreshold Address Ca threshold} + . + +Record elmo_trace := +{ + st_fst : composite_state ELMO_component; + trace : list (composite_transition_item ELMO_component); + st_lst : composite_state ELMO_component; +}. + +Definition constrained_elmo_trace (tr : elmo_trace) : Prop := + finite_constrained_trace_init_to FreeELMO (st_fst tr) (st_lst tr) (trace tr). + +Definition elmo_replay_observation + (tr : elmo_trace) (i : index) (obs : Observation) : option elmo_trace := + let st_lst' := state_update ELMO_component (st_lst tr) i (st_lst tr i <+> obs) in + match obs with + | MkObservation Send (MkMessage s_msg) => + if (decide (s_msg = st_lst tr i)) then + let item := Build_transition_item (T := composite_type ELMO_component) + (existT i Send) None st_lst' (Some (MkMessage s_msg)) + in + Some + {| + st_fst := st_fst tr; + trace := trace tr ++ [item]; + st_lst := st_lst' + |} + else None + | MkObservation Receive msg => + if (decide (ELMO_component_valid Receive (st_lst tr i) (Some msg))) then + let item := Build_transition_item (T := composite_type ELMO_component) + (existT i Receive) (Some msg) st_lst' None + in + Some + {| + st_fst := st_fst tr; + trace := trace tr ++ [item]; + st_lst := st_lst' + |} + else None + end. + +Definition option_elmo_replay_observation + (i : index) (obs : Observation) (otr : option elmo_trace) : option elmo_trace := + otr ≫= fun tr => elmo_replay_observation tr i obs. + +Lemma elmo_replay_observation_constrained + (tr : elmo_trace) (i : index) (obs : Observation) : + forall tr', elmo_replay_observation tr i obs = Some tr' -> + constrained_elmo_trace tr -> + constrained_elmo_trace tr' + /\ + st_lst tr' i = st_lst tr i <+> obs + /\ + forall (j : index), j <> i -> st_lst tr' j = st_lst tr j. +Proof. + intros tr' Htr' [Htr Hinit]. + destruct obs as [[] msg]; cbn in Htr'. + - case_decide; [| done]. + apply Some_inj in Htr' as <-; cbn; repeat split; intros; state_update_simpl; + [| by cbn; apply Hinit.. | done | done]. + eapply finite_valid_trace_from_to_app; [done |]. + apply finite_valid_trace_from_to_singleton. + repeat split; [..| done]. + + by apply valid_trace_last_pstate in Htr. + + by apply any_message_is_valid_in_preloaded. + - destruct msg as [s_msg]. + case_decide; [| done]; subst. + apply Some_inj in Htr' as <-; cbn; repeat split; intros; state_update_simpl; + [| by cbn; apply Hinit.. | done | done]. + eapply finite_valid_trace_from_to_app; [done |]. + apply finite_valid_trace_from_to_singleton. + repeat split; [..| by constructor]. + + by apply valid_trace_last_pstate in Htr. + + by apply any_message_is_valid_in_preloaded. +Qed. + +Definition elmo_replay_observations + (tr : elmo_trace) (i : index) (obss : list Observation) : option elmo_trace := + foldr (option_elmo_replay_observation i) (Some tr) obss. + +Lemma elmo_replay_observations_constrained + (tr : elmo_trace) (i : index) (obss : list Observation) : + forall tr', elmo_replay_observations tr i obss = Some tr' -> + constrained_elmo_trace tr -> + constrained_elmo_trace tr' + /\ + st_lst tr' i = st_lst tr i <++> obss + /\ + forall (j : index), j <> i -> st_lst tr' j = st_lst tr j. +Proof. + revert tr; induction obss using rev_ind; cbn. + - inversion 1. + split; [done |]. + by repeat split; symmetry; apply addObservations_nil. + - intros tr tr'; unfold elmo_replay_observations. + rewrite foldr_snoc; intros Htr' Htr. + destruct option_elmo_replay_observation as [tr1 |] eqn:Htr1. + + apply IHobss in Htr' as (Htr' & Hlst_tr'i & Hlst_tr'j); + [| by eapply elmo_replay_observation_constrained]. + apply elmo_replay_observation_constrained in Htr1 + as (? & Hlst_tr1i & Hlst_tr1j); [| done]. + split_and!; [done |..]. + * rewrite Hlst_tr'i, Hlst_tr1i; destruct (st_lst tr i). + by unfold addObservation, addObservation', addObservations; cbn; simplify_list_eq. + * by intros ? ?; rewrite Hlst_tr'j, Hlst_tr1j. + + exfalso; clear -Htr'. + revert tr' Htr'; induction obss; [done |]. + by cbn; destruct foldr; cbn; [intros; eapply IHobss |]. +Qed. + +Definition elmo_replay_component_state + (tr : elmo_trace) (i : index) (si : State) : option elmo_trace := + elmo_replay_observations tr i (obs si). + +Lemma elmo_replay_component_state_constrained + (tr : elmo_trace) (i : index) (si : State) : + initial_state_prop (ELMO_component i) (st_lst tr i) -> + adr si = idx i -> + forall tr', elmo_replay_component_state tr i si = Some tr' -> + constrained_elmo_trace tr -> + constrained_elmo_trace tr' + /\ + st_lst tr' i = si + /\ + forall (j : index), j <> i -> st_lst tr' j = st_lst tr j. +Proof. + intros Hi His tr' Heqtr' Htr. + eapply elmo_replay_observations_constrained in Htr + as (Htr' & Hlst_tr'i & Hlst_tr'j); [| done]. + destruct Hi as [Hobsi Hadri]. + split_and!; [done | | done]. + rewrite Hlst_tr'i. + destruct (st_lst tr i), si; cbn in *; subst. + unfold addObservations; f_equal; cbn. + by apply app_nil_r. +Qed. + +Lemma elmo_replay_component_state_constrained_rev + (tr : elmo_trace) (i : index) (si : State) : + initial_state_prop (ELMO_component i) (st_lst tr i) -> + constrained_state_prop (ELMO_component i) si -> + exists tr', elmo_replay_component_state tr i si = Some tr' + /\ st_lst tr' i = si + /\ forall j, j <> i -> st_lst tr' j = st_lst tr j. +Proof. +Admitted. + +Definition option_elmo_replay_component_state (s : composite_state ELMO_component) + (i : index) (otr : option elmo_trace) : option elmo_trace := + otr ≫= fun tr => elmo_replay_component_state tr i (s i). + +Definition elmo_initial_trace : elmo_trace := + {| + st_fst := ` (composite_s0 ELMO_component); + trace := []; + st_lst := ` (composite_s0 ELMO_component); + |}. + +Definition elmo_replay_composite_state + (s : composite_state ELMO_component) : option elmo_trace := + foldr (option_elmo_replay_component_state s) (Some elmo_initial_trace) (enum index). + +Lemma elmo_replay_composite_state_constrained (s : composite_state ELMO_component) : + (forall i, adr (s i) = idx i) -> + forall tr', elmo_replay_composite_state s = Some tr' -> + constrained_elmo_trace tr' /\ st_lst tr' = s. +Proof. + unfold elmo_replay_composite_state; intros Hadr tr' Heqtr'. + pose proof (Hnodup := NoDup_enum index). + remember (enum index) as indices. + assert (Hall : Forall (fun i => st_lst elmo_initial_trace i = st_fst elmo_initial_trace i) indices) + by (rewrite Forall_forall; done). + assert (Htr : constrained_elmo_trace elmo_initial_trace). + { + split; [| done]. + by constructor; apply initial_state_is_valid. + } + cut (constrained_elmo_trace tr' + /\ Forall (fun i => st_lst tr' i = s i) indices + /\ forall j, j ∉ indices -> st_lst tr' j = st_lst elmo_initial_trace j). + { + subst; rewrite Forall_forall; intros (? & Halli & _). + split; [done |]. + by extensionality i; apply Halli, elem_of_enum. + } + clear Heqindices; revert Hall tr' Heqtr' Htr. + generalize elmo_initial_trace as tr. + revert Hnodup; induction indices; cbn; intros; + [by inversion Heqtr'; subst; split_and!; [| constructor |] |]. + apply NoDup_cons in Hnodup as [Ha Hnodup]. + apply Forall_cons in Hall as [Heqa Hall]. + rewrite Forall_cons. + destruct foldr as [tr'' |] eqn: Hfold; [| done]. + cbn in Heqtr'. + apply proj2 in Htr as Hinit. + eapply IHindices in Htr as (Htr'' & Halli & Hallj); [| done..]. + eapply elmo_replay_component_state_constrained in Htr'' + as (Htr' & Hlsta & Hlstj ); [..| done]. + - split_and!; [done | done | |]. + + rewrite Forall_forall in Halli |- *. + intros j Hj; rewrite Hlstj by (contradict Ha; subst; done). + by apply Halli. + + intros j; rewrite elem_of_cons; intros Hj. + rewrite Hlstj by (contradict Hj; left; done). + by apply Hallj; contradict Hj; right. + - rewrite Hallj, Heqa by done. + by apply Hinit. + - by apply Hadr. +Qed. + +Lemma elmo_replayed_composite_state_is_constrained + (s : composite_state ELMO_component) : + (forall i : index, adr (s i) = idx i) -> + is_Some (elmo_replay_composite_state s) -> + composite_constrained_state_prop ELMO_component s. +Proof. + intros ? [tr' Heqtr']. + apply elmo_replay_composite_state_constrained in Heqtr' as [Htr' <-]; [| done]. + unfold constrained_elmo_trace, finite_constrained_trace_init_to in Htr'. + by apply valid_trace_last_pstate in Htr'. +Qed. + +Lemma elmo_replayed_composite_state_is_constrained_rev + (s : composite_state ELMO_component) : + composite_constrained_state_prop ELMO_component s -> + is_Some (elmo_replay_composite_state s). +Proof. + intros Hs. + cut (exists tr', elmo_replay_composite_state s = Some tr' + /\ forall j, j ∉ enum index -> st_lst tr' j = st_lst elmo_initial_trace j); + [by intros (? & ? & _); eexists |]. + unfold elmo_replay_composite_state. + pose proof (Hnodup := NoDup_enum index). + assert (Hinit : composite_initial_state_prop ELMO_component (st_fst elmo_initial_trace)) + by done. + assert (Halli : Forall (fun i => st_lst elmo_initial_trace i = st_fst elmo_initial_trace i) (enum index)) + by (apply Forall_forall; done). + revert Hinit Halli; generalize elmo_initial_trace as tr. + revert Hnodup; generalize (enum index) as indices. + induction indices; intros; cbn; [by eexists; split |]. + apply Forall_cons in Halli as [Hlsta Halli]. + apply NoDup_cons in Hnodup as [Ha Hnodup]. + eapply IHindices in Halli as (tr' & -> & Hallj); [| done..]. + destruct (elmo_replay_component_state_constrained_rev tr' a (s a)) + as (tr'' & Heqtr'' & Hlst_tr''a & Htr''allj). + - rewrite Hallj, Hlsta by done. + by apply Hinit. + - by apply constrained_state_prop_component. + - eexists; split; [done |]. + intros j Hj. + rewrite Htr''allj by (contradict Hj; subst; left). + by apply Hallj; contradict Hj; right. +Qed. + +#[export] Instance ELMO_constrained_state_prop_dec : + forall (s : composite_state ELMO_component), + Decision (composite_constrained_state_prop ELMO_component s). +Proof. + intros s. + eapply (Decision_iff + (P := (forall i : index, adr (s i) = idx i) + /\ is_Some (elmo_replay_composite_state s))); + [| by typeclasses eauto]. + split; [by intros []; apply elmo_replayed_composite_state_is_constrained |]. + intros Hs; split; [| by apply elmo_replayed_composite_state_is_constrained_rev]. + by intros i; apply ELMO_reachable_adr, constrained_state_prop_component. +Qed. + +End sec_ELMO_state_replayable. + Lemma ELMO_initial_state_equivocating_validators : forall s : composite_state ELMO_component, composite_initial_state_prop ELMO_component s ->