generate proofs for spinlock automatically

examples/proofs/spinlock/generated_code.v

@@ -7,40 +7,40 @@ Set Default Proof Using "Type".
 (* Generated from [examples/spinlock.c]. *)
 Section code.
   Definition file_0 : string := "examples/spinlock.c".
-  Definition loc_2 : location_info := LocationInfo file_0 6 4 6 19.
-  Definition loc_3 : location_info := LocationInfo file_0 6 4 6 14.
-  Definition loc_4 : location_info := LocationInfo file_0 6 4 6 8.
-  Definition loc_5 : location_info := LocationInfo file_0 6 4 6 8.
-  Definition loc_6 : location_info := LocationInfo file_0 6 17 6 18.
-  Definition loc_9 : location_info := LocationInfo file_0 11 4 11 23.
-  Definition loc_10 : location_info := LocationInfo file_0 12 4 14 5.
-  Definition loc_11 : location_info := LocationInfo file_0 12 4 14 5.
-  Definition loc_12 : location_info := LocationInfo file_0 12 144 14 5.
-  Definition loc_13 : location_info := LocationInfo file_0 13 8 13 21.
-  Definition loc_14 : location_info := LocationInfo file_0 12 4 14 5.
-  Definition loc_15 : location_info := LocationInfo file_0 12 4 14 5.
-  Definition loc_16 : location_info := LocationInfo file_0 13 8 13 16.
-  Definition loc_17 : location_info := LocationInfo file_0 13 19 13 20.
-  Definition loc_18 : location_info := LocationInfo file_0 12 10 12 142.
-  Definition loc_19 : location_info := LocationInfo file_0 12 10 12 130.
-  Definition loc_20 : location_info := LocationInfo file_0 12 10 12 59.
-  Definition loc_21 : location_info := LocationInfo file_0 12 60 12 71.
-  Definition loc_22 : location_info := LocationInfo file_0 12 61 12 71.
-  Definition loc_23 : location_info := LocationInfo file_0 12 61 12 65.
-  Definition loc_24 : location_info := LocationInfo file_0 12 61 12 65.
-  Definition loc_25 : location_info := LocationInfo file_0 12 73 12 82.
-  Definition loc_26 : location_info := LocationInfo file_0 12 74 12 82.
-  Definition loc_27 : location_info := LocationInfo file_0 12 84 12 85.
-  Definition loc_28 : location_info := LocationInfo file_0 12 134 12 142.
-  Definition loc_29 : location_info := LocationInfo file_0 12 141 12 142.
-  Definition loc_30 : location_info := LocationInfo file_0 11 21 11 22.
-  Definition loc_35 : location_info := LocationInfo file_0 19 4 19 74.
-  Definition loc_36 : location_info := LocationInfo file_0 19 4 19 35.
-  Definition loc_37 : location_info := LocationInfo file_0 19 36 19 47.
-  Definition loc_38 : location_info := LocationInfo file_0 19 37 19 47.
-  Definition loc_39 : location_info := LocationInfo file_0 19 37 19 41.
-  Definition loc_40 : location_info := LocationInfo file_0 19 37 19 41.
-  Definition loc_41 : location_info := LocationInfo file_0 19 49 19 50.
+  Definition loc_2 : location_info := LocationInfo file_0 8 4 8 19.
+  Definition loc_3 : location_info := LocationInfo file_0 8 4 8 14.
+  Definition loc_4 : location_info := LocationInfo file_0 8 4 8 8.
+  Definition loc_5 : location_info := LocationInfo file_0 8 4 8 8.
+  Definition loc_6 : location_info := LocationInfo file_0 8 17 8 18.
+  Definition loc_9 : location_info := LocationInfo file_0 13 4 13 23.
+  Definition loc_10 : location_info := LocationInfo file_0 15 4 17 5.
+  Definition loc_11 : location_info := LocationInfo file_0 15 4 17 5.
+  Definition loc_12 : location_info := LocationInfo file_0 15 144 17 5.
+  Definition loc_13 : location_info := LocationInfo file_0 16 8 16 21.
+  Definition loc_14 : location_info := LocationInfo file_0 15 4 17 5.
+  Definition loc_15 : location_info := LocationInfo file_0 15 4 17 5.
+  Definition loc_16 : location_info := LocationInfo file_0 16 8 16 16.
+  Definition loc_17 : location_info := LocationInfo file_0 16 19 16 20.
+  Definition loc_18 : location_info := LocationInfo file_0 15 10 15 142.
+  Definition loc_19 : location_info := LocationInfo file_0 15 10 15 130.
+  Definition loc_20 : location_info := LocationInfo file_0 15 10 15 59.
+  Definition loc_21 : location_info := LocationInfo file_0 15 60 15 71.
+  Definition loc_22 : location_info := LocationInfo file_0 15 61 15 71.
+  Definition loc_23 : location_info := LocationInfo file_0 15 61 15 65.
+  Definition loc_24 : location_info := LocationInfo file_0 15 61 15 65.
+  Definition loc_25 : location_info := LocationInfo file_0 15 73 15 82.
+  Definition loc_26 : location_info := LocationInfo file_0 15 74 15 82.
+  Definition loc_27 : location_info := LocationInfo file_0 15 84 15 85.
+  Definition loc_28 : location_info := LocationInfo file_0 15 134 15 142.
+  Definition loc_29 : location_info := LocationInfo file_0 15 141 15 142.
+  Definition loc_30 : location_info := LocationInfo file_0 13 21 13 22.
+  Definition loc_35 : location_info := LocationInfo file_0 22 4 22 74.
+  Definition loc_36 : location_info := LocationInfo file_0 22 4 22 35.
+  Definition loc_37 : location_info := LocationInfo file_0 22 36 22 47.
+  Definition loc_38 : location_info := LocationInfo file_0 22 37 22 47.
+  Definition loc_39 : location_info := LocationInfo file_0 22 37 22 41.
+  Definition loc_40 : location_info := LocationInfo file_0 22 37 22 41.
+  Definition loc_41 : location_info := LocationInfo file_0 22 49 22 50.
 
   (* Definition of struct [atomic_flag]. *)
   Program Definition struct_atomic_flag := {|

examples/proofs/spinlock/generated_proof_sl_init.v

@@ -3,6 +3,7 @@ From refinedc.examples.spinlock Require Import generated_code.
 From refinedc.examples.spinlock Require Import generated_spec.
 From refinedc.examples.spinlock Require Import spinlock_def.
 From refinedc.examples.spinlock Require Import spinlock_proof.
+From refinedc.examples.spinlock Require Import spinlock_proof.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/spinlock.c]. *)

