如何在 VST 中处理 "Forall (closed_wrt_vars (eq _z')) P " 个目标？

Question

这次我要证明调用其他函数。 vars.c:

int pure0 ()
{
    return 0;
}

int get0(int* arr)
{
    int z = pure0();
    return 0;
}

我的证明开始 - verif_vars.v:

Require Import floyd.proofauto.
Require Import vars.

Local Open Scope logic.
Local Open Scope Z.

Definition get0_spec :=
  DECLARE _get0
    WITH sh : share, arr : Z->val, varr : val
    PRE [_arr OF (tptr tint)]
        PROP ()
        LOCAL (`(eq varr) (eval_id _arr);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr 0 100) (eval_id _arr))
    POST [tint] `(array_at tint sh arr 0 100 varr).

Definition pure0_spec :=
  DECLARE _pure0
    WITH sh : share
    PRE []
        PROP ()
        LOCAL ()
        SEP ()
    POST [tint] local(`(eq (Vint (Int.repr 0))) retval).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get0_spec :: pure0_spec ::nil.

Lemma body_pure0: semax_body Vprog Gprog f_pure0 pure0_spec.
Proof.
  start_function.
  forward.
Qed.


Lemma body_get0: semax_body Vprog Gprog f_get0 get0_spec.
Proof.
  start_function.
  name arrarg _arr.
  forward_call (sh).
  entailer!.

导致目标：

2 subgoals, subgoal 1 (ID 566)

  Espec : OracleKind
  sh : share
  arr : Z -> val
  varr : val
  Delta := abbreviate : tycontext
  POSTCONDITION := abbreviate : ret_assert
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  arrarg : name _arr
  ============================
   Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

subgoal 2 (ID 567) is:
 DO_THE_after_call_TACTIC_NOW

我想它声明，函数调用不会改变 arr 内容，这对我来说很明显。

我可以用这个目标做什么？此处适用哪种策略，该语句的确切含义是什么？我是否应该丰富 pure0 规范以某种方式指出它不会修改任何内容？

Answer 1

解决方案，在vst/progs/verif_reverse.v中使用：

auto with closed.

遗憾的是，它只回答了一半的问题。

Answer 2

第一：写VST/Verifiable-C题时，请注明您使用的是哪个版本的VST。看来您使用的是 1.4.

第二：我不确定这是否回答了您所有的问题，但是，

"closed_wrt_vars S P" 表示提升的断言 P 对于集合 S 中的所有变量都是封闭的。也就是说，S 是一组 C 语言标识符，可以代表不可寻址的局部变量（"temps"，而不是 "vars")。 P 是 "environ->mpred" 形式的断言，而 "closed" 意味着如果您将 "environ" 更改为集合 S 中的任何变量具有不同的值，则 P 的真实性将不会改变。

"Forall" 是 Coq 的标准库谓词，用于将谓词应用于列表。所以，

 Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

意味着，让集合 S 成为仅包含变量 _z' 的单例集合。我们在这里断言列表中的所有谓词都是封闭的w.r.t。 S. 列表中只有一个谓词，它是 "trivially lifted"，也就是说，对于任何谓词 (P: mpred)，提升的谓词

`(P)

等价于 (fun rho:environ => P)。简单地说，`P 不关心您对 rho 所做的操作，包括更改 _z' 的值。

"auto with closed"（或者只是为了确定，"auto 50 with closed"）应该处理这个，并且你表明它确实处理了它。所以我假设你剩下的问题是，"what's going on here?"，我希望我回答了。

Answer 3

顺便说一句（与你的问题无关），前提条件 `isptr (eval_id _arr) 对于 get0 可能是不必要的。 `(array_at tint sh arr 0 100) (eval_id _arr)).

已经暗示了它

此外，假设您确实想要 `isptr (eval_id _arr) 作为前提条件；你可以考虑把它写成，

   PROP (isptr varr)
   LOCAL (`(eq varr) (eval_id _arr))
   SEP (`(array_at tint sh arr 0 100 varr))

（在某些方面）更简单也更 "canonical"。

如何在 VST 中处理 "Forall (closed_wrt_vars (eq _z')) P " 个目标？

How to handle "Forall (closed_wrt_vars (eq _z')) P " goals in VST?

verifiable-c