nunchaku fails to find a counterexample for a simple list-based map implementation

[samuelgruetter]

trafficstars

Versions:

• nunchaku 0.5.1 70e510138ab0efd037b3351750b2b428a97c890c
• CVC4 version 1.5 (shipped with Isabelle 2017)

The following example

val K : type.
val V : type.

data tuple := pair K V.

data list :=
  nil
| cons tuple list.

data option :=
  None
| Some V.

rec get : list -> K -> option :=
  forall k. get nil k = None;
  forall ki vi k rest. get (cons (pair ki vi) rest) k =
    (if (ki = k) then Some vi else get rest k).

rec filter : (tuple -> prop) -> list -> list :=
  forall f. filter f nil = nil;
  forall f h t. filter f (cons h t) =
    (if (f h) then (cons h (filter f t)) else (filter f t)).

rec remove : list -> K -> list :=
  forall l k. remove l k = filter (fun t.
     match t with
     | pair ki vi -> ki != k
     end)
     l.

rec put : list -> K -> V -> list :=
  put = (fun l k v. cons (pair k v) (remove l k)).

val l: list.
val k1: K.
val k2: K.
val v: V.

# Missing hypothesis:
# axiom k1 != k2.

goal ~ (get (put l k1 v) k2 = get l k2).

returns UNKNOWN, even though a simple counterexample exists, as shown by nitpick in Isabelle2017:

theory ListMapTests
  imports Main
begin

typedecl K
typedecl V

datatype tuple = pair K V

datatype list = nil | cons tuple list

datatype option = None | Some V

fun get :: "list ⇒ K ⇒ option" where
  "get nil k = None" |
  "get (cons (pair ki vi) rest) k = 
    (if (ki = k) then Some vi else get rest k)"

fun filter :: "(tuple ⇒ bool) ⇒ list ⇒ list" where
  "filter f nil = nil" |
  "filter f (cons h t) =
     (if (f h) then (cons h (filter f t)) else (filter f t))"

fun remove :: "list ⇒ K ⇒ list" where
  "remove l k = filter (λ t. case t of pair ki vi ⇒ ki ≠ k) l"

fun put :: "list ⇒ K ⇒ V ⇒ list" where
  "put l k v = cons (pair k v) (remove l k)"

lemma "get (put l k1 v) k2 = get l k2"
  nitpick

which returns

Nitpick found a counterexample for card K = 2 and card V = 2:

  Free variables:
    k1 = K⇩1
    k2 = K⇩1
    l = nil
    v = V⇩1

I understand that nunchaku has not yet received as much development time as nitpick and the tools powering it, but do you have an estimate of how far nunchaku is away from being able to solve examples like this one? Or is there a simple change I can make to the input file so that it works?

[c-cube]

It might be a difference between cvc4 and kodkod. I suppose you only have cvc4, right?

You may try opam install smbc, it works well on such examples.

$ ./nunchaku -t 30 foo.nun -s smbc  
SAT: {
  type V := {}.
  type K := {$K_0}.
  val v := v.
  val k1 := $K_0.
  val k2 := $K_0.
  val l := nil.
}
{backend:smbc, time:0.0s}

You can also install kodkod(i), but the kodkod backend is not very good at the moment (it must lack some optimizations nitpick does, cc @blanchette). If you happen to be on archlinux I wrote a user packge, otherwise you can look on the website.

[samuelgruetter]

Sorry for not bothering to install smbc in the first place :wink: Now I installed smbc and indeed it works! I'm just a bit surprised by the output line

  type V := {}.

It seems to contradict the assumption val v: V., so strictly speaking, this is not a model?

[c-cube]

Ah good catch, could you report that on smbc's repo? In this case it's because v is never used, but still.