Changeset 948 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 13, 2011, 3:28:26 PM (9 years ago)

Author:

sacerdot

Message:

Some progress on the Call case.

File:

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

src/ASM/AssemblyProof.ma

@@ -2047 +2047 @@
 qed.
 
+lemma special_function_registers_8051_write_at_stack_pointer:
+ ∀T,s,x.
+    special_function_registers_8051 T (write_at_stack_pointer T s x)
+  = special_function_registers_8051 T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
+lemma get_8051_sfr_write_at_stack_pointer:
+ ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
+ #T #s #x #y whd in ⊢ (??%%) //
+qed.
+
+lemma code_memory_write_at_stack_pointer:
+ ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
+(*
+lemma low_internal_ram_write_at_stack_pointer:
+ ∀T,s,x. low_internal_ram T (write_at_stack_pointer T s x) = low_internal_ram T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) normalize nodelta; // 
+qed.
+
+lemma high_internal_ram_write_at_stack_pointer:
+ ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+*)
+
+lemma external_ram_write_at_stack_pointer:
+ ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
+lemma special_function_registers_8052_write_at_stack_pointer:
+ ∀T,s,x.
+    special_function_registers_8052 T (write_at_stack_pointer T s x)
+  = special_function_registers_8052 T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
+lemma p1_latch_write_at_stack_pointer:
+ ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
+lemma p3_latch_write_at_stack_pointer:
+ ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
+lemma clock_write_at_stack_pointer:
+ ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
+ #T #s #x whd in ⊢ (??(??%)?)
+ cases (split ????) #nu #nl normalize nodelta;
+ cases (get_index_v bool ????) %
+qed.
+
 lemma eq_rect_Type1_r:
   ∀A: Type[1].
@@ -2163 +2237 @@
        #result #flags
        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
-  |4: (* Jmp *) #label #MAP
+  |5: (* Call *) #label #MAP
+      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
       whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
-       [3: (* long *) #H1 #H2 #EQ %[@1]
+       [ (* short *) #abs @⊥ destruct (abs)
+       |3: (* long *) #H1 #H2 #EQ %[@1]
            (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
            change in ⊢ (? → ??%?) with (execute_1_0 ??)
@@ -2172 +2248 @@
            >H2b >(eq_instruction_to_eq … H2a)
            generalize in match EQ; -EQ;
+           whd in ⊢ (???% → ??%?);
+           cases (half_add ???) #carry #new_sp normalize nodelta;
+           >(eq_bv_to_eq … H2c)
+           change with
+            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
+                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
+           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
+           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
+           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
+           cases (half_add ???) #carry' #new_sp' normalize nodelta;
            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
-           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX
-           generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP %
-       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
-           generalize in match
-            (refl ?
-             (sub_16_with_carry
-              (sigma 〈preamble,instr_list〉 (program_counter … ps))
-              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
-              false))
-           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
-           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
-           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
-           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (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 #H2b whd in ⊢ (% → ?) #H2c
-           >H2b >(eq_instruction_to_eq … H2a)
-           generalize in match EQ; -EQ;
-           whd in ⊢ (???% → ?);
-           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
-           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
-           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
-           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
-           generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP
-           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
-           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
+           @split_eq_status;(* whd in ⊢ (??%%)*)
+            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
+              >code_memory_write_at_stack_pointer %
+            | change with
+               (low_internal_ram ?
+                (write_at_stack_pointer ?
+                 (set_8051_sfr ?
+                  (write_at_stack_pointer ?
+                   (set_low_internal_ram ? ps
+                    (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? ps)))
+                  pc_bl) ??) pc_bu) = ?)
+            |
+            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
+              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
+              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
+              >external_ram_write_at_stack_pointer %
+            | change with (? = sigma ?(address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
+              >EQ0 % 
+            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
+              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8051_write_at_stack_pointer %
+            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
+              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8052_write_at_stack_pointer %
+            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
+              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p1_latch_write_at_stack_pointer %
+            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
+              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p3_latch_write_at_stack_pointer %
+            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
+              >clock_write_at_stack_pointer whd in ⊢ (???%)
+              >clock_write_at_stack_pointer whd in ⊢ (???%)
+              >clock_write_at_stack_pointer %]
        | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
          generalize in match
@@ -2232 +2329 @@
              ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
            cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
-           generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP           
            @split_eq_status try %
             [ change with (? = sigma ? (address_of_word_labels ps label))
               (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
             | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
-              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
-(*  |5: (* Call *) #label
+              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
+  |4: (* Jmp *) #label #MAP
+      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
       whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
-       [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1]
+       [3: (* long *) #H1 #H2 #EQ %[@1]
            (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
            change in ⊢ (? → ??%?) with (execute_1_0 ??)
@@ -2247 +2344 @@
            >H2b >(eq_instruction_to_eq … H2a)
            generalize in match EQ; -EQ;
-           [2: whd in ⊢ (???% → ??%?);
-               cases (half_add ???) #carry #new_sp normalize nodelta;
-               >(eq_bv_to_eq … H2c)
-               change with
-                ((?=let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 newppc in ?) →
-                    (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
-               (* MISMATCH ON WHAT IS ON THE STACK!!!! *)
-               (* HOW TO PROVE THIS?? *)
-           ]
            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
-           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX
-            [2: % | ]
-       |4: (* short Call *) #abs @⊥ destruct (abs)
-       |1: (* short Jmp *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
+       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
            generalize in match
             (refl ?
@@ -2315 +2401 @@
              (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
              ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
-           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
+           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7    
            @split_eq_status try %
             [ change with (? = sigma ? (address_of_word_labels ps label))
               (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
             | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
-              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
+              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
   | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
     [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]