From 2d11b9325efe166c89198753a0eff7970c726bc1 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Mon, 25 May 2026 21:18:17 -0700
Subject: [PATCH 01/17] refactor: preparing for future

---
 .../src/CryptolSAWCore/CryptolEnv.hs          | 56 +++++++++++--------
 1 file changed, 32 insertions(+), 24 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index eb515c2d5e..ffdeadd53a 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -106,7 +106,7 @@ import           Cryptol.Utils.Ident
 
 -- local:
 import qualified CryptolSAWCore.Cryptol as C
-import           CryptolSAWCore.FileReader 
+import           CryptolSAWCore.FileReader
 import           CryptolSAWCore.GlobalCryptolEnv
 import           CryptolSAWCore.Panic
 import qualified CryptolSAWCore.Pretty as CryPP
@@ -204,9 +204,9 @@ initCryptolEnv sc = do
 
   -- initialize the module environment stored in the context
   (_,refTop) <- liftModuleM sc $ do
-    MM.modifyModuleEnv $ \env -> 
+    MM.modifyModuleEnv $ \env ->
       env { ME.meSearchPath = cryptolPaths ++
-              (instDir </> "lib") : ME.meSearchPath env 
+              (instDir </> "lib") : ME.meSearchPath env
            }
     -- Load Cryptol prelude and magic Array module
     _ <- MB.loadModuleFrom False (MM.FromModule preludeName)
@@ -313,22 +313,26 @@ getNamingEnv sc env = do
   modEnv <- eModuleEnv sc
   return $ eExtraNaming env
     `MR.shadowing`
-    (mconcat $ map (getNamingEnvForImport modEnv)
-                  (eImports env)
-    )
+    (foldr (getNamingEnvForImport modEnv)
+           mempty
+           (eImports env))
 
--- | Get the `MR.NamingEnv` for one `T.Import`.
+-- | Extend the `MR.NamingEnv` for one `T.Import`.
 getNamingEnvForImport :: ME.ModuleEnv
                       -> (ImportVisibility, T.Import)
                       -> MR.NamingEnv
-getNamingEnvForImport modEnv (vis, imprt) =
-    MN.interpImportEnv'
-      MN.nameToPNameWithQualifiers (T.iAs imprt) (T.iSpec imprt)
-         -- adjusting for qualified imports
-  $ MN.namingEnvNames
-  $ computeNamingEnv lm vis
+                      -> MR.NamingEnv
+getNamingEnvForImport modEnv (vis, imprt) nmEnv0 =
+  nmEnv1 <> nmEnv0
 
   where
+  nmEnv1 =
+      MN.interpImportEnv'
+        MN.nameToPNameWithQualifiers (T.iAs imprt) (T.iSpec imprt)
+           -- adjusting for qualified imports
+    $ MN.namingEnvNames
+    $ computeNamingEnv lm vis
+
   modName :: C.ModName
   modName = P.thing $ T.iModule imprt
 
@@ -629,8 +633,8 @@ bindExtCryptolModule sc (modName, ecm) =
 -- add the module into the import list.
 bindLoadedModule ::
   SharedContext -> (P.ModName, P.Located C.ModName) -> CryptolEnv -> IO CryptolEnv
-bindLoadedModule _ (asName, origName) env = 
-  return $ C.mapImports 
+bindLoadedModule _ (asName, origName) env =
+  return $ C.mapImports
     ((:) (mkImport PublicAndPrivate origName (Just asName) Nothing)) env
 
 -- | bindCryptolModule - when we have the @cryptol_prims ()@ created
@@ -845,7 +849,7 @@ importCryptolModule _sc _env (Right __nm) _as True _vis _imps =
   -- FIXME: this will be implemented in #2618 (soon).
   fail $ "`import submodule` is unsupported."
 importCryptolModule _sc _env (Left _)  _as True _vis _imps =
-  -- importing submodule by FilePath: disallowed:
+  -- importing submodule by FilePath is an error.
   fail $ "`import submodule PATHNAME` is not allowed."
      -- NOTE: this is allowed by parser (thus we can get here).
      -- FIXME: Would we want to implement this check in the typechecker?
@@ -893,7 +897,7 @@ bindExtraVar :: SharedContext -> (Ident, TypedTerm) -> CryptolEnv -> IO CryptolE
 bindExtraVar sc (ident, TypedTerm (TypedTermSchema schema) trm) env0 = do
   name <- bindIdent sc ident
   let pname = P.mkUnqual ident
-  addExtraVars sc (Map.singleton name schema) 
+  addExtraVars sc (Map.singleton name schema)
   addToAllTerms sc (Map.singleton name trm)
   return $ C.mapNaming (MR.shadowing $ MN.singletonNS C.NSValue pname name) env0
 
@@ -934,7 +938,7 @@ bindTySyn sc (ident, T.Forall [] [] ty) env = do
   addExtraTySyns sc (Map.singleton name tysyn)
   let pname = P.mkUnqual ident
   return $ C.mapNaming (MR.shadowing (MN.singletonNS C.NSType pname name)) env
-  
+
 bindTySyn _ _ env = pure env -- only monomorphic types may be bound
 
 -- | Add a new Cryptol integer type as an "extra" declration.
@@ -957,13 +961,18 @@ bindIntegerType sc (ident, n) env = do
 meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig
 meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)
 
-
 -- | Look up an identifier in the Cryptol environment and return its
 --   full name.
 resolveIdentifier ::
   (HasCallStack) =>
   SharedContext -> CryptolEnv -> Text -> IO (Maybe T.Name)
-resolveIdentifier sc env nm = do
+resolveIdentifier sc env = resolveIdentifier' sc env C.NSValue
+
+
+resolveIdentifier' ::
+  (HasCallStack) =>
+  SharedContext -> CryptolEnv -> C.NameSpace -> Text -> IO (Maybe T.Name)
+resolveIdentifier' sc env nameSpace nm =
   case splitOn (pack "::") nm of
     []  -> pure Nothing
            -- FIXME: shouldn't this be error?
@@ -973,14 +982,13 @@ resolveIdentifier sc env nm = do
     -- FIXME: Is there no function that parses Text into PName?
 
   where
-
   doResolve pnm = do
     nameEnv <- getNamingEnv sc env
     (res, _ws) <- runModuleM sc $
       MM.interactive (MB.rename interactiveName nameEnv
-                            (MR.resolveNameUse C.NSValue pnm))
+                            (MR.resolveNameUse nameSpace pnm))
     case res of
-      Left _ -> return Nothing
+      Left _  -> pure Nothing
       Right x -> pure (Just x)
 
 -- | Read a Cryptol expression from `InputText` and return it as a
@@ -1012,7 +1020,7 @@ pExprToTypedTerm sc env pexpr = do
     -- Eliminate patterns:
     npe <- MM.interactive (MB.noPat pexpr)
 
