Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Cryptol/pr1136 #200

Closed
wants to merge 9 commits into from
Closed

Cryptol/pr1136 #200

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
4c6b436
Adapt to GaloisInc/cryptol#1128 "persistent-solver2".
Apr 8, 2021
ad96185
Remove obsolete code
robdockins Mar 17, 2021
9b64193
Fix corner case in `cryptolTypeOfFirstOrderType`
robdockins Mar 17, 2021
a74984d
Communicate counterexamples values via `ExtCns` instead of `String`.
robdockins Mar 17, 2021
ffed23f
Put more things in `Prop`.
robdockins Mar 18, 2021
ea58738
Do the right thing when encountering 0 width bitvectors in the What4 …
robdockins Apr 6, 2021
24f6478
Update `cryptol-saw-core` to track Cryptol changes.
robdockins Apr 15, 2021
2193614
Replace the old `splitAt` primitive with separate `take` and `drop` p…
robdockins Apr 15, 2021
eee8543
Use the newly-exposed `defaultSolverConfig`
robdockins Apr 16, 2021
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
6 changes: 3 additions & 3 deletions cryptol-saw-core/css/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ import Cryptol.Utils.Logger (quietLogger)
import qualified Verifier.SAW.Cryptol as C
import Verifier.SAW.SharedTerm
import qualified Verifier.SAW.Cryptol.Prelude as C
import Verifier.SAW.CryptolEnv (schemaNoUser)
import Verifier.SAW.CryptolEnv (schemaNoUser, meSolverConfig)


import qualified Data.ABC as ABC
Expand Down Expand Up @@ -92,7 +92,7 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do
modEnv <- CM.initialModuleEnv
let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
(e,warn) <-
SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
SMT.withSolver (meSolverConfig modEnv) $ \s ->
CM.loadModuleByPath inputModule (minp s)
mapM_ (print . pp) warn
case e of
Expand Down Expand Up @@ -133,7 +133,7 @@ extractCryptol sc modEnv input = do
Right x -> return x
let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
(exprResult, exprWarnings) <-
SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
SMT.withSolver (meSolverConfig modEnv) $ \s ->
CM.checkExpr pexpr (minp s)
mapM_ (print . pp) exprWarnings
((_, expr, schema), _modEnv') <-
Expand Down
37 changes: 26 additions & 11 deletions cryptol-saw-core/saw/Cryptol.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1208,22 +1208,37 @@ ecCat =
-- Case for (TCNum m, TCInf)
(\ (a:sort 0) -> streamAppend a m));

ecSplitAt : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a ->
#(seq m a, seq n a);
ecSplitAt =
ecTake : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq m a;
ecTake =
Num_rec
(\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq m a)

(\ (m:Nat) ->
Num_rec
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> Vec m a)
-- The case (TCNum m, TCNum n)
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> take a m n xs)
-- The case (TCNum m, infinity)
(\ (a:sort 0) -> \ (xs: Stream a) -> streamTake a m xs))

(Num_rec
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a)
-- The case (TCInf, TCNum n)
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
-- The case (TCInf, TCInf)
(\ (a:sort 0) -> \ (xs:Stream a) -> xs));

ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a;
ecDrop =
finNumRec
(\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a ->
#(seq m a, seq n a))
(\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq n a)
(\ (m:Nat) ->
Num_rec
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a ->
#(Vec m a, seq n a))
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a)
-- The case (TCNum n, TCNum m)
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) ->
(take a m n xs, drop a m n xs))
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs)
-- The case (TCNum m, infinity)
(\ (a:sort 0) -> \ (xs: Stream a) ->
(streamTake a m xs, streamDrop a m xs)));
(\ (a:sort 0) -> \ (xs: Stream a) -> streamDrop a m xs));

ecJoin : (m n : Num) -> (a : sort 0) -> seq m (seq n a) -> seq (tcMul m n) a;
ecJoin m =
Expand Down
83 changes: 46 additions & 37 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@ import Text.URI

