3 ms·

Author here. I would be happy to get proof review.

by kushti 11y ago

microcolonel 11y ago
Good luck, hope you find the other person who knows what they're reading.
yodsanklai 11y ago
Could you tell us how the notions of processes, configurations and events are formalized? it seems there are a lot of axioms in your development. Are they needed?
- kushti 11y ago
  All those entities are used in my proof, while messages are skipped at all(so they are needed for better understanding only, while for proof's sake we can have a talk only about system's state transitions). Process is the inductive set: Inductive Process := | FinishedProcess: Binary -> Process | proceed: nat -> Process. then configuration is just a list of processes: Definition Configuration := list Process. Events are enumerated with naturals numbers, with two (abstract) functions for transition from one configuration to another, and to choose process by event: Parameter eventFn : Configuration -> nat -> Configuration. Parameter chooseFn : Configuration -> nat -> Process. We can compare processes by using chooseFn: Axiom Decidability: forall cfg n1 n2, chooseFn cfg n1 = chooseFn cfg n2 \/ chooseFn cfg n1 <> chooseFn cfg n2. and as eventFn is abstract, it seems 'run' function using eventFn needs for following axioms to be commutative: Axiom RunCommutativity: forall cfg s1 s2, run (run cfg s1) s2 = run cfg (s1 ++ s2). Axiom RunCommutativity2: forall cfg step s, run (run cfg [step]) s = run cfg (step :: s). Other axioms are following original paper pretty directly: 1. Partially correct protocol could decides on a single value only: Axiom Consistency: forall cfg, ~(decidedValue cfg true /\ decidedValue cfg false). 2. There's no change in value after consideration(termination property of a consensus algorithm): Axiom Termination: forall cfg b step, decidedValue cfg b -> decidedValue (eventFn cfg step) b. 3. "By the total correctness of P, and the fact that there are always admissible runs, V > 0" Axiom Correctness: forall cfg, bivalent cfg \/ univalent cfg. 4. As messaging is asynchronous, we can swap two events involving different processes: Axiom Async1: forall cfg step1 step2, (chooseFn cfg step1) <> (chooseFn cfg step2) -> run cfg ([step1;step2]) = run cfg ([step2;step1]). Please note, there's no any limitation on synchronicity inside a process. 5. Initial configuration properties, i.e. both values are reachable from it Axiom InitialNoConsensus: ~decided InitialConfiguration. Axiom TrueReacheable: exists s1, decidedValue (run InitialConfiguration s1) true. Axiom FalseReacheable: exists s2, decidedValue (run InitialConfiguration s2) false. While original proof considering set of applicable messages, my proof uses only randomStep function returning some possible event to happen in current configuration, and AnotherProcessStepExists axiom stating any process can make a step in any round(in my formulation, if some process is involved in any step, there's other step for other process). Axiom AnotherProcessStepExists: forall cfg step, exists step0, chooseFn cfg step <> chooseFn cfg step0. Parameter randomStep: Configuration -> nat. That's all! There are two other axioms which could be (and will be if so) proven probably, but anyway there's no doubt in them: Axiom Correctness6: forall cfg s, univalent_true cfg -> univalent_true (run cfg s). Axiom Correctness7: forall cfg s, univalent_false cfg -> univalent_false (run cfg s).
  - kushti 11y ago
    Copypasted it into repos' README along with some Markdown for better readability’s sake: https://github.com/ConsensusResearch/flp https://github.com/ConsensusResearch/flp
gergoerdi 11y ago
(** A particular execution, defined by a possibly infinite sequence of events from a starting configuration C is called a schedule and the sequence of steps taken to realise the schedule is a run **) Definition Schedule := list nat. Is `list` codata by default in Coq?
- CHY872 11y ago
  Don't you want https://coq.inria.fr/library/Coq.Lists.Streams.html https://coq.inria.fr/library/Coq.Lists.Streams.html ?
- kushti 11y ago
  list is inductive type for sure, not coinductive. But it could be used for modelling infinite(but countable) sequences in the sense that following property being hold: forall (m:nat), exists (l: list nat), length l > m.

Author here. I would be happy to get proof review.

by kushti 11y ago

Author here. I would be happy to get proof review.

microcolonel 11y ago

Good luck, hope you find the other person who knows what they're reading.

yodsanklai 11y ago

Could you tell us how the notions of processes, configurations and events are formalized? it seems there are a lot of axioms in your development. Are they needed?

kushti 11y ago
All those entities are used in my proof, while messages are skipped at all(so they are needed for better understanding only, while for proof's sake we can have a talk only about system's state transitions). Process is the inductive set: Inductive Process := | FinishedProcess: Binary -> Process | proceed: nat -> Process. then configuration is just a list of processes: Definition Configuration := list Process. Events are enumerated with naturals numbers, with two (abstract) functions for transition from one configuration to another, and to choose process by event: Parameter eventFn : Configuration -> nat -> Configuration. Parameter chooseFn : Configuration -> nat -> Process. We can compare processes by using chooseFn: Axiom Decidability: forall cfg n1 n2, chooseFn cfg n1 = chooseFn cfg n2 \/ chooseFn cfg n1 <> chooseFn cfg n2. and as eventFn is abstract, it seems 'run' function using eventFn needs for following axioms to be commutative: Axiom RunCommutativity: forall cfg s1 s2, run (run cfg s1) s2 = run cfg (s1 ++ s2). Axiom RunCommutativity2: forall cfg step s, run (run cfg [step]) s = run cfg (step :: s). Other axioms are following original paper pretty directly: 1. Partially correct protocol could decides on a single value only: Axiom Consistency: forall cfg, ~(decidedValue cfg true /\ decidedValue cfg false). 2. There's no change in value after consideration(termination property of a consensus algorithm): Axiom Termination: forall cfg b step, decidedValue cfg b -> decidedValue (eventFn cfg step) b. 3. "By the total correctness of P, and the fact that there are always admissible runs, V > 0" Axiom Correctness: forall cfg, bivalent cfg \/ univalent cfg. 4. As messaging is asynchronous, we can swap two events involving different processes: Axiom Async1: forall cfg step1 step2, (chooseFn cfg step1) <> (chooseFn cfg step2) -> run cfg ([step1;step2]) = run cfg ([step2;step1]). Please note, there's no any limitation on synchronicity inside a process. 5. Initial configuration properties, i.e. both values are reachable from it Axiom InitialNoConsensus: ~decided InitialConfiguration. Axiom TrueReacheable: exists s1, decidedValue (run InitialConfiguration s1) true. Axiom FalseReacheable: exists s2, decidedValue (run InitialConfiguration s2) false. While original proof considering set of applicable messages, my proof uses only randomStep function returning some possible event to happen in current configuration, and AnotherProcessStepExists axiom stating any process can make a step in any round(in my formulation, if some process is involved in any step, there's other step for other process). Axiom AnotherProcessStepExists: forall cfg step, exists step0, chooseFn cfg step <> chooseFn cfg step0. Parameter randomStep: Configuration -> nat. That's all! There are two other axioms which could be (and will be if so) proven probably, but anyway there's no doubt in them: Axiom Correctness6: forall cfg s, univalent_true cfg -> univalent_true (run cfg s). Axiom Correctness7: forall cfg s, univalent_false cfg -> univalent_false (run cfg s).
- kushti 11y ago
  Copypasted it into repos' README along with some Markdown for better readability’s sake: https://github.com/ConsensusResearch/flp https://github.com/ConsensusResearch/flp

gergoerdi 11y ago

(** A particular execution, defined by a possibly infinite sequence of events from a starting configuration C is called a schedule and the sequence of steps taken to realise the schedule is a run **) Definition Schedule := list nat. Is `list` codata by default in Coq?

CHY872 11y ago
Don't you want https://coq.inria.fr/library/Coq.Lists.Streams.html https://coq.inria.fr/library/Coq.Lists.Streams.html ?
kushti 11y ago
list is inductive type for sure, not coinductive. But it could be used for modelling infinite(but countable) sequences in the sense that following property being hold: forall (m:nat), exists (l: list nat), length l > m.