Coq prelude update

cryptol-saw-core/saw/Cryptol.sawcore

@@ -1533,7 +1533,7 @@ ecParmap a b n pb =
 ecFoldl : (n : Num) -> (a : sort 0) -> (b : sort 0) -> (a -> b -> a) -> a -> seq n b -> a;
 ecFoldl n a b f z =
   Num#rec (\ (n : Num) -> seq n b -> a)
-    (\ (n : Nat) -> \ (xs : Vec n b) -> foldr b a n (\ (y : b) -> \ (x : a) -> f x y) z (reverse n b xs))
+    (\ (n : Nat) -> \ (xs : Vec n b) -> foldl b a n f z xs)
     (\ (xs : Stream b) -> error a "Unexpected infinite stream in foldl" )
     n;
 

saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v

@@ -46,7 +46,7 @@ Ltac solveUnsafeAssertStep :=
   | [ |- min ?n (S ?n) = ?n ] => apply min_S
   end.
 
-Ltac solveUnsafeAssert := repeat (solveUnsafeAssertStep; simpl).
+Ltac solveUnsafeAssert := repeat (solveUnsafeAssertStep; simpl); trivial.
 
 Definition cbc_enc_helper n : Eq Num (tcMin n (tcAdd (TCNum 1) n)) n :=
   ltac:(solveUnsafeAssert).

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v

@@ -8,7 +8,7 @@ From CryptolToCoq Require Export CompM.
 
 Definition sort (n : nat) := Type.
 
-Axiom error : forall (a : Type), String.string -> a.
+Axiom error : forall {a : Type}, String.string -> a.
 
 Definition String := String.string.
 

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

@@ -108,6 +108,12 @@ Fixpoint foldr (a b : Type) (n : Nat) (f : a -> b -> b) (base : b) (v : Vec n a)
   | Vector.cons hd _ tl => f hd (foldr _ _ _ f base tl)
   end.
 
