Started with latch

theories/examples/latch/latch.c

+#include <stdbool.h>
+#include "latch.h"
+
+ [[rc::manual_proof("refinedc.examples.latch:latch_proof, type_latch_wait")]]
+void latch_wait(struct latch* latch) {
+  bool expected = false;
+  while(atomic_compare_exchange_strong(&latch->released, &expected, false) == (bool)true) {
+    expected = false;
+  }
+  // TODO: replace the code with the code below once atomic_load is implemented
+  /* while(atomic_load(&latch->released) == (_Bool)false) {} */
+}
+
+[[rc::manual_proof("refinedc.examples.latch:latch_proof, type_latch_release")]]
+void latch_release(struct latch* latch) {
+  atomic_store(&latch->released, true);
+}

theories/examples/latch/latch.h

+#ifndef LATCH_H
+#define LATCH_H
+
+#include <stddef.h>
+#include <stdbool.h>
+#include <stdatomic.h>
+
+//@rc::import latch_def from refinedc.examples.latch
+
+struct latch {
+    atomic_bool released;
+};
+
+#define LATCH_INIT ((struct latch){.released = false})
+
+[[rc::parameters("p : loc", "beta : own_state", "P : {iProp Σ}")]]
+[[rc::args("p @ &frac<beta, latch<P>>")]]
+[[rc::ensures("p @ &frac<beta, latch<P>>", "[P]")]]
+void latch_wait(struct latch* latch);
+
+[[rc::parameters("p : loc", "beta : own_state", "P : {iProp Σ}")]]
+[[rc::args("p @ &frac<beta, latch<P>>")]]
+[[rc::requires("[P]")]]
+[[rc::ensures("p @ &frac<beta, latch<P>>")]]
+void latch_release(struct latch* latch);
+
+#endif

