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
*
Make [reflect] a typeclass and add a bunch of lemmas
Jason Gross
2019-03-04
*
Add better computation of carry chain
Jason Gross
2019-01-26
*
Split up PushButtonSynthesis.v
Jason Gross
2019-01-18
*
Rename Translation.v
jadep
2019-01-17
*
separate toplevel2 into several files; fix up final barrett proof
jadep
2019-01-17
*
Move StringMap into Strings/
Jason Gross
2019-01-15
*
Add StringMap
Jason Gross
2019-01-15
*
Add String_as_OT
Jason Gross
2019-01-15
*
Autocompute s and c in WBW Montgomery
Jason Gross
2019-01-14
*
remove old pipeline
Andres Erbsen
2019-01-09
*
move src/Experiments/NewPipeline/ to src/
Andres Erbsen
2019-01-09
*
new pipeline: refactor glue, split into more files
Jason Gross
2019-01-05
*
Add has_body tactic
Jason Gross
2018-12-21
*
Finish rewriter proofs modulo funext
Jason Gross
2018-12-19
*
Add ZRange.OperationBounds
Jason Gross
2018-12-11
*
Add related_sigT_by_eq
Jason Gross
2018-11-16
*
Add PositiveSet Facts
Jason Gross
2018-10-29
*
Add some lemmas about ex, and, eq
Jason Gross
2018-10-29
*
Add CPSId tactics
Jason Gross
2018-10-28
*
Add some equality lemmas about Positive{Map,Set}
Jason Gross
2018-10-23
*
Add interp-correctness condition for rewriter
Jason Gross
2018-10-11
*
Rename [normalize_commutative_identifier] file to match tactic name
Jason Gross
2018-10-10
*
Add [normalize_commutative_identifier] tactic
Jason Gross
2018-10-10
*
Add ListUtil.ForallIn
Jason Gross
2018-10-09
*
Add some lemmas about Bool.reflect
Jason Gross
2018-09-27
*
Add list_elementwise_eqlistA
Jason Gross
2018-09-14
*
Add PrimitiveSigma
Jason Gross
2018-09-14
*
Add a rudimentary arg parse module
Jason Gross
2018-08-30
*
Add src/Util/PER.v
Jason Gross
2018-08-29
*
Minor improvements to various ZUtil things; bounds
Jason Gross
2018-08-25
*
Bump bbv
Jason Gross
2018-08-24
*
Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil
Jason Gross
2018-08-23
*
Add more operation-specific proofs
Jason Gross
2018-08-21
*
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
[next]