From 9a780b6d9b3462efb5b8359bb18111a845fa1ff5 Mon Sep 17 00:00:00 2001 From: wkolowski Date: Mon, 11 Dec 2023 13:28:14 +0100 Subject: [PATCH] Code review. --- theories/Core/AnnotatedVLSM.v | 14 ++--- .../ByzantineTraces/LimitedByzantineTraces.v | 14 +++-- theories/Core/Composition.v | 12 ++--- .../Equivocation/MsgDepLimitedEquivocation.v | 35 ++++++------ theories/Core/MessageDependencies.v | 33 ++++++------ theories/Core/VLSM.v | 54 ++++++++++--------- theories/Examples/ELMO/ELMO.v | 16 +++--- 7 files changed, 87 insertions(+), 91 deletions(-) diff --git a/theories/Core/AnnotatedVLSM.v b/theories/Core/AnnotatedVLSM.v index d9b1eb84..f0047e61 100644 --- a/theories/Core/AnnotatedVLSM.v +++ b/theories/Core/AnnotatedVLSM.v @@ -254,8 +254,8 @@ Definition annotated_projection_validator_prop_alt : Prop := annotated_composite_label_project annotated_composite_state_project annotated_composite_label_lift annotated_composite_state_lift. -Lemma preloaded_annotated_composite_preloaded_projection - : VLSM_projection +Lemma preloaded_annotated_composite_preloaded_projection : + VLSM_projection (pre_loaded_with_all_messages_vlsm AnnotatedFree) (pre_loaded_with_all_messages_vlsm (IM i)) annotated_composite_label_project annotated_composite_state_project. @@ -289,14 +289,14 @@ Proof. - by intro; intros; apply any_message_is_valid_in_preloaded. Qed. -Lemma annotated_composite_preloaded_projection - : VLSM_projection AnnotatedFree (pre_loaded_with_all_messages_vlsm (IM i)) +Lemma annotated_composite_preloaded_projection : + VLSM_projection AnnotatedFree (pre_loaded_with_all_messages_vlsm (IM i)) annotated_composite_label_project annotated_composite_state_project. Proof. apply @VLSM_incl_projection_trans - with (MY := (pre_loaded_with_all_messages_vlsm AnnotatedFree)); - [| by apply preloaded_annotated_composite_preloaded_projection]. - by apply (vlsm_incl_pre_loaded_with_all_messages_vlsm AnnotatedFree). + with (MY := (pre_loaded_with_all_messages_vlsm AnnotatedFree)). + - by apply (vlsm_incl_pre_loaded_with_all_messages_vlsm AnnotatedFree). + - by apply preloaded_annotated_composite_preloaded_projection. Qed. Definition annotated_composite_induced_validator : VLSM message diff --git a/theories/Core/ByzantineTraces/LimitedByzantineTraces.v b/theories/Core/ByzantineTraces/LimitedByzantineTraces.v index 8d990129..2193d3ec 100644 --- a/theories/Core/ByzantineTraces/LimitedByzantineTraces.v +++ b/theories/Core/ByzantineTraces/LimitedByzantineTraces.v @@ -389,11 +389,9 @@ Proof. subst non_byzantine. induction Hbyzantine using finite_valid_trace_rev_ind. - split; [| by apply empty_subseteq]. - cut (initial_state_prop Limited bs). - { - by split; [constructor; apply initial_state_is_valid |]. - } - by split; cbn; [apply lift_sub_state_initial |]. + assert (Hisp : initial_state_prop Limited bs) + by (split; cbn; [apply lift_sub_state_initial |]; done). + by split; [constructor; apply initial_state_is_valid |]. - subst s_reset_byzantine bs btr. unfold pre_VLSM_embedding_finite_trace_project; rewrite !map_app. rewrite @msg_dep_annotate_trace_with_equivocators_app; cbn. @@ -402,9 +400,9 @@ Proof. ; destruct IHHbyzantine as [[Htr0_ann Hsi_ann] Htr0_eqv_byzantine] ; cbn in Htr0_eqv_byzantine |- *. remember (@finite_trace_last _ (annotated_type (free_composite_vlsm IM) _) _ _) - as lst in Htr0_eqv_byzantine at 1 |- * at 1 2 3 4 5 6. - assert (Hlsti : original_state lst = lift_sub_state IM (elements (list_to_set (enum index) ∖ byzantine)) - (finite_trace_last si tr0)). + as lst in Htr0_eqv_byzantine at 1 |- * at 1 2 3 4 5 6. + assert (Hlsti : original_state lst = lift_sub_state IM + (elements (list_to_set (enum index) ∖ byzantine)) (finite_trace_last si tr0)). { subst lst; rewrite msg_dep_annotate_trace_with_equivocators_last_original_state; symmetry. apply (pre_VLSM_embedding_finite_trace_last _ _ diff --git a/theories/Core/Composition.v b/theories/Core/Composition.v index 00203382..72aba1dc 100644 --- a/theories/Core/Composition.v +++ b/theories/Core/Composition.v @@ -657,7 +657,7 @@ Ltac state_update_simpl := *) (** - We call a [composite_state] constrained is it is constrained for the + We call a [composite_state] constrained if it is constrained for the [free_composite_vlsm]. *) Definition composite_constrained_state_prop @@ -665,14 +665,12 @@ Definition composite_constrained_state_prop (IM : index -> VLSM message) (s : composite_state IM) : Prop := constrained_state_prop (free_composite_vlsm IM) s. -(** - If a composite state is constrained, so are all of its component states. -*) +(** If a composite state is constrained, so are all of its component states. *) Lemma composite_constrained_state_project - message `{EqDecision index} (IM : index -> VLSM message) + (message : Type) `{EqDecision index} (IM : index -> VLSM message) (s : composite_state IM) i : - composite_constrained_state_prop IM s -> - constrained_state_prop (IM i) (s i). + composite_constrained_state_prop IM s -> + constrained_state_prop (IM i) (s i). Proof. intros [om Hproto]. induction Hproto; [by apply initial_state_is_valid; cbn |]. diff --git a/theories/Core/Equivocation/MsgDepLimitedEquivocation.v b/theories/Core/Equivocation/MsgDepLimitedEquivocation.v index 017a51a6..16d853b8 100644 --- a/theories/Core/Equivocation/MsgDepLimitedEquivocation.v +++ b/theories/Core/Equivocation/MsgDepLimitedEquivocation.v @@ -121,7 +121,7 @@ Definition coeqv_limited_equivocation_projection_validator_prop_alt : index -> P HasBeenSentCapability coeqv_limited_equivocation_vlsm := { has_been_sent := - fun (sigma : state coeqv_limited_equivocation_vlsm) (m : message)=> + fun (sigma : state coeqv_limited_equivocation_vlsm) (m : message) => composite_has_been_sent IM (original_state sigma) m }. Next Obligation. @@ -137,20 +137,19 @@ Proof. with (lY := li) in Ht as Hti; [| by apply (composite_project_label_eq IM)]. cbn in Hti. apply has_been_sent_step_update with (msg := msg) in Hti. - destruct Ht as [_ Ht]; cbn in Ht; unfold annotated_transition in Ht. - cbn in Ht; destruct transition; inversion Ht; subst; cbn in *; clear Ht. + destruct Ht as [_ Ht]; cbn in Ht; unfold annotated_transition in Ht; cbn in Ht. + destruct transition; inversion Ht; subst; cbn in *; clear Ht. split. - intros [i_msg Hmsg]. destruct (decide (i = i_msg)) as [<- | Hi_msg]. + cbn in Hmsg; apply Hti in Hmsg as [-> | Hmsg]; [by left |]. by right; eexists. + by right; state_update_simpl; eexists. - - cbn in *. - intros [-> | Hmsg]; [by eexists; apply Hti; left |]. + - intros [-> | Hmsg]; [by eexists; apply Hti; left |]. destruct Hmsg as [i_msg Hmsg]. - destruct (decide (i = i_msg)) as [<- | Hi_msg]; - [by eexists; apply Hti; right |]. - by exists i_msg; state_update_simpl. + destruct (decide (i = i_msg)) as [<- | Hi_msg]. + + by eexists; apply Hti; right. + + by exists i_msg; state_update_simpl. Qed. End sec_coequivocating_senders_limited_equivocation. @@ -782,12 +781,11 @@ Lemma constrained_limited_to_annotated_limited_valid_state RelDecision (is_equivocating_tracewise_no_has_been_sent IM A sender)} `{!WitnessedEquivocation.WitnessedEquivocationCapability (Cv := Cv) IM threshold A sender} (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies) : - forall (s : composite_state IM), - valid_state_prop - (tracewise_limited_equivocation_vlsm_composition IM threshold A sender (Cv := Cv)) - s -> - exists (sigma : state Limited), - valid_state_prop Limited sigma /\ original_state sigma = s. + forall (s : composite_state IM), + valid_state_prop (tracewise_limited_equivocation_vlsm_composition + IM threshold A sender (Cv := Cv)) s -> + exists (sigma : state Limited), + valid_state_prop Limited sigma /\ original_state sigma = s. Proof. intros s Hs. eapply @limited_valid_state_has_trace_exhibiting_limited_equivocation @@ -803,11 +801,10 @@ Lemma constrained_limited_to_annotated_limited_valid_message RelDecision (is_equivocating_tracewise_no_has_been_sent IM A sender)} `{!WitnessedEquivocation.WitnessedEquivocationCapability (Cv := Cv) IM threshold A sender} (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies) : - forall (m : message), - valid_message_prop - (tracewise_limited_equivocation_vlsm_composition IM threshold A sender (Cv := Cv)) - m -> - valid_message_prop Limited m. + forall (m : message), + valid_message_prop (tracewise_limited_equivocation_vlsm_composition + IM threshold A sender (Cv := Cv)) m -> + valid_message_prop Limited m. Proof. intros msg Hmsg. apply emitted_messages_are_valid_iff in Hmsg as [Hmsg | ([s im] & [i li] & s' & Ht)]; diff --git a/theories/Core/MessageDependencies.v b/theories/Core/MessageDependencies.v index c4852ac2..f9e7aa72 100644 --- a/theories/Core/MessageDependencies.v +++ b/theories/Core/MessageDependencies.v @@ -849,8 +849,9 @@ Proof. by rewrite composite_has_been_directly_observed_sent_received_iff; intros []. } destruct Hobs as [Hobs | m' [i Hobs] Hhb]; [done | exists i]. - by eapply msg_dep_full_node_happens_before_reflects_has_been_directly_observed; - cycle 2; [eapply composite_constrained_state_project |..]. + eapply msg_dep_full_node_happens_before_reflects_has_been_directly_observed; + [done | done | | done..]. + by eapply composite_constrained_state_project. Qed. Lemma msg_dep_locally_is_globally_equivocating @@ -1270,26 +1271,26 @@ Definition transition_preserves_global_equivocation Inductive TraceMonotonicGlobalEquivocation : composite_state IM -> list (composite_transition_item IM) -> Prop := -| tpge_initial : forall (s : composite_state IM), - TraceMonotonicGlobalEquivocation s [] -| tpge_step : forall (s : composite_state IM) (item : composite_transition_item IM) - (tr : list (composite_transition_item IM)), - transition_preserves_global_equivocation s item -> - TraceMonotonicGlobalEquivocation (destination item) tr -> - TraceMonotonicGlobalEquivocation s (item :: tr). +| tpge_initial : + forall (s : composite_state IM), TraceMonotonicGlobalEquivocation s [] +| tpge_step : + forall (s : composite_state IM) (item : composite_transition_item IM) + (tr : list (composite_transition_item IM)), + transition_preserves_global_equivocation s item -> + TraceMonotonicGlobalEquivocation (destination item) tr -> + TraceMonotonicGlobalEquivocation s (item :: tr). Definition trace_monotonic_global_equivocation (s : composite_state IM) (tr : list (composite_transition_item IM)) : Prop := - forall (pre suf : list (composite_transition_item IM)) - (item : composite_transition_item IM), - tr = pre ++ [item] ++ suf -> - transition_preserves_global_equivocation (finite_trace_last s pre) item. + forall (pre suf : list (composite_transition_item IM)) (item : composite_transition_item IM), + tr = pre ++ [item] ++ suf -> + transition_preserves_global_equivocation (finite_trace_last s pre) item. Lemma trace_monotonic_global_equivocation_def_equiv : forall (s : composite_state IM) (tr : list (composite_transition_item IM)), - trace_monotonic_global_equivocation s tr - <-> - TraceMonotonicGlobalEquivocation s tr. + trace_monotonic_global_equivocation s tr + <-> + TraceMonotonicGlobalEquivocation s tr. Proof. split. - remember (length tr) as n; revert s tr Heqn. diff --git a/theories/Core/VLSM.v b/theories/Core/VLSM.v index d129c15b..17efde78 100644 --- a/theories/Core/VLSM.v +++ b/theories/Core/VLSM.v @@ -1459,8 +1459,8 @@ Proof. by auto using finite_valid_trace_from_to_extend. Qed. -Lemma finite_valid_trace_from_to_snoc - (s f : state X) (ls : list transition_item) (item : transition_item): +Lemma finite_valid_trace_from_to_snoc : + forall (s f : state X) (ls : list transition_item) (item : transition_item X), finite_valid_trace_from_to s f (ls ++ [item]) <-> let m := finite_trace_last s ls in finite_valid_trace_from_to s m ls /\ @@ -1506,43 +1506,45 @@ Proof. by eauto using finite_valid_trace_from_to_last. Qed. -Lemma finite_valid_trace_init_to_snoc - (si sf : state X) (tr : list transition_item) (item : transition_item): - finite_valid_trace_init_to si sf (tr ++ [item]) <-> - finite_valid_trace_init_to si (finite_trace_last si tr) tr /\ - input_valid_transition_item (finite_trace_last si tr) item /\ - destination item = sf. +Lemma finite_valid_trace_init_to_snoc : + forall (si sf : state X) (tr : list transition_item) (item : transition_item X), + finite_valid_trace_init_to si sf (tr ++ [item]) <-> + finite_valid_trace_init_to si (finite_trace_last si tr) tr /\ + input_valid_transition_item (finite_trace_last si tr) item /\ + destination item = sf. Proof. - unfold finite_valid_trace_init_to; rewrite finite_valid_trace_from_to_snoc. + unfold finite_valid_trace_init_to; intros. + rewrite finite_valid_trace_from_to_snoc. by itauto. Qed. -Lemma finite_valid_trace_init_to_snoc_rev - {si sf : state X} {tr : list transition_item} {item : transition_item}: - finite_valid_trace_init_to si sf tr -> - input_valid_transition_item sf item -> - finite_valid_trace_init_to si (destination item) (tr ++ [item]). +Lemma finite_valid_trace_init_to_snoc_rev : + forall {si sf : state X} {tr : list transition_item} {item : transition_item X}, + finite_valid_trace_init_to si sf tr -> + input_valid_transition_item sf item -> + finite_valid_trace_init_to si (destination item) (tr ++ [item]). Proof. - unfold finite_valid_trace_init_to; rewrite finite_valid_trace_from_to_snoc. - intros [Htr Hinit]. + unfold finite_valid_trace_init_to. + intros * [Htr Hinit] Hivt. + rewrite finite_valid_trace_from_to_snoc. apply finite_valid_trace_from_to_last in Htr as Hsf; subst sf. by itauto. Qed. -Lemma finite_valid_trace_init_to_prefix - {si sf : state X} {pre tr : list transition_item} : - finite_valid_trace_init_to si sf tr -> - pre `prefix_of` tr -> - finite_valid_trace_init_to si (finite_trace_last si pre) pre. +Lemma finite_valid_trace_init_to_prefix : + forall {si sf : state X} {pre tr : list (transition_item X)}, + finite_valid_trace_init_to si sf tr -> + pre `prefix_of` tr -> + finite_valid_trace_init_to si (finite_trace_last si pre) pre. Proof. - intros [] [suf ->]; split; [| done]. + intros * [] [suf ->]; split; [| done]. by eapply finite_valid_trace_from_to_app_split. Qed. -Lemma finite_valid_trace_init_to_prefix_1 - {si sf : state X} {pre suf : list transition_item} : - finite_valid_trace_init_to si sf (pre ++ suf) -> - finite_valid_trace_init_to si (finite_trace_last si pre) pre. +Lemma finite_valid_trace_init_to_prefix_1 : + forall {si sf : state X} {pre suf : list (transition_item X)}, + finite_valid_trace_init_to si sf (pre ++ suf) -> + finite_valid_trace_init_to si (finite_trace_last si pre) pre. Proof. by intros; eapply finite_valid_trace_init_to_prefix; [| eexists]. Qed. Lemma extend_right_finite_trace_from_to diff --git a/theories/Examples/ELMO/ELMO.v b/theories/Examples/ELMO/ELMO.v index 2a214680..22c77924 100644 --- a/theories/Examples/ELMO/ELMO.v +++ b/theories/Examples/ELMO/ELMO.v @@ -49,18 +49,19 @@ Proof. - intros v vs Hv Hvs. rewrite sum_weights_disj_union, Hvs by set_solver. replace (sum_weights (set_map _ ({[v]} ∪ _))) - with (sum_weights (set_map (C := listset (Message_validator idx)) (D := listset Address) proj1_sig {[v]} ∪ set_map (D := listset Address) proj1_sig vs)) + with (sum_weights (set_map (C := listset (Message_validator idx)) + (D := listset Address) proj1_sig {[v]} ∪ set_map (D := listset Address) proj1_sig vs)) by (apply sum_weights_proper; rewrite set_map_union; done). rewrite sum_weights_disj_union; cycle 1. + rewrite set_map_singleton. - cut (` v ∉ set_map (D := listset Address) proj1_sig vs); [by set_solver |]. + cut (`v ∉ set_map (D := listset Address) proj1_sig vs); [by set_solver |]. contradict Hv. apply elem_of_map in Hv as (v' & Hv' & Hv). by apply dsig_eq in Hv' as ->. + replace (sum_weights (set_map _ {[v]})) - with (sum_weights (Cv := listset Address) {[` v]}); - [by rewrite !sum_weights_singleton |]. - by apply sum_weights_proper; rewrite set_map_singleton. + with (sum_weights (Cv := listset Address) {[` v]}). + * by rewrite !sum_weights_singleton. + * by apply sum_weights_proper; rewrite set_map_singleton. Qed. Definition immediate_dependency (m1 m2 : Message) : Prop := @@ -1410,9 +1411,8 @@ Definition ELMO_global_equivocation : Definition ELMO_not_heavy : composite_state ELMO_component -> Prop := not_heavy (1 := ELMO_global_equivocation). -Definition ELMO_equivocating_validators : - composite_state ELMO_component -> listset Address := - equivocating_validators (1 := ELMO_global_equivocation). +Definition ELMO_equivocating_validators : composite_state ELMO_component -> listset Address := + equivocating_validators (1 := ELMO_global_equivocation). Lemma ELMO_equivocating_validators_are_Message_validators : forall (s : composite_state ELMO_component) (a : Address),