index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Add CSE correctness files for Z-specialization
Jason Gross
2017-04-15
*
Add more constant notations
Jason Gross
2017-04-15
*
Also unfold lift3_sig
Jason Gross
2017-04-15
*
Update notation files
Jason Gross
2017-04-15
*
Generalize linearize a bit more
Jason Gross
2017-04-15
*
More robust pipeline
Jason Gross
2017-04-15
*
More powerful inversion_zrange
Jason Gross
2017-04-15
*
Add a bit more power to side conditions in reflective_interp rewrite db
Jason Gross
2017-04-15
*
Generalize MapCastCorrect a bit
Jason Gross
2017-04-15
*
Fix hint for SimplifyArith
Jason Gross
2017-04-15
*
Update display of ladderstep130
Jason Gross
2017-04-14
*
Prelinearize so we can simplify more arithmetic in pipeline
Jason Gross
2017-04-14
*
Better version of linearize without a-normal form
Jason Gross
2017-04-14
*
Use 128/256 in ladderstep 130
Jason Gross
2017-04-14
*
Split off a-normal form from flattening
Jason Gross
2017-04-14
*
Remove old versions of wordsize selection
Jason Gross
2017-04-14
*
Remove useless import
Jason Gross
2017-04-14
*
Add CSE specialized to Z
Jason Gross
2017-04-14
*
lemmas about ladderstep on zero
Andres Erbsen
2017-04-14
*
Add base_type_leb_total
Jason Gross
2017-04-14
*
Add some CSE properties
Jason Gross
2017-04-14
*
Ask for leb on op codes and base types, not flat types
Jason Gross
2017-04-14
*
Add support for cse-modulo-normalization
Jason Gross
2017-04-14
*
stronger ladderstep correctness proof courtesy Teo
Andres Erbsen
2017-04-14
*
Add hand-cse'd version of square
Jason Gross
2017-04-14
*
Add display of square
Jason Gross
2017-04-14
*
Update ladderstep display
Jason Gross
2017-04-14
*
Handle new ladderstep and square in dsiplay
Jason Gross
2017-04-14
*
Add test for square
Jason Gross
2017-04-14
*
Add for-loop combinator
Jason Gross
2017-04-14
*
Update CSE proof with some help from Adam
Jason Gross
2017-04-14
*
Clean up ladderstep goal with help from Andres
Jason Gross
2017-04-14
*
Prove interp correctness of register reassign
Jason Gross
2017-04-13
*
Add Named.Syntax.Interp
Jason Gross
2017-04-13
*
X25519: wrap synthesized code in donna-c64, run SUPERCOP benchmarks
Andres Erbsen
2017-04-13
*
Add lookupb_remove
Jason Gross
2017-04-13
*
Add lookupb_removeb_same
Jason Gross
2017-04-13
*
Add lookupb_remove_not_in
Jason Gross
2017-04-13
*
Update display logs
Jason Gross
2017-04-13
*
Update display to not line-wrap
Jason Gross
2017-04-13
*
Add ContextOnOk
Jason Gross
2017-04-13
*
Remove dead code in comments
Jason Gross
2017-04-13
*
Update ladderstep display
Jason Gross
2017-04-13
*
Rewrite the ladderstep goal
Jason Gross
2017-04-13
*
Handle implications in pipeline glue
Jason Gross
2017-04-13
*
Add Util.Logic.ImplAnd
Jason Gross
2017-04-13
*
Add eexists_sig_etransitivity_for_rewrite_fun_R
Jason Gross
2017-04-13
*
Add lift4_sig_sig
Jason Gross
2017-04-13
*
Add eexists_sig_etransitivity_R
Jason Gross
2017-04-13
*
Add commented out proof of equivalence in MxDH
Jason Gross
2017-04-12
[next]