Changeset 989 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 17, 2011, 10:28:19 AM (10 years ago)

Author:

sacerdot

Message:

Type of build_maps strengthened.

File:

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

src/ASM/AssemblyProof.ma

@@ -1670 +1670 @@
 qed.
 
+axiom get_arg_8_set_low_internal_ram:
+ ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
+
 lemma eq_rect_Type1_r:
   ∀A: Type[1].
@@ -1872 +1875 @@
        #result #flags
        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
-  |5: (* Call *) #label #MAP
+(*  |5: (* Call *) #label #MAP
       generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
       whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
@@ -2060 +2063 @@
             | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
-  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
+*)  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
     [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #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 ??)
-       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
        * * #H2a #H2b whd in ⊢ (% → ?) #H2c
        >H2b >(eq_instruction_to_eq … H2a)
@@ -2070 +2073 @@
        @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
        @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
-       normalize nodelta; #MAP;
+       normalize nodelta; #MAP; (*
        [1: change in ⊢ (? → %) with
         ((let 〈result,flags〉 ≝
@@ -2078 +2081 @@
              (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
              false (DIRECT ARG2))
-           ? in ?) = ?) //
-       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
-        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
-       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
+           ? in ?) = ?)
+        [2,3: %]
+        change in ⊢ (???% → ?) with
+         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
+        >get_arg_8_set_clock *)
+       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
+         [2,4: #abs @⊥ normalize in abs; destruct (abs)
+         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
+       [ change in ⊢ (? → %) with
+        ((let 〈result,flags〉 ≝
+          add_8_with_carry
+           (get_arg_8 ? ps false ACC_A)
+           (get_arg_8 ?
+             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
+             false (DIRECT ARG2))
+           ? in ?) = ?)
+          >get_arg_8_set_low_internal_ram
+       
+        cases (add_8_with_carry ???)
+         
+        [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_eq … H2c) %