From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From VLSM.Core Require Import VLSM VLSMProjections Composition.[Loading ML file coq-itauto.plugin ... done]
From VLSM.Core Require Import Equivocation.

Core: The Full Node Constraint

Section sec_full_node_constraint.

Context
  `{EqDecision message}
  `{finite.Finite index}
  (IM : index -> VLSM message)
  (Free := free_composite_vlsm IM)
  `{forall i : index, HasBeenSentCapability (IM i)}
  `{forall i : index, HasBeenReceivedCapability (IM i)}
  (admissible_index : composite_state IM -> index -> Prop)
  (** admissible equivocator index: this index can equivocate from given state *)
  .

Given a composite state s, a message m, and a component index i if there is a machine we say that message m can be node_generated_without_further_equivocation by component i if the message can be produced by component i preloaded with all messages in a trace in which all message equivocation is done through messages causing no_additional_equivocations to state s (message has_been_directly_observed in s).

Definition node_generated_without_further_equivocation
  (s : composite_state IM)
  (m : message)
  (i : index)
  : Prop
  := exists (si : state (IM i)),
    can_produce (preloaded_with_all_messages_vlsm (IM i)) si m /\
    state_received_not_sent_invariant (IM i) si (composite_has_been_directly_observed IM s).

Similar to the condition above, but now the message is required to be generated by the machine preloaded only with messages causing no_additional_equivocations to state s.

Definition node_generated_without_further_equivocation_alt
  (s : composite_state IM)
  (m : message)
  (i : index)
  : Prop
  := can_emit (preloaded_vlsm (IM i) (composite_has_been_directly_observed IM s)) m.

The equivocation-based abstract definition of the full node condition stipulates that a message can be received in a state s if either it causes no_additional_equivocations to state s, or it can be node_generated_without_further_equivocation by an admissible component.

Definition full_node_condition_for_admissible_equivocators
  (l : composite_label IM)
  (som : composite_state IM * option message)
  : Prop
  :=
  let (s, om) := som in
  match om with
  | None => True
  | Some m =>
    composite_has_been_directly_observed IM s m \/
    exists (i : index), admissible_index s i /\ node_generated_without_further_equivocation s m i
  end.

Similar to the condition above, but using the node_generated_without_further_equivocation_alt property.

Definition full_node_condition_for_admissible_equivocators_alt
  (l : composite_label IM)
  (som : composite_state IM * option message)
  : Prop
  :=
  let (s, om) := som in
  match om with
  | None => True
  | Some m =>
    composite_has_been_directly_observed IM s m \/
    exists (i : index), admissible_index s i /\
    node_generated_without_further_equivocation_alt s m i
  end.

We here show that if a machine has the cannot_resend_message_stepwise_property, then the node_generated_without_further_equivocation property is stronger than the node_generated_without_further_equivocation_alt property.

Lemma node_generated_without_further_equivocation_weaken
  (i : index)
  (Hno_resend : cannot_resend_message_stepwise_prop (IM i))
  (s : composite_state IM)
  (Hs : constrained_state_prop (free_composite_vlsm IM) s)
  (m : message)
  (Hsmi : node_generated_without_further_equivocation s m i)
  : node_generated_without_further_equivocation_alt s m i.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
s: composite_state IM
Hs: constrained_state_prop (free_composite_vlsm IM) s
m: message
Hsmi: node_generated_without_further_equivocation s m
  i
node_generated_without_further_equivocation_alt s m i
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
s: composite_state IM
Hs: constrained_state_prop (free_composite_vlsm IM) s
m: message
Hsmi: node_generated_without_further_equivocation s m
  i
node_generated_without_further_equivocation_alt s m i
  destruct Hsmi as [si [Hsim Hsi]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
s: composite_state IM
Hs: constrained_state_prop (free_composite_vlsm IM) s
m: message
si: state (IM i)
Hsim: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) si
  m
Hsi: state_received_not_sent_invariant 
  (IM i) si
  (composite_has_been_directly_observed IM s)
node_generated_without_further_equivocation_alt s m i
  apply can_emit_iff.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
s: composite_state IM
Hs: constrained_state_prop (free_composite_vlsm IM) s
m: message
si: state (IM i)
Hsim: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) si
  m
Hsi: state_received_not_sent_invariant 
  (IM i) si
  (composite_has_been_directly_observed IM s)