theories/examples/latch/latch_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [theories/examples/latch/latch.c]. *)
+Section code.
+  Definition file_0 : string := "theories/examples/latch/latch.c".
+  Definition loc_2 : location_info := LocationInfo file_0 6 2 6 21.
+  Definition loc_3 : location_info := LocationInfo file_0 7 2 9 3.
+  Definition loc_4 : location_info := LocationInfo file_0 7 2 9 3.
+  Definition loc_5 : location_info := LocationInfo file_0 7 147 9 3.
+  Definition loc_6 : location_info := LocationInfo file_0 8 4 8 17.
+  Definition loc_7 : location_info := LocationInfo file_0 7 2 9 3.
+  Definition loc_8 : location_info := LocationInfo file_0 7 2 9 3.
+  Definition loc_9 : location_info := LocationInfo file_0 8 4 8 12.
+  Definition loc_10 : location_info := LocationInfo file_0 8 15 8 16.
+  Definition loc_11 : location_info := LocationInfo file_0 7 8 7 145.
+  Definition loc_12 : location_info := LocationInfo file_0 7 8 7 133.
+  Definition loc_13 : location_info := LocationInfo file_0 7 8 7 57.
+  Definition loc_14 : location_info := LocationInfo file_0 7 58 7 74.
+  Definition loc_15 : location_info := LocationInfo file_0 7 59 7 74.
+  Definition loc_16 : location_info := LocationInfo file_0 7 59 7 64.
+  Definition loc_17 : location_info := LocationInfo file_0 7 59 7 64.
+  Definition loc_18 : location_info := LocationInfo file_0 7 76 7 85.
+  Definition loc_19 : location_info := LocationInfo file_0 7 77 7 85.
+  Definition loc_20 : location_info := LocationInfo file_0 7 87 7 88.
+  Definition loc_21 : location_info := LocationInfo file_0 7 137 7 145.
+  Definition loc_22 : location_info := LocationInfo file_0 7 144 7 145.
+  Definition loc_23 : location_info := LocationInfo file_0 6 19 6 20.
+  Definition loc_28 : location_info := LocationInfo file_0 16 2 16 77.
+  Definition loc_29 : location_info := LocationInfo file_0 16 2 16 33.
+  Definition loc_30 : location_info := LocationInfo file_0 16 34 16 50.
+  Definition loc_31 : location_info := LocationInfo file_0 16 35 16 50.
+  Definition loc_32 : location_info := LocationInfo file_0 16 35 16 40.
+  Definition loc_33 : location_info := LocationInfo file_0 16 35 16 40.
+  Definition loc_34 : location_info := LocationInfo file_0 16 52 16 53.
+
+  (* Definition of struct [atomic_flag]. *)
+  Program Definition struct_atomic_flag := {|
+    sl_members := [
+      (Some "_Value", it_layout bool_it)
+    ];
+  |}.
+  Solve Obligations with solve_struct_obligations.
+
+  (* Definition of struct [latch]. *)
+  Program Definition struct_latch := {|
+    sl_members := [
+      (Some "released", it_layout bool_it)
+    ];
+  |}.
+  Solve Obligations with solve_struct_obligations.
+
+  (* Definition of function [latch_wait]. *)
+  Definition impl_latch_wait : function := {|
+    f_args := [
+      ("latch", LPtr)
+    ];
+    f_local_vars := [
+      ("expected", it_layout bool_it)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "expected" <-{ it_layout bool_it }
+          LocInfoE loc_23 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_23 (i2v 0 i32))) ;
+        locinfo: loc_3 ;
+        Goto "#1"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_11 ;
+        if: LocInfoE loc_11 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_11 ((LocInfoE loc_12 (CAS
+            (IntOp bool_it)
+            (LocInfoE loc_14 (&(LocInfoE loc_15 ((LocInfoE loc_16 (!{LPtr} (LocInfoE loc_17 ("latch")))) at{struct_latch} "released"))))
+            (LocInfoE loc_18 (&(LocInfoE loc_19 ("expected"))))
+            (LocInfoE loc_20 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_20 (i2v 0 i32)))))) ={IntOp bool_it, IntOp bool_it} (LocInfoE loc_21 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_22 (i2v 1 i32)))))))
+        then
+        locinfo: loc_6 ;
+          Goto "#2"
+        else
+        Goto "#3"
+      ]> $
+      <[ "#2" :=
+        locinfo: loc_6 ;
+        LocInfoE loc_9 ("expected") <-{ it_layout bool_it }
+          LocInfoE loc_10 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_10 (i2v 0 i32))) ;
+        locinfo: loc_7 ;
+        Goto "continue2"
+      ]> $
+      <[ "#3" :=
+        Return (VOID)
+      ]> $
+      <[ "continue2" :=
+        locinfo: loc_3 ;
+        Goto "#1"
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [latch_release]. *)
+  Definition impl_latch_release : function := {|
+    f_args := [
+      ("latch", LPtr)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_28 ;
+        LocInfoE loc_31 ((LocInfoE loc_32 (!{LPtr} (LocInfoE loc_33 ("latch")))) at{struct_latch} "released") <-{ it_layout bool_it, ScOrd }
+          LocInfoE loc_34 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_34 (i2v 1 i32))) ;
+        Return (VOID)
+      ]> $∅
+    )%E
+  |}.
+End code.

