Changeset 933 for src

Timestamp:

Jun 10, 2011, 3:20:34 AM (10 years ago)

Author:

sacerdot

Message:

New proof strategy.

File:

• src/ASM/AssemblyProof.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -1930 +1930 @@
        whd in ⊢ (???% → ??%?);
        >ignore_clock
-       >get_arg_8_set_program_counter [2,4,6:%]
-       >get_arg_8_set_program_counter [2,4,6:%]
-       >get_arg_8_set_program_counter [2,4,6:%]
-       >get_arg_8_set_program_counter [2,4,6:%]
-       >get_arg_8_set_code_memory
-       >get_arg_8_set_program_counter [2,4,6:%]
-       >get_arg_8_set_program_counter [2,4,6:%]
-       >get_arg_8_set_code_memory
-       [1,2: cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?)
-       | cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?)]
+       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
+       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
+       normalize nodelta;
+       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
        #result #flags
        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
-       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 
+       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
     | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
        normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
@@ -1955 +1949 @@
        [1,2,3,4: cases (half_add ???) #carry #result
         #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
-        whd in ⊢ (??%%)
-         %
+        XXX
        >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %