Changeset 1591 for src/ASM/ASMCosts.ma

Timestamp:

Dec 6, 2011, 5:24:45 PM (8 years ago)

Author:

mulligan

Message:

work from today

File:

• src/ASM/ASMCosts.ma (modified) (5 diffs)

src/ASM/ASMCosts.ma

@@ -72 +72 @@
   mk_abstract_status
    Status
-   (λs,s'. eject … (execute_1 s) = s')
+   (λs,s'. (execute_1 s) = s')
    (λs,class. ASM_classify s = class)
    (current_instruction_is_labelled cost_labels)
@@ -91 +91 @@
   //
 qed.
-
-axiom size:
-  ∀a: Type[0].
-  ∀n: nat.
-    BitVectorTrie Byte 16 → nat.
-
-(* XXX: need some precondition about pc not being too "big" to avoid overflow *)
-axiom fetch_pc_lt_new_pc:
-  ∀mem: BitVectorTrie Byte 16.
-  ∀pc: Word.
-  ∀proof: nat_of_bitvector … pc < size Byte 16 mem.
-    nat_of_bitvector … pc < nat_of_bitvector … (\snd (\fst (fetch … mem pc))).
   
 axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
@@ -108 +96 @@
     m - n ≤ m - S o → S m - n ≤ m - o.
 
-axiom strengthened_invariant:
+lemma strengthened_invariant:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀program_size: nat.
-  ∀code_memory_size: nat.
+  ∀total_program_size: nat.
   ∀new_program_counter: Word.
   ∀program_counter: Word.
-    code_memory_size ≤ size Byte 16 code_memory →
-    program_size < code_memory_size →
-      let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … program_size))) in
+    total_program_size ≤ code_memory_size →
+      let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
         Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
           new_program_counter = \snd (\fst (fetch … code_memory program_counter)) →
-            nat_of_bitvector … program_counter < program_size →
-              nat_of_bitvector … new_program_counter < program_size.
+            nat_of_bitvector … program_counter ≤ total_program_size →
+              nat_of_bitvector … new_program_counter ≤ total_program_size.
+  #code_memory #total_program_size #new_program_counter #program_counter
+  #relation_total_program_code_memory_size #end_instruction_is_ok
+  #new_program_counter_from_fetch #program_counter_within_program
+  >new_program_counter_from_fetch
+  lapply (sig2 ? ? (fetch code_memory program_counter)) #assm
+    
         
 (* XXX: use memoisation here in the future *)
 let rec block_cost
   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
-    (program_counter: Word) (program_size: nat) (code_memory_size: nat)
-      (size_invariant: code_memory_size ≤ size Byte 16 code_memory)
-        (pc_invariant: nat_of_bitvector … program_counter < code_memory_size)
+    (program_counter: Word) (program_size: nat) (total_program_size: nat)
+      (size_invariant: total_program_size ≤ code_memory_size)
+        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
           (final_instr_invariant:
-            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in
+            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
               Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
-                on program_size: initial_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
-  match program_size return λprogram_size: nat. initial_program_size - nat_of_bitvector … program_counter < program_size → nat with
+                on program_size: total_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
+  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter < program_size → nat with
   [ O ⇒ λabsurd. ⊥
   | S program_size ⇒ λrecursive_case.
-    let ticks ≝ \snd (fetch … code_memory pc) in
-    let instr ≝ \fst (\fst (fetch … mem pc)) in
-    let newpc ≝ \snd (\fst (fetch … mem pc)) in
+    let ticks ≝ \snd (fetch … code_memory program_counter) in
+    let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in
+    let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in
     match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
     [ None ⇒
@@ -143 +135 @@
         match classify return λx. ∀classify_refl: x = classify. nat with
         [ cl_jump ⇒ λclassify_refl. ticks
-        | cl_call ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
+        | cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
         | cl_return ⇒ λclassify_refl. ticks
-        | cl_other ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
+        | cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
         ] (refl … classify)
     | Some _ ⇒ ticks
@@ -153 +145 @@
     cases(lt_to_not_zero … absurd)
   |2,4:
-    cut(nat_of_bitvector … pc < nat_of_bitvector … newpc)
+    cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)
     [1,3:
-      @fetch_pc_lt_new_pc
+      @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *)
       lapply(transitive_lt
         (nat_of_bitvector 16 pc)