include "utilities/binary/Z.ma". include "ASM/BitVector.ma". include "ASM/Arithmetic.ma". include "utilities/binary/division.ma". let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝ match bv with [ VEmpty ⇒ OZ | VCons n' h t ⇒ if h then pos (fold_left ??? (λacc,b.if b then (p1 acc) else (p0 acc)) one t) else (Z_of_unsigned_bitvector ? t) ]. definition Z_of_signed_bitvector ≝ λn.λbv:BitVector n. match bv with [ VEmpty ⇒ OZ | VCons n' h t ⇒ if h then - (Zsucc (Z_of_unsigned_bitvector ? (negation_bv ? t))) else (Z_of_unsigned_bitvector n' t) ]. (* Reverses, so LSB first. *) let rec bits_of_pos (p:Pos) : list bool ≝ match p with [ one ⇒ [true] | p0 p' ⇒ false::(bits_of_pos p') | p1 p' ⇒ true::(bits_of_pos p') ]. let rec zeroext_reversed (n:nat) (m:nat) (bv:BitVector n) on m : BitVector m ≝ match m with [ O ⇒ [[ ]] | S m' ⇒ match bv with [ VEmpty ⇒ zero (S m') | VCons n' h t ⇒ VCons ? m' h (zeroext_reversed n' m' t) ] ]. let rec bitvector_of_Z (n:nat) (z:Z) on z : BitVector n ≝ match z with [ OZ ⇒ zero n | pos p ⇒ let bits ≝ bits_of_pos p in reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) | neg p ⇒ match p with [ one ⇒ maximum ? | _ ⇒ let bits ≝ bits_of_pos (pred p) in let pz ≝ reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) in negation_bv ? pz ] ]. theorem bv_Z_unsigned_min : ∀n. ∀bv:BitVector n. OZ ≤ Z_of_unsigned_bitvector n bv. #n #bv elim bv [ // | #m * #t #IH whd in ⊢ (??%); // ] qed. (* Use bit counting to show the max *) let rec pos_length (p:Pos) : nat ≝ match p with [ one ⇒ O | p0 q ⇒ S (pos_length q) | p1 q ⇒ S (pos_length q) ]. lemma pos_length_lt: ∀p,q. pos_length p < pos_length q → p < q. #p elim p [ * [ normalize #H elim (absurd ? H (not_le_Sn_n 0)) | #q #_ @(lt_one_S (p0 q)) | #q #_ >p0_times2 /2/ ] | #p' #IH * [ normalize #H elim (absurd ? H (not_le_Sn_O ?)) | #q #H change with (one+ (p0 p') < one+(p0 q)) @monotonic_lt_plus_r >p0_times2 >(p0_times2 q) @monotonic_lt_times_r @IH @le_S_S_to_le @H | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q)) >p0_times2 >(p0_times2 q) change with (succ one * succ p' ≤ succ one * q) @monotonic_le_times_r @IH @le_S_S_to_le @H ] | #p' #IH * [ normalize #H elim (absurd ? H (not_le_Sn_O ?)) | #q #H change with ((p0 p') < succ (p0 q)) @le_S >p0_times2 >(p0_times2 q) @monotonic_lt_times_r @IH @le_S_S_to_le @H | #q #H >p0_times2 >(p0_times2 q) @monotonic_lt_times_r @IH @le_S_S_to_le @H ] ] qed. lemma bvZ_length : ∀n.∀bv:BitVector n. match Z_of_unsigned_bitvector n bv with [ OZ ⇒ True | pos p ⇒ pos_length p < n | neg p ⇒ False ]. #n #bv elim bv [ @I | #m * [ 2: #tl normalize cases (Z_of_unsigned_bitvector m tl) normalize /2/ | #tl #_ normalize @le_S_S change with (? ≤ pos_length one + m) generalize in ⊢ (?(?(?????%?))(?(?%)?)); elim tl [ // | #o * #t normalize #IH #p IH @refl ] qed. theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n. #n #bv normalize lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 by pos_length_lt/ qed. lemma Zopp_le: ∀x,y. x ≤ y → -y ≤ -x. * [ 2,3: #p ] * [ 2,3: #q ] // qed. theorem bv_Z_signed_min : ∀n. ∀bv:BitVector n. - Z_two_power_nat n ≤ Z_of_signed_bitvector n bv. #n * [ // | #m * [ #bv @Zopp_le @(transitive_Zle … (Z_two_power_nat m)) [ @Zlt_to_Zle @bv_Z_unsigned_max | normalize // ] | #bv @(transitive_Zle … 0) // ] ] qed. theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n. #n #bv @(vector_inv_n ? (S n) ? bv) * [ #t whd in ⊢ (?%%); lapply (bv_Z_unsigned_min … (negation_bv n t)) cases (Z_of_unsigned_bitvector n (negation_bv n t)) // #p * | #t whd in ⊢ (?%?); // ] qed. (* TODO *) axiom Z_of_unsigned_bitvector_of_Z : ∀n,z. Z_of_unsigned_bitvector n (bitvector_of_Z n z) = modZ z (Z_two_power_nat n). axiom bitvector_of_Z_of_unsigned_bitvector : ∀n,bv. bitvector_of_Z n (Z_of_unsigned_bitvector n bv) = bv.