diff options
Diffstat (limited to 'src/Experiments/SimplyTypedArithmetic.v')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 79bedd94b..db74517cf 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -6887,7 +6887,10 @@ Section rcarry_mul. Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q. Let idxs := (seq 0 n ++ [0; 1])%list%nat. Let coef := 2. - Let upperbound_tight := (2^Qceiling limbwidth + 2^(Qceiling limbwidth - 3))%Z. + Let tight_upperbounds : list Z + := List.map + (fun v : Z => Qceiling (11/10 * v)) + (encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c (s-1)). Let prime_bound : ZRange.type.option.interp (type.Z) := Some r[0~>(s - Associational.eval c - 1)]%zrange. @@ -6896,9 +6899,9 @@ Section rcarry_mul. Let relax_zrange := relax_zrange_of_machine_wordsize. Let tight_bounds : list (ZRange.type.option.interp type.Z) - := List.repeat (Some r[0~>upperbound_tight]%zrange) n. + := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds. Let loose_bounds : list (ZRange.type.option.interp type.Z) - := List.repeat (Some r[0 ~> 3*upperbound_tight]%zrange) n. + := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds. Definition check_args {T} (res : Pipeline.ErrorT T) : Pipeline.ErrorT T @@ -7037,7 +7040,7 @@ Section rcarry_mul. | lia | rewrite interp_reify_list, ?map_map | rewrite map_ext with (g:=id), map_id - | rewrite repeat_length + | progress distr_length | progress cbv [Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in * | progress cbv [Qle] in * | progress cbn -[reify_list] in * @@ -7539,7 +7542,7 @@ Module X25519_32. Definition machine_wordsize := 32. Derive base_25p5_carry_mul - SuchThat (rcarry_mul_correctT n s c base_25p5_carry_mul) + SuchThat (rcarry_mul_correctT n s c machine_wordsize base_25p5_carry_mul) As base_25p5_carry_mul_correct. Proof. Time solve_rcarry_mul machine_wordsize. Time Qed. |