Ignore:
Timestamp:
Jun 10, 2011, 3:20:34 AM (8 years ago)
Author:
sacerdot
Message:

New proof strategy.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r932 r933  
    19301930       whd in ⊢ (???% → ??%?);
    19311931       >ignore_clock
    1932        >get_arg_8_set_program_counter [2,4,6:%]
    1933        >get_arg_8_set_program_counter [2,4,6:%]
    1934        >get_arg_8_set_program_counter [2,4,6:%]
    1935        >get_arg_8_set_program_counter [2,4,6:%]
    1936        >get_arg_8_set_code_memory
    1937        >get_arg_8_set_program_counter [2,4,6:%]
    1938        >get_arg_8_set_program_counter [2,4,6:%]
    1939        >get_arg_8_set_code_memory
    1940        [1,2: cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?)
    1941        | cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?)]
     1932       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
     1933       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
     1934       normalize nodelta;
     1935       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    19421936       #result #flags
    19431937       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
    1944        >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 
     1938       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
    19451939    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
    19461940       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     
    19551949       [1,2,3,4: cases (half_add ???) #carry #result
    19561950        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
    1957         whd in ⊢ (??%%)
    1958          %
     1951        XXX
    19591952       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
    19601953 
Note: See TracChangeset for help on using the changeset viewer.