Validators for message-dependent limited equivocation (#9)

* Byzantine traces result for message-dependency-based limited
message-equivocation

* Relaxing validator assumption to message-validation

* Refactoring and documentation

Co-authored-by: Wojciech Kołowski <[email protected]>
Co-authored-by: Karl Palmskog <[email protected]>

theories/VLSM/Core/AnnotatedVLSM.v

@@ -1,6 +1,14 @@
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import ListExtras.
-From VLSM.Core Require Import VLSM VLSMProjections.
+From VLSM.Core Require Import VLSM VLSMProjections Validator Composition ProjectionTraces.
+
+(** * State-annotated VLSMs
+
+This module describes the VLSM obtained by augmenting the states of an existing
+VLSM with annotations and providing additional validity constraints taking into
+account the annotations, and a function for updating the annotations following a
+transition.
+*)
 
 Section sec_annotated_vlsm.
 
@@ -170,3 +178,167 @@ Proof.
 Qed.
 
 End sec_annotated_vlsm_projections.
+
+Section sec_composite_annotated_vlsm_projections.
+
+(** ** Specializing [projection_validator_prop]erties to annotated compositions.  *)
+
+Context
+  {message : Type}
+  `{EqDecision index}
+  (IM : index -> VLSM message)
+  (Free := free_composite_vlsm IM)
+  {annotation : Type}
+  (initial_annotation_prop : annotation -> Prop)
+  `{Inhabited (sig initial_annotation_prop)}
+  (annotated_constraint : @label _ (annotated_type Free annotation) -> annotated_state Free annotation  * option message -> Prop)
+  (annotated_transition_state : @label _ (annotated_type Free annotation) -> annotated_state Free annotation * option message -> annotation)
+  (AnnotatedFree : VLSM message := annotated_vlsm Free annotation initial_annotation_prop annotated_constraint annotated_transition_state)
+  (i : index)
+  .
+
+Definition annotated_composite_label_project : vlabel AnnotatedFree -> option (vlabel (IM i))
+  := composite_project_label IM i.
+
+Definition annotated_composite_state_project : vstate AnnotatedFree -> vstate (IM i)
+  := fun s => original_state s i.
+
+Definition annotated_projection_validator_prop : Prop :=
+  @projection_validator_prop _ AnnotatedFree (IM i)
+    annotated_composite_label_project annotated_composite_state_project.
+
+Definition annotated_message_validator_prop : Prop :=
+  @message_validator_prop _ AnnotatedFree (IM i).
+
+Definition annotated_composite_label_lift : vlabel (IM i) -> vlabel AnnotatedFree
+  := lift_to_composite_label IM i.
+
+Definition annotated_composite_state_lift : vstate (IM i) -> vstate AnnotatedFree
+  := fun si =>
+     @Build_annotated_state _ (free_composite_vlsm IM) _
+      (lift_to_composite_state IM i si) (` inhabitant).
+
+Definition annotated_projection_validator_prop_alt : Prop :=
+  @projection_validator_prop_alt _ AnnotatedFree (IM i)
+    annotated_composite_label_project annotated_composite_state_project
+    annotated_composite_label_lift annotated_composite_state_lift.
+
+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 basic_VLSM_projection.
+  - intros [_i _li] li.
+    unfold annotated_composite_label_project, composite_project_label; cbn.
+    case_decide; [| congruence].
+    subst _i; cbn; inversion_clear 1.
+    intros (s, ann) om (_ & _ & [Hv _] & _) _ _.
+    assumption.
+  - intros [_i _li] li.
+    unfold annotated_composite_label_project, composite_project_label; cbn.
+    case_decide; [| congruence].
+    subst _i; cbn; inversion_clear 1.
+    intros [s ann] iom [s' ann'] oom.
+    unfold input_valid_transition; cbn
+    ; unfold annotated_transition; cbn
+    ; destruct (vtransition _ _ _) as (si', om').
+    intros [_ Ht]; inversion Ht.
+    f_equal; symmetry.
+    apply state_update_eq.
+  - intros [j lj].
+    unfold annotated_composite_label_project, composite_project_label; cbn.
+    case_decide as Hij; [congruence |].
+    intros _ [s ann] iom [s' ann'] oom.
+    unfold input_valid_transition; cbn
+    ; unfold annotated_transition; cbn
+    ; destruct (vtransition _ _ _) as (si', om').
+    intros [_ Ht]; inversion Ht.
+    apply state_update_neq; congruence.
+  - intros [s ann] [Hs _]; cbn; apply Hs.
+  - intro; intros; apply any_message_is_valid_in_preloaded.
+Qed.
+
+Definition annotated_composite_induced_projection : VLSM message
+  := projection_induced_vlsm AnnotatedFree (type (IM i))
+    annotated_composite_label_project annotated_composite_state_project
+    annotated_composite_label_lift annotated_composite_state_lift.
+
+Lemma annotated_composite_induced_projection_transition_None
+  : weak_projection_transition_consistency_None _ _ annotated_composite_label_project annotated_composite_state_project.
+Proof.
+  intros [j lj].
+  unfold annotated_composite_label_project, composite_project_label; cbn.
+  case_decide as Hij; [congruence |].
+  intros _ sX omX s'X om'X [_ Ht]; revert Ht; cbn.
+  unfold annotated_transition; cbn
+  ; destruct (vtransition _ _ _) as (si', om')
+  ; inversion 1; clear Ht; subst om' s'X; cbn.
+  rewrite state_update_neq by congruence; reflexivity.
+Qed.
+
+Lemma annotated_composite_induced_projection_label_lift
+  : induced_projection_label_lift_prop _ _
+    annotated_composite_label_project annotated_composite_label_lift.
+Proof.
+  apply component_label_projection_lift with (constraint := free_constraint IM).
+Qed.
+
+Lemma annotated_composite_induced_projection_state_lift
+  : induced_projection_state_lift_prop _ _
+    annotated_composite_state_project annotated_composite_state_lift.
+Proof.
+  intros si; apply state_update_eq.
+Qed.
+
+Lemma annotated_composite_induced_projection_initial_lift
+  : strong_full_projection_initial_state_preservation (IM i) AnnotatedFree
+    annotated_composite_state_lift.
+Proof.
+  split; cbn.
+  - apply lift_to_composite_state_initial; assumption.
+  - destruct inhabitant; assumption.
+Qed.
+
+Lemma annotated_composite_induced_projection_transition_consistency
+  : induced_projection_transition_consistency_Some _ _
+    annotated_composite_label_project annotated_composite_state_project.
+Proof.
+  intros [i1 li1] [i2 li2] li.
+  unfold annotated_composite_label_project, composite_project_label; cbn.
+  case_decide as Hi1; [| congruence].
+  subst i1; cbn; inversion_clear 1.
+  case_decide as Hi2; [| congruence].
+  subst i2; cbn; inversion_clear 1.
+  intros [s1 ann1] [s2 ann2]
+  ; unfold annotated_transition; cbn
+  ; intros <- iom sX1' oom1
+  ;destruct (vtransition _ _ _) as (si', om').
+  inversion_clear 1; intros sX2' oom2; inversion_clear 1.
+  split; [cbn | reflexivity].
+  rewrite !state_update_eq; reflexivity.
+Qed.
+
+Definition annotated_composite_induced_projection_transition_Some :=
+  basic_weak_projection_transition_consistency_Some _ _ _ _ _ _
+    annotated_composite_induced_projection_label_lift
+    annotated_composite_induced_projection_state_lift
+    annotated_composite_induced_projection_transition_consistency.
+
+Definition annotated_composite_induced_projection_is_projection :=
+  projection_induced_vlsm_is_projection _ _ _ _ _ _
+    annotated_composite_induced_projection_transition_None
+    annotated_composite_induced_projection_transition_Some.
+
+Lemma annotated_projection_validator_prop_alt_iff
+  : annotated_projection_validator_prop_alt <-> annotated_projection_validator_prop.
+Proof.
+  apply projection_validator_prop_alt_iff.
+  - apply annotated_composite_preloaded_projection.
+  - apply annotated_composite_induced_projection_transition_None.
+  - apply annotated_composite_induced_projection_label_lift.
+  - apply annotated_composite_induced_projection_state_lift.
+  - apply annotated_composite_induced_projection_initial_lift.
+  - apply annotated_composite_induced_projection_transition_consistency.
+Qed.
+
+End sec_composite_annotated_vlsm_projections.

theories/VLSM/Core/ByzantineTraces.v

@@ -393,7 +393,7 @@ Section composite_validator_byzantine_traces.
             (X := composite_vlsm IM constraint)
             (PreLoadedX := pre_loaded_with_all_messages_vlsm X)
             (FreeX := free_composite_vlsm IM)
-            (Hvalidator: forall i : index, component_projection_validator_prop IM constraint i)
+            (Hvalidator: forall i : index, component_message_validator_prop IM constraint i)
             .
 
 (**
@@ -432,18 +432,10 @@ included in <<X>> to prove our main result.
           destruct l as (i, li). simpl in *.
           specialize (valid_state_project_preloaded_to_preloaded _ IM constraint lst i Hlst)
             as Hlsti.
-          assert (Hiv : input_valid (pre_loaded_with_all_messages_vlsm (IM i)) li (lst i, iom)).
-          { split; [assumption|]. split; [|assumption].
-            eexists _. apply (pre_loaded_with_all_messages_message_valid_initial_state_message (IM i)).
-          }
-          apply Hvalidator in Hiv.
-          clear -Hiv.
-          destruct Hiv as [_ [_ [_ [Hinput _]]]].
-          destruct Hinput as [s Hinput].
-          exists s.
-          revert Hinput.
-          apply (constraint_subsumption_valid_state_message_preservation IM constraint).
-          intro. intros. destruct som. apply H.
+          destruct iom as [im |]; [| apply option_valid_message_None].
+          eapply Hvalidator; split; [eassumption |]; split; [| eassumption].
+          eexists _.
+          apply (pre_loaded_with_all_messages_message_valid_initial_state_message (IM i)).
     Qed.
 
 (**

theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v

@@ -526,7 +526,7 @@ End fixed_byzantine_traces.
 
 In this section we show that while equivocators can always appear as byzantine
 to the protocol-abiding nodes, the converse is also true if the protocol-
-abiding nodes satisfy the [projection_validator_prop]erty, which basically
+abiding nodes satisfy the [projection_message_validator_prop]erty, which basically
 allows them to locally verify the authenticity of a received message.
 *)
 
@@ -775,7 +775,7 @@ End assuming_initial_messages_lift.
 Context
   (Hvalidator:
     forall i : index, i ∉ selection ->
-    component_projection_validator_prop IM (fixed_equivocation_constraint IM selection) i)
+    component_message_validator_prop IM (fixed_equivocation_constraint IM selection) i)
   .
 
 Lemma validator_fixed_non_byzantine_vlsm_lift_initial_message
@@ -793,9 +793,7 @@ Proof.
     by exists i, (exist _ m Him).
   - destruct Hseeded as [Hsigned [i [Hi [li [si Hpre_valid]]]]].
     apply set_diff_elim2 in Hi.
-    specialize (Hvalidator i Hi _ _ Hpre_valid)
-      as [sX [Heqsi [HsX [Hm HvX]]]].
-    assumption.
+    eapply Hvalidator; eassumption.
 Qed.
 
 (** The VLSM corresponding to the induced projection from a fixed-set byzantine