Integer and Z types support

[weaversa]

Is it the case that saw just doesn't support these types yet?

$ cat bug.saw
prove_print z3 {{\(x:(Z 17)) -> \y -> x ^^ y == x ^^ y}};
$ saw bug.saw
[01:31:57.920] Loading file "bug.saw"
[01:31:57.945] You have encountered a bug in SawCore's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< --------------------------------------------------- 
  Revision:  f6ed78a6ddafc64d0e2ce255d1e2c320f44dc7a9
  Branch:    HEAD
  Location:  Verifier.SAW.Simulator.Prims
  Message:   no implementation for exp on IntMod
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-KY4ti7hLSPq8fvt7lFZgTk:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:255:13 in saw-core-0.1-KY4ti7hLSPq8fvt7lFZgTk:Verifier.SAW.Simulator.Prims
%< --------------------------------------------------- 

And another:

$ cat bug1.saw
let {{
  func: (Z 17) -> (Z 17) -> (Z 17)
  func x y = x + y
}};

prove_print (unint_z3 ["func"])  {{\(x:(Z 17)) -> \y -> func x y == func y x}};

$ saw bug1.saw
[01:32:41.536] Loading file "bug1.saw"
[01:32:41.581] Stack trace:
"prove_print" (bug1.saw:6:1-6:12):
"unint_z3" (bug1.saw:6:14-6:22):
Could not create sbv argument for <<integer>>

[atomb]

The translation for Integer and Z n into SAWCore isn't entirely complete. It partly exists, but needs to be fleshed out. We expect to have that done in time for the August 0.6 release.

[atomb]

With the latest version of SAW, we instead get saw: asPredType: unsupported dependent SAW-Core type because the type of ^^ makes the type of y no longer determined. With a type annotating setting y to be an Integer, we get a panic including Message: Verifier.SAW.Simulator.toBits <<integer>>. Going past that, setting the type of y to [8], it succeeds. The bottom line seems to be that we don't support non-bitvector exponents and have a bunch of very hard-to-decipher error messages.

[msaaltink]

Support has improved but is still incomplete. For example, some Integer examples work:

let {{
  type T' = Integer
  f': T' -> T'
  f' x = h' (h' x)
  h': T' -> T'
  h' x = undefined
  }};

prove_print (w4_unint_z3 ["h'"]) {{ \x y -> y == h' x ==> h' y == f' x }};

but the equivalent in a Z type fails strangely:

let {{
  type T = Z 7
  f: T -> T
  f x = h (h x)
  h: T -> T
  h x = undefined
  }};

prove_print (w4_unint_z3 ["h"]) {{ \x y -> y == h x ==> h y == f x }};

Here, a recent SAW fails with

prove: 1 unsolved subgoal(s)
Invalid: [x = 2, y = 148666]

[msaaltink]

Here's a simpler example showing that SAW does not do equality reasoning for Z types. Consider first a successful case, in Integer:

let {{ g: Integer -> Integer; g x = x }};

prove (w4_unint_z3 ["g"]) {{\x y -> x == y ==> g x == g y }};

We do not need to know anything about g for this reasoning to work.

The similar goal in a Z type

let {{ f: Z 7 -> Z 7; f x = x }};

prove (w4_unint_z3 ["f"]) {{\x y -> x == y ==> f x == f y }};

fails.

[brianhuffman]

This last example is an interesting case, and it reveals a limitation of how we currently encode goals involving Z types in the proof backends. Variables of type Z n are encoded in SMT-lib as integer variables, and then the equality relation is encoded as equivalence mod n. Furthermore, an uninterpreted function of type Z n -> Z n is encoded in SMT-lib as an uninterpreted function from integers to integers. This means that the solver is free to find counterexamples where the uninterpreted function does not respect equivalence mod n.

To fix this, it seems like we would need to send extra lemmas to the solver stating that uninterpreted functions respect the appropriate equivalence relations for their input and output types. For example, for f : Z 7 -> Z 7, the SMT-lib query would declare f : Int -> Int and an assumption forall x y, (x%7 == y%7) ==> f(x)%7 == f(y)%7. The problem with this is that assumptions like this contain quantifiers.

Another approach that would let us avoid universally-quantified lemmas would be to encode an uninterpreted function f : Z 7 -> Z 7 in SMT-lib by declaring an uninterpreted g : Int -> Int and then defining f x = g (x % 7) % 7, to ensure that defined f must respect the equivalence relation. This is probably the approach I would take.

[robdockins]

Most of the issues in this thread have now been resolved. However, there are still some issues with exponentiation that I've moved into a new, more focused, ticket: #923