scalar multiplication

1 files changed, 48 insertions, 0 deletions

diff --git a/src/Curves/ScalarMult.v b/src/Curves/ScalarMult.v
new file mode 100644
index 000000000..d71550413
--- /dev/null
+++ b/src/Curves/ScalarMult.v
@@ -0,0 +1,48 @@
+Require Import ZArith.BinInt.
+Require Import List Util.ListUtil.
+
+
+Section ScalarMult.
+  Variable G : Type.
+  Variable neutral : G.
+  Variable add : G -> G -> G.
+  Local Infix "+" := add.
+
+  Fixpoint scalarMultSpec (n:nat) (g:G) : G :=
+    match n with 
+    | O => neutral
+    | S n' => g + scalarMultSpec n' g
+    end
+  .
+
+  (* ng = 
+  *  (n/2)(g+g) + g if n odd
+  *  (n/2)(g+g)     if n even
+  *  g              if n == 1
+  *)
+  Fixpoint scalarMultPos (n:positive) (g:G) : G :=
+    match n with
+    | xI n' => scalarMultPos n' (g + g) + g
+    | xO n' => scalarMultPos n' (g + g)
+    | xH => g
+    end
+  .
+
+  Definition scalarMultNat (n:nat) (g:G) : G :=
+    match n with
+    | O => neutral
+    | S n' => scalarMultPos (Pos.of_succ_nat n') g
+    end
+  .
+
+  Definition sel {T} (b:bool) (x y:T) := if b then y else x.
+  Definition scalarMultStaticZ (bitLengthN:nat) (n:Z) (g:G): G :=
+   fst (fold_right
+     (fun (i : nat) (s : G * G) => let (Q, P) := s in
+      let Q' := sel (Z.testbit (Z.of_nat i) n) Q (Q + P) in
+      let P' := P+P in
+        (Q',  P + P))
+     (neutral, g) (* initial state *)
+     (seq 0 bitLengthN)) (* range of i *)
+  .
+End ScalarMult.