added latch and support atomic load

frontend/ail_to_coq.ml

@@ -668,7 +668,18 @@ and translate_call : type a. a call_place -> loc -> bool -> ail_expr
             begin
               ignore (e1, l1, layout);
               match place with
-              | In_Expr -> (Call_atomic_expr(Deref(true, layout, e1)), l1)
+              | In_Expr ->
+                 let e1 =
+                   match e1.elt with
+                   | AddrOf(e) -> e
+                   | _         -> forbidden loc "atomic load whose RHS is \
+                                                 not of the form [&e]"
+                 in
+                 let gen =
+                   if lval then Deref(true, layout, e1)
+                   else Use(true, layout, e1)
+                 in
+                 (Call_atomic_expr(gen), l1)
               | In_Stmt -> not_impl loc "call to builtin atomic (load)"
             end
         | AilBatomic(AilBAexchange)                ->

frontend/coq_pp.ml

@@ -170,8 +170,10 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
     | SkipE(e)                      ->
         pp "SkipE (%a)" pp_expr e
     | Use(atomic,lay,e)             ->
-        if atomic then panic_no_pos "Use on atomics not supported.";
-        pp "use{%a} (%a)" (pp_layout false) lay pp_expr e
+        if atomic then
+          pp "use{%a, ScOrd} (%a)" (pp_layout false) lay pp_expr e
+        else
+          pp "use{%a} (%a)" (pp_layout false) lay pp_expr e
     | AddrOf(e)                     ->
         pp "&(%a)" pp_expr e
     | GetMember(e,name,false,field) ->

theories/examples/latch/latch.c

