Во-первых, имейте в виду, что вы используете статический анализатор, а не тестер во время выполнения. Таким образом, утверждение может быть верным во время выполнения, но статический анализатор не может это доказать. Тот факт, что статический анализатор может доказать второе, уже довольно поразителен. Но я бы всегда советовал менять порядок утверждений, потому что утверждение после первого недоказанного всегда доказывается при условии, что недоказанное утверждение истинно. В вашем случае это все еще bullspec не может быть решено, несмотря ни на что.

Причина, по которой это в настоящее время не может быть проверено, заключается в том, что аксиома, которая косвенно служит для оценки длины последовательности в присутствии литерала последовательности без потребления топлива, еще не реализована. Смотрите этот похожий выпуск. Это означает, что для вашего второго примера «оценка» функции с использованием аксиом не потребляет «топливо» (я вернусь к этому позже), но для первого неудачного примера она не может развернуть функцию достаточно для выполнения вычислений. .

Что вы можете сделать на данный момент:

Придумайте лемму и докажите ее (сложно)

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

а затем напишите:

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

Передайте длину последовательности в качестве параметра-призрака в 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
}

проверяет, потому что теперь он может развернуть функцию, применяемую к литералам, без топлива.

Разверните bullspec с помощью проверочной отладки, чтобы увидеть, где он блокируется.

Если это утверждение должно быть верным, то что должно быть верным раньше? Вы можете развернуть определение функции и утвердить промежуточные результаты. Если вы утверждаете что-то нетривиальное, что Дафни сможет наконец доказать, все остальное будет доказано. Я развернул функцию всего за 3 шага.

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
}

Дайте больше топлива вашей функции (лучше всего в вашем случае)

Просто изменив определение вашей функции, вы можете дать верификатору больше топлива для ее создания. Для вашего случая топлива 3 достаточно.

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