Add symbolic integers (naturals)

A deep embedding for integers.
Right now it only distinguishes natural numbers from general (unknown)
integers.

theories/c_translation/derived.v

@@ -4,6 +4,7 @@ From iris.algebra Require Import frac auth.
 From iris_c.lib Require Import locking_heap mset flock U.
 From iris_c.c_translation Require Import proofmode translation.
 
+(* TODO: this should be subsumbed by the deep embedding of the integers *)
 Class ValToNat (v : val) (n : nat) :=
   val_to_nat : v = #n.
 

theories/vcgen/dcexpr.v

@@ -12,10 +12,19 @@ Inductive dloc :=
 Global Instance dloc_decision : EqDecision dloc.
 Proof. solve_decision. Defined.
 
+(* Symbolic integers *)
+(* TODO: these should account for known non-natural integers as well *)
+Inductive dint : Type :=
+| dNat : nat → dint
+| dIntUnknown : Z → dint.
+
+Global Instance dint_decision : EqDecision dint.
+Proof. solve_decision. Defined.
+
 (* This data type is kind of redundant, as long as we don't have symbolic
 Booleans and integers *)
 Inductive dbase_lit : Type :=
-  | dLitInt : Z → dbase_lit
+  | dLitInt : dint → dbase_lit
   | dLitBool : bool → dbase_lit
   | dLitUnit : dbase_lit
   | dLitUnknown : base_lit → dbase_lit.
@@ -38,9 +47,16 @@ Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
   | dLocUnknown l => l
   end.
 
+Definition dint_interp (di : dint) : Z :=
+  match di with
+  | dNat n => Z.of_nat n
+  (* | dInt z => z *)
+  | dIntUnknown z => z
+  end.
+
 Definition dbase_lit_interp (l : dbase_lit) : base_lit :=
   match l with
-  | dLitInt x => LitInt x
+  | dLitInt x => LitInt (dint_interp x)
   | dLitBool b => LitBool b
   | dLitUnit => LitUnit
   | dLitUnknown l => l
@@ -54,18 +70,53 @@ Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
   | dValUnknown v => v
   end.
 
+Definition dval_to_nat (dv : dval) : option nat :=
+  match dv with
+  | dLitV (dLitInt (dNat n)) => Some n
+  | _ => None
+  end.
+
+Lemma dval_to_nat_correct E dv n :
+  dval_to_nat dv = Some n →
+  dval_interp E dv = #n.
+Proof.
+  intros Hv.
+  destruct dv; try inversion Hv.
+  case_match; simplify_eq/=.
+  case_match; simplify_eq/=.
+  done.
+Qed.
+
+(* TODO: beter heuristics here for operations like sub and div *) 
+Definition dbin_op_eval_nat (op : bin_op) (n1 n2 : nat) : dbase_lit :=
+  match op with
+  | PlusOp => dLitInt $ dNat $ (n1 + n2)%nat
+  | MinusOp => dLitInt $ dIntUnknown $ Z.of_nat n1 - Z.of_nat n2
+  | MultOp => dLitInt $ dNat $ (n1 * n2)%nat
+  | QuotOp => dLitInt $ dIntUnknown $ Z.of_nat n1 `quot` Z.of_nat n2
+  | RemOp => dLitInt $ dIntUnknown $ Z.of_nat n1 `rem` Z.of_nat n2
+  | AndOp => dLitInt $ dNat $ Nat.land n1 n2
+  | OrOp => dLitInt $ dNat $ Nat.lor n1 n2
+  | XorOp => dLitInt $ dNat $ Nat.lxor n1 n2
+  | ShiftLOp => dLitInt $ dIntUnknown $ Z.of_nat n1 ≪ Z.of_nat n2
+  | ShiftROp => dLitInt $ dIntUnknown $ Z.of_nat n1 ≫ Z.of_nat n2
+  | LeOp => dLitBool (bool_decide (n1 ≤ n2))
+  | LtOp => dLitBool (bool_decide (n1 < n2))
+  | EqOp => dLitBool (bool_decide (n1 = n2))
+  end.
+
 Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
   match op with
