From dec2ef3f905ba59b1fbe5a1784dc42b94be102f7 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Mon, 20 Feb 2023 16:24:29 -0500
Subject: [PATCH 01/19] first attempt at write_coq_cryptol_module_monadic

---
 .../src/Verifier/SAW/Cryptol/Monadify.hs      | 62 ++++++++++++++-----
 examples/mr_solver/monadify_module.saw        |  3 +
 src/SAWScript/Interpreter.hs                  | 16 ++++-
 src/SAWScript/Prover/Exporter.hs              |  9 ++-
 4 files changed, 71 insertions(+), 19 deletions(-)
 create mode 100644 examples/mr_solver/monadify_module.saw

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index d1633e4111..adef08240f 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -90,6 +90,8 @@ import Verifier.SAW.Name
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.OpenTerm
+import Verifier.SAW.TypedTerm
+import Verifier.SAW.Cryptol (Env)
 -- import Verifier.SAW.SCTypeCheck
 import Verifier.SAW.Recognizer
 -- import Verifier.SAW.Position
@@ -1487,12 +1489,12 @@ monadifyName (ImportedName uri _) =
   do frag <- URI.mkFragment (T.pack "M")
      return $ ImportedName (uri { URI.uriFragment = Just frag }) []
 
--- | Monadify a 'Term' of the specified type with an optional body, bind the
--- result to a fresh SAW core constant generated from the supplied name, and
--- then convert that constant back to a 'MonTerm'
-monadifyNamedTerm :: SharedContext -> MonadifyEnv ->
-                     NameInfo -> Maybe Term -> Term -> IO MonTerm
-monadifyNamedTerm sc env nmi maybe_trm tp =
+-- | Monadify a 'Term' of the specified type with an optional body and bind the
+-- result to a fresh SAW core constant generated from the supplied name
+monadifyNamedTermH :: SharedContext -> MonadifyEnv ->
+                      NameInfo -> Maybe Term -> Term ->
+                      IO (MonType, Term)
+monadifyNamedTermH sc env nmi maybe_trm tp =
   trace ("Monadifying " ++ T.unpack (toAbsoluteName nmi)) $
   let ?specMParams = monEnvParams env in
   do let mtp = monadifyType [] tp
@@ -1504,15 +1506,23 @@ monadifyNamedTerm sc env nmi maybe_trm tp =
            do trm' <- monadifyCompleteTerm sc env trm tp
               scConstant' sc nmi' trm' comp_tp
          Nothing -> scOpaqueConstant sc nmi' tp
+     return (mtp, const_trm)
+
+-- | Monadify a 'Term' of the specified type with an optional body, bind the
+-- result to a fresh SAW core constant generated from the supplied name, and
+-- then convert that constant back to a 'MonTerm'
+monadifyNamedTerm :: SharedContext -> MonadifyEnv ->
+                     NameInfo -> Maybe Term -> Term -> IO MonTerm
+monadifyNamedTerm sc env nmi maybe_trm tp =
+  let ?specMParams = monEnvParams env in
+  do (mtp, const_trm) <- monadifyNamedTermH sc env nmi maybe_trm tp
      return $ fromCompTerm mtp $ closedOpenTerm const_trm
 
--- | Monadify a term with the specified type along with all constants it
--- contains, adding the monadifications of those constants to the monadification
--- environment
-monadifyTermInEnv :: SharedContext -> MonadifyEnv ->
-                     Term -> Term -> IO (Term, MonadifyEnv)
-monadifyTermInEnv sc top_env top_trm top_tp =
-  flip runStateT top_env $
+-- | Monadify all the constants contained in the given term, adding the
+-- monadifications of those constants to the monadification environment
+monadifyContainedConstants :: SharedContext -> MonadifyEnv -> Term -> IO MonadifyEnv
+monadifyContainedConstants sc top_env top_trm =
+  flip execStateT top_env $
   do lift $ ensureCryptolMLoaded sc
      let const_infos =
            map snd $ Map.toAscList $ getConstantSet top_trm
@@ -1521,5 +1531,27 @@ monadifyTermInEnv sc top_env top_trm top_tp =
        if Map.member nmi (monEnvMonTable env) then return () else
          do mtrm <- lift $ monadifyNamedTerm sc env nmi maybe_body tp
             modify $ monEnvAdd nmi (monMacro0 mtrm)
-     env <- get
-     lift $ monadifyCompleteTerm sc env top_trm top_tp
+
+-- | Monadify a term with the specified type along with all constants it
+-- contains, adding the monadifications of those constants to the monadification
+-- environment
+monadifyTermInEnv :: SharedContext -> MonadifyEnv ->
+                     Term -> Term -> IO (Term, MonadifyEnv)
+monadifyTermInEnv sc top_env top_trm top_tp =
+  do env <- monadifyContainedConstants sc top_env top_trm
+     tm <- monadifyCompleteTerm sc env top_trm top_tp
+     return (tm, env)
+
+-- | Monadify each term in the given 'CryptolModule' along with all constants each
+-- contains, returning a new module which each term monadified, and adding the
+-- monadifications of all encountered constants to the monadification environment
+monadifyCryptolModule :: SharedContext -> Env -> MonadifyEnv ->
+                         CryptolModule -> IO (CryptolModule, MonadifyEnv)
+monadifyCryptolModule sc cry_env top_env (CryptolModule tysyns top_tts) =
+  flip runStateT top_env $
+  fmap (CryptolModule tysyns) $ flip mapM top_tts $ \top_tt -> StateT $ \env ->
+    do let top_tm = ttTerm top_tt
+       top_tp <- ttTypeAsTerm sc cry_env top_tt
+       (tm, env') <- monadifyTermInEnv sc env top_tm top_tp
+       tm' <- mkTypedTerm sc tm
+       return (tm', env')
diff --git a/examples/mr_solver/monadify_module.saw b/examples/mr_solver/monadify_module.saw
new file mode 100644
index 0000000000..dcf3192acc
--- /dev/null
+++ b/examples/mr_solver/monadify_module.saw
@@ -0,0 +1,3 @@
+enable_experimental;
+// write_coq_cryptol_module "monadify.cry" "monadify_gen.v" [] ["fib"];
+write_coq_cryptol_module_monadic "monadify.cry" "monadify_gen_m.v" [] [];
\ No newline at end of file
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index f2e4a8bd73..6a47d3c754 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1468,7 +1468,7 @@ primitives = Map.fromList
     ]
 
   , prim "write_coq_cryptol_module" "String -> String -> [(String, String)] -> [String] -> TopLevel ()"
-    (pureVal writeCoqCryptolModule)
+    (pureVal (writeCoqCryptolModule False))
     Experimental
     [ "Write out a representation of a Cryptol module in Gallina syntax for"
     , "Coq."
@@ -1481,6 +1481,20 @@ primitives = Map.fromList
     , "The fourth argument is a list of identifiers to skip translating."
     ]
 
+  , prim "write_coq_cryptol_module_monadic" "String -> String -> [(String, String)] -> [String] -> TopLevel ()"
+    (pureVal (writeCoqCryptolModule True))
+    Experimental
+    [ "Write out a representation of a Cryptol module in Gallina syntax for"
+    , "Coq, using the monadified version of the given module."
+    , "The first argument is the file containing the module to export."
+    , "The second argument is the name of the file to output into,"
+    , "use an empty string to output to standard output."
+    , "The third argument is a list of pairs of notation substitutions:"
+    , "the operator on the left will be replaced with the identifier on"
+    , "the right, as we do not support notations on the Coq side."
+    , "The fourth argument is a list of identifiers to skip translating."
+    ]
+
   , prim "write_coq_sawcore_prelude" "String -> [(String, String)] -> [String] -> TopLevel ()"
     (pureVal writeCoqSAWCorePrelude)
     Experimental
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 2ade25044e..04600c3239 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -70,6 +70,7 @@ import Lang.JVM.ProcessUtils (readProcessExitIfFailure)
 import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule,
                                 ImportPrimitiveOptions(..), mkCryEnv)
 import Verifier.SAW.Cryptol.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule)
+import Verifier.SAW.Cryptol.Monadify (defaultMonEnv, monadifyCryptolModule)
 import Verifier.SAW.ExternalFormat(scWriteExternal)
 import Verifier.SAW.FiniteValue
 import Verifier.SAW.Module (emptyModule, moduleDecls)
@@ -477,12 +478,13 @@ writeCoqProp name notations skips path t =
      writeCoqTerm name notations skips path tm
 
 writeCoqCryptolModule ::
+  Bool ->
   FilePath ->
   FilePath ->
   [(String, String)] ->
   [String] ->
   TopLevel ()
-writeCoqCryptolModule inputFile outputFile notations skips = io $ do
+writeCoqCryptolModule mon inputFile outputFile notations skips = io $ do
   sc  <- mkSharedContext
   ()  <- scLoadPreludeModule sc
   ()  <- scLoadCryptolModule sc
@@ -491,6 +493,8 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
   cryptolPrimitivesForSAWCoreModule <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule
   let primOpts = ImportPrimitiveOptions{ allowUnknownPrimitives = True }
   (cm, _) <- loadCryptolModule sc primOpts env inputFile
+  cry_env <- mkCryEnv env
+  cm' <- if mon then fst <$> monadifyCryptolModule sc cry_env defaultMonEnv cm else return cm
   let cryptolPreludeDecls = mapMaybe Coq.moduleDeclName (moduleDecls cryptolPrimitivesForSAWCoreModule)
   let configuration =
         withImportCryptolPrimitivesForSAWCoreExtra $
@@ -499,8 +503,7 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
   let nm = takeBaseName inputFile
-  cry_env <- mkCryEnv env
-  res <- Coq.translateCryptolModule sc cry_env nm configuration cryptolPreludeDecls cm
+  res <- Coq.translateCryptolModule sc cry_env nm configuration cryptolPreludeDecls cm'
   case res of
     Left e -> putStrLn $ show e
     Right cmDoc ->

From 66d972b64c8ca0b94c13bb0520edfe1ce3910bd2 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Mon, 20 Feb 2023 18:30:46 -0500
Subject: [PATCH 02/19] include aliases in `monadifyName`, handle `#` char in
 `escapeIdent`

---
 cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs        | 5 +++--
 .../src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs     | 5 +++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index adef08240f..403a91d0a4 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1485,9 +1485,10 @@ monadifyName :: NameInfo -> IO NameInfo
 monadifyName (ModuleIdentifier ident) =
   return $ ModuleIdentifier $ mkIdent (identModule ident) $
   T.append (identBaseName ident) (T.pack "M")
-monadifyName (ImportedName uri _) =
+monadifyName (ImportedName uri aliases) =
   do frag <- URI.mkFragment (T.pack "M")
-     return $ ImportedName (uri { URI.uriFragment = Just frag }) []
+     let aliases' = concatMap (\a -> [a, T.append a (T.pack "#M")]) aliases
+     return $ ImportedName (uri { URI.uriFragment = Just frag }) aliases'
 
 -- | Monadify a 'Term' of the specified type with an optional body and bind the
 -- result to a fresh SAW core constant generated from the supplied name
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
index 435beea5fa..bf14ea5a57 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -589,9 +589,10 @@ sawCorePreludeSpecialTreatmentMap configuration =
 
 escapeIdent :: String -> String
 escapeIdent str
-  | all okChar str = str
-  | otherwise      = "Op_" ++ zEncodeString str
+  | all okChar strR = strR
+  | otherwise       = "Op_" ++ zEncodeString str
  where
+   strR = map (\c -> if c `elem` ("#" :: String) then '_' else c) str
    okChar x = isAlphaNum x || x `elem` ("_'" :: String)
 
 zipSnippet :: String

From 15451fe0f3c285098f7c4bac00e2e894e620ed65 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 2 Mar 2023 13:14:01 -0500
Subject: [PATCH 03/19] add seqZipM, monadify uncurry, recursively monadify
 contained constants

---
 cryptol-saw-core/saw/CryptolM.sawcore         | 107 +++++++++++-------
 .../src/Verifier/SAW/Cryptol/Monadify.hs      | 102 +++++++++++------
 saw-core/prelude/Prelude.sawcore              |  17 ++-
 3 files changed, 149 insertions(+), 77 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index 2e2ac7846f..19a369660e 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -6,6 +6,12 @@ module CryptolM where
 -- import Prelude;
 import Cryptol;
 
+-- Alternate versions of gen and at to get around the behavior of the default prims
+genCryM : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;
+genCryM = gen;
+atCryM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a;
+atCryM = at;
+
 
 --------------------------------------------------------------------------------
 -- Monadic assertions
@@ -116,43 +122,41 @@ bvVecMapM : (E:EvType) -> (stack:FunStack) ->
             (a -> SpecM E stack b) -> BVVec n len a ->
             SpecM E stack (BVVec n len b);
 bvVecMapM E stack a b n len f xs = bvVecMapInvarM E stack a b n len f xs True;
+-}
 
 vecMapInvarBindM : (E:EvType) -> (stack:FunStack) ->
-                   (a b c : isort 0) -> (n : Nat) -> (a -> SpecM E stack b) ->
+                   (a b c : isort 0) -> (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
                    Vec n a -> Bool -> (Vec n b -> SpecM E stack c) ->
                    SpecM E stack c;
 vecMapInvarBindM E stack a b c n f xs invar cont =
-  existsM (Vec n b) c (\ (ys0:Vec n b) ->
-    multiArgFixM
-      (LRT_Fun Nat (\ (_:Nat) ->
-       LRT_Fun (Vec n b) (\ (_:Vec n b) ->
-       LRT_Ret c)))
-      (\ (rec : Nat -> Vec n b -> SpecM E stack c) (i:Nat) (ys:Vec n b) ->
-         invariantHint (SpecM E stack c) (and (ltNat i (Succ n)) invar)
-           (maybe (IsLtNat i n) (SpecM E stack c)
-                  (cont ys)
+  bindS E stack (Vec n b) c
+    (existsS E stack (Vec n b)) (\ (ys0:Vec n b) ->
+    multiArgFixS E stack
+      (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))
+      (\ (rec : Nat -> Vec n b -> SpecM E (pushFunStack (singletonFrame (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))) stack) c)
+         (i:Nat) (ys:Vec n b) ->
+         invariantHint (SpecM E (pushFunStack (singletonFrame (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))) stack) c) (and (ltNat i (Succ n)) invar)
+           (maybe (IsLtNat i n) (SpecM E (pushFunStack (singletonFrame (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))) stack) c)
+                  (pushStackS E (singletonFrame (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))) stack c
+                              (cont ys))
                   (\ (pf:IsLtNat i n) ->
-                     bindS E stack b c
-                           (f (atWithProof n a xs i pf))
+                     bindS E (pushFunStack (singletonFrame (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))) stack) b c
+                           (pushStackS E (singletonFrame (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c)))) stack b
+                                       (f i (atWithProof n a xs i pf)))
                            (\ (y:b) -> rec (Succ i)
                                            (updWithProof n b ys i y pf)))
                   (proveLtNat i n)))
       0 ys0);
 
 vecMapInvarM : (E:EvType) -> (stack:FunStack) ->
-               (a b : isort 0) -> (n : Nat) -> (a -> SpecM E stack b) ->
+               (a b : isort 0) -> (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
                Vec n a -> Bool -> SpecM E stack (Vec n b);
 vecMapInvarM E stack a b n f xs invar =
   vecMapInvarBindM E stack a b (Vec n b) n f xs invar (retS E stack (Vec n b));
 
 vecMapM : (E:EvType) -> (stack:FunStack) -> (a b : isort 0) -> (n : Nat) ->
-          (a -> SpecM E stack b) -> Vec n a -> SpecM E stack (Vec n b);
+          (Nat -> a -> SpecM E stack b) -> Vec n a -> SpecM E stack (Vec n b);
 vecMapM E stack a b n f xs = vecMapInvarM E stack a b n f xs True;
--}
-
-primitive
-vecMapM : (E:EvType) -> (stack:FunStack) -> (a b : isort 0) -> (n : Nat) ->
-          (a -> SpecM E stack b) -> Vec n a -> SpecM E stack (Vec n b);
 
 -- Computational version of seqMap
 seqMapM : (E:EvType) -> (stack:FunStack) ->
@@ -160,7 +164,7 @@ seqMapM : (E:EvType) -> (stack:FunStack) ->
           mseq E stack n a -> SpecM E stack (mseq E stack n b);
 seqMapM E stack a b n_top f =
   Num_rec (\ (n:Num) -> mseq E stack n a -> SpecM E stack (mseq E stack n b))
