Changeset 181
 Timestamp:
 Oct 13, 2010, 4:27:18 PM (9 years ago)
 Location:
 Csemantics
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Integers.ma
r15 r181 156 156 ndefinition neg : int → int ≝ λx. repr ( unsigned x). 157 157 158 (*159 ndefinition zero_ext : Z → int → int ≝160 λn,x. repr (modZ (unsigned x) (two_p n)).161 ndefinition sign_ext : Z → int → int ≝162 λn,x. repr (let p ≝ two_p n in163 let y ≝ modZ (unsigned x) p in164 if Zltb y (two_p (n1)) then y else y  p).165 *)166 158 nlet rec zero_ext (n:Z) (x:int) on x : int ≝ 167 159 repr (modZ (unsigned x) (two_p n)). … … 204 196 ndefinition Z_shift_add ≝ λb: bool. λx: Z. 205 197 if b then 2 * x + 1 else 2 * x. 206 (* 207 Definition Z_bin_decomp (x: Z) : bool * Z := 208 match x with 209  Z0 => (false, 0) 210  Zpos p => 211 match p with 212  xI q => (true, Zpos q) 213  xO q => (false, Zpos q) 214  xH => (true, 0) 215 end 216  Zneg p => 217 match p with 218  xI q => (true, Zneg q  1) 219  xO q => (false, Zneg q) 220  xH => (true, 1) 221 end 222 end. 223 *) 224 naxiom bits_of_Z : nat → Z → Z → bool. 225 naxiom Z_of_bits : nat → (Z → bool) → Z. 226 (* 227 Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z > bool := 228 match n with 229  O => 230 (fun i: Z => false) 231  S m => 232 let (b, y) := Z_bin_decomp x in 233 let f := bits_of_Z m y in 234 (fun i: Z => if zeq i 0 then b else f (i  1)) 235 end. 236 237 Fixpoint Z_of_bits (n: nat) (f: Z > bool) {struct n}: Z := 238 match n with 239  O => 0 240  S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1))) 241 end. 242 *) 198 199 ndefinition Z_bin_decomp : Z → bool × Z ≝ 200 λx.match x with 201 [ OZ ⇒ 〈false, OZ〉 202  pos p ⇒ 203 match p with 204 [ p1 q ⇒ 〈true, pos q〉 205  p0 q ⇒ 〈false, pos q〉 206  one ⇒ 〈true, OZ〉 207 ] 208  neg p ⇒ 209 match p with 210 [ p1 q ⇒ 〈true, Zpred (neg q)〉 211  p0 q ⇒ 〈false, neg q〉 212  one ⇒ 〈true, neg one〉 213 ] 214 ]. 215 216 nlet rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝ 217 match n with 218 [ O ⇒ λi:Z. false 219  S m ⇒ 220 match Z_bin_decomp x with [ mk_pair b y ⇒ 221 let f ≝ bits_of_Z m y in 222 λi:Z. if eqZb i 0 then b else f (Zpred i) ] 223 ]. 224 225 nlet rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝ 226 match n with 227 [ O ⇒ OZ 228  S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i))) 229 ]. 230 243 231 (* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *) 244 232 … … 744 732 apply eqmod_refl. red; exists (1); ring. 745 733 Qed. 746 747 Theorem unsigned_range:748 forall i, 0 <= unsigned i < modulus.749 Proof.750 destruct i; simpl. auto.751 Qed.752 Hint Resolve unsigned_range: ints.753 754 Theorem unsigned_range_2:755 forall i, 0 <= unsigned i <= max_unsigned.756 Proof.757 intro; unfold max_unsigned.758 generalize (unsigned_range i). omega.759 Qed.760 Hint Resolve unsigned_range_2: ints.761 734 *) 735 736 ntheorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus. 737 #i; ncases i; #i' H; ncases H; /2/; 738 nqed. 739 740 ntheorem unsigned_range_2: 741 ∀i. 0 ≤ unsigned i ∧ unsigned i ≤ max_unsigned. 742 #i; nrewrite > (?:max_unsigned = modulus  1); //; (* unfold *) 743 nlapply (unsigned_range i); *; #Hz Hm; @; 744 ##[ //; 745 ## nrewrite < (Zpred_Zsucc (unsigned i)); 746 nrewrite < (Zpred_Zplus_neg_O modulus); 747 napply monotonic_Zle_Zpred; 748 /2/; 749 ##] nqed. 750 762 751 naxiom signed_range: 763 752 ∀i. min_signed ≤ signed i ∧ signed i ≤ max_signed. 764 753 (* 754 #i; nwhd in ⊢ (?(??%)(?%?)); 755 nlapply (unsigned_range i); *; nletin n ≝ (unsigned i); #H1 H2; 756 napply (Zltb_elim_Type0); #H3; 757 ##[ @; ##[ napply (transitive_Zle ? OZ); //; 758 ## nrewrite < (Zpred_Zsucc n); 759 nrewrite < (Zpred_Zplus_neg_O half_modulus); 760 napply monotonic_Zle_Zpred; /2/; 761 ##] 762 ## @; ##[ nrewrite > half_modulus_modulus; 763 765 764 Theorem signed_range: 766 765 forall i, min_signed <= signed i <= max_signed. 
Csemantics/README
r178 r181 10 10 11 11  The memory model is executable; some small tests can be found in 12 test/memorymodel.ma. Note that the handling of integer values is 13 axiomatised, so conversions are not yet evaluated. 12 test/memorymodel.ma. 14 13 15  The C syntax has been ported, minus a few lemmas that are not used by16 the semantics.14  The Clight syntax file has been ported, minus a few lemmas that are not used 15 by the semantics. 17 16 18  Most of the smallstep C semantics has been ported, although a few of the 19 underlying arithmetic functions are only present as axioms. 20 21  Nonetheless, this is sufficient to animate the semantics of several simple C 22 programs in test. 17  The smallstep inductively defined Clight semantics has been ported. 23 18 24 19  A collection of definitions and lemmas that probably ought to be in 25 20 matita's standard library can be found in extralib.ma. 26 21 27  Some of the machine integers (i.e., integers modulo) resultsare28 given as axioms in Integers.ma. Implementing them should be routine now that22  Some of the theory about machine integers (i.e., integers modulo) are 23 given as axioms in Integers.ma. Proving them should be routine now that 29 24 we have a binary representation of integers. The CompCert version is given 30 25 as a functor on the word size  we don't have an equivalent of this yet. … … 122 117 Integers.ma 123 118 124 Most of the operations have been ported, although some have been left as 125 axioms because the underlying operation is not present. The use of the 126 Coq module system to abstract over the word size has been left out for 127 now. 119 The operations have been ported, although the results about them generally 120 have not. The equality results have been left axiomatised because they 121 require proof irrelevance because each integer carries a proof that it is 122 in range. The use of the Coq module system to abstract over the word size 123 has been left out for now. 128 124 129 125 Maps.ma … … 143 139 Values.ma 144 140 145 The definitions about values which don't rely on arithmetics operations that 146 haven't been ported yet are done. The other definitions and most of the 147 lemmas still remain to be done. 141 The definitions about operations relevant to the Clight semantics have been 142 ported. The other definitions and most of the lemmas still remain to be done. 148 143 149 144 
Csemantics/extralib.ma
r173 r181 83 83 84 84 (* should be proved in nat.ma, but it's not! *) 85 naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ]. 85 nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ]. 86 #n; nelim n; 87 ##[ #m; ncases m; //; 88 ## #n' IH m; ncases m; ##[ /2/; ## #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %; 89 nlapply (IH m'); ncases (eqb n' m'); /2/; ##] 90 ##] nqed. 86 91 87 92 nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m  false ⇒ n ≠ m ]. … … 269 274 ## napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb) 270 275 ##] nqed. 276 277 nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc. 278 #x y; ncases x; ncases y; /2/; 279 #n m; napply (pos_cases … n); napply (pos_cases … m); 280 ##[ //; 281 ## #n'; /2/; 282 ## #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m')); /2/; 283 ## #n' m'; #H; nnormalize in H; 284 nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m'); /2/; 285 ##] nqed. 286 287 nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred. 288 #x y; ncases x; ncases y; 289 ##[ ##1,2,7,8,9: /2/; 290 ## ##3,4: #m; nnormalize; *; 291 ## #m n; napply (pos_cases … n); napply (pos_cases … m); 292 ##[ ##1,2: /2/; 293 ## #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n')); /2/; 294 ## #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m'); /2/; 295 ##] 296 ## #m n; nnormalize; *; 297 ##] nqed. 298 299 nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m). 300 #n; ncases n; //; #n'; #a b H; 301 ##[ napply (pos_elim … n'); 302 ##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b); /2/; 303 ## #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n'')); //; 304 nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …); /2/; 305 ##] 306 ## napply (pos_elim … n'); 307 ##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b); /2/; 308 ## #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n'')); //; 309 nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …); /2/; 310 ##] 311 ##] nqed. 312 313 nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n). 314 /2/; nqed. 271 315 272 316 nlet rec Z_times (x:Z) (y:Z) : Z ≝
Note: See TracChangeset
for help on using the changeset viewer.