diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 15:51:41 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 15:51:41 +0100 |
| commit | d8f1751b88d0013166412677c965079700e36557 (patch) | |
| tree | 31d77a659be99826c9d892f6bfb7b692c4d5ec92 /kvx/FPDivision64.v | |
| parent | 9bb316c0f32cd88cd95895111401ff7995938fec (diff) | |
| download | compcert-kvx-d8f1751b88d0013166412677c965079700e36557.tar.gz compcert-kvx-d8f1751b88d0013166412677c965079700e36557.zip | |
done for small a
Diffstat (limited to 'kvx/FPDivision64.v')
| -rw-r--r-- | kvx/FPDivision64.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 0d11c3cb..a53169b8 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1366,7 +1366,9 @@ Proof. with (-(a' - a' / b' * b')+b')%Z by ring. rewrite <- MOD. rewrite Int64.signed_repr; cycle 1. - { admit. + { change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + lia. } rewrite zlt_true by lia. ring. @@ -1376,8 +1378,10 @@ Proof. replace (a' / b' * b' - a')%Z with (-(a' - a' / b' * b'))%Z by ring. rewrite <- MOD. rewrite Int64.signed_repr ; cycle 1. - { admit. + { change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + lia. } rewrite zlt_false by lia. reflexivity. -Admitted. +Qed. |