Coq translator: fix array literal support (#1815)

* changed the implementation of write_coq_cryptol_module so that the output types of Coq Definitions generated from cryptol modules are annotated with the translations of their types

* added more haddocks and other comments

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

@@ -19,7 +19,7 @@ import Cryptol.Utils.PP (pretty)
 import qualified Cryptol.Utils.Ident as C (mkIdent)
 import qualified Cryptol.Utils.RecordMap as C (recordFromFields)
 
-import Verifier.SAW.Cryptol (scCryptolType)
+import Verifier.SAW.Cryptol (scCryptolType, Env, importKind, importSchema)
 import Verifier.SAW.FiniteValue
 import Verifier.SAW.Recognizer (asExtCns)
 import Verifier.SAW.SharedTerm
@@ -49,6 +49,13 @@ data TypedTermType
  deriving Show
 
 
+-- | Convert the 'ttTerm' field of a 'TypedTerm' to a SAW core term
+ttTypeAsTerm :: SharedContext -> Env -> TypedTerm -> IO Term
+ttTypeAsTerm sc env (TypedTerm (TypedTermSchema schema) _) =
+  importSchema sc env schema
+ttTypeAsTerm sc _ (TypedTerm (TypedTermKind k) _) = importKind sc k
+ttTypeAsTerm _ _ (TypedTerm (TypedTermOther tp) _) = return tp
+
 ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm
 ttTermLens f tt = tt `seq` fmap (\x -> tt{ttTerm = x}) (f (ttTerm tt))
 

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

@@ -32,12 +32,13 @@ import           Verifier.SAW.Module
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Term.Functor
 -- import Verifier.SAW.Term.CtxTerm
-import qualified Verifier.SAW.Translation.Coq.CryptolModule    as CryptolModuleTranslation
+import qualified Verifier.SAW.Translation.Coq.CryptolModule    as CMT
 import qualified Verifier.SAW.Translation.Coq.SAWModule        as SAWModuleTranslation
 import           Verifier.SAW.Translation.Coq.Monad
 import           Verifier.SAW.Translation.Coq.SpecialTreatment
 import qualified Verifier.SAW.Translation.Coq.Term             as TermTranslation
 import           Verifier.SAW.TypedTerm
+import           Verifier.SAW.Cryptol (Env)
 --import Verifier.SAW.Term.Pretty
 -- import qualified Verifier.SAW.UntypedAST as Un
 
@@ -92,8 +93,11 @@ traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a
 text :: String -> Doc ann
 text = pretty
 
--- | Eventually, different modules may want different preambles.  For now,
--- we hardcode a sufficient set of imports for all our purposes.
+-- | Generate a preamble for a Coq file, containing a list of Coq imports. This
+-- includes standard imports, one of which is the @VectorNotations@ module to
+-- support the vector literals used to translate SAW core array values, along
+-- with any user-supplied imports in the 'postPreamble' field of the
+-- supplied 'TranslationConfiguration'.
 preamble :: TranslationConfiguration -> Doc ann
 preamble (TranslationConfiguration { vectorModule, postPreamble }) = text [i|
 (** Mandatory imports from saw-core-coq *)
@@ -102,7 +106,7 @@ From Coq Require Import String.
 From Coq Require Import Vectors.Vector.
 From CryptolToCoq Require Import SAWCoreScaffolding.
 From CryptolToCoq Require Import #{vectorModule}.
-Import ListNotations.
+Import VectorNotations.
 
 (** Post-preamble section specified by you *)
 #{postPreamble}
@@ -111,15 +115,17 @@ Import ListNotations.
 |]
 
 translateTermAsDeclImports ::
-  TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann)
-translateTermAsDeclImports configuration name t = do
+  TranslationConfiguration -> Coq.Ident -> Term -> Term ->
+  Either (TranslationError Term) (Doc ann)
+translateTermAsDeclImports configuration name t tp = do
   doc <-
     TermTranslation.translateDefDoc
       configuration
       (TermTranslation.TranslationReader Nothing)
-      [] name t
+      [] name t tp
   return $ vcat [preamble configuration, hardline <> doc]
 
+-- | Translate a SAW core module to a Coq module
 translateSAWModule :: TranslationConfiguration -> Module -> Doc ann
 translateSAWModule configuration m =
   let name = show $ translateModuleName (moduleName m)
@@ -134,21 +140,20 @@ translateSAWModule configuration m =
      , ""
      ]
 
+-- | Translate a Cryptol module to a Coq module
 translateCryptolModule ::
+  SharedContext -> Env ->
   Coq.Ident {- ^ Section name -} ->
   TranslationConfiguration ->
   -- | List of already translated global declarations
   [String] ->
   CryptolModule ->
