index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Specific
Commit message (
Expand
)
Author
Age
...
*
Add display of square
Jason Gross
2017-04-14
*
Update ladderstep display
Jason Gross
2017-04-14
*
Handle new ladderstep and square in dsiplay
Jason Gross
2017-04-14
*
Add test for square
Jason Gross
2017-04-14
*
Clean up ladderstep goal with help from Andres
Jason Gross
2017-04-14
*
X25519: wrap synthesized code in donna-c64, run SUPERCOP benchmarks
Andres Erbsen
2017-04-13
*
Update display logs
Jason Gross
2017-04-13
*
Update display to not line-wrap
Jason Gross
2017-04-13
*
Update ladderstep display
Jason Gross
2017-04-13
*
Rewrite the ladderstep goal
Jason Gross
2017-04-13
*
Add eexists_sig_etransitivity_for_rewrite_fun_R
Jason Gross
2017-04-13
*
Add lift4_sig_sig
Jason Gross
2017-04-13
*
Add eexists_sig_etransitivity_R
Jason Gross
2017-04-13
*
Split off Compilers.Named.Context
Jason Gross
2017-04-10
*
Update display logs
Jason Gross
2017-04-07
*
Parameterize bounds analysis over round_up
Jason Gross
2017-04-07
*
Add Ladderstep130 display log
Jason Gross
2017-04-07
*
Add display for ladderstep 130-bit
Jason Gross
2017-04-07
*
Revert "Don't print ladderstep four times"
Jason Gross
2017-04-07
*
Add ladderstep display log
Jason Gross
2017-04-07
*
Don't print ladderstep four times
Jason Gross
2017-04-07
*
Add working display of ladderstep
Jason Gross
2017-04-07
*
Add display logs
Jason Gross
2017-04-07
*
Display un-interped C code
Jason Gross
2017-04-07
*
Add 130-bit 3-register synthesis
Jason Gross
2017-04-07
*
Add Display files and targets
Jason Gross
2017-04-07
*
Use [refine_reflectively] again in ladderstep
Jason Gross
2017-04-07
*
Use carry_mul
Jason Gross
2017-04-07
*
Add IntegrationTestLadderstep.v
Jason Gross
2017-04-07
*
Merge branch 'rename-everything'. Closes #14.
Andres Erbsen
2017-04-06
|
\
|
*
rename-everything
Andres Erbsen
2017-04-06
|
*
remove unused files
Andres Erbsen
2017-04-06
*
|
Add IntegrationTest for Sub
Jason Gross
2017-04-06
*
|
FIx encoding of [coef]; instead of [encode 2p], it should be [encode p + enco...
jadep
2017-04-06
*
|
Rename IntegrationTest{=>Mul}.v
Jason Gross
2017-04-06
|
*
start removing BaseSystem
Andres Erbsen
2017-04-06
*
|
Switch to 51-bit limbs
Jason Gross
2017-04-06
*
|
Compute the bitwidth in integration test
Jason Gross
2017-04-06
*
|
don't hardcode number of limbs
jadep
2017-04-06
*
|
Compute weight function from other terms
jadep
2017-04-06
|
/
*
Use tactics from MoveLetIn in integration test
Jason Gross
2017-04-05
*
Add [Proof using] to most proofs
Jason Gross
2017-04-04
*
Move sigma MapProjections to a separate file
Jason Gross
2017-04-04
*
Use a more robust way of saving context definitions in IntegrationTest
Jason Gross
2017-04-03
*
More fine-grained tactic imports
Jason Gross
2017-04-03
*
Split off liftn_sig, add lift{3,4}_sig
Jason Gross
2017-04-03
*
Synthesize mul instead of add
Jason Gross
2017-04-03
*
Work around an anomaly in pretyping/constr_matching
Jason Gross
2017-04-03
*
Document some tactics from Jade's pipleine side
Jason Gross
2017-04-03
*
Finally, a fully working IntegrationTest
Jason Gross
2017-04-03
[prev]
[next]