examples/proofs/spinlock/generated_proof_sl_lock.v

@@ -13,5 +13,23 @@ Section proof_sl_lock.
   (* Typing proof for [sl_lock]. *)
   Lemma type_sl_lock :
     ⊢ typed_function impl_sl_lock type_of_sl_lock.
-  Proof. refine type_sl_lock. Qed.
+  Proof.
+    start_function "sl_lock" ([[p gamma] beta]) => arg_lock local_expected.
+    split_blocks ((
+      <[ "#1" :=
+        arg_lock ◁ₗ (p @ (&frac{beta} (spinlock (gamma)))) ∗
+        local_expected ◁ₗ (false @ (boolean (bool_it)))
+    ]> $
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "sl_lock" "#0".
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "sl_lock" "#1".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: try by rewrite /bytes_per_int/=; have ->: bytes_per_addr = 8%nat; solve_goal.
+    all: print_sidecondition_goal "sl_lock".
+  Qed.
 End proof_sl_lock.

examples/proofs/spinlock/generated_proof_sl_unlock.v

@@ -13,5 +13,16 @@ Section proof_sl_unlock.
   (* Typing proof for [sl_unlock]. *)
   Lemma type_sl_unlock :
     ⊢ typed_function impl_sl_unlock type_of_sl_unlock.
-  Proof. refine type_sl_unlock. Qed.
+  Proof.
+    start_function "sl_unlock" ([[p gamma] beta]) => arg_lock.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "sl_unlock" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "sl_unlock".
+  Qed.
 End proof_sl_unlock.

examples/proofs/spinlock/spinlock_proof.v

@@ -5,9 +5,10 @@ From refinedc.examples.spinlock Require Import spinlock_def.
 From refinedc.examples.spinlock Require Import generated_code generated_spec.
 Set Default Proof Using "Type".
 
+Typeclasses Transparent spinlock spinlocked_ex spinlock_token spinlocked_ex_token.
+
 Section type.
   Context `{!typeG Σ} `{!lockG Σ}.
-  Typeclasses Transparent spinlock spinlocked_ex spinlock_token spinlocked_ex_token.
 
 
   Lemma type_sl_init:
@@ -26,25 +27,4 @@ Section type.
     Unshelve. all: prepare_sideconditions; solve_goal.
   Qed.
 
-  Lemma type_sl_lock:
-    ⊢ typed_function impl_sl_lock type_of_sl_lock.
-  Proof.
-    start_function "sl_lock" ([[p γ] β]) => vl vexpected.
-    split_blocks ({[ "#1" := vl ◁ₗ p @ &frac{β} (spinlock γ) ∗ vexpected ◁ₗ false @ boolean bool_it ]}%I : gmap label (iProp Σ)) (∅ : gmap label (iProp Σ)).
-
-    - repeat liRStep; liShow.
-    - repeat liRStep; liShow.
-      Unshelve. all: prepare_sideconditions; try solve_goal.
-      rewrite /bytes_per_int/=. have ->: bytes_per_addr = 8%nat; solve_goal.
-  Qed.
-
-  Lemma type_sl_unlock:
-    ⊢ typed_function impl_sl_unlock type_of_sl_unlock.
-  Proof.
-    start_function "sl_unlock" ([[p γ] β]) => vl. split_blocks (∅ : gmap label (iProp Σ)) (∅ : gmap label (iProp Σ)).
-
-    repeat liRStep; liShow.
-    Unshelve. all: prepare_sideconditions; solve_goal.
-  Qed.
-
 End type.

examples/spinlock.c

 #include <stdbool.h>
 #include <spinlock.h>
 
+//@rc::import spinlock_proof from refinedc.examples.spinlock (for proofs only)
+
  [[rc::manual_proof("refinedc.examples.spinlock:spinlock_proof, type_sl_init")]]
 void sl_init(struct spinlock* lock) {
     lock->lock = 0;
 }
 
- [[rc::manual_proof("refinedc.examples.spinlock:spinlock_proof, type_sl_lock")]]
+[[rc::tactics("all: try by rewrite /bytes_per_int/=; have ->: bytes_per_addr = 8%nat; solve_goal.")]]
 void sl_lock(struct spinlock* lock) {
     bool expected = 0;
+    [[rc::inv_vars("expected : false @ boolean<bool_it>")]]
     while(atomic_compare_exchange_strong(&lock->lock, &expected, 1) == (bool)false) {
         expected = 0;
     }
 }
 
- [[rc::manual_proof("refinedc.examples.spinlock:spinlock_proof, type_sl_unlock")]]
+
 void sl_unlock(struct spinlock* lock) {
     atomic_store(&lock->lock, 0);
 }