starting to port RefinedVST to wp

refinedVST/lithium/instances.v

@@ -106,7 +106,7 @@ Lemma subsume_sep_list_insert_in_ig {prop:bi} {B} A id ig i x (l1 : list A) (l2
   return subsume (sep_list id A ig l1 f) (λ x : B, sep_list id A ig (l2 x) f) T.
 Proof.
   unfold CanSolve, sep_list => ?. iIntros "Hsub [<- Hl]".
-  rewrite insert_length. iApply "Hsub". iSplit; [done|].
+  rewrite length_insert. iApply "Hsub". iSplit; [done|].
   destruct (decide (i < length l1)%nat). 2: { by rewrite list_insert_ge; [|lia]. }
   iDestruct (big_sepL_insert_acc with "Hl") as "[? Hl]". { by apply: list_lookup_insert. }
   have [//|y ?]:= lookup_lt_is_Some_2 l1 i.
@@ -126,7 +126,7 @@ Lemma subsume_sep_list_insert_not_in_ig {prop:bi} A B id ig i x (l1 : list A) l2
       exhale <affine> f i x2;
       return T y.
 Proof.
-  unfold CanSolve, sep_list. iIntros (?) "[% Hsub] [<- Hl]". rewrite big_sepL_insert // insert_length.
+  unfold CanSolve, sep_list. iIntros (?) "[% Hsub] [<- Hl]". rewrite big_sepL_insert // length_insert.
   iDestruct "Hl" as "[Hx Hl]". case_bool_decide => //.
   iDestruct ("Hsub" with "Hx [Hl]") as "[% [[%Heq Hl] [% [% [? HT]]]]]". {
     iSplit; [done|]. iApply (big_sepL_impl with "Hl"). iIntros "!>" (???) "?".

refinedVST/lithium/simpl_instances.v

@@ -350,7 +350,7 @@ Proof.
   clear IsEx0. unfold SimplAndUnsafe in *. elim: ig l1 l2.
   - move => ??/=. move => ?. naive_solver.
   - move => i ig IH l1 l2/= [x /IH Hi ] i'.
-    move: (Hi i') => [<- Hlookup]. rewrite insert_length. split => //.
+    move: (Hi i') => [<- Hlookup]. rewrite length_insert. split => //.
     move => Hi'. rewrite -Hlookup ?list_lookup_insert_ne; set_solver.
 Qed.
 
@@ -367,10 +367,10 @@ Global Instance simpl_fmap_app_and {A B} (l : list A) l1 l2 (f : A → B):
 Proof.
   split.
   - move => [Hl1 Hl2]; subst.
-    rewrite -Hl1 -fmap_app fmap_length take_length_le ?take_drop //.
-    rewrite -Hl1 fmap_length take_length. lia.
+    rewrite -Hl1 -fmap_app length_fmap length_take_le ?take_drop //.
+    rewrite -Hl1 length_fmap length_take. lia.
   - move => /fmap_app_inv [? [? [? [? Hfmap]]]]; subst.
-    by rewrite fmap_length take_app_length drop_app_length.
+    by rewrite length_fmap take_app_length drop_app_length.
 Qed.
 Global Instance simpl_fmap_assume_inj_Unsafe {A B} (l1 l2 : list A) (f : A → B) `{!AssumeInj (=) (=) f}:
   SimplAndUnsafe (f <$> l1 = f <$> l2) (l1 = l2).
@@ -383,11 +383,11 @@ Proof.
   - move => [n'[?[??]]]; subst.
     have ->: (n = n' + (n - n'))%nat by lia. rewrite replicate_add. do 2 f_equal. lia.
   - move => Hr.
-    have Hn: (n = length l1 + length l2)%nat by rewrite -(replicate_length n x) -app_length Hr.
-    move: Hr. rewrite Hn replicate_add => /app_inj_1[|<- <-]. 1: by rewrite replicate_length.
+    have Hn: (n = length l1 + length l2)%nat by rewrite -(length_replicate n x) -app_length Hr.
+    move: Hr. rewrite Hn replicate_add => /app_inj_1[|<- <-]. 1: by rewrite length_replicate.
     exists (length l1). repeat split => //.
-    + rewrite !replicate_length. f_equal. lia.
-    + rewrite !replicate_length. lia.
+    + rewrite !length_replicate. f_equal. lia.
+    + rewrite !length_replicate. lia.
 Qed.
 
 Global Instance simpl_replicate_eq_nil {A} (x : A) n :

refinedVST/typing/automation/proof_state.v

@@ -22,7 +22,7 @@ Inductive BLOCK_PRECOND_HINT := | BLOCK_PRECOND (bid : label).
 Inductive ASSERT_COND_HINT := | ASSERT_COND (id : string).
 
 (* The `{!typeG Σ} is necessary to infer Σ if P is True. *)
-Definition IPROP_HINT `{!typeG Σ} {A B} (a : A) (P : B → iProp Σ) : Prop := True.
+Definition IPROP_HINT `{!typeG OK_ty Σ} {A B} (a : A) (P : B → iProp Σ) : Prop := True.
 Arguments IPROP_HINT : simpl never.
 
 Notation "'block' bid : P" := (IPROP_HINT (BLOCK_PRECOND bid) (λ _ : unit, P)) (at level 200, only printing).
@@ -34,7 +34,7 @@ Arguments CODE_MARKER : simpl never.
 Ltac unfold_code_marker_and_compute_map_lookup :=
   unfold CODE_MARKER in *; solvers.compute_map_lookup.
 
-Definition RETURN_MARKER `{!typeG Σ} {cs:compspecs} (R : val → type → iProp Σ) : val → type → iProp Σ := R.
+Definition RETURN_MARKER `{!typeG OK_ty Σ} {cs:compspecs} (R : val → type → iProp Σ) : val → type → iProp Σ := R.
 Notation "'HIDDEN'" := (RETURN_MARKER _) (only printing).
 
 
@@ -162,7 +162,7 @@ Ltac print_coq_hyps :=
     lazymatch X with
     | IPROP_HINT _ _ => fail
     | gFunctors => fail
-    | typeG _ => fail
+    | typeG _ _ => fail
     | globalG _ => fail
     | _ => idtac H ":" X; fail
     end

refinedVST/typing/boolean.v

@@ -22,7 +22,7 @@ Definition is_bool_ot (ot : op_type) (it : int_type) (stn : bool_strictness) : P
   end.*)
 
 Section is_bool_ot.
-  Context `{!typeG Σ}.
+  Context `{!typeG OK_ty Σ}.
 
   Lemma represents_boolean_eq stn n b :
     represents_boolean stn n b → bool_decide (n ≠ 0) = b.
@@ -48,33 +48,35 @@ Section is_bool_ot.
 End is_bool_ot.
 
 Section generic_boolean.
-  Context `{!typeG Σ} {cs : compspecs}.
+  Context `{!typeG OK_ty Σ} {cs : compspecs}.
 
   Program Definition generic_boolean_type (stn: bool_strictness) (it: Ctypes.type) (b: bool) : type := {|
     ty_has_op_type ot mt := (*is_bool_ot ot it stn*) ot = it;
     ty_own β l :=
-      ∃ v n, ⌜val_to_Z v it = Some n⌝ ∧
+      ∃ v n, ⌜tc_val it v⌝ ∧
+             ⌜val_to_Z v it = Some n⌝ ∧
              ⌜represents_boolean stn n b⌝ ∧
              ⌜field_compatible it [] l⌝ ∧
              l ↦_it[β] v;
-      ty_own_val v := ∃ n, <affine> ⌜val_to_Z v it = Some n⌝ ∗ <affine> ⌜represents_boolean stn n b⌝;
+      ty_own_val v := ∃ n, <affine> ⌜tc_val it v ∧ val_to_Z v it = Some n⌝ ∗ <affine> ⌜represents_boolean stn n b⌝;
   |}%I.
   Next Obligation.
-    iIntros (??????) "(%v&%n&%&%&%&Hl)". iExists v, n.
+    iIntros (??????) "(%v&%n&%&%&%&%&Hl)". iExists v, n.
     by iMod (heap_mapsto_own_state_share with "Hl") as "$".
   Qed.
   Next Obligation.
-    iIntros (??????->) "(%&%&_&_&H&_)" => //.
+    iIntros (??????->) "(%&%&_&_&_&H&_)" => //.
   Qed.
   Next Obligation.
-    iIntros (??????->) "(%&%&%)". iPureIntro. destruct v; try done.
-    - rewrite /has_layout_val /tc_val' =>?. destruct it; try done.
-  Admitted.
+    iIntros (??????->) "(%&(%&%)&%)". iPureIntro. destruct v; try done.
+    - rewrite /has_layout_val /tc_val' =>?. destruct it; done.
+    - rewrite /has_layout_val /tc_val' =>?. destruct it; done.
+  Qed.
   Next Obligation.
-    iIntros (??????->) "(%&%&%&%&%&?)". eauto with iFrame.
+    iIntros (??????->) "(%&%&%&%&%&%&?)". eauto with iFrame.
   Qed.
   Next Obligation.
-    iIntros (?????? v -> ?) "Hl (%n&%&%)". iExists v, n; eauto with iFrame.
+    iIntros (?????? v -> ?) "Hl (%n&(%&%)&%)". iExists v, n; eauto with iFrame.
   Qed.
 (*  Next Obligation.
     iIntros (????????). apply: mem_cast_compat_bool; [naive_solver|]. iPureIntro. naive_solver.
@@ -85,10 +87,10 @@ Section generic_boolean.
 
   Global Program Instance generic_boolean_copyable b stn it : Copyable (b @ generic_boolean stn it).
   Next Obligation.
-    iIntros (????????) "(%v&%n&%&%&%&Hl)".
+    iIntros (????????) "(%v&%n&%&%&%&%&Hl)".
     simpl in *; subst.
     iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //.
-    iSplitR; first done; iExists q, v; eauto 8 with iFrame.
+    iSplitR; first done; iExists q, v; eauto 9 with iFrame.
   Qed.
 
 (*  Global Instance alloc_alive_generic_boolean b stn it β: AllocAlive (b @ generic_boolean stn it) β True.
@@ -115,7 +117,7 @@ Notation u8 := (Tint I8 Unsigned noattr).
 Notation builtin_boolean := (generic_boolean StrictBool u8).
 
 Section generic_boolean.
-  Context `{!typeG Σ} {cs : compspecs}.
+  Context `{!typeG OK_ty Σ} {cs : compspecs}.
 
   Inductive trace_if_bool :=
   | TraceIfBool (b : bool).
@@ -125,7 +127,7 @@ Section generic_boolean.
      li_trace (TraceIfBool b, b') (if b' then T1 else T2))
     ⊢ typed_if it v (v ◁ᵥ b @ generic_boolean stn it) T1 T2.
   Proof.
-    unfold case_destruct, li_trace. iIntros "[% Hs] (%n&%Hv&%Hb)".
+    unfold case_destruct, li_trace. iIntros "[% Hs] (%n&(%Hv&%)&%Hb)".
     apply represents_boolean_eq in Hb as <-.
     destruct it, v; try discriminate; eauto.
   Qed.
@@ -147,21 +149,22 @@ Section generic_boolean.
 End generic_boolean.
 
 Section boolean.
-  Context `{!typeG Σ} {cs : compspecs}.
+  Context `{!typeG OK_ty Σ} {cs : compspecs}.
 
   Lemma type_relop_boolean b1 b2 op b it v1 v2
     (Hop : match op with
-           | Oeq => Some (eqb b1 b2)
-           | One => Some (negb (eqb b1 b2))
+           | Cop.Oeq => Some (eqb b1 b2)
+           | Cop.One => Some (negb (eqb b1 b2))
            | _ => None
            end = Some b) T:
     T (i2v (bool_to_Z b) tint) (b @ boolean tint)
     ⊢ typed_bin_op v1 ⎡v1 ◁ᵥ b1 @ boolean it⎤
                  v2 ⎡v2 ◁ᵥ b2 @ boolean it⎤ op it it T.
   Proof.
-    iIntros "HT (%n1&%Hv1&%Hb1) (%n2&%Hv2&%Hb2) %Φ HΦ".
+    iIntros "HT (%n1&(%Hty1&%Hv1)&%Hb1) (%n2&(%Hty2&%Hv2)&%Hb2) %Φ HΦ".
     rewrite /wp_binop.
-    iIntros (?) "$".
+    (* some of this should move up to a wp rule in lifting_expr *)
+    iIntros "!>" (?) "$ !>".
     iExists (i2v (bool_to_Z b) tint); iSplit.
     - iStopProof; split => rho; monPred.unseal.
       apply bi.pure_intro.
@@ -176,8 +179,7 @@ Section boolean.
           -- subst; destruct s; inv Hv1; destruct b1, b2; simpl in *; congruence.
           -- destruct s; inv Hv1; destruct (eqb_spec b1 b2); try done; subst.
              ++ exploit (signed_inj i0 i1); congruence.
-             ++ if_tac in H0; inv H0.
-                if_tac in Hv2; inv Hv2.
+             ++ rewrite -H0 in Hv2.
                 exploit (unsigned_eq_eq i0 i1); congruence.
         * pose proof (Int64.eq_spec i i0) as Heq.
           destruct (Int64.eq i i0).
@@ -195,10 +197,10 @@ Section boolean.
       iSplit; [by destruct b | done].
   Qed.
   Definition type_eq_boolean_inst b1 b2 :=
-    [instance type_relop_boolean b1 b2 Oeq (eqb b1 b2)].
+    [instance type_relop_boolean b1 b2 Cop.Oeq (eqb b1 b2)].
   Global Existing Instance type_eq_boolean_inst.
   Definition type_ne_boolean_inst b1 b2 :=
-    [instance type_relop_boolean b1 b2 One (negb (eqb b1 b2))].
+    [instance type_relop_boolean b1 b2 Cop.One (negb (eqb b1 b2))].
   Global Existing Instance type_ne_boolean_inst.
 
 (*  (* TODO: replace this with a typed_cas once it is refactored to take E as an argument. *)
@@ -265,12 +267,12 @@ End boolean.
 Notation "'if' p " := (TraceIfBool p) (at level 100, only printing).
 
 Section builtin_boolean.
-  Context `{!typeG Σ} {cs : compspecs}.
+  Context `{!typeG OK_ty Σ} {cs : compspecs}.
 
   Lemma type_val_builtin_boolean b T:
     (T (b @ builtin_boolean)) ⊢ typed_value (Val.of_bool b) T.
   Proof.
-    iIntros "HT". iExists _. iFrame. iPureIntro. exists (if b then 1 else 0); destruct b; simpl; auto.
+    iIntros "HT". iExists _. iFrame. iPureIntro. exists (if b then 1 else 0); destruct b; simpl; done.
   Qed.
   Definition type_val_builtin_boolean_inst := [instance type_val_builtin_boolean].
   Global Existing Instance type_val_builtin_boolean_inst.

refinedVST/typing/globals.v

@@ -2,20 +2,20 @@ From VST.typing Require Export type.
 From VST.typing Require Import programs.
 From VST.typing Require Import type_options.
 
-Record global_type `{!typeG Σ} {cs : compspecs} := GT {
+Record global_type `{!typeG OK_ty Σ} {cs : compspecs} := GT {
   gt_A : Type;
   gt_type : gt_A → type;
 }.
 Arguments GT {_ _ _} _ _.
 
-Class globalG `{!typeG Σ} {cs : compspecs} := {
+Class globalG `{!typeG OK_ty Σ} {cs : compspecs} := {
   global_locs : gmap string address;
   global_initialized_types : gmap string global_type;
 }.
-Arguments globalG _ {_ _}.
+Arguments globalG _ _ {_ _}.
 
 Section globals.
-  Context `{!typeG Σ} {cs : compspecs} `{!globalG Σ}.
+  Context `{!typeG OK_ty Σ} {cs : compspecs} `{!globalG OK_ty Σ}.
   Import EqNotations.
 
   Definition global_with_type (name : string) (β : own_state) (ty : type) : iProp Σ :=

refinedVST/typing/programs.v

@@ -12,7 +12,7 @@ Open Scope Z.
 Definition val_to_Z (v : val) (t : Ctypes.type) : option Z :=
   match v, t with
   | Vint i, Tint _ Signed _ => Some (Int.signed i)
-  | Vint i, Tint sz Unsigned _ => if zlt (Int.unsigned i) (Z.pow 2 (bitsize_intsize sz)) then Some (Int.unsigned i) else None
+  | Vint i, Tint sz Unsigned _ => Some (Int.unsigned i)
   | Vlong i, Tlong Signed _ => Some (Int64.signed i)
   | Vlong i, Tlong Unsigned _ => Some (Int64.unsigned i)
   | _, _ => None
@@ -23,6 +23,11 @@ Proof.
   destruct sz; simpl; rep_lia.
 Qed.
 
+Lemma bitsize_half_max : forall sz, Z.pow 2 (bitsize_intsize sz - 1) ≤ Int.half_modulus.
+Proof.
+  destruct sz; simpl; rep_lia.
+Qed.
+
 Definition i2v n t :=
   match t with
   | Tint _ _ _ => Vint (Int.repr n)
@@ -32,17 +37,26 @@ Definition i2v n t :=
 
 Definition in_range (n:Z) (t: Ctypes.type) : Prop :=
   match t with
-  | Tint sz Signed _ => repable_signed n
+  | Tint IBool _ _ => 0 <= n < 2
+  | Tint sz Signed _ => - Z.pow 2 (bitsize_intsize sz - 1) <= n < Z.pow 2 (bitsize_intsize sz - 1)
   | Tint sz Unsigned _ => 0 <= n < Z.pow 2 (bitsize_intsize sz)
   | Tlong Signed _ => Int64.min_signed <= n <= Int64.max_signed
   | Tlong Unsigned _ => 0 <= n <= Int64.max_unsigned
   | _ => False
   end.
 
-Lemma val_to_Z_in_range : forall v t n, val_to_Z v t = Some n -> in_range n t.
+Lemma in_range_i2v : forall n t, in_range n t -> tc_val t (i2v n t).
 Proof.
-  intros; destruct v, t; try discriminate; destruct s; inv H; constructor; try rep_lia.
-  all: if_tac in H1; inv H1; rep_lia.
+  intros; destruct t; try done; simpl in *.
+  destruct i; simpl in *; try done.
+  - destruct s.
+    + rewrite Int.signed_repr; rep_lia.
+    + rewrite Int.unsigned_repr; rep_lia.
+  - destruct s.
+    + rewrite two_power_pos_equiv Int.signed_repr; rep_lia.
+    + rewrite Int.unsigned_repr; rep_lia.
+  - destruct (decide (n = 0)); subst; auto.
+    assert (n = 1) as -> by lia; auto.
 Qed.
 
 Definition int_eq v1 v2 :=
@@ -61,7 +75,8 @@ Proof.
   unfold elem_of, elem_of_type.
   destruct t; try solve [
     refine (right _ );  unfold not; intros; inv H].
-  all: destruct s;  unfold in_range;  apply _.
+  - destruct i0; (apply _ || destruct s; apply _).
+  - destruct s; apply _.
 Qed.
 
 (* Global Instance int_elem_of_type : ElemOf Integers.int Ctypes.type :=
@@ -72,12 +87,27 @@ Proof.
   intros.
   destruct t; try done; rewrite /val_to_Z /i2v; destruct s; simpl in H. 
   - rewrite Int.signed_repr //.
-  - rewrite Int.unsigned_repr; last by pose proof (bitsize_max i); rep_lia.
-    if_tac; [done | lia].
+    pose proof (bitsize_half_max i).
+    destruct i; rep_lia.
+  - rewrite Int.unsigned_repr //.
+    pose proof (bitsize_max i); destruct i; rep_lia.
   - rewrite Int64.signed_repr //.
   - rewrite Int64.unsigned_repr //.
 Qed.
 
+Lemma val_to_Z_in_range : forall t v n, val_to_Z v t = Some n -> tc_val t v -> n ∈ t.
+Proof.
+  destruct v; try done; destruct t; try done; simpl; intros.
+  - destruct i0; [destruct s; inv H; hnf; simpl; try rep_lia..|].
+    + rewrite two_power_pos_equiv in H0; lia.
+    + destruct H0, s; inv H; hnf.
+      * by rewrite Int.signed_zero.
+      * by rewrite Int.unsigned_zero.
+      * by rewrite Int.signed_one.
+      * by rewrite Int.unsigned_one.
+  - destruct s; inv H; hnf; rep_lia.
+Qed.
+
 Lemma signed_inj_64 : forall i1 i2, Int64.signed i1 = Int64.signed i2 -> i1 = i2.
 Proof.
   intros ?? H%(f_equal Int64.repr).
@@ -244,7 +274,7 @@ Section judgements.
   Class TypedUnOp (v : val) (P : assert) (o : Cop.unary_operation) (ot : Ctypes.type) : Type :=
     typed_un_op_proof T : iProp_to_Prop (typed_un_op v P o ot T).
 
-  Definition typed_exprs (el : list expr) (tl : typelist) (T : list val → list type → assert) : assert :=
+  Definition typed_exprs (el : list expr) (tl : list Ctypes.type) (T : list val → list type → assert) : assert :=
     (∀ Φ, (∀ vl (tys : list type), ([∗ list] v;ty∈vl;tys, ⎡v ◁ᵥ ty⎤) -∗ T vl tys -∗ Φ vl) -∗ wp_exprs el tl Φ).
   Global Arguments typed_exprs _ _ _%_I.
 
@@ -1329,12 +1359,12 @@ Section typing.
       simpl in *.
       destruct (Int.eq i0 Int.zero) eqn: Heq.
       + apply Int.same_if_eq in Heq as ->.
-        destruct s; [|if_tac in Hv]; inv Hv; done.
+        destruct s; inv Hv; done.
       + case_bool_decide; try done.
-        subst; destruct s; [|if_tac in Hv]; inv Hv.
+        subst; destruct s; inv Hv.
         * apply (val_lemmas.signed_inj _ Int.zero) in H0 as ->.
           rewrite Int.eq_true // in Heq.
-        * apply (client_lemmas.unsigned_eq_eq _ Int.zero) in H1 as ->.
+        * apply (client_lemmas.unsigned_eq_eq _ Int.zero) in H0 as ->.
           rewrite Int.eq_true // in Heq.
     - destruct v; try done.
       iSplit; first done; iFrame.