Merge pull request #1 from plv/master

Arbitrary-base positional number system

7 files changed, 662 insertions, 44 deletions

diff --git a/.gitignore b/.gitignore
index ae784f4a5..cec91e9a6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
+bedrock
 fiat
 *~
diff --git a/_CoqProject b/_CoqProject
index 538b6efc9..7f2624ee8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,11 +2,14 @@
 -R fiat/src Fiat
 -R bedrock/Bedrock Bedrock
 src/Tactics/VerdiTactics.v
+src/Util/ListUtil.v
 src/Galois/Galois.v
 src/Galois/GaloisTheory.v
+src/Galois/ZGaloisField.v
 src/Galois/GaloisExamples.v
 src/Galois/AbstractGaloisField.v
 src/Galois/ComputationalGaloisField.v
-src/Galois/ZGaloisField.v
+src/Galois/BaseSystem.v
 src/Curves/PointFormats.v
+src/Assembly/WordBounds.v
 src/Curves/Curve25519.v
diff --git a/src/Assembly/WordBounds.v b/src/Assembly/WordBounds.v
new file mode 100644
index 000000000..e05fcb1d4
--- /dev/null
+++ b/src/Assembly/WordBounds.v
@@ -0,0 +1,122 @@
+Require Import Bedrock.Word.
+Import BinNums PArith.BinPos NArith.BinNat NArith.Ndigits.
+
+Definition wordUn (f : N -> N) {sz : nat} (x : word sz) :=
+	NToWord sz (f (wordToN x)).
+Definition wshr {l} n := @wordUn (fun x => N.shiftr x n) l.
+Lemma wshr_test : (wordToN (wshr 3 (NToWord 32 (128- 19)))) = 13%N.
+	reflexivity.
+Qed.
+
+Module WordBoundsExamples.
+  Definition u31 := word 31.
+  Definition U31 := NToWord 31.
+  Definition u64 := word 64.
+  Definition U64 := NToWord 64.
+
+	Definition c2  : u64 := NToWord _  2.
+	Definition c19_31 : u31 := NToWord _ 19.
+	Definition c19 : u64 := NToWord _ 19.
+	Definition c38 : u64 := NToWord _ 38.
+	Definition t25_31 : u31 := NToWord _ (Npos (2^25)).
+	Definition t26_31 : u31 := NToWord _ (Npos (2^26)).
+	Definition t25 : u64 := NToWord _ (Npos (2^25)).
+	Definition t26 : u64 := NToWord _ (Npos (2^26)).
+	Definition t27 : u64 := NToWord _ (Npos (2^26)).
+	Definition m25 : u64 := t25^-(NToWord _ 1).
+	Definition m26 : u64 := t26^-(NToWord _ 1).
+	Definition r25 (hSk hk:u64) : (u64 * u64) := (hSk ^+ wshr 25 hk, wand m25 hk).
+	Definition r26 (hSk hk:u64) : (u64 * u64) := (hSk ^+ wshr 26 hk, wand m26 hk).
+	Definition r25mod (hSk hk:u64) : (u64 * u64) := (hSk ^+ c19^*wshr 25 hk, wand m25 hk).
+
+	Lemma simple_add_rep : forall (a b c d:N),
+		(a < Npos(2^29) -> b < Npos(2^29) -> c < Npos(2^29) -> d < Npos(2^29))%N ->
+		wordToN(U31 a ^+ U31 b ^+ U31 c ^+ U31 d) = (a + b + c + d)%N.
+	Admitted.
+
+	Lemma simple_add_bound : forall (a b c d:u64),
+		a < t25 -> b < t25 -> c < t25 -> d < t25 ->
+		(a ^+ b ^+ c ^+ d) < t27.
+	Admitted.
+
+  (* the bounds can as well be stated in N if the _rep lemma works.
+  I am not sure whether it is a better idea to propagate the bounds in word or
+  in N, though -- proving rep requires propagating bounds for the subexpressions.
+  *)
+
+	Lemma simple_linear_rep : forall (a b:N), (a < Npos(2^25) + Npos(2^26) -> b < Npos(2^25))%N -> 
+		wordToN((U31 a)^*c19_31 ^+ U31 b) = (a*19 + b)%N.
+	Admitted.
+
+	Lemma simple_linear_bound : forall (a b:u31), a < t25_31 ^+ t26_31 -> b < t25_31 -> 
+		a^*c19_31 ^+ b < (NToWord _ 1946157056). (* (2**26+2**25)*19 + 2**25 = 1946157056 *)
+	Admitted.
+
+	Lemma simple_mul_carry_rep : forall (a b c:N), (a < Npos(2^26) -> b < Npos(2^26) -> c < Npos(2^26))%N ->
+		wordToN(wshr 26 (U64 a ^* U64 b) ^+ U64 c) = ((a*b)/(2^26) + c)%N.
+  Admitted.
+
+	Lemma simple_mul_carry_bound : forall (a b c:u64), a < t26 -> b < t26 -> c < t26 ->
+		wshr 26 (a ^* b) ^+ c < t27.
+	Admitted.
+
+	Lemma simple_mul_reduce_rep : forall (a b c:N), (a < Npos(2^26) -> b < Npos(2^26))%N ->
+		wordToN(wand m26 (U64 a ^* U64 b)) = ((a*b) mod (2^26) + c)%N.
+  Admitted.
+
+	Lemma sandy2x_bound : forall
+		(* this example is transcribed by hand from <https://eprint.iacr.org/2015/943.pdf> section 2.2.
+			 it is very representative of the bounds check / absence-of-overflow proofs we actually
+			 want to do. However, given its size, presence of transcription errors is totally plausible.
+       A corresponding _rep proof will also necessary.*)
+		(f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : u64)
+		(g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : u64),
+  	f0 < t26 -> g0 < t26 ->
+  	f1 < t25 -> g1 < t25 ->
+  	f2 < t26 -> g2 < t26 ->
+  	f3 < t25 -> g3 < t25 ->
+  	f4 < t26 -> g4 < t26 ->
+  	f5 < t25 -> g5 < t25 ->
+  	f6 < t26 -> g6 < t26 ->
+  	f7 < t25 -> g7 < t25 ->
+  	f8 < t26 -> g8 < t26 ->
+  	f9 < t25 -> g9 < t25 ->
+
+		let h0 := f0^*g0 ^+ c38^*f1^*g9 ^+ c19^*f2^*g8 ^+  c38^*f3^*g7 ^+ c19^*f4^*g6 ^+ c38^*f5^*g5 ^+ c19^*f6^*g4 ^+ c38^*f7^*g3 ^+ c19^*f8^*g2 ^+ c38^*f9^*g1 in
+		let h1 := f0^*g1 ^+      f1^*g0 ^+ c19^*f2^*g9 ^+  c19^*f3^*g8 ^+ c19^*f4^*g7 ^+ c19^*f5^*g6 ^+ c19^*f6^*g5 ^+ c19^*f7^*g4 ^+ c19^*f8^*g3 ^+ c19^*f9^*g2 in
+		let h2 := f0^*g2 ^+ c2^* f1^*g1 ^+      f2^*g0 ^+  c38^*f3^*g9 ^+ c19^*f4^*g8 ^+ c38^*f5^*g7 ^+ c19^*f6^*g6 ^+ c38^*f7^*g5 ^+ c19^*f8^*g4 ^+ c38^*f9^*g3 in
+		let h3 := f0^*g3 ^+      f1^*g2 ^+      f2^*g1 ^+       f3^*g0 ^+ c19^*f4^*g9 ^+ c19^*f5^*g8 ^+ c19^*f6^*g7 ^+ c19^*f7^*g6 ^+ c19^*f8^*g5 ^+ c19^*f9^*g4 in
+		let h4 := f0^*g4 ^+ c2^* f1^*g3 ^+      f2^*g2 ^+  c2^* f3^*g1 ^+      f4^*g0 ^+ c38^*f5^*g9 ^+ c19^*f6^*g8 ^+ c38^*f7^*g7 ^+ c19^*f8^*g6 ^+ c38^*f9^*g5 in
+		let h5 := f0^*g5 ^+      f1^*g4 ^+      f2^*g3 ^+       f3^*g2 ^+      f4^*g1 ^+      f5^*g0 ^+ c19^*f6^*g9 ^+ c19^*f7^*g8 ^+ c19^*f8^*g7 ^+ c19^*f9^*g6 in
+		let h6 := f0^*g6 ^+ c2^* f1^*g5 ^+      f2^*g4 ^+  c2^* f3^*g3 ^+      f4^*g2 ^+ c2^* f5^*g1 ^+      f6^*g0 ^+ c38^*f7^*g9 ^+ c19^*f8^*g8 ^+ c38^*f9^*g7 in
+		let h7 := f0^*g7 ^+      f1^*g6 ^+      f2^*g5 ^+       f3^*g4 ^+      f4^*g3 ^+      f5^*g2 ^+      f6^*g1 ^+      f7^*g0 ^+ c19^*f8^*g9 ^+ c19^*f9^*g8 in
+		let h8 := f0^*g8 ^+ c2^* f1^*g7 ^+      f2^*g6 ^+  c2^* f3^*g5 ^+      f4^*g4 ^+ c2^* f5^*g3 ^+      f6^*g2 ^+ c2^* f7^*g1 ^+      f8^*g0 ^+ c38^*f9^*g9 in
+		let h9 := f0^*g9 ^+      f1^*g8 ^+      f2^*g7 ^+       f3^*g6 ^+      f4^*g5 ^+      f5^*g4 ^+      f6^*g3 ^+      f7^*g2 ^+      f8^*g1 ^+      f9^*g0 in
+		
+		let (h1_1, h0_1) := r26 h1 h0 in
+		let (h2_1, h1_2) := r25 h2 h1_1 in
+		let (h3_1, h2_2) := r26 h3 h2_1 in
+		let (h4_1, h3_2) := r25 h4 h3_1 in
+
+		let (h6_1, h5_1) := r25 h6 h5 in
+		let (h7_1, h6_2) := r26 h7 h6_1 in
+		let (h8_1, h7_2) := r25 h8 h7_1 in
+		let (h9_1, h8_2) := r26 h9 h8_1 in
+		let (h0_2, h9_2) := r25mod h0_1 h9_1 in
+		let (h1_3, h0_2) := r26 h1_2 h0_1 in
+
+		let (h5_2, h4_2) := r26 h5_1 h4_1 in
+		let (h6_2, h5_3) := r25 h6_1 h5_2 in
+
+  	h0_2 < t26 /\
+  	h1_3 < t27 /\
+  	h2_2 < t26 /\
+  	h3_2 < t25 /\
+  	h4_2 < t26 /\
+  	h5_3 < t25 /\
+  	h6_2 < t27 /\
+  	h7_2 < t25 /\
+  	h8_2 < t26 /\
+  	h9_2 < t25.
+	Admitted.
+End WordBoundsExamples.
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 7af310257..8ab81e0a8 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -66,8 +66,6 @@ Module PointFormats.
     Parameter projY : point -> GF.
     Parameter unifiedAdd : point -> point -> point.
 