+#include <stdbool.h>
+#include "latch.h"
+
+void latch_wait(struct latch* latch) {
+  while(atomic_load(&latch->released) == (_Bool)false) {}
+}
+
+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 5 2 5 94.
+  Definition loc_3 : location_info := LocationInfo file_0 5 2 5 94.
+  Definition loc_4 : location_info := LocationInfo file_0 5 92 5 94.
+  Definition loc_5 : location_info := LocationInfo file_0 5 2 5 94.
+  Definition loc_6 : location_info := LocationInfo file_0 5 2 5 94.
+  Definition loc_7 : location_info := LocationInfo file_0 5 8 5 90.
+  Definition loc_8 : location_info := LocationInfo file_0 5 8 5 78.
+  Definition loc_9 : location_info := LocationInfo file_0 5 8 5 38.
+  Definition loc_10 : location_info := LocationInfo file_0 5 39 5 55.
+  Definition loc_11 : location_info := LocationInfo file_0 5 40 5 55.
+  Definition loc_12 : location_info := LocationInfo file_0 5 40 5 45.
+  Definition loc_13 : location_info := LocationInfo file_0 5 40 5 45.
+  Definition loc_14 : location_info := LocationInfo file_0 5 82 5 90.
+  Definition loc_15 : location_info := LocationInfo file_0 5 89 5 90.
+  Definition loc_18 : location_info := LocationInfo file_0 9 2 9 77.
+  Definition loc_19 : location_info := LocationInfo file_0 9 2 9 33.
+  Definition loc_20 : location_info := LocationInfo file_0 9 34 9 50.
+  Definition loc_21 : location_info := LocationInfo file_0 9 35 9 50.
+  Definition loc_22 : location_info := LocationInfo file_0 9 35 9 40.
+  Definition loc_23 : location_info := LocationInfo file_0 9 35 9 40.
+  Definition loc_24 : location_info := LocationInfo file_0 9 52 9 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 := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_2 ;
+        Goto "#1"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_7 ;
+        if: LocInfoE loc_7 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_7 ((LocInfoE loc_8 (use{it_layout bool_it, ScOrd} (LocInfoE loc_11 ((LocInfoE loc_12 (!{LPtr} (LocInfoE loc_13 ("latch")))) at{struct_latch} "released")))) ={IntOp bool_it, IntOp bool_it} (LocInfoE loc_14 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_15 (i2v 0 i32)))))))
+        then
+        locinfo: loc_5 ;
+          Goto "#2"
+        else
+        Goto "#3"
+      ]> $
+      <[ "#2" :=
+        locinfo: loc_5 ;
+        Goto "continue2"
+      ]> $
+      <[ "#3" :=
+        Return (VOID)
+      ]> $
+      <[ "continue2" :=
+        locinfo: loc_2 ;
+        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_18 ;
+        LocInfoE loc_21 ((LocInfoE loc_22 (!{LPtr} (LocInfoE loc_23 ("latch")))) at{struct_latch} "released") <-{ it_layout bool_it, ScOrd }
+          LocInfoE loc_24 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_24 (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 Σ}.
+
+  Definition latch (P : iProp Σ) : type :=
+    struct struct_latch [atomic_bool bool_it (□ P) True].
+
+  Global Program Instance movable_latch P : Movable (latch P) := ltac:(apply: movable_struct).
+
+  Lemma latch_simplify_hyp l β P T:
+    (l ◁ₗ{β} struct struct_latch [atomic_bool bool_it (□ P) True] -∗ T) -∗
+    simplify_hyp (l ◁ₗ{β} latch P) T.
+  Proof. done. Qed.
+  Global Instance latch_simplify_hyp_inst l β P:
+    SimplifyHypPlace l β (latch P) (Some 100%N) :=
+    λ T, i2p (latch_simplify_hyp l β P T).
+
+  Lemma latch_simplify_goal l β P T:
+    T (l ◁ₗ{β} struct struct_latch [atomic_bool bool_it (□ P) True]) -∗
+    simplify_goal (l ◁ₗ{β} latch P) T.
+  Proof. iIntros "HT". iExists _. iFrame. iIntros "$". Qed.
+  Global Instance latch_simplify_goal_inst l β P:
+    SimplifyGoalPlace l β (latch P) (Some 100%N) :=
+    λ T, i2p (latch_simplify_goal l β P T).
+
+  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.
+
+Typeclasses Opaque latch.

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.
+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.
+    start_function "latch_release" ([[p beta] P]) => arg_latch.
+    split_blocks ((
+      ∅
+    )%I : gmap block_id (iProp Σ)) ((
+      ∅
+    )%I : gmap block_id (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "latch_release" "#0".
+    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    all: print_sidecondition_goal "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.
+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.
+    start_function "latch_wait" ([[p beta] P]) => arg_latch.
+    split_blocks ((
+      <[ "#1" :=
+        arg_latch ◁ₗ (p @ (&frac{beta} (latch (P))))
+    ]> $
+      ∅
+    )%I : gmap block_id (iProp Σ)) ((
+      ∅
+    )%I : gmap block_id (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "latch_wait" "#0".
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "latch_wait" "#1".
+    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    all: print_sidecondition_goal "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/lang/lang.v

@@ -1078,6 +1078,16 @@ Proof.
   - by destruct l, l' => [[]].
 Qed.
 
+Lemma heap_upd_heap_at_id l v flk flk' h:
+  heap_at_go l v flk' h →
+  (∀ st, flk (Some st) = st) →
+  heap_upd l v flk h = h.
+Proof.
+  elim: v l => //= b v IH l [[lk[Hlk ?]]?] Hflk. rewrite IH //.
+  apply: partial_alter_self_alt'. by rewrite Hlk Hflk.
+Qed.
+
+
 Lemma heap_block_free_upd_list ls vs h l flk:
   heap_block_free h l → l.1 ∉ ls.*1 →
   heap_block_free (heap_upd_list ls vs flk h) l.

theories/lang/lifting.v

@@ -40,6 +40,10 @@ Instance cas_atomic s ot (v1 v2 v3 : val) : Atomic s (CAS ot v1 v2 v3).
 Proof. solve_atomic. Qed.
 Instance skipe_atomic s (v : val) : Atomic s (SkipE v).
 Proof. solve_atomic. Qed.
+Instance deref_atomic s (l : loc) ly : Atomic s (Deref ScOrd ly l).
+Proof. solve_atomic. Qed.
+Instance use_atomic s (l : loc) ly : Atomic s (Use ScOrd ly l).
+Proof. rewrite /Use. solve_atomic. Qed.
 
 (*** Lifting of expressions *)
 
@@ -90,28 +94,37 @@ Proof.
   iIntros "!#" (v h). rewrite Hop. iIntros (?). subst. by iApply "HΦ".
 Qed.
 
-Lemma wp_deref v Φ vl l ly q E:
+Lemma wp_deref v Φ vl l ly q E o:
+  o = ScOrd ∨ o = Na1Ord →
   val_to_loc vl = Some l →
   l `has_layout_loc` ly →
   v `has_layout_val` ly →
-  l↦{q}v -∗ ▷ (l ↦{q} v -∗ Φ v) -∗ WP !{ly} (Val vl) @ E {{ Φ }}.
+  l↦{q}v -∗ ▷ (l ↦{q} v -∗ Φ v) -∗ WP !{ly, o} (Val vl) @ E {{ Φ }}.
 Proof.
-  iIntros (Hl Hll Hlv) "Hmt HΦ".
+  iIntros (Ho Hl Hll Hlv) "Hmt HΦ".
   iApply wp_lift_head_step; auto.
   iIntros ([h ub fn] ???) "(%&Hhctx&Hfctx)".
-  iMod (heap_read_na with "Hhctx Hmt") as "(% & Hσ & Hσclose)" => //.
-  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver. iModIntro.
-  iSplit; first by eauto 7 using DerefS.
-  iIntros "!#" (e2 σ2 efs Hst). inv_expr_step. iMod "Hclose" as "$". iModIntro. unfold end_st, end_expr.
-  have <- : (v = v') by apply: heap_at_inj_val.
-  iFrame => /=. iSplit; first by eauto 7 using block_used_agree_heap_upd.
-  iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros ([h2 fn2] ???) "(%&Hhctx&Hfctx)". iMod ("Hσclose" with "Hhctx") as (?) "(Hσ & Hv)".
-  iModIntro; iSplit; first by eauto 7 using DerefS.
-  iIntros "!#" (e2 σ2 efs Hst) "!#". inv_expr_step.
-  have <- : (v = v'0) by apply: heap_at_inj_val.
-  iFrame. iSplitR => //=. iSplit; first by eauto 7 using block_used_agree_heap_upd.
-  by iApply "HΦ".
+  destruct o; try by destruct Ho.
+  - iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver. iModIntro.
+    iDestruct (heap_mapsto_lookup_q (λ st, ∃ n, st = RSt n) with "Hhctx Hmt") as %Hat. naive_solver.
+    iSplit; first by eauto 7 using DerefS.
+    iIntros "!#" (e2 σ2 efs Hst). inv_expr_step. iMod "Hclose" as "$". iModIntro. unfold end_st, end_expr.
+    have <- : (v = v') by apply: heap_at_inj_val.
+    rewrite /heap_fmap/=. erewrite heap_upd_heap_at_id => //.
+    iFrame. iSplit => //. iApply @wp_value. by iApply "HΦ".
+  - iMod (heap_read_na with "Hhctx Hmt") as "(% & Hσ & Hσclose)" => //.
+    iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver. iModIntro.
+    iSplit; first by eauto 7 using DerefS.
+    iIntros "!#" (e2 σ2 efs Hst). inv_expr_step. iMod "Hclose" as "$". iModIntro. unfold end_st, end_expr.
+    have <- : (v = v') by apply: heap_at_inj_val.
+    iFrame => /=. iSplit; first by eauto 7 using block_used_agree_heap_upd.
+    iApply wp_lift_atomic_head_step_no_fork; auto.
+    iIntros ([h2 fn2] ???) "(%&Hhctx&Hfctx)". iMod ("Hσclose" with "Hhctx") as (?) "(Hσ & Hv)".
+    iModIntro; iSplit; first by eauto 7 using DerefS.
+    iIntros "!#" (e2 σ2 efs Hst) "!#". inv_expr_step.
+    have <- : (v = v'0) by apply: heap_at_inj_val.
+    iFrame. iSplitR => //=. iSplit; first by eauto 7 using block_used_agree_heap_upd.
+      by iApply "HΦ".
 Qed.
 
 Lemma wp_cas_fail vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it q E:

theories/lithium/classes.v

@@ -51,9 +51,13 @@ Class RelatedTo {Σ} (pat : iProp Σ) : Type := {
 Arguments rt_fic {_ _} _.
 
 (** * [IntroPersistent] *)
-Class IntroPersistent {Σ} (P : iProp Σ) := {
-  ip_persistent :> Persistent P
+(** ** Definition *)
+Class IntroPersistent {Σ} (P P' : iProp Σ) := {
+  ip_persistent : P -∗ □ P'
 }.
+(** ** Instances *)
+Global Instance intro_persistent_intuit Σ (P : iProp Σ) : IntroPersistent (□ P) P.
+Proof. constructor. iIntros "$". Qed.
 
 (** * [accu] *)
 Definition accu {Σ} (f : iProp Σ → iProp Σ) : iProp Σ :=

theories/lithium/interpreter.v

@@ -83,6 +83,16 @@ Section coq_tactics.
     iIntros "HΔ".  iSplit => //. by iApply HΔ.
   Qed.
 
+  Lemma tac_do_intro_intuit_sep Δ (P Q : iProp Σ) :
+    envs_entails (envs_clear_spatial Δ) (P ∗ True) → envs_entails Δ Q → envs_entails Δ (□ P ∗ Q).
+  Proof.
+    rewrite envs_entails_eq => HP HQ. iIntros "Henv".
+    iSplit.
+    - iDestruct (envs_clear_spatial_sound with "Henv") as "[#Henv _]".
+      iModIntro. iDestruct (HP with "Henv") as "[$ _]".
+    - by iApply HQ.
+  Qed.
+
   (* TODO: have a generic super intros which does simplification along
   the awy in an efficient manner and which subsumes SimplifyHypPlace, SimplifyHypVal and SimplImpl*)
   Lemma tac_do_intro i (P : iProp Σ) T Δ o {SH:SimplifyHyp P o} :
@@ -104,20 +114,21 @@ Section coq_tactics.
     all: by iDestruct (HP with "Henv") as "$".
   Qed.
 
-  Lemma tac_do_intro_intuit i (P : iProp Σ) T Δ o `{!IntroPersistent P} {SH:SimplifyHyp P o} :
-    match o, envs_app true (Esnoc Enil i P) Δ with
+  Lemma tac_do_intro_intuit i (P P' : iProp Σ) T Δ o `{!IntroPersistent P P'} {SH:SimplifyHyp P o} :
+    match o, envs_app true (Esnoc Enil i P') Δ with
     | Some 0%N, _ => envs_entails Δ (SH T).(i2p_P)
     | _, None => False
     | _, Some Δ' => envs_entails Δ' T
     end →
     envs_entails Δ (P -∗ T).
   Proof.
-    rewrite envs_entails_eq => HP. iIntros "Henv #Hl".
+    rewrite envs_entails_eq => HP. iIntros "Henv HP".
     destruct o as [[|?] |]. {
-      iDestruct (HP with "Henv") as "HP".
-      iDestruct (i2p_proof with "HP Hl") as "$".
+      iDestruct (HP with "Henv") as "HSH".
+      iDestruct (i2p_proof with "HSH HP") as "$".
     }
     all: case_match => //.
+    all: iDestruct (ip_persistent with "HP") as "#HP'".
     all: rewrite envs_app_sound //=; simpl.
     all: iDestruct ("Henv" with "[$]") as "Henv".
     all: by iDestruct (HP with "Henv") as "$".
@@ -599,6 +610,8 @@ Ltac liSep :=
     | bi_exist _ => notypeclasses refine (tac_sep_exist_assoc _ _ _ _)
     | bi_emp => notypeclasses refine (tac_sep_emp _ _ _)
     | (⌜_⌝)%I => notypeclasses refine (tac_do_intro_pure_and _ _ _ _)
+    (* TODO: Is this really the right thing to do? *)
+    | (□ ?P)%I => notypeclasses refine (tac_do_intro_intuit_sep _ _ _ _ _)
     | match ?x with _ => _ end => fail "should not have match in sep"
     | ?P => first [
                convert_to_i2p P ltac:(fun converted =>
@@ -616,7 +629,7 @@ Ltac liWand :=
   let wand_intro :=
       let H := liFresh in
       first [
-          simple notypeclasses refine (tac_do_intro_intuit H _ _ _ _ _); [shelve | solve [refine _] | solve [refine _] | li_pm_reduce]
+          simple notypeclasses refine (tac_do_intro_intuit H _ _ _ _ _ _); [shelve | shelve | solve [refine _] | solve [refine _] | li_pm_reduce]
          | simple notypeclasses refine (tac_do_intro H _ _ _ _ _); [shelve | solve [refine _] | li_pm_reduce]
         ] in
   lazymatch goal with

theories/typing/atomic_bool.v

@@ -61,6 +61,18 @@ Section programs.
     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)))) -∗
+    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.
+  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).
+
   Lemma type_write_atomic_bool l β it PT PF v ty `{!Movable ty} T:
     (∃ b, subsume (v ◁ᵥ ty) (v ◁ᵥ b @ boolean it) (⌜ty.(ty_layout) = it⌝ ∗ (if b then PT else PF) ∗ T (atomic_bool it PT PF))) -∗
     typed_write_end true v ty l β (atomic_bool it PT PF) T.

theories/typing/automation.v

@@ -45,7 +45,7 @@ Ltac convert_to_i2p_tac P ::=
   | typed_if ?v ?ty ?s1 ?s2 ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedIf _ _) _ _ _ _ _ _ _).(i2p_proof))
   | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _ _).(i2p_proof))
   | typed_assert ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _) _ _ _ _ _ _).(i2p_proof))
-  | typed_read_end ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _) _).(i2p_proof))
+  | typed_read_end ?a ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _) _).(i2p_proof))
   | typed_write_end ?a ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _) _).(i2p_proof))
   | typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _).(i2p_proof))
   | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))
@@ -172,7 +172,7 @@ Ltac liRExpr :=
     lazymatch e' with
     | W.Val _ => notypeclasses refine (tac_fast_apply (type_val _ _) _)
     | W.Loc _ => notypeclasses refine (tac_fast_apply (type_val _ _) _)
-    | W.Use _ _ _ => notypeclasses refine (tac_fast_apply (type_use _ _ _) _)
+    | W.Use _ _ _ => notypeclasses refine (tac_fast_apply (type_use _ _ _ _) _)
     | W.AddrOf _ => notypeclasses refine (tac_fast_apply (type_addr_of _ _) _)
     | W.BinOp _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_bin_op _ _ _ _ _ _) _)
     | W.UnOp _ _ _ => notypeclasses refine (tac_fast_apply (type_un_op _ _ _ _) _)
@@ -187,7 +187,7 @@ Ltac liRExpr :=
 Ltac liRJudgement :=
   lazymatch goal with
     | |- envs_entails _ (typed_write _ _ _ _ _) => notypeclasses refine (tac_fast_apply (type_write _ _ _ _ _ _ _) _); [ solve [refine _ ] |]
-    | |- envs_entails _ (typed_read _ _ _) => notypeclasses refine (tac_fast_apply (type_read _ _ _ _ _) _); [ solve [refine _ ] |]
+    | |- envs_entails _ (typed_read _ _ _ _) => notypeclasses refine (tac_fast_apply (type_read _ _ _ _ _ _) _); [ solve [refine _ ] |]
     | |- envs_entails _ (typed_callable _ _ _) => notypeclasses refine (tac_fast_apply (type_callable _ _ _ _) _)
     | |- envs_entails _ (typed_addr_of _ _) => notypeclasses refine (tac_fast_apply (type_addr_of_place _ _ _ _) _); [solve [refine _] |]
   end.

theories/typing/globals.v

@@ -30,8 +30,8 @@ Section globals.
   Global Instance initialized_persistent A name (x : A) : Persistent (initialized name x).
   Proof. apply _. Qed.
 
-  Global Instance initialized_intro_persistent A name (x : A) : IntroPersistent (initialized name x).
-  Proof. constructor. apply _. Qed.
+  Global Instance initialized_intro_persistent A name (x : A) : IntroPersistent (initialized name x) (initialized name x).
+  Proof. constructor. iIntros "#$". Qed.
 
   Lemma simplify_global_with_type_hyp name β ty l T `{!FastDone (global_locs !! name = Some l)} :
     (l ◁ₗ{β} ty -∗ T) -∗

theories/typing/optional.v

@@ -356,14 +356,14 @@ Section optionalO.
     TypedBinOp v1 (v1 ◁ᵥ b @ optionalO ty optty)%I v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 :=
     λ T, i2p (type_neq_optionalO A v1 v2 ty optty ot1 ot2 T b).
 
-  Lemma read_optionalO_case A l b (ty : A → type) optty ly (T : val → type →</