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 inline_const_and_op{f,} specializations
Jason Gross
2017-10-22
*
Add another unfolding database
Jason Gross
2017-10-22
*
Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2
Jason Gross
2017-10-22
*
Add ZExtended/InlineConstAndOp.v
Jason Gross
2017-10-22
*
Add StripExpr
Jason Gross
2017-10-22
*
Add tight and loose bounds, no carry in add, sub
Jason Gross
2017-10-22
*
Unfold P.bound1 in fenz
Jason Gross
2017-10-21
*
Add MapType
Jason Gross
2017-10-21
*
Add SmartValf_option
Jason Gross
2017-10-20
*
Add ZExtended/Syntax.v
Jason Gross
2017-10-20
*
Add GeneralizeVar{Wf,Interp}.v
Jason Gross
2017-10-20
*
Generalize wf_compile a bit
Jason Gross
2017-10-20
*
Add GeneralizeVar
Jason Gross
2017-10-20
*
Add a version of exprf that lives in Set
Jason Gross
2017-10-20
*
Add Z.InlineConstAndOp*
Jason Gross
2017-10-20
*
Add InlineConstAndOpInterp.v
Jason Gross
2017-10-20
*
Add interpf_invert_PairsConst
Jason Gross
2017-10-20
*
Add InlineConstAndOpWf.v
Jason Gross
2017-10-20
*
Add wff_SmartPairf_SmartVarfMap_same
Jason Gross
2017-10-20
*
Add SmartVarVarf_Pair, SmartPairfSmartVarVarf_SmartVarf
Jason Gross
2017-10-20
*
Add wff_invert_PairsConst
Jason Gross
2017-10-20
*
Better typing on postprocess_for_const_and_op
Jason Gross
2017-10-20
*
Add InlineConstAndOp
Jason Gross
2017-10-20
*
Add curry{3,4}
Jason Gross
2017-10-20
*
Fix arguments of previous commit
Jason Gross
2017-10-20
*
Add invert_PairsConst
Jason Gross
2017-10-20
*
Add invert_Pairs
Jason Gross
2017-10-20
*
Allow partial-inlining in the inliner
Jason Gross
2017-10-20
*
gmpsec.c: generic constant-time montgomery ladder implementation using mpn_se...
Andres Erbsen
2017-10-20
*
Allow inlining expressions not returning Tbase
Jason Gross
2017-10-20
*
Prove flatten_binding_list_interpf_SmartPairf_same
Jason Gross
2017-10-20
*
Add wff_SmartPairf
Jason Gross
2017-10-20
*
Fix bug in previous commit
Jason Gross
2017-10-20
*
Use div_cps, modulo_cps
Jason Gross
2017-10-20
*
Use fold_right_cps2 to get eqb_cps to get the right continuation type
Jason Gross
2017-10-19
*
Add more unfolds to basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-19
*
Switch arithmetic to cps for Z * Z under the hood
Jason Gross
2017-10-19
*
Add mul_split_cps'
Jason Gross
2017-10-19
*
Move tactics around in src/Arithmetic/CoreUnfolder.v
Jason Gross
2017-10-19
*
Update ZUtil cps definitions
Jason Gross
2017-10-19
*
Pattern over cps lemmas in Arithmetic/Core
Jason Gross
2017-10-19
*
Add ZUtil.CPS
Jason Gross
2017-10-19
*
Unfold more things in basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-18
*
Add display logs
Jason Gross
2017-10-18
*
Add more constant notations
Jason Gross
2017-10-18
*
Fix a scope issue with solve_constant_sig
Jason Gross
2017-10-18
*
Separate out a24 constant as a Z
Jason Gross
2017-10-18
*
Saner checking for freeze and ladderstep
Jason Gross
2017-10-18
*
Remake some curves
Jason Gross
2017-10-18
*
Use a larger modinv_fuel
Jason Gross
2017-10-18
[next]