refactor spinlock

.gitignore

@@ -12,5 +12,4 @@ Makefile.coq.conf
 _opam
 /theories/examples/tutorial/tutorial
 *.timing
-*.gen
 .lia.cache

examples/include/spinlock.h

@@ -5,7 +5,6 @@
 #include <stdatomic.h>
 
 //@rc::require refinedc.examples.spinlock
-//@rc::import spinlock_annot from refinedc.examples.spinlock (for code only)
 //@rc::import spinlock_def from refinedc.examples.spinlock
 //@rc::context `{!lockG Σ}
 
@@ -22,13 +21,13 @@ void sl_init(struct spinlock* lock);
 
 [[rc::parameters("p : loc", "gamma : lock_id", "beta : own_state")]]
 [[rc::args("p @ &frac<beta, spinlock<gamma>>")]]
-[[rc::ensures("frac beta p : spinlock<gamma>", "[spinlock_token gamma []]")]]
+[[rc::ensures("frac beta p : spinlock<gamma>", "[lock_token gamma []]")]]
 void sl_lock(struct spinlock* lock);
 
 
 [[rc::parameters("p : loc", "gamma : lock_id", "beta : own_state")]]
 [[rc::args("p @ &frac<beta, spinlock<gamma>>")]]
-[[rc::requires("[spinlock_token gamma []]")]]
+[[rc::requires("[lock_token gamma []]")]]
 [[rc::ensures("frac beta p : spinlock<gamma>")]]
 [[rc::annot_args("0 : 1 LockA")]]
 void sl_unlock(struct spinlock* lock);

examples/lock.c

@@ -11,10 +11,10 @@ struct [[rc::refined_by("n1 : Z", "n2 : Z", "n3 : Z")]]
     [[rc::field("spinlock<l>")]]
     struct spinlock lock;
 
-    [[rc::field("spinlocked_ex<l, {\"locked_int\"}, n2, λ n. n @ int<size_t>>")]]
+    [[rc::field("tylocked_ex<l, {\"locked_int\"}, n2, λ n. n @ int<size_t>>")]]
     size_t locked_int;
 
