Merge branch 'master' of github.mit.edu:plv/fiat-crypto

13 files changed, 579 insertions, 270 deletions

diff --git a/src/Assembly/AsmComputation.v b/src/Assembly/Asm.v
index e2186df81..e2186df81 100644
--- a/src/Assembly/AsmComputation.v
+++ b/src/Assembly/Asm.v
diff --git a/src/Assembly/Computation.v b/src/Assembly/Computation.v
new file mode 100644
index 000000000..33af0974e
--- /dev/null
+++ b/src/Assembly/Computation.v
@@ -0,0 +1,175 @@
+
+Require Import EqNat Peano_dec.
+Require Import Bedrock.Word.
+
+(* Very basic definitions *)
+
+Definition wordSize := 32.
+
+Definition Name := nat.
+
+Definition WordCount := nat.
+
+Definition WordList (words: WordCount) :=
+  {x: list (word wordSize) | length x = words}.
+
+Inductive Pointer :=
+  | ListPtr: forall n, WordList n -> Pointer.
+
+Definition TypeBindings := Name -> option WordCount.
+
+Definition Bindings := Name -> option Pointer.
+
+(* Primary inductive language definitions *)
+
+Inductive CTerm (words: WordCount) :=
+  | CConst : WordList words -> CTerm words
+  | CVar : Name -> CTerm words
+  | CConcat: forall t1 t2, t1 + t2 = words -> CTerm t1 -> CTerm t2 -> CTerm words
+  | CHead: forall n: nat, gt n words -> CTerm n -> CTerm words
+  | CTail: forall n: nat, gt n words -> CTerm n -> CTerm words.
+
+Inductive CExpr (words: WordCount) :=
+  | CLift : (CTerm words) -> (CExpr words)
+  | CNot : (CExpr words) -> (CExpr words)
+  | COpp : (CExpr words) -> (CExpr words)
+  | COr : (CExpr words) -> (CExpr words) -> (CExpr words)
+  | CAnd : (CExpr words) -> (CExpr words) -> (CExpr words)
+  | CXor : (CExpr words) -> (CExpr words) -> (CExpr words)
+  | CRShift : forall n: nat, (CExpr words) -> (CExpr words)
+  | CLShift : forall n: nat, (CExpr words) -> (CExpr words)
+  | CPlus : (CExpr words) -> (CExpr words) -> (CExpr words)
+  | CMinus : (CExpr words) -> (CExpr words) -> (CExpr words)
+  | CMult : forall n: nat,  n*2 = words ->
+      (CExpr n) -> (CExpr n) -> (CExpr words)
+  | CDiv : (CExpr words) -> (CExpr words) -> (CExpr words)
+  | CMod : (CExpr words) -> (CExpr words) -> (CExpr words).
+
+Definition bindType (name: Name) (type: WordCount) (bindings: TypeBindings)
+    : Name -> option WordCount :=
+  fun x => if (beq_nat x name) then Some type else bindings x.
+
+Inductive Sub (inputs: TypeBindings) (output: WordCount) :=
+  | CRet : CExpr output -> Sub inputs output 
+  | CCompose : forall resultName resultSize,
+           inputs resultName = None
+        -> (Sub inputs resultSize)
+        -> (Sub (bindType resultName resultSize inputs) output)
+        -> (Sub inputs output)
+  | CIte : (Sub inputs 1)    (* condition *)
+        -> (Sub inputs output)  (* then *)
+        -> (Sub inputs output)  (* else *)
+        -> (Sub inputs output)
+  | CLet : forall (name: Name) (n: WordCount),
+            CExpr n
+        -> (Sub (bindType name n inputs) output)
+        -> (Sub inputs output)
+  | CRepeat : forall (bindOutputTo: Name) (n: nat),
+           inputs bindOutputTo <> None
+        -> (Sub (bindType bindOutputTo output inputs) output)
+        -> (Sub inputs output).
+
+(* Some simple option-monad sugar *)
+
+Definition optionReturn {A} (x : A) := Some x.
+ 
+Definition optionBind {A B} (a : option A) (f : A -> option B) : option B :=
+  match a with
+  | Some x => f x
+  | None => None
+  end.
+
+Notation "'do' A <- B ; C" := (optionBind B (fun A => C))
+    (at level 200, X ident, A at level 100, B at level 200).
+
+Definition optionType {n m} (w: WordList n): option (WordList m).
+  destruct (eq_nat_dec n m);
+  abstract (try rewrite e in *; first [exact (Some w) | exact None]).
+Defined.
+
+Definition wordListConcat {t1 t2 words}:
+    t1 + t2 = words -> WordList t1 -> WordList t2 -> WordList words.
+  intros; exists ((proj1_sig H0) ++ (proj1_sig H1))%list.
+  abstract (destruct H0, H1; simpl;
+    rewrite List.app_length; intuition).
+Defined.
+
+Definition wordListHead {n words}:
+    gt n words -> WordList n -> WordList words.
+  intros; exists (List.firstn words (proj1_sig H0)).
+  abstract (destruct H0; simpl;
+    rewrite List.firstn_length; intuition).
+Defined.
+
+Lemma skipnLength: forall A m (x: list A),
+  ge (length x) m ->
+  length (List.skipn m x) = length x - m.
+Proof.
+  intros; assert (length x = length (List.firstn m x ++ List.skipn m x)%list).
+  - rewrite List.firstn_skipn; trivial.
+  - rewrite H0; rewrite List.app_length; rewrite List.firstn_length.
+    replace (min m (length x)) with m; try rewrite min_l; intuition.
+Qed.
+
+Definition wordListTail {n words}:
+    gt n words -> WordList n -> WordList words.
+  intros; exists (List.skipn (n - words) (proj1_sig H0)).
+  abstract (destruct H0; simpl;
+    rewrite skipnLength; rewrite e; intuition).
+Defined.
+
+(* Now some basic evaluation routines *)
+
+Fixpoint evalTerm {n} (bindings: Bindings) (term: CTerm n):
+    option (WordList n) :=
+  match term with
+  | CConst lst => Some lst
+  | CVar name =>
+      do p <- bindings name ;
+      match p with
+      | ListPtr m lst => optionType lst
+      end
+  | CConcat t1 t2 pf term1 term2 =>
+      do a <- evalTerm bindings term1;
+      do b <- evalTerm bindings term2;
+      Some (wordListConcat pf a b)%list
+  | CHead n pf t =>
+      do x <- evalTerm bindings t;
+      Some (wordListHead pf x)
+  | CTail n pf t =>
+      do x <- evalTerm bindings t;
+      Some (wordListTail pf x)
+  end.
+
+Fixpoint evalExpr {n} (expr: CExpr n): option (word n) :=
+  match expr with
+  | CLift term => None
+  | CNot a => None
+  | COpp a => None
+  | COr a b =>
+      do x <- evalExpr a;
+      do y <- evalExpr b;
+      Some (x |^ y)%word
+  | CAnd a b => None
+  | CXor a b => None
+  | CRShift shift a => None
+  | CLShift shift a => None
+  | CPlus a b => None
+  | CMinus a b => None
+  | CMult _ _ a b => None
+  | CDiv a b => None
+  | CMod a b => None
+  end.
+
+Fixpoint evalSub (inputs: Name -> option WordCount) (output: WordCount) (sub: Sub inputs output)
+    : word output :=
+  match sub with
+  | CRet e => natToWord output 0
+  | CCompose resName resSize _ a b => natToWord output 0
+  | CIte cond thenSub elseSub => natToWord output 0
+  | CLet name wordCount expr inside => natToWord output 0
+  | CRepeat inName times _ inside => natToWord output 0
+  end.
+
+(* Equivalence Lemmas *)
+
diff --git a/src/Assembly/ConstrainedComputation.v b/src/Assembly/ConstrainedComputation.v
deleted file mode 100644
index f36b75187..000000000
--- a/src/Assembly/ConstrainedComputation.v
+++ /dev/null
@@ -1,154 +0,0 @@
-
-Require Import Bedrock.Word.
-
-(* THEORY: if we permit operations on joined types, we can represent
- *         vector operations without searching *)
-Inductive CType: Set :=
-  | Int32: CType
-  | Int64: CType
-  | Join: CType -> CType -> CType .
-
-Definition cTypeToWord(type: CType): Type :=
-  match type with
-  | Int32 => word 32
-  | Int64 => word 64
-  | Join a b => (cTypeToWord a) * (cTypeToWord b)
-  end.
-
-Definition bits(type: CType): nat :=
-  match type with
-  | Int32 => 32
-  | Int64 => 64
-  | Join a b => (bits a) + (bits b)
-  end.
-
-Inductive UnaryOp :=
-  | CNot | COpp.
-
-Inductive BinaryOp :=
-  | CPlus | CMinus  | CMult
-  | CDiv  | CAnd    | COr
-  | CXor  | CRShift | CLShift.
-
-Inductive CTerm (type: CType) :=
-  | CConst : (word (bits type)) -> (CTerm type)
-  | CVar : Name -> CTerm type
-  | CJoin : forall t1 t2, CTerm t1 -> CTerm t2 -> CTerm (Join t1 t2)
-  | CLeft : CTerm (Join type _) -> CTerm type
-  | CRight : CTerm (Join _ type) -> CTerm type.
-
-Inductive CExpr (type: CType) :=
-  | TermExpr : (CTerm type) -> (CExpr type)
-  | UnaryExpr : UnaryOp -> (CTerm type) -> (CExpr type)
-  | BinaryExpr : BinaryOp -> (CTerm type) -> (CTerm type) -> (CExpr type).
-
-Inductive Sub (inType: CType) (outType: CType) :=
-  | CRet : Expr outType -> Sub inType outType
-  | CCompose : forall medType,
-           (Sub inType medType)
-        -> (Sub medType outType)
-        -> (Sub inType outType)
-  | CIte : (Sub inType Int32)    (* condition *)
-        -> (Sub inType outType)  (* then *)
-        -> (Sub inType outType)  (* else *)
-        -> (Sub inType outType)
-  | CLet : Name -> CTerm ->
-        -> (Sub inType outType)
-        -> (Sub inType outType).
-
-Definition bindTerm {valueType objectType} (var: Name) (value: CTerm valueType) (object: CTerm objectType): CTerm objectType :=
-  match valueType with
-  | objectType =>
-    match object with
-    | CConst _ => object
-    | CVar name => if (name = var) then value else object end
-    | CJoin left right =>
-        CJoin (bindTerm var value left) (bindTerm var value right)
-    | CLeft from => CLeft (bindTerm var value larger)
-    | CRight from => CRight (bindTerm var value larger)
-    end
-  | _ => object.
-
-Definition bindExpr {valueType objectType} (var: Name) (value: CTerm valueType) (object: CExpr objectType): CExpr objectType :=
-  match object with
-  | TermExpr term => TermExpr (bindTerm var value term)
-  | UnaryExpr op term => UnaryExpr op (bindTerm var value term)
-  | BinaryExpr op term1 term2 =>
-      BinaryExpr op (bindTerm var value term1) (bindTerm var value term2)
-  end.
-
-Definition bind {valueType fromType toType} (var: Name) (value: CTerm) (object: Sub fromType toType): Sub fromType toType :=
-  match object with
-  | CRet expr => CRet (bindExpr var value expr)
-  | CCompose left right =>
-      CCompose (bind var value left) (bind var value right)
-  | CIte cond thenSub elseSub =>
-      CIte (bind var value cond)
-           (bind var value thenSub)
-           (bind var value elseSub)
-  | CLet name bindTo sub =>
-      CLet name bindTo (bind var value sub)
-  end.
-
-Inductive TermEquiv {t} (left: CTerm t) (right: (cTypeToWord t)) :=
-  | EquivInt32: forall (w: (word (bits Int32))), TermEquiv (CConst w) w
-  | EquivInt64: forall (w: (word (bits Int64))), TermEquiv (CConst w) w
-  | EquivJoin: forall aComp bComp aGallina bGallina,
-      TermEquiv aComp aGallina
-   -> TermEquiv bComp bGallina
-   -> TermEquiv (CJoin aComp bComp) (aGallina, bGallina)
-  | EquivLeft: forall aComp aGallina,
-      TermEquiv aComp aGallina
-   -> TermEquiv (CLeft aComp) (fst aGallina)
-  | EquivRight: forall aComp aGallina,
-      TermEquiv aComp aGallina
-   -> TermEquiv (CRight aComp) (snd aGallina).
-
-Definition applyBinaryOp {n: nat} (op: UnaryOp) (a b: word n) :=
-  match op with
-  | CPlus => Word.plus a b
-  | CMinus => Word.minus a b
-  | CMult => Word.mult a b
-  | CDiv => Word.div a b
-  | CAnd => Word.and a b
-  | COr => Word.or a b
-  | CXor => Word.xor a b
-  | CRShift => Word.rshift a b
-  | CLShift => Word.lshift a b
-  end.
-
-Definition applyUnaryOp {n: nat} (op: UnaryOp) (w: word n) :=
-  match op with
-  | CNot => Word.not w
-  | COpp => Word.opp w
-  end.
-
-Inductive ExprEquiv {t} (left: CExpr t) (right: (cTypeToWord t)) :=
-  | EquivNop: forall aComp aGallina,
-      TermEquiv aComp aGallina
-   -> ExprEquiv (TermExpr aComp) aGallina
-  | EquivNot: forall aComp aGallina op,
-      TermEquiv aComp aGallina
-   -> ExprEquiv (UnaryExpr op aComp) (applyUnaryOp op aGallina)
-  | EquivPlus: forall aComp aGallina bComp bGallina op,
-      TermEquiv aComp aGallina
-   -> TermEquiv bComp bGallina
-   -> ExprEquiv (BinaryExpr op aComp bComp) (applyBinaryOp aGallina bGallina).
-
-Inductive SubEquiv {fromType toType} (left: Sub fromType toType) (right: (cTypeToWord fromType) -> (cTypeToWord toType)) :=
-  | EquivRet: forall aComp aGallina,
-      ExprEquiv aComp aGallina
-   -> SubEquiv (CRet aComp) (fun x => aGallina)
-  | EquivComp: forall fComp fGallina gComp gGallina,
-      SubEquiv fComp fGallina
-   -> SubEquiv gComp gGallina
-   -> SubEquiv (CCompose fComp gComp) (fun x => gGallina (fGallina x))
-  | EquivIte: forall (fComp: Sub fromType Int32) fGallina gComp gGallina,
-      SubEquiv fComp fGallina
-   -> SubEquiv gComp gGallina
-   -> SubEquiv hComp hGallina
-   -> SubEquiv (CIte fComp gComp hComp)
-        (fun x => if (neq 0 (fGallina x)) then gGallina x else hGallina x)
-  | EquivLet: forall name bindTo sub fGallina,
-      SubEquiv (bind name bindTo sub) fGallina
-   -> SubEquiv (CLet name bindTo sub) fGallina.
diff --git a/src/Assembly/ConstrainedDSL.v b/src/Assembly/DSL.v
index 2cb07a5d4..2cb07a5d4 100644
--- a/src/Assembly/ConstrainedDSL.v
+++ b/src/Assembly/DSL.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 baa6bd2a7..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.
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index b9821ded0..835cea5f9 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -1,52 +1,13 @@
 Require Import List.
