Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update Heapster, Monadification, and MRSolver to handle high-order Sp…
…ecM functions (#2017) * wrote translateCompletePureFun * re-added translateCompleteFunPerm, with documentation reflecting the fact that it now generates a SpecDef type * added helper functions to SAWTranslation.hs to support IRTTranslation.hs * added the notion of pure vs impure type translations, to support IRTTranslation * added psubstOfSubst * added an OpenTermLike instance for OpenTerm itself * Finished rewriting IRTTranslation.hs * added one more import to HeapsterBuiltins.hs to get it to compile * fixed some variable-binding issues in the definition of defineSpecOpenTerm * added applyCallClos to the prelude * fixed translation code that was only applying closures to apply and call them * added the LRT_SpecM constructor to LRT output types * fixed the translation of the folding and unfolding functions for recursive shapes and permissions to use exprCtxPureTypeTerms for the arguments, to match their definitions * fixed importDefSpecTerm to turn the import into a SpecImp * changed all uses of the LetRecType eliminator to use the explicit eliminator * fixed permEnvAddGlobalSymFun to use a spec definition translation instead of a translation term * fixed up call to importDefSpecTerm to use its new def * removed old CompM Coq files from _CoqProject * Got all the Coq export stuff for the prelude working * changed Void to translate to the Empty_set type in the Coq standard library * removed SpecMExtra from the defaul list of imports in Coq files generated by Heapster * Changed the type-checker to *not* normalize argument types in lambdas and pis when they are type-checked, in order to make the Coq translation work in cases where these argument types have identifiers that translate to alternate Coq definitions * added the termIsClosed function to test if a SAW core term is closed * refactored the saw-core-coq translator so that all the local variable information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; also fixed #1927 * moved linked_list.sawcore to use the new SpecDef framework * replaced llvmZeroInitValue with a new function translateZeroInit that directly translates an LLVM zero initializer to a Heapster permission + SAW core term, so that we use repeatBVVec in the SAW term rather than a giant vector literal * updated mbox_proofs.v after changes to the Coq translator * renamed askTrr and localTrr to askTR and localTR * replaced a number of equality tests on the free variables of terms against emptyBitSet with the new termIsClosed function * replaced checkGroundTerm with the now standard termIsClosed function * whoops, fixed a few lingering bugs related to using termIsClosed * made a few fixes to make the code more readable * a few more tweaks to make the code look nicer * finished writing a comment on withSAWVar * indentation change requested by review * started defining type descriptions; removed the old IRT stuff * Defined tpElem and indElem * Updated the SAW core prelude with the new definition of SpecM based on TpDescs * renamed arithmetic kinds to expression kinds * fixed a comment; added Tp_BVVec * whoops, fixed the type of FixS * fix defaultMonTable entry for PZeroMSeq, add PZeroMSeqBool * add missing takeCryM and dropCryM defns, VWord cases in MRSolver/SMT.hs * allow Integer in monadifyType (for Cryptol prelude fns like abs, sext) * include info about the errorS in ReturnNotError * check whether assumptions and assertions are provable or not in mrRefines * fixed indentation * added the Sigmas type * Working on rewriting SAWTranslation.hs to work with the new definition of SpecM * Got the first portion of SAWTranslation.hs to compile with the new version of SpecM * updated the translation of the implication rules to work with the new SpecM monad * updated the translation of the EndLifetime rule * Started translating recursive and opaque shapes * updated the translations of shapes and permissions to also contain the translation of shapes and permissions to types, not just type descriptions; also updated the translation of shape expressions to generate this information * added explicit substitutions to type descriptions, for use in translating named type descriptions * updated the translation of Crucible expressions * updated the translation of jump targets and statements * whoops, just realized that lownedTransTerm needs to partially apply its function to the existing ps_extra * changed the MultiFixBodies type to a single function type over all the function indexes that returns a tuple of all the specFuns, instead of a tuple of functions over the function indexes * small tweak to the type of LetRecS * finished updating the translation of CFGs to the new SpecM monad * always unfold assumingS, assertingS in normComp * defined translateCFGs in the new SpecM monad * finished updating tcTranslateAddCFGs to the new SpecM * finished updating the remaining top-level entrypoints in SAWTranslation.hs * added the TranslateDescs instances for permissions and atomic permissions; define the translations for the folding and unfolding rules for recursive shapes and permissions * changed recursive permissions to have a body with a permission variable free, similar to how recursive shapes work * implemented translateCompleteFunType * removed the no longer needed IRTTranslation.hs file * started updating HeapsterBuiltins.hs to work with the new SpecM monad * Moved most of the details of adding and translating recursive permissions to SAWTranslation.hs * finished defining the heapster_define_recursive_shape in the new SpecM monad approach; updated the interpreter docs for the commands that have so far been updated * expanded the comments on SomePartialNamedShape * updated more of HeapsterBuiltins.hs to work with the new SpecM * finished updating SAW to the new SpecM monad! * added varKindExpr for use in translating descriptions from expression variables * fixed BV proofs to use the correct, non-monadic type to pass to the errorS combinator * bug fix: the type description for an existential permission needs to handle the special case of an equality permission in the body of the existential * implemented proveEqNat * added a Tp_M constructor to the output type of function descriptions; changed pis to lambdas for generated functions; changed constants to use the more general constKindExpr function * whoops, translateCallEntry should not pass in the top-level arguments as inputs * removed some unused arguments; made some small cosmetic changes * updated Coq translation to work with the new SpecM monad * updated CryptolM.sawcore to work with the new SpecM monad * redefined all the SpecM definitions in a new SpecM.v module in saw-core-coq, which now supplies the operations for type-level expressions * whoops, fixed the translation of function permissions to apply SpecM to the return type * whoops, re-added invariantHint * updated arrays.sawcore to the new SpecM * started working on a new arrays example for iteratively initializing arrays * whoops, forgot to add the type description argument to heapster_define_opaque_llvmshape in Interpreter.hs * whoops, was computing the type of the type function incorrectly in heapster_define_opaque_llvmshape * make atM, updateM cases of MRSolver more flexible * updating the rust_data example to work with the new SpecM monad, and also to contain a few lifetime examples * whoops, forgot to update the translation of the SImpl_ElimLLVMBlockNamed rule for defined shapes to accommodate the fact that shapes now translate to have 0 or more element instead of always just 1 * added helper definitions for writing type descriptions * more SAW translation bug fixes: made sure to add the Tp_M constructor for the return types of functional type descriptions; fixed some of the array types to reflect the fact that cell shapes can have 0 or more types instead of just 1 * re-enabled the ref_sum example in rust_data * added projTupleOpenTerm' to OpenTerm.hs * fixed the LLVM global translations in LLVMGlobalConst.hs to match the new translation of shapes as 0 or more types instead of a fixed 1 type * changed transTerms to have a monadic version for permissions * whoops, used pairTypeOpenTerm instead o9f pairOpenTerm in tupleOpenTerm' * whoops, forgot to add a SpecM to the output type of LambdaS * small bug fixes * whoops, messed up the translation of the SImpl_LLVMArrayCellReturn rule when converting to monadic transTermsM * bug fix in bindTransM to use lambdaTupleTransM; also added some FIXMEs for optimizing the translation of lifetimes * fixed projTupleOpenTerm' and its uses to be consistent * make MRSolver debug commands uniformly named * warn on Heapster implication failures * Changed tpElemEnv to no longer use function indices at all * moved SpecM and its related definitions to its own SAW core module * updated Heapster to use the new version of SpecM that does not use FunIxs and is contained in a separate SpecM SAW core module * whoops, forgot to update an identifier from the Prelude to the SpecM module * small bug fixes in the translation * updated Coq translation to work with the new definition of SpecM * more small bug fixes to the translation * bug fixes to get folding of inductive types to work properly * updated the arrays and linked_list examples to work with the new version of SpecM * whoops, tpElem needs to be applied to an event type * uncommented a bunch of the old rust_data functions, and got them working * changed translateCallEntry to not convert permissions to terms and then back again when it calls non-recursive entrypoints * moved the SpecM OpenTerm operations to OpenTerm.hs * add case for unset variable plus offset to proveEqH * make minor tweaks to refinement in MRSolver, errors in Heapster * started updating monadification to work with the new SpecM type * combined monadifyType and monadifyNum into a single monadifyTpExpr function; replaced the Either type used for type- vs term-level arguments with a new helper type MonArg * updated a bit more of Monadify.hs * mostly finished updating monadification, other than quantifying over event types * changed the EventType type to hold an arbitrary term, rather than just an identifier, in order to support event type polymorphism in monadification * added documentation for monadifyLambdas and monadifyEtaExpand * updated comments to remove SpecMParams * re-added an updated version of refinesS * updated MR solver to work with the new definition of SpecM * whoops, changed some identifiers from the Prelude to the new SpecM SAW core module; also made sure the SpecM and CryptolM modules are loaded when needed * updated a use of EvType from the Prelude to the SpecM SAW core module * whoops, forgot to monadify the bitvector type * updated monadify example to work with the new SpecM * whoops, forgot to update a number of SpecM identifiers to the new SpecM module * added a case to the MR solver normalizer to recognize LetRecS terms * whoops, updated two more identifiers to point to the new SpecM module * small bug fixes * updated SpecPrims to work with the new SpecM monad * fixed the printing for NormComp and friends to have the correct number of underscores for the new SpecM * removed the notion of an indescribable num expression, replacing it with just Num terms * reordered to arguments of Tp_Seq to match the definition of Vec, seq, and mseq * updated the SMT solver part of MR solver to use the new SpecM in the new SpecM SAW core module * whoops, updated mrGetInvariant to use the new version of assertFiniteS * whoops, fixed the argument order when constructing a Tp_BVVec * added support to MR solver for a new fixpoint operation forNatLtThenS that is defined by induction on Nat instead of via FixS; added MR solver reasoning about vector maps using forNatLtThenS * refactored the MaybeElim cases by defining a function asDecProp that checks if a proposition can be decided by MR solver * updated the MR solver normalizer to unfold forNatLtThenSBody when it applies that function to form the body of a forNatLtThenS corecursive function * added refinesS_eq combinator * finished updating arrays_mr_solver.saw example to work * updated mr_solver_unit_tests.saw example to work * add PPOpts to MREnv, make naming of P.P. fns. consistent (see PPInCtxM docs) * add mrsolver_set_debug_printing_depth * only check fn body, not arg values, when checking whether a fn is recursive * expand `FunBind |= FunBind` case to include all `FunName`s * add check for reflexivity in mrProveRel * improve error messages for `FunBind |= FunBind` case * add error handling for return types not being equal to refinementTermH * when applying a FunAssump, always substEvars in the rewritten RHS * have both arguments to mrLambdaLift2 be in the same context * added genBVVecNoPf and atBVVecNoPf primitives to the SAW core prelude * updated MR solver to use a more general notion of injective representation in place of the previously-used injective conversions; note that this change is not yet complete... * finished implementing injUnifyRepr * fixed lifting bug in mrApplyRepr * fixed mrTrySetAppliedEVar to correctly handle higher-order variables * changed genBVVecNoPf to use gen instead of genBVVec * changed the normalizer to prefer caller-supplied primitives over its default primitive implementations * updated implementations of the primitives to work directly with gen and at * fixed a lifting bug in generalizeCoIndHyp * commented out the no-longer used cases of instUVar * added evar lowering as part of mrProvable, to ensure evars over function variables do not become higher-order variables in SMT * whoops, forgot to lift the arg0 repr in generalizeCoIndHyp * added loop detection to proveCoIndHyp * added calls to mrIndexBVVec in the mrProveRelH for vectors, though mrIndexBVVec is not yet defined... * resolve all but one unused import and variable warnings * add mrAtBVVec, potentially finish BVVec case of mrProveRelH' * add `genBVVecNoPf` case to `asGenBVVecTerm` * add `mkInjReprType` to forall/exists cases of `mrRefines` * removed TermLike instance for tuples of length longer than 7 because those do not work with GHC 8.10 * Fixed vecLenIx to use mrAtVec and mrAtBVVec instead of directly applying the at and atBVVec accessors * changed heapster_init_env to add an import of the SpecM SAW core module instead of Prelude when it creates a SAW core module * updated the docs for heapster_define_reachability_perm * started updating mbox example to work with the new SpecM monad... * add case for `Vec const_n` back to Monadification * clean up MRSolver/SMT.hs * add special handling of constant-length vecs in VecLength, etc. * add scWhnf to mrFunOutType and do some minor cleanup * fix ConstNatVecLen case of mrVecLenGen * remove top-level type conversion check from mrProveRel * add a (albeit hacky) check for type equality back to refinementTermH * add mrNormOpenTerm before any calls to mrRefinesFunH or mkInjReprType * change "Prelude." to "SpecM.", remove unused OpenTerm code * only unfold main fun in warnErrs, unfold __bodies in print_fun_trans * added tuple shapes; changed the translation of memblock permissions to always be 0 or 1 terms, tupling what used to be multiple terms together; still need to update the translations of the implication rules for memblock permissions to work with this new translation * updated the translations of the memblock implication rules * added more debug info for translating LLVM globals * whoops, fixed the translation of sequence shapes where both sides have no empty translations * updated permEnvAddGlobalConst to fit with the new translation of memblock permissions to have 0 or 1 terms * added parsing support for tuple shapes * added an explicit tuple shape to the type of memcpy in rust_data.saw * fix type error in unsafeAssertMacro * attempting to get `take` to work property with MRSolver smtNorm * add VVec case to primGenVec, use iteWithProof instead of maybe * make the translation of `ETrans_Shape Nothing` be `unitTpDesc` * simplify types of assumingS/assertingS, add non-S versions, fix typo * resolve some unused import warnings * expand tuples for exists/forall evars, get arrays_mr_solver working again * handle SpecM fns in mrProveEq, clean up unused heterogeneity * minimize `sawLet`s and beta normalize in `heapster_print_fun_trans` * add Dilithium example * update pinned commit of entree-specs * fix Haddock in Heapster + MRSolver, fix typos found by @RyanGlScott * add more info about generating dilithium2.bc * add comments about dilithium commit sha * updated the commit number for the entree-specs repo * removed references to functions that are no longer used from unfold_bv_funs * removing unsafeAsserts from the definition of iteWithProof because the unsafeAssert Coq tactic is currently defined *after* the translation to Coq of the Prelude * changed the Coq translations of tcAdd and tcMul to be written by hand in SpecM.v instead of automatically generated * changed SpecM.v to rely on CryptolPrimitivesForSAWCore.v rather than the other way around, so that it can use the generated Num operations like tcAdd and tcMul * fixed up the imports for the heapster_export_coq command * added MR solver support for the iteWithProof combinator * changed all the examples to import SpecM instead of the SAW core Prelude * added checks to heapster_define_opaque_perm and heapster_define_opaque_llvmshape to make sure the user-supplied type and type description match * updated global_var example to work * added more info to the error message when a type does not match a type description * updated checkTypeAgreesWithDesc, since the previous version was incorrect * updated memcpy example to work with the new SpecM * updated ListDescType to the correct version to agree with ListDesc, now that Heapster checks that these agree * started updating the string_set example, but ended up commenting most of it out * commented out stuff that does not work in the Heapster examples for now * added an override for iteWithProof when calling into SMT * added tracing for terms being inserted by Heapster commands when the debug level is at least 2 * removed iso_recursive example, since it is now superseded by the linked_list example * whoops, forgot to remove the iso_recursive example from the _CoqProject * simplified memcpy permissions to help with translation * commented out all the _proofs.v files from the _CoqProject * updated rust_lifetimes example to work with the new SpecM * commented out the processBlocks function from the sha512 example because it currently has a panic * updated io example to work with the new SpecM --------- Co-authored-by: Eddy Westbrook <[email protected]>
- Loading branch information
