From 0af7c4e3cfae6c1cd7cdcabcfb1e1f11144d7bf4 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Mon, 15 Sep 2025 22:27:02 -0700 Subject: [PATCH 01/26] refactor: new function loadAndTranslateModule, extracted from importModule function. --- .../src/CryptolSAWCore/CryptolEnv.hs | 99 ++++++++++--------- 1 file changed, 55 insertions(+), 44 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 09e113431..a597d8196 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -625,6 +625,56 @@ extractDefFromCryptolModule (CryptolModule _ tm) name = -------------------------------------------------------------------------------- +loadAndTranslateModule :: + (?fileReader :: FilePath -> IO ByteString) => + SharedContext {- ^ Shared context for creating terms -} -> + CryptolEnv {- ^ Extend this environment -} -> + Either FilePath P.ModName {- ^ Where to find the module -} -> + IO (P.Located P.ModName, CryptolEnv) +loadAndTranslateModule sc env src = + do let modEnv = eModuleEnv env + (mtop, modEnv') <- liftModuleM modEnv $ + case src of + Left path -> MB.loadModuleByPath True path + Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn) + m <- case mtop of + T.TCTopModule mod' -> pure mod' + T.TCTopSignature {} -> + fail "Expected a module but found an interface." + + checkNotParameterized m + + -- Regenerate SharedTerm environment: + let oldModNames = map ME.lmName + $ ME.lmLoadedModules + $ ME.meLoadedModules modEnv + isNew m' = T.mName m' `notElem` oldModNames + newModules = filter isNew + $ map ME.lmModule + $ ME.lmLoadedModules + $ ME.meLoadedModules modEnv' + newDeclGroups = concatMap T.mDecls newModules + newNominal = Map.difference (ME.loadedNominalTypes modEnv') + (ME.loadedNominalTypes modEnv) + + newTermEnv <- + do oldCryEnv <- mkCryEnv env + cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv + newCryEnv <- C.importTopLevelDeclGroups + sc C.defaultPrimitiveOptions cEnv newDeclGroups + return (C.envE newCryEnv) + + let -- XXX: it would be better to have the real position, but it + -- seems to have been thrown away on the Cryptol side. + locate x = P.Located P.emptyRange x + + return ( locate $ T.mName m + , env{ eModuleEnv = modEnv' + , eTermEnv = newTermEnv + , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) + } + ) + -- | @'importModule' sc env src as vis imps@ - extend the Cryptol -- environment with a module. Closely mirrors the sawscript command "import". -- @@ -642,56 +692,17 @@ importModule :: ImportVisibility {- ^ What visibility to give symbols from this module -} -> Maybe P.ImportSpec {- ^ What to import -} -> IO CryptolEnv -importModule sc env src as vis imps = do - let modEnv = eModuleEnv env - (mtop, modEnv') <- liftModuleM modEnv $ - case src of - Left path -> MB.loadModuleByPath True path - Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn) - m <- case mtop of - T.TCTopModule mod' -> pure mod' - T.TCTopSignature {} -> - fail "Expected a module but found an interface." - - checkNotParameterized m - - -- Regenerate SharedTerm environment: - let oldModNames = map ME.lmName - $ ME.lmLoadedModules - $ ME.meLoadedModules modEnv - isNew m' = T.mName m' `notElem` oldModNames - newModules = filter isNew - $ map ME.lmModule - $ ME.lmLoadedModules - $ ME.meLoadedModules modEnv' - newDeclGroups = concatMap T.mDecls newModules - newNominal = Map.difference (ME.loadedNominalTypes modEnv') - (ME.loadedNominalTypes modEnv) - - newTermEnv <- - do oldCryEnv <- mkCryEnv env - cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv - newCryEnv <- C.importTopLevelDeclGroups - sc C.defaultPrimitiveOptions cEnv newDeclGroups - return (C.envE newCryEnv) - - let newImport = (vis, P.Import { T.iModule= locate $ T.mName m +importModule sc env src as vis imps = + do + (modName, env') <- loadAndTranslateModule sc env src + let newImport = (vis, P.Import { T.iModule= modName , T.iAs = as , T.iSpec = imps , T.iInst = Nothing , T.iDoc = Nothing } ) - -- XXX: it would be better to have the real position, but it - -- seems to have been thrown away on the Cryptol side. - locate x = P.Located P.emptyRange x - - return $ - env{ eModuleEnv = modEnv' - , eTermEnv = newTermEnv - , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) - , eImports = newImport : eImports env - } + return $ env'{ eImports = newImport : eImports env } bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv) bindIdent ident env = (name, env') From 5a4d5685a8e26d3d164aa72dc79e8e89c73c6e3f Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 22:29:13 -0700 Subject: [PATCH 02/26] comments and whitespace --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index a597d8196..532f7f82e 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -462,10 +462,6 @@ loadCryptolModule sc env path = do checkNotParameterized m - -- NOTE: unclear what's happening here! - -- - FIXME: understand and doc. - -- - `m` not used (directly) but translating the modEnv' - -- - this behavior is not in `importModule` let ifaceDecls = getAllIfaceDecls modEnv' (types, modEnv'') <- liftModuleM modEnv' $ do @@ -546,13 +542,13 @@ mkCryptolModule m types newTermEnv = (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) (T.mTySyns m) ) - -- FIXME: TODO: ensure type synonym in submodule is included. + -- FIXME: TODO: ensure type synonyms in submodule are included. -- create the map of symbols: ( Map.filterWithKey (\k _ -> Set.member k names) $ Map.intersectionWith (\t x -> TypedTerm (TypedTermSchema t) x) - types -- NOTE: only use of this variable. + types newTermEnv ) @@ -670,9 +666,9 @@ loadAndTranslateModule sc env src = return ( locate $ T.mName m , env{ eModuleEnv = modEnv' - , eTermEnv = newTermEnv - , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) - } + , eTermEnv = newTermEnv + , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) + } ) -- | @'importModule' sc env src as vis imps@ - extend the Cryptol From 2cf28124bc1a639a077b2dbbe1ecc4f4455c5b83 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 22:31:29 -0700 Subject: [PATCH 03/26] refactor: move code for generating CryptolModule into mkCryptolModule - See comments in mkCryptolModule that justify the refactor (i.e., that modEnv' == modEnv'') --- .../src/CryptolSAWCore/CryptolEnv.hs | 62 +++++++++---------- 1 file changed, 29 insertions(+), 33 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 532f7f82e..89e15f479 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -462,22 +462,6 @@ loadCryptolModule sc env path = do checkNotParameterized m - - let ifaceDecls = getAllIfaceDecls modEnv' - (types, modEnv'') <- liftModuleM modEnv' $ do - do prims <- MB.getPrimMap - -- generate the primitive map; a monad reader - TM.inpVars `fmap` - MB.genInferInput P.emptyRange prims NoParams ifaceDecls - - -- NOTE: inpVars are the variables that are in scope. - -- FIXME: we are possibly doing unnecessary computation here (see - -- source code for MB.getPrimMap and MB.genInferInput.) - - -- FIXME: it appears (need to verify) that modEnv'' == modEnv' - -- if this true, we can simplify and move this section - -- into `mkCryptolModule`. - -- Regenerate SharedTerm environment: let oldModNames = map ME.lmName $ ME.lmLoadedModules @@ -486,7 +470,7 @@ loadCryptolModule sc env path = do newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules - $ ME.meLoadedModules modEnv'' + $ ME.meLoadedModules modEnv' newDeclGroups = concatMap T.mDecls newModules newNominal = Map.difference (ME.loadedNominalTypes modEnv') (ME.loadedNominalTypes modEnv) @@ -498,18 +482,15 @@ loadCryptolModule sc env path = do sc C.defaultPrimitiveOptions cEnv newDeclGroups return (C.envE newCryEnv) - cryptolModule <- mkCryptolModule m types newTermEnv - -- NOTE: Bringing the module-handle into {{-}} scope is not handled -- here; it is done rather in `bindCryptolModule`, ONLY if the -- user binds the `cryptolModule` returned here at the saw -- command line. - return ( cryptolModule - , env { eModuleEnv = modEnv'' - , eTermEnv = newTermEnv - , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) - } + let env' = env { eModuleEnv = modEnv' + , eTermEnv = newTermEnv + , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) + } -- NOTE here the difference between this function and -- `importModule`: -- 1. the `eImports` field is not updated, as @@ -517,7 +498,9 @@ loadCryptolModule sc env path = do -- brought into scope inside {{ }} constructs. -- 2. modEnv'' vs modEnv' (which may not be different, see -- notes above). - ) + + cryptolModule <- mkCryptolModule m env' + return (cryptolModule, env') -- | mkCryptolModule -- @@ -525,15 +508,28 @@ loadCryptolModule sc env path = do -- - This incorrectly excludes both submodules and their contents from -- the NamingEnvs in `CryptolModule` --- - Regarding the CLI API: the `CryptolModule` type is exposed to --- the SAWScript CLI, is this necessary? - -mkCryptolModule :: T.Module - -> Map MN.Name T.Schema - -> Map MN.Name Term - -> IO CryptolModule -mkCryptolModule m types newTermEnv = +mkCryptolModule :: + (?fileReader :: FilePath -> IO ByteString) => + T.Module -> CryptolEnv -> IO CryptolModule +mkCryptolModule m env = do + let newTermEnv = eTermEnv env + modEnv = eModuleEnv env + ifaceDecls = getAllIfaceDecls modEnv + (types, _modEnv) <- liftModuleM modEnv $ do + -- NOTE: _modEnv == modEnv + -- - as we elaborate below, the monadic actions are all 'readers' + do prims <- MB.getPrimMap + -- generate the primitive map; a monad reader + TM.inpVars `fmap` + MB.genInferInput P.emptyRange prims NoParams ifaceDecls + -- NOTE: inpVars are the variables that are in scope. + -- FIXME: + -- - Why are we calling mB.genInferInput then projecting out + -- `inpVars`? + -- - If we had inlined, it appears that this is functional code. + -- - (Maybe because of information hiding?) + let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name return $ CryptolModule From 6949e218416166668a0b3a70d42473ed30af67ec Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 22:48:47 -0700 Subject: [PATCH 04/26] refactors --- .../src/CryptolSAWCore/CryptolEnv.hs | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 89e15f479..22d494698 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -622,7 +622,7 @@ loadAndTranslateModule :: SharedContext {- ^ Shared context for creating terms -} -> CryptolEnv {- ^ Extend this environment -} -> Either FilePath P.ModName {- ^ Where to find the module -} -> - IO (P.Located P.ModName, CryptolEnv) + IO (T.Module, CryptolEnv) loadAndTranslateModule sc env src = do let modEnv = eModuleEnv env (mtop, modEnv') <- liftModuleM modEnv $ @@ -656,11 +656,7 @@ loadAndTranslateModule sc env src = sc C.defaultPrimitiveOptions cEnv newDeclGroups return (C.envE newCryEnv) - let -- XXX: it would be better to have the real position, but it - -- seems to have been thrown away on the Cryptol side. - locate x = P.Located P.emptyRange x - - return ( locate $ T.mName m + return ( m , env{ eModuleEnv = modEnv' , eTermEnv = newTermEnv , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) @@ -686,8 +682,8 @@ importModule :: IO CryptolEnv importModule sc env src as vis imps = do - (modName, env') <- loadAndTranslateModule sc env src - let newImport = (vis, P.Import { T.iModule= modName + (mod', env') <- loadAndTranslateModule sc env src + let newImport = (vis, P.Import { T.iModule= locatedUnknown (T.mName mod') , T.iAs = as , T.iSpec = imps , T.iInst = Nothing @@ -696,6 +692,12 @@ importModule sc env src as vis imps = ) return $ env'{ eImports = newImport : eImports env } +locatedUnknown :: a -> P.Located a +locatedUnknown x = P.Located P.emptyRange x + -- XXX: it would be better to have the real position, but it + -- seems to have been thrown away on the Cryptol side in the uses + -- of this function. + bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv) bindIdent ident env = (name, env') where From 04717fa9f126823d1a214e8e66ff70a732edfcf7 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 22:52:48 -0700 Subject: [PATCH 05/26] improve fail message --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 22d494698..37c051f69 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -632,7 +632,13 @@ loadAndTranslateModule sc env src = m <- case mtop of T.TCTopModule mod' -> pure mod' T.TCTopSignature {} -> - fail "Expected a module but found an interface." + fail $ + "Expected a module, but " + ++ (case src of + Left path -> show path + Right mn -> show mn + ) + ++ " is an interface." checkNotParameterized m From 910f9ff0e55d8b03e50d4f45319da74e6a549f83 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 23:03:04 -0700 Subject: [PATCH 06/26] comments. --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 37c051f69..52f450b08 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -443,7 +443,7 @@ checkNotParameterized m = -- This is used to implement the "cryptol_load" primitive in which a -- handle to the module is returned and can be bound to a SAWScript -- variable. - +-- loadCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => SharedContext -> @@ -484,7 +484,7 @@ loadCryptolModule sc env path = do -- NOTE: Bringing the module-handle into {{-}} scope is not handled -- here; it is done rather in `bindCryptolModule`, ONLY if the - -- user binds the `cryptolModule` returned here at the saw + -- user binds the `cryptolModule` returned here at the SAW -- command line. let env' = env { eModuleEnv = modEnv' @@ -528,7 +528,7 @@ mkCryptolModule m env = -- - Why are we calling mB.genInferInput then projecting out -- `inpVars`? -- - If we had inlined, it appears that this is functional code. - -- - (Maybe because of information hiding?) + -- - (Possibly because of information hiding?) let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name return $ From 50826d5a4d8601cfb52758b2257351f4c270c73f Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 23:03:55 -0700 Subject: [PATCH 07/26] refactor: fold loadAndTranslateModule --- .../src/CryptolSAWCore/CryptolEnv.hs | 53 ++----------------- 1 file changed, 4 insertions(+), 49 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 52f450b08..a1e6399f4 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -432,11 +432,6 @@ checkNotParameterized m = , "Either use a ` import, or make a module instantiation." ] --- FIXME: Code duplication, these two functions are highly similar: --- - loadCryptolModule --- - importModule --- - TODO: "common up" the common code per #2569. - -- | loadCryptolModule - load a cryptol module and return a handle to -- the `CryptolModule`. The contents of the module are not imported. -- @@ -450,56 +445,16 @@ loadCryptolModule :: CryptolEnv -> FilePath -> IO (CryptolModule, CryptolEnv) -loadCryptolModule sc env path = do - let modEnv = eModuleEnv env - (mtop, modEnv') <- liftModuleM modEnv $ - MB.loadModuleByPath True path - m <- case mtop of - T.TCTopModule mod' -> pure mod' - T.TCTopSignature {} -> - fail $ - "Expected a module, but " ++ show path ++ " is an interface." - - checkNotParameterized m - - -- Regenerate SharedTerm environment: - let oldModNames = map ME.lmName - $ ME.lmLoadedModules - $ ME.meLoadedModules modEnv - isNew m' = T.mName m' `notElem` oldModNames - newModules = filter isNew - $ map ME.lmModule - $ ME.lmLoadedModules - $ ME.meLoadedModules modEnv' - newDeclGroups = concatMap T.mDecls newModules - newNominal = Map.difference (ME.loadedNominalTypes modEnv') - (ME.loadedNominalTypes modEnv) - - newTermEnv <- - do oldCryEnv <- mkCryEnv env - cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv - newCryEnv <- C.importTopLevelDeclGroups - sc C.defaultPrimitiveOptions cEnv newDeclGroups - return (C.envE newCryEnv) +loadCryptolModule sc env path = + do + (mod', env') <- loadAndTranslateModule sc env (Left path) -- NOTE: Bringing the module-handle into {{-}} scope is not handled -- here; it is done rather in `bindCryptolModule`, ONLY if the -- user binds the `cryptolModule` returned here at the SAW -- command line. - let env' = env { eModuleEnv = modEnv' - , eTermEnv = newTermEnv - , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) - } - -- NOTE here the difference between this function and - -- `importModule`: - -- 1. the `eImports` field is not updated, as - -- this module (as a whole) is not being - -- brought into scope inside {{ }} constructs. - -- 2. modEnv'' vs modEnv' (which may not be different, see - -- notes above). - - cryptolModule <- mkCryptolModule m env' + cryptolModule <- mkCryptolModule mod' env' return (cryptolModule, env') -- | mkCryptolModule From 6693057413fa79cddeaa3298ed72986850bb7985 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 23:24:59 -0700 Subject: [PATCH 08/26] comments, refactors --- .../src/CryptolSAWCore/CryptolEnv.hs | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index a1e6399f4..3cc43653e 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -435,6 +435,11 @@ checkNotParameterized m = -- | loadCryptolModule - load a cryptol module and return a handle to -- the `CryptolModule`. The contents of the module are not imported. -- +-- NOTE: Bringing the module-handle into {{-}} scope is not handled +-- here; it is done rather in `bindCryptolModule`, ONLY if the +-- user binds the `cryptolModule` returned here at the SAW +-- command line. +-- -- This is used to implement the "cryptol_load" primitive in which a -- handle to the module is returned and can be bound to a SAWScript -- variable. @@ -448,21 +453,15 @@ loadCryptolModule :: loadCryptolModule sc env path = do (mod', env') <- loadAndTranslateModule sc env (Left path) - - -- NOTE: Bringing the module-handle into {{-}} scope is not handled - -- here; it is done rather in `bindCryptolModule`, ONLY if the - -- user binds the `cryptolModule` returned here at the SAW - -- command line. - cryptolModule <- mkCryptolModule mod' env' return (cryptolModule, env') --- | mkCryptolModule +-- | mkCryptolModule - translate a T.Module to a CryptolModule -- -- FIXME: -- - This incorrectly excludes both submodules and their contents from --- the NamingEnvs in `CryptolModule` - +-- both of the NamingEnvs in `CryptolModule` +-- mkCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => T.Module -> CryptolEnv -> IO CryptolModule @@ -653,11 +652,12 @@ importModule sc env src as vis imps = ) return $ env'{ eImports = newImport : eImports env } -locatedUnknown :: a -> P.Located a -locatedUnknown x = P.Located P.emptyRange x - -- XXX: it would be better to have the real position, but it - -- seems to have been thrown away on the Cryptol side in the uses - -- of this function. + where + locatedUnknown :: a -> P.Located a + locatedUnknown x = P.Located P.emptyRange x + -- XXX: it would be better to have the real position, but it + -- seems to have been thrown away on the Cryptol side in the uses + -- of this function. bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv) bindIdent ident env = (name, env') From 4bffbdd5740f1833701f5867dd3b1f0efbb80bda Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 17 Sep 2025 23:30:16 -0700 Subject: [PATCH 09/26] refactor: make names more consistent - s/importModule/importCryptolModule/g; --- crux-mir-comp/src/Mir/Cryptol.hs | 2 +- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 14 +++++++------- otherTests/cryptol-saw-core/CryptolVerifierTC.hs | 10 +++++----- saw-script/src/SAWScript/Interpreter.hs | 2 +- saw-server/src/SAWServer/CryptolSetup.hs | 4 ++-- 5 files changed, 16 insertions(+), 16 deletions(-) diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 51dc44ce3..1a90dfbc9 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -238,7 +238,7 @@ loadCryptolFunc col sig modulePath name = do let ?fileReader = BS.readFile ce <- liftIO (readIORef (mirCryEnv mirState)) let modName = Cry.textToModName modulePath - ce' <- liftIO $ SAW.importModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing + ce' <- liftIO $ SAW.importCryptolModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing liftIO (writeIORef (mirCryEnv mirState) ce') -- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath) -- tt <- liftIO $ SAW.extractDefFromCryptolModule m (Text.unpack name) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 3cc43653e..1ba010644 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -18,7 +18,7 @@ module CryptolSAWCore.CryptolEnv , bindCryptolModule , extractDefFromCryptolModule , combineCryptolEnv - , importModule + , importCryptolModule , bindTypedTerm , bindType , bindInteger @@ -115,7 +115,7 @@ data InputText = InputText -------------------------------------------------------------------------------- --- | 'ImportVisibility' - Should a given import (see 'importModule') +-- | 'ImportVisibility' - Should a given import (see 'importCryptolModule') -- result in all symbols being visible (as they are for focused -- modules in the Cryptol REPL) or only public symbols? Making all -- symbols visible is useful for verification and code generation. @@ -529,10 +529,10 @@ updateFFITypes m eTermEnv' eFFITypes' = -- -- FIXME: -- - submodules are not handled correctly below. --- - the code is duplicating functionality that we have with `importModule` +-- - the code is duplicating functionality that we have with `importCryptolModule` -- TODO: -- - new design in PR #2593 (addressing issue #2569) should replace --- this function so that the fundamental work is done via `importModule`. +-- this function so that the fundamental work is done via `importCryptolModule`. bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv bindCryptolModule (modName, CryptolModule sm tm) env = @@ -623,7 +623,7 @@ loadAndTranslateModule sc env src = } ) --- | @'importModule' sc env src as vis imps@ - extend the Cryptol +-- | @'importCryptolModule' sc env src as vis imps@ - extend the Cryptol -- environment with a module. Closely mirrors the sawscript command "import". -- -- NOTE: @@ -631,7 +631,7 @@ loadAndTranslateModule sc env src = -- - 'vis' we can import public definitions or *all* (i.e., internal -- and public) definitions. -importModule :: +importCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => SharedContext {- ^ Shared context for creating terms -} -> CryptolEnv {- ^ Extend this environment -} -> @@ -640,7 +640,7 @@ importModule :: ImportVisibility {- ^ What visibility to give symbols from this module -} -> Maybe P.ImportSpec {- ^ What to import -} -> IO CryptolEnv -importModule sc env src as vis imps = +importCryptolModule sc env src as vis imps = do (mod', env') <- loadAndTranslateModule sc env src let newImport = (vis, P.Import { T.iModule= locatedUnknown (T.mName mod') diff --git a/otherTests/cryptol-saw-core/CryptolVerifierTC.hs b/otherTests/cryptol-saw-core/CryptolVerifierTC.hs index 15130f3fd..0c9a1f0c5 100644 --- a/otherTests/cryptol-saw-core/CryptolVerifierTC.hs +++ b/otherTests/cryptol-saw-core/CryptolVerifierTC.hs @@ -27,15 +27,15 @@ main = let ?fileReader = BS.readFile cenv0 <- CEnv.initCryptolEnv sc putStrLn "Translated Cryptol.cry!" - cenv1 <- CEnv.importModule sc cenv0 (Right N.floatName) Nothing CEnv.OnlyPublic Nothing + cenv1 <- CEnv.importCryptolModule sc cenv0 (Right N.floatName) Nothing CEnv.OnlyPublic Nothing putStrLn "Translated Float.cry!" - cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing CEnv.OnlyPublic Nothing + cenv2 <- CEnv.importCryptolModule sc cenv1 (Right N.arrayName) Nothing CEnv.OnlyPublic Nothing putStrLn "Translated Array.cry!" - cenv3 <- CEnv.importModule sc cenv2 (Right N.suiteBName) Nothing CEnv.OnlyPublic Nothing + cenv3 <- CEnv.importCryptolModule sc cenv2 (Right N.suiteBName) Nothing CEnv.OnlyPublic Nothing putStrLn "Translated SuiteB.cry!" - cenv4 <- CEnv.importModule sc cenv3 (Right N.primeECName) Nothing CEnv.OnlyPublic Nothing + cenv4 <- CEnv.importCryptolModule sc cenv3 (Right N.primeECName) Nothing CEnv.OnlyPublic Nothing putStrLn "Translated PrimeEC.cry!" - cenv5 <- CEnv.importModule sc cenv4 (Right N.preludeReferenceName) Nothing CEnv.OnlyPublic Nothing + cenv5 <- CEnv.importCryptolModule sc cenv4 (Right N.preludeReferenceName) Nothing CEnv.OnlyPublic Nothing putStrLn "Translated Reference.cry!" cenv6 <- CEnv.parseDecls sc cenv5 (CEnv.InputText superclassContents "superclass.cry" 1 1) putStrLn "Translated superclass.cry!" diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 84d298e71..9d9b52dcd 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -915,7 +915,7 @@ interpretTopStmt printBinds stmt = do let mLoc = iModule imp qual = iAs imp spec = iSpec imp - cenv' <- io $ CEnv.importModule sc (rwCryptol rw) mLoc qual CEnv.PublicAndPrivate spec + cenv' <- io $ CEnv.importCryptolModule sc (rwCryptol rw) mLoc qual CEnv.PublicAndPrivate spec putTopLevelRW $ rw { rwCryptol = cenv' } --showCryptolEnv diff --git a/saw-server/src/SAWServer/CryptolSetup.hs b/saw-server/src/SAWServer/CryptolSetup.hs index 8f5840717..4340489ee 100644 --- a/saw-server/src/SAWServer/CryptolSetup.hs +++ b/saw-server/src/SAWServer/CryptolSetup.hs @@ -41,7 +41,7 @@ cryptolLoadModule (CryptolLoadModuleParams modName) = let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader let ?fileReader = fileReader - cenv' <- liftIO $ try $ CEnv.importModule sc cenv (Right modName) qual CEnv.PublicAndPrivate importSpec + cenv' <- liftIO $ try $ CEnv.importCryptolModule sc cenv (Right modName) qual CEnv.PublicAndPrivate importSpec case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> @@ -76,7 +76,7 @@ cryptolLoadFile (CryptolLoadFileParams fileName) = let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader let ?fileReader = fileReader - cenv' <- liftIO $ try $ CEnv.importModule sc cenv (Left fileName) qual CEnv.PublicAndPrivate importSpec + cenv' <- liftIO $ try $ CEnv.importCryptolModule sc cenv (Left fileName) qual CEnv.PublicAndPrivate importSpec case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> From a45b92bf858680f8581df0bbd2ecae2aec6ce91c Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Fri, 19 Sep 2025 14:13:41 -0700 Subject: [PATCH 10/26] improve comments --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 1ba010644..f534d96cd 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -432,6 +432,7 @@ checkNotParameterized m = , "Either use a ` import, or make a module instantiation." ] + -- | loadCryptolModule - load a cryptol module and return a handle to -- the `CryptolModule`. The contents of the module are not imported. -- @@ -456,6 +457,7 @@ loadCryptolModule sc env path = cryptolModule <- mkCryptolModule mod' env' return (cryptolModule, env') + -- | mkCryptolModule - translate a T.Module to a CryptolModule -- -- FIXME: @@ -524,12 +526,18 @@ updateFFITypes m eTermEnv' eFFITypes' = "Cannot find foreign function in term environment: " <> Text.pack (show nm) ] --- | bindCryptolModule - ad hoc function called when `D <-cryptol_load` is seen --- on the command line. +-- | bindCryptolModule - ad hoc function/hook that allows for extending +-- the Cryptol env with the names in a CryptolModule. +-- +-- Three command line variants get us here: +-- > D <- cryptol_load "PATH" +-- > x <- return (cryptol_prims ()) +-- > let x = cryptol_prims () -- -- FIXME: -- - submodules are not handled correctly below. --- - the code is duplicating functionality that we have with `importCryptolModule` +-- - the code is somewhat duplicating functionality that we +-- already have with `importCryptolModule` -- TODO: -- - new design in PR #2593 (addressing issue #2569) should replace -- this function so that the fundamental work is done via `importCryptolModule`. From 7c3d477ea10722f7b878b078b487c6e0ed16389d Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Fri, 19 Sep 2025 16:48:22 -0700 Subject: [PATCH 11/26] comments, refactors (re-ordering, folding locatedUnknown, new mkImport) --- .../src/CryptolSAWCore/CryptolEnv.hs | 144 ++++++++++-------- 1 file changed, 82 insertions(+), 62 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index f534d96cd..7197269f1 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -103,6 +103,9 @@ import CryptolSAWCore.TypedTerm import Cryptol.ModuleSystem.Env (ModContextParams(NoParams)) -- import SAWCentral.AST (Located(getVal, locatedPos), Import(..)) + +---- Key Types ----------------------------------------------------------------- + -- | Parse input, together with information about where it came from. data InputText = InputText { inpText :: Text -- ^ Parse this @@ -241,15 +244,16 @@ initCryptolEnv sc = do termEnv <- genTermEnv sc modEnv3 cryEnv0 -- The module names in P.Import are now Located, so give them an empty position. - let preludeName' = P.Located P.emptyRange preludeName - preludeReferenceName' = P.Located P.emptyRange preludeReferenceName - arrayName' = P.Located P.emptyRange arrayName + let preludeName' = locatedUnknown preludeName + preludeReferenceName' = locatedUnknown preludeReferenceName + arrayName' = locatedUnknown arrayName return CryptolEnv - { eImports = [ (OnlyPublic, P.Import preludeName' Nothing Nothing Nothing Nothing) - , (OnlyPublic, P.Import preludeReferenceName' (Just preludeReferenceName) Nothing Nothing Nothing) - , (OnlyPublic, P.Import arrayName' Nothing Nothing Nothing Nothing) - ] + { eImports = + [ mkImport OnlyPublic preludeName' Nothing Nothing + , mkImport OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing + , mkImport OnlyPublic arrayName' Nothing Nothing + ] , eModuleEnv = modEnv3 , eExtraNames = mempty , eExtraTypes = Map.empty @@ -260,9 +264,10 @@ initCryptolEnv sc = do , eFFITypes = Map.empty } + -- | Translate all declarations in all loaded modules to SAWCore terms -- NOTE: used only for initialization code. - +-- genTermEnv :: SharedContext -> ME.ModuleEnv -> C.Env -> IO (Map T.Name Term) genTermEnv sc modEnv cryEnv0 = do let declGroups = concatMap T.mDecls @@ -304,8 +309,8 @@ ioParseResult res = case res of -- NamingEnv and Related ------------------------------------------------------- --- | @'getNamingEnv' env@ - get the full 'MR.NamingEnv' based on all the 'eImports' - +-- | @'getNamingEnv' env@ - get the full 'MR.NamingEnv' based on all +-- the 'eImports' getNamingEnv :: CryptolEnv -> MR.NamingEnv getNamingEnv env = eExtraNames env @@ -362,6 +367,7 @@ runInferOutput out = do MM.typeCheckWarnings nm warns MM.typeCheckingFailed nm errs + -- Translate ------------------------------------------------------------------- mkCryEnv :: @@ -414,8 +420,7 @@ translateDeclGroups sc env dgs = , eTermEnv = C.envE cryEnv' } --------------------------------------------------------------------------------- - +---- Misc Exports -------------------------------------------------------------- combineCryptolEnv :: CryptolEnv -> CryptolEnv -> IO CryptolEnv combineCryptolEnv chkEnv newEnv = @@ -425,13 +430,7 @@ combineCryptolEnv chkEnv newEnv = return chkEnv{ eModuleEnv = menv' } -checkNotParameterized :: T.Module -> IO () -checkNotParameterized m = - when (T.isParametrizedModule m) $ - fail $ unlines [ "Cannot load parameterized modules directly." - , "Either use a ` import, or make a module instantiation." - ] - +---- CryptolModule/ExtCryptolModule functions: --------------------------------- -- | loadCryptolModule - load a cryptol module and return a handle to -- the `CryptolModule`. The contents of the module are not imported. @@ -504,28 +503,6 @@ mkCryptolModule m env = newTermEnv ) -updateFFITypes :: T.Module -> Map MN.Name Term -> Map NameInfo T.FFI -> Map NameInfo T.FFI -updateFFITypes m eTermEnv' eFFITypes' = - foldr (\(nm, ty) -> Map.insert (getNameInfo nm) ty) - eFFITypes' - (T.findForeignDecls m) - where - getNameInfo nm = - case Map.lookup nm eTermEnv' of - Just tm -> - case asConstant tm of - Just n -> nameInfo n - Nothing -> - panic "updateFFITypes" [ - "SAWCore term of Cryptol name is not Constant", - "Name: " <> Text.pack (show nm), - "Term: " <> Text.pack (showTerm tm) - ] - Nothing -> - panic "updateFFITypes" [ - "Cannot find foreign function in term environment: " <> Text.pack (show nm) - ] - -- | bindCryptolModule - ad hoc function/hook that allows for extending -- the Cryptol env with the names in a CryptolModule. -- @@ -577,7 +554,7 @@ extractDefFromCryptolModule (CryptolModule _ tm) name = -- FIXME: this is ad hoc, somehow invoke parse for name, or the like? --------------------------------------------------------------------------------- +---- Core functions for loading and Translating Modules ------------------------ loadAndTranslateModule :: (?fileReader :: FilePath -> IO ByteString) => @@ -631,12 +608,44 @@ loadAndTranslateModule sc env src = } ) +checkNotParameterized :: T.Module -> IO () +checkNotParameterized m = + when (T.isParametrizedModule m) $ + fail $ unlines [ "Cannot load parameterized modules directly." + , "Either use a ` import, or make a module instantiation." + ] + +updateFFITypes :: T.Module -> Map MN.Name Term -> Map NameInfo T.FFI -> Map NameInfo T.FFI +updateFFITypes m eTermEnv' eFFITypes' = + foldr (\(nm, ty) -> Map.insert (getNameInfo nm) ty) + eFFITypes' + (T.findForeignDecls m) + where + getNameInfo nm = + case Map.lookup nm eTermEnv' of + Just tm -> + case asConstant tm of + Just n -> nameInfo n + Nothing -> + panic "updateFFITypes" [ + "SAWCore term of Cryptol name is not Constant", + "Name: " <> Text.pack (show nm), + "Term: " <> Text.pack (showTerm tm) + ] + Nothing -> + panic "updateFFITypes" [ + "Cannot find foreign function in term environment: " <> Text.pack (show nm) + ] + + +---- import -------------------------------------------------------------------- + -- | @'importCryptolModule' sc env src as vis imps@ - extend the Cryptol -- environment with a module. Closely mirrors the sawscript command "import". -- -- NOTE: --- - the module can be qualified or not (per 'as' argument). per --- - 'vis' we can import public definitions or *all* (i.e., internal +-- - the module can be qualified or not (per 'as' argument). +-- - per 'vis' we can import public definitions or *all* (i.e., internal -- and public) definitions. importCryptolModule :: @@ -651,21 +660,25 @@ importCryptolModule :: importCryptolModule sc env src as vis imps = do (mod', env') <- loadAndTranslateModule sc env src - let newImport = (vis, P.Import { T.iModule= locatedUnknown (T.mName mod') - , T.iAs = as - , T.iSpec = imps - , T.iInst = Nothing - , T.iDoc = Nothing - } - ) - return $ env'{ eImports = newImport : eImports env } - - where - locatedUnknown :: a -> P.Located a - locatedUnknown x = P.Located P.emptyRange x - -- XXX: it would be better to have the real position, but it - -- seems to have been thrown away on the Cryptol side in the uses - -- of this function. + return $ env'{ eImports = mkImport vis (locatedUnknown (T.mName mod')) as imps + : eImports env + } + +mkImport :: ImportVisibility + -> P.Located C.ModName + -> Maybe C.ModName + -> Maybe T.ImportSpec + -> (ImportVisibility, T.Import) +mkImport vis nm as imps = (vis, P.Import { T.iModule= nm + , T.iAs = as + , T.iSpec = imps + , T.iInst = Nothing + , T.iDoc = Nothing + } + ) + + +---- Binding ------------------------------------------------------------------- bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv) bindIdent ident env = (name, env') @@ -717,6 +730,7 @@ bindInteger (ident, n) env = (name, env') = bindIdent ident env tysyn = T.TySyn name [] [] (T.tNum n) Nothing + -------------------------------------------------------------------------------- meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig @@ -754,7 +768,6 @@ resolveIdentifier env nm = Left _ -> pure Nothing Right (x,_) -> pure (Just x) - parseTypedTerm :: (HasCallStack, ?fileReader :: FilePath -> IO ByteString) => SharedContext -> CryptolEnv -> InputText -> IO TypedTerm @@ -821,7 +834,7 @@ parseDecls sc env input = do (_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls)) -- Create a Module to contain the declarations - let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName + let rmodule = P.Module { P.mName = locatedUnknown interactiveName , P.mDef = P.NormalModule rdecls , P.mInScope = mempty , P.mDocTop = Nothing @@ -911,7 +924,14 @@ typeNoUser t = schemaNoUser :: T.Schema -> T.Schema schemaNoUser (T.Forall params props ty) = T.Forall params props (typeNoUser ty) ------------------------------------------------------------- + +---- Local Utility Functions --------------------------------------------------- + +locatedUnknown :: a -> P.Located a +locatedUnknown x = P.Located P.emptyRange x + -- XXX: it would be better to have the real position, but it + -- seems to have been thrown away on the Cryptol side in the uses + -- of this function. liftModuleM :: (?fileReader :: FilePath -> IO ByteString) => From 86878b247855a96881a7478c81d3dab9c433dbe5 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Fri, 19 Sep 2025 20:00:08 -0700 Subject: [PATCH 12/26] refactor (with dead code, thus no compile), in prep for ... --- .../src/CryptolSAWCore/CryptolEnv.hs | 72 ++++++++++++++----- 1 file changed, 55 insertions(+), 17 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 7197269f1..e6f7381a8 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -115,8 +115,16 @@ data InputText = InputText } +-- | ExtCryptolModule - Extended CryptolModule; we keep track of +-- whether this module came directly from a constructed +-- `CryptolModule` or whether it came from parsing a Cryptol module +-- in filesystem (in which case it is loaded). +data ExtCryptolModule = + ECM_LoadedModule (P.Located C.ModName) -- source is load + | ECM_CryptolModule CryptolModule -- source in cryptol_prims + -- deriving (Show) + -- FIXME: TODO: more instances --------------------------------------------------------------------------------- -- | 'ImportVisibility' - Should a given import (see 'importCryptolModule') -- result in all symbols being visible (as they are for focused @@ -432,18 +440,39 @@ combineCryptolEnv chkEnv newEnv = ---- CryptolModule/ExtCryptolModule functions: --------------------------------- --- | loadCryptolModule - load a cryptol module and return a handle to --- the `CryptolModule`. The contents of the module are not imported. --- --- NOTE: Bringing the module-handle into {{-}} scope is not handled --- here; it is done rather in `bindCryptolModule`, ONLY if the --- user binds the `cryptolModule` returned here at the SAW --- command line. +-- | loadCryptolModule - load a cryptol module and returns the +-- `ExtCryptolModule`. The contents of the module are not directly +-- imported into the environment. -- -- This is used to implement the "cryptol_load" primitive in which a -- handle to the module is returned and can be bound to a SAWScript -- variable. -- +-- NOTE: Bringing the module into {{-}} scope is not handled +-- here; it is done rather in `bindExtCryptolModule`, ONLY if the +-- user binds the `cryptolModule` returned here at the SAW +-- command line. +loadExtCryptolModule :: + (?fileReader :: FilePath -> IO ByteString) => + SharedContext -> + CryptolEnv -> + FilePath -> + IO (ExtCryptolModule, CryptolEnv) +loadExtCryptolModule sc env path = + do + (mod', env') <- loadAndTranslateModule sc env (Left path) + return (ECM_LoadedModule (locatedUnknown (T.mName mod')), env') + + +-- | loadCryptolModule +-- +-- NOTE: +-- - the path to this function from the command line is only via +-- the experimental "write_coq_cryptol_module" command. +-- +-- FIXME: This incorrectly (in MkCryptolModule) excludes both +-- submodules and their contents from the NamingEnvs in +-- `CryptolModule` loadCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => SharedContext -> @@ -453,16 +482,10 @@ loadCryptolModule :: loadCryptolModule sc env path = do (mod', env') <- loadAndTranslateModule sc env (Left path) - cryptolModule <- mkCryptolModule mod' env' - return (cryptolModule, env') - + cm <- mkCryptolModule mod' env' + return (cm, env') -- | mkCryptolModule - translate a T.Module to a CryptolModule --- --- FIXME: --- - This incorrectly excludes both submodules and their contents from --- both of the NamingEnvs in `CryptolModule` --- mkCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => T.Module -> CryptolEnv -> IO CryptolModule @@ -503,7 +526,7 @@ mkCryptolModule m env = newTermEnv ) --- | bindCryptolModule - ad hoc function/hook that allows for extending +-- | bindExtCryptolModule - ad hoc function/hook that allows for extending -- the Cryptol env with the names in a CryptolModule. -- -- Three command line variants get us here: @@ -518,6 +541,21 @@ mkCryptolModule m env = -- TODO: -- - new design in PR #2593 (addressing issue #2569) should replace -- this function so that the fundamental work is done via `importCryptolModule`. +-- +bindExtCryptolModule :: + (P.ModName, ExtCryptolModule) -> CryptolEnv -> CryptolEnv +bindExtCryptolModule (modName, ecm) = + case ecm of + ECM_CryptolModule cm -> bindCryptolModule (modName, cm) + ECM_LoadedModule nm -> bindLoadedModule (modName, nm) + +bindLoadedModule :: + (P.ModName, P.Located C.ModName) -> CryptolEnv -> CryptolEnv +bindLoadedModule (asName, origName) env = + env{eImports= mkImport PublicAndPrivate origName (Just asName) Nothing + : eImports env + } + bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv bindCryptolModule (modName, CryptolModule sm tm) env = From 11cdf1843b5c0877f7720210232c2cfa912c2fcf Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sat, 20 Sep 2025 20:49:52 -0700 Subject: [PATCH 13/26] generalize the internals of "CryptolModule" (as seen on command-line) and updating code to reflect this - CryptolModule (as known at the command line) is generalized to ExtCryptolModule, - this allows for a module to be represented as EITHER - CryptolModule (2 namespaces), or - the name of a loaded module - This allows for simpler and newly shared code - This now should support submodules when we `cryptol_load`. --- .../src/CryptolSAWCore/CryptolEnv.hs | 66 ++++++++++++------- intTests/test_saw_submodule_access1/test.sh | 6 +- .../test_load_D.saw | 48 ++++++++++++-- saw-central/src/SAWCentral/Builtins.hs | 11 ++-- saw-central/src/SAWCentral/Value.hs | 6 +- saw-script/src/SAWScript/Interpreter.hs | 8 +-- 6 files changed, 99 insertions(+), 46 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index e6f7381a8..01ffeff91 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -9,14 +9,20 @@ Stability : provisional {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE LambdaCase #-} module CryptolSAWCore.CryptolEnv ( ImportVisibility(..) , CryptolEnv(..) + + , ExtCryptolModule(..) + , showExtCryptolModule , initCryptolEnv , loadCryptolModule - , bindCryptolModule - , extractDefFromCryptolModule + , loadExtCryptolModule + , bindExtCryptolModule + + , extractDefFromExtCryptolModule , combineCryptolEnv , importCryptolModule , bindTypedTerm @@ -114,18 +120,6 @@ data InputText = InputText , inpCol :: Int -- ^ On this column number } - --- | ExtCryptolModule - Extended CryptolModule; we keep track of --- whether this module came directly from a constructed --- `CryptolModule` or whether it came from parsing a Cryptol module --- in filesystem (in which case it is loaded). -data ExtCryptolModule = - ECM_LoadedModule (P.Located C.ModName) -- source is load - | ECM_CryptolModule CryptolModule -- source in cryptol_prims - -- deriving (Show) - -- FIXME: TODO: more instances - - -- | 'ImportVisibility' - Should a given import (see 'importCryptolModule') -- result in all symbols being visible (as they are for focused -- modules in the Cryptol REPL) or only public symbols? Making all @@ -438,7 +432,23 @@ combineCryptolEnv chkEnv newEnv = return chkEnv{ eModuleEnv = menv' } ----- CryptolModule/ExtCryptolModule functions: --------------------------------- +---- CryptolModule/ExtCryptolModule types and functions: ----------------------- + + +-- | ExtCryptolModule - Extended CryptolModule; we keep track of +-- whether this module came directly from a constructed +-- `CryptolModule` or whether it came from parsing a Cryptol module +-- from filesystem (in which case it is loaded). +data ExtCryptolModule = + ECM_LoadedModule (P.Located C.ModName) -- ^ source is parsed/loaded + | ECM_CryptolModule CryptolModule -- ^ source, constructed + -- (e.g., via cryptol_prims) + +showExtCryptolModule :: ExtCryptolModule -> String +showExtCryptolModule = + \case + ECM_LoadedModule name -> "loaded module '" ++ show(pp name) ++ "'" + ECM_CryptolModule cm -> showCryptolModule cm -- | loadCryptolModule - load a cryptol module and returns the -- `ExtCryptolModule`. The contents of the module are not directly @@ -581,16 +591,22 @@ bindCryptolModule (modName, CryptolModule sm tm) env = addTSyn name = MN.shadowing (MN.singletonNS C.NSType (P.mkQual modName (MN.nameIdent name)) name) -- | NOTE: this is only used in the "cryptol_extract" primitive. -extractDefFromCryptolModule :: CryptolModule -> Text -> IO TypedTerm -extractDefFromCryptolModule (CryptolModule _ tm) name = - case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of - Just t -> return t - Nothing -> fail $ Text.unpack $ "Binding not found: " <> name - -- FIXME: unfortunate we have lost the name of the module. - - -- FIXME: bug: we can't access definitions in submodules. - -- FIXME: this is ad hoc, somehow invoke parse for name, or the like? - +extractDefFromExtCryptolModule :: ExtCryptolModule -> Text -> IO TypedTerm +extractDefFromExtCryptolModule ecm name = + case ecm of + ECM_LoadedModule _modname -> + -- do env' <- bindLoadedModule ... + panic "extractDefFromExtCryptolModule" + ["FIXME: not implemented yet: need plumbing!"] + ECM_CryptolModule (CryptolModule _ tm) -> + case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of + Just t -> return t + Nothing -> fail $ Text.unpack $ "Binding not found: " <> name + + -- FIXME: bug: we can't access definitions in submodules. + -- FIXME: this is ad hoc, somehow invoke parse for name, or the like? + -- FIXME: if one had a CryptolModule with qualified names (e.g., it + -- was generated from a module with submodules), would this work? ---- Core functions for loading and Translating Modules ------------------------ diff --git a/intTests/test_saw_submodule_access1/test.sh b/intTests/test_saw_submodule_access1/test.sh index c6c01a2e6..79e3e0452 100755 --- a/intTests/test_saw_submodule_access1/test.sh +++ b/intTests/test_saw_submodule_access1/test.sh @@ -5,10 +5,6 @@ $SAW test_import_errors.saw $SAW test_import_D.saw -! $SAW test_load_D.saw - - # finishing https://github.com/GaloisInc/saw-script/pull/2593 - # should allow test_load_D.saw to succeed. (as it should) - # TODO: remove the ! above when that PR is done. +$SAW test_load_D.saw $SAW test_UseFunctors.saw diff --git a/intTests/test_saw_submodule_access1/test_load_D.saw b/intTests/test_saw_submodule_access1/test_load_D.saw index 09c0a0df1..c73eba4de 100644 --- a/intTests/test_saw_submodule_access1/test_load_D.saw +++ b/intTests/test_saw_submodule_access1/test_load_D.saw @@ -1,9 +1,47 @@ -D <- cryptol_load "D.cry"; +//////////////////////////////////////////////// +DDD <- cryptol_load "D.cry"; -print (eval_int {{D::D2::d2}}); // should succeed +print (eval_int {{DDD::D2::d2}}); // should succeed + +return DDD; // confirming fails of things that shouldn't be in scope: -fails (do {return {{ d2 }};}); -fails (do {return {{ D::d2 }};}); +fails (do {return {{D::D2::d2}};}); // 'D' not in scope. +fails (do {return {{ d2 }};}); // this requires DDD qualifier +fails (do {return {{ DDD::d2 }};}); // missing submodule qualifier. + +//////////////////////////////////////////////// +// Secondary bindings + +print "secondary bindings:"; + +DDD2 <- return DDD; +let DDD3 = DDD; + +print (eval_int {{DDD2::D2::d2}}); // should succeed +print (eval_int {{DDD3::D2::d2}}); // should succeed + +///////////////////////////////////////////// +// NOW let's see how the prims work: + +let CP1 = cryptol_prims (); +CP2 <- return (cryptol_prims ()); + +print ""; +print "{{ CP1::trunc }}"; +print {{ CP1::trunc }}; + +print ""; +print "{{ CP2::uext }}"; +print {{ CP2::uext }}; + +print ""; +fails (do {return {{ uext }};}); // not (directly) in scope. + +print "CP1 sext:"; +do {y <- cryptol_extract CP1 "sext"; print y;}; + +print "CP2 sgt:"; +do {y <- cryptol_extract CP2 "sgt"; print y;}; -print "done"; \ No newline at end of file +print "done"; diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index c5c13995f..4c4e8a11b 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -2046,8 +2046,11 @@ get_env name = do Nothing -> fail $ "Environment variable not found: " ++ Text.unpack name Just v -> return $ Text.pack v -cryptol_prims :: TopLevel CryptolModule -cryptol_prims = CryptolModule Map.empty <$> Map.fromList <$> traverse parsePrim prims +cryptol_prims :: TopLevel CEnv.ExtCryptolModule +cryptol_prims = + CEnv.ECM_CryptolModule + <$> CryptolModule Map.empty + <$> Map.fromList <$> traverse parsePrim prims where prims :: [(Text, Ident, Text)] prims = @@ -2082,13 +2085,13 @@ cryptol_prims = CryptolModule Map.empty <$> Map.fromList <$> traverse parsePrim putTopLevelRW $ rw { rwCryptol = cenv' } return (n', TypedTerm (TypedTermSchema s') t') -cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CryptolModule +cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CEnv.ExtCryptolModule cryptol_load fileReader path = do sc <- getSharedContext rw <- getTopLevelRW let ce = rwCryptol rw let ?fileReader = fileReader - (m, ce') <- io $ CEnv.loadCryptolModule sc ce path + (m, ce') <- io $ CEnv.loadExtCryptolModule sc ce path putTopLevelRW $ rw { rwCryptol = ce' } return m diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 2beb60f9e..bb6cd8701 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -558,7 +558,7 @@ data Value | VJavaType JavaType | VLLVMType LLVM.Type | VMIRType MIR.Ty - | VCryptolModule CryptolModule + | VCryptolModule CEnv.ExtCryptolModule | VJavaClass JSS.Class | VLLVMModule (Some CMSLLVM.LLVMModule) | VMIRModule RustModule @@ -692,7 +692,7 @@ showsPrecValue opts nenv p v = VJavaType {} -> showString "<>" VLLVMType t -> showString (show (Crucible.LLVM.ppType t)) VMIRType t -> showString (show (PP.pretty t)) - VCryptolModule m -> showString (showCryptolModule m) + VCryptolModule m -> showString (CEnv.showExtCryptolModule m) VLLVMModule (Some m) -> showString (CMSLLVM.showLLVMModule m) VMIRModule m -> shows (PP.pretty (m^.rmCS^.collection)) VMIRAdt adt -> shows (PP.pretty adt) @@ -1148,7 +1148,7 @@ extendEnv sc name ty md v rw = VInteger n -> pure $ CEnv.bindInteger (ident, n) ce VCryptolModule m -> - pure $ CEnv.bindCryptolModule (modname, m) ce + pure $ CEnv.bindExtCryptolModule (modname, m) ce VString s -> do tt <- typedTermOfString sc (Text.unpack s) pure $ CEnv.bindTypedTerm (ident, tt) ce diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 9d9b52dcd..9682709a2 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -1579,10 +1579,10 @@ instance FromValue MIR.Ty where fromValue _ (VMIRType t) = t fromValue _ _ = error "fromValue MIRType" -instance IsValue CryptolModule where +instance IsValue CEnv.ExtCryptolModule where toValue _name m = VCryptolModule m -instance FromValue CryptolModule where +instance FromValue CEnv.ExtCryptolModule where fromValue _ (VCryptolModule m) = m fromValue _ _ = error "fromValue CryptolModule" @@ -2201,7 +2201,7 @@ do_offline_w4_unint_yices :: [Text] -> Text -> ProofScript () do_offline_w4_unint_yices unints path = offline_w4_unint_yices unints (Text.unpack path) -do_cryptol_load :: (FilePath -> IO BS.ByteString) -> Text -> TopLevel CryptolModule +do_cryptol_load :: (FilePath -> IO BS.ByteString) -> Text -> TopLevel CEnv.ExtCryptolModule do_cryptol_load loader path = cryptol_load loader (Text.unpack path) @@ -4122,7 +4122,7 @@ primitives = Map.fromList [ "Load the given file as a Cryptol module." ] , prim "cryptol_extract" "CryptolModule -> String -> TopLevel Term" - (pureVal CEnv.extractDefFromCryptolModule) + (pureVal CEnv.extractDefFromExtCryptolModule) Current [ "Load a single definition from a Cryptol module and translate it into" , "a 'Term'." From 72406e0b153bd6decdaa7f2fa498f0d2e40c975d Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Tue, 23 Sep 2025 18:26:39 -0700 Subject: [PATCH 14/26] refactors, comments, whitespace --- .../src/CryptolSAWCore/CryptolEnv.hs | 81 +++++++++++-------- 1 file changed, 46 insertions(+), 35 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 01ffeff91..c348382c2 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -131,7 +131,8 @@ data InputText = InputText -- data ImportVisibility = OnlyPublic -- ^ behaves like a normal Cryptol "import" - | PublicAndPrivate -- ^ allows viewing of both "private" sections and (arbitrarily nested) submodules. + | PublicAndPrivate -- ^ allows viewing of both "private" sections + -- and (arbitrarily nested) submodules. deriving (Eq, Show) @@ -188,6 +189,7 @@ nameMatcher xs = in last cs == identText (C.ogName og) && init cs == C.modNameChunksText top ++ map identText ns + -- Initialize ------------------------------------------------------------------ -- | initCryptolEnv - Create initial CryptolEnv, this involves loading @@ -227,7 +229,7 @@ initCryptolEnv sc = do _ <- MB.loadModuleFrom False (MM.FromModule arrayName) return () - -- Load Cryptol reference implementations + -- Load Cryptol reference implementation ((_,refTop), modEnv3) <- liftModuleM modEnv2 $ MB.loadModuleFrom False (MM.FromModule preludeReferenceName) @@ -476,13 +478,13 @@ loadExtCryptolModule sc env path = -- | loadCryptolModule -- --- NOTE: +-- NOTE RE CALLERS: -- - the path to this function from the command line is only via -- the experimental "write_coq_cryptol_module" command. -- --- FIXME: This incorrectly (in MkCryptolModule) excludes both --- submodules and their contents from the NamingEnvs in --- `CryptolModule` +-- This function (note `mkCryptolModule`) returns the public types and values +-- of the module in a `CryptolModule` structure. +-- loadCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => SharedContext -> @@ -495,7 +497,11 @@ loadCryptolModule sc env path = cm <- mkCryptolModule mod' env' return (cm, env') --- | mkCryptolModule - translate a T.Module to a CryptolModule + +-- | mkCryptolModule m env - translate a @m :: T.Module@ to a `CryptolModule` +-- +-- This function returns the public types and values of the module `m` +-- as a `CryptolModule` structure. mkCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => T.Module -> CryptolEnv -> IO CryptolModule @@ -504,9 +510,9 @@ mkCryptolModule m env = let newTermEnv = eTermEnv env modEnv = eModuleEnv env ifaceDecls = getAllIfaceDecls modEnv - (types, _modEnv) <- liftModuleM modEnv $ do - -- NOTE: _modEnv == modEnv - -- - as we elaborate below, the monadic actions are all 'readers' + (types, _modEnv) <- liftModuleM modEnv $ + -- NOTE: _modEnv == modEnv, because, as we elaborate below, + -- the monadic actions are all 'readers'. do prims <- MB.getPrimMap -- generate the primitive map; a monad reader TM.inpVars `fmap` @@ -518,28 +524,32 @@ mkCryptolModule m env = -- - If we had inlined, it appears that this is functional code. -- - (Possibly because of information hiding?) - let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name return $ - CryptolModule - -- create type synonym Map, keep only the exports: - (Map.filterWithKey - (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) - (T.mTySyns m) - ) - -- FIXME: TODO: ensure type synonyms in submodule are included. - - -- create the map of symbols: - ( Map.filterWithKey (\k _ -> Set.member k names) - $ Map.intersectionWith - (\t x -> TypedTerm (TypedTermSchema t) x) - types - newTermEnv - ) - --- | bindExtCryptolModule - ad hoc function/hook that allows for extending --- the Cryptol env with the names in a CryptolModule. + let + -- we're keeping only the exports of `m`: + vNameSet = MEx.exported C.NSValue (T.mExports m) + tNameSet = MEx.exported C.NSType (T.mExports m) + in + CryptolModule + -- create Map of type synonyms + (Map.filterWithKey + (\k _ -> Set.member k tNameSet) + (T.mTySyns m) + ) + + -- create Map of the `TypedTerm` s: + ( Map.filterWithKey (\k _ -> Set.member k vNameSet) + $ Map.intersectionWith + (\t x -> TypedTerm (TypedTermSchema t) x) + types + newTermEnv + ) + +-- | bindExtCryptolModule - ad hoc function/hook that allows for +-- extending the Cryptol environment with the names in a Cryptol +-- module, `ExtCryptolModule`. -- --- Three command line variants get us here: +-- NOTE RE CALLERS: Three command line variants get us here: -- > D <- cryptol_load "PATH" -- > x <- return (cryptol_prims ()) -- > let x = cryptol_prims () @@ -608,6 +618,7 @@ extractDefFromExtCryptolModule ecm name = -- FIXME: if one had a CryptolModule with qualified names (e.g., it -- was generated from a module with submodules), would this work? + ---- Core functions for loading and Translating Modules ------------------------ loadAndTranslateModule :: @@ -969,10 +980,10 @@ declareName env mname input = do typeNoUser :: T.Type -> T.Type typeNoUser t = case t of - T.TCon tc ts -> T.TCon tc (map typeNoUser ts) - T.TVar {} -> t - T.TUser _ _ ty -> typeNoUser ty - T.TRec fields -> T.TRec (fmap typeNoUser fields) + T.TCon tc ts -> T.TCon tc (map typeNoUser ts) + T.TVar {} -> t + T.TUser _ _ ty -> typeNoUser ty + T.TRec fields -> T.TRec (fmap typeNoUser fields) T.TNominal nt ts -> T.TNominal nt (fmap typeNoUser ts) schemaNoUser :: T.Schema -> T.Schema @@ -988,7 +999,7 @@ locatedUnknown x = P.Located P.emptyRange x -- of this function. liftModuleM :: - (?fileReader :: FilePath -> IO ByteString) => + (?fileReader :: FilePath -> IO ByteString) => ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv) liftModuleM env m = do let minp solver = MM.ModuleInput { From 1abc03879d6279e7530dca16be6e83126b8b78f9 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Tue, 23 Sep 2025 18:40:22 -0700 Subject: [PATCH 15/26] revert (misguided) c923c717b revert c923c717b... improve submodule support for CLI `cryptol_load` --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 3 --- 1 file changed, 3 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index c348382c2..7006ecba1 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -581,7 +581,6 @@ bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv bindCryptolModule (modName, CryptolModule sm tm) env = env { eExtraNames = flip (foldr addName) (Map.keys tm') $ flip (foldr addTSyn) (Map.keys sm) $ - flip (foldr addSubModule) (Map.keys tm') $ eExtraNames env , eExtraTSyns = Map.union sm (eExtraTSyns env) , eExtraTypes = Map.union (fmap fst tm') (eExtraTypes env) @@ -596,8 +595,6 @@ bindCryptolModule (modName, CryptolModule sm tm) env = addName name = MN.shadowing (MN.singletonNS C.NSValue (P.mkQual modName (MN.nameIdent name)) name) - addSubModule name = MN.shadowing (MN.singletonNS C.NSModule (P.mkQual modName (MN.nameIdent name)) name) - addTSyn name = MN.shadowing (MN.singletonNS C.NSType (P.mkQual modName (MN.nameIdent name)) name) -- | NOTE: this is only used in the "cryptol_extract" primitive. From 873ee631a66b12a7d62a91f2b624e9f07b8c394a Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Tue, 23 Sep 2025 18:43:19 -0700 Subject: [PATCH 16/26] comments: move/improve; change whitespace/identing --- .../src/CryptolSAWCore/CryptolEnv.hs | 46 +++++++++++-------- 1 file changed, 28 insertions(+), 18 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 7006ecba1..1cac7562e 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -478,7 +478,7 @@ loadExtCryptolModule sc env path = -- | loadCryptolModule -- --- NOTE RE CALLERS: +-- NOTE RE CALLS TO: -- - the path to this function from the command line is only via -- the experimental "write_coq_cryptol_module" command. -- @@ -547,21 +547,13 @@ mkCryptolModule m env = -- | bindExtCryptolModule - ad hoc function/hook that allows for -- extending the Cryptol environment with the names in a Cryptol --- module, `ExtCryptolModule`. +-- module, represented here by a `ExtCryptolModule`. -- --- NOTE RE CALLERS: Three command line variants get us here: +-- NOTE RE CALLS TO: Three command line variants get us here: -- > D <- cryptol_load "PATH" -- > x <- return (cryptol_prims ()) -- > let x = cryptol_prims () -- --- FIXME: --- - submodules are not handled correctly below. --- - the code is somewhat duplicating functionality that we --- already have with `importCryptolModule` --- TODO: --- - new design in PR #2593 (addressing issue #2569) should replace --- this function so that the fundamental work is done via `importCryptolModule`. --- bindExtCryptolModule :: (P.ModName, ExtCryptolModule) -> CryptolEnv -> CryptolEnv bindExtCryptolModule (modName, ecm) = @@ -575,8 +567,16 @@ bindLoadedModule (asName, origName) env = env{eImports= mkImport PublicAndPrivate origName (Just asName) Nothing : eImports env } + -- FIXME:MT: PublicAndPrivate?! - +-- | bindCryptolModule - binding when we have the ECM_CryptolModule side. +-- +-- NOTE: +-- - this code is duplicating functionality that we already have with +-- `importCryptolModule`. We would like to have just one piece of +-- code that computes the names (i.e., have just "one source of +-- truth" here). +-- bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv bindCryptolModule (modName, CryptolModule sm tm) env = env { eExtraNames = flip (foldr addName) (Map.keys tm') $ @@ -593,9 +593,13 @@ bindCryptolModule (modName, CryptolModule sm tm) env = f (TypedTerm (TypedTermSchema s) x) = Just (s,x) f _ = Nothing - addName name = MN.shadowing (MN.singletonNS C.NSValue (P.mkQual modName (MN.nameIdent name)) name) + addName name = + MN.shadowing + (MN.singletonNS C.NSValue (P.mkQual modName (MN.nameIdent name)) name) - addTSyn name = MN.shadowing (MN.singletonNS C.NSType (P.mkQual modName (MN.nameIdent name)) name) + addTSyn name = + MN.shadowing + (MN.singletonNS C.NSType (P.mkQual modName (MN.nameIdent name)) name) -- | NOTE: this is only used in the "cryptol_extract" primitive. extractDefFromExtCryptolModule :: ExtCryptolModule -> Text -> IO TypedTerm @@ -610,10 +614,16 @@ extractDefFromExtCryptolModule ecm name = Just t -> return t Nothing -> fail $ Text.unpack $ "Binding not found: " <> name - -- FIXME: bug: we can't access definitions in submodules. - -- FIXME: this is ad hoc, somehow invoke parse for name, or the like? - -- FIXME: if one had a CryptolModule with qualified names (e.g., it - -- was generated from a module with submodules), would this work? + -- NOTE RE CALLS TO: + -- - currently we can only get to this branch when CryptolModule + -- is the one created with `cryptol_prims` (Haskell function and + -- SAWScript function). E.g., + -- + -- > cryptol_extract (cryptol_prims ()) "trunc" + -- + -- FIXME: this code is somewhat ad hoc, might we rather invoke + -- parse for name, or the like? However, we expect this code + -- would likely go away after we address Issue #. ---- Core functions for loading and Translating Modules ------------------------ From 5341ca91c11b742d983e8d1f8ab9f526077c289d Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 24 Sep 2025 14:37:10 -0700 Subject: [PATCH 17/26] refactor: re-plumb to get more arguments to `extractDefFromExtCryptolModule` --- .../src/CryptolSAWCore/CryptolEnv.hs | 18 ++++++++++++------ saw-central/src/SAWCentral/Builtins.hs | 7 +++++++ saw-script/src/SAWScript/Interpreter.hs | 2 +- 3 files changed, 20 insertions(+), 7 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 1cac7562e..dc6a39791 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -601,18 +601,24 @@ bindCryptolModule (modName, CryptolModule sm tm) env = MN.shadowing (MN.singletonNS C.NSType (P.mkQual modName (MN.nameIdent name)) name) --- | NOTE: this is only used in the "cryptol_extract" primitive. -extractDefFromExtCryptolModule :: ExtCryptolModule -> Text -> IO TypedTerm -extractDefFromExtCryptolModule ecm name = + +-- | extractDefFromExtCryptolModule sc en ecm name - interpret `name` as a definition in +-- the module `ecm`, return the TypedTerm. +-- +-- NOTE RE CALLS TO: this is (only) used for the "cryptol_extract" primitive. +-- +extractDefFromExtCryptolModule :: + SharedContext -> CryptolEnv -> ExtCryptolModule -> Text -> IO TypedTerm +extractDefFromExtCryptolModule sc env ecm name = case ecm of ECM_LoadedModule _modname -> -- do env' <- bindLoadedModule ... panic "extractDefFromExtCryptolModule" ["FIXME: not implemented yet: need plumbing!"] ECM_CryptolModule (CryptolModule _ tm) -> - case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of - Just t -> return t - Nothing -> fail $ Text.unpack $ "Binding not found: " <> name + case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of + Just t -> return t + Nothing -> fail $ Text.unpack $ "Binding not found: " <> name -- NOTE RE CALLS TO: -- - currently we can only get to this branch when CryptolModule diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index 4c4e8a11b..ada022fde 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -2095,6 +2095,13 @@ cryptol_load fileReader path = do putTopLevelRW $ rw { rwCryptol = ce' } return m +cryptol_extract :: CEnv.ExtCryptolModule -> Text -> TopLevel TypedTerm +cryptol_extract ecm var = do + sc <- getSharedContext + rw <- getTopLevelRW + let ce = rwCryptol rw + io $ CEnv.extractDefFromExtCryptolModule sc ce ecm var + cryptol_add_path :: FilePath -> TopLevel () cryptol_add_path path = do rw <- getTopLevelRW diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 9682709a2..8ea56846f 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -4122,7 +4122,7 @@ primitives = Map.fromList [ "Load the given file as a Cryptol module." ] , prim "cryptol_extract" "CryptolModule -> String -> TopLevel Term" - (pureVal CEnv.extractDefFromExtCryptolModule) + (pureVal cryptol_extract) Current [ "Load a single definition from a Cryptol module and translate it into" , "a 'Term'." From c7a3f80cae0ed88759d7ad331145b88f7daf690e Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 24 Sep 2025 14:38:00 -0700 Subject: [PATCH 18/26] finish "generalize the internals of "CryptolModule" by finishing extractDefFromExtCryptolModule --- .../src/CryptolSAWCore/CryptolEnv.hs | 26 ++++++++++++++++--- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index dc6a39791..795c46e08 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -611,10 +611,19 @@ extractDefFromExtCryptolModule :: SharedContext -> CryptolEnv -> ExtCryptolModule -> Text -> IO TypedTerm extractDefFromExtCryptolModule sc env ecm name = case ecm of - ECM_LoadedModule _modname -> - -- do env' <- bindLoadedModule ... - panic "extractDefFromExtCryptolModule" - ["FIXME: not implemented yet: need plumbing!"] + ECM_LoadedModule loadedModName -> + do let localMN = C.packModName + [ "INTERNAL" + , C.modNameToText (P.thing loadedModName) + ] + env' = bindLoadedModule (localMN, loadedModName) env + -- FIXME: PublicAndPrivate now. ? + expr = noLoc (C.modNameToText localMN <> "::" <> name) + -- FIXME: be more robust? create an identifier? + let ?fileReader = panic "fileReader" + ["extractDefFromExtCryptolModule"] + parseTypedTerm sc env' expr + ECM_CryptolModule (CryptolModule _ tm) -> case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of Just t -> return t @@ -1005,6 +1014,15 @@ schemaNoUser (T.Forall params props ty) = T.Forall params props (typeNoUser ty) ---- Local Utility Functions --------------------------------------------------- +noLoc :: Text -> InputText +noLoc x = InputText + { inpText = x + , inpFile = "(internalUse)" + , inpLine = 1 + , inpCol = 1 + } + + locatedUnknown :: a -> P.Located a locatedUnknown x = P.Located P.emptyRange x -- XXX: it would be better to have the real position, but it From 9d16944bdb337801e192c7c734e66546253ad030 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Wed, 24 Sep 2025 22:23:26 -0700 Subject: [PATCH 19/26] comments --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 795c46e08..3c94e50c8 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -567,7 +567,6 @@ bindLoadedModule (asName, origName) env = env{eImports= mkImport PublicAndPrivate origName (Just asName) Nothing : eImports env } - -- FIXME:MT: PublicAndPrivate?! -- | bindCryptolModule - binding when we have the ECM_CryptolModule side. -- @@ -617,9 +616,7 @@ extractDefFromExtCryptolModule sc env ecm name = , C.modNameToText (P.thing loadedModName) ] env' = bindLoadedModule (localMN, loadedModName) env - -- FIXME: PublicAndPrivate now. ? expr = noLoc (C.modNameToText localMN <> "::" <> name) - -- FIXME: be more robust? create an identifier? let ?fileReader = panic "fileReader" ["extractDefFromExtCryptolModule"] parseTypedTerm sc env' expr @@ -637,9 +634,9 @@ extractDefFromExtCryptolModule sc env ecm name = -- > cryptol_extract (cryptol_prims ()) "trunc" -- -- FIXME: this code is somewhat ad hoc, might we rather invoke - -- parse for name, or the like? However, we expect this code - -- would likely go away after we address Issue #. - + -- parse for name, or the like? However, this code becomes + -- unnecessary after addressing Issue #2645 (turning + -- cryptol_prims into a built-in Cryptol module). ---- Core functions for loading and Translating Modules ------------------------ From 9d5136ed26fb75f7431564399d8f6b3538b03277 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Thu, 25 Sep 2025 09:58:25 -0700 Subject: [PATCH 20/26] plumb ?fileReader down. --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 3 +-- saw-central/src/SAWCentral/Builtins.hs | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 3c94e50c8..fde9e2dab 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -607,6 +607,7 @@ bindCryptolModule (modName, CryptolModule sm tm) env = -- NOTE RE CALLS TO: this is (only) used for the "cryptol_extract" primitive. -- extractDefFromExtCryptolModule :: + (?fileReader :: FilePath -> IO ByteString) => SharedContext -> CryptolEnv -> ExtCryptolModule -> Text -> IO TypedTerm extractDefFromExtCryptolModule sc env ecm name = case ecm of @@ -617,8 +618,6 @@ extractDefFromExtCryptolModule sc env ecm name = ] env' = bindLoadedModule (localMN, loadedModName) env expr = noLoc (C.modNameToText localMN <> "::" <> name) - let ?fileReader = panic "fileReader" - ["extractDefFromExtCryptolModule"] parseTypedTerm sc env' expr ECM_CryptolModule (CryptolModule _ tm) -> diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index ada022fde..94dd118f3 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -2100,6 +2100,7 @@ cryptol_extract ecm var = do sc <- getSharedContext rw <- getTopLevelRW let ce = rwCryptol rw + let ?fileReader = StrictBS.readFile io $ CEnv.extractDefFromExtCryptolModule sc ce ecm var cryptol_add_path :: FilePath -> TopLevel () From 970121240adf9a170cf45770728553f1c7720532 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sat, 27 Sep 2025 15:54:03 -0700 Subject: [PATCH 21/26] refactor mkCryptolModule (inline internals and simplify) --- .../src/CryptolSAWCore/CryptolEnv.hs | 35 ++++--------------- 1 file changed, 7 insertions(+), 28 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index fde9e2dab..d935bf81c 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -418,8 +418,7 @@ translateDeclGroups sc env dgs = let names = map T.dName decls let newTypes = Map.fromList [ (T.dName d, T.dSignature d) | d <- decls ] let addName name = MR.shadowing (MN.singletonNS C.NSValue (P.mkUnqual (MN.nameIdent name)) name) - return env - { eExtraNames = foldr addName (eExtraNames env) names + return env{ eExtraNames = foldr addName (eExtraNames env) names , eExtraTypes = Map.union (eExtraTypes env) newTypes , eTermEnv = C.envE cryEnv' } @@ -494,38 +493,18 @@ loadCryptolModule :: loadCryptolModule sc env path = do (mod', env') <- loadAndTranslateModule sc env (Left path) - cm <- mkCryptolModule mod' env' - return (cm, env') + return (mkCryptolModule mod' env', env') -- | mkCryptolModule m env - translate a @m :: T.Module@ to a `CryptolModule` -- -- This function returns the public types and values of the module `m` -- as a `CryptolModule` structure. -mkCryptolModule :: - (?fileReader :: FilePath -> IO ByteString) => - T.Module -> CryptolEnv -> IO CryptolModule +mkCryptolModule :: T.Module -> CryptolEnv -> CryptolModule mkCryptolModule m env = - do - let newTermEnv = eTermEnv env - modEnv = eModuleEnv env - ifaceDecls = getAllIfaceDecls modEnv - (types, _modEnv) <- liftModuleM modEnv $ - -- NOTE: _modEnv == modEnv, because, as we elaborate below, - -- the monadic actions are all 'readers'. - do prims <- MB.getPrimMap - -- generate the primitive map; a monad reader - TM.inpVars `fmap` - MB.genInferInput P.emptyRange prims NoParams ifaceDecls - -- NOTE: inpVars are the variables that are in scope. - -- FIXME: - -- - Why are we calling mB.genInferInput then projecting out - -- `inpVars`? - -- - If we had inlined, it appears that this is functional code. - -- - (Possibly because of information hiding?) - - return $ - let + let + ifaceDecls = getAllIfaceDecls (eModuleEnv env) + types = Map.map MI.ifDeclSig (MI.ifDecls ifaceDecls) -- we're keeping only the exports of `m`: vNameSet = MEx.exported C.NSValue (T.mExports m) tNameSet = MEx.exported C.NSType (T.mExports m) @@ -542,7 +521,7 @@ mkCryptolModule m env = $ Map.intersectionWith (\t x -> TypedTerm (TypedTermSchema t) x) types - newTermEnv + (eTermEnv env) ) -- | bindExtCryptolModule - ad hoc function/hook that allows for From dbd44c5032cbf3364dfcce377434fbd18ce69b94 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sat, 27 Sep 2025 15:55:04 -0700 Subject: [PATCH 22/26] wibble to improve messages (info and error) --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index d935bf81c..42247a867 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -419,9 +419,9 @@ translateDeclGroups sc env dgs = let newTypes = Map.fromList [ (T.dName d, T.dSignature d) | d <- decls ] let addName name = MR.shadowing (MN.singletonNS C.NSValue (P.mkUnqual (MN.nameIdent name)) name) return env{ eExtraNames = foldr addName (eExtraNames env) names - , eExtraTypes = Map.union (eExtraTypes env) newTypes - , eTermEnv = C.envE cryEnv' - } + , eExtraTypes = Map.union (eExtraTypes env) newTypes + , eTermEnv = C.envE cryEnv' + } ---- Misc Exports -------------------------------------------------------------- @@ -448,7 +448,7 @@ data ExtCryptolModule = showExtCryptolModule :: ExtCryptolModule -> String showExtCryptolModule = \case - ECM_LoadedModule name -> "loaded module '" ++ show(pp name) ++ "'" + ECM_LoadedModule name -> "loaded module '" ++ show(pp (P.thing name)) ++ "'" ECM_CryptolModule cm -> showCryptolModule cm -- | loadCryptolModule - load a cryptol module and returns the @@ -508,7 +508,7 @@ mkCryptolModule m env = -- we're keeping only the exports of `m`: vNameSet = MEx.exported C.NSValue (T.mExports m) tNameSet = MEx.exported C.NSType (T.mExports m) - in + in CryptolModule -- create Map of type synonyms (Map.filterWithKey @@ -592,12 +592,13 @@ extractDefFromExtCryptolModule sc env ecm name = case ecm of ECM_LoadedModule loadedModName -> do let localMN = C.packModName - [ "INTERNAL" + [ "INTERNAL_EXTRACT_MODNAME" , C.modNameToText (P.thing loadedModName) ] env' = bindLoadedModule (localMN, loadedModName) env expr = noLoc (C.modNameToText localMN <> "::" <> name) parseTypedTerm sc env' expr + -- FIXME: error message for bad `name` exposes the `localMN` to user. ECM_CryptolModule (CryptolModule _ tm) -> case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of From 95e7bead6e7a4170b8dd36aff2dcc99d54753979 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sat, 27 Sep 2025 22:23:49 -0700 Subject: [PATCH 23/26] refactor --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 42247a867..ea0fb78a3 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -471,8 +471,8 @@ loadExtCryptolModule :: IO (ExtCryptolModule, CryptolEnv) loadExtCryptolModule sc env path = do - (mod', env') <- loadAndTranslateModule sc env (Left path) - return (ECM_LoadedModule (locatedUnknown (T.mName mod')), env') + (m, env') <- loadAndTranslateModule sc env (Left path) + return (ECM_LoadedModule (locatedUnknown (T.mName m)), env') -- | loadCryptolModule From b8750806399140ce5c0aac77663013caea924c4f Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sat, 27 Sep 2025 22:38:00 -0700 Subject: [PATCH 24/26] Improve how we show a ECM_LoadedModule to the user. --- .../src/CryptolSAWCore/CryptolEnv.hs | 36 +++++++++++++------ 1 file changed, 26 insertions(+), 10 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index ea0fb78a3..1cff4fc0d 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -433,7 +433,7 @@ combineCryptolEnv chkEnv newEnv = return chkEnv{ eModuleEnv = menv' } ----- CryptolModule/ExtCryptolModule types and functions: ----------------------- +---- Types and functions for CryptolModule & ExtCryptolModule ------------------ -- | ExtCryptolModule - Extended CryptolModule; we keep track of @@ -441,15 +441,28 @@ combineCryptolEnv chkEnv newEnv = -- `CryptolModule` or whether it came from parsing a Cryptol module -- from filesystem (in which case it is loaded). data ExtCryptolModule = - ECM_LoadedModule (P.Located C.ModName) -- ^ source is parsed/loaded - | ECM_CryptolModule CryptolModule -- ^ source, constructed - -- (e.g., via cryptol_prims) + -- | source is parsed/loaded + ECM_LoadedModule + { ecm_name :: P.Located C.ModName + , ecm_show :: String -- ^ how we show this on SAWScript CLI, + -- We can't look at state to compute show, + -- thus this (albeit adhoc). + } + + -- | source is internal/constructed (e.g., via cryptol_prims) + | ECM_CryptolModule {ecm_cm :: CryptolModule} showExtCryptolModule :: ExtCryptolModule -> String showExtCryptolModule = \case - ECM_LoadedModule name -> "loaded module '" ++ show(pp (P.thing name)) ++ "'" - ECM_CryptolModule cm -> showCryptolModule cm + ECM_LoadedModule name s -> + unlines ["Loaded module '" ++ show(pp (P.thing name)) ++ "':" + , s + ] + ECM_CryptolModule cm -> + unlines [ "Internal module:" + , showCryptolModule cm + ] -- | loadCryptolModule - load a cryptol module and returns the -- `ExtCryptolModule`. The contents of the module are not directly @@ -472,7 +485,10 @@ loadExtCryptolModule :: loadExtCryptolModule sc env path = do (m, env') <- loadAndTranslateModule sc env (Left path) - return (ECM_LoadedModule (locatedUnknown (T.mName m)), env') + let s = showCryptolModule (mkCryptolModule m env') + -- how to show, need to compute this here. + -- FIXME: this only shows public names, not internal. + return (ECM_LoadedModule (locatedUnknown (T.mName m)) s, env') -- | loadCryptolModule @@ -537,8 +553,8 @@ bindExtCryptolModule :: (P.ModName, ExtCryptolModule) -> CryptolEnv -> CryptolEnv bindExtCryptolModule (modName, ecm) = case ecm of - ECM_CryptolModule cm -> bindCryptolModule (modName, cm) - ECM_LoadedModule nm -> bindLoadedModule (modName, nm) + ECM_CryptolModule cm -> bindCryptolModule (modName, cm) + ECM_LoadedModule nm _ -> bindLoadedModule (modName, nm) bindLoadedModule :: (P.ModName, P.Located C.ModName) -> CryptolEnv -> CryptolEnv @@ -590,7 +606,7 @@ extractDefFromExtCryptolModule :: SharedContext -> CryptolEnv -> ExtCryptolModule -> Text -> IO TypedTerm extractDefFromExtCryptolModule sc env ecm name = case ecm of - ECM_LoadedModule loadedModName -> + ECM_LoadedModule loadedModName _ -> do let localMN = C.packModName [ "INTERNAL_EXTRACT_MODNAME" , C.modNameToText (P.thing loadedModName) From e90fffffbcfdb9c037f6d17f4694af5a001b814c Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sat, 27 Sep 2025 23:40:28 -0700 Subject: [PATCH 25/26] comments --- cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 1cff4fc0d..46bb93e82 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -48,7 +48,6 @@ module CryptolSAWCore.CryptolEnv ) where ---import qualified Control.Exception as X import Data.ByteString (ByteString) import qualified Data.Text as Text import Data.Map (Map) @@ -614,8 +613,10 @@ extractDefFromExtCryptolModule sc env ecm name = env' = bindLoadedModule (localMN, loadedModName) env expr = noLoc (C.modNameToText localMN <> "::" <> name) parseTypedTerm sc env' expr - -- FIXME: error message for bad `name` exposes the `localMN` to user. + -- FIXME: error message for bad `name` exposes the + -- `localMN` to user. Fixing locally is challenging, as + -- the error is not an exception we can handle here. ECM_CryptolModule (CryptolModule _ tm) -> case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of Just t -> return t From 93fd2d80cd31e9f11c8427ce2ab46e383bba44f9 Mon Sep 17 00:00:00 2001 From: Mark Tullsen Date: Sun, 28 Sep 2025 00:01:36 -0700 Subject: [PATCH 26/26] new tests --- intTests/test_saw_submodule_access1/A2.cry | 4 +++ intTests/test_saw_submodule_access1/G.cry | 6 ++++ intTests/test_saw_submodule_access1/H.cry | 8 +++++ .../HWithSubmodules.cry | 18 ++++++++++++ intTests/test_saw_submodule_access1/test.sh | 6 ++++ .../test_load_extract_D.saw | 27 +++++++++++++++++ .../test_private.saw | 19 ++++++++++++ .../test_private_with_submodules.saw | 29 +++++++++++++++++++ 8 files changed, 117 insertions(+) create mode 100644 intTests/test_saw_submodule_access1/A2.cry create mode 100644 intTests/test_saw_submodule_access1/G.cry create mode 100644 intTests/test_saw_submodule_access1/H.cry create mode 100644 intTests/test_saw_submodule_access1/HWithSubmodules.cry create mode 100644 intTests/test_saw_submodule_access1/test_load_extract_D.saw create mode 100644 intTests/test_saw_submodule_access1/test_private.saw create mode 100644 intTests/test_saw_submodule_access1/test_private_with_submodules.saw diff --git a/intTests/test_saw_submodule_access1/A2.cry b/intTests/test_saw_submodule_access1/A2.cry new file mode 100644 index 000000000..e1c7e0750 --- /dev/null +++ b/intTests/test_saw_submodule_access1/A2.cry @@ -0,0 +1,4 @@ +module A2 where + +a : [32] +a = 3 diff --git a/intTests/test_saw_submodule_access1/G.cry b/intTests/test_saw_submodule_access1/G.cry new file mode 100644 index 000000000..56c79d902 --- /dev/null +++ b/intTests/test_saw_submodule_access1/G.cry @@ -0,0 +1,6 @@ +submodule M where + x = 0x02 + +import submodule M as Q::R + +y = Q::R::x \ No newline at end of file diff --git a/intTests/test_saw_submodule_access1/H.cry b/intTests/test_saw_submodule_access1/H.cry new file mode 100644 index 000000000..c323b077c --- /dev/null +++ b/intTests/test_saw_submodule_access1/H.cry @@ -0,0 +1,8 @@ +module H where + +a : [32] +a = 4 + +private + b : [32] + b = 5 diff --git a/intTests/test_saw_submodule_access1/HWithSubmodules.cry b/intTests/test_saw_submodule_access1/HWithSubmodules.cry new file mode 100644 index 000000000..77cf0c8ca --- /dev/null +++ b/intTests/test_saw_submodule_access1/HWithSubmodules.cry @@ -0,0 +1,18 @@ +module H where + +a : [32] +a = 4 + +private + b : [32] + b = 5 + +submodule H2 where + + c : [32] + c = 6 + + private + + d : [32] + d = 7 diff --git a/intTests/test_saw_submodule_access1/test.sh b/intTests/test_saw_submodule_access1/test.sh index 79e3e0452..1e20d03e7 100755 --- a/intTests/test_saw_submodule_access1/test.sh +++ b/intTests/test_saw_submodule_access1/test.sh @@ -7,4 +7,10 @@ $SAW test_import_D.saw $SAW test_load_D.saw +$SAW test_load_extract_D.saw + $SAW test_UseFunctors.saw + +$SAW test_private.saw + +$SAW test_private_with_submodules.saw diff --git a/intTests/test_saw_submodule_access1/test_load_extract_D.saw b/intTests/test_saw_submodule_access1/test_load_extract_D.saw new file mode 100644 index 000000000..da732753a --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_load_extract_D.saw @@ -0,0 +1,27 @@ +//////////////////////////////////////////////// +DDD <- cryptol_load "D.cry"; + +print (eval_int {{DDD::D2::d2}}); + +print DDD; + +//// cryptol_extract /////////////////////////// + +do { y <- cryptol_extract DDD "D2::d2"; print y;}; +do { y <- cryptol_extract DDD "D2::d2"; print y;}; +fails (do {y <- cryptol_extract DDD "notinscope"; print y;}); + +print DDD; + + +//// cryptol_prims //////////////////////////// + +let PRIMS = cryptol_prims (); + +do {y <- cryptol_extract PRIMS "sext"; print y;}; + +fails (do {y <- cryptol_extract PRIMS "notinscope"; print y;}); + +print PRIMS; + +print "done"; diff --git a/intTests/test_saw_submodule_access1/test_private.saw b/intTests/test_saw_submodule_access1/test_private.saw new file mode 100644 index 000000000..e43caf02b --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_private.saw @@ -0,0 +1,19 @@ +////////////////////////////////////////////// +// testing import: +import "H.cry" as HI; + +print (eval_int {{HI::a}}); // public, should succeed. +print (eval_int {{HI::b}}); // private, should succeed. + + +////////////////////////////////////////////// +// testing cryptol_load +HL <- cryptol_load "H.cry"; + +print HL; + +print (eval_int {{HL::a}}); // public, should succeed. +print (eval_int {{HL::b}}); // private, should succeed. + +do {x <- cryptol_extract HL "a"; print x;}; // public, should succeed. +do {x <- cryptol_extract HL "b"; print x;}; // private, should succeed. diff --git a/intTests/test_saw_submodule_access1/test_private_with_submodules.saw b/intTests/test_saw_submodule_access1/test_private_with_submodules.saw new file mode 100644 index 000000000..9c8e75e03 --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_private_with_submodules.saw @@ -0,0 +1,29 @@ +////////////////////////////////////////////// +// testing import: +import "HWithSubmodules.cry" as HI; + +print (eval_int {{HI::a}}); // public, should succeed. +print (eval_int {{HI::b}}); // private, should succeed. +print (eval_int {{HI::H2::c}}); // public, should succeed. +fails (do {print (eval_int {{ HI::H2::d }});}); // private, should succeed. + // + +////////////////////////////////////////////// +// testing cryptol_load +HL <- cryptol_load "HWithSubmodules.cry"; +print HL; + +print (eval_int {{HL::a}}); // public, should succeed. +print (eval_int {{HL::b}}); // private, should succeed. +print (eval_int {{HL::H2::c}}); // public, should succeed. + +fails (do {print (eval_int {{HL::H2::d}});}); // private, should succeed. + +do {x <- cryptol_extract HL "a"; print x;}; // public, should succeed. +do {x <- cryptol_extract HL "b"; print x;}; // private, should succeed. +do {x <- cryptol_extract HL "H2::c"; print x;}; // public, should succeed. +fails (do {x <- cryptol_extract HL "H2::d"; print x;}); // private, should succeed. + +// QUESTION: +// This does seem to 'match' what `cryptol` REPL does. +// What we want?