+Require Import Util.ListUtil.
 Require Import ZArith.ZArith ZArith.Zdiv.
 Require Import Omega.
 
-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)
-    | [ 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)).
-
 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).
-  SearchAbout Pos.succ.
   rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
   apply Zmult_gt_0_compat; auto; reflexivity.
 Qed.
diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v
index 35faf3f03..f649701b7 100644
--- a/src/Galois/GaloisExamples.v
+++ b/src/Galois/GaloisExamples.v
@@ -1,8 +1,7 @@
 
 Require Import Zpower ZArith Znumtheory.
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
-Require Import Crypto.Galois.ComputationalGaloisField.
-Require Import Crypto.Galois.AbstractGaloisField.
+Require Import Crypto.Galois.ZGaloisField.
 
 Definition two_5_1 := (two_p 5) - 1.
 Lemma two_5_1_prime : prime two_5_1.
@@ -21,9 +20,8 @@ Module Modulus127_1 <: Modulus.
 End Modulus127_1.
 
 Module Example31.
-  Module Field := Galois Modulus31.
-  Module Theory := ComputationalGaloisField Modulus31.
-  Import Modulus31 Theory Field.
+  Module Theory := ZGaloisField Modulus31.
+  Import Theory.
   Local Open Scope GF_scope.
 
   Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2).