-          (\ (n:Nat) -> vecMapM E stack a b n f)
+          (\ (n:Nat) -> vecMapM E stack a b n (\(i:Nat) -> f))
           (\ (s:Stream (SpecM E stack a)) ->
              retS E stack (Stream (SpecM E stack b))
                   (streamMap (SpecM E stack a) (SpecM E stack b)
@@ -261,19 +265,50 @@ mletM : (E:EvType) -> (stack:FunStack) ->
         (a -> SpecM E stack (mseq E stack n b)) ->
         SpecM E stack (mseq E stack n (a * b));
 
--- FIXME
-primitive
+-- An alternate version of zip from Prelude to get around the default Prim
+zipCryM : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
+zipCryM a b m n xs ys =
+  genCryM (minNat m n) (a * b) (\ (i:Nat) -> (atCryM m a xs i, atCryM n b ys i));
+
 seqZipM : (E:EvType) -> (stack:FunStack) ->
-          (a b : sort 0) -> (m n : Num) -> mseq E stack m a ->
-          mseq E stack n b -> SpecM E stack (mseq E stack (tcMin m n) (a * b));
-{-
-seqZipM a b m n ms1 ms2 =
-  seqMap
-    (CompM a * CompM b) (CompM (a * b)) (tcMin m n)
-    (\ (p : CompM a * CompM b) ->
-       bindM2 a b (a*b) p.(1) p.(2) (\ (x:a) (y:b) -> returnM (a*b) (x,y)))
-    (seqZip (CompM a) (CompM b) m n ms1 ms2);
--}
+          (a b : sort 0) -> (m n : Num) ->
+          mseq E stack m a -> mseq E stack n b ->
+          SpecM E stack (mseq E stack (tcMin m n) (a * b));
+seqZipM E stack a b m n =
+  Num_rec
+    (\ (m:Num) -> mseq E stack m a -> mseq E stack n b
+               -> SpecM E stack (mseq E stack (tcMin m n) (a * b)))
+    (\ (m : Nat) ->
+       Num_rec
+         (\ (n:Num) -> Vec m a -> mseq E stack n b
+                    -> SpecM E stack (mseq E stack (tcMin (TCNum m) n) (a * b)))
+         (\ (n:Nat) ->
+          \ (xs:Vec m a) -> \ (ys:Vec n b) ->
+            retS E stack (Vec (minNat m n) (a * b)) (zipCryM a b m n xs ys))
+         (\ (xs:Vec m a) -> \ (ys:Stream (SpecM E stack b)) ->
+            vecMapM E stack a (a * b) m
+              (\ (i : Nat) (x : a) ->
+                fmapS E stack b (a * b) (\ (y : b) -> (x,y))
+                  (streamGet (SpecM E stack b) ys i))
+              xs)
+         n)
+    (Num_rec
+       (\ (n:Num) -> Stream (SpecM E stack a) -> mseq E stack n b
+                  -> SpecM E stack (mseq E stack (tcMin TCInf n) (a * b)))
+       (\ (n:Nat) ->
+        \ (xs:Stream (SpecM E stack a)) -> \ (ys:Vec n b) ->
+          vecMapM E stack b (a * b) n
+            (\ (i : Nat) (y : b) ->
+              fmapS E stack a (a * b) (\ (x : a) -> (x,y))
+                (streamGet (SpecM E stack a) xs i))
+            ys)
+       (\ (xs:Stream (SpecM E stack a)) -> \ (ys:Stream (SpecM E stack b)) ->
+          retS E stack (Stream (SpecM E stack (a * b)))
+            (streamMap2 (SpecM E stack a) (SpecM E stack b) (SpecM E stack (a * b))
+               (fmapS2 E stack a b (a * b) (\ (x:a) -> \ (y:b) -> (x, y)))
+               xs ys))
+       n)
+    m;
 
 
 --------------------------------------------------------------------------------
@@ -402,12 +437,6 @@ PLiteralSeqBoolM E stack =
 
 -- Sequences
 
--- Alternate versions of gen and at to get around the behavior of the default prims
-genCryM : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;
-genCryM = gen;
-atCryM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a;
-atCryM = at;
-
 -- FIXME: a number of the non-monadic versions of these functions contain calls
 -- to finNumRec, which calls error on non-finite numbers. The monadic versions
 -- of these, below, should be reimplemented to not contain finNumRec, but to
@@ -573,7 +602,7 @@ ecSplitM E stack =
                streamMap (Vec (Succ n') (SpecM E stack a))
                          (SpecM E stack (Vec (Succ n') a))
                          (vecMapM E stack (SpecM E stack a) a (Succ n')
-                                  (id (SpecM E stack a)))
+                                  (\(i:Nat) (x:SpecM E stack a) -> x))
                          (streamSplit (SpecM E stack a) (Succ n') xs))
             n));
        -- No case for (TCInf, TCInf), shouldn't happen
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index 403a91d0a4..487c3dc15d 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1230,6 +1230,25 @@ eitherMacro = MonMacro 3 $ \_ args ->
                             (MTyArrow (MTyArrow mtp_b mtp_c)
                              (MTyArrow (mkMonType0 tp_eith) mtp_c))) eith_app
 
+-- | The macro for uncurry, which converts the application @uncurry a b c@
+-- to @uncurry a b (CompM c)@
+uncurryMacro :: MonMacro
+uncurryMacro = MonMacro 3 $ \_ args ->
+  usingSpecMParams $
+  do let (tp_a, tp_b, tp_c) =
+           case args of
+             [t1, t2, t3] -> (t1, t2, t3)
+             _ -> error "uncurryMacro: wrong number of arguments!"
+     mtp_a <- monadifyTypeM tp_a
+     mtp_b <- monadifyTypeM tp_b
+     mtp_c <- monadifyTypeM tp_c
+     let unc_app = applyGlobalOpenTerm "Prelude.uncurry" [toArgType mtp_a,
+                                                          toArgType mtp_b,
+                                                          toCompType mtp_c]
+     let tp_tup = pairTypeOpenTerm (toArgType mtp_a) (toArgType mtp_b)
+     return $ fromCompTerm (MTyArrow (MTyArrow mtp_a (MTyArrow mtp_b mtp_c))
+                            (MTyArrow (mkMonType0 tp_tup) mtp_c)) unc_app
+
 -- | The macro for invariantHint, which converts @invariantHint a cond m@
 -- to @invariantHint (CompM a) cond m@ and which contains any binds in the body
 -- to the body
@@ -1357,6 +1376,7 @@ defaultMonTable =
   , mmCustom "Prelude.ite" iteMacro
   , mmCustom "Prelude.fix" fixMacro
   , mmCustom "Prelude.either" eitherMacro
+  , mmCustom "Prelude.uncurry" uncurryMacro
   , mmCustom "Prelude.invariantHint" invariantHintMacro
   , mmCustom "Prelude.asserting" (assertingOrAssumingMacro True)
   , mmCustom "Prelude.assuming" (assertingOrAssumingMacro False)
@@ -1368,6 +1388,7 @@ defaultMonTable =
 
     -- List comprehensions
   , mmArg "Cryptol.from" "CryptolM.fromM" True
+  , mmArg "Cryptol.seqZip" "CryptolM.seqZipM" True
     -- FIXME: continue here...
 
     -- PEq constraints
@@ -1490,48 +1511,54 @@ monadifyName (ImportedName uri aliases) =
      let aliases' = concatMap (\a -> [a, T.append a (T.pack "#M")]) aliases
      return $ ImportedName (uri { URI.uriFragment = Just frag }) aliases'
 
--- | Monadify a 'Term' of the specified type with an optional body and bind the
--- result to a fresh SAW core constant generated from the supplied name
-monadifyNamedTermH :: SharedContext -> MonadifyEnv ->
-                      NameInfo -> Maybe Term -> Term ->
-                      IO (MonType, Term)
-monadifyNamedTermH sc env nmi maybe_trm tp =
+-- | The implementation of 'monadifyNamedTerm' in the @StateT MonadifyEnv IO@ monad
+monadifyNamedTermH :: SharedContext -> NameInfo -> Maybe Term -> Term ->
+                      StateT MonadifyEnv IO MonTerm
+monadifyNamedTermH sc nmi maybe_trm tp =
   trace ("Monadifying " ++ T.unpack (toAbsoluteName nmi)) $
-  let ?specMParams = monEnvParams env in
+  get >>= \env -> let ?specMParams = monEnvParams env in
   do let mtp = monadifyType [] tp
-     nmi' <- monadifyName nmi
-     comp_tp <- completeOpenTerm sc $ toCompType mtp
+     nmi' <- lift $ monadifyName nmi
+     comp_tp <- lift $ completeOpenTerm sc $ toCompType mtp
      const_trm <-
        case maybe_trm of
          Just trm ->
-           do trm' <- monadifyCompleteTerm sc env trm tp
-              scConstant' sc nmi' trm' comp_tp
-         Nothing -> scOpaqueConstant sc nmi' tp
-     return (mtp, const_trm)
+          --  trace ("" ++ ppTermInMonCtx env trm ++ "\n\n") $
+           do trm' <- monadifyTermInEnvH sc trm tp
+              lift $ scConstant' sc nmi' trm' comp_tp
+         Nothing -> lift $ scOpaqueConstant sc nmi' tp
+     return $ fromCompTerm mtp $ closedOpenTerm const_trm
 
 -- | Monadify a 'Term' of the specified type with an optional body, bind the
 -- result to a fresh SAW core constant generated from the supplied name, and
--- then convert that constant back to a 'MonTerm'
+-- then convert that constant back to a 'MonTerm'. Like 'monadifyTermInEnv',
+-- this function also monadifies all constants the body contains, and adds
+-- the monadifications of those constants to the monadification environment.
 monadifyNamedTerm :: SharedContext -> MonadifyEnv ->
-                     NameInfo -> Maybe Term -> Term -> IO MonTerm
+                     NameInfo -> Maybe Term -> Term ->
+                     IO (MonTerm, MonadifyEnv)
 monadifyNamedTerm sc env nmi maybe_trm tp =
-  let ?specMParams = monEnvParams env in
-  do (mtp, const_trm) <- monadifyNamedTermH sc env nmi maybe_trm tp
-     return $ fromCompTerm mtp $ closedOpenTerm const_trm
+  flip runStateT env $ monadifyNamedTermH sc nmi maybe_trm tp
 
--- | Monadify all the constants contained in the given term, adding the
--- monadifications of those constants to the monadification environment
-monadifyContainedConstants :: SharedContext -> MonadifyEnv -> Term -> IO MonadifyEnv
-monadifyContainedConstants sc top_env top_trm =
-  flip execStateT top_env $
+-- | The implementation of 'monadifyTermInEnv' in the @StateT MonadifyEnv IO@ monad
+monadifyTermInEnvH :: SharedContext -> Term -> Term ->
+                      StateT MonadifyEnv IO Term
+monadifyTermInEnvH sc top_trm top_tp =
   do lift $ ensureCryptolMLoaded sc
      let const_infos =
            map snd $ Map.toAscList $ getConstantSet top_trm
      forM_ const_infos $ \(nmi,tp,maybe_body) ->
        get >>= \env ->
-       if Map.member nmi (monEnvMonTable env) then return () else
-         do mtrm <- lift $ monadifyNamedTerm sc env nmi maybe_body tp
+       if isPreludeName nmi ||
+          Map.member nmi (monEnvMonTable env) then return () else
+         do mtrm <- monadifyNamedTermH sc nmi maybe_body tp
             modify $ monEnvAdd nmi (monMacro0 mtrm)
+     env <- get
+     lift $ monadifyCompleteTerm sc env top_trm top_tp
+  where preludeModules = mkModuleName <$> [["Prelude"], ["Cryptol"]]
+        isPreludeName = \case
+          ModuleIdentifier ident -> identModule ident `elem` preludeModules
+          _ -> False
 
 -- | Monadify a term with the specified type along with all constants it
 -- contains, adding the monadifications of those constants to the monadification
@@ -1539,20 +1566,23 @@ monadifyContainedConstants sc top_env top_trm =
 monadifyTermInEnv :: SharedContext -> MonadifyEnv ->
                      Term -> Term -> IO (Term, MonadifyEnv)
 monadifyTermInEnv sc top_env top_trm top_tp =
-  do env <- monadifyContainedConstants sc top_env top_trm
-     tm <- monadifyCompleteTerm sc env top_trm top_tp
-     return (tm, env)
+  flip runStateT top_env $ monadifyTermInEnvH sc top_trm top_tp
+
+-- | The implementation of 'monadifyCryptolModule' in the @StateT MonadifyEnv IO@ monad
+monadifyCryptolModuleH :: SharedContext -> Env -> CryptolModule ->
+                          StateT MonadifyEnv IO CryptolModule
+monadifyCryptolModuleH sc cry_env (CryptolModule tysyns top_tts) =
+  fmap (CryptolModule tysyns) $ flip mapM top_tts $ \top_tt ->
+    do let top_tm = ttTerm top_tt
+       top_tp <- lift $ ttTypeAsTerm sc cry_env top_tt
+       tm <- monadifyTermInEnvH sc top_tm top_tp
+       tm' <- lift $ mkTypedTerm sc tm
+       return tm'
 
 -- | Monadify each term in the given 'CryptolModule' along with all constants each
 -- contains, returning a new module which each term monadified, and adding the
 -- monadifications of all encountered constants to the monadification environment
 monadifyCryptolModule :: SharedContext -> Env -> MonadifyEnv ->
                          CryptolModule -> IO (CryptolModule, MonadifyEnv)
-monadifyCryptolModule sc cry_env top_env (CryptolModule tysyns top_tts) =
-  flip runStateT top_env $
-  fmap (CryptolModule tysyns) $ flip mapM top_tts $ \top_tt -> StateT $ \env ->
-    do let top_tm = ttTerm top_tt
-       top_tp <- ttTypeAsTerm sc cry_env top_tt
-       (tm, env') <- monadifyTermInEnv sc env top_tm top_tp
-       tm' <- mkTypedTerm sc tm
-       return (tm', env')
+monadifyCryptolModule sc cry_env top_env cry_mod =
+  flip runStateT top_env $ monadifyCryptolModuleH sc cry_env cry_mod
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 07b146bbdb..23f226fd6c 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -3048,9 +3048,22 @@ assertingS : (E:EvType) -> (stack:FunStack) -> (a : sort 0) -> Bool ->
 assertingS E stack a cond m =
   bindS E stack #() a (assertBoolS E stack cond) (\ (_:#()) -> m);
 
+-- Lift a computation into a stack with an additional frame
+primitive pushStackS : (E:EvType) -> (frame:List1 LetRecType) ->
+                       (stack:FunStack) -> (A:sort 0) ->
+                       SpecM E stack A -> SpecM E (pushFunStack frame stack) A;
+
 -- Lift a computation in the empty stack to an arbitrary stack
-primitive liftStackS : (E:EvType) -> (stack:FunStack) -> (A:sort 0) ->
-                       SpecM E emptyFunStack A -> SpecM E stack A;
+liftStackS : (E:EvType) -> (stack:FunStack) -> (A:sort 0) ->
+             SpecM E emptyFunStack A -> SpecM E stack A;
+liftStackS E stack A m0 =
+  List1#rec
+  (List1 LetRecType)
+  (\ (stack:FunStack) -> SpecM E stack A)
+  m0
+  (\ (frame:List1 LetRecType) (stack:FunStack) (m:SpecM E stack A) ->
+     pushStackS E frame stack A m)
+  stack;
 
 -- The computation that nondeterministically chooses one computation or another.
 -- As a specification, represents the disjunction of two specifications.

From 1547ca8697cdff91e593f4ce0b46a733d44c0e3a Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 6 Mar 2023 06:50:29 -0800
Subject: [PATCH 04/19] fixed bug in monadifyNamedTermH, where primitives were
 being monadified into their pure type instead of their monadic type

---
 cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index 487c3dc15d..abee757c23 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1526,7 +1526,7 @@ monadifyNamedTermH sc nmi maybe_trm tp =
           --  trace ("" ++ ppTermInMonCtx env trm ++ "\n\n") $
            do trm' <- monadifyTermInEnvH sc trm tp
               lift $ scConstant' sc nmi' trm' comp_tp
-         Nothing -> lift $ scOpaqueConstant sc nmi' tp
+         Nothing -> lift $ scOpaqueConstant sc nmi' comp_tp
      return $ fromCompTerm mtp $ closedOpenTerm const_trm
 
 -- | Monadify a 'Term' of the specified type with an optional body, bind the

From 6195b0f827f780504a2a2b9df2c8a428eea09691 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 6 Mar 2023 07:28:20 -0800
Subject: [PATCH 05/19] changed write_coq_cryptol_primitives_for_sawcore to
 also write CryptolM.sawcore to a Coq file

---
 saw-core-coq/coq/_CoqProject              |  3 ++-
 saw-core-coq/saw/generate_scaffolding.saw |  2 +-
 src/SAWScript/Interpreter.hs              | 16 +++++++++-------
 src/SAWScript/Prover/Exporter.hs          | 11 +++++++++--
 4 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/saw-core-coq/coq/_CoqProject b/saw-core-coq/coq/_CoqProject
index 66f5300e6b..1ca05b0d81 100644
--- a/saw-core-coq/coq/_CoqProject
+++ b/saw-core-coq/coq/_CoqProject
@@ -1,8 +1,9 @@
 -Q generated/CryptolToCoq   CryptolToCoq
 -Q handwritten/CryptolToCoq CryptolToCoq
 
-generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
 generated/CryptolToCoq/SAWCorePrelude.v
+generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+generated/CryptolToCoq/CryptolMPrimitivesForSAWCore.v
 
 handwritten/CryptolToCoq/CompM.v
 handwritten/CryptolToCoq/CompMExtra.v
diff --git a/saw-core-coq/saw/generate_scaffolding.saw b/saw-core-coq/saw/generate_scaffolding.saw
index 645db4a8d3..708552fe18 100644
--- a/saw-core-coq/saw/generate_scaffolding.saw
+++ b/saw-core-coq/saw/generate_scaffolding.saw
@@ -1,3 +1,3 @@
 enable_experimental;
 write_coq_sawcore_prelude                "../coq/generated/CryptolToCoq/SAWCorePrelude.v" [] [];
-write_coq_cryptol_primitives_for_sawcore "../coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v" [] [];
+write_coq_cryptol_primitives_for_sawcore "../coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v" "../coq/generated/CryptolToCoq/CryptolMPrimitivesForSAWCore.v" [] [];
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 6a47d3c754..4434dd21e1 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1508,17 +1508,19 @@ primitives = Map.fromList
     , "The third argument is a list of identifiers to skip translating."
     ]
 
-  , prim "write_coq_cryptol_primitives_for_sawcore" "String -> [(String, String)] -> [String] -> TopLevel ()"
+  , prim "write_coq_cryptol_primitives_for_sawcore"
+    "String -> String -> [(String, String)] -> [String] -> TopLevel ()"
     (pureVal writeCoqCryptolPrimitivesForSAWCore)
     Experimental
-    [ "Write out a representation of cryptol-saw-core's Cryptol.sawcore in"
-    , "Gallina syntax for Coq."
-    , "The first argument is the name of the file to output into,"
-    , "use an empty string to output to standard output."
-    , "The second argument is a list of pairs of notation substitutions:"
+    [ "Write out a representation of cryptol-saw-core's Cryptol.sawcore and "
+    , "CryptolM.sawcore in Gallina syntax for Coq."
+    , "The first two arguments are the names of the output files for translating "
+    , "Cryptol.sawcore and CryptolM.sawcore, respectively."
+    , "Use an empty string to output to standard output."
+    , "The third argument is a list of pairs of notation substitutions:"
     , "the operator on the left will be replaced with the identifier on"
     , "the right, as we do not support notations on the Coq side."
-    , "The third argument is a list of identifiers to skip translating."
+    , "The fourth argument is a list of identifiers to skip translating."
     ]
 
   , prim "offline_coq" "String -> ProofScript ()"
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 04600c3239..c42662dcd1 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -70,6 +70,7 @@ import Lang.JVM.ProcessUtils (readProcessExitIfFailure)
 import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule,
                                 ImportPrimitiveOptions(..), mkCryEnv)
 import Verifier.SAW.Cryptol.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule)
+import Verifier.SAW.Cryptol.PreludeM (cryptolMModule, scLoadCryptolMModule)
 import Verifier.SAW.Cryptol.Monadify (defaultMonEnv, monadifyCryptolModule)
 import Verifier.SAW.ExternalFormat(scWriteExternal)
 import Verifier.SAW.FiniteValue
@@ -530,16 +531,18 @@ writeCoqSAWCorePrelude outputFile notations skips = do
   writeFile outputFile (show . vcat $ [ Coq.preamble configuration, doc ])
 
 writeCoqCryptolPrimitivesForSAWCore ::
-  FilePath ->
+  FilePath -> FilePath ->
   [(String, String)] ->
   [String] ->
   IO ()
-writeCoqCryptolPrimitivesForSAWCore outputFile notations skips = do
+writeCoqCryptolPrimitivesForSAWCore outputFile outputFileM notations skips = do
   sc <- mkSharedContext
   () <- scLoadPreludeModule sc
   () <- scLoadCryptolModule sc
+  () <- scLoadCryptolMModule sc
   () <- scLoadModule sc (emptyModule (mkModuleName ["CryptolPrimitivesForSAWCore"]))
   m  <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule
+  m_mon <- scFindModule sc (Un.moduleName cryptolMModule)
   let configuration =
         withImportSAWCorePreludeExtra $
         withImportSAWCorePrelude $
@@ -548,6 +551,10 @@ writeCoqCryptolPrimitivesForSAWCore outputFile notations skips = do
   writeFile outputFile (show . vcat $ [ Coq.preamble configuration
                                       , doc
                                       ])
+  let doc_mon = Coq.translateSAWModule configuration m_mon
+  writeFile outputFileM (show . vcat $ [ Coq.preamble configuration
+                                       , doc_mon
+                                       ])
 
 -- | Tranlsate a SAWCore term into an AIG
 bitblastPrim :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> Term -> IO (AIG.Network l g)

From 94866c376bce7684894f711e9c3cbb68f2b8a318 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 9 Mar 2023 17:13:18 -0500
Subject: [PATCH 06/19] add qsort, use new SortFlags type as extra arg of Sort
 constructor

---
 cryptol-saw-core/saw/CryptolM.sawcore         | 58 +++++++++--------
 .../src/Verifier/SAW/Cryptol/Monadify.hs      |  2 +-
 .../src/Verifier/SAW/Translation/Coq/Term.hs  | 57 +++++++++--------
 saw-core/prelude/Prelude.sawcore              |  4 +-
 saw-core/src/Verifier/SAW/Conversion.hs       |  2 +-
 saw-core/src/Verifier/SAW/ExternalFormat.hs   |  8 +--
 saw-core/src/Verifier/SAW/Grammar.y           | 13 +++-
 saw-core/src/Verifier/SAW/Lexer.x             |  3 +-
 saw-core/src/Verifier/SAW/OpenTerm.hs         |  2 +-
 saw-core/src/Verifier/SAW/Recognizer.hs       | 10 +--
 saw-core/src/Verifier/SAW/SharedTerm.hs       |  9 ++-
 saw-core/src/Verifier/SAW/Term/CtxTerm.hs     |  2 +-
 saw-core/src/Verifier/SAW/Term/Functor.hs     | 63 +++++++++++++++----
 saw-core/src/Verifier/SAW/Term/Pretty.hs      |  2 +-
 saw-core/src/Verifier/SAW/Typechecker.hs      |  3 +-
 saw-core/src/Verifier/SAW/TypedAST.hs         |  1 +
 saw-core/src/Verifier/SAW/UntypedAST.hs       |  4 +-
 17 files changed, 150 insertions(+), 93 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index 19a369660e..bf82dacc8e 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -125,7 +125,8 @@ bvVecMapM E stack a b n len f xs = bvVecMapInvarM E stack a b n len f xs True;
 -}
 
 vecMapInvarBindM : (E:EvType) -> (stack:FunStack) ->
-                   (a b c : isort 0) -> (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
+                   (a : sort 0) -> (b : qsort 0) -> (c : sort 0) ->
+                   (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
                    Vec n a -> Bool -> (Vec n b -> SpecM E stack c) ->
                    SpecM E stack c;
 vecMapInvarBindM E stack a b c n f xs invar cont =
@@ -149,18 +150,21 @@ vecMapInvarBindM E stack a b c n f xs invar cont =
       0 ys0);
 
 vecMapInvarM : (E:EvType) -> (stack:FunStack) ->
-               (a b : isort 0) -> (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
+               (a : sort 0) -> (b : qsort 0) ->
+               (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
                Vec n a -> Bool -> SpecM E stack (Vec n b);
 vecMapInvarM E stack a b n f xs invar =
   vecMapInvarBindM E stack a b (Vec n b) n f xs invar (retS E stack (Vec n b));
 
-vecMapM : (E:EvType) -> (stack:FunStack) -> (a b : isort 0) -> (n : Nat) ->
-          (Nat -> a -> SpecM E stack b) -> Vec n a -> SpecM E stack (Vec n b);
+vecMapM : (E:EvType) -> (stack:FunStack) ->
+          (a : sort 0) -> (b : qsort 0) ->
+          (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
+          Vec n a -> SpecM E stack (Vec n b);
 vecMapM E stack a b n f xs = vecMapInvarM E stack a b n f xs True;
 
 -- Computational version of seqMap
 seqMapM : (E:EvType) -> (stack:FunStack) ->
-          (a b : sort 0) -> (n : Num) -> (a -> SpecM E stack b) ->
+          (a : sort 0) -> (b : qsort 0) -> (n : Num) -> (a -> SpecM E stack b) ->
           mseq E stack n a -> SpecM E stack (mseq E stack n b);
 seqMapM E stack a b n_top f =
   Num_rec (\ (n:Num) -> mseq E stack n a -> SpecM E stack (mseq E stack n b))
@@ -191,7 +195,7 @@ seqToMseq E stack n_top a =
 -- Auxiliary functions
 
 bvVecAtM : (E:EvType) -> (stack:FunStack) ->
-           (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) ->
+           (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
            BVVec n len a -> Vec n Bool -> SpecM E stack a;
 bvVecAtM E stack n len a xs i =
   maybe (is_bvult n i len) (SpecM E stack a)
@@ -200,7 +204,7 @@ bvVecAtM E stack n len a xs i =
         (bvultWithProof n i len);
 
 atM : (E:EvType) -> (stack:FunStack) ->
-      (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> SpecM E stack a;
+      (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> SpecM E stack a;
 atM E stack n a xs i =
   maybe (IsLtNat i n) (SpecM E stack a)
         (errorS E stack a "atM: invalid sequence index")
@@ -208,7 +212,7 @@ atM E stack n a xs i =
         (proveLtNat i n);
 
 bvVecUpdateM : (E:EvType) -> (stack:FunStack) ->
-               (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) ->
+               (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
                BVVec n len a -> Vec n Bool -> a ->
                SpecM E stack (BVVec n len a);
 bvVecUpdateM E stack n len a xs i x =
@@ -219,7 +223,7 @@ bvVecUpdateM E stack n len a xs i x =
         (bvultWithProof n i len);
 
 fromBVVecUpdateM : (E:EvType) -> (stack:FunStack) ->
-                   (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) ->
+                   (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
                    BVVec n len a -> Vec n Bool -> a ->
                    a -> (m : Nat) -> SpecM E stack (Vec m a);
 fromBVVecUpdateM E stack n len a xs i x def m =
@@ -231,7 +235,7 @@ fromBVVecUpdateM E stack n len a xs i x def m =
         (bvultWithProof n i len);
 
 updateM : (E:EvType) -> (stack:FunStack) ->
-          (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a ->
+          (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> a ->
           SpecM E stack (Vec n a);
 updateM E stack n a xs i x =
   maybe (IsLtNat i n) (SpecM E stack (Vec n a))
@@ -240,12 +244,12 @@ updateM E stack n a xs i x =
         (proveLtNat i n);
 
 eListSelM : (E:EvType) -> (stack:FunStack) ->
-            (a : isort 0) -> (n : Num) -> mseq E stack n a -> Nat ->
+            (a : sort 0) -> (n : Num) -> mseq E stack n a -> Nat ->
             SpecM E stack a;
 eListSelM E stack a =
   Num_rec (\ (n:Num) -> mseq E stack n a -> Nat -> SpecM E stack a)
           (\ (n:Nat) -> atM E stack n a)
-          (eListSel (SpecM E stack a) TCInf);
+          (streamGet (SpecM E stack a));
 
 
 --------------------------------------------------------------------------------
@@ -266,12 +270,12 @@ mletM : (E:EvType) -> (stack:FunStack) ->
         SpecM E stack (mseq E stack n (a * b));
 
 -- An alternate version of zip from Prelude to get around the default Prim
-zipCryM : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
+zipCryM : (a b : isort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
 zipCryM a b m n xs ys =
   genCryM (minNat m n) (a * b) (\ (i:Nat) -> (atCryM m a xs i, atCryM n b ys i));
 
 seqZipM : (E:EvType) -> (stack:FunStack) ->
-          (a b : sort 0) -> (m n : Num) ->
+          (a b : qisort 0) -> (m n : Num) ->
           mseq E stack m a -> mseq E stack n b ->
           SpecM E stack (mseq E stack (tcMin m n) (a * b));
 seqZipM E stack a b m n =
@@ -491,11 +495,11 @@ ecRotRM E stack =
     (\ (m:Nat) -> ecRotR (TCNum m));
 
 ecCatM : (E:EvType) -> (stack:FunStack) ->
-         (m : Num) -> isFinite m -> (n : Num) -> (a : sort 0) ->
+         (m : Num) -> isFinite m -> (n : Num) -> (a : isort 0) ->
          mseq E stack m a -> mseq E stack n a -> mseq E stack (tcAdd m n) a;
 ecCatM E stack =
   Num_rec_fin
-    (\ (m:Num) -> (n:Num) -> (a:sort 0) -> mseq E stack m a -> mseq E stack n a ->
+    (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq E stack m a -> mseq E stack n a ->
                   mseq E stack (tcAdd m n) a)
     (\ (m:Nat) ->
        Num_rec
@@ -535,7 +539,7 @@ ecDropM : (E:EvType) -> (stack:FunStack) ->
           mseq E stack (tcAdd m n) a -> mseq E stack n a;
 
 ecJoinM : (E:EvType) -> (stack:FunStack) -> 
-          (m n : Num) -> (a : sort 0) -> mseq E stack m (mseq E stack n a) ->
+          (m n : Num) -> (a : isort 0) -> mseq E stack m (mseq E stack n a) -
           mseq E stack (tcMul m n) a;
 ecJoinM E stack =
   Num_rec
@@ -574,24 +578,24 @@ splitCryM m n a v =
       atCryM (mulNat m n) a v (addNat (mulNat i n) j)));
 
 ecSplitM : (E:EvType) -> (stack:FunStack) ->
-           (m n : Num) -> (a : sort 0) -> mseq E stack (tcMul m n) a ->
+           (m n : Num) -> (a : qisort 0) -> mseq E stack (tcMul m n) a ->\
            mseq E stack m (mseq E stack n a);
 ecSplitM E stack =
   Num_rec
-    (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq E stack (tcMul m n) a ->
+    (\ (m:Num) -> (n:Num) -> (a:qisort 0) -> mseq E stack (tcMul m n) a ->
        mseq E stack m (mseq E stack n a))
     (\ (m:Nat) ->
        finNumRec
-         (\ (n:Num) -> (a:isort 0) -> mseq E stack (tcMul (TCNum m) n) a ->
+         (\ (n:Num) -> (a:qisort 0) -> mseq E stack (tcMul (TCNum m) n) a ->
             Vec m (mseq E stack n a))
          -- Case for (TCNum m, TCNum n)
-         (\ (n:Nat) -> \ (a:isort 0) -> splitCryM m n a))
+         (\ (n:Nat) -> \ (a:qisort 0) -> splitCryM m n a))
          -- No case for (TCNum m, TCInf), shouldn't happen
     (finNumRec
-       (\ (n:Num) -> (a:isort 0) -> mseq E stack (tcMul TCInf n) a ->
+       (\ (n:Num) -> (a:qisort 0) -> mseq E stack (tcMul TCInf n) a ->
           Stream (SpecM E stack (mseq E stack n a)))
        -- Case for (TCInf, TCNum n)
-       (\ (n:Nat) -> \ (a:isort 0) ->
+       (\ (n:Nat) -> \ (a:qisort 0) ->
           natCase
             (\ (n':Nat) ->
                mseq E stack (if0Nat Num n' (TCNum 0) TCInf) a ->
@@ -608,10 +612,10 @@ ecSplitM E stack =
        -- No case for (TCInf, TCInf), shouldn't happen
 
 ecReverseM : (E:EvType) -> (stack:FunStack) ->
-             (n : Num) -> isFinite n -> (a : sort 0) -> mseq E stack n a ->
+             (n : Num) -> isFinite n -> (a : isort 0) -> mseq E stack n a ->
              mseq E stack n a;
 ecReverseM E stack =
-  Num_rec_fin (\ (n:Num) -> (a : sort 0) -> mseq E stack n a -> mseq E stack n a)
+  Num_rec_fin (\ (n:Num) -> (a : isort 0) -> mseq E stack n a -> mseq E stack n a)
               (\ (n:Nat) -> ecReverse (TCNum n));
 
 -- FIXME
@@ -621,7 +625,7 @@ ecTransposeM : (E:EvType) -> (stack:FunStack) ->
                mseq E stack n (mseq E stack m a);
 
 ecAtM : (E:EvType) -> (stack:FunStack) ->
-        (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix ->
+        (n : Num) -> (a : sort 0) -> (ix : sort 0) -> PIntegral ix ->
         mseq E stack n a -> ix -> SpecM E stack a;
 ecAtM E stack n_top a ix pix =
   Num_rec
@@ -637,7 +641,7 @@ ecAtM E stack n_top a ix pix =
     n_top;
 
 ecUpdateM : (E:EvType) -> (stack:FunStack) ->
-            (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix ->
+            (n : Num) -> (a : sort 0) -> (ix : sort 0) -> PIntegral ix ->
             mseq E stack n a -> ix -> a -> SpecM E stack (mseq E stack n a);
 ecUpdateM E stack n_top a ix pix =
   Num_rec
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index abee757c23..e3ef8912be 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -137,7 +137,7 @@ typedSubsTermType :: TypedSubsTerm -> TypedSubsTerm
 typedSubsTermType tst =
   TypedSubsTerm { tpSubsIndex = Nothing, tpSubsFreeVars = tpSubsFreeVars tst,
                   tpSubsTermF = tpSubsTypeF tst,
-                  tpSubsTypeF = FTermF (Sort (tpSubsSort tst) False),
+                  tpSubsTypeF = FTermF (Sort (tpSubsSort tst) noFlags),
                   tpSubsSort = sortOf (tpSubsSort tst) }
 
 -- | Count the number of right-nested pi-abstractions of a 'TypedSubsTerm'
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
index 01b91a27e7..2dac1bf2a2 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -464,10 +464,9 @@ translateParam ::
   TermTranslationMonad m =>
   (LocalName, Term) -> m [Coq.Binder]
 translateParam (n, ty) =
-  translateBinder n ty >>= \case
-    Left (n',ty') -> return [Coq.Binder n' (Just ty')]
-    Right (n',ty',nh,nhty) ->
-      return [Coq.Binder n' (Just ty'), Coq.ImplicitBinder nh (Just nhty)]
+  translateBinder n ty >>= \(n',ty',nhs) ->
+    return $ Coq.Binder n' (Just ty') :
+             map (\(nh,nhty) -> Coq.ImplicitBinder nh (Just nhty)) nhs
 
 translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term
 translatePi binders body = withLocalTranslationState $ do
@@ -479,44 +478,44 @@ translatePiBinder ::
   TermTranslationMonad m => (LocalName, Term) -> m [Coq.PiBinder]
 translatePiBinder (n, ty) =
   translateBinder n ty >>= \case
-    Left (n',ty')
+    (n',ty',[])
       | n == "_"  -> return [Coq.PiBinder Nothing ty']
       | otherwise -> return [Coq.PiBinder (Just n') ty']
-    Right (n',ty',nh,nhty) ->
-      return [Coq.PiBinder (Just n') ty', Coq.PiImplicitBinder (Just nh) nhty]
+    (n',ty',nhs) ->
+      return $ Coq.PiBinder (Just n') ty' :
+               map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs
 
 translateBinder ::
   TermTranslationMonad m =>
   LocalName ->
   Term ->
-  m (Either (Coq.Ident,Coq.Type) (Coq.Ident,Coq.Type,Coq.Ident,Coq.Type))
-translateBinder n ty@(asPiList -> (args, asISort -> Just _s)) =
+  m (Coq.Ident,Coq.Type,[(Coq.Ident,Coq.Type)])
+translateBinder n ty@(asPiList -> (args, asSortWithFlags -> mb_sort)) =
   do ty' <- translateTerm ty
      n' <- freshenAndBindName n
-     hty' <- translateInhHyp args (Coq.Var n')
-     hn' <- translateLocalIdent ("Inh_" <> n )
-     return $ Right (n',ty',hn',hty')
-translateBinder n ty =
-  do ty' <- translateTerm ty
-     n'  <- freshenAndBindName n
-     return $ Left (n',ty')
-
-translateInhHyp ::
+     let flagValues = sortFlagsToList $ maybe noFlags snd mb_sort
+         flagLocalNames = [("Inh", "SAWCoreScaffolding.Inhabited"),
+                           ("QT", "QuantType")]
+     nhs <- forM (zip flagValues flagLocalNames) $ \(fi,(prefix,tc)) ->
+       if not fi then return []
+       else do nhty <- translateImplicitHyp (Coq.Var tc) args (Coq.Var n')
+               nh <- translateLocalIdent (prefix <> "_" <> n)
+               return [(nh,nhty)]
+     return (n',ty',concat nhs)
+
+translateImplicitHyp ::
   TermTranslationMonad m =>
-  [(LocalName, Term)] -> Coq.Term -> m Coq.Term
-translateInhHyp [] tm = return (Coq.App (Coq.Var "SAWCoreScaffolding.Inhabited") [tm])
-translateInhHyp args tm = withLocalTranslationState $
+  Coq.Term -> [(LocalName, Term)] -> Coq.Term -> m Coq.Term
+translateImplicitHyp tc [] tm = return (Coq.App tc [tm])
+translateImplicitHyp tc args tm = withLocalTranslationState $
   do args' <- mapM (uncurry translateBinder) args
      return $ Coq.Pi (concatMap mkPi args')
-                (Coq.App (Coq.Var "SAWCoreScaffolding.Inhabited") [Coq.App tm (map mkArg args')])
+                (Coq.App tc [Coq.App tm (map mkArg args')])
  where
-  mkPi (Left (nm,ty)) =
-    [Coq.PiBinder (Just nm) ty]
-  mkPi (Right (nm,ty,hnm,hty)) =
-    [Coq.PiBinder (Just nm) ty, Coq.PiImplicitBinder (Just hnm) hty]
-
-  mkArg (Left (nm,_)) = Coq.Var nm
-  mkArg (Right (nm,_,_,_)) = Coq.Var nm
+  mkPi (nm,ty,nhs) =
+    Coq.PiBinder (Just nm) ty :
+    map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs
+  mkArg (nm,_,_) = Coq.Var nm
 
 -- | Translate a local name from a saw-core binder into a fresh Coq identifier.
 translateLocalIdent :: TermTranslationMonad m => LocalName -> m Coq.Ident
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 23f226fd6c..74755e6683 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -3011,11 +3011,11 @@ primitive errorS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> String ->
                    SpecM E stack a;
 
 -- The spec that universally quantifies over all return values of type a
-primitive forallS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
+primitive forallS : (E:EvType) -> (stack:FunStack) -> (a:qsort 0) ->
                     SpecM E stack a;
 
 -- The spec that existentially quantifies over all return values of type a
-primitive existsS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
+primitive existsS : (E:EvType) -> (stack:FunStack) -> (a:qsort 0) ->
                     SpecM E stack a;
 
 -- Assume a proposition holds
diff --git a/saw-core/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs
index 2d6e2615d4..da72c6222a 100644
--- a/saw-core/src/Verifier/SAW/Conversion.hs
+++ b/saw-core/src/Verifier/SAW/Conversion.hs
@@ -282,7 +282,7 @@ asAnySort = asVar $ \t -> do Sort v _ <- R.asFTermF t; return v
 
 -- | Match a specific sort.
 asSort :: Sort -> Matcher ()
-asSort s = Matcher (termToPat (Unshared (FTermF (Sort s False)))) fn
+asSort s = Matcher (termToPat (Unshared (FTermF (Sort s noFlags)))) fn
   where fn t = do s' <- R.asSort t
                   guard (s == s')
 
diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs
index 13b69f7a0e..5c0482b25d 100644
--- a/saw-core/src/Verifier/SAW/ExternalFormat.hs
+++ b/saw-core/src/Verifier/SAW/ExternalFormat.hs
@@ -184,8 +184,8 @@ scWriteExternal t0 =
             RecordValue elems   -> pure $ unwords ["Record", show elems]
             RecordProj e prj    -> pure $ unwords ["RecordProj", show e, Text.unpack prj]
             Sort s h
-              | s == propSort -> pure $ unwords ["Prop", show h]
-              | otherwise     -> pure $ unwords ["Sort", drop 5 (show s), show h]
+              | s == propSort -> pure $ unwords ("Prop" : map show (sortFlagsToList h))
+              | otherwise     -> pure $ unwords ("Sort" : drop 5 (show s) : map show (sortFlagsToList h))
                                                         -- /\ Ugly hack to drop "sort "
             NatLit n            -> pure $ unwords ["Nat", show n]
             ArrayValue e v      -> pure $ unwords ("Array" : show e :
@@ -347,8 +347,8 @@ scReadExternal sc input =
         ["Record", elems] ->
           FTermF <$> (RecordValue <$> (traverse (traverse getTerm) =<< readM elems))
         ["RecordProj", e, prj] -> FTermF <$> (RecordProj <$> readIdx e <*> pure (Text.pack prj))
-        ["Prop", h]         -> FTermF <$> (Sort propSort <$> readM h)
-        ["Sort", s, h]      -> FTermF <$> (Sort <$> (mkSort <$> readM s) <*> readM h)
+        ("Prop" : h)        -> FTermF <$> (Sort propSort . sortFlagsFromList <$> (mapM readM h))
+        ("Sort" : s : h)    -> FTermF <$> (Sort <$> (mkSort <$> readM s) <*> (sortFlagsFromList <$> mapM readM h))
         ["Nat", n]          -> FTermF <$> (NatLit <$> readM n)
         ("Array" : e : es)  -> FTermF <$> (ArrayValue <$> readIdx e <*> (V.fromList <$> traverse readIdx es))
         ("String" : ts)     -> FTermF <$> (StringLit <$> (readM (unwords ts)))
diff --git a/saw-core/src/Verifier/SAW/Grammar.y b/saw-core/src/Verifier/SAW/Grammar.y
index a37fee8d01..6764c297f3 100644
--- a/saw-core/src/Verifier/SAW/Grammar.y
+++ b/saw-core/src/Verifier/SAW/Grammar.y
@@ -73,6 +73,8 @@ import Verifier.SAW.Lexer
   'module'    { PosPair _ (TKey "module") }
   'sort'      { PosPair _ (TKey "sort") }
   'isort'     { PosPair _ (TKey "isort") }
+  'qsort'     { PosPair _ (TKey "qsort") }
+  'qisort'    { PosPair _ (TKey "qisort") }
   'Prop'      { PosPair _ (TKey "Prop") }
   'where'     { PosPair _ (TKey "where") }
   'axiom'     { PosPair _ (TKey "axiom") }
@@ -182,9 +184,8 @@ AtomTerm
   | string                       { StringLit (pos $1) (Text.pack (tokString (val $1))) }
   | Ident                        { Name $1 }
   | IdentRec                     { Recursor Nothing $1 }
-  | 'Prop'                       { Sort (pos $1) propSort False }
-  | 'sort' nat                   { Sort (pos $1) (mkSort (tokNat (val $2))) False }
-  | 'isort' nat                  { Sort (pos $1) (mkSort (tokNat (val $2))) True }
+  | 'Prop'                       { Sort (pos $1) propSort noFlags }
+  | Sort nat                     { Sort (pos $1) (mkSort (tokNat (val $2))) (val $1) }
   | AtomTerm '.' Ident           { RecordProj $1 (val $3) }
   | AtomTerm '.' IdentRec        {% parseRecursorProj $1 $3 }
   | AtomTerm '.' nat             {% parseTupleSelector $1 (fmap tokNat $3) }
@@ -201,6 +202,12 @@ Ident : ident { fmap (Text.pack . tokIdent) $1 }
 IdentRec :: { PosPair Text }
 IdentRec : identrec { fmap (Text.pack . tokRecursor) $1 }
 
+Sort :: { PosPair SortFlags }
+Sort : 'sort'   { fmap (const $ SortFlags False False) $1 }
+     | 'isort'  { fmap (const $ SortFlags True  False) $1 }
+     | 'qsort'  { fmap (const $ SortFlags False True ) $1 }
+     | 'qisort' { fmap (const $ SortFlags True  True ) $1 }
+
 FieldValue :: { (PosPair FieldName, Term) }
 FieldValue : Ident '=' Term { ($1, $3) }
 
diff --git a/saw-core/src/Verifier/SAW/Lexer.x b/saw-core/src/Verifier/SAW/Lexer.x
index ffb2e9f77b..714a3c87bb 100644
--- a/saw-core/src/Verifier/SAW/Lexer.x
+++ b/saw-core/src/Verifier/SAW/Lexer.x
@@ -73,7 +73,8 @@ $idchar    = [a-z A-Z 0-9 \' \_]
 @punct = "#" | "," | "->" | "." | ";" | ":" | "=" | "*"
        | "\" | "(" | ")" | "[" | "]" | "{" | "}" | "|"
 @keywords = "data" | "hiding" | "import" | "module" | "injectCode"
-          | "sort" | "isort" | "Prop" | "where" | "primitive" | "axiom"
+          | "sort" | "isort" | "qsort" | "qisort"
+          | "Prop" | "where" | "primitive" | "axiom"
 @key = @punct | @keywords
 
 @escape      = \\ ($charesc | @ascii | @decimal | o @octal | x @hex)
diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs
index 08cfb71ac4..362cf45f85 100644
--- a/saw-core/src/Verifier/SAW/OpenTerm.hs
+++ b/saw-core/src/Verifier/SAW/OpenTerm.hs
@@ -131,7 +131,7 @@ flatOpenTerm ftf = OpenTerm $
 
 -- | Build an 'OpenTerm' for a sort
 sortOpenTerm :: Sort -> OpenTerm
-sortOpenTerm s = flatOpenTerm (Sort s False)
+sortOpenTerm s = flatOpenTerm (Sort s noFlags)
 
 -- | Build an 'OpenTerm' for a natural number literal
 natOpenTerm :: Natural -> OpenTerm
diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs
index e7be1a8b61..54f4746ae8 100644
--- a/saw-core/src/Verifier/SAW/Recognizer.hs
+++ b/saw-core/src/Verifier/SAW/Recognizer.hs
@@ -56,7 +56,7 @@ module Verifier.SAW.Recognizer
   , asConstant
   , asExtCns
   , asSort
-  , asISort
+  , asSortWithFlags
     -- * Prelude recognizers.
   , asBool
   , asBoolType
@@ -340,12 +340,12 @@ asSort t = do
     Sort s _ -> return s
     _      -> Nothing
 
-asISort :: Recognizer Term Sort
-asISort t = do
+asSortWithFlags :: Recognizer Term (Sort, SortFlags)
+asSortWithFlags t = do
   ftf <- asFTermF t
   case ftf of
-    Sort s True -> return s
-    _           -> Nothing
+    Sort s h -> return (s, h)
+    _      -> Nothing
 
 
 
diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index f459e55da4..82fa91cae4 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -104,6 +104,7 @@ module Verifier.SAW.SharedTerm
   , scApplyCtor
   , scSort
   , scISort
+  , scSortWithFlags
     -- *** Variables and constants
   , scLocalVar
   , scConstant
@@ -1360,11 +1361,15 @@ scApplyCtor sc c args = scCtorApp sc (ctorName c) args
 
 -- | Create a term from a 'Sort'.
 scSort :: SharedContext -> Sort -> IO Term
-scSort sc s = scFlatTermF sc (Sort s False)
+scSort sc s = scFlatTermF sc (Sort s noFlags)
+
+-- | Create a term from a 'Sort', and set the given advisory flags
+scSortWithFlags :: SharedContext -> Sort -> SortFlags -> IO Term
+scSortWithFlags sc s h = scFlatTermF sc (Sort s h)
 
 -- | Create a term from a 'Sort', and set the advisory "inhabited" flag
 scISort :: SharedContext -> Sort -> IO Term
-scISort sc s = scFlatTermF sc (Sort s True)
+scISort sc s = scSortWithFlags sc s $ noFlags { flagInhabited = True }
 
 -- | Create a literal term from a 'Natural'.
 scNat :: SharedContext -> Natural -> IO Term
diff --git a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs
index ddb79fe7e0..49644b9860 100644
--- a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs
+++ b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs
@@ -402,7 +402,7 @@ ctxVars2 vars1 vars2 =
 
 -- | Build a 'CtxTerm' for a 'Sort'
 ctxSort :: MonadTerm m => Sort -> m (CtxTerm ctx (Typ a))
-ctxSort s = CtxTerm <$> mkFlatTermF (Sort s False)
+ctxSort s = CtxTerm <$> mkFlatTermF (Sort s noFlags)
 
 -- | Apply two 'CtxTerm's
 ctxApply :: MonadTerm m => m (CtxTerm ctx (a -> b)) -> m (CtxTerm ctx a) ->
diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs
index 59c3e3276d..5e8343e941 100644
--- a/saw-core/src/Verifier/SAW/Term/Functor.hs
+++ b/saw-core/src/Verifier/SAW/Term/Functor.hs
@@ -55,6 +55,7 @@ module Verifier.SAW.Term.Functor
   , alistAllFields
     -- * Sorts
   , Sort, mkSort, propSort, sortOf, maxSort
+  , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
     -- * Sets of free variables
   , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets
   , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems
@@ -132,6 +133,50 @@ maxSort :: [Sort] -> Sort
 maxSort [] = propSort
 maxSort ss = maximum ss
 
+-- | This type represents a set of advisory flags for 'Sort's that are mostly
+-- ignored, but are used in the Coq export process to indicate where various
+-- typeclass instances are necessary in function definitions. In the concrete
+-- syntax "isort", "qsort", etc. is used to indicate cases where these flags
+-- are set. Note in particular that this flag does not affect typechecking,
+-- so missing or overeager "isort"/"qsort" annotations will only be detected
+-- via the Coq export.
+--
+-- * If 'flagInhabited' is 'True', an implicit @Inhabited@ typeclass argument
+--   will be added during Coq translation. In the concrete syntax, an "i" is
+--   prepended to the sort (e.g. "isort").
+-- * If 'flagQuantType' is 'True', an implicit @QuantType@ typeclass argument
+--   will be added during Coq translation. In the concrete syntax, an "q" is
+--   prepended to the sort (e.g. "qsort", "qisort").
+data SortFlags = SortFlags { flagInhabited :: Bool
+                           , flagQuantType :: Bool }
+    deriving (Eq, Ord, Generic, TH.Lift)
+
+instance Hashable SortFlags -- automatically derived
+
+instance Show SortFlags where
+  showsPrec _ (SortFlags i q) =
+    showString $ (if q then "q" else "") ++
+                 (if i then "i" else "")
+
+-- | The 'SortFlags' object with no flags set
+noFlags :: SortFlags
+noFlags = SortFlags False False
+
+-- | Combine two 'SortFlags' by setting each flag in the result if and only if
+-- it flag is set in both inputs
+cbnFlags :: SortFlags -> SortFlags -> SortFlags
+cbnFlags (SortFlags i1 q1) (SortFlags i2 q2) =
+  SortFlags (i1 && i2) (q1 && q2)
+
+-- | Convert a 'SortFlags' to a list of 'Bool's, indicating which flags are set
+sortFlagsToList :: SortFlags -> [Bool]
+sortFlagsToList (SortFlags i q) = [i, q]
+
+-- | Build a 'SortFlags' from a list of 'Bool's indicating which flags are set
+sortFlagsFromList :: [Bool] -> SortFlags
+sortFlagsFromList h = SortFlags (isTrue h 0) (isTrue h 1)
+  where isTrue xs i = i < length xs && xs !! i
+
 
 -- Flat Terms ------------------------------------------------------------------
 
@@ -191,17 +236,9 @@ data FlatTermF e
   | RecordProj e !FieldName
 
     -- | Sorts, aka universes, are the types of types; i.e., an object is a
-    -- "type" iff it has type @Sort s@ for some s.
-    --
-    -- The extra boolean argument is an advisory flag that is used to
-    -- indicate that types in this sort are expected to be inhabited.
-    -- In the concrete syntax "isort" is used to indicate cases where
-    -- this flag is set.  This flag is mostly ignored, but is used in
-    -- the Coq export process to indicate where "Inhabited" class
-    -- instances are necessary in function definitions. Note in particular
-    -- that this flag does not affect typechecking, so missing or overeager
-    -- "isort" annotations will only be detected via the Coq export.
-  | Sort !Sort !Bool
+    -- "type" iff it has type @Sort s@ for some s. See 'SortFlags' for an
+    -- explanation of the extra argument.
+  | Sort !Sort !SortFlags
 
     -- Primitive builtin values
     -- | Natural number with given value.
@@ -315,8 +352,8 @@ zipWithFlatTermF f = go
     go (RecordProj e1 fld1) (RecordProj e2 fld2)
       | fld1 == fld2 = Just $ RecordProj (f e1 e2) fld1
 
-    go (Sort sx hx) (Sort sy hy) | sx == sy = Just (Sort sx (hx && hy))
-         -- /\ NB, it's not entirely clear how the inhabited flag should be propagated
+    go (Sort sx hx) (Sort sy hy) | sx == sy = Just (Sort sx (cbnFlags hx hy))
+         -- /\ NB, it's not entirely clear how the flags should be propagated
     go (NatLit i) (NatLit j) | i == j = Just (NatLit i)
     go (StringLit s) (StringLit t) | s == t = Just (StringLit s)
     go (ArrayValue tx vx) (ArrayValue ty vy)
diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs
index f574da49b3..c3eb60da4a 100644
--- a/saw-core/src/Verifier/SAW/Term/Pretty.hs
+++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs
@@ -484,7 +484,7 @@ ppFlatTermF prec tf =
     RecordValue alist ->
       ppRecord False <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecTerm t) alist
     RecordProj e fld -> ppProj fld <$> ppTerm' PrecArg e
-    Sort s h -> return ((if h then pretty ("i"::String) else mempty) <> viaShow s)
+    Sort s h -> return (viaShow h <> viaShow s)
     NatLit i -> ppNat <$> (ppOpts <$> ask) <*> return (toInteger i)
     ArrayValue (asBoolType -> Just _) args
       | Just bits <- mapM asBool $ V.toList args ->
diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs
index c2ccb0903a..a7c21ad96e 100644
--- a/saw-core/src/Verifier/SAW/Typechecker.hs
+++ b/saw-core/src/Verifier/SAW/Typechecker.hs
@@ -400,7 +400,8 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
   -- type of d as (p1:param1) -> ... -> (i1:ix1) -> ... -> Type s
   (dt_ixs, dtSort) <-
     case Un.asPiList dt_tp of
-      (ixs, Un.Sort _ s False) -> return (ixs, s) -- NB, don't allow `isort`
+      (ixs, Un.Sort _ s h) | h == noFlags ->
+        return (ixs, s) -- NB, don't allow `isort`, etc.
       _ -> err "Wrong form for type of datatype"
   dt_ixs_typed <- typeInferCompleteCtx dt_ixs
   let dtIndices = map (\(x,tp,_) -> (x,tp)) dt_ixs_typed
diff --git a/saw-core/src/Verifier/SAW/TypedAST.hs b/saw-core/src/Verifier/SAW/TypedAST.hs
index 30bc6a9ade..3a01d74411 100644
--- a/saw-core/src/Verifier/SAW/TypedAST.hs
+++ b/saw-core/src/Verifier/SAW/TypedAST.hs
@@ -70,6 +70,7 @@ module Verifier.SAW.TypedAST
  , scPrettyTermInCtx
    -- * Primitive types.
  , Sort, mkSort, propSort, sortOf, maxSort
+ , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
  , Ident(..), identName, mkIdent
  , NameInfo(..), toShortName, toAbsoluteName
  , parseIdent
diff --git a/saw-core/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs
index d889210fe2..86644ec840 100644
--- a/saw-core/src/Verifier/SAW/UntypedAST.hs
+++ b/saw-core/src/Verifier/SAW/UntypedAST.hs
@@ -33,6 +33,7 @@ module Verifier.SAW.UntypedAST
   , mkTupleSelector
   , FieldName
   , Sort, mkSort, propSort, sortOf
+  , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
   , badTerm
   , module Verifier.SAW.Position
   , moduleName
@@ -56,13 +57,14 @@ import Verifier.SAW.Position
 import Verifier.SAW.TypedAST
   ( ModuleName, mkModuleName
   , Sort, mkSort, propSort, sortOf
+  , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
   , FieldName, DefQualifier
   , LocalName
   )
 
 data Term
   = Name (PosPair Text)
-  | Sort Pos Sort Bool
+  | Sort Pos Sort SortFlags
   | App Term Term
   | Lambda Pos TermCtx Term
   | Pi Pos TermCtx Term

From 7ba3edd0214ea95f927a05e208562ca4316fe696 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 9 Mar 2023 17:21:46 -0500
Subject: [PATCH 07/19] get Coq translation of CryptolM to typecheck

---
 cryptol-saw-core/saw/CryptolM.sawcore         | 30 +++-----
 .../src/Verifier/SAW/Cryptol/Monadify.hs      | 76 ++++++++++---------
 .../CryptolToCoq/SAWCorePreludeExtra.v        | 60 +++++++++++++++
 .../coq/handwritten/CryptolToCoq/SpecMExtra.v | 58 --------------
 src/SAWScript/Prover/Exporter.hs              |  6 +-
 5 files changed, 117 insertions(+), 113 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index bf82dacc8e..70a1c93dda 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -441,12 +441,6 @@ PLiteralSeqBoolM E stack =
 
 -- Sequences
 
--- FIXME: a number of the non-monadic versions of these functions contain calls
--- to finNumRec, which calls error on non-finite numbers. The monadic versions
--- of these, below, should be reimplemented to not contain finNumRec, but to
--- just use Num_rec_fin directly, rather than using it and then calling out to
--- the non-monadic version with finNumRec.
-
 ecShiftLM : (E:EvType) -> (stack:FunStack) ->
             (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
             mseq E stack m a -> ix -> mseq E stack m a;
@@ -539,20 +533,20 @@ ecDropM : (E:EvType) -> (stack:FunStack) ->
           mseq E stack (tcAdd m n) a -> mseq E stack n a;
 
 ecJoinM : (E:EvType) -> (stack:FunStack) -> 
-          (m n : Num) -> (a : isort 0) -> mseq E stack m (mseq E stack n a) -
-          mseq E stack (tcMul m n) a;
+          (m n : Num) -> isFinite n -> (a : isort 0) ->
+          mseq E stack m (mseq E stack n a) -> mseq E stack (tcMul m n) a;
 ecJoinM E stack =
   Num_rec
-    (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq E stack m (mseq E stack n a) ->
-       mseq E stack (tcMul m n) a)
+    (\ (m:Num) -> (n:Num) -> isFinite n -> (a:isort 0) ->
+       mseq E stack m (mseq E stack n a) -> mseq E stack (tcMul m n) a)
     (\ (m:Nat) ->
-       finNumRec
+       Num_rec_fin
          (\ (n:Num) -> (a:isort 0) -> Vec m (mseq E stack n a) ->
             mseq E stack (tcMul (TCNum m) n) a)
          -- Case for (TCNum m, TCNum n)
          (\ (n:Nat) -> \ (a:isort 0) -> joinCryM m n a))
          -- No case for (TCNum m, TCInf), shoudn't happen
-    (finNumRec
+    (Num_rec_fin
        (\ (n:Num) -> (a:isort 0) -> Stream (SpecM E stack (mseq E stack n a)) ->
           mseq E stack (tcMul TCInf n) a)
        -- Case for (TCInf, TCNum n)
@@ -578,20 +572,20 @@ splitCryM m n a v =
       atCryM (mulNat m n) a v (addNat (mulNat i n) j)));
 
 ecSplitM : (E:EvType) -> (stack:FunStack) ->
-           (m n : Num) -> (a : qisort 0) -> mseq E stack (tcMul m n) a ->\
-           mseq E stack m (mseq E stack n a);
+           (m n : Num) -> isFinite n -> (a : qisort 0) ->
+           mseq E stack (tcMul m n) a -> mseq E stack m (mseq E stack n a);
 ecSplitM E stack =
   Num_rec
-    (\ (m:Num) -> (n:Num) -> (a:qisort 0) -> mseq E stack (tcMul m n) a ->
-       mseq E stack m (mseq E stack n a))
+    (\ (m:Num) -> (n:Num) -> isFinite n -> (a:qisort 0) ->
+       mseq E stack (tcMul m n) a -> mseq E stack m (mseq E stack n a))
     (\ (m:Nat) ->
-       finNumRec
+       Num_rec_fin
          (\ (n:Num) -> (a:qisort 0) -> mseq E stack (tcMul (TCNum m) n) a ->
             Vec m (mseq E stack n a))
          -- Case for (TCNum m, TCNum n)
          (\ (n:Nat) -> \ (a:qisort 0) -> splitCryM m n a))
          -- No case for (TCNum m, TCInf), shouldn't happen
-    (finNumRec
+    (Num_rec_fin
        (\ (n:Num) -> (a:qisort 0) -> mseq E stack (tcMul TCInf n) a ->
           Stream (SpecM E stack (mseq E stack n a)))
        -- Case for (TCInf, TCNum n)
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index e3ef8912be..5511aac4f4 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1287,28 +1287,33 @@ assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args ->
        [specMEvType params, specMStack params,
         toArgType mtp, toArgTerm atrm_cond, toCompTerm mtrm]
 
--- | Make a 'MonMacro' that maps a named global whose first argument is @n:Num@
--- to a global of semi-pure type that takes an additional argument of type
--- @isFinite n@. The 'Bool' flag indicates whether the current 'SpecMParams'
+-- | @finMacro i from to params_p@ makes a 'MonMacro' that maps a named global
+-- @from@ whose @i@th argument is @n:Num@ to a named global @to@ of semi-pure
+-- type that takes an additional argument of type @isFinite n@ as its @(i+1)@th
+-- argument. The @params_p@ flag indicates whether the current 'SpecMParams'
 -- should be passed as the first two arguments to @to@.
-fin1Macro :: Ident -> Ident -> Bool -> MonMacro
-fin1Macro from to params_p =
-  MonMacro 1 $ \glob args -> usingSpecMParams $
-  do if globalDefName glob == ModuleIdentifier from && length args == 1 then
+finMacro :: Int -> Ident -> Ident -> Bool -> MonMacro
+finMacro i from to params_p =
+  MonMacro (i+1) $ \glob args -> usingSpecMParams $
+  do if globalDefName glob == ModuleIdentifier from && length args == i+1 then
        return ()
        else error ("Monadification macro for " ++ show from ++
                    " applied incorrectly")
-     -- Monadify the first arg, n, and build a proof it is finite
-     n_mtp <- monadifyTypeM (head args)
+     -- Monadify the first @i@ args
+     args_mtps <- mapM monadifyTypeM (init args)
+     let args_m = map toArgType args_mtps
+     -- Monadify the @i@th arg, @n:Num@, and build a proof it is finite
+     n_mtp <- monadifyTypeM (last args)
      let n = toArgType n_mtp
      fin_pf <- assertIsFinite n_mtp
-     -- Apply the type of @glob@ to n, and apply @to@ to n and fin_pf
+     -- Apply the type of @glob@ to the monadified arguments and @n@,
+     -- and apply @to@ to the monadified arguments, @n@, and @fin_pf@
      let glob_tp = monadifyType [] $ globalDefType glob
-     let glob_tp_app = applyMonType glob_tp $ Left n_mtp
+     let glob_tp_app = foldl applyMonType glob_tp (map Left (args_mtps ++ [n_mtp]))
      let to_app =
            applyOpenTermMulti (globalOpenTerm to)
            ((if params_p then (paramsToTerms ?specMParams ++) else id)
-            [n, toArgTerm fin_pf])
+            args_m ++ [n, toArgTerm fin_pf])
      -- Finally, return @to n fin_pf@ as a MonTerm of monadified type @to_tp n@
      return $ ArgMonTerm $ fromSemiPureTerm glob_tp_app to_app
 
@@ -1339,10 +1344,10 @@ mmSemiPure from_id to_id params_p =
   (ModuleIdentifier from_id, semiPureGlobalMacro from_id to_id params_p)
 
 -- | Build a 'MacroMapping' for an identifier to a semi-pure named function
--- whose first argument is a @Num@ that requires an @isFinite@ proof
-mmSemiPureFin1 :: Ident -> Ident -> Bool -> MacroMapping
-mmSemiPureFin1 from_id to_id params_p =
-  (ModuleIdentifier from_id, fin1Macro from_id to_id params_p)
+-- whose @i@th argument argument is a @Num@ that requires an @isFinite@ proof
+mmSemiPureFin :: Int -> Ident -> Ident -> Bool -> MacroMapping
+mmSemiPureFin i from_id to_id params_p =
+  (ModuleIdentifier from_id, finMacro i from_id to_id params_p)
 
 -- | Build a 'MacroMapping' for an identifier to itself as a semi-pure function
 mmSelf :: Ident -> MacroMapping
@@ -1392,33 +1397,33 @@ defaultMonTable =
     -- FIXME: continue here...
 
     -- PEq constraints
-  , mmSemiPureFin1 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" True
-  , mmSemiPureFin1 "Cryptol.PEqSeqBool" "CryptolM.PEqMSeqBool" True
+  , mmSemiPureFin 0 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" True
+  , mmSemiPureFin 0 "Cryptol.PEqSeqBool" "CryptolM.PEqMSeqBool" True
 
     -- PCmp constraints
-  , mmSemiPureFin1 "Cryptol.PCmpSeq" "CryptolM.PCmpMSeq" True
-  , mmSemiPureFin1 "Cryptol.PCmpSeqBool" "CryptolM.PCmpMSeqBool" True
+  , mmSemiPureFin 0 "Cryptol.PCmpSeq" "CryptolM.PCmpMSeq" True
+  , mmSemiPureFin 0 "Cryptol.PCmpSeqBool" "CryptolM.PCmpMSeqBool" True
 
     -- PSignedCmp constraints
-  , mmSemiPureFin1 "Cryptol.PSignedCmpSeq" "CryptolM.PSignedCmpMSeq" True
-  , mmSemiPureFin1 "Cryptol.PSignedCmpSeqBool" "CryptolM.PSignedCmpMSeqBool" True
+  , mmSemiPureFin 0 "Cryptol.PSignedCmpSeq" "CryptolM.PSignedCmpMSeq" True
+  , mmSemiPureFin 0 "Cryptol.PSignedCmpSeqBool" "CryptolM.PSignedCmpMSeqBool" True
 
     -- PZero constraints
-  , mmSemiPureFin1 "Cryptol.PZeroSeq" "CryptolM.PZeroMSeq" True
+  , mmSemiPureFin 0 "Cryptol.PZeroSeq" "CryptolM.PZeroMSeq" True
 
     -- PLogic constraints
   , mmSemiPure "Cryptol.PLogicSeq" "CryptolM.PLogicMSeq" True
-  , mmSemiPureFin1 "Cryptol.PLogicSeqBool" "CryptolM.PLogicMSeqBool" True
+  , mmSemiPureFin 0 "Cryptol.PLogicSeqBool" "CryptolM.PLogicMSeqBool" True
 
     -- PRing constraints
   , mmSemiPure "Cryptol.PRingSeq" "CryptolM.PRingMSeq" True
-  , mmSemiPureFin1 "Cryptol.PRingSeqBool" "CryptolM.PRingMSeqBool" True
+  , mmSemiPureFin 0 "Cryptol.PRingSeqBool" "CryptolM.PRingMSeqBool" True
 
     -- PIntegral constraints
-  , mmSemiPureFin1 "Cryptol.PIntegeralSeqBool" "CryptolM.PIntegeralMSeqBool" True
+  , mmSemiPureFin 0 "Cryptol.PIntegeralSeqBool" "CryptolM.PIntegeralMSeqBool" True
 
     -- PLiteral constraints
-  , mmSemiPureFin1 "Cryptol.PLiteralSeqBool" "CryptolM.PLiteralSeqBoolM" True
+  , mmSemiPureFin 0 "Cryptol.PLiteralSeqBool" "CryptolM.PLiteralSeqBoolM" True
 
     -- The Cryptol Literal primitives
   , mmSelf "Cryptol.ecNumber"
@@ -1443,20 +1448,21 @@ defaultMonTable =
   , mmSemiPure "Cryptol.ecShiftL" "CryptolM.ecShiftLM" True
   , mmSemiPure "Cryptol.ecShiftR" "CryptolM.ecShiftRM" True
   , mmSemiPure "Cryptol.ecSShiftR" "CryptolM.ecSShiftRM" True
-  , mmSemiPureFin1 "Cryptol.ecRotL" "CryptolM.ecRotLM" True
-  , mmSemiPureFin1 "Cryptol.ecRotR" "CryptolM.ecRotRM" True
-  , mmSemiPureFin1 "Cryptol.ecCat" "CryptolM.ecCatM" True
+  , mmSemiPureFin 0 "Cryptol.ecRotL" "CryptolM.ecRotLM" True
+  , mmSemiPureFin 0 "Cryptol.ecRotR" "CryptolM.ecRotRM" True
+  , mmSemiPureFin 0 "Cryptol.ecCat" "CryptolM.ecCatM" True
   , mmSemiPure "Cryptol.ecTake" "CryptolM.ecTakeM" True
-  , mmSemiPureFin1 "Cryptol.ecDrop" "CryptolM.ecDropM" True
-  , mmSemiPure "Cryptol.ecJoin" "CryptolM.ecJoinM" True
-  , mmSemiPure "Cryptol.ecSplit" "CryptolM.ecSplitM" True
-  , mmSemiPureFin1 "Cryptol.ecReverse" "CryptolM.ecReverseM" True
+  , mmSemiPureFin 0 "Cryptol.ecDrop" "CryptolM.ecDropM" True
+  , mmSemiPureFin 0 "Cryptol.ecDrop" "CryptolM.ecDropM" True
+  , mmSemiPureFin 1 "Cryptol.ecJoin" "CryptolM.ecJoinM" True
+  , mmSemiPureFin 1 "Cryptol.ecSplit" "CryptolM.ecSplitM" True
+  , mmSemiPureFin 0 "Cryptol.ecReverse" "CryptolM.ecReverseM" True
   , mmSemiPure "Cryptol.ecTranspose" "CryptolM.ecTransposeM" True
   , mmArg "Cryptol.ecAt" "CryptolM.ecAtM" True
   , mmArg "Cryptol.ecUpdate" "CryptolM.ecUpdateM" True
   -- , mmArgFin1 "Cryptol.ecAtBack" "CryptolM.ecAtBackM"
   -- , mmSemiPureFin2 "Cryptol.ecFromTo" "CryptolM.ecFromToM"
-  , mmSemiPureFin1 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM" True
+  , mmSemiPureFin 0 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM" True
   -- , mmSemiPureNthFin 5 "Cryptol.ecFromThenTo" "CryptolM.ecFromThenToM"
   , mmSemiPure "Cryptol.ecInfFrom" "CryptolM.ecInfFromM" True
   , mmSemiPure "Cryptol.ecInfFromThen" "CryptolM.ecInfFromThenM" True
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
index c9921e60b5..00d990f4e3 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
@@ -151,3 +151,63 @@ Proof.
   etransitivity; [ | apply gen_at_BVVec ].
   f_equal; repeat (apply functional_extensionality_dep; intro); eauto.
 Qed.
+
+
+(***
+ *** QuantType Instances
+ ***)
+
+(** Simple QuantType Instances **)
+
+Program Instance QuantType_Bool : QuantType Bool :=
+  { quantEnc := QEnc_nat;
+    quantEnum := fun n => match n with
+                          | 0 => false
+                          | S _ => true
+                          end;
+    quantEnumInv := fun b => if b then 1 else 0 }.
+Next Obligation.
+  destruct a; reflexivity.
+Defined.
+
+
+(** QuantType Vec Instance **)
+
+(* Build the encoding of the N-tuple of a given encoding *)
+Fixpoint QEnc_NTuple n (qenc : QuantEnc) : QuantEnc :=
+  match n with
+  | 0 => QEnc_prop True
+  | S n' => QEnc_pair qenc (QEnc_NTuple n' qenc)
+  end.
+
+(* The quantEnum function for Vec n a *)
+Definition quantEnum_Vec n A `{QuantType A} :
+  encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A :=
+  nat_rect
+    (fun n => encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A)
+    (fun _ => VectorDef.nil _)
+    (fun n enumF x => VectorDef.cons _ (quantEnum (fst x)) _ (enumF (snd x)))
+    n.
+
+(* The quantEnumInv function for Vec n a *)
+Definition quantEnumInv_Vec n A `{QuantType A} :
+  Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))) :=
+  nat_rect
+    (fun n => Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))))
+    (fun _ => I)
+    (fun n enumInvF x => (quantEnumInv (VectorDef.hd x), enumInvF (VectorDef.tl x)))
+    n.
+
+Program Instance QuantType_Vec n A `{QuantType A} : QuantType (Vec n A) :=
+  { quantEnc := QEnc_NTuple n (quantEnc (A:=A));
+    quantEnum := quantEnum_Vec n A;
+    quantEnumInv := quantEnumInv_Vec n A }.
+Next Obligation.
+  induction a.
+  - reflexivity.
+  - simpl. rewrite quantEnumSurjective. rewrite IHa. reflexivity.
+Defined.
+
+Program Instance QuantType_bitvector w : QuantType (bitvector w) :=
+  QuantType_Vec w _.
+
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SpecMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SpecMExtra.v
index 9991bd5d93..9ffbe67deb 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SpecMExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SpecMExtra.v
@@ -14,64 +14,6 @@ From EnTree Require Export
 Import SAWCorePrelude.
 
 
-(***
- *** QuantType Instances
- ***)
-
-(** Simple QuantType Instances **)
-
-Program Instance QuantType_Bool : QuantType Bool :=
-  { quantEnc := QEnc_nat;
-    quantEnum := fun n => match n with
-                          | 0 => false
-                          | S _ => true
-                          end;
-    quantEnumInv := fun b => if b then 1 else 0 }.
-Next Obligation.
-  destruct a; reflexivity.
-Defined.
-
-
-(** QuantType Vec Instance **)
-
-(* Build the encoding of the N-tuple of a given encoding *)
-Fixpoint QEnc_NTuple n (qenc : QuantEnc) : QuantEnc :=
-  match n with
-  | 0 => QEnc_prop True
-  | S n' => QEnc_pair qenc (QEnc_NTuple n' qenc)
-  end.
-
-(* The quantEnum function for Vec n a *)
-Definition quantEnum_Vec n A `{QuantType A} :
-  encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A :=
-  nat_rect
-    (fun n => encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A)
-    (fun _ => VectorDef.nil _)
-    (fun n enumF x => VectorDef.cons _ (quantEnum (fst x)) _ (enumF (snd x)))
-    n.
-
-(* The quantEnumInv function for Vec n a *)
-Definition quantEnumInv_Vec n A `{QuantType A} :
-  Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))) :=
-  nat_rect
-    (fun n => Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))))
-    (fun _ => I)
-    (fun n enumInvF x => (quantEnumInv (VectorDef.hd x), enumInvF (VectorDef.tl x)))
-    n.
-
-Program Instance QuantType_Vec n A `{QuantType A} : QuantType (Vec n A) :=
-  { quantEnc := QEnc_NTuple n (quantEnc (A:=A));
-    quantEnum := quantEnum_Vec n A;
-    quantEnumInv := quantEnumInv_Vec n A }.
-Next Obligation.
-  induction a.
-  - reflexivity.
-  - simpl. rewrite quantEnumSurjective. rewrite IHa. reflexivity.
-Defined.
-
-Program Instance QuantType_bitvector w : QuantType (bitvector w) :=
-  QuantType_Vec w _.
-
 
 (***
  *** Additional Automation
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index c42662dcd1..a7c4f7ad53 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -547,12 +547,14 @@ writeCoqCryptolPrimitivesForSAWCore outputFile outputFileM notations skips = do
         withImportSAWCorePreludeExtra $
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
+  let configuration_mon =
+        withImportCryptolPrimitivesForSAWCore configuration
   let doc = Coq.translateSAWModule configuration m
   writeFile outputFile (show . vcat $ [ Coq.preamble configuration
                                       , doc
                                       ])
-  let doc_mon = Coq.translateSAWModule configuration m_mon
-  writeFile outputFileM (show . vcat $ [ Coq.preamble configuration
+  let doc_mon = Coq.translateSAWModule configuration_mon m_mon
+  writeFile outputFileM (show . vcat $ [ Coq.preamble configuration_mon
                                        , doc_mon
                                        ])
 

From 435f7fcbba6c99f5953da98c625980d75d29d839 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 9 Mar 2023 18:12:23 -0500
Subject: [PATCH 08/19] implement ecTakeM

---
 cryptol-saw-core/saw/CryptolM.sawcore         | 45 +++++++++++++------
 .../src/Verifier/SAW/Cryptol/Monadify.hs      |  2 +-
 2 files changed, 33 insertions(+), 14 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index 70a1c93dda..370605ddf9 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -190,6 +190,12 @@ seqToMseq E stack n_top a =
           (streamMap a (SpecM E stack a) (retS E stack a))
           n_top;
 
+vecSequenceM : (E:EvType) -> (stack:FunStack) ->
+               (a : qsort 0) -> (n : Nat) ->
+               Vec n (SpecM E stack a) -> SpecM E stack (Vec n a);
+vecSequenceM E stack a n =
+  vecMapM E stack (SpecM E stack a) a n (\(i:Nat) (x:SpecM E stack a) -> x);
+
 
 --------------------------------------------------------------------------------
 -- Auxiliary functions
@@ -506,18 +512,32 @@ ecCatM E stack =
             streamAppend (SpecM E stack a) m
                          (map a (SpecM E stack a) (retS E stack a) m v)));
 
--- FIXME
-primitive
 ecTakeM : (E:EvType) -> (stack:FunStack) ->
-          (m n : Num) -> (a : sort 0) -> mseq E stack (tcAdd m n) a ->
-          mseq E stack m a;
-{-
-ecTakeM =
-  Num_rec (\ (m:Num) -> (n:Num) -> (a:sort 0) -> mseq (tcAdd m n) a -> mseq m a)
-          (\ (m:Nat) -> ecTake (TCNum m))
-          (\ (n:Num) (a:sort 0) (s:Stream (CompM a)) ->
-             ecTake TCInf n (CompM a) s);
--}
+          (m n : Num) -> (a : qisort 0) -> mseq E stack (tcAdd m n) a ->
+          SpecM E stack (mseq E stack m a);
+ecTakeM E stack =
+  Num_rec
+    (\ (m:Num) -> (n:Num) -> (a:qisort 0) -> mseq E stack (tcAdd m n) a ->
+       SpecM E stack (mseq E stack m a))
+    (\ (m:Nat) ->
+       Num_rec
+         (\ (n:Num) -> (a:qisort 0) -> mseq E stack (tcAdd (TCNum m) n) a ->
+            SpecM E stack (Vec m a))
+         -- The case (TCNum m, TCNum n)
+         (\ (n:Nat) -> \ (a:qisort 0) -> \ (xs: Vec (addNat m n) a) ->
+            retS E stack (Vec m a) (take a m n xs))
+         -- The case (TCNum m, infinity)
+         (\ (a:qisort 0) -> \ (xs: Stream (SpecM E stack a)) ->
+            vecSequenceM E stack a m (streamTake (SpecM E stack a) m xs)))
+    (Num_rec
+      (\ (n:Num) -> (a:qisort 0) -> mseq E stack (tcAdd TCInf n) a ->
+         SpecM E stack (Stream (SpecM E stack a)))
+        -- The case (TCInf, TCNum n)
+        (\ (n:Nat) -> \ (a:qisort 0) -> \ (xs:Stream (SpecM E stack a)) ->
+           retS E stack (Stream (SpecM E stack a)) xs)
+        -- The case (TCInf, TCInf)
+        (\ (a:qisort 0) -> \ (xs:Stream (SpecM E stack a)) ->
+           retS E stack (Stream (SpecM E stack a)) xs));
 
 -- An alternate version of join from Prelude to get around the default Prim
 joinCryM : (m n : Nat) -> (a : isort 0) ->
@@ -599,8 +619,7 @@ ecSplitM E stack =
             (\ (n':Nat) (xs : Stream (SpecM E stack a)) -> 
                streamMap (Vec (Succ n') (SpecM E stack a))
                          (SpecM E stack (Vec (Succ n') a))
-                         (vecMapM E stack (SpecM E stack a) a (Succ n')
-                                  (\(i:Nat) (x:SpecM E stack a) -> x))
+                         (vecSequenceM E stack a (Succ n'))
                          (streamSplit (SpecM E stack a) (Succ n') xs))
             n));
        -- No case for (TCInf, TCInf), shouldn't happen
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index 5511aac4f4..e28ff89123 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1451,7 +1451,7 @@ defaultMonTable =
   , mmSemiPureFin 0 "Cryptol.ecRotL" "CryptolM.ecRotLM" True
   , mmSemiPureFin 0 "Cryptol.ecRotR" "CryptolM.ecRotRM" True
   , mmSemiPureFin 0 "Cryptol.ecCat" "CryptolM.ecCatM" True
-  , mmSemiPure "Cryptol.ecTake" "CryptolM.ecTakeM" True
+  , mmArg "Cryptol.ecTake" "CryptolM.ecTakeM" True
   , mmSemiPureFin 0 "Cryptol.ecDrop" "CryptolM.ecDropM" True
   , mmSemiPureFin 0 "Cryptol.ecDrop" "CryptolM.ecDropM" True
   , mmSemiPureFin 1 "Cryptol.ecJoin" "CryptolM.ecJoinM" True

From 1e46b2e53aaf46c2157230e0c78b755430de17fb Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Mon, 13 Mar 2023 11:04:45 -0400
Subject: [PATCH 09/19] implement ecDropM

---
 cryptol-saw-core/saw/CryptolM.sawcore | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index 370605ddf9..9a9c991a8a 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -539,6 +539,20 @@ ecTakeM E stack =
         (\ (a:qisort 0) -> \ (xs:Stream (SpecM E stack a)) ->
            retS E stack (Stream (SpecM E stack a)) xs));
 
+ecDropM : (E:EvType) -> (stack:FunStack) ->
+          (m : Num) -> isFinite m -> (n : Num) -> (a : isort 0) ->
+          mseq E stack (tcAdd m n) a -> mseq E stack n a;
+ecDropM E stack =
+  Num_rec_fin
+    (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq E stack (tcAdd m n) a -> mseq E stack n a)
+    (\ (m:Nat) ->
+       Num_rec
+         (\ (n:Num) -> (a:isort 0) -> mseq E stack (tcAdd (TCNum m) n) a -> mseq E stack n a)
+         -- The case (TCNum m, TCNum n)
+         (\ (n:Nat) -> \ (a:isort 0) -> drop a m n)
+         -- The case (TCNum m, infinity)
+         (\ (a:isort 0) -> streamDrop (SpecM E stack a) m));
+
 -- An alternate version of join from Prelude to get around the default Prim
 joinCryM : (m n : Nat) -> (a : isort 0) ->
            Vec m (Vec n a) -> Vec (mulNat m n) a;
@@ -546,12 +560,6 @@ joinCryM m n a v =
   genCryM (mulNat m n) a (\ (i : Nat) ->
     atCryM n a (at m (Vec n a) v (divNat i n)) (modNat i n));
 
--- FIXME
-primitive
-ecDropM : (E:EvType) -> (stack:FunStack) ->
-          (m : Num) -> isFinite m -> (n : Num) -> (a : sort 0) ->
-          mseq E stack (tcAdd m n) a -> mseq E stack n a;
-
 ecJoinM : (E:EvType) -> (stack:FunStack) -> 
           (m n : Num) -> isFinite n -> (a : isort 0) ->
           mseq E stack m (mseq E stack n a) -> mseq E stack (tcMul m n) a;

From 2bff6581b4a350ded0d5520bbb16971a0f22b67b Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 16 Mar 2023 12:04:12 -0400
Subject: [PATCH 10/19] finish implementing monadic list comprehension
 primitives

---
 cryptol-saw-core/saw/CryptolM.sawcore         | 182 +++++++++++++++---
 .../src/Verifier/SAW/Cryptol/Monadify.hs      |   3 +-
 2 files changed, 153 insertions(+), 32 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index 9a9c991a8a..2faef1d11d 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -12,6 +12,27 @@ genCryM = gen;
 atCryM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a;
 atCryM = at;
 
+-- Alternate versions of Prelude functions, changed to use genCryM and atCryM
+
+joinCryM : (m n : Nat) -> (a : isort 0) ->
+           Vec m (Vec n a) -> Vec (mulNat m n) a;
+joinCryM m n a v =
+  genCryM (mulNat m n) a (\ (i : Nat) ->
+    atCryM n a (at m (Vec n a) v (divNat i n)) (modNat i n));
+
+zipCryM : (a b : isort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
+zipCryM a b m n xs ys =
+  genCryM (minNat m n) (a * b) (\ (i:Nat) -> (atCryM m a xs i, atCryM n b ys i));
+
+splitCryM : (m n : Nat) -> (a : isort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
+splitCryM m n a v =
+  genCryM m (Vec n a) (\ (i : Nat) ->
+    genCryM n a (\ (j : Nat) ->
+      atCryM (mulNat m n) a v (addNat (mulNat i n) j)));
+
+zipSameM : (a b : isort 0) -> (n : Nat) -> Vec n a -> Vec n b -> Vec n (a * b);
+zipSameM a b n x y = genCryM n (a*b) (\ (i : Nat) -> (atCryM n a x i, atCryM n b y i));
+
 
 --------------------------------------------------------------------------------
 -- Monadic assertions
@@ -156,6 +177,13 @@ vecMapInvarM : (E:EvType) -> (stack:FunStack) ->
 vecMapInvarM E stack a b n f xs invar =
   vecMapInvarBindM E stack a b (Vec n b) n f xs invar (retS E stack (Vec n b));
 
+vecMapBindM : (E:EvType) -> (stack:FunStack) ->
+              (a : sort 0) -> (b : qsort 0) -> (c : sort 0) ->
+              (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
+              Vec n a -> (Vec n b -> SpecM E stack c) ->
+              SpecM E stack c;
+vecMapBindM E stack a b c n f xs = vecMapInvarBindM E stack a b c n f xs True;
+
 vecMapM : (E:EvType) -> (stack:FunStack) ->
           (a : sort 0) -> (b : qsort 0) ->
           (n : Nat) -> (Nat -> a -> SpecM E stack b) ->
@@ -257,28 +285,126 @@ eListSelM E stack a =
           (\ (n:Nat) -> atM E stack n a)
           (streamGet (SpecM E stack a));
 
+streamJoinM : (E:EvType) -> (stack:FunStack) ->
+              (a : isort 0) -> (n : Nat) ->
+              Stream (SpecM E stack (Vec (Succ n) a)) ->
+              Stream (SpecM E stack a);
+streamJoinM E stack a n s =
+  MkStream (SpecM E stack a) (\ (i:Nat) ->
+     fmapS E stack (Vec (Succ n) a) a
+       (\ (xs:Vec (Succ n) a) -> at (Succ n) a xs (modNat i (Succ n)))
+       (streamGet (SpecM E stack (Vec (Succ n) a)) s
+                  (divNat i (Succ n))) );
+
 
 --------------------------------------------------------------------------------
 -- List comprehensions
 
--- FIXME
-primitive
 fromM : (E:EvType) -> (stack:FunStack) ->
-        (a b : sort 0) -> (m n : Num) -> mseq E stack m a ->
+        (a b : qisort 0) -> (m n : Num) -> mseq E stack m a ->
         (a -> SpecM E stack (mseq E stack n b)) ->
-        SpecM E stack (seq (tcMul m n) (a * b));
+        SpecM E stack (mseq E stack (tcMul m n) (a * b));
+fromM E stack a b m n =
+  Num_rec
+    (\ (m:Num) -> mseq E stack m a ->
+       (a -> SpecM E stack (mseq E stack n b)) ->
+       SpecM E stack (mseq E stack (tcMul m n) (a * b)))
+    (\ (m:Nat) ->
+       Num_rec
+         (\ (n:Num) -> Vec m a ->
+            (a -> SpecM E stack (mseq E stack n b)) ->
+            SpecM E stack (mseq E stack (tcMul (TCNum m) n) (a * b)))
+         -- Case 1: (TCNum m, TCNum n)
+         (\ (n:Nat) ->
+            \ (xs : Vec m a) ->
+            \ (k : a -> SpecM E stack (Vec n b)) ->
+              vecMapBindM E stack a (Vec n (a * b))
+                (Vec (mulNat m n) (a * b)) m
+                (\ (i:Nat) -> \ (x:a) -> 
+                   fmapS E stack (Vec n b) (Vec n (a * b))
+                     (map b (a * b) (\ (y : b) -> (x, y)) n) (k x))
+                xs (\ (kxs:Vec m (Vec n (a * b))) ->
+                      retS E stack (Vec (mulNat m n) (a * b))
+                        (joinCryM m n (a * b) kxs)))
+         -- Case 2: n = (TCNum m, TCInf)
+         (natCase
+            (\ (m':Nat) -> Vec m' a ->
+               (a -> SpecM E stack (Stream (SpecM E stack b))) ->
+               SpecM E stack (mseq E stack (if0Nat Num m' (TCNum 0) TCInf) (a * b)))
+            (\ (xs : Vec 0 a) ->
+             \ (k : a -> SpecM E stack (Stream (SpecM E stack b))) ->
+               retS E stack (Vec 0 (a * b)) (EmptyVec (a * b)))
+            (\ (m' : Nat) ->
+             \ (xs : Vec (Succ m') a) ->
+             \ (k : a -> SpecM E stack (Stream (SpecM E stack b))) ->
+               (\ (x:a) ->
+                  fmapS E stack (Stream (SpecM E stack b)) (Stream (SpecM E stack (a * b)))
+                    (streamMap (SpecM E stack b) (SpecM E stack (a * b))
+                       (fmapS E stack b (a * b) (\ (y:b) -> (x, y))))
+                    (k x))
+               (head m' a xs))
+            m)
+         n)
+    (Num_rec
+       (\ (n:Num) -> Stream (SpecM E stack a) ->
+          (a -> SpecM E stack (mseq E stack n b)) ->
+          SpecM E stack (mseq E stack (tcMul TCInf n) (a * b)))
+       -- Case 3: (TCInf, TCNum n)
+       (\ (n:Nat) ->
+          natCase
+            (\ (n':Nat) -> Stream (SpecM E stack a) ->
+               (a -> SpecM E stack (Vec n' b)) ->
+               SpecM E stack (mseq E stack (if0Nat Num n' (TCNum 0) TCInf) (a * b)))
+            (\ (xs : Stream (SpecM E stack a)) ->
+             \ (k : a -> SpecM E stack (Vec 0 b)) ->
+               retS E stack (Vec 0 (a * b)) (EmptyVec (a * b)))
+            (\ (n' : Nat) ->
+             \ (xs : Stream (SpecM E stack a)) ->
+             \ (k : a -> SpecM E stack (Vec (Succ n') b)) ->
+               retS E stack (Stream (SpecM E stack (a * b)))
+                 (streamJoinM E stack (a * b) n'
+                    (streamMap (SpecM E stack a)
+                       (SpecM E stack (Vec (Succ n') (a * b)))
+                       (\ (m:SpecM E stack a) ->
+                          bindS E stack a (Vec (Succ n') (a * b)) m
+                            (\ (x:a) ->
+                               fmapS E stack (Vec (Succ n') b) (Vec (Succ n') (a * b))
+                                 (map b (a * b) (\ (y:b) -> (x, y)) (Succ n'))
+                                 (k x)))
+                       xs)))
+            n)
+       -- Case 4: (TCInf, TCInf)
+       (\ (xs : Stream (SpecM E stack a)) ->
+        \ (k : a -> SpecM E stack (Stream (SpecM E stack b))) ->
+          bindS E stack a (Stream (SpecM E stack (a * b)))
+            (streamGet (SpecM E stack a) xs 0)
+            (\ (x:a) ->
+               fmapS E stack (Stream (SpecM E stack b)) (Stream (SpecM E stack (a * b)))
+                 (streamMap (SpecM E stack b) (SpecM E stack (a * b))
+                    (fmapS E stack b (a * b) (\ (y:b) -> (x, y))))
+                 (k x)))
+       n)
+    m;
 
--- FIXME
-primitive
 mletM : (E:EvType) -> (stack:FunStack) ->
-        (a b : sort 0) -> (n : Num) -> a ->
+        (a : sort 0) -> (b : isort 0) -> (n : Num) -> a ->
         (a -> SpecM E stack (mseq E stack n b)) ->
         SpecM E stack (mseq E stack n (a * b));
-
--- An alternate version of zip from Prelude to get around the default Prim
-zipCryM : (a b : isort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
-zipCryM a b m n xs ys =
-  genCryM (minNat m n) (a * b) (\ (i:Nat) -> (atCryM m a xs i, atCryM n b ys i));
+mletM E stack a b n =
+  Num_rec
+    (\ (n:Num) -> a ->
+       (a -> SpecM E stack (mseq E stack n b)) ->
+       SpecM E stack (mseq E stack n (a * b)))
+    (\ (n:Nat) -> \ (x:a) -> \ (f:a -> SpecM E stack (Vec n b)) ->
+       fmapS E stack (Vec n b) (Vec n (a * b))
+         (map b (a * b) (\ (y : b) -> (x, y)) n)
+         (f x))
+    (\ (x:a) -> \ (f:a -> SpecM E stack (Stream (SpecM E stack b))) ->
+       fmapS E stack (Stream (SpecM E stack b)) (Stream (SpecM E stack (a * b)))
+         (streamMap (SpecM E stack b) (SpecM E stack (a * b))
+            (fmapS E stack b (a * b) (\ (y:b) -> (x, y))))
+         (f x))
+    n;
 
 seqZipM : (E:EvType) -> (stack:FunStack) ->
           (a b : qisort 0) -> (m n : Num) ->
@@ -320,6 +446,18 @@ seqZipM E stack a b m n =
        n)
     m;
 
+seqZipSameM : (E:EvType) -> (stack:FunStack) ->
+              (a b : isort 0) -> (n : Num) ->
+              mseq E stack n a -> mseq E stack n b ->
+              mseq E stack n (a * b);
+seqZipSameM E stack a b n =
+  Num_rec
+    (\ (n : Num) -> mseq E stack n a -> mseq E stack n b -> mseq E stack n (a * b))
+    (\ (n : Nat) -> zipSameM a b n)
+    (streamMap2 (SpecM E stack a) (SpecM E stack b) (SpecM E stack (a * b))
+       (fmapS2 E stack a b (a * b) (\ (x:a) -> \ (y:b) -> (x,y))))
+    n;
+
 
 --------------------------------------------------------------------------------
 -- Monadic versions of the Cryptol typeclass instances
@@ -553,13 +691,6 @@ ecDropM E stack =
          -- The case (TCNum m, infinity)
          (\ (a:isort 0) -> streamDrop (SpecM E stack a) m));
 
--- An alternate version of join from Prelude to get around the default Prim
-joinCryM : (m n : Nat) -> (a : isort 0) ->
-           Vec m (Vec n a) -> Vec (mulNat m n) a;
-joinCryM m n a v =
-  genCryM (mulNat m n) a (\ (i : Nat) ->
-    atCryM n a (at m (Vec n a) v (divNat i n)) (modNat i n));
-
 ecJoinM : (E:EvType) -> (stack:FunStack) -> 
           (m n : Num) -> isFinite n -> (a : isort 0) ->
           mseq E stack m (mseq E stack n a) -> mseq E stack (tcMul m n) a;
@@ -584,21 +715,10 @@ ecJoinM E stack =
                mseq E stack (if0Nat Num n' (TCNum 0) TCInf) a)
             (\ (s:Stream (SpecM E stack (Vec 0 a))) -> EmptyVec a)
             (\ (n':Nat) -> \ (s:Stream (SpecM E stack (Vec (Succ n') a))) ->
-               MkStream (SpecM E stack a) (\ (i:Nat) ->
-                  fmapS E stack (Vec (Succ n') a) a
-                    (\ (v:Vec (Succ n') a) -> at (Succ n') a v (modNat i (Succ n')))
-                    (streamGet (SpecM E stack (Vec (Succ n') a)) s
-                               (divNat i (Succ n'))) ))
+               streamJoinM E stack a n' s)
             n));
        -- No case for (TCInf, TCInf), shouldn't happen
 
--- An alternate version of split from Prelude to get around the default Prim
-splitCryM : (m n : Nat) -> (a : isort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
-splitCryM m n a v =
-  genCryM m (Vec n a) (\ (i : Nat) ->
-    genCryM n a (\ (j : Nat) ->
-      atCryM (mulNat m n) a v (addNat (mulNat i n) j)));
-
 ecSplitM : (E:EvType) -> (stack:FunStack) ->
            (m n : Num) -> isFinite n -> (a : qisort 0) ->
            mseq E stack (tcMul m n) a -> mseq E stack m (mseq E stack n a);
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index e28ff89123..60b38bf1bb 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1393,8 +1393,9 @@ defaultMonTable =
 
     -- List comprehensions
   , mmArg "Cryptol.from" "CryptolM.fromM" True
+  , mmArg "Cryptol.mlet" "CryptolM.mletM" True
   , mmArg "Cryptol.seqZip" "CryptolM.seqZipM" True
-    -- FIXME: continue here...
+  , mmSemiPure "Cryptol.seqZipSame" "CryptolM.seqZipSameM" True
 
     -- PEq constraints
   , mmSemiPureFin 0 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" True

From 4f8a2408bd7871658b106e450347cbd7dd248174 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 16 Mar 2023 14:18:26 -0400
Subject: [PATCH 11/19] generalize finMacro, implement ecFromToM, etc.

---
 cryptol-saw-core/saw/CryptolM.sawcore         |  66 ++++++++---
 .../src/Verifier/SAW/Cryptol/Monadify.hs      | 110 ++++++++++--------
 2 files changed, 113 insertions(+), 63 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index 2faef1d11d..a63d26d26a 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -30,8 +30,12 @@ splitCryM m n a v =
     genCryM n a (\ (j : Nat) ->
       atCryM (mulNat m n) a v (addNat (mulNat i n) j)));
 
-zipSameM : (a b : isort 0) -> (n : Nat) -> Vec n a -> Vec n b -> Vec n (a * b);
-zipSameM a b n x y = genCryM n (a*b) (\ (i : Nat) -> (atCryM n a x i, atCryM n b y i));
+zipSameCryM : (a b : isort 0) -> (n : Nat) -> Vec n a -> Vec n b -> Vec n (a * b);
+zipSameCryM a b n x y = genCryM n (a*b) (\ (i : Nat) -> (atCryM n a x i, atCryM n b y i));
+
+reverseCryM : (n : Nat) -> (a : isort 0) -> Vec n a -> Vec n a;
+reverseCryM n a xs = genCryM n a (\ (i : Nat) -> atCryM n a xs (subNat (subNat n 1) i));
+
 
 
 --------------------------------------------------------------------------------
@@ -453,7 +457,7 @@ seqZipSameM : (E:EvType) -> (stack:FunStack) ->
 seqZipSameM E stack a b n =
   Num_rec
     (\ (n : Num) -> mseq E stack n a -> mseq E stack n b -> mseq E stack n (a * b))
-    (\ (n : Nat) -> zipSameM a b n)
+    (\ (n : Nat) -> zipSameCryM a b n)
     (streamMap2 (SpecM E stack a) (SpecM E stack b) (SpecM E stack (a * b))
        (fmapS2 E stack a b (a * b) (\ (x:a) -> \ (y:b) -> (x,y))))
     n;
@@ -757,7 +761,7 @@ ecReverseM : (E:EvType) -> (stack:FunStack) ->
              mseq E stack n a;
 ecReverseM E stack =
   Num_rec_fin (\ (n:Num) -> (a : isort 0) -> mseq E stack n a -> mseq E stack n a)
-              (\ (n:Nat) -> ecReverse (TCNum n));
+              (\ (n:Nat) -> reverseCryM n);
 
 -- FIXME
 primitive
@@ -803,32 +807,64 @@ ecUpdateM E stack n_top a ix pix =
                                             "ecUpdateM: invalid sequence index") i)
     n_top;
 
--- FIXME
-primitive
 ecAtBackM : (E:EvType) -> (stack:FunStack) ->
-            (n : Num) -> isFinite n -> (a ix : sort 0) -> PIntegral ix ->
+            (n : Num) -> isFinite n -> (a : isort 0) ->
+            (ix : sort 0) -> PIntegral ix ->
             mseq E stack n a -> ix -> SpecM E stack a;
+ecAtBackM E stack n pf a ix pix xs =
+  ecAtM E stack n a ix pix (ecReverseM E stack n pf a xs);
 
--- FIXME
-primitive
 ecFromToM : (E:EvType) -> (stack:FunStack) ->
             (first : Num) -> isFinite first -> (last : Num) -> isFinite last ->
-            (a : isort 0) -> PLiteral a ->
+            (a : sort 0) -> PLiteral a ->
             mseq E stack (tcAdd (TCNum 1) (tcSub last first)) a;
+ecFromToM E stack =
+  Num_rec_fin
+    (\ (first:Num) -> (last:Num) -> isFinite last ->
+       (a : sort 0) -> PLiteral a ->
+       mseq E stack (tcAdd (TCNum 1) (tcSub last first)) a)
+    (\ (first:Nat) ->
+       Num_rec_fin
+         (\ (last:Num) -> (a : sort 0) -> PLiteral a ->
+            mseq E stack (tcAdd (TCNum 1) (tcSub last (TCNum first))) a)
+         (\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
+            genCryM (addNat 1 (subNat last first)) a
+                    (\ (i : Nat) -> pa (addNat i first))));
 
--- FIXME
-primitive
 ecFromToLessThanM : (E:EvType) -> (stack:FunStack) ->
                     (first : Num) -> isFinite first -> (bound : Num) ->
-                    (a : isort 0) -> PLiteralLessThan a ->
+                    (a : sort 0) -> PLiteralLessThan a ->
                     mseq E stack (tcSub bound first) a;
+ecFromToLessThanM E stack first pf bound a =
+  Num_rec_fin
+    (\ (first:Num) -> PLiteralLessThan a ->
+       mseq E stack (tcSub bound first) a)
+    (\ (first:Nat) ->
+       Num_rec
+         (\ (bound:Num) -> PLiteralLessThan a ->
+            mseq E stack (tcSub bound (TCNum first)) a)
+         (\ (bound:Nat) -> \ (pa : PLiteralLessThan a) ->
+            genCryM (subNat bound first) a
+                    (\ (i : Nat) -> pa (addNat i first)))
+         (\ (pa : PLiteralLessThan a) ->
+            MkStream (SpecM E stack a)
+                     (\ (i : Nat) -> retS E stack a (pa (addNat i first))))
+         bound)
+    first pf;
 
--- FIXME
-primitive
 ecFromThenToM :
   (E:EvType) -> (stack:FunStack) ->
   (first next last : Num) -> (a : sort 0) -> (len : Num) -> isFinite len ->
   PLiteral a -> PLiteral a -> PLiteral a -> mseq E stack len a;
+ecFromThenToM E stack first next _ a =
+  Num_rec_fin
+    (\ (len:Num) -> PLiteral a -> PLiteral a -> PLiteral a -> mseq E stack len a)
+    (\ (len:Nat) -> \ (pa : PLiteral a) -> \ (_ : PLiteral a) -> \ (_ : PLiteral a) ->
+       genCryM len a
+               (\ (i : Nat) ->
+                  pa (subNat (addNat (getFinNat first)
+                                     (mulNat i (getFinNat next)))
+                             (mulNat i (getFinNat first)))));
 
 ecInfFromM : (E:EvType) -> (stack:FunStack) ->
              (a : sort 0) -> PIntegral a -> a -> mseq E stack TCInf a;
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
index 60b38bf1bb..2e549a0969 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
@@ -1287,35 +1287,40 @@ assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args ->
        [specMEvType params, specMStack params,
         toArgType mtp, toArgTerm atrm_cond, toCompTerm mtrm]
 
--- | @finMacro i from to params_p@ makes a 'MonMacro' that maps a named global
--- @from@ whose @i@th argument is @n:Num@ to a named global @to@ of semi-pure
--- type that takes an additional argument of type @isFinite n@ as its @(i+1)@th
--- argument. The @params_p@ flag indicates whether the current 'SpecMParams'
--- should be passed as the first two arguments to @to@.
-finMacro :: Int -> Ident -> Ident -> Bool -> MonMacro
-finMacro i from to params_p =
-  MonMacro (i+1) $ \glob args -> usingSpecMParams $
-  do if globalDefName glob == ModuleIdentifier from && length args == i+1 then
+-- | @finMacro b i j from to params_p@ makes a 'MonMacro' that maps a named
+-- global @from@ whose @i@th through @(i+j-1)@th arguments are @Num@s, to a
+-- named global @to@, which is of semi-pure type if and only if @b@ is 'True',
+-- that takes an additional argument of type @isFinite n@ after each of the
+-- aforementioned @Num@ arguments. The @params_p@ flag indicates whether the
+-- current 'SpecMParams' should be passed as the first two arguments to @to@.
+finMacro :: Bool -> Int -> Int -> Ident -> Ident -> Bool -> MonMacro
+finMacro isSemiPure i j from to params_p =
+  MonMacro (i+j) $ \glob args -> usingSpecMParams $
+  do if globalDefName glob == ModuleIdentifier from && length args == i+j then
        return ()
        else error ("Monadification macro for " ++ show from ++
                    " applied incorrectly")
+     let (init_args, fin_args) = splitAt i args
      -- Monadify the first @i@ args
-     args_mtps <- mapM monadifyTypeM (init args)
-     let args_m = map toArgType args_mtps
-     -- Monadify the @i@th arg, @n:Num@, and build a proof it is finite
-     n_mtp <- monadifyTypeM (last args)
-     let n = toArgType n_mtp
-     fin_pf <- assertIsFinite n_mtp
-     -- Apply the type of @glob@ to the monadified arguments and @n@,
-     -- and apply @to@ to the monadified arguments, @n@, and @fin_pf@
+     init_args_mtps <- mapM monadifyTypeM init_args
+     let init_args_m = map toArgType init_args_mtps
+     -- Monadify the @i@th through @(i+j-1)@th args and build proofs that they are finite
+     fin_args_mtps <- mapM monadifyTypeM fin_args
+     let fin_args_m = map toArgType fin_args_mtps
+     fin_pfs <- mapM assertIsFinite fin_args_mtps
+     -- Apply the type of @glob@ to the monadified arguments and apply @to@ to the
+     -- monadified arguments along with the proofs that the latter arguments are finite
      let glob_tp = monadifyType [] $ globalDefType glob
-     let glob_tp_app = foldl applyMonType glob_tp (map Left (args_mtps ++ [n_mtp]))
+     let glob_tp_app = foldl applyMonType glob_tp (map Left (init_args_mtps ++ fin_args_mtps))
      let to_app =
            applyOpenTermMulti (globalOpenTerm to)
            ((if params_p then (paramsToTerms ?specMParams ++) else id)
-            args_m ++ [n, toArgTerm fin_pf])
-     -- Finally, return @to n fin_pf@ as a MonTerm of monadified type @to_tp n@
-     return $ ArgMonTerm $ fromSemiPureTerm glob_tp_app to_app
+            init_args_m ++ concatMap (\(n,pf) -> [n, toArgTerm pf]) (zip fin_args_m fin_pfs))
+     -- Finally, return the result as semi-pure dependent on @isSemiPure@
+     return $ if isSemiPure
+              then ArgMonTerm $ fromSemiPureTerm glob_tp_app to_app
+              else ArgMonTerm $ (if params_p then id else liftCompStack)
+                              $ fromArgTerm glob_tp_app to_app
 
 -- | The macro for fix
 --
@@ -1344,10 +1349,11 @@ mmSemiPure from_id to_id params_p =
   (ModuleIdentifier from_id, semiPureGlobalMacro from_id to_id params_p)
 
 -- | Build a 'MacroMapping' for an identifier to a semi-pure named function
--- whose @i@th argument argument is a @Num@ that requires an @isFinite@ proof
-mmSemiPureFin :: Int -> Ident -> Ident -> Bool -> MacroMapping
-mmSemiPureFin i from_id to_id params_p =
-  (ModuleIdentifier from_id, finMacro i from_id to_id params_p)
+-- whose @i@th through @(i+j-1)@th arguments are @Num@s that require
+-- @isFinite@ proofs
+mmSemiPureFin :: Int -> Int -> Ident -> Ident -> Bool -> MacroMapping
+mmSemiPureFin i j from_id to_id params_p =
+  (ModuleIdentifier from_id, finMacro True i j from_id to_id params_p)
 
 -- | Build a 'MacroMapping' for an identifier to itself as a semi-pure function
 mmSelf :: Ident -> MacroMapping
@@ -1362,6 +1368,14 @@ mmArg from_id to_id params_p =
   (ModuleIdentifier from_id,
    argGlobalMacro (ModuleIdentifier from_id) to_id params_p)
 
+-- | Build a 'MacroMapping' for an identifier to a function of argument type,
+-- whose @i@th through @(i+j-1)@th arguments are @Num@s that require
+-- @isFinite@ proofs, where the 'Bool' flag indicates whether the current
+-- 'SpecMArgs' should be passed as additional arguments to the "to" identifier
+mmArgFin :: Int -> Int -> Ident -> Ident -> Bool -> MacroMapping
+mmArgFin i j from_id to_id params_p =
+  (ModuleIdentifier from_id, finMacro False i j from_id to_id params_p)
+
 -- | Build a 'MacroMapping' from an identifier and a custom 'MonMacro'
 mmCustom :: Ident -> MonMacro -> MacroMapping
 mmCustom from_id macro = (ModuleIdentifier from_id, macro)
@@ -1398,33 +1412,33 @@ defaultMonTable =
   , mmSemiPure "Cryptol.seqZipSame" "CryptolM.seqZipSameM" True
 
     -- PEq constraints
-  , mmSemiPureFin 0 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" True
-  , mmSemiPureFin 0 "Cryptol.PEqSeqBool" "CryptolM.PEqMSeqBool" True
+  , mmSemiPureFin 0 1 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" True
+  , mmSemiPureFin 0 1 "Cryptol.PEqSeqBool" "CryptolM.PEqMSeqBool" True
 
     -- PCmp constraints
-  , mmSemiPureFin 0 "Cryptol.PCmpSeq" "CryptolM.PCmpMSeq" True
-  , mmSemiPureFin 0 "Cryptol.PCmpSeqBool" "CryptolM.PCmpMSeqBool" True
+  , mmSemiPureFin 0 1 "Cryptol.PCmpSeq" "CryptolM.PCmpMSeq" True
+  , mmSemiPureFin 0 1 "Cryptol.PCmpSeqBool" "CryptolM.PCmpMSeqBool" True
 
     -- PSignedCmp constraints
-  , mmSemiPureFin 0 "Cryptol.PSignedCmpSeq" "CryptolM.PSignedCmpMSeq" True
-  , mmSemiPureFin 0 "Cryptol.PSignedCmpSeqBool" "CryptolM.PSignedCmpMSeqBool" True
+  , mmSemiPureFin 0 1 "Cryptol.PSignedCmpSeq" "CryptolM.PSignedCmpMSeq" True
+  , mmSemiPureFin 0 1 "Cryptol.PSignedCmpSeqBool" "CryptolM.PSignedCmpMSeqBool" True
 
     -- PZero constraints
-  , mmSemiPureFin 0 "Cryptol.PZeroSeq" "CryptolM.PZeroMSeq" True
+  , mmSemiPureFin 0 1 "Cryptol.PZeroSeq" "CryptolM.PZeroMSeq" True
 
     -- PLogic constraints
   , mmSemiPure "Cryptol.PLogicSeq" "CryptolM.PLogicMSeq" True
-  , mmSemiPureFin 0 "Cryptol.PLogicSeqBool" "CryptolM.PLogicMSeqBool" True
+  , mmSemiPureFin 0 1 "Cryptol.PLogicSeqBool" "CryptolM.PLogicMSeqBool" True
 
     -- PRing constraints
   , mmSemiPure "Cryptol.PRingSeq" "CryptolM.PRingMSeq" True
-  , mmSemiPureFin 0 "Cryptol.PRingSeqBool" "CryptolM.PRingMSeqBool" True
+  , mmSemiPureFin 0 1 "Cryptol.PRingSeqBool" "CryptolM.PRingMSeqBool" True
 
     -- PIntegral constraints
-  , mmSemiPureFin 0 "Cryptol.PIntegeralSeqBool" "CryptolM.PIntegeralMSeqBool" True
+  , mmSemiPureFin 0 1 "Cryptol.PIntegeralSeqBool" "CryptolM.PIntegeralMSeqBool" True
 
     -- PLiteral constraints
-  , mmSemiPureFin 0 "Cryptol.PLiteralSeqBool" "CryptolM.PLiteralSeqBoolM" True
+  , mmSemiPureFin 0 1 "Cryptol.PLiteralSeqBool" "CryptolM.PLiteralSeqBoolM" True
 
     -- The Cryptol Literal primitives
   , mmSelf "Cryptol.ecNumber"
@@ -1449,22 +1463,22 @@ defaultMonTable =
   , mmSemiPure "Cryptol.ecShiftL" "CryptolM.ecShiftLM" True
   , mmSemiPure "Cryptol.ecShiftR" "CryptolM.ecShiftRM" True
   , mmSemiPure "Cryptol.ecSShiftR" "CryptolM.ecSShiftRM" True
-  , mmSemiPureFin 0 "Cryptol.ecRotL" "CryptolM.ecRotLM" True
-  , mmSemiPureFin 0 "Cryptol.ecRotR" "CryptolM.ecRotRM" True
-  , mmSemiPureFin 0 "Cryptol.ecCat" "CryptolM.ecCatM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecRotL" "CryptolM.ecRotLM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecRotR" "CryptolM.ecRotRM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecCat" "CryptolM.ecCatM" True
   , mmArg "Cryptol.ecTake" "CryptolM.ecTakeM" True
-  , mmSemiPureFin 0 "Cryptol.ecDrop" "CryptolM.ecDropM" True
-  , mmSemiPureFin 0 "Cryptol.ecDrop" "CryptolM.ecDropM" True
-  , mmSemiPureFin 1 "Cryptol.ecJoin" "CryptolM.ecJoinM" True
-  , mmSemiPureFin 1 "Cryptol.ecSplit" "CryptolM.ecSplitM" True
-  , mmSemiPureFin 0 "Cryptol.ecReverse" "CryptolM.ecReverseM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecDrop" "CryptolM.ecDropM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecDrop" "CryptolM.ecDropM" True
+  , mmSemiPureFin 1 1 "Cryptol.ecJoin" "CryptolM.ecJoinM" True
+  , mmSemiPureFin 1 1 "Cryptol.ecSplit" "CryptolM.ecSplitM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecReverse" "CryptolM.ecReverseM" True
   , mmSemiPure "Cryptol.ecTranspose" "CryptolM.ecTransposeM" True
   , mmArg "Cryptol.ecAt" "CryptolM.ecAtM" True
   , mmArg "Cryptol.ecUpdate" "CryptolM.ecUpdateM" True
-  -- , mmArgFin1 "Cryptol.ecAtBack" "CryptolM.ecAtBackM"
-  -- , mmSemiPureFin2 "Cryptol.ecFromTo" "CryptolM.ecFromToM"
-  , mmSemiPureFin 0 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM" True
-  -- , mmSemiPureNthFin 5 "Cryptol.ecFromThenTo" "CryptolM.ecFromThenToM"
+  , mmArgFin 0 1 "Cryptol.ecAtBack" "CryptolM.ecAtBackM" True
+  , mmSemiPureFin 0 2 "Cryptol.ecFromTo" "CryptolM.ecFromToM" True
+  , mmSemiPureFin 0 1 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM" True
+  , mmSemiPureFin 4 1 "Cryptol.ecFromThenTo" "CryptolM.ecFromThenToM" True
   , mmSemiPure "Cryptol.ecInfFrom" "CryptolM.ecInfFromM" True
   , mmSemiPure "Cryptol.ecInfFromThen" "CryptolM.ecInfFromThenM" True
   , mmArg "Cryptol.ecError" "CryptolM.ecErrorM" True

From 7f37068336257d7df76dd94f2b4128a502fbcd32 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 17 Mar 2023 12:50:19 -0400
Subject: [PATCH 12/19] implement ecTransposeM

---
 cryptol-saw-core/saw/CryptolM.sawcore | 45 +++++++++++++++++++++++++--
 1 file changed, 42 insertions(+), 3 deletions(-)

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
index a63d26d26a..7c458c6b86 100644
--- a/cryptol-saw-core/saw/CryptolM.sawcore
+++ b/cryptol-saw-core/saw/CryptolM.sawcore
@@ -36,6 +36,11 @@ zipSameCryM a b n x y = genCryM n (a*b) (\ (i : Nat) -> (atCryM n a x i, atCryM
 reverseCryM : (n : Nat) -> (a : isort 0) -> Vec n a -> Vec n a;
 reverseCryM n a xs = genCryM n a (\ (i : Nat) -> atCryM n a xs (subNat (subNat n 1) i));
 
+transposeCryM : (m n : Nat) -> (a : isort 0) -> Vec m (Vec n a) -> Vec n (Vec m a);
+transposeCryM m n a xss =
+  genCryM n (Vec m a) (\ (j : Nat) ->
+    genCryM m a (\ (i : Nat) -> atCryM n a (atCryM m (Vec n a) xss i) j));
+
 
 
 --------------------------------------------------------------------------------
@@ -763,11 +768,45 @@ ecReverseM E stack =
   Num_rec_fin (\ (n:Num) -> (a : isort 0) -> mseq E stack n a -> mseq E stack n a)
               (\ (n:Nat) -> reverseCryM n);
 
--- FIXME
-primitive
 ecTransposeM : (E:EvType) -> (stack:FunStack) ->
-               (m n : Num) -> (a : sort 0) -> mseq E stack m (mseq E stack n a) ->
+               (m n : Num) -> (a : qisort 0) -> mseq E stack m (mseq E stack n a) ->
                mseq E stack n (mseq E stack m a);
+ecTransposeM E stack m n a =
+  Num_rec
+    (\ (m : Num) -> mseq E stack m (mseq E stack n a) ->
+       mseq E stack n (mseq E stack m a))
+    (\ (m : Nat) ->
+      Num_rec
+        (\ (n : Num) -> Vec m (mseq E stack n a) ->
+           mseq E stack n (Vec m a))
+        (\ (n : Nat) -> transposeCryM m n a)
+        (\ (xss : Vec m (Stream (SpecM E stack a))) ->
+          MkStream (SpecM E stack (Vec m a)) (\ (i : Nat) ->
+            vecMapM E stack (Stream (SpecM E stack a)) a m
+              (\ (j:Nat) -> \ (xs:Stream (SpecM E stack a)) ->
+                 streamGet (SpecM E stack a) xs i)
+              xss))
+        n
+    )
+    ( Num_rec
+        (\ (n : Num) -> Stream (SpecM E stack (mseq E stack n a)) ->
+           mseq E stack n (Stream (SpecM E stack a)))
+        (\ (n : Nat) -> \ (xss : Stream (SpecM E stack (Vec n a))) ->
+          genCryM n (Stream (SpecM E stack a)) (\ (i : Nat) ->
+            MkStream (SpecM E stack a) (\ (j : Nat) ->
+              fmapS E stack (Vec n a) a
+                (\ (xs:Vec n a) -> atCryM n a xs i)
+                (streamGet (SpecM E stack (Vec n a)) xss j))))
+        (\ (xss : Stream (SpecM E stack (Stream (SpecM E stack a)))) ->
+          MkStream (SpecM E stack (Stream (SpecM E stack a))) (\ (i : Nat) ->
+            retS E stack (Stream (SpecM E stack a))
+              (MkStream (SpecM E stack a) (\ (j : Nat) ->
+                 bindS E stack (Stream (SpecM E stack a)) a
+                   (streamGet (SpecM E stack (Stream (SpecM E stack a))) xss j)
+                   (\ (xs:Stream (SpecM E stack a)) -> streamGet (SpecM E stack a) xs i)))))
+        n
+    )
+    m;
 
 ecAtM : (E:EvType) -> (stack:FunStack) ->
         (n : Num) -> (a : sort 0) -> (ix : sort 0) -> PIntegral ix ->

From 63db8c6bdbd11946f191452f313036b19236a13d Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 17 Mar 2023 12:58:25 -0400
Subject: [PATCH 13/19] move Prelude QuantType instances to their correct
 locations

---
 .../CryptolToCoq/SAWCorePreludeExtra.v        | 60 -------------------
 .../CryptolToCoq/SAWCoreScaffolding.v         | 11 ++++
 .../CryptolToCoq/SAWCoreVectorsAsCoqVectors.v | 35 +++++++++++
 3 files changed, 46 insertions(+), 60 deletions(-)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
index 00d990f4e3..c9921e60b5 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
@@ -151,63 +151,3 @@ Proof.
   etransitivity; [ | apply gen_at_BVVec ].
   f_equal; repeat (apply functional_extensionality_dep; intro); eauto.
 Qed.
-
-
-(***
- *** QuantType Instances
- ***)
-
-(** Simple QuantType Instances **)
-
-Program Instance QuantType_Bool : QuantType Bool :=
-  { quantEnc := QEnc_nat;
-    quantEnum := fun n => match n with
-                          | 0 => false
-                          | S _ => true
-                          end;
-    quantEnumInv := fun b => if b then 1 else 0 }.
-Next Obligation.
-  destruct a; reflexivity.
-Defined.
-
-
-(** QuantType Vec Instance **)
-
-(* Build the encoding of the N-tuple of a given encoding *)
-Fixpoint QEnc_NTuple n (qenc : QuantEnc) : QuantEnc :=
-  match n with
-  | 0 => QEnc_prop True
-  | S n' => QEnc_pair qenc (QEnc_NTuple n' qenc)
-  end.
-
-(* The quantEnum function for Vec n a *)
-Definition quantEnum_Vec n A `{QuantType A} :
-  encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A :=
-  nat_rect
-    (fun n => encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A)
-    (fun _ => VectorDef.nil _)
-    (fun n enumF x => VectorDef.cons _ (quantEnum (fst x)) _ (enumF (snd x)))
-    n.
-
-(* The quantEnumInv function for Vec n a *)
-Definition quantEnumInv_Vec n A `{QuantType A} :
-  Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))) :=
-  nat_rect
-    (fun n => Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))))
-    (fun _ => I)
-    (fun n enumInvF x => (quantEnumInv (VectorDef.hd x), enumInvF (VectorDef.tl x)))
-    n.
-
-Program Instance QuantType_Vec n A `{QuantType A} : QuantType (Vec n A) :=
-  { quantEnc := QEnc_NTuple n (quantEnc (A:=A));
-    quantEnum := quantEnum_Vec n A;
-    quantEnumInv := quantEnumInv_Vec n A }.
-Next Obligation.
-  induction a.
-  - reflexivity.
-  - simpl. rewrite quantEnumSurjective. rewrite IHa. reflexivity.
-Defined.
-
-Program Instance QuantType_bitvector w : QuantType (bitvector w) :=
-  QuantType_Vec w _.
-
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
index 5695821c90..3c3063709d 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
@@ -118,6 +118,17 @@ Global Instance Inhabited_unit : Inhabited unit :=
 Global Instance Inhabited_bool : Inhabited bool :=
   MkInhabited bool false.
 
+Program Instance QuantType_Bool : QuantType Bool :=
+ { quantEnc := QEnc_nat;
+   quantEnum := fun n => match n with
+                         | 0 => false
+                         | S _ => true
+                         end;
+   quantEnumInv := fun b => if b then 1 else 0 }.
+Next Obligation.
+ destruct a; reflexivity.
+Defined.
+
 (* SAW uses an alternate form of eq_rect where the motive function P also
 depends on the equality proof itself *)
 Definition Eq__rec (A : Type) (x : A) (P: forall y, x=y -> Type) (p:P x eq_refl) y (e:x=y) :
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
index dce38ce7b2..866c163a67 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
@@ -86,6 +86,41 @@ Qed.
 Instance Inhabited_Vec (n:nat) (a:Type) {Ha:Inhabited a} : Inhabited (Vec n a) :=
   MkInhabited (Vec n a) (gen n a (fun _ => inhabitant)).
 
+(* Build the encoding of the N-tuple of a given encoding *)
+Fixpoint QEnc_NTuple n (qenc : QuantEnc) : QuantEnc :=
+ match n with
+ | 0 => QEnc_prop True
+ | S n' => QEnc_pair qenc (QEnc_NTuple n' qenc)
+ end.
+
+(* The quantEnum function for Vec n a *)
+Definition quantEnum_Vec n A `{QuantType A} :
+ encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A :=
+ nat_rect
+   (fun n => encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A)
+   (fun _ => VectorDef.nil _)
+   (fun n enumF x => VectorDef.cons _ (quantEnum (fst x)) _ (enumF (snd x)))
+   n.
+
+(* The quantEnumInv function for Vec n a *)
+Definition quantEnumInv_Vec n A `{QuantType A} :
+ Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))) :=
+ nat_rect
+   (fun n => Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))))
+   (fun _ => I)
+   (fun n enumInvF x => (quantEnumInv (VectorDef.hd x), enumInvF (VectorDef.tl x)))
+   n.
+
+Program Instance QuantType_Vec n A `{QuantType A} : QuantType (Vec n A) :=
+ { quantEnc := QEnc_NTuple n (quantEnc (A:=A));
+   quantEnum := quantEnum_Vec n A;
+   quantEnumInv := quantEnumInv_Vec n A }.
+Next Obligation.
+ induction a.
+ - reflexivity.
+ - simpl. rewrite quantEnumSurjective. rewrite IHa. reflexivity.
+Defined.
+  
 Theorem gen_domain_eq n T : forall f g (domain_eq : forall i, f i = g i),
     gen n T f = gen n T g.
 Proof.

From f51b683af19173d1d79a2ca84d3d8ca43ca8ab01 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 17 Mar 2023 13:02:51 -0400
Subject: [PATCH 14/19] remove temporary fix in SpecialTreatment

---
 .../src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs     | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
index bf14ea5a57..435beea5fa 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -589,10 +589,9 @@ sawCorePreludeSpecialTreatmentMap configuration =
 
 escapeIdent :: String -> String
 escapeIdent str
-  | all okChar strR = strR
-  | otherwise       = "Op_" ++ zEncodeString str
+  | all okChar str = str
+  | otherwise      = "Op_" ++ zEncodeString str
  where
-   strR = map (\c -> if c `elem` ("#" :: String) then '_' else c) str
    okChar x = isAlphaNum x || x `elem` ("_'" :: String)
 
 zipSnippet :: String

From 37ba74292c63b88eb4984d45ca51cc0c71118906 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 17 Mar 2023 13:18:44 -0400
Subject: [PATCH 15/19] remove manual monadify_term calls in
 sha512_mr_solver.saw

---
 heapster-saw/examples/sha512_mr_solver.saw | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw
index bd7ea87192..030af51294 100644
--- a/heapster-saw/examples/sha512_mr_solver.saw
+++ b/heapster-saw/examples/sha512_mr_solver.saw
@@ -12,20 +12,6 @@ processBlocks <- parse_core_mod "SHA512" "processBlocks";
 // mr_solver_test round_00_15 round_00_15;
 
 import "sha512.cry";
-// FIXME: Why aren't we monadifying these automatically when they're used?
-monadify_term {{ K }};
-monadify_term {{ SIGMA_0 }};
-monadify_term {{ SIGMA_1 }};
-monadify_term {{ sigma_0 }};
-monadify_term {{ sigma_1 }};
-monadify_term {{ Ch }};
-monadify_term {{ Maj }};
-monadify_term {{ round_00_15_spec }};
-monadify_term {{ round_16_80_spec }};
-monadify_term {{ processBlock_loop_spec }};
-monadify_term {{ processBlock_spec }};
-monadify_term {{ processBlocks_loop_spec }};
-monadify_term {{ processBlocks_spec }};
 
 mr_solver_prove round_00_15 {{ round_00_15_spec }};
 mr_solver_prove round_16_80 {{ round_16_80_spec }};

From b5151cc9e78eae4b3ddbd3d2527226e69477f314 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 23 Mar 2023 12:56:29 -0400
Subject: [PATCH 16/19] replace cbnFlags, sortFlagsToList w/ Applicative,
 Foldable instances

---
 .../src/Verifier/SAW/Translation/Coq/Term.hs  |  3 +-
 saw-core/src/Verifier/SAW/ExternalFormat.hs   |  5 +-
 saw-core/src/Verifier/SAW/Term/Functor.hs     | 47 ++++++++++---------
 saw-core/src/Verifier/SAW/TypedAST.hs         |  2 +-
 saw-core/src/Verifier/SAW/UntypedAST.hs       |  4 +-
 5 files changed, 32 insertions(+), 29 deletions(-)

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
index 2dac1bf2a2..7f86b72c4e 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -34,6 +34,7 @@ import qualified Control.Monad.Except                          as Except
 import qualified Control.Monad.Fail                            as Fail
 import           Control.Monad.Reader                          hiding (fail, fix)
 import           Control.Monad.State                           hiding (fail, fix, state)
+import           Data.Foldable                                 as Foldable (toList)
 import           Data.Char                                     (isDigit)
 import qualified Data.IntMap                                   as IntMap
 import           Data.List                                     (intersperse, sortOn)
@@ -493,7 +494,7 @@ translateBinder ::
 translateBinder n ty@(asPiList -> (args, asSortWithFlags -> mb_sort)) =
   do ty' <- translateTerm ty
      n' <- freshenAndBindName n
-     let flagValues = sortFlagsToList $ maybe noFlags snd mb_sort
+     let flagValues = Foldable.toList $ maybe noFlags snd mb_sort
          flagLocalNames = [("Inh", "SAWCoreScaffolding.Inhabited"),
                            ("QT", "QuantType")]
      nhs <- forM (zip flagValues flagLocalNames) $ \(fi,(prefix,tc)) ->
diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs
index 5c0482b25d..d2beaddbfd 100644
--- a/saw-core/src/Verifier/SAW/ExternalFormat.hs
+++ b/saw-core/src/Verifier/SAW/ExternalFormat.hs
@@ -18,6 +18,7 @@ module Verifier.SAW.ExternalFormat (
   ) where
 
 import Control.Monad.State.Strict as State
+import Data.Foldable as F
 #if !MIN_VERSION_base(4,8,0)
 import Data.Traversable
 #endif
@@ -184,8 +185,8 @@ scWriteExternal t0 =
             RecordValue elems   -> pure $ unwords ["Record", show elems]
             RecordProj e prj    -> pure $ unwords ["RecordProj", show e, Text.unpack prj]
             Sort s h
-              | s == propSort -> pure $ unwords ("Prop" : map show (sortFlagsToList h))
-              | otherwise     -> pure $ unwords ("Sort" : drop 5 (show s) : map show (sortFlagsToList h))
+              | s == propSort -> pure $ unwords ("Prop" : map show (F.toList h))
+              | otherwise     -> pure $ unwords ("Sort" : drop 5 (show s) : map show (F.toList h))
                                                         -- /\ Ugly hack to drop "sort "
             NatLit n            -> pure $ unwords ["Nat", show n]
             ArrayValue e v      -> pure $ unwords ("Array" : show e :
diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs
index 5e8343e941..36154e83ac 100644
--- a/saw-core/src/Verifier/SAW/Term/Functor.hs
+++ b/saw-core/src/Verifier/SAW/Term/Functor.hs
@@ -55,7 +55,7 @@ module Verifier.SAW.Term.Functor
   , alistAllFields
     -- * Sorts
   , Sort, mkSort, propSort, sortOf, maxSort
-  , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
+  , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
     -- * Sets of free variables
   , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets
   , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems
@@ -63,11 +63,12 @@ module Verifier.SAW.Term.Functor
   , looseVars, smallestFreeVar
   ) where
 
+import Control.Applicative (liftA2)
 import Data.Bits
 #if !MIN_VERSION_base(4,8,0)
 import Data.Foldable (Foldable)
 #endif
-import qualified Data.Foldable as Foldable (and, foldl')
+import qualified Data.Foldable as Foldable (and, foldl', toList)
 import Data.Hashable
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -137,45 +138,45 @@ maxSort ss = maximum ss
 -- ignored, but are used in the Coq export process to indicate where various
 -- typeclass instances are necessary in function definitions. In the concrete
 -- syntax "isort", "qsort", etc. is used to indicate cases where these flags
--- are set. Note in particular that this flag does not affect typechecking,
+-- are set. Note in particular that these flags do not affect typechecking,
 -- so missing or overeager "isort"/"qsort" annotations will only be detected
 -- via the Coq export.
 --
+-- Note that this is the functor version of the type that is actually used
+-- in 'FlatTermF', 'SortFlags', which has 'Bool' values for its flags.
+--
 -- * If 'flagInhabited' is 'True', an implicit @Inhabited@ typeclass argument
 --   will be added during Coq translation. In the concrete syntax, an "i" is
 --   prepended to the sort (e.g. "isort").
 -- * If 'flagQuantType' is 'True', an implicit @QuantType@ typeclass argument
 --   will be added during Coq translation. In the concrete syntax, an "q" is
 --   prepended to the sort (e.g. "qsort", "qisort").
-data SortFlags = SortFlags { flagInhabited :: Bool
-                           , flagQuantType :: Bool }
-    deriving (Eq, Ord, Generic, TH.Lift)
+data SortFlagsF a = SortFlags { flagInhabited :: a
+                              , flagQuantType :: a }
+    deriving (Functor, Foldable, Eq, Ord, Generic, TH.Lift)
+
+instance Applicative SortFlagsF where
+  pure a = SortFlags a a
+  (SortFlags f1 f2) <*> (SortFlags a1 a2) = SortFlags (f1 a1) (f2 a2)
+
+-- | 'SortFlagsF' with 'Bool' values for its flags
+type SortFlags = SortFlagsF Bool
 
 instance Hashable SortFlags -- automatically derived
 
 instance Show SortFlags where
-  showsPrec _ (SortFlags i q) =
-    showString $ (if q then "q" else "") ++
-                 (if i then "i" else "")
+  showsPrec _ = showString . concat . reverse . Foldable.toList .
+                liftA2 (\s b -> if b then s else "") flagPrefixes
+    where flagPrefixes = SortFlags "i" "q"
 
 -- | The 'SortFlags' object with no flags set
 noFlags :: SortFlags
-noFlags = SortFlags False False
-
--- | Combine two 'SortFlags' by setting each flag in the result if and only if
--- it flag is set in both inputs
-cbnFlags :: SortFlags -> SortFlags -> SortFlags
-cbnFlags (SortFlags i1 q1) (SortFlags i2 q2) =
-  SortFlags (i1 && i2) (q1 && q2)
-
--- | Convert a 'SortFlags' to a list of 'Bool's, indicating which flags are set
-sortFlagsToList :: SortFlags -> [Bool]
-sortFlagsToList (SortFlags i q) = [i, q]
+noFlags = pure False
 
 -- | Build a 'SortFlags' from a list of 'Bool's indicating which flags are set
 sortFlagsFromList :: [Bool] -> SortFlags
-sortFlagsFromList h = SortFlags (isTrue h 0) (isTrue h 1)
-  where isTrue xs i = i < length xs && xs !! i
+sortFlagsFromList bs = fmap (\i -> i < length bs && bs !! i) flagIndices
+  where flagIndices = SortFlags 0 1
 
 
 -- Flat Terms ------------------------------------------------------------------
@@ -352,7 +353,7 @@ zipWithFlatTermF f = go
     go (RecordProj e1 fld1) (RecordProj e2 fld2)
       | fld1 == fld2 = Just $ RecordProj (f e1 e2) fld1
 
-    go (Sort sx hx) (Sort sy hy) | sx == sy = Just (Sort sx (cbnFlags hx hy))
+    go (Sort sx hx) (Sort sy hy) | sx == sy = Just (Sort sx (liftA2 (&&) hx hy))
          -- /\ NB, it's not entirely clear how the flags should be propagated
     go (NatLit i) (NatLit j) | i == j = Just (NatLit i)
     go (StringLit s) (StringLit t) | s == t = Just (StringLit s)
diff --git a/saw-core/src/Verifier/SAW/TypedAST.hs b/saw-core/src/Verifier/SAW/TypedAST.hs
index 3a01d74411..2755d93492 100644
--- a/saw-core/src/Verifier/SAW/TypedAST.hs
+++ b/saw-core/src/Verifier/SAW/TypedAST.hs
@@ -70,7 +70,7 @@ module Verifier.SAW.TypedAST
  , scPrettyTermInCtx
    -- * Primitive types.
  , Sort, mkSort, propSort, sortOf, maxSort
- , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
+ , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
  , Ident(..), identName, mkIdent
  , NameInfo(..), toShortName, toAbsoluteName
  , parseIdent
diff --git a/saw-core/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs
index 86644ec840..29f15cf59c 100644
--- a/saw-core/src/Verifier/SAW/UntypedAST.hs
+++ b/saw-core/src/Verifier/SAW/UntypedAST.hs
@@ -33,7 +33,7 @@ module Verifier.SAW.UntypedAST
   , mkTupleSelector
   , FieldName
   , Sort, mkSort, propSort, sortOf
-  , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
+  , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
   , badTerm
   , module Verifier.SAW.Position
   , moduleName
@@ -57,7 +57,7 @@ import Verifier.SAW.Position
 import Verifier.SAW.TypedAST
   ( ModuleName, mkModuleName
   , Sort, mkSort, propSort, sortOf
-  , SortFlags(..), noFlags, cbnFlags, sortFlagsToList, sortFlagsFromList
+  , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
   , FieldName, DefQualifier
   , LocalName
   )

From 05ef2cbeacca2d7b55f66ae87ecf890c23455b52 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 23 Mar 2023 13:29:46 -0400
Subject: [PATCH 17/19] add Haddock to binder-related defns in Coq translator

---
 saw-core-coq/src/Language/Coq/AST.hs          |  4 ++++
 .../src/Verifier/SAW/Translation/Coq/Term.hs  | 23 +++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/saw-core-coq/src/Language/Coq/AST.hs b/saw-core-coq/src/Language/Coq/AST.hs
index 052166ae2d..c2f3533e70 100644
--- a/saw-core-coq/src/Language/Coq/AST.hs
+++ b/saw-core-coq/src/Language/Coq/AST.hs
@@ -42,11 +42,15 @@ data Term
 -- | Type synonym useful for indicating when a term is used as a type.
 type Type = Term
 
+-- | An 'Ident' with an optional 'Type', which may be explicit or implicit.
+-- For use representing the bound variables in 'Lambda's, 'Let's, etc.
 data Binder
   = Binder Ident (Maybe Type)
   | ImplicitBinder Ident (Maybe Type)
     deriving (Show)
 
+-- | An 'Type' with an optional 'Ident', which may be explicit or implicit.
+-- For use representing arguments in 'Pi' types.
 data PiBinder
   = PiBinder (Maybe Ident) Type
   | PiImplicitBinder (Maybe Ident) Type
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
index 7f86b72c4e..3b492d3c1b 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -456,11 +456,17 @@ freshenAndBindName n =
 mkLet :: (Coq.Ident, Coq.Term) -> Coq.Term -> Coq.Term
 mkLet (name, rhs) body = Coq.Let name [] Nothing rhs body
 
+-- | Given a list of 'LocalName's and their corresponding types (as 'Term's),
+-- return a list of explicit 'Binder's, for use representing the bound
+-- variables in 'Lambda's, 'Let's, etc.
 translateParams ::
   TermTranslationMonad m =>
   [(LocalName, Term)] -> m [Coq.Binder]
 translateParams bs = concat <$> mapM translateParam bs
 
+-- | Given a 'LocalName' and its type (as a 'Term'), return an explicit
+-- 'Binder', for use representing a bound variable in a 'Lambda',
+-- 'Let', etc.
 translateParam ::
   TermTranslationMonad m =>
   (LocalName, Term) -> m [Coq.Binder]
@@ -469,12 +475,20 @@ translateParam (n, ty) =
     return $ Coq.Binder n' (Just ty') :
              map (\(nh,nhty) -> Coq.ImplicitBinder nh (Just nhty)) nhs
 
+-- | Given a list of 'LocalName's and their corresponding types (as 'Term's)
+-- representing argument types and a 'Term' representing the return type,
+-- return the resulting 'Pi', with additional implicit arguments added after
+-- each instance of @isort@, @qsort@, etc.
 translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term
 translatePi binders body = withLocalTranslationState $ do
   bindersT <- concat <$> mapM translatePiBinder binders
   bodyT <- translateTermLet body
   return $ Coq.Pi bindersT bodyT
 
+-- | Given a 'LocalName' and its type (as a 'Term'), return an explicit
+-- 'PiBinder' followed by zero or more implicit 'PiBinder's representing
+-- additonal implicit typeclass arguments, added if the given type is @isort@,
+-- @qsort@, etc.
 translatePiBinder ::
   TermTranslationMonad m => (LocalName, Term) -> m [Coq.PiBinder]
 translatePiBinder (n, ty) =
@@ -486,6 +500,10 @@ translatePiBinder (n, ty) =
       return $ Coq.PiBinder (Just n') ty' :
                map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs
 
+-- | Given a 'LocalName' and its type (as a 'Term'), return the translation of
+-- the 'LocalName' as an 'Ident', the translation of the type as a 'Type',
+-- and zero or more additional 'Ident's and 'Type's representing additonal
+-- implicit typeclass arguments, added if the given type is @isort@, etc.
 translateBinder ::
   TermTranslationMonad m =>
   LocalName ->
@@ -504,6 +522,11 @@ translateBinder n ty@(asPiList -> (args, asSortWithFlags -> mb_sort)) =
                return [(nh,nhty)]
      return (n',ty',concat nhs)
 
+-- | Given a typeclass (as a 'Term'), a list of 'LocalName's and their
+-- corresponding types (as 'Term's), and a type-level function with argument
+-- types given by the prior list, return a 'Pi' of the given arguments, inside
+-- of which is an 'App' of the typeclass to the fully-applied type-level
+-- function
 translateImplicitHyp ::
   TermTranslationMonad m =>
   Coq.Term -> [(LocalName, Term)] -> Coq.Term -> m Coq.Term

From a997f3f61ae7b52747ee9af9931c2374f0004280 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 23 Mar 2023 13:37:29 -0400
Subject: [PATCH 18/19] add Haddock to writeCoqCryptolModule

---
 src/SAWScript/Prover/Exporter.hs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index a7c4f7ad53..39d56f3455 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -478,6 +478,14 @@ writeCoqProp name notations skips path t =
      tm <- io (propToTerm sc t)
      writeCoqTerm name notations skips path tm
 
+-- | Write out a representation of a Cryptol module in Gallina syntax for Coq,
+-- using the monadified version of the given module iff the first argument is
+-- 'True'. The first argument is the file containing the module to export. The
+-- second argument is the name of the file to output into, use an empty string
+-- to output to standard output. The third argument is a list of pairs of
+-- notation substitutions: the operator on the left will be replaced with the
+-- identifier on the right, as we do not support notations on the Coq side.
+-- The fourth argument is a list of identifiers to skip translating.
 writeCoqCryptolModule ::
   Bool ->
   FilePath ->

From 95988c87d3710a4c563017539d88f235ea4d9eef Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Mon, 27 Mar 2023 12:50:20 -0400
Subject: [PATCH 19/19] change SortFlagsF back to SortFlags

---
 .../src/Verifier/SAW/Translation/Coq/Term.hs  |  3 +-
 saw-core/src/Verifier/SAW/ExternalFormat.hs   |  5 +--
 saw-core/src/Verifier/SAW/Term/Functor.hs     | 43 +++++++++----------
 saw-core/src/Verifier/SAW/TypedAST.hs         |  2 +-
 saw-core/src/Verifier/SAW/UntypedAST.hs       |  4 +-
 5 files changed, 26 insertions(+), 31 deletions(-)

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
index 3b492d3c1b..983259ea9c 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -34,7 +34,6 @@ import qualified Control.Monad.Except                          as Except
 import qualified Control.Monad.Fail                            as Fail
 import           Control.Monad.Reader                          hiding (fail, fix)
 import           Control.Monad.State                           hiding (fail, fix, state)
-import           Data.Foldable                                 as Foldable (toList)
 import           Data.Char                                     (isDigit)
 import qualified Data.IntMap                                   as IntMap
 import           Data.List                                     (intersperse, sortOn)
@@ -512,7 +511,7 @@ translateBinder ::
 translateBinder n ty@(asPiList -> (args, asSortWithFlags -> mb_sort)) =
   do ty' <- translateTerm ty
      n' <- freshenAndBindName n
-     let flagValues = Foldable.toList $ maybe noFlags snd mb_sort
+     let flagValues = sortFlagsToList $ maybe noFlags snd mb_sort
          flagLocalNames = [("Inh", "SAWCoreScaffolding.Inhabited"),
                            ("QT", "QuantType")]
      nhs <- forM (zip flagValues flagLocalNames) $ \(fi,(prefix,tc)) ->
diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs
index d2beaddbfd..5c0482b25d 100644
--- a/saw-core/src/Verifier/SAW/ExternalFormat.hs
+++ b/saw-core/src/Verifier/SAW/ExternalFormat.hs
@@ -18,7 +18,6 @@ module Verifier.SAW.ExternalFormat (
   ) where
 
 import Control.Monad.State.Strict as State
-import Data.Foldable as F
 #if !MIN_VERSION_base(4,8,0)
 import Data.Traversable
 #endif
@@ -185,8 +184,8 @@ scWriteExternal t0 =
             RecordValue elems   -> pure $ unwords ["Record", show elems]
             RecordProj e prj    -> pure $ unwords ["RecordProj", show e, Text.unpack prj]
             Sort s h
-              | s == propSort -> pure $ unwords ("Prop" : map show (F.toList h))
-              | otherwise     -> pure $ unwords ("Sort" : drop 5 (show s) : map show (F.toList h))
+              | s == propSort -> pure $ unwords ("Prop" : map show (sortFlagsToList h))
+              | otherwise     -> pure $ unwords ("Sort" : drop 5 (show s) : map show (sortFlagsToList h))
                                                         -- /\ Ugly hack to drop "sort "
             NatLit n            -> pure $ unwords ["Nat", show n]
             ArrayValue e v      -> pure $ unwords ("Array" : show e :
diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs
index 36154e83ac..f926736883 100644
--- a/saw-core/src/Verifier/SAW/Term/Functor.hs
+++ b/saw-core/src/Verifier/SAW/Term/Functor.hs
@@ -55,7 +55,7 @@ module Verifier.SAW.Term.Functor
   , alistAllFields
     -- * Sorts
   , Sort, mkSort, propSort, sortOf, maxSort
-  , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
+  , SortFlags(..), noFlags, sortFlagsLift2, sortFlagsToList, sortFlagsFromList
     -- * Sets of free variables
   , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets
   , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems
@@ -63,12 +63,11 @@ module Verifier.SAW.Term.Functor
   , looseVars, smallestFreeVar
   ) where
 
-import Control.Applicative (liftA2)
 import Data.Bits
 #if !MIN_VERSION_base(4,8,0)
 import Data.Foldable (Foldable)
 #endif
-import qualified Data.Foldable as Foldable (and, foldl', toList)
+import qualified Data.Foldable as Foldable (and, foldl')
 import Data.Hashable
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -142,41 +141,39 @@ maxSort ss = maximum ss
 -- so missing or overeager "isort"/"qsort" annotations will only be detected
 -- via the Coq export.
 --
--- Note that this is the functor version of the type that is actually used
--- in 'FlatTermF', 'SortFlags', which has 'Bool' values for its flags.
---
 -- * If 'flagInhabited' is 'True', an implicit @Inhabited@ typeclass argument
 --   will be added during Coq translation. In the concrete syntax, an "i" is
 --   prepended to the sort (e.g. "isort").
 -- * If 'flagQuantType' is 'True', an implicit @QuantType@ typeclass argument
 --   will be added during Coq translation. In the concrete syntax, an "q" is
 --   prepended to the sort (e.g. "qsort", "qisort").
-data SortFlagsF a = SortFlags { flagInhabited :: a
-                              , flagQuantType :: a }
-    deriving (Functor, Foldable, Eq, Ord, Generic, TH.Lift)
-
-instance Applicative SortFlagsF where
-  pure a = SortFlags a a
-  (SortFlags f1 f2) <*> (SortFlags a1 a2) = SortFlags (f1 a1) (f2 a2)
-
--- | 'SortFlagsF' with 'Bool' values for its flags
-type SortFlags = SortFlagsF Bool
+data SortFlags = SortFlags { flagInhabited :: Bool
+                           , flagQuantType :: Bool }
+    deriving (Eq, Ord, Generic, TH.Lift)
 
 instance Hashable SortFlags -- automatically derived
 
 instance Show SortFlags where
-  showsPrec _ = showString . concat . reverse . Foldable.toList .
-                liftA2 (\s b -> if b then s else "") flagPrefixes
-    where flagPrefixes = SortFlags "i" "q"
+  showsPrec _ (SortFlags i q) = showString $
+    concatMap (\(b,s) -> if b then s else "")
+              [(q,"q"), (i,"i")]
 
 -- | The 'SortFlags' object with no flags set
 noFlags :: SortFlags
-noFlags = pure False
+noFlags = SortFlags False False
+
+-- | Apply a binary operation to corresponding flags of two 'SortFlags'
+sortFlagsLift2 :: (Bool -> Bool -> Bool) -> SortFlags -> SortFlags -> SortFlags
+sortFlagsLift2 f (SortFlags i1 q1) (SortFlags i2 q2) = SortFlags (f i1 i2) (f q1 q2)
+
+-- | Convert a 'SortFlags' to a list of 'Bool's, indicating which flags are set
+sortFlagsToList :: SortFlags -> [Bool]
+sortFlagsToList (SortFlags i q) = [i, q]
 
 -- | Build a 'SortFlags' from a list of 'Bool's indicating which flags are set
 sortFlagsFromList :: [Bool] -> SortFlags
-sortFlagsFromList bs = fmap (\i -> i < length bs && bs !! i) flagIndices
-  where flagIndices = SortFlags 0 1
+sortFlagsFromList bs = SortFlags (isSet 0) (isSet 1)
+  where isSet i = i < length bs && bs !! i
 
 
 -- Flat Terms ------------------------------------------------------------------
@@ -353,7 +350,7 @@ zipWithFlatTermF f = go
     go (RecordProj e1 fld1) (RecordProj e2 fld2)
       | fld1 == fld2 = Just $ RecordProj (f e1 e2) fld1
 
-    go (Sort sx hx) (Sort sy hy) | sx == sy = Just (Sort sx (liftA2 (&&) hx hy))
+    go (Sort sx hx) (Sort sy hy) | sx == sy = Just (Sort sx (sortFlagsLift2 (&&) hx hy))
          -- /\ NB, it's not entirely clear how the flags should be propagated
     go (NatLit i) (NatLit j) | i == j = Just (NatLit i)
     go (StringLit s) (StringLit t) | s == t = Just (StringLit s)
diff --git a/saw-core/src/Verifier/SAW/TypedAST.hs b/saw-core/src/Verifier/SAW/TypedAST.hs
index 2755d93492..2ddfab2329 100644
--- a/saw-core/src/Verifier/SAW/TypedAST.hs
+++ b/saw-core/src/Verifier/SAW/TypedAST.hs
@@ -70,7 +70,7 @@ module Verifier.SAW.TypedAST
  , scPrettyTermInCtx
    -- * Primitive types.
  , Sort, mkSort, propSort, sortOf, maxSort
- , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
+ , SortFlags(..), noFlags, sortFlagsLift2, sortFlagsToList, sortFlagsFromList
  , Ident(..), identName, mkIdent
  , NameInfo(..), toShortName, toAbsoluteName
  , parseIdent
diff --git a/saw-core/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs
index 29f15cf59c..ca541e92b5 100644
--- a/saw-core/src/Verifier/SAW/UntypedAST.hs
+++ b/saw-core/src/Verifier/SAW/UntypedAST.hs
@@ -33,7 +33,7 @@ module Verifier.SAW.UntypedAST
   , mkTupleSelector
   , FieldName
   , Sort, mkSort, propSort, sortOf
-  , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
+  , SortFlags(..), noFlags, sortFlagsLift2, sortFlagsToList, sortFlagsFromList
   , badTerm
   , module Verifier.SAW.Position
   , moduleName
@@ -57,7 +57,7 @@ import Verifier.SAW.Position
 import Verifier.SAW.TypedAST
   ( ModuleName, mkModuleName
   , Sort, mkSort, propSort, sortOf
-  , SortFlagsF(..), SortFlags, noFlags, sortFlagsFromList
+  , SortFlags(..), noFlags, sortFlagsLift2, sortFlagsToList, sortFlagsFromList
   , FieldName, DefQualifier
   , LocalName
   )