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

8 files changed, 420 insertions, 735 deletions

diff --git a/src/Assembly/Asm.v b/src/Assembly/Asm.v
deleted file mode 100644
index e2186df81..000000000
--- a/src/Assembly/Asm.v
+++ /dev/null
@@ -1,66 +0,0 @@
-
-Require Export Bedrock.Word.
-
-Inductive AsmType: Set :=
-  | Int32    | Int64
-  | Float80  | Int128
-  | Pointer.
-
-Definition Name := String.
-
-Inductive AsmVar (type: AsmType) :=
-  | StackAsmVar : Name -> AsmVar
-  | MemoryAsmVar : Name -> AsmVar
-  | Register : Name -> AsmVar.
-
-Definition bits (type: AsmType): nat :=
-  match type with
-  | Int32 => 32
-  | Int64 => 64
-  | Float80 => 80
-  | Int128 => 128
-  | Pointer => 64
-  end.
-
-Definition isDouble (a b: AsmType): Prop :=
-  match (a, b) with
-  | (Int32, Int64) => True
-  | (Int64, Int128) => True
-  | _ => False
-  end.
-
-Inductive UnaryOp :=
-  | AsmId | AsmNot | AsmOpp.
-
-Inductive BinaryOp :=
-  | AsmPlus | AsmMinus  | AsmMult
-  | AsmDiv  | AsmAnd    | AsmOr
-  | AsmXor  | AsmRShift | AsmLShift.
-
-Inductive AsmTerm (type: AsmType) :=
-  | AsmConst : (word (bits type)) -> (AsmTerm type)
-  | AsmVarTerm : AsmVar type -> AsmTerm type
-  | AsmRef: AsmVar type -> AsmTerm Pointer
-  | AsmDeref: AsmVar Pointer -> AsmTerm type.
-
-Inductive AsmExpr (type: AsmType) :=
-  | Unary : UnaryOp -> (AsmTerm type) -> (AsmExpr type)
-  | Binary : BinaryOp -> (AsmTerm type) -> (AsmTerm type) -> (AsmExpr type).
-
-Inductive AsmComputation :=
-  | AsmDeclare : forall t, AsmVar t -> AsmComputation
-  | AsmSet : forall t, AsmVar t -> Expr t -> AsmComputation
-  | AsmDestruct : forall t1 t2,
-    isDouble t1 t2 -> AsmVar t1 -> AsmVar t1 -> AsmExpr t2
-      -> Unit.
-  | AsmConstruct : forall t1 t2,
-    isDouble t1 t2 -> AsmVar t2 -> AsmExpr t1 -> AsmExpr t1
-      -> Unit.
-  | AsmSeq : AsmComputation -> AsmComputation -> AsmComputation
-  | AsmLabel : String -> AsmComputation -> AsmComputation
-  | AsmGoto : String -> AsmComputation
-  | AsmIf : forall t, (AsmTerm t) -> AsmComputation -> AsmComputation.
-
-Inductive AsmSub :=
-  | Asm: forall t,
-    list ((AsmVar t) * (AsmTerm t)) -> AsmComputation -> AsmTerm t.
diff --git a/src/Assembly/AsmDSL.v b/src/Assembly/AsmDSL.v
deleted file mode 100644
index 791b07391..000000000
--- a/src/Assembly/AsmDSL.v
+++ /dev/null
@@ -1,34 +0,0 @@
-
-Require Import AsmComputation.
-
-Notation "stack32 A" := StackAsmVar A.
-Notation "int32 A" := MemoryAsmVar A.
-Notation "reg32 A" := Register A.
-
-Notation "{{ A }}" := AsmConst A.
-
-Notation "** A" := AsmRef A.
-Notation "&& A" := AsmDeref A.
-
-Notation "~ A" := Unary AsmNot A.
-Notation "- A" := Unary AsmOpp A.
-Notation "A + B" := Binary AsmPlus A B.
-Notation "A - B" := Binary AsmMinus A B.
-Notation "A * B" := Binary AsmMult A B.
-Notation "A / B" := Binary AsmDiv A B.
-Notation "A & B" := Binary AsmAnd A B.
-Notation "A | B" := Binary AsmOr A B.
-Notation "A ^ B" := Binary AsmXor A B.
-Notation "A >> B" := Binary AsmRShift A B.
-Notation "A << B" := Binary AsmLShift A B.
-
-Notation "declare A" := AsmDeclare A
-Notation "A ::= B" := AsmSet A B
-Notation "(A B) =:= C" := AsmDestruct A B C
-Notation "A =:= (B C)" := AsmConstruct A B C
-Notation "A ;; B" := AsmSeq A B
-Notation "A :: B" := AsmLabel A B
-Notation "goto A" := AsmGoto A
-Notation "A ? B" := AsmIf A B
-
-Notation "enter A do B" := Asm A B
diff --git a/src/Assembly/Computation.v b/src/Assembly/Computation.v
deleted file mode 100644
index 33af0974e..000000000
--- a/src/Assembly/Computation.v
+++ /dev/null
@@ -1,175 +0,0 @@
-
-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/DSL.v b/src/Assembly/DSL.v
deleted file mode 100644
index 2cb07a5d4..000000000
--- a/src/Assembly/DSL.v
+++ /dev/null
@@ -1,28 +0,0 @@
-
-Require Export ConstrainedComputation.
-
-Notation "const A" := CConst A.
-Notation "var A" := CVar A.
-Notation "A : B" := CJoin A B.
-Notation "left A" := CLeft A.
-Notation "right A" := CRight A.
-
-Notation "~ A" := UnaryExpr CNot A.
-Notation "- A" := UnaryExpr COpp A.
-Notation "A + B" := BinaryExpr CPlus A B.
-Notation "A - B" := BinaryExpr CMinus A B.
-Notation "A * B" := BinaryExpr CMult A B.
-Notation "A / B" := BinaryExpr CDiv A B.
-Notation "A & B" := BinaryExpr CAnd A B.
-Notation "A | B" := BinaryExpr COr A B.
-Notation "A ^ B" := BinaryExpr CXor A B.
-Notation "A >> B" := BinaryExpr CRShift A B.
-Notation "A << B" := BinaryExpr CLShift A B.
-
-Definition toExpr {type} (term: CTerm type) = TermExpr term.
-Coersion toExpr: {type} CTerm type >-> CExpr type.
-
-Notation "ret A" := CRet A
-Notation "A . B" := CCompose A B
-Notation "A ? B : C" := CIte A B C
-Notation "set A to B in C" := CLet A B C
diff --git a/src/Assembly/WordBounds.v b/src/Assembly/WordBounds.v
deleted file mode 100644
index e05fcb1d4..000000000
--- a/src/Assembly/WordBounds.v
+++ /dev/null
@@ -1,122 +0,0 @@
-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 a11c4dce6..4e36cca11 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -221,9 +221,6 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     onCurve (x2, y2) ->
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
-    (* TODO: this proof was made inconsistent by an actually
-             correct version of root_nonzero. This adds the necessary
-             hypothesis*)
     unfold onCurve; intuition; whatsNotZero.
 
     pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
