diff options
author | Jason Gross <jgross@mit.edu> | 2019-01-13 04:42:03 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-01-14 11:25:10 -0800 |
commit | 08222f8c6228eaf3a6be44c4dbdca066813efd8c (patch) | |
tree | 437fe03546bdfff932bad932904264cadc93effb /src/PushButtonSynthesis.v | |
parent | fa3ae820b785c2d98248bf805c76acfd7cc47e17 (diff) |
Autocompute s and c in WBW Montgomery
This allows us to support primes which are not a power of 2.
We also add p484 as an example.
To support this, I added a small parser combinator library which can
parse arithmetic expressions involving `()^*/+-` and decimal digits.
Closes #486
Closes #342
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
22m14.42s | Total | 12m14.76s || +9m59.65s | +81.61%
--------------------------------------------------------------------------------------------
9m41.91s | p484_32.c | N/A || +9m41.90s | ∞
0m11.51s | p484_64.c | N/A || +0m11.50s | ∞
3m16.22s | p384_32.c | 3m12.02s || +0m04.19s | +2.18%
4m12.18s | PushButtonSynthesis.vo | 4m10.16s || +0m02.02s | +0.80%
0m45.08s | ExtractionHaskell/word_by_word_montgomery | 0m45.24s || -0m00.16s | -0.35%
0m38.14s | p521_32.c | 0m38.12s || +0m00.02s | +0.05%
0m31.80s | p521_64.c | 0m31.78s || +0m00.01s | +0.06%
0m31.09s | ExtractionHaskell/unsaturated_solinas | 0m30.77s || +0m00.32s | +1.03%
0m24.18s | ExtractionHaskell/saturated_solinas | 0m24.21s || -0m00.03s | -0.12%
0m17.38s | ExtractionOCaml/word_by_word_montgomery | 0m17.35s || +0m00.02s | +0.17%
0m13.39s | secp256k1_32.c | 0m13.59s || -0m00.19s | -1.47%
0m13.14s | p256_32.c | 0m13.04s || +0m00.10s | +0.76%
0m10.58s | ExtractionOCaml/unsaturated_solinas | 0m10.73s || -0m00.15s | -1.39%
0m10.23s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || -0m00.10s | -1.06%
0m07.88s | ExtractionOCaml/saturated_solinas | 0m07.94s || -0m00.06s | -0.75%
0m06.78s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.86s || -0m00.08s | -1.16%
0m06.28s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || -0m00.13s | -2.18%
0m06.00s | p224_32.c | 0m05.97s || +0m00.03s | +0.50%
0m05.50s | p384_64.c | 0m05.35s || +0m00.15s | +2.80%
0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.08s || +0m00.20s | +3.93%
0m05.10s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.11s | +2.40%
0m04.12s | ExtractionHaskell/saturated_solinas.hs | 0m04.15s || -0m00.03s | -0.72%
0m02.14s | curve25519_32.c | 0m02.28s || -0m00.13s | -6.14%
0m01.44s | CLI.vo | 0m01.42s || +0m00.02s | +1.40%
0m01.44s | curve25519_64.c | 0m01.57s || -0m00.13s | -8.28%
0m01.14s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.02s | +2.70%
0m01.12s | p256_64.c | 0m00.98s || +0m00.14s | +14.28%
0m01.11s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.05s | -5.12%
0m01.03s | secp256k1_64.c | 0m01.15s || -0m00.11s | -10.43%
0m01.02s | p224_64.c | 0m00.99s || +0m00.03s | +3.03%
0m00.21s | Util/Strings/ParseArithmetic.vo | N/A || +0m00.21s | ∞
Diffstat (limited to 'src/PushButtonSynthesis.v')
-rw-r--r-- | src/PushButtonSynthesis.v | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/src/PushButtonSynthesis.v b/src/PushButtonSynthesis.v index c8e1e97df..b16f62a7f 100644 --- a/src/PushButtonSynthesis.v +++ b/src/PushButtonSynthesis.v @@ -1488,12 +1488,12 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very Local Opaque expr.Interp. Section __. - Context (s : Z) - (c : list (Z * Z)) + Context (m : Z) (machine_wordsize : Z). + Let s := 2^Z.log2_up m. + Let c := [(1, s - m)]. Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). - Let m := s - Associational.eval c. Let r := 2^machine_wordsize. Let r' := match Z.modinv r m with | Some r' => r' @@ -1510,7 +1510,7 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very := Partition.partition (weight 8 1) n_bytes (s-1). Let upperbounds : list Z := prime_upperbound_list. Definition prime_bound : ZRange.type.option.interp (base.type.Z) - := Some r[0~>(s - Associational.eval c - 1)]%zrange. + := Some r[0~>m-1]%zrange. Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) @@ -1519,7 +1519,7 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). Definition m_enc : list Z - := encode (UniformWeight.uweight machine_wordsize) n s c (s-Associational.eval c). + := encode (UniformWeight.uweight machine_wordsize) n s c m. Definition possible_values_of_machine_wordsize := [1; machine_wordsize; 2 * machine_wordsize]%Z. @@ -1540,19 +1540,17 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very (fun '(b, e) k => if b:bool then Error e else k) res [(negb (1 <? machine_wordsize)%Z, Pipeline.Value_not_ltZ "machine_wordsize <= 1" 1 machine_wordsize); - ((negb (0 <? Associational.eval c))%Z, Pipeline.Value_not_ltZ "Associational.eval c ≤ 0" 0 (Associational.eval c)); - ((negb (Associational.eval c <? s))%Z, Pipeline.Value_not_ltZ "s ≤ Associational.eval c" (Associational.eval c) s); - ((s =? 0)%Z, Pipeline.Values_not_provably_distinctZ "s = 0" s 0); + ((negb (0 <? Associational.eval c))%Z, Pipeline.Value_not_ltZ "c ≤ 0" 0 (Associational.eval c)); + ((negb (1 <? m))%Z, Pipeline.Value_not_ltZ "m ≤ 1" 1 m); ((n =? 0)%nat, Pipeline.Values_not_provably_distinctZ "n = 0" n 0%nat); ((r' =? 0)%Z, Pipeline.No_modular_inverse "r⁻¹ mod m" r m); (negb ((r * r') mod m =? 1)%Z, Pipeline.Values_not_provably_equalZ "(r * r') mod m ≠ 1" ((r * r') mod m) 1); (negb ((m * m') mod r =? (-1) mod r)%Z, Pipeline.Values_not_provably_equalZ "(m * m') mod r ≠ (-1) mod r" ((m * m') mod r) ((-1) mod r)); (negb (s <=? r^n), Pipeline.Value_not_leZ "r^n ≤ s" s (r^n)); - (negb (1 <? s - Associational.eval c), Pipeline.Value_not_ltZ "s - Associational.eval c ≤ 1" 1 (s - Associational.eval c)); - (negb (s =? 2^Z.log2 s), Pipeline.Values_not_provably_equalZ "s ≠ 2^log2(s) (needed for from_bytes)" s (2^Z.log2 s)); (negb (s <=? UniformWeight.uweight machine_wordsize n), Pipeline.Value_not_leZ "weight n < s (needed for from_bytes)" s (UniformWeight.uweight machine_wordsize n)); (negb (UniformWeight.uweight machine_wordsize n =? UniformWeight.uweight 8 n_bytes), Pipeline.Values_not_provably_equalZ "weight n ≠ bytes_weight n_bytes (needed for from_bytes)" (UniformWeight.uweight machine_wordsize n) (UniformWeight.uweight 8 n_bytes))]. + Local Arguments Z.mul !_ !_. Local Ltac use_curve_good_t := repeat first [ assumption | progress rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in * @@ -1565,14 +1563,17 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very | progress cbv [Qle] in * | progress cbn -[reify_list] in * | progress intros - | solve [ auto ] ]. + | solve [ auto with zarith ] + | rewrite Z.log2_pow2 by use_curve_good_t ]. Context (curve_good : check_args (Success tt) = Success tt). Lemma use_curve_good - : Z.pos (Z.to_pos m) = s - Associational.eval c + : Z.pos (Z.to_pos m) = m + /\ m = s - Associational.eval c /\ Z.pos (Z.to_pos m) <> 0 /\ s - Associational.eval c <> 0 + /\ 0 < s /\ s <> 0 /\ 0 < machine_wordsize /\ n <> 0%nat @@ -1605,7 +1606,9 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] end. repeat apply conj. - { destruct (s - Associational.eval c) eqn:?; cbn; lia. } + { destruct m eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } { use_curve_good_t. } { use_curve_good_t. } { use_curve_good_t. } @@ -1860,7 +1863,7 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very intros [v1 v0]; cbn [fst snd]. rename x into x'. generalize dependent (eval (n:=n') lgr x'). - cbv [m]. + replace m with (s - Associational.eval c) in * by easy. intro x; intros ??? H; subst x'. eapply In_nth_error in H; destruct H as [i H]. rewrite nth_error_combine in H. @@ -1942,11 +1945,11 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very cbv [bytes_valid] in H. destruct H as [_ H]. pose proof use_curve_good. - cbv [m UniformWeight.uweight] in *; destruct_head'_and; lia. + cbv [UniformWeight.uweight] in *; destruct_head'_and; lia. Qed. Local Ltac solve_extra_bounds_side_conditions := - solve [ cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; cbv [m] in *; lia + solve [ cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia | cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto | now apply weight_bounded_of_bytes_valid | eapply length_of_valid; eassumption ]. |