-  | PlusOp => dLitInt (n1 + n2)
-  | MinusOp => dLitInt (n1 - n2)
-  | MultOp => dLitInt (n1 * n2)
-  | QuotOp => dLitInt (n1 `quot` n2)
-  | RemOp => dLitInt (n1 `rem` n2)
-  | AndOp => dLitInt (Z.land n1 n2)
-  | OrOp => dLitInt (Z.lor n1 n2)
-  | XorOp => dLitInt (Z.lxor n1 n2)
-  | ShiftLOp => dLitInt (n1 ≪ n2)
-  | ShiftROp => dLitInt (n1 ≫ n2)
+  | PlusOp => dLitInt $ dIntUnknown $ n1 + n2
+  | MinusOp => dLitInt $ dIntUnknown $ n1 - n2
+  | MultOp => dLitInt $ dIntUnknown $ n1 * n2
+  | QuotOp => dLitInt $ dIntUnknown $ n1 `quot` n2
+  | RemOp => dLitInt $ dIntUnknown $ n1 `rem` n2
+  | AndOp => dLitInt $ dIntUnknown $ Z.land n1 n2
+  | OrOp => dLitInt $ dIntUnknown $ Z.lor n1 n2
+  | XorOp => dLitInt $ dIntUnknown $ Z.lxor n1 n2
+  | ShiftLOp => dLitInt $ dIntUnknown $ n1 ≪ n2
+  | ShiftROp => dLitInt $ dIntUnknown $ n1 ≫ n2
   | LeOp => dLitBool (bool_decide (n1 ≤ n2))
   | LtOp => dLitBool (bool_decide (n1 < n2))
   | EqOp => dLitBool (bool_decide (n1 = n2))
@@ -101,7 +152,10 @@ Definition dbin_op_eval
     then Some $ dLitV $ dLitBool
               $ bool_decide (dbase_lit_interp l1 = dbase_lit_interp l2)
     else match l1, l2 with
-         | dLitInt n1, dLitInt n2 => Some $ dLitV $ dbin_op_eval_int op n1 n2
+         | dLitInt (dNat n1), dLitInt (dNat n2) =>
+           Some $ dLitV $ dbin_op_eval_nat op n1 n2
+         | dLitInt z1, dLitInt z2 =>
+           Some $ dLitV $ dbin_op_eval_int op (dint_interp z1) (dint_interp z2)
          | dLitBool b1, dLitBool b2 => dLitV <$> dbin_op_eval_bool op b1 b2
          | _, _ => None
          end
@@ -110,7 +164,9 @@ Definition dbin_op_eval
 
 Definition dptr_plus_eval (E: known_locs) (dv1 dv2 : dval) : option dval :=
   match dv1,dv2 with
-  | dLocV (dLoc i j), dLitV (dLitInt o) =>
+  | dLocV (dLoc i j), dLitV (dLitInt (dNat o)) =>
+    (* TODO: here we need to additionaly check wether the argument 
+       is a natural number *)
     match offset_of_val (LitV (LitInt o)) with
     | None => None
     | Some k => Some $ dLocV $ dLoc i (j + k)
@@ -123,8 +179,12 @@ Lemma dptr_plus_eval_correct E dv1 dv2 w :
   cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E w).
 Proof.
   destruct dv1 as [?|??|[??|]|u1],dv2 as [[]|??|?|u2]; try naive_solver.
-  rewrite /cbin_op_eval /=. case_option_guard; inversion 1.
-  by rewrite cloc_of_to_val /= cloc_plus_plus.
+  rewrite /cbin_op_eval /=.
+  destruct d; last by inversion 1.
+  case_option_guard; inversion 1. 
+  rewrite cloc_of_to_val /=. 
+  case_option_guard; last contradiction. simpl.
+  rewrite cloc_plus_plus //.
 Qed.
 
 Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : option dval :=