-    (* TODO: split module here? *)
-
     Parameter rep : point -> Spec.point -> Prop.
     Local Notation "P '~=' rP" := (rep P rP) (at level 70).
     Axiom mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y.
@@ -78,8 +76,8 @@ Module PointFormats.
   End CompleteTwistedEdwardsPointFormat.
 
   Module CompleteTwistedEdwardsFacts (Import ta:TwistedA) (Import td:TwistedD).
-    Module M := CompleteTwistedEdwardsSpec ta td.
-    Import M.
+    Module Import Spec := CompleteTwistedEdwardsSpec ta td.
+
     Lemma twistedAddCompletePlus : forall (P1 P2:point)
       (oc1:onCurve P1) (oc2:onCurve P2),
       let x1 := projX P1 in
@@ -131,7 +129,7 @@ Module PointFormats.
 
 
   Module CompleteTwistedEdwardsSpecPointFormat (ta:TwistedA) (td:TwistedD)
-      <: (CompleteTwistedEdwardsPointFormat ta td).
+      <: CompleteTwistedEdwardsPointFormat ta td.
     Module Spec := CompleteTwistedEdwardsSpec ta td.
     Definition point := Spec.point.
     Definition mkPoint := Spec.mkPoint.
@@ -178,16 +176,18 @@ Module PointFormats.
     End ta.
     Import ta.
 
