Addressing code review comments.

Coq/EC/GeneratorMul.v

@@ -115,13 +115,16 @@ Section GeneratorMulWNAF.
     OddWindow w ->
     pExpMultiple n w == groupMul_doubleAdd_signed (Z.shiftl w (Z.of_nat (numPrecompExponentGroups * wsize * n))) p.
 
+  (* An alternative semantics for double/add operations that perform all additions by a table lookup. If the required value is not
+  in the table, then the operation fails. *)
   Definition evalWindowMult_precomp(p : GroupElem) (m : WindowedMultOp) (e : GroupElem) :=
   match m with
   | wm_Add n w => 
     if (divides numPrecompExponentGroups n) then (Some (groupAdd (pExpMultiple (Nat.div n numPrecompExponentGroups) w) e)) else None
   | wm_Double n => Some (groupDouble_n (n * wsize) e)
   end.
 
+  (* Evaluate a double/add program using table lookups of addition operations. *)
   Fixpoint groupMul_signedWindows_precomp (e : GroupElem)(ws : list WindowedMultOp) : option GroupElem :=
     match ws with
     | nil => Some e
@@ -132,6 +135,13 @@ Section GeneratorMulWNAF.
       end
     end.
 
+  (* Convert a simple windowed multiplication by permuting the addition operations and inserting doublings in a specific way. Then 
+  run the double/add program using the semantics that performs all add operations by table lookup. This will only succeed 
+  if doublings were inserted in a way that ensures all the add operations can be performed by table lookups. For example,
+  we can permute the numbers [0, 1, 2, 3, ...] (describing the position of each window) to get [0, 4, 8, ..., 1, 5, 9, ..., 2, 6, 10, ....]
+  and then insert a doubling after each part to decrease the following values by 1. This will result in a list where additions have 
+  exponents that look like [0, 4, 8, ..., 0, 4, 8, ..., 0, 4, 8, ...]. These additions can be calculated using table lookups into a table
+  that only includes multiples of 2^0, 2^4, 2^8, etc. *)
   Definition groupedMul_precomp d ws :=
     match (permuteAndDouble ws d (flatten (groupIndices numWindows numPrecompExponentGroups)) (endIndices (groupIndices numWindows numPrecompExponentGroups))) with
     | None => None
@@ -574,51 +584,6 @@ Section GeneratorMulWNAF.
 
   Qed.
 
-  Definition groupMul := groupMul groupAdd idElem.
-  Definition preCompTable := preCompTable groupAdd idElem groupDouble wsize.  
-
-  Hint Resolve groupMul_proper : typeclass_instances.
-
-  Fixpoint basePreCompTable m x n :=
-    match n with
-    | 0%nat => nil
-    | S n' => (preCompTable x) :: (basePreCompTable m (groupDouble_n m x) n')
-    end.
-
-  Theorem basePreCompTable_correct : forall n m x n1 n2,
-    (n1 < n)%nat ->
-    (n2 < Nat.pow 2 (pred wsize))%nat-> 
-    (List.nth n2 (List.nth n1 (basePreCompTable m x n) List.nil) idElem) == (groupMul ((2 * n2 + 1) * (Nat.pow 2 (n1 * m))) x).
-
-    induction n; destruct n1; intros; simpl in *; try lia.
-    unfold preCompTable.
-    erewrite preCompTable_nth; eauto.
-    simpl.
-    repeat rewrite plus_0_r.
-    repeat rewrite Nat.mul_1_r.
-    reflexivity.
-    unfold tableSize.
-    rewrite Nat.shiftl_1_l.
-    rewrite Nat.sub_1_r.
-    trivial.
-
-    erewrite IHn.
-    repeat rewrite plus_0_r.
-    unfold groupMul.
-    rewrite groupMul_assoc; eauto.
-    rewrite groupMul_assoc; eauto.
-    apply groupMul_proper; eauto.
-    unfold groupDouble_n.
-    rewrite groupDouble_n_groupMul_equiv; eauto.
-    rewrite plus_comm.
-    rewrite Nat.pow_add_r.
-    rewrite groupMul_assoc; eauto.
-    reflexivity.
-    lia.
-    trivial.
-
-  Qed.
-
 End GeneratorMulWNAF.
 
 Section ComputeBaseTable.

Coq/EC/GroupMulWNAF.v

@@ -690,67 +690,6 @@ Section GroupMulWNAF.
 
   Qed.
 
