Add support for translating opaque constants from unknown

`primitive` declarations from Cryptol into `Parameter`
declarations in Coq.

In the Coq generator, distinguish between `ExtCns` values
and opauqe constants.  ExtCns values are translated using
the Coq `Variable` declaration, wherease opaque constants
are translated using the `Parameter` declaration.
At top-level, these declarations are essentially the same.
However `Parameter` interacts with the module system,
whereas `Variable` interacts with the section mechanism.
Currently, we make use of neither, but the distinction
may eventually be useful.

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

@@ -653,17 +653,31 @@ proveProp sc env prop =
 
         _ -> do panic "proveProp" [pretty prop]
 
-importPrimitive :: SharedContext -> Env -> C.Name -> C.Schema -> IO Term
-importPrimitive sc env n sch
+importPrimitive :: SharedContext -> ImportPrimitiveOptions -> Env -> C.Name -> C.Schema -> IO Term
+importPrimitive sc primOpts env n sch
+  -- lookup primitive in the main primitive lookup table
   | Just nm <- C.asPrim n, Just term <- Map.lookup nm allPrims = term sc
+
+  -- lookup primitive in the main reference implementation lookup table
   | Just nm <- C.asPrim n, Just expr <- Map.lookup nm (envRefPrims env) =
       do t <- importSchema sc env sch
          e <- importExpr sc env expr
          nmi <- importName n
          scConstant' sc nmi e t
+
+  -- Optionally, create an opaque constant representing the primitive
+  -- if it doesn't match one of the ones we know about.
+  | Just _ <- C.asPrim n, allowUnknownPrimitives primOpts =
+      do t <- importSchema sc env sch
+         nmi <- importName n
+         scOpaqueConstant sc nmi t
+
+  -- Panic if we don't know the given primitive (TODO? probably shouldn't be a panic)
   | Just nm <- C.asPrim n = panic "Unknown Cryptol primitive name" [show nm]
+
   | otherwise = panic "Improper Cryptol primitive name" [show n]
 
+
 allPrims :: Map C.PrimIdent (SharedContext -> IO Term)
 allPrims = prelPrims <> arrayPrims <> floatPrims <> suiteBPrims <> primeECPrims
 
@@ -1245,9 +1259,9 @@ importName cnm =
 -- definitions. (With subterm sharing, this is not as bad as it might
 -- seem.) We might want to think about generating let or where
 -- expressions instead.
-importDeclGroup :: Bool -> SharedContext -> Env -> C.DeclGroup -> IO Env
+importDeclGroup :: DeclGroupOptions -> SharedContext -> Env -> C.DeclGroup -> IO Env
 
-importDeclGroup isTopLevel sc env (C.Recursive [decl]) =
+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)]
@@ -1258,11 +1272,11 @@ importDeclGroup isTopLevel sc env (C.Recursive [decl]) =
          let x = nameToLocalName (C.dName decl)
          f' <- scLambda sc x t' e'
          rhs <- scGlobalApply sc "Prelude.fix" [t', f']
-         rhs' <- if isTopLevel then
-                    do nmi <- importName (C.dName decl)
-                       scConstant' sc nmi rhs t'
-                 else
-                   return rhs
+         rhs' <- case declOpts of
+                   TopLevelDeclGroup _ ->
+                     do nmi <- importName (C.dName decl)
+                        scConstant' sc nmi rhs t'
+                   NestedDeclGroup -> return rhs
          let env' = env { envE = Map.insert (C.dName decl) (rhs', 0) (envE env)
                         , envC = Map.insert (C.dName decl) (C.dSignature decl) (envC env) }
          return env'
@@ -1272,7 +1286,7 @@ importDeclGroup isTopLevel sc env (C.Recursive [decl]) =
 -- We handle this by "tupling up" all the declarations using a record and
 -- taking the fixpoint at this record type.  The desired declarations are then
 -- achieved by projecting the field names from this record.
-importDeclGroup isTopLevel sc env (C.Recursive decls) =
+importDeclGroup declOpts sc env (C.Recursive decls) =
   do -- build the environment for the declaration bodies
      let dm = Map.fromList [ (C.dName d, d) | d <- decls ]
 
@@ -1319,44 +1333,63 @@ importDeclGroup isTopLevel sc env (C.Recursive decls) =
      let mkRhs d t =
            do let s = nameToFieldName (C.dName d)
               r <- scRecordSelect sc rhs s
