VLSM release 1.3

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

| Pa...

VLSM release 1.2

Release compatible with Coq 8.15 and Coq-std++ 1.7.0.

VLSM release 1.1

Release compatible with Coq 8.13 and Coq-std++ 1.6.0.

VLSM release 1.0

Release compatible with Coq 8.13 and Coq-std++ 1.5.0.