| Commit message (Collapse) | Author | Age |
|
|
|
| |
This gets most of the way to 10 in #14.
|
|
|
|
|
|
|
|
|
|
|
| |
This will eventually make a number of proofs easier.
Unfortunately, the correctness lemmas for AddCoordinates and LadderStep
no longer work (because of different arities), and there's a proof in
Experiments/Ed25519 that I've admitted.
The correctness lemmas will be easy to re-add when we have a more
general version that handle arbitrary type shapes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This reverts commit fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b.
Revert "copy_bounds"
This reverts commit 4c395e83de3c0baf7f8639fa2fbe2b62ba509682.
Revert "Add Common10_4Op"
This reverts commit 677733838139ff09d4a2dd9ff82258492a9a5bab.
Revert "Add Expr10_4Op"
This reverts commit 540740e8a423d0ec9d1dddb173f772c441dc0a1a.
Revert "Add i10top_correct_and_bounded"
This reverts commit bc4184ce6086971799630a0419881c8d344811ca.
Revert "Add appify10"
This reverts commit 66b63b406d9c78a0cecbbf89e5baf282231215c5.
|
| |
|
|
|
|
| |
Grrrrrr, code duplication for ladderstep
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
I haven't found a good way to genericize the proofs of relatedness
things, mostly because Modules and functors are annoying.
|
|
For bounds analysis
|