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 StringMap
Jason Gross
2019-01-15
*
Add String_as_OT
Jason Gross
2019-01-15
*
Ensure that we only left-shift on unsigned values
Jason Gross
2019-01-15
*
Fix computation of INTX_MIN
Jason Gross
2019-01-15
*
Don't cast signed to unsigned before shifting
Jason Gross
2019-01-15
*
We don't need to encode c with taps in WBW montgomery
Jason Gross
2019-01-14
*
Autocompute s and c in WBW Montgomery
Jason Gross
2019-01-14
*
remove old pipeline
Andres Erbsen
2019-01-09
*
move src/Experiments/NewPipeline/ to src/
Andres Erbsen
2019-01-09
*
Fix for 8.7
Jason Gross
2019-01-07
*
Merge remote-tracking branch 'origin/fix_fancy4'
Andres Erbsen
2019-01-07
|
\
*
|
Update README.md
Jason Gross
2019-01-05
*
|
prove admit
Andres Erbsen
2019-01-05
*
|
build on Coq master
Andres Erbsen
2019-01-05
*
|
new pipeline: refactor glue, split into more files
Jason Gross
2019-01-05
|
*
Update fancy rewriter output with new compilation output
Jason Gross
2019-01-03
|
*
Finish proving fancy rewrite rules
Jason Gross
2019-01-03
|
*
Fix bounds checking on shift
Jason Gross
2019-01-03
|
*
comment out broken code so things build
jadep
2019-01-03
|
*
try to fix fancy rewrite rules; current output is incorrect
jadep
2019-01-03
|
*
WIP
jadep
2019-01-03
|
*
remove dead code
jadep
2019-01-03
|
*
remove whitespace, print statements, and some dead tactics
jadep
2019-01-03
|
*
fixed up some of the fancy rewrite rules
jadep
2019-01-03
|
*
WIP: prove that barrett_red256 is a valid expression modulo some issues with ...
jadep
2019-01-03
|
*
WIP: expand valid_ident and prove of_prefancy_correct using it
jadep
2019-01-03
|
*
WIP : made everything more concrete and proved of_Expr. Still to do for of_Ex...
jadep
2019-01-03
|
*
WIP
jadep
2019-01-03
|
*
WIP
jadep
2019-01-03
|
*
WIP
jadep
2019-01-03
|
*
WIP
jadep
2019-01-03
|
/
*
Prove that convert_bases partitions
Jason Gross
2019-01-03
*
Do not rely on `Refine Instance Mode`
Maxime Dénès
2019-01-02
*
Remove WBW Mont lemmas from push_eval
Jason Gross
2018-12-26
*
Add eval_* lemmas for WBW Mont Arith operations
Jason Gross
2018-12-26
*
Move le_{add,sub}_1_* to ZUtil.Le
Jason Gross
2018-12-25
*
from_montgomery{_ => }mod, for consistency with other naming
Jason Gross
2018-12-24
*
Add correctness in arithmetic for mulx, addcarryx, subborrowx
Jason Gross
2018-12-21
*
Add has_body tactic
Jason Gross
2018-12-21
*
Add eval_freeze_to_bytesmod to push_eval
Jason Gross
2018-12-21
*
Add length_encode_no_reduce to distr_length
Jason Gross
2018-12-21
*
Add `Proof using` directives in Arithmetic
Jason Gross
2018-12-21
*
Fix a few minor things in Arithmetic
Jason Gross
2018-12-21
*
remove unneeded lemma and do some micro-performance-optimization at one stick...
jadep
2018-12-21
*
remove proof duplication
jadep
2018-12-21
*
fix hints and [Proof using] statements so that proofs go through
jadep
2018-12-21
*
prove [small_sub_then_maybe_add]
jadep
2018-12-21
*
prove [eval_sub_then_maybe_add]
jadep
2018-12-21
*
fix hints and [Proof using] statements so that proofs go through
jadep
2018-12-21
*
prove [small_conditional_sub]
jadep
2018-12-21
[prev]
[next]