Merge new base system (#112)

* Added sketch of new low-level base system code

* Implemented and proved addition

* Implemented carrying, which requires defining over Z rather than arbitrary ring

* Proved carry and proved ring-ness of base system ops

* Implemented split operation

* Started implementing modular reduction

* NewBaseSystem: prettify some proofs

* andres base

* improve andresbase

* new base

* first draft of goldilocks karatsuba

* Factored out goldilocks karatsuba

* Implement and prove karatsuba

* goldilocks cleanup

remodularize

* merge karatsuba and goldilocs karatsuba parameter blocks

* carry impl and proofs (not yet synthesis-ready)

* newbasesystem: use rewrite databases

* carry index range fix (TODO: allow for carry-then-reduce)

* simpler carry implementation

* Added compact operation for saturated base systems (this handles carries after multiplying or adding)

* debugging reduction for compact_rows

* rewrote compact

* Converted saturated section to CPS

* some progress on cps conversion for non-saturated stuff

* Converted associational non-saturated code to CPS, temporarily commented out examples

* pushed cps conversion through Positional

* moved list/tuple stuff to top of file

* proved lingering lemma

* worked on generic-style goal for simplified operations

* finished proving the generic-form example goal, revising a couple earlier lemmas

* revised previous lemmas

* finished revising previous lemmas

* removed commented-out code

* fixed non-terminating string in comment

* fix for 8.5

* removed old file

* better automation part 1

* better automation part 2 (goodbye proofs)

* better automation part 3/3

* some work on freeze

* remove saturated code and clean up exported-operations code

* Move helper lemmas for list/tuple CPS stuff to new CPSUtil file

* qualified imports

* fix runtime notations and module-level Let as per comments

* moved push_id to CPSUtil and cancel_pair lemmas to Prod

* fixed typo

* correctly generalized and moved lift_tuple2 (now called lift2_sig) and converted chained_carries into a fold

* moved karatsuba section to new file

* rename lemmas and definitions (now cps definitions are consistently <name>_cps and non-cps equivalents have no suffix)

* updated timing on mulT

* renamed push_eval to push_basesystem_eval

1 files changed, 49 insertions, 0 deletions

diff --git a/src/Karatsuba.v b/src/Karatsuba.v
new file mode 100644
index 000000000..47ae2facf
--- /dev/null
+++ b/src/Karatsuba.v
@@ -0,0 +1,49 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Import Crypto.Util.ZUtil.
+Local Open Scope Z_scope.
+
+Section Karatsuba.
+  Context {T : Type} (eval : T -> Z)
+          (sub : T -> T -> T)
+          (eval_sub : forall x y, eval (sub x y) = eval x - eval y)
+          (mul : T -> T -> T)
+          (eval_mul : forall x y, eval (mul x y) = eval x * eval y)
+          (add : T -> T -> T)
+          (eval_add : forall x y, eval (add x y) = eval x + eval y)
+          (scmul : Z -> T -> T)
+          (eval_scmul : forall c x, eval (scmul c x) = c * eval x)
+          (split : Z -> T -> T * T)
+          (eval_split : forall s x, s <> 0 -> eval (fst (split s x)) + s * (eval (snd (split s x))) = eval x)
+  .
+
+  Definition karatsuba_mul s (x y : T) : T :=
+      let xab := split s x in
+      let yab := split s y in
+      let xy0 := mul (fst xab) (fst yab) in
+      let xy2 := mul (snd xab) (snd yab) in
+      let xy1 := sub (mul (add (fst xab) (snd xab)) (add (fst yab) (snd yab))) (add xy2 xy0) in
+      add (add (scmul (s^2) xy2) (scmul s xy1)) xy0.
+
+  Lemma eval_karatsuba_mul s x y (s_nonzero:s <> 0) :
+    eval (karatsuba_mul s x y) = eval x * eval y.
+  Proof. cbv [karatsuba_mul]; repeat rewrite ?eval_sub, ?eval_mul, ?eval_add, ?eval_scmul.
+         rewrite <-(eval_split s x), <-(eval_split s y) by assumption; ring. Qed.
+
+
+  Definition goldilocks_mul s (xs ys : T) : T :=
+    let a_b := split s xs in
+    let c_d := split s ys in
+    let ac := mul (fst a_b) (fst c_d) in
+    (add (add ac (mul (snd a_b) (snd c_d)))
+         (scmul s (sub (mul (add (fst a_b) (snd a_b)) (add (fst c_d) (snd c_d))) ac))).
+
+  Local Existing Instances Z.equiv_modulo_Reflexive RelationClasses.eq_Reflexive Z.equiv_modulo_Symmetric Z.equiv_modulo_Transitive Z.mul_mod_Proper Z.add_mod_Proper Z.modulo_equiv_modulo_Proper.
+
+  Lemma goldilocks_mul_correct (p : Z) (p_nonzero : p <> 0) s (s_nonzero : s <> 0) (s2_modp : (s^2) mod p = (s+1) mod p) xs ys :
+    (eval (goldilocks_mul s xs ys)) mod p = (eval xs * eval ys) mod p.
+  Proof. cbv [goldilocks_mul]; Zmod_to_equiv_modulo.
+    repeat rewrite ?eval_mul, ?eval_add, ?eval_sub, ?eval_scmul, <-?(eval_split s xs), <-?(eval_split s ys) by assumption; ring_simplify.
+    setoid_rewrite s2_modp.
+    apply f_equal2; nsatz. Qed.
+End Karatsuba.