Question about .strategies in QCP

[fanweneddie]

Hi authors,

I am interested in understanding the .strategies files in QCP, and I have 2 questions:

1. My current understanding is that, to prove that a program satisfies its pre&postcondition, QCP may rely on several kinds of user-provided proof information: reasoning rules defined in .strategies files, assertions and loop invariants in the source program, and, when automatic proof is insufficient, manually completed proofs in *_manual.v. Is this understanding correct?

2. I am not sure if the rules defined in .strategies files are verified. If not, then I guess .strategies should better be used as a library file, instead of having users define their (probably unsound) rules. For example, in array_shape.strategies in Malice project, I can define a rule that derives ceil_shape(p, x, y) trivially

id : 29
priority : core(1)
right : IntArray::ceil_shape(?p, ?x, ?y) at 0
action : right_erase(0);

It would make this incorrect program pass the verification.

#include "verification_stdlib.h"
#include "verification_list.h"
#include "int_array_def.h"
#include "sll_shape_def.h"

int array_max(int *a, int n)
/*@ Require 0 <= n && n < INT_MAX
    Ensure IntArray::ceil_shape(a, 0, n)
*/
{
return 0;
}

Thanks in advance!
Wen