diff --git a/_CoqProject b/_CoqProject index 064f5e8d..04b5230f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -50,6 +50,7 @@ theories/Core/AnnotatedVLSM.v theories/Core/ByzantineTraces.v theories/Core/TraceableVLSM.v theories/Core/HistoryVLSM.v +theories/Core/Validators/FreeCompositionValidator.v theories/Core/Equivocation/FixedSetEquivocation.v theories/Core/Equivocation/MsgDepFixedSetEquivocation.v diff --git a/theories/Core/MessageDependencies.v b/theories/Core/MessageDependencies.v index 73805092..44bc82c7 100644 --- a/theories/Core/MessageDependencies.v +++ b/theories/Core/MessageDependencies.v @@ -1050,10 +1050,12 @@ Context (IM : index -> VLSM message) `{forall i, HasBeenSentCapability (IM i)} `{forall i, HasBeenReceivedCapability (IM i)} - `{FullMessageDependencies message Cm message_dependencies full_message_dependencies} {validator : Type} (A : validator -> index) (sender : message -> option validator) + `(message_dependencies : message -> Cm) + `(full_message_dependencies : message -> Cm) + `{FullMessageDependencies message Cm message_dependencies full_message_dependencies} . (** diff --git a/theories/Core/Validators/FreeCompositionValidator.v b/theories/Core/Validators/FreeCompositionValidator.v new file mode 100644 index 00000000..72768ae1 --- /dev/null +++ b/theories/Core/Validators/FreeCompositionValidator.v @@ -0,0 +1,283 @@ +From VLSM.Lib Require Import Itauto. +From stdpp Require Import prelude. +From VLSM.Core Require Import VLSM Composition Equivocation MessageDependencies. +From VLSM.Core Require Import VLSMProjections ProjectionTraces. + +(** * Sufficient conditions for being a validator for the free composition + + In this module we give sufficient conditions for a component to be a + validator for the free composition it is part of. + + Namely, we show that if an indexed collection of VLSMs <> satisfies + the [channel_authentication_prop]erty, the [MessageDependencies] and + [FullMessageDependencies] assumptions, the [HasBeenSentCapability] and + [HasBeenReceivedCapability], then any component, which for every valid input + guarantees that the message and all its dependencies are [emittable] by one + of the components, is a validator for the free composition of <> + (lemma [free_valid_message_yields_projection_validator]). + + Specialized (simpler) conditions are provided and proved for components which + additionally satisfy the [message_dependencies_full_node_condition_prop]erty. +*) + +(** ** Message validators are validators for the free composition *) + +Section sec_free_composition_validator. + +Context + `{EqDecision index} + `(IM : index -> VLSM message) + . + +(** + If a component is a message-validator for the free composition, then any + constrained trace of the component lifts to a valid trace of the composition. +*) +Lemma free_component_message_validator_valid_trace : + forall (i : index), + component_message_validator_prop IM (free_constraint IM) i -> + forall is fi tr, + finite_constrained_trace_init_to (IM i) is fi tr -> + finite_valid_trace_init_to (free_composite_vlsm IM) (lift_to_composite_state' IM i is) + (lift_to_composite_state' IM i fi) (lift_to_composite_finite_trace IM i tr). +Proof. + intros i Hvalid isi fi tri Htri. + apply pre_traces_with_valid_inputs_are_valid. + - by apply (VLSM_embedding_finite_valid_trace_init_to + (lift_to_composite_preloaded_VLSM_embedding IM i)). + - rewrite Forall_forall. + intros item Hitem. + apply elem_of_list_fmap in Hitem as (itemi & -> & Hitem); cbn in isi, fi. + apply elem_of_list_split in Hitem as (pre & suf & Heqtri). + destruct Htri as [Htri _]. + apply valid_trace_forget_last in Htri. + eapply (input_valid_transition_to (preloaded_with_all_messages_vlsm (IM i))) + in Heqtri as Ht; [| done]. + destruct itemi, input as [m |]; cbn in *; + [| by apply option_valid_message_None]. + unshelve eapply VLSM_incl_valid_message; + [| by apply free_composite_vlsm_spec | by do 2 red |]. + by eapply Hvalid, input_valid_transition_iff; eexists. +Qed. + +(** + If a component is a message-validator for the free composition, + then it is also a "full" validator for the free composition. +*) +Lemma free_component_message_validator_yields_validator : + forall (i : index), + component_message_validator_prop IM (free_constraint IM) i -> + component_projection_validator_prop IM (free_constraint IM) i. +Proof. + intros i Hvalid li si iom Ht. + unfold input_constrained in Ht. + apply input_valid_transition_iff in Ht as [[si' oom] Ht]. + apply (exists_right_finite_trace_from (preloaded_with_all_messages_vlsm (IM i))) + in Ht as (isi & tri & Htri & Hsi'). + apply free_component_message_validator_valid_trace in Htri as [Htr _]; [| done]. + setoid_rewrite map_app in Htr. + apply finite_valid_trace_from_to_app_split in Htr as [_ Ht]. + apply valid_trace_forget_last, first_transition_valid in Ht as [Hv _]. + eexists; split; cycle 1. + - apply (@VLSM_incl_input_valid _ _ (free_composite_vlsm IM)); [| done]. + by apply free_composite_vlsm_spec. + - cut (si = (lift_to_composite_state' IM i (finite_trace_last isi tri)) i); + [by intros ->; rewrite (lift_to_composite_finite_trace_last IM) |]. + by subst si; state_update_simpl. +Qed. + +End sec_free_composition_validator. + +(** ** Sufficient conditions for being a message validator for the free composition *) + +Section sec_free_composition_message_validator. + +Context + `{EqDecision index} + `(IM : index -> VLSM message) + `(sender : message -> option validator) + (A : validator -> index) + (Hchannel : channel_authentication_prop IM A sender) + `{FinSet message Cm} + (message_dependencies : message -> Cm) + (full_message_dependencies : message -> Cm) + `{!FullMessageDependencies message_dependencies full_message_dependencies} + `{forall i : index, HasBeenSentCapability (IM i)} + `{forall i : index, HasBeenReceivedCapability (IM i)} + `{forall i : index, MessageDependencies (IM i) message_dependencies} + . + +(** Captures the union of constrained messages over all components of <>. *) +Definition emittable (m : message) : Prop := + exists i, can_emit (preloaded_with_all_messages_vlsm (IM i)) m. + +(** + A sufficient condition for determining that a message is valid for the free + composition (see lemma [free_valid_message_is_valid]). +*) +Inductive free_valid_message (m : message) : Prop := +{ + fvm_emittable : emittable m; + fvm_dependencies : set_Forall free_valid_message (message_dependencies m); +}. + +(** + A component satisfies the [free_valid_message_condition] property + if the validity of receiving a message in a (constrained) state implies the + [free_valid_message] property for that message +*) +Definition free_valid_message_condition (i : index) : Prop := + forall l s m, + input_constrained (IM i) l (s, Some m) -> + free_valid_message m. + +(** + Under full-node assumptions, [free_valid_message_condition] can be + simplified to only requiring that the message is [emittable]. +*) +Definition full_node_free_valid_message_condition (i : index) : Prop := + forall l s m, + input_constrained (IM i) l (s, Some m) -> + emittable m. + +Lemma full_node_free_valid_message_entails_helper : + forall (i : index), + message_dependencies_full_node_condition_prop (IM i) message_dependencies -> + full_node_free_valid_message_condition i -> + forall l s m, + input_constrained (IM i) l (s, Some m) -> + (forall dm, has_been_directly_observed (IM i) s dm -> free_valid_message dm) -> + free_valid_message m. +Proof. + intros i Hfulli Hfree l s m Hv Hobs. + constructor; [by eapply Hfree |]. + intros dm Hdm. + eapply Hobs, Hfulli; [| done]. + by apply Hv. +Qed. + +Lemma full_node_free_valid_message_entails : + forall (i : index), + message_dependencies_full_node_condition_prop (IM i) message_dependencies -> + full_node_free_valid_message_condition i -> + free_valid_message_condition i. +Proof. + intros i Hfulli Hfree l s m Hv. + eapply full_node_free_valid_message_entails_helper; [done.. |]. + destruct Hv as [Hs _]. + induction Hs using valid_state_prop_ind; intros dm Hdm; + [by contradict Hdm; apply has_been_directly_observed_no_inits |]. + eapply has_been_directly_observed_step_update in Hdm; [| done]. + destruct Hdm as [[-> | ->]|]; [.. | by apply IHHs]. + - by destruct Ht; eapply full_node_free_valid_message_entails_helper. + - assert (Hdm : can_produce (preloaded_with_all_messages_vlsm (IM i)) s' dm) + by (eexists _,_; done). + apply message_dependencies_are_necessary in Hdm as Hdeps. + constructor; [by eexists; apply can_emit_iff; eexists |]. + intros dm' Hdm'. + assert (dm' <> dm). + { + intros ->. + eapply (irreflexivity (msg_dep_happens_before message_dependencies) dm). + by constructor. + } + eapply Hdeps, has_been_directly_observed_step_update in Hdm'; [| done]. + destruct Hdm' as [[-> | Hdm'] |]; [.. | by congruence | by apply IHHs]. + by destruct Ht; eapply full_node_free_valid_message_entails_helper. +Qed. + +Lemma free_valid_message_emittable_from_dependencies : + forall (m : message), + free_valid_message m -> + Emittable_from_dependencies_prop IM A sender message_dependencies m. +Proof. + intros m [[i Hemit] _]. + apply Hchannel in Hemit as Hauth. + unfold channel_authenticated_message in Hauth. + destruct (sender m) eqn: Hsender; [| done]. + apply Some_inj in Hauth as <-. + constructor 1 with v; [done |]. + by apply message_dependencies_are_sufficient. +Qed. + +Lemma msg_dep_reflects_free_valid_message : + forall (dm m : message), + msg_dep_rel message_dependencies dm m -> + free_valid_message m -> free_valid_message dm. +Proof. + intros dm m Hdep [_ Hall]. + by apply Hall. +Qed. + +Lemma free_valid_message_is_valid : + forall m : message, + free_valid_message m -> + valid_message_prop (free_composite_vlsm IM) m. +Proof. + intros m Hm. + eapply free_valid_from_all_dependencies_emitable_from_dependencies; [done |]. + unfold all_dependencies_emittable_from_dependencies_prop. + intros dm; rewrite elem_of_cons. + intros [-> | Hdm]; [by apply free_valid_message_emittable_from_dependencies |]. + apply free_valid_message_emittable_from_dependencies. + apply elem_of_elements, full_message_dependencies_happens_before in Hdm. + eapply msg_dep_happens_before_reflect; [| done..]. + by apply msg_dep_reflects_free_valid_message. +Qed. + +Section sec_free_valid_message_validators. + +(** + If the validity predicate of a component implies that its input message + satisfies [free_valid_message], then the component is a message validator, + and therefore, a validator for the free composition. +*) + +Context + (i : index) + (Hfree_valid_message_inputs : free_valid_message_condition i) + . + +Lemma free_valid_message_yields_message_validator : + component_message_validator_prop IM (free_constraint IM) i. +Proof. + intros li si im Him. + unshelve eapply VLSM_incl_valid_message; + [| by apply free_composite_vlsm_spec | by do 2 red |]. + by eapply free_valid_message_is_valid, Hfree_valid_message_inputs, Him. +Qed. + +Lemma free_valid_message_yields_projection_validator : + component_projection_validator_prop IM (free_constraint IM) i. +Proof. + by apply free_component_message_validator_yields_validator, + free_valid_message_yields_message_validator. +Qed. + +End sec_free_valid_message_validators. + +Section sec_full_node_free_valid_message_validators. + +Context + (i : index) + (Hfulli : message_dependencies_full_node_condition_prop (IM i) message_dependencies) + (Hfree : full_node_free_valid_message_condition i) + . + +Lemma full_node_free_valid_message_yields_message_validator : + component_message_validator_prop IM (free_constraint IM) i. +Proof. + by apply free_valid_message_yields_message_validator, + full_node_free_valid_message_entails. +Qed. + +Lemma full_node_free_valid_message_yields_projection_validator : + component_projection_validator_prop IM (free_constraint IM) i. +Proof. + by apply free_valid_message_yields_projection_validator, + full_node_free_valid_message_entails. +Qed. + +End sec_full_node_free_valid_message_validators. + +End sec_free_composition_message_validator. diff --git a/theories/Examples/ELMO/MO.v b/theories/Examples/ELMO/MO.v index 474cf53a..8feaadfa 100644 --- a/theories/Examples/ELMO/MO.v +++ b/theories/Examples/ELMO/MO.v @@ -4,6 +4,7 @@ From stdpp Require Import prelude finite. From VLSM.Lib Require Import Preamble ListExtras StdppExtras. From VLSM.Core Require Import VLSM PreloadedVLSM VLSMProjections Composition. From VLSM.Core Require Import Equivocation Validator ProjectionTraces. +From VLSM.Core Require Import MessageDependencies FreeCompositionValidator. From VLSM.Examples Require Import BaseELMO UMO. (** * ELMO: Protocol Definitions and Properties for MO @@ -41,6 +42,25 @@ Inductive MO_msg_valid (P : Address -> Prop) : Message -> Prop := forall m mr : Message, MO_msg_valid P m -> MO_msg_valid P mr -> MO_msg_valid P (m <*> MkObservation Receive mr). +Lemma MO_msg_valid_P_adr (P : Address -> Prop) (m : Message) : + MO_msg_valid P m -> P (adr (state m)). +Proof. + by induction 1. +Qed. + +Lemma MO_msg_valid_dep (P : Address -> Prop) (m : Message) : + MO_msg_valid P m -> + forall dm, dm ∈ Message_dependencies m -> MO_msg_valid P dm. +Proof. + unfold Message_dependencies. + intros Hv dm Hdm. + apply elem_of_list_to_set, elem_of_list_fmap in Hdm as (o & -> & Ho). + revert o Ho; induction Hv; cbn; intros. + - by destruct m, state; cbn in *; subst; inversion Ho. + - by apply elem_of_addObservation in Ho as [-> |]; [| apply IHHv]. + - by apply elem_of_addObservation in Ho as [-> |]; [| apply IHHv1]. +Qed. + Section sec_alternative_definition_of_validity. (** ** Alternative definition of validity @@ -843,357 +863,122 @@ Context Definition MO : VLSM Message := free_composite_vlsm M. -(** We set up aliases for some functions operating on free VLSM composition. *) - -Definition MO_state : Type := composite_state M. -Definition MO_label : Type := composite_label M. -Definition MO_transition_item : Type := composite_transition_item M. - -(** We can lift labels, states and traces from an MO component to the MO protocol. *) - -Definition lift_to_MO_label - (i : index) (li : VLSM.label (M i)) : MO_label := - lift_to_composite_label M i li. - -Definition lift_to_MO_state - (us : MO_state) (i : index) (si : VLSM.state (M i)) : MO_state := - lift_to_composite_state M us i si. - -Definition lift_to_MO_trace - (us : MO_state) (i : index) (tr : list (transition_item (M i))) - : list MO_transition_item := - pre_VLSM_embedding_finite_trace_project - _ _ (lift_to_MO_label i) (lift_to_MO_state us i) tr. - -#[local] Hint Rewrite @state_update_twice : state_update. - -#[local] Hint Unfold lift_to_MO_label : state_update. -#[local] Hint Unfold lift_to_MO_state : state_update. -#[local] Hint Unfold lift_to_MO_trace : state_update. - -(** - We can also lift properties from MO components to the MO protocol, among - them [valid_state_prop], [valid_message_prop], [input_valid_transition] - and the various kinds of traces. -*) - -Lemma lift_to_MO : - forall (us : MO_state) (Hus : valid_state_prop MO us) (i : index), - VLSM_weak_embedding (M i) MO (lift_to_MO_label i) (lift_to_MO_state us i). -Proof. by intros; apply lift_to_free_weak_embedding. Qed. - -Lemma lift_to_MO_valid_state_prop : - forall (i : index) (s : State) (us : MO_state), - valid_state_prop MO us -> valid_state_prop (M i) s -> - valid_state_prop MO (lift_to_MO_state us i s). -Proof. - intros is s us Hvsp. - by eapply VLSM_weak_embedding_valid_state, lift_to_MO. -Qed. - -Lemma lift_to_MO_valid_message_prop : - forall (i : index) (om : option Message), - option_valid_message_prop (M i) om -> - option_valid_message_prop MO om. -Proof. - intros i [] Hovmp; cycle 1. - - by exists (``(vs0 MO)); constructor. - - eapply VLSM_weak_embedding_valid_message. - + by apply (lift_to_MO (``(vs0 MO))); exists None; constructor. - + by inversion 1. - + by apply Hovmp. -Qed. - -Lemma lift_to_MO_input_valid_transition : - forall (i : index) (lbl : Label) (s1 s2 : State) (iom oom : option Message) (us : MO_state), - valid_state_prop MO us -> - input_valid_transition (M i) lbl (s1, iom) (s2, oom) -> - input_valid_transition MO - (lift_to_MO_label i lbl) - (lift_to_MO_state us i s1, iom) - (lift_to_MO_state us i s2, oom). -Proof. - intros i lbl s1 s2 iom oom us Hivt. - by apply @VLSM_weak_embedding_input_valid_transition, lift_to_MO. -Qed. - -Lemma lift_to_MO_finite_valid_trace_from_to : - forall (i : index) (s1 s2 : State) (tr : list (transition_item (M i))) (us : MO_state), - valid_state_prop MO us -> - finite_valid_trace_from_to (M i) s1 s2 tr -> - finite_valid_trace_from_to - MO (lift_to_MO_state us i s1) (lift_to_MO_state us i s2) (lift_to_MO_trace us i tr). -Proof. - intros i s1 s2 tr us Hvsp Hfvt. - by eapply (VLSM_weak_embedding_finite_valid_trace_from_to (lift_to_MO _ Hvsp i)). -Qed. - -Lemma lift_to_MO_constrained_state_prop : - forall (i : index) (s : State) (us : MO_state), - constrained_state_prop MO us -> constrained_state_prop (M i) s -> - constrained_state_prop MO (lift_to_MO_state us i s). -Proof. - intros is s us Hvsp. - by eapply VLSM_weak_embedding_valid_state, lift_to_preloaded_free_weak_embedding. -Qed. - -Lemma lift_to_preloaded_MO_option_valid_message_prop : - forall (i : index) (om : option Message), - option_valid_message_prop (preloaded_with_all_messages_vlsm (M i)) om -> - option_valid_message_prop (preloaded_with_all_messages_vlsm MO) om. -Proof. - intros i [] Hovmp; cycle 1. - - by exists (``(vs0 MO)); constructor. - - eapply VLSM_weak_embedding_valid_message. - + eapply (lift_to_preloaded_free_weak_embedding _ i (``(vs0 MO))). - by exists None; constructor. - + by inversion 1; cbn; [| right]. - + by apply Hovmp. -Qed. - -Lemma lift_to_MO_input_constrained_transition : - forall (i : index) (lbl : Label) (s1 s2 : State) (iom oom : option Message) (us : MO_state), - constrained_state_prop MO us -> - input_constrained_transition (M i) lbl (s1, iom) (s2, oom) -> - input_constrained_transition MO - (lift_to_MO_label i lbl) - (lift_to_MO_state us i s1, iom) - (lift_to_MO_state us i s2, oom). -Proof. - intros i lbl s1 s2 iom oom us Hivt. - by apply @VLSM_weak_embedding_input_valid_transition, lift_to_preloaded_free_weak_embedding. -Qed. - -Lemma lift_to_MO_finite_constrained_trace_from_to : - forall (i : index) (s1 s2 : State) (tr : list (transition_item (M i))) (us : MO_state), - constrained_state_prop MO us -> - finite_constrained_trace_from_to (M i) s1 s2 tr -> - finite_constrained_trace_from_to MO - (lift_to_MO_state us i s1) (lift_to_MO_state us i s2) (lift_to_MO_trace us i tr). -Proof. - intros i s1 s2 tr us Hvsp Hfvt. - unshelve eapply (@VLSM_weak_embedding_finite_valid_trace_from_to _ - (preloaded_with_all_messages_vlsm (M i)) - (preloaded_with_all_messages_vlsm MO) _ _); [| done]. - by apply lift_to_preloaded_free_weak_embedding. -Qed. - -(** *** Lifting lemmas for validating theorem *) - -Lemma initial_state_prop_lift_to_MO : - forall (i : index) (s : State), - initial_state_prop (M i) s -> - initial_state_prop MO (lift_to_MO_state (``(vs0 MO)) i s). -Proof. - intros i s Hisp j; cbn. - by destruct (decide (i = j)); subst; state_update_simpl. -Qed. - -Lemma finite_valid_trace_init_to_lift_to_MO : - forall (i : index) (s : State), - initial_state_prop (M i) s -> - finite_valid_trace_init_to MO - (lift_to_MO_state (``(vs0 MO)) i s) (lift_to_MO_state (``(vs0 MO)) i s) []. -Proof. - constructor; cycle 1. - - by apply initial_state_prop_lift_to_MO. - - constructor; exists None; constructor; [| done]. - by apply initial_state_prop_lift_to_MO. -Qed. - -Lemma option_valid_message_prop_initial : - forall i : index, - option_valid_message_prop MO (Some (MkMessage (MkState [] (idx i)))). -Proof. - intros i. - remember (MkMessage (MkState [] (idx i))) as m. - exists (state_update M (``(vs0 MO)) i (state m <+> MkObservation Send m)). - by econstructor 2 with - (s := ``(vs0 MO)) (_om := None) (_s := ``(vs0 MO)) (om := None) (l := existT i Send); - [by repeat split; constructor.. | rewrite Heqm]. -Qed. - -Lemma option_valid_message_prop_addObservationToMessage_Send : - forall m : Message, - option_valid_message_prop MO (Some m) -> - option_valid_message_prop MO (Some (m <*> MkObservation Send m)). -Proof. - intros m [s' IH]. - inversion IH; subst; [by inversion Hom as [j []]; inversion x |]. - destruct l as [k []], om as [m' |]; - inversion Hv; subst; clear Hv; - inversion Ht; subst; clear Ht. - unfold addObservationToMessage; cbn; red. - remember (s k <+> MkObservation Send (MkMessage (s k))) as sk'. - remember (state_update M s k sk') as ss. - assert (Heq : ss k = sk') by (subst; state_update_simpl; done). - rewrite <- Heq in *; clear Heqsk'. - exists (state_update M ss k (ss k <+> MkObservation Send (MkMessage (ss k)))). - by econstructor 2 with (s := ss) (_s := ``(vs0 MO)) (om := None) (l := existT k Send); - [| constructor | repeat split; constructor |]. -Qed. - -Lemma option_valid_message_prop_addObservationToMessage_Receive : - forall m mr : Message, - MO_msg_valid P' mr -> - option_valid_message_prop MO (Some m) -> - option_valid_message_prop MO (Some mr) -> - option_valid_message_prop MO (Some (m <*> MkObservation Receive mr)). -Proof. - intros m mr Hvalid [sm IH1] [smr IH2]. - inversion IH1; subst; [by inversion Hom as [j []]; inversion x |]. - destruct l as [k []], om as [m' |]; - inversion Hv; subst; clear Hv; - inversion Ht; subst; clear Ht. - exists (state_update M s k (s k <+> MkObservation Receive mr <+> - MkObservation Send (MkMessage (s k <+> MkObservation Receive mr)))). - econstructor 2 with - (s := state_update M s k (s k <+> MkObservation Receive mr)) (_om := None) - (_s := ``(vs0 MO)) (om := None) (l := existT k Send); cycle 1. - - by constructor. - - by repeat split; constructor. - - by cbn; state_update_simpl. - - by econstructor 2 with (s := s) (om := Some mr) (l := existT k Receive); - [| | repeat split; constructor |]. -Qed. - -Lemma option_valid_message_prop_MO_msg_valid : - forall m : Message, - MO_msg_valid P' m -> option_valid_message_prop MO (Some m). -Proof. - induction 1. - - destruct H1 as (_ & i & Heq). - replace m with (MkMessage (MkState [] (idx i))) by (apply eq_Message; done). - by apply option_valid_message_prop_initial. - - by apply option_valid_message_prop_addObservationToMessage_Send. - - by apply option_valid_message_prop_addObservationToMessage_Receive. -Qed. +(** *** Validators *) -Lemma lift_to_MO_finite_valid_trace_init_to : - forall (i : index) (s1 s2 : State) (tr : list (transition_item (M i))), - finite_constrained_trace_init_to (M i) s1 s2 tr -> - finite_valid_trace_init_to MO (lift_to_MO_state (``(vs0 MO)) i s1) - (lift_to_MO_state (``(vs0 MO)) i s2) (lift_to_MO_trace (``(vs0 MO)) i tr). -Proof. - intros i s1 s2 tr [Hfvt Hisp]. - induction Hfvt using finite_valid_trace_from_to_rev_ind; cbn; - [by apply finite_valid_trace_init_to_lift_to_MO |]. - constructor; [| by apply initial_state_prop_lift_to_MO]. - unfold lift_to_MO_trace, pre_VLSM_embedding_finite_trace_project. - rewrite map_app. - eapply finite_valid_trace_from_to_app; cbn; [by apply IHHfvt |]. - apply valid_trace_add_last; [| done]. - apply first_transition_valid; cbn. - destruct Ht as [(Hvsp & _ & Hvalid) Ht], l, iom as [im |]; cbn in *; - inversion Hvalid; subst; clear Hvalid; - inversion Ht; subst; cbn in *; clear Ht; cycle 1. - - repeat split. - + by eapply finite_valid_trace_from_to_last_pstate, IHHfvt. - + by apply option_valid_message_None. - + by constructor. - + by cbn; state_update_simpl. - - repeat split. - + by eapply finite_valid_trace_from_to_last_pstate, IHHfvt. - + by apply option_valid_message_prop_MO_msg_valid. +Lemma MO_reachable_view (s : State) i : + constrained_state_prop (M i) s + <-> + UMO_reachable (const (MO_msg_valid P')) s /\ adr s = idx i. +Proof. + eapply iff_trans. + - apply UMO_based_valid_reachable; cbn; [by inversion 1 | | done]. + by cbn; split; inversion 1; [| constructor]. + - apply Morphisms_Prop.and_iff_morphism; cbn; [| by firstorder]. + by split; apply UMO_reachable_impl; inversion 1; subst; [| constructor..]. +Qed. + +Lemma MO_reachable_adr (s : State) i : + constrained_state_prop (M i) s -> adr s = idx i. +Proof. + by intros Hadr; apply MO_reachable_view in Hadr as []. +Qed. + +Lemma MO_channel_authentication_prop : + channel_authentication_prop M (Message_sender_index idx) (Message_sender idx). +Proof. + intros i m ((s & []) & [] & s' & [(Hs & _ & Hv) Ht]); + inversion Hv; subst; inversion Ht; subst. + unfold channel_authenticated_message, Message_sender. + erewrite MO_reachable_adr by done. + case_decide as Hadr; cbn. + - by f_equal; apply Message_sender_index_inv. + - by contradict Hadr; rewrite adr2idx_idx. +Qed. + +Lemma cannot_resend_message_stepwise_MO_component i : + cannot_resend_message_stepwise_prop (M i). +Proof. + intros ? * [(Hs & _ & Hv) Ht]; + inversion Hv; subst; inversion Ht; subst; + simpl; split; intros Hobs. + - by apply elem_of_sentMessages, obs_sizeState in Hobs; cbn in Hobs; lia. + - rewrite receivedMessages_addObservation, decide_False in Hobs by (intro; done). + by apply elem_of_receivedMessages, obs_sizeState in Hobs; cbn in Hobs; lia. +Qed. + +#[export] Instance MessageDependencies_MO_component i : + MessageDependencies (M i) Message_dependencies. +Proof. + constructor. + - intros m s' ((s, iom) & l & [(_ & _ & Hv) Ht]) dm Hdm; cbn in *. + apply elem_of_list_to_set, elem_of_list_fmap in Hdm as (o & -> & Hy). + inversion Hv; subst; inversion Ht; subst; cbn in *; clear Ht. + red; unfold Message; simpl. + destruct o as [[] ?]. + + right; apply elem_of_receivedMessages_addObservation. + by right; apply elem_of_receivedMessages. + + left; apply elem_of_sentMessages_addObservation. + by right; apply elem_of_sentMessages. + - intros m Hm. + apply can_emit_has_trace in Hm as (is & tr & item & Htr & Houtput). + apply (can_emit_from_valid_trace + (preloaded_vlsm (M i) (fun msg : Message => msg ∈ Message_dependencies m))) + with is (tr ++ [item]); cycle 1. + + apply Exists_exists; eexists. + by split; [apply elem_of_app; right; left |]. + + eapply lift_preloaded_trace_to_seeded; + [by apply cannot_resend_message_stepwise_MO_component | | done]. + intros dm [Hrcv Hnsnd]. + apply elem_of_list_to_set, elem_of_list_fmap. + exists (MkObservation Receive dm); split; [done |]. + apply elem_of_receivedMessages. + destruct Htr as [Htr His]. + apply finite_valid_trace_from_app_iff in Htr as [Htr Hitem]. + apply valid_trace_add_default_last in Htr. + apply first_transition_valid in Hitem as [(_ & _ & Hv) Ht]. + destruct item, l, input; cbn in *; inversion Hv; subst; inversion Ht; subst. + clear Hv Ht Hnsnd; cbn. + assert (Hrcv' : trace_has_message (field_selector input) dm tr). + { + apply Exists_exists in Hrcv as (dm_item & Hdm_item & Hdm). + rewrite elem_of_app, elem_of_list_singleton in Hdm_item. + destruct Hdm_item as [Hdm_item | ->]; cbn in Hdm; [| done]. + by apply Exists_exists; eexists. + } + by eapply @has_been_received_examine_one_trace with (vlsm := M i) in Hrcv'; cycle 1. +Qed. + +Lemma MO_msg_valid_free : + forall (m : Message), + MO_msg_valid P' m -> + free_valid_message M Message_dependencies m. +Proof. + induction m as (m & Hind) using (well_founded_ind + (msg_dep_happens_before_wf Message_dependencies Message_full_dependencies _)). + intros Hm; constructor. + - remember (adr (state m)) as a; symmetry in Heqa. + eapply constrained_state_prop_MO_msg_valid in Heqa as Hstate_m; [| done]. + apply MO_msg_valid_P_adr in Hm as (_ & i & Hi). + rewrite <- Heqa, <- Hi in Hstate_m. + red; unfold can_emit; cbn. + exists i, (state m, None), Send, (state m <+> MkObservation Send m). + repeat split; [done | ..]. + + by apply any_message_is_valid_in_preloaded. + by constructor. - + by cbn; state_update_simpl. + + by destruct m as [[]]. + - by intros dm Hdm; apply Hind; [constructor | eapply MO_msg_valid_dep]. Qed. -Lemma lift_preloaded_component_to_MO : - forall i : index, - VLSM_embedding (preloaded_with_all_messages_vlsm (M i)) MO - (lift_to_MO_label i) (lift_to_MO_state (``(vs0 MO)) i). -Proof. - constructor; intros. - by eapply valid_trace_forget_last, lift_to_MO_finite_valid_trace_init_to, - finite_valid_trace_init_add_last. -Qed. - -(** - Every state in a MO component gives rise to a unique trace leading to this - state, which we can then lift to the MO protocol. -*) -Definition MO_component_state2trace - (s : MO_state) (i : index) : list MO_transition_item := - lift_to_MO_trace s i (state2trace (s i)). - -(** - Iterating [MO_component_state2trace] shows that every reachable MO state contains a - trace that leads to this state. However, this trace is not unique, because - we can concatenate the lifted traces in any order. -*) -Fixpoint MO_state2trace_aux - (us : MO_state) (is : list index) : list MO_transition_item := - match is with - | [] => [] - | i :: is' => - MO_state2trace_aux (state_update _ us i (MkState [] (idx i))) is' ++ MO_component_state2trace us i - end. - -Definition MO_state2trace - (us : MO_state) : list MO_transition_item := - MO_state2trace_aux us (enum index). - -Lemma finite_constrained_trace_init_to_MO_state2trace : - forall us : MO_state, - constrained_state_prop MO us -> - finite_constrained_trace_init_to MO (``(vs0 MO)) us (MO_state2trace us). -Proof. - intros us Hvsp; split; [| done]. - unfold MO_state2trace. - assert (Hall : forall i, i ∉ enum index -> us i = MkState [] (idx i)) - by (intros i Hin; contradict Hin; apply elem_of_enum). - revert us Hall Hvsp. - generalize (enum index) as is. - induction is as [| i is']; cbn; intros us Hall Hvsp. - - replace us with (fun n : index => MkState [] (idx n)). - + by constructor; apply initial_state_is_valid; compute. - + extensionality i; rewrite Hall; [done |]. - by apply not_elem_of_nil. - - eapply finite_valid_trace_from_to_app. - + apply IHis'. - * intros j Hj. destruct (decide (i = j)); subst; state_update_simpl; [done |]. - by apply Hall; rewrite elem_of_cons; intros []. - * by apply pre_composite_free_update_state_with_initial. - + replace us with (state_update M us i (us i)) at 2 by (state_update_simpl; done). - apply lift_to_MO_finite_constrained_trace_from_to; [done |]. - apply (composite_constrained_state_project _ us i) in Hvsp as Hvsp'. - apply valid_state_has_trace in Hvsp' as (s & tr & [Hfvt Hinit]). - replace s with (MkState [] (idx i)) in *; cycle 1. - * by inversion Hinit; destruct s; cbn in *; subst. - * by eapply finite_constrained_trace_init_to_state2trace. -Qed. - -(** *** Validators *) - Lemma MO_component_validating : - forall i : index, component_projection_validator_prop M (free_constraint M) i. + forall (i : index), + component_projection_validator_prop M (free_constraint M) i. Proof. - unfold component_projection_validator_prop. - intros i lj sj omi * Hiv. - red in Hiv; apply input_valid_transition_iff in Hiv as [[s m] Ht]. - destruct (exists_right_finite_trace_from _ _ _ _ _ _ Ht) as (s' & tr & Hfvt & Hlast). - apply lift_to_MO_finite_valid_trace_init_to in Hfvt as [Hfvt _]. - unfold lift_to_MO_trace, pre_VLSM_embedding_finite_trace_project in Hfvt; - rewrite map_app in Hfvt. - apply finite_valid_trace_from_to_app_split in Hfvt as [_ Hfvt]. - remember (finite_trace_last _ _) as ftl. - change (finite_trace_last _ _) - with (finite_trace_last - (lift_to_MO_state (fun j : index => MkState [] (idx j)) i s') - (lift_to_MO_trace (fun j : index => MkState [] (idx j)) i tr)) in Heqftl. - apply valid_trace_forget_last, first_transition_valid in Hfvt; cbn in *. - destruct Hfvt as [[Hvps [Hovmp Hv]] Ht']; cbn in Hv. - unfold lift_to_MO_trace in Heqftl; cbn in Heqftl. - rewrite <- pre_VLSM_embedding_finite_trace_last, Hlast in Heqftl. - exists ftl; split; [by rewrite Heqftl; state_update_simpl |]. - split_and!; [| | done..]. - - eapply VLSM_incl_valid_state; [| by apply Hvps]. - by apply free_composite_vlsm_spec. - - destruct Hovmp as [ss Hvsmp]. - exists ss. - apply VLSM_incl_valid_state_message; [| by do 2 red | done]. - by apply free_composite_vlsm_spec. + intros i. + eapply free_valid_message_yields_projection_validator; + [by apply MO_channel_authentication_prop | by typeclasses eauto |]. + intros li si m (_ & _ & Hv). + inversion Hv as [? ? Hm |]; subst; clear i si Hv. + by apply MO_msg_valid_free. Qed. (** *** Equivocation *)