-
-  Fixpoint groupMul_signedWindows_exp (ws : list SignedWindow) n : GroupElem :=
-  match ws with
-  | nil => idElem
-  | w :: ws' => groupAdd (groupMul_doubleAdd_signed (zDouble_n (n * wsize) w) p) (groupMul_signedWindows_exp ws' (S n))
-  end.
-
-  Theorem groupDouble_n_add : forall n1 n2 e,
-    groupDouble_n (n1 + n2) e = groupDouble_n n1 (groupDouble_n n2 e).
-
-    induction n1; intros; simpl in *.
-    reflexivity.
-    rewrite IHn1.
-    reflexivity.
-  Qed.
-
-  Theorem groupAdd_groupDouble_n_distr : forall n e1 e2,
-    groupAdd (groupDouble_n n e1) (groupDouble_n n e2) == groupDouble_n n (groupAdd e1 e2).
-
-    induction n; intros; simpl in *.
-    reflexivity.
-    rewrite <- groupDouble_distrib.
-    rewrite <- IHn.
-    reflexivity.
-
-  Qed.
-
-  Theorem groupDouble_n_id : forall n,
-    groupDouble_n n idElem == idElem.
-
-    induction n; intros; simpl in *.
-    reflexivity.
-    rewrite IHn.
-    rewrite groupDouble_correct.
-    apply groupAdd_id.
-
-  Qed.
-
-  Theorem groupMul_signedWindows_exp_equiv : forall ws n,
-    Forall RegularWindow ws ->
-    groupDouble_n (wsize * n) (groupMul_signedWindows ws) == groupMul_signedWindows_exp ws n.
-
-    induction ws; intros; simpl in *.
-    apply groupDouble_n_id.
-
-    unfold groupAdd_signedWindow.
-    rewrite <- IHws.
-    rewrite zDouble_n_mul.
-    replace (wsize * S n)%nat with (n * wsize + wsize)%nat; try lia.
-    rewrite groupDouble_n_add.
-    rewrite groupAdd_groupDouble_n_distr.
-    replace (wsize * n)%nat with (n * wsize)%nat; try lia.
-    apply groupDouble_n_equiv_compat.
-    apply groupAdd_proper.
-    apply bMultiple_correct.
-    inversion H; clear H; subst.
-    trivial.
-    reflexivity.
-    inversion H; trivial.
-  Qed.
-
   End SignedWindows.
 
   (* signed odd windows *)

Coq/EC/WindowedMulMachine.v

@@ -103,7 +103,7 @@ Definition multiSelect(A : Type)(ls : list A)(lsn : list nat) : option (list A)
 
 
 Inductive WindowedMultOp :=
-  | wm_Add : nat -> Z -> WindowedMultOp (* wm_Add n z means add z * 2^n to the accumulator *)  
+  | wm_Add : nat -> Z -> WindowedMultOp (* Add (z * 2^n) * g to the accumulator, where g is a group element *)  
   | wm_Double : nat -> WindowedMultOp (* Double the value in the accumulator *)
 .
 
@@ -118,7 +118,11 @@ Fixpoint signedWindowsToProg (ws : list SignedWindow)(n : nat) :=
 
 (* Operations that preserve the value *)
 
-(* Insert a double at the head of the list and adjust exponents on remaining items *)
+(* Insert a double at the head of the list and adjust exponents on remaining items. This operation factors the
+doubling out of the remaining list, and it will only succeed in circumstances where each element in the list has
+the required factors. For example, if we want to double 5 times at the beginning of the list, this will succeed 
+if an only if the list looks like [x1 * 2^(y1 + 5), x2 * 2^(y2 + 5), ... , xn * 2^(yn + 5)]. In other words, it will 
+succeed if and only if each exponent is at least 5. *)
 Definition decrExp (n : nat)(p : WindowedMultOp) :=
   match p with
   | wm_Add n' w =>
@@ -1717,6 +1721,9 @@ Theorem permuteAndDouble_grouped_equiv_if : forall perm ws d ls,
 Qed.
 
 
+(* Machine semantics requires a group. The following section assumes an arbitrary group, and the semantics is defined
+in terms of this group. The section also fixes a group element (usually the generator of some interesting group), and multiples
+of this group element are added by the wm_Add operation. *)
 Section MachineEval.
 
   Variable GroupElem : Type.
@@ -1760,9 +1767,9 @@ Section MachineEval.
     bMultiple w == groupMul_doubleAdd_signed w p.
 
   Definition groupMul_signedWindows := groupMul_signedWindows groupAdd idElem groupDouble wsize bMultiple.