@@ -32,13 +30,13 @@ Module Example31.
     field; trivial.
   Qed.
 
-  Lemma example2: forall x: GF, x * (ZToGF 2) = x + x.
+  Lemma example2: forall x: GF, x * (inject 2) = x + x.
   Proof.
     intros; simpl.
     field.
   Qed.
 
-  Lemma example3: forall x: GF, x ^ 2 + (ZToGF 2) * x + (ZToGF 1) = (x + (ZToGF 1)) ^ 2.
+  Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2.
   Proof.
     intros; simpl.
     field; trivial.
@@ -47,8 +45,8 @@ Module Example31.
 End Example31.
 
 Module TimesZeroTransparentTestModule.
-  Module Theory := ComputationalGaloisField Modulus127_1.
-  Import Modulus127_1 Theory Theory.Field.
+  Module Theory := ZGaloisField Modulus127_1.
+  Import Theory.
   Local Open Scope GF_scope.
 
   Lemma timesZero : forall a, a*0 = 0.
@@ -58,13 +56,12 @@ Module TimesZeroTransparentTestModule.
 End TimesZeroTransparentTestModule.
 
 Module TimesZeroParametricTestModule (M: Modulus).
-  Module Theory := AbstractGaloisField M.
-  Import M Theory Theory.Field.
+  Module Theory := ZGaloisField M.
+  Import Theory.
   Local Open Scope GF_scope.
 
   Lemma timesZero : forall a, a*0 = 0.
     intros.
     field.
-    ring. (* field doesn't work but ring does :) *)
   Qed.
 End TimesZeroParametricTestModule.
diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v
index e95eed864..8fa1b4113 100644
--- a/src/Galois/GaloisTheory.v
+++ b/src/Galois/GaloisTheory.v
@@ -158,14 +158,7 @@ Module GaloisTheory (M: Modulus).
 
   (* Ring properties *)
 
-  Ltac GFexp_tac t :=
-    match t with
-    | Z0 => N0
-    | Zpos ?n => Ncst (Npos n)
-    | Z_of_N ?n => Ncst n
-    | NtoZ ?n => Ncst n
-    | _ => NotConstant
-    end.
+  Ltac GFexp_tac t := Ncst t.
 
   Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y.
   Proof.
diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v
index 23b1c8dd8..bf9efa964 100644
--- a/src/Galois/ZGaloisField.v
+++ b/src/Galois/ZGaloisField.v
@@ -1,6 +1,6 @@
 
 Require Import BinInt BinNat ZArith Znumtheory.
-Require Import BoolEq.
+Require Import BoolEq Field_theory.
 Require Import Galois GaloisTheory.
 
 Module ZGaloisField (M: Modulus).
@@ -26,13 +26,59 @@ Module ZGaloisField (M: Modulus).
       symmetry; apply Zeq_bool_eq; trivial.
   Qed.
 
+  Lemma GFmorph_div_theory: 
+      div_theory eq Zplus Zmult inject Z.quotrem.
+  Proof.
+    constructor; intros; intuition.
+    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
+      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+
+    eq_remove_proofs; demod;
+      rewrite <- (Z.quot_rem' a b);
+      destruct a; simpl; trivial.
+  Qed.
+
+  Lemma injectZeroIsGFZero :
+    GFzero = inject 0.
+  Proof.
+    apply gf_eq; simpl; trivial.
+  Qed.
+
+  Lemma injectOneIsGFOne :
+    GFone = inject 1.
+  Proof.
+    apply gf_eq; simpl; intuition.
+    symmetry; apply Zmod_small; destruct modulus; simpl;
+      apply prime_ge_2 in p; intuition.
+  Qed.
+
+  Ltac GFpreprocess :=
+    repeat rewrite injectZeroIsGFZero;
+    repeat rewrite injectOneIsGFOne.
+
+  Ltac GFpostprocess :=
+    repeat rewrite <- injectZeroIsGFZero;
+    repeat rewrite <- injectOneIsGFOne.
+
+  Ltac GFconstant t :=
+    match t with
+    | inject ?x => x
+    | _ => NotConstant
+    end.
+
   Add Ring GFring_Z : GFring_theory
     (morphism GFring_morph,
+     constants [GFconstant],
+     div GFmorph_div_theory,
      power_tac GFpower_theory [GFexp_tac]).
 
   Add Field GFfield_Z : GFfield_theory
     (morphism GFring_morph,
-     power_tac GFpower_theory [GFexp_tac]).
+     preprocess [GFpreprocess],
+     postprocess [GFpostprocess],
+     constants [GFconstant],
+     div GFmorph_div_theory,
+     power_tac GFpower_theory [GFexp_tac]). 
 
 End ZGaloisField.
 
diff --git a/src/Rep/BinGF.v b/src/Rep/BinGF.v
new file mode 100644
index 000000000..138277870
--- /dev/null
+++ b/src/Rep/BinGF.v
@@ -0,0 +1,139 @@
+
+Require Import ZArith.
+Require Import Bedrock.Word.
+Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
+Require Import Crypto.Galois.ZGaloisField.
+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).
+  Module Field := ZGaloisField M.
+  Import Field Spec.
+  Local Open Scope GF_scope.
+  Local Open Scope list.
+
+  Definition bits {k} (x: word k) := k.
+
+  Definition BinGF := {lst: list (word wordSize) | length lst = numWords}.
+
+  Definition splitGt {n m} {H : (n > m)%nat} (w : word n) : word m * word (n - m).
+  Proof.
+    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 copies {A} (x : A) (n : nat) : list A :=
+    match n with
+    | O => nil
+    | S n' => x :: copies x n'
+    end.
+
+  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.
+
+  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.
+
+  Lemma length_copies : forall A (x : A) n, length (copies x n) = n.
+  Proof.
+    induction n; simpl; auto.
+  Qed.
+
+  Hint Rewrite length_cast length_copies.
+
+  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}.
+  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))).
+
+  Fixpoint combineAll' (b: list (word wordSize)): word (wordSize * (length b)).
+    induction b.
+
+    - simpl.
+      replace (wordSize * 0)%nat with 0%nat; intuition.
+      exact (natToWord 0 0).
+
+    - replace (wordSize * length (a :: b))%nat
+        with (wordSize + wordSize * length b)%nat.
+      + exact (combine a IHb).
+      + simpl; rewrite mult_succ_r; intuition.
+  Defined.
+
+  Definition combineAll (b: BinGF): GF :=
+    inject (Z.of_N (wordToN (combineAll' (proj1_sig b)))).
+
+  Definition binEquiv a b := combineAll a = combineAll b.
+
+  Lemma combine_split:
+    forall (x: GF) (len: nat),
+    combineAll (splitGF x) = x.
+  Admitted.
+
+  Record unaryOp: Set := mkUnary {
+    f : GF -> GF;
+    binF : BinGF -> BinGF;
+
+    unaryCompat : forall (a b: GF),
+      a = b -> f a = f b;
+
+    unaryBinCompat : forall (a b: BinGF),
+      binEquiv a b -> binEquiv (binF a) (binF b);
+
+    unaryCorrect: forall (a: GF),
+      f a = combineAll (binF (splitGF a))
+  }.
+
+  Record binaryOp: Set := mkBinary {
+    g : GF -> GF -> GF;
+    binG : BinGF -> BinGF -> BinGF;
+
+    binaryCompat : forall (a b c d: GF),
+      a = b -> c = d -> g a c = g b d;
+
+    binaryBinCompat : forall (a b c d: BinGF),
+      binEquiv a b -> binEquiv c d ->
+      binEquiv (binG a c) (binG b d);
+
+    binaryCorrect: forall (a b: GF),
+      g a b = combineAll (binG (splitGF a) (splitGF b))
+  }.
+
+End GFBits.
diff --git a/src/Rep/WordEquivalence.v b/src/Rep/WordEquivalence.v
deleted file mode 100644
index 4005adc2a..000000000
--- a/src/Rep/WordEquivalence.v
+++ /dev/null
@@ -1,52 +0,0 @@
-
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
-
-Module GFBits (M: Modulus).
-  Module T := GaloisTheory Modulus31.
-  Import M T T.Field.
-  Local Open Scope GF_scope.
-
-  Definition wordSize: nat := 32.
-  Definition bits {k} (word k) := k.
-
-  (* I think we shouldn't fix this, but rather have a lemma for how
-   * many bits we need to represent a given prime *)
-  Definition numWords: nat :=
-    let b := (bits (NtoWord (Z.to_N modulus)))
-    in (1 + b / 32)%nat.
-
-  Definition BinGF :=
-    {lst: list (word wordSize) | length lst = numWords}.
-
-  Fixpoint splitWords {sz} (len: nat) (x: word sz): {x: list (word wordSize) | length x = len} :=
-    match len with
-    | O => []
-    | S len' =>
-      if(sz - wordSize >? 0)
-      then Cons (split1 wordSize (sz - wordSize) x)
-                (splitWords len' (split2 wordSize (sz - wordSize) x))
-      else zext x wordSize
-    end.
-
-  Fixpoint combineAll (b: BinGF) :=
-    match (proj1_sig b) with
-    | [] => natToWord 0
-    | Cons x xs => combine x (combineAll xs)
-    end.
-
-  wordEq a b := wordToN (combineAll a) = wordToN (combineAll b)
-
-  Definition toZ (b: BinGF) := Z.of_N (wordToN (combineAll b)).
-  Definition toGF (b: BinGF) := ZToGF ((toZ b) mod modulus)
-
-  Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x))
-  Definition fromGF (x: GF) := fromZ (proj1_sig x).
-
-  toZ a + toZ b = toZ (a ^+ b)
-  
-  Lemma equivalent_GF : BinEquiv x y <-> x = toGF y.
-  Admitted.
-
-  Lemma equivalent_word : BinEquiv x y <-> weq y (fromGF x).
-  Admitted.
-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.