Ignore:
Timestamp:
Jun 10, 2011, 2:53:49 AM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r930 r931  
    19211921  |6: (* Mov *)
    19221922  | (* Instruction *) -pi; *
    1923     [1,2: (* ADD, ADDC *) #arg1 #arg2 #H1 #H2 #EQ %[1,3:@1]
     1923    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #H1 #H2 #EQ %[1,3,5:@1]
    19241924       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    19251925       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    19301930       whd in ⊢ (???% → ??%?);
    19311931       >ignore_clock
    1932        >get_arg_8_set_program_counter [2,4:%]
    1933        >get_arg_8_set_program_counter [2,4:%]
    1934        >get_arg_8_set_program_counter [2,4:%]
    1935        >get_arg_8_set_program_counter [2,4:%]
     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) ?)]
     1942       #result #flags
     1943       #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 %
     1945    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
     1946       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     1947       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     1948       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     1949       * #H2a whd in ⊢ (% → ?) #H2b
     1950       >ignore_clock in EQ;
     1951       >(eq_instruction_to_eq … H2a)
     1952       whd in ⊢ (???% → ??%?);
     1953       >ignore_clock
     1954       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
     1955       [1,2,3,4: XXX
     1956       >get_arg_8_set_program_counter try % [2:%]
     1957       >get_arg_8_set_program_counter [2:%]
     1958       >get_arg_8_set_program_counter [2:%]
    19361959       >get_arg_8_set_code_memory
    19371960       >get_arg_8_set_program_counter [2,4:%]
    19381961       >get_arg_8_set_program_counter [2,4:%]
    19391962       >get_arg_8_set_code_memory
    1940        cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags
    1941        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
     1963       cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags
     1964       *)#EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; %
    19421965       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
    1943     |
     1966 
Note: See TracChangeset for help on using the changeset viewer.