Changeset 1514

Timestamp:

Nov 17, 2011, 5:41:08 PM (8 years ago)

Author:

mulligan

Message:

changes from today. matita keeps dieing

Location:

src/ASM

Files:

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

src/ASM/CostsProof.ma

@@ -257 +257 @@
 qed.
 
-lemma plus_minus_rearrangement:
+lemma plus_minus_rearrangement_1:
   ∀m, n, o: nat.
   ∀proof_n_m: n < m.
@@ -300 +300 @@
 qed.
 
+axiom plus_minus_rearrangement_2:
+  ∀m, n, o: nat.
+    (m - n) + (n - o) = m - o.
+
 example set_program_counter_ignores_clock:
   ∀s: Status.
@@ -461 +465 @@
       normalize nodelta; cases addressing_mode
       normalize nodelta;
-      
+      [1,2,3,4,8,9,15,16,17,18,19:
+        #assm whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |5,6,7,10,11,12,14:
+        whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |13:
+        #irrelevant
+        normalize nodelta;
+        >set_program_counter_ignores_clock
+        >set_program_counter_ignores_clock
+        >clock_set_clock //
+      ]
+  |8: cases daemon (* XXX: my god *) 
+  |7: #acc_a cases acc_a #addressing_mode
+      normalize nodelta; cases addressing_mode
+      normalize nodelta;
+      [1,2,3,4,8,9,15,16,17,18,19:
+        #assm whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |6,7,10,11,12,13,14:
+        whd in ⊢ (% → ?)
+        #absurd cases(absurd)
+      |5:
+        #irrelevant #acc_dptr_acc_pc
+        normalize nodelta;
+        cases daemon (* XXX: my god *)
+      ]
+  ]
+qed.
 
 lemma current_instruction_cost_is_ok:
@@ -476 +509 @@
     \snd (fetch (code_memory … s) (program_counter … s)));
   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));
+  #instr_pc #ticks normalize nodelta;
+  cases (\fst instr_pc)
+  [1:
+    #addr11 normalize nodelta;
+    cases addr11 #addressing_mode
+    cases addressing_mode
+    [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
+      >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
+      >commutative_plus
+      <plus_minus
+      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
+      %
+    ]
+  |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
+      >commutative_plus
+      <plus_minus
+      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
+      %
+    ]
+  |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
+      >commutative_plus
+      <plus_minus
+      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
+      %
+    ]
+  |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
+      >commutative_plus
+      <plus_minus
+      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
+      %
+    ]
+  |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
+      >commutative_plus
+      <plus_minus
+      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
+      %
+    ]
+  |6:
+    #indirect_dptr cases indirect_dptr #addressing_mode
+    normalize nodelta; cases addressing_mode
+    normalize nodelta;
+    [1,2,3,4,8,9,15,16,17,18,19:
+      #assm whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |5,6,7,10,11,12,14:
+      whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |13:
+      #irrelevant
+      normalize nodelta;
+      >set_program_counter_ignores_clock
+      >set_program_counter_ignores_clock
+      >clock_set_clock
+      >commutative_plus
+      <plus_minus
+      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
+      %
+    ]
+  |7:
+    #acc_a cases acc_a #addressing_mode
+    normalize nodelta; cases addressing_mode
+    normalize nodelta;
+    [1,2,3,4,8,9,15,16,17,18,19:
+      #assm whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |6,7,10,11,12,13,14:
+      whd in ⊢ (% → ?)
+      #absurd cases(absurd)
+    |5:
+      #irrelevant #acc_dptr_acc_pc
+      normalize nodelta;
+      cases daemon (* XXX: todo *)
+    ]
+  |8: cases daemon (* XXX: todo *)
+  ]
+qed.
 
 let rec compute_max_trace_label_label_cost_is_ok
@@ -540 +732 @@
           let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
             sum = pc_after)
-        normalize nodelta;
+        normalize nodelta; #relation_pre_after_fun_call
+        >plus_minus_rearrangement_2 in match (
+          (clock (BitVectorTrie Byte 16) after_fun_call
+            -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
+          +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
+            -clock (BitVectorTrie Byte 16) pre_fun_call)));
         >(plus_minus_rearrangement
           (clock (BitVectorTrie Byte 16) after_fun_call)

src/ASM/Interpret.ma

@@ -582 +582 @@
               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
               let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
-              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
+              let new_addr ≝ \snd (half_add ? dptr big_acc) in
               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
                 set_8051_sfr ? s SFR_ACC_A result
             | ACC_PC ⇒ λacc_pc: True.
               let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
-              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
+              let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
               (* DPM: Under specified: does the carry from PC incrementation affect the *)
               (*      addition of the PC with the DPTR? At the moment, no.              *)
               let s ≝ set_program_counter ? s inc_pc in
-              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
+              let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
               let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
                 set_8051_sfr ? s SFR_ACC_A result