@@ -296,7 +293,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Defined.
   Local Hint Unfold onCurve mkPoint.
 
-  Definition zero : point. exists (0, 1).
+  Definition zero : point. refine (mkPoint (0, 1) _).
     abstract (unfold onCurve; field).
   Defined.
 
@@ -356,6 +353,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     let 'exist P2' pf2 := P2 in
     mkPoint (unifiedAdd' P1' P2') (unifiedAdd'_onCurve' _ _ pf1 pf2).
   Local Infix "+" := unifiedAdd.
+  SearchAbout Pos.iter_op.
 
   Fixpoint scalarMult (n:nat) (P : point) : point :=
     match n with
@@ -429,8 +427,12 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
   Qed.
 
   Lemma zeroIsIdentity : forall P, P + zero = P.
-    (* Should follow from zeroIsIdentity', but dependent types... *)
-  Admitted.
+  Proof.
+    unfold zero, unifiedAdd.
+    destruct P as [[x y] pf].
+    simpl.
+    apply point_eq; field; auto.
+  Qed.
   Hint Resolve zeroIsIdentity.
 
   Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P).
@@ -676,7 +678,7 @@ Module ExtendedM1 (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEd
         pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H;
         match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
       ) || (
-        pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as Hm;
+        pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H;
         match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
       ); repeat apply mul_nonzero_nonzero; auto 10
     end.
diff --git a/src/Scratch/fermat.v b/src/Scratch/fermat.v
deleted file mode 100644
index 947ffce15..000000000
--- a/src/Scratch/fermat.v
+++ /dev/null
@@ -1,185 +0,0 @@
-Require Import NPeano.
-Require Import List.
-Require Import Sorting.Permutation.
-Require Import BinInt.
-Require Import Util.ListUtil.
-Require Znumtheory.
-
-Lemma all_neq_NoDup : forall {T} (xs:list T),
-  (forall i j x y,
-  nth_error xs i = Some x ->
-  nth_error xs j = Some y ->
-  i <> j -> x <> y) <->  NoDup xs.
-Admitted.
-
-Definition F (q:nat) := { n : nat | n = n mod q}.
- 
-Section Fq.
-  Context {q : nat}.
-  Axiom q_prime : Znumtheory.prime (Z.of_nat q).
-  Let Fq := F q.
-
-  Lemma q_is_succ : q = S (q-1). Admitted.
-
-  Definition natToField (n:nat) : Fq. exists (n mod q). abstract admit. Defined.
-  Definition fieldToNat (n:Fq) : nat := proj1_sig n.
-  Coercion fieldToNat : Fq >-> nat.
-
-  Definition zero : Fq. exists 0. abstract admit. Defined.
-  Definition one : Fq. exists 1. abstract admit. Defined.
-
-  Definition add (a b: Fq) : Fq.  exists (a+b mod q); abstract admit. Defined.
-  Infix "+" := add.
-  Definition mul (a b: Fq) : Fq.  exists (a*b mod q); abstract admit. Defined.
-  Infix "*" := mul.
-  Definition pow (a:Fq) (n:nat) : Fq. exists (pow a n mod q). abstract admit. Defined.
-  Infix "^" := pow.
-
-  Axiom opp : Fq -> Fq.
-  Axiom opp_spec : forall a, opp a + a = zero.
-  Definition sub a b := add a (opp b).
-  Infix "-" := sub.
-
-  Axiom inv : Fq -> Fq.
-  Axiom inv_spec : forall a, inv a * a = one.
-  Definition div a b := mul a (inv b).
-  Infix "/" := div.
-
-  Fixpoint replicate {T} n (x:T) : list T := match n with O => nil | S n' => x::replicate n' x end.
-  Definition prod := fold_right mul one.
-
-  Lemma mul_one_l : forall a, one * a = a. Admitted.
-  Lemma mul_one_r : forall a, a * one = a. Admitted.
-
-  Lemma mul_cancel_l : forall a, a <> zero -> forall b c, a * b = a * c -> b = c. Admitted.
-  Lemma mul_cancel_r : forall a, a <> zero -> forall b c, b * a = c * c -> b = c. Admitted.
-  Lemma mul_cancel_l_1 : forall a, a <> zero -> forall b, a * b = a -> b = one. Admitted.
-  Lemma mul_cancel_r_1 : forall a, a <> zero -> forall b, b * a = a -> b = one. Admitted.
-  
-  Lemma mul_0_why : forall a b, a * b = zero -> a = zero \/ b = zero. Admitted.
-
-  Lemma mul_assoc : forall a b c, a * (b * c) = a * b * c. Admitted.
-  Lemma mul_assoc_pairs' : forall a b c d, (a * b) * (c * d) = a * (c * (b * d)). Admitted.
-
-  Lemma div_cancel : forall a, a <> zero -> forall b c, b / a = c / a -> b = c. Admitted.
-  Lemma div_cancel_neq : forall a, a <> zero -> forall b c, b / a <> c / a -> b <> c. Admitted.
-
-  Lemma div_mul : forall a, a <> zero -> forall b, (a * b) / a = b. Admitted.
-
-  Hint Resolve mul_assoc.
-  Hint Rewrite div_mul.
-
-  Lemma pow_zero : forall (n:nat), zero^n = zero. Admitted.
-
-  Lemma pow_S : forall a n, a ^ S n = a * a ^ n. Admitted.
-
-  Lemma prod_replicate : forall a n, a ^ n = prod (replicate n a). Admitted.
-
-  Lemma prod_perm : forall xs ys, Permutation xs ys -> prod xs = prod ys. Admitted.
-
-  Hint Resolve pow_zero mul_one_l mul_one_r prod_replicate.
-
-
-  Definition F_eq_dec : forall (a b:Fq), {a = b} + {a <> b}. Admitted.
-
-  Definition elements : list Fq := map natToField (seq 0 q).
-  Lemma elements_all : forall (a:Fq), In a elements. Admitted.
-  Lemma elements_unique : forall (a:Fq), NoDup elements. Admitted.
-  Lemma length_elements : length elements = q. Admitted.
-
-  Definition invertibles : list Fq := map natToField (seq 1 (q-1)%nat).
-  Lemma invertibles_all : forall (a:Fq), a <> zero -> In a invertibles. Admitted.
-  Lemma invertibles_unique : NoDup invertibles. Admitted.
-  Lemma prod_invertibles_nonzero : prod invertibles <> zero. Admitted.
-  Lemma length_invertibles : length invertibles = (q-1)%nat. Admitted.
-
-  Hint Resolve invertibles_unique.
-
-  Section FermatsLittleTheorem.
-    Variable a : Fq.
-    Axiom a_nonzero : a <> zero.
-    Hint Resolve a_nonzero.
-
-    Definition bag := map (mul a) invertibles.
-    Lemma bag_unique : NoDup bag.
-    Proof.
-      unfold bag; intros.
-      eapply all_neq_NoDup; intros.
-      eapply div_cancel_neq; eauto.
-      eapply all_neq_NoDup; eauto;
-      match goal with
-      | [H: nth_error (map _ _) ?i = Some _ |- _ ] =>
-        destruct (nth_error_map _ _ _ _ _ _ H) as [t [HtIn HtEq]]; rewrite <- HtEq; autorewrite with core; auto
-      end.
-    Qed.
-
-    Lemma bag_invertibles : forall b, b <> zero -> In b bag.
-    Proof.
-      unfold bag; intros.
-      assert (b/a <> zero) as Hdnz by admit.
-      replace b with (a * (b/a)) by admit.
-      destruct (In_nth_error_value _ _ (invertibles_all _ Hdnz)).
-      eauto using nth_error_value_In, map_nth_error.
-    Qed.
-
-    Lemma In_bag_equiv_In_invertibles : forall b, In b bag <-> In b invertibles.
-    Proof.
-      unfold bag; intros.
-      case (F_eq_dec b zero); intuition; subst;
-          eauto using invertibles_all, bag_invertibles;
-          repeat progress match goal with
-          | [ H : In _ (map _ _) |- _ ] => rewrite in_map_iff in H; destruct H;
-              pose proof a_nonzero; intuition
-          | [ H : ?a * ?b = zero |- _ ] => destruct (mul_0_why a b H); clear H;
-              intuition; try solve [subst; auto]
-          end.
-      assert (In zero invertibles -> In zero (map (mul a) invertibles)) by admit; auto.
-    Qed.
-
-    Lemma bag_perm_elements : Permutation bag invertibles.
-    Proof.
-      eauto using NoDup_Permutation, bag_unique, invertibles_unique, In_bag_equiv_In_invertibles.
-    Qed.
-
-    Hint Resolve prod_perm bag_perm_elements.
-    Lemma prod_bag_ref : prod bag = prod invertibles.
-    Proof.
-      auto.
-    Qed.
-
-    Lemma prod_bag_interspersed : prod (flat_map (fun b => a::b::nil) invertibles) = prod invertibles.
-    Proof.
-      intros.
-      rewrite <- prod_bag_ref.
-      unfold bag.
-      induction invertibles; auto; simpl.
-      rewrite IHl.
-      auto.
-    Qed.
-
-    Lemma prod_bag_sorted : prod (replicate (q-1)%nat a) * prod invertibles = prod invertibles.
-      rewrite <- length_invertibles.
-      rewrite <- prod_bag_interspersed at 2.
-      induction invertibles; auto; simpl.
-      rewrite mul_assoc_pairs'; repeat f_equal; auto.
-    Qed.
-      
-    Theorem fermat' : a <> zero -> a^(q-1) = one.
-    Proof.
-      rewrite prod_replicate; eauto using mul_cancel_r_1, prod_bag_sorted, prod_invertibles_nonzero.
-    Qed.
-  End FermatsLittleTheorem.
-
-  Theorem fermat (a:Fq) : a^q = a.
-  Proof.
-    case (F_eq_dec a zero); intros; subst; auto.
-    rewrite q_is_succ, pow_S, fermat'; auto.
-  Qed.
-End Fq.
-Arguments fermat' : default implicits.
-Arguments fermat : default implicits.
-Arguments elements : default implicits.
-Arguments invertibles : default implicits.
-
-Print Assumptions fermat.
-Check fermat.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 4b06e5230..732779a1a 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -6,7 +6,7 @@ Require Import QArith.QArith QArith.Qround.
 Require Import VerdiTactics.
 Close Scope Q.
 
-Ltac twoIndices i j base := 
+Ltac twoIndices i j base :=
     intros;
     assert (In i (seq 0 (length base))) by nth_tac;
     assert (In j (seq 0 (length base))) by nth_tac;
@@ -15,7 +15,9 @@ Ltac twoIndices i j base :=
 
 Module Base25Point5_10limbs <: BaseCoefs.
   Local Open Scope Z_scope.
-  Definition base := map (fun i => two_p (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10).
+  Definition log_base := Eval compute in map (fun i => (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10).
+  Definition base := map (fun x => 2 ^ x) log_base.
+
   Lemma base_positive : forall b, In b base -> b > 0.
   Proof.
     compute; intuition; subst; intuition.
@@ -71,7 +73,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
     twoIndices i j base.
   Qed.
 
-  Lemma base_succ : forall i, ((S i) < length base)%nat -> 
+  Lemma base_succ : forall i, ((S i) < length base)%nat ->
     let b := nth_default 0 base in
     b (S i) mod b i = 0.
   Proof.
@@ -93,139 +95,433 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
   Proof.
     rewrite Zle_is_le_bool; auto.
   Qed.
+
+  Lemma base_range : forall i, 0 <= nth_default 0 log_base i <= k.
+  Proof.
+    intros i.
+    destruct (lt_dec i (length log_base)) as [H|H].
+    { repeat (destruct i as [|i]; [cbv; intuition; discriminate|simpl in H; try omega]). }
+    { rewrite nth_default_eq, nth_overflow by omega. cbv. intuition; discriminate. }
+  Qed.
+
+  Lemma base_monotonic: forall i : nat, (i < pred (length log_base))%nat ->
+      (0 <= nth_default 0 log_base i <= nth_default 0 log_base (S i)).
+  Proof.
+  intros i H.
+  repeat (destruct i; [cbv; intuition; congruence|]); 
+      contradict H; cbv; firstorder.
+  Qed.      
 End GF25519Base25Point5Params.
 
 Module GF25519Base25Point5 := GFPseudoMersenneBase Base25Point5_10limbs Modulus25519 GF25519Base25Point5Params.
 
-Ltac expand_list ls :=
-  let Hlen := fresh "Hlen" in
-  match goal with [H: ls = ?lsdef |- _ ] =>
-      assert (Hlen:length ls=length lsdef) by (f_equal; exact H)
-  end;
-  simpl in Hlen;
-  repeat progress (let n:=fresh ls in destruct ls as [|n ]; try solve [revert Hlen; clear; discriminate]);
-  clear Hlen.
+Section GF25519Base25Point5Formula.
+  Import GF25519Base25Point5 Base25Point5_10limbs GF25519Base25Point5 GF25519Base25Point5Params.
+  Import Field.
+
+Definition Z_add_opt := Eval compute in Z.add.
+Definition Z_sub_opt := Eval compute in Z.sub.
+Definition Z_mul_opt := Eval compute in Z.mul.
+Definition Z_div_opt := Eval compute in Z.div.
+Definition Z_pow_opt := Eval compute in Z.pow.
 
-Ltac letify r :=
+Definition nth_default_opt {A} := Eval compute in @nth_default A.
+Definition map_opt {A B} := Eval compute in @map A B.
+
+Ltac opt_step :=
   match goal with
-  | [ H' : r = _ |- _ ] =>
-    match goal with
-    | [ H : ?x = ?e |- _ ] =>
-      is_var x;
-      match goal with (* only letify equations that appear nowhere other than r *)
-      | _ => clear H H' x; fail 1
-      | _ => fail 2
-      end || idtac;
-      pattern x in H';
-      match type of H' with
-      | (fun z => r = @?e' z) x =>
-        let H'' := fresh "H" in
-        assert (H'' : r = let x := e in e' x) by
-          (* congruence is slower for every subsequent letify *)
-          (rewrite H'; subst x; reflexivity);
-        clear H'; subst x; rename H'' into H'; cbv beta in H'
-      end
-    end
+  | [ |- _ = match ?e with nil => _ | _ => _ end :> ?T ]
+    => refine (_ : match e with nil => _ | _ => _ end = _);
+       destruct e
   end.
 
-Ltac expand_list_equalities := repeat match goal with
-  | [H: (?x::?xs = ?y::?ys) |- _ ] =>
-      let eq_head := fresh "Heq" x in
-      assert (x = y) as eq_head by (eauto using cons_eq_head);
-      assert (xs = ys) by (eauto using cons_eq_tail);
-      clear H
-  | [H:?x = ?x|-_] => clear H
-end.
+Definition E_mul_bi'_step
+           (mul_bi' : nat -> E.digits -> list Z)
+           (i : nat) (vsr : E.digits)
+  : list Z
+  := match vsr with
+     | [] => []
+     | v :: vsr' => (v * E.crosscoef i (length vsr'))%Z :: mul_bi' i vsr'
+     end.
 
-Section GF25519Base25Point5Formula.
-  Import GF25519Base25Point5.
-  Import Field.
+Definition E_mul_bi'_opt_step_sig
+           (mul_bi' : nat -> E.digits -> list Z)
+           (i : nat) (vsr : E.digits)
+  : { l : list Z | l = E_mul_bi'_step mul_bi' i vsr }.
+Proof.
+  eexists.
+  cbv [E_mul_bi'_step].
+  opt_step.
+  { reflexivity. }
+  { cbv [E.crosscoef EC.base Base25Point5_10limbs.base].
+    change Z.div with Z_div_opt.
+    change Z.pow with Z_pow_opt.
+    change Z.mul with Z_mul_opt at 2 3 4 5.
+    change @nth_default with @nth_default_opt.
+    change @map with @map_opt.
+    reflexivity. }
+Defined.
+
+Definition E_mul_bi'_opt_step
+           (mul_bi' : nat -> E.digits -> list Z)
+           (i : nat) (vsr : E.digits)
+  : list Z
+  := Eval cbv [proj1_sig E_mul_bi'_opt_step_sig] in
+      proj1_sig (E_mul_bi'_opt_step_sig mul_bi' i vsr).
+
+Fixpoint E_mul_bi'_opt
+         (i : nat) (vsr : E.digits) {struct vsr}
+  : list Z
+  := E_mul_bi'_opt_step E_mul_bi'_opt i vsr.
+
+Definition E_mul_bi'_opt_correct
+           (i : nat) (vsr : E.digits)
+  : E_mul_bi'_opt i vsr = E.mul_bi' i vsr.
+Proof.
+  revert i; induction vsr as [|vsr vsrs IHvsr]; intros.
+  { reflexivity. }
+  { simpl E.mul_bi'.
+    rewrite <- IHvsr; clear IHvsr.
+    unfold E_mul_bi'_opt, E_mul_bi'_opt_step.
+    apply f_equal2; [ | reflexivity ].
+    cbv [E.crosscoef EC.base Base25Point5_10limbs.base].
+    change Z.div with Z_div_opt.
+    change Z.pow with Z_pow_opt.
+    change Z.mul with Z_mul_opt at 2.
+    change @nth_default with @nth_default_opt.
+    change @map with @map_opt.
+    reflexivity. }
+Qed.
+
+Definition E_mul'_step
+           (mul' : E.digits -> E.digits -> E.digits)
+           (usr vs : E.digits)
+  : E.digits
+  := match usr with
+     | [] => []
+     | u :: usr' => E.add (E.mul_each u (E.mul_bi (length usr') vs)) (mul' usr' vs)
+     end.
+
+Definition E_mul'_opt_step_sig
+           (mul' : E.digits -> E.digits -> E.digits)
+           (usr vs : E.digits)
+  : { d : E.digits | d = E_mul'_step mul' usr vs }.
+Proof.
+  eexists.
+  cbv [E_mul'_step].
+  match goal with
+  | [ |- _ = match ?e with nil => _ | _ => _ end :> ?T ]
+    => refine (_ : match e with nil => _ | _ => _ end = _);
+         destruct e
+  end.
+  { reflexivity. }
+  { cbv [E.mul_each E.mul_bi].
+    rewrite <- E_mul_bi'_opt_correct.
+    reflexivity. }
+Defined.
+
+Definition E_mul'_opt_step
+           (mul' : E.digits -> E.digits -> E.digits)
+           (usr vs : E.digits)
+  : E.digits
+  := Eval cbv [proj1_sig E_mul'_opt_step_sig] in proj1_sig (E_mul'_opt_step_sig mul' usr vs).
+
+Fixpoint E_mul'_opt
+         (usr vs : E.digits)
+  : E.digits
+  := E_mul'_opt_step E_mul'_opt usr vs.
+
+Definition E_mul'_opt_correct
+         (usr vs : E.digits)
+  : E_mul'_opt usr vs = E.mul' usr vs.
+Proof.
+  revert vs; induction usr as [|usr usrs IHusr]; intros.
+  { reflexivity. }
+  { simpl.
+    rewrite <- IHusr; clear IHusr.
+    apply f_equal2; [ | reflexivity ].
+    cbv [E.mul_each E.mul_bi].
+    rewrite <- E_mul_bi'_opt_correct.
+    reflexivity. }
+Qed.
+
+Definition mul_opt_sig (us vs : T) : { b : B.digits | b = mul us vs }.
+Proof.
+  eexists.
+  cbv [mul E.mul E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base reduce].
+  rewrite <- E_mul'_opt_correct.
+  reflexivity.
+Defined.
+
+Definition mul_opt (us vs : T) : B.digits
+  := Eval cbv [proj1_sig mul_opt_sig] in proj1_sig (mul_opt_sig us vs).
+
+Definition mul_opt_correct us vs
+  : mul_opt us vs = mul us vs
+  := proj2_sig (mul_opt_sig us vs).
+
+Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R)
+  : (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b).
+Proof.
+  destruct (eq_nat_dec x y) as [H|H];
+    [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
+    | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
+Qed.
+
+Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A)
+  : (if b then f x else g x) = (if b then f else g) x.
+Proof.
+  destruct b; reflexivity.
+Qed.
 
-  Hint Rewrite
-    Z.mul_0_l
-    Z.mul_0_r
-    Z.mul_1_l
-    Z.mul_1_r
-    Z.add_0_l
-    Z.add_0_r
-    Z.add_assoc
-    Z.mul_assoc
-    : Z_identities.
-
-  Ltac deriveModularMultiplicationWithCarries carryscript :=
-  let h := fresh "h" in
-  let fg := fresh "fg" in
-  let Hfg := fresh "Hfg" in
-  intros;
-  repeat match goal with
-  | [ Hf: rep ?fs ?f, Hg: rep ?gs ?g |- rep _ ?ret ] =>
-      remember (carry_sequence carryscript (mul fs gs)) as fg;
-      assert (rep fg ret) as Hfg; [subst fg; apply carry_sequence_rep, mul_rep; eauto|]
-  | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition)
-  | [ Heqfg: fg = carry_sequence _ (mul _ _) |- rep _ ?ret ] =>
-      (* expand bignum multiplication *)
-      cbv [plus
-        seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
-        mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c
-        E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg;
-      repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *)
-          let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end;
-      autorewrite with Z_identities in Heqfg;
-      (* speparate out carries *)
-      match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end;
-      (* one equation per limb *)
-      expand_list h; expand_list_equalities;
-      (* expand carry *)
-      cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg
-  | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a
-  | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *)
-      let cr := fresh "cr" in
-      remember (carry i (x::xs)) as cr in Hfg;
-      match goal with [ Heq : cr = ?crdef |- _ ] =>
-          (* is there any simpler way to do this? *)
-          cbv [carry carry_simple carry_and_reduce] in Heq;
-          simpl eq_nat_dec in Heq; cbv iota beta in Heq;
-          cbv [set_nth nth_default nth_error value add_to_nth] in Heq;
-          expand_list cr; expand_list_equalities
-      end
-  | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H;
-      match goal with [Heqc: c = cap i |- _ ] =>
-          (* is there any simpler way to do this? *)
-          unfold cap, Base25Point5_10limbs.base in Heqc;
-          simpl eq_nat_dec in Heqc;
-          cbv [nth_default nth_error value error] in Heqc;
-          simpl map in Heqc;
-          cbv [GF25519Base25Point5Params.k] in Heqc
-      end;
-      subst c;
-      repeat rewrite Zdiv_1_r in H;
-      repeat rewrite two_power_pos_equiv in H;
-      repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder));
-      repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity));
-      repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity));
-      simpl Z.sub in H;
-      unfold  GF25519Base25Point5Params.c in H
-  | [H: context[Z.ones ?l] |- _ ] =>
-          (* postponing this to the main loop makes the autorewrite slow *)
-        let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c
-  | [ |- _ ] => abstract (solve [auto])
-  | [ |- _ ] => progress intros
+Lemma map_nth_default_always {A B} (f : A -> B) (n : nat) (x : A) (l : list A)
+  : nth_default (f x) (map f l) n = f (nth_default x l n).
+Proof.
+  revert n; induction l; simpl; intro n; destruct n; [ try reflexivity.. ].
+  nth_tac.
+Qed.
+
+Definition log_cap_opt_sig
+           (i : nat)
+  : { z : Z | i < length (Base25Point5_10limbs.log_base) -> (2^z)%Z = cap i }.
+Proof.
+  eexists.
+  cbv [cap Base25Point5_10limbs.base].
+  intros.
+  rewrite map_length in *.
+  About map_nth_default.
+  erewrite map_nth_default; [|assumption].
+  instantiate (2 := 0%Z).
+  (** For the division of maps of (2 ^ _) over lists, replace it with 2 ^ (_ - _) *)
+  
+  lazymatch goal with
+  | [ |- _ = (if eq_nat_dec ?a ?b then (2^?x/2^?y)%Z else (nth_default 0 (map (fun x => (2^x)%Z) ?ls) ?si / 2^?d)%Z)  ]
+    => transitivity (2^if eq_nat_dec a b then (x-y)%Z else nth_default 0 ls si - d)%Z;
+        [ apply f_equal | break_if ]
+  end.
+  
+  Focus 2.
+  apply Z.pow_sub_r; [clear;firstorder|apply base_range].
+  Focus 2.
+  erewrite map_nth_default by (omega); instantiate (1 := 0%Z).
+  rewrite <- Z.pow_sub_r; [ reflexivity | .. ].
+    { clear; abstract firstorder. }
+    { apply base_monotonic. omega. }
+  Unfocus.
+  rewrite <-beq_nat_eq_nat_dec.
+  change Z.sub with Z_sub_opt.
+  change @nth_default with @nth_default_opt.
+  change @map with @map_opt.
+  reflexivity.
+Defined.
+
+Definition log_cap_opt (i : nat)
+  := Eval cbv [proj1_sig log_cap_opt_sig] in proj1_sig (log_cap_opt_sig i).
+
+Definition log_cap_opt_correct (i : nat)
+  : i < length Base25Point5_10limbs.log_base -> (2^log_cap_opt i = cap i)%Z
+  := proj2_sig (log_cap_opt_sig i).
+
+Definition carry_opt_sig
+           (i : nat) (b : B.digits)
+  : { d : B.digits | i < length Base25Point5_10limbs.log_base -> d = carry i b }.
+Proof.
+  eexists ; intros.
+  cbv [carry].
+  rewrite <- pull_app_if_sumbool.
+  cbv beta delta [carry_and_reduce carry_simple add_to_nth Base25Point5_10limbs.base].
+  rewrite map_length.
+  repeat lazymatch goal with
+         | [ |- context[cap ?i] ]
+           => replace (cap i) with (2^log_cap_opt i)%Z by (apply log_cap_opt_correct; assumption)
+  end.
+  lazymatch goal with
+  | [ |- _ = (if ?br then ?c else ?d) ]
+    => let x := fresh "x" in let y := fresh "y" in evar (x:B.digits); evar (y:B.digits); transitivity (if br then x else y); subst x; subst y
+  end.
+  Focus 2.
+  cbv zeta.
+  break_if;
+    rewrite <- Z.land_ones, <- Z.shiftr_div_pow2 by (
+        pose proof (base_range i); pose proof (base_monotonic i);
+        change @nth_default with @nth_default_opt in *;
+        cbv beta delta [log_cap_opt]; rewrite beq_nat_eq_nat_dec; break_if; change Z_sub_opt with Z.sub; omega);
+    reflexivity.
+  change @nth_default with @nth_default_opt.
+  change @map with @map_opt.
+  rewrite <- @beq_nat_eq_nat_dec.
+  reflexivity.
+Defined.
+
+Definition carry_opt i b
+  := Eval cbv beta iota delta [proj1_sig carry_opt_sig] in proj1_sig (carry_opt_sig i b).
+
+Definition carry_opt_correct i b : i < length Base25Point5_10limbs.log_base -> carry_opt i b = carry i b := proj2_sig (carry_opt_sig i b).
+
+Definition carry_sequence_opt_sig (is : list nat) (us : B.digits)
+  : { b : B.digits | (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> b = carry_sequence is us }.
+Proof.
+  eexists. intros H.
+  cbv [carry_sequence].
+  transitivity (fold_right carry_opt us is).
+  Focus 2.
+  { induction is; [ reflexivity | ].
+    simpl; rewrite IHis, carry_opt_correct.
+    - reflexivity.
+    - apply H; apply in_eq.
+    - intros. apply H. right. auto.
+    }
+  Unfocus.
+  reflexivity.
+Defined.
+
+Definition carry_sequence_opt is us := Eval cbv [proj1_sig carry_sequence_opt_sig] in
+                                        proj1_sig (carry_sequence_opt_sig is us).
+
+Definition carry_sequence_opt_correct is us
+  : (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> carry_sequence_opt is us = carry_sequence is us
+  := proj2_sig (carry_sequence_opt_sig is us).
+
+Definition Let_In {A P} (x : A) (f : forall y : A, P y)
+  := let y := x in f y.
+
+Definition carry_opt_cps_sig
+           {T}
+           (i : nat)
+           (f : B.digits -> T)
+           (b : B.digits)
+  : { d : T |  i < length Base25Point5_10limbs.log_base -> d = f (carry i b) }.
+Proof.
+  eexists. intros H.
+  rewrite <- carry_opt_correct by assumption.
+  cbv beta iota delta [carry_opt].
+  (* TODO: how to match the goal here? Alternatively, rewrite under let binders in carry_opt_sig and remove cbv zeta and restore original match from jgross's commit *)
+  lazymatch goal with [ |- ?LHS = _ ] =>
+  change (LHS = Let_In (nth_default_opt 0%Z b i) (fun di => (f (if beq_nat i (pred (length Base25Point5_10limbs.log_base))
+      then
+       set_nth 0
+         (c *
+          Z.shiftr (di) (log_cap_opt i) +
+          nth_default_opt 0
+            (set_nth i (Z.land di (Z.ones (log_cap_opt i)))
+               b) 0)%Z
+         (set_nth i (Z.land (nth_default_opt 0%Z b i) (Z.ones (log_cap_opt i))) b)
+      else
+       set_nth (S i)
+         (Z.shiftr (di) (log_cap_opt i) +
+          nth_default_opt 0
+            (set_nth i (Z.land (di) (Z.ones (log_cap_opt i)))
+               b) (S i))%Z
+         (set_nth i (Z.land (nth_default_opt 0%Z b i) (Z.ones (log_cap_opt i))) b)))))
   end.
+  reflexivity.
+Defined.
+
+Definition carry_opt_cps {T} i f b
+  := Eval cbv beta iota delta [proj1_sig carry_opt_cps_sig] in proj1_sig (@carry_opt_cps_sig T i f b).
+
+Definition carry_opt_cps_correct {T} i f b :
+  i < length Base25Point5_10limbs.log_base ->
+  @carry_opt_cps T i f b = f (carry i b)
+  := proj2_sig (carry_opt_cps_sig i f b).
+
+Definition carry_sequence_opt_cps_sig (is : list nat) (us : B.digits)
+  : { b : B.digits | (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> b = carry_sequence is us }.
+Proof.
+  eexists.
+  cbv [carry_sequence].
+  transitivity (fold_right carry_opt_cps id (List.rev is) us).
+  Focus 2.
+  { 
+    assert (forall i, In i (rev is) -> i < length Base25Point5_10limbs.log_base) as Hr. {
+      subst. intros. rewrite <- in_rev in *. auto. }
+    remember (rev is) as ris eqn:Heq.
+    rewrite <- (rev_involutive is), <- Heq.
+    clear H Heq is.
+    rewrite fold_left_rev_right.
+    revert us; induction ris; [ reflexivity | ]; intros.
+    { simpl.
+      rewrite <- IHris; clear IHris; [|intros; apply Hr; right; assumption].
+      rewrite carry_opt_cps_correct; [reflexivity|].
+      apply Hr; left; reflexivity.
+      } }
+  Unfocus.
+  reflexivity.
+Defined.
+
+Definition carry_sequence_opt_cps is us := Eval cbv [proj1_sig carry_sequence_opt_cps_sig] in
+                                            proj1_sig (carry_sequence_opt_cps_sig is us).
+
+Definition carry_sequence_opt_cps_correct is us
+  : (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> carry_sequence_opt_cps is us = carry_sequence is us
+  := proj2_sig (carry_sequence_opt_cps_sig is us).
+
+Lemma mul_opt_rep:
+  forall (u v : T) (x y : GF), rep u x -> rep v y -> rep (mul_opt u v) (x * y)%GF.
+Proof.
+  intros.
+  rewrite mul_opt_correct.
+  auto using mul_rep.
+Qed.
+
+Lemma carry_sequence_opt_cps_rep
+     : forall (is : list nat) (us : list Z) (x : GF),
+       (forall i : nat, In i is -> i < length Base25Point5_10limbs.base) ->
+       length us = length Base25Point5_10limbs.base ->
+       rep us x -> rep (carry_sequence_opt_cps is us) x.
+Proof.
+  intros.
+  rewrite carry_sequence_opt_cps_correct by assumption.
+  apply carry_sequence_rep; assumption.
+Qed.
+
+Definition carry_mul_opt 
+           (is : list nat)
+           (us vs : list Z)
+           : list Z
+  := Eval cbv [B.add
+    E.add E.mul E.mul' E.mul_bi E.mul_bi' E.mul_each E.zeros EC.base E_mul'_opt
+    E_mul'_opt_step E_mul_bi'_opt E_mul_bi'_opt_step
+    List.app List.rev Z_div_opt Z_mul_opt Z_pow_opt
+    Z_sub_opt app beq_nat log_cap_opt carry_opt_cps carry_sequence_opt_cps error firstn
+    fold_left fold_right id length map map_opt mul mul_opt nth_default nth_default_opt
+    nth_error plus pred reduce rev seq set_nth skipn value base] in 
+    carry_sequence_opt_cps is (mul_opt us vs).
+
+Lemma carry_mul_opt_correct
+  : forall (is : list nat) (us vs : list Z) (x  y: GF),
+    rep us x -> rep vs y ->
+    (forall i : nat, In i is -> i < length Base25Point5_10limbs.base) ->
+    length (mul_opt us vs) = length base ->
+    rep (carry_mul_opt is us vs) (x*y)%GF.
+Proof.
+  intros is us vs x y; intros.
+  change (carry_mul_opt _ _ _) with (carry_sequence_opt_cps is (mul_opt us vs)).
+  apply carry_sequence_opt_cps_rep, mul_opt_rep; auto.
+Qed.
+  
 
   Lemma GF25519Base25Point5_mul_reduce_formula :
-    forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 
+    forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
       {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
                         -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
                         -> rep ls (f*g)%GF}.
   Proof.
-
     eexists.
+    intros f g Hf Hg.
 
-    Time deriveModularMultiplicationWithCarries (rev [0;1;2;3;4;5;6;7;8;9;0]).
-    (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *)
+    pose proof (carry_mul_opt_correct [0;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
+    forward Hfg; [abstract (clear; cbv; intros; repeat break_or_hyp; intuition)|].
+    specialize (Hfg H); clear H.
+    forward Hfg; [exact eq_refl|].
+    specialize (Hfg H); clear H.
 
-    Time repeat letify fg; subst fg; eauto.
+    cbv [log_base map k c carry_mul_opt] in Hfg.
+    cbv beta iota delta [Let_In] in Hfg.
+    rewrite ?Z.mul_0_l, ?Z.mul_0_r, ?Z.mul_1_l, ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_0_r in Hfg.
+    rewrite ?Z.mul_assoc, ?Z.add_assoc in Hfg.
+    exact Hfg.
   Time Defined.
 End GF25519Base25Point5Formula.
 
@@ -234,6 +530,3 @@ Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
  * More Ltac acrobatics will be needed to get out that formula for further use in Coq.
  * The easiest fix will be to make the proof script above fully automated,
  * using [abstract] to contain the proof part. *)
-
-
-