证明数组存储时的奇怪 VST 目标

Question

现在我要证明一个简单的数组访问过程（文件arr.c）：

void set(int* arr, int key, int val)
{
    arr[key] = val;
}

文件 arr.c 被翻译成 arr.v:

...
Definition f_set := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_arr, (tptr tint)) :: (_key, tint) :: (_val, tint) :: nil);
  fn_vars := nil;
  fn_temps := nil;
  fn_body :=
(Sassign
  (Ederef
    (Ebinop Oadd (Etempvar _arr (tptr tint)) (Etempvar _key tint)
      (tptr tint)) tint) (Etempvar _val tint))
|}.
...

这是我证明的开头（文件verif_arr.v）：

Require Import floyd.proofauto.
Require Import arr.

Local Open Scope logic.
Local Open Scope Z.

Inductive repr : Z -> val -> Prop :=
| mk_repr : forall z, z >= 0 -> z < Int.modulus -> repr z (Vint (Int.repr z)).

Function aPut (arr:Z -> val) (k:Z) (v:val) : Z -> val :=
  fun (kk:Z) => if (Z.eq_dec k kk) then v else arr kk.

Definition set_spec :=
  DECLARE _set
    WITH sh : share, k : Z, arr : Z->val, vk : val, v : val, varr : val
    PRE [_key OF tint, _val OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i);
              writable_share sh; repr k vk)
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `(eq v) (eval_id _val);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tvoid] `(array_at tint sh (aPut arr k v)
                            0 100 varr).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := set_spec :: nil.

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  name valarg _val.
  forward.
  entailer!.

在 entailer!. 策略之后，我得到了：

3 subgoals, subgoal 1 (ID 1261)

  Espec : OracleKind
  sh : share
  k : Z
  arr : Z -> val
  H : 0 <= k < 100
  H0 : forall i : Z, 0 <= i < 100 -> is_int (arr i)
  H1 : writable_share sh
  Delta := abbreviate : tycontext
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  karg : name _key
  arrarg : name _arr
  valarg : name _val
  rho : environ
  H2 : repr k (eval_id _key rho)
  POSTCONDITION := abbreviate : ret_assert
  H3 : isptr (eval_id _arr rho)
  ============================
   offset_val (Int.repr (sizeof tint * 0)) (eval_id _arr rho) =
   force_val (sem_add_pi tint (eval_id _arr rho) (eval_id _key rho))

subgoal 2 (ID 1266) is:
 ?890 = force_val (sem_cast_neutral (eval_id _val rho))
subgoal 3 (ID 1235) is:
 semax Delta
   (PROP  ()
    LOCAL  (`(eq vk) (eval_id _key); `(eq varr) (eval_id _arr);
    `(eq v) (eval_id _val); `isptr (eval_id _arr))
    SEP  (`(array_at tint sh (upd arr 0 ?890) 0 100) (eval_id _arr)))
   (Sreturn None) POSTCONDITION

现在问题：

在规范set_spec中有一个先决条件'(array_at tint sh arr 0 100) (eval_id _arr)（这里代替'应该是反引号，这会破坏格式）。为什么假设列表中没有这个陈述？
在我看来，第一个子目标试图取消引用数组的第 0 个单元格 (arr + 0)，它应该等于第一个键单元格 (arr + key)。这与代码或 post 条件无关，当然无法证明。这里出了什么问题？

我使用：

VST版本:

Definition svn_rev := "6834P".
Definition release := "1.5".
Definition date := "2014-10-02".

CompCert 版本：2.4

Coq 版本:

The Coq Proof Assistant, version 8.4pl3 (January 2014)
compiled on Jan 19 2014 23:14:16 with OCaml 4.01.0

编辑：

post 条件中的最后 local ... 部分原来是多余的。

Answer 1

首先，在Delta假设中，前提条件'(array_at tint sh arr 0 100) (eval_id _arr)实际上存在于abbreviate之后。
其次，事实证明，entailer!. 策略并不安全，并且可以从符合条件的目标中产生无法证明的目标。在这种情况下，
- 首先我需要提供附加条件 is_int v 才能将其分配给 "all ints" 数组的单元格。貌似VST无法从CompCert注解中推导出类型
- 然后 entailer!. 我需要首先分别证明右边的所有命题，然后我可以应用 entailer 来组合假设。

这是正确的规范和证明：

Inductive repr : Z -> val -> Prop :=
| mk_repr : forall z, z >= 0 -> z < Int.modulus -> repr z (Vint (Int.repr z)).

Function aPut (arr:Z -> val) (k:Z) (v:val) : Z -> val :=
  fun (kk:Z) => if (Z.eq_dec k kk) then v else arr kk.

Definition set_spec :=
  DECLARE _set
    WITH sh : share, k : Z, arr : Z->val, vk : val, v : val, varr : val
    PRE [_key OF tint, _val OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i);
              writable_share sh; repr k vk; is_int v)
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `(eq v) (eval_id _val);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tvoid] `(array_at tint sh (aPut arr k v)
                            0 100 varr).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := set_spec :: nil.

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  name valarg _val.
  forward.
  instantiate (1:=v).
  instantiate (2:=k).
  assert (offset_val (Int.repr (sizeof tint * k)) (eval_id _arr rho) =
          force_val (sem_add_pi tint (eval_id _arr rho) (eval_id _key rho))).
  inversion H2.
  rewrite sem_add_pi_ptr.
  unfold force_val.
  apply f_equal2.
  rewrite mul_repr.
  auto.
  auto.
  assumption.

  assert (eval_id _val rho = force_val (sem_cast_neutral (eval_id _val rho))).
  apply is_int_e in H3.
  destruct H3 as [n VtoN].
  rewrite VtoN.
  auto.
  entailer.
  forward.
Qed.

证明数组存储时的奇怪 VST 目标

Weird VST goal while proving array store

verifiable-c

编辑：