-    
+
     let npe' = MR.rename npe
     re <- MM.interactive (MB.rename interactiveName nameEnv npe')
       -- NOTE: if a name is not in scope, it is reported here.

From 5f7125788c94827e2c7494fbfd63bf9379161caf Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Tue, 26 May 2026 12:57:53 -0700
Subject: [PATCH 02/17] refactor: generalizing in preparation

---
 .../src/CryptolSAWCore/Cryptol.hs             |  3 +
 .../src/CryptolSAWCore/CryptolEnv.hs          | 23 ++++---
 .../src/CryptolSAWCore/GlobalCryptolEnv.hs    | 69 ++++++++++---------
 3 files changed, 50 insertions(+), 45 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
index 9dbdbdea87..d39832158e 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
@@ -26,6 +26,8 @@ between these two modules is mostly a function of historical accident.
 
 module CryptolSAWCore.Cryptol
   ( module CryptolSAWCore.GlobalCryptolEnv
+  , ImportVisibility(..)
+  , IsSubmodule
 
   , isErasedProp
   , proveProp
@@ -118,6 +120,7 @@ import CryptolSAWCore.Panic
 import qualified CryptolSAWCore.Pretty as CryPP
 import CryptolSAWCore.GlobalCryptolEnv
 
+
 -- | bindTParam' - create a binding for a type parameter, returning 3-tuple:
 --                 - environment
 --                 - the SAWCore kind of the parameter
diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index ffdeadd53a..c1f49a1f15 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -230,9 +230,9 @@ initCryptolEnv sc = do
       arrayName'            = locatedUnknown arrayName
 
   let env0 = C.mapImports (\_ ->
-            [ mkImport OnlyPublic preludeName'          Nothing Nothing
-            , mkImport OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing
-            , mkImport OnlyPublic arrayName'            Nothing Nothing
+            [ mkImport False OnlyPublic preludeName'          Nothing Nothing
+            , mkImport False OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing
+            , mkImport False OnlyPublic arrayName'            Nothing Nothing
             ]) $ C.initEnv
   C.addRefPrims sc refPrims
   -- Generate SAWCore translations for all values in scope
@@ -319,10 +319,10 @@ getNamingEnv sc env = do
 
 -- | Extend the `MR.NamingEnv` for one `T.Import`.
 getNamingEnvForImport :: ME.ModuleEnv
-                      -> (ImportVisibility, T.Import)
+                      -> (C.IsSubmodule, ImportVisibility, T.Import)
                       -> MR.NamingEnv
                       -> MR.NamingEnv
-getNamingEnvForImport modEnv (vis, imprt) nmEnv0 =
+getNamingEnvForImport modEnv (_isSubmod, vis, imprt) nmEnv0 =
   nmEnv1 <> nmEnv0
 
   where
@@ -635,7 +635,7 @@ bindLoadedModule ::
   SharedContext -> (P.ModName, P.Located C.ModName) -> CryptolEnv -> IO CryptolEnv
 bindLoadedModule _ (asName, origName) env =
   return $ C.mapImports
-    ((:) (mkImport PublicAndPrivate origName (Just asName) Nothing)) env
+    ((:) (mkImport False PublicAndPrivate origName (Just asName) Nothing)) env
 
 -- | bindCryptolModule - when we have the @cryptol_prims ()@ created
 --   object, add the `CryptolModule` to the relevant maps in the
@@ -842,7 +842,7 @@ importCryptolModule sc env src as False vis imps =
   -- importing full module:
   do
   mod' <- loadAndTranslateModule sc src
-  let import' = mkImport vis (locatedUnknown (T.mName mod')) as imps
+  let import' = mkImport False vis (locatedUnknown (T.mName mod')) as imps
   return $ C.mapImports (\imports -> import':imports) env
 importCryptolModule _sc _env (Right __nm) _as True _vis _imps =
   -- importing submodule by name:
@@ -855,12 +855,13 @@ importCryptolModule _sc _env (Left _)  _as True _vis _imps =
      -- FIXME: Would we want to implement this check in the typechecker?
 
 -- | Create an entry for the `eImports` list in `CryptolEnv`.
-mkImport :: ImportVisibility
+mkImport :: C.IsSubmodule
+         -> ImportVisibility
          -> P.Located C.ModName
          -> Maybe C.ModName
          -> Maybe T.ImportSpec
-         -> (ImportVisibility, T.Import)
-mkImport vis nm as imps =
+         -> (C.IsSubmodule, ImportVisibility, T.Import)
+mkImport isSubmodule vis nm as imps =
     let im = T.Import { T.iModule = nm
                       , T.iAs     = as
                       , T.iSpec   = imps
@@ -868,7 +869,7 @@ mkImport vis nm as imps =
                       , T.iDoc    = Nothing
                       }
     in
-    (vis, im)
+    (isSubmodule, vis, im)
 
 
 ---- Binding -------------------------------------------------------------------
diff --git a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
index 51a3d7660e..83637ef0d4 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
@@ -12,7 +12,7 @@ Portability : non-portable (language extensions)
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ViewPatterns #-}
 
-module CryptolSAWCore.GlobalCryptolEnv 
+module CryptolSAWCore.GlobalCryptolEnv
   ( ImportVisibility(..)
   , isToplevel
   , sameHeight
@@ -109,6 +109,7 @@ data ImportVisibility
                      --   and (arbitrarily nested) submodules.
   deriving (Eq, Show)
 
+type IsSubmodule = Bool  -- FIXME[MT]: right place?
 
 -- | The global environment for capturing the Cryptol state, both
 --   Cryptol's own state and the state associated with
@@ -137,7 +138,7 @@ data GlobalCryptolEnv = GlobalCryptolEnv
 initGlobalEnv :: ME.ModuleEnv -> GlobalCryptolEnv
 initGlobalEnv modEnv = refreshCryptolEnv $
     GlobalCryptolEnv modEnv
-      mempty mempty mempty mempty mempty mempty mempty mempty mempty 
+      mempty mempty mempty mempty mempty mempty mempty mempty mempty
       mempty
 
 instance IsMetadata GlobalCryptolEnv where
@@ -167,9 +168,9 @@ instance IsMetadata GlobalCryptolEnv where
   restoreMetadata chk now = return $
     let newMEnv = geModuleEnv now
         chkMEnv = geModuleEnv chk
-    in chk { geModuleEnv = chkMEnv 
+    in chk { geModuleEnv = chkMEnv
                { ME.meNameSeeds = ME.meNameSeeds newMEnv
-               , ME.meSupply = ME.meSupply newMEnv 
+               , ME.meSupply = ME.meSupply newMEnv
                }
            }
 
@@ -182,7 +183,7 @@ instance IsMetadata GlobalCryptolEnv where
 
 data CryptolFrame =
   CryptolFrame { fNamingEnv :: MR.NamingEnv
-               , fImports :: [(ImportVisibility, C.Import)] 
+               , fImports :: [(ImportVisibility, C.Import)]
                }
 
 initFrame :: CryptolFrame
@@ -203,12 +204,12 @@ isToplevel (CryptolEnv (_ :| frames)) = null frames
 
 -- | Test if the scopes have the same number of frames pushed.
 sameHeight :: CryptolEnv -> CryptolEnv -> Bool
-sameHeight (CryptolEnv scope1) (CryptolEnv scope2) = 
+sameHeight (CryptolEnv scope1) (CryptolEnv scope2) =
   NE.length scope1 == NE.length scope2
 
-mapCurFrame :: 
-  (CryptolFrame -> CryptolFrame) -> 
-  CryptolEnv -> 
+mapCurFrame ::
+  (CryptolFrame -> CryptolFrame) ->
+  CryptolEnv ->
   CryptolEnv
 mapCurFrame f (CryptolEnv (frame :| frames)) =
   CryptolEnv (f frame :| frames)
@@ -225,30 +226,30 @@ popScope (CryptolEnv frames) = case snd (NE.uncons frames) of
   Just frames' -> CryptolEnv frames'
 
 -- | Map the naming environment of the frame currently in scope.
-mapNaming :: 
-  (MR.NamingEnv -> MR.NamingEnv) -> 
-  CryptolEnv -> 
+mapNaming ::
+  (MR.NamingEnv -> MR.NamingEnv) ->
+  CryptolEnv ->
   CryptolEnv
-mapNaming f = mapCurFrame $ 
+mapNaming f = mapCurFrame $
       \fr -> fr {fNamingEnv = f (fNamingEnv fr) }
 
 -- | Map the module imports of the frame currently in scope.
-mapImports :: 
-  ([(ImportVisibility, C.Import)] -> [(ImportVisibility, C.Import)] ) -> 
-  CryptolEnv -> 
+mapImports ::
+  ([(ImportVisibility, C.Import)] -> [(ImportVisibility, C.Import)] ) ->
+  CryptolEnv ->
   CryptolEnv
-mapImports f = mapCurFrame $ 
+mapImports f = mapCurFrame $
       \fr -> fr {fImports = f (fImports fr) }
 
 -- | Run the inner action bracketed new frame pushed/popped on
 --   the 'CryptolScope' stack.
 --   Fails if the inner action changes the scope height
 --   (i.e. it does not properly bracket its pushes and pops).
-withFreshScope :: 
+withFreshScope ::
   MonadFail m =>
-  CryptolEnv -> 
-  (CryptolEnv -> 
-  m (a, CryptolEnv)) -> 
+  CryptolEnv ->
+  (CryptolEnv ->
+  m (a, CryptolEnv)) ->
   m (a, CryptolEnv)
 withFreshScope env0 f = do
   let env1 = pushScope env0
@@ -319,7 +320,7 @@ eRefPrims = getGlobal geRefPrims
 
 -- | Add entries to 'eRefPrims'
 addRefPrims :: SharedContext -> Map C.PrimIdent C.Expr -> IO ()
-addRefPrims sc m = mapGlobal sc $ \genv -> 
+addRefPrims sc m = mapGlobal sc $ \genv ->
   genv { geRefPrims = Map.union m (geRefPrims genv) }
 
 -- | Map from names of Cryptol primitives to their implementations
@@ -329,7 +330,7 @@ ePrims = getGlobal gePrims
 
 -- | Add entries to 'ePrims'
 addPrims :: SharedContext -> Map C.PrimIdent Term -> IO ()
-addPrims sc m = mapGlobal sc $ \genv -> 
+addPrims sc m = mapGlobal sc $ \genv ->
   genv { gePrims = Map.union m (gePrims genv) }
 
 -- | Map from names of Cryptol primitive types to their
@@ -339,7 +340,7 @@ ePrimTypes = getGlobal gePrimTypes
 
 -- | Add entries to 'ePrimTypes'
 addPrimTypes :: SharedContext -> Map C.PrimIdent Term -> IO ()
-addPrimTypes sc m = mapGlobal sc $ \genv -> 
+addPrimTypes sc m = mapGlobal sc $ \genv ->
   genv { gePrimTypes = Map.union m (gePrimTypes genv) }
 
 
@@ -362,8 +363,8 @@ meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)
 -- | Add an entry to the 'ME.meSearchPath' of the 'eModuleEnv'.
 addSearchPath :: SharedContext -> FilePath -> IO ()
 addSearchPath sc fp = mapGlobal sc $ \genv ->
-  genv { geModuleEnv = (geModuleEnv genv) 
-    { ME.meSearchPath = fp : ME.meSearchPath (geModuleEnv genv) } } 
+  genv { geModuleEnv = (geModuleEnv genv)
+    { ME.meSearchPath = fp : ME.meSearchPath (geModuleEnv genv) } }
 
 -- | Run an 'MM.ModuleM' action using the module environment from
 -- 'eModuleEnv'. If the action is successful, updates the module
@@ -401,7 +402,7 @@ eExtraTySyns = getGlobal geExtraTySyns
 
 -- | Add entries to 'eExtraTySyns'
 addExtraTySyns :: SharedContext -> Map C.Name C.TySyn -> IO ()
-addExtraTySyns sc m = mapGlobal sc $ \genv -> 
+addExtraTySyns sc m = mapGlobal sc $ \genv ->
   genv { geExtraTySyns = Map.union m (geExtraTySyns genv) }
 
 -- | Formerly @eExtraTypes@, holds the Cryptol-level
@@ -412,9 +413,9 @@ eExtraVars = getGlobal geExtraVars
 
 -- | Add entries to both 'eExtraVars' and 'eAllVars'
 addExtraVars :: SharedContext -> Map C.Name C.Schema -> IO ()
-addExtraVars sc m = mapGlobal sc $ \genv -> 
+addExtraVars sc m = mapGlobal sc $ \genv ->
   genv { geExtraVars = Map.union m (geExtraVars genv)
-       , geAllVars = Map.union m (geAllVars genv) 
+       , geAllVars = Map.union m (geAllVars genv)
        }
 
 -- | Map from Cryptol names to Cryptol types. This is
@@ -457,7 +458,7 @@ eTyVars = getGlobal geTyVars
 
 -- | Add entries to 'eTyVars'
 addTyVars :: SharedContext -> Map Int Term -> IO ()
-addTyVars sc m = mapGlobal sc $ \genv -> 
+addTyVars sc m = mapGlobal sc $ \genv ->
   genv { geTyVars = Map.union m (geTyVars genv) }
 
 -- | Map from Cryptol `C.Prop`, which are type constraints, to
@@ -483,7 +484,7 @@ eTyProps = getGlobal geTyProps
 --   This is not expensive, but would become problematic
 --   if we wanted to enforce a write-once policy.
 addTyProps :: SharedContext -> Map C.Prop (Term, [FieldName]) -> IO ()
-addTyProps sc m = mapGlobal sc $ \genv -> 
+addTyProps sc m = mapGlobal sc $ \genv ->
   genv { geTyProps = Map.union m (geTyProps genv)  }
 
 -- | The translations for all Cryptol names in scope. It maps names to
@@ -508,7 +509,7 @@ eFFITypes = getGlobal geFFITypes
 
 -- | Add entries to 'eFFITypes'
 addFFITypes :: SharedContext -> Map NameInfo C.FFI -> IO ()
-addFFITypes sc m = mapGlobal sc $ \genv -> 
+addFFITypes sc m = mapGlobal sc $ \genv ->
   genv { geFFITypes = Map.union m (geFFITypes genv) }
 
 --
@@ -530,7 +531,7 @@ addFFITypes sc m = mapGlobal sc $ \genv ->
 -- irregularities that can creep in when we reimplement Cryptol name
 -- resolution.
 eExtraNaming :: CryptolEnv -> MR.NamingEnv
-eExtraNaming (CryptolEnv (frame :| frames)) = 
+eExtraNaming (CryptolEnv (frame :| frames)) =
   foldr (\fr ne -> ne `MR.shadowing` (fNamingEnv fr)) (fNamingEnv frame) frames
 
 -- | The list of Cryptol modules which have been brought into the
@@ -541,7 +542,7 @@ eExtraNaming (CryptolEnv (frame :| frames)) =
 --   should only correspond to modules that are present in the module
 --   environment *and* have been translated into SAWCore.
 eImports :: CryptolEnv -> [(ImportVisibility, C.Import)]
-eImports (CryptolEnv frames) = 
+eImports (CryptolEnv frames) =
   concat $ map fImports $ NE.toList frames
 
 

From 53b78931751034adb186097a75fdc08aa1a0b677 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Fri, 29 May 2026 16:52:53 -0700
Subject: [PATCH 03/17] refactor: modulo fail...

in "import submodule" code,
  - fail is replaced with /logging and future-use code/
and the new code is effectively a NOP.
---
 .../src/CryptolSAWCore/CryptolEnv.hs          | 66 +++++++++++++++----
 1 file changed, 54 insertions(+), 12 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index c1f49a1f15..861729dcf7 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -322,7 +322,7 @@ getNamingEnvForImport :: ME.ModuleEnv
                       -> (C.IsSubmodule, ImportVisibility, T.Import)
                       -> MR.NamingEnv
                       -> MR.NamingEnv
-getNamingEnvForImport modEnv (_isSubmod, vis, imprt) nmEnv0 =
+getNamingEnvForImport modEnv (isSubmod, vis, imprt) nmEnv0 =
   nmEnv1 <> nmEnv0
 
   where
@@ -331,17 +331,31 @@ getNamingEnvForImport modEnv (_isSubmod, vis, imprt) nmEnv0 =
         MN.nameToPNameWithQualifiers (T.iAs imprt) (T.iSpec imprt)
            -- adjusting for qualified imports
     $ MN.namingEnvNames
-    $ computeNamingEnv lm vis
+    $ baseNamingEnvToAdd
 
-  modName :: C.ModName
-  modName = P.thing $ T.iModule imprt
+  baseNamingEnvToAdd =
+    if isSubmod then
+      -- find the submodule in the current environment (`nmEnv0`) and compute
+      -- namingEnv:
+      error "isSubmod"
 
-  lm = case ME.lookupModule modName modEnv of
-         Just lm' -> lm'
-         Nothing  -> panic "getNamingEnvForImport"
-                       ["cannot lookupModule: " <> CryPP.pp modName]
+    else
+      -- find the top-level loaded module and compute NamingEnv:
+      --   NOTE: does not depend on `nmEnv0`
+      let
+        modName :: C.ModName
+        modName = P.thing $ T.iModule imprt
 
--- | Compute a `MR.NamingEnv` for a module based on the
+        lm = case ME.lookupModule modName modEnv of
+               Just lm' -> lm'
+               Nothing  -> panic "getNamingEnvForImport"
+                             ["cannot lookupModule: " <> CryPP.pp modName]
+
+      in
+        computeNamingEnv lm vis
+
+
+-- | Compute a `MR.NamingEnv` for a loaded module based on the
 --   `ImportVisibility`.
 computeNamingEnv :: ME.LoadedModule -> ImportVisibility -> MR.NamingEnv
 computeNamingEnv lm vis =
@@ -844,10 +858,38 @@ importCryptolModule sc env src as False vis imps =
   mod' <- loadAndTranslateModule sc src
   let import' = mkImport False vis (locatedUnknown (T.mName mod')) as imps
   return $ C.mapImports (\imports -> import':imports) env
-importCryptolModule _sc _env (Right __nm) _as True _vis _imps =
+  return $ env' {eImports = import' : eImports env }
+importCryptolModule _sc env (Right modName) _as True _vis _imps =
   -- importing submodule by name:
