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 ErrorT monad, and Show class
Jason Gross
2018-06-15
*
Add decimal_string_of_Z
Jason Gross
2018-06-15
*
Add some lemmas and defs to ListUtil.FoldBool
Jason Gross
2018-06-14
*
Set universe polymorphism in CPSNotations
Jason Gross
2018-06-14
*
Add notations for cpsbind, cps_option_bind
Jason Gross
2018-06-14
*
Actually use primitive projections in PrimitiveHList
Jason Gross
2018-06-13
*
Minor refactoring
Jason Gross
2018-06-13
*
Add PrimitiveHList, PrimitiveProd
Jason Gross
2018-06-13
*
Move Option.List.map to OptionList.map to fix name clashes in Tuple
Jason Gross
2018-06-04
*
Add Option.List.map
Jason Gross
2018-06-04
*
Move cps notations into a scope
Jason Gross
2018-06-01
*
Add more bind reserved notations
Jason Gross
2018-05-31
*
fix over-indented line
Jade Philipoom
2018-05-31
*
prove prefancy->fancy for barrett special case
Jade Philipoom
2018-05-31
*
move around some Lets so that 8.8 doesn't error
Jade Philipoom
2018-05-31
*
relocate ok_expr tactics and fix an admit with a silly bounds relaxation hack
Jade Philipoom
2018-05-31
*
Proved pre-fancy barrett reduction correct (except 1 admit for bounds
Jade Philipoom
2018-05-31
*
temporary workaround for #352
Jade Philipoom
2018-05-31
*
Define machine model, write prefancy->fancy pass, and prove Montgomery code c...
Jade Philipoom
2018-05-31
*
[WIP] shifting adds
Jade Philipoom
2018-05-31
*
change order of additions so that they a) make more sense and b) are more sui...
Jade Philipoom
2018-05-31
*
tweak binders so that shifts from base conversion get inlined
Jade Philipoom
2018-05-31
*
remove unneeded comment and extra whitespace
Jade Philipoom
2018-05-31
*
end-to-end proof for montgomery
Jade Philipoom
2018-05-31
*
Proofs for pre-fancy pass (could use cleanup)
Jade Philipoom
2018-05-31
*
proofs for straightline pass (with admits for some depth stuff that should be...
Jade Philipoom
2018-05-31
*
Move function argument out of fixpoint of List.map2
Jason Gross
2018-05-21
*
Compatibility after Coq PR#262.
Hugo Herbelin
2018-05-14
*
finish pushing through changes to dummy and factor out identifier match
Jade Philipoom
2018-05-07
*
replace dummy_var with dummy_arrow and change style of straightline tests to ...
Jade Philipoom
2018-05-07
*
clean up shared notations and constant-rewriting logic for prefancy
Jade Philipoom
2018-05-07
*
prefancy now works on barrett (modulo add-opp=>sub)
Jade Philipoom
2018-05-07
*
Move straightline and prefancy stuff above barrett reduction
Jade Philipoom
2018-05-07
*
Translating to 'pre-fancy' form now works on Montgomery
Jade Philipoom
2018-05-07
*
move depth to a more sensible location
Jade Philipoom
2018-05-07
*
Translation to straightline code now works correctly on montgomery256
Jade Philipoom
2018-05-07
*
Translation to straightline code (first attempts, mostly working)
Jade Philipoom
2018-05-07
*
fix the placement of a dlet to make more sense
Jade Philipoom
2018-05-07
*
Backtrack on moving a notation to Notations.v, to fix conflict
Jason Gross
2018-05-06
*
Fix notations to not conflict with bbv
Jason Gross
2018-05-06
*
More reserved notations
Jason Gross
2018-05-06
*
Add another notation
Jason Gross
2018-05-06
*
Fix a typo in last commit
Jason Gross
2018-05-06
*
Add a reserved notation for #v
Jason Gross
2018-05-06
*
Don't use vm_compute with existentials
Jason Gross
2018-05-05
*
Update comment
Jason Gross
2018-05-05
*
Fully finish flat_map
Jason Gross
2018-05-05
*
Fix flat_map
Jason Gross
2018-05-05
*
WIP on lists as cons cells
Jason Gross
2018-05-05
*
Remove vinterp_arrow function
Jason Gross
2018-05-05
[prev]
[next]