Changeset 946 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 13, 2011, 11:37:46 AM (10 years ago)

Author:

sacerdot

Message:

Jmp case repaired after addition of MAP hypothesis.

File:

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

src/ASM/AssemblyProof.ma

@@ -2068 +2068 @@
 qed.
 
+(*
 lemma blah:
   ∀p: pseudo_instruction.
@@ -2085 +2086 @@
                      else None internal_pseudo_address_map )
                     =Some internal_pseudo_address_map M')
+*)
 
 lemma main_thm:
@@ -2161 +2163 @@
        #result #flags
        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
-(*  |4,5: (* Jmp, Call *) #label
+  |4: (* Jmp *) #label #MAP
+      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
+       [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 ??)
+           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;
+           #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 *)
+       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+         generalize in match
+          (refl …
+            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
+         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
+         generalize in match
+          (refl …
+            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
+         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
+         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
+         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
+         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #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) whd in ⊢ (??%?)
+           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
+           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
+           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
+           generalize in match (refl … (split bool 4 4 pc_bu))
+           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
+           generalize in match (refl … (split bool 3 8 rest_addr))
+           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
+           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
+           generalize in match
+            (refl …
+             (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
+           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
       whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
        [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1]
@@ -2243 +2320 @@
               (* 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 *)*) *)
+              @(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]