theories/examples/latch/latch_def.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.latch Require Import latch_code.
+Set Default Proof Using "Type".
+
+Definition latchN : namespace := nroot.@"lockN".
+
+Section type.
+  Context `{!typeG Σ}.
+
+  Program Definition latch (P : iProp Σ) : type := {|
+    ty_own β l := (match β return _ with
+                  | Own => ∃ b, l ◁ₗ struct struct_latch [b @ boolean u8] ∗ if b then □ P else True
+                  | Shr => ⌜l at{struct_latch}ₗ "released" `has_layout_loc` bool_it⌝ ∗
+                          l ◁ₗ{Shr} struct struct_latch [ singleton_place (l at{struct_latch}ₗ "released")] ∗
+                          inv latchN (∃ b, l at{struct_latch}ₗ "released" ↦ i2v (Z_of_bool b) u8 ∗
+                                            if b then □ P else True)
+                  end)%I
+  |}.
+  Next Obligation.
+    iIntros (γ l E HE) => /=. rewrite /ty_own/=. iDestruct 1 as (b) "[[$ [% [Hs _]]] Hown]".
+    iDestruct (ty_aligned with "Hs") as %?. iSplitR => //. iSplitR => //.
+    iApply inv_alloc. iIntros "!#". iExists b. iFrame.
+    (* TODO: don't unfold here *)
+    rewrite /boolean/boolean_inner_type/int_inner_type.
+    iDestruct "Hs" as (v Hv ?) "Hv" => /=. rewrite /GetMemberLoc/= /val_of_bool/i2v Hv. iFrame.
+  Qed.
+
+  Lemma latch_subsume P1 P2 l T β:
+    ⌜P1 = P2⌝ ∗ T -∗
+    subsume (l ◁ₗ{β} latch P1) (l ◁ₗ{β} latch P2) T.
+  Proof. iIntros "[-> $] $". Qed.
+
+  Global Instance latch_subsume_inst P1 P2 l β:
+    Subsume (l ◁ₗ{β} latch P1) (l ◁ₗ{β} latch P2) :=
+    λ T, i2p (latch_subsume P1 P2 l T β).
+
+  Definition LATCH_INIT := val_of_bool false.
+End type.

theories/examples/latch/latch_proof.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.latch Require Import latch_def latch_spec latch_code.
+Set Default Proof Using "Type".
+
+Section type.
+  Context `{!typeG Σ}.
+
+  Lemma type_latch_wait:
+    ⊢ typed_function impl_latch_wait type_of_latch_wait.
+  Proof. Admitted.
+
+  Lemma type_latch_release:
+    ⊢ typed_function impl_latch_release type_of_latch_release.
+  Proof. Admitted.
+
+End type.

theories/examples/latch/latch_proof_latch_release.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.latch Require Import latch_code.
+From refinedc.examples.latch Require Import latch_spec.
+From refinedc.examples.latch Require Import latch_def.
+From refinedc.examples.latch Require Import latch_proof.
+Set Default Proof Using "Type".
+
+(* Generated from [theories/examples/latch/latch.c]. *)
+Section proof_latch_release.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [latch_release]. *)
+  Lemma type_latch_release :
+    ⊢ typed_function impl_latch_release type_of_latch_release.
+  Proof. refine type_latch_release. Qed.
+End proof_latch_release.

theories/examples/latch/latch_proof_latch_wait.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.latch Require Import latch_code.
+From refinedc.examples.latch Require Import latch_spec.
+From refinedc.examples.latch Require Import latch_def.
+From refinedc.examples.latch Require Import latch_proof.
+Set Default Proof Using "Type".
+
+(* Generated from [theories/examples/latch/latch.c]. *)
+Section proof_latch_wait.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [latch_wait]. *)
+  Lemma type_latch_wait :
+    ⊢ typed_function impl_latch_wait type_of_latch_wait.
+  Proof. refine type_latch_wait. Qed.
+End proof_latch_wait.

theories/examples/latch/latch_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.latch Require Import latch_code.
+From refinedc.examples.latch Require Import latch_def.
+Set Default Proof Using "Type".
+
+(* Generated from [theories/examples/latch/latch.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Type definitions. *)
+
+  (* Function [atomic_thread_fence] has been skipped. *)
+
+  (* Function [atomic_signal_fence] has been skipped. *)
+
+  (* Specifications for function [latch_wait]. *)
+  Definition type_of_latch_wait :=
+    fn(∀ (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (latch (P)))); True)
+      → ∃ () : (), (void); (p ◁ₗ{beta} (latch (P))) ∗ (P).
+
+  (* Specifications for function [latch_release]. *)
+  Definition type_of_latch_release :=
+    fn(∀ (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (latch (P)))); (P))
+      → ∃ () : (), (void); (p ◁ₗ{beta} (latch (P))).
+End spec.

