Add a stub typeclass dictionary for the Field instance for Z n

cryptol-saw-core/saw/Cryptol.sawcore

@@ -899,6 +899,20 @@ PFieldRational =
   };
 
 
+PFieldIntMod : (n : Nat) -> PField (IntMod n);
+PFieldIntMod n =
+  { fieldRing = PRingIntMod n
+  , recip     = \(x : IntMod n) -> error (IntMod n) "Unimplemented: recip IntMod"
+  , fieldDiv  = \(x y : IntMod n) -> error (IntMod n) "Unimplemented: (/.) IntMod"
+  };
+
+PFieldIntModNum : (n : Num) -> PField (IntModNum n);
+PFieldIntModNum num =
+  Num#rec (\ (n : Num) -> PField (IntModNum n))
+    PFieldIntMod
+    (error (PField (IntModNum TCInf)) "PFieldIntModNum: no instance for inf")
+    num;
+
 -- Round class
 
 PRound : sort 0 -> sort 1;

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -189,6 +189,7 @@ importPC sc pc =
     C.PGeq       -> panic "importPC PGeq" []
     C.PFin       -> panic "importPC PFin" []
     C.PHas _     -> panic "importPC PHas" []
+    C.PPrime     -> panic "importPC PPrime" []
     C.PZero      -> scGlobalDef sc "Cryptol.PZero"
     C.PLogic     -> scGlobalDef sc "Cryptol.PLogic"
     C.PRing      -> scGlobalDef sc "Cryptol.PRing"
@@ -449,6 +450,10 @@ proveProp sc env prop =
         -- instance Field Rational
         (C.pIsField -> Just (C.tIsRational -> True))
           -> do scGlobalApply sc "Cryptol.PFieldRational" []
+        -- instance (prime p) => Field (Z p)
+        (C.pIsField -> Just (C.tIsIntMod -> Just n))
+          -> do n' <- importType sc env n
+                scGlobalApply sc "Cryptol.PFieldIntModNum" [n']
         -- instance (ValidFloat e p) => Field (Float e p)
         (C.pIsField -> Just (C.tIsFloat -> Just (e, p)))
           -> do e' <- importType sc env e

cryptol-saw-core/test/instance.cry

@@ -188,6 +188,10 @@ fieldRational = recip
 fieldFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p
 fieldFloat = recip
 
+/* instance (prime p) => Field (Z p) */
+fieldZ : {p} prime p => Z p -> Z p
+fieldZ = recip
+
 ////////////////////////////////////////////////////////////////////////////////
 // Round