∃ s0 : state
         (preloaded_vlsm (IM i)
            (composite_has_been_directly_observed IM s)),
  can_produce
    (preloaded_vlsm (IM i)
       (composite_has_been_directly_observed IM s)) s0
    m exists si.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
s: composite_state IM
Hs: constrained_state_prop (free_composite_vlsm IM) s
m: message
si: state (IM i)
Hsim: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) si
  m
Hsi: state_received_not_sent_invariant 
  (IM i) si
  (composite_has_been_directly_observed IM s)
can_produce
  (preloaded_vlsm (IM i)
     (composite_has_been_directly_observed IM s)) si m
  revert Hsim.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
s: composite_state IM
Hs: constrained_state_prop (free_composite_vlsm IM) s
m: message
si: state (IM i)
Hsi: state_received_not_sent_invariant 
  (IM i) si
  (composite_has_been_directly_observed IM s)
can_produce (preloaded_with_all_messages_vlsm (IM i))
  si m
→ can_produce
    (preloaded_vlsm (IM i)
       (composite_has_been_directly_observed IM s)) si
    m
  by eapply lift_generated_to_seeded.
Qed.

if all machines satisfy the cannot_resend_message_stepwise_property, then the full_node_condition_for_admissible_equivocators is stronger than the full_node_condition_for_admissible_equivocators_alt.

Lemma full_node_condition_for_admissible_equivocators_subsumption
  (Hno_resend : forall i : index, cannot_resend_message_stepwise_prop (IM i))
  : preloaded_constraint_subsumption (free_composite_vlsm IM)
      full_node_condition_for_admissible_equivocators
      full_node_condition_for_admissible_equivocators_alt.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
preloaded_constraint_subsumption
  (free_composite_vlsm IM)
  full_node_condition_for_admissible_equivocators
  full_node_condition_for_admissible_equivocators_alt
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
preloaded_constraint_subsumption
  (free_composite_vlsm IM)
  full_node_condition_for_admissible_equivocators
  full_node_condition_for_admissible_equivocators_alt
  intros l (s, [m |]) [Hs [_ [_ Hc]]]; [| done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
Hc: full_node_condition_for_admissible_equivocators l
  (s, Some m)
full_node_condition_for_admissible_equivocators_alt l
  (s, Some m)
  destruct Hc as [Hno_equiv | Hfull]; [by left |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
Hfull: ∃ i : index,
  admissible_index s i
  ∧ node_generated_without_further_equivocation
      s m i
full_node_condition_for_admissible_equivocators_alt l
  (s, Some m)
  right.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
Hfull: ∃ i : index,
  admissible_index s i
  ∧ node_generated_without_further_equivocation
      s m i
∃ i : index,
  admissible_index s i
  ∧ node_generated_without_further_equivocation_alt s
      m i
  destruct Hfull as [i [Hi Hfull]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
i: index
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
∃ i : index,
  admissible_index s i
  ∧ node_generated_without_further_equivocation_alt s
      m i
  exists i.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
i: index
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
admissible_index s i
∧ node_generated_without_further_equivocation_alt s m
    i split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
Hno_resend: ∀ i : index,
  cannot_resend_message_stepwise_prop
    (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
i: index
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
node_generated_without_further_equivocation_alt s m i
  specialize (Hno_resend i).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
node_generated_without_further_equivocation_alt s m i
  apply node_generated_without_further_equivocation_weaken; [done | | done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
constrained_state_prop (free_composite_vlsm IM) s
  revert Hs.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
valid_state_prop
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
  s
→ constrained_state_prop (free_composite_vlsm IM) s
  apply VLSM_incl_valid_state.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
IM: index → VLSM message
Free:= free_composite_vlsm IM: VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
admissible_index: composite_state IM → index → Prop
i: index
Hno_resend: cannot_resend_message_stepwise_prop
  (IM i)
l: label (free_composite_vlsm IM)
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm 
        (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators))
m: message
Hi: admissible_index s i
Hfull: node_generated_without_further_equivocation s
  m i
VLSM_incl_part
  (preloaded_vlsm_machine
     (constrained_vlsm (free_composite_vlsm IM)
        full_node_condition_for_admissible_equivocators)
     (λ _ : message, True))
  (preloaded_vlsm_machine (free_composite_vlsm IM)
     (λ _ : message, True))
  by apply preloaded_constraint_subsumption_incl_free.
Qed.

End sec_full_node_constraint.