Dettman Multiplication Arithmetic #1500
Conversation
OwenConoly
force-pushed
the
dettman-mul-only-arith
branch
2 times, most recently
from
b96724a to
7db96f0
Compare
OwenConoly
force-pushed
the
dettman-mul-only-arith
branch
from
3ad1a1a to
e693787
Compare
|
OwenConoly
force-pushed
the
dettman-mul-only-arith
branch
from
e693787 to
94909fe
Compare
|
oops |
OwenConoly
force-pushed
the
dettman-mul-only-arith
branch
from
94909fe to
846c5d4
Compare
| Qed. | ||
| Lemma reifiable_existsb_is_existsb : forall (f : X -> bool) (l : list X), | ||
| existsb f l = List.existsb f l. | ||
| Proof. reflexivity. Qed. |
There was a problem hiding this comment.
How does this end up being provable by reflexivity?
There was a problem hiding this comment.
I wasn't expecting it to be! I don't fully understand how Coq represents fixpoints, but apparently it's very good at simplifying them.
There was a problem hiding this comment.
I guess it's probably the case that List.existsb is set up to be fix existsb (A : Type) (l : list A) : bool, and fold_right probably simplifies to something similar. You can check with Print.
OwenConoly
force-pushed
the
dettman-mul-only-arith
branch
2 times, most recently
from
3c076f9 to
a6b7254
Compare
…e term collection).
…n multiplication algorithm--it now multiplies c by 16, instead of bit-shifting x before multiplying by c, as before. Defined and proved a term-collecting function for numbers in associative representation. The mulmod function now uses the term-collection function. With term collection, the mulmod function now appears to have been defined properly. Refactored, putting mulmod function, generalized mulmod function, and helper functions in separate files.
…sly, there was a reification error). Compiling general version now outputs identical C code to compiling specific version.
…ized mulmod algorithm--compiling to C with 9-limb representation for multiplication modulo 2^512 - 569.
…cation algorithm fails to compile to Bedrock2 for some reason.
…oved BitcoinMultiplication folder.
…cation. Also renamed some other functions.
…dded automatic limb number, limb width inference to cli.
…hetic modification.
JasonGross
force-pushed
the
dettman-mul-only-arith
branch
from
a6b7254 to
d5eb3cd
Compare
|
I've rebased. Is this ready for merge? |
|
Yes! |
|
Do we want to just merge, or to rebase and merge? |
|
Merge away :) Let's leave these commits grouped in a merge commit as we didn't test the intermediate ones. |
This is a part of #1481. It just adds the Dettman multiplication algorithm to the Arithmetic directory.