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
*
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
*
Revert "update coq-scripts"
Jason Gross
2017-04-13
*
add CVE-2017-3732 to crypto-defects.md
Andres Erbsen
2017-04-12
*
update coq-scripts
Andres Erbsen
2017-04-12
*
Add commented out proof of equivalence in MxDH
Jason Gross
2017-04-12
*
Add denoter for symbolic_expr
Jason Gross
2017-04-12
*
SOp needs to hold the type of the arguments, for denote
Jason Gross
2017-04-12
*
Hold types in SFst and SSnd
Jason Gross
2017-04-12
*
More comment on Saturated.v, explaining representation and the [compact] oper...
jadep
2017-04-11
*
More WIP on CSE interp
Jason Gross
2017-04-11
*
Extend cse context when inlining
Jason Gross
2017-04-11
*
Add initial version of CSE interp
Jason Gross
2017-04-11
*
Generalize prepend_prefix
Jason Gross
2017-04-10
*
Fix missing 'by tac' in rewrite_hyp
Jason Gross
2017-04-10
*
Finish CSE_Wf
Jason Gross
2017-04-10
*
Finish most of wf for CSE
Jason Gross
2017-04-10
*
Reorder parameters for ease of partial instantiation, add symbolic_expr_dec
Jason Gross
2017-04-10
*
Add dec_of_bool_dec
Jason Gross
2017-04-10
*
Add lookupb_extendb_full
Jason Gross
2017-04-10
*
Fix CSE to correctly symbolize expressions
Jason Gross
2017-04-10
*
Relax extendb, and prove a property about length
Jason Gross
2017-04-10
*
Key on flat_type not base_type, in CSE
Jason Gross
2017-04-10
*
Add flatten_binding_list_SmartVarfMap2_pair_In_split
Jason Gross
2017-04-10
*
Add flatten_binding_list_SmartVarfMap2_pair_same_in_eq2
Jason Gross
2017-04-10
*
Use Named.Context in CSE, so we can reuse context lemmas
Jason Gross
2017-04-10
*
Add AListContext, WeakListContext
Jason Gross
2017-04-10
*
Split off Compilers.Named.Context
Jason Gross
2017-04-10
*
Add rewrite_hyp ... by tac
Jason Gross
2017-04-10
*
Finish the last of the admits in word-size-selection!
Jason Gross
2017-04-09
*
Split off ZUtil.Stabilization, finish IsBoundedBy!
Jason Gross
2017-04-09
*
Add Z.lt_le_flip_Proper_flip_impl
Jason Gross
2017-04-09
*
More wip on bounds
Jason Gross
2017-04-09
*
Add Z.pow_nonneg to zarith
Jason Gross
2017-04-09
*
More progress on bounds
Jason Gross
2017-04-09
*
Don't take abs in upper_lor_and_bounds
Jason Gross
2017-04-09
[next]