Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (7 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r2172 r2272  
    2727  #m #s #v
    2828  whd in match write_at_stack_pointer; normalize nodelta
    29   cases(vsplit … 4 4 ?) #nu #nl normalize nodelta
    30   cases(get_index_v … 4 nu 0 ?) //
     29  cases(vsplit … 1 7 ?) #bit_one #seven_bits normalize nodelta
     30  cases (head' bool ??) normalize nodelta //
    3131qed.
    3232
     
    236236  = special_function_registers_8051 T cm s.
    237237 #T #cm #s #x whd in ⊢ (??(???%)?);
    238  cases (vsplit ????) #nu #nl normalize nodelta;
    239  cases (get_index_v bool ????) %
     238 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     239  cases (head' bool ??) normalize nodelta %
    240240qed.
    241241
     
    297297 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
    298298 #T #cm #s #x whd in ⊢ (??(???%)?);
    299  cases (vsplit ????) #nu #nl normalize nodelta;
    300  cases (get_index_v bool ????) %
     299 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     300 cases (head' bool ??) %
    301301qed.
    302302
     
    306306  = special_function_registers_8052 T cm s.
    307307 #T #cm #s #x whd in ⊢ (??(???%)?);
    308  cases (vsplit ????) #nu #nl normalize nodelta;
    309  cases (get_index_v bool ????) %
     308 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     309 cases (head' bool ??) %
    310310qed.
    311311
     
    313313 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
    314314 #T #cm #s #x whd in ⊢ (??(???%)?);
    315  cases (vsplit ????) #nu #nl normalize nodelta;
    316  cases (get_index_v bool ????) %
     315 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     316 cases (head' bool ??) %
    317317qed.
    318318
     
    320320 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
    321321 #T #cm #s #x whd in ⊢ (??(???%)?);
    322  cases (vsplit ????) #nu #nl normalize nodelta;
    323  cases (get_index_v bool ????) %
     322 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     323 cases (head' bool ??) %
    324324qed.
    325325
     
    412412  #m #cm #s #v
    413413  whd in match write_at_stack_pointer; normalize nodelta
    414   cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
    415   cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
     414 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     415 cases (head' bool ??) %
    416416qed.
    417417
Note: See TracChangeset for help on using the changeset viewer.