import qualified Cryptol.Eval.Type as TV
import qualified Cryptol.Backend.Monad as V
import qualified Cryptol.Backend.SeqMap as V
import qualified Cryptol.Backend.WordValue as V
import qualified Cryptol.Eval.Value as V
import qualified Cryptol.Eval.Concrete as V
import Cryptol.Eval.Type (evalValType)
Expand All @@ -45,6 +47,7 @@ import qualified Cryptol.ModuleSystem.Name as C
import qualified Cryptol.Utils.Ident as C
( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim
, ModName, modNameToText, identText, interactiveName
, ModPath(..), modPathSplit
)
import qualified Cryptol.Utils.RecordMap as C
import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
Expand Down Expand Up @@ -740,7 +743,8 @@ prelPrims =

-- -- Sequences primitives
, ("#", flip scGlobalDef "Cryptol.ecCat") -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
, ("splitAt", flip scGlobalDef "Cryptol.ecSplitAt") -- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c)
, ("take", flip scGlobalDef "Cryptol.ecTake") -- {front, back, a} [front + back]a -> [front]a
, ("drop", flip scGlobalDef "Cryptol.ecDrop") -- {front, back, a} (fin front) => [front + back]a -> [back]a
, ("join", flip scGlobalDef "Cryptol.ecJoin") -- {a,b,c} (fin b) => [a][b]c -> [a * b]c
, ("split", flip scGlobalDef "Cryptol.ecSplit") -- {a,b,c} (fin b) => [a * b] c -> [a][b] c
, ("reverse", flip scGlobalDef "Cryptol.ecReverse") -- {a,b} (fin a) => [a] b -> [a] b
Expand Down Expand Up @@ -1231,18 +1235,20 @@ importName cnm =
case C.nameInfo cnm of
C.Parameter -> fail ("Cannot import non-top-level name: " ++ show cnm)
C.Declared modNm _
| modNm == C.interactiveName ->
| modNm == C.TopModule C.interactiveName ->
let shortNm = C.identText (C.nameIdent cnm)
aliases = [shortNm]
uri = cryptolURI [shortNm] (Just (C.nameUnique cnm))
in pure (ImportedName uri aliases)

| otherwise ->
let modNmTxt = C.modNameToText modNm
modNms = Text.splitOn "::" modNmTxt
shortNm = C.identText (C.nameIdent cnm)
aliases = [shortNm, modNmTxt <> "::" <> shortNm]
uri = cryptolURI (modNms ++ [shortNm]) Nothing
let (topMod, nested) = C.modPathSplit modNm
modNmTxt = C.modNameToText topMod
modNms = (Text.splitOn "::" modNmTxt) ++ map C.identText nested
shortNm = C.identText (C.nameIdent cnm)
longNm = Text.intercalate "::" ([modNmTxt] ++ map C.identText nested ++ [shortNm])
aliases = [shortNm, longNm]
uri = cryptolURI (modNms ++ [shortNm]) Nothing
in pure (ImportedName uri aliases)

-- | Currently this imports declaration groups by inlining all the
Expand Down Expand Up @@ -1639,22 +1645,22 @@ scCryptolEq sc x y =

-- | Convert from SAWCore's Value type to Cryptol's, guided by the
-- Cryptol type schema.
exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value
exportValueWithSchema :: C.Schema -> SC.CValue -> V.Eval V.Value
exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v
exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema")
exportValueWithSchema _ _ = pure (V.VPoly mempty (error "exportValueWithSchema"))
-- TODO: proper support for polymorphic values

exportValue :: TV.TValue -> SC.CValue -> V.Value
exportValue :: TV.TValue -> SC.CValue -> V.Eval V.Value
exportValue ty v = case ty of

TV.TVBit ->
V.VBit (SC.toBool v)
pure (V.VBit (SC.toBool v))

