source: src/ASM/BitVectorZ.ma @ 2270

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