Changeset 3033 for src/ASM


Ignore:
Timestamp:
Mar 29, 2013, 12:53:35 PM (7 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2796 r3033  
    958958  ∀size, m: nat.
    959959  ∀size_proof: 0 < size.
    960     m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
    961   normalize in size_proof; normalize @le_S_S assumption
     960    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 0 ? = false.
     961@(transitive_le … size_proof) @le_S %
    962962qed.
    963963   
     
    10121012definition sign_extension: Byte → Word ≝
    10131013  λc.
    1014     let b ≝ get_index_v ? 8 c 1 ? in
     1014    let b ≝ get_index_v ? 8 c 0 ? in
    10151015      [[ b; b; b; b; b; b; b; b ]] @@ c.
    10161016  normalize
Note: See TracChangeset for help on using the changeset viewer.