Changeset 931 for src

Timestamp:

Jun 10, 2011, 2:53:49 AM (10 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -1921 +1921 @@
   |6: (* Mov *)
   | (* Instruction *) -pi; *
-    [1,2: (* ADD, ADDC *) #arg1 #arg2 #H1 #H2 #EQ %[1,3:@1]
+    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #H1 #H2 #EQ %[1,3,5:@1]
        normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
        change in ⊢ (? → ??%?) with (execute_1_0 ??)
@@ -1930 +1930 @@
        whd in ⊢ (???% → ??%?);
        >ignore_clock
-       >get_arg_8_set_program_counter [2,4:%]
-       >get_arg_8_set_program_counter [2,4:%]
-       >get_arg_8_set_program_counter [2,4:%]
-       >get_arg_8_set_program_counter [2,4:%]
+       >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) ?)]
+       #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 % 
+    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
+       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+       change in ⊢ (? → ??%?) with (execute_1_0 ??)
+       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+       * #H2a whd in ⊢ (% → ?) #H2b
+       >ignore_clock in EQ;
+       >(eq_instruction_to_eq … H2a)
+       whd in ⊢ (???% → ??%?);
+       >ignore_clock
+       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
+       [1,2,3,4: XXX
+       >get_arg_8_set_program_counter try % [2:%]
+       >get_arg_8_set_program_counter [2:%]
+       >get_arg_8_set_program_counter [2:%]
        >get_arg_8_set_code_memory
        >get_arg_8_set_program_counter [2,4:%]
        >get_arg_8_set_program_counter [2,4:%]
        >get_arg_8_set_code_memory
-       cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags
-       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
+       cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #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 % 
-    |
+