@@ -144,8 +204,15 @@ Proof.
   unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
   { inversion 1. rewrite /bin_op_eval /=. f_equal. simplify_eq /=.
     do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
-  { destruct dl1, dl2, op; simpl; intros; simplify_eq/=; auto. }
-Qed.
+  { destruct dl1 as [[d1| ]| | |], dl2 as [[d2| ]| | | ], op;
+      simpl; intros; simplify_eq/=; auto.
+    by rewrite Nat2Z.inj_add.
+    by rewrite Nat2Z.inj_mul.
+    admit. (* Z.land vs Nat.land *)
+    admit. (* lor *)
+    admit. (* xor *)
+  }
+Admitted.
 
 Lemma dcbin_op_eval_correct E op dv1 dv2 w :
   dcbin_op_eval E op dv1 dv2 = Some w →
@@ -163,8 +230,8 @@ Definition dun_op_eval
   | dLitV dl =>
     match op, dl with
     | NegOp, dLitBool b => Some $ dLitV $ dLitBool (negb b)
-    | NegOp, dLitInt n => Some $ dLitV $ dLitInt (Z.lnot n)
-    | MinusUnOp, dLitInt n => Some $ dLitV $ dLitInt (- n)
+    | NegOp, dLitInt (dIntUnknown n) => Some $ dLitV $ dLitInt $ dIntUnknown (Z.lnot n)
+    | MinusUnOp, dLitInt (dIntUnknown n) => Some $ dLitV $ dLitInt $ dIntUnknown (- n)
     | _,_ => None
     end
   | _ => None
@@ -175,7 +242,7 @@ Lemma dun_op_eval_correct E op dv w :
   un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
 Proof.
   destruct dv as [dl | |v|]=> //=.
-  destruct op, dl; intros; simplify_eq/=; auto.
+  destruct op, dl as [[?| ]| | |]; intros; simplify_eq/=; auto.
 Qed.
 
 (** Dexpr *)
@@ -391,13 +458,35 @@ Global Instance into_cloc_plus_plus l l' i j :
   IntoCLocPlus (cloc_plus l j) l' (i + j).
 Proof. rewrite /IntoCLocPlus=> ->. by rewrite cloc_plus_plus. Qed.
 
+(** ** IntoDInt *)
+Class IntoDInt (i : Z) (l : dint) :=
+  into_dint : i = dint_interp l.
+
+Global Instance intodint_zero : IntoDInt 0 (dNat 0).
+Proof. done. Qed.
+
+Global Instance intodint_pos (o : positive) :
+  IntoDInt (Z.pos o) (dNat (Pos.to_nat o)).
+Proof. rewrite /IntoDInt. by rewrite -positive_nat_Z. Qed.
+
+(* DF: This is here to reify unknown naturals, ie meta-variables which
+   value is unknown, but we do know that they are natural numbers *)
+Global Instance intodint_of_nat (n : nat) :
+  IntoDInt (Z.of_nat n) (dNat n).
+Proof. done. Qed.
+
+Global Instance intodint_unknown (i : Z) :
+  IntoDInt i (dIntUnknown i) | 100.
+Proof. done. Qed.
+
 (** ** IntoDBaseLit *)
 Class IntoDBaseLit (l : base_lit) (dl : dbase_lit) :=
   into_dbase_lit : l = dbase_lit_interp dl.
 
-Global Instance into_dbase_lit_int i :
-  IntoDBaseLit (LitInt i) (dLitInt i).
-Proof. split; eauto. Qed.
+Global Instance into_dbase_lit_dint i l :
+  IntoDInt i l →
+  IntoDBaseLit (LitInt i) (dLitInt l).
+Proof. intros ->. split; eauto. Qed.
 
 Global Instance into_dbase_lit_default l :
   IntoDBaseLit l (dLitUnknown l) | 1000.

theories/vcgen/tests/basics.v

@@ -97,7 +97,7 @@ Section test.
     rewrite Qp_half_half. eauto 42 with iFrame.
   Qed.
 
-   Lemma test6 (l : cloc) (z0 : Z) R:
+  Lemma test6 (l : cloc) (z0 : Z) R:
     l ↦C #z0 -∗
     AWP ♯ₗl +=ᶜ ♯1 @ R {{ v, ⌜v = #z0⌝ ∧ l ↦C[LLvl] #(z0+1) }}.
   Proof.

theories/vcgen/tests/memcpy.v

@@ -93,9 +93,9 @@ Section memcpy.
     AWP a_invoke memcpy (♯ₗp |||ᶜ (♯ₗq |||ᶜ ♯n)) @ R {{ _, p ↦C∗ ls2 ∗ q ↦C∗ ls2 }}.
   Proof.
     iIntros (? ?) "Hp Hq". vcg_solver. awp_lam.
-    iApply awp_bind. vcg_solver. iExists 1%nat; iSplit; first done.
+    iApply awp_bind. vcg_solver.
     iIntros (pp) "[Hpp _]". vcg_continue. iIntros "Hpp". awp_let.
-    iApply awp_bind. vcg_solver. iIntros "Hpp". iExists 1%nat; iSplit; first done.
+    iApply awp_bind. vcg_solver. iIntros "Hpp".
     iIntros (qq) "[Hqq _]". vcg_continue. iIntros "Hpp Hqq". awp_let.
     repeat awp_proj. awp_let. (* iApply awp_bind hangs without the set *)
     set (e :=( whileᶜ (_) { _ })%E).

theories/vcgen/tests/unknowns.v

@@ -29,11 +29,36 @@ Section tests_vcg.
     k ↦C #10 -∗ AWP allocᶜ (♯2,♯11) =ᶜ ∗ᶜ♯ₗk +ᶜ ♯2 {{ v, ⌜v = #12⌝ }}.
   Proof.
     iIntros "Hk". vcg_solver. iIntros "Hk".
-    iExists 2%nat. iSplit; first done.
     iIntros (l) "[Hl1 [Hl2 _]]".
     vcg_continue. eauto 42 with iFrame.
   Qed.
 
+  (* TODO: should we even allow to alloc arrays of size zero?
+     According to the standrad, malloc'ing zero bytes is
+     implementation-defined behaviour *)
+  Lemma test3 (n : nat) (m : Z) :
+    n ≥ 1 →
+    (AWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }})%I.
+  Proof.
+    intros ?. iStartProof.
+    vcg_solver.
+    iIntros (l) "Hl". assert (∃ m, n = S m) as [k ->]. exists (pred n). omega.
+    iDestruct "Hl" as "[Hl Hls]". (* TODO: this looks ridiculous *)
+    vcg_continue. eauto 42 with iFrame.
+  Qed.
+
+  Lemma test3_NOMATCH (n : Z) (m : Z) :
+    1 ≤ n →
+    (AWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }})%I.
+  Proof.
+    intros ?. iStartProof.
+    vcg_solver.
+    match goal with
+    | [ |- environments.envs_entails _
+      (∃ n0 : nat, _)%I] => idtac
+    end.
+  Abort.
+
   Lemma test6 (l k : cloc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
     (∀ Φ, Φ #11 -∗ awp e1 True Φ) -∗
     (∀ Φ, Φ #12 -∗ awp e2 True Φ) -∗

theories/vcgen/vcgen.v

@@ -123,9 +123,15 @@ Section vcg.
 
   Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
       (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ :=
-    mapsto_wand_list E m (∃ n : nat,
-      ⌜ dval_interp E dv1 = #n ⌝ ∧
-      ∀ l, l ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val l))%I.
+    match dval_to_nat dv1 with
+    | Some n =>
+      mapsto_wand_list E m (
+        ∀ l, l ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val l))%I
+    | None =>
+      mapsto_wand_list E m (∃ n : nat,
+        ⌜ dval_interp E dv1 = #n ⌝ ∧
+        ∀ l, l ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val l))%I
+    end.
 
   Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
       (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ :=
@@ -798,6 +804,23 @@ Section vcg_spec.
       iExists (dloc_interp E (dLoc i 0)), (dval_interp E dw), w'. iFrame; eauto.
    Qed.
 
+  Lemma vcg_wp_alloc_correct E m dv1 dv2 Φ :
+    denv_interp E m -∗
+    vcg_wp_alloc E dv1 dv2 m Φ -∗
+    ∃ n : nat, ⌜dval_interp E dv1 = #n⌝
+         ∧ (∀ l : cloc, l ↦C∗ replicate n (dval_interp E dv2)
+            -∗ vcg_wp_continuation E Φ (cloc_to_val l)).
+  Proof.
+    iIntros "Hm Hwp".
+    rewrite /vcg_wp_alloc.
+    destruct (dval_to_nat dv1) as [n|] eqn:Hdv1.
+    - iExists n. iSplit. iPureIntro; by apply dval_to_nat_correct.
+      rewrite mapsto_wand_list_spec.
+      iApply ("Hwp" with "Hm").
+    - rewrite mapsto_wand_list_spec.
+      iApply ("Hwp" with "Hm").
+  Qed.
+
   Lemma vcg_wp_store_correct E m dv1 dv2 Φ :
     denv_wf E m →
     dval_wf E dv2 →
@@ -863,21 +886,25 @@ Section vcg_spec.
         iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
         iDestruct 1 as (E' dw m'' -> Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]".
         rewrite (dval_interp_mono E E') //.
-        rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'".
+        iCombine "HmNew Hm'" as "Hm'".
         rewrite (denv_interp_mono E E') // denv_merge_interp.
-        iDestruct ("H" with "Hm'") as (n ->) "HΦ". iExists n; iSplit; first done.
-        iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ".
+        iDestruct (vcg_wp_alloc_correct with "Hm' H") as (n ?) "Hcont"; eauto.
+        iExists n; iSplit; eauto.
+        iIntros (l) "Hl". iSpecialize ("Hcont" with "Hl").
+        by iApply (vcg_wp_continuation_mono with "Hcont").
       + specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
         iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]";
         first done. clear Heqsp.
         iDestruct (IHde2 with "Hm' Hwp") as "Hde2"; try done.
         iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
         iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 -> ???) "[Hm' H]".
-        rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'".
+        rewrite (dval_interp_mono E E') //.
+        iCombine "HmNew Hm'" as "Hm'".
         rewrite (denv_interp_mono E E') // denv_merge_interp.
-        rewrite !(dval_interp_mono E E') // .
-        iDestruct ("H" with "Hm'") as (n ->) "HΦ". iExists n; iSplit; first done.
-        iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ".
+        iDestruct (vcg_wp_alloc_correct with "Hm' H") as (n ?) "Hcont"; eauto.
+        iExists n; iSplit; eauto.
+        iIntros (l) "Hl". iSpecialize ("Hcont" with "Hl").
+        by iApply (vcg_wp_continuation_mono with "Hcont").
     - rewrite IHde //. iRename "Hm" into "Hawp".
       iSpecialize ("Hawp" with "Hwp"); simpl.
       iApply (a_load_spec_exists_frac with "[Hawp]").