Changeset 1639 for src/ASM/ASMCosts.ma

Timestamp:

Jan 10, 2012, 5:27:41 PM (9 years ago)

Author:

mulligan

Message:

changes from today

File:

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

src/ASM/ASMCosts.ma

@@ -92 +92 @@
 qed. 
     
-definition good_program_counter: BitVectorTrie Byte 16 → Word → nat → Prop ≝
+definition good_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
   λcode_memory: BitVectorTrie Byte 16.
+  λprogram_size: nat.
   λprogram_counter: Word.
-  λprogram_size: nat.
     ∃n: nat.
       let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in
@@ -102 +102 @@
             nat_of_bitvector 16 tail_program_counter < nat_of_bitvector 16 program_counter.
 
+axiom half_add_zero:
+  ∀n: nat.
+  ∀b: BitVector n.
+    \snd (half_add n (zero …) b) = b.
+
+lemma fetch_program_counter_n_half_add:
+  ∀n: nat.
+  ∀code_memory: BitVectorTrie Byte 16.
+    fetch_program_counter_n (S n) code_memory (zero …) =
+      let program_counter ≝ fetch_program_counter_n n code_memory (zero …) in
+      let 〈instr, new_program_counter, cost〉 ≝ fetch code_memory program_counter in
+        \snd (half_add … program_counter new_program_counter).
+  #n #code_memory elim n
+  [1:
+    whd in match (fetch_program_counter_n 1 code_memory (zero …));
+    normalize in match (fetch_program_counter_n 0 code_memory (zero …));
+    change with (
+      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory (zero …) in
+        program_counter
+    ) in ⊢ (??%?);
+    cases (fetch code_memory (zero …)) #instr #program_counter normalize nodelta
+    generalize in match instr; #instr
+    cases instr #instr #program_counter normalize nodelta
+    >half_add_zero %
+  |2:
+    #n' #ind_hyp
+    whd in match (fetch_program_counter_n (S (S n')) code_memory (zero …));
+    >ind_hyp (* XXX: things start going wrong here!
+    generalize in match (let (program_counter:Word) ≝
+                  fetch_program_counter_n n' code_memory (zero 16) in 
+           let 〈eta40050,cost〉 ≝fetch code_memory program_counter in 
+           let 〈instr,new_program_counter〉 ≝eta40050 in 
+           \snd  (half_add 16 program_counter new_program_counter));
+    #B normalize nodelta
+    cases (fetch code_memory B) #instr_program_counter #cost normalize nodelta
+    cases instr_program_counter #instr #program_counter normalize nodelta *)
+    cases daemon
+  ]
+qed.
+    
 definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
   λcode_memory: BitVectorTrie Byte 16.
@@ -121 +161 @@
       | DJNZ src_trgt relative ⇒ True
       | _                      ⇒
-          good_program_counter code_memory program_counter total_program_size
+          good_program_counter code_memory total_program_size program_counter
       ]
     | LCALL addr         ⇒
       match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
       [ ADDR16 addr ⇒ λaddr16: True.
-          good_program_counter code_memory addr total_program_size ∧
-            good_program_counter code_memory program_counter total_program_size
+          good_program_counter code_memory total_program_size addr ∧
+            good_program_counter code_memory total_program_size program_counter
       | _ ⇒ λother: False. ⊥
       ] (subaddressing_modein … addr)
@@ -137 +177 @@
         let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
         let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
-          good_program_counter code_memory new_program_counter total_program_size ∧
-            good_program_counter code_memory program_counter total_program_size
+          good_program_counter code_memory total_program_size new_program_counter ∧
+            good_program_counter code_memory total_program_size program_counter
       | _ ⇒ λother: False. ⊥
       ] (subaddressing_modein … addr)
@@ -150 +190 @@
         let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
         let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
-          (good_program_counter code_memory new_program_counter total_program_size) ∧
-            (good_program_counter code_memory program_counter total_program_size)
+          (good_program_counter code_memory total_program_size new_program_counter) ∧
+            (good_program_counter code_memory total_program_size program_counter)
       | _ ⇒ λother: False. ⊥
       ] (subaddressing_modein … addr)
@@ -157 +197 @@
       match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
       [ ADDR16 addr ⇒ λaddr16: True.
-          good_program_counter code_memory addr total_program_size ∧
-            good_program_counter code_memory program_counter total_program_size
+          good_program_counter code_memory total_program_size addr ∧
+            good_program_counter code_memory total_program_size program_counter
       | _ ⇒ λother: False. ⊥
       ] (subaddressing_modein … addr)
@@ -165 +205 @@
       [ RELATIVE addr ⇒ λrelative: True.
         let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in
-          good_program_counter code_memory new_program_counter total_program_size ∧
-            good_program_counter code_memory program_counter total_program_size
+          good_program_counter code_memory total_program_size new_program_counter ∧
+            good_program_counter code_memory total_program_size program_counter
       | _ ⇒ λother: False. ⊥
       ] (subaddressing_modein … addr)
     | JMP   addr     ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
     | MOVC  src trgt ⇒
-        good_program_counter code_memory program_counter total_program_size
+        good_program_counter code_memory total_program_size program_counter
     ].
   cases other
