Opaque constants

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
@@ -603,13 +643,17 @@ translateTermUnshared t = withLocalTranslationState $ do
     badTerm          = Except.throwError $ BadTerm t
 
 -- | In order to turn fixpoint computations into iterative computations, we need
--- to be able to create "dummy" values at the type of the computation.  For now,
--- we will support arbitrary nesting of vectors of boolean values.
+-- to be able to create "dummy" values at the type of the computation.
 defaultTermForType ::
   TermTranslationMonad m =>
   Term -> m Coq.Term
 defaultTermForType typ = do
   case typ of
+    (asBoolType -> Just ()) -> translateIdent (mkIdent preludeName "False")
+
+    (isGlobalDef "Prelude.Nat" -> Just ()) -> return $ Coq.NatLit 0
+
+    (asIntegerType -> Just ()) -> return $ Coq.ZLit 0
 
     (asSeq -> Just (n, typ')) -> do
       seqConst <- translateIdent (mkIdent (mkModuleName ["Cryptol"]) "seqConst")
@@ -618,13 +662,19 @@ defaultTermForType typ = do
       defaultT <- defaultTermForType typ'
       return $ Coq.App seqConst [ nT, typ'T, defaultT ]
 
-    (asBoolType -> Just ()) -> translateIdent (mkIdent preludeName "False")
+    (asPairType -> Just (x,y)) -> do
+      x' <- defaultTermForType x
+      y' <- defaultTermForType y
+      return $ Coq.App (Coq.Var "pair") [x',y']
 
-    _ ->
-      return $ Coq.App (Coq.Var "error")
-      [Coq.StringLit ("Could not generate default value of type " ++ showTerm typ)]
+    (asPiList -> (bs,body))
+      | not (null bs)
+      , looseVars body == emptyBitSet ->
+      do bs'   <- forM bs $ \ (_nm, ty) -> Coq.Binder "_" . Just <$> translateTerm ty
+         body' <- defaultTermForType body
+         return $ Coq.Lambda bs' body'
 
-    -- _ -> Except.throwError $ CannotCreateDefaultValue typ
+    _ -> Except.throwError $ CannotCreateDefaultValue typ
 
 translateTermToDocWith ::
   TranslationConfiguration ->

saw-core/src/Verifier/SAW/ExternalFormat.hs

@@ -134,9 +134,12 @@ scWriteExternal t0 =
         Lambda s t e   -> pure $ unwords ["Lam", Text.unpack s, show t, show e]
         Pi s t e       -> pure $ unwords ["Pi", Text.unpack s, show t, show e]
         LocalVar i     -> pure $ unwords ["Var", show i]
-        Constant ec e  ->
+        Constant ec (Just e)  ->
             do stashName ec
                pure $ unwords ["Constant", show (ecVarIndex ec), show (ecType ec), show e]
+        Constant ec Nothing ->
+            do stashName ec
+               pure $ unwords ["ConstantOpaque", show (ecVarIndex ec), show (ecType ec)]
         FTermF ftf     ->
           case ftf of
             Primitive ec ->
@@ -295,7 +298,8 @@ scReadExternal sc input =
         ["Lam", x, t, e]    -> Lambda (Text.pack x) <$> readIdx t <*> readIdx e
         ["Pi", s, t, e]     -> Pi (Text.pack s) <$> readIdx t <*> readIdx e
         ["Var", i]          -> pure $ LocalVar (read i)
-        ["Constant",i,t,e]  -> Constant <$> readEC i t <*> readIdx e
+        ["Constant",i,t,e]  -> Constant <$> readEC i t <*> (Just <$> readIdx e)
+        ["ConstantOpaque",i,t]  -> Constant <$> readEC i t <*> pure Nothing
         ["Primitive", i, t] -> FTermF <$> (Primitive <$> readPrimName i t)
         ["Unit"]            -> pure $ FTermF UnitValue
         ["UnitT"]           -> pure $ FTermF UnitType

saw-core/src/Verifier/SAW/Recognizer.hs

@@ -313,8 +313,8 @@ asLocalVar :: Recognizer Term DeBruijnIndex
 asLocalVar (unwrapTermF -> LocalVar i) = return i
 asLocalVar _ = Nothing
 
-asConstant :: Recognizer Term (ExtCns Term, Term)
-asConstant (unwrapTermF -> Constant ec t) = return (ec, t)
+asConstant :: Recognizer Term (ExtCns Term, Maybe Term)
+asConstant (unwrapTermF -> Constant ec mt) = return (ec, mt)
 asConstant _ = Nothing
 
 asExtCns :: Recognizer Term (ExtCns Term)

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -360,7 +360,7 @@ ruleOfProp (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) ann =
   Just $ mkRewriteRule [] x y ann
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) ann =
   Just $ mkRewriteRule [] x y ann
-ruleOfProp (unwrapTermF -> Constant _ body) ann = ruleOfProp body ann
+ruleOfProp (unwrapTermF -> Constant _ (Just body)) ann = ruleOfProp body ann
 ruleOfProp (R.asEq -> Just (_, x, y)) ann =
   Just $ mkRewriteRule [] x y ann
 ruleOfProp (R.asEqTrue -> Just body) ann = ruleOfProp body ann