Added dettman multiplication algorithm, made changes to equivalence checker#1481

Closed

OwenConoly wants to merge 20 commits intomit-plv:masterfrom OwenConoly:better_bounds

+40,772-34,767

Commits on Jul 31, 2022

Added first draft of bitcoin multiplication algorithm (no intermediate term collection).
OwenConoly
committed

Commits on Aug 1, 2022

Fixed problem with redundant bit shift in generated C code for bitcoin multiplication algorithm--it now multiplies c by 16, instead of bit-shifting x before multiplying by c, as before. Defined and…
OwenConoly
committed
Added c file containing code that results from compiling bitcoin mulmod algorithm.
OwenConoly
committed
Made generalized bitcoin mulmod algorithm work with compiler (previously, there was a reification error). Compiling general version now outputs identical C code to compiling specific version.
OwenConoly
committed
Proved general form of bitcoin mulmod algorithm. Added appropriate hypotheses.
OwenConoly
committed
Split up files in BitcoinMultiplication folder. Added test of generalized mulmod algorithm--compiling to C with 9-limb representation for multiplication modulo 2^512 - 569.
OwenConoly
committed
Added bitcoin multiplication command line interface. Bitcoin multiplication algorithm fails to compile to Bedrock2 for some reason.
OwenConoly
committed
Refactored HelpfulFunctions.v (split into Core.v and ListUtil.v). Removed BitcoinMultiplication folder.
OwenConoly
committed
Renamed files, modules, etc: BitcoinMultiplication -> DettmanMultiplication. Also renamed some other functions.
OwenConoly
committed

Commits on Sep 9, 2022

added or-to-add rewriting; better bounds analysis to assembly checker
OwenConoly
committed

Commits on Nov 7, 2022