diff --git a/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v index 2db369f2..71cda519 100644 --- a/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v +++ b/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v @@ -2,8 +2,8 @@ From Cdcl Require Import Itauto. Local Tactic Notation "itauto" := itauto auto. From stdpp Require Import prelude finite. From Coq Require Import FunctionalExtensionality. From VLSM.Lib Require Import Preamble StdppListSet FinFunExtras ListExtras. -From VLSM Require Import Core.VLSM Core.MessageDependencies Core.VLSMProjections Core.Composition Core.ProjectionTraces Core.SubProjectionTraces Core.ByzantineTraces. -From VLSM Require Import Core.Validator Core.Equivocation Core.EquivocationProjections Core.Equivocation.NoEquivocation Core.Equivocation.FixedSetEquivocation. +From VLSM.Core Require Import VLSM MessageDependencies VLSMProjections Composition ProjectionTraces SubProjectionTraces ByzantineTraces Validator Equivocation EquivocationProjections. +From VLSM.Core.Equivocation Require Import NoEquivocation FixedSetEquivocation MsgDepFixedSetEquivocation. (** * VLSM Compositions with a fixed set of byzantine nodes @@ -23,48 +23,7 @@ nodes and equivocating ones. Therefore, when analyzing the security of a protocol it suffices to consider equivocating nodes. *) -Section emit_any_signed_message_vlsm. - -(** ** A machine which can emit any valid message for a given node - -This VLSM is similar to the [emit_any_message_vlsm] with the exception of the -validity predicate which requires that the sender of the emitted message -corresponds to the given node. -*) - -Context - {message : Type} - {index : Type} - {validator : Type} - (A : validator -> index) - (sender : message -> option validator) - (node_idx : index) - . - -(** The [valid]ity predicate allows sending only signed messages -*) -Definition signed_messages_valid - (l : @label message all_messages_type) - (som : @state message all_messages_type * option message) - : Prop := - channel_authenticated_message A sender node_idx l. - -Definition emit_any_signed_message_vlsm_machine - : VLSMMachine all_messages_type - := - {| initial_state_prop := fun s => True - ; initial_message_prop := fun m => False - ; s0 := all_messages_state_inh - ; transition := all_messages_transition - ; valid := signed_messages_valid - |}. - -Definition emit_any_signed_message_vlsm - := mk_vlsm emit_any_signed_message_vlsm_machine. - -End emit_any_signed_message_vlsm. - -Section fixed_byzantine_traces. +Section sec_fixed_byzantine_traces. Context {message : Type} @@ -79,6 +38,15 @@ Context (can_emit_signed : channel_authentication_prop IM A sender) (Hsender_safety : sender_safety_alt_prop IM A sender := channel_authentication_sender_safety IM A sender can_emit_signed) + (non_byzantine : set index := set_diff (enum index) byzantine) + . + +Section sec_fixed_byzantine_replacements. + +Context + (byzantine_replacements_IM : sub_index byzantine -> VLSM message) + (no_initial_messages_in_byzantine_IM : no_initial_messages_in_IM_prop byzantine_replacements_IM) + (can_emit_signed_byzantine : channel_authentication_prop byzantine_replacements_IM (sub_IM_A byzantine A) (sub_IM_sender byzantine A sender)) . (** Given a collection of nodes indexed by an <>, we define the @@ -86,27 +54,31 @@ associated fixed byzantine collection of nodes by replacing the nodes corresponding to the indices in a given <> with byzantine nodes, i.e., nodes which can emit any (signed) message. *) -Definition fixed_byzantine_IM : index -> VLSM message := - update_IM IM byzantine (fun i => emit_any_signed_message_vlsm A sender (` i)). +Definition fixed_byzantine_IM + : index -> VLSM message := + update_IM IM byzantine byzantine_replacements_IM. Lemma fixed_byzantine_IM_no_initial_messages : forall i m, ~vinitial_message_prop (fixed_byzantine_IM i) m. Proof. unfold fixed_byzantine_IM, update_IM. simpl. intros i m Hm. - by case_decide; [|destruct (no_initial_messages_in_IM i m)]. + case_decide. + - by eapply no_initial_messages_in_byzantine_IM. + - by eapply no_initial_messages_in_IM. Qed. Lemma fixed_byzantine_IM_preserves_channel_authentication : channel_authentication_prop fixed_byzantine_IM A sender. Proof. unfold fixed_byzantine_IM, update_IM. simpl. - intros i m Hm. + intros i m. case_decide. - - destruct Hm as [(s0, om) [l [s1 [[_ [_ Hv]] Ht]]]]. - cbn in Hv, Ht. - unfold signed_messages_valid, channel_authenticated_message in Hv. - by inversion Ht; subst. + - intro Hm; apply can_emit_signed_byzantine in Hm. + unfold channel_authenticated_message, sub_IM_A, sub_IM_sender in Hm |- *. + destruct (sender m) as [v|]; [|inversion Hm]. + case_decide; [|inversion Hm]; cbn; f_equal. + by apply Some_inj, dec_sig_eq_iff in Hm. - by apply can_emit_signed. Qed. @@ -115,47 +87,116 @@ Definition fixed_byzantine_IM_sender_safety channel_authentication_sender_safety fixed_byzantine_IM A sender fixed_byzantine_IM_preserves_channel_authentication. -Definition message_as_byzantine_label - (m : message) - (i : index) - (Hi : i ∈ byzantine) - : composite_label fixed_byzantine_IM. -Proof. - exists i. - unfold fixed_byzantine_IM, update_IM. - simpl. - by rewrite decide_True. -Defined. - -Context - (non_byzantine : set index := set_diff (enum index) byzantine) - . - (** Constraint requiring only that the non-byzantine nodes are not equivocating. *) Definition non_byzantine_not_equivocating_constraint : composite_label fixed_byzantine_IM -> composite_state fixed_byzantine_IM * option message -> Prop := sub_IM_not_equivocating_constraint fixed_byzantine_IM non_byzantine A sender. -(** The first definition of the [fixed_byzantine_trace_prop]erty: +Definition fixed_byzantine_composite_vlsm : VLSM message := + composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint. -Fixed byzantine traces are projections to the subset of protocol-following nodes -of traces which are valid for the composition in which a fixed set of nodes -were replaced by byzantine nodes and the rest are protocol-following -(i.e., they are not equivocating). +(** +Given that we're only looking at the composition of nodes in the +[non_byzantine], we can define their subset as either a subset of the +[fixed_byzantine_IM] or of the original <>. + +As it turns out, the first definition is easier to prove equivalent to the +induced [fixed_non_byzantine_projection], while the second is easier to work +with in general because it makes no reference to byzantine nodes. + +Therefore we'll first be defining them both below and show that they are +equivalent to each-other using the generic Lemma [same_IM_full_projection]. *) -Definition fixed_byzantine_trace_prop - (is : composite_state (sub_IM fixed_byzantine_IM non_byzantine)) - (tr : list (composite_transition_item (sub_IM fixed_byzantine_IM non_byzantine))) - : Prop := - exists bis btr, - finite_valid_trace (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint) bis btr /\ - composite_state_sub_projection fixed_byzantine_IM non_byzantine bis = is /\ - finite_trace_sub_projection fixed_byzantine_IM non_byzantine btr = tr. + +Definition pre_loaded_fixed_non_byzantine_vlsm' : VLSM message := + pre_loaded_with_all_messages_vlsm (free_composite_vlsm (sub_IM fixed_byzantine_IM non_byzantine)). + +Lemma pre_loaded_fixed_non_byzantine_vlsm'_projection + : VLSM_projection fixed_byzantine_composite_vlsm pre_loaded_fixed_non_byzantine_vlsm' + (composite_label_sub_projection_option fixed_byzantine_IM non_byzantine) + (composite_state_sub_projection fixed_byzantine_IM non_byzantine). +Proof. + constructor; [apply induced_sub_projection_is_projection|]. + intros sX trX HtrX. + apply + (VLSM_projection_finite_valid_trace + (induced_sub_projection_is_projection fixed_byzantine_IM non_byzantine _)) + in HtrX. + revert HtrX. + apply VLSM_incl_finite_valid_trace. + apply induced_sub_projection_preloaded_free_incl. +Qed. + +Definition pre_loaded_fixed_non_byzantine_vlsm : VLSM message := + pre_loaded_with_all_messages_vlsm (free_composite_vlsm (sub_IM IM non_byzantine)). + +Definition non_byzantine_nodes_same sub_i + : sub_IM fixed_byzantine_IM non_byzantine sub_i = sub_IM IM non_byzantine sub_i. +Proof. + unfold sub_IM, fixed_byzantine_IM, update_IM; cbn. + case_decide as Hi; [| done]. + contradict Hi; apply selection_complement_index_not_in_selection. +Defined. + +Definition non_byzantine_nodes_same_sym := same_IM_sym non_byzantine_nodes_same. + +Lemma pre_loaded_fixed_non_byzantine_vlsm_full_projection + : VLSM_full_projection + pre_loaded_fixed_non_byzantine_vlsm' + pre_loaded_fixed_non_byzantine_vlsm + (same_IM_label_rew non_byzantine_nodes_same) + (same_IM_state_rew non_byzantine_nodes_same). +Proof. + apply same_IM_preloaded_free_full_projection. +Qed. + +Lemma pre_loaded_fixed_non_byzantine_vlsm_full_projection' + : VLSM_full_projection + pre_loaded_fixed_non_byzantine_vlsm + pre_loaded_fixed_non_byzantine_vlsm' + (same_IM_label_rew non_byzantine_nodes_same_sym) + (same_IM_state_rew non_byzantine_nodes_same_sym). +Proof. + apply same_IM_preloaded_free_full_projection. +Qed. + +Definition pre_loaded_fixed_non_byzantine_label_projection := + (mbind (Some ∘ (same_IM_label_rew non_byzantine_nodes_same))) ∘ + (composite_label_sub_projection_option fixed_byzantine_IM non_byzantine). + +Definition pre_loaded_fixed_non_byzantine_state_projection := + (same_IM_state_rew non_byzantine_nodes_same) ∘ + (composite_state_sub_projection fixed_byzantine_IM non_byzantine). + +Lemma pre_loaded_fixed_non_byzantine_vlsm_projection + : VLSM_projection fixed_byzantine_composite_vlsm pre_loaded_fixed_non_byzantine_vlsm + pre_loaded_fixed_non_byzantine_label_projection + pre_loaded_fixed_non_byzantine_state_projection. +Proof. + apply (@VLSM_projection_composition _ _ _ pre_loaded_fixed_non_byzantine_vlsm _ _ pre_loaded_fixed_non_byzantine_vlsm'_projection), + @VLSM_full_projection_is_projection, pre_loaded_fixed_non_byzantine_vlsm_full_projection. +Qed. + +Definition pre_loaded_fixed_non_byzantine_label_component_projection i := + (mbind (sub_label_element_project IM non_byzantine i)) ∘ + pre_loaded_fixed_non_byzantine_label_projection. + +Definition pre_loaded_fixed_non_byzantine_state_component_projection i (Hi : i ∈ non_byzantine) := + sub_state_element_project IM non_byzantine i Hi ∘ + pre_loaded_fixed_non_byzantine_state_projection. + +Lemma pre_loaded_fixed_non_byzantine_vlsm_component_projection i (Hi : i ∈ non_byzantine) + : VLSM_projection fixed_byzantine_composite_vlsm (pre_loaded_with_all_messages_vlsm (IM i)) + (pre_loaded_fixed_non_byzantine_label_component_projection i) + (pre_loaded_fixed_non_byzantine_state_component_projection i Hi). +Proof. + apply (VLSM_projection_composition pre_loaded_fixed_non_byzantine_vlsm_projection (sub_preloaded_all_component_projection IM non_byzantine i Hi _)). +Qed. (** ** Byzantine traces characterization as projections. *) -Section fixed_byzantine_traces_as_projections. +Section sec_fixed_non_byzantine_projection. Definition fixed_non_byzantine_projection : VLSM message := pre_induced_sub_projection fixed_byzantine_IM non_byzantine non_byzantine_not_equivocating_constraint. @@ -165,27 +206,23 @@ Lemma fixed_non_byzantine_projection_initial_state_preservation composite_initial_state_prop (sub_IM fixed_byzantine_IM non_byzantine) s. Proof. split. - - intros Hs sub_i. - destruct Hs as [sX [HeqsX Hinitial]]. - subst. + - intros (sX & HeqsX & Hinitial) sub_i; subst. apply Hinitial. - intros Hs. - exists (lift_sub_state fixed_byzantine_IM non_byzantine s). - split. + eexists; split. + apply composite_state_sub_projection_lift_to. - + by apply (lift_sub_state_initial fixed_byzantine_IM non_byzantine). + + apply (lift_sub_state_initial fixed_byzantine_IM); assumption. Qed. Lemma fixed_non_byzantine_projection_incl_preloaded : VLSM_incl fixed_non_byzantine_projection (pre_loaded_with_all_messages_vlsm (free_composite_vlsm (sub_IM fixed_byzantine_IM non_byzantine))). Proof. - apply basic_VLSM_strong_incl. - - by intros s H1; apply fixed_non_byzantine_projection_initial_state_preservation. - - by intros. - - by split; [eapply induced_sub_projection_valid_preservation |]. - - intros l s om s' om'; cbn. - (* an ugly trick to get the forward direction from an iff (<->) lemma *) - by eapply proj1; rapply @induced_sub_projection_transition_preservation. + apply basic_VLSM_strong_incl; intros ? *. + - apply fixed_non_byzantine_projection_initial_state_preservation. + - intros _; compute; trivial. + - split; [|exact I]. + eapply induced_sub_projection_valid_preservation; eassumption. + - intro Ht; apply induced_sub_projection_transition_preservation in Ht; assumption. Qed. (** The induced projection from the composition of [fixed_byzantine_IM] under @@ -197,115 +234,345 @@ Lemma fixed_non_byzantine_projection_friendliness (induced_sub_projection_is_projection fixed_byzantine_IM non_byzantine non_byzantine_not_equivocating_constraint). Proof. - apply induced_sub_projection_friendliness. - apply induced_sub_projection_lift. - intros s1 s2 Heq l om. - destruct om as [m|]; [|itauto]. - cbn. - destruct (sender m) as [v|]; [|itauto]. - simpl. - case_decide as HAv; [|itauto]. - replace (s2 (A v)) with (s1 (A v)); [itauto|]. - exact (equal_f_dep Heq (dexist (A v) HAv)). -Qed. - -(** Characterization result for the first definition: -the [fixed_byzantine_trace_prop]erty is equivalent to the -[finite_valid_trace_prop]erty of the [pre_induced_sub_projection] of the -the composition in which a fixed set of nodes were replaced by byzantine nodes -and the rest are protocol-following to the set of protocol-following nodes. -*) -Lemma fixed_byzantine_trace_char1 is tr - : fixed_byzantine_trace_prop is tr <-> - finite_valid_trace fixed_non_byzantine_projection is tr. -Proof. - apply and_comm. - apply (projection_friendly_trace_char (induced_sub_projection_is_projection _ _ _)). - apply fixed_non_byzantine_projection_friendliness. + apply induced_sub_projection_friendliness, induced_sub_projection_lift. + intros s1 s2 Heq l [m|]; [|intuition]; cbn. + destruct (sender m) as [v|]; [|intuition]; cbn. + case_decide as HAv; [|intuition]. + replace (s2 (A v)) with (s1 (A v)); [intuition|]. + apply (equal_f_dep Heq (dexist (A v) HAv)). Qed. -End fixed_byzantine_traces_as_projections. +End sec_fixed_non_byzantine_projection. -(** ** Fixed Byzantine traces as traces pre-loaded with signed messages +End sec_fixed_byzantine_replacements. -In this section we'll be showing that byzantine traces correspond to traces of -the composition of nodes in the [non_byzantine], preloaded with messages -signed by the nodes in the <>. + +Definition byzantine_replacements : Type := + { byzantine_replacements_IM : sub_index byzantine -> VLSM message | + no_initial_messages_in_IM_prop byzantine_replacements_IM /\ + channel_authentication_prop byzantine_replacements_IM (sub_IM_A byzantine A) (sub_IM_sender byzantine A sender) + }. + +(** The first definition of the [fixed_byzantine_trace_prop]erty: + +Fixed byzantine traces are projections to the subset of protocol-following nodes +of traces which are valid for the composition in which a fixed set of nodes +were replaced by byzantine nodes and the rest are protocol-following +(i.e., they are not equivocating). *) +Definition fixed_byzantine_trace : Type := + { byz_IM : byzantine_replacements & { istr | + finite_valid_trace (fixed_byzantine_composite_vlsm (` byz_IM)) istr.1 istr.2}}. -Section fixed_byzantine_traces_as_pre_loaded. +Definition trace_exposed_to_fixed_byzantine_behavior_prop + (is : composite_state (sub_IM IM non_byzantine)) + (tr : list (composite_transition_item (sub_IM IM non_byzantine))) + : Prop := + exists byz_tr : fixed_byzantine_trace, + match byz_tr with + existT (exist _ byz_IM _) (exist _ (byzantine_is, byzantine_tr) _) => + pre_loaded_fixed_non_byzantine_state_projection byz_IM byzantine_is = is /\ + VLSM_projection_trace_project (pre_loaded_fixed_non_byzantine_vlsm_projection byz_IM) byzantine_tr = tr + end. -Definition fixed_set_signed_message (m : message) : Prop := - non_sub_index_authenticated_message non_byzantine A sender m /\ - (exists i, i ∈ non_byzantine /\ exists l s, input_valid (pre_loaded_with_all_messages_vlsm (IM i)) l (s, Some m)). +End sec_fixed_byzantine_traces. -(** -Given that we're only looking at the composition of nodes in the -[non_byzantine], we can define their subset as either a subset of the -[fixed_byzantine_IM] or of the original <>. +Section fixed_non_equivocating_vs_byzantine. -As it turns out, the first definition is easier to prove equivalent to the -induced [fixed_non_byzantine_projection], while the second is easier to work -with in general because it makes no reference to byzantine nodes. +Context + {message : Type} + `{finite.Finite index} + (IM : index -> VLSM message) + `{Hbs : forall i : index, HasBeenSentCapability (IM i)} + `{Hbr : forall i : index, HasBeenReceivedCapability (IM i)} + (selection : set index) + {validator : Type} + (A : validator -> index) + (sender : message -> option validator) + (selection_complement := set_diff (enum index) selection) + (Fixed : VLSM message := fixed_equivocation_vlsm_composition IM selection) + (StrongFixed := strong_fixed_equivocation_vlsm_composition IM selection) + (FixedNonEquivocating : VLSM message := pre_induced_sub_projection IM selection_complement (fixed_equivocation_constraint IM selection)) + (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM) + (can_emit_signed : channel_authentication_prop IM A sender) + (Hsender_safety : sender_safety_alt_prop IM A sender := + channel_authentication_sender_safety IM A sender can_emit_signed) + . -Therefore we'll first be defining them both below and show that they are -equivalent to each-other using the generic Lemma [same_IM_full_projection]. -*) +Definition byzantine_id_replacements_same_IM + : forall i, fixed_byzantine_IM IM selection (fun sub_i => IM (` sub_i)) i = IM i + := update_IM_id_same_IM IM selection. -Definition pre_loaded_fixed_non_byzantine_vlsm' : VLSM message := - composite_no_equivocation_vlsm_with_pre_loaded (sub_IM fixed_byzantine_IM non_byzantine) (free_constraint _) fixed_set_signed_message. +Definition byzantine_id_replacements_same_IM_sym := same_IM_sym byzantine_id_replacements_same_IM. -Definition pre_loaded_fixed_non_byzantine_vlsm : VLSM message := - composite_no_equivocation_vlsm_with_pre_loaded (sub_IM IM non_byzantine) (free_constraint _) fixed_set_signed_message. +Lemma byzantine_id_replacements_full_projection + : VLSM_full_projection + (fixed_byzantine_composite_vlsm IM selection A sender (fun sub_i => IM (` sub_i))) + (composite_vlsm IM (sub_IM_not_equivocating_constraint IM selection_complement A sender)) + (same_IM_label_rew byzantine_id_replacements_same_IM) + (same_IM_state_rew byzantine_id_replacements_same_IM). +Proof. + apply same_IM_full_projection; intros s Hs l [m|]; [|trivial]. + subst selection_complement + ; unfold non_byzantine_not_equivocating_constraint, + sub_IM_not_equivocating_constraint. + destruct (sender m) as [v|]; [|trivial]; cbn. + case_decide as HAv; [|trivial]. + unfold sub_IM, fixed_byzantine_IM; cbn; intro Hsent. + eapply VLSM_full_projection_has_been_sent in Hsent + ; [eassumption|apply same_VLSM_preloaded_full_projection|]. + eapply VLSM_projection_valid_state in Hs + ; [| apply preloaded_component_projection with (j := A v)]. + assumption. +Qed. -Lemma non_byzantine_nodes_same - : forall sub_i, sub_IM fixed_byzantine_IM non_byzantine sub_i = sub_IM IM non_byzantine sub_i. +Lemma byzantine_id_replacements_full_projection_rev + : VLSM_full_projection + (composite_vlsm IM (sub_IM_not_equivocating_constraint IM selection_complement A sender)) + (fixed_byzantine_composite_vlsm IM selection A sender (fun sub_i => IM (` sub_i))) + (same_IM_label_rew byzantine_id_replacements_same_IM_sym) + (same_IM_state_rew byzantine_id_replacements_same_IM_sym). Proof. - intro sub_i. - destruct_dec_sig sub_i i Hi Heqsub_i. - subst. - unfold sub_IM, fixed_byzantine_IM, update_IM. - simpl. - apply set_diff_elim2 in Hi. - by rewrite decide_False. + apply same_IM_full_projection; intros s Hs l [m|]; [|trivial]. + subst selection_complement + ; unfold non_byzantine_not_equivocating_constraint, + sub_IM_not_equivocating_constraint. + destruct (sender m) as [v|]; [|trivial]; cbn. + case_decide as HAv; [|trivial]. + unfold sub_IM, fixed_byzantine_IM; cbn; intro Hsent. + eapply VLSM_full_projection_has_been_sent in Hsent + ; [eassumption|apply same_VLSM_preloaded_full_projection|]. + eapply VLSM_projection_valid_state in Hs + ; [| apply preloaded_component_projection with (j := A v)]. + assumption. Qed. -Lemma non_byzantine_nodes_same_sym - : forall sub_i, sub_IM IM non_byzantine sub_i = sub_IM fixed_byzantine_IM non_byzantine sub_i. +Lemma fixed_sub_IM_non_equivocating_subsumption + : input_valid_constraint_subsumption IM + (fixed_equivocation_constraint IM selection) + (sub_IM_not_equivocating_constraint IM selection_complement A sender). Proof. - intro. symmetry. apply non_byzantine_nodes_same. + intros l (s, [m|]) Hv; cbn; [|trivial]. + apply (fixed_strong_equivocation_subsumption IM selection) + in Hv as Hstrong_v. + destruct Hv as (Hs & _). + destruct (sender m) as [v|] eqn:Hsender; cbn; [|trivial]. + case_decide as HAv; [|trivial]. + unfold sub_IM; cbn. + destruct Hstrong_v as [(i & Hi & Hsent) | Hemitted]; cycle 1. + - exfalso; apply set_diff_elim2 in HAv; contradict HAv. + eapply (sub_can_emit_sender IM); eassumption. + - eapply VLSM_incl_valid_state in Hs; [|apply constraint_free_incl]. + apply + (VLSM_incl_valid_state + (vlsm_incl_pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))) + in Hs. + cut (@has_been_sent _ _ (Hbs (A v)) (s (A v)) m). + { eapply has_been_sent_irrelevance, + valid_state_project_preloaded_to_preloaded, Hs. + } + eapply valid_state_has_trace in Hs as (is & tr & Htr). + eapply (has_been_sent_iff_by_sender IM). 1-3: eassumption. + eexists; eassumption. Qed. -Lemma pre_loaded_fixed_non_byzantine_vlsm_full_projection - : VLSM_full_projection - pre_loaded_fixed_non_byzantine_vlsm' - pre_loaded_fixed_non_byzantine_vlsm - (same_IM_label_rew non_byzantine_nodes_same) - (same_IM_state_rew non_byzantine_nodes_same). +Lemma fixed_non_equivocating_incl_sub_non_equivocating + : VLSM_incl FixedNonEquivocating + (pre_induced_sub_projection IM (set_diff (enum index) selection) + (sub_IM_not_equivocating_constraint IM + (set_diff (enum index) selection) A sender)). Proof. - apply same_IM_full_projection. - intros s1 Hs1 l1 om [Hom _]. - split; [| done]. - destruct om as [m |]; [| done]. - destruct Hom as [Hsent | Hseeded]; [left | by right]. - by eapply same_IM_composite_has_been_sent_preservation. + apply induced_sub_projection_constraint_subsumption_incl, + fixed_sub_IM_non_equivocating_subsumption. Qed. -Lemma pre_loaded_fixed_non_byzantine_vlsm_full_projection' - : VLSM_full_projection - pre_loaded_fixed_non_byzantine_vlsm - pre_loaded_fixed_non_byzantine_vlsm' - (same_IM_label_rew non_byzantine_nodes_same_sym) - (same_IM_state_rew non_byzantine_nodes_same_sym). +Lemma Fixed_sub_IM_non_equivocating_incl + : VLSM_incl Fixed (composite_vlsm IM (sub_IM_not_equivocating_constraint IM selection_complement A sender)). +Proof. + apply constraint_subsumption_incl, fixed_sub_IM_non_equivocating_subsumption. +Qed. + +Lemma fixed_equivocating_traces_are_byzantine_component i (Hi : i ∈ set_diff (enum index) selection) + : byzantine_id_replacements_same_IM_sym i + = + non_byzantine_nodes_same_sym IM selection (fun sub_i => IM (`sub_i)) (dexist i Hi). +Proof. + unfold byzantine_id_replacements_same_IM_sym, + non_byzantine_nodes_same_sym, same_IM_sym + ; f_equal. + unfold byzantine_id_replacements_same_IM, non_byzantine_nodes_same, + update_IM_id_same_IM, fixed_byzantine_IM, update_IM; cbn. + apply set_diff_elim2 in Hi as Hni. + case_decide; [contradiction|reflexivity]. +Qed. + +Lemma fixed_equivocating_traces_are_byzantine_label l + : pre_loaded_fixed_non_byzantine_label_projection IM selection (fun sub_i => IM (`sub_i)) + (same_IM_label_rew byzantine_id_replacements_same_IM_sym l) + = + composite_label_sub_projection_option IM selection_complement l. +Proof. + destruct l as (i, li). + unfold pre_loaded_fixed_non_byzantine_label_projection, + composite_label_sub_projection_option, composite_label_sub_projection, same_IM_label_rew + ; subst selection_complement; cbn. + case_decide as Hi; [|reflexivity]; cbn. + do 2 f_equal. + rewrite <- same_VLSM_label_rew_21 + with (Heq := non_byzantine_nodes_same IM selection (fun sub_i => IM (`sub_i)) (dexist i Hi)). + do 2 f_equal. + apply fixed_equivocating_traces_are_byzantine_component. +Qed. + +Lemma fixed_equivocating_traces_are_byzantine_state s + : pre_loaded_fixed_non_byzantine_state_projection IM selection (fun sub_i => IM (`sub_i)) + (same_IM_state_rew byzantine_id_replacements_same_IM_sym s) + = + composite_state_sub_projection IM selection_complement s. +Proof. + unfold pre_loaded_fixed_non_byzantine_state_projection, + composite_state_sub_projection, same_IM_state_rew. + extensionality sub_i; cbn. + rewrite <- same_VLSM_state_rew_21 + with (Heq := non_byzantine_nodes_same IM selection (fun sub_i => IM (`sub_i)) sub_i). + f_equal; destruct_dec_sig sub_i i Hi Heqsub_i; subst; cbn; f_equal. + apply fixed_equivocating_traces_are_byzantine_component. +Qed. + +Lemma fixed_equivocating_traces_are_byzantine_trace tr +: VLSM_projection_trace_project + (pre_loaded_fixed_non_byzantine_vlsm_projection IM selection A sender (fun sub_i => IM (`sub_i))) + (VLSM_full_projection_finite_trace_project byzantine_id_replacements_full_projection_rev tr) += + finite_trace_sub_projection IM selection_complement tr. +Proof. + induction tr; [reflexivity|]; cbn; rewrite IHtr. + replace (pre_VLSM_projection_transition_item_project _ _ _ _ _) with + (pre_VLSM_projection_transition_item_project (composite_type IM) + (composite_type (sub_IM IM selection_complement)) + (composite_label_sub_projection_option IM selection_complement) + (composite_state_sub_projection IM selection_complement) a) + ; [reflexivity|]. + destruct a; unfold pre_VLSM_projection_transition_item_project; cbn. + rewrite fixed_equivocating_traces_are_byzantine_state, + fixed_equivocating_traces_are_byzantine_label. + reflexivity. +Qed. + +Program Definition fixed_equivocating_traces_are_byzantine_replacements + : byzantine_replacements selection A sender := + exist _ (fun sub_i => IM (` sub_i)) _. +Next Obligation. + split. + - apply sub_IM_preserves_no_initial_messages; assumption. + - apply sub_IM_preserves_channel_authentication; assumption. +Qed. + +Program Definition fixed_equivocating_traces_are_byzantine_traces eis etr + (Htr : finite_valid_trace Fixed eis etr) + : fixed_byzantine_trace IM selection A sender := + (existT fixed_equivocating_traces_are_byzantine_replacements + (exist _ + (same_IM_state_rew byzantine_id_replacements_same_IM_sym eis, + VLSM_full_projection_finite_trace_project byzantine_id_replacements_full_projection_rev etr) + _)). +Next Obligation. + intros; cbn. + apply (VLSM_full_projection_finite_valid_trace byzantine_id_replacements_full_projection_rev). + revert Htr; apply VLSM_incl_finite_valid_trace. + apply Fixed_sub_IM_non_equivocating_incl. +Qed. + +Lemma fixed_equivocating_traces_are_byzantine eis etr + : finite_valid_trace Fixed eis etr -> + trace_exposed_to_fixed_byzantine_behavior_prop IM selection A sender + (composite_state_sub_projection IM selection_complement eis) + (finite_trace_sub_projection IM selection_complement etr). Proof. - apply same_IM_full_projection. - intros s1 Hs1 l1 om [Hom _]. - split; [| done]. - destruct om as [m |]; [| done]. - destruct Hom as [Hsent | Hseeded]; [left | by right]. - by eapply same_IM_composite_has_been_sent_preservation. + intros Htr. + exists (fixed_equivocating_traces_are_byzantine_traces _ _ Htr); cbn; split. + - apply fixed_equivocating_traces_are_byzantine_state. + - apply fixed_equivocating_traces_are_byzantine_trace. Qed. +Context + (Hvalidator: + forall i : index, i ∉ selection -> + component_message_validator_prop IM (fixed_equivocation_constraint IM selection) i) + . + +Lemma fixed_byzantine_traces_are_equivocating + (byz_tr : fixed_byzantine_trace IM selection A sender) + : match byz_tr with + existT (exist _ byz_IM _) (exist _ (byzantine_is, byzantine_tr) _) => + exists eis, composite_state_sub_projection IM selection_complement eis = pre_loaded_fixed_non_byzantine_state_projection IM selection byz_IM byzantine_is /\ + exists etr, finite_trace_sub_projection IM selection_complement etr = VLSM_projection_trace_project (pre_loaded_fixed_non_byzantine_vlsm_projection IM selection A sender byz_IM) byzantine_tr /\ + finite_valid_trace Fixed eis etr + end. +Proof. + destruct byz_tr as ((byz_IM & no_initial_byz & can_emit_byz) & (byz_is, byz_tr) & Hbyz_tr); cbn in *. + eexists; split; [apply composite_state_sub_projection_lift|]. + eexists; split; [apply composite_trace_sub_projection_lift|]. + assert + (Hinit : composite_initial_state_prop IM + (lift_sub_state IM selection_complement + (pre_loaded_fixed_non_byzantine_state_projection IM selection byz_IM byz_is))). + { destruct Hbyz_tr as [_ Hinit] + ; eapply VLSM_projection_initial_state in Hinit + ; [| apply pre_loaded_fixed_non_byzantine_vlsm_projection]. + apply lift_sub_state_initial; assumption. + } + split; [|assumption]. + induction Hbyz_tr using finite_valid_trace_rev_ind + ; [constructor; apply initial_state_is_valid; assumption|]. + specialize (IHHbyz_tr Hinit). + unfold VLSM_projection_trace_project, pre_VLSM_projection_finite_trace_project; + rewrite map_option_app. + unfold pre_VLSM_full_projection_finite_trace_project; rewrite map_app. + apply finite_valid_trace_from_app_iff; split; [assumption|]; cbn. + remember (finite_trace_last (lift_sub_state _ _ _) _) as lst. + assert (Hlst : valid_state_prop Fixed lst) + by (subst; apply finite_valid_trace_last_pstate; assumption). + destruct l as (i, li); unfold pre_VLSM_projection_transition_item_project, pre_loaded_fixed_non_byzantine_label_projection, composite_label_sub_projection_option; cbn. + case_decide as Hi; [|constructor; assumption]; cbn. + unfold composite_label_sub_projection; cbn. + apply finite_valid_trace_singleton; cbn. + repeat split. + - assumption. + - destruct iom as [im|]; [|apply option_valid_message_None]. + apply set_diff_elim2 in Hi as Hni. + specialize (VLSM_projection_input_valid_transition (pre_loaded_fixed_non_byzantine_vlsm_component_projection IM selection A sender byz_IM i Hi) (existT i li)) as Hproj. + remember (pre_loaded_fixed_non_byzantine_label_component_projection _ _ _ _ _) as somelY. + unfold pre_loaded_fixed_non_byzantine_label_component_projection, pre_loaded_fixed_non_byzantine_label_projection, composite_label_sub_projection_option in HeqsomelY; cbn in HeqsomelY. + case_decide as H_i; [|contradiction]; unfold sub_label_element_project in HeqsomelY; cbn in HeqsomelY. + rewrite decide_True_pi with eq_refl in HeqsomelY; cbn in HeqsomelY; subst somelY. + specialize (Hproj _ eq_refl _ _ _ _ Hx) as [Hv _]. + eapply (Hvalidator i); [assumption|eassumption]. + - destruct Hx as [(_ & _ & Hv & _) _]. + revert Hv; cbn. + clear -Heqlst Hi. + subst lst. revert li. + unfold same_VLSM_label_rew, non_byzantine_nodes_same, fixed_byzantine_IM, update_IM; cbn. + + admit. +Admitted. + +(* + +(** ** Fixed Byzantine traces as traces pre-loaded with signed messages + +In this section we'll be showing that byzantine traces correspond to traces of +the composition of nodes in the [non_byzantine], preloaded with messages +signed by the nodes in the <>. +*) + +Section fixed_byzantine_traces_as_pre_loaded. + +Definition fixed_set_signed_message (m : message) : Prop := + non_sub_index_authenticated_message non_byzantine A sender m /\ + (exists i, i ∈ non_byzantine /\ exists l s, input_valid (pre_loaded_with_all_messages_vlsm (IM i)) l (s, Some m)). + + (** We next show that the [fixed_non_byzantine_projection] and [pre_loaded_fixed_non_byzantine_vlsm'] are [VLSM_eq]ual. @@ -534,36 +801,6 @@ Context channel_authentication_sender_safety IM A sender can_emit_signed) . -Lemma fixed_non_equivocating_incl_sub_non_equivocating - : VLSM_incl FixedNonEquivocating - (pre_induced_sub_projection IM (set_diff (enum index) selection) - (sub_IM_not_equivocating_constraint IM - (set_diff (enum index) selection) A sender)). -Proof. - apply induced_sub_projection_constraint_subsumption_incl. - intros l (s, om) Hv. - apply (fixed_strong_equivocation_subsumption IM selection) - in Hv as Hstrong_v. - destruct Hv as (Hs & Hom & Hv & Hc). - destruct om; [| done]. - cbn; destruct (sender m) as [v |] eqn: Hsender; [| done]; cbn. - case_decide as HAv; [| done]. - unfold sub_IM; cbn. - apply (VLSM_incl_valid_state (constraint_free_incl IM (fixed_equivocation_constraint IM selection))) in Hs. - apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))) in Hs. - assert (Hpre_si : forall i, valid_state_prop (pre_loaded_with_all_messages_vlsm (IM i)) (s i)). - { - intro i. - revert Hs. - apply valid_state_project_preloaded_to_preloaded. - } - apply set_diff_elim2 in HAv. - destruct Hstrong_v as [(i & Hi & Hsent) | Hemitted]. - - apply valid_state_has_trace in Hs as (is & tr & Htr). - by eapply has_been_sent_iff_by_sender; [| | | exists i]. - - by contradict HAv; eapply sub_can_emit_sender. -Qed. - Lemma fixed_non_equivocating_incl_fixed_non_byzantine : VLSM_incl FixedNonEquivocating PreNonByzantine. Proof. @@ -746,7 +983,7 @@ End assuming_initial_messages_lift. Context (Hvalidator: forall i : index, i ∉ selection -> - component_message_validator_prop IM (fixed_equivocation_constraint IM selection) i) + component_message_validator_prop IM (fixed_equivocation_constraint IM Hbs Hbr selection) i) . Lemma validator_fixed_non_byzantine_vlsm_lift_initial_message @@ -806,5 +1043,6 @@ Proof. Qed. End validator_fixed_set_byzantine. +*) End fixed_non_equivocating_vs_byzantine. diff --git a/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v index 4fefcd7d..7599f83a 100644 --- a/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v +++ b/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v @@ -7,6 +7,8 @@ From VLSM.Core Require Import Validator Equivocation Equivocation.FixedSetEquivo From VLSM.Core Require Import Equivocation.LimitedEquivocation Equivocation.LimitedEquivocation. From VLSM.Core Require Import Equivocation.MsgDepLimitedEquivocation Equivocation.TraceWiseEquivocation. +(* + (** * VLSM Compositions with byzantine nodes of limited weight In this module we define and study protocol executions allowing a @@ -20,7 +22,7 @@ projections of traces of the composition of the regular nodes under a composition constraint allowing only a limited amount of equivocation. *) -Section limited_byzantine_traces. +Section sec_limited_byzantine_traces. Context {message : Type} @@ -66,6 +68,26 @@ Context (Hfull : forall i, message_dependencies_full_node_condition_prop message_dependencies (IM i)) . +Program Definition limited_equivocating_traces_are_byzantine is tr + (Htr : finite_valid_trace Limited is tr) + (equivocators := state_annotation (finite_trace_last is tr)) + : limited_byzantine_trace := + existT (exist _ equivocators _) + (fixed_equivocating_traces_are_byzantine_traces IM equivocators Datatypes.id sender no_initial_messages_in_IM Hchannel (original_state is) (pre_VLSM_full_projection_finite_trace_project + (type Limited) (composite_type IM) Datatypes.id original_state + tr) _). +Next Obligation. + intros; cbn. + eapply msg_dep_fixed_limited_equivocation_witnessed; eassumption. +Qed. +Next Obligation. + intros; cbn. + eapply msg_dep_fixed_limited_equivocation_witnessed; eassumption. +Qed. + + +End sec_limited_byzantine_traces. + (** ** Assuming the byzantine nodes are known We will first fix a selection of <> nodes of limited weight and analyze traces with the [fixed_limited_byzantine_trace_prop]erty w.r.t. that @@ -470,3 +492,4 @@ Proof. Qed. End sec_msg_dep_limited_byzantine_traces. +*) \ No newline at end of file diff --git a/theories/VLSM/Core/Composition.v b/theories/VLSM/Core/Composition.v index 31b4a4a3..296209be 100644 --- a/theories/VLSM/Core/Composition.v +++ b/theories/VLSM/Core/Composition.v @@ -1,6 +1,6 @@ From Cdcl Require Import Itauto. Local Tactic Notation "itauto" := itauto auto. From stdpp Require Import prelude finite. -From Coq Require Import Streams FunctionalExtensionality FinFun Eqdep. +From Coq Require Import Streams FunctionalExtensionality FinFun Eqdep Program. From VLSM Require Import Lib.Preamble Lib.ListExtras Lib.StdppListSet Lib.StreamExtras. From VLSM Require Import Core.VLSM Core.Plans Core.VLSMProjections. @@ -1462,7 +1462,9 @@ Definition same_IM_state_rew : composite_state IM2 := fun i => same_VLSM_state_rew (Heq i) (s1 i). -Section pre_loaded_constrained. +Definition same_IM_sym : forall i, IM2 i = IM1 i := fun i => eq_sym (Heq i). + +Section sec_same_IM_constrained. Context (constraint1 : composite_label IM1 -> composite_state IM1 * option message -> Prop) @@ -1471,10 +1473,15 @@ Context : forall s1, valid_state_prop (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM1)) s1 -> forall l1 om, constraint1 l1 (s1,om) -> constraint2 (same_IM_label_rew l1) (same_IM_state_rew s1, om)) + . + +Section sec_same_IM_preloaded_full_projection. + +Context (seed : message -> Prop) . -Lemma same_IM_full_projection +Lemma same_IM_preloaded_full_projection : VLSM_full_projection (pre_loaded_vlsm (composite_vlsm IM1 constraint1) seed) (pre_loaded_vlsm (composite_vlsm IM2 constraint2) seed) @@ -1510,7 +1517,28 @@ Proof. + by exists (exist _ m Hm). Qed. -End pre_loaded_constrained. +End sec_same_IM_preloaded_full_projection. + +Lemma same_IM_full_projection + : VLSM_full_projection + (composite_vlsm IM1 constraint1) + (composite_vlsm IM2 constraint2) + same_IM_label_rew + same_IM_state_rew. +Proof. + constructor. + intros s1 tr1 Htr1. + apply + (VLSM_eq_finite_valid_trace + (vlsm_is_pre_loaded_with_False (composite_vlsm IM2 constraint2))), + (VLSM_full_projection_finite_valid_trace + (same_IM_preloaded_full_projection (fun _ => False))), + (VLSM_eq_finite_valid_trace + (vlsm_is_pre_loaded_with_False (composite_vlsm IM1 constraint1))). + assumption. +Qed. + +End sec_same_IM_constrained. Lemma same_IM_preloaded_free_full_projection : VLSM_full_projection @@ -1519,21 +1547,47 @@ Lemma same_IM_preloaded_free_full_projection same_IM_label_rew same_IM_state_rew. Proof. - constructor. - intros s1 tr1 Htr1. - specialize (pre_loaded_with_all_messages_vlsm_is_pre_loaded_with_True (free_composite_vlsm IM1)) as Heq1. - apply (VLSM_eq_finite_valid_trace Heq1) in Htr1. - clear Heq1. - specialize (same_IM_full_projection (free_constraint IM1) (free_constraint IM2)) - as Hproj. - spec Hproj; [done |]. - specialize (Hproj (fun _ => True)). - apply (VLSM_full_projection_finite_valid_trace Hproj) in Htr1. - specialize (pre_loaded_with_all_messages_vlsm_is_pre_loaded_with_True (free_composite_vlsm IM2)) as Heq2. - by apply (VLSM_eq_finite_valid_trace Heq2). + constructor; intros. + assert + (Hproj : + VLSM_full_projection + (pre_loaded_vlsm (free_composite_vlsm IM1) (const True)) + (pre_loaded_vlsm (free_composite_vlsm IM2) (const True)) + same_IM_label_rew + same_IM_state_rew) + by (apply same_IM_preloaded_full_projection; done). + by apply + (VLSM_eq_finite_valid_trace + (pre_loaded_with_all_messages_vlsm_is_pre_loaded_with_True (free_composite_vlsm IM2))), + (VLSM_full_projection_finite_valid_trace Hproj), + (VLSM_eq_finite_valid_trace + (pre_loaded_with_all_messages_vlsm_is_pre_loaded_with_True (free_composite_vlsm IM1))). Qed. End sec_same_IM_full_projection. Arguments same_IM_label_rew {_ _ _ _} _ _ : assert. Arguments same_IM_state_rew {_ _ _ _} _ _ _ : assert. +Arguments same_IM_sym {_ _ _ _} _ _ : assert. + +Lemma same_IM_state_rew_12 + {message : Type} + `{EqDecision index} + {IM1 IM2 : index -> VLSM message} + (Heq : forall i, IM1 i = IM2 i) + : forall s : composite_state IM1, + same_IM_state_rew (same_IM_sym Heq) (same_IM_state_rew Heq s) = s. +Proof. + intro; extensionality i; apply same_VLSM_state_rew_12. +Qed. + +Lemma same_IM_state_rew_21 + {message : Type} + `{EqDecision index} + {IM1 IM2 : index -> VLSM message} + (Heq : forall i, IM1 i = IM2 i) + : forall s : composite_state IM2, + same_IM_state_rew Heq (same_IM_state_rew (same_IM_sym Heq) s) = s. +Proof. + intro; extensionality i; apply same_VLSM_state_rew_21. +Qed. diff --git a/theories/VLSM/Core/Equivocators/Composition/Projections.v b/theories/VLSM/Core/Equivocators/Composition/Projections.v index 7a3e6c0c..c3d1c53f 100644 --- a/theories/VLSM/Core/Equivocators/Composition/Projections.v +++ b/theories/VLSM/Core/Equivocators/Composition/Projections.v @@ -1472,7 +1472,7 @@ Lemma equivocators_total_VLSM_projection_trace_project Proof. induction tr using rev_ind; [done |]. rewrite equivocators_total_trace_project_app by (eexists; done). - rewrite @pre_VLSM_projection_finite_trace_project_app. + rewrite pre_VLSM_projection_finite_trace_project_app. apply finite_valid_trace_from_app_iff in Hpre_tr as [Hpre_tr Hpre_x]. specialize (IHtr Hpre_tr). rewrite IHtr. diff --git a/theories/VLSM/Core/MessageDependencies.v b/theories/VLSM/Core/MessageDependencies.v index 9b94d5f6..ea284240 100644 --- a/theories/VLSM/Core/MessageDependencies.v +++ b/theories/VLSM/Core/MessageDependencies.v @@ -69,11 +69,26 @@ relation. Definition msg_dep_rel : relation message := fun m1 m2 => m1 ∈ message_dependencies m2. -(** The transitive closure ([clos_trans_1n]) of the [msg_dep_rel]ation is a -happens-before relation. +(** The transitive closure of the [msg_dep_rel]ation is a happens-before +relation. *) Definition msg_dep_happens_before : relation message := flip (clos_trans_1n _ (flip msg_dep_rel)). +(** The relaxed (local) full node condition for a given <> +function requires that a state (receiving the message) is aware of all +of <>'s dependencies. +*) +Definition relaxed_message_dependencies_full_node_condition + (s : vstate X) + (m : message) + : Prop := + forall dm, dm ∈ message_dependencies m -> + exists obs_m, has_been_observed X s obs_m /\ msg_dep_happens_before dm obs_m. + +Definition relaxed_message_dependencies_full_node_condition_prop : Prop := + forall l s m, + vvalid X l (s, Some m) -> relaxed_message_dependencies_full_node_condition s m. + (** Unrolling one the [msg_dep_happens_before] relation one step. *) Lemma msg_dep_happens_before_iff_one x z : msg_dep_happens_before x z <-> diff --git a/theories/VLSM/Core/SubProjectionTraces.v b/theories/VLSM/Core/SubProjectionTraces.v index b15766d7..b378b16a 100644 --- a/theories/VLSM/Core/SubProjectionTraces.v +++ b/theories/VLSM/Core/SubProjectionTraces.v @@ -103,6 +103,15 @@ Definition composite_label_sub_projection := existT (dexist i e) (projT2 l). +Lemma composite_label_sub_projection_pi + (l : composite_label IM) + (i := projT1 l) + (e e' : sub_index_prop i) + : composite_label_sub_projection l e = composite_label_sub_projection l e'. +Proof. + apply (@dec_sig_sigT_eq _ _ sub_index_prop_dec (fun i => vlabel (IM i))); reflexivity. +Qed. + Definition lift_sub_label (l : composite_label sub_IM) : composite_label IM @@ -269,9 +278,7 @@ Proof. simpl in HlX2_pr. inversion HlX2_pr. subst _i. - apply - (@dec_sig_sigT_eq_rev _ _ _ sub_index_prop_dec (fun i => vlabel (IM i))) - in HlX2_pr as ->. + apply (dec_sig_sigT_eq_rev (fun i => vlabel (IM i))) in HlX2_pr as ->. apply f_equal_dep with (x := dexist i Hi) in HsXeq_pr as HsXeq_pri. cbv in HsXeq_pri. cbn in Ht1, Ht2. @@ -315,32 +322,32 @@ Proof. - apply weak_induced_sub_projection_transition_consistency_Some. Qed. -Lemma induced_sub_projection_valid_projection l s om - (Hv : vvalid pre_induced_sub_projection l (s, om)) - : exists i, i ∈ sub_index_list /\ - exists l s, input_valid (pre_loaded_with_all_messages_vlsm (IM i)) l (s, om). +Lemma induced_sub_projection_valid_projection_strong i Hi li s om + : vvalid pre_induced_sub_projection (existT (dexist i Hi) li) (s, om) -> + input_valid (pre_loaded_with_all_messages_vlsm (IM i)) li (s (dexist i Hi), om). Proof. - destruct l as (sub_i, li). - destruct Hv as (lX & sX & [HlX Heqs (HsX & Hom & Hv)]). - destruct lX as [i _li]. - unfold composite_label_sub_projection_option in HlX. - simpl in HlX. - case_decide; [|congruence]. - unfold composite_label_sub_projection in HlX. - simpl in HlX. - apply Some_inj in HlX. - inversion HlX. subst. - simpl_existT. subst. - exists i. - split; [done |]. - cbn in Hv. - exists li, (sX i). + intros ((_i, _li) & sX & [HlX [=] (HsX & Hom & Hv)]); + unfold composite_label_sub_projection_option in HlX; cbn in HlX. + case_decide as H_i; [|congruence]. + unfold composite_label_sub_projection in HlX; cbn in HlX. + apply Some_inj in HlX; inversion HlX; subst; unfold sub_IM in li; cbn in li. + apply (dec_sig_sigT_eq_rev (fun i => vlabel (IM i))) in HlX as ->. repeat split; [|apply any_message_is_valid_in_preloaded|apply Hv]. apply (VLSM_projection_valid_state (preloaded_component_projection IM i)). apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))). by apply (VLSM_incl_valid_state (constraint_free_incl IM constraint)). Qed. +Lemma induced_sub_projection_valid_projection l s om + (Hv : vvalid pre_induced_sub_projection l (s, om)) + : exists i, i ∈ sub_index_list /\ + exists l s, input_valid (pre_loaded_with_all_messages_vlsm (IM i)) l (s, om). +Proof. + destruct l as (sub_i, li); destruct_dec_sig sub_i i Hi Heqsub_i; subst. + exists i; split; [assumption|]. + eexists _,_; eapply induced_sub_projection_valid_projection_strong; eassumption. +Qed. + Lemma induced_sub_projection_transition_is_composite l s om : vtransition pre_induced_sub_projection l (s, om) = composite_transition sub_IM l (s, om). Proof. @@ -358,6 +365,24 @@ Proof. apply lift_sub_state_to_eq. Qed. +Lemma induced_sub_projection_preloaded_free_incl + : VLSM_incl pre_induced_sub_projection (pre_loaded_with_all_messages_vlsm (free_composite_vlsm sub_IM)). +Proof. + apply basic_VLSM_strong_incl. + - intros s (sX & <- & HsX) sub_i. + destruct_dec_sig sub_i i Hi Heqsub_i. + subst. apply HsX. + - cbv; intuition. + - intros (sub_i, li) s om Hv. + split; [cbn |exact I]. + destruct_dec_sig sub_i i Hi Heqsub_i; subst. + apply induced_sub_projection_valid_projection_strong. + assumption. + - intros l s om s' om'; cbn; intros <-. + symmetry. + rapply induced_sub_projection_transition_is_composite. +Qed. + End sec_induced_sub_projection. Section induced_sub_projection_subsumption. @@ -1737,6 +1762,54 @@ Proof. all: done. Qed. +Lemma sub_preloaded_component_projection constraint P + : VLSM_projection + (pre_loaded_vlsm (composite_vlsm (sub_IM IM indices) constraint) P) + (pre_loaded_with_all_messages_vlsm (IM j)) + sub_label_element_project sub_state_element_project. +Proof. + apply basic_VLSM_projection. + - intros (sub_i, lXi) lY HlX_pr; destruct_dec_sig sub_i i Hi Heqsub_i; subst. + unfold sub_label_element_project in HlX_pr; cbn in HlX_pr. + case_decide as Hij; [|congruence]; apply Some_inj in HlX_pr; subst; cbn. + intros s om (_ & _ & Hv & _) _ _; revert Hv; cbn. + replace (s (dexist _ _)) with (sub_state_element_project s) + by apply sub_IM_state_pi. + auto. + - intros (sub_i, lXi) lY HlX_pr; destruct_dec_sig sub_i i Hi Heqsub_i; subst. + unfold sub_label_element_project in HlX_pr; cbn in HlX_pr. + case_decide as Hij; [|congruence]; apply Some_inj in HlX_pr; subst; cbn. + intros * [_ Ht]; revert Ht; cbn. + replace (s (dexist _ _)) with (sub_state_element_project s) + by apply sub_IM_state_pi. + destruct (vtransition _ _ _); inversion_clear 1; f_equal. + symmetry; apply sub_IM_state_update_eq. + - intros (sub_i, lXi) HlX_pr; destruct_dec_sig sub_i i Hi Heqsub_i; subst. + unfold sub_label_element_project in HlX_pr; cbn in HlX_pr. + case_decide as Hij; [congruence|]; clear HlX_pr. + intros * [_ Ht]; revert Ht; cbn. + destruct (vtransition _ _ _); inversion_clear 1. + apply sub_IM_state_update_neq; congruence. + - intros s Hs; apply (Hs (dexist j Hj)). + - intro; intros; apply any_message_is_valid_in_preloaded. +Qed. + +Lemma sub_preloaded_all_component_projection constraint + : VLSM_projection + (pre_loaded_with_all_messages_vlsm (composite_vlsm (sub_IM IM indices) constraint)) + (pre_loaded_with_all_messages_vlsm (IM j)) + sub_label_element_project sub_state_element_project. +Proof. + constructor; [constructor|]; cbn; intros sX trX HtrX. + - apply (@final_state_project message (pre_loaded_vlsm (composite_vlsm (sub_IM IM indices) constraint) (fun m => true))). + + apply (projection_type _ _ _ _ (sub_preloaded_component_projection constraint (fun m => True))). + + revert HtrX; apply VLSM_incl_finite_valid_trace_from. + apply pre_loaded_with_all_messages_vlsm_is_pre_loaded_with_True_l. + - apply (VLSM_projection_finite_valid_trace (sub_preloaded_component_projection constraint (fun m => True))). + revert HtrX; apply VLSM_incl_finite_valid_trace. + apply pre_loaded_with_all_messages_vlsm_is_pre_loaded_with_True_l. +Qed. + End sub_composition_element. Section sub_composition_preloaded_lift. @@ -1898,12 +1971,27 @@ Definition update_IM for fixed-set equivocation model, similar to the one for byzantine traces. *) +Definition update_IM_id_same_IM + : forall i, update_IM (fun sub_i => IM (` sub_i)) i = IM i. +Proof. + intro; unfold update_IM; case_decide; reflexivity. +Defined. + Context (replacement_IM : sub_index selection -> VLSM message) (updated_IM := update_IM replacement_IM) (selection_complement : set index := set_diff (enum index) selection) . +Lemma selection_complement_index_not_in_selection + (sub_i : sub_index selection_complement) + : ~ (`sub_i ∈ selection). +Proof. + destruct_dec_sig sub_i i Hi Heqsub_i; subst; cbn in *. + eapply set_diff_elim2; eassumption. +Qed. + + Global Instance update_IM_complement_Hbs `{forall i : index, HasBeenSentCapability (IM i)} : forall sub_i : sub_index selection_complement, diff --git a/theories/VLSM/Core/VLSM.v b/theories/VLSM/Core/VLSM.v index dc3013ff..f0f8477f 100644 --- a/theories/VLSM/Core/VLSM.v +++ b/theories/VLSM/Core/VLSM.v @@ -2766,6 +2766,30 @@ Context (Heq : X1 = X2) . +Lemma same_VLSM_label_rew_12 (l1 : vlabel X1) + : same_VLSM_label_rew (eq_sym Heq) (same_VLSM_label_rew Heq l1) = l1. +Proof. + subst; reflexivity. +Qed. + +Lemma same_VLSM_label_rew_21 (l2 : vlabel X2) + : same_VLSM_label_rew Heq (same_VLSM_label_rew (eq_sym Heq) l2) = l2. +Proof. + subst; reflexivity. +Qed. + +Lemma same_VLSM_state_rew_12 (s1 : vstate X1) + : same_VLSM_state_rew (eq_sym Heq) (same_VLSM_state_rew Heq s1) = s1. +Proof. + subst; reflexivity. +Qed. + +Lemma same_VLSM_state_rew_21 (s2 : vstate X2) + : same_VLSM_state_rew Heq (same_VLSM_state_rew (eq_sym Heq) s2) = s2. +Proof. + subst; reflexivity. +Qed. + Lemma same_VLSM_valid_preservation l1 s1 om : vvalid X1 l1 (s1, om) -> vvalid X2 (same_VLSM_label_rew Heq l1) (same_VLSM_state_rew Heq s1, om). diff --git a/theories/VLSM/Core/VLSMProjections.v b/theories/VLSM/Core/VLSMProjections.v index 5550bb30..9831e4d5 100644 --- a/theories/VLSM/Core/VLSMProjections.v +++ b/theories/VLSM/Core/VLSMProjections.v @@ -1,10 +1,12 @@ From Cdcl Require Import Itauto. Local Tactic Notation "itauto" := itauto auto. From stdpp Require Import prelude. +From Coq Require Import FunctionalExtensionality. From VLSM.Lib Require Import Preamble ListExtras StreamExtras StreamFilters. From VLSM.Core Require Import VLSM. From VLSM.Core.VLSMProjections Require Export VLSMPartialProjection VLSMTotalProjection. From VLSM.Core.VLSMProjections Require Export VLSMEmbedding VLSMInclusion VLSMEquality. + Section same_VLSM_full_projection. Context @@ -23,4 +25,70 @@ Proof. - by apply same_VLSM_initial_message_preservation. Qed. +Lemma same_VLSM_preloaded_full_projection + : VLSM_full_projection + (pre_loaded_with_all_messages_vlsm X1) (pre_loaded_with_all_messages_vlsm X2) + (same_VLSM_label_rew Heq) (same_VLSM_state_rew Heq). +Proof. + apply basic_VLSM_strong_full_projection. + - cbv; apply same_VLSM_valid_preservation. + - cbv; apply same_VLSM_transition_preservation. + - cbv; apply same_VLSM_initial_state_preservation. + - cbv; trivial. +Qed. + End same_VLSM_full_projection. + +Section VLSM_projection_composition. + +Context + {message} + [X Y Z : VLSM message] + `(HXY : VLSM_projection X Y xy_label xy_state) + `(HYZ : VLSM_projection Y Z yz_label yz_state) + . + +Lemma pre_VLSM_projection_composition_transition_item_project + : pre_VLSM_projection_transition_item_project (type X) (type Z) + (mbind yz_label ∘ xy_label) (yz_state ∘ xy_state) + = + mbind (pre_VLSM_projection_transition_item_project (type Y) (type Z) yz_label yz_state) + ∘ (pre_VLSM_projection_transition_item_project (type X) (type Y) xy_label xy_state). +Proof. + extensionality item; destruct item; cbn. + unfold pre_VLSM_projection_transition_item_project; cbn. + destruct (xy_label l) as [lY|]; reflexivity. +Qed. + +Lemma pre_VLSM_projection_composition_finite_trace_project + : pre_VLSM_projection_finite_trace_project (type X) (type Z) + (mbind yz_label ∘ xy_label) (yz_state ∘ xy_state) + = + pre_VLSM_projection_finite_trace_project (type Y) (type Z) yz_label yz_state + ∘ pre_VLSM_projection_finite_trace_project (type X) (type Y) xy_label xy_state. +Proof. + unfold pre_VLSM_projection_finite_trace_project. + setoid_rewrite pre_VLSM_projection_composition_transition_item_project. + setoid_rewrite map_option_comp_bind. + reflexivity. +Qed. + +Lemma VLSM_projection_composition + : VLSM_projection X Z (mbind yz_label ∘ xy_label) (yz_state ∘ xy_state). +Proof. + constructor; [constructor|]; intros sX trX HtrX + ; replace (pre_VLSM_projection_finite_trace_project _ _ _ _) + with + ((pre_VLSM_projection_finite_trace_project (type Y) (type Z) yz_label yz_state + ∘ pre_VLSM_projection_finite_trace_project (type X) (type Y) xy_label xy_state)) + by (symmetry; apply pre_VLSM_projection_composition_finite_trace_project). + - unfold compose. + erewrite final_state_project; [|eapply projection_type; eassumption|assumption]. + eapply final_state_project; [apply projection_type; assumption|]. + apply VLSM_projection_finite_valid_trace_from with (Hsimul := HXY); assumption. + - apply VLSM_projection_finite_valid_trace with (Hsimul := HYZ), + VLSM_projection_finite_valid_trace with (Hsimul := HXY). + assumption. +Qed. + +End VLSM_projection_composition. \ No newline at end of file diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v index 8a593f46..38e31b0e 100644 --- a/theories/VLSM/Lib/ListExtras.v +++ b/theories/VLSM/Lib/ListExtras.v @@ -1,10 +1,20 @@ From Cdcl Require Import Itauto. Local Tactic Notation "itauto" := itauto auto. From stdpp Require Import prelude finite. -From Coq Require Import FinFun. +From Coq Require Import FinFun FunctionalExtensionality. From VLSM Require Import Lib.Preamble. (** * Utility lemmas about lists *) +Lemma map_comp + [A B C : Type] + (f : A -> B) + (g : B -> C) + : map (g ∘ f) = map g ∘ map f. +Proof. + extensionality l. + induction l; cbn; rewrite ?IHl; reflexivity. +Qed. + (** A list is empty if it has no members *) Lemma empty_nil [X:Type] (l:list X) : (forall v, ~In v l) -> l = []. @@ -1090,6 +1100,38 @@ Definition map_option ) []. +Lemma map_option_comp_r + [A B C : Type] (f : A -> B) (g : B -> option C) : + map_option (g ∘ f) = map_option g ∘ map f. +Proof. + extensionality l. + induction l; cbn; rewrite ?IHl; reflexivity. +Qed. + +Lemma map_option_comp_l + [A B C : Type] + (f : A -> option B) + (g : B -> C) + : map_option (option_map g ∘ f) = map g ∘ map_option f. +Proof. + extensionality l. + induction l; [reflexivity|]. + cbn. + rewrite IHl. + destruct (f a) as [b|]; reflexivity. +Qed. + +Lemma map_option_comp_bind + [A B C : Type] + (f : A -> option B) + (g : B -> option C) + : map_option (mbind g ∘ f) = map_option g ∘ map_option f. +Proof. + extensionality l. + induction l; [reflexivity|]; cbn; rewrite IHl. + destruct (f a) as [b|]; reflexivity. +Qed. + Lemma map_option_app {A B : Type} (f : A -> option B) diff --git a/theories/VLSM/Lib/Preamble.v b/theories/VLSM/Lib/Preamble.v index e4ab3059..249f2e24 100644 --- a/theories/VLSM/Lib/Preamble.v +++ b/theories/VLSM/Lib/Preamble.v @@ -167,6 +167,8 @@ Proof. - right. intro contra. elim n. revert contra. apply dsig_eq. Qed. +Arguments dec_sig_sigT_eq_rev {_ _ _ _} _. + Lemma ex_out (A : Type) (P : Prop) (Q : A -> Prop): (exists x, P /\ Q x) <-> (P /\ exists x, Q x). Proof. firstorder. Qed.