theories/examples/tutorial/t5_main.c

 #include "list.h"
 #include "alloc_internal.h"
+#include "../latch/latch.h"
 
 #define DATA_SIZE 10000
 static unsigned char allocator_data[DATA_SIZE];
 
+[[rc::global("latch<{alloc_initialized}>")]]
+static struct latch initialized = LATCH_INIT;
+
+[[rc::requires("[initialized \"initialized\" ()]")]]
 [[rc::requires("[global_with_type \"allocator_state\" Own (uninit struct_alloc_state)]")]]
 [[rc::requires("[global_with_type \"allocator_data\" Own (uninit (mk_layout (Z.to_nat 10000) 3))]")]]
 [[rc::returns("int<i32>")]]
 int main() {
     init_alloc();
     free(DATA_SIZE, allocator_data);
+    latch_release(&initialized);
+
+    test();
+    return 0;
+}
+
+[[rc::requires("[initialized \"initialized\" ()]")]]
+[[rc::returns("int<i32>")]]
+int main2() {
+    latch_wait(&initialized);
 
     test();
     return 0;

theories/examples/tutorial/t5_main_code.v

@@ -7,20 +7,35 @@ Set Default Proof Using "Type".
 (* Generated from [theories/examples/tutorial/t5_main.c]. *)
 Section code.
   Definition file_0 : string := "theories/examples/tutorial/t5_main.c".
-  Definition loc_2 : location_info := LocationInfo file_0 11 4 11 17.
-  Definition loc_3 : location_info := LocationInfo file_0 12 4 12 32.
-  Definition loc_4 : location_info := LocationInfo file_0 14 4 14 11.
-  Definition loc_5 : location_info := LocationInfo file_0 15 4 15 13.
-  Definition loc_6 : location_info := LocationInfo file_0 15 11 15 12.
-  Definition loc_7 : location_info := LocationInfo file_0 14 4 14 8.
-  Definition loc_8 : location_info := LocationInfo file_0 14 4 14 8.
-  Definition loc_9 : location_info := LocationInfo file_0 12 4 12 8.
-  Definition loc_10 : location_info := LocationInfo file_0 12 4 12 8.
-  Definition loc_11 : location_info := LocationInfo file_0 12 9 12 14.
-  Definition loc_12 : location_info := LocationInfo file_0 12 16 12 30.
-  Definition loc_13 : location_info := LocationInfo file_0 12 16 12 30.
-  Definition loc_14 : location_info := LocationInfo file_0 11 4 11 14.
-  Definition loc_15 : location_info := LocationInfo file_0 11 4 11 14.
+  Definition loc_2 : location_info := LocationInfo file_0 16 4 16 17.
+  Definition loc_3 : location_info := LocationInfo file_0 17 4 17 32.
+  Definition loc_4 : location_info := LocationInfo file_0 18 4 18 32.
+  Definition loc_5 : location_info := LocationInfo file_0 20 4 20 11.
+  Definition loc_6 : location_info := LocationInfo file_0 21 4 21 13.
+  Definition loc_7 : location_info := LocationInfo file_0 21 11 21 12.
+  Definition loc_8 : location_info := LocationInfo file_0 20 4 20 8.
+  Definition loc_9 : location_info := LocationInfo file_0 20 4 20 8.
+  Definition loc_10 : location_info := LocationInfo file_0 18 4 18 17.
+  Definition loc_11 : location_info := LocationInfo file_0 18 4 18 17.
+  Definition loc_12 : location_info := LocationInfo file_0 18 18 18 30.
+  Definition loc_13 : location_info := LocationInfo file_0 18 19 18 30.
+  Definition loc_14 : location_info := LocationInfo file_0 17 4 17 8.
+  Definition loc_15 : location_info := LocationInfo file_0 17 4 17 8.
+  Definition loc_16 : location_info := LocationInfo file_0 17 9 17 14.
+  Definition loc_17 : location_info := LocationInfo file_0 17 16 17 30.
+  Definition loc_18 : location_info := LocationInfo file_0 17 16 17 30.
+  Definition loc_19 : location_info := LocationInfo file_0 16 4 16 14.
+  Definition loc_20 : location_info := LocationInfo file_0 16 4 16 14.
+  Definition loc_23 : location_info := LocationInfo file_0 27 4 27 29.
+  Definition loc_24 : location_info := LocationInfo file_0 29 4 29 11.
+  Definition loc_25 : location_info := LocationInfo file_0 30 4 30 13.
+  Definition loc_26 : location_info := LocationInfo file_0 30 11 30 12.
+  Definition loc_27 : location_info := LocationInfo file_0 29 4 29 8.
+  Definition loc_28 : location_info := LocationInfo file_0 29 4 29 8.
+  Definition loc_29 : location_info := LocationInfo file_0 27 4 27 14.
+  Definition loc_30 : location_info := LocationInfo file_0 27 4 27 14.
+  Definition loc_31 : location_info := LocationInfo file_0 27 15 27 27.
+  Definition loc_32 : location_info := LocationInfo file_0 27 16 27 27.
 
   (* Definition of struct [atomic_flag]. *)
   Program Definition struct_atomic_flag := {|
@@ -57,8 +72,16 @@ Section code.
   |}.
   Solve Obligations with solve_struct_obligations.
 
+  (* Definition of struct [latch]. *)
+  Program Definition struct_latch := {|
+    sl_members := [
+      (Some "released", it_layout bool_it)
+    ];
+  |}.
+  Solve Obligations with solve_struct_obligations.
+
   (* Definition of function [main]. *)
-  Definition impl_main (allocator_data test free init_alloc : loc): function := {|
+  Definition impl_main (allocator_data initialized test free init_alloc latch_release : loc): function := {|
     f_args := [
     ];
     f_local_vars := [
@@ -67,15 +90,38 @@ Section code.
     f_code := (
       <[ "#0" :=
         locinfo: loc_2 ;
-        "_" <- LocInfoE loc_15 (init_alloc) with [  ] ;
+        "_" <- LocInfoE loc_20 (init_alloc) with [  ] ;
         locinfo: loc_3 ;
-        "_" <- LocInfoE loc_10 (free) with
-          [ LocInfoE loc_11 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_11 (i2v 10000 i32))) ;
-          LocInfoE loc_12 (&(LocInfoE loc_13 (allocator_data))) ] ;
+        "_" <- LocInfoE loc_15 (free) with
+          [ LocInfoE loc_16 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_16 (i2v 10000 i32))) ;
+          LocInfoE loc_17 (&(LocInfoE loc_18 (allocator_data))) ] ;
         locinfo: loc_4 ;
-        "_" <- LocInfoE loc_8 (test) with [  ] ;
+        "_" <- LocInfoE loc_11 (latch_release) with
+          [ LocInfoE loc_12 (&(LocInfoE loc_13 (initialized))) ] ;
         locinfo: loc_5 ;
-        Return (LocInfoE loc_6 (i2v 0 i32))
+        "_" <- LocInfoE loc_9 (test) with [  ] ;
+        locinfo: loc_6 ;
+        Return (LocInfoE loc_7 (i2v 0 i32))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [main2]. *)
+  Definition impl_main2 (initialized test latch_wait : loc): function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_23 ;
+        "_" <- LocInfoE loc_30 (latch_wait) with
+          [ LocInfoE loc_31 (&(LocInfoE loc_32 (initialized))) ] ;
+        locinfo: loc_24 ;
+        "_" <- LocInfoE loc_28 (test) with [  ] ;
+        locinfo: loc_25 ;
+        Return (LocInfoE loc_26 (i2v 0 i32))
       ]> $∅
     )%E
   |}.

