Release known to be compatible with Coq 8.16 to 8.18 and Coq-std++ 1.9.0.
The theory behind this release is described in this paper. A mapping between different sections in the paper and the Coq definitions/results in the release is given below.
Section 2
| Paper | Coq |
|---|---|
| VLSM definition | VLSM.Core.VLSM#VLSMType, VLSM.Core.VLSM#VLSMMachine, VLSM.Core.VLSM#VLSM |
| valid states | VLSM.Core.VLSM#valid_state_prop |
| valid messages | VLSM.Core.VLSM#valid_message_prop, VLSM.Core.VLSM#option_valid_message_prop |
| valid states and messages | VLSM.Core.VLSM#valid_state_message_prop |
| valid transitions | VLSM.Core.VLSM#input_valid_transition |
| finite traces | VLSM.Core.VLSM#finite_valid_trace |
| infinite traces | VLSM.Core.VLSM#infinite_valid_trace |
| terminating traces | VLSM.Core.VLSM#terminating_trace_prop |
| complete traces | VLSM.Core.VLSM#complete_trace_prop |
Section 3
| Paper | Coq |
|---|---|
| free composition definition | VLSM.Core.Composition#free_composite_vlsm |
| constrained composition definition | VLSM.Core.Composition#composite_vlsm |
Section 4
| Paper | Coq |
|---|---|
| projection VLSM definition | VLSM.Core.ProjectionTraces#composite_vlsm_constrained_projection |
| projection of traces | VLSM.Core.Validator#component_projection |
| projection friendliness | VLSM.Core.VLSMProjections.VLSMTotalProjection#projection_friendly_prop |
| sub-trace | VLSM.Core.VLSMProjections.VLSMTotalProjection#VLSM_weak_projection_trace_project, VLSM.Core.VLSMProjections#pre_VLSM_projection_finite_trace_project |
| projection to a subset of components | VLSM.Core.SubProjectionTraces#pre_induced_sub_projection |
| composition of a subset of components | VLSM.Core.SubProjectionTraces#free_sub_vlsm_composition |
Section 5
| Paper | Coq |
|---|---|
| hasBeenSent capability | VLSM.Core.Equivocation#oracle_stepwise_props, VLSM.Core.Equivocation#HasBeenSentCapability |
| channel authentication assumption | VLSM.Core.Equivocation#channel_authentication_prop |
| no equivocation constraint | VLSM.Core.Equivocation.NoEquivocation#composite_no_equivocations |
| message dependencies assumption | VLSM.Core.MessageDependencies#MessageDependencies |
| full message dependencies assumption | VLSM.Core.MessageDependencies#FullMessageDependencies |
| full node assumption | VLSM.Core.MessageDependencies#message_dependencies_full_node_condition_prop |
| state equivocators | VLSM.Core.Equivocators.Equivocators#equivocator_vlsm |
| composition with fixed set of state equivocators | VLSM.Core.Equivocators.FixedEquivocation#equivocators_fixed_equivocations_vlsm |
| composition with fixed set of message equivocators | VLSM.Core.Equivocation.MsgDepFixedSetEquivocation#msg_dep_full_node_fixed_set_equivocation_constraint_subsumption |
| Relaxed model for fixed equivocation | VLSM.Core.Equivocation.FixedSetEquivocation#fixed_equivocation_vlsm_composition equivalent to the above under full-node assumptions as per VLSM.Core.Equivocation.MsgDepFixedSetEquivocation#full_node_fixed_equivocation_eq |
| equivalence between state and message fixed-equivocation for the relaxed model | VLSM.Core.Equivocators.FixedEquivocation#fixed_equivocators_valid_trace_project, VLSM.Core.Equivocators.FixedEquivocation#fixed_equivocators_vlsm_projection, VLSM.Core.Equivocators.FixedEquivocationSimulation#no_equivocating_equivocators_finite_valid_trace_init_to_rev |
| threshold | VLSM.Core.ReachableThreshold#ReachableThreshold, using Lib.Measurable for weights |
| composition with limited state-equivocation | VLSM.Core.Equivocators.LimitedStateEquivocation#equivocators_limited_equivocations_vlsm |
| traces with limited message-equivocation | VLSM.Core.Equivocation.LimitedMessageEquivocation#fixed_limited_equivocation_prop |
| simulation of traces with limited message-equivocation | VLSM.Core.Equivocators.LimitedEquivocationSimulation#limited_equivocators_finite_valid_trace_init_to_rev |
| projection to traces with limited message-equivocation | VLSM.Core.Equivocators.LimitedStateEquivocation#equivocators_limited_valid_trace_projects_to_fixed_limited_equivocation |
| The limited message-equivocation model | VLSM.Core.Equivocation.MsgDepLimitedEquivocation#full_node_limited_equivocation_vlsm |
| equivalence between state and message limited-equivocation | VLSM.Core.Equivocators.LimitedStateEquivocation#equivocators_limited_valid_trace_projects_to_annotated_limited_equivocation, VLSM.Core.Equivocators.LimitedEquivocationSimulation#equivocators_limited_valid_trace_projects_to_annotated_limited_equivocation_rev |
Section 6
| Paper | Coq |
|---|---|
| validator for a composition constraint | VLSM.Core.Validator#projection_validator_prop |
| alternative definition of validator | VLSM.Core.Validator#projection_validator_prop_alt |
| validator definition based on transitions | VLSM.Core.Validator#transition_validator |
| equivalence between definitions | VLSM.Core.Validator#projection_validator_messages_transitions, VLSM.Core.Validator#transition_validator_messages |
| Byzantine node with no attribution | VLSM.Core.ByzantineTraces#emit_any_message_vlsm |
| Byzantine nodes with message attribution | VLSM.Core.ByzantineTraces.FixedSetByzantineTraces#emit_any_signed_message_vlsm |
| the projection of a validator doesn't change in the presence of Byzantine faults | VLSM.Core.ByzantineTraces#validator_component_byzantine_fault_tolerance |
| model for fixed Byzantine behavior | VLSM.Core.ByzantineTraces.FixedSetByzantineTraces#non_byzantine_not_equivocating_constraint |
| equivalence to fixed-set message-equivocation model for validators | VLSM.Core.ByzantineTraces.FixedSetByzantineTraces#validator_fixed_non_byzantine_eq_fixed_non_equivocating |
| traces assuming a limited amount of Byzantine nodes | VLSM.Core.ByzantineTraces.LimitedByzantineTraces#limited_byzantine_trace_prop |
| equivalence to the limited message-equivocation model for validators | VLSM.Core.ByzantineTraces.LimitedByzantineTraces#msg_dep_validator_limited_non_equivocating_byzantine_traces_are_limited_non_equivocating |
Map of the ELMO example
UMO
Component and protocol
| Paper | Coq |
|---|---|
| UMO component | VLSM.Examples.ELMO.UMO#UMO_component |
| extract a unique trace from a state | VLSM.Examples.ELMO.UMO#constrained_state_contains_unique_constrained_trace |
| UMO protocol | VLSM.Examples.ELMO.UMO#UMO |
| extract a trace from a composite state | VLSM.Examples.ELMO.UMO#finite_valid_trace_from_to_UMO_state2trace_RUMO |
Observability relations
| Paper | Coq |
|---|---|
| state-prefix relation | VLSM.Examples.ELMO.UMO#state_suffix |
| state-prefix for sent messages | VLSM.Examples.ELMO.UMO#state_suffix_totally_orders_sent_messages_UMO_reachable_aux |
| sent messages totally ordered by state-prefix | VLSM.Examples.ELMO.UMO#state_suffix_totally_orders_sent_messages_UMO_reachable_aux' |
| characterization for sent messages | VLSM.Examples.ELMO.UMO#sentMessages_characterization |
| directly-observed relation | VLSM.Examples.ELMO.UMO#directly_observable |
| directly-observed for sent messages | VLSM.Examples.ELMO.UMO#directly_observable_totally_orders_sent_messages_UMO_reachable |
| was-sent-before relation | VLSM.Examples.ELMO.UMO#was_sent_before |
| first characterization for was-sent-before relation | VLSM.Examples.ELMO.UMO#was_sent_before_characterization_1 |
| second characterization for was-sent-before relation | VLSM.Examples.ELMO.UMO#was_sent_before_characterization_2 |
| sent messages totally ordered by was-sent-before | VLSM.Examples.ELMO.UMO#was_sent_before_totally_orders_sentMessages_UMO_reachable |
| sent-comparable relation | VLSM.Examples.ELMO.UMO#sent_comparable |
| incomparable relation | VLSM.Examples.ELMO.UMO#incomparable |
| observation in composite state | VLSM.Examples.ELMO.UMO#UMO_obs |
| characterization for sent messages in composite states | VLSM.Examples.ELMO.UMO#UMO_sentMessages_characterization |
MO
Component and protocol
| Paper | Coq |
|---|---|
| MO component | VLSM.Examples.ELMO.MO#MO_component |
| definition of valid received message in a MO component | VLSM.Examples.ELMO.MO#MO_msg_valid |
| alternative definition for valid received messages | VLSM.Examples.ELMO.MO#MO_msg_valid_alt |
| equivalence of the above definitions | VLSM.Examples.ELMO.MO#MO_msg_valid__MO_msg_valid_alt |
| checking state-prefix between sent observations | VLSM.Examples.ELMO.MO#state_suffix_totally_orders_valid_sent_messages' |
| extract a unique trace from a state | VLSM.Examples.ELMO.MO#constrained_state_contains_unique_constrained_trace |
| valid received message is a constrained state in the sender component | VLSM.Examples.ELMO.MO#constrained_state_prop_MO_msg_valid |
| MO protocol | VLSM.Examples.ELMO.MO#MO |
| extract a trace from a composite state | VLSM.Examples.ELMO.MO#finite_valid_trace_from_to_MO_state2trace_RMO |
Observability relations
| Paper | Coq |
|---|---|
| recursive observations (robs) | VLSM.Examples.ELMO.BaseELMO#rec_obs |
| robs is monotone for states | VLSM.Examples.ELMO.MO#rec_obs_input_valid_transition |
| robs of sent/received messages are in robs | VLSM.Examples.ELMO.MO#messages_rec_obs |
| connection between robs and obs | VLSM.Examples.ELMO.MO#unfold_robs |
| a state is not in its recursive observations | VLSM.Examples.ELMO.MO#rec_obs_acyclic |
| in a composite state in which all last observations are sent observations, there is a state component which was not received as a message in the composite state | |
| recursive observations for composite state | |
| robs is monotone for composite states |
Equivocation
| Paper | Coq |
|---|---|
| local equivocators | VLSM.Examples.ELMO.MO#local_equivocators |
| global equivocators | |
| equivalent definition for global equivocators in a composite state | VLSM.Examples.ELMO.MO#global_equivocators |
| the two notions of global equivocators coincide | |
| if robs is monotone, then local equivocators are monotone | |
| in a valid transition, local equivocators are monotone | |
| component's local equivocators included in global equivocators | VLSM.Examples.ELMO.MO#local_equivocator_inclusion |
| for any "receive" valid transition, global equivocators are monotone and the only new possible equivocator is the sender of the message | |
| for any "receive" valid transition such that the message was already sent, global equivocators remain the same | |
| construction of tr_min | |
| unfolding constrained composite state | |
| global equivocators are monotone on tr_min | |
| global equivocators on tr_min do not exceed global equivocators on the final state of tr_min |
Validators
| Paper | Coq |
|---|---|
| every MO component in a MO protocol is a validator for the protocol | VLSM.Examples.ELMO.MO#MO_component_validating |
ELMO
Component and protocol
| Paper | Coq |
|---|---|
| full node assumption for ELMO | VLSM.Examples.ELMO.ELMO#full_node |
| happens-before relation | happens_before section variable |
| simple local equivocators | VLSM.Examples.ELMO.ELMO#local_equivocators_simple |
| simple global equivocators | |
| if messages monotone, then simple local equivocators monotone | |
| full local equivocators | VLSM.Examples.ELMO.ELMO#local_equivocators_full |
| ELMO component | VLSM.Examples.ELMO.ELMO#ELMO_component |
| extract a unique trace from a state | VLSM.Examples.ELMO.ELMO#ELMO_unique_traces |
| ELMO protocol | |
| extract a trace from a composite state |
Observability relations
| Paper | Coq |
|---|---|
| connection between messages and robs under full node | VLSM.Examples.ELMO.ELMO#full_node_messages_iff_rec_obs |
Equivocation
| Paper | Coq |
|---|---|
| adr of s not in local equivocators of s | VLSM.Examples.ELMO.ELMO#local_equivocators_simple_no_self |
| full local equivocators monotone | VLSM.Examples.ELMO.ELMO#local_equivocators_full_nondecreasing |
| local equivocators, simple local equivocators and full local equivocators coincide | VLSM.Examples.ELMO.ELMO#local_equivocators_simple_iff_full, VLSM.Examples.ELMO.ELMO#local_equivocators_iff_simple, VLSM.Examples.ELMO.ELMO#local_equivocators_iff_full |
| psi_msg_valid_full holds for every constrained state | VLSM.Examples.ELMO.ELMO#ELMO_reachable_msg_valid_full |
| psi_full_node holds for every constrained state and message | VLSM.Examples.ELMO.ELMO#reachable_full_node_for_all_messages |
| every sent message is a constrained state | VLSM.Examples.ELMO.ELMO#reachable_sent_messages_reachable |
| if a received message in a constrained state satisfies the validity predicate then it is a constrained state in the sender component | VLSM.Examples.ELMO.ELMO#receivable_messages_reachable |
| global equivocators and simple global equivocators coincide | VLSM.Examples.ELMO.ELMO#ELMO_global_equivocators_iff_simple |
| unfolding constrained composite state | VLSM.Examples.ELMO.ELMO#composite_reachable_predecessor |
| tr_min is a trace in an ELMO protocol |
Validators
| Paper | Coq |
|---|---|
| message involved in valid transition from valid composite state is valid | VLSM.Examples.ELMO.ELMO#ELMO_valid_states_only_receive_valid_messages |
| technical lemma | VLSM.Examples.ELMO.ELMO#special_receivable_messages_emittable_in_future |
| key lemma for validator result: | VLSM.Examples.ELMO.ELMO#reflecting_composite_for_reachable_component |
| every ELMO component in an ELMO protocol is a validator for the protocol |