Prove insertion sort

Author: yunshengtw

src/program_proof/tulip/paxos/program/paxos_ascend.v

@@ -32,8 +32,8 @@ Section ascend.
     iIntros "[%Hsz Hrespp]".
     iNamed "Hpx".
     wp_apply (wp_Paxos__cquorum with "Hsc").
-    iIntros (ok) "[Hsc %Hquorum]".
-    wp_if_destruct.
+    iIntros "Hsc".
+    case_bool_decide as Hquorum; wp_pures; last first.
     { iApply "HΦ".
       iFrame "HtermcP HtermlP HiscandP HlogP HentspP".
       by iFrame "∗ # %".

src/program_proof/tulip/paxos/program/paxos_cquorum.v

@@ -1,5 +1,6 @@
 From Perennial.program_proof.tulip.paxos Require Import prelude.
 From Perennial.program_proof.tulip.paxos.program Require Import repr.
+From Perennial.program_proof.tulip.program Require Import quorum.
 From Goose.github_com.mit_pdos.tulip Require Import paxos quorum.
 
 Section cquorum.
@@ -8,11 +9,26 @@ Section cquorum.
   Theorem wp_Paxos__cquorum (px : loc) (n : u64) nids :
     {{{ own_paxos_sc px nids }}}
       Paxos__cquorum #px #n
-    {{{ (ok : bool), RET #ok; own_paxos_sc px nids ∗ ⌜size nids / 2 < uint.Z n⌝ }}}.
+    {{{ RET #(bool_decide (size nids / 2 < uint.Z n)); own_paxos_sc px nids }}}.
   Proof.
+    iIntros (Φ) "Hpx HΦ".
+    wp_rec.
+
     (*@ func (px *Paxos) cquorum(n uint64) bool {                               @*)
     (*@     return quorum.ClassicQuorum(px.sc) <= n                             @*)
     (*@ }                                                                       @*)
-  Admitted.
+    iNamed "Hpx".
+    wp_loadField.
+    wp_apply wp_ClassicQuorum.
+    iIntros (x Hx).
+    wp_pures.
+    case_bool_decide as Hc1.
+    { case_bool_decide as Hc2; last word.
+      iApply "HΦ". by iFrame "∗ %".
+    }
+    { case_bool_decide as Hc2; first word.
+      iApply "HΦ". by iFrame "∗ %".
+    }
+  Qed.
 
 End cquorum.

src/program_proof/tulip/paxos/program/paxos_push.v

@@ -34,9 +34,9 @@ Section push.
     wp_apply (wp_MapLen with "Hlsnpeers").
     iIntros "[%Hszlsnpeers Hlsnpeers]".
     wp_apply (wp_Paxos__cquorum with "Hsc").
-    iIntros (ok) "[Hsc %Hqsize]".
+    iIntros "Hsc".
     (* Not using [wp_if_destruct] to prevent it eating equality about [nids]. *)
-    destruct ok eqn:Hok; last first.
+    case_bool_decide as Hqsize; wp_pures; last first.
     { wp_pures.
       iApply "HΦ".
       iFrame "Hcand".