在验证数组存储时的奇怪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)。这与代码或后置条件无关，当然也是不可证明的。这里出了什么问题？

我用：

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!.策略是不安全的，可以从合格的目标中产生无法证明的目标。在这种情况下，

- first I need to supply additional condition `is_int v` to be able to assign it to a cell of an "all ints" array. Seemingly VST can't deduce the type from CompCert annotations.
- then instead of `entailer!.` I need to prove first all propositions on the right hand side separately, and then I can apply `entailer` to combine hypotheses.

​

以下是正确的规范和证明：

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.