I have 2 functions, all is for checking how many values that are the same values and same index in 2 sequences, example:

• requires there's no duplicates in the sequence s:= [1,3,2,5,6] u:= [2,3,4,5,1]

==> bullspec(s,u) = 2

So both my 2 functions return the right value but the assertion of one is true, other is false Here are my 2 functions:

function bullspec(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if |s| == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[|s|-1] in u && s[|s|-1]==u[|s|-1] 
    then (1   bullspec(s[..|s|-1], u))
    else bullspec(s[..|s|-1],u)
  )
}

and

function bullspec2(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if |s| == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[0] in u && s[0] == u[0]
    then (1   bullspec2(s[1..], u))
    else bullspec2(s[1..], u)
  )
}

I have a method Main below:

method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec(sys, usr) == 1; //Assertion might not hold
  assert bullspec2(sys, usr) == 1; //This is good
}

The difference between 2 functions is the loop recusive, one start from the beginning, other start from the end, and somehow the backward make assertion works well

I try to write some ensures statements but there's no working.

CodePudding user response：

First, please be aware that you are using a static analyzer, not a run-time tester. So the assertion might hold at run-time, but the static analyzer can't prove it. The fact that the static analyzer can prove the second one is pretty astounding already. But I would always advise you switch the order of assertions, because an assertion after a first unproven one is always proved with the condition that the unproven one is true. In your case, it's still bullspec that can't be resolved, no matter what.

The reason why it currently fail to verify is that the axiom that indirectly serves at evaluating a sequence's length in the presence of a sequence literal without consuming fuel is not implemented yet. See this similar issue. That means that, for your second example, "evaluating" the function using axioms does not consume "fuel" (I'll go back to that later), but for the first failing example, it cannot unroll the function enough to do the computation.

What you can do for now is:

Create a lemma and prove it (hard)

lemma bullspec2equalsBullspec(s:seq<nat>, u:seq<nat>): nat
  ensures  bullspec2(sys, usr) == bullspec(sys, usr)
{
  // TODO
}

and then write:

assert bullspec2(sys, usr) == 1;
assert bullspec(sys, usr) == 1 by {
  bullspec2equalsBullspec(sys, usr);
}

Pass the sequence's length as a ghost parameter in bullspec

function bullspec(s:seq<nat>, u:seq<nat>, length: nat): nat
  requires |s| == length
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if length == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[length-1] in u && s[length-1]==u[length-1] 
    then (1   bullspec(s[..length-1], u,length-1))
    else bullspec(s[..length-1],u,length-1)
  )
}
/// ...
method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec2(sys, usr) == 1; //This is good
  assert bullspec(sys, usr, 5) == 1; //This is good
}

verifies because now it can unroll the function applied to literals without fuel.

Unroll bullspec by verification debugging to see where it blocks.

If this assertion should hold, what should hold before? You can unroll the function's definition and assert intermediate results. If you assert something non-trivial that Dafny can finally prove, all the rest will be proven. I unrolled the function for 3 steps only.

method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec2(sys, usr) == 1; //This is good

  var sys1 := sys[..|sys|-1];
  var sys2 := sys1[..|sys1|-1];
  var sys3 := sys2[..|sys2|-1];
  var sys4 := sys3[..|sys3|-1];
  var sys5 := sys4[..|sys4|-1];

  assert bullspec(sys3, usr) == 1; 
  assert bullspec(sys2, usr) == 1; 
  assert bullspec(sys1, usr) == 1; 
  assert bullspec(sys, usr) == 1; //Assertion might not hold
}

Give more fuel to your function (best in your case)

By just changing the definition of your function, you can give it more fuel for the verifier to instantiate it. For your case, a fuel of 3 is sufficient.

function {:fuel 10} bullspec(s:seq<nat>, u:seq<nat>): nat