index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
_CoqProject
Commit message (
Expand
)
Author
Age
*
Add the file proving split_bounds correct
Jason Gross
2018-08-13
*
Split up rewrite rules proofs into multiple files
Jason Gross
2018-08-13
*
Start setting up abs-int interp proofs
Jason Gross
2018-08-06
*
Add related_iff_app_curried
Jason Gross
2018-08-06
*
Add GENERATEDIdentifiersWithoutTypesProofs.v
Jason Gross
2018-08-02
*
Integrate Wf and Interp proofs
Jason Gross
2018-07-30
*
Add Wf proofs about MiscCompilerPasses
Jason Gross
2018-07-26
*
Add Wf lemmas about SubstVar
Jason Gross
2018-07-26
*
Add basic wf proofs
Jason Gross
2018-07-26
*
Add some inversion lemmas and tactics
Jason Gross
2018-07-25
*
Montgomery reduction in new pipeline
Jason Gross
2018-07-21
*
Make Z.div_mod_to_quot_rem stronger
Jason Gross
2018-07-10
*
Shuffle some ZUtil lemmas around
Jason Gross
2018-07-08
*
Add ZUtil.Sorting
Jason Gross
2018-06-29
*
Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...
Jason Gross
2018-06-26
*
New pipeline, split among files
Jason Gross
2018-06-17
*
Add ErrorT monad, and Show class
Jason Gross
2018-06-15
*
Add PrimitiveHList, PrimitiveProd
Jason Gross
2018-06-13
*
Move Option.List.map to OptionList.map to fix name clashes in Tuple
Jason Gross
2018-06-04
*
make update-_CoqProject
Jason Gross
2018-05-05
*
Merge pull request #335 from mit-plv/cpsloops
Andres Erbsen
2018-04-18
|
\
*
|
Add new assembly-mimicking operations rshi, cc_m, and cc_l
Jade Philipoom
2018-04-11
*
|
Update number/string conversions
Jason Gross
2018-04-09
|
*
move Loops from Experiments to Util
Andres Erbsen
2018-03-27
|
*
remove old loops code
Andres Erbsen
2018-03-27
|
/
*
Add Algebra.SubsetoidRing
Jason Gross
2018-03-12
*
make update-_CoqProject
Jason Gross
2018-03-10
*
Prove another Barrett reduction variant.
David Benjamin
2018-03-09
*
Add new modular addition operation on Z
Jade Philipoom
2018-02-23
*
Add pointed types
Jason Gross
2018-02-18
*
Add a file to parse taps with Coq notations
Jason Gross
2018-02-14
*
Add some string utility functions
Jason Gross
2018-02-13
*
Add string conversions
Jason Gross
2018-02-11
*
Split off ZRange lemmas
Jason Gross
2018-02-10
*
Add some ZRange operations
Jason Gross
2018-02-10
*
minor updates needed to make it compile with bbv
Samuel Gruetter
2018-02-05
*
add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock di...
Samuel Gruetter
2018-02-05
*
Add x25519 donna versions with the new way of generating C code
Jason Gross
2018-01-15
*
Generate fecarry for solinas
Jason Gross
2018-01-10
*
Factor out fsatz lemmas
Jason Gross
2018-01-09
*
@davidben merged Jacobian+affine into Jacobian+Jacobian
Andres Erbsen
2018-01-09
*
Jacobian coordinates
Andres Erbsen
2018-01-09
*
Add Tactics.RunTacticAsConstr
Jason Gross
2017-11-26
*
Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v
Jason Gross
2017-11-24
*
Make a copy of Demo.v
Jason Gross
2017-11-24
*
Add ModInv autosolver
Jason Gross
2017-11-16
*
Update GeneralizeVar to ensure Wf
Jason Gross
2017-11-13
*
Make pipeline options more easily extensible
Jason Gross
2017-11-13
*
Add faster version of intros [a b] for reflective stuff
Jason Gross
2017-11-13
*
Add autosolve admit package
Jason Gross
2017-11-12
[next]