Changeset 948


Ignore:
Timestamp:
Jun 13, 2011, 3:28:26 PM (8 years ago)
Author:
sacerdot
Message:

Some progress on the Call case.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r946 r948  
    20472047qed.
    20482048
     2049lemma special_function_registers_8051_write_at_stack_pointer:
     2050 ∀T,s,x.
     2051    special_function_registers_8051 T (write_at_stack_pointer T s x)
     2052  = special_function_registers_8051 T s.
     2053 #T #s #x whd in ⊢ (??(??%)?)
     2054 cases (split ????) #nu #nl normalize nodelta;
     2055 cases (get_index_v bool ????) %
     2056qed.
     2057
     2058lemma get_8051_sfr_write_at_stack_pointer:
     2059 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
     2060 #T #s #x #y whd in ⊢ (??%%) //
     2061qed.
     2062
     2063lemma code_memory_write_at_stack_pointer:
     2064 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
     2065 #T #s #x whd in ⊢ (??(??%)?)
     2066 cases (split ????) #nu #nl normalize nodelta;
     2067 cases (get_index_v bool ????) %
     2068qed.
     2069
     2070(*
     2071lemma low_internal_ram_write_at_stack_pointer:
     2072 ∀T,s,x. low_internal_ram T (write_at_stack_pointer T s x) = low_internal_ram T s.
     2073 #T #s #x whd in ⊢ (??(??%)?)
     2074 cases (split ????) #nu #nl normalize nodelta;
     2075 cases (get_index_v bool ????) normalize nodelta; //
     2076qed.
     2077
     2078lemma high_internal_ram_write_at_stack_pointer:
     2079 ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s.
     2080 #T #s #x whd in ⊢ (??(??%)?)
     2081 cases (split ????) #nu #nl normalize nodelta;
     2082 cases (get_index_v bool ????) %
     2083qed.
     2084*)
     2085
     2086lemma external_ram_write_at_stack_pointer:
     2087 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
     2088 #T #s #x whd in ⊢ (??(??%)?)
     2089 cases (split ????) #nu #nl normalize nodelta;
     2090 cases (get_index_v bool ????) %
     2091qed.
     2092
     2093lemma special_function_registers_8052_write_at_stack_pointer:
     2094 ∀T,s,x.
     2095    special_function_registers_8052 T (write_at_stack_pointer T s x)
     2096  = special_function_registers_8052 T s.
     2097 #T #s #x whd in ⊢ (??(??%)?)
     2098 cases (split ????) #nu #nl normalize nodelta;
     2099 cases (get_index_v bool ????) %
     2100qed.
     2101
     2102lemma p1_latch_write_at_stack_pointer:
     2103 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
     2104 #T #s #x whd in ⊢ (??(??%)?)
     2105 cases (split ????) #nu #nl normalize nodelta;
     2106 cases (get_index_v bool ????) %
     2107qed.
     2108
     2109lemma p3_latch_write_at_stack_pointer:
     2110 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
     2111 #T #s #x whd in ⊢ (??(??%)?)
     2112 cases (split ????) #nu #nl normalize nodelta;
     2113 cases (get_index_v bool ????) %
     2114qed.
     2115
     2116lemma clock_write_at_stack_pointer:
     2117 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
     2118 #T #s #x whd in ⊢ (??(??%)?)
     2119 cases (split ????) #nu #nl normalize nodelta;
     2120 cases (get_index_v bool ????) %
     2121qed.
     2122
    20492123lemma eq_rect_Type1_r:
    20502124  ∀A: Type[1].
     
    21632237       #result #flags
    21642238       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
    2165   |4: (* Jmp *) #label #MAP
     2239  |5: (* Call *) #label #MAP
     2240      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
    21662241      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
    2167        [3: (* long *) #H1 #H2 #EQ %[@1]
     2242       [ (* short *) #abs @⊥ destruct (abs)
     2243       |3: (* long *) #H1 #H2 #EQ %[@1]
    21682244           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    21692245           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    21722248           >H2b >(eq_instruction_to_eq … H2a)
    21732249           generalize in match EQ; -EQ;
     2250           whd in ⊢ (???% → ??%?);
     2251           cases (half_add ???) #carry #new_sp normalize nodelta;
     2252           >(eq_bv_to_eq … H2c)
     2253           change with
     2254            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
     2255                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
     2256           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
     2257           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;
     2258           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
     2259           cases (half_add ???) #carry' #new_sp' normalize nodelta;
    21742260           #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 *)
     2261           @split_eq_status;(* whd in ⊢ (??%%)*)
     2262            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
     2263              >code_memory_write_at_stack_pointer %
     2264            | change with
     2265               (low_internal_ram ?
     2266                (write_at_stack_pointer ?
     2267                 (set_8051_sfr ?
     2268                  (write_at_stack_pointer ?
     2269                   (set_low_internal_ram ? ps
     2270                    (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? ps)))
     2271                  pc_bl) ??) pc_bu) = ?)
     2272            |
     2273            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
     2274              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
     2275              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
     2276              >external_ram_write_at_stack_pointer %
     2277            | change with (? = sigma ?(address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
     2278              >EQ0 %
     2279            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
     2280              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
     2281              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
     2282              >special_function_registers_8051_write_at_stack_pointer %
     2283            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
     2284              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
     2285              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
     2286              >special_function_registers_8052_write_at_stack_pointer %
     2287            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
     2288              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
     2289              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
     2290              >p1_latch_write_at_stack_pointer %
     2291            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
     2292              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
     2293              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
     2294              >p3_latch_write_at_stack_pointer %
     2295            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
     2296              >clock_write_at_stack_pointer whd in ⊢ (???%)
     2297              >clock_write_at_stack_pointer whd in ⊢ (???%)
     2298              >clock_write_at_stack_pointer %]
    22022299       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    22032300         generalize in match
     
    22322329             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
    22332330           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
    2234            generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP           
    22352331           @split_eq_status try %
    22362332            [ change with (? = sigma ? (address_of_word_labels ps label))
    22372333              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    22382334            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    2239               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    2240 (*  |5: (* Call *) #label
     2335              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
     2336  |4: (* Jmp *) #label #MAP
     2337      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
    22412338      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
    2242        [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1]
     2339       [3: (* long *) #H1 #H2 #EQ %[@1]
    22432340           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    22442341           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    22472344           >H2b >(eq_instruction_to_eq … H2a)
    22482345           generalize in match EQ; -EQ;
    2249            [2: whd in ⊢ (???% → ??%?);
    2250                cases (half_add ???) #carry #new_sp normalize nodelta;
    2251                >(eq_bv_to_eq … H2c)
    2252                change with
    2253                 ((?=let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 newppc in ?) →
    2254                     (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    2255                (* MISMATCH ON WHAT IS ON THE STACK!!!! *)
    2256                (* HOW TO PROVE THIS?? *)
    2257            ]
    22582346           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
    2259            cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX
    2260             [2: % | ]
    2261        |4: (* short Call *) #abs @⊥ destruct (abs)
    2262        |1: (* short Jmp *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     2347           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
     2348       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    22632349           generalize in match
    22642350            (refl ?
     
    23152401             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
    23162402             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
    2317            cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
     2403           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
    23182404           @split_eq_status try %
    23192405            [ change with (? = sigma ? (address_of_word_labels ps label))
    23202406              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    23212407            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    2322               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
     2408              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    23232409  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    23242410    [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.