theories/examples/tutorial/t5_main_proof_main.v

@@ -2,6 +2,7 @@ From refinedc.typing Require Import typing.
 From refinedc.examples.tutorial Require Import t5_main_code.
 From refinedc.examples.tutorial Require Import t5_main_spec.
 From refinedc.examples.spinlock Require Import spinlock_def.
+From refinedc.examples.latch Require Import latch_def.
 Set Default Proof Using "Type".
 
 (* Generated from [theories/examples/tutorial/t5_main.c]. *)
@@ -10,12 +11,15 @@ Section proof_main.
   Context `{!lockG Σ}.
 
   (* Typing proof for [main]. *)
-  Lemma type_main (allocator_data test free init_alloc : loc) :
+  Lemma type_main (allocator_data initialized test free init_alloc latch_release : loc) :
     global_locs !! "allocator_data" = Some allocator_data →
+    global_locs !! "initialized" = Some initialized →
+    global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)) →
     test ◁ᵥ test @ function_ptr type_of_test -∗
     free ◁ᵥ free @ function_ptr type_of_free -∗
     init_alloc ◁ᵥ init_alloc @ function_ptr type_of_init_alloc -∗
-    typed_function (impl_main allocator_data test free init_alloc) type_of_main.
+    latch_release ◁ᵥ latch_release @ function_ptr type_of_latch_release -∗
+    typed_function (impl_main allocator_data initialized test free init_alloc latch_release) type_of_main.
   Proof.
     start_function "main" ([]).
     split_blocks ((

theories/examples/tutorial/t5_main_proof_main2.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tutorial Require Import t5_main_code.
+From refinedc.examples.tutorial Require Import t5_main_spec.
+From refinedc.examples.spinlock Require Import spinlock_def.
+From refinedc.examples.latch Require Import latch_def.
+Set Default Proof Using "Type".
+
+(* Generated from [theories/examples/tutorial/t5_main.c]. *)
+Section proof_main2.
+  Context `{!typeG Σ} `{!globalG Σ}.
+  Context `{!lockG Σ}.
+
+  (* Typing proof for [main2]. *)
+  Lemma type_main2 (initialized test latch_wait : loc) :
+    global_locs !! "initialized" = Some initialized →
+    global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)) →
+    test ◁ᵥ test @ function_ptr type_of_test -∗
+    latch_wait ◁ᵥ latch_wait @ function_ptr type_of_latch_wait -∗
+    typed_function (impl_main2 initialized test latch_wait) type_of_main2.
+  Proof.
+    start_function "main2" ([]).
+    split_blocks ((
+      ∅
+    )%I : gmap block_id (iProp Σ)) ((
+      ∅
+    )%I : gmap block_id (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "main2" "#0".
+    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    all: print_sidecondition_goal "main2".
+  Qed.
+End proof_main2.

theories/examples/tutorial/t5_main_spec.v

 From refinedc.typing Require Import typing.
 From refinedc.examples.tutorial Require Import t5_main_code.
 From refinedc.examples.spinlock Require Import spinlock_def.
+From refinedc.examples.latch Require Import latch_def.
 Set Default Proof Using "Type".
 
 (* Generated from [theories/examples/tutorial/t5_main.c]. *)
@@ -174,9 +175,24 @@ Section spec.
     fn(∀ () : (); (global_with_type "allocator_state" Own (uninit struct_alloc_state)))
       → ∃ () : (), (void); (alloc_initialized).
 
+  (* Specifications for function [latch_wait]. *)
+  Definition type_of_latch_wait :=
+    fn(∀ (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (latch (P)))); True)
+      → ∃ () : (), (void); (p ◁ₗ{beta} (latch (P))) ∗ (P).
+
+  (* Specifications for function [latch_release]. *)
+  Definition type_of_latch_release :=
+    fn(∀ (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (latch (P)))); (P))
+      → ∃ () : (), (void); (p ◁ₗ{beta} (latch (P))).
+
   (* Specifications for function [main]. *)
   Definition type_of_main :=