-    [[rc::field("spinlocked_ex<l, {\"locked_struct\"}, n3, λ n3. ...>")]]
+    [[rc::field("tylocked_ex<l, {\"locked_struct\"}, n3, λ n3. ...>")]]
     struct [[rc::exists("a : Z", "b : Z")]]
            [[rc::constraints("{n3 = (a + b)%Z}", "{n3 ∈ size_t}")]] lock_test_inner {
 

examples/mpool.c

@@ -69,7 +69,7 @@ mpool {
   [[rc::field("spinlock<lid>")]]
   struct spinlock lock;
 
-  [[rc::field("spinlocked_ex<lid, {\"locked\"}, entries, λ entries. ...>")]]
+  [[rc::field("tylocked_ex<lid, {\"locked\"}, entries, λ entries. ...>")]]
   struct [[rc::exists("entries_in_chunks: nat", "entries_in_entry_list: nat")]]
          [[rc::constraints("{(entries = entries_in_chunks + entries_in_entry_list)%nat}")]]
     mpool_locked_inner {

examples/paper_example_2_1.c

@@ -38,7 +38,7 @@ void *alloc(struct mem_t *d, size_t size) {
 struct spinlock lock;
 
 [[rc::parameters("lid : lock_id")]]
-[[rc::global("spinlocked<lid, {\"data\"}, mem_t>")]]
+[[rc::global("tylocked<lid, {\"data\"}, mem_t>")]]
 struct mem_t data;
 
 [[rc::parameters("lid : lock_id", "n : nat")]]

examples/proofs/lock/generated_code.v

 From refinedc.lang Require Export notation.
 From refinedc.lang Require Import tactics.
 From refinedc.typing Require Import annotations.
-From refinedc.examples.spinlock Require Import spinlock_annot.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/lock.c]. *)

examples/proofs/lock/generated_spec.v

@@ -17,10 +17,10 @@ Section spec.
     struct struct_lock_test [@{type}
       (n1 @ (int (size_t))) ;
       (spinlock (l)) ;
-      (spinlocked_ex (l) ("locked_int") (n2) (λ n,
+      (tylocked_ex (l) ("locked_int") (n2) (λ n,
         n @ (int (size_t))
       )) ;
-      ((spinlocked_ex (l) ("locked_struct") (n3) (λ n3,
+      ((tylocked_ex (l) ("locked_struct") (n3) (λ n3,
         tyexists (λ a : Z,
         tyexists (λ b : Z,
         constrained (struct struct_lock_test_inner [@{type}
@@ -52,10 +52,10 @@ Section spec.
       struct struct_lock_test [@{type}
         (n1 @ (int (size_t))) ;
         (spinlock (l)) ;
-        (spinlocked_ex (l) ("locked_int") (n2) (λ n,
+        (tylocked_ex (l) ("locked_int") (n2) (λ n,
           n @ (int (size_t))
         )) ;
-        ((spinlocked_ex (l) ("locked_struct") (n3) (λ n3,
+        ((tylocked_ex (l) ("locked_struct") (n3) (λ n3,
           tyexists (λ a : Z,
           tyexists (λ b : Z,
           constrained (struct struct_lock_test_inner [@{type}
@@ -105,11 +105,11 @@ Section spec.
   (* Specifications for function [sl_lock]. *)
   Definition type_of_sl_lock :=
     fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); True)
-      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (spinlock_token gamma []).
+      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (lock_token gamma []).
 
   (* Specifications for function [sl_unlock]. *)
   Definition type_of_sl_unlock :=
-    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (spinlock_token gamma []))
+    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (lock_token gamma []))
       → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))).
 
   (* Specifications for function [init]. *)

examples/proofs/mpool/generated_code.v

 From refinedc.lang Require Export notation.
 From refinedc.lang Require Import tactics.
 From refinedc.typing Require Import annotations.
-From refinedc.examples.spinlock Require Import spinlock_annot.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/mpool.c]. *)

examples/proofs/mpool/generated_spec.v

@@ -134,7 +134,7 @@ Section spec.
     constrained (struct struct_mpool [@{type}
       (entry_size @ (int (size_t))) ;
       (spinlock (lid)) ;
-      ((spinlocked_ex (lid) ("locked") (entries) (λ entries,
+      ((tylocked_ex (lid) ("locked") (entries) (λ entries,
         tyexists (λ entries_in_chunks : nat,
         tyexists (λ entries_in_entry_list : nat,
         constrained (struct struct_mpool_locked_inner [@{type}
@@ -169,7 +169,7 @@ Section spec.
       constrained (struct struct_mpool [@{type}
         (entry_size @ (int (size_t))) ;
         (spinlock (lid)) ;
-        ((spinlocked_ex (lid) ("locked") (entries) (λ entries,
+        ((tylocked_ex (lid) ("locked") (entries) (λ entries,
           tyexists (λ entries_in_chunks : nat,
           tyexists (λ entries_in_entry_list : nat,
           constrained (struct struct_mpool_locked_inner [@{type}
@@ -225,11 +225,11 @@ Section spec.
   (* Specifications for function [sl_lock]. *)
   Definition type_of_sl_lock :=
     fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); True)
-      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (spinlock_token gamma []).
+      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (lock_token gamma []).
 
   (* Specifications for function [sl_unlock]. *)
   Definition type_of_sl_unlock :=
-    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (spinlock_token gamma []))
+    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (lock_token gamma []))
       → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))).
 
   (* Specifications for function [round_pointer_up]. *)

examples/proofs/paper_example_2_1/generated_code.v

 From refinedc.lang Require Export notation.
 From refinedc.lang Require Import tactics.
 From refinedc.typing Require Import annotations.
-From refinedc.examples.spinlock Require Import spinlock_annot.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/paper_example_2_1.c]. *)

examples/proofs/paper_example_2_1/generated_proof_thread_safe_alloc.v

@@ -13,7 +13,7 @@ Section proof_thread_safe_alloc.
   Lemma type_thread_safe_alloc (global_data global_lock global_alloc global_sl_lock global_sl_unlock : loc) :
     global_locs !! "data" = Some global_data →
     global_locs !! "lock" = Some global_lock →
-    global_initialized_types !! "data" = Some (GT lock_id (λ 'lid, (spinlocked (lid) ("data") (mem_t)) : type)) →
+    global_initialized_types !! "data" = Some (GT lock_id (λ 'lid, (tylocked (lid) ("data") (mem_t)) : type)) →
     global_initialized_types !! "lock" = Some (GT lock_id (λ 'lid, (spinlock (lid)) : type)) →
     global_alloc ◁ᵥ global_alloc @ function_ptr type_of_alloc -∗
     global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -∗

examples/proofs/paper_example_2_1/generated_spec.v

@@ -80,11 +80,11 @@ Section spec.
   (* Specifications for function [sl_lock]. *)
   Definition type_of_sl_lock :=
     fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); True)
-      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (spinlock_token gamma []).
+      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (lock_token gamma []).
 
   (* Specifications for function [sl_unlock]. *)
   Definition type_of_sl_unlock :=
-    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (spinlock_token gamma []))
+    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (lock_token gamma []))
       → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))).
 
   (* Specifications for function [alloc]. *)

examples/proofs/paper_example_2_2/generated_code.v

 From refinedc.lang Require Export notation.
 From refinedc.lang Require Import tactics.
 From refinedc.typing Require Import annotations.
-From refinedc.examples.spinlock Require Import spinlock_annot.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/paper_example_2_2.c]. *)

examples/proofs/paper_example_2_2/generated_spec.v

@@ -90,11 +90,11 @@ Section spec.
   (* Specifications for function [sl_lock]. *)
   Definition type_of_sl_lock :=
     fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); True)
-      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (spinlock_token gamma []).
+      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (lock_token gamma []).
 
   (* Specifications for function [sl_unlock]. *)
   Definition type_of_sl_unlock :=
-    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (spinlock_token gamma []))
+    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (lock_token gamma []))
       → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))).
 
   (* Specifications for function [free]. *)

examples/proofs/spinlock/generated_code.v

 From refinedc.lang Require Export notation.
 From refinedc.lang Require Import tactics.
 From refinedc.typing Require Import annotations.
-From refinedc.examples.spinlock Require Import spinlock_annot.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/spinlock.c]. *)

examples/proofs/spinlock/generated_spec.v

@@ -22,10 +22,10 @@ Section spec.
   (* Specifications for function [sl_lock]. *)
   Definition type_of_sl_lock :=
     fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); True)
-      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (spinlock_token gamma []).
+      → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))) ∗ (lock_token gamma []).
 
   (* Specifications for function [sl_unlock]. *)
   Definition type_of_sl_unlock :=
-    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (spinlock_token gamma []))
+    fn(∀ (p, gamma, beta) : loc * lock_id * own_state; (p @ (&frac{beta} (spinlock (gamma)))); (lock_token gamma []))
       → ∃ () : (), (void); (p ◁ₗ{beta} (spinlock (gamma))).
 End spec.

examples/proofs/spinlock/spinlock_annot.v

-Inductive LockAnnot : Type := LockA | UnlockA.

examples/proofs/spinlock/spinlock_def.v

 From refinedc.typing Require Import typing.
-From refinedc.examples.spinlock Require Import spinlock_annot generated_code.
-From iris.algebra Require Import csum excl auth cmra_big_op.
-From iris.algebra Require Import big_op gset frac agree.
+From refinedc.examples.spinlock Require Import generated_code.
 Set Default Proof Using "Type".
 
-Definition lockN : namespace := nroot.@"lockN".
-Definition lock_id := gname.
-
-(** Registering the necessary ghost state. *)
-Class lockG Σ := LockG {
-   lock_inG :> inG Σ (authR (gset_disjUR string));
-   lock_excl_inG :> inG Σ (exclR unitO);
-}.
-Definition lockΣ : gFunctors :=
-  #[GFunctor (constRF (authR (gset_disjUR string)));
-    GFunctor (constRF (exclR unitO))].
-Instance subG_lockG {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. solve_inG. Qed.
-
 Section type.
   Context `{!typeG Σ} `{!lockG Σ}.
 
-  Definition spinlock_token (γ : lock_id) (l : list string) : iProp Σ :=
-    ∃ s : gset string, ⌜l ≡ₚ elements s⌝ ∗ own γ (● GSet s).
-
   Definition spinlock (γ : lock_id) : type :=
-    struct struct_spinlock [atomic_bool bool_it True (spinlock_token γ [])].
+    struct struct_spinlock [atomic_bool bool_it True (lock_token γ [])].
 
   Global Program Instance movable_spinlock γ : Movable (spinlock γ) := ltac:(apply: movable_struct).
 
-  Program Definition spinlocked_ex {A} (γ : lock_id) (n : string) (x : A) (ty : A → type) : type := {|
-    ty_own β l := (match β return _ with
-                  | Own => l ◁ₗ ty x
-                  | Shr => ∃ γ', inv lockN ((∃ x', l ◁ₗ ty x' ∗ own γ' (Excl ()))  ∨ own γ (◯ GSet {[ n ]}))
-                  end)%I
-  |}.
-  Next Obligation.
-    iIntros (A γ n x ty l E HE) "Hl".
-    iMod (own_alloc (Excl ())) as (γ') "Hown" => //.
-    iExists _. iApply inv_alloc. iIntros "!#". iLeft. iExists _. by iFrame.
-  Qed.
-
-  Global Program Instance movable_spinlocked_ex A γ n x (ty : A → type) `{!Movable (ty x)}: Movable (spinlocked_ex γ n x ty) := {|
-    ty_layout := (ty x).(ty_layout);
-    ty_own_val v := (v ◁ᵥ (ty x))%I;
-  |}.
-  Next Obligation. iIntros (A γ n x ty ? v) "Hl". by iApply ty_aligned. Qed.
-  Next Obligation. iIntros (A γ n x ty ? v) "Hl". by iApply ty_size_eq. Qed.
-  Next Obligation. iIntros (A γ n x ty ? l) "Hl". by iApply ty_deref. Qed.
-  Next Obligation. iIntros (A γ n x ty ? l l') "Hl". by iApply ty_ref. Qed.
-
-
   Lemma spinlock_subsume γ1 γ2 l T β:
     ⌜γ1 = γ2⌝ ∗ T -∗
     subsume (l ◁ₗ{β} spinlock γ1) (l ◁ₗ{β} spinlock γ2) T.
   Proof. iIntros "[-> $] $". Qed.
-
   Global Instance spinlock_subsume_inst γ1 γ2 l β:
     Subsume (l ◁ₗ{β} spinlock γ1) (l ◁ₗ{β} spinlock γ2) :=
     λ T, i2p (spinlock_subsume γ1 γ2 l T β).
 
-  Lemma spinlocked_simplify_hyp_place A γ n x (ty : A → type) T l:
-    (l ◁ₗ ty x -∗ T)  -∗
-    simplify_hyp (l ◁ₗ spinlocked_ex γ n x ty) T.
-  Proof. done. Qed.
-  Global Instance spinlocked_simplify_hyp_place_inst A γ n x (ty : A → type) l:
-    SimplifyHypPlace l Own (spinlocked_ex γ n x ty) (Some 0%N) :=
-    λ T, i2p (spinlocked_simplify_hyp_place A γ n x ty T l).
-
-  Lemma spinlocked_simplify_goal_place A γ n x (ty : A → type) T l:
-    T (l ◁ₗ ty x) -∗
-    simplify_goal (l ◁ₗ spinlocked_ex γ n x ty) T.
-  Proof. iIntros "HT". iExists _. iFrame. iIntros "$". Qed.
-
-  Global Instance spinlocked_simplify_goal_place_inst A γ n x (ty : A → type) l:
-    SimplifyGoalPlace l Own (spinlocked_ex γ n x ty) (Some 0%N) :=
-    λ T, i2p (spinlocked_simplify_goal_place A γ n x ty T l).
-
-  Lemma spinlocked_subsume A γ n x1 x2 (ty : A → type) l β T:
-    ⌜β = Own → x1 = x2⌝ ∗ T -∗
-    subsume (l ◁ₗ{β} spinlocked_ex γ n x1 ty) (l ◁ₗ{β} spinlocked_ex γ n x2 ty) T.
-  Proof. iIntros "[% $] Hl". by destruct β; naive_solver. Qed.
-  Global Instance spinlocked_subsume_inst A γ n x1 x2 (ty : A → type) l β:
-    Subsume (l ◁ₗ{β} spinlocked_ex γ n x1 ty) (l ◁ₗ{β} spinlocked_ex γ n x2 ty) | 10 :=
-    λ T, i2p (spinlocked_subsume A γ n x1 x2 ty l β T).
-
-  Definition spinlocked_ex_token {A} (γ : lock_id) (n : string) (l : loc) (β : own_state) (ty : A → type)  : iProp Σ :=
-    (∀ E x, ⌜↑lockN ⊆ E⌝ -∗ l ◁ₗ ty x ={E}=∗ l ◁ₗ{β} spinlocked_ex γ n x ty ∗ own γ (◯ GSet {[ n ]}))%I.
-
-  Lemma locked_open A n s l γ (x : A) ty β E:
-    n ∉ s → ↑lockN ⊆ E →
-    l ◁ₗ{β} spinlocked_ex γ n x ty -∗
-      spinlock_token γ s ={E}=∗
-      ▷ ∃ x', l ◁ₗ ty x' ∗ spinlock_token γ (n :: s) ∗ spinlocked_ex_token γ n l β ty ∗ ⌜β = Own → x = x'⌝.
-  Proof.
-    iIntros (Hnotin ?) "Hl Hown".
-    iDestruct "Hown" as (st Hperm) "Hown". rewrite ->Hperm in Hnotin.
-    iMod (own_update with "Hown") as "[Hown Hs]". { eapply auth_update_alloc.
-      apply (gset_disj_alloc_empty_local_update st {[n]}). set_solver. }
-    rewrite {1}/ty_own /=.
-    iAssert (spinlock_token γ (n :: s)) with "[Hown]" as "$". {
-      iExists _. iFrame. iPureIntro. rewrite Hperm elements_union_singleton //. set_solver.
-    }
-    destruct β. { iIntros "!# !#". iExists _. iFrame. iSplit => //. by iIntros (???) "$". }
-    iDestruct "Hl" as (γ') "#Hinv".
-    iInv "Hinv" as "[Hl|>Hn]" "Hc". 2: {
-      iDestruct (own_valid_2 with "Hs Hn") as %Hown. exfalso. move: Hown.
-      rewrite -auth_frag_op auth_frag_valid gset_disj_valid_op. set_solver.
-    }
-    iMod ("Hc" with "[Hs]") as "_". by iRight.
-    iIntros "!# !#". iDestruct "Hl" as (x') "[Hl Hexcl]".
-    iExists _. iFrame. iSplitL => //.
-    (** locked_token *)
-    iIntros (E' x'' ?) "Hl".
-    iInv "Hinv" as "[H|>$]" "Hc". 1: {
-      have ? : Inhabited A by apply (populate x).
-      iDestruct "H" as (?) "[_ >He]".
-        by iDestruct (own_valid_2 with "Hexcl He") as %Hown%exclusive_l.
-    }
-    iMod ("Hc" with "[Hl Hexcl]") as "_". 2: by iExists _.
-    iModIntro. iLeft. iExists _. iFrame.
-  Qed.
-
-  Lemma locked_close A n s l γ (x : A) ty β E:
-    ↑lockN ⊆ E →
-    spinlocked_ex_token γ n l β ty -∗ l ◁ₗ ty x -∗ spinlock_token γ (n :: s) ={E}=∗
-    spinlock_token γ s ∗ l ◁ₗ{β} spinlocked_ex γ n x ty.
-  Proof.
-    iIntros (HE) "Hlocked Hl Hlock".
-    iMod ("Hlocked" with "[//] Hl") as "[$ Hn]".
-    iDestruct "Hlock" as (st Hst) "Htok".
-    iExists (st ∖ {[n]}). iSplitR. {
-      iPureIntro. move: (Hst). rewrite {1}(union_difference_L {[n]} st).
-      rewrite ->elements_union_singleton => ?; last set_solver.
-      by apply: Permutation.Permutation_cons_inv.
-      set_unfold => ??. subst. apply elem_of_elements. rewrite -Hst. set_solver.
-    }
-    iCombine "Htok" "Hn" as "Htok".
-    iMod (own_update with "Htok") as "$" => //.
-    eapply auth_update_dealloc.
-      by apply gset_disj_dealloc_local_update.
-  Qed.
-
-  Lemma annot_unlock A l T β γ n ty (x : A):
-    (find_in_context (FindDirect (spinlock_token γ)) (λ s : list string, ⌜n∉s⌝ ∗ (∀ x',
-        spinlock_token γ (n :: s) -∗ spinlocked_ex_token γ n l β ty -∗ ⌜β = Own → x = x'⌝ -∗
-                       l ◁ₗ ty x' -∗ T))) -∗
-    typed_annot_stmt UnlockA l β (spinlocked_ex γ n x ty) T.
-  Proof.
-    iDestruct 1 as (s) "(Hs&%&HT)". iIntros "Hlocked".
-    iMod (locked_open with "Hlocked Hs") as "Htok" => //.
-    iApply step_fupd_intro => //. iModIntro.
-    iDestruct "Htok" as (x') "(Hl&Hs&Htok&%)".
-    by iApply ("HT" with "Hs Htok [//] Hl").
-  Qed.
-  Global Instance annot_unlock_inst A l β γ n ty (x : A):
-    TypedAnnotStmt UnlockA l β (spinlocked_ex γ n x ty) :=
-    λ T, i2p (annot_unlock A l T β γ n ty x).
-
-
-  Lemma type_annot_lock (l : loc) (ty : mtype) T:
-    (∃ β γ, subsume (l ◁ᵥ ty) (l ◁ₗ{β} spinlock γ) (
-      find_in_context (FindDirect (spinlock_token γ)) (λ s : list string, foldr (λ t T,
-        find_in_context (FindDirect (λ '(existT A (l2, ty)), spinlocked_ex_token (A:=A) γ t l2 β ty)) (λ '(existT A (l2, ty)), ∃ x,
-          l2 ◁ₗ ty x ∗ (l2 ◁ₗ{β} spinlocked_ex γ t x ty -∗ T))) (l ◁ₗ{β} spinlock γ -∗ spinlock_token γ [] -∗ T) s))) -∗
-    typed_annot_expr 1%nat LockA l ty T.
-  Proof.
-    iDestruct 1 as (β γ) "Hsub". iIntros "Hl".
-    iDestruct ("Hsub" with "Hl") as "[Hlock H]".
-    iDestruct "H" as (s) "[Htok Hs]".
-    iApply step_fupd_intro => //. iModIntro.
-    iInduction s as [|t s] "IH" => /=. by iApply ("Hs" with "Hlock Htok").
-    iDestruct "Hs" as ([A [l2 ty2]]) "[Hlt H]".
-    iDestruct "H" as (x) "[Hl HT]".
-    iMod (locked_close with "Hlt Hl Htok") as "[Htok Hl]" => //.
-    iApply ("IH" with "Hlock Htok"). by iApply "HT".
-  Qed.
-  Global Instance type_annot_lock_inst (l : loc) ty :
-    TypedAnnotExpr 1%nat LockA l ty :=
-    λ T, i2p (type_annot_lock l ty T).
+  Global Instance spinlock_with_lock_id γ : WithLockId (spinlock γ) γ := I.
 End type.
 
-(* TODO> DO something stronger, e.g. sealing? *)
-Typeclasses Opaque spinlock spinlocked_ex spinlock_token spinlocked_ex_token.
-Notation spinlocked γ n ty := (spinlocked_ex γ n tt (λ _, ty)).
-Notation spinlocked_token γ n l β ty := (spinlocked_ex_token γ n l β (λ _ : unit, ty)).
+Typeclasses Opaque spinlock.

examples/proofs/spinlock/spinlock_proof.v

@@ -5,7 +5,7 @@ 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.
+Typeclasses Transparent spinlock.
 
 Section type.
   Context `{!typeG Σ} `{!lockG Σ}.
@@ -16,10 +16,7 @@ Section type.
   Proof.
     start_function "sl_init" (p) => vl. split_blocks (∅ : gmap label (iProp Σ)) (∅ : gmap label (iProp Σ)).
 
-    iApply fupd_typed_stmt.
-    iMod (own_alloc (● GSet ∅)) as (γ) "Hown"; [ by apply auth_auth_valid |].
-    iAssert (spinlock_token γ []) with "[Hown]" as "?"; [ by iExists _; iFrame |].
-    iModIntro.
+    iApply fupd_typed_stmt. iMod alloc_lock_token as (γ) "?". iModIntro.
 
     repeat liRStep; liShow.
     liInst Hevar γ.

linux/pkvm/early_alloc.c

@@ -45,11 +45,9 @@ extern void clear_page(void *to);
 
 [[rc::parameters("base : loc", "given : nat", "remaining : nat", "n : nat")]]
 [[rc::args("n @ int<u32>")]]
-[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
-[[rc::returns("{0%nat < n ≤ remaining} @ optional<&own<uninit<PAGES<n>>>>")]]
-[[rc::ensures("global mem : {if bool_decide (0%nat < n ≤ remaining) then "
-                            "(base, given + n, remaining - n)%nat else "
-                            "(base, given, remaining)} @ region")]]
+[[rc::requires("global mem : {(base, given, remaining)} @ region", "{0%nat < n ≤ remaining}")]]
+[[rc::returns("&own<uninit<PAGES<n>>>")]]
+[[rc::ensures("global mem : {(base, given + n, remaining - n)%nat} @ region")]]
 [[rc::trust_me]] // FIXME
 void *hyp_early_alloc_contig(unsigned int nr_pages){
   uintptr_t ret = cur, p;
@@ -73,18 +71,11 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
   return rc_copy_alloc_id((void *) ret, base);
 }
 
-//[[rc::parameters("n : nat")]]
-//[[rc::args("uninit<void*>")]]
-//[[rc::requires("global mem : n @ region")]]
-//[[rc::returns("{n ≠ 0%nat} @ optional<&own<uninit<PAGE>>>")]]
-//[[rc::ensures("global mem : {if bool_decide (n ≠ 0%nat) then (n - 1)%nat else n} @ region")]]
 [[rc::parameters("base : loc", "given : nat", "remaining : nat")]]
 [[rc::args("uninit<void*>")]]
-[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
-[[rc::returns("{remaining ≠ 0%nat} @ optional<&own<uninit<PAGE>>>")]]
-[[rc::ensures("global mem : {if bool_decide (remaining ≠ 0%nat) then "
-                            "(base, given + 1, remaining - 1)%nat else "
-                            "(base, given, remaining)} @ region")]]
+[[rc::requires("global mem : {(base, given, remaining)} @ region", "{remaining ≠ 0%nat}")]]
+[[rc::returns("&own<uninit<PAGE>>")]]
+[[rc::ensures("global mem : {(base, given + 1, remaining - 1)%nat} @ region")]]
 void *hyp_early_alloc_page(void *arg){
   return hyp_early_alloc_contig(1);
 }