Make goal_eval_unint handle Z n types.

[brianhuffman]

Fixes #1120.

[robdockins]

I think this works OK... but I'm a little concerned that we might not be reflecting the equivalence relation on Z n properly. Given where this occurs, I think it's OK, but haven't completely formed the argument in my head.

[brianhuffman]

You're probably thinking of #745, where we discussed the problem of uninterpreted functions with Z n argument types; this was fixed in GaloisInc/saw-core#93 (commit f01e444 specifically), which added these lines to applyUnintApp to reduce arguments of type Z n modulo n before passing them to an uninterpreted function:

saw-script/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

Lines 844 to 846 in 6d3f39c

	VIntMod n si -> do n' <- W.intLit sym (toInteger n)
	si' <- W.intMod sym si n'
	return (extendUnintApp app0 si' BaseIntegerRepr)

[brianhuffman]

Upon further testing, it appears that there are some other serious problems with round-tripping of terms involving Z n through what4 using goal_eval_unint. While this PR in its current state makes the example from the original post in #1120 work, that is only because what4 was able to simplify the entire expression to True. With something a bit more complicated, what4 will return an expression involving integer arithmetic operators, which are then translated to saw-core expressions having the wrong types. The resulting terms reveal errors with check_goal, and cause panics if passed along to w4.

let {{
  g: Z 7 -> Z 7
  g x = x + 1
 }};
prove do { goal_eval_unint ["g"]; print_goal; check_goal; w4; } {{ \x y -> x == y ==> g x == g y }};

[13:57:06.420] Goal prove (goal number 0):
[13:57:06.420] let { x@1 = Bool
      -> Bool
      x@2 = Integer
      -> Integer
      -> Integer
      x@3 = Integer
      -> Integer
      -> Bool
      x@4 = Prelude.Nat
      -> Integer
      x@5 = natToInt 0
      x@6 = IntModNum (Cryptol.TCNum 7)
      x@7 = natToInt 6
      x@8 = natToInt 7
    }
 in (x : x@6)
-> (y : x@6)
-> EqTrue
     (Prelude.or
        (not (intEq x@5 (intMod (intAdd x (intMul x@7 y)) x@8)))
        (intEq x@5
           (intMod
              (intAdd (g (intMod x x@8)) (intMul x@7 (g (intMod y x@8))))
              x@8)))
[13:57:06.421] Stack trace:
"prove" (/Users/huffman/Documents/saw/issue1120.saw:15:1-15:6):
"check_goal" (/Users/huffman/Documents/saw/issue1120.saw:15:47-15:57):
Inferred type
  Prelude.IntMod 7
Not a subtype of expected type
  Prelude.Integer
For term
  x

[brianhuffman]

I'll revert to draft status until we can figure out how to fix this properly.

[brianhuffman]

I just pushed a revised version of this PR, and I believe that it takes care of all the saw-core type errors that we were seeing before. I had to add a couple of new ArgTerm constructors that insert fromIntMod and toIntMod coercions in the right places.

Here's an example that exercises all the new IntMod features:

sawscript> let {{ g (x:Z 7) = x + 1 }}
sawscript> prove do {goal_eval_unint ["g"]; print_goal; check_goal;} {{ \(x:Z 7) -> g (x * 2) + 3 == 0 }}
[00:03:04.316] Goal prove (goal number 0):
[00:03:04.316] let { x@1 = Prelude.Nat
      -> sort 0
      x@2 = Integer
      -> Integer
      -> Integer
      x@3 = Prelude.Nat
      -> Integer
      x@4 = (n : Prelude.Nat)
      -> IntMod n
      -> Integer
      x@5 = natToInt 7
    }
 in (x : IntModNum (Cryptol.TCNum 7))
-> EqTrue
     (intEq (natToInt 0)
        (intMod
           (intAdd (natToInt 3)
              (fromIntMod 7
                 (g
                    (toIntMod 7
                       (intMod (intMul (natToInt 2) (fromIntMod 7 x)) x@5)))))
           x@5))
[00:03:04.321] Prop
[00:03:04.321] prove: 1 unsolved subgoal(s)
[00:03:04.321] Unfinished: 1 goals remaining