TV.TVInteger ->
V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")
pure (V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer"))

TV.TVIntMod _modulus ->
V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")
pure (V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod"))

TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")"

Expand All @@ -1666,28 +1672,29 @@ exportValue ty v = case ty of
case v of
SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w)
SC.VVector xs
| TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs))
(V.finiteSeqMap . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)))
| otherwise -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $
map (V.ready . exportValue e . SC.runIdentity . force) $ Vector.toList xs
| TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) <$>
V.bitmapWordVal V.Concrete (toInteger (Vector.length xs))
(V.finiteSeqMap V.Concrete . map (V.ready . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)
| otherwise -> pure . V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $
map (\x -> exportValue e (SC.runIdentity (force x))) (Vector.toList xs)
_ -> error $ "exportValue (on seq type " ++ show ty ++ ")"

-- infinite streams
TV.TVStream e ->
case v of
SC.VExtra (SC.CStream trie) -> V.VStream (V.IndexSeqMap $ \i -> V.ready $ exportValue e (IntTrie.apply trie i))
SC.VExtra (SC.CStream trie) -> pure $ V.VStream (V.indexSeqMap $ \i -> exportValue e (IntTrie.apply trie i))
_ -> error $ "exportValue (on seq type " ++ show ty ++ ")"

-- tuples
TV.TVTuple etys -> V.VTuple (exportTupleValue etys v)
TV.TVTuple etys -> pure $ V.VTuple $ exportTupleValue etys v

-- records
TV.TVRec fields ->
V.VRecord (C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v)
pure . V.VRecord . C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v

-- functions
TV.TVFun _aty _bty ->
V.VFun mempty (error "exportValue: TODO functions")
pure $ V.VFun mempty (error "exportValue: TODO functions")

-- abstract types
TV.TVAbstract{} ->
Expand All @@ -1702,8 +1709,8 @@ exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value]
exportTupleValue tys v =
case (tys, v) of
([] , SC.VUnit ) -> []
([t] , _ ) -> [V.ready $ exportValue t v]
(t : ts, SC.VPair x y) -> (V.ready $ exportValue t (run x)) : exportTupleValue ts (run y)
([t] , _ ) -> [exportValue t v]
(t : ts, SC.VPair x y) -> (exportValue t (run x)) : exportTupleValue ts (run y)
_ -> error $ "exportValue: expected tuple"
where
run = SC.runIdentity . force
Expand All @@ -1712,12 +1719,11 @@ exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> [(C.Ident, V.Eval V.
exportRecordValue fields v =
case (fields, v) of
([] , SC.VUnit ) -> []
([(n, t)] , _ ) -> [(n, V.ready $ exportValue t v)]
((n, t) : ts, SC.VPair x y) ->
(n, V.ready $ exportValue t (run x)) : exportRecordValue ts (run y)
([(n, t)] , _ ) -> [(n, exportValue t v)]
((n, t) : ts, SC.VPair x y) -> (n, exportValue t (run x)) : exportRecordValue ts (run y)
(_, SC.VRecordValue (alistAllFields
(map (C.identText . fst) fields) -> Just ths)) ->
zipWith (\(n,t) x -> (n, V.ready $ exportValue t (run x))) fields ths
zipWith (\(n,t) x -> (n, exportValue t (run x))) fields ths
_ -> error $ "exportValue: expected record"
where
run = SC.runIdentity . force
Expand All @@ -1726,20 +1732,23 @@ fvAsBool :: FirstOrderValue -> Bool
fvAsBool (FOVBit b) = b
fvAsBool _ = error "fvAsBool: expected FOVBit value"

exportFirstOrderValue :: FirstOrderValue -> V.Value
exportFirstOrderValue :: FirstOrderValue -> V.Eval V.Value
exportFirstOrderValue fv =
case fv of
FOVBit b -> V.VBit b
FOVInt i -> V.VInteger i
FOVIntMod _ i -> V.VInteger i
FOVWord w x -> V.word V.Concrete (toInteger w) x
FOVBit b -> pure (V.VBit b)
FOVInt i -> pure (V.VInteger i)
FOVIntMod _ i -> pure (V.VInteger i)
FOVWord w x -> V.word V.Concrete (toInteger w) x
FOVVec t vs
| t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap . map (V.ready . V.VBit . fvAsBool) $ vs)))
| otherwise -> V.VSeq len (V.finiteSeqMap (map (V.ready . exportFirstOrderValue) vs))
| t == FOTBit -> V.VWord len <$> (V.bitmapWordVal V.Concrete len
(V.finiteSeqMap V.Concrete . map (V.ready . fvAsBool) $ vs))
| otherwise -> pure (V.VSeq len (V.finiteSeqMap V.Concrete (map exportFirstOrderValue vs)))
where len = toInteger (length vs)
FOVArray{} -> error $ "exportFirstOrderValue: unsupported FOT Array"
FOVTuple vs -> V.VTuple (map (V.ready . exportFirstOrderValue) vs)
FOVRec vm -> V.VRecord $ C.recordFromFields [ (C.mkIdent n, V.ready $ exportFirstOrderValue v) | (n, v) <- Map.assocs vm ]
FOVTuple vs -> pure $ V.VTuple $ map exportFirstOrderValue vs
FOVRec vm ->
do let vm' = fmap exportFirstOrderValue vm
pure $ V.VRecord $ C.recordFromFields [ (C.mkIdent n, v) | (n, v) <- Map.assocs vm' ]

importFirstOrderValue :: FirstOrderType -> V.Value -> IO FirstOrderValue
importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
Expand All @@ -1748,7 +1757,7 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
go t v = case (t,v) of
(FOTBit , V.VBit b) -> return (FOVBit b)
(FOTInt , V.VInteger i) -> return (FOVInt i)
(FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete =<< wv)
(FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete wv)
(FOTVec _ ty , V.VSeq len xs) -> FOVVec ty <$> traverse (go ty =<<) (V.enumerateSeqMap len xs)
(FOTTuple tys , V.VTuple xs) -> FOVTuple <$> traverse (\(ty, x) -> go ty =<< x) (zip tys xs)
(FOTRec fs , V.VRecord xs) ->
Expand Down
30 changes: 14 additions & 16 deletions cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ module Verifier.SAW.CryptolEnv
, InputText(..)
, lookupIn
, resolveIdentifier
, meSolverConfig
)
where

