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
*
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
*
Better error message on pose_modinv failure
Jason Gross
2017-10-18
*
Only require half_sz_nonzero in karatsuba (it fails for sz=1)
Jason Gross
2017-10-18
*
Add sanity check of base_le_bitwidth
Jason Gross
2017-10-18
*
Better error messages on m_enc_bounded
Jason Gross
2017-10-18
*
Karatsuba in gallina
Jason Gross
2017-10-18
*
Explicitly specify base
Jason Gross
2017-10-18
*
Move more of carry_sig, zero_sig, one_sig, etc to gallina
Jason Gross
2017-10-18
*
Allow forcing a bitwidth to work
Jason Gross
2017-10-18
*
Add a few more base things
Jason Gross
2017-10-18
*
Add sz2'_nonzero
Jason Gross
2017-10-18
*
Move coef, coef_mod to gallina
Jason Gross
2017-10-18
*
Add some more helper lemmas to synthesis
Jason Gross
2017-10-18
*
Better error messages when m_enc_correct_montgomery fails
Jason Gross
2017-10-18
*
Run remake_curves.py
Jason Gross
2017-10-18
*
Fix make_curve.py to handle files from generate_parameters
Jason Gross
2017-10-18
*
Add chained_carries_cps' lemmas
Jason Gross
2017-10-18
*
Extract rexpr_sig from the record
Jason Gross
2017-10-18
*
Extract evars from reflective pipeline
Jason Gross
2017-10-18
*
Add a comment
Jason Gross
2017-10-18
*
Fix synthesis output record
Jason Gross
2017-10-18
*
Package reflective pipeline side-conditions into a record
Jason Gross
2017-10-18
*
Remove admitted encode_correct proof
Jason Gross
2017-10-18
*
Lemmas about wt_gen
Jason Gross
2017-10-18
*
Stronger pose_proof_tuple
Jason Gross
2017-10-18
*
Update OutputType
Jason Gross
2017-10-18
*
Add final synthesis output type
Jason Gross
2017-10-18
*
Turn CurveParameters into a record
Jason Gross
2017-10-18
*
Add newline at end of CurveParameters
Jason Gross
2017-10-18
*
Support p256 / montgomery in json format
Jason Gross
2017-10-18
*
Reorganize the curve-specific synthesis framework
Jason Gross
2017-10-18
*
Support curves with +2^... in them
Jason Gross
2017-10-18
*
Add default computation for goldilocks
Jason Gross
2017-10-18
*
Fix Makefile deps with move of IntegrationTestDisplayCommon
Jason Gross
2017-10-18
*
Default carry chains in json files
Jason Gross
2017-10-18
*
Handle generating the correct c from 2^448-2^224-1
Jason Gross
2017-10-18
*
Fold Karatsuba into json format and synthesis
Jason Gross
2017-10-18
*
Build curve-specific files from json
Jason Gross
2017-10-18
*
Generate C64 from python script and json
Jason Gross
2017-10-18
*
Reorgainze synthesis framework files into a Framework folder
Jason Gross
2017-10-18
*
Replace curve-specific definitions with tactics
Jason Gross
2017-10-18
*
Factor out specific code underlying ReificationTypes
Jason Gross
2017-10-18
*
Add 8.7-only CacheTerm
Jason Gross
2017-10-18
*
Add more notation constants
Jason Gross
2017-10-18
*
Update .travis.yml from 8.7+beta2 to 8.7.0
Jason Gross
2017-10-18
*
Update .travis.yml to be 8.7-only
Jason Gross
2017-10-18
*
projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptional
Andres Erbsen
2017-10-18
*
Revert "Add -compat 8.6 to _CoqProject"
Jason Gross
2017-10-18
[next]