-    fn(∀ () : (); (global_with_type "allocator_state" Own (uninit struct_alloc_state)) ∗ (global_with_type "allocator_data" Own (uninit (mk_layout (Z.to_nat 10000) 3))))
+    fn(∀ () : (); (initialized "initialized" ()) ∗ (global_with_type "allocator_state" Own (uninit struct_alloc_state)) ∗ (global_with_type "allocator_data" Own (uninit (mk_layout (Z.to_nat 10000) 3))))
+      → ∃ () : (), (int (i32)); True.
+
+  (* Specifications for function [main2]. *)
+  Definition type_of_main2 :=
+    fn(∀ () : (); (initialized "initialized" ()))
       → ∃ () : (), (int (i32)); True.
 End spec.
 

theories/examples/tutorial/t_adequacy.v

 From refinedc.typing Require Import typing.
 From refinedc.examples.spinlock Require Import spinlock_code spinlock_def spinlock_proof.
+From refinedc.examples.latch Require Import latch_code latch_def latch_proof.
 From refinedc.examples.tutorial Require Import t3_list_code t4_alloc_code t5_main_code.
 From refinedc.examples.tutorial Require Import t3_list_spec t4_alloc_spec t5_main_spec.
 From refinedc.examples.tutorial Require Import t5_main_proof_main t4_alloc_proof_init_alloc t4_alloc_proof_alloc t4_alloc_proof_free t3_list_proof_test t3_list_proof_reverse t3_list_proof_pop t3_list_proof_push t3_list_proof_is_empty t3_list_proof_init t3_list_proof_member.
