Skip to content

add SAWCoreCryptol module for converting SAWCore terms back into Cryptol #3230

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
danmatichuk wants to merge 12 commits into
base: master
Choose a base branch
from
Draft

add SAWCoreCryptol module for converting SAWCore terms back into Cryptol #3230

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
5e4425a
replace CrytolEnvStack with scopes within CryptolEnv
danmatichuk May 11, 2026
06d8891
add test for issue #3167
danmatichuk May 11, 2026
3c5b62c
refactor CryptolEnv into GlobalCryptolEnv and CryptolScope
danmatichuk May 14, 2026
97516aa
move global Cryptol environment into SharedContext metadata
danmatichuk May 22, 2026
1cb26de
replace implicit-param ?fileReader with context data
danmatichuk May 24, 2026
ad7c543
use restoreMetadata when re-initializing data
danmatichuk May 26, 2026
8241146
generalize liftModuleM
danmatichuk May 26, 2026
9e1653d
delete stale comment
danmatichuk May 27, 2026
2b6fceb
add SAWCoreCryptol module for converting SAWCore terms back into Cryptol
danmatichuk May 7, 2026
3949aa7
define 'withError' for GHC 9.4 compatibility
danmatichuk May 8, 2026
4aa52c6
SAWCoreCryptol: add caching and record support
danmatichuk Jun 2, 2026
69c3ff4
SAWCoreCryptol: drop redundant type annotations, support prefix ops
danmatichuk Jun 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions crucible-mir-comp/src/Mir/Compositional/State.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
module Mir.Compositional.State where

import Control.Monad(foldM)
import qualified Data.ByteString as BS
import Data.IORef
import Data.Set(Set)
import qualified Data.Set as Set
Expand Down Expand Up @@ -47,7 +46,6 @@ newMirState =
sc <- SAW.mkSharedContext
SAW.scLoadPreludeModule sc
SAW.scLoadCryptolModule sc
let ?fileReader = BS.readFile
env <- newIORef =<< SAW.initCryptolEnv sc
unintRef <- newIORef mempty
sawcoreState <- SAW.newSAWCoreState sc
Expand Down
6 changes: 2 additions & 4 deletions crux-mir-comp/src/Mir/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ where
import Control.Lens (use, (^.), (^?), to, ix)
import Control.Monad
import Control.Monad.IO.Class
import qualified Data.ByteString as BS
import Data.IORef
import qualified Data.Kind as Kind
import Data.String (fromString)
Expand Down Expand Up @@ -237,16 +236,15 @@ loadCryptolFunc col sig modulePath name = do
sym <- getSymInterface
let mirState = sym ^. W4.userState
let sc = mirSharedContext mirState
let ?fileReader = BS.readFile
ce <- liftIO (readIORef (mirCryEnv mirState))
let modName = Cry.textToModName modulePath
ce' <- liftIO $ SAW.importCryptolModule sc ce (Right modName) Nothing False 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)
(tt, ce'') <- liftIO $ SAW.parseTypedTerm sc ce' $
tt <- liftIO $ SAW.parseTypedTerm sc ce' $
SAW.InputText name "<string>" 1 1
liftIO (writeIORef (mirCryEnv mirState) ce'')
liftIO (writeIORef (mirCryEnv mirState) ce')

ppopts <- liftIO $ SAW.scGetPPOpts sc
args <-
Expand Down
Loading
Loading