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

Update Heapster, Monadification, and MRSolver to handle high-order SpecM functions #2017

Merged
merged 316 commits into from
Feb 9, 2024
Merged

Update Heapster, Monadification, and MRSolver to handle high-order SpecM functions #2017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
316 commits
Select commit Hold shift + click to select a range
e33b2d5
wrote translateCompletePureFun
Aug 24, 2023
05abdfa
re-added translateCompleteFunPerm, with documentation reflecting the …
Aug 24, 2023
3ac386c
added helper functions to SAWTranslation.hs to support IRTTranslation.hs
Aug 26, 2023
5f92e7b
added the notion of pure vs impure type translations, to support IRTT…
Aug 26, 2023
fc54d6b
added psubstOfSubst
Aug 26, 2023
a26bdd7
added an OpenTermLike instance for OpenTerm itself
Aug 27, 2023
d071365
Finished rewriting IRTTranslation.hs
Aug 27, 2023
6b313be
added one more import to HeapsterBuiltins.hs to get it to compile
Aug 27, 2023
2225e4f
fixed some variable-binding issues in the definition of defineSpecOpe…
Aug 27, 2023
c865572
added applyCallClos to the prelude
Aug 27, 2023
70e7594
fixed translation code that was only applying closures to apply and c…
Aug 27, 2023
f360be7
added the LRT_SpecM constructor to LRT output types
Aug 27, 2023
4fb514d
fixed the translation of the folding and unfolding functions for recu…
Aug 28, 2023
f8704f6
fixed importDefSpecTerm to turn the import into a SpecImp
Aug 29, 2023
7be0221
changed all uses of the LetRecType eliminator to use the explicit eli…
Aug 29, 2023
6fe20fc
fixed permEnvAddGlobalSymFun to use a spec definition translation ins…
Aug 29, 2023
f7ad5b0
fixed up call to importDefSpecTerm to use its new def
Aug 29, 2023
c3ce460
removed old CompM Coq files from _CoqProject
Aug 29, 2023
eaafb04
Got all the Coq export stuff for the prelude working
Aug 29, 2023
bf877ff
changed Void to translate to the Empty_set type in the Coq standard l…
Aug 31, 2023
4686bf2
removed SpecMExtra from the defaul list of imports in Coq files gener…
Aug 31, 2023
421c124
Changed the type-checker to *not* normalize argument types in lambdas…
Aug 31, 2023
693883d
Merge branch 'master' into saw-core-coq/var-binding-fix
Aug 31, 2023
b74252b
added the termIsClosed function to test if a SAW core term is closed
Sep 1, 2023
599a177
refactored the saw-core-coq translator so that all the local variable…
Sep 1, 2023
d8b5ab2
moved linked_list.sawcore to use the new SpecDef framework
Sep 1, 2023
34690eb
replaced llvmZeroInitValue with a new function translateZeroInit that…
Sep 1, 2023
7195c58
updated mbox_proofs.v after changes to the Coq translator
Sep 1, 2023
f3fd417
renamed askTrr and localTrr to askTR and localTR
Sep 1, 2023
655a9cb
replaced a number of equality tests on the free variables of terms ag…
Sep 1, 2023
09ee22b
replaced checkGroundTerm with the now standard termIsClosed function
Sep 1, 2023
e651848
whoops, fixed a few lingering bugs related to using termIsClosed
Sep 1, 2023
6f7ffe7
made a few fixes to make the code more readable
Sep 1, 2023
5d7a40e
a few more tweaks to make the code look nicer
Sep 1, 2023
1e953dc
finished writing a comment on withSAWVar
Sep 1, 2023
e7f98ee
indentation change requested by review
Sep 1, 2023
2081a64
Merge branch 'master' into saw-core-coq/var-binding-fix
Sep 1, 2023
83af6dc
Merge branch 'saw-core-coq/var-binding-fix' into heapster/higher-order
Sep 1, 2023
058f77a
started defining type descriptions; removed the old IRT stuff
Sep 28, 2023
4eb1da4
Defined tpElem and indElem
Sep 29, 2023
21c8136
Updated the SAW core prelude with the new definition of SpecM based o…
Oct 1, 2023
3801677
renamed arithmetic kinds to expression kinds
Oct 3, 2023
7b5e3e4
fixed a comment; added Tp_BVVec
Oct 4, 2023
ca85494
whoops, fixed the type of FixS
Oct 4, 2023
ea16103
fix defaultMonTable entry for PZeroMSeq, add PZeroMSeqBool
m-yac Oct 12, 2023
3e96850
add missing takeCryM and dropCryM defns, VWord cases in MRSolver/SMT.hs
m-yac Oct 12, 2023
b114765
allow Integer in monadifyType (for Cryptol prelude fns like abs, sext)
m-yac Oct 12, 2023
5035480
include info about the errorS in ReturnNotError
m-yac Oct 12, 2023
2fcba40
check whether assumptions and assertions are provable or not in mrRef…
m-yac Oct 12, 2023
539afa0
fixed indentation
Oct 13, 2023
702ef82
added the Sigmas type
Oct 13, 2023
4cd2921
Working on rewriting SAWTranslation.hs to work with the new definitio…
Oct 13, 2023
488adaa
Got the first portion of SAWTranslation.hs to compile with the new ve…
Oct 13, 2023
556f95d
updated the translation of the implication rules to work with the new…
Oct 17, 2023
648ef60
updated the translation of the EndLifetime rule
Oct 17, 2023
93e5207
Started translating recursive and opaque shapes
Oct 17, 2023
c15590f
updated the translations of shapes and permissions to also contain th…
Oct 17, 2023
d7d0397
added explicit substitutions to type descriptions, for use in transla…
Oct 18, 2023
07b70ee
updated the translation of Crucible expressions
Oct 18, 2023
6d2398e
updated the translation of jump targets and statements
Oct 18, 2023
efde48f
whoops, just realized that lownedTransTerm needs to partially apply i…
Oct 18, 2023
12f626f
changed the MultiFixBodies type to a single function type over all th…
Oct 19, 2023
a533489
small tweak to the type of LetRecS
Oct 19, 2023
b615ddb
finished updating the translation of CFGs to the new SpecM monad
Oct 19, 2023
e0c14e0
always unfold assumingS, assertingS in normComp
m-yac Oct 19, 2023
1fb9b98
defined translateCFGs in the new SpecM monad
Oct 20, 2023
0f71b2b
finished updating tcTranslateAddCFGs to the new SpecM
Oct 20, 2023
94e5db7
finished updating the remaining top-level entrypoints in SAWTranslati…
Oct 20, 2023
fa01175
added the TranslateDescs instances for permissions and atomic permiss…
Oct 21, 2023
c9e0fb6
changed recursive permissions to have a body with a permission variab…
Oct 21, 2023
20edac7
implemented translateCompleteFunType
Oct 21, 2023
91c2547
removed the no longer needed IRTTranslation.hs file
Oct 21, 2023
8473d0c
started updating HeapsterBuiltins.hs to work with the new SpecM monad
Oct 21, 2023
c78e2f2
Moved most of the details of adding and translating recursive permiss…
Oct 22, 2023
97158f9
finished defining the heapster_define_recursive_shape in the new Spec…
Oct 22, 2023
6b71ded
expanded the comments on SomePartialNamedShape
Oct 23, 2023
cf5d645
updated more of HeapsterBuiltins.hs to work with the new SpecM
Oct 23, 2023
18cea15
finished updating SAW to the new SpecM monad!
Oct 23, 2023
d4ea602
added varKindExpr for use in translating descriptions from expression…
Oct 23, 2023
030a927
fixed BV proofs to use the correct, non-monadic type to pass to the e…
Oct 23, 2023
951d232
bug fix: the type description for an existential permission needs to …
Oct 24, 2023
524bb91
implemented proveEqNat
Oct 24, 2023
95ed96b
added a Tp_M constructor to the output type of function descriptions;…
Oct 24, 2023
a732068
whoops, translateCallEntry should not pass in the top-level arguments…
Oct 24, 2023
b0a4935
removed some unused arguments; made some small cosmetic changes
Oct 24, 2023
529a149
updated Coq translation to work with the new SpecM monad
Oct 24, 2023
094ccce
updated CryptolM.sawcore to work with the new SpecM monad
Oct 24, 2023
536f6c1
redefined all the SpecM definitions in a new SpecM.v module in saw-co…
Oct 25, 2023
893ff1c
whoops, fixed the translation of function permissions to apply SpecM …
Oct 25, 2023
4bc68fc
whoops, re-added invariantHint
Oct 25, 2023
a582e5c
updated arrays.sawcore to the new SpecM
Oct 25, 2023
8d88703
started working on a new arrays example for iteratively initializing …
Oct 25, 2023
a0473d8
whoops, forgot to add the type description argument to heapster_defin…
Oct 25, 2023
b40bed4
whoops, was computing the type of the type function incorrectly in he…
Oct 25, 2023
401594d
make atM, updateM cases of MRSolver more flexible
m-yac Oct 25, 2023
1bc1a09
updating the rust_data example to work with the new SpecM monad, and …
Oct 25, 2023
3e8525c
whoops, forgot to update the translation of the SImpl_ElimLLVMBlockNa…
Oct 25, 2023
5b9fbb7
added helper definitions for writing type descriptions
Oct 25, 2023
e3f1f80
more SAW translation bug fixes: made sure to add the Tp_M constructor…
Oct 25, 2023
b3ef9a7
re-enabled the ref_sum example in rust_data
Oct 26, 2023
f1a0fd7
added projTupleOpenTerm' to OpenTerm.hs
Oct 26, 2023
9f7ad32
fixed the LLVM global translations in LLVMGlobalConst.hs to match the…
Oct 26, 2023
96eb8a9
changed transTerms to have a monadic version for permissions
Oct 27, 2023
39e6f36
whoops, used pairTypeOpenTerm instead o9f pairOpenTerm in tupleOpenTerm'
Oct 27, 2023
012bb8b
whoops, forgot to add a SpecM to the output type of LambdaS
Oct 27, 2023
e0cd677
small bug fixes
Oct 27, 2023
bf92122
whoops, messed up the translation of the SImpl_LLVMArrayCellReturn ru…
Oct 27, 2023
3e27d9c
bug fix in bindTransM to use lambdaTupleTransM; also added some FIXME…
Oct 27, 2023
b975f82
Merge branch 'master' into heapster/higher-order-no-stack
Oct 28, 2023
f62b493
fixed projTupleOpenTerm' and its uses to be consistent
Oct 28, 2023
fbd3d74
make MRSolver debug commands uniformly named
m-yac Nov 2, 2023
55be2bb
warn on Heapster implication failures
m-yac Nov 3, 2023
e2fb523
Changed tpElemEnv to no longer use function indices at all
Nov 6, 2023
45a0142
moved SpecM and its related definitions to its own SAW core module
Nov 7, 2023
9a6d36f
updated Heapster to use the new version of SpecM that does not use Fu…
Nov 8, 2023
8656ca0
whoops, forgot to update an identifier from the Prelude to the SpecM …
Nov 8, 2023
9d9bc37
small bug fixes in the translation
Nov 8, 2023
b74a972
updated Coq translation to work with the new definition of SpecM
Nov 8, 2023
1dcab38
more small bug fixes to the translation
Nov 8, 2023
44dd134
bug fixes to get folding of inductive types to work properly
Nov 8, 2023
31e8862
updated the arrays and linked_list examples to work with the new vers…
Nov 8, 2023
0f276fc
whoops, tpElem needs to be applied to an event type
Nov 8, 2023
35a2a8d
uncommented a bunch of the old rust_data functions, and got them working
Nov 8, 2023
dc862fd
changed translateCallEntry to not convert permissions to terms and th…
Nov 8, 2023
0ea6c18
moved the SpecM OpenTerm operations to OpenTerm.hs
Nov 14, 2023
60c4c55
add case for unset variable plus offset to proveEqH
m-yac Nov 15, 2023
c5a46c6
make minor tweaks to refinement in MRSolver, errors in Heapster
m-yac Nov 15, 2023
ca12e4b
started updating monadification to work with the new SpecM type
Nov 19, 2023
a8c9e54
combined monadifyType and monadifyNum into a single monadifyTpExpr fu…
Nov 20, 2023
db9cc4e
updated a bit more of Monadify.hs
Nov 20, 2023
e923082
mostly finished updating monadification, other than quantifying over …
Nov 21, 2023
edd56e4
changed the EventType type to hold an arbitrary term, rather than jus…
Nov 21, 2023
ef693fa
added documentation for monadifyLambdas and monadifyEtaExpand
Nov 21, 2023
8fee78a
updated comments to remove SpecMParams
Nov 21, 2023
c245e10
re-added an updated version of refinesS
Nov 23, 2023
4d6332f
updated MR solver to work with the new definition of SpecM
Nov 23, 2023
d1a24df
whoops, changed some identifiers from the Prelude to the new SpecM SA…
Nov 23, 2023
0aa46dd
updated a use of EvType from the Prelude to the SpecM SAW core module
Nov 23, 2023
9deee50
whoops, forgot to monadify the bitvector type
Nov 23, 2023
a1d71a1
updated monadify example to work with the new SpecM
Nov 24, 2023
3e17ce8
whoops, forgot to update a number of SpecM identifiers to the new Spe…
Nov 25, 2023
1bc0121
added a case to the MR solver normalizer to recognize LetRecS terms
Nov 26, 2023
37d0a5e
whoops, updated two more identifiers to point to the new SpecM module
Nov 26, 2023
197cfae
small bug fixes
Nov 26, 2023
5a66180
updated SpecPrims to work with the new SpecM monad
Nov 26, 2023
a25fd49
fixed the printing for NormComp and friends to have the correct numbe…
Nov 26, 2023
4e89f30
removed the notion of an indescribable num expression, replacing it w…
Nov 27, 2023
a9faa65
reordered to arguments of Tp_Seq to match the definition of Vec, seq,…
Nov 27, 2023
5e8c31f
updated the SMT solver part of MR solver to use the new SpecM in the …
Nov 27, 2023
a5b0f0f
whoops, updated mrGetInvariant to use the new version of assertFiniteS
Nov 27, 2023
313c1ac
whoops, fixed the argument order when constructing a Tp_BVVec
Nov 30, 2023
1c83a4a
added support to MR solver for a new fixpoint operation forNatLtThenS…
Nov 30, 2023
e57b690
refactored the MaybeElim cases by defining a function asDecProp that …
Dec 1, 2023
497997f
updated the MR solver normalizer to unfold forNatLtThenSBody when it …
Dec 1, 2023
2c39941
added refinesS_eq combinator
Dec 4, 2023
7544ab3
finished updating arrays_mr_solver.saw example to work
Dec 4, 2023
d361c28
updated mr_solver_unit_tests.saw example to work
Dec 4, 2023
1673f40
add PPOpts to MREnv, make naming of P.P. fns. consistent (see PPInCtx…
m-yac Dec 6, 2023
fe6678a
add mrsolver_set_debug_printing_depth
m-yac Dec 6, 2023
a805bd0
only check fn body, not arg values, when checking whether a fn is rec…
m-yac Dec 6, 2023
7b42926
expand `FunBind |= FunBind` case to include all `FunName`s
m-yac Dec 6, 2023
ce04ec7
add check for reflexivity in mrProveRel
m-yac Dec 6, 2023
fb569f7
improve error messages for `FunBind |= FunBind` case
m-yac Dec 6, 2023
8045090
add error handling for return types not being equal to refinementTermH
m-yac Dec 6, 2023
79f26d1
when applying a FunAssump, always substEvars in the rewritten RHS
m-yac Dec 6, 2023
f8ab0a1
have both arguments to mrLambdaLift2 be in the same context
m-yac Dec 6, 2023
ba83966
added genBVVecNoPf and atBVVecNoPf primitives to the SAW core prelude
Dec 13, 2023
5c7dedc
updated MR solver to use a more general notion of injective represent…
Dec 13, 2023
5669365
finished implementing injUnifyRepr
Dec 14, 2023
b79f215
fixed lifting bug in mrApplyRepr
Dec 14, 2023
ef82d73
fixed mrTrySetAppliedEVar to correctly handle higher-order variables
Dec 14, 2023
833ec1a
changed genBVVecNoPf to use gen instead of genBVVec
Dec 14, 2023
0cec5c5
changed the normalizer to prefer caller-supplied primitives over its …
Dec 14, 2023
0f695b1
updated implementations of the primitives to work directly with gen a…
Dec 14, 2023
b1e4853
fixed a lifting bug in generalizeCoIndHyp
Dec 14, 2023
00f242a
commented out the no-longer used cases of instUVar
Dec 14, 2023
6be5284
added evar lowering as part of mrProvable, to ensure evars over funct…
Dec 14, 2023
6e4d2e4
whoops, forgot to lift the arg0 repr in generalizeCoIndHyp
Dec 14, 2023
7897e70
added loop detection to proveCoIndHyp
Dec 14, 2023
c1e15ae
added calls to mrIndexBVVec in the mrProveRelH for vectors, though mr…
Dec 14, 2023
71b8125
resolve all but one unused import and variable warnings
m-yac Dec 15, 2023
97d6695
add mrAtBVVec, potentially finish BVVec case of mrProveRelH'
m-yac Dec 15, 2023
c859c55
add `genBVVecNoPf` case to `asGenBVVecTerm`
m-yac Dec 15, 2023
6c8797a
add `mkInjReprType` to forall/exists cases of `mrRefines`
m-yac Dec 15, 2023
076d21d
removed TermLike instance for tuples of length longer than 7 because …
Dec 15, 2023
11a3f05
Fixed vecLenIx to use mrAtVec and mrAtBVVec instead of directly apply…
Dec 15, 2023
c5a70a8
Merge branch 'mrsolver-dilithium' into heapster/higher-order-no-stack
m-yac Dec 17, 2023
4d11bff
changed heapster_init_env to add an import of the SpecM SAW core modu…
Dec 18, 2023
cfc8544
updated the docs for heapster_define_reachability_perm
Dec 18, 2023
aac9638
started updating mbox example to work with the new SpecM monad...
Dec 18, 2023
c6a47ed
add case for `Vec const_n` back to Monadification
m-yac Dec 20, 2023
9e06939
clean up MRSolver/SMT.hs
m-yac Dec 20, 2023
30c863a
add special handling of constant-length vecs in VecLength, etc.
m-yac Dec 20, 2023
a0a0774
Merge branch 'heapster/higher-order-no-stack' of github.com:GaloisInc…
Dec 24, 2023
040891e
add scWhnf to mrFunOutType and do some minor cleanup
m-yac Dec 25, 2023
3858031
fix ConstNatVecLen case of mrVecLenGen
m-yac Dec 25, 2023
c8d3fa0
remove top-level type conversion check from mrProveRel
m-yac Dec 25, 2023
62c9977
add a (albeit hacky) check for type equality back to refinementTermH
m-yac Dec 25, 2023
9660e9d
add mrNormOpenTerm before any calls to mrRefinesFunH or mkInjReprType
m-yac Dec 25, 2023
cf23d1e
change "Prelude." to "SpecM.", remove unused OpenTerm code
m-yac Dec 26, 2023
4db5da6
only unfold main fun in warnErrs, unfold __bodies in print_fun_trans
m-yac Dec 26, 2023
0cf71be
added tuple shapes; changed the translation of memblock permissions t…
Dec 28, 2023
8ab89dd
updated the translations of the memblock implication rules
Dec 28, 2023
43a2319
added more debug info for translating LLVM globals
Dec 29, 2023
1f9b980
whoops, fixed the translation of sequence shapes where both sides hav…
Dec 29, 2023
ba071ac
updated permEnvAddGlobalConst to fit with the new translation of memb…
Dec 29, 2023
97b7593
added parsing support for tuple shapes
Dec 29, 2023
ca65cb1
added an explicit tuple shape to the type of memcpy in rust_data.saw
Dec 29, 2023
e566d3e
fix type error in unsafeAssertMacro
m-yac Jan 1, 2024
61f4cfe
attempting to get `take` to work property with MRSolver smtNorm
m-yac Jan 1, 2024
b538fb9
add VVec case to primGenVec, use iteWithProof instead of maybe
m-yac Jan 4, 2024
fa02d6b
Merge branch 'heapster/tuple-shape' into heapster/higher-order-no-stack
m-yac Jan 4, 2024
d7b0ccc
make the translation of `ETrans_Shape Nothing` be `unitTpDesc`
m-yac Jan 4, 2024
4395e58
simplify types of assumingS/assertingS, add non-S versions, fix typo
m-yac Jan 4, 2024
efe0e54
Merge remote-tracking branch 'origin/master' into heapster/higher-ord…
m-yac Jan 16, 2024
91f311d
resolve some unused import warnings
m-yac Jan 16, 2024
9398ba8
expand tuples for exists/forall evars, get arrays_mr_solver working a…
m-yac Jan 16, 2024
98b3446
handle SpecM fns in mrProveEq, clean up unused heterogeneity
m-yac Jan 23, 2024
2e7cef4
minimize `sawLet`s and beta normalize in `heapster_print_fun_trans`
m-yac Jan 23, 2024
cd15f29
add Dilithium example
m-yac Jan 24, 2024
416f64c
update pinned commit of entree-specs
m-yac Jan 24, 2024
b100897
fix Haddock in Heapster + MRSolver, fix typos found by @RyanGlScott
m-yac Jan 24, 2024
2ac59d6
add more info about generating dilithium2.bc
m-yac Jan 24, 2024
56b964d
add comments about dilithium commit sha
m-yac Jan 24, 2024
b25813e
Merge branch 'master' into heapster/higher-order-no-stack
Feb 2, 2024
50dd970
updated the commit number for the entree-specs repo
Feb 2, 2024
ec47ec1
removed references to functions that are no longer used from unfold_b…
Feb 3, 2024
7ec0f62
removing unsafeAsserts from the definition of iteWithProof because th…
Feb 3, 2024
4189f44
changed the Coq translations of tcAdd and tcMul to be written by hand…
Feb 3, 2024
67e0410
changed SpecM.v to rely on CryptolPrimitivesForSAWCore.v rather than …
Feb 3, 2024
6546f81
fixed up the imports for the heapster_export_coq command
Feb 3, 2024
ccc537e
added MR solver support for the iteWithProof combinator
Feb 3, 2024
ec6d5ba
changed all the examples to import SpecM instead of the SAW core Prelude
Feb 3, 2024
ecd1ce7
added checks to heapster_define_opaque_perm and heapster_define_opaqu…
Feb 3, 2024
2862381
updated global_var example to work
Feb 3, 2024
4767825
added more info to the error message when a type does not match a typ…
Feb 3, 2024
e440d4d
updated checkTypeAgreesWithDesc, since the previous version was incor…
Feb 6, 2024
a277fa9
updated memcpy example to work with the new SpecM
Feb 6, 2024
7e61ad9
updated ListDescType to the correct version to agree with ListDesc, n…
Feb 6, 2024
a3a25d9
started updating the string_set example, but ended up commenting most…
Feb 6, 2024
5e1ec6b
commented out stuff that does not work in the Heapster examples for now
Feb 6, 2024
da7c090
added an override for iteWithProof when calling into SMT
Feb 8, 2024
3874eda
added tracing for terms being inserted by Heapster commands when the …
Feb 8, 2024
1aed8de
removed iso_recursive example, since it is now superseded by the link…
Feb 8, 2024
1860d0d
whoops, forgot to remove the iso_recursive example from the _CoqProject
Feb 9, 2024
9a4df7d
simplified memcpy permissions to help with translation
Feb 9, 2024
4b9b06f
commented out all the _proofs.v files from the _CoqProject
Feb 9, 2024
5c1dc8e
updated rust_lifetimes example to work with the new SpecM
Feb 9, 2024
62679e9
commented out the processBlocks function from the sha512 example beca…
Feb 9, 2024
c7a9085
updated io example to work with the new SpecM
Feb 9, 2024
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: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -333,7 +333,7 @@ jobs:

# If you change the entree-specs commit below, make sure you update the
# documentation in saw-core-coq/README.md accordingly.
- run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb
- run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#5cf91e69c08376bcb17a95a8d2bf2daf406ae8cd

# FIXME: the following steps generate Coq libraries for the SAW core to
# Coq translator and builds them; if we do other Coq tests, these steps
Expand Down
2 changes: 2 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 @@ -15,6 +15,7 @@ Description:

extra-source-files:
saw/Cryptol.sawcore
saw/SpecM.sawcore
saw/CryptolM.sawcore

library
Expand All @@ -39,6 +40,7 @@ library
sbv,
vector,
text,
template-haskell,
executable-path,
filepath
hs-source-dirs: src
Expand Down
1,065 changes: 478 additions & 587 deletions cryptol-saw-core/saw/CryptolM.sawcore
View file
Open in desktop

Large diffs are not rendered by default.

Loading
Loading