-  -- FIXME: this will be implemented in #2618 (soon).
-  fail $ "`import submodule` is unsupported."
+  do
+  let modNameTxt = C.modNameToText modName
+  mName <- resolveIdentifier' C.NSModule env modNameTxt
+    -- FIXME: dups dealt with??
+  name <-
+    case mName of
+      Nothing -> fail $ "submodule `"
+                        <> Text.unpack modNameTxt
+                        <> "` is not in scope"
+      Just nm -> return nm
+  print $ "name = " ++ show (name :: T.Name)
+  print $ "submodule: " <> (C.identText $ MN.nameIdent name)
+  -- let import' = error "NIY"
+  _nmEnv <-
+    case ME.modContextOf (P.ImpNested name) (eModuleEnv env) of
+      Just mc -> do
+                 -- putStrLn "\nexported:" >> print (ME.mctxExported mc)
+                 let ne =
+                      MN.filterUNames
+                        (`Set.member` ME.mctxExported mc)
+                        (ME.mctxNames mc)
+
+                 return ne
+      Nothing -> panic "modContextOf" []
+  return env
+    -- FIXME: partial implementation here in this function, so
+    --        let's just be a nop, eventually we'll have this:
+    -- {eImports = import' : eImports env }
+
 importCryptolModule _sc _env (Left _)  _as True _vis _imps =
   -- importing submodule by FilePath is an error.
   fail $ "`import submodule PATHNAME` is not allowed."

From 3b8d004dfa39b5c1c6936ba7baba61a65d7e2b00 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 30 May 2026 14:31:18 -0700
Subject: [PATCH 04/17] refactor: varia; Bool -> IsSubmodule

---
 .../src/CryptolSAWCore/CryptolEnv.hs          | 91 ++++++++++---------
 1 file changed, 47 insertions(+), 44 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index 861729dcf7..2b0225b977 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -848,53 +848,56 @@ importCryptolModule ::
   CryptolEnv                {- ^ Extend this environment -} ->
   Either FilePath P.ModName {- ^ Where to find the module -} ->
   Maybe P.ModName           {- ^ Name qualifier -} ->
-  Bool                      {- ^ isSubmodule: True if 'import submodule ...' -} ->
+  C.IsSubmodule             {- ^ isSubmodule: True if 'import submodule ...' -} ->
   ImportVisibility          {- ^ What visibility to give symbols from this module -} ->
   Maybe P.ImportSpec        {- ^ What to import -} ->
   IO CryptolEnv
-importCryptolModule sc env src as False vis imps =
-  -- importing full module:
-  do
-  mod' <- loadAndTranslateModule sc src
-  let import' = mkImport False vis (locatedUnknown (T.mName mod')) as imps
-  return $ C.mapImports (\imports -> import':imports) env
-  return $ env' {eImports = import' : eImports env }
-importCryptolModule _sc env (Right modName) _as True _vis _imps =
-  -- importing submodule by name:
-  do
-  let modNameTxt = C.modNameToText modName
-  mName <- resolveIdentifier' C.NSModule env modNameTxt
-    -- FIXME: dups dealt with??
-  name <-
-    case mName of
-      Nothing -> fail $ "submodule `"
-                        <> Text.unpack modNameTxt
-                        <> "` is not in scope"
-      Just nm -> return nm
-  print $ "name = " ++ show (name :: T.Name)
-  print $ "submodule: " <> (C.identText $ MN.nameIdent name)
-  -- let import' = error "NIY"
-  _nmEnv <-
-    case ME.modContextOf (P.ImpNested name) (eModuleEnv env) of
-      Just mc -> do
-                 -- putStrLn "\nexported:" >> print (ME.mctxExported mc)
-                 let ne =
-                      MN.filterUNames
-                        (`Set.member` ME.mctxExported mc)
-                        (ME.mctxNames mc)
-
-                 return ne
-      Nothing -> panic "modContextOf" []
-  return env
-    -- FIXME: partial implementation here in this function, so
-    --        let's just be a nop, eventually we'll have this:
-    -- {eImports = import' : eImports env }
-
-importCryptolModule _sc _env (Left _)  _as True _vis _imps =
-  -- importing submodule by FilePath is an error.
-  fail $ "`import submodule PATHNAME` is not allowed."
-     -- NOTE: this is allowed by parser (thus we can get here).
-     -- FIXME: Would we want to implement this check in the typechecker?
+importCryptolModule sc env src as isSubmodule vis imps =
+  if isSubmodule then
+   case src of
+     Left _ ->
+         -- importing submodule by FilePath is an error.
+         fail $ "`import submodule PATHNAME` is not allowed."
+         -- NOTE: this is allowed by parser (thus we can get here).
+         -- FIXME: Would we want to implement this check in the typechecker?
+     Right modName ->
+         -- importing submodule by name:
+         do
+         let modNameTxt = C.modNameToText modName
+         mName <- resolveIdentifier' C.NSModule env modNameTxt
+           -- FIXME: are submodule name dups dealt with??
+         name <-
+           case mName of
+             Nothing -> fail $ "submodule `"
+                               <> Text.unpack modNameTxt
+                               <> "` is not in scope"
+             Just nm -> return nm
+         print $ "name = " ++ show (name :: T.Name)
+         print $ "submodule: " <> (C.identText $ MN.nameIdent name)
+         -- let import' = error "NIY"
+         _nmEnv <-
+           case ME.modContextOf (P.ImpNested name) (eModuleEnv env) of
+             Just mc -> do
+                        -- putStrLn "\nexported:" >> print (ME.mctxExported mc)
+                        let ne =
+                             MN.filterUNames
+                               (`Set.member` ME.mctxExported mc)
+                               (ME.mctxNames mc)
+
+                        return ne
+             Nothing -> panic "modContextOf" []
+         return env
+           -- FIXME: partial implementation here in this function, so
+           --        let's just be a nop, eventually we'll have this:
+           --        {eImports = import' : eImports env }
+           -- FIXME: possibly need to do the `C.mapImports` here also.
+
+  else -- importing full module:
+    do
+    mod' <- loadAndTranslateModule sc src
+    let import' = mkImport False vis (locatedUnknown (T.mName mod')) as imps
+    return $ C.mapImports (\imports -> import':imports) env
+
 
 -- | Create an entry for the `eImports` list in `CryptolEnv`.
 mkImport :: C.IsSubmodule

From bc3492b79c439dca1352e373a1cce15725303905 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 30 May 2026 14:48:18 -0700
Subject: [PATCH 05/17] refactor: generalize isSubModule to ImportInfo

---
 .../src/CryptolSAWCore/Cryptol.hs             |  5 ++
 .../src/CryptolSAWCore/CryptolEnv.hs          | 55 ++++++++++---------
 2 files changed, 33 insertions(+), 27 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
index d39832158e..54a1953c8e 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
@@ -28,6 +28,7 @@ module CryptolSAWCore.Cryptol
   ( module CryptolSAWCore.GlobalCryptolEnv
   , ImportVisibility(..)
   , IsSubmodule
+  , ImportInfo(..)
 
   , isErasedProp
   , proveProp
@@ -121,6 +122,10 @@ import qualified CryptolSAWCore.Pretty as CryPP
 import CryptolSAWCore.GlobalCryptolEnv
 
 
+-- | capture extra information needed for "import submodule"
+data ImportInfo = ImportNested C.Name  -- ^ "import submodule ..."
+                | ImportTop            -- ^ "import ...
+
 -- | bindTParam' - create a binding for a type parameter, returning 3-tuple:
 --                 - environment
 --                 - the SAWCore kind of the parameter
diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index 2b0225b977..73005df00a 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -230,9 +230,9 @@ initCryptolEnv sc = do
       arrayName'            = locatedUnknown arrayName
 
   let env0 = C.mapImports (\_ ->
-            [ mkImport False OnlyPublic preludeName'          Nothing Nothing
-            , mkImport False OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing
-            , mkImport False OnlyPublic arrayName'            Nothing Nothing
+            [ mkImport C.ImportTop OnlyPublic preludeName'          Nothing Nothing
+            , mkImport C.ImportTop OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing
+            , mkImport C.ImportTop OnlyPublic arrayName'            Nothing Nothing
             ]) $ C.initEnv
   C.addRefPrims sc refPrims
   -- Generate SAWCore translations for all values in scope
@@ -319,10 +319,10 @@ getNamingEnv sc env = do
 
 -- | Extend the `MR.NamingEnv` for one `T.Import`.
 getNamingEnvForImport :: ME.ModuleEnv
-                      -> (C.IsSubmodule, ImportVisibility, T.Import)
+                      -> (C.ImportInfo, ImportVisibility, T.Import)
                       -> MR.NamingEnv
                       -> MR.NamingEnv
-getNamingEnvForImport modEnv (isSubmod, vis, imprt) nmEnv0 =
+getNamingEnvForImport modEnv (importInfo, vis, imprt) nmEnv0 =
   nmEnv1 <> nmEnv0
 
   where
@@ -334,25 +334,26 @@ getNamingEnvForImport modEnv (isSubmod, vis, imprt) nmEnv0 =
     $ baseNamingEnvToAdd
 
   baseNamingEnvToAdd =
-    if isSubmod then
-      -- find the submodule in the current environment (`nmEnv0`) and compute
-      -- namingEnv:
-      error "isSubmod"
+    case importInfo of
+      C.ImportNested _n ->
+          -- find the submodule in the current environment (`nmEnv0`)
+          -- and compute namingEnv:
+          error "NIY: import submodule"
 
-    else
-      -- find the top-level loaded module and compute NamingEnv:
-      --   NOTE: does not depend on `nmEnv0`
-      let
-        modName :: C.ModName
-        modName = P.thing $ T.iModule imprt
+      C.ImportTop ->
+        -- find the top-level loaded module and compute NamingEnv:
+        --   NOTE: does not depend on `nmEnv0`
+        let
+          modName :: C.ModName
+          modName = P.thing $ T.iModule imprt
 
-        lm = case ME.lookupModule modName modEnv of
-               Just lm' -> lm'
-               Nothing  -> panic "getNamingEnvForImport"
-                             ["cannot lookupModule: " <> CryPP.pp modName]
+          lm = case ME.lookupModule modName modEnv of
+                 Just lm' -> lm'
+                 Nothing  -> panic "getNamingEnvForImport"
+                               ["cannot lookupModule: " <> CryPP.pp modName]
 
-      in
-        computeNamingEnv lm vis
+        in
+          computeNamingEnv lm vis
 
 
 -- | Compute a `MR.NamingEnv` for a loaded module based on the
@@ -649,7 +650,7 @@ bindLoadedModule ::
   SharedContext -> (P.ModName, P.Located C.ModName) -> CryptolEnv -> IO CryptolEnv
 bindLoadedModule _ (asName, origName) env =
   return $ C.mapImports
-    ((:) (mkImport False PublicAndPrivate origName (Just asName) Nothing)) env
+    ((:) (mkImport C.ImportTop PublicAndPrivate origName (Just asName) Nothing)) env
 
 -- | bindCryptolModule - when we have the @cryptol_prims ()@ created
 --   object, add the `CryptolModule` to the relevant maps in the
@@ -895,18 +896,18 @@ importCryptolModule sc env src as isSubmodule vis imps =
   else -- importing full module:
     do
     mod' <- loadAndTranslateModule sc src
-    let import' = mkImport False vis (locatedUnknown (T.mName mod')) as imps
+    let import' = mkImport C.ImportTop vis (locatedUnknown (T.mName mod')) as imps
     return $ C.mapImports (\imports -> import':imports) env
 
 
 -- | Create an entry for the `eImports` list in `CryptolEnv`.
-mkImport :: C.IsSubmodule
+mkImport :: C.ImportInfo
          -> ImportVisibility
          -> P.Located C.ModName
          -> Maybe C.ModName
          -> Maybe T.ImportSpec
-         -> (C.IsSubmodule, ImportVisibility, T.Import)
-mkImport isSubmodule vis nm as imps =
+         -> (C.ImportInfo, ImportVisibility, T.Import)
+mkImport importKind vis nm as imps =
     let im = T.Import { T.iModule = nm
                       , T.iAs     = as
                       , T.iSpec   = imps
@@ -914,7 +915,7 @@ mkImport isSubmodule vis nm as imps =
                       , T.iDoc    = Nothing
                       }
     in
-    (isSubmodule, vis, im)
+    (importKind, vis, im)
 
 
 ---- Binding -------------------------------------------------------------------

From e0957f8081e8c38ada445ef29272b684837b9eb4 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Fri, 5 Jun 2026 22:40:06 -0700
Subject: [PATCH 06/17] feat: new code to support submodule import

---
 .../src/CryptolSAWCore/CryptolEnv.hs          | 214 ++++++++++++------
 1 file changed, 148 insertions(+), 66 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index 73005df00a..dd111ce3c4 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -103,6 +103,7 @@ import           Cryptol.Utils.Ident
                            , mkIdent, interactiveName, identText
                            , textToModName
                            , prelPrim)
+import           Cryptol.Utils.PP (pretty) -- pp, Doc
 
 -- local:
 import qualified CryptolSAWCore.Cryptol as C
@@ -117,6 +118,9 @@ import           SAWCore.SharedTerm (NameInfo, SharedContext, Term, ppTerm)
 import           SAWSupport.Console
 import qualified SAWSupport.Pretty as PPS
 
+-- FIXME: temporary:
+-- import qualified Debug.Trace as TR
+
 ---- Key Types -----------------------------------------------------------------
 
 -- | Input to send to Cryptol's parser, including the starting source position.
@@ -317,7 +321,7 @@ getNamingEnv sc env = do
            mempty
            (eImports env))
 
--- | Extend the `MR.NamingEnv` for one `T.Import`.
+-- | Extend the `MR.NamingEnv` for a single `T.Import`.
 getNamingEnvForImport :: ME.ModuleEnv
                       -> (C.ImportInfo, ImportVisibility, T.Import)
                       -> MR.NamingEnv