@@ -8,14 +9,17 @@ From refinedc.typing Require Import adequacy.
 
 
 Section adequate.
-  Context (block_allocator_data block_allocator_state : Z).
+  Context (block_allocator_data block_allocator_state block_initialized : Z).
   Let loc_allocator_data := block_to_loc block_allocator_data.
   Let loc_allocator_state := block_to_loc block_allocator_state.
+  Let loc_initialized := block_to_loc block_initialized.
   Context (loc_sl_init loc_sl_lock loc_sl_unlock
+           loc_latch_wait loc_latch_release
            loc_init loc_is_empty loc_push loc_pop loc_member loc_reverse loc_test
            loc_alloc loc_free loc_init_alloc
-           loc_main : loc).
-  Context (Hlayout : loc_allocator_state `has_layout_loc` struct_alloc_state).
+           loc_main loc_main2 : loc).
+  Context (Hlayout_alloc_state : loc_allocator_state `has_layout_loc` struct_alloc_state).
+  Context (Hlayout_initialized : loc_initialized `has_layout_loc` struct_latch).
   Definition functions  : list function := [
     impl_sl_init; impl_sl_lock; impl_sl_unlock;
 
@@ -26,7 +30,8 @@ Section adequate.
     impl_free loc_allocator_state loc_sl_lock loc_sl_unlock;
     impl_init_alloc loc_allocator_state loc_sl_init;
 
-    impl_main loc_allocator_data loc_test loc_free loc_init_alloc
+    impl_main loc_allocator_data loc_initialized loc_test loc_free loc_init_alloc loc_latch_release;
+    impl_main2 loc_initialized loc_test loc_latch_wait
   ].
   Definition function_locs : list loc := [
     loc_sl_init; loc_sl_lock; loc_sl_unlock;
@@ -35,18 +40,25 @@ Section adequate.
 
     loc_alloc; loc_free; loc_init_alloc;
 
-    loc_main
+    loc_main; loc_main2
   ].