Changeset 3033 for src/ASM/Arithmetic.ma

Timestamp:

Mar 29, 2013, 12:53:35 PM (8 years ago)

Author:

sacerdot

Message:

Bug fixed: sign_extension was extending according to the _second_ bit, not
the first one!

File:

• src/ASM/Arithmetic.ma (modified) (2 diffs)

src/ASM/Arithmetic.ma

@@ -958 +958 @@
   ∀size, m: nat.
   ∀size_proof: 0 < size.
-    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
-  normalize in size_proof; normalize @le_S_S assumption
+    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 0 ? = false.
+@(transitive_le … size_proof) @le_S %
 qed.
     
@@ -1012 +1012 @@
 definition sign_extension: Byte → Word ≝
   λc.
-    let b ≝ get_index_v ? 8 c 1 ? in
+    let b ≝ get_index_v ? 8 c 0 ? in
       [[ b; b; b; b; b; b; b; b ]] @@ c.
   normalize