Changeset 1573

Timestamp:

Nov 28, 2011, 5:13:04 PM (9 years ago)

Author:

mulligan

Message:

more complicated than it appears :(

Location:

src/ASM

Files:

• CostsProof.ma (modified) (6 diffs)
• Interpret.ma (modified) (1 diff)

src/ASM/CostsProof.ma

@@ +1 @@
+
 include "ASM/ASMCosts.ma".
 include "ASM/WellLabeled.ma".
@@ -250 +251 @@
 lemma current_instruction_cost_non_zero:
   ∀s: Status.
-    0 ≤ current_instruction_cost s.
-  //
-qed.
+    current_instruction_cost s > 0.
+  #s
+  cases s
+  #code_memory #hi_ram #lo_ram #x_ram #pc #sfr_8051 #sfr_8052 #p1_latch
+  #p2_latch #clock
+  change with (\snd  (fetch ? ?)) in ⊢ (?%?);
+  change with (fetch0 ? ?) in match (fetch ? ?);
+  change with (
+     let 〈pc,v〉 ≝ next code_memory pc in 
+     let 〈b,v0〉 ≝head bool 7 v in
+       ?) in match (fetch0 ? ?);
+  normalize nodelta;
+
+  cases(fetch (code_memory … s) (program_counter … s))
+  #instruction_pc
+  cases(instruction_pc)
+  #instruction #pc
+  cases(instruction)
+  [ #addr11
 
 lemma le_monotonic_plus:
@@ -276 +293 @@
 qed.
     
-lemma minus_m_n_le_n_m:
+axiom minus_m_n_gt_o_O_le_n_m:
   ∀m, n, o.
     m - n = o → o > 0 → n ≤ m.
-  #m #n #o #eq_hyp
-  cases o
-  [ #absrd normalize in absrd; @le
-  normalize in ⊢ (% → ?);
-  <eq_hyp in ⊢ (% → ?);
-  #lt_hyp
-  generalize in match (le_plus_to_minus_l 1 n m ? lt_hyp);
-  [1: /2/ | 
-qed.
-  
 
 let rec compute_max_trace_label_label_cost_is_ok
@@ -333 +340 @@
         #the_status #assm
         whd in match eject; normalize nodelta
-        @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
+        @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
         [1: assumption
-        |2: @current_instruction_cost_non_zero
+        |2: @(current_instruction_cost_non_zero start_status)
         ]
       ]
@@ -352 +359 @@
         #the_status #assm
         whd in match eject; normalize nodelta
-        @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
+        @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
         [1: assumption
         |2: @current_instruction_cost_non_zero
@@ -375 +382 @@
         #trace_any_label_eq #trace_any_label_le
         >trace_label_return_eq >trace_any_label_eq
-        cases daemon (* XXX: complete me *)
+        >commutative_plus
+        
+        cut ((clock (BitVectorTrie Byte 16) status_after_fun_call
+  -clock (BitVectorTrie Byte 16) status_start_fun_call
+  +current_instruction_cost status_pre_fun_call
+  +(clock (BitVectorTrie Byte 16) status_final
+    -clock (BitVectorTrie Byte 16) status_after_fun_call) =
+          ((clock (BitVectorTrie Byte 16) status_after_fun_call
+            - clock (BitVectorTrie Byte 16) status_start_fun_call)
+          + (clock (BitVectorTrie Byte 16) status_final
+          - clock (BitVectorTrie Byte 16) status_after_fun_call))
+          + current_instruction_cost status_pre_fun_call))
+        [ 1:
+          cases daemon (* XXX: complete me *)
+        | 2:
+          #eq_hyp >eq_hyp
+          >plus_minus_rearrangement_1
+          [1:
+          |2, 3:
+            assumption
+          ]
+        ]
       |2:
         cases daemon (* XXX: complete me *)

src/ASM/Interpret.ma

@@ -785 +785 @@
 
 definition current_instruction_cost ≝
-  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
+  λs: Status. 
+    \snd (fetch (code_memory … s) (program_counter … s)).
 
 definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