Skip to content
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

Monadified Cryptol-to-SAWCore translation #1552

Merged
merged 104 commits into from
Feb 7, 2022
Merged

Monadified Cryptol-to-SAWCore translation #1552

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
104 commits
Select commit Hold shift + click to select a range
6b3c6a2
added more OpenTerm combinators, including: a "failure term"; getting…
Jul 7, 2021
1eadf8b
added Monadify.hs
Jul 7, 2021
ffb1dcb
saving progress on monadification...
Jul 8, 2021
359b05e
figured out how to monadify applications, but still working on lambda…
Jul 13, 2021
8ce3cfe
finished a first version of monadification, ready for testing...
Jul 13, 2021
f6f87a6
refactored monadifyInBinding and monadifyTermAndRun; wrote the top-le…
Jul 14, 2021
7ea9b5a
added the monadify_term function to the interpreter
Jul 14, 2021
de31405
added bindTCMOpenTerm
Jul 15, 2021
7fdbe29
changed monadification to work on plain old Terms rather than TypedSu…
Jul 15, 2021
83a9873
bug fix: when getting the type of a term in OpenTerm, need to use the…
Jul 15, 2021
5d9a64f
added support for datatypes and constructors in monadification
Jul 15, 2021
667ca9c
whoops, monadify_term should not call mkTypedTerm, but just use scTyp…
Jul 15, 2021
cb8eac6
added openOpenTerm
Jul 16, 2021
cccce09
trying a different approach to monadification, where we make explicit…
Jul 16, 2021
399ddb0
added OpenTerm combinators for record terms
Jul 16, 2021
9e8efdf
started writing monadifyTerm in the new monadification approach
Jul 17, 2021
4b19d22
added extCnsOpenTerm; also added a warning to bindTCMOpenTerm
Jul 18, 2021
b7b27d8
finished the application cases of the new approach to monadification;…
Jul 18, 2021
5725209
tweaked monadifyApply to take in an ArgMonTerm instead of a MonTerm
Jul 18, 2021
8a9e4ab
switched to allowing pure terms at any type
Jul 19, 2021
a384c31
added monadifyType case for Nums
Jul 19, 2021
fb4b708
added monadification macros in order to handle unsafeAssert; also add…
Jul 19, 2021
5d278e1
changed monadification to treat primitives and definitions the same way
Jul 19, 2021
b1c5256
changed the top-level monadify call to take in the un-normalized type
Jul 20, 2021
fa95365
added slightly different versions of tupleOpenTerm and tupleTypeOpenT…
Jul 20, 2021
2d7f140
added support for tuple and record projections, in two ways: changed …
Jul 20, 2021
549e2f3
added a case to monadify Eq types
Jul 20, 2021
4f84431
whoops, was treating globally defined constants in the wrong way!
Jul 20, 2021
2d56f2c
fixed the macro for unsafeAssert to return a computational instead of…
Jul 22, 2021
3189bcf
whoops, it is Cryptol.Num, not Prelude.Num
Jul 22, 2021
6063a12
added bindPPOpenTerm, for error reporting
Jul 22, 2021
e38e971
changed asTypedGlobalDef to not accidentally unfold constants; added …
Jul 22, 2021
74780be
added "monadified sequence" types mvec and mseq; added new versions o…
Jul 26, 2021
394f744
completely removed the concept of pure terms, because they were not r…
Jul 26, 2021
a890e9f
added monadification test case
Jul 26, 2021
9f5c359
updated some comments
Aug 11, 2021
f60e68b
added a process to monadify an entire cryptol environment
Aug 13, 2021
f716b2d
whoops, want to handle globals that are pure but do not require speci…
Aug 13, 2021
e892c92
updating example a bit...
Aug 13, 2021
1509a5e
whoops, fixed an infinite loop when monadifying a non-lambda of funct…
Aug 13, 2021
8ba6285
attempting to monadify all the user-defined cryptol names, but that l…
Aug 13, 2021
0c1e98c
switched from an approach based on monadifying a CryptolEnv to a lazy…
Aug 13, 2021
6212889
updated example for latest changes to monadification
Aug 13, 2021
2a7ad72
slightly more sophistication in monadifying seq types
Aug 13, 2021
1453141
whoops, when monadifying constants, forgot to skip the constants we h…
Aug 13, 2021
1d1740a
added a macro for if-then-else
Aug 14, 2021
bdf6ec3
moved the monadic versions of Cryptol primitives to a new module, Cry…
Aug 18, 2021
bcf30a4
whoops, wrong module name in the CryptolM module
Aug 18, 2021
a3380ac
condensed the multiple different sorts of mappings for monadifying pr…
Aug 19, 2021
1f750ec
added a few more examples to the monadification test
Aug 19, 2021
c2060e4
fixed spacing
Aug 19, 2021
03cb065
got monadification working for non-mutual fixedpoints
Aug 19, 2021
428ed0c
added the set_monadification command
Aug 25, 2021
9c59f79
added existsM and forallM monadic combinators to the CompM monad
Aug 25, 2021
4a1191f
wrote Cryptol versions of the exists and forall specifications, along…
Aug 26, 2021
655f029
rewrote all fixed-point monadic combinators to be written in terms of…
Aug 26, 2021
c125284
small updates to MR solver to add comments and make globals use arbit…
Aug 27, 2021
5c3f7df
added letRecM back as a primitive, and started trying to define the o…
Oct 6, 2021
d7a36cd
started rewriting MRSolver
Oct 6, 2021
3cbd954
added bitSetElems
Oct 7, 2021
0d58184
wrote a simple verison of mrProveEq, using mrProveEqSimple
Oct 7, 2021
f9593de
whoops, fixed small bugs in bitSetElems
Oct 8, 2021
5db0dba
added an instance of MonadTerm for any monad transformer
Oct 8, 2021
f5fb97d
got an initial versio of mrProveEq to compile
Oct 8, 2021
914e752
rewrote the normalizer for MRSolver
Oct 8, 2021
ab6f761
added the ExtCns case to asTypedGlobalDef
Oct 11, 2021
380b589
wrote up the cases of the new mrRefines function, though it does not …
Oct 11, 2021
06c87a9
almost got mrRefines to compile
Oct 12, 2021
f090389
added a VarIndex to GlobalDef, to use as a sorting key
Oct 12, 2021
00d03f9
finished a complete version of the MRSolver module that at least comp…
Oct 12, 2021
208207a
added the top-level call to mr_solver
Oct 12, 2021
0d3e3f4
renamed the monadify examples directory to be called mr_solver
Oct 13, 2021
7439ed4
added a catch block to scCryptolType, so that panics in the simulator…
Oct 13, 2021
6083153
whoops, fixed the type of the mr_solver interpreter command
Oct 13, 2021
d8353c2
MR Solver bug fixes: changed mrProvableRaw to use termToProp instead …
Oct 13, 2021
75cbc45
changed the mr_solver command to return whether the proof succeeded
Oct 13, 2021
9fe4efb
fixed mrProveEq to correctly compute the types of its inputs
Oct 13, 2021
c7a6b84
removed calls to scEq, which only works on closed terms
Oct 13, 2021
89134da
added debug printing to mr_solver, and added the mr_solver_debug comm…
Oct 13, 2021
4c83ba7
added mr_solver unit tests
Oct 13, 2021
f6b34a3
added some noErrors proofs to our MR solver unit tests
Oct 14, 2021
ddc5208
changed the handling of recursive functions so that the bodies of rec…
Oct 14, 2021
6844092
changed GlobalDefs to contain an unfolded body for constants
Oct 14, 2021
593ac5e
added support for unfolding non-recursive functions
Oct 14, 2021
643a816
added unit tests for unfolding contstants
Oct 14, 2021
33e3dcb
defined multiFixM in terms of letRecM
Oct 15, 2021
0e2799f
added a convertibility check to the default case of proveEq
Oct 15, 2021
c8be70d
added unfolding of non-recursive functions to mrRefines, and removed …
Oct 15, 2021
9dd26a1
added compFunComp to simplify the composition of returns; added uniqu…
Oct 16, 2021
bccff0b
added a note to my future self
Nov 4, 2021
57a37c7
added some more MR solver tests
Nov 4, 2021
9f05f56
Merge remote-tracking branch 'origin/master' into feature/monadification
Jan 21, 2022
23ba285
whoops, the previous merge added some operations to Prelude.sawcore t…
Jan 21, 2022
6f24d06
fixed a type error in CryptolM.sawcore introduced by the merge
Jan 21, 2022
4488998
updated Monadify.hs to work with merge
Jan 21, 2022
7126366
added the monadifyName function, to map the name of a constant to the…
Jan 22, 2022
67c2663
changed efq to specifically mention FalseProp, and added an efq1 to w…
Jan 23, 2022
949564b
updated the cryptol monadification translation to have finite computa…
Jan 23, 2022
432c940
removed some debug printing
Jan 23, 2022
db0eff5
rn "<=" to "|=" in MRSolver.hs, improve MRS + monadification CLI output
m-yac Feb 5, 2022
a7df8c0
fix test: mr_solver loop1 noErrorsRec1
m-yac Feb 5, 2022
e134e9a
Merge branch 'master' into feature/monadification
m-yac Feb 5, 2022
409b39c
update SAWServer.hs with rwMonadify
m-yac Feb 5, 2022
095c83b
prefixed unused symbols with underscores
Feb 7, 2022
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
3 changes: 3 additions & 0 deletions cryptol-saw-core/cryptol-saw-core.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ library
data-inttrie >= 0.1.4,
integer-gmp,
modern-uri,
mtl,
panic,
saw-core,
saw-core-aig,
Expand All @@ -44,7 +45,9 @@ library
Verifier.SAW.Cryptol
Verifier.SAW.Cryptol.Panic
Verifier.SAW.Cryptol.Prelude
Verifier.SAW.Cryptol.PreludeM
Verifier.SAW.Cryptol.Simpset
Verifier.SAW.Cryptol.Monadify
Verifier.SAW.CryptolEnv
Verifier.SAW.TypedTerm
GHC-options: -Wall -Werror
Expand Down
2 changes: 0 additions & 2 deletions cryptol-saw-core/saw/Cryptol.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1886,5 +1886,3 @@ axiom demote_add_distr
(ecNumber (tcAdd x y) (TCNum w))
(bvAdd w (ecNumber x (TCNum w)) (ecNumber y (TCNum w)));
-}

--------------------------------------------------------------------------------
Loading