-  Either (TranslationError Term) (Doc ann)
-translateCryptolModule nm configuration globalDecls m =
-  let decls = CryptolModuleTranslation.translateCryptolModule
-              configuration
-              globalDecls
-              m
-  in
-  Coq.ppDecl . Coq.Section nm <$> decls
+  IO (Either (TranslationError Term) (Doc ann))
+translateCryptolModule sc env nm configuration globalDecls m =
+  fmap (fmap (Coq.ppDecl . Coq.Section nm)) $
+  CMT.translateCryptolModule sc env configuration globalDecls m
 
+-- | Extract out the 'String' name of a declaration in a SAW core module
 moduleDeclName :: ModuleDecl -> Maybe String
 moduleDeclName (TypeDecl (DataType { dtName })) = Just (identName dtName)
 moduleDeclName (DefDecl  (Def      { defIdent })) = Just (identName defIdent)

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

@@ -12,23 +12,26 @@ import           Cryptol.ModuleSystem.Name          (Name, nameIdent)
 import           Cryptol.Utils.Ident                (unpackIdent)
 import qualified Language.Coq.AST                   as Coq
 import           Verifier.SAW.Term.Functor          (Term)
+import           Verifier.SAW.SharedTerm            (SharedContext)
 import           Verifier.SAW.Translation.Coq.Monad
 import qualified Verifier.SAW.Translation.Coq.Term  as TermTranslation
 import           Verifier.SAW.TypedTerm
+import           Verifier.SAW.Cryptol (Env)
 
 
-
+-- | Translate a list of named terms with their types to a Coq definitions
 translateTypedTermMap ::
-  TermTranslation.TermTranslationMonad m => Map.Map Name TypedTerm -> m [Coq.Decl]
-translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
+  TermTranslation.TermTranslationMonad m => [(Name,Term,Term)] -> m [Coq.Decl]
+translateTypedTermMap defs = forM defs translateAndRegisterEntry
   where
-    translateAndRegisterEntry (name, symbol) = do
-      let t = ttTerm symbol
+    translateAndRegisterEntry (name, t, tp) = do
       let nameStr = unpackIdent (nameIdent name)
-      term <- TermTranslation.withLocalTranslationState $ do
-        modify $ set TermTranslation.localEnvironment [nameStr]
-        TermTranslation.translateTerm t
-      let decl = TermTranslation.mkDefinition nameStr term
+      decl <-
+        TermTranslation.withLocalTranslationState $
+        do modify $ set TermTranslation.localEnvironment [nameStr]
+           t_trans <- TermTranslation.translateTerm t
+           tp_trans <- TermTranslation.translateTerm tp
+           return $ TermTranslation.mkDefinition nameStr t_trans tp_trans
       modify $ over TermTranslation.globalDeclarations (nameStr :)
       return decl
 
@@ -37,16 +40,22 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
 -- terms, and accumulating the translated declarations of all top-level
 -- declarations encountered.
 translateCryptolModule ::
+  SharedContext -> Env ->
   TranslationConfiguration ->
   -- | List of already translated global declarations
   [String] ->
   CryptolModule ->
