use multithreaded adequacy

theories/examples/latch/latch_def.v

@@ -37,6 +37,16 @@ Section type.
     λ T, i2p (latch_subsume P1 P2 l T β).
 
   Definition LATCH_INIT := val_of_bool false.
+
+  Lemma latch_init l E P:
+    ↑shrN ⊆ E →
+    l `has_layout_loc` struct_latch →
+    l ↦ LATCH_INIT ={E}=∗ l ◁ₗ{Shr} latch P.
+  Proof.
+    iIntros (? ?) "Hl".
+    iApply ty_share => //. iApply (ty_ref with "[] Hl") => //.
+    rewrite /ty_own_val/=. repeat iSplit => //. rewrite /ty_own_val/=/ty_own_val/=. by iExists false.
+  Qed.
 End type.
 
 Typeclasses Opaque latch.

theories/examples/tutorial/t5_main.c

 #include "list.h"
 #include "alloc_internal.h"
+#include "../latch/latch.h"
+
+[[rc::global("latch<{alloc_initialized}>")]]
+static struct latch initialized = LATCH_INIT;
 
 #define DATA_SIZE 10000
 static unsigned char allocator_data[DATA_SIZE];
 
+[[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 (initialized allocator_data 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 (initialized allocator_data test free init_alloc latch_release : loc) :
+    global_locs !! "initialized" = Some initialized →
     global_locs !! "allocator_data" = Some allocator_data →
+    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 initialized allocator_data 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_latch_release latch_proof_latch_wait.
 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.
+From refinedc.examples.tutorial Require Import t5_main_proof_main t5_main_proof_main2 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.
 From refinedc.typing Require Import adequacy.
 (* Set Default Proof Using "Type". *)
 
 
 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;
 
+    impl_latch_wait; impl_latch_release;
+
     impl_init; impl_is_empty; impl_push loc_alloc; impl_pop loc_free; impl_member; impl_reverse;
     impl_test loc_alloc loc_free loc_init loc_is_empty loc_push loc_pop loc_reverse loc_member;
 
@@ -26,33 +32,43 @@ 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_initialized loc_allocator_data 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;
 
+    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_main; loc_main2
   ].
 
   Definition initial_heap : gmap Z (list mbyte) :=
     <[block_allocator_data := replicate (Z.to_nat 10000) Poison ]> $
-    <[block_allocator_state := replicate (struct_alloc_state).(ly_size) Poison ]> $ ∅.
+    <[block_allocator_state := replicate (struct_alloc_state).(ly_size) Poison ]> $
+    <[block_initialized := LATCH_INIT ]> $
+    ∅.
 
   Definition global_locs : gmap string loc :=
     <["allocator_data" := loc_allocator_data]> $
-    <["allocator_state" := loc_allocator_state]> $ ∅.
+    <["allocator_state" := loc_allocator_state]> $
+    <["initialized" := loc_initialized]> $
+    ∅.
   Definition global_types `{!typeG Σ} `{!lockG Σ} : gmap string global_type :=
-    <["allocator_state" := GT unit (λ '(), t4_alloc_spec.alloc_state)]> $ ∅.
+    <["allocator_state" := GT unit (λ '(), t4_alloc_spec.alloc_state)]> $
+    (* We need to use initialized_raw to avoid a cyclic definition of globalG  *)
+    <["initialized" := GT unit (λ '(), latch (initialized_raw "allocator_state" () (Some loc_allocator_state) (Some (GT unit (λ '(), t4_alloc_spec.alloc_state)))))]> $
+    ∅.
 
 
   Lemma tutorial_adequate n κs t2 σ2:
-    NoDup [block_allocator_data; block_allocator_state] →
+    NoDup [block_allocator_data; block_allocator_state; block_initialized] →
     NoDup function_locs →
-    nsteps (Λ := stmt_lang) n ([initial_thread_state loc_main],
+    nsteps (Λ := stmt_lang) n (initial_thread_state <$> [loc_main; loc_main2],
                                initial_state (fn_lists_to_fns function_locs functions)
                                              (heap_list_to_heap initial_heap)) κs (t2, σ2) →
     ∀ e2, e2 ∈ t2 → not_stuck e2 σ2.
@@ -66,11 +82,10 @@ Section adequate.
     exists global_locs, global_types => Hglobals.
     iIntros "Hmt Hfn".
 
-    iDestruct (heap_list_to_heap_insert with "Hmt") as "[Hdata Hmt]". {
-      rewrite lookup_insert_ne //.
-      move: HNDblocks => /NoDup_cons[??]. set_solver.
-    }
-    iDestruct (heap_list_to_heap_insert with "Hmt") as "[Hstate Hmt]". done.
+    move: HNDblocks => /NoDup_cons[?/NoDup_cons[? _]].
+    iDestruct (heap_list_to_heap_insert with "Hmt") as "[Hdata Hmt]"; [rewrite !lookup_insert_ne //; set_solver|].
+    iDestruct (heap_list_to_heap_insert with "Hmt") as "[Hstate Hmt]"; [rewrite !lookup_insert_ne //; set_solver|].
+    iDestruct (heap_list_to_heap_insert with "Hmt") as "[Hinit Hmt]"; [done|].
     iClear "Hmt".
 
     have Hin := I.
@@ -80,24 +95,28 @@ Section adequate.
     ).
 
     iAssert (
-        typed_function (functions !!! 13%nat) type_of_main ∗
-        typed_function (functions !!! 12%nat) type_of_init_alloc ∗
-        typed_function (functions !!! 11%nat) type_of_free ∗
-        typed_function (functions !!! 10%nat) type_of_alloc ∗
-        typed_function (functions !!! 9%nat) type_of_test ∗
-        typed_function (functions !!! 8%nat) type_of_reverse ∗
-        typed_function (functions !!! 7%nat) type_of_member ∗
-        typed_function (functions !!! 6%nat) type_of_pop ∗
-        typed_function (functions !!! 5%nat) type_of_push ∗
-        typed_function (functions !!! 4%nat) type_of_is_empty ∗
-        typed_function (functions !!! 3%nat) type_of_init ∗
+        typed_function (functions !!! 16%nat) type_of_main2 ∗
+        typed_function (functions !!! 15%nat) type_of_main ∗
+        typed_function (functions !!! 14%nat) type_of_init_alloc ∗
+        typed_function (functions !!! 13%nat) type_of_free ∗
+        typed_function (functions !!! 12%nat) type_of_alloc ∗
+        typed_function (functions !!! 11%nat) type_of_test ∗
+        typed_function (functions !!! 10%nat) type_of_reverse ∗
+        typed_function (functions !!! 9%nat) type_of_member ∗
+        typed_function (functions !!! 8%nat) type_of_pop ∗
+        typed_function (functions !!! 7%nat) type_of_push ∗
+        typed_function (functions !!! 6%nat) type_of_is_empty ∗
+        typed_function (functions !!! 5%nat) type_of_init ∗
+        typed_function (functions !!! 4%nat) type_of_latch_release ∗
+        typed_function (functions !!! 3%nat) type_of_latch_wait ∗
         typed_function (functions !!! 2%nat) type_of_sl_unlock ∗
         typed_function (functions !!! 1%nat) type_of_sl_lock ∗
         typed_function (functions !!! 0%nat) type_of_sl_init
-      )%I as "[Hmain _]". {
+      )%I as "(Hmain2&Hmain&_)". {
       simpl.
-      iLöb as "IH". iDestruct "IH" as "(?&?&?&?&?&?&?&?&?&?&?&?&?&?)".
+      iLöb as "IH". iDestruct "IH" as "(?&?&?&?&?&?&?&?&?&?&?&?&?&?&?&?&?)".
       repeat iSplit.
+      - iApply type_main2 => //; iExists _; repeat iSplit => //.
       - iApply type_main => //; iExists _; repeat iSplit => //.
       - iApply type_init_alloc => //; iExists _; repeat iSplit => //.
       - iApply type_free => //; iExists _; repeat iSplit => //.
@@ -109,16 +128,21 @@ Section adequate.
       - iApply type_push => //; iExists _; repeat iSplit => //.
       - iApply type_is_empty => //; iExists _; repeat iSplit => //.
       - iApply type_init => //; iExists _; repeat iSplit => //.
+      - iApply type_latch_release => //; iExists _; repeat iSplit => //.
+      - iApply type_latch_wait => //; iExists _; repeat iSplit => //.
       - iApply type_sl_unlock => //; iExists _; repeat iSplit => //.
       - iApply type_sl_lock => //; iExists _; repeat iSplit => //.
       - iApply type_sl_init => //; iExists _; repeat iSplit => //.
     }
-    iModIntro. iSplitL => //.
-    iExists _. iSplitR.
-    - iExists _. repeat iSplit => //.
-    - iSplitL "Hstate"; iExists _; iSplit => //; iExists _; iEval (simpl).
-      + iFrame "Hstate" => //.
-      + iFrame "Hdata" => //.
+    iMod (latch_init with "Hinit") as "#Hinit" => //.
+    iModIntro. iSplitL => //. 2: iSplitL => //.
+    all: iExists _; iSplitR; [iExists _; repeat iSplit => // |].
+    - iSplitR. 2: iSplitL "Hstate".
+      + iApply initialized_intro => //=. iExists eq_refl => /=. iApply "Hinit".
+      + iExists _; iSplit => //; iExists _; iEval (simpl).
+        iFrame "Hstate" => //.
+      + iExists _; iSplit => //; iExists _; iEval (simpl). iFrame "Hdata" => //.
+    - iApply initialized_intro => //=. iExists eq_refl => /=. iApply "Hinit".
   Qed.
 End adequate.
 

theories/lang/lang.v

@@ -379,6 +379,13 @@ Proof.
   split; destruct b => /=; lia.
 Qed.
 
+Lemma i2v_bool_length b it:
+  length (i2v (Z_of_bool b) it) = it_length it.
+Proof. by have /val_of_int_length -> := val_of_int_bool b it. Qed.
+Lemma i2v_bool_Some b it:
+  val_to_int (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
+Proof. apply val_to_of_int. apply val_of_int_bool. Qed.
+
 Arguments val_to_int : simpl never.
 Arguments val_of_int : simpl never.
 Arguments val_to_loc : simpl never.

theories/typing/atomic_bool.v

@@ -54,21 +54,32 @@ Section programs.
     Subsume (l ◁ₗ n @ int it)%I (l ◁ₗ atomic_bool it PT PF) :=
     λ T, i2p (subsume_atomic_bool_own_int l n it PT PF T).
 
-  Lemma i2v_bool_length b it:
-    length (i2v (Z_of_bool b) it) = it_length it.
-  Proof. by have /val_of_int_length -> := val_of_int_bool b it. Qed.
-  Lemma i2v_bool_Some b it:
-    val_to_int (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
-  Proof. apply val_to_of_int. apply val_of_int_bool. Qed.
-
   Lemma type_read_atomic_bool l β it PT PF T:
-    (∀ b, destruct_hint (DHintDestruct bool b) tt ((if b then PT else PF) -∗ (if b then PT else PF) ∗ T (i2v (Z_of_bool b) it) (atomic_bool it PT PF) (t2mt (b @ boolean it)))) -∗
+    (∀ b v, destruct_hint (DHintDestruct bool b) tt ((if b then PT else PF) -∗ (if b then PT else PF) ∗ T v (atomic_bool it PT PF) (t2mt (b @ boolean it)))) -∗
     typed_read_end true l β (atomic_bool it PT PF) it T.
   Proof.
     iIntros "HT Hl". unfold destruct_hint.
     destruct β.
     - iDestruct "Hl" as (b) "[Hl Hif]".
-  Admitted.
+      iMod (fupd_intro_mask') as "Hclose". 2: iModIntro. done.
+      iDestruct (ty_aligned with "Hl") as %?.
+      iDestruct (ty_deref with "Hl") as (v) "[Hl #Hv]".
+      iDestruct (ty_size_eq with "Hv") as %?.
+      iExists _, _, _, (t2mt (b @ boolean it)). iFrame "∗Hv". do 2 iSplitR => //=.
+      iIntros "!# Hl". iMod "Hclose". iModIntro.
+      iDestruct ("HT" with "Hif") as "[Hif $]".
+      iExists b. iFrame.
+        by iApply (ty_ref with "[] Hl Hv").
+    - iDestruct "Hl" as (Hly) "#Hinv".
+      iInv "Hinv" as (b) "[>Hl Hif]" "Hclose".
+      iMod (fupd_intro_mask') as "Hclose2". 2: iModIntro. solve_ndisj.
+      iExists _, _, _, (t2mt (b @ boolean it)). iFrame.
+      rewrite /has_layout_val i2v_bool_length.
+      do 2 iSplitR => //=. iSplitR => //. { by rewrite /ty_own_val/= val_of_int_bool. }
+      iIntros "!# Hl". iDestruct ("HT" with "Hif") as "[Hif $]".
+      iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"). { iExists _. by iFrame. }
+      iModIntro. by iSplitR.
+  Qed.
   Global Instance type_read_atomic_bool_inst l β it PT PF:
     TypedReadEnd true l β (atomic_bool it PT PF) it | 10 :=
     λ T, i2p (type_read_atomic_bool l β it PT PF T).

theories/typing/globals.v

@@ -23,10 +23,17 @@ Section globals.
   Definition global_with_type (name : string) (β : own_state) (ty : type) : iProp Σ :=
     (∃ l, ⌜global_locs !! name = Some l⌝ ∗ l ◁ₗ{β} ty)%I.
 
-  Definition initialized {A} (name : string) (x : A) : iProp Σ :=
-    (∃ l ty, ⌜global_locs !! name = Some l⌝ ∗ ⌜global_initialized_types !! name = Some ty⌝ ∗
+  (* A version of initialized that does not depend on globalG. This is
+  a work-around to allow the type of one global to refer to another as
+  long as there are no cycles (see t_adequacy). The proper solution
+  would be to use higher-order ghost state instead of globalG. *)
+  Definition initialized_raw {A} (name : string) (x : A) (l' : option loc) (ty' : option global_type)  : iProp Σ :=
+    (∃ l ty, ⌜l' = Some l⌝ ∗ ⌜ty' = Some ty⌝ ∗
           ∃ Heq : A = ty.(gt_A), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x))%I.
 
+  Definition initialized {A} (name : string) (x : A) : iProp Σ :=
+    initialized_raw name x (global_locs !! name) (global_initialized_types !! name).
+
   Global Instance initialized_persistent A name (x : A) : Persistent (initialized name x).
   Proof. apply _. Qed.
 
@@ -61,10 +68,17 @@ Section globals.
     SimplifyHyp (initialized name x) (Some 0%N) :=
     λ T, i2p (simplify_initialized_hyp A x name ty l T).
 
+  Lemma initialized_intro A ty name l (x : A) :
+    global_locs !! name = Some l →
+    global_initialized_types !! name = Some ty →
+    (∃ (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x)) -∗
+    initialized name x.
+  Proof. iIntros (??) "Hl". iExists _, _. by iFrame. Qed.
+
   Lemma simplify_initialized_goal A (x : A) name l ty T `{!FastDone (global_locs !! name = Some l)} `{!FastDone (global_initialized_types !! name = Some ty)} :
     T ((∃ (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x))) -∗
     simplify_goal (initialized name x) T.
-  Proof. unfold FastDone in *. iIntros "HT". iExists _. iFrame. iIntros "?". iExists _, _. by iFrame. Qed.
+  Proof. unfold FastDone in *. iIntros "HT". iExists _. iFrame. by iApply initialized_intro. Qed.
   Global Instance simplify_initialized_goal_inst A (x : A) name ty l `{!FastDone (global_locs !! name = Some l)}  `{!FastDone (global_initialized_types !! name = Some ty)}:
     SimplifyGoal (initialized name x) (Some 0%N) :=
     λ T, i2p (simplify_initialized_goal A x name l ty T).