Some clarify regardig binop evaluation

_CoqProject

@@ -23,4 +23,5 @@ theories/tests/swap.v
 theories/tests/fact.v
 theories/tests/memcpy.v
 theories/tests/gcd.v
+theories/tests/binop.v
 # theories/tests/lists.v

theories/tests/memcpy.v

@@ -98,9 +98,12 @@ Section memcpy.
     vcg_continue. iIntros "Hpp Hqq".
     repeat awp_proj. awp_let. set (e :=( whileᶜ (_) { _ })%E).
     unfold e. vcg_solver. iIntros "Hpp Hqq".
-    (* Ouch, this goal is ugly. We either need to embed naturals into the
+    (* RK: Ouch, this goal is ugly. We either need to embed naturals into the
     reified syntax, or let the binop evaluator be total and generate
     side-conditions (here 0 ≤ n) for the result to be well-formed. *)
+    (* The issue here actually is that dereferecing of pp returns a pointer to p -- which is _not_ a reified location in our setting!
+       So the vcgen cannot symbolically perform pointer arithmetic.
+       See the binop tests for details *)
     rewrite cloc_of_to_val /=. case_option_guard; last first.
     { exfalso. omega. } simpl.
     iExists (cloc_to_val (cloc_plus p n)). rewrite Nat2Z.id.

theories/vcgen/dcexpr.v

@@ -165,12 +165,7 @@ 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 (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)
-    end
+    Some $ dLocV $ dLoc i (j + o)
   | _,_ => None
   end.
 
@@ -182,16 +177,16 @@ Proof.
   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 //.
+  - rewrite cloc_of_to_val /=. do 2 f_equal.
+    rewrite cloc_plus_plus // Nat2Z.id //.
+  - simplify_eq/=. omega.
 Qed.
 
 Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : option dval :=
   match op with
   | CBinOp op' => dbin_op_eval E op' dv1 dv2
   | PtrPlusOp => dptr_plus_eval E dv1 dv2
-  | PtrLtOp => None
+  | PtrLtOp => None (* TODO! *)
   end.
 
 Lemma dbin_op_eval_correct E op dv1 dv2 w :