viperproject/silicon

Domain axioms not instantiated for all relevant cases

marcoeilers opened this issue · 3 comments

marcoeilers commented

The following example does not verify in Silicon even though it should:

domain Val  {}

domain WellFoundedOrder[T]  {

  function decreasing(arg1: T, arg2: T): Bool

  function bounded(arg1: T): Bool
}

domain List[V]  {

  function Nil(): List[V]

  function Cons(value: V, tail: List[V]): List[V]

  function get_List_value(t: List[V]): V

  function get_List_tail(t: List[V]): List[V]

  function List_tag(t: List[V]): Int

  axiom {
    (forall value: V, tail: List[V] ::
      { (Cons(value, tail): List[V]) }
      value == (get_List_value((Cons(value, tail): List[V])): V))
  }

  axiom {
    (forall value: V, tail: List[V] ::
      { (Cons(value, tail): List[V]) }
      tail == (get_List_tail((Cons(value, tail): List[V])): List[V]))
  }

  axiom {
    (List_tag((Nil(): List[V])): Int) == 1
  }

  axiom {
    (forall value: V, tail: List[V] ::
      { (Cons(value, tail): List[V]) }
      (List_tag((Cons(value, tail): List[V])): Int) == 0)
  }

  axiom {
    (forall t: List[V] ::
      { (List_tag(t): Int) }
      { (get_List_value(t): V) }
      { (get_List_tail(t): List[V]) }
      (List_tag(t) == 1 && t == (Nil(): List[V])) ||
      (List_tag(t) == 0 && exists v: V, l: List[V] :: t == Cons(v, l))
      //(t == (Cons((get_List_value(t): V), (get_List_tail(t): List[V])): List[V]))
      )
  }
}

domain ListWellFoundedOrder[V]  {

  axiom {
    (bounded((Nil(): List[V])): Bool)
  }

  axiom {
    (forall value: V, tail: List[V] ::
      { (Cons(value, tail): List[V]) }
      (bounded((Cons(value, tail): List[V])): Bool) &&
      (decreasing(tail, (Cons(value, tail): List[V])): Bool))
  }
}

// decreases l
function len(l: List[Val]): Int
  ensures result >= 0
{
  ((List_tag(l): Int) == 1 ? 0 : 1 + len((get_List_tail(l): List[Val])))
}

// decreases l
method len_termination_proof(l: List[Val])
{
  if ((List_tag(l): Int) == 1) {
  } else {
    assert (decreasing((get_List_tail(l): List[Val]), old(l)): Bool) &&
      (bounded(old(l)): Bool)}
}

The issue seems to be that the axioms in ListWellFoundedOrder are not instantiated for type argument Val, even though they obviously need to be.

mschwerhoff commented

Potentially related: #526, #300

marcoeilers commented

Ha, funny, I just ran the tests with my fix and saw that this fixes the unexpected output for issue #300. And I tried #526 manually and that fixes it, too. Nice! Thanks for pointing those out!