replace CryptolEnvStack with scopes within CryptolEnv by danmatichuk · Pull Request #3242 · GaloisInc/saw-script

danmatichuk · 2026-05-11T23:45:41Z

splits up the CryptolEnv datatype into GlobalCryptolEnv for globally-tracked Cryptol translation data, and CryptolEnv for data that's only relevant for scoping "extra" names (i.e. injected SAWScript values) needed for parsing Cryptol.

The GlobalCryptolEnv is stored as global metadata in the SharedContext, and only accessible indirectly via the functions in CryptolSAWCore.GlobalCryptolEnv. In the majority of cases, functions with the shape SharedContext -> CryptolEnv -> a -> IO (b, CryptolEnv) have been rewritten into SharedContext -> a -> IO b.

The previous CryptolEnvStack has been replaced by having CryptolEnv itself provide push/pop scope functions. Importantly, the data from GlobalCryptolEnv that was previously part of this stack is now unscoped. This is internally consistent because the names in the global environment are globally-unique (generated with unique nonces from the Cryptol module environment).

Although this reworks a large chunk of the Cryptol environment code, this change shouldn't affect any currently-working SAW scripts, but should resolve issues with SAWScript scopes capturing stale Cryptol environments.

fixes issue where restoring a checkpoint to before initialization would throw away data that would otherwise have been preserved

sauclovian-g

Some comments from a first run, mostly cosmetic stuff.

The basic approach seems sound.

sauclovian-g · 2026-06-03T03:51:13Z

+--   This is intended to be a write-once record of any work done
+--   during translation, analagous to the 'SharedContext' from
+---  SAWCore. Rather than directly accessing this environment,


Suggested change

-- This is intended to be a write-once record of any work done

-- during translation, analagous to the 'SharedContext' from

--- SAWCore. Rather than directly accessing this environment,

--

-- This is intended to be a write-once record of any work done

-- during translation, analogous to the 'SharedContext' from

-- SAWCore. Rather than directly accessing this environment,

(and similarly below and elsewhere, please put empty lines between comment paragraphs and include the initial -- in them so it's all one big comment (I'm not sure offhand if Haddock will collect or ignore following comment fragments, but I think it will probably ignore them and that's not what we want...))

sauclovian-g · 2026-06-03T03:51:41Z

+--   includes a scoped naming environment via 'CryptolScope'.
+
+
+--


Did you mean to keep the rest of this? Hopefully it's now out of date

(also some of it, like "There is now one environment type", is now wrong)

sauclovian-g · 2026-06-03T04:04:52Z

+  }
+
+-- | Initialize the global environment with the given 'ME.ModuleEnv',
+--   and populate the 'geAllVars' accordingly.


Suggested change

-- and populate the 'geAllVars' accordingly.

-- and populate the 'geAllVars' field accordingly.

sauclovian-g · 2026-06-03T04:07:45Z

+    let newMEnv = geModuleEnv chk
+        chkMEnv = geModuleEnv now


These names seem backwards...?

sauclovian-g · 2026-06-03T04:12:50Z

+  let env1 = pushScope env0
+  (a, env2) <- f env1
+  unless (sameHeight env1 env2) $
+    fail "withFreshScope: mismatched push/pops"


This should probably be a panic. There seems to be only one user, that doesn't abuse it.

sauclovian-g · 2026-06-03T05:49:10Z

+         let _cryenv = cc ^. jccCryptolEnv
+         ety_tm <- liftIO $ Cryptol.translateType sc ety


Suggested change

let _cryenv = cc ^. jccCryptolEnv

ety_tm <- liftIO $ Cryptol.translateType sc ety

ety_tm <- liftIO $ Cryptol.translateType sc ety

sauclovian-g · 2026-06-03T05:54:45Z

               -- NOTE: implementation of loadCryptolModule, now uses this default:
               --   defaultPrimitiveOptions = ImportPrimitiveOptions{allowUnknownPrimitives=True}
-  import_env <- refreshCryptolEnv env
+  let import_env = env


Can you remove this? The only thing that uses it downstream doesn't need it.

sauclovian-g · 2026-06-03T06:00:54Z

  CryptolModule ->
  IO (Either TranslationError [Rocq.Decl])
-translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) =
+translateCryptolModule sc _env configuration globalDecls (CryptolModule _ tm) =


Can you remove this one? It only has the one call site

sauclovian-g · 2026-06-03T06:04:45Z

-primEnviron :: Options -> BuiltinContext -> CryptolEnvStack -> Environ
-primEnviron opts bic cryenvs =
+primEnviron :: Options -> BuiltinContext -> CEnv.CryptolEnv -> Environ
+primEnviron opts bic env =


Suggested change

primEnviron opts bic env =

primEnviron opts bic cenv =

sauclovian-g · 2026-06-03T06:05:05Z

        varenv = ScopedMap.push $ ScopedMap.seed $ primValueEnv opts bic
    in
-    Environ varenv tyenv cryenvs
+    Environ varenv tyenv env


Suggested change

Environ varenv tyenv env

Environ varenv tyenv cenv

There are too many things just "env" could be...

danmatichuk requested a review from sauclovian-g May 11, 2026 23:45

danmatichuk force-pushed the cryptol-scopes branch 4 times, most recently from e1bde62 to 45e96ed Compare May 15, 2026 18:34

sauclovian-g changed the title ~~replace CrytolEnvStack with scopes within CryptolEnv~~ replace CryptolEnvStack with scopes within CryptolEnv May 15, 2026

danmatichuk force-pushed the cryptol-scopes branch 2 times, most recently from dbf2a17 to dfc303c Compare May 22, 2026 23:27

danmatichuk force-pushed the cryptol-scopes branch from 8beef55 to 4c575af Compare May 26, 2026 23:56

danmatichuk requested a review from brianhuffman June 1, 2026 21:00

danmatichuk added 8 commits June 1, 2026 15:08

replace CrytolEnvStack with scopes within CryptolEnv

5e4425a

add test for issue #3167

06d8891

refactor CryptolEnv into GlobalCryptolEnv and CryptolScope

3c5b62c

move global Cryptol environment into SharedContext metadata

97516aa

replace implicit-param ?fileReader with context data

1cb26de

use restoreMetadata when re-initializing data

ad7c543

fixes issue where restoring a checkpoint to before initialization would throw away data that would otherwise have been preserved

generalize liftModuleM

8241146

delete stale comment

9e1653d

danmatichuk force-pushed the cryptol-scopes branch from 350fb67 to 9e1653d Compare June 1, 2026 22:08

sauclovian-g reviewed Jun 3, 2026

View reviewed changes

danmatichuk added 2 commits June 5, 2026 17:55

move context-based 'FileReader' into own module

db54907

don't export setModuleEnv, move and rename liftModuleM

c96987a

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

replace CryptolEnvStack with scopes within CryptolEnv#3242

replace CryptolEnvStack with scopes within CryptolEnv#3242
danmatichuk wants to merge 10 commits into
masterfrom
cryptol-scopes

danmatichuk commented May 11, 2026 •

edited

Loading

Uh oh!

sauclovian-g left a comment

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

sauclovian-g Jun 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		-- includes a scoped naming environment via 'CryptolScope'.


		--

	-- and populate the 'geAllVars' accordingly.
	-- and populate the 'geAllVars' field accordingly.

		let _cryenv = cc ^. jccCryptolEnv
		ety_tm <- liftIO $ Cryptol.translateType sc ety

Uh oh!

Conversation

danmatichuk commented May 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sauclovian-g left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

danmatichuk commented May 11, 2026 •

edited

Loading