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

This time I'm proving function calling other. vars.c:

int pure0 ()
{
    return 0;
}

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

My proof start - 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!.

Which induces the goal:

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

I suppose it states, that the function call does not alter arr contents, which is quite obvious for me.

What can I do with this goal? Which tactic applies here, and what exactly means the statement? Should I enrich the pure0 spec to somehow point out, that it does not modify anything?

Solution

FIRST: When writing VST/Verifiable-C questions, please indicate which version of VST you are using. It appears you are using 1.4.

SECOND: I am not sure this answers all your questions, but,

"closed_wrt_vars S P" says that the lifted assertion P is closed with respect to all the variables in the set S. That is, S is a set of C-language identifiers that may stand for nonaddressable local variables ("temps", not "vars"). P is an assertion of the form "environ->mpred", and "closed" means that if you change the "environ" to have different values for any of the variables in set S, then the truth of P will not change.

"Forall" is Coq's standard library predicate to apply a predicate to a list. So,

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

means, let the set S be the singleton set containing just the variable _z'. We assert here that all the predicates in the list are closed w.r.t. S. There's exactly one predicate in the list, and it's "trivially lifted", that is, for any predicate (P: mpred), the lifted predicate

`(P)

is equivalent to (fun rho:environ => P). Trivially, then, `P doesn't care what you do to rho, including changing the value of _z'.

The "auto with closed" (or just to be sure, "auto 50 with closed") should take care of this, and you indicate that it does take care of it. So I assume that the rest of your question was, "what's going on here?", and I hope I answered it.