T1169

.github/ci.sh

@@ -134,10 +134,7 @@ install_system_deps() {
 test_dist() {
   setup_dist_bins
   setup_external_tools
-  if $IS_WIN; then
-    echo "Warning: janky hacky workaround to #764"
-    sed -i 's!/!\\!g' tests/modsys/T14.icry.stdout
-  fi
+  echo "test-runner version: $($BIN/test-runner --version)"
   $BIN/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol tests
 }
 

README.md

@@ -1,4 +1,4 @@
-[![Cryptol](https://github.com/GaloisInc/cryptol/actions/workflows/build.yml/badge.svg?event=push)](https://github.com/GaloisInc/cryptol/actions/workflows/ci.yml)
+[![Cryptol](https://github.com/GaloisInc/cryptol/workflows/Cryptol/badge.svg)](https://github.com/GaloisInc/cryptol/actions?query=workflow%3ACryptol)
 
 # Cryptol, version 2
 

cabal.GHC-8.10.2.config

@@ -183,7 +183,7 @@ constraints: any.Cabal ==3.2.0.0,
              any.test-framework ==0.8.2.0,
              any.test-framework-hunit ==0.3.0.2,
              test-framework-hunit -base3 +base4,
-             any.test-lib ==0.2.2,
+             any.test-lib ==0.3,
              any.text ==1.2.4.1,
              any.text-short ==0.1.3,
              text-short -asserts,

cabal.GHC-8.10.3.config

@@ -223,7 +223,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.test-framework ==0.8.2.0,
              any.test-framework-hunit ==0.3.0.2,
              test-framework-hunit -base3 +base4,
-             any.test-lib ==0.2.2,
+             any.test-lib ==0.3,
              any.text ==1.2.4.1,
              any.text-short ==0.1.3,
              text-short -asserts,

cabal.GHC-8.6.5.config

@@ -184,7 +184,7 @@ constraints: any.Cabal ==2.4.0.1,
              any.test-framework ==0.8.2.0,
              any.test-framework-hunit ==0.3.0.2,
              test-framework-hunit -base3 +base4,
-             any.test-lib ==0.2.1,
+             any.test-lib ==0.3,
              any.text ==1.2.4.0,
              any.tf-random ==0.5,
              any.th-abstraction ==0.3.2.0,

cabal.GHC-8.8.4.config

@@ -181,7 +181,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.test-framework ==0.8.2.0,
              any.test-framework-hunit ==0.3.0.2,
              test-framework-hunit -base3 +base4,
-             any.test-lib ==0.2.1,
+             any.test-lib ==0.3,
              any.text ==1.2.4.0,
              any.tf-random ==0.5,
              any.th-abstraction ==0.3.2.0,

cryptol-remote-api/python/cryptol/__init__.py

@@ -4,6 +4,7 @@
 
 import base64
 import os
+from enum import Enum
 from dataclasses import dataclass
 from distutils.spawn import find_executable
 from typing import Any, List, NoReturn, Optional, Union
@@ -172,8 +173,13 @@ def __init__(self, connection : HasProtocolState, expr : Any) -> None:
     def process_result(self, res : Any) -> Any:
         return res['type schema']
 
+class SmtQueryType(str, Enum):
+    PROVE = 'prove'
+    SAFE  = 'safe'
+    SAT   = 'sat'
+
 class CryptolProveSat(argo.Command):
-    def __init__(self, connection : HasProtocolState, qtype : str, expr : Any, solver : solver.Solver, count : Optional[int]) -> None:
+    def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : solver.Solver, count : Optional[int]) -> None:
         super(CryptolProveSat, self).__init__(
             'prove or satisfy',
             {'query type': qtype,
@@ -186,12 +192,12 @@ def __init__(self, connection : HasProtocolState, qtype : str, expr : Any, solve
 
     def process_result(self, res : Any) -> Any:
         if res['result'] == 'unsatisfiable':
-            if self.qtype == 'sat':
+            if self.qtype == SmtQueryType.SAT:
                 return False
-            elif self.qtype == 'prove':
+            elif self.qtype == SmtQueryType.PROVE or self.qtype == SmtQueryType.SAFE:
                 return True
             else:
-                raise ValueError("Unknown prove/sat query type: " + self.qtype)
+                raise ValueError("Unknown SMT query type: " + self.qtype)
         elif res['result'] == 'invalid':
             return [from_cryptol_arg(arg['expr'])
                     for arg in res['counterexample']]
@@ -200,15 +206,19 @@ def process_result(self, res : Any) -> Any:
                     for m in res['models']
                     for arg in m]
         else:
-            raise ValueError("Unknown sat result " + str(res))
+            raise ValueError("Unknown SMT result: " + str(res))
 
 class CryptolProve(CryptolProveSat):
     def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
-        super(CryptolProve, self).__init__(connection, 'prove', expr, solver, 1)
+        super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1)
 
 class CryptolSat(CryptolProveSat):
     def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None:
-        super(CryptolSat, self).__init__(connection, 'sat', expr, solver, count)
+        super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count)
+
+class CryptolSafe(CryptolProveSat):
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
+        super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1)
 
 class CryptolNames(argo.Command):
     def __init__(self, connection : HasProtocolState) -> None:
@@ -257,7 +267,7 @@ def connect(command : Optional[str]=None,
     :param cryptol_path: A replacement for the contents of
       the ``CRYPTOLPATH`` environment variable (if provided).
 
-    :param url: A URL at which to connect to an already running Cryptol 
+    :param url: A URL at which to connect to an already running Cryptol
     HTTP server.
 
     :param reset_server: If ``True``, the server that is connected to will be
@@ -439,6 +449,13 @@ def prove(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
         self.most_recent_result = CryptolProve(self, expr, solver)
         return self.most_recent_result
 
+    def safe(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
+        """Check via an external SMT solver that the given term is safe for all inputs,
+        which means it cannot encounter a run-time error.
+        """
+        self.most_recent_result = CryptolSafe(self, expr, solver)
+        return self.most_recent_result
+
     def names(self) -> argo.Command:
         """Discover the list of names currently in scope in the current context."""
         self.most_recent_result = CryptolNames(self)

cryptol-remote-api/python/tests/cryptol/test_AES.py

@@ -28,8 +28,8 @@ def test_AES(self):
         decrypted_ct = c.call("aesDecrypt", (ct, key)).result()
         self.assertEqual(pt, decrypted_ct)
 
-        # c.safe("aesEncrypt")
-        # c.safe("aesDecrypt")
+        self.assertTrue(c.safe("aesEncrypt"))
+        self.assertTrue(c.safe("aesDecrypt"))
         self.assertTrue(c.check("AESCorrect").result().success)
         # c.prove("AESCorrect") # probably takes too long for this script...?
 

cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py

@@ -138,6 +138,15 @@ def test_check(self):
         self.assertEqual(len(res.args), 1)
         self.assertIsInstance(res.error_msg, str)
 
+    def test_safe(self):
+        c = self.c
+        res = c.safe("\\x -> x==(x:[8])").result()
+        self.assertTrue(res)
+
+        res = c.safe("\\x -> x / (x:[8])").result()
+        self.assertEqual(res, [BV(size=8, value=0)])
+
+
     def test_many_usages_one_connection(self):
         c = self.c
         for i in range(0,100):

cryptol-remote-api/src/CryptolServer/Sat.hs

@@ -157,6 +157,7 @@ instance FromJSON ProveSatParams where
            \case
              "sat" -> pure (SatQuery numResults)
              "prove" -> pure ProveQuery
+             "safe" -> pure SafetyQuery
              _ -> empty)
       num v = ((JSON.withText "all" $
                \t -> if t == "all" then pure AllSat else empty) v) <|>
@@ -174,17 +175,23 @@ instance Doc.DescribedParams ProveSatParams where
                      ++ (concat (map (\p -> [Doc.Literal (T.pack p), Doc.Text ", "]) proverNames))
                      ++ [Doc.Text "."]))
     , ("expression",
-      Doc.Paragraph [Doc.Text "The predicate (i.e., function) to check for satisfiability; "
-                    , Doc.Text "must be a monomorphic function with return type Bit." ])
+      Doc.Paragraph [ Doc.Text "The function to check for validity, satisfiability, or safety"
+                    , Doc.Text " depending on the specified value for "
+                    , Doc.Literal "query type"
+                    , Doc.Text ". For validity and satisfiability checks, the function must be a predicate"
+                    , Doc.Text " (i.e., monomorphic function with return type Bit)."
+                    ])
     , ("result count",
       Doc.Paragraph [Doc.Text "How many satisfying results to search for; either a positive integer or "
-                    , Doc.Literal "all", Doc.Text"."])
+                    , Doc.Literal "all", Doc.Text". Only affects satisfiability checks."])
     , ("query type",
-      Doc.Paragraph [ Doc.Text "Whether to attempt to prove ("
+      Doc.Paragraph [ Doc.Text "Whether to attempt to prove the predicate is true for all possible inputs ("
                     , Doc.Literal "prove"
-                    , Doc.Text ") or satisfy ("
+                    , Doc.Text "), find some inputs which make the predicate true ("
                     , Doc.Literal "sat"
-                    , Doc.Text ") the predicate."
+                    , Doc.Text "), or prove a function is safe ("
+                    , Doc.Literal "safe"
+                    , Doc.Text ")."
                     ]
       )
     ]

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -16,6 +16,7 @@
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedStrings #-}
 module Cryptol.ModuleSystem.NamingEnv where
 
 import Data.List (nub)
