From 453514077affbf3fbc684e970790c541ef96470a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 27 Jun 2023 09:04:40 -0700 Subject: [PATCH] UInt128: proof taming cf. #2978 --- ulib/FStar.UInt128.fst | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index af785ac29e5..205bb2eb286 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -234,7 +234,9 @@ let mod_add_small n1 n2 k = mod_add n1 n2 k; Math.small_modulo_lemma_1 (n1%k + n2%k) k -#push-options "--z3rlimit 100 --split_queries no" +// This proof is pretty stable with the calc proof, but it can fail +// ~1% of the times, so add a retry. +#push-options "--split_queries no --z3rlimit 20 --retry 5" let add_mod (a b: t) : Pure t (requires True) (ensures (fun r -> (v a + v b) % pow2 128 = v r)) = @@ -248,14 +250,19 @@ let add_mod (a b: t) : Pure t let b_h = U64.v b.high in carry_sum_ok a.low b.low; Math.lemma_mod_plus_distr_l (a_h + b_h) ((a_l + b_l) / (pow2 64)) (pow2 64); - assert (U64.v r.high == (a_h + b_h + (a_l + b_l) / (pow2 64)) % pow2 64); - // mod_mul (a_h + b_h + (a_l + b_l) / (pow2 64)) (pow2 64) (pow2 64); - assert (U64.v r.high * pow2 64 == - (a_h * pow2 64 + - b_h * pow2 64 + - (a_l + b_l) / (pow2 64) * (pow2 64)) % pow2 128) - by (Tactics.SMT.set_rlimit 200); - // mod_mod (U64.v r.low) (pow2 64) (pow2 64); + calc (==) { + U64.v r.high * pow2 64; + == {} + ((a_h + b_h + (a_l + b_l) / (pow2 64)) % pow2 64) * pow2 64; + == { mod_mul (a_h + b_h + (a_l + b_l) / (pow2 64)) (pow2 64) (pow2 64) } + ((a_h + b_h + (a_l + b_l) / (pow2 64)) * pow2 64) % (pow2 64 * pow2 64); + == {} + ((a_h + b_h + (a_l + b_l)/(pow2 64)) * pow2 64) + % pow2 128; + == {} + (a_h * pow2 64 + b_h * pow2 64 + ((a_l + b_l)/(pow2 64)) * pow2 64) + % pow2 128; + }; assert (U64.v r.low == (U64.v r.low) % pow2 128); mod_add_small (a_h * pow2 64 + b_h * pow2 64 +