Refactor the [int] type to use [val_to_Z]..

examples/proofs/wrapping_add/wrapping_rules.v

@@ -21,16 +21,16 @@ Section type.
     iDestruct ("HT" with "Hty2") as (Hv2) "HT".
     iIntros (Φ) "HΦ".
     iDestruct ("HT" with "[] []" ) as (??) "HT".
-    1-2: iPureIntro; by apply: val_of_Z_in_range.
+    1-2: iPureIntro; by apply: val_to_Z_in_range.
     have /val_of_Z_is_some[v Hv] : ((n1 + n2) `mod` int_modulus it1) ∈ it1 by apply int_modulus_mod_in_range.
-    move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. subst it2.
+    subst it2.
     iApply (wp_binop_det v). iSplit.
     - iIntros (σ v') "_ !%". split.
       + inversion 1; simplify_eq/=.
         by destruct it1 as [? []]; simplify_eq/=.
       + move => ->. econstructor => //.
         by destruct it1 as [? []]; simplify_eq/=.
-    - iIntros "!>". iApply "HΦ"; last done. by iPureIntro.
+    - iIntros "!>". iApply "HΦ"; last done. iPureIntro. by apply val_to_of_int.
   Qed.
 
   Global Instance macro_wrapping_add_inst it1 it2 e1 e2 :

linux/pkvm/proofs/spinlock/spinlock_proof.v

@@ -161,8 +161,6 @@ Section proofs.
              iApply (wp_cas_suc _ _ _ v2 v4 next next _ _ _ u16 _ _ with "Hnext Hticket") => //.
              { by rewrite val_to_of_loc. }
              { by rewrite val_to_of_loc. }
-             { by apply val_to_of_int. }
-             { by apply val_to_of_int. }
              { cbv. lia. }
              iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (true @ boolean bool_it))%I) => //.
              repeat liRStep; liShow.
@@ -210,8 +208,6 @@ Section proofs.
              iApply (wp_cas_fail _ _ _ v2 v4 next i _ _ _ u16 _ _ with "Hnext Hticket") => //.
              { by rewrite val_to_of_loc. }
              { by rewrite val_to_of_loc. }
-             { by apply val_to_of_int. }
-             { by apply val_to_of_int. }
              { cbv. lia. }
              iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (false @ boolean bool_it))%I) => //.
              repeat liRStep; liShow.
@@ -280,8 +276,6 @@ Section proofs.
              iApply (wp_cas_suc _ _ _ v2 v4 next next _ _ _ u16 _ _ with "Hnext Hticket") => //.
              { by rewrite val_to_of_loc. }
              { by rewrite val_to_of_loc. }
-             { by apply val_to_of_int. }
-             { by apply val_to_of_int. }
              { cbv. lia. }
              iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (true @ boolean bool_it))%I) => //.
              iRename select (p at{struct_hyp_spinlock}ₗ _ ↦ _)%I into "Hnext".
@@ -320,8 +314,6 @@ Section proofs.
              iApply (wp_cas_fail _ _ _ v2 v4 next i _ _ _ u16 _ _ with "Hnext Hticket") => //.
              { by rewrite val_to_of_loc. }
              { by rewrite val_to_of_loc. }
-             { by apply val_to_of_int. }
-             { by apply val_to_of_int. }
              { cbv. lia. }
              iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (false @ boolean bool_it))%I) => //.
              iRename select (p at{struct_hyp_spinlock}ₗ _ ↦ _)%I into "Hnext".
@@ -382,7 +374,7 @@ Section proofs.
           iDestruct "Hcases" as "[[Hticket' %] | Htok]".
           { iExFalso. by iApply (ticket_non_duplicable with "Hticket Hticket'"). }
           iAssert (⌜owner ∈ u16⌝)%I as %[??].
