Compute tight bounds in a different way

We compute them as 1.1*(s-1), which is a simpler way to express that
they vary across limbs for nonuniform bases.  This allows 32-bit 25519
sub to boundscheck.

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.