@@ -106,6 +107,11 @@ merge :: [Name] -> [Name] -> [Name]
 merge xs ys | xs == ys  = xs
             | otherwise = nub (xs ++ ys)
 
+instance PP NamingEnv where
+  ppPrec _ (NamingEnv mps)   = vcat $ map ppNS $ Map.toList mps
+    where ppNS (ns,xs) = pp ns $$ nest 2 (vcat (map ppNm (Map.toList xs)))
+          ppNm (x,as)  = pp x <+> "->" <+> hsep (punctuate comma (map pp as))
+
 -- | Generate a mapping from 'PrimIdent' to 'Name' for a
 -- given naming environment.
 toPrimMap :: NamingEnv -> PrimMap

src/Cryptol/ModuleSystem/Renamer.hs

@@ -161,8 +161,10 @@ renameModule' thisNested env mpath m =
          allImps   = openLoop allNested env openDs imps
 
      (inScope,decls') <-
-        shadowNames allImps $
+        shadowNames' CheckNone allImps $
         shadowNames' CheckOverlap env $
+                          -- maybe we should allow for a warning
+                          -- if a local name shadows an imported one?
         do inScope <- getNamingEnv
            ds      <- renameTopDecls' (allNested,mpath) (mDecls m)
            pure (inScope, ds)

src/Cryptol/ModuleSystem/Renamer/Monad.hs

@@ -250,10 +250,16 @@ checkEnv check (NamingEnv lenv) r rw0
 
   where
   newEnv         = NamingEnv newMap
-  (rwFin,newMap) = Map.mapAccumWithKey doNS rw0 lenv
+  (rwFin,newMap) = Map.mapAccumWithKey doNS rw0 lenv  -- lenv 1 ns at a time
   doNS rw ns     = Map.mapAccumWithKey (step ns) rw
 
-  step ns acc k xs = (acc', [head xs])
+  -- namespace, current state, k : parse name, xs : possible entities for k
+  step ns acc k xs = (acc', case check of
+                              CheckNone -> xs
+                              _         -> [head xs]
+                              -- we've already reported an overlap error,
+                              -- so resolve arbitrarily to  the first entry
+                      )
     where
     acc' = acc
       { rwWarnings =

tests/cryptol-test-runner.cabal

@@ -16,7 +16,7 @@ flag static
 
 executable cryptol-test-runner
   Main-is:             Main.hs
-  build-depends:       base,filepath,test-lib
+  build-depends:       base,filepath,test-lib >= 0.3
   GHC-options:         -Wall -O2
   Default-language:    Haskell2010
 

tests/modsys/T14.icry.stdout.mingw32

@@ -0,0 +1,4 @@
+Loading module Cryptol
+
+Parse error at .\T14\Main.cry:3:9,
+  unexpected: MalformedUtf8

tests/modsys/T15.icry

@@ -0,0 +1 @@
+:module T15::B

tests/modsys/T15.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T15::A
+Loading module T15::B

tests/modsys/T15/A.cry

@@ -0,0 +1,5 @@
+module T15::A where
+
+update = 0x02
+
+

tests/modsys/T15/B.cry

@@ -0,0 +1,3 @@
+module T15::B where
+
+import T15::A

tests/modsys/T16.icry

@@ -0,0 +1 @@
+:module T16::B

tests/modsys/T16.icry.stdout

@@ -0,0 +1,9 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T16::A
+Loading module T16::B
+
+[error] at ./T16/B.cry:5:5--5:11
+    Multiple definitions for symbol: update
+    (at Cryptol:844:11--844:17, update)
+    (at ./T16/A.cry:3:1--3:7, T16::A::update)

tests/modsys/T16.icry.stdout.mingw32

@@ -0,0 +1,9 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T16::A
+Loading module T16::B
+
+[error] at .\T16\B.cry:5:5--5:11
+    Multiple definitions for symbol: update
+    (at Cryptol:844:11--844:17, update)
+    (at .\T16\A.cry:3:1--3:7, T16::A::update)

tests/modsys/T16/A.cry

@@ -0,0 +1,5 @@
+module T16::A where
+
+update = 0x02
+
+

tests/modsys/T16/B.cry

@@ -0,0 +1,5 @@
+module T16::B where
+
+import T16::A
+
+f = update

tests/modsys/T17.icry

@@ -0,0 +1 @@
+:module T17::B

tests/modsys/T17.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T17::A
+Loading module T17::A1
+Loading module T17::B

tests/modsys/T17/A.cry

@@ -0,0 +1,5 @@
+module T17::A where
+
+u = 0x02
+
+

tests/modsys/T17/A1.cry

@@ -0,0 +1,5 @@
+module T17::A1 where
+
+u = 0x03
+
+

tests/modsys/T17/B.cry

@@ -0,0 +1,4 @@
+module T17::B where
+
+import T17::A
+import T17::A1

tests/modsys/T18.icry

@@ -0,0 +1 @@
+:module T18::B

tests/modsys/T18.icry.stdout

@@ -0,0 +1,10 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T18::A
+Loading module T18::A1
+Loading module T18::B
+
+[error] at ./T18/B.cry:6:5--6:6
+    Multiple definitions for symbol: u
+    (at ./T18/A.cry:3:1--3:2, T18::A::u)
+    (at ./T18/A1.cry:3:1--3:2, T18::A1::u)

tests/modsys/T18.icry.stdout.mingw32

@@ -0,0 +1,10 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T18::A
+Loading module T18::A1
+Loading module T18::B
+
+[error] at .\T18\B.cry:6:5--6:6
+    Multiple definitions for symbol: u
+    (at .\T18\A.cry:3:1--3:2, T18::A::u)
+    (at .\T18\A1.cry:3:1--3:2, T18::A1::u)

tests/modsys/T18/A.cry

@@ -0,0 +1,5 @@
+module T18::A where
+
+u = 0x02
+
+

tests/modsys/T18/A1.cry

@@ -0,0 +1,5 @@
+module T18::A1 where
+
+u = 0x03
+
+

tests/modsys/T18/B.cry

@@ -0,0 +1,6 @@
+module T18::B where
+
+import T18::A
+import T18::A1
+
+f = u