From VLSM.Lib Require Import Itauto.[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]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude finite.
From Coq Require Import Streams FunctionalExtensionality Eqdep_dec.
From VLSM.Lib Require Import Preamble ListExtras.
From VLSM.Core Require Import VLSM Plans VLSMProjections.

Paxos: Abstract Specification of Consensus

A very high-level specification of the consensus problem, following Lamport.

It does not even explicitly model multiple nodes, just the set of values which any node thinks have been agreed upon as the consensus value.

The only allowed transition is moving from an empty set to a singleton set.

Note that this captures the safety and liveness properties of never thinking multiple (distinct) values have been selected and eventually selecting a value, but cannot specify any properties about if and when correct nodes learn of the consensus.

Section sec_consensus_spec.

Context
  (V VSet : Type)
  `{FinSet V VSet}
  .

Definition consensus_state : Type := VSet.
Definition consensus_message : Type := False.

This type can be seen as a degenerate case when defining a sum type for expressing different steps in a transition system.

Inductive consensus_action : Type :=
| Decided (v : V).

To enable TLA-style refinement, we need to allow stutter actions in our transition system. Hence, we use None to express stuttering, i.e., a no-op transition.

Definition consensus_label : Type := option consensus_action.

Definition consensus_type : VLSMType False :=
{|
  state := consensus_state;
  label := consensus_label;
|}.

A consensus_state is initial when the the consensus set is empty.

Definition consensus_initial_state_prop (s : consensus_state) : Prop := s ≡ ∅.

There are no initial messages.

Definition consensus_initial_message_prop (m : consensus_message) : Prop := False.

Definition consensus_valid (l : consensus_label) :
  consensus_state * option consensus_message -> Prop :=
  fun '(s, _) =>
  match l with
  | None => True
  | Some (Decided _) => s ≡ ∅
  end.

Definition consensus_transition (l : consensus_label) :
  consensus_state * option consensus_message -> consensus_state * option consensus_message :=
  fun '(s, _) =>
  match l with
  | None => (s, None)
  | Some (Decided v) => ({[ v ]} ∪ s, None)
  end.

Definition consensus_vlsm_machine : VLSMMachine consensus_type :=
{|
  initial_state_prop := consensus_initial_state_prop;
  s0 := populate (_ ↾ (reflexivity _ : consensus_initial_state_prop ∅));
  initial_message_prop := consensus_initial_message_prop;
  transition := consensus_transition;
  valid := consensus_valid;
|}.

Definition consensus_vlsm := mk_vlsm consensus_vlsm_machine.

Lemma consensus_invariant :
  forall (s : state consensus_vlsm),
    valid_state_prop _ s ->
    s ≡ ∅ \/ exists v : V, s ≡ {[ v ]}.V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
∀ s : state consensus_vlsm,
  valid_state_prop consensus_vlsm s
  → s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
Proof.V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
∀ s : state consensus_vlsm,
  valid_state_prop consensus_vlsm s
  → s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
  intros s Hs.V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
s: state consensus_vlsm
Hs: valid_state_prop consensus_vlsm s
s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
  induction Hs using valid_state_prop_ind; [by left |].V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
s': state consensus_vlsm
l: label consensus_vlsm
om, om': option False
s: state consensus_vlsm
Ht: input_valid_transition consensus_vlsm l (
  s, om) (s', om')
IHHs: s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
s' ≡ ∅ ∨ (∃ v : V, s' ≡ {[v]})
  destruct Ht as [(_ & _ & Hvalid) Hstep]; cbn in Hvalid.V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
s': state consensus_vlsm
l: label consensus_vlsm
om, om': option False
s: state consensus_vlsm
Hvalid: match l with
| Some (Decided _) => s ≡ ∅
| None => True
end
Hstep: transition l (s, om) = (s', om')
IHHs: s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
s' ≡ ∅ ∨ (∃ v : V, s' ≡ {[v]})
  destruct l as [[v] |]; inversion Hstep; subst s'; [| done].V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
v: V
om, om': option False
s: state consensus_vlsm
Hvalid: s ≡ ∅
Hstep: transition (Some (Decided v)) (s, om) =
({[v]} ∪ s, om')
IHHs: s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
H9: None = om'
{[v]} ∪ s ≡ ∅ ∨ (∃ v0 : V, {[v]} ∪ s ≡ {[v0]})
  right; exists v.V, VSet: Type
H: ElemOf V VSet
H0: Empty VSet
H1: Singleton V VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements V VSet
EqDecision0: EqDecision V
H6: FinSet V VSet
v: V
om, om': option False
s: state consensus_vlsm
Hvalid: s ≡ ∅
Hstep: transition (Some (Decided v)) (s, om) =
({[v]} ∪ s, om')
IHHs: s ≡ ∅ ∨ (∃ v : V, s ≡ {[v]})
H9: None = om'
{[v]} ∪ s ≡ {[v]}
  by rewrite Hvalid, (right_id ∅ (∪)).
Qed.

End sec_consensus_spec.