@@ -328,33 +332,66 @@ getNamingEnvForImport modEnv (importInfo, vis, imprt) nmEnv0 =
   where
   nmEnv1 =
       MN.interpImportEnv'
-        MN.nameToPNameWithQualifiers (T.iAs imprt) (T.iSpec imprt)
+        nameToPName (T.iAs imprt) (T.iSpec imprt)
            -- adjusting for qualified imports
     $ MN.namingEnvNames
     $ baseNamingEnvToAdd
 
+  -- For submodules, strip the submodule nesting to get unqualified names.
+  -- For top-level modules, use nameToPNameWithQualifiers to preserve paths.
+  nameToPName =
+    case importInfo of
+      C.ImportNested nm -> stripSubmodulePrefix nm
+      C.ImportTop       -> MN.nameToPNameWithQualifiers
+
   baseNamingEnvToAdd =
     case importInfo of
-      C.ImportNested _n ->
-          -- find the submodule in the current environment (`nmEnv0`)
-          -- and compute namingEnv:
-          error "NIY: import submodule"
+      C.ImportNested nm ->
+          -- find the submodule in the current environment and compute namingEnv
+          -- respecting the visibility parameter (PublicAndPrivate vs OnlyPublic)
+          case ME.modContextOf (P.ImpNested nm) modEnv of
+              Just mc ->
+                case vis of
+                  PublicAndPrivate ->
+                    -- Include all names (public and private) from the submodule
+                    ME.mctxNames mc
+                  OnlyPublic ->
+                    -- Include only exported names
+                    MN.filterUNames (`Set.member` ME.mctxExported mc)
+                                    (ME.mctxNames mc)
+              Nothing -> panic "getNamingEnvForImport"
+                               ["name: " <> Text.pack (show nm)]
 
       C.ImportTop ->
-        -- find the top-level loaded module and compute NamingEnv:
-        --   NOTE: does not depend on `nmEnv0`
-        let
-          modName :: C.ModName
-          modName = P.thing $ T.iModule imprt
-
-          lm = case ME.lookupModule modName modEnv of
-                 Just lm' -> lm'
-                 Nothing  -> panic "getNamingEnvForImport"
-                               ["cannot lookupModule: " <> CryPP.pp modName]
-
-        in
-          computeNamingEnv lm vis
-
+          -- find the top-level loaded module and compute NamingEnv:
+          --   NOTE: does not depend on `nmEnv0`
+          let
+            modName :: C.ModName
+            modName = P.thing $ T.iModule imprt
+
+            lm = case ME.lookupModule modName modEnv of
+                   Just lm' -> lm'
+                   Nothing  -> panic "getNamingEnvForImport"
+                                 ["cannot lookupModule: " <> CryPP.pp modName]
+          in
+            computeNamingEnv lm vis
+
+
+-- | Strip the submodule path prefix from a Name.
+-- E.g., intuitively:
+--    stripSubmodulePrefix "X.Y" "X.Y.Z.name" == "Z.name"
+--
+stripSubmodulePrefix :: MN.Name -> MN.Name -> P.PName
+stripSubmodulePrefix submodName name =
+  case C.modPathCommon submodPath (MN.nameModPath name) of
+    Just (_, [], path) | not (null path) ->
+        P.Qual (C.packModName (map C.identText path)) nmIdent
+    _ ->
+        P.UnQual' nmIdent (MN.nameSrc name)
+  where
+  nmIdent = MN.nameIdent name
+  submodPath = C.Nested (MN.nameModPath submodName)
+                        (MN.nameIdent submodName)
 
 -- | Compute a `MR.NamingEnv` for a loaded module based on the
 --   `ImportVisibility`.
@@ -371,7 +408,6 @@ computeNamingEnv lm vis =
     --    - Does not include privates in submodules (which makes for
     --      much of the complications of this function).
     --    - Includes everything in scope at the toplevel of 'lm' module
-
     envTopLevels :: MR.NamingEnv
     envTopLevels = ME.lmNamingEnv lm
 
@@ -740,7 +776,7 @@ extractDefFromExtCryptolModule sc env_0 ecm name =
 
 -- | Load a Cryptol module and translate its contents to SAWCore.
 --
--- There are three paths here:
+-- There are three paths that lead here:
 --    - `importCryptolModule`, which is the back end for SAWScript @import@
 --    - `loadExtCryptolModule`, which is the back end for SAWScript @cryptol_load@
 --    - `loadCryptolModule`, which is used for Rocq export and from crux-mir-comp
@@ -855,50 +891,97 @@ importCryptolModule ::
   IO CryptolEnv
 importCryptolModule sc env src as isSubmodule vis imps =
   if isSubmodule then
