Changeset 946


Ignore:
Timestamp:
Jun 13, 2011, 11:37:46 AM (8 years ago)
Author:
sacerdot
Message:

Jmp case repaired after addition of MAP hypothesis.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r945 r946  
    20682068qed.
    20692069
     2070(*
    20702071lemma blah:
    20712072  ∀p: pseudo_instruction.
     
    20852086                     else None internal_pseudo_address_map )
    20862087                    =Some internal_pseudo_address_map M')
     2088*)
    20872089
    20882090lemma main_thm:
     
    21612163       #result #flags
    21622164       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
    2163 (*  |4,5: (* Jmp, Call *) #label
     2165  |4: (* Jmp *) #label #MAP
     2166      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
     2167       [3: (* long *) #H1 #H2 #EQ %[@1]
     2168           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     2169           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     2170           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2171           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     2172           >H2b >(eq_instruction_to_eq … H2a)
     2173           generalize in match EQ; -EQ;
     2174           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     2175           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX
     2176           generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP %
     2177       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     2178           generalize in match
     2179            (refl ?
     2180             (sub_16_with_carry
     2181              (sigma 〈preamble,instr_list〉 (program_counter … ps))
     2182              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
     2183              false))
     2184           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
     2185           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
     2186           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
     2187           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
     2188           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     2189           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     2190           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2191           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     2192           >H2b >(eq_instruction_to_eq … H2a)
     2193           generalize in match EQ; -EQ;
     2194           whd in ⊢ (???% → ?);
     2195           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     2196           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
     2197           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
     2198           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
     2199           generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP
     2200           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
     2201           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
     2202       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     2203         generalize in match
     2204          (refl …
     2205            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
     2206         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
     2207         generalize in match
     2208          (refl …
     2209            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
     2210         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
     2211         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
     2212         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
     2213         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
     2214         change in ⊢ (? →??%?) with (execute_1_0 ??)
     2215           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2216           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     2217           >H2b >(eq_instruction_to_eq … H2a)
     2218           generalize in match EQ; -EQ;
     2219           whd in ⊢ (???% → ?);
     2220           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     2221           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
     2222           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
     2223           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
     2224           generalize in match (refl … (split bool 4 4 pc_bu))
     2225           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
     2226           generalize in match (refl … (split bool 3 8 rest_addr))
     2227           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
     2228           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
     2229           generalize in match
     2230            (refl …
     2231             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
     2232             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
     2233           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
     2234           generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP           
     2235           @split_eq_status try %
     2236            [ change with (? = sigma ? (address_of_word_labels ps label))
     2237              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
     2238            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
     2239              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
     2240(*  |5: (* Call *) #label
    21642241      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
    21652242       [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1]
     
    22432320              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    22442321            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    2245               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    2246   (*|5: (* Call *)*) *)
     2322              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
    22472323  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    22482324    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
Note: See TracChangeset for help on using the changeset viewer.