Changeset 2149
 Timestamp:
 Jul 3, 2012, 4:19:38 AM (5 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2124 r2149 179 179 ] 180 180 qed. 181 182 axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n. 181 183 182 184 axiom nat_of_bitvector_bitvector_of_nat_inverse: … … 719 721 qed. 720 722 723 axiom le_to_le_nat_of_bitvector_add: 724 ∀n,v,m1,m2. 725 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 → 726 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤ 727 nat_of_bitvector n (add n v (bitvector_of_nat n m2)). 728 729 lemma lt_to_lt_nat_of_bitvector_add: 730 ∀n,v,m1,m2. 731 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 732 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) < 733 nat_of_bitvector n (add n v (bitvector_of_nat n m2)). 734 #n #v #m1 #m2 #m2_ok #bounded #H 735 lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption 736 #K @(transitive_le … (K H)) 737 cases daemon (*CSC: TRUE, complete*) 738 qed. 739 721 740 definition sign_bit : ∀n. BitVector n → bool ≝ 722 741 λn,v. match v with [ VEmpty ⇒ false  VCons _ h _ ⇒ h ]. 
src/ASM/AssemblyProof.ma
r2148 r2149 276 276 qed. 277 277 278 (*CSC: move elsewhere*)279 lemma flatten_singleton:280 ∀A,a. flatten A [a] = a.281 #A #a normalize //282 qed.283 284 (*CSC: move elsewhere*)285 lemma length_flatten_cons:286 ∀A,hd,tl.287 flatten A (hd::tl) = hd + flatten A tl.288 #A #hd #tl normalize //289 qed.290 291 lemma tech_transitive_lt_3:292 ∀n1,n2,n3,b.293 n1 < b → n2 < b → n3 < b →294 n1 + n2 + n3 < 3 * b.295 #n1 #n2 #n3 #b #H1 #H2 #H3296 @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ]297 @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ]298 @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] //299 qed.300 301 278 lemma assembly1_pseudoinstruction_lt_2_to_16: 302 279 ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi. … … 338 315  #dptr #id normalize in ⊢ (?%?); // 339 316 ] 340 qed.341 342 (*CSC: move elsewhere *)343 lemma m_lt_1_to_m_refl_0:344 ∀m: nat.345 m < 1 → m = 0.346 #m cases m try (#irrelevant %)347 #m' whd in ⊢ (% → ?); #relevant348 lapply (le_S_S_to_le … relevant)349 change with (? < ? → ?) relevant #relevant350 cases (lt_to_not_zero … relevant)351 qed.352 353 (*CSC: move elsewhere*)354 axiom le_to_le_nat_of_bitvector_add:355 ∀n,v,m1,m2.356 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →357 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤358 nat_of_bitvector n (add n v (bitvector_of_nat n m2)).359 360 (*CSC: move elsewhere*)361 lemma lt_to_lt_nat_of_bitvector_add:362 ∀n,v,m1,m2.363 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →364 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <365 nat_of_bitvector n (add n v (bitvector_of_nat n m2)).366 #n #v #m1 #m2 #m2_ok #bounded #H367 lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption368 #K @(transitive_le … (K H))369 cases daemon (*CSC: TRUE, complete*)370 317 qed. 371 318 … … 413 360 qed. 414 361 415 (*CSC: move elsewhere *)416 axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.417 418 362 (* This is a non trivial consequence of fetch_assembly_pseudo + 419 load_code_memory_ok because the finite amount of memory. In363 load_code_memory_ok because of the finite amount of memory. In 420 364 particular the case when the compiled program exhausts the 421 code memory is very tricky. *) 365 code memory is very tricky. It also requires monotonicity of 366 sigma in the outofbounds region too. *) 422 367 lemma assembly_ok: 423 368 ∀program. 
src/ASM/Util.ma
r2125 r2149 1725 1725 qed. 1726 1726 1727 lemma flatten_singleton: 1728 ∀A,a. flatten A [a] = a. 1729 #A #a normalize // 1730 qed. 1731 1732 lemma length_flatten_cons: 1733 ∀A,hd,tl. 1734 flatten A (hd::tl) = hd + flatten A tl. 1735 #A #hd #tl normalize // 1736 qed. 1737 1738 lemma tech_transitive_lt_3: 1739 ∀n1,n2,n3,b. 1740 n1 < b → n2 < b → n3 < b → 1741 n1 + n2 + n3 < 3 * b. 1742 #n1 #n2 #n3 #b #H1 #H2 #H3 1743 @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ] 1744 @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ] 1745 @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] // 1746 qed. 1747 1748 lemma m_lt_1_to_m_refl_0: 1749 ∀m: nat. 1750 m < 1 → m = 0. 1751 #m cases m try (#irrelevant %) 1752 #m' whd in ⊢ (% → ?); #relevant 1753 lapply (le_S_S_to_le … relevant) 1754 change with (? < ? → ?) relevant #relevant 1755 cases (lt_to_not_zero … relevant) 1756 qed.
Note: See TracChangeset
for help on using the changeset viewer.