(Z3) Incomplete Theory of Arithmetic?

[WeeknightMVP]

Looks like I've exposed a gap with the Z type in the Z3 Prover interface:

module Scratch where
  /** predicate over value of arbitrary type */
  type Pred T = T -> Bit

  /** predicate over two values of arbitrary type */
  type BinaryPred T = T -> T -> Bit

  /** binary operation from type X to type Y */
  type Binary X Y = X -> X -> Y

  /** bitvectors sufficiently wide to hold values from 0 to `(p - 1) */
  type BV p = [width (p - 1)]

  /** The third clause should follow from the second, but without it, 
   *  `is_m_field_homomorphic` does not type check. */
  type constraint WeirdConstraint p =
    (fin p, p >= 2, 1 + width (p - 1) >= width p)

  /** maps a p-modular integer (Z p) to a p-modular bitvector (BV p) */
  m: {p} (fin p, p >= 1) => (Z p) -> (BV p)
  m n = fromInteger (fromZ n)

  /** Is `m` field homomorphic over integer operations? */
  is_m_field_homomorphic: {p} (WeirdConstraint p) => BinaryPred (Z p)
  is_m_field_homomorphic x y =
       x +> y == x >+ y
    /\ x *> y == x >* y    // This clause triggers an "incomplete theory" error message.
    /\ m`{p} 1 == 1
      where
        safe_add: {n} (fin n) => [n] -> [n] -> [n+1]
        safe_add u v = (0b0 # u) + (0b0 # v)

        safe_mul: {n} (fin n) => [n] -> [n] -> [n*2]
        safe_mul u v = (zext u) * (zext v)

        (+>): Binary (Z p) (BV p)
        (+>) u v = m (u + v)

        (*>): Binary (Z p) (BV p)
        (*>) u v = m (u * v)

        (>+): Binary (Z p) (BV p)
        (>+) u v = drop ((safe_add (m u) (m v)) % `p)

        (>*): Binary (Z p) (BV p)
        (>*) u v = drop ((safe_mul (m u) (m v)) % `p)

is_m_field_homomorphic (the property that mapping m is commutative over (Z p) and (BV p), which are fields if p is prime, for respective modular addition, multiplication, and identity) requires explicit specification of what I think should be an implicit constraint, but more interestingly, Z3 fails to prove this property for most values of p:

ΓöÅΓöüΓò╕ΓöÅΓöüΓöôΓò╗ Γò╗ΓöÅΓöüΓöôΓò║Γö│Γò╕ΓöÅΓöüΓöôΓò╗
Γöâ  ΓöúΓö│Γö¢ΓöùΓö│Γö¢ΓöúΓöüΓö¢ Γöâ Γöâ ΓöâΓöâ
ΓöùΓöüΓò╕Γò╣ΓöùΓò╕ Γò╣ Γò╣   Γò╣ ΓöùΓöüΓö¢ΓöùΓöüΓò╕
version 2.6.0 (9b97c74)

Loading module Cryptol
Loading module Scratch

Scratch> :prove is_m_field_homomorphic`{2}
Q.E.D.
(Total Elapsed Time: 0.189s, using Z3)
Scratch> :prove is_m_field_homomorphic`{3}
Q.E.D.
(Total Elapsed Time: 0.266s, using Z3)
Scratch> :prove is_m_field_homomorphic`{4}
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))
(Total Elapsed Time: 0.161s, using Z3)
Scratch> :exhaust is_m_field_homomorphic`{4}
Using exhaustive testing.
Passed 16 tests.
Q.E.D.
Scratch> :prove is_m_field_homomorphic`{5}
Q.E.D.
(Total Elapsed Time: 2.266s, using Z3)
Scratch> :prove is_m_field_homomorphic`{6}
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))
(Total Elapsed Time: 0.547s, using Z3)
Scratch> :prove is_m_field_homomorphic`{7}
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))
(Total Elapsed Time: 3.655s, using Z3)
Scratch> :prove is_m_field_homomorphic`{8}
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))
(Total Elapsed Time: 1.308s, using Z3)
Scratch> :prove is_m_field_homomorphic`{9}
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))
(Total Elapsed Time: 5.969s, using Z3)
Scratch> :prove is_m_field_homomorphic`{10} /* ... */
Ctrl-C
Scratch> :exhaust is_m_field_homomorphic`{10}
Using exhaustive testing.
Passed 100 tests.
Q.E.D.

