Changeset 2149


Ignore:
Timestamp:
Jul 3, 2012, 4:19:38 AM (5 years ago)
Author:
sacerdot
Message:

Code shuffling to proper places.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2124 r2149  
    179179 ]
    180180qed.
     181
     182axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
    181183
    182184axiom nat_of_bitvector_bitvector_of_nat_inverse:
     
    719721qed.
    720722
     723axiom 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
     729lemma 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
     735lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
     736#K @(transitive_le … (K H))
     737cases daemon (*CSC: TRUE, complete*)
     738qed.
     739
    721740definition sign_bit : ∀n. BitVector n → bool ≝
    722741λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
  • src/ASM/AssemblyProof.ma

    r2148 r2149  
    276276qed.
    277277
    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 #H3
    296  @(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 
    301278lemma assembly1_pseudoinstruction_lt_2_to_16:
    302279  ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
     
    338315| #dptr #id normalize in ⊢ (?%?); //
    339316]
    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 ⊢ (% → ?); #relevant
    348   lapply (le_S_S_to_le … relevant)
    349   change with (? < ? → ?) -relevant #relevant
    350   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 #H
    367 lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
    368 #K @(transitive_le … (K H))
    369 cases daemon (*CSC: TRUE, complete*)
    370317qed.
    371318
     
    413360qed.
    414361
    415 (*CSC: move elsewhere *)
    416 axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
    417 
    418362(* This is a non trivial consequence of fetch_assembly_pseudo +
    419    load_code_memory_ok because the finite amount of memory. In
     363   load_code_memory_ok because of the finite amount of memory. In
    420364   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 out-of-bounds region too. *)     
    422367lemma assembly_ok:
    423368  ∀program.
  • src/ASM/Util.ma

    r2125 r2149  
    17251725qed.
    17261726
     1727lemma flatten_singleton:
     1728 ∀A,a. flatten A [a] = a.
     1729#A #a normalize //
     1730qed.
     1731
     1732lemma length_flatten_cons:
     1733 ∀A,hd,tl.
     1734  |flatten A (hd::tl)| = |hd| + |flatten A tl|.
     1735 #A #hd #tl normalize //
     1736qed.
     1737
     1738lemma 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 // ] //
     1746qed.
     1747
     1748lemma 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)
     1756qed.
Note: See TracChangeset for help on using the changeset viewer.