-          { rewrite /ty_own_val /=. by iDestruct "Hv" as %Hv%val_of_Z_in_range. }
+          { rewrite /ty_own_val /=. by iDestruct "Hv" as %Hv%val_to_Z_in_range. }
           iAssert (⌜owner < next⌝)%I as %?.
           { destruct (decide (owner < next)); first done. iExFalso.
             iDestruct (ty_size_eq with "Hv") as %?.
@@ -484,7 +476,7 @@ Section proofs.
         (* Learn that [next'] actually is [max_int u16]. *)
         iAssert ⌜next' = max_int u16⌝%I as %->.
         { iDestruct (ty_deref with "Hnext") as (w) "[_ H]". iDestruct "H" as %Hnext.
-          iPureIntro. apply val_of_Z_in_range in Hnext as [??]. lia. }
+          iPureIntro. apply val_to_Z_in_range in Hnext as [??]. lia. }
         (* We perform the write and close the invariant. *)
         iDestruct (ty_aligned with "Howner") as %?.
         iDestruct (ty_deref with "Howner") as (v') "[Hl Hv]".
@@ -511,7 +503,7 @@ Section proofs.
         iAssert ⌜owner' = 0⌝%I as %->.
         { destruct (decide (owner' = 0)) => //. iExFalso.
           iDestruct (ty_deref with "Howner") as (?) "[? Hv]".
-          iDestruct "Hv" as %Howner%val_of_Z_in_range. destruct Howner as [Howner ?].
+          iDestruct "Hv" as %Howner%val_to_Z_in_range. destruct Howner as [Howner ?].
           iDestruct (overlaping_ticket_ranges with "[] Htk Htr1") as "$".
           iPureIntro. exists 0. split; apply elem_of_seqZ; try done.
           split => //. rewrite /min_int /= in Howner. lia. }
@@ -558,7 +550,7 @@ Section proofs.
         iDestruct (ty_aligned with "Howner") as %?.
         iDestruct (ty_deref with "Howner") as (v') "[Hl Hv]".
         iDestruct (ty_size_eq with "Hv") as %?.
-        iDestruct "Hv" as %?%val_of_Z_in_range.
+        iDestruct "Hv" as %?%val_to_Z_in_range.
         iSplitL "Hl". { iExists _. by iFrame "Hl". }
         iIntros "!> Hl".
         iMod "Hclose" as "_". iMod ("Hclose_inv" with "[Htok H● H◯ Hticket Hnext Hl Htk1 Htk2]") as "_".
@@ -568,8 +560,8 @@ Section proofs.
           iSplit. { iPureIntro. by lia. }
           iDestruct ((ty_ref (t := (owner + 1) @ int u16)) with "[] Hl []") as "$" => //.
           { iPureIntro. rewrite /i2v.
-            destruct (val_of_Z (owner + 1) u16) eqn:Heq => //. exfalso.
-            assert (owner + 1 ∈ u16) as Hu16%val_of_Z_is_some by (split; lia).
+            destruct (val_of_Z (owner + 1)) eqn:Heq => /=; first by apply val_to_of_int.
+            exfalso. assert (owner + 1 ∈ u16) as Hu16%val_of_Z_is_some by (split; lia).
             destruct Hu16 as [??]. by simplify_eq. }
           iRight. iFrame "Htok". by iExists _. }
         iModIntro.

theories/lang/byte.v

@@ -23,3 +23,10 @@ Proof.
   - left. assert (H1 = H2) as ->; [|done]. apply proof_irrel.
   - right. naive_solver.
 Qed.
+
+Lemma byte_eq (b1 b2 : byte) :
+  b1 = b2 ↔ b1.(byte_val) = b2.(byte_val).
+Proof.
+  destruct b1, b2. split; simpl; [ naive_solver|].
+  intros. subst. f_equal. apply proof_irrel.
+Qed.

theories/lang/int_type.v

@@ -123,3 +123,19 @@ Proof.
   destruct it as [? []] => //.
   split; unfold min_int, max_int => /=; lia.
 Qed.
+
+Lemma elem_of_int_type_0_to_127 (n : Z) (it : int_type):
+  0 ≤ n ≤ 127 → n ∈ it.
+Proof.
+  move => [??]. rewrite /elem_of /int_elem_of_it.
+  have ? := min_int_le_0 it.
+  have ? := max_int_ge_127 it.
+  lia.
+Qed.
+
+Lemma Z_of_bool_elem_of_int_type (b : bool) (it : int_type):
+  Z_of_bool b ∈ it.
+Proof.
+  apply elem_of_int_type_0_to_127.
+  destruct b => /=; lia.
+Qed.

theories/lang/val.v

@@ -138,6 +138,41 @@ Lemma val_of_Z_in_range it z v:
   val_of_Z z it = Some v → z ∈ it.
 Proof. rewrite /val_of_Z. case_bool_decide; by eauto. Qed.
 
+Lemma val_to_Z_go_in_range v n:
+  val_to_Z_go v = Some n → 0 ≤ n < 2 ^ (length v * bits_per_byte).
+Proof.
+  elim: v n => /=.
+  - move => n [] <-. split; first lia.
+    apply Z.pow_pos_nonneg; lia.
+  - move => ? v IH n. case_match => //.
+    destruct (val_to_Z_go v) => /=; last done.
+    move => [] <-. move: (IH z eq_refl).
+    move: (byte_constr b). rewrite /byte_modulus /bits_per_byte.
+    move => [??] [??]. split; first lia.
+    have ->: S (length v) * 8 = 8 + length v * 8 by lia.
+    rewrite Z.pow_add_r; lia.
+Qed.
+
+Lemma val_to_Z_in_range v it n:
+  val_to_Z v it = Some n → n ∈ it.
+Proof.
+  rewrite /val_to_Z. case_decide as Hlen; last done.
+  destruct (val_to_Z_go v) eqn:Heq => /=; last done.
+  move: Heq => /val_to_Z_go_in_range.
+  rewrite Hlen /elem_of /int_elem_of_it /max_int /min_int.
+  rewrite /int_half_modulus /int_modulus /bits_per_int.
+  destruct (it_signed it) eqn:Hsigned => /=.
+  - case_decide => /=.
+    + move => [??] [] ?. simplify_eq.
+      assert (2 ^ (bytes_per_int it * bits_per_byte) =
+              2 * 2 ^ (bytes_per_int it * bits_per_byte - 1)) as Heq.
+      { rewrite Z.sub_1_r. rewrite Z_pow_pred_r => //. rewrite /bits_per_byte.
+        have ? := bytes_per_int_gt_0 it. lia. }
+      rewrite Heq. lia.
+    + move => [??] [] ?. lia.
+  - move => [??] [] ?. lia.
+Qed.
+
 Lemma val_to_of_int z it v:
   val_of_Z z it = Some v → val_to_Z v it = Some z.
 Proof.
@@ -185,6 +220,47 @@ Lemma i2v_bool_Some b it:
   val_to_Z (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
 Proof. apply val_to_of_int. apply val_of_Z_bool. Qed.
 
+Lemma val_to_Z_go_Some_inj v1 v2 n:
+  length v1 = length v2 →
+  val_to_Z_go v1 = Some n →
+  val_to_Z_go v2 = Some n →
+  v1 = v2.
+Proof.
+  elim: v1 v2 n; first by destruct v2.
+  move => b1 v1 IH [] b2 v2 // n /= [] Hlen.
+  destruct b1 as [b1|?|] => //. destruct b2 as [b2|?|] => //.
+  destruct (val_to_Z_go v1) as [n1|] eqn:Hn1 => //.
+  destruct (val_to_Z_go v2) as [n2|] eqn:Hn2 => //.
+  move => /= [] <- [] Heq.
+  assert (n1 = n2 ∧ byte_val b1 = byte_val b2) as [??].
+  { move: Heq. clear.
+    have H1 := byte_constr b1.
+    have H2 := byte_constr b2.
+    move: H1 H2. rewrite /byte_modulus. lia. }
+  simplify_eq. f_equal; last by eapply IH. f_equal.
+  by apply byte_eq.
+Qed.
+
+Lemma val_to_Z_Some_inj v1 v2 it n:
+  val_to_Z v1 it = Some n →
+  val_to_Z v2 it = Some n →
+  v1 = v2.
+Proof.
+  rewrite /val_to_Z.
+  case_decide as Hlen1; last done.
+  case_decide as Hlen2; last done.
+  destruct (val_to_Z_go v1) as [n1|] eqn:Hn1 => //=.
+  destruct (val_to_Z_go v2) as [n2|] eqn:Hn2 => //=.
+  move: (Hn1) => /val_to_Z_go_in_range [Hb1 HB1]; rewrite Hlen1 in HB1.
+  move: (Hn2) => /val_to_Z_go_in_range [Hb2 HB2]; rewrite Hlen2 in HB2.
+  have Hlen: length v1 = length v2 by rewrite Hlen1 Hlen2.
+  move => <- Heq_if. eapply val_to_Z_go_Some_inj => //.
+  rewrite Hn2; f_equal. move: Heq_if.
+  rewrite /int_modulus /int_half_modulus /bits_per_int.
+  destruct (it_signed it) => /=; last naive_solver.
+  repeat case_bool_decide => /=; naive_solver lia.
+Qed.
+
 Arguments val_to_Z : simpl never.
 Arguments val_of_Z : simpl never.
 Typeclasses Opaque val_to_Z val_of_Z val_of_bool.

theories/typing/array.v

@@ -222,7 +222,7 @@ Section array.
     iDestruct ("HP" with "Hv") as (Hv) "HP".
     iDestruct "HP" as (? Hlen) "HP".
     have [|ty ?]:= lookup_lt_is_Some_2 tys (Z.to_nat i). lia.
-    iApply wp_ptr_offset => //. by apply val_to_of_loc. by apply val_to_of_int.
+    iApply wp_ptr_offset => //. by apply val_to_of_loc.
     iIntros "!#". iExists _. iSplit => //.
     iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //. rewrite Z2Nat.id//.
     iApply ("HP" $! ty with "[//] Hl"). iIntros (l' ty2 β2 typ R) "Hl' Htyp HT".

theories/typing/atomic_bool.v

@@ -7,34 +7,36 @@ Section atomic_bool.
   Context `{!typeG Σ}.
 
   Program Definition atomic_bool (it : int_type) (PT PF : iProp Σ) : type := {|
-    ty_own β l := (match β return _ with
-                  | Own => ∃ b, l ◁ₗ b @ boolean it ∗ if b then PT else PF
-                  | Shr => ⌜l `has_layout_loc` it⌝ ∗
-                          inv atomic_boolN (∃ b, l ↦ i2v (Z_of_bool b) it ∗ if b then PT else PF)
-                  end)%I
-  |}.
+    ty_own β l :=
+      match β return _ with
+      | Own => ∃ b, l ◁ₗ b @ boolean it ∗ if b then PT else PF
+      | Shr => ⌜l `has_layout_loc` it⌝ ∗
+               inv atomic_boolN (∃ b, l ↦ i2v (Z_of_bool b) it ∗ if b then PT else PF)
+      end;
+  |}%I.
   Next Obligation.
-    iIntros (PT PF l E HE) => /=. iDestruct 1 as (b) "[Hb Hown]".
+    iIntros "%it %PT %PF %l %E %HE (%b&Hb&Hown)".
     iDestruct (ty_aligned with "Hb") as %?. iSplitR => //.
-    iApply inv_alloc. iIntros "!#". iExists b. iFrame.
-    iDestruct (ty_deref with "Hb") as (v) "[Hl Hb]".
-    (* TODO: don't unfold here *)
-    rewrite /i2v. by iDestruct "Hb" as %->.
+    iApply inv_alloc. iNext. iExists b. iFrame.
+    iDestruct (ty_deref with "Hb") as "(%v&Hl&Hb)".
+    by iDestruct (boolean_own_val_eq with "Hb") as %<-.
   Qed.
 
   Global Program Instance movable_atomic_bool it PT PF : Movable (atomic_bool it PT PF) := {|
     ty_layout := it_layout it;
     ty_own_val v := ∃ b, v ◁ᵥ b @ boolean it ∗ if b then PT else PF;
   |}%I.
-  Next Obligation. iIntros (it PT PF l). iDestruct 1 as (?) "[Hb _]". by iApply (ty_aligned with "Hb"). Qed.
-  Next Obligation. iIntros (it PT PF v). iDestruct 1 as (?) "[Hb _]". by iApply (ty_size_eq with "Hb"). Qed.
+  Next Obligation. iIntros (????) "[% [Hb _]]". by iApply (ty_aligned with "Hb"). Qed.
+  Next Obligation. iIntros (????) "[% [Hb _]]". by iApply (ty_size_eq with "Hb"). Qed.
   Next Obligation.
-    iIntros (it PT PF v). iDestruct 1 as (?) "[Hb ?]".
-    iDestruct (ty_deref with "Hb") as (?) "[? ?]". eauto with iFrame.
+    iIntros (????) "[% [Hb ?]]".
+    iDestruct (ty_deref with "Hb") as (?) "[? ?]".
+    eauto with iFrame.
   Qed.
   Next Obligation.
-    iIntros (it PT PF l v ?) "Hl". iDestruct 1 as (?) "[Hb ?]".
-    iDestruct (ty_ref with "[] Hl Hb") as "?" => //. iExists _. iFrame.
+    iIntros (??????) "Hl [%b [Hb ?]]".
+    iDestruct (ty_ref with "[] Hl Hb") as "?" => //.
+    iExists b. iFrame.
   Qed.
 
 End atomic_bool.
@@ -57,29 +59,35 @@ Section programs.
     λ T, i2p (subsume_atomic_bool_own_int l n it PT PF T).
 
   Lemma type_read_atomic_bool l β it PT PF T:
-    (∀ 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)))) -∗
+    (∀ 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]".
+    unfold destruct_hint. iIntros "HT Hl". destruct β.
+    - iDestruct "Hl" as "[%b [Hl Hif]]".
       iApply fupd_mask_intro => //. iIntros "Hclose".
       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 => //=.
+      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").
+      iExists b. iFrame. by iApply (ty_ref with "[] Hl Hv").
     - iDestruct "Hl" as (Hly) "#Hinv".
       iInv "Hinv" as (b) "[>Hl Hif]" "Hclose".
       iApply fupd_mask_intro. set_solver. iIntros "Hclose2".
       iExists _, _, _, (t2mt (b @ boolean it)). iFrame.
       rewrite /has_layout_val i2v_bool_length.
-      do 2 iSplitR => //=. iSplitR => //. { by rewrite /ty_own_val/= val_of_Z_bool. }
+      do 2 iSplitR => //=. iSplitR; first by iApply boolean_own_val_eq.
       iIntros "!# Hl". iDestruct ("HT" with "Hif") as "[Hif $]".
-      iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"). { iExists _. by iFrame. }
+      iMod "Hclose2" as "_".
+      iMod ("Hclose" with "[-]"). { iExists _. by iFrame. }
       iModIntro. by iSplitR.
   Qed.
   Global Instance type_read_atomic_bool_inst l β it PT PF:
@@ -87,13 +95,19 @@ Section programs.
     λ 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))) -∗
+    (∃ 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.
   Proof.
-    iIntros "HT Hl Hv". iDestruct "HT" as (bnew) "Hsub".
-    iDestruct ("Hsub" with "Hv") as "(Hnew&->&Hif'&HT)".
+    iIntros "[%bnew Hsub] Hl Hv".
+    iDestruct ("Hsub" with "Hv") as "(Hnew&->&Hif_new&HT)".
     destruct β.
-    - iDestruct "Hl" as (bold) "[Hl Hif]".
+    - iDestruct "Hl" as "[%bold [Hl Hif_old]]".
       iApply fupd_mask_intro => //. iIntros "Hc".
       iDestruct (ty_aligned with "Hl") as %?.
       iDestruct (ty_deref with "Hl") as (vb) "[Hmt Hold]".
@@ -104,12 +118,13 @@ Section programs.
       iApply (@ty_ref with "[] Hl") => //. done.
     - iDestruct "Hl" as (?) "#Hinv".
       iInv "Hinv" as (b) "[>Hmt Hif]" "Hc".
-      iApply fupd_mask_intro; first solve_ndisj. iIntros "Hc2".
-      iSplitL "Hmt".
+      iApply fupd_mask_intro; first solve_ndisj.
+      iIntros "Hc2". iSplitL "Hmt".
       { iExists _; iFrame; iPureIntro; split => //. apply i2v_bool_length. }
       iIntros "!# Hl". iMod "Hc2".
-      iMod ("Hc" with "[Hif' Hl Hnew]").
-      { iModIntro. iExists bnew. iFrame. rewrite /i2v. by iDestruct "Hnew" as %->. }
+      iDestruct (boolean_own_val_eq with "Hnew") as %->.
+      iMod ("Hc" with "[Hif_new Hl]").
+      { iModIntro. iExists bnew. iFrame. }
       iModIntro. iExists _. iFrame. by iSplit.
   Qed.
   Global Instance type_write_atomic_bool_inst l β it PT PF v ty `{!Movable ty}:
@@ -117,37 +132,51 @@ Section programs.
     λ T, i2p (type_write_atomic_bool l β it PT PF v ty T).
 
   Lemma type_cas_atomic_bool (l : loc) β it PT PF lexp Pexp vnew Pnew T:
-    (∃ bexp bnew, subsume Pexp (lexp ◁ₗ bexp @ boolean it) (
-                  subsume Pnew (vnew ◁ᵥ bnew @ boolean it) ( ⌜bytes_per_int it ≤ bytes_per_addr⌝%nat ∗ (
-        ((if bexp then PT else PF) -∗ (if bnew then PT else PF) ∗ (
-            l ◁ₗ{β} atomic_bool it PT PF -∗ lexp ◁ₗ bexp @ boolean it -∗
-              T (val_of_bool true) (t2mt (true @ boolean bool_it)))) ∧
-            (l ◁ₗ{β} atomic_bool it PT PF -∗ lexp ◁ₗ negb bexp @ boolean it -∗
-                             T (val_of_bool false) (t2mt (false @ boolean bool_it)))
-    )))) -∗
+    (∃ bexp bnew,
+      subsume Pexp (lexp ◁ₗ bexp @ boolean it) (
+        subsume Pnew (vnew ◁ᵥ bnew @ boolean it) (
+          ⌜bytes_per_int it ≤ bytes_per_addr⌝%nat ∗ (
+            ((if bexp then PT else PF) -∗
+             (if bnew then PT else PF) ∗ (
+                l ◁ₗ{β} atomic_bool it PT PF -∗ lexp ◁ₗ bexp @ boolean it -∗
+                T (val_of_bool true) (t2mt (true @ boolean bool_it)))) ∧
+            (l ◁ₗ{β} atomic_bool it PT PF -∗
+             lexp ◁ₗ negb bexp @ boolean it -∗
+             T (val_of_bool false) (t2mt (false @ boolean bool_it)))
+           )
+        )
+      )
+    ) -∗
     typed_cas (IntOp it) l (l ◁ₗ{β} (atomic_bool it PT PF))%I lexp Pexp vnew Pnew T.
   Proof.
-    iDestruct 1 as (bexp bnew) "Hsub". iIntros "Hl Hlexp Hvnew".
+    iIntros "(%bexp&%bnew&Hsub) Hl Hlexp Hvnew".
     iDestruct ("Hsub" with "Hlexp") as "[Hlexp Hsub]".
     iDestruct ("Hsub" with "Hvnew") as "[Hvnew [% Hsub]]".
     iIntros (Φ) "HΦ".
     (* TODO: don't unfold here *)
-    rewrite {1 2}/boolean/boolean_inner_type/int_inner_type/=.
+    rewrite {1 2}/boolean/boolean_inner_type/int/int_inner_type/=.
     iDestruct "Hlexp" as (ve Hve Hle) "He" => /=.
     iDestruct "Hvnew" as %Hvnew.
     destruct β.
     - iDestruct "Hl" as (b) "[Hb Hif]".
       (* TODO: don't unfold here *)
-      rewrite {1}/boolean/boolean_inner_type/int_inner_type/=.
+      rewrite {1}/boolean/boolean_inner_type/int/int_inner_type/=.
       iDestruct "Hb" as (vb Hvb Hlb) "Hb" => /=.
       destruct (decide (b = bexp)); subst.
-      + iApply (wp_cas_suc with "Hb He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply: val_of_Z_length].
+      + iApply (wp_cas_suc with "Hb He") => //.
+        { by apply val_to_of_loc. }
+        { by apply val_to_of_loc. }
+        { by eapply val_to_Z_length. }
         iIntros "!# Hb Hexp".
         iDestruct "Hsub" as "[Hsub _]". iDestruct ("Hsub" with "Hif") as "[Hif HT]".
         iApply "HΦ". 2: iApply ("HT" with "[Hb Hif]"). done.
         * iExists bnew. iFrame "Hif". iExists _. by iFrame.
         * iExists _. by iFrame.
-      + iApply (wp_cas_fail with "Hb He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply: val_of_Z_length]; try by [destruct b,bexp].
+      + iApply (wp_cas_fail with "Hb He") => //.
+        { by apply val_to_of_loc. }
+        { by apply val_to_of_loc. }
+        { by eapply val_to_Z_length. }
+        { by destruct b, bexp. }
         iIntros "!# Hb Hexp".
         iDestruct "Hsub" as "[_ HT]".
         iApply "HΦ". 2: iApply ("HT" with "[Hb Hif]"). done.
@@ -157,20 +186,42 @@ Section programs.
       iInv "Hinv" as "Hb".
       iDestruct "Hb" as (b) "[>Hmt Hif]".
       destruct (decide (b = bexp)); subst.
-      + iApply (wp_cas_suc with "Hmt He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply: val_of_Z_length]; try by [apply i2v_bool_Some].
+      + iApply (wp_cas_suc with "Hmt He") => //.
+        { by apply val_to_of_loc. }
+        { by apply val_to_of_loc. }
+        { apply val_to_of_int. rewrite /i2v.
+          have Hin: Z_of_bool bexp ∈ it by apply Z_of_bool_elem_of_int_type.
+          apply val_of_Z_is_some in Hin. destruct Hin as [? ->]. done. }
+        { by eapply val_to_Z_length. }
         iIntros "!# Hb Hexp".
         iDestruct "Hsub" as "[Hsub _]". iDestruct ("Hsub" with "Hif") as "[Hif HT]".
-        iModIntro. iSplitL "Hb Hif". { by iExists bnew; iFrame; rewrite /i2v Hvnew. }
+        iModIntro. iSplitL "Hb Hif".
+        { iExists bnew. iFrame.
+          assert (vnew = i2v (Z_of_bool bnew) it) as ->; last done.
+          rewrite /i2v.
+          have Hin: Z_of_bool bnew ∈ it by apply Z_of_bool_elem_of_int_type.
+          apply val_of_Z_is_some in Hin. destruct Hin as [? Heq]. rewrite Heq /=.
+          apply val_to_of_int in Heq. by eapply val_to_Z_Some_inj. }
         iApply "HΦ". 2: iApply ("HT" with "[]"). done.
         * by iSplit.
         * iExists _. by iFrame.
-      + iApply (wp_cas_fail with "Hmt He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply i2v_bool_Some]; try by [apply: val_of_Z_length]; try by [destruct b,bexp].
+      + iApply (wp_cas_fail with "Hmt He") => //.
+        { by apply val_to_of_loc. }
+        { by apply val_to_of_loc. }
+        { apply val_to_of_int. rewrite /i2v.
+          have Hin: Z_of_bool b ∈ it by apply Z_of_bool_elem_of_int_type.
+          apply val_of_Z_is_some in Hin. destruct Hin as [? ->]. done. }
+        { by eapply val_to_Z_length. }
+        { by destruct b, bexp. }
         iIntros "!# Hb Hexp".
         iDestruct "Hsub" as "[_ HT]".
         iModIntro. iSplitL "Hb Hif". { by iExists b; iFrame; rewrite /i2v Hvnew. }
         iApply "HΦ". 2: iApply ("HT" with "[]"). done.
         * by iSplit.
-        * iExists _. iFrame. rewrite val_of_Z_bool. by destruct b, bexp.
+        * iExists _. iFrame. iSplit; last done. iPureIntro. rewrite /i2v.
+          have Hin: Z_of_bool b ∈ it by apply Z_of_bool_elem_of_int_type.
+          apply val_of_Z_is_some in Hin. destruct Hin as [? Heq]. rewrite Heq /=.
+          apply val_to_of_int in Heq. rewrite Heq. by destruct b, bexp.
   Qed.
   Global Instance type_cas_atomic_bool_inst (l : loc) β it PT PF (lexp : loc) Pexp vnew Pnew:
     TypedCas (IntOp it) l (l ◁ₗ{β} (atomic_bool it PT PF))%I lexp Pexp vnew Pnew :=

theories/typing/bytes.v

@@ -149,10 +149,10 @@ Section bytewise.
     typed_bin_op v2 (v2 ◁ᵥ n @ int it) p (p ◁ₗ{β} bytewise P ly) (PtrOffsetOp u8) (IntOp it) PtrOp T.
   Proof.
     iIntros "HT" (Hint) "Hp". iIntros (Φ) "HΦ".
-    move: (Hint) => /val_of_Z_in_range?.
+    move: (Hint) => /val_to_Z_in_range?.
     iDestruct ("HT" with "[//]") as (??) "HT".
     iDestruct (split_bytewise (Z.to_nat n) with "Hp") as "[H1 H2]"; [lia..|].
-    iApply wp_ptr_offset. by apply val_to_of_loc. by apply val_to_of_int. done.
+    iApply wp_ptr_offset. by apply val_to_of_loc. done. done.
     iModIntro. rewrite offset_loc_sz1//.
     iApply ("HΦ" with "[H2]"). 2: iApply ("HT" with "H1 []"). rewrite Z2Nat.id; [|lia]. by iFrame.
     by iPureIntro.

theories/typing/int.v

@@ -7,35 +7,34 @@ Section int.
 
   (* Separate definition such that we can make it typeclasses opaque later. *)
   Program Definition int_inner_type (it : int_type) (n : Z) : type := {|
-    ty_own β l := (∃ v, ⌜val_of_Z n it = Some v⌝ ∗ ⌜l `has_layout_loc` it⌝ ∗ l ↦[β] v)%I
-  |}.
+    ty_own β l := ∃ v, ⌜val_to_Z v it = Some n⌝ ∗ ⌜l `has_layout_loc` it⌝ ∗ l ↦[β] v;
+  |}%I.
   Next Obligation.
-    iIntros (it n l). iDestruct 1 as (v Hv Hl) "H". iExists _. do 2 iSplitR => //. by iApply heap_mapsto_own_state_share.
+    iIntros (it n l ??) "(%v&%Hv&%Hl&H)". iExists v.
+    do 2 (iSplitR; first done). by iApply heap_mapsto_own_state_share.
   Qed.
 
   Program Definition int (it : int_type) : rtype := {|
     rty_type := Z;
-    rty := int_inner_type it
+    rty := int_inner_type it;