Expand Down Expand Up @@ -152,7 +153,7 @@ nameMatcher xs =
case modNameChunks (textToModName (pack xs)) of
[] -> const False
[x] -> (packIdent x ==) . MN.nameIdent
cs -> let m = MN.Declared (packModName (map pack (init cs))) MN.UserName
cs -> let m = MN.Declared (C.TopModule (packModName (map pack (init cs)))) MN.UserName
i = packIdent (last cs)
in \n -> MN.nameIdent n == i && MN.nameInfo n == m

Expand Down Expand Up @@ -252,7 +253,7 @@ getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv
syms = case vis of
OnlyPublic -> MI.ifPublic ifc
PublicAndPrivate -> MI.ifPublic ifc `mappend` M.ifPrivate ifc
return $ MN.interpImport i syms
return $ MN.interpImportIface i syms

getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls
getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me)))
Expand Down Expand Up @@ -363,13 +364,13 @@ loadCryptolModule sc env path = do
newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups
newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)

let names = MEx.eBinds (T.mExports m) -- :: Set T.Name
let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
let tm' = Map.filterWithKey (\k _ -> Set.member k names) $
Map.intersectionWith TypedTerm types newTermEnv
let env' = env { eModuleEnv = modEnv''
, eTermEnv = newTermEnv
}
let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.eTypes (T.mExports m))) (T.mTySyns m)
let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) (T.mTySyns m)
return (CryptolModule sm' tm', env')

bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv
Expand Down Expand Up @@ -429,7 +430,7 @@ bindIdent ident env = (name, env')
modEnv = eModuleEnv env
supply = ME.meSupply modEnv
fixity = Nothing
(name, supply') = MN.mkDeclared interactiveName MN.UserName ident fixity P.emptyRange supply
(name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply
modEnv' = modEnv { ME.meSupply = supply' }
env' = env { eModuleEnv = modEnv' }

Expand Down Expand Up @@ -466,6 +467,9 @@ bindInteger (ident, n) env =

--------------------------------------------------------------------------------

meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig
meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)

resolveIdentifier ::
(?fileReader :: FilePath -> IO ByteString) =>
CryptolEnv -> Text -> IO (Maybe T.Name)
Expand All @@ -480,10 +484,10 @@ resolveIdentifier env nm =
nameEnv = getNamingEnv env

doResolve pnm =
SMT.withSolver (ME.meSolverConfig modEnv) $ \s ->
SMT.withSolver (meSolverConfig modEnv) $ \s ->
do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
(res, _ws) <- MM.runModuleM (minp s) $
MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm))
MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm))
case res of
Left _ -> pure Nothing
Right (x,_) -> pure (Just x)
Expand Down Expand Up @@ -544,18 +548,12 @@ parseDecls sc env input = do
-- Convert from 'Decl' to 'TopDecl' so that types will be generalized
let topdecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npdecls ]