@@ -298 +338 @@
 qed.
 
-lemma subaddressing_mode_elim':
+axiom subaddressing_mode_elim':
   ∀T: Type[2].
   ∀m: nat.
@@ -305 +345 @@
   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
   ∀n: nat.
-  
   ∀v: Vector addressing_mode_tag n.
   ∀proof.
     subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
-  #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
+(*  #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
   elim v
   [ #proof normalize
     
-qed.
+qed. *)
 
 (*
@@ -362 +401 @@
 
 axiom fetch_program_counter_n_technical:
+  ∀n: nat.
   ∀code_memory: BitVectorTrie Byte 16.
   ∀program_counter, program_counter': Word.
-  ∀instruction: instruction.
-  ∀ticks, n: nat.
-  program_counter' = \snd (\fst (fetch code_memory program_counter)) →
-    program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
+  program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
+    program_counter' = \snd (\fst (fetch code_memory program_counter)) →
       program_counter = fetch_program_counter_n n code_memory (zero …).
     
@@ -382 +420 @@
       [ None   ⇒
         match instruction return λx. x = instruction → ? with
-        [ RealInstruction instruction ⇒ λreal_instruction.
-          match instruction return λx. x = instruction → ? with
+        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
+          match real_instruction return λx. x = real_instruction → ? with
           [ RET                    ⇒ λinstr. ticks
           | JC   relative          ⇒ λinstr. ticks
@@ -396 +434 @@
           | _                      ⇒ λinstr.
               ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
-          ] (refl … instruction)
+          ] (refl … real_instruction)
         | ACALL addr     ⇒ λinstr.
             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
@@ -412 +450 @@
       ]
   ].
-  [1:
+  [1: (* ACALL *)
     generalize in match good_program_witness;
     whd in match good_program; normalize nodelta
     cases FETCH normalize nodelta
     cases instr normalize nodelta
-    @(subaddressing_mode_elim … [[ addr11 ]]) #new_addr
+    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
@@ -434 +472 @@
         program_size' + (nat_of_bitvector … program_counter'))
     @lt_n_o_to_plus_m_n_lt_plus_m_o
-    >(fetch_program_counter_n_technical code_memory program_counter
-      program_counter' instruction ticks n)
+    >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
     /2 by pair_destruct_2/
-  |7:
+  |2:
+    generalize in match good_program_witness;
+    whd in match good_program in ⊢ (? → %); normalize nodelta
+    cases FETCH normalize nodelta
+    cases instr normalize nodelta
+    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
+    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
+    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
+    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
+    * #ignore #good_program_counter_assm
+    cases (fetch code_memory program_counter') #instruction_program_counter #cost normalize nodelta
+    cases instruction_program_counter #instruction #program_counter normalize nodelta
+    cases instruction
+    [1:
+      #addr11 normalize nodelta
+      cases addr11 #addressing_mode
+      cases addressing_mode
+      try (#assm #proof normalize in proof; cases proof)
+      try (#proof normalize in proof; cases proof)
+      normalize nodelta
+  |3: (* LCALL *)
     generalize in match good_program_witness;
     whd in match good_program; normalize nodelta
     cases FETCH normalize nodelta
     cases instr normalize nodelta
-    @(subaddressing_mode_elim … [[ acc_dptr; acc_pc ]]) #new_addr
-    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
-    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
-    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
+    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     #assm cases assm #ignore
     whd in match good_program_counter; normalize nodelta * #n * *
@@ -459 +513 @@
         program_size' + (nat_of_bitvector … program_counter'))
     @lt_n_o_to_plus_m_n_lt_plus_m_o
-    >(fetch_program_counter_n_technical code_memory program_counter
-      program_counter' instruction ticks n)
+    >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
     /2 by pair_destruct_2/
-  |3,5,7,9,11:
-    (* XXX etc. need the subaddressing_mode_elim generalizing *)
-  |2:
+  |5: (* JMP *)
     generalize in match good_program_witness;
-    whd in match (good_program code_memory program_counter total_program_size);
+    whd in match good_program; normalize nodelta
     cases FETCH normalize nodelta
     cases instr normalize nodelta
-    @subaddressing_mode_elim #new_addr
-    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
-    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
-    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
-    #assm cases assm #ignore #good_program_counter
-    whd in match (good_program code_memory program_counter' total_program_size);
-    cases(fetch code_memory program_counter') #instruction_program_counter'' #ticks''
-    cases(instruction_program_counter'') #instruction'' #program_counter'' normalize nodelta
-    
-  [2:
-    (* generalize in match good_program_witness; *)
+    cases daemon (* XXX ??? *)
+  |7: (* MOVC *)
+    generalize in match good_program_witness;
     whd in match good_program; normalize nodelta
     cases FETCH normalize nodelta
-    cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta
-    cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta
-    cases acall normalize nodelta
-    cases addr #subaddressing_mode cases subaddressing_mode
-    try (#assm #absurd normalize in absurd; cases absurd)
-    try (#absurd normalize in absurd; cases absurd)
-    normalize nodelta
-    cases instruction'
-    try (#assm normalize nodelta)
-    [7:
-      #irrelevant
-      whd in match good_program_counter; normalize nodelta
+    cases instr normalize nodelta
+    cases daemon (* XXX ??? *)
+  |9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,
+   49,51,53,55,57,59,61,63: (* ADD and similar non-branching instructions *)
+    generalize in match good_program_witness;
+    whd in match good_program; normalize nodelta
+    cases FETCH normalize nodelta
+    cases real_instruction_refl
+    cases instr normalize nodelta
+    whd in match good_program_counter; normalize nodelta
+    * #the_n * *
+    #program_counter_fetch_program_counter_n' #program_counter_lt_total_program_size'
+    #fetch_program_n_lt_program_counter'
+    @(transitive_le
+      total_program_size
+      (S program_size' + nat_of_bitvector … program_counter)
+      (program_size' + nat_of_bitvector … program_counter')
+      recursive_case)
+    normalize in match (S program_size' + nat_of_bitvector … program_counter);
+    >plus_n_Sm
+    @monotonic_le_plus_r
+    change with (
+      nat_of_bitvector … program_counter <
+        nat_of_bitvector … program_counter')
+    generalize in match (
+      fetch_program_counter_n_technical the_n code_memory
+        program_counter program_counter' program_counter_fetch_program_counter_n');
+    #hyp >hyp
+    >program_counter_fetch_program_counter_n'
+  ]
+qed.