diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-01 15:02:23 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-05-01 15:02:58 -0400 |
commit | df5218b25d73bc95becc6d1c9db124951dccd925 (patch) | |
tree | a1294d95a0ab8747774ce44cb0574bd0f49f76fa | |
parent | 59f465cf644987cc208a1a9b99d2f79719f24a0a (diff) |
Clean up implementation
With help from Andres
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v | 43 |
1 files changed, 20 insertions, 23 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v index 080911b64..99c0f1793 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v @@ -42,20 +42,22 @@ Section columns. (f : tuple (list Z) n -> T), T) (Columns_mul_cps : forall (weight : nat -> Z) - (n m : nat) - (a b : tuple (list Z) n) + (na nb m : nat) + (a : tuple (list Z) na) + (a : tuple (list Z) nb) T (f : tuple (list Z) m -> T), T). Context (modulo div : Z -> Z -> Z) (add_get_carry : Z -> Z -> Z -> Z * Z) - (k' : nat) + (p_len : nat) (s : Z). - Let k := S k'. - Context (p : tuple (list Z) k) - (p' : Z) (* [-p⁻¹] *). + Context (p : tuple (list Z) p_len) + (k0 : Z) (* [(-p⁻¹) mod 2ˢ] *). Local Notation weight := (fun i : nat => 2^(Z.of_nat i * s))%Z. Section body. + Context (k' : nat). + Let k := (S (k' + p_len)). Context (T : tuple Z k). Local Notation Pos2Col t := (@Columns.from_associational @@ -65,28 +67,23 @@ Section columns. Local Notation encode z := (Pos2Col (@B.Positional.encode weight modulo div k z)). Local Notation compact := (@Columns.compact weight add_get_carry div modulo k). - Local Notation mul a b := (@Columns_mul_cps weight k k a b _ id). + Local Notation mul a b := (@Columns_mul_cps weight _ _ k a b _ id). Local Notation add a b := (@Columns_add_cps weight k a b _ id). - Let N := 2^s. - Let k0 := p' mod N. - - Let T1 := (hd T) mod N. - Let Y := (T1 * k0) mod N. - Let T2 := mul p (encode Y). + Let T1 := (hd T) (*mod (2^s)*). + Let Y := (T1 * k0) mod (2^s). + Let T2 := mul ((Y::nil)%list : tuple _ 1) p. Let T3 := add (Pos2Col T) T2. - Definition carry_to_highest_and_drop_lowest (ts : tuple Z k) (c : Z) : tuple Z k - := Tuple.left_append c (tl ts). - Definition redc_body : tuple Z k - := let '(c, ts) := compact T3 in carry_to_highest_and_drop_lowest ts c. + Definition (*carry_to_highest_and_*)drop_lowest (ts : tuple Z k) (c : Z) : tuple Z (pred k) + := (*Tuple.left_append c*) (tl ts). + Definition redc_body : tuple Z (pred k) + := let '(c, ts) := compact T3 in + (*carry_to_highest_and_*)drop_lowest ts c. End body. - Fixpoint redc_for (T : tuple Z k) (count : nat) : tuple Z k + Fixpoint redc (count : nat) : tuple Z (count + p_len) -> tuple Z p_len := match count with - | O => T - | S count' => redc_for (redc_body T) count' + | O => fun T => T + | S count' => fun T => redc count' (redc_body _ T) end. - - Definition redc (T : tuple Z k) : tuple Z k - := redc_for T k. End columns. |