Changeset 2149 for src

Timestamp:

Jul 3, 2012, 4:19:38 AM (9 years ago)

Author:

sacerdot

Message:

Code shuffling to proper places.

Location:

src/ASM

Files:

• Arithmetic.ma (modified) (2 diffs)
• AssemblyProof.ma (modified) (3 diffs)
• Util.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -179 +179 @@
  ]
 qed.
+
+axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
 
 axiom nat_of_bitvector_bitvector_of_nat_inverse:
@@ -719 +721 @@
 qed.
 
+axiom le_to_le_nat_of_bitvector_add:
+  ∀n,v,m1,m2.
+    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 → 
+      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
+      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
+
+lemma lt_to_lt_nat_of_bitvector_add:
+  ∀n,v,m1,m2.
+    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 
+      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
+      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
+#n #v #m1 #m2 #m2_ok #bounded #H
+lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
+#K @(transitive_le … (K H))
+cases daemon (*CSC: TRUE, complete*)
+qed.
+
 definition sign_bit : ∀n. BitVector n → bool ≝
 λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].

src/ASM/AssemblyProof.ma

@@ -276 +276 @@
 qed.
 
-(*CSC: move elsewhere*)
-lemma flatten_singleton:
- ∀A,a. flatten A [a] = a.
-#A #a normalize //
-qed.
-
-(*CSC: move elsewhere*)
-lemma length_flatten_cons:
- ∀A,hd,tl.
-  |flatten A (hd::tl)| = |hd| + |flatten A tl|.
- #A #hd #tl normalize //
-qed.
-
-lemma tech_transitive_lt_3:
- ∀n1,n2,n3,b.
-  n1 < b → n2 < b → n3 < b →
-   n1 + n2 + n3 < 3 * b.
- #n1 #n2 #n3 #b #H1 #H2 #H3
- @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ]
- @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ]
- @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] //
-qed.
-
 lemma assembly1_pseudoinstruction_lt_2_to_16:
   ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
@@ -338 +315 @@
 | #dptr #id normalize in ⊢ (?%?); //
 ]
-qed.
-
-(*CSC: move elsewhere *)
-lemma m_lt_1_to_m_refl_0:
-  ∀m: nat.
-    m < 1 → m = 0.
-  #m cases m try (#irrelevant %)
-  #m' whd in ⊢ (% → ?); #relevant
-  lapply (le_S_S_to_le … relevant)
-  change with (? < ? → ?) -relevant #relevant
-  cases (lt_to_not_zero … relevant)
-qed.
-
-(*CSC: move elsewhere*)          
-axiom le_to_le_nat_of_bitvector_add:
-  ∀n,v,m1,m2.
-    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 → 
-      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
-      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
-
-(*CSC: move elsewhere*)          
-lemma lt_to_lt_nat_of_bitvector_add:
-  ∀n,v,m1,m2.
-    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 
-      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
-      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
-#n #v #m1 #m2 #m2_ok #bounded #H
-lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
-#K @(transitive_le … (K H))
-cases daemon (*CSC: TRUE, complete*)
 qed.
 
@@ -413 +360 @@
 qed.
 
-(*CSC: move elsewhere *)
-axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
-
 (* This is a non trivial consequence of fetch_assembly_pseudo +
-   load_code_memory_ok because the finite amount of memory. In
+   load_code_memory_ok because of the finite amount of memory. In
    particular the case when the compiled program exhausts the
-   code memory is very tricky. *)      
+   code memory is very tricky. It also requires monotonicity of
+   sigma in the out-of-bounds region too. *)      
 lemma assembly_ok:
   ∀program.

src/ASM/Util.ma

@@ -1725 +1725 @@
 qed.
 
+lemma flatten_singleton:
+ ∀A,a. flatten A [a] = a.
+#A #a normalize //
+qed.
+
+lemma length_flatten_cons:
+ ∀A,hd,tl.
+  |flatten A (hd::tl)| = |hd| + |flatten A tl|.
+ #A #hd #tl normalize //
+qed.
+
+lemma tech_transitive_lt_3:
+ ∀n1,n2,n3,b.
+  n1 < b → n2 < b → n3 < b →
+   n1 + n2 + n3 < 3 * b.
+ #n1 #n2 #n3 #b #H1 #H2 #H3
+ @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ]
+ @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ]
+ @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] //
+qed.
+
+lemma m_lt_1_to_m_refl_0:
+  ∀m: nat.
+    m < 1 → m = 0.
+  #m cases m try (#irrelevant %)
+  #m' whd in ⊢ (% → ?); #relevant
+  lapply (le_S_S_to_le … relevant)
+  change with (? < ? → ?) -relevant #relevant
+  cases (lt_to_not_zero … relevant)
+qed.