Changeset 930

Timestamp:

Jun 10, 2011, 2:19:09 AM (10 years ago)

Author:

sacerdot

Message:

Comment, Cost, ADD, ADC cases done.

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -1814 +1814 @@
 qed.
 
+axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
+
+lemma get_register_set_program_counter:
+ ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
+ #T #s #pc %
+qed.
+
+lemma get_8051_sfr_set_program_counter:
+ ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
+ #T #s #pc %
+qed.
+
+lemma get_bit_addressable_sfr_set_program_counter:
+ ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
+ #T #s #pc %
+qed.
+
+lemma low_internal_ram_set_program_counter:
+ ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
+ #T #s #pc %
+qed.
+
+lemma get_arg_8_set_program_counter:
+ ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
+  ∀T,s,pc,b.∀arg:l.
+   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
+ [2,3: cases arg; *; normalize //]
+ #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
+qed.
+
+lemma get_arg_8_set_code_memory:
+ ∀T1,T2,s,code_mem,b,arg.
+   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
+ #T1 #T2 #s #code_mem #b #arg %
+qed.
+
+lemma set_code_memory_set_flags:
+ ∀T1,T2,s,f1,f2,f3,code_mem.
+  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
+   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
+ #T1 #T2 #s #f1 #f2 #f3 #code_mem whd in ⊢ (??(???%?)%)
+ cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
+qed.
+
+lemma set_program_counter_set_flags:
+ ∀T1,s,f1,f2,f3,pc.
+  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
+   set_flags … (set_program_counter … s pc) f1 f2 f3.
+ #T1 #s #f1 #f2 #f3 #pc whd in ⊢ (??(??%?)%)
+ cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
+qed.
+
+lemma program_counter_set_flags:
+ ∀T1,s,f1,f2,f3.
+  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
+ #T1 #s #f1 #f2 #f3 whd in ⊢ (??(??%)?) cases (split ????) #nu #nl %
+qed.
+
+axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.
+
 lemma main_thm:
  ∀ticks_of.
@@ -1830 +1890 @@
     #abs @⊥ normalize in abs; destruct (abs) ]
  * #labels #costs generalize in match (refl … (code_memory … ps))
- cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ normalize nodelta;
+ cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
  generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
   [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ]
@@ -1850 +1910 @@
  #K <K generalize in match K; -K;
  (* STATEMENT WITH EQUALITY HERE *)
- whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta;
+ whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ0 normalize nodelta;
  cases (fetch_pseudo_instruction instr_list (program_counter … ps))
  #pi #newppc normalize nodelta; * #instructions *;
  cases pi normalize nodelta;
-  [ (* Instruction *)
-  | (* Comment *) #comment #H1 #H2 #EQ %[@0] >EQ
-    whd in ⊢ (???(???(??%)))
-    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1
-    >K1 in H2; whd in ⊢ (% → ?) #H2 <(eq_bv_to_eq … H2)
-    
-  | (* Cost *)
-  | (* Jmp *)
-  | (* Call *)
-  | (* Mov *)
-  ]
-qed.
+  [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0]
+    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+    #H2 >(eq_bv_to_eq … H2) >ignore_clock in EQ; #EQ >EQ %
+  |4: (* Jmp *)
+  |5: (* Call *)
+  |6: (* Mov *)
+  | (* Instruction *) -pi; *
+    [1,2: (* ADD, ADDC *) #arg1 #arg2 #H1 #H2 #EQ %[1,3:@1]
+       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+       change in ⊢ (? → ??%?) with (execute_1_0 ??)
+       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+       * #H2a whd in ⊢ (% → ?) #H2b
+       >ignore_clock in EQ;
+       >(eq_instruction_to_eq … H2a)
+       whd in ⊢ (???% → ??%?);
+       >ignore_clock
+       >get_arg_8_set_program_counter [2,4:%]
+       >get_arg_8_set_program_counter [2,4:%]
+       >get_arg_8_set_program_counter [2,4:%]
+       >get_arg_8_set_program_counter [2,4:%]
+       >get_arg_8_set_code_memory
+       >get_arg_8_set_program_counter [2,4:%]
+       >get_arg_8_set_program_counter [2,4:%]
+       >get_arg_8_set_code_memory
+       cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags
+       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
+       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 
+    |