Formalize stability as a special case of fpaxos

mit-pdos · Nov 2, 2024 · 0f21fb9 · 0f21fb9
1 parent fda28ed
commit 0f21fb9
Show file tree

Hide file tree

Showing 3 changed files with 488 additions and 5 deletions.
diff --git a/src/program_proof/rsm/fpaxos_inv.v b/src/program_proof/rsm/fpaxos_inv.v
@@ -554,7 +554,7 @@ Section pure.
     { by apply map_subseteq_size, map_filter_subseteq_mono. }
     pose proof (nfast_nfastneg_dom_size bs n v) as Hsize.
     epose proof (quorums_sufficient _ _ _ Hqc Hqf) as Hsuff.
-    lia.
+    clear -Hsizef Hf Hsize Hc Hsizec Hsuff. lia.
   Qed.
 
   Lemma vp_impl_pac bs ps :

diff --git a/src/program_proof/rsm/pure/quorum.v b/src/program_proof/rsm/pure/quorum.v
@@ -94,9 +94,8 @@ Section lemma.
     fquorum_size c qf ->
     2 * size c < size qc + 2 * size qf.
   Proof.
+    rewrite /cquorum_size /fquorum_size.
     intros Hsizec Hsizef.
-    unfold cquorum_size in Hsizec.
-    unfold fquorum_size in Hsizef.
     lia.
   Qed.
 
@@ -119,4 +118,12 @@ Section lemma.
     lia.
   Qed.
 
+  Lemma fquorum_non_empty_q c q :
+    fquorum c q -> q ≠ ∅.
+  Proof.
+    intros (Hincl & Hsize & Hnz).
+    rewrite -size_non_empty_iff_L.
+    lia.
+  Qed.
+
 End lemma.