diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-20 07:58:42 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-20 07:58:42 -0400 |
| commit | 9e2ffb6198c3dcb6b40a5b75699f275542ec5709 (patch) | |
| tree | 282c0b885d5df8a6d4a6f7e9b53bc2184e1306b1 /src/Arithmetic/Saturated.v | |
| parent | 6ef07499aed3a023c19cee4ec1cb797ea861c60c (diff) | |
rename Columns.sub_cps to make it clear that no balance is added
Diffstat (limited to 'src/Arithmetic/Saturated.v')
| -rw-r--r-- | src/Arithmetic/Saturated.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 7b27fa0ff..c3240834c 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -491,7 +491,7 @@ Module Columns. (fun Q => from_associational_cps weight n3 (P++Q) (fun R => compact_cps (div:=div) (modulo:=modulo) (add_get_carry:=Z.add_get_carry_full) weight R f))). - Definition sub_cps {n} (p q : Z^n) {T} (f : (Z*Z^n)->T) := + Definition unbalanced_sub_cps {n} (p q : Z^n) {T} (f : (Z*Z^n)->T) := B.Positional.to_associational_cps weight p (fun P => B.Positional.negate_snd_cps weight q (fun nq => B.Positional.to_associational_cps weight nq @@ -510,7 +510,7 @@ Module Columns. End Columns. Hint Unfold Columns.add_cps - Columns.sub_cps + Columns.unbalanced_sub_cps Columns.mul_cps. Hint Rewrite @Columns.compact_digit_id @@ -579,9 +579,9 @@ Section Freeze. [freeze] has the following steps: (1) subtract modulus in a carrying loop (in our framework, this - consists of two steps; [Columns.sub_cps] combines the input p and - the modulus m such that the ith limb in the output is the list - [p[i];-m[i]]. We can then call [Columns.compact].) + consists of two steps; [Columns.unbalanced_sub_cps] combines the + input p and the modulus m such that the ith limb in the output is + the list [p[i];-m[i]]. We can then call [Columns.compact].) (2) look at the final carry, which should be either 0 or -1. If it's -1, then we add the modulus back in. Otherwise we add 0 for constant-timeness. @@ -589,7 +589,7 @@ Section Freeze. the carry in step 3 was -1, so they cancel out. *) Definition freeze_cps {n} mask (m:Z^n) (p:Z^n) {T} (f : Z^n->T) := - Columns.sub_cps weight p m + Columns.unbalanced_sub_cps weight p m (fun carry_p => conditional_add_cps mask (fst carry_p) (snd carry_p) m (fun carry_r => f (snd carry_r))) . |