diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-07 19:12:03 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-07 19:12:03 +0100 |
| commit | cd444fa2200427a1e792716ad5cbac9c1eac872e (patch) | |
| tree | 0234766749d0e33dced87979bba9cddb0e1ea410 /kvx | |
| parent | b11fd5400cb042f4b0727e08d2fa53929092f74c (diff) | |
| download | compcert-kvx-cd444fa2200427a1e792716ad5cbac9c1eac872e.tar.gz compcert-kvx-cd444fa2200427a1e792716ad5cbac9c1eac872e.zip | |
progress in proofs
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 851a6cc4..f61cc48c 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -208,5 +208,39 @@ Proof. destruct C7 as (C7R & C7F & _). split. assumption. + rewrite C7R. + rewrite C6R. + rewrite C5R. + rewrite C4R. + rewrite B2R_Bopp. + rewrite C3R. + rewrite C2R. + rewrite C1R. + rewrite C0R. + cbn. + set(b1 := IZR b') in *. + replace (round radix2 (FLT_exp (-1074) 53) ZnearestE 1) with 1%R by gappa. + set (bd := round radix2 (FLT_exp (-1074) 53) ZnearestE b1). + set (x0 := round radix2 (FLT_exp (-1074) 53) ZnearestE + (round radix2 (FLT_exp (-149) 24) ZnearestE + (1 / round radix2 (FLT_exp (-149) 24) ZnearestE b1))). + set (alpha0 := (- x0 * bd + 1)%R). + set (y1 := (round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0 * x0 + x0)%R). + set (x1 := round radix2 (FLT_exp (-1074) 53) ZnearestE y1). + replace (x1 - 1/b1)%R with ((y1-1/b1)+(x1-y1))%R by ring. + + assert(alpha0 = -((x0-1/bd)/(1/bd)))%R as alpha0_EQ. + { unfold alpha0. + field. + unfold bd. + gappa. + } + assert(y1-1/b1 = ((round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0) + - alpha0) * x0 + + alpha0*(x0-1/b1) - ((bd-b1)/b1) * x0)%R as y1_EQ. + { unfold y1, alpha0. + field. + lra. + } Admitted. |