-  Either (TranslationError Term) [Coq.Decl]
-translateCryptolModule configuration globalDecls (CryptolModule _ tm) =
-  reverse . view TermTranslation.topLevelDeclarations . snd
-  <$> TermTranslation.runTermTranslationMonad
-      configuration
-      (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
-      globalDecls
-      []
-      (translateTypedTermMap tm)
+  IO (Either (TranslationError Term) [Coq.Decl])
+translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) =
+  do defs <-
+       forM (Map.assocs tm) $ \(nm, t) ->
+       do tp <- ttTypeAsTerm sc env t
+          return (nm, ttTerm t, tp)
+     return
+       (reverse . view TermTranslation.topLevelDeclarations . snd <$>
+        TermTranslation.runTermTranslationMonad
+        configuration
+        (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
+        globalDecls
+        []
+        (translateTypedTermMap defs))

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

@@ -16,6 +16,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
 
 {- |
 Module      : Verifier.SAW.Translation.Coq
@@ -240,7 +241,8 @@ translateConstant ec maybe_body =
        Just body ->
          -- If the definition has a body, add it as a definition
          do b <- withTopTranslationState $ translateTermLet body
-            modify $ over topLevelDeclarations $ (mkDefinition renamed b :)
+            tp <- withTopTranslationState $ translateTermLet (ecType ec)
+            modify $ over topLevelDeclarations $ (mkDefinition renamed b tp :)
        Nothing ->
          -- If not, add it as a Coq Variable declaration
          do tp <- withTopTranslationState $ translateTermLet (ecType ec)
@@ -338,7 +340,8 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
                   [Coq.NatLit (intValue w), Coq.ZLit (BV.asSigned w bv)])
     ArrayValue _ vec -> do
       elems <- Vector.toList <$> mapM translateTerm vec
-      return (Coq.App (Coq.Var "Vector.of_list") [Coq.List elems])
+      -- NOTE: with VectorNotations, this is actually a Coq vector literal
+      return $ Coq.List elems
     StringLit s -> pure (Coq.Scope (Coq.StringLit (Text.unpack s)) "string")
 
     ExtCns ec -> translateConstant ec Nothing
@@ -425,9 +428,20 @@ withTopTranslationState m =
      modify $ set nextSharedName "var__0"
      m
 
-mkDefinition :: Coq.Ident -> Coq.Term -> Coq.Decl
-mkDefinition name (Coq.Lambda bs t) = Coq.Definition name bs Nothing t
-mkDefinition name t = Coq.Definition name [] Nothing t
+-- | Generate a Coq @Definition@ with a given name, body, and type, using the
+-- lambda-bound variable names for the variables if they are available
+mkDefinition :: Coq.Ident -> Coq.Term -> Coq.Term -> Coq.Decl
+mkDefinition name (Coq.Lambda bs t) (Coq.Pi bs' tp)
+  | length bs' == length bs =
+    -- NOTE: there are a number of cases where length bs /= length bs', such as
+    -- where the type of a definition is computed from some input (so might not
+    -- have any explicit pi-abstractions), or where the body of a definition is
+    -- a partially applied function (so might not have any lambdas). We could in
+    -- theory try to handle these more complex cases by assigning names to some
+    -- of the arguments, but it's not really necessary for the translation to be
+    -- correct, so we just do the simple thing here.
+    Coq.Definition name bs (Just tp) t
+mkDefinition name t tp = Coq.Definition name [] (Just tp) t
 
 -- | Make sure a name is not used in the current environment, adding
 -- or incrementing a numeric suffix until we find an unused name. When
@@ -661,31 +675,36 @@ defaultTermForType typ = do
 
     _ -> Except.throwError $ CannotCreateDefaultValue typ
 
+-- | Translate a SAW core term along with its type to a Coq term and its Coq
+-- type, and pass the results to the supplied function
 translateTermToDocWith ::
   TranslationConfiguration ->
   TranslationReader ->
-  [String] ->
-  [String] ->
-  (Coq.Term -> Doc ann) ->
-  Term ->
+  [String] -> -- ^ globals that have already been translated
+  [String] -> -- ^ string names of local variables in scope
+  (Coq.Term -> Coq.Term -> Doc ann) ->
+  Term -> Term ->
   Either (TranslationError Term) (Doc ann)
-translateTermToDocWith configuration r globalDecls localEnv f t = do
-  (term, state) <-
-    runTermTranslationMonad configuration r globalDecls localEnv (translateTermLet t)
+translateTermToDocWith configuration r globalDecls localEnv f t tp_trm = do
+  ((term, tp), state) <-
+    runTermTranslationMonad configuration r globalDecls localEnv
+    ((,) <$> translateTermLet t <*> translateTermLet tp_trm)
   let decls = view topLevelDeclarations state
   return $
     vcat $
     [ (vcat . intersperse hardline . map Coq.ppDecl . reverse) decls
     , if null decls then mempty else hardline
-    , f term
+    , f term tp
     ]
 
+-- | Translate a SAW core 'Term' and its type (given as a 'Term') to a Coq
+-- definition with the supplied name
 translateDefDoc ::
   TranslationConfiguration ->
   TranslationReader ->
   [String] ->
-  Coq.Ident -> Term ->
+  Coq.Ident -> Term -> Term ->
   Either (TranslationError Term) (Doc ann)
 translateDefDoc configuration r globalDecls name =
   translateTermToDocWith configuration r globalDecls [name]
-  (Coq.ppDecl . mkDefinition name)
+  (\ t tp -> Coq.ppDecl $ mkDefinition name t tp)

src/SAWScript/Prover/Exporter.hs

@@ -67,7 +67,8 @@ import Prettyprinter.Render.Text
 
 import Lang.JVM.ProcessUtils (readProcessExitIfFailure)
 
-import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule, ImportPrimitiveOptions(..))
+import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule,
+                                ImportPrimitiveOptions(..), mkCryEnv)
 import Verifier.SAW.Cryptol.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule)
 import Verifier.SAW.ExternalFormat(scWriteExternal)
 import Verifier.SAW.FiniteValue
@@ -455,7 +456,9 @@ writeCoqTerm name notations skips path t = do
         withImportCryptolPrimitivesForSAWCore $
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
-  case Coq.translateTermAsDeclImports configuration name t of
+  sc <- getSharedContext
+  tp <- io $ scTypeOf sc t
+  case Coq.translateTermAsDeclImports configuration name t tp of
     Left err -> throwTopLevel $ "Error translating: " ++ show err
     Right doc -> io $ case path of
       "" -> print doc
@@ -496,7 +499,9 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
   let nm = takeBaseName inputFile
-  case Coq.translateCryptolModule nm configuration cryptolPreludeDecls cm of
+  cry_env <- mkCryEnv env
+  res <- Coq.translateCryptolModule sc cry_env nm configuration cryptolPreludeDecls cm
+  case res of
     Left e -> putStrLn $ show e
     Right cmDoc ->
       writeFile outputFile