index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
/
SimplyTypedArithmetic.v
Commit message (
Expand
)
Author
Age
*
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
*
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
*
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
*
tweak definition of flatten to use an index rather than check the length of t...
Jade Philipoom
2018-04-30
*
fix the placement of a dlet to make more sense
Jade Philipoom
2018-04-30
*
In reassocation, don't reassociate additions
Jason Gross
2018-04-26
*
Fix a printout
Jason Gross
2018-04-26
*
Revert most of "Make reassociation optional"
Jason Gross
2018-04-26
*
Make reassociation optional
Jason Gross
2018-04-26
*
Compute tight bounds in a different way
Jason Gross
2018-04-26
*
Don't introduce extra lambdas and apps in uncurry
Jason Gross
2018-04-26
*
Add some Positional Hint Rewrites
Jason Gross
2018-04-26
*
pass-through after Jason's review
Jade Philipoom
2018-04-19
*
add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati...
Jade Philipoom
2018-04-19
*
Also include argument bounds in bounds-analysis-failure message
Jason Gross
2018-04-18
*
Actually display the error messages from pipeline failures
Jason Gross
2018-04-18
*
Add a Z.cast2 case to bounds extraction
Jason Gross
2018-04-18
*
Also include the syntax tree in bounds analysis errors
Jason Gross
2018-04-18
*
move requires to top of file
Jade Philipoom
2018-04-11
*
barrett reduction definition and proof
Jade Philipoom
2018-04-11
[next]