vault backup: 2025-03-31 10:17:33

Concurrent Systems/notes/9 - Consensus.md

@@ -215,10 +215,17 @@ IDEA: decide bit by bit the final outcome
 PROP[1..n][1..h] array of n h-bits proposals, all init at ⊥ BC[1..h] array of h binary consensus objects
 
 bmv_propose(i,v) :=
-	PROP[i] <- binary_repr_h(v)
+	PROP[i] <- binary_repr_h(v) # scrivo la rappresentazione binaria
 	for k=1 to h do
 		P <- {PROP[j][k] | PROP[j]≠⊥ ∧ PROP[j][1..k-1]=res[1..k-1]}
 		let b be an element of P
 		res[k] <- BC[k].propose(b)
 	return value(res)
 ```
+(exercise: remove `∧ PROP[j][1..k-1]=res[1..k-1]` and execution in which a consensus property can be broken)
+
+*Proof:*
+- 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