source:src/ASM/BitVectorZ.ma@847

Last change on this file since 847 was 700, checked in by campbell, 10 years ago

Get Clight semantics going again (except for problems CexecEquiv? that I caused
earlier).

File size: 4.0 KB
Line
1
2include "utilities/binary/Z.ma".
3include "ASM/BitVector.ma".
4include "ASM/Arithmetic.ma".
5
6let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
7match 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
14definition Z_of_signed_bitvector ≝
15λn.λbv:BitVector n.
16match 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. *)
24let rec bits_of_pos (p:Pos) : list bool ≝
25match p with
26[ one ⇒ [true]
27| p0 p' ⇒ false::(bits_of_pos p')
28| p1 p' ⇒  true::(bits_of_pos p')
29].
30
31let rec zeroext_reversed (n:nat) (m:nat) (bv:BitVector n) on m : BitVector m ≝
32match 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
41let rec bitvector_of_Z (n:nat) (z:Z) on z : BitVector n ≝
42match 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
57theorem bv_Z_unsigned_min : ∀n. ∀bv:BitVector n. OZ ≤ Z_of_unsigned_bitvector n bv.
58#n #bv elim bv
59[ //
60| #m * #t #IH whd in ⊢ (??%) //
61] qed.
62
63(* Use bit counting to show the max *)
64
65let rec pos_length (p:Pos) : nat ≝
66match p with
67[ one ⇒ O
68| p0 q ⇒ S (pos_length q)
69| p1 q ⇒ S (pos_length q)
70].
71
72lemma 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)
86      @monotonic_le_times_r @IH
87      @le_S_S_to_le @H
88    ]
89| #p' #IH
90  * [ normalize #H elim (absurd ? H (not_le_Sn_O ?))
91    | #q #H change with ((p0 p') < succ (p0 q)) @le_S
92      >p0_times2 >(p0_times2 q)
93      @monotonic_lt_times_r @IH
94      @le_S_S_to_le @H
95    | #q #H
96      >p0_times2 >(p0_times2 q)
97      @monotonic_lt_times_r @IH
98      @le_S_S_to_le @H
99    ]
100] qed.
101
102lemma bvZ_length : ∀n.∀bv:BitVector n. match Z_of_unsigned_bitvector n bv with
103[ OZ ⇒ True | pos p ⇒ pos_length p < n | neg p ⇒ False ].
104#n #bv elim bv
105[ @I
106| #m *
107[ 2: #tl normalize cases (Z_of_unsigned_bitvector m tl) normalize /2/
108| #tl #_ normalize @le_S_S
109  change with (? ≤ pos_length one + m)
110  generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl
111  [ // | #o * #t normalize #IH #p <plus_n_Sm
112    change with (? ≤ pos_length (p1 p) + o)
113    @IH
114  ]
115] qed.
116
117lemma two_power_length : ∀n. pos_length (two_power_nat n) = n.
118#n elim n
119[ @refl
120| #m #IH normalize > IH @refl
121] qed.
122
123theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n.
124#n #bv normalize
125lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/
126qed.
127
128lemma Zopp_le: ∀x,y. x ≤ y → -y ≤ -x.
129* [ 2,3: #p ] * [ 2,3: #q ] //
130qed.
131
132theorem bv_Z_signed_min : ∀n. ∀bv:BitVector n. - Z_two_power_nat n ≤ Z_of_signed_bitvector n bv.
133#n *
134[ //
135| #m *
136  [ #bv @Zopp_le @(transitive_Zle … (Z_two_power_nat m))
137    [ @Zlt_to_Zle @bv_Z_unsigned_max
138    | normalize //
139    ]
140  | #bv @(transitive_Zle … 0) //
141  ]
142] qed.
143
144theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n.
145#n #bv @(vector_inv_n ? (S n) ? bv) *
146[ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t))
147  cases (Z_of_unsigned_bitvector n (negation_bv n t)) //
148  #p *
149| #t whd in ⊢ (?%?) //
150] qed.
Note: See TracBrowser for help on using the repository browser.