vault backup: 2025-03-31 10:25:22

Concurrent Systems/notes/9 - Consensus.md

@@ -228,4 +228,9 @@ bmv_propose(i,v) :=
 - Wait freedom: trivial
 - Integrity: trivial
 - Agreement: by agreement of the h binary consensus objects
-- Validity: for all k, we prove that, if dec is the decided value, then there exists a j such that $p_j$ is participating
+- Validity: for all k, we prove that, if dec is the decided value, then there exists a j such that $p_j$ is participating (`PROP[j] ≠ ⊥`) and `dec[1...k] = PROP[j][1...k]`
+	- by construction, P contains the k-th bits of the proposals whose first (k-1) bits coincide with the first k-1 bits decides so far:
+		- for every  b ∈ P, there exists a j such that `PROP[j] ≠ ⊥`,
+		- `PROP[j][1..k-1] = dec[1..k-1]` and `PROP[j][k] = b`
+	-  whatever b ∈ P is selected in the k-th binary consensus, there exists a j such that `PROP[j] ≠ ⊥` and `PROP[j][1..k] = dec[1..k]`
+	- by taking `k = h`, we can conclude.