Changeset 1511 for src/ASM/CostsProof.ma

Timestamp:

Nov 16, 2011, 5:35:24 PM (9 years ago)

Author:

mulligan

Message:

proofs, added, changes to execute_1_0 function therefore required to remove excess lets

File:

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

src/ASM/CostsProof.ma

@@ -55 +55 @@
 definition current_instruction_cost ≝
   λs: Status.
-  let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in
-    cost.
+    \snd (fetch (code_memory … s) (program_counter … s)).
 
 definition next_instruction_properly_relates_program_counters ≝
@@ -64 +63 @@
   let pc_before ≝ program_counter … before in
   let pc_after ≝ program_counter … after in
-  let 〈carry, sum〉 ≝ half_add … pc_before (bitvector_of_nat … size) in
+  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
     sum = pc_after.
 
@@ -70 +69 @@
   λs: Status.
   let pc ≝ program_counter … s in
-  let 〈instruction, new_pc, cost〉 ≝ fetch … (code_memory … s) pc in
-    instruction.
+  \fst (\fst (fetch … (code_memory … s) pc)).
 
 definition current_instruction_is_labelled ≝
@@ -302 +300 @@
 qed.
 
-lemma status_execution_progresses_processor_clock:
+example set_program_counter_ignores_clock:
+  ∀s: Status.
+  ∀pc: Word.
+    clock … (set_program_counter … s pc) = clock … s.
+  #s #pc %
+qed.
+
+example set_low_internal_ram_ignores_clock:
+  ∀s: Status.
+  ∀ram: BitVectorTrie Byte 7.
+    clock … (set_low_internal_ram … s ram) = clock … s.
+  #s #ram %
+qed.
+
+example set_8051_sfr_ignores_clock:
+  ∀s: Status.
+  ∀sfr: SFR8051.
+  ∀v: Byte.
+    clock … (set_8051_sfr ? s sfr v) = clock … s.
+  #s #sfr #v %
+qed.
+
+example clock_set_clock:
+  ∀s: Status.
+  ∀v.
+    clock … (set_clock … s v) = v.
+  #s #v %
+qed.
+
+example write_at_stack_pointer_ignores_clock:
+  ∀s: Status.
+  ∀sp: Byte.
+    clock … (write_at_stack_pointer … s sp) = clock … s.
+  #s #sp
+  change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with (
+      let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
+        ?);
+  normalize nodelta;
+  cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP))
+  #nu #nl normalize nodelta;
+  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
+  [ normalize nodelta; %
+  | normalize nodelta; %
+  ]
+qed.
+
+example status_execution_progresses_processor_clock:
   ∀s: Status.
     clock … s ≤ clock … (execute 1 s).