+Fixpoint foldl (a b : Type) (n : Nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : b :=
+  match v with
+  | Vector.nil => acc
+  | Vector.cons hd _ tl => foldl _ _ _ f (f acc hd) tl
+  end.
+
 Fixpoint foldl_dep (a : Type) (b : Nat -> Type) (n : Nat)
          (f : forall n, b n -> a -> b (S n)) (base : b O) (v : Vec n a) : b n :=
   match v with
@@ -125,9 +131,9 @@ Fixpoint tuple_foldl_dep (a : Type) (b : Nat -> Type) (n : Nat)
 
 Definition EmptyVec := Vector.nil.
 
-Definition coerceVec (a : sort 0) (m n : Nat) (eq : Eq Nat m n) (v : Vec m a) : Vec n a :=
+Definition coerceVec (a : sort 0) (m n : Nat) (H : Eq Nat m n) (v : Vec m a) : Vec n a :=
   match
-    eq_sym eq in eq _ n'
+    eq_sym H in eq _ n'
     return Vec n' a -> Vec n a
   with
   | eq_refl => fun x => x

saw-core-coq/saw-core-coq.cabal

@@ -27,7 +27,8 @@ library
     text,
     parameterized-utils,
     bv-sized,
-    vector
+    vector,
+    zenc
   hs-source-dirs: src
   exposed-modules:
      Language.Coq.AST

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

@@ -26,10 +26,12 @@ module Verifier.SAW.Translation.Coq.SpecialTreatment where
 
 import           Control.Lens                       (_1, _2, over)
 import           Control.Monad.Reader               (asks)
+import           Data.Char                          (isAlphaNum)
 import qualified Data.Map                           as Map
 import           Data.String.Interpolate            (i)
 import qualified Data.Text                          as Text
 import           Prelude                            hiding (fail)
+import           Text.Encoding.Z                    (zEncodeString)
 
 import qualified Language.Coq.AST                   as Coq
 import           Verifier.SAW.SharedTerm
@@ -316,6 +318,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("coerceVec",     mapsTo vectorsModule "coerceVec")
   , ("eq_Vec",        skip)
   , ("foldr",         mapsTo vectorsModule "foldr")
+  , ("foldl",         mapsTo vectorsModule "foldl")
   , ("gen",           mapsTo vectorsModule "gen")
   , ("rotateL",       mapsTo vectorsModule "rotateL")
   , ("rotateR",       mapsTo vectorsModule "rotateR")
@@ -446,14 +449,22 @@ sawCorePreludeSpecialTreatmentMap configuration =
 constantsRenamingMap :: [(String, String)] -> Map.Map String String
 constantsRenamingMap notations = Map.fromList notations
 
+escapeIdent :: String -> String
+escapeIdent str
+  | all okChar str = str
+  | otherwise      = "Op_" ++ zEncodeString str
+ where
+   okChar x = isAlphaNum x || x `elem` ("_'" :: String)
+
 -- TODO: Now that ExtCns contains a unique identifier, it might make sense
 -- to check those here to avoid some captures?
 translateConstant :: [(String, String)] -> ExtCns e -> String
 translateConstant notations (EC {..}) =
-  Map.findWithDefault
-    (Text.unpack (toShortName ecName))
-    (Text.unpack (toShortName ecName))
-    (constantsRenamingMap notations) -- TODO short name doesn't seem right
+  escapeIdent $
+    Map.findWithDefault
+      (Text.unpack (toShortName ecName))
+      (Text.unpack (toShortName ecName))
+      (constantsRenamingMap notations) -- TODO short name doesn't seem right
 
 zipSnippet :: String
 zipSnippet = [i|

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

@@ -170,10 +170,10 @@ translateIdentWithArgs i args = do
   currentModuleName <- asks (view currentModule . otherConfiguration)
   let identToCoq ident =
         if Just (identModule ident) == currentModuleName
-          then identName ident
+          then escapeIdent (identName ident)
           else
             show (translateModuleName (identModule ident))
-            ++ "." ++ identName ident
+            ++ "." ++ escapeIdent (identName ident)
   specialTreatment <- findSpecialTreatment i
   applySpecialTreatment identToCoq (atUseSite specialTreatment)
 
@@ -404,8 +404,7 @@ translatePi binders body = withLocalTranslationState $ do
 
 -- | Translate a local name from a saw-core binder into a fresh Coq identifier.
 translateLocalIdent :: TermTranslationMonad m => LocalName -> m Coq.Ident
-translateLocalIdent x = freshVariant ident0
-  where ident0 = Text.unpack x -- TODO: use some string encoding to ensure lexically valid Coq identifiers
+translateLocalIdent x = freshVariant (escapeIdent (Text.unpack x))
 
 -- | Find an fresh, as-yet-unused variant of the given Coq identifier.
 freshVariant :: TermTranslationMonad m => Coq.Ident -> m Coq.Ident

saw-core/prelude/Prelude.sawcore

@@ -951,6 +951,7 @@ axiom at_single : (a : sort 0) -> (x : a) -> (i : Nat) -> Eq a (at 1 a (single a
 primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
 
 primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -> b;
+primitive foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
 
 reverse : (n : Nat) -> (a : sort 0) -> Vec n a -> Vec n a;
 reverse n a xs = gen n a (\ (i : Nat) -> at n a xs (subNat (subNat n 1) i));

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -353,6 +353,7 @@ constMap bp = Map.fromList
   , ("Prelude.split", splitOp bp)
   , ("Prelude.zip", vZipOp (bpUnpack bp))
   , ("Prelude.foldr", foldrOp (bpUnpack bp))
+  , ("Prelude.foldl", foldlOp (bpUnpack bp))
   , ("Prelude.rotateL", rotateLOp bp)
   , ("Prelude.rotateR", rotateROp bp)
   , ("Prelude.shiftL", shiftLOp bp)
@@ -1058,6 +1059,21 @@ foldrOp unpack =
     xv <- toVector unpack xs
     lift (V.foldr g (force z) xv)
 
+-- foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
+foldlOp :: (VMonadLazy l, Show (Extra l)) => Unpack l -> Prim l
+foldlOp unpack =
+  constFun $
+  constFun $
+  constFun $
+  strictFun $ \f ->
+  primFun $ \z ->
+  strictFun $ \xs ->
+  PrimExcept $ do
+    let g m x = do f1 <- apply f =<< delay m
+                   apply f1 x
+    xv <- toVector unpack xs
+    lift (V.foldl g (force z) xv)
+
 -- op :: Integer -> Integer;
 intUnOp :: VMonad l => (VInt l -> MInt l) -> Prim l
 intUnOp f =

src/SAWScript/Prover/Exporter.hs

@@ -418,6 +418,16 @@ withImportCryptolPrimitivesForSAWCore config@(Coq.TranslationConfiguration { Coq
    ]
   }
 
+
+withImportCryptolPrimitivesForSAWCoreExtra ::
+  Coq.TranslationConfiguration  -> Coq.TranslationConfiguration
+withImportCryptolPrimitivesForSAWCoreExtra config@(Coq.TranslationConfiguration { Coq.postPreamble }) =
+  config { Coq.postPreamble = postPreamble ++ unlines
+   [ "From CryptolToCoq Require Import CryptolPrimitivesForSAWCoreExtra."
+   ]
+  }
+
+
 writeCoqTerm ::
   String ->
   [(String, String)] ->
@@ -427,8 +437,8 @@ writeCoqTerm ::
   TopLevel ()
 writeCoqTerm name notations skips path t = do
   let configuration =
-        withImportSAWCorePrelude $
         withImportCryptolPrimitivesForSAWCore $
+        withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
   case Coq.translateTermAsDeclImports configuration name t of
     Left err -> throwTopLevel $ "Error translating: " ++ show err
@@ -464,22 +474,15 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
   (cm, _) <- loadCryptolModule sc env inputFile
   let cryptolPreludeDecls = map Coq.moduleDeclName (moduleDecls cryptolPrimitivesForSAWCoreModule)
   let configuration =
-        withImportSAWCorePrelude $
+        withImportCryptolPrimitivesForSAWCoreExtra $
         withImportCryptolPrimitivesForSAWCore $
+        withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
   case Coq.translateCryptolModule configuration cryptolPreludeDecls cm of
     Left e -> putStrLn $ show e
     Right cmDoc ->
       writeFile outputFile
-      (show . vcat $ [ Coq.preamble configuration
-                     , "From CryptolToCoq Require Import SAWCorePrelude."
-                     , "Import SAWCorePrelude."
-                     , "From CryptolToCoq Require Import CryptolPrimitivesForSAWCore."
-                     , "Import CryptolPrimitives."
-                     , "From CryptolToCoq Require Import CryptolPrimitivesForSAWCoreExtra."
-                     , ""
-                     , cmDoc
-                     ])
+      (show . vcat $ [ Coq.preamble configuration, cmDoc])
 
 nameOfSAWCorePrelude :: Un.ModuleName
 nameOfSAWCorePrelude = Un.moduleName preludeModule