-    Module M := CompleteTwistedEdwardsSpec ta td.
+    Module Spec := CompleteTwistedEdwardsSpec ta td.
 
     Module Format <: CompleteTwistedEdwardsPointFormat ta td.
-      Module Spec := CompleteTwistedEdwardsSpec ta td.
+      Module Import Facts := CompleteTwistedEdwardsFacts ta td.
+
       (** [projective] represents a point on an elliptic curve using projective
       * Edwards coordinates for twisted edwards curves with a=-1 (see
       * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html>
       * <https://en.wikipedia.org/wiki/Edwards_curve#Projective_homogeneous_coordinates>) *)
       Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}.
       Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z).
+
       Definition twistedToProjective (P : Spec.point) : projective :=
         let x := Spec.projX P in
         let y := Spec.projY P in
@@ -205,11 +205,6 @@ Module PointFormats.
       Lemma twistedProjectiveInv : forall P,
         projectiveToTwisted (twistedToProjective P) = P.
       Proof.
-    (* FIXME: this is copied from CompleteTwistedEdwardsFacts because I don't know how to get it to be in scope here *)
-    Ltac twisted := autounfold; intros;
-                    repeat match goal with
-                               | [ x : Spec.point |- _ ] => destruct x
-                           end; simpl; repeat (ring || f_equal); field.
         twisted.
       Qed.
 
@@ -246,6 +241,7 @@ Module PointFormats.
       Qed.
 
       Lemma twistedToExtendedValid : forall (P : Spec.point), extendedValid (twistedToExtended P).
+      Proof.
         autounfold.
         destruct P.
         simpl.
@@ -255,6 +251,7 @@ Module PointFormats.
       Definition rep (P:point) (rP:Spec.point) : Prop :=
         extendedToTwisted P = rP /\ extendedValid P.
       Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Spec.mkPoint x y).