-              if isTopLevel then
-                do nmi <- importName (C.dName d)
-                   scConstant' sc nmi r t
-              else
-                return r
+              case declOpts of
+                TopLevelDeclGroup _ ->
+                  do nmi <- importName (C.dName d)
+                     scConstant' sc nmi r t
+                NestedDeclGroup -> return r
      rhss <- sequence (Map.intersectionWith mkRhs dm tm)
 
      let env' = env { envE = Map.union (fmap (\v -> (v, 0)) rhss) (envE env)
                     , envC = Map.union (fmap C.dSignature dm) (envC env)
                     }
      return env'
 
-importDeclGroup isTopLevel sc env (C.NonRecursive decl) =
+importDeclGroup declOpts sc env (C.NonRecursive decl) =
   case C.dDefinition decl of
     C.DPrim
-     | isTopLevel -> do
-        rhs <- importPrimitive sc env (C.dName decl) (C.dSignature decl)
+     | TopLevelDeclGroup primOpts <- declOpts -> do
+        rhs <- importPrimitive sc primOpts env (C.dName decl) (C.dSignature decl)
         let env' = env { envE = Map.insert (C.dName decl) (rhs, 0) (envE env)
-                      , envC = Map.insert (C.dName decl) (C.dSignature decl) (envC env) }
+                       , envC = Map.insert (C.dName decl) (C.dSignature decl) (envC env)
+                       }
         return env'
      | otherwise -> do
         panic "importDeclGroup" ["Primitive declarations only allowed at top-level:", show (C.dName decl)]
 
     C.DExpr expr -> do
      rhs <- importExpr' sc env (C.dSignature decl) expr
-     rhs' <- if not isTopLevel then return rhs else do
-       nmi <- importName (C.dName decl)
-       t <- importSchema sc env (C.dSignature decl)
-       scConstant' sc nmi rhs t
+     rhs' <- case declOpts of
+               TopLevelDeclGroup _ ->
+                 do nmi <- importName (C.dName decl)
+                    t <- importSchema sc env (C.dSignature decl)
+                    scConstant' sc nmi rhs t
+               NestedDeclGroup -> return rhs
      let env' = env { envE = Map.insert (C.dName decl) (rhs', 0) (envE env)
                     , envC = Map.insert (C.dName decl) (C.dSignature decl) (envC env) }
      return env'
 
+data ImportPrimitiveOptions =
+  ImportPrimitiveOptions
+  { allowUnknownPrimitives :: Bool
+    -- ^ Should unknown primitives be translated as fresh external constants?
+  }
+
+defaultPrimitiveOptions :: ImportPrimitiveOptions
+defaultPrimitiveOptions =
+  ImportPrimitiveOptions
+  { allowUnknownPrimitives = False
+  }
+
+data DeclGroupOptions
+  = TopLevelDeclGroup ImportPrimitiveOptions
+  | NestedDeclGroup
+
 importDeclGroups :: SharedContext -> Env -> [C.DeclGroup] -> IO Env
-importDeclGroups sc = foldM (importDeclGroup False sc)
+importDeclGroups sc = foldM (importDeclGroup NestedDeclGroup sc)
 
-importTopLevelDeclGroups :: SharedContext -> Env -> [C.DeclGroup] -> IO Env
-importTopLevelDeclGroups sc = foldM (importDeclGroup True sc)
+importTopLevelDeclGroups :: SharedContext -> ImportPrimitiveOptions -> Env -> [C.DeclGroup] -> IO Env
+importTopLevelDeclGroups sc primOpts = foldM (importDeclGroup (TopLevelDeclGroup primOpts) sc)
 
 coerceTerm :: SharedContext -> Env -> C.Type -> C.Type -> Term -> IO Term
 coerceTerm sc env t1 t2 e

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

@@ -33,6 +33,8 @@ module Verifier.SAW.CryptolEnv
   , lookupIn
   , resolveIdentifier
   , meSolverConfig
+  , C.ImportPrimitiveOptions(..)
+  , C.defaultPrimitiveOptions
   )
   where
 
@@ -309,7 +311,7 @@ translateDeclGroups ::
   SharedContext -> CryptolEnv -> [T.DeclGroup] -> IO CryptolEnv
 translateDeclGroups sc env dgs =
   do cryEnv <- mkCryEnv env
-     cryEnv' <- C.importTopLevelDeclGroups sc cryEnv dgs
+     cryEnv' <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions cryEnv dgs
      termEnv' <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE cryEnv')
 
      let decls = concatMap T.groupDecls dgs
@@ -328,7 +330,7 @@ genTermEnv sc modEnv cryEnv0 = do
   let declGroups = concatMap T.mDecls
                  $ filter (not . T.isParametrizedModule)
                  $ ME.loadedModules modEnv
