Skip to content
Snippets Groups Projects
Commit 2906eb6f authored by Pierre Roux's avatar Pierre Roux
Browse files
parent bc24e51c
No related branches found
No related tags found
1 merge request!549Adapt to https://github.com/coq/coq/pull/18928
...@@ -21,11 +21,12 @@ ...@@ -21,11 +21,12 @@
data : list (bv 64) data : list (bv 64)
H : bv_unsigned l < bv_unsigned r H : bv_unsigned l < bv_unsigned r
H0 : bv_unsigned r ≤ Z.of_nat (length data) H0 : bv_unsigned r ≤ Z.of_nat (length data)
H1 : ¬ bv_swrap 128 (bv_unsigned l) >= H1 :
bv_swrap 128 ¬ bv_swrap 128 (bv_unsigned l) >=
(bv_wrap 64 bv_swrap 128
(bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + (bv_wrap 64
bv_unsigned l + 0)) (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 +
bv_unsigned l + 0))
============================ ============================
bv_unsigned l < bv_unsigned l <
bv_wrap 64 bv_wrap 64
...@@ -46,9 +47,10 @@ goal 2 is: ...@@ -46,9 +47,10 @@ goal 2 is:
i, n : bv 64 i, n : bv 64
H : bv_unsigned i < bv_unsigned n H : bv_unsigned i < bv_unsigned n
H0 : bv_wrap 64 H0 :
(bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) + bv_wrap 64
1) ≠ 0%Z (bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) + 1)
≠ 0%Z
============================ ============================
bv_wrap 64 (bv_unsigned i + 1) < bv_unsigned n bv_wrap 64 (bv_unsigned i + 1) < bv_unsigned n
1 goal 1 goal
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment