[547] | 1 | |
---|
[700] | 2 | include "utilities/binary/Z.ma". |
---|
| 3 | include "ASM/BitVector.ma". |
---|
| 4 | include "ASM/Arithmetic.ma". |
---|
[547] | 5 | |
---|
| 6 | let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝ |
---|
| 7 | match bv with |
---|
| 8 | [ VEmpty ⇒ OZ |
---|
| 9 | | VCons n' h t ⇒ |
---|
| 10 | if h then pos (fold_left ??? (λacc,b.if b then (p1 acc) else (p0 acc)) one t) |
---|
| 11 | else (Z_of_unsigned_bitvector ? t) |
---|
| 12 | ]. |
---|
| 13 | |
---|
| 14 | definition Z_of_signed_bitvector ≝ |
---|
| 15 | λn.λbv:BitVector n. |
---|
| 16 | match bv with |
---|
| 17 | [ VEmpty ⇒ OZ |
---|
| 18 | | VCons n' h t ⇒ |
---|
| 19 | if h then - (Zsucc (Z_of_unsigned_bitvector ? (negation_bv ? t))) |
---|
| 20 | else (Z_of_unsigned_bitvector n' t) |
---|
| 21 | ]. |
---|
| 22 | |
---|
| 23 | (* Reverses, so LSB first. *) |
---|
| 24 | let rec bits_of_pos (p:Pos) : list bool ≝ |
---|
| 25 | match p with |
---|
| 26 | [ one ⇒ [true] |
---|
| 27 | | p0 p' ⇒ false::(bits_of_pos p') |
---|
| 28 | | p1 p' ⇒ true::(bits_of_pos p') |
---|
| 29 | ]. |
---|
| 30 | |
---|
| 31 | let rec zeroext_reversed (n:nat) (m:nat) (bv:BitVector n) on m : BitVector m ≝ |
---|
| 32 | match m with |
---|
| 33 | [ O ⇒ [[ ]] |
---|
| 34 | | S m' ⇒ |
---|
| 35 | match bv with |
---|
| 36 | [ VEmpty ⇒ zero (S m') |
---|
| 37 | | VCons n' h t ⇒ VCons ? m' h (zeroext_reversed n' m' t) |
---|
| 38 | ] |
---|
| 39 | ]. |
---|
| 40 | |
---|
| 41 | let rec bitvector_of_Z (n:nat) (z:Z) on z : BitVector n ≝ |
---|
| 42 | match z with |
---|
| 43 | [ OZ ⇒ zero n |
---|
| 44 | | pos p ⇒ |
---|
| 45 | let bits ≝ bits_of_pos p in |
---|
| 46 | reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) |
---|
| 47 | | neg p ⇒ |
---|
| 48 | match p with |
---|
| 49 | [ one ⇒ maximum ? |
---|
| 50 | | _ ⇒ |
---|
| 51 | let bits ≝ bits_of_pos (pred p) in |
---|
| 52 | let pz ≝ reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) in |
---|
| 53 | negation_bv ? pz |
---|
| 54 | ] |
---|
| 55 | ]. |
---|
| 56 | |
---|
| 57 | theorem bv_Z_unsigned_min : ∀n. ∀bv:BitVector n. OZ ≤ Z_of_unsigned_bitvector n bv. |
---|
| 58 | #n #bv elim bv |
---|
| 59 | [ // |
---|
[1516] | 60 | | #m * #t #IH whd in ⊢ (??%); // |
---|
[547] | 61 | ] qed. |
---|
| 62 | |
---|
| 63 | (* Use bit counting to show the max *) |
---|
| 64 | |
---|
| 65 | let rec pos_length (p:Pos) : nat ≝ |
---|
| 66 | match p with |
---|
| 67 | [ one ⇒ O |
---|
| 68 | | p0 q ⇒ S (pos_length q) |
---|
| 69 | | p1 q ⇒ S (pos_length q) |
---|
| 70 | ]. |
---|
| 71 | |
---|
| 72 | lemma pos_length_lt: ∀p,q. pos_length p < pos_length q → p < q. |
---|
| 73 | #p elim p |
---|
| 74 | [ * [ normalize #H elim (absurd ? H (not_le_Sn_n 0)) |
---|
| 75 | | #q #_ @(lt_one_S (p0 q)) |
---|
| 76 | | #q #_ >p0_times2 /2/ |
---|
| 77 | ] |
---|
| 78 | | #p' #IH |
---|
| 79 | * [ normalize #H elim (absurd ? H (not_le_Sn_O ?)) |
---|
| 80 | | #q #H change with (one+ (p0 p') < one+(p0 q)) @monotonic_lt_plus_r |
---|
| 81 | >p0_times2 >(p0_times2 q) |
---|
| 82 | @monotonic_lt_times_r @IH |
---|
| 83 | @le_S_S_to_le @H |
---|
| 84 | | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q)) |
---|
| 85 | >p0_times2 >(p0_times2 q) |
---|
[891] | 86 | change with (succ one * succ p' ≤ succ one * q) |
---|
[547] | 87 | @monotonic_le_times_r @IH |
---|
| 88 | @le_S_S_to_le @H |
---|
| 89 | ] |
---|
| 90 | | #p' #IH |
---|
| 91 | * [ normalize #H elim (absurd ? H (not_le_Sn_O ?)) |
---|
| 92 | | #q #H change with ((p0 p') < succ (p0 q)) @le_S |
---|
| 93 | >p0_times2 >(p0_times2 q) |
---|
| 94 | @monotonic_lt_times_r @IH |
---|
| 95 | @le_S_S_to_le @H |
---|
| 96 | | #q #H |
---|
| 97 | >p0_times2 >(p0_times2 q) |
---|
| 98 | @monotonic_lt_times_r @IH |
---|
| 99 | @le_S_S_to_le @H |
---|
| 100 | ] |
---|
| 101 | ] qed. |
---|
| 102 | |
---|
| 103 | lemma bvZ_length : ∀n.∀bv:BitVector n. match Z_of_unsigned_bitvector n bv with |
---|
| 104 | [ OZ ⇒ True | pos p ⇒ pos_length p < n | neg p ⇒ False ]. |
---|
| 105 | #n #bv elim bv |
---|
| 106 | [ @I |
---|
| 107 | | #m * |
---|
| 108 | [ 2: #tl normalize cases (Z_of_unsigned_bitvector m tl) normalize /2/ |
---|
| 109 | | #tl #_ normalize @le_S_S |
---|
| 110 | change with (? ≤ pos_length one + m) |
---|
[1516] | 111 | generalize in ⊢ (?(?(?????%?))(?(?%)?)); elim tl |
---|
[547] | 112 | [ // | #o * #t normalize #IH #p <plus_n_Sm |
---|
| 113 | change with (? ≤ pos_length (p1 p) + o) |
---|
| 114 | @IH |
---|
| 115 | ] |
---|
| 116 | ] qed. |
---|
| 117 | |
---|
| 118 | lemma two_power_length : ∀n. pos_length (two_power_nat n) = n. |
---|
| 119 | #n elim n |
---|
| 120 | [ @refl |
---|
| 121 | | #m #IH normalize > IH @refl |
---|
| 122 | ] qed. |
---|
| 123 | |
---|
| 124 | theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n. |
---|
| 125 | #n #bv normalize |
---|
| 126 | lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/ |
---|
| 127 | qed. |
---|
| 128 | |
---|
| 129 | lemma Zopp_le: ∀x,y. x ≤ y → -y ≤ -x. |
---|
| 130 | * [ 2,3: #p ] * [ 2,3: #q ] // |
---|
| 131 | qed. |
---|
| 132 | |
---|
| 133 | theorem bv_Z_signed_min : ∀n. ∀bv:BitVector n. - Z_two_power_nat n ≤ Z_of_signed_bitvector n bv. |
---|
| 134 | #n * |
---|
| 135 | [ // |
---|
| 136 | | #m * |
---|
| 137 | [ #bv @Zopp_le @(transitive_Zle … (Z_two_power_nat m)) |
---|
| 138 | [ @Zlt_to_Zle @bv_Z_unsigned_max |
---|
| 139 | | normalize // |
---|
| 140 | ] |
---|
| 141 | | #bv @(transitive_Zle … 0) // |
---|
| 142 | ] |
---|
| 143 | ] qed. |
---|
| 144 | |
---|
| 145 | theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n. |
---|
| 146 | #n #bv @(vector_inv_n ? (S n) ? bv) * |
---|
[1516] | 147 | [ #t whd in ⊢ (?%%); lapply (bv_Z_unsigned_min … (negation_bv n t)) |
---|
[547] | 148 | cases (Z_of_unsigned_bitvector n (negation_bv n t)) // |
---|
| 149 | #p * |
---|
[1516] | 150 | | #t whd in ⊢ (?%?); // |
---|
[547] | 151 | ] qed. |
---|