-- Label each TopDecl with the "interactive" module for unique name generation
let (mdecls :: [MN.InModule (P.TopDecl P.PName)]) = map (MN.InModule interactiveName) topdecls
nameEnv1 <- MN.liftSupply (MN.namingEnv' mdecls)

-- Resolve names
let nameEnv = nameEnv1 `MR.shadowing` getNamingEnv env
(rdecls :: [P.TopDecl T.Name]) <- MM.interactive (MB.rename interactiveName nameEnv (traverse MR.rename topdecls))
(_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@robdockins I am not really sure, but perhaps there is a problem here. Note that in the old code the naming environment in which we do the resolving already has the names added to it, while in the new one it does not...

Otoh, I don't understand why the old code was doing that in the first place, and what you've replaced it with makes sense to me, so perhaps the problem is not here.

To be more help, I should probably just check out the code and run it, ping me on the chat if that'd be useful.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wondered about this code too, but I think it's unrelated, actually. I think this code is for dealing with declarations appearing inside the {{ ... }} delimiters in SAWScript. The code for importing modules is further above, and is barely changed.


-- Create a Module to contain the declarations
let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName
, P.mInstance = Nothing
, P.mImports = []
, P.mDecls = rdecls
}

Expand Down Expand Up @@ -623,7 +621,7 @@ declareName env mname input = do
let modEnv = eModuleEnv env
(cname, modEnv') <-
liftModuleM modEnv $ MM.interactive $
MN.liftSupply (MN.mkDeclared mname MN.UserName (P.getIdent pname) Nothing P.emptyRange)
MN.liftSupply (MN.mkDeclared C.NSValue (C.TopModule mname) MN.UserName (P.getIdent pname) Nothing P.emptyRange)
let env' = env { eModuleEnv = modEnv' }
return (cname, env')

Expand All @@ -646,7 +644,7 @@ liftModuleM ::
ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv)
liftModuleM env m =
do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env
SMT.withSolver (ME.meSolverConfig env) $ \s ->
SMT.withSolver (meSolverConfig env) $ \s ->
MM.runModuleM (minp s) m >>= moduleCmdResult

defaultEvalOpts :: E.EvalOpts
Expand Down
2 changes: 2 additions & 0 deletions cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,8 @@ cryptolTypeOfFirstOrderType fot =
FOTInt -> C.tInteger
FOTIntMod n -> C.tIntMod (C.tNum n)
FOTVec n t -> C.tSeq (C.tNum n) (cryptolTypeOfFirstOrderType t)
-- NB, special case, don't produce 1-tuples
FOTTuple [x] -> cryptolTypeOfFirstOrderType x
FOTTuple ts -> C.tTuple (map cryptolTypeOfFirstOrderType ts)
FOTArray a b ->
C.tArray
Expand Down
Loading