Changeset 3033


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

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

Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/arithmetic.ml

    r2775 r3033  
    297297(** val fbs_diff_rect_Type4 :
    298298    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    299 let rec fbs_diff_rect_Type4 h_fbs_diff' x_1368 = function
     299let rec fbs_diff_rect_Type4 h_fbs_diff' x_4 = function
    300300| Fbs_diff' (n, m) -> h_fbs_diff' n m
    301301
    302302(** val fbs_diff_rect_Type5 :
    303303    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    304 let rec fbs_diff_rect_Type5 h_fbs_diff' x_1371 = function
     304let rec fbs_diff_rect_Type5 h_fbs_diff' x_7 = function
    305305| Fbs_diff' (n, m) -> h_fbs_diff' n m
    306306
    307307(** val fbs_diff_rect_Type3 :
    308308    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    309 let rec fbs_diff_rect_Type3 h_fbs_diff' x_1374 = function
     309let rec fbs_diff_rect_Type3 h_fbs_diff' x_10 = function
    310310| Fbs_diff' (n, m) -> h_fbs_diff' n m
    311311
    312312(** val fbs_diff_rect_Type2 :
    313313    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    314 let rec fbs_diff_rect_Type2 h_fbs_diff' x_1377 = function
     314let rec fbs_diff_rect_Type2 h_fbs_diff' x_13 = function
    315315| Fbs_diff' (n, m) -> h_fbs_diff' n m
    316316
    317317(** val fbs_diff_rect_Type1 :
    318318    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    319 let rec fbs_diff_rect_Type1 h_fbs_diff' x_1380 = function
     319let rec fbs_diff_rect_Type1 h_fbs_diff' x_16 = function
    320320| Fbs_diff' (n, m) -> h_fbs_diff' n m
    321321
    322322(** val fbs_diff_rect_Type0 :
    323323    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    324 let rec fbs_diff_rect_Type0 h_fbs_diff' x_1383 = function
     324let rec fbs_diff_rect_Type0 h_fbs_diff' x_19 = function
    325325| Fbs_diff' (n, m) -> h_fbs_diff' n m
    326326
     
    760760  let b =
    761761    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    762       (Nat.S Nat.O)))))))) c (Nat.S Nat.O)
     762      (Nat.S Nat.O)))))))) c Nat.O
    763763  in
    764764  Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  • 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.