Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Monadified Cryptol-to-SAWCore translation (#1552)
* added more OpenTerm combinators, including: a "failure term"; getting the type of a term; and applying a pi type to an argument * added Monadify.hs * saving progress on monadification... * figured out how to monadify applications, but still working on lambdas... * finished a first version of monadification, ready for testing... * refactored monadifyInBinding and monadifyTermAndRun; wrote the top-level entrypoint monadifyTerm * added the monadify_term function to the interpreter * added bindTCMOpenTerm * changed monadification to work on plain old Terms rather than TypedSubsTerms * bug fix: when getting the type of a term in OpenTerm, need to use the current typing context * added support for datatypes and constructors in monadification * whoops, monadify_term should not call mkTypedTerm, but just use scTypeOf directly * added openOpenTerm * trying a different approach to monadification, where we make explicit MonType and MonKind data structures * added OpenTerm combinators for record terms * started writing monadifyTerm in the new monadification approach * added extCnsOpenTerm; also added a warning to bindTCMOpenTerm * finished the application cases of the new approach to monadification; updated the top-level entrypoint to be called monadify instead of monadifyTerm * tweaked monadifyApply to take in an ArgMonTerm instead of a MonTerm * switched to allowing pure terms at any type * added monadifyType case for Nums * added monadification macros in order to handle unsafeAssert; also added numAssertEqM as the monadified version of unsafeAssert applied to the Num type * changed monadification to treat primitives and definitions the same way * changed the top-level monadify call to take in the un-normalized type * added slightly different versions of tupleOpenTerm and tupleTypeOpenTerm match scTupleValue and scTupleType * added support for tuple and record projections, in two ways: changed MTyTuple to just MTyPair; and changed monadifyTerm to take an optional type, which allows monadification to do inference when there is a tuple or record selector and we do not have its whole type * added a case to monadify Eq types * whoops, was treating globally defined constants in the wrong way! * fixed the macro for unsafeAssert to return a computational instead of argument term; reorganized the "from" and "to" operations between monadification terms and OpenTerms to avoid these sorts of mistakes in the future * whoops, it is Cryptol.Num, not Prelude.Num * added bindPPOpenTerm, for error reporting * changed asTypedGlobalDef to not accidentally unfold constants; added more info to the error message in toPureTerm * added "monadified sequence" types mvec and mseq; added new versions of some of the Cryptol typeclasses to support these * completely removed the concept of pure terms, because they were not really correct anyway... * added monadification test case * updated some comments * added a process to monadify an entire cryptol environment * whoops, want to handle globals that are pure but do not require special-purpose macros * updating example a bit... * whoops, fixed an infinite loop when monadifying a non-lambda of functional type * attempting to monadify all the user-defined cryptol names, but that looks to be all of the cryptol prelude as well... * switched from an approach based on monadifying a CryptolEnv to a lazy / as-needed approach that just monadifies any constants that occur in a term * updated example for latest changes to monadification * slightly more sophistication in monadifying seq types * whoops, when monadifying constants, forgot to skip the constants we have already handled! * added a macro for if-then-else * moved the monadic versions of Cryptol primitives to a new module, CryptolM, and finished a lot more of them * whoops, wrong module name in the CryptolM module * condensed the multiple different sorts of mappings for monadifying primitives into a single list * added a few more examples to the monadification test * fixed spacing * got monadification working for non-mutual fixedpoints * added the set_monadification command * added existsM and forallM monadic combinators to the CompM monad * wrote Cryptol versions of the exists and forall specifications, along with some specifications derived from those combinators * rewrote all fixed-point monadic combinators to be written in terms of multiFixM * small updates to MR solver to add comments and make globals use arbitrary NameInfos so they can support monadified cryptol terms * added letRecM back as a primitive, and started trying to define the other fixed-point operations in terms of it (though that is still in progres...) * started rewriting MRSolver * added bitSetElems * wrote a simple verison of mrProveEq, using mrProveEqSimple * whoops, fixed small bugs in bitSetElems * added an instance of MonadTerm for any monad transformer * got an initial versio of mrProveEq to compile * rewrote the normalizer for MRSolver * added the ExtCns case to asTypedGlobalDef * wrote up the cases of the new mrRefines function, though it does not yet compile... * almost got mrRefines to compile * added a VarIndex to GlobalDef, to use as a sorting key * finished a complete version of the MRSolver module that at least compiles without warnings * added the top-level call to mr_solver * renamed the monadify examples directory to be called mr_solver * added a catch block to scCryptolType, so that panics in the simulator when trying to evaluate the type of an expression just turn into a lack of a Cryptol type rather than a top-level panic * whoops, fixed the type of the mr_solver interpreter command * MR Solver bug fixes: changed mrProvableRaw to use termToProp instead of boolToProp; changed askMRSolver to check convertibility of the types not of the terms themselves; and added an error case for refinement of evar computations, since we cannot yet handle evars as computations * changed the mr_solver command to return whether the proof succeeded * fixed mrProveEq to correctly compute the types of its inputs * removed calls to scEq, which only works on closed terms * added debug printing to mr_solver, and added the mr_solver_debug command to set the debug level * added mr_solver unit tests * added some noErrors proofs to our MR solver unit tests * changed the handling of recursive functions so that the bodies of recursive functions need to line up * changed GlobalDefs to contain an unfolded body for constants * added support for unfolding non-recursive functions * added unit tests for unfolding contstants * defined multiFixM in terms of letRecM * added a convertibility check to the default case of proveEq * added unfolding of non-recursive functions to mrRefines, and removed it from normalization * added compFunComp to simplify the composition of returns; added uniquifyName to give each uvar a distinct name; removed the case for FunBinds where we have the same function on both sides, since we do not want it to fire when we have, e.g., fixM on both sides * added a note to my future self * added some more MR solver tests * whoops, the previous merge added some operations to Prelude.sawcore twice * fixed a type error in CryptolM.sawcore introduced by the merge * updated Monadify.hs to work with merge * added the monadifyName function, to map the name of a constant to the name of its monadification * changed efq to specifically mention FalseProp, and added an efq1 to work on types in sort 1 * updated the cryptol monadification translation to have finite computational sequence (i.e., vectors) be strict, in order to make it easier to prove things about them * removed some debug printing * rn "<=" to "|=" in MRSolver.hs, improve MRS + monadification CLI output * fix test: mr_solver loop1 noErrorsRec1 * update SAWServer.hs with rwMonadify * prefixed unused symbols with underscores Co-authored-by: Matthew Yacavone <[email protected]>
- Loading branch information
