Ignore:
Timestamp:
Jun 11, 2011, 11:37:20 PM (8 years ago)
Author:
sacerdot
Message:

Jmp case finished up to arithmetical properties.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r940 r941  
    19621962qed.
    19631963
     1964lemma split_eq_status:
     1965 ∀T.
     1966 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
     1967 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
     1968  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
     1969   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
     1970   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
     1971 //
     1972qed.
     1973
    19641974lemma main_thm:
    19651975 ∀ps,s,s''.
     
    20172027           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
    20182028           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    2019        | (* short *)
    2020        | (* medium *)
    2021        ]
     2029       | (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     2030           generalize in match
     2031            (refl ?
     2032             (sub_16_with_carry
     2033              (sigma 〈preamble,instr_list〉 (program_counter … ps))
     2034              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
     2035              false))
     2036           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
     2037           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
     2038           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
     2039           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
     2040           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     2041           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     2042           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2043           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     2044           >H2b >(eq_instruction_to_eq … H2a)
     2045           generalize in match EQ; -EQ;
     2046           whd in ⊢ (???% → ?);
     2047           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     2048           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
     2049           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
     2050           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
     2051           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
     2052           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
     2053       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     2054         generalize in match
     2055          (refl …
     2056            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
     2057         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
     2058         generalize in match
     2059          (refl …
     2060            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
     2061         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
     2062         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
     2063         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
     2064         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
     2065         change in ⊢ (? →??%?) with (execute_1_0 ??)
     2066           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2067           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     2068           >H2b >(eq_instruction_to_eq … H2a)
     2069           generalize in match EQ; -EQ;
     2070           whd in ⊢ (???% → ?);
     2071           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     2072           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
     2073           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
     2074           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
     2075           generalize in match (refl … (split bool 4 4 pc_bu))
     2076           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
     2077           generalize in match (refl … (split bool 3 8 rest_addr))
     2078           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
     2079           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
     2080           generalize in match
     2081            (refl …
     2082             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
     2083             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
     2084           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
     2085           @split_eq_status try %
     2086            [ change with (? = sigma ? (address_of_word_labels ps label))
     2087              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
     2088            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
     2089              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    20222090  |5: (* Call *)
    20232091  |6: (* Mov *)
Note: See TracChangeset for help on using the changeset viewer.