index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Arithmetic
Commit message (
Expand
)
Author
Age
*
Add some more things to basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-18
*
Add basesystem_partial_evaluation_unfolder db
Jason Gross
2017-10-18
*
Unfold more things in core unfolder
Jason Gross
2017-10-18
*
Allow instantiating type arguments without reducing matches
Jason Gross
2017-10-18
*
Pattern more things in arithmetic/core
Jason Gross
2017-10-17
*
Add MulSplitUnfolder
Jason Gross
2017-10-17
*
Add faster arithmetic unfolding
Jason Gross
2017-10-15
*
Extend basesystem_partial_evaluation_RHS
Jason Gross
2017-10-15
*
Fix a typo in the previous commit
Jason Gross
2017-10-14
*
Split up solve_op_mod_eq
Jason Gross
2017-10-14
*
Add UniformWeightInstances
Jason Gross
2017-10-09
*
Add cbv_runtime in Arithmetic/Core
Jason Gross
2017-07-08
*
More fine-grained tactics imports
Jason Gross
2017-07-08
*
Remove some admitted lemmas
Jason Gross
2017-07-07
*
enforce use of [F.zero], [F.one]; prove Ed25519 admits
Andres Erbsen
2017-07-07
*
prove ModularArithmeticTheorems admits
Andres Erbsen
2017-07-06
*
Fix a typo that ends up not mattering
Jason Gross
2017-07-06
*
Closed under the global context
Andres Erbsen
2017-07-02
*
prove [MontgomeryAPI.small_add]
Andres Erbsen
2017-07-02
*
fix [small_div] arguments
Andres Erbsen
2017-07-02
*
[small] admits progress...
Andres Erbsen
2017-07-01
*
proved small_sat_add
jadep
2017-07-01
*
change opp to runtime_opp
jadep
2017-07-01
*
proved remaining [eval] admits in MontgomeryAPI
jadep
2017-07-01
*
Prove saturated carrying-subtraction-chain correct
jadep
2017-07-01
*
Prove saturated carrying-addition-chain correct
jadep
2017-06-30
*
Reorganization of saturated arithmetic
jadep
2017-06-29
*
create directory for saturated arithmetic in preparation for splitting into m...
jadep
2017-06-29
*
Merge branch 'addsubchains'
jadep
2017-06-29
|
\
*
|
new add/carry chain logic with admitted proofs
jadep
2017-06-29
*
|
Skeleton for add/subtract chains (see #222)
jadep
2017-06-29
|
*
Fix the sense of op_{get,with}_carry in Saturated
Jason Gross
2017-06-29
|
*
Adapt to new arguments of saturated things
Jason Gross
2017-06-29
|
*
Fix type signatures of saturated things for WBW
Jason Gross
2017-06-29
|
*
new add/carry chain logic with admitted proofs
jadep
2017-06-29
|
*
Skeleton for add/subtract chains (see #222)
jadep
2017-06-28
|
/
*
proved eval_mod and eval_div (last remaining eval_ admits in Saturated)
jadep
2017-06-27
*
Add a comment for nonzero_cps
Jason Gross
2017-06-26
*
Fix a broken proof
Jason Gross
2017-06-26
*
Factor out admitted proof into admitted lemma
Jason Gross
2017-06-26
*
Add nonzero synthesis
Jason Gross
2017-06-26
*
indentation
Jason Gross
2017-06-25
*
Prove map2_zselect
Jason Gross
2017-06-25
*
Fixes #219
jadep
2017-06-25
*
Clean up some montgomery wbw instantiation, make display
Jason Gross
2017-06-24
*
Fill in axioms for sub_then_maybe_add; this required fiddling with updated ar...
jadep
2017-06-24
*
made conditional_add a wrapper, defined and proved sub_then_maybe_add
jadep
2017-06-24
*
Make a 'conditionals' section in Columns, and move conditional_add there
jadep
2017-06-24
*
Add (partially admitted) integration tests for add, sub, opp
Jason Gross
2017-06-22
*
P256: Partial work on add, sub, opp
Jason Gross
2017-06-22
[next]