-   case src of
-     Left _ ->
-         -- importing submodule by FilePath is an error.
-         fail $ "`import submodule PATHNAME` is not allowed."
-         -- NOTE: this is allowed by parser (thus we can get here).
-         -- FIXME: Would we want to implement this check in the typechecker?
-     Right modName ->
-         -- importing submodule by name:
-         do
-         let modNameTxt = C.modNameToText modName
-         mName <- resolveIdentifier' C.NSModule env modNameTxt
-           -- FIXME: are submodule name dups dealt with??
-         name <-
-           case mName of
-             Nothing -> fail $ "submodule `"
-                               <> Text.unpack modNameTxt
-                               <> "` is not in scope"
-             Just nm -> return nm
-         print $ "name = " ++ show (name :: T.Name)
-         print $ "submodule: " <> (C.identText $ MN.nameIdent name)
-         -- let import' = error "NIY"
-         _nmEnv <-
-           case ME.modContextOf (P.ImpNested name) (eModuleEnv env) of
-             Just mc -> do
-                        -- putStrLn "\nexported:" >> print (ME.mctxExported mc)
-                        let ne =
-                             MN.filterUNames
-                               (`Set.member` ME.mctxExported mc)
-                               (ME.mctxNames mc)
-
-                        return ne
-             Nothing -> panic "modContextOf" []
-         return env
-           -- FIXME: partial implementation here in this function, so
-           --        let's just be a nop, eventually we'll have this:
-           --        {eImports = import' : eImports env }
-           -- FIXME: possibly need to do the `C.mapImports` here also.
-
-  else -- importing full module:
+    -- importing submodule (which is in current scope):
+    case src of
+      Left _ ->
+          fail $ "`import submodule PATHNAME` is not allowed."
+          -- NOTE: this is allowed by parser (thus we can reach this code).
+          -- FIXME: Would we want to implement this check in the typechecker?
+
+      Right modName ->
+          -- importing submodule by name:
+          do
+          let modNameTxt = C.modNameToText modName
+          mName <- resolveIdentifier' C.NSModule env modNameTxt
+          name <- case mName of
+              Nothing -> fail $ "submodule `"
+                                <> Text.unpack modNameTxt
+                                <> "` is not in scope or ambiguous"
+                         -- FIXME: distinguish dups from not in scope!
+              Just nm -> return nm
+
+          let import' = mkImport
+                          (C.ImportNested name)
+                          vis (locatedUnknown modName) as imps
+                        -- FIXME[MT]: verify the above works.
+                        -- FIXME: modname unused?
+                        --   Refactor to make unnecessary?
+
+          -- DEBUG:
+          when debug $
+            do
+            putStrLn $ "modName = " ++ show modName
+            putStrLn $ "name = " ++ show (name :: T.Name)
+            putStrLn $ "submodule: "
+                        ++ (Text.unpack $ C.identText $ MN.nameIdent name)
+            debugImportMT env import'
+
+          return $ env {eImports = import' : eImports env }
+            -- FIXME: need to do the `C.mapImports` here also?
+
+  else -- importing full module (by path or name):
     do
     mod' <- loadAndTranslateModule sc src
-    let import' = mkImport C.ImportTop vis (locatedUnknown (T.mName mod')) as imps
+    let modName = locatedUnknown (T.mName mod')
+    let import' = mkImport C.ImportTop vis modName as imps
+
+    -- DEBUG:
+    when debug $ putStrLn $ "modName= " ++ show modName
+    when debug $ debugImportMT env' import'
+
     return $ C.mapImports (\imports -> import':imports) env
 
+debug :: Bool
+debug = False
+
+-- Function to print a NamingEnv to stdout
+printNamingEnv :: MN.NamingEnv -> IO ()
+printNamingEnv = putStrLn . pretty
+
+{-
+DEBUG: print what users of the import will get (~ dup-ing getNamingEnvForImport)
+-}
+debugImportMT :: CryptolEnv
+              -> (C.ImportInfo, ImportVisibility, T.Import)
+              -> IO ()
+debugImportMT env (info,vis,imprt) =
+  do
+  putStrLn $ "vis: " ++ show vis
+  case vis of
+    OnlyPublic -> return ()
+    _          ->
+        do
+        let ne1_OP =
+                getNamingEnvForImport modEnv (info,OnlyPublic,imprt) mempty
+        putStrLn "ne1_OP (ne1 but only public):"
+        printNamingEnv ne1_OP -- OnlyPublic
+
+  let ne1    = getNamingEnvForImport modEnv (info,vis,imprt) mempty
+  putStrLn "\nimprt:"
+  print imprt
+  putStrLn "\nne1:"
+  printNamingEnv ne1
+
+  where
+  modEnv = eModuleEnv env
+
+  modName :: C.ModName
+  modName = P.thing $ T.iModule imprt
+
+  _lm = case ME.lookupModule modName modEnv of
+         Just lm' -> lm'
+         Nothing  -> panic "debugImportMT: getNamingEnvForImport"
+                       ["cannot lookupModule: " <> CryPP.pp modName]
 
 -- | Create an entry for the `eImports` list in `CryptolEnv`.
 mkImport :: C.ImportInfo
@@ -907,7 +990,7 @@ mkImport :: C.ImportInfo
          -> Maybe C.ModName
          -> Maybe T.ImportSpec
          -> (C.ImportInfo, ImportVisibility, T.Import)
-mkImport importKind vis nm as imps =
+mkImport importInfo vis nm as imps =
     let im = T.Import { T.iModule = nm
                       , T.iAs     = as
                       , T.iSpec   = imps
@@ -915,7 +998,7 @@ mkImport importKind vis nm as imps =
                       , T.iDoc    = Nothing
                       }
     in
-    (importKind, vis, im)
+    (importInfo, vis, im)
 
 
 ---- Binding -------------------------------------------------------------------
@@ -1021,8 +1104,7 @@ resolveIdentifier' ::
   SharedContext -> CryptolEnv -> C.NameSpace -> Text -> IO (Maybe T.Name)
 resolveIdentifier' sc env nameSpace nm =
   case splitOn (pack "::") nm of
-    []  -> pure Nothing
-           -- FIXME: shouldn't this be error?
+    []  -> panic "resolveIdentifier'" ["splitOn returning []!"]
     [i] -> doResolve (P.mkUnqual (C.mkIdent i))
     xs  -> let (qs,i) = (init xs, last xs)
            in  doResolve (P.Qual (C.packModName qs) (C.mkIdent i))

From a33476087be54ffe86e3f6fe61f2ecbe579eb718 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 6 Jun 2026 20:41:49 -0700
Subject: [PATCH 07/17] test: extend/update tests in
 intTests/test_saw_submodule_import/

---
 intTests/test_saw_submodule_access1/D.cry     |  4 +-
 intTests/test_saw_submodule_import/F.cry      | 27 +++++++++++++
 .../cryptol-bug/D.cry                         |  4 ++
 .../cryptol-bug/F.cry                         | 16 ++++++++
 .../cryptol-bug/G.cry                         | 40 +++++++++++++++++++
 .../testGoodImport1.log.good                  |  6 +++
 .../testGoodImport1.saw                       | 26 ++++++++++++
 .../testGoodImport2.log.good                  |  7 ++++
 .../testGoodImport2.saw                       | 27 +++++++++++++
 .../testGoodImport3.log.good                  | 19 +++++++++
 .../testGoodImport3.saw                       | 22 ++++++++++
 .../testGoodImport4.log.good                  | 20 ++++++++++
 .../testGoodImport4.saw                       | 19 +++++++++
 .../testGoodImport5.saw                       | 12 ++++++
 .../testImportErrors1.saw                     |  1 +
 .../testImportErrors2.log.good                |  2 +-
 .../testImportErrors2.saw                     |  2 +
 .../testImportErrors3.log.good                |  6 +++
 .../testImportErrors3.saw                     |  4 ++
 19 files changed, 262 insertions(+), 2 deletions(-)
 create mode 100644 intTests/test_saw_submodule_import/F.cry
 create mode 100644 intTests/test_saw_submodule_import/cryptol-bug/D.cry
 create mode 100644 intTests/test_saw_submodule_import/cryptol-bug/F.cry
 create mode 100644 intTests/test_saw_submodule_import/cryptol-bug/G.cry
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport2.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport2.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport3.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport3.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport4.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport4.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport5.saw
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors3.log.good
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors3.saw

diff --git a/intTests/test_saw_submodule_access1/D.cry b/intTests/test_saw_submodule_access1/D.cry
index c806e3e091..1d0414090c 100644
--- a/intTests/test_saw_submodule_access1/D.cry
+++ b/intTests/test_saw_submodule_access1/D.cry
@@ -14,6 +14,7 @@ submodule D2 where
 
   submodule D3 where
     d3 = d00 + d2 + 1  // 14229
+    d4 = d5
 
     type D3TySy = [32]
 
@@ -21,5 +22,6 @@ submodule D2 where
 //  - type synonyms and values
 d01 : D2::D3::D3TySy
 d01 = 5 + D2::d2   // D2 is not referencable till now!
-    + D2::D3::d3   
+    + D2::D3::d3
 
+d5 = 1  // we can reference this from above submodule!
diff --git a/intTests/test_saw_submodule_import/F.cry b/intTests/test_saw_submodule_import/F.cry
new file mode 100644
index 0000000000..bc327efc59
--- /dev/null
+++ b/intTests/test_saw_submodule_import/F.cry
@@ -0,0 +1,27 @@
+module F where
+
+import D as D_A (d00, notinscope)
+import D as D_B hiding (d00, notinscope)
+
+x = D_A::d00
+
+// NOTE: one cannot import qualified names in 'D', e.g., D2::d2, D2::D3
+import D(d00)             //
+import D                  // D2 now in scope
+import D(D2)              // D2 in scope
+import D hiding (D2,d01)  // cryptol allows us to hide submodule D2
+
+import submodule D2 (d2,D3)
+
+x2 = d2
+
+import submodule D3 (d3)
+
+x3 = d3
+
+submodule D2a = submodule D2
+
+x4 = D2a::d2
+
+submodule FSubMod where
+  d3' = 1 + x4
diff --git a/intTests/test_saw_submodule_import/cryptol-bug/D.cry b/intTests/test_saw_submodule_import/cryptol-bug/D.cry
new file mode 100644
index 0000000000..c2ac844c56
--- /dev/null
+++ b/intTests/test_saw_submodule_import/cryptol-bug/D.cry
@@ -0,0 +1,4 @@
+module D where
+
+submodule D2 where
+  d2 = 2
diff --git a/intTests/test_saw_submodule_import/cryptol-bug/F.cry b/intTests/test_saw_submodule_import/cryptol-bug/F.cry
new file mode 100644
index 0000000000..612494c2fe
--- /dev/null
+++ b/intTests/test_saw_submodule_import/cryptol-bug/F.cry
@@ -0,0 +1,16 @@
+module F where
+
+import D                   // D2 now in scope
+
+submodule D2a = submodule D2  // PREVIEW: problematic when F imported.
+
+x1 = D2a::d2                  // sanity check.
+
+submodule D3 where            // PREVIEW: works as expected.
+  d3 = 3
+
+private submodule D4 where    // PREVIEW: works as expected.
+  d4 = 4
+
+submodule D4a = submodule D4  // PREVEW: works as expected
+                              //   D4a is public alias to private submodule
diff --git a/intTests/test_saw_submodule_import/cryptol-bug/G.cry b/intTests/test_saw_submodule_import/cryptol-bug/G.cry
new file mode 100644
index 0000000000..6bf3ab72ce
--- /dev/null
+++ b/intTests/test_saw_submodule_import/cryptol-bug/G.cry
@@ -0,0 +1,40 @@
+module G where
+
+import F
+
+// things work when D3 is submodule defined in F:
+import submodule D3
+x1 = d3
+
+
+// things work when D4a is an alias to private sub-module of F:
+import submodule D4a
+x2 = d4
+
+
+/*
+// when we try to import private submodule, we get reasonable error:
+import submodule D4  // gives error HERE.
+                     //   Module not in scope: D4
+x3 = d4              // doesn't get here.
+*/
+
+
+/*
+// Gives slightly suspicious errors/non-errors
+// when we try to import a submodule "two imports away" that should not be
+// visible.
+import submodule D2
+  // INTERESTING and SUSPICIOUS:
+  //   The submodule D2 is not in scope, but we do not get this message
+  //     "Module not in scope: D2"
+  //   -
+x4 = d2
+  // This gives error:
+  //   Value not in scope: d2
+*/
+
+// The problematic case:
+import submodule D2a
+x5 = d2
+     // d2 reference crashes cryptol.
diff --git a/intTests/test_saw_submodule_import/testGoodImport1.log.good b/intTests/test_saw_submodule_import/testGoodImport1.log.good
index 4d67535fe7..2016318ff8 100644
--- a/intTests/test_saw_submodule_import/testGoodImport1.log.good
+++ b/intTests/test_saw_submodule_import/testGoodImport1.log.good
@@ -1,2 +1,8 @@
 Loading file "testGoodImport1.saw"
+12114
+14229
+14229
+12114
+14229
+14229
 done
diff --git a/intTests/test_saw_submodule_import/testGoodImport1.saw b/intTests/test_saw_submodule_import/testGoodImport1.saw
index 71edc9f5ad..0632fc7575 100644
--- a/intTests/test_saw_submodule_import/testGoodImport1.saw
+++ b/intTests/test_saw_submodule_import/testGoodImport1.saw
@@ -1,3 +1,29 @@
 import "D.cry";
 
+// access vars fully qualified:
+print {{D2::d2}};
+print {{D2::D3::d3}};
+
+// direct import of doubly nested submodule:
+import submodule D2::D3 as D2_D3;
+print {{D2_D3::d3}};
+
+
+// submodule D2 is in scope, let's import it:
+import submodule D2;
+
+// can now access `D2::d2` w/o "D2" prefix:
+print {{d2}};
+
+// and D3 is in scope:
+print {{D3::d3}};
+
+///////////////////////////////////////
+// Now test we can import what's brought in scope by import.
+
+// let's import submodule D3.
+import submodule D3;
+
+print {{d3}};  // can now access w/o "D3::" prefix.
+
 print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport2.log.good b/intTests/test_saw_submodule_import/testGoodImport2.log.good
new file mode 100644
index 0000000000..7c2f2d8336
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport2.log.good
@@ -0,0 +1,7 @@
+Loading file "testGoodImport2.saw"
+12114
+14229
+12114
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport2.saw b/intTests/test_saw_submodule_import/testGoodImport2.saw
new file mode 100644
index 0000000000..d45f02745d
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport2.saw
@@ -0,0 +1,27 @@
+// This test mirrors testGoodImport1 but with "import submodule ... as ..."
+//                                                                  --
+
+import "D.cry";
+
+// access vars fully qualified:
+print {{D2::d2}};
+print {{D2::D3::d3}};
+
+// submodule D2 is in scope, let's import it qualified:
+import submodule D2 as MYD2;
+
+// can now access elements w/ "MYD2" prefix:
+print {{MYD2::d2}};
+
+// and we can accesss submodule D3 via MYD2::D3
+print {{MYD2::D3::d3}};
+
+///////////////////////////////////////
+// Now test we can import what's brought in scope by import.
+
+// let's import submodule D3:
+import submodule MYD2::D3 as MYD3;
+
+print {{MYD3::d3}}; // can now access w/ "MYD3::" prefix.
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport3.log.good b/intTests/test_saw_submodule_import/testGoodImport3.log.good
new file mode 100644
index 0000000000..e5009a6445
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport3.log.good
@@ -0,0 +1,19 @@
+Loading file "testGoodImport3.saw"
+12114
+Error: Cryptol: [error] at testGoodImport3.saw:13:22--13:28
+    Value not in scope: D3::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport3.saw:13:1-13:33 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport3.saw:19:27--19:33
+    Type not in scope: D2TySy
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport3.saw:19:1-19:39 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport3.saw b/intTests/test_saw_submodule_import/testGoodImport3.saw
new file mode 100644
index 0000000000..bb270debef
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport3.saw
@@ -0,0 +1,22 @@
+// Exercise more of the `import submodule` variances.
+
+import "D.cry";
+
+import submodule D2 (d2);
+
+print {{d2}};
+
+// expected failures:
+
+// test 1: ensure submodules of D2 are not in scope: /////
+
+fails ( do { print {{D3::d3}}; } );
+  // should fail b/c D3 & D3::d3 are not in scope
+
+
+// test 2: ensure types in D2 are not in scope: //////////
+
+fails ( do { print {{ 0 : D2TySy }}; } );
+  // should fail b/c D2TySy is not in scope
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport4.log.good b/intTests/test_saw_submodule_import/testGoodImport4.log.good
new file mode 100644
index 0000000000..6409e5e0d4
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport4.log.good
@@ -0,0 +1,20 @@
+Loading file "testGoodImport4.saw"
+14229
+0
+Error: Cryptol: [error] at testGoodImport4.saw:16:22--16:24
+    Value not in scope: d2
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport4.saw:16:1-16:29 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport4.saw:17:26--17:32
+    Type not in scope: D2TySy
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport4.saw:17:1-17:37 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport4.saw b/intTests/test_saw_submodule_import/testGoodImport4.saw
new file mode 100644
index 0000000000..f3a402792f
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport4.saw
@@ -0,0 +1,19 @@
+// Exercise more of the `import submodule` variances.
+
+import "D.cry";
+
+import submodule D2 hiding (d2 D2TySy);
+
+
+// test 1: check we can access names not hid:
+
+print {{D3::d3 }};
+print {{0 : D3::D3TySy }};
+
+
+// test 2: ensure hidden symbols are hiddden:
+
+fails ( do { print {{d2}}; } );
+fails ( do { print {{0 : D2TySy}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport5.saw b/intTests/test_saw_submodule_import/testGoodImport5.saw
new file mode 100644
index 0000000000..35c4a785f6
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport5.saw
@@ -0,0 +1,12 @@
+// Exercise more of the `import submodule` variances.
+
+import "D.cry";
+
+import submodule D2::D3 as X::Y::Z;
+
+// test 1: check we can access names not hid:
+
+print {{ X::Y::Z::d3 }};
+print {{ 0 : X::Y::Z::D3TySy }};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors1.saw b/intTests/test_saw_submodule_import/testImportErrors1.saw
index f62a753078..ad4ff5d3a2 100644
--- a/intTests/test_saw_submodule_import/testImportErrors1.saw
+++ b/intTests/test_saw_submodule_import/testImportErrors1.saw
@@ -1,3 +1,4 @@
 import submodule "D.cry";
+  // An error to "import submodule" a top-level module.
 
 print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors2.log.good b/intTests/test_saw_submodule_import/testImportErrors2.log.good
index 6449490fbb..d12bf560e1 100644
--- a/intTests/test_saw_submodule_import/testImportErrors2.log.good
+++ b/intTests/test_saw_submodule_import/testImportErrors2.log.good
@@ -1,6 +1,6 @@
 Loading file "testImportErrors2.saw"
 Stack trace:
    (builtin) (at top level)
-`import submodule` is unsupported.
+submodule `D` is not in scope or ambiguous
 
 FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors2.saw b/intTests/test_saw_submodule_import/testImportErrors2.saw
index 2e4c424cc1..7377c1c027 100644
--- a/intTests/test_saw_submodule_import/testImportErrors2.saw
+++ b/intTests/test_saw_submodule_import/testImportErrors2.saw
@@ -1,3 +1,5 @@
 import submodule D;
+  // D is not in scope, thus an error.
+  // NOTE: we do not search for top-level modules named 'D'.
 
 print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors3.log.good b/intTests/test_saw_submodule_import/testImportErrors3.log.good
new file mode 100644
index 0000000000..db55677faf
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors3.log.good
@@ -0,0 +1,6 @@
+Loading file "testImportErrors3.saw"
+Stack trace:
+   (builtin) (at top level)
+submodule `D3` is not in scope or ambiguous
+
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors3.saw b/intTests/test_saw_submodule_import/testImportErrors3.saw
new file mode 100644
index 0000000000..8a03492d9b
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors3.saw
@@ -0,0 +1,4 @@
+import "D.cry";
+
+// import submodule D2::D3;   // this would work
+import submodule D3;          // this should *not* work

From 84adc7c26b68db32fe5fe3705e139a4175b15162 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Fri, 26 Jun 2026 14:50:32 -0700
Subject: [PATCH 08/17] test: fix to support new sub/module import syntax

---
 intTests/test_saw_submodule_import/testGoodImport4.saw | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/intTests/test_saw_submodule_import/testGoodImport4.saw b/intTests/test_saw_submodule_import/testGoodImport4.saw
index f3a402792f..a9a93d284e 100644
--- a/intTests/test_saw_submodule_import/testGoodImport4.saw
+++ b/intTests/test_saw_submodule_import/testGoodImport4.saw
@@ -2,7 +2,7 @@
 
 import "D.cry";
 
-import submodule D2 hiding (d2 D2TySy);
+import submodule D2 hiding (d2, D2TySy);
 
 
 // test 1: check we can access names not hid:

From 607203727d83250a9572b0dd688544cfe92ffbb5 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 15 Aug 2026 20:02:48 -0700
Subject: [PATCH 09/17] FIXME: fix existing type-errors (now builds, but ...)

---
 .../src/CryptolSAWCore/Cryptol.hs             |  5 ---
 .../src/CryptolSAWCore/CryptolEnv.hs          | 34 +++++++++++--------
 .../src/CryptolSAWCore/GlobalCryptolEnv.hs    | 19 ++++++++---
 3 files changed, 34 insertions(+), 24 deletions(-)

diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
index 54a1953c8e..d0d0fcf588 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
@@ -27,7 +27,6 @@ between these two modules is mostly a function of historical accident.
 module CryptolSAWCore.Cryptol
   ( module CryptolSAWCore.GlobalCryptolEnv
   , ImportVisibility(..)
-  , IsSubmodule
   , ImportInfo(..)
 
   , isErasedProp
@@ -122,10 +121,6 @@ import qualified CryptolSAWCore.Pretty as CryPP
 import CryptolSAWCore.GlobalCryptolEnv
 
 
--- | capture extra information needed for "import submodule"
-data ImportInfo = ImportNested C.Name  -- ^ "import submodule ..."
-                | ImportTop            -- ^ "import ...
-
 -- | bindTParam' - create a binding for a type parameter, returning 3-tuple:
 --                 - environment
 --                 - the SAWCore kind of the parameter
diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index dd111ce3c4..1d15576739 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -305,7 +305,6 @@ ioParseResult res = case res of
 --   on with `MR.shadowing` so they hide any imported occurrences.
 --   The environment for each scoping level then shadows everything
 --   above it.
-
 --
 --   Note that while each `sImports` is (mostly) maintained with more
 --   recent imports at the front of the list, this should be
@@ -321,9 +320,9 @@ getNamingEnv sc env = do
            mempty
            (eImports env))
 
--- | Extend the `MR.NamingEnv` for a single `T.Import`.
+-- | Extend the `MR.NamingEnv` for a single import (`ImportData)
 getNamingEnvForImport :: ME.ModuleEnv
-                      -> (C.ImportInfo, ImportVisibility, T.Import)
+                      -> ImportData
                       -> MR.NamingEnv
                       -> MR.NamingEnv
 getNamingEnvForImport modEnv (importInfo, vis, imprt) nmEnv0 =
@@ -902,7 +901,7 @@ importCryptolModule sc env src as isSubmodule vis imps =
           -- importing submodule by name:
           do
           let modNameTxt = C.modNameToText modName
-          mName <- resolveIdentifier' C.NSModule env modNameTxt
+          mName <- resolveIdentifier' sc env C.NSModule modNameTxt
           name <- case mName of
               Nothing -> fail $ "submodule `"
                                 <> Text.unpack modNameTxt
@@ -924,10 +923,10 @@ importCryptolModule sc env src as isSubmodule vis imps =
             putStrLn $ "name = " ++ show (name :: T.Name)
             putStrLn $ "submodule: "
                         ++ (Text.unpack $ C.identText $ MN.nameIdent name)
-            debugImportMT env import'
+            debugImportMT sc import'
 
-          return $ env {eImports = import' : eImports env }
-            -- FIXME: need to do the `C.mapImports` here also?
+          return $ C.mapImports (\imports -> import':imports) env
+            -- FIXME[MT]: Verify you understand what's happening.
 
   else -- importing full module (by path or name):
     do
@@ -937,7 +936,7 @@ importCryptolModule sc env src as isSubmodule vis imps =
 
     -- DEBUG:
     when debug $ putStrLn $ "modName= " ++ show modName
-    when debug $ debugImportMT env' import'
+    when debug $ debugImportMT sc import'
 
     return $ C.mapImports (\imports -> import':imports) env
 
@@ -949,13 +948,16 @@ printNamingEnv :: MN.NamingEnv -> IO ()
 printNamingEnv = putStrLn . pretty
 
 {-
-DEBUG: print what users of the import will get (~ dup-ing getNamingEnvForImport)
+DEBUG: print what users of the import will get (someawhat duplicating
+       getNamingEnvForImport)
 -}
-debugImportMT :: CryptolEnv
-              -> (C.ImportInfo, ImportVisibility, T.Import)
+debugImportMT :: SharedContext
+              -> ImportData
               -> IO ()
-debugImportMT env (info,vis,imprt) =
+debugImportMT sc (info,vis,imprt) =
   do
+  modEnv <- eModuleEnv sc
+
   putStrLn $ "vis: " ++ show vis
   case vis of
     OnlyPublic -> return ()
@@ -973,15 +975,17 @@ debugImportMT env (info,vis,imprt) =
   printNamingEnv ne1
 
   where
-  modEnv = eModuleEnv env
 
+  {-
   modName :: C.ModName
   modName = P.thing $ T.iModule imprt
 
+   -- FIXME[MT]: what was this: ?
   _lm = case ME.lookupModule modName modEnv of
          Just lm' -> lm'
          Nothing  -> panic "debugImportMT: getNamingEnvForImport"
                        ["cannot lookupModule: " <> CryPP.pp modName]
+  -}
 
 -- | Create an entry for the `eImports` list in `CryptolEnv`.
 mkImport :: C.ImportInfo
@@ -989,7 +993,7 @@ mkImport :: C.ImportInfo
          -> P.Located C.ModName
          -> Maybe C.ModName
          -> Maybe T.ImportSpec
-         -> (C.ImportInfo, ImportVisibility, T.Import)
+         -> ImportData
 mkImport importInfo vis nm as imps =
     let im = T.Import { T.iModule = nm
                       , T.iAs     = as
@@ -1101,7 +1105,7 @@ resolveIdentifier sc env = resolveIdentifier' sc env C.NSValue
 
 resolveIdentifier' ::
   (HasCallStack) =>
-  SharedContext -> CryptolEnv -> C.NameSpace -> Text -> IO (Maybe T.Name)
+  SharedContext -> CryptolEnv -> C.Namespace -> Text -> IO (Maybe T.Name)
 resolveIdentifier' sc env nameSpace nm =
   case splitOn (pack "::") nm of
     []  -> panic "resolveIdentifier'" ["splitOn returning []!"]
diff --git a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
index 83637ef0d4..6dcc629ab8 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
@@ -14,6 +14,9 @@ Portability : non-portable (language extensions)
 
 module CryptolSAWCore.GlobalCryptolEnv
   ( ImportVisibility(..)
+  , IsSubmodule
+  , ImportInfo(..)
+  , ImportData
   , isToplevel
   , sameHeight
   , pushScope
@@ -109,7 +112,15 @@ data ImportVisibility
                      --   and (arbitrarily nested) submodules.
   deriving (Eq, Show)
 
-type IsSubmodule = Bool  -- FIXME[MT]: right place?
+-- | type synonym indicating module is nested (is submodule)
+type IsSubmodule = Bool
+
+-- | capture extra information needed for "import submodule"
+data ImportInfo = ImportNested C.Name  -- ^ "import submodule ..."
+                | ImportTop            -- ^ "import ...
+
+type ImportData = (ImportInfo, ImportVisibility, C.Import)
+  -- FIXME: change to datatype.
 
 -- | The global environment for capturing the Cryptol state, both
 --   Cryptol's own state and the state associated with
@@ -183,7 +194,7 @@ instance IsMetadata GlobalCryptolEnv where
 
 data CryptolFrame =
   CryptolFrame { fNamingEnv :: MR.NamingEnv
-               , fImports :: [(ImportVisibility, C.Import)]
+               , fImports :: [ImportData]
                }
 
 initFrame :: CryptolFrame
@@ -235,7 +246,7 @@ mapNaming f = mapCurFrame $
 
 -- | Map the module imports of the frame currently in scope.
 mapImports ::
-  ([(ImportVisibility, C.Import)] -> [(ImportVisibility, C.Import)] ) ->
+  ([ImportData] -> [ImportData]) ->
   CryptolEnv ->
   CryptolEnv
 mapImports f = mapCurFrame $
@@ -541,7 +552,7 @@ eExtraNaming (CryptolEnv (frame :| frames)) =
 --   according to the associated 'ImportVisibility'. The modules here
 --   should only correspond to modules that are present in the module
 --   environment *and* have been translated into SAWCore.
-eImports :: CryptolEnv -> [(ImportVisibility, C.Import)]
+eImports :: CryptolEnv -> [ImportData]
 eImports (CryptolEnv frames) =
   concat $ map fImports $ NE.toList frames
 

From 227c1681f60a901c102591e6c1016ab01b306da6 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 15 Aug 2026 20:29:47 -0700
Subject: [PATCH 10/17] test: add vetted .log.good file

---
 intTests/test_saw_submodule_import/testGoodImport5.log.good | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport5.log.good

diff --git a/intTests/test_saw_submodule_import/testGoodImport5.log.good b/intTests/test_saw_submodule_import/testGoodImport5.log.good
new file mode 100644
index 0000000000..40c0d6a95a
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport5.log.good
@@ -0,0 +1,4 @@
+Loading file "testGoodImport5.saw"
+14229
+0
+done

From 0a441ee6e938037fd3ff3dc9ea1a344eada8b7ad Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 15 Aug 2026 22:52:08 -0700
Subject: [PATCH 11/17] test: add tests for `import` and `import submodule` of
 newtypes

---
 intTests/test_saw_import/M.cry                |  5 +++
 .../test_saw_import/testNewTypes.log.good     | 22 ++++++++++
 intTests/test_saw_import/testNewTypes.saw     | 12 +++++
 intTests/test_saw_submodule_import/M.cry      | 12 +++++
 .../testNewTypes.log.good                     | 44 +++++++++++++++++++
 .../testNewTypes.saw                          | 40 +++++++++++++++++
 6 files changed, 135 insertions(+)
 create mode 100644 intTests/test_saw_import/M.cry
 create mode 100644 intTests/test_saw_import/testNewTypes.log.good
 create mode 100644 intTests/test_saw_import/testNewTypes.saw
 create mode 100644 intTests/test_saw_submodule_import/M.cry
 create mode 100644 intTests/test_saw_submodule_import/testNewTypes.log.good
 create mode 100644 intTests/test_saw_submodule_import/testNewTypes.saw

diff --git a/intTests/test_saw_import/M.cry b/intTests/test_saw_import/M.cry
new file mode 100644
index 0000000000..cc4347482c
--- /dev/null
+++ b/intTests/test_saw_import/M.cry
@@ -0,0 +1,5 @@
+module M where
+newtype T = { x : Bit }
+t1 = T{x= 1}
+
+type U = T
diff --git a/intTests/test_saw_import/testNewTypes.log.good b/intTests/test_saw_import/testNewTypes.log.good
new file mode 100644
index 0000000000..167f53bded
--- /dev/null
+++ b/intTests/test_saw_import/testNewTypes.log.good
@@ -0,0 +1,22 @@
+Loading file "testNewTypes.saw"
+{x = True}
+{x = True}
+
+errors follow:
+
+Error: Cryptol: [error] at testNewTypes.saw:9:25--9:26
+    Type not in scope: T
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:9:1-9:31 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testNewTypes.saw:12:20--12:21
+    Value not in scope: T
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:12:1-12:31 (at top level)
+
+(Failure was expected, continuing)
diff --git a/intTests/test_saw_import/testNewTypes.saw b/intTests/test_saw_import/testNewTypes.saw
new file mode 100644
index 0000000000..a6aef1a09d
--- /dev/null
+++ b/intTests/test_saw_import/testNewTypes.saw
@@ -0,0 +1,12 @@
+import "M.cry" hiding (T);
+
+print {{ t1 }};
+print {{ t1:U }};
+
+print "\nerrors follow:\n";
+
+// the Type T (of the newtype) is hidden, will fail:
+fails (do{print {{ t1 : T }};}) ;
+
+// the constructor T of the newtype is hidden, will fail:
+fails (do{print {{ T{x=1} }};}) ;
diff --git a/intTests/test_saw_submodule_import/M.cry b/intTests/test_saw_submodule_import/M.cry
new file mode 100644
index 0000000000..29ddc72199
--- /dev/null
+++ b/intTests/test_saw_submodule_import/M.cry
@@ -0,0 +1,12 @@
+module M where
+
+submodule S1 where
+
+  newtype T1 = { x : [8] }
+
+  t11 = T1{x= 1}
+
+type T2 = S1::T1
+
+T2 = (S1::T1)
+t2 = T2{x=2}
diff --git a/intTests/test_saw_submodule_import/testNewTypes.log.good b/intTests/test_saw_submodule_import/testNewTypes.log.good
new file mode 100644
index 0000000000..5246c38aea
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testNewTypes.log.good
@@ -0,0 +1,44 @@
+Loading file "testNewTypes.saw"
+{x = 2}
+{x = 2}
+{x = 3}
+
+
+errors follow:
+
+
+Error: Cryptol: [error] at testNewTypes.saw:16:20--16:23
+    Value not in scope: t11
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:16:1-16:28 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testNewTypes.saw:19:25--19:27
+    Type not in scope: T1
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:19:1-19:32 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testNewTypes.saw:22:20--22:22
+    Value not in scope: T1
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:22:1-22:32 (at top level)
+
+(Failure was expected, continuing)
+
+
+M::S1::T1
+{x = 1}
+{x = 2}
+{x = 2}
+{x = 2}
+{x = 2}
+{x = 3}
+{x = 3}
+{x = 3}
diff --git a/intTests/test_saw_submodule_import/testNewTypes.saw b/intTests/test_saw_submodule_import/testNewTypes.saw
new file mode 100644
index 0000000000..6ca658c101
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testNewTypes.saw
@@ -0,0 +1,40 @@
+import "M.cry";
+
+print {{ t2 }};
+print {{ t2 : T2 }};
+print {{ T2{x=3} : T2 }};
+
+/* *******************************
+  errors:
+ */
+
+print "\n";
+print "errors follow:";
+print "\n";
+
+// cannot access t11 (in submodule)
+fails (do{print {{ t11 }};}) ;
+
+// cannot access T1 type (in submodule)
+fails (do{print {{ t2 : T1 }};}) ;
+
+// cannot access T1 constructor (in submodule)
+fails (do{print {{ T1{x=3} }};}) ;
+
+print "\n";
+
+/* *******************************
+   import the submodule and test:
+ */
+
+import submodule S1;
+
+print (type {{t11}}) ;
+print {{t11}}  ;
+print {{t2}}   ;
+print {{t2 : T2}} ;
+print {{t2 : T1}} ;
+print {{t2 : S1::T1}} ;
+print {{ T2{x=3} }} ;
+print {{ T1{x=3} }} ;
+print {{ T1{x=3} : T1 }} ;

From 15bb839fb4dacd99d733ebfcf0df86929be3f1bb Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Sat, 15 Aug 2026 23:01:39 -0700
Subject: [PATCH 12/17] test: whitespace

---
 intTests/test_saw_import/M.cry | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/intTests/test_saw_import/M.cry b/intTests/test_saw_import/M.cry
index cc4347482c..a6af940ee4 100644
--- a/intTests/test_saw_import/M.cry
+++ b/intTests/test_saw_import/M.cry
@@ -1,5 +1,7 @@
 module M where
+
 newtype T = { x : Bit }
+
 t1 = T{x= 1}
 
 type U = T

From cf354949d5514de2b223901676d6e128d1527f45 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Tue, 18 Aug 2026 19:05:35 -0700
Subject: [PATCH 13/17] test: add more tests for test_saw_submodule_import

---
 .../testGoodImport10.log.good                 |  6 +++++
 .../testGoodImport10.saw                      | 13 ++++++++++
 .../testGoodImport5.log.good                  | 25 +++++++++++++++++++
 .../testGoodImport5.saw                       | 12 ++++++++-
 .../testGoodImport6.log.good                  | 11 ++++++++
 .../testGoodImport6.saw                       | 14 +++++++++++
 .../testGoodImport8.log.good                  |  5 ++++
 .../testGoodImport8.saw                       | 19 ++++++++++++++
 8 files changed, 104 insertions(+), 1 deletion(-)
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport10.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport10.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport6.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport6.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport8.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport8.saw

diff --git a/intTests/test_saw_submodule_import/testGoodImport10.log.good b/intTests/test_saw_submodule_import/testGoodImport10.log.good
new file mode 100644
index 0000000000..dd5ab92aa2
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport10.log.good
@@ -0,0 +1,6 @@
+Loading file "testGoodImport10.saw"
+12114
+14229
+0
+0
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport10.saw b/intTests/test_saw_submodule_import/testGoodImport10.saw
new file mode 100644
index 0000000000..7f724458ce
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport10.saw
@@ -0,0 +1,13 @@
+// Test: Import with empty hiding list (should import everything)
+
+import "D.cry";
+
+import submodule D2 hiding ();
+
+// Everything should be accessible
+print {{d2}};
+print {{D3::d3}};
+print {{0 : D2TySy}};
+print {{0 : D3::D3TySy}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport5.log.good b/intTests/test_saw_submodule_import/testGoodImport5.log.good
index 40c0d6a95a..720ca07f6f 100644
--- a/intTests/test_saw_submodule_import/testGoodImport5.log.good
+++ b/intTests/test_saw_submodule_import/testGoodImport5.log.good
@@ -1,4 +1,29 @@
 Loading file "testGoodImport5.saw"
 14229
 0
+14229
+Error: Cryptol: [error] at testGoodImport5.saw:17:23--17:25
+    Value not in scope: d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport5.saw:17:1-17:31 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport5.saw:18:23--18:31
+    Value not in scope: Y::Z::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport5.saw:18:1-18:37 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport5.saw:19:23--19:31
+    Value not in scope: X::Y::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport5.saw:19:1-19:37 (at top level)
+
+(Failure was expected, continuing)
 done
diff --git a/intTests/test_saw_submodule_import/testGoodImport5.saw b/intTests/test_saw_submodule_import/testGoodImport5.saw
index 35c4a785f6..4e736eeb82 100644
--- a/intTests/test_saw_submodule_import/testGoodImport5.saw
+++ b/intTests/test_saw_submodule_import/testGoodImport5.saw
@@ -4,9 +4,19 @@ import "D.cry";
 
 import submodule D2::D3 as X::Y::Z;
 
-// test 1: check we can access names not hid:
+// test 1: check we can access names:
 
 print {{ X::Y::Z::d3 }};
 print {{ 0 : X::Y::Z::D3TySy }};
 
+// test 2: still access the 'default' names brought into scope by 1st import?
+print {{ D2::D3::d3 }};
+
+// test 3:
+// Various fails
+fails ( do { print {{ d3 }}; } );
+fails ( do { print {{ Y::Z::d3 }}; } );
+fails ( do { print {{ X::Y::d3 }}; } );
+
+
 print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport6.log.good b/intTests/test_saw_submodule_import/testGoodImport6.log.good
new file mode 100644
index 0000000000..288c8c3383
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport6.log.good
@@ -0,0 +1,11 @@
+Loading file "testGoodImport6.saw"
+14229
+Error: Cryptol: [error] at testGoodImport6.saw:12:26--12:38
+    Type not in scope: MyD3::D3TySy
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport6.saw:12:1-12:43 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport6.saw b/intTests/test_saw_submodule_import/testGoodImport6.saw
new file mode 100644
index 0000000000..d7b648026e
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport6.saw
@@ -0,0 +1,14 @@
+// Test: Import nested submodule with 'as' and 'hiding' together
+
+import "D.cry";
+
+// Test importing deeply nested submodule with both 'as' and 'hiding'
+import submodule D2::D3 as MyD3 hiding (D3TySy);
+
+// Should work: d3 is imported
+print {{MyD3::d3}};
+
+// Should fail: D3TySy is hidden
+fails ( do { print {{0 : MyD3::D3TySy}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport8.log.good b/intTests/test_saw_submodule_import/testGoodImport8.log.good
new file mode 100644
index 0000000000..32c9f55d75
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport8.log.good
@@ -0,0 +1,5 @@
+Loading file "testGoodImport8.saw"
+12114
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport8.saw b/intTests/test_saw_submodule_import/testGoodImport8.saw
new file mode 100644
index 0000000000..417fb67436
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport8.saw
@@ -0,0 +1,19 @@
+// Test: Import submodule qualified, then import nested submodule
+//       from the qualified name
+
+import "D.cry";
+
+// Import D2 qualified as MyD2
+import submodule D2 as MyD2;
+
+// Now import the nested D3 via the qualified path
+import submodule MyD2::D3 as MyD3;
+
+// Both should work:
+print {{MyD2::d2}};
+print {{MyD3::d3}};
+
+// Test accessing via full path through MyD2
+print {{MyD2::D3::d3}};
+
+print "done";

From 329b48ac5414bef7a676a90fcd192f4860e47975 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Tue, 18 Aug 2026 19:12:05 -0700
Subject: [PATCH 14/17] test: add new group of tests, test_cryptolquotes

- tests how sawscript variables become accessible in {{-}}s
---
 intTests/test_cryptolquotes/.gitignore            |  3 +++
 intTests/test_cryptolquotes/Makefile              |  5 +++++
 intTests/test_cryptolquotes/P.cry                 |  9 +++++++++
 intTests/test_cryptolquotes/test.sh               |  1 +
 intTests/test_cryptolquotes/testQuotes1a.log.good |  8 ++++++++
 intTests/test_cryptolquotes/testQuotes1a.saw      | 11 +++++++++++
 intTests/test_cryptolquotes/testQuotes1b.log.good |  4 ++++
 intTests/test_cryptolquotes/testQuotes1b.saw      |  7 +++++++
 intTests/test_cryptolquotes/testQuotes2a.log.good |  9 +++++++++
 intTests/test_cryptolquotes/testQuotes2a.saw      | 12 ++++++++++++
 intTests/test_cryptolquotes/testQuotes2b.log.good |  4 ++++
 intTests/test_cryptolquotes/testQuotes2b.saw      |  7 +++++++
 12 files changed, 80 insertions(+)
 create mode 100644 intTests/test_cryptolquotes/.gitignore
 create mode 100644 intTests/test_cryptolquotes/Makefile
 create mode 100644 intTests/test_cryptolquotes/P.cry
 create mode 100755 intTests/test_cryptolquotes/test.sh
 create mode 100644 intTests/test_cryptolquotes/testQuotes1a.log.good
 create mode 100644 intTests/test_cryptolquotes/testQuotes1a.saw
 create mode 100644 intTests/test_cryptolquotes/testQuotes1b.log.good
 create mode 100644 intTests/test_cryptolquotes/testQuotes1b.saw
 create mode 100644 intTests/test_cryptolquotes/testQuotes2a.log.good
 create mode 100644 intTests/test_cryptolquotes/testQuotes2a.saw
 create mode 100644 intTests/test_cryptolquotes/testQuotes2b.log.good
 create mode 100644 intTests/test_cryptolquotes/testQuotes2b.saw

diff --git a/intTests/test_cryptolquotes/.gitignore b/intTests/test_cryptolquotes/.gitignore
new file mode 100644
index 0000000000..4619758def
--- /dev/null
+++ b/intTests/test_cryptolquotes/.gitignore
@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff
diff --git a/intTests/test_cryptolquotes/Makefile b/intTests/test_cryptolquotes/Makefile
new file mode 100644
index 0000000000..c9e12c62ae
--- /dev/null
+++ b/intTests/test_cryptolquotes/Makefile
@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean
diff --git a/intTests/test_cryptolquotes/P.cry b/intTests/test_cryptolquotes/P.cry
new file mode 100644
index 0000000000..e221a32fd5
--- /dev/null
+++ b/intTests/test_cryptolquotes/P.cry
@@ -0,0 +1,9 @@
+module P where
+
+p1 = "p1"
+
+submodule P2 where
+  p2 = "p2"
+
+  submodule P3 where
+    p3 = "p3"
\ No newline at end of file
diff --git a/intTests/test_cryptolquotes/test.sh b/intTests/test_cryptolquotes/test.sh
new file mode 100755
index 0000000000..5fcd79d0a6
--- /dev/null
+++ b/intTests/test_cryptolquotes/test.sh
@@ -0,0 +1 @@
+exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@"
diff --git a/intTests/test_cryptolquotes/testQuotes1a.log.good b/intTests/test_cryptolquotes/testQuotes1a.log.good
new file mode 100644
index 0000000000..498b12066e
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1a.log.good
@@ -0,0 +1,8 @@
+Loading file "testQuotes1a.saw"
+ss: p1a
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+testQuotes1a.saw:9:5-9:7: Warning: Redeclaration of p1
+testQuotes1a.saw:1:5-1:7: Warning: Previous declaration was here
+ss: p1b
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes1a.saw b/intTests/test_cryptolquotes/testQuotes1a.saw
new file mode 100644
index 0000000000..be594195c4
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1a.saw
@@ -0,0 +1,11 @@
+let p1 = "ss: p1a";
+print p1;
+print {{ p1 }};
+
+import "P.cry";
+
+print {{ p1 }};
+
+let p1 = "ss: p1b";
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_cryptolquotes/testQuotes1b.log.good b/intTests/test_cryptolquotes/testQuotes1b.log.good
new file mode 100644
index 0000000000..c43d2ba49a
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1b.log.good
@@ -0,0 +1,4 @@
+Loading file "testQuotes1b.saw"
+[112, 49]
+ss: p1b
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes1b.saw b/intTests/test_cryptolquotes/testQuotes1b.saw
new file mode 100644
index 0000000000..a65802454e
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1b.saw
@@ -0,0 +1,7 @@
+import "P.cry";
+
+print {{ p1 }};
+
+let p1 = "ss: p1b";
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_cryptolquotes/testQuotes2a.log.good b/intTests/test_cryptolquotes/testQuotes2a.log.good
new file mode 100644
index 0000000000..48415fb59c
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2a.log.good
@@ -0,0 +1,9 @@
+Loading file "testQuotes2a.saw"
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+testQuotes2a.saw:10:5-10:7: Warning: Redeclaration of p1
+testQuotes2a.saw:1:5-1:7: Warning: Previous declaration was here
+[115, 115, 58, 32, 112, 49, 98]
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes2a.saw b/intTests/test_cryptolquotes/testQuotes2a.saw
new file mode 100644
index 0000000000..5bce2aaac7
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2a.saw
@@ -0,0 +1,12 @@
+let p1 = {{ "ss: p1a" }};
+print p1;
+print {{ p1 }};
+
+import "P.cry";
+
+print p1;
+print {{ p1 }};
+
+let p1 = {{ "ss: p1b" }};
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_cryptolquotes/testQuotes2b.log.good b/intTests/test_cryptolquotes/testQuotes2b.log.good
new file mode 100644
index 0000000000..6c5e6eaa1c
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2b.log.good
@@ -0,0 +1,4 @@
+Loading file "testQuotes2b.saw"
+[112, 49]
+[115, 115, 58, 32, 112, 49, 98]
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes2b.saw b/intTests/test_cryptolquotes/testQuotes2b.saw
new file mode 100644
index 0000000000..868ea30d41
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2b.saw
@@ -0,0 +1,7 @@
+import "P.cry";
+
+print {{ p1 }};
+
+let p1 = {{ "ss: p1b" }};
+print p1;
+print {{ p1 }};

From 74ef884aeb69d2ea71073925446388e6002dea91 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Tue, 18 Aug 2026 21:27:26 -0700
Subject: [PATCH 15/17] test: new test.

---
 .../testGoodImport11.log.good                 |  9 +++++++
 .../testGoodImport11.saw                      | 27 +++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport11.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport11.saw

diff --git a/intTests/test_saw_submodule_import/testGoodImport11.log.good b/intTests/test_saw_submodule_import/testGoodImport11.log.good
new file mode 100644
index 0000000000..2138969663
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport11.log.good
@@ -0,0 +1,9 @@
+Loading file "testGoodImport11.saw"
+12114
+("MYSTRING", 5)
+12114
+testGoodImport11.saw:23:5-23:7: Warning: Redeclaration of d2
+testGoodImport11.saw:13:5-13:7: Warning: Previous declaration was here
+12115
+12115
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport11.saw b/intTests/test_saw_submodule_import/testGoodImport11.saw
new file mode 100644
index 0000000000..6e1ff7b2d9
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport11.saw
@@ -0,0 +1,27 @@
+// Test: Shadowing - import submodule that shadows top-level names
+
+import "D.cry";
+
+// Import D2 unqualified (brings d2 into scope)
+import submodule D2;
+
+// print D2::d2:
+print {{d2}};         // we get the value in D::D2::d2
+
+
+// Define sawscript local variable that does not shadow (no Cryptol type for)
+let d2 = ("MYSTRING",5);
+print d2;
+
+// Original d2 is shadowed inside {{-}}'s as ...
+print {{d2}};
+  // still, we get the value in D::D2::d2
+  // because the type of d2 is not one of the
+  // 'special' "use inside {{-}}" types.
+
+// Define sawscript local variable that does shadow:
+let d2 = {{d2 + 1}};
+print d2;        //
+print {{d2}};   // this and ^, both show 12115 == D::D2::D1 + 1
+
+print "done";

From 0f28884ccc6377cb94024b2f2b36f18ad85899e0 Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Tue, 18 Aug 2026 22:06:20 -0700
Subject: [PATCH 16/17] test: more tests

---
 .../testGoodImport12.log.good                 |  8 +++++++
 .../testGoodImport12.saw                      | 21 +++++++++++++++++++
 .../testGoodImport13.log.good                 | 18 ++++++++++++++++
 .../testGoodImport13.saw                      | 12 +++++++++++
 .../testGoodImport14.log.good                 |  6 ++++++
 .../testGoodImport14.saw                      | 17 +++++++++++++++
 .../testGoodImport14b.log.good                |  7 +++++++
 .../testGoodImport14b.saw                     | 19 +++++++++++++++++
 8 files changed, 108 insertions(+)
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport12.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport12.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport13.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport13.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport14.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport14.saw
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport14b.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport14b.saw

diff --git a/intTests/test_saw_submodule_import/testGoodImport12.log.good b/intTests/test_saw_submodule_import/testGoodImport12.log.good
new file mode 100644
index 0000000000..665c2c4583
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport12.log.good
@@ -0,0 +1,8 @@
+Loading file "testGoodImport12.saw"
+12114
+12114
+12114
+14229
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport12.saw b/intTests/test_saw_submodule_import/testGoodImport12.saw
new file mode 100644
index 0000000000..aeb964b4cb
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport12.saw
@@ -0,0 +1,21 @@
+// Test: Import same submodule with multiple different qualifications
+
+import "D.cry";
+
+// Import D2 unqualified
+import submodule D2;
+
+// Also import D2 with qualification
+import submodule D2 as D2_Alias;
+
+// Both should work:
+print {{d2}};           // from unqualified import
+print {{D2::d2}};       // original qualified path
+print {{D2_Alias::d2}}; // from aliased import
+
+// Nested submodule should work through all paths:
+print {{D3::d3}};
+print {{D2::D3::d3}};
+print {{D2_Alias::D3::d3}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport13.log.good b/intTests/test_saw_submodule_import/testGoodImport13.log.good
new file mode 100644
index 0000000000..003939bb5f
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport13.log.good
@@ -0,0 +1,18 @@
+Loading file "testGoodImport13.saw"
+Error: Cryptol: [error] at testGoodImport13.saw:9:22--9:24
+    Value not in scope: d2
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport13.saw:9:1-9:29 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport13.saw:10:22--10:28
+    Value not in scope: D3::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport13.saw:10:1-10:33 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport13.saw b/intTests/test_saw_submodule_import/testGoodImport13.saw
new file mode 100644
index 0000000000..26e5bf2c5e
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport13.saw
@@ -0,0 +1,12 @@
+// Test: Import with parenthesized empty list (different from no parens)
+
+import "D.cry";
+
+// Empty list means import nothing
+import submodule D2 ();
+
+// Should fail - nothing was imported
+fails ( do { print {{d2}}; } );
+fails ( do { print {{D3::d3}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport14.log.good b/intTests/test_saw_submodule_import/testGoodImport14.log.good
new file mode 100644
index 0000000000..22a1477006
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14.log.good
@@ -0,0 +1,6 @@
+Loading file "testGoodImport14.saw"
+14229
+12114
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport14.saw b/intTests/test_saw_submodule_import/testGoodImport14.saw
new file mode 100644
index 0000000000..7298d2b2dd
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14.saw
@@ -0,0 +1,17 @@
+// Test: Import nested submodule, then separately import its parent
+
+import "D.cry";
+
+// First import the nested D3
+import submodule D2::D3 as MyD3;
+print {{MyD3::d3}};
+
+// Now import its parent D2
+import submodule D2;
+print {{d2}};
+
+// Both paths to D3 should work:
+print {{MyD3::d3}};
+print {{D3::d3}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport14b.log.good b/intTests/test_saw_submodule_import/testGoodImport14b.log.good
new file mode 100644
index 0000000000..115a174b78
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14b.log.good
@@ -0,0 +1,7 @@
+Loading file "testGoodImport14b.saw"
+14229
+12114
+14229
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport14b.saw b/intTests/test_saw_submodule_import/testGoodImport14b.saw
new file mode 100644
index 0000000000..a90b5e5527
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14b.saw
@@ -0,0 +1,19 @@
+// Test: Import nested submodule, then separately import its parent
+//    - Differs from testGoodImport14.saw: 1st `import submodule` has no `as`
+
+import "D.cry";
+
+// First import the nested D3
+import submodule D2::D3;
+print {{d3}};
+
+// Now import its parent D2
+import submodule D2;
+print {{d2}};
+
+// All paths to D::D2::D3::d should work:
+print {{d3}};
+print {{D3::d3}};
+print {{D2::D3::d3}};
+
+print "done";

From 811847ce883864c909187a6315ea578fa4bbdbae Mon Sep 17 00:00:00 2001
From: Mark Tullsen <tullsen@galois.com>
Date: Tue, 18 Aug 2026 22:14:39 -0700
Subject: [PATCH 17/17] test: more tests, verifying failures also.

---
 .../testGoodImport15.log.good                      | 11 +++++++++++
 .../test_saw_submodule_import/testGoodImport15.saw | 14 ++++++++++++++
 .../testImportErrors4.log.good                     |  3 +++
 .../testImportErrors4.saw                          |  8 ++++++++
 .../testImportErrors5.log.good                     |  6 ++++++
 .../testImportErrors5.saw                          |  8 ++++++++
 .../testImportErrors6.log.good                     |  3 +++
 .../testImportErrors6.saw                          |  8 ++++++++
 .../testImportErrors7.log.good                     |  3 +++
 .../testImportErrors7.saw                          |  8 ++++++++
 10 files changed, 72 insertions(+)
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport15.log.good
 create mode 100644 intTests/test_saw_submodule_import/testGoodImport15.saw
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors4.log.good
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors4.saw
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors5.log.good
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors5.saw
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors6.log.good
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors6.saw
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors7.log.good
 create mode 100644 intTests/test_saw_submodule_import/testImportErrors7.saw

diff --git a/intTests/test_saw_submodule_import/testGoodImport15.log.good b/intTests/test_saw_submodule_import/testGoodImport15.log.good
new file mode 100644
index 0000000000..9488810994
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport15.log.good
@@ -0,0 +1,11 @@
+Loading file "testGoodImport15.saw"
+0
+Error: Cryptol: [error] at testGoodImport15.saw:12:22--12:24
+    Value not in scope: d2
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport15.saw:12:1-12:29 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport15.saw b/intTests/test_saw_submodule_import/testGoodImport15.saw
new file mode 100644
index 0000000000..1eb95d6399
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport15.saw
@@ -0,0 +1,14 @@
+// Test: Selective import of type synonym but not values
+
+import "D.cry";
+
+// Import only the type synonym, not the value
+import submodule D2 (D2TySy);
+
+// Should work: type is imported
+print {{0 : D2TySy}};
+
+// Should fail: value was not imported
+fails ( do { print {{d2}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors4.log.good b/intTests/test_saw_submodule_import/testImportErrors4.log.good
new file mode 100644
index 0000000000..06eb5ca2f2
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors4.log.good
@@ -0,0 +1,3 @@
+Loading file "testImportErrors4.saw"
+testImportErrors4.saw:6:24-6:26: Error: Syntax error: missing ')'
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors4.saw b/intTests/test_saw_submodule_import/testImportErrors4.saw
new file mode 100644
index 0000000000..2b4323134d
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors4.saw
@@ -0,0 +1,8 @@
+// Test: Error case - trying to import submodule with wrong qualification
+
+import "D.cry";
+
+// This should error: trying to use full qualified path in import spec list
+import submodule D2 (D2::d2);
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors5.log.good b/intTests/test_saw_submodule_import/testImportErrors5.log.good
new file mode 100644
index 0000000000..d917f0e154
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors5.log.good
@@ -0,0 +1,6 @@
+Loading file "testImportErrors5.saw"
+Stack trace:
+   (builtin) (at top level)
+submodule `D2::D4` is not in scope or ambiguous
+
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors5.saw b/intTests/test_saw_submodule_import/testImportErrors5.saw
new file mode 100644
index 0000000000..c564752113
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors5.saw
@@ -0,0 +1,8 @@
+// Test: Error case - importing nonexistent submodule
+
+import "D.cry";
+
+// D2 exists, but D2::D4 does not
+import submodule D2::D4;
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors6.log.good b/intTests/test_saw_submodule_import/testImportErrors6.log.good
new file mode 100644
index 0000000000..f22e8da740
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors6.log.good
@@ -0,0 +1,3 @@
+Loading file "testImportErrors6.saw"
+testImportErrors6.saw:6:27-6:29: Error: Syntax error: missing name
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors6.saw b/intTests/test_saw_submodule_import/testImportErrors6.saw
new file mode 100644
index 0000000000..9eee5691f4
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors6.saw
@@ -0,0 +1,8 @@
+// Test: Error case - trying to import with 'as' using invalid path syntax
+
+import "D.cry";
+
+// Invalid: empty component in path
+import submodule D2 as A::::B;
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors7.log.good b/intTests/test_saw_submodule_import/testImportErrors7.log.good
new file mode 100644
index 0000000000..bccd61f948
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors7.log.good
@@ -0,0 +1,3 @@
+Loading file "testImportErrors7.saw"
+testImportErrors7.saw:6:26-6:32: Error: Syntax error: missing ';'
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors7.saw b/intTests/test_saw_submodule_import/testImportErrors7.saw
new file mode 100644
index 0000000000..f01aa5e777
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors7.saw
@@ -0,0 +1,8 @@
+// Test: Error case - hiding and importing list together (should conflict)
+
+import "D.cry";
+
+// This should be an error: can't have both hiding and import list
+import submodule D2 (d2) hiding (D2TySy);
+
+print "done";