Merge pull request #1778 from GaloisInc/T1777-isNumeric-prime

Add `prime` to `isNumeric`, define `cryPrime` SMT-LIB function

lib/CryptolTC.z3

@@ -75,6 +75,15 @@
   (cryBool true)
 )
 
+
+(declare-fun cryPrimeUnknown (Int) Bool)
+
+(define-fun cryPrime ((x InfNat)) MaybeBool
+  (ite (isErr x) cryErrProp
+    (cryBool (and (isFin x) (cryPrimeUnknown (value x)))))
+)
+
+
 ; ------------------------------------------------------------------------------
 ; Basic Cryptol assume/assert
 
@@ -327,14 +336,14 @@
 
 ; (declare-fun L () InfNat)
 ; (declare-fun w () InfNat)
-; 
+;
 ; (assert (cryVar L))
 ; (assert (cryVar w))
-; 
+;
 ; (assert (cryAssume (cryFin w)))
 ; (assert (cryAssume (cryGeq w (cryNat 1))))
 ; (assert (cryAssume (cryGeq (cryMul (cryNat 2) w) (cryWidth L))))
-; 
+;
 ; (assert (cryProve
 ;   (cryGeq
 ;     (cryMul
@@ -343,7 +352,7 @@
 ;         (cryMul (cryNat 16) w))
 ;       (cryMul (cryNat 16) w))
 ;     (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w))))))
-; 
+;
 ; (check-sat)
 
 

src/Cryptol/TypeCheck/Solver/SMT.hs

@@ -348,7 +348,8 @@ flatGoal g = [ g { goal = p } | p <- pSplitAnd (goal g) ]
 
 -- | Assumes no 'And'
 isNumeric :: Prop -> Bool
-isNumeric ty = matchDefault False $ msum [ is (|=|), is (|/=|), is (|>=|), is aFin ]
+isNumeric ty = matchDefault False $ msum [ is (|=|), is (|/=|), is (|>=|)
+                                         , is aFin, is aPrime ]
   where
   is f = f ty >> return True
 
@@ -368,6 +369,7 @@ toSMT tvs ty = matchDefault (panic "toSMT" [ "Unexpected type", show ty ])
   , aNat            ~> "cryNat"
 
   , aFin            ~> "cryFin"
+  , aPrime          ~> "cryPrime"
   , (|=|)           ~> "cryEq"
   , (|/=|)          ~> "cryNeq"
   , (|>=|)          ~> "cryGeq"

src/Cryptol/TypeCheck/TypePat.hs

@@ -24,7 +24,7 @@ module Cryptol.TypeCheck.TypePat
   , aRec
   , (|->|)
 
-  , aFin, (|=|), (|/=|), (|>=|)
+  , aFin, aPrime, (|=|), (|/=|), (|>=|)
   , aAnd
   , aTrue
 
@@ -165,6 +165,9 @@ aRec = \a -> case tNoUser a of
 aFin :: Pat Prop Type
 aFin = tp PFin ar1
 
+aPrime :: Pat Prop Type
+aPrime = tp PPrime ar1
+
 (|=|) :: Pat Prop (Type,Type)
 (|=|) = tp PEqual ar2