Also, can an inverse mapping m' satisfying this property be expressed in Cryptol?

  /** maps a p-modular bitvector (BV p) to a p-modular integer (Z p) */
  m': {p} is_Z p => (BV p) -> (Z p)
  m' n = zero // TODO

  /** Does `m'` retract `m` (map a value mapped by `m` back to the same value)? */
  does_m'_retract_m: {p} (fin p, p >= 1) => Pred (Z p)
  does_m'_retract_m n =
    m' (m n) == n

[yav]

I added an extra rule so the weird extra constraint shouldn't be needed anymore (I know that's not the ticket is about, but I figured I might as well fix it).

[brianhuffman]

This property involves integers and multiplication; it's not hard to find such properties that z3 can't handle. Also, this one is particularly bad because it uses fromInteger to convert integers to bitvectors. This function is encoded in SMTLib using a bunch of repeated integer divs and mods by 2 to extract the bits, which are then concatenated together at the end. (There is a built-in int2bv function in z3, but as I understand it, if int2bv is not eliminated by applying rewrite rules, then it is treated as an uninterpreted function, which can lead to bogus counterexamples. SBV's translation, which we use, is hard for z3 to reason about, but at least is semantically correct.)

As a workaround, you might want to state your properties using toInteger instead of fromInteger. For example, you can state your field homomorphism property using a relation rel instead of a function m:

rel : {p} (fin p, p >= 1) => Z p -> BV p -> Bool
rel x y = fromZ x == toInteger y

/** Is `m` field homomorphic over integer operations? */
is_rel_field_homomorphic: {p} (WeirdConstraint p, p >= 1) => Z p -> BV p -> Z p -> BV p -> Bool
is_rel_field_homomorphic x x' y y' =
  rel x x' ==>
  rel y y' ==>
  rel (x + y) (x' >+ y') /\
  rel (x * y) (x' >* y') /\
  rel`{p} 1 1
    where
      safe_add: {n} (fin n) => [n] -> [n] -> [n+1]
      safe_add u v = (0b0 # u) + (0b0 # v)

      safe_mul: {n} (fin n) => [n] -> [n] -> [n*2]
      safe_mul u v = (zext u) * (zext v)

      (>+) : Binary (BV p) (BV p)
      (>+) u v = drop ((safe_add u v) % `p)

      (>*) : Binary (BV p) (BV p)
      (>*) u v = drop ((safe_mul u v) % `p)

This one scales a lot better with z3:

Main> :prove is_rel_field_homomorphic`{2}
Q.E.D.
(Total Elapsed Time: 0.030s, using Z3)
Main> :prove is_rel_field_homomorphic`{3}
Q.E.D.
(Total Elapsed Time: 0.039s, using Z3)
Main> :prove is_rel_field_homomorphic`{4}
Q.E.D.
(Total Elapsed Time: 0.042s, using Z3)
Main> :prove is_rel_field_homomorphic`{20}
Q.E.D.
(Total Elapsed Time: 4.438s, using Z3)

[brianhuffman]

I should mention another thing: When you try to prove a cryptol property with variables of type Z p, those are encoded in SMTLib as Int variables with range assumptions 0 <= x and x < p. Technically, integer arithmetic problems with upper and lower bounds on all variables should be completely decidable, but I'm not sure how to get z3 to notice that.

[brianhuffman]

Closing because the undecidability of integer arithmetic is not something we can do anything about.