index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Fix (hopefully) overlap in reg
Jason Gross
2017-09-05
*
Fix schedule to be in correct order
Jason Gross
2017-09-05
*
WIP
Jason Gross
2017-09-05
*
Fix schedule
Jason Gross
2017-09-05
*
WIP on reg alloc
Jason Gross
2017-09-04
*
chmod +x
Jason Gross
2017-09-04
*
Add display files (temporary, kind-of)
Jason Gross
2017-09-04
*
WIP Update compile with registers
Jason Gross
2017-09-04
*
More WIP on register allocation
Jason Gross
2017-08-17
*
Handle most of register allocation
Jason Gross
2017-08-14
*
Handle equality in parsing
Jason Gross
2017-08-14
*
Fixup header and footer
Jason Gross
2017-08-14
*
Update scheduler to know about implicit mulx arg
Jason Gross
2017-08-14
*
Use a more realistic processor model
Jason Gross
2017-08-13
*
Revert "Revert "Subset compiler differently""
Jason Gross
2017-08-13
*
Revert "Subset compiler differently"
Jason Gross
2017-08-13
*
Subset compiler differently
Jason Gross
2017-08-13
*
Add heuristic search
Jason Gross
2017-08-13
*
Add decidable equality with nil
Jason Gross
2017-08-13
*
Update the graph maker
Jason Gross
2017-08-13
*
Update exhaustive search compiler
Jason Gross
2017-08-13
*
Add memoize.py to zinc compiler folder
Jason Gross
2017-08-11
*
wip on register allocation in python
Jason Gross
2017-08-09
*
Fix the sense of dependencies in zinc generation
Jason Gross
2017-08-09
*
Get all scheduling done in one frame
Jason Gross
2017-08-09
*
Fix wip
Jason Gross
2017-08-09
*
Larger instruction window for zinc
Jason Gross
2017-08-09
*
Add a faster version of the zinc compiler
Jason Gross
2017-08-06
*
Add initial stab at C-compilation by optimization
Jason Gross
2017-08-06
*
Update crypto-defects.md
Andres Erbsen
2017-07-29
*
Factor out some of the preglue synthesis code
Jason Gross
2017-07-08
*
Unfold tuple arguments in reflective pipeline
Jason Gross
2017-07-08
*
Add cbv_runtime in Arithmetic/Core
Jason Gross
2017-07-08
*
Make some tactics a bit more powerful
Jason Gross
2017-07-08
*
Also test coq v8.7 on travis
Jason Gross
2017-07-08
*
Fix Demo.v
Jason Gross
2017-07-08
*
More fine-grained tactics imports
Jason Gross
2017-07-08
*
More fine-grained imports
Jason Gross
2017-07-08
*
Add UnfoldArg
Jason Gross
2017-07-08
*
Update .gitignore with compilation outputs
Jason Gross
2017-07-08
*
Fix format warning in gcc
Jason Gross
2017-07-08
*
Fix CSE_sym denote
Jason Gross
2017-07-07
*
Fix proofs broken by previous commit
Jason Gross
2017-07-07
*
Stronger contexts
Jason Gross
2017-07-07
*
README: recommend against Coq 8.5
Andres Erbsen
2017-07-07
*
Remove some admitted lemmas
Jason Gross
2017-07-07
*
enforce use of [F.zero], [F.one]; prove Ed25519 admits
Andres Erbsen
2017-07-07
*
prove ModularArithmeticTheorems admits
Andres Erbsen
2017-07-06
*
Curves/Edwards/Affine: prove point compression admits
Andres Erbsen
2017-07-06
*
prove an admit in ArithmeticSynthesisTest
Andres Erbsen
2017-07-06
[next]