From abfe1f76492d3a1b73f4c93898a858ecf213ced2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20Ko=C5=82owski?= Date: Wed, 13 Dec 2023 13:59:51 +0100 Subject: [PATCH 1/4] Define input_constrained_transition_to and use it instead of input_valid_transition_to of preloaded (#369) --- theories/Core/Equivocators/FixedEquivocationSimulation.v | 4 ++-- theories/Core/PreloadedVLSM.v | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/theories/Core/Equivocators/FixedEquivocationSimulation.v b/theories/Core/Equivocators/FixedEquivocationSimulation.v index 9fa95629..21ed9d99 100644 --- a/theories/Core/Equivocators/FixedEquivocationSimulation.v +++ b/theories/Core/Equivocators/FixedEquivocationSimulation.v @@ -311,8 +311,8 @@ Proof. apply proj1 in Him_etr. replace (im_ert' ++ [item]) with (im_ert' ++ [item] ++ []) in Him_etr by (rewrite app_assoc; apply app_nil_r). - specialize (input_valid_transition_to (pre_loaded_with_all_messages_vlsm - (free_composite_vlsm (equivocator_IM (sub_IM IM (elements equivocating))))) + specialize (input_constrained_transition_to + (free_composite_vlsm (equivocator_IM (sub_IM IM (elements equivocating)))) _ _ _ _ _ Him_etr eq_refl) as Ht. rewrite finite_trace_last_is_last. diff --git a/theories/Core/PreloadedVLSM.v b/theories/Core/PreloadedVLSM.v index 8edac183..e9a40d9b 100644 --- a/theories/Core/PreloadedVLSM.v +++ b/theories/Core/PreloadedVLSM.v @@ -558,6 +558,9 @@ Definition input_constrained := Definition input_constrained_transition := input_valid_transition (pre_loaded_with_all_messages_vlsm X). +Definition input_constrained_transition_to := + input_valid_transition_to (pre_loaded_with_all_messages_vlsm X). + Definition input_constrained_transition_item := input_valid_transition_item (pre_loaded_with_all_messages_vlsm X). From d3fa6331da76adca3f85d107d7ecf56bea2a7154 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20Ko=C5=82owski?= Date: Wed, 13 Dec 2023 14:00:45 +0100 Subject: [PATCH 2/4] Define finite_constrained_trace and use it instead of finite_valid_trace of preloaded (#370) --- theories/Core/Equivocation.v | 2 +- theories/Core/Equivocation/NoEquivocation.v | 2 +- .../Core/Equivocation/WitnessedEquivocation.v | 2 +- .../EquivocatorsCompositionProjections.v | 4 ++-- .../Core/Equivocators/FixedEquivocation.v | 20 ++++++++++--------- .../Equivocators/LimitedStateEquivocation.v | 2 +- theories/Core/PreloadedVLSM.v | 3 +++ 7 files changed, 20 insertions(+), 15 deletions(-) diff --git a/theories/Core/Equivocation.v b/theories/Core/Equivocation.v index c2b68b3c..51a2202c 100644 --- a/theories/Core/Equivocation.v +++ b/theories/Core/Equivocation.v @@ -2716,7 +2716,7 @@ Lemma lift_preloaded_trace_to_seeded (tr : list transition_item) (Htrm : trace_received_not_sent_before_or_after_invariant tr P) (is : state (PreX)) - (Htr : finite_valid_trace PreX is tr) + (Htr : finite_constrained_trace X is tr) : finite_valid_trace (pre_loaded_vlsm X P) is tr. Proof. unfold trace_received_not_sent_before_or_after_invariant in Htrm. diff --git a/theories/Core/Equivocation/NoEquivocation.v b/theories/Core/Equivocation/NoEquivocation.v index 0738327b..6b555e76 100644 --- a/theories/Core/Equivocation/NoEquivocation.v +++ b/theories/Core/Equivocation/NoEquivocation.v @@ -108,7 +108,7 @@ Qed. *) Lemma no_equivocations_preloaded_traces : forall (is : state (pre_loaded_with_all_messages_vlsm X)) (tr : list transition_item), - finite_valid_trace (pre_loaded_with_all_messages_vlsm X) is tr -> finite_valid_trace X is tr. + finite_constrained_trace X is tr -> finite_valid_trace X is tr. Proof. intros is tr Htr. induction Htr using finite_valid_trace_rev_ind; diff --git a/theories/Core/Equivocation/WitnessedEquivocation.v b/theories/Core/Equivocation/WitnessedEquivocation.v index 97fea96d..16a84033 100644 --- a/theories/Core/Equivocation/WitnessedEquivocation.v +++ b/theories/Core/Equivocation/WitnessedEquivocation.v @@ -489,7 +489,7 @@ Proof. forall is tr, m = set_size (equivocating_validators (finite_trace_last is tr)) -> n = length tr -> - finite_valid_trace PreFree is tr -> + finite_constrained_trace Free is tr -> trace_witnessing_equivocation_prop is tr -> let s := finite_trace_last is tr in exists (is' : state PreFree) (tr' : list transition_item), diff --git a/theories/Core/Equivocators/EquivocatorsCompositionProjections.v b/theories/Core/Equivocators/EquivocatorsCompositionProjections.v index ab061d86..96fffa9a 100644 --- a/theories/Core/Equivocators/EquivocatorsCompositionProjections.v +++ b/theories/Core/Equivocators/EquivocatorsCompositionProjections.v @@ -1007,7 +1007,7 @@ Lemma preloaded_equivocators_valid_trace_project_inv (is : composite_state (equivocator_IM IM)) (tr : list (composite_transition_item (equivocator_IM IM))) (final_state := finite_trace_last is tr) - (Htr : finite_valid_trace PreFreeE is tr) + (Htr : finite_constrained_trace FreeE is tr) (trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM) (Hproject : equivocators_trace_project final_descriptors tr = Some (trX, initial_descriptors)) @@ -2125,7 +2125,7 @@ Proof. apply VLSM_incl_finite_valid_trace_from; [| done]. by apply constrained_preloaded_incl. - intros * Htr. - assert (Hpre_tr : finite_valid_trace PreFreeE sX trX). + assert (Hpre_tr : finite_constrained_trace FreeE sX trX). { apply VLSM_incl_finite_valid_trace; [| done]. by apply constrained_preloaded_incl. diff --git a/theories/Core/Equivocators/FixedEquivocation.v b/theories/Core/Equivocators/FixedEquivocation.v index f75cbf99..f5c2eb91 100644 --- a/theories/Core/Equivocators/FixedEquivocation.v +++ b/theories/Core/Equivocators/FixedEquivocation.v @@ -490,7 +490,7 @@ Proof. by apply equivocators_fixed_equivocations_vlsm_incl_free. } assert - (Htr'pre : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) is tr'). + (Htr'pre : finite_constrained_trace FreeE is tr'). { split; [| done]. specialize (vlsm_incl_pre_loaded_with_all_messages_vlsm FreeE) as Hincl. @@ -570,7 +570,7 @@ Proof. by (apply finite_valid_trace_last_pstate, Htr'pre). apply proper_sent; [done |]. apply has_been_sent_consistency; [typeclasses eauto | done |]. - by exists is, tr', (valid_trace_add_default_last Htr'pre). + by red in Htr'pre; exists is, tr', (valid_trace_add_default_last Htr'pre). + exists trX'. exists initial_descriptors. subst foldx. split; [done |]. split; [by apply Htr_project |]. split; [| done]. @@ -628,14 +628,14 @@ Proof. subst lst. rewrite Hfinal_state. - assert (Htr_Pre : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) is tr). + assert (Htr_Pre : finite_constrained_trace FreeE is tr). { apply VLSM_incl_finite_valid_trace; [| done]. by apply constrained_preloaded_incl. } - assert (HtrX_Pre : finite_valid_trace (pre_loaded_with_all_messages_vlsm Free) - (equivocators_state_project IM initial_descriptors is) trX). + assert (HtrX_Pre : finite_constrained_trace Free + (equivocators_state_project IM initial_descriptors is) trX). { revert HtrX_Free; apply VLSM_incl_finite_valid_trace. by apply vlsm_incl_pre_loaded_with_all_messages_vlsm. @@ -650,6 +650,7 @@ Proof. rewrite (has_been_directly_observed_sent_received_iff Free) by done. right. apply proper_sent; [done |]. apply has_been_sent_consistency; [by typeclasses eauto | done |]. + red in HtrX_Pre. exists (equivocators_state_project IM initial_descriptors is), trX, (valid_trace_add_default_last HtrX_Pre). @@ -752,7 +753,7 @@ Proof. intros pre item suf m Heq Hm Hitem. destruct (free_equivocators_valid_trace_project descriptors is tr Hproper Htr) as [trX [initial_descriptors [Hinitial_descriptors [Htr_project [Hfinal_state HtrXFree]]]]]. - assert (HtrXPre : finite_valid_trace (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) + assert (HtrXPre : finite_constrained_trace (free_composite_vlsm IM) (equivocators_state_project IM initial_descriptors is) trX). { revert HtrXFree; apply VLSM_incl_finite_valid_trace. @@ -763,7 +764,7 @@ Proof. subst lst_trX s; cbn in Hfinal_state |- *; rewrite Hfinal_state. by apply finite_valid_trace_last_pstate, HtrXPre. } - assert (Htr_free : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) is tr). + assert (Htr_free : finite_constrained_trace FreeE is tr). { apply VLSM_incl_finite_valid_trace; [| done]. by apply constrained_preloaded_incl. @@ -968,7 +969,7 @@ Proof. elim Hno. clear Hno. apply composite_has_been_directly_observed_sent_received_iff. left. - assert (HtrX_free : finite_valid_trace (pre_loaded_with_all_messages_vlsm Free) + assert (HtrX_free : finite_constrained_trace Free (equivocators_state_project IM initial_descriptors is) trX). { revert HtrX; apply VLSM_incl_finite_valid_trace. @@ -980,6 +981,7 @@ Proof. rewrite Hlast_state. apply (composite_proper_sent IM); [done |]. apply has_been_sent_consistency; [by typeclasses eauto | done |]. + red in HtrX_free. exists (equivocators_state_project IM initial_descriptors is), trX, (valid_trace_add_default_last HtrX_free). clear HtrX HtrX_free Hfree_lst. @@ -1300,7 +1302,7 @@ Proof. - apply PreFreeE_Free_vlsm_projection_type. apply VLSM_incl_finite_valid_trace_from; [| done]. by apply equivocators_fixed_equivocations_vlsm_incl_PreFree. - - assert (Hpre_tr : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) sX trX). + - assert (Hpre_tr : finite_constrained_trace FreeE sX trX). { apply VLSM_incl_finite_valid_trace; [| done]. by apply equivocators_fixed_equivocations_vlsm_incl_PreFree. diff --git a/theories/Core/Equivocators/LimitedStateEquivocation.v b/theories/Core/Equivocators/LimitedStateEquivocation.v index 6072dddc..47f09972 100644 --- a/theories/Core/Equivocators/LimitedStateEquivocation.v +++ b/theories/Core/Equivocators/LimitedStateEquivocation.v @@ -368,7 +368,7 @@ Proof. revert HtrX. apply VLSM_incl_finite_valid_trace_from. by apply constrained_preloaded_incl. - intro HtrX. - assert (Hpre_tr : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) sX trX). + assert (Hpre_tr : finite_constrained_trace FreeE sX trX). { apply VLSM_incl_finite_valid_trace; [| done]. by apply constrained_preloaded_incl. diff --git a/theories/Core/PreloadedVLSM.v b/theories/Core/PreloadedVLSM.v index e9a40d9b..96c980a5 100644 --- a/theories/Core/PreloadedVLSM.v +++ b/theories/Core/PreloadedVLSM.v @@ -573,6 +573,9 @@ Definition finite_constrained_trace_from := Definition finite_constrained_trace_init_to := finite_valid_trace_init_to (pre_loaded_with_all_messages_vlsm X). +Definition finite_constrained_trace := + finite_valid_trace (pre_loaded_with_all_messages_vlsm X). + Definition constrained_state_prop := valid_state_prop (pre_loaded_with_all_messages_vlsm X). From b93f499428a16a22865e8c1627036216f595e919 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20Ko=C5=82owski?= Date: Wed, 13 Dec 2023 14:48:42 +0100 Subject: [PATCH 3/4] Define constrained_trace_prop (#371) --- theories/Core/ByzantineTraces.v | 2 +- theories/Core/PreloadedVLSM.v | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/theories/Core/ByzantineTraces.v b/theories/Core/ByzantineTraces.v index cb55f6ee..b4e9258d 100644 --- a/theories/Core/ByzantineTraces.v +++ b/theories/Core/ByzantineTraces.v @@ -52,7 +52,7 @@ Definition byzantine_trace_prop (tr : Trace M) : Prop := Lemma byzantine_pre_loaded_with_all_messages : forall (tr : Trace M), byzantine_trace_prop tr -> - valid_trace_prop (pre_loaded_with_all_messages_vlsm M) tr. + constrained_trace_prop M tr. Proof. intros tr [M' Htr]; cbn in Htr. by apply proj_pre_loaded_with_all_messages_incl in Htr. diff --git a/theories/Core/PreloadedVLSM.v b/theories/Core/PreloadedVLSM.v index 96c980a5..93eed555 100644 --- a/theories/Core/PreloadedVLSM.v +++ b/theories/Core/PreloadedVLSM.v @@ -576,6 +576,12 @@ Definition finite_constrained_trace_init_to := Definition finite_constrained_trace := finite_valid_trace (pre_loaded_with_all_messages_vlsm X). +Definition constrained_trace_from_prop := + valid_trace_from_prop (pre_loaded_with_all_messages_vlsm X). + +Definition constrained_trace_prop := + valid_trace_prop (pre_loaded_with_all_messages_vlsm X). + Definition constrained_state_prop := valid_state_prop (pre_loaded_with_all_messages_vlsm X). From 4da39badf0053fbb0e1da3a093c1384029564c6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20Ko=C5=82owski?= Date: Wed, 13 Dec 2023 16:51:28 +0100 Subject: [PATCH 4/4] Cleanup the use of pre_loaded_with_all_messages_vlsm (#372) --- theories/Core/ByzantineTraces.v | 25 +++++++--------- theories/Core/Composition.v | 9 ++++-- theories/Core/Equivocation.v | 15 ++++------ .../Core/Equivocation/FixedSetEquivocation.v | 3 -- .../Equivocation/LimitedMessageEquivocation.v | 1 - .../Core/Equivocation/TraceWiseEquivocation.v | 5 ++-- theories/Core/EquivocationProjections.v | 6 ++-- .../FixedEquivocationSimulation.v | 2 -- theories/Core/Equivocators/FullReplayTraces.v | 10 +++---- .../Equivocators/LimitedStateEquivocation.v | 7 +++-- theories/Core/Equivocators/SimulatingFree.v | 4 +-- theories/Core/MessageDependencies.v | 12 ++++---- theories/Core/ProjectionTraces.v | 4 +-- theories/Core/SubProjectionTraces.v | 1 - theories/Core/VLSM.v | 4 +-- theories/Core/Validator.v | 30 ++++++++----------- .../Examples/Tutorial/PrimesComposition.v | 4 +-- 17 files changed, 60 insertions(+), 82 deletions(-) diff --git a/theories/Core/ByzantineTraces.v b/theories/Core/ByzantineTraces.v index b4e9258d..70c803ff 100644 --- a/theories/Core/ByzantineTraces.v +++ b/theories/Core/ByzantineTraces.v @@ -149,13 +149,11 @@ Qed. Section sec_pre_loaded_with_all_messages_byzantine_alt. (** - Let <> denote the [pre_loaded_with_all_messages_vlsm] of <>, - let <> denote the free composition of <> with the [emit_any_message_vlsm], + Let <> denote the free composition of <> with the [emit_any_message_vlsm], and let <> denote the projection of <> to the component of <>. *) Context - (PreLoaded := pre_loaded_with_all_messages_vlsm M) (Alt1 := binary_free_composition_fst M emit_any_message_vlsm) (Alt := binary_free_composition M emit_any_message_vlsm) . @@ -165,13 +163,13 @@ Context of <> into <>. *) Lemma alt_pre_loaded_with_all_messages_incl : - VLSM_incl Alt1 PreLoaded. + VLSM_incl Alt1 (pre_loaded_with_all_messages_vlsm M). Proof. by intros t Hvt; apply byzantine_pre_loaded_with_all_messages, byzantine_alt_byzantine. Qed. (** - To prove the reverse inclusion (between <> and <>) we will use the + To prove the reverse inclusion (between preloaded <> and <>) we will use the [basic_VLSM_incl] meta-result about proving inclusions between VLSMs which states that: @@ -212,9 +210,9 @@ Proof. by apply any_message_is_valid_in_preloaded. Qed. Definition lifted_alt_state (s : state M) : state Alt := lift_to_composite_state' (binary_IM M emit_any_message_vlsm) first s. -(** Lifting a valid state of <> we obtain a valid state of <>. *) +(** Lifting a constrained state of <> we obtain a valid state of <>. *) Lemma preloaded_alt_valid_state : - forall (sj : state PreLoaded) (om : option message), + forall (sj : state M) (om : option message), constrained_state_message_prop M sj om -> valid_state_prop Alt (lifted_alt_state sj). Proof. @@ -238,9 +236,9 @@ Qed. results above to show that <> is included in <>. *) Lemma pre_loaded_with_all_messages_alt_incl : - VLSM_incl PreLoaded Alt1. + VLSM_incl (pre_loaded_with_all_messages_vlsm M) Alt1. Proof. - apply (basic_VLSM_incl PreLoaded Alt1); intro; intros; + apply (basic_VLSM_incl _ Alt1); intro; intros; [done | by apply alt_proj_option_valid_message | | by apply H]. exists (lifted_alt_state s). split; [done |]. @@ -252,7 +250,7 @@ Qed. (** Hence, <> and <> are actually trace-equivalent. *) Lemma pre_loaded_with_all_messages_alt_eq : - VLSM_eq PreLoaded Alt1. + VLSM_eq (pre_loaded_with_all_messages_vlsm M) Alt1. Proof. split. - by apply pre_loaded_with_all_messages_alt_incl. @@ -331,17 +329,16 @@ Context (IM : index -> VLSM message) (constraint : composite_label IM -> composite_state IM * option message -> Prop) (X := composite_vlsm IM constraint) - (PreLoadedX := pre_loaded_with_all_messages_vlsm X) (Hvalidator : forall i : index, component_message_validator_prop IM constraint i) . (** - Since we know that <> contains precisely the byzantine traces - of <>, we just need to show that <> is included in <> to + Since we know that preloaded <> contains precisely the byzantine traces + of <>, we just need to show that preloaded <> is included in <> to prove our main result. *) Lemma validator_pre_loaded_with_all_messages_incl : - VLSM_incl PreLoadedX X. + VLSM_incl (pre_loaded_with_all_messages_vlsm X) X. Proof. apply VLSM_incl_finite_traces_characterization. intros s tr Htr. diff --git a/theories/Core/Composition.v b/theories/Core/Composition.v index 997f1082..1f9092e9 100644 --- a/theories/Core/Composition.v +++ b/theories/Core/Composition.v @@ -1333,7 +1333,6 @@ Context `{EqDecision index} (IM : index -> VLSM message) (Free := free_composite_vlsm IM) - (RFree := pre_loaded_with_all_messages_vlsm Free) . Definition composite_valid_transition l s1 iom s2 oom : Prop := @@ -1344,7 +1343,9 @@ Definition composite_valid_transition_item composite_valid_transition (l item) s (input item) (destination item) (output item). Lemma composite_valid_transition_reachable_iff l s1 iom s2 oom : - composite_valid_transition l s1 iom s2 oom <-> valid_transition RFree l s1 iom s2 oom. + composite_valid_transition l s1 iom s2 oom + <-> + valid_transition (pre_loaded_with_all_messages_vlsm Free) l s1 iom s2 oom. Proof. by split; intros []; constructor. Qed. @@ -1356,7 +1357,9 @@ Definition composite_valid_transition_future : relation (composite_state IM) := tc composite_valid_transition_next. Lemma composite_valid_transition_next_reachable_iff s1 s2 : - composite_valid_transition_next s1 s2 <-> valid_transition_next RFree s1 s2. + composite_valid_transition_next s1 s2 + <-> + valid_transition_next (pre_loaded_with_all_messages_vlsm Free) s1 s2. Proof. by split; intros []; econstructor; apply composite_valid_transition_reachable_iff. Qed. diff --git a/theories/Core/Equivocation.v b/theories/Core/Equivocation.v index 51a2202c..da1b3c38 100644 --- a/theories/Core/Equivocation.v +++ b/theories/Core/Equivocation.v @@ -1029,7 +1029,6 @@ Proof. intros l s im s' om Htrans msg. rename Htrans into Htrans'. pose proof Htrans' as [[Hproto_s [Hproto_m Hvalid]] Htrans]. - set (preloaded := pre_loaded_with_all_messages_vlsm vlsm) in * |- *. pose proof (valid_state_has_trace _ _ Hproto_s) as [is [tr [Htr Hinit]]]. pose proof (Htr' := extend_right_finite_trace_from_to _ Htr Htrans'). @@ -2615,7 +2614,6 @@ Context {message : Type} `{EqDecision message} (X : VLSM message) - (PreX := pre_loaded_with_all_messages_vlsm X) `{HasBeenSentCapability message X} `{HasBeenReceivedCapability message X} . @@ -2625,7 +2623,7 @@ Definition state_received_not_sent (s : state X) (m : message) : Prop := Lemma state_received_not_sent_trace_iff (m : message) - (s is : state (PreX)) + (s is : state (pre_loaded_with_all_messages_vlsm X)) (tr : list transition_item) (Htr : finite_constrained_trace_init_to X is s tr) : state_received_not_sent s m <-> trace_received_not_sent_before_or_after tr m. @@ -2654,7 +2652,7 @@ Definition state_received_not_sent_invariant Lemma state_received_not_sent_invariant_trace_iff (P : message -> Prop) - (s is : state (PreX)) + (s is : state (pre_loaded_with_all_messages_vlsm X)) (tr : list transition_item) (Htr : finite_constrained_trace_init_to X is s tr) : state_received_not_sent_invariant s P <-> @@ -2673,8 +2671,8 @@ Definition cannot_resend_message_stepwise_prop : Prop := Lemma cannot_resend_received_message_in_future (Hno_resend : cannot_resend_message_stepwise_prop) - (s1 s2 : state (PreX)) - (Hfuture : in_futures PreX s1 s2) + (s1 s2 : state (pre_loaded_with_all_messages_vlsm X)) + (Hfuture : in_futures (pre_loaded_with_all_messages_vlsm X) s1 s2) : forall m : message, state_received_not_sent s1 m -> state_received_not_sent s2 m. Proof. @@ -2715,7 +2713,7 @@ Lemma lift_preloaded_trace_to_seeded (P : message -> Prop) (tr : list transition_item) (Htrm : trace_received_not_sent_before_or_after_invariant tr P) - (is : state (PreX)) + (is : state (pre_loaded_with_all_messages_vlsm X)) (Htr : finite_constrained_trace X is tr) : finite_valid_trace (pre_loaded_vlsm X P) is tr. Proof. @@ -2788,7 +2786,7 @@ Lemma lift_generated_to_seeded (s : state X) (Hequiv_s : state_received_not_sent_invariant s P) (m : message) - (Hgen : can_produce PreX s m) + (Hgen : can_produce (pre_loaded_with_all_messages_vlsm X) s m) : can_produce (pre_loaded_vlsm X P) s m. Proof. apply non_empty_valid_trace_from_can_produce. @@ -2843,7 +2841,6 @@ Context `{forall i : index, (HasBeenReceivedCapability (IM i))} (constraint : composite_label IM -> composite_state IM * option message -> Prop) (X := composite_vlsm IM constraint) - (PreX := pre_loaded_with_all_messages_vlsm X) (Y := free_composite_vlsm IM) (PreY := pre_loaded_with_all_messages_vlsm Y). diff --git a/theories/Core/Equivocation/FixedSetEquivocation.v b/theories/Core/Equivocation/FixedSetEquivocation.v index aad2c8df..a1112db8 100644 --- a/theories/Core/Equivocation/FixedSetEquivocation.v +++ b/theories/Core/Equivocation/FixedSetEquivocation.v @@ -650,7 +650,6 @@ Context (Fixed := fixed_equivocation_vlsm_composition IM equivocators) (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators) (Free := free_composite_vlsm IM) - (PreFree := pre_loaded_with_all_messages_vlsm Free) . (** @@ -741,7 +740,6 @@ Context (Free := free_composite_vlsm IM) (Fixed := fixed_equivocation_vlsm_composition IM equivocators) (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators) - (PreFree := pre_loaded_with_all_messages_vlsm Free) . (** @@ -1041,7 +1039,6 @@ Context (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators) (StrongFixedNonEquivocating := pre_induced_sub_projection IM (elements non_equivocators) (strong_fixed_equivocation_constraint IM equivocators)) - (PreFree := pre_loaded_with_all_messages_vlsm Free) . (** diff --git a/theories/Core/Equivocation/LimitedMessageEquivocation.v b/theories/Core/Equivocation/LimitedMessageEquivocation.v index 0a22e316..fd2a4d1d 100644 --- a/theories/Core/Equivocation/LimitedMessageEquivocation.v +++ b/theories/Core/Equivocation/LimitedMessageEquivocation.v @@ -199,7 +199,6 @@ Context `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)} (Fixed := fixed_equivocation_vlsm_composition IM equivocators) (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators) - (PreFree := pre_loaded_with_all_messages_vlsm Free) (Limited : VLSM message := tracewise_limited_equivocation_vlsm_composition (Cv := Cv) IM threshold A sender) (HBE : BasicEquivocation (composite_state IM) validator Cv threshold := equivocation_dec_tracewise IM threshold A sender) diff --git a/theories/Core/Equivocation/TraceWiseEquivocation.v b/theories/Core/Equivocation/TraceWiseEquivocation.v index dc170968..f991f198 100644 --- a/theories/Core/Equivocation/TraceWiseEquivocation.v +++ b/theories/Core/Equivocation/TraceWiseEquivocation.v @@ -32,7 +32,6 @@ Context `{finite.Finite validator} (A : validator -> index) (sender : message -> option validator) - (PreFree := pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) . (** @@ -96,7 +95,7 @@ Lemma elem_of_equivocating_senders_in_trace : v ∈ equivocating_senders_in_trace tr <-> exists (m : message), (sender m = Some v) /\ - equivocation_in_trace PreFree m tr. + equivocation_in_trace (free_composite_vlsm IM) m tr. Proof. unfold equivocating_senders_in_trace. rewrite elem_of_remove_dups, elem_of_list_omap. @@ -170,7 +169,7 @@ Definition is_equivocating_tracewise_no_has_been_sent (Htr : finite_constrained_trace_init_to (free_composite_vlsm IM) is s tr), exists (m : message), (sender m = Some v) /\ - equivocation_in_trace PreFree m tr. + equivocation_in_trace (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) m tr. Lemma is_equivocating_tracewise_no_has_been_sent_equivocating_senders_in_trace (s : composite_state IM) diff --git a/theories/Core/EquivocationProjections.v b/theories/Core/EquivocationProjections.v index ac3c7d6a..f8bf3364 100644 --- a/theories/Core/EquivocationProjections.v +++ b/theories/Core/EquivocationProjections.v @@ -423,7 +423,6 @@ Context (A : validator -> index) (sender : message -> option validator) (Hsender_safety : sender_safety_alt_prop IM A sender) - (PreFree := pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) (j : index) (m : message) (Hj : option_map A (sender m) = Some j) @@ -434,8 +433,9 @@ Context by the free composition (pre-loaded with all messages), then it can also be emitted by the component corresponding to its sender (pre-loaded with all messages). *) -Lemma can_emit_projection - : can_emit PreFree m -> can_emit (pre_loaded_with_all_messages_vlsm (IM j)) m. +Lemma can_emit_projection : + can_emit (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) m -> + can_emit (pre_loaded_with_all_messages_vlsm (IM j)) m. Proof. destruct (sender m) as [v |] eqn: Hsender; simpl in Hj; [| by congruence]. apply Some_inj in Hj. diff --git a/theories/Core/Equivocators/FixedEquivocationSimulation.v b/theories/Core/Equivocators/FixedEquivocationSimulation.v index 21ed9d99..7c6b6a32 100644 --- a/theories/Core/Equivocators/FixedEquivocationSimulation.v +++ b/theories/Core/Equivocators/FixedEquivocationSimulation.v @@ -40,7 +40,6 @@ Context (X : VLSM message := strong_fixed_equivocation_vlsm_composition IM equivocating) (XE : VLSM message := equivocators_fixed_equivocations_vlsm IM (elements equivocating)) (FreeE := free_composite_vlsm (equivocator_IM IM)) - (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE) (SubFreeE := free_composite_vlsm (sub_IM (equivocator_IM IM) (elements equivocating))) (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM) . @@ -393,7 +392,6 @@ Context (X : VLSM message := composite_vlsm IM (composite_no_equivocations IM)) (XE : VLSM message := equivocators_fixed_equivocations_vlsm IM []) (FreeE := free_composite_vlsm (equivocator_IM IM)) - (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE) . Lemma no_equivocating_equivocators_finite_valid_trace_init_to_rev diff --git a/theories/Core/Equivocators/FullReplayTraces.v b/theories/Core/Equivocators/FullReplayTraces.v index 6581e8b3..f9b42780 100644 --- a/theories/Core/Equivocators/FullReplayTraces.v +++ b/theories/Core/Equivocators/FullReplayTraces.v @@ -32,9 +32,7 @@ Context (equivocating : list index) (Free := free_composite_vlsm IM) (FreeE := free_composite_vlsm (equivocator_IM IM)) - (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE) (FreeSubE := free_composite_vlsm (sub_IM (equivocator_IM IM) equivocating)) - (PreFreeSubE := pre_loaded_with_all_messages_vlsm FreeSubE) (SeededXE : VLSM message := seeded_equivocators_no_equivocation_vlsm IM equivocating seed) . @@ -564,7 +562,7 @@ End sec_pre_loaded_constrained_projection. Lemma SeededXE_PreFreeE_weak_embedding (full_replay_state : composite_state (equivocator_IM IM)) (Hfull_replay_state : constrained_state_prop FreeE full_replay_state) - : VLSM_weak_embedding SeededXE PreFreeE + : VLSM_weak_embedding SeededXE (pre_loaded_with_all_messages_vlsm FreeE) (lift_equivocators_sub_label_to full_replay_state) (lift_equivocators_sub_state_to full_replay_state). Proof. @@ -583,8 +581,10 @@ Qed. Lemma PreFreeSubE_PreFreeE_weak_embedding (full_replay_state : composite_state (equivocator_IM IM)) - (Hfull_replay_state : constrained_state_prop FreeE full_replay_state) - : VLSM_weak_embedding PreFreeSubE PreFreeE + (Hfull_replay_state : constrained_state_prop FreeE full_replay_state) : + VLSM_weak_embedding + (pre_loaded_with_all_messages_vlsm FreeSubE) + (pre_loaded_with_all_messages_vlsm FreeE) (lift_equivocators_sub_label_to full_replay_state) (lift_equivocators_sub_state_to full_replay_state). Proof. diff --git a/theories/Core/Equivocators/LimitedStateEquivocation.v b/theories/Core/Equivocators/LimitedStateEquivocation.v index 47f09972..56f12d93 100644 --- a/theories/Core/Equivocators/LimitedStateEquivocation.v +++ b/theories/Core/Equivocators/LimitedStateEquivocation.v @@ -64,7 +64,6 @@ Context (HBE : BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold := equivocating_indices_BasicEquivocation IM threshold) (FreeE : VLSM message := free_composite_vlsm (equivocator_IM IM)) - (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE) . Definition equivocators_limited_equivocations_constraint @@ -88,8 +87,10 @@ Proof. Qed. (** Inclusion of preloaded machine in the preloaded free composition. *) -Lemma preloaded_equivocators_limited_equivocations_vlsm_incl_free - : VLSM_incl (pre_loaded_with_all_messages_vlsm equivocators_limited_equivocations_vlsm) PreFreeE. +Lemma preloaded_equivocators_limited_equivocations_vlsm_incl_free : + VLSM_incl + (pre_loaded_with_all_messages_vlsm equivocators_limited_equivocations_vlsm) + (pre_loaded_with_all_messages_vlsm FreeE). Proof. by apply basic_VLSM_incl_preloaded; intros ? *; [intro | inversion 1 | intro]. Qed. diff --git a/theories/Core/Equivocators/SimulatingFree.v b/theories/Core/Equivocators/SimulatingFree.v index 0610e419..3b37df6f 100644 --- a/theories/Core/Equivocators/SimulatingFree.v +++ b/theories/Core/Equivocators/SimulatingFree.v @@ -38,7 +38,6 @@ Context composite_state (equivocator_IM IM) * option message -> Prop) (CE := pre_loaded_vlsm (composite_vlsm (equivocator_IM IM) constraintE) seed) (FreeE := free_composite_vlsm (equivocator_IM IM)) - (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE) . Definition last_in_trace_except_from @@ -111,7 +110,7 @@ Lemma generalized_equivocators_finite_valid_trace_init_to_rev finite_valid_trace_init_to CE is s tr /\ finite_trace_last_output trX = finite_trace_last_output tr. Proof. - assert (HinclE : VLSM_incl CE PreFreeE) + assert (HinclE : VLSM_incl CE (pre_loaded_with_all_messages_vlsm FreeE)) by apply constrained_pre_loaded_vlsm_incl_pre_loaded_with_all_messages. induction HtrX using finite_valid_trace_init_to_rev_strong_ind. - specialize (lift_initial_to_equivocators_state IM _ His) as Hs. @@ -240,7 +239,6 @@ Context (IM : index -> VLSM message) `{forall i : index, HasBeenSentCapability (IM i)} (FreeE := free_composite_vlsm (equivocator_IM IM)) - (PreFreeE := pre_loaded_with_all_messages_vlsm FreeE) (seed : message -> Prop) (SeededXE : VLSM message := composite_no_equivocation_vlsm_with_pre_loaded (equivocator_IM IM) (free_constraint _) seed) diff --git a/theories/Core/MessageDependencies.v b/theories/Core/MessageDependencies.v index 8d28644a..95325c44 100644 --- a/theories/Core/MessageDependencies.v +++ b/theories/Core/MessageDependencies.v @@ -275,7 +275,6 @@ Context `{!HasBeenSentCapability X} `{!HasBeenReceivedCapability X} `{!Irreflexive (msg_dep_happens_before message_dependencies)} - (R := pre_loaded_with_all_messages_vlsm X) . (** @@ -294,7 +293,7 @@ Inductive HasBeenObserved (s : state X) (m : message) : Prop := HasBeenObserved s m. Lemma transition_preserves_HasBeenObserved : - forall l s im s' om, input_valid_transition R l (s, im) (s', om) -> + forall l s im s' om, input_constrained_transition X l (s, im) (s', om) -> forall msg, HasBeenObserved s msg -> HasBeenObserved s' msg. Proof. intros * Ht msg Hbefore; inversion Hbefore as [Hobs | m Hobs Hdep]. @@ -303,7 +302,7 @@ Proof. Qed. Lemma HasBeenObserved_step_update : - forall l s im s' om, input_valid_transition R l (s, im) (s', om) -> + forall l s im s' om, input_constrained_transition X l (s, im) (s', om) -> forall msg, HasBeenObserved s' msg <-> @@ -606,7 +605,6 @@ Context `{forall i, HasBeenReceivedCapability (IM i)} `{!Irreflexive (msg_dep_happens_before message_dependencies)} (Free := free_composite_vlsm IM) - (RFree := pre_loaded_with_all_messages_vlsm Free) . (** @@ -645,7 +643,7 @@ Proof. Qed. Lemma transition_preserves_CompositeHasBeenObserved : - forall l s im s' om, input_valid_transition RFree l (s, im) (s', om) -> + forall l s im s' om, input_constrained_transition Free l (s, im) (s', om) -> forall msg, CompositeHasBeenObserved s msg -> CompositeHasBeenObserved s' msg. Proof. destruct (free_composite_has_been_directly_observed_stepwise_props IM) as []. @@ -655,7 +653,7 @@ Proof. Qed. Lemma CompositeHasBeenObserved_step_update : - forall l s im s' om, input_valid_transition RFree l (s, im) (s', om) -> + forall l s im s' om, input_constrained_transition Free l (s, im) (s', om) -> forall msg, CompositeHasBeenObserved s' msg <-> @@ -742,7 +740,7 @@ Qed. Lemma composite_observed_before_send_subsumes_msg_dep_rel `{forall i, MessageDependencies (IM i) message_dependencies} : - forall m, can_emit RFree m -> + forall m, can_emit (pre_loaded_with_all_messages_vlsm Free) m -> forall dm, msg_dep_rel message_dependencies dm m -> composite_observed_before_send dm m. Proof. diff --git a/theories/Core/ProjectionTraces.v b/theories/Core/ProjectionTraces.v index 378b661a..b386e23f 100644 --- a/theories/Core/ProjectionTraces.v +++ b/theories/Core/ProjectionTraces.v @@ -198,7 +198,7 @@ Qed. Lemma pre_loaded_with_all_messages_projection_input_valid_transition_eq (s1 s2 : composite_state IM) (om1 om2 : option message) - (l : label (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))) + (l : label (free_composite_vlsm IM)) (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2)) (Hl : projT1 l = j) : input_constrained_transition (IM (projT1 l)) @@ -216,7 +216,7 @@ Qed. Lemma pre_loaded_with_all_messages_projection_input_valid_transition_neq [s1 s2 : composite_state IM] [om1 om2 : option message] - [l : label (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))] + [l : label (free_composite_vlsm IM)] (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2)) [i : index] (Hi : i <> projT1 l) diff --git a/theories/Core/SubProjectionTraces.v b/theories/Core/SubProjectionTraces.v index 30f2f63e..a5eb01f9 100644 --- a/theories/Core/SubProjectionTraces.v +++ b/theories/Core/SubProjectionTraces.v @@ -374,7 +374,6 @@ Context (Free := free_composite_vlsm IM) (Sub_Free := free_composite_vlsm sub_IM) (X := composite_vlsm IM constraint) - (Pre := pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) . Program Definition sub_index_list_annotate : list sub_index := diff --git a/theories/Core/VLSM.v b/theories/Core/VLSM.v index 17efde78..cbd21e7c 100644 --- a/theories/Core/VLSM.v +++ b/theories/Core/VLSM.v @@ -791,8 +791,8 @@ Qed. (** For VLSMs initialized with many initial messages such as - the [composite_vlsm_induced_projection] or the [pre_loaded_with_all_messages_vlsm], - the question of whether a [VLSM] [can_emit] a message <> becomes more + the [composite_vlsm_induced_projection] the question of + whether a [VLSM] [can_emit] a message <> becomes more useful than that whether <> is a [valid_message]. *) diff --git a/theories/Core/Validator.v b/theories/Core/Validator.v index 7b09d256..014c0a85 100644 --- a/theories/Core/Validator.v +++ b/theories/Core/Validator.v @@ -58,7 +58,6 @@ Context (Y : VLSM message) (label_project : label X -> option (label Y)) (state_project : state X -> state Y) - (PreY := pre_loaded_with_all_messages_vlsm Y) . (** @@ -479,12 +478,11 @@ Context (Hproji := projection_induced_validator_is_projection _ _ _ _ _ _ Hlabel_lift Hstate_lift Htransition_consistency Htransition_None) - (PreY := pre_loaded_with_all_messages_vlsm Y) - (Hproj : VLSM_projection X PreY label_project state_project) + (Hproj : VLSM_projection X (pre_loaded_with_all_messages_vlsm Y) label_project state_project) . (** - If there is a [VLSM_projection] from <> to <> and the + If there is a [VLSM_projection] from <> to preloaded <> and the [projection_induced_validator_is_projection], then a [transition] [valid] for the [projection_induced_validator] has the same output as the transition on <>. *) @@ -503,7 +501,7 @@ Proof. Qed. Lemma induced_validator_incl_preloaded_with_all_messages - : VLSM_incl Xi PreY. + : VLSM_incl Xi (pre_loaded_with_all_messages_vlsm Y). Proof. apply basic_VLSM_incl. - by intros is (s & <- & Hs); apply (VLSM_projection_initial_state Hproj). @@ -586,13 +584,13 @@ Context . (** - We can show that <> is included in <> by applying the meta-lemma + We can show that preloaded <> is included in <> by applying the meta-lemma [VLSM_incl_finite_traces_characterization], and by induction on the length of a trace. The [projection_validator_prop]erty is used to translate [input_valid]ity for the preloaded machine into the [pre_projection_induced_validator]. *) Lemma pre_loaded_with_all_messages_validator_proj_incl - : VLSM_incl PreY Xi. + : VLSM_incl (pre_loaded_with_all_messages_vlsm Y) Xi. Proof. (* reduce inclusion to inclusion of finite traces. *) apply VLSM_incl_finite_traces_characterization. @@ -617,12 +615,12 @@ Qed. (** Given that any projection is included in the [pre_loaded_with_all_messages_vlsm] of its component (Lemma [proj_pre_loaded_with_all_messages_incl]), we conclude - that <> and <> are trace-equal. This means that all the + that preloaded <> and <> are trace-equal. This means that all the byzantine behavior of a component which is a validator is exhibited by its corresponding projection. *) Lemma pre_loaded_with_all_messages_validator_proj_eq - : VLSM_eq PreY Xi. + : VLSM_eq (pre_loaded_with_all_messages_vlsm Y) Xi. Proof. split. - by apply pre_loaded_with_all_messages_validator_proj_incl. @@ -735,7 +733,6 @@ Context (constraint : composite_label IM -> composite_state IM * option message -> Prop) (X := composite_vlsm IM constraint) (i : index) - (PreXi := pre_loaded_with_all_messages_vlsm (IM i)) . Definition composite_project_label (l : composite_label IM) @@ -840,7 +837,6 @@ Context (constraint : composite_label IM -> composite_state IM * option message -> Prop) (X := composite_vlsm IM constraint) (i : index) - (PreXi := pre_loaded_with_all_messages_vlsm (IM i)) . (** @@ -1002,20 +998,18 @@ Definition self_validator_vlsm_prop := Context (Hvalidator : self_validator_vlsm_prop) - (PreX := pre_loaded_with_all_messages_vlsm X) . (** - Let <> be the [pre_loaded_with_all_messages_vlsm] associated to X. From Lemma [vlsm_incl_pre_loaded_with_all_messages_vlsm] we know that <> is - included in <>. + included in preloaded <>. To prove the converse we use the [self_validator_vlsm_prop]erty to verify the conditions of meta-lemma [VLSM_incl_finite_traces_characterization]. *) -Lemma pre_loaded_with_all_messages_self_validator_vlsm_incl - : VLSM_incl PreX X. +Lemma pre_loaded_with_all_messages_self_validator_vlsm_incl : + VLSM_incl (pre_loaded_with_all_messages_vlsm X) X. Proof. unfold self_validator_vlsm_prop in Hvalidator. destruct X as (T & M). simpl in *. @@ -1036,10 +1030,10 @@ Proof. by eapply Hvalidator. Qed. -(** We conclude that <> and <> are trace-equal. *) +(** We conclude that <> and preloaded <> are trace-equal. *) Lemma pre_loaded_with_all_messages_self_validator_vlsm_eq - : VLSM_eq PreX X. + : VLSM_eq (pre_loaded_with_all_messages_vlsm X) X. Proof. split. - by apply pre_loaded_with_all_messages_self_validator_vlsm_incl. diff --git a/theories/Examples/Tutorial/PrimesComposition.v b/theories/Examples/Tutorial/PrimesComposition.v index 0f5435af..6453d5a7 100644 --- a/theories/Examples/Tutorial/PrimesComposition.v +++ b/theories/Examples/Tutorial/PrimesComposition.v @@ -544,9 +544,7 @@ Lemma even_constrained_primes_composition_no_validator : EvenConstraint p. Proof. intros p Hnv. - cut (input_valid - (pre_loaded_with_all_messages_vlsm - (indexed_radix_vlsms (λ p0 : primes, `p0) p)) () (3, Some 3)). + cut (input_constrained (indexed_radix_vlsms (λ p0 : primes, `p0) p) () (3, Some 3)). { intro Hiv. apply Hnv in Hiv as (s & _ & _ & _ & _ & Hc).