goal_eval_unint chokes on modular types

[msaaltink]

With these definitions

let {{
  f: Integer -> Integer
  f x = x+1

  g: Z 7 -> Z 7
  g x = x + 1
 }};

prove (w4_unint_z3 ["f"]) {{ f 0 == f 0 }};
prove do { goal_eval_unint ["f"]; w4; } {{ f 0 == f 0 }};

prove (w4_unint_z3 ["g"]) {{ g 0 == g 0 }};
prove do { goal_eval_unint ["g"]; w4; } {{ g 0 == g 0 }};

SAW is fine until the last line, where it fails with the message

could not create uninterpreted function argument of type (IntMod 7)

[brianhuffman]

Related to #1045.

[brianhuffman]

I attempted to make an easy fix for this in #1274, but as it turns out there is an additional problem that we also need to deal with: Because what4 does not have an integers-mod-n type, we need to translate everything to what4 integer operations. Then when we translate those back from what4 to saw-core, they turn into saw-core operations on type Integer, which is the wrong type.

If we put a call to check_goal after goal_eval_unint, we can see that the resulting goals are not well-typed:

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

We need to decide what we should do here. Probably the easiest way to fix it is to have goal_eval_unint just turn all additions, subtractions, and multiplications on type IntMod n into the corresponding operations on Integer, and insert the coercions toIntMod and fromIntMod in the right places to make the terms well-typed.