-  #status
-  cases status
-  #ignore1 #ignore2 #ignore3 #ignore4 #ignore5 #ignore6 #ignore7 #ignore8
-  #ignore9 #clock
-  
+  #s
+  change in match (execute 1 s) with (execute_1 s);
+  change in match (execute_1 s) with (
+    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
+                               (program_counter (BitVectorTrie Byte 16) s)
+    in 
+      execute_1_0 s instr_pc_ticks);
+  normalize nodelta;
+  whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
+     (program_counter (BitVectorTrie Byte 16) s)));
+  normalize nodelta;
+  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
+           (program_counter (BitVectorTrie Byte 16) s))
+  #instruction_pc #ticks
+  normalize nodelta;
+  cases instruction_pc
+  #instruction #pc
+  cases instruction
+  [1:
+    #addr11 cases addr11 #addressing_mode
+    normalize nodelta; cases addressing_mode
+    normalize nodelta;
+    [1,2,3,4,8,9,15,16,17,19:
+      #assm whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |5,6,7,10,11,12,13,14:
+      whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |18:
+      #addr11 #irrelevant
+      normalize nodelta;
+      >set_program_counter_ignores_clock
+      normalize nodelta;
+      >set_program_counter_ignores_clock
+      >write_at_stack_pointer_ignores_clock
+      >set_8051_sfr_ignores_clock
+      >write_at_stack_pointer_ignores_clock
+      >set_8051_sfr_ignores_clock
+      >clock_set_clock //
+    ]
+  |2:
+    #addr16 cases addr16 #addressing_mode
+    normalize nodelta; cases addressing_mode
+    normalize nodelta;
+    [1,2,3,4,8,9,15,16,17,18:
+      #assm whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |5,6,7,10,11,12,13,14:
+      whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |19:
+      #addr16 #irrelevant
+      normalize nodelta;
+      >set_program_counter_ignores_clock
+      >write_at_stack_pointer_ignores_clock
+      >set_8051_sfr_ignores_clock
+      >write_at_stack_pointer_ignores_clock
+      >set_8051_sfr_ignores_clock
+      >clock_set_clock
+      >set_program_counter_ignores_clock //
+    ]
+  |3: #addr11 cases addr11 #addressing_mode
+      normalize nodelta; cases addressing_mode
+      normalize nodelta;
+      [1,2,3,4,8,9,15,16,17,19:
+        #assm whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |5,6,7,10,11,12,13,14:
+        whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |18:
+        #word11 #irrelevant
+        normalize nodelta;
+        >set_program_counter_ignores_clock
+        >clock_set_clock
+        >set_program_counter_ignores_clock //
+      ]
+  |4: #addr16 cases addr16 #addressing_mode
+      normalize nodelta; cases addressing_mode
+      normalize nodelta;
+      [1,2,3,4,8,9,15,16,17,18:
+        #assm whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |5,6,7,10,11,12,13,14:
+        whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |19:
+        #word #irrelevant
+        normalize nodelta;
+        >set_program_counter_ignores_clock
+        >clock_set_clock
+        >set_program_counter_ignores_clock //
+      ]
+  |5: #relative cases relative #addressing_mode
+      normalize nodelta; cases addressing_mode
+      normalize nodelta;
+      [1,2,3,4,8,9,15,16,18,19:
+        #assm whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |5,6,7,10,11,12,13,14:
+        whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |17:
+        #byte #irrelevant
+        normalize nodelta;
+        >set_program_counter_ignores_clock
+        >set_program_counter_ignores_clock
+        >clock_set_clock //
+      ]
+  |6: #indirect_dptr cases indirect_dptr #addressing_mode
+      normalize nodelta; cases addressing_mode
+      normalize nodelta;
+      
+
+lemma current_instruction_cost_is_ok:
+  ∀s: Status.
+    current_instruction_cost s = clock … (execute 1 s) - clock … s.
+  #s
+  change in match (execute 1 s) with (execute_1 s);
+  change in match (execute_1 s) with (
+    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
+                               (program_counter (BitVectorTrie Byte 16) s)
+    in 
+      execute_1_0 s instr_pc_ticks);
+  change in ⊢ (??%?) with (
+    \snd (fetch (code_memory … s) (program_counter … s)));
+  normalize nodelta;
 
 let rec compute_max_trace_label_label_cost_is_ok
@@ -348 +514 @@
   |2: cases the_trace
     [1: #the_status #not_return #not_jump #not_cost
+        change in ⊢ (??%?) with (current_instruction_cost the_status);
+        @current_instruction_cost_is_ok
     |2: #the_status #is_return
+        change in ⊢ (??%?) with (current_instruction_cost the_status);
+        @current_instruction_cost_is_ok
     |3: #the_status #is_jump #is_cost
+        change in ⊢ (??%?) with (current_instruction_cost the_status);
+        @current_instruction_cost_is_ok
     |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
-        #next_intruction_coherence #call_trace #final_trace
+        #next_instruction_coherence #call_trace #final_trace
+        change in ⊢ (??%?) with (
+          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
+          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
+          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
+            call_trace_cost + current_instruction_cost + final_trace_cost)
+        normalize nodelta;
+        >current_instruction_cost_is_ok
+        >compute_max_trace_label_return_cost_is_ok
+        >compute_max_trace_label_label_pre_cost_is_ok
+        generalize in match next_instruction_coherence;
+        change in ⊢ (% → ?) with (
+          let size ≝ current_instruction_cost pre_fun_call in
+          let pc_before ≝ program_counter … pre_fun_call in
+          let pc_after ≝ program_counter … after_fun_call in
+          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
+            sum = pc_after)
+        normalize nodelta;
+        >(plus_minus_rearrangement
+          (clock (BitVectorTrie Byte 16) after_fun_call)
+          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
+          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
     |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
         #is_not_jump #is_not_ret #is_not_labelled
-        @current_instruction_cost
+        change in ⊢ (??%?) with (
+          let current_instruction_cost ≝ current_instruction_cost status_pre in
+          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
+            current_instruction_cost + tail_trace_cost)
+        normalize nodelta;
+        >compute_max_trace_label_label_pre_cost_is_ok
+        >current_instruction_cost_is_ok
     ]
   ]