Merge pull request #1809 from GaloisInc/cryptol-T1491

Python: Bump `argo-client`, `mypy`, `cryptol` versions

.github/workflows/ci.yml

@@ -315,7 +315,8 @@ jobs:
               cd saw-remote-api/python/
               poetry update
               poetry install
-              poetry run mypy saw_client/
+              poetry run mypy --install-types --non-interactive saw_client/ || true
+              poetry run mypy --install-types --non-interactive saw_client/
             os: macos-12
           - name: Check docs
             test: saw-remote-api/scripts/check_docs.sh
@@ -337,7 +338,7 @@ jobs:
 
       - uses: actions/setup-python@v2
         with:
-          python-version: '3.9'
+          python-version: '3.11'
 
       - uses: abatilo/actions-poetry@v2.0.0
         with:

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

@@ -1050,6 +1050,9 @@ importExpr sc env expr =
     C.ELocated _ e ->
       importExpr sc env e
 
+    C.EPropGuards {} ->
+      error "Using contsraint guards is not yet supported by SAW."
+
   where
     the :: Maybe a -> IO a
     the = maybe (panic "importExpr" ["internal type error"]) return
@@ -1063,6 +1066,9 @@ importExpr sc env expr =
 importExpr' :: SharedContext -> Env -> C.Schema -> C.Expr -> IO Term
 importExpr' sc env schema expr =
   case expr of
+    C.EPropGuards {} ->
+      error "Using contsraint guards is not yet supported by SAW."
+
     C.ETuple es ->
       do ty <- the (C.isMono schema)
          ts <- the (C.tIsTuple ty)
@@ -1284,6 +1290,10 @@ importDeclGroup declOpts sc env (C.Recursive [decl]) =
   case C.dDefinition decl of
     C.DPrim ->
       panic "importDeclGroup" ["Primitive declarations cannot be recursive:", show (C.dName decl)]
+
+    C.DForeign {} ->
+      error "`foreign` imports may not be used in SAW specifications"
+
     C.DExpr expr ->
       do env1 <- bindName sc (C.dName decl) (C.dSignature decl) env
          t' <- importSchema sc env (C.dSignature decl)
@@ -1329,6 +1339,8 @@ importDeclGroup declOpts sc env (C.Recursive decls) =
      let extractDeclExpr decl =
            case C.dDefinition decl of
              C.DExpr expr -> importExpr' sc env2 (C.dSignature decl) expr
+             C.DForeign {} ->
+               error "`foreign` imports may not be used in SAW specifications"
              C.DPrim ->
                 panic "importDeclGroup"
                         [ "Primitive declarations cannot be recursive:"
@@ -1366,6 +1378,9 @@ importDeclGroup declOpts sc env (C.Recursive decls) =
 
 importDeclGroup declOpts sc env (C.NonRecursive decl) =
   case C.dDefinition decl of
+    C.DForeign {} ->
+      error "`foreign` imports may not be used in SAW specifications"
+
     C.DPrim
      | TopLevelDeclGroup primOpts <- declOpts -> do
         rhs <- importPrimitive sc primOpts env (C.dName decl) (C.dSignature decl)
@@ -1480,7 +1495,7 @@ tNoUser initialTy =
   case C.tNoUser initialTy of
     C.TNewtype nt _ -> C.TRec $ C.ntFields nt
     t -> t
-  
+
 
 -- | Deconstruct a cryptol tuple type as a pair according to the
 -- saw-core tuple type encoding.
@@ -1596,6 +1611,10 @@ importMatches sc env [C.Let decl]
 
 importMatches sc env (C.Let decl : matches) =
   case C.dDefinition decl of
+
+    C.DForeign {} ->
+      error "`foreign` imports may not be used in SAW specifications"
+
     C.DPrim -> do
      panic "importMatches" ["Primitive declarations not allowed in 'let':", show (C.dName decl)]
     C.DExpr expr -> do

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

@@ -372,7 +372,7 @@ loadCryptolModule ::
   IO (CryptolModule, CryptolEnv)
 loadCryptolModule sc primOpts env path = do
   let modEnv = eModuleEnv env
-  (m, modEnv') <- liftModuleM modEnv (MB.loadModuleByPath path)
+  (m, modEnv') <- liftModuleM modEnv (snd <$> MB.loadModuleByPath True path)
   checkNotParameterized m
 
   let ifaceDecls = getAllIfaceDecls modEnv'
@@ -439,7 +439,7 @@ importModule sc env src as vis imps = do
   (m, modEnv') <-
     liftModuleM modEnv $
     case src of
-      Left path -> MB.loadModuleByPath path
+      Left path -> snd <$> MB.loadModuleByPath True path
       Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn)
   checkNotParameterized m
 

saw-remote-api/python/mypy.ini

@@ -1,6 +1,6 @@
 [mypy]
 no_implicit_optional = True
-python_version = 3.7
+python_version = 3.11
 warn_return_any = True
 warn_unused_configs = True
 warn_unused_ignores = True

saw-remote-api/python/pyproject.toml

@@ -14,11 +14,11 @@ include = [
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = "2.12.4" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
-argo-client = "0.0.10"
+cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+argo-client = "0.0.11"
 
 [tool.poetry.dev-dependencies]
-mypy = "^0.812"
+mypy = "^0.991"
 
 [build-system]
 requires = ["poetry>=1.1.4", "setuptools>=40.8.0"]