-  cryEnv <- C.importTopLevelDeclGroups sc cryEnv0 declGroups
+  cryEnv <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions cryEnv0 declGroups
   traverse (\(t, j) -> incVars sc 0 j t) (C.envE cryEnv)
 
 --------------------------------------------------------------------------------
@@ -343,9 +345,12 @@ checkNotParameterized m =
 
 loadCryptolModule ::
   (?fileReader :: FilePath -> IO ByteString) =>
-  SharedContext -> CryptolEnv -> FilePath ->
+  SharedContext ->
+  C.ImportPrimitiveOptions ->
+  CryptolEnv ->
+  FilePath ->
   IO (CryptolModule, CryptolEnv)
-loadCryptolModule sc env path = do
+loadCryptolModule sc primOpts env path = do
   let modEnv = eModuleEnv env
   (m, modEnv') <- liftModuleM modEnv (MB.loadModuleByPath path)
   checkNotParameterized m
@@ -361,7 +366,7 @@ loadCryptolModule sc env path = do
   let isNew m' = T.mName m' `notElem` oldModNames
   let newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules $ ME.meLoadedModules modEnv''
   let newDeclGroups = concatMap T.mDecls newModules
-  newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups
+  newCryEnv <- C.importTopLevelDeclGroups sc primOpts oldCryEnv newDeclGroups
   newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
   let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
@@ -422,7 +427,7 @@ importModule sc env src as vis imps = do
   let isNew m' = T.mName m' `notElem` oldModNames
   let newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules $ ME.meLoadedModules modEnv'
   let newDeclGroups = concatMap T.mDecls newModules
-  newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups
+  newCryEnv <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions oldCryEnv newDeclGroups
   newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
   return env { eImports = (vis, P.Import (T.mName m) as imps) : eImports env

saw-core-coq/src/Language/Coq/AST.hs

@@ -70,6 +70,8 @@ data Decl
   = Axiom Ident Type
   | Comment String
   | Definition Ident [Binder] (Maybe Type) Term
+  | Parameter Ident Type
+  | Variable Ident Type
   | InductiveDecl Inductive
   | Snippet String
   deriving (Show)

saw-core-coq/src/Language/Coq/Pretty.hs

@@ -146,6 +146,12 @@ ppDecl decl = case decl of
   Axiom nm ty ->
     (nest 2 $
      hsep ([text "Axiom", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
+  Parameter nm ty ->
+    (nest 2 $
+     hsep ([text "Parameter", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
+  Variable nm ty ->
+    (nest 2 $
+     hsep ([text "Variable", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
   Comment s ->
     text "(*" <+> text s <+> text "*)" <> hardline
   Definition nm bs mty body ->

saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs

@@ -16,6 +16,8 @@ import           Verifier.SAW.Translation.Coq.Monad
 import qualified Verifier.SAW.Translation.Coq.Term  as TermTranslation
 import           Verifier.SAW.TypedTerm
 
+
+
 translateTypedTermMap ::
   TermTranslation.TermTranslationMonad m => Map.Map Name TypedTerm -> m [Coq.Decl]
 translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -130,6 +130,8 @@ namedDecls = concatMap filterNamed
   where
     filterNamed :: Coq.Decl -> [String]
     filterNamed (Coq.Axiom n _)                               = [n]
+    filterNamed (Coq.Parameter n _)                           = [n]
+    filterNamed (Coq.Variable n _)                            = [n]
     filterNamed (Coq.Comment _)                               = []
     filterNamed (Coq.Definition n _ _ _)                      = [n]
     filterNamed (Coq.InductiveDecl (Coq.Inductive n _ _ _ _)) = [n]
@@ -292,7 +294,25 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
         in
         foldM addElement (Coq.App (Coq.Var "Vector.nil") [Coq.Var "_"]) (Vector.reverse vec)
     StringLit s -> pure (Coq.Scope (Coq.StringLit (Text.unpack s)) "string")
-    ExtCns (EC _ _ _) -> errorTermM "External constants not supported"
+
+    ExtCns ec ->
+      do configuration <- asks translationConfiguration
+         let renamed = translateConstant (notations configuration) ec
+         alreadyTranslatedDecls <- getNamesOfAllDeclarations
+         let definitionsToSkip = skipDefinitions configuration
+         if elem renamed alreadyTranslatedDecls || elem renamed definitionsToSkip
+           then Coq.Var <$> pure renamed
+           else do
+             tp <-
+              -- Translate type in a top-level name scope
+              withLocalTranslationState $
+              do modify $ set localEnvironment []
+                 modify $ set unavailableIdents reservedIdents
+                 modify $ set sharedNames IntMap.empty
+                 modify $ set nextSharedName "var__0"
+                 translateTermLet (ecType ec)
+             modify $ over topLevelDeclarations $ (Coq.Variable renamed tp :)
+             Coq.Var <$> pure renamed
 
     -- The translation of a record type {fld1:tp1, ..., fldn:tpn} is
     -- RecordTypeCons fld1 tp1 (... (RecordTypeCons fldn tpn RecordTypeNil)...).
@@ -579,8 +599,28 @@ translateTermUnshared t = withLocalTranslationState $ do
       | n < length env -> Coq.Var <$> pure (env !! n)
       | otherwise -> Except.throwError $ LocalVarOutOfBounds t
 
-  -- Constants come with a body
-    Constant n body -> do
+    -- Constants with no body
+    Constant n Nothing -> do
+      configuration <- asks translationConfiguration
+      let renamed = translateConstant (notations configuration) n
+      alreadyTranslatedDecls <- getNamesOfAllDeclarations
+      let definitionsToSkip = skipDefinitions configuration
+      if elem renamed alreadyTranslatedDecls || elem renamed definitionsToSkip
+        then Coq.Var <$> pure renamed
+        else do
+          tp <-
+           -- Translate type in a top-level name scope
+           withLocalTranslationState $
+           do modify $ set localEnvironment []
+              modify $ set unavailableIdents reservedIdents
+              modify $ set sharedNames IntMap.empty
+              modify $ set nextSharedName "var__0"
+              translateTermLet (ecType n)
+          modify $ over topLevelDeclarations $ (Coq.Parameter renamed tp :)
+          Coq.Var <$> pure renamed
+
+    -- Constants with a body
+    Constant n (Just body) -> do
       configuration <- asks translationConfiguration
       let renamed = translateConstant (notations configuration) n
       alreadyTranslatedDecls <- getNamesOfAllDeclarations

src/SAWScript/Builtins.hs

@@ -1481,7 +1481,7 @@ cryptol_load fileReader path = do
   rw <- getTopLevelRW
   let ce = rwCryptol rw
   let ?fileReader = fileReader
-  (m, ce') <- io $ CEnv.loadCryptolModule sc ce path
+  (m, ce') <- io $ CEnv.loadCryptolModule sc CEnv.defaultPrimitiveOptions ce path
   putTopLevelRW $ rw { rwCryptol = ce' }
   return m
 

src/SAWScript/Prover/Exporter.hs

@@ -66,7 +66,7 @@ import Prettyprinter (vcat)
 
 import Lang.JVM.ProcessUtils (readProcessExitIfFailure)
 
-import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule)
+import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule, ImportPrimitiveOptions(..))
 import Verifier.SAW.Cryptol.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule)
 import Verifier.SAW.ExternalFormat(scWriteExternal)
 import Verifier.SAW.FiniteValue
@@ -471,7 +471,8 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
   let ?fileReader = BS.readFile
   env <- initCryptolEnv sc
   cryptolPrimitivesForSAWCoreModule <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule
-  (cm, _) <- loadCryptolModule sc env inputFile
+  let primOpts = ImportPrimitiveOptions{ allowUnknownPrimitives = True }
+  (cm, _) <- loadCryptolModule sc primOpts env inputFile
   let cryptolPreludeDecls = map Coq.moduleDeclName (moduleDecls cryptolPrimitivesForSAWCoreModule)
   let configuration =
         withImportCryptolPrimitivesForSAWCoreExtra $

src/SAWScript/X86.hs

@@ -127,7 +127,7 @@ import Verifier.SAW.Recognizer(asBool)
 import Verifier.SAW.Simulator.What4.ReturnTrip (sawRegisterSymFunInterp, toSC, saw_ctx)
 
 -- Cryptol Verifier
-import Verifier.SAW.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule)
+import Verifier.SAW.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule,defaultPrimitiveOptions)
 import Verifier.SAW.Cryptol.Prelude(scLoadPreludeModule,scLoadCryptolModule)
 
 -- SAWScript
@@ -365,7 +365,7 @@ loadCry sym mb =
      env <- initCryptolEnv sc
      case mb of
        Nothing   -> return env
-       Just file -> snd <$> loadCryptolModule sc env file
+       Just file -> snd <$> loadCryptolModule sc defaultPrimitiveOptions env file
 
 
 --------------------------------------------------------------------------------