-  Definition groupMul_signedWindows_exp := groupMul_signedWindows_exp groupAdd idElem groupDouble groupInverse wsize p.
   Definition groupDouble_n := groupDouble_n groupDouble.
 
+  (* Semantics of a single double or add operation *)
   Definition evalWindowMult (m : WindowedMultOp)(e : GroupElem) :=
     match m with
     | wm_Add n w => (groupAdd (groupMul_doubleAdd_signed (zDouble_n (n * wsize) w) p) e)
@@ -1784,12 +1791,75 @@ Section MachineEval.
 
   Qed.
 
+  (* Semantics of a program comprising a list of operations that are executed in order *)
   Fixpoint groupMul_signedWindows_prog (ws : list WindowedMultOp) : GroupElem :=
     match ws with
     | nil => idElem
     | w :: ws' => evalWindowMult w (groupMul_signedWindows_prog ws')
     end.
 
+  (* groupMul_signedWindows_exp takes a number n and a list of windows, and effectively
+  multiplies each window by 2^(n + wsize) before performing the usual signed window multiplication operation. 
+  This is an intermediate definition that simplifies an equivalence proof. *)
+  Fixpoint groupMul_signedWindows_exp (ws : list SignedWindow) n : GroupElem :=
+    match ws with
+    | nil => idElem
+    | w :: ws' => groupAdd (groupMul_doubleAdd_signed (zDouble_n (n * wsize) w) p) (groupMul_signedWindows_exp ws' (S n))
+    end.
+
+  Theorem groupDouble_n_add : forall n1 n2 e,
+    groupDouble_n (n1 + n2) e = groupDouble_n n1 (groupDouble_n n2 e).
+
+    induction n1; intros; simpl in *.
+    reflexivity.
+    rewrite IHn1.
+    reflexivity.
+  Qed.
+
+  Theorem groupAdd_groupDouble_n_distr : forall n e1 e2,
+    groupAdd (groupDouble_n n e1) (groupDouble_n n e2) == groupDouble_n n (groupAdd e1 e2).
+
+    induction n; intros; simpl in *.
+    reflexivity.
+    rewrite <- groupDouble_distrib; eauto.
+
+  Qed.
+
+  Theorem groupDouble_n_id : forall n,
+    groupDouble_n n idElem == idElem.
+
+    induction n; intros; simpl in *.
+    reflexivity.
+    rewrite IHn.
+    rewrite groupDouble_correct.
+    apply groupAdd_id.
+
+  Qed.
+
+  Theorem groupMul_signedWindows_exp_equiv : forall ws n,
+    Forall RegularWindow ws ->
+    groupDouble_n (wsize * n) (groupMul_signedWindows ws) == groupMul_signedWindows_exp ws n.
+
+    induction ws; intros; simpl in *.
+    apply groupDouble_n_id.
+
+    unfold groupAdd_signedWindow.
+    rewrite <- IHws.
+    unfold groupMul_doubleAdd_signed.
+    rewrite zDouble_n_mul; eauto.
+    replace (wsize * S n)%nat with (n * wsize + wsize)%nat; try lia.
+    rewrite groupDouble_n_add.
+    rewrite groupAdd_groupDouble_n_distr.
+    replace (wsize * n)%nat with (n * wsize)%nat; try lia.
+    apply groupDouble_n_equiv_compat; eauto.
+    apply groupAdd_proper.
+    apply bMultiple_correct.
+    inversion H; clear H; subst.
+    trivial.
+    reflexivity.
+    inversion H; trivial.
+  Qed.
+
   Theorem groupMul_signedWindows_prog_equiv : forall ws n,
     groupMul_signedWindows_prog (signedWindowsToProg ws n) == groupMul_signedWindows_exp ws n.
 
@@ -2034,6 +2104,10 @@ Section MachineEval.
     discriminate.
   Qed.
 
+  (* Prove that programs produced by the permuteAndDouble function produce the same result
+  as the function that performed group multiplication using signed windows defined in GroupMulWNAF.
+  This existing function is already proved to be correct in GroupMulWNAF. Also, permuteAndDouble may fail,
+  and this equivalence holds any time this function succeeds. *)
   Theorem permuteAndDouble_equiv : forall ws d perm doubles ps,
     Forall RegularWindow ws -> 
     Permutation perm (seq 0 (length ws)) ->