+      Proof.
         split.
         apply twistedExtendedInv.
         apply twistedToExtendedValid.
@@ -268,9 +265,11 @@ Module PointFormats.
                                | [ x : rep ?a ?b |- _ ] => destruct x
                                end).
       Lemma projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP.
+      Proof.
         rep.
       Qed.
       Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP.
+      Proof.
         rep.
       Qed.
 
@@ -353,10 +352,13 @@ Module PointFormats.
 
       Lemma unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ ->
         P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ).
+      Proof.
         split; rep.
         apply unifiedAddToTwisted; auto.
         apply unifiedAddCon; auto.
       Qed.
+
+      Module Spec := Spec.
     End Format.
   End Minus1Twisted.
 
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
new file mode 100644
index 000000000..77428e549
--- /dev/null
+++ b/src/Galois/BaseSystem.v
@@ -0,0 +1,386 @@
+Require Import List.
+Require Import Util.ListUtil.
+Require Import ZArith.ZArith ZArith.Zdiv.
+Require Import Omega.
+
+Local Open Scope Z.
+
+Lemma pos_pow_nat_pos : forall x n, 
+  Z.pos x ^ Z.of_nat n > 0.
+  do 2 (intros; induction n; subst; simpl in *; auto with zarith).
+  rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
+  apply Zmult_gt_0_compat; auto; reflexivity.
+Qed.
+
+Module Type BaseCoefs.
+  (** [BaseCoefs] represent the weights of each digit in a positional number system, with the weight of least significant digit presented first. The following requirements on the base are preconditions for using it with BaseSystem. *)
+  Parameter base : list Z.
+  Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too... *)
+  Axiom base_good :
+    forall i j, (i+j < length base)%nat ->
+    let b := nth_default 0 base in
+    let r := (b i * b j) / b (i+j)%nat in
+    b i * b j = r * b (i+j)%nat.
+End BaseCoefs.
+
+Module BaseSystem (Import B:BaseCoefs).
+  (** [BaseSystem] implements an constrained positional number system.
+      A wide variety of bases are supported: the base coefficients are not
+      required to be powers of 2, and it is NOT necessarily the case that
+      $b_{i+j} = b_i b_j$. Implementations of addition and multiplication are
+      provided, with focus on near-optimal multiplication performance on
+      non-trivial but small operands: maybe 10 32-bit integers or so. This
+      module does not handle carries automatically: if no restrictions are put
+      on the use of a [BaseSystem], each digit is unbounded. This has nothing
+      to do with modular arithmetic either.
+  *)
+  Definition digits : Type := list Z.
+
+  Definition accumulate p acc := fst p * snd p + acc.
+  Definition decode' bs u  := fold_right accumulate 0 (combine u bs).
+  Definition decode := decode' base.
+  Hint Unfold accumulate.
+
+  Fixpoint add (us vs:digits) : digits :=
+    match us,vs with
+      | u::us', v::vs' => u+v :: add us' vs'
+      | _, nil => us
+      | _, _ => vs
+    end.
+  Infix ".+" := add (at level 50).
+
+  Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs.
+  Proof.
+    unfold decode', accumulate.
+    induction bs; destruct us; destruct vs; auto; simpl; try rewrite IHbs; ring.
+  Qed.
+
+  Lemma decode_nil : forall bs, decode' bs nil = 0.
+    auto.
+  Qed.
+
+  (* mul_geomseq is a valid multiplication algorithm if b_i = b_1^i *)
+  Fixpoint mul_geomseq (us vs:digits) : digits :=
+    match us,vs with
+      | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs
+      | _, _ => nil
+    end.
+
+  Definition mul_each u := map (Z.mul u).
+  Lemma mul_each_rep : forall bs u vs, decode' bs (mul_each u vs) = u * decode' bs vs.
+  Proof.
+    unfold decode', accumulate.
+    induction bs; destruct vs; auto; simpl; try rewrite IHbs; ring.
+  Qed.
+
+  Definition crosscoef i j : Z := 
+    let b := nth_default 0 base in
+    (b(i) * b(j)) / b(i+j)%nat.
+
+  Fixpoint zeros n := match n with O => nil | S n' => 0::zeros n' end.
+  Lemma zeros_rep : forall bs n, decode' bs (zeros n) = 0.
+    unfold decode', accumulate.
+    induction bs; destruct n; auto; simpl; try rewrite IHbs; ring.
+  Qed.
+  Lemma length_zeros : forall n, length (zeros n) = n.
+    induction n; simpl; auto.
+  Qed.
+
+  Ltac boring :=
+    simpl; intuition;
+    repeat match goal with
+             | [ H : _ |- _ ] => rewrite H; clear H
+             | _ => progress autounfold in *
+             | _ => progress try autorewrite with core
+             | _ => progress simpl in *
+             | _ => progress intuition
+           end; ring || eauto.
+
+  Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m).
+  Proof.
+    induction n; boring.
+  Qed.
+
+  Lemma zeros_app0 : forall m, zeros m ++ 0 :: nil = zeros (S m).
+  Proof.
+    induction m; boring.
+  Qed.
+
+  Hint Rewrite zeros_app0.
+
+  Lemma rev_zeros : forall n, rev (zeros n) = zeros n.
+  Proof.
+    induction n; boring.
+  Qed.
+
+  Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys.
+  Proof.
+    induction xs; boring.
+  Qed.
+
+  (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *)
+  Fixpoint mul_bi' (i:nat) (vsr:digits) := 
+    match vsr with
+    | v::vsr' => v * crosscoef i (length vsr') :: mul_bi' i vsr'
+    | nil => nil
+    end.
+  Definition mul_bi (i:nat) (vs:digits) : digits :=
+    zeros i ++ rev (mul_bi' i (rev vs)).
+
+  Infix ".*" := mul_bi (at level 40).
+
+  (*
+  Definition mul_bi (i:nat) (vs:digits) : digits :=
+    let mkEntry := (fun (p:(nat*Z)) => let (j, v) := p in v * crosscoef i j) in
+    zeros i ++ map mkEntry (@enumerate Z vs).
+  *)
+
+  Hint Unfold nth_default.
+
+  Hint Extern 1 (@eq Z _ _) => ring.
+
+  Lemma decode'_cons : forall x1 x2 xs1 xs2,
+    decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2.
+  Proof.
+    unfold decode'; boring.
+  Qed.
+
+  Hint Rewrite decode'_cons.
+
+  Lemma decode_single : forall n bs x,
+    decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x.
+  Proof.
+    induction n; destruct bs; boring.
+  Qed.
+
+  Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys.
+  Proof.
+    boring.
+  Qed.
+
+  Hint Rewrite zeros_rep peel_decode.
+
+  Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs.
+  Proof.
+    induction xs; destruct bs; boring.
+  Qed.
+
+  Lemma mul_bi_single : forall m n x,
+    (n + m < length base)%nat ->
+    decode (n .* (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n.
+  Proof.
+    unfold mul_bi, decode.
+    destruct m; simpl; ssimpl_list; simpl; intros. {
+      rewrite decode_single.
+      unfold crosscoef; simpl.
+      rewrite plus_0_r.
+      ring_simplify.
+      replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring.
+      rewrite Z_div_mult; try ring.
+
+      apply base_positive.
+      rewrite nth_default_eq.
+      apply nth_In.
+      rewrite plus_0_r in *.
+      auto.
+    } {
+      simpl; ssimpl_list; simpl.
+      replace (mul_bi' n (rev (zeros m) ++ 0 :: nil)) with (zeros (S m)) by admit.
+      intros; simpl; ssimpl_list; simpl.
+      rewrite length_zeros.
+      rewrite app_cons_app_app.
+      rewrite rev_zeros.
+      intros; simpl; ssimpl_list; simpl.
+      rewrite zeros_app0.
+      rewrite app_assoc.
+      rewrite app_zeros_zeros.
+      rewrite decode_single.
+      unfold crosscoef; simpl; ring_simplify.
+      rewrite NPeano.Nat.add_1_r.
+      rewrite base_good by auto.
+      rewrite Z_div_mult.
+      rewrite <- Z.mul_assoc.
+      rewrite <- Z.mul_comm.
+      rewrite <- Z.mul_assoc.
+      rewrite <- Z.mul_assoc.
+      destruct (Z.eq_dec x 0); subst; try ring.
+      rewrite Z.mul_cancel_l by auto.
+      rewrite <- base_good by auto.
+      ring.
+
+      apply base_positive.
+      rewrite nth_default_eq.
+      apply nth_In; auto.
+    }
+  Qed.
+
+  Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil).
+    induction vs; boring; f_equal; ring.
+  Qed.
+
+  Lemma set_higher : forall bs vs x,
+    decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x.
+  Proof.
+    intros.
+    rewrite set_higher'.
+    rewrite add_rep.
+    f_equal.
+    apply decode_single.
+  Qed.
+
+  Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n.
+    induction n; auto.
+    simpl; f_equal; auto. 
+  Qed.
+
+  Lemma mul_bi_add : forall n us vs,
+    n .* (us .+ vs) = n .* us .+ n .* vs.
+  Proof.
+  Admitted.
+
+  Lemma mul_bi_rep : forall i vs,
+    (i + length vs < length base)%nat ->
+    decode (i .* vs) = decode vs * nth_default 0 base i.
+  Proof.
+    unfold decode.
+    induction vs using rev_ind; intros; simpl. {
+      unfold mul_bi, decode.
+      ssimpl_list; rewrite zeros_rep; simpl.
+      unfold decode'; simpl.
+      ring.
+    } {
+      assert (i + length vs < length base)%nat as inbounds. {
+        rewrite app_length in *; simpl in *.
+        rewrite NPeano.Nat.add_1_r, <- plus_n_Sm in *.
+        etransitivity; eauto.
+      }
+
+      rewrite set_higher.
+      ring_simplify.
+      rewrite <- IHvs by auto; clear IHvs.
+      simpl in *.
+      rewrite <- mul_bi_single by auto.
+      rewrite <- add_rep.
+      rewrite <- mul_bi_add.
+      rewrite set_higher'.
+      auto.
+    }
+  Qed.
+
+  (* mul' is multiplication with the FIRST ARGUMENT REVERSED *)
+  Fixpoint mul' (usr vs:digits) : digits :=
+    match usr with
+      | u::usr' => 
+        mul_each u (length usr' .* vs) .+ mul' usr' vs
+      | _ => nil
+    end.
+  Definition mul us := mul' (rev us).
+  Infix "#*" := mul (at level 40).
+
+  Lemma mul'_rep : forall us vs,
+    (length us + length vs <= length base)%nat ->
+    decode (mul' (rev us) vs) = decode us * decode vs.
+  Proof.
+    unfold decode.
+    induction us using rev_ind; intros; simpl; try apply decode_nil.
+
+    assert (length us + length vs < length base)%nat as inbounds. {
+      rewrite app_length in *; simpl in *.
+      rewrite plus_comm in *.
+      rewrite NPeano.Nat.add_1_r, <- plus_n_Sm in *.
+      auto.
+    }
+
+    ssimpl_list.
+    rewrite add_rep.
+    rewrite IHus by (rewrite le_trans; eauto); clear IHus.
+    rewrite set_higher.
+    rewrite mul_each_rep.
+    rewrite mul_bi_rep by auto; unfold decode.
+    ring.
+  Qed.
+
+  Lemma mul_rep : forall us vs,
+    (length us + length vs <= length base)%nat ->
+    decode (us #* vs) = decode us * decode vs.
+  Proof.
+    exact mul'_rep.
+  Qed.
+End BaseSystem.
+
+Module Type PolynomialBaseParams.
+  Parameter b1 : positive. (* the value at which the polynomial is evaluated *)
+  Parameter baseLength : nat. (* 1 + degree of the polynomial *)
+End PolynomialBaseParams.
+
+Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs.
+  (** PolynomialBaseCoeffs generates base vectors for [BaseSystem] using the extra assumption that $b_{i+j} = b_j b_j$. *)
+  Definition bi i := (Zpos b1)^(Z.of_nat i).
+  Definition base := map bi (seq 0 baseLength).
+
+  Lemma base_positive : forall b, In b base -> b > 0.
+  Proof.
+    unfold base.
+    intros until 0; intro H.
+    rewrite in_map_iff in *.
+    destruct H; destruct H.
+    subst.
+    apply pos_pow_nat_pos.
+  Qed.
+
+  Lemma base_good:
+    forall i j, (i + j < length base)%nat ->
+    let b := nth_default 0 base in
+    let r := (b i * b j) / b (i+j)%nat in
+    b i * b j = r * b (i+j)%nat.
+  Proof.
+    unfold base, nth_default; nth_tac.
+
+    clear.
+    unfold bi.
+    rewrite Nat2Z.inj_add, Zpower_exp by
+      (replace 0 with (Z.of_nat 0) by auto; rewrite <- Nat2Z.inj_ge; omega).
+    rewrite Z_div_same_full; try ring.
+    rewrite <- Z.neq_mul_0.
+    split; apply Z.pow_nonzero; try apply Zle_0_nat; try solve [intro H; inversion H].
+  Qed.
+End PolynomialBaseCoefs.
+
+Module BasePoly2Degree32Params <: PolynomialBaseParams.
+  Definition b1 := 2%positive.
+  Definition baseLength := 32%nat.
+End BasePoly2Degree32Params.
+
+Import ListNotations.
+
+Module BaseSystemExample.
+  Module BasePoly2Degree32Coefs := PolynomialBaseCoefs BasePoly2Degree32Params.
+  Module BasePoly2Degree32 := BaseSystem BasePoly2Degree32Coefs.
+  Import BasePoly2Degree32.
+
+  Example three_times_two : [1;1;0] #* [0;1;0] = [0;1;1;0;0].
+  Proof.
+    reflexivity.
+  Qed.
+
+  (* python -c "e = lambda x: '['+''.join(reversed(bin(x)[2:])).replace('1','1;').replace('0','0;')[:-1]+']'; print(e(19259)); print(e(41781))" *)
+  Definition a := [1;1;0;1;1;1;0;0;1;1;0;1;0;0;1].
+  Definition b := [1;0;1;0;1;1;0;0;1;1;0;0;0;1;0;1].
+  Example da : decode a = 19259.
+  Proof.
+    reflexivity.
+  Qed.
+  Example db : decode b = 41781.
+  Proof.
+    reflexivity.
+  Qed.
+  Example encoded_ab :
+    a #*b =[1;1;1;2;2;4;2;2;4;5;3;3;3;6;4;2;5;3;4;3;2;1;2;2;2;0;1;1;0;1].
+  Proof.
+    reflexivity.
+  Qed.
+  Example dab : decode (a #* b) = 804660279.
+  Proof.
+    reflexivity.
+  Qed.
+End BaseSystemExample.
diff --git a/src/Rep/BinGF.v b/src/Rep/BinGF.v
index a19ae788b..138277870 100644
--- a/src/Rep/BinGF.v
+++ b/src/Rep/BinGF.v
@@ -8,6 +8,8 @@ Require Import Eqdep_dec.
 Module Type BitSpec.
   Parameter wordSize: nat.
   Parameter numWords: nat.
+
+  Axiom wordSize_pos : (wordSize > 0)%nat.
 End BitSpec.
 
 Module GFBits (M: Modulus) (Spec: BitSpec).
@@ -20,45 +22,64 @@ Module GFBits (M: Modulus) (Spec: BitSpec).
 
   Definition BinGF := {lst: list (word wordSize) | length lst = numWords}.
 
-  Definition convertWordSize {a b: nat} (x: word a): a = b -> word b.
-    intro H; rewrite H in x; exact x.
-  Defined.
-
-  Lemma convert_invertible:
-    forall (a b: nat) (x: word a) (H1: a = b) (H2: b = a),
-      convertWordSize (convertWordSize x H1) H2 = x.
+  Definition splitGt {n m} {H : (n > m)%nat} (w : word n) : word m * word (n - m).
   Proof.
-    intros; destruct H2; simpl.
-    replace H1 with (eq_refl b); simpl; intuition.
-    apply UIP_dec; exact eq_nat_dec.
-  Qed.
+    refine (let w' := match _ : (n = m + (n - m))%nat in _ = N return word N with
+                     | eq_refl => w
+                     end in
+            (split1 m (n - m) w', split2 m (n - m) w'));
+    abstract omega.
+  Defined.
 
-  Fixpoint splitWords' (sz: nat) (len: nat) (x: word sz): list (word wordSize).
-    induction len, (gt_dec sz wordSize).
+  Fixpoint copies {A} (x : A) (n : nat) : list A :=
+    match n with
+    | O => nil
+    | S n' => x :: copies x n'
+    end.
 
-    - refine nil.
+  Definition splitWords' : forall (len : nat) {sz: nat} (x: word sz), list (word wordSize).
+  Proof.
+    refine (fix splitWords' (len : nat) {sz : nat} (w : word sz) {struct len} : list (word wordSize) :=
+              match len with
+              | O => nil
+              | S len' =>
+                if gt_dec sz wordSize
+                then let (w1, w2) := splitGt w in
+                     w1 :: splitWords' len' w2
+                else match _ in _ = N return list (word N) with
+                      | eq_refl => zext w (wordSize - sz) :: copies (wzero _) len'
+                     end
+              end)%nat; clear splitWords'; abstract omega.
+  Defined.
 
-    - refine nil.
+  Lemma length_cast : forall A (F : A -> Type) x1 x2 (pf : x1 = x2) x xs,
+    length (match pf in _ = X return list (F X) with
+            | eq_refl => x :: xs
+            end) = S (length xs).
+  Proof.
+    destruct pf; auto.
+  Qed.
 
-    - assert (sz = wordSize + (sz - wordSize))%nat. intuition.
-      assert (z := convertWordSize x H).
-      refine (
-        cons (split1 wordSize (sz - wordSize) z)
-             (splitWords' (sz - wordSize)%nat len
-               (split2 wordSize (sz - wordSize) z))).
+  Lemma length_copies : forall A (x : A) n, length (copies x n) = n.
+  Proof.
+    induction n; simpl; auto.
+  Qed.
 
-    - assert (sz + (wordSize - sz) = wordSize)%nat. intuition.
-      assert (z := convertWordSize (zext x (wordSize - sz)) H).
-      refine (cons z nil).
+  Hint Rewrite length_cast length_copies.
 
-  Admitted.
+  Lemma length_splitWords' : forall len sz (w : word sz), length (splitWords' len w) = len.
+  Proof.
+    induction len; simpl; intuition;
+    match goal with
+    | [ |- context[match ?E with _ => _ end] ] => destruct E
+    end; simpl; try rewrite IHlen; autorewrite with core; reflexivity.
+  Qed.    
 
   Definition splitWords {sz} (len: nat) (x: word sz):
-      {x: list (word wordSize) | length x = len}.
-    exists (splitWords' sz len x).
-
-    induction len, (gt_dec sz wordSize).
-  Admitted.
+    {x: list (word wordSize) | length x = len}.
+  Proof.
+    exists (splitWords' len x); apply length_splitWords'.
+  Defined.
 
   Definition splitGF (x: GF) :=
     splitWords numWords (NToWord (numWords * wordSize)%nat (Z.to_N (proj1_sig x))).
@@ -116,4 +137,3 @@ Module GFBits (M: Modulus) (Spec: BitSpec).
   }.
 
 End GFBits.
-
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
new file mode 100644
index 000000000..5604ebcc3
--- /dev/null
+++ b/src/Util/ListUtil.v
@@ -0,0 +1,84 @@
+Require Import List.
+Require Import Omega.
+Require Import Arith.Peano_dec.
+
+Ltac nth_tac' := 
+  intros; simpl in *; unfold error,value in *; repeat progress (match goal with
+    | [  |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros
+    | [ |- context[(if lt_dec ?a ?b then _ else _) = _] ] => destruct (lt_dec a b)
+    | [ |- context[_ = (if lt_dec ?a ?b then _ else _)] ] => destruct (lt_dec a b)
+    | [ H: context[(if lt_dec ?a ?b then _ else _) = _] |- _ ] => destruct (lt_dec a b)
+    | [ H: context[_ = (if lt_dec ?a ?b then _ else _)] |- _ ] => destruct (lt_dec a b)
+    | [ H: _ /\ _ |- _ ] => destruct H
+    | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst
+    | [ H: None = Some _  |- _ ] => inversion H
+    | [ H: Some _ = None |- _ ] => inversion H
+    | [ |- Some _ = Some _ ] => apply f_equal
+  end); eauto; try (autorewrite with list in *); try omega; eauto.
+Lemma nth_error_map : forall A B (f:A->B) i xs y,
+  nth_error (map f xs) i = Some y ->
+  exists x, nth_error xs i = Some x /\ f x = y.
+Proof.
+  induction i; destruct xs; nth_tac'.
+Qed.
+
+Lemma nth_error_seq : forall i start len,
+  nth_error (seq start len) i =
+  if lt_dec i len
+  then Some (start + i)
+  else None.
+  induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'.
+Qed.
+
+Lemma nth_error_length_error : forall A i (xs:list A), nth_error xs i = None ->
+  i >= length xs.
+Proof.
+  induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega.
+Qed.
+
+Ltac nth_tac := 
+  repeat progress (try nth_tac'; try (match goal with
+    | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H
+    | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H
+    | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H
+  end)).
+
+Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys.
+Proof.
+  induction xs; simpl; repeat match goal with
+           | [ H : _ |- _ ] => rewrite H; clear H
+           | _ => progress intuition
+         end; eauto.
+Qed.
+
+(* xs[n] := x *)
+Fixpoint set_nth {T} n x (xs:list T) {struct n} :=
+	match n with
+	| O => match xs with
+				 | nil => nil
+				 | x'::xs' => x::xs'
+				 end
+	| S n' =>  match xs with
+				 | nil => nil
+				 | x'::xs' => x'::set_nth n' x xs'
+				 end
+  end.
+
+Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) (x x':T),
+  nth_error (set_nth m x xs) n =
+  if eq_nat_dec n m
+  then (if lt_dec n (length xs) then Some x else None)
+  else nth_error xs n.
+Proof.
+	induction m.
+
+	destruct n, xs; auto.
+
+	intros; destruct xs, n; auto.
+	simpl; unfold error; match goal with
+		[ |- None = if ?x then None else None ] => destruct x
+	end; auto.
+
+	simpl nth_error; erewrite IHm by auto; clear IHm.
+	destruct (eq_nat_dec n m), (eq_nat_dec (S n) (S m)); nth_tac.
+Qed.