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 more files to nobigmem
Jason Gross
2018-05-15
*
Fix a bug in previous commit
Jason Gross
2018-05-15
*
Add nobigmem target for Coq's ci
Jason Gross
2018-05-15
*
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
*
Revert "WIP on inductive base_value"
Jason Gross
2018-05-05
*
WIP on inductive base_value
Jason Gross
2018-05-05
*
Revert "WIP with andres, not working pattern language"
Jason Gross
2018-05-05
*
WIP with andres, not working pattern language
Jason Gross
2018-05-05
*
Add comment about leaky abstraction
Jason Gross
2018-05-05
*
Split off specialization to base types from specialization to idents
Jason Gross
2018-05-05
*
make update-_CoqProject
Jason Gross
2018-05-05
*
Add type variables / substitutions
Jason Gross
2018-05-05
*
Change some notations for more readability by Andres
Jason Gross
2018-05-05
*
Update cast -> annotate
Jason Gross
2018-05-05
*
Parameterize over types and identifiers
Jason Gross
2018-05-05
*
Add notes
Jason Gross
2018-05-05
*
Add partial evaluation
Jason Gross
2018-05-05
*
Some experiments with partial evaluation with letin without cps
Jason Gross
2018-05-05
*
Bump versions of Coq we test on travis
Jason Gross
2018-05-02
*
un-hardcode # of reductions
Jade Philipoom
2018-04-30
*
print saturated mulmod for p192 on 32-bit, add note about p256
Jade Philipoom
2018-04-30
*
fixed too-many-additions problem by fixing number of limbs in from_associational
Jade Philipoom
2018-04-30
*
Fix some carry logic
Jade Philipoom
2018-04-30
*
First stab at generating code for saturated solinas modular
Jade Philipoom
2018-04-30
*
fix comment
Jade Philipoom
2018-04-30
*
Fix bounds analysis for saturated ops and remove unneeded comment
Jade Philipoom
2018-04-30
*
first stab at reifying barrett
Jade Philipoom
2018-04-30
*
fix definitions of saturated operations to avoid unnecessary work, and make M...
Jade Philipoom
2018-04-30
[next]