Changeset 989 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 17, 2011, 10:28:19 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r988 r989 1670 1670 qed. 1671 1671 1672 axiom get_arg_8_set_low_internal_ram: 1673 ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z. 1674 1672 1675 lemma eq_rect_Type1_r: 1673 1676 ∀A: Type[1]. … … 1872 1875 #result #flags 1873 1876 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *) 1874 |5: (* Call *) #label #MAP1877 (* |5: (* Call *) #label #MAP 1875 1878 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP; 1876 1879 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta; … … 2060 2063 | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2061 2064 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2062 | (* Instruction *) -pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta;2065 *) | (* Instruction *) -pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta; 2063 2066 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1] 2064 2067 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2065 2068 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2066 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2069 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2067 2070 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2068 2071 >H2b >(eq_instruction_to_eq … H2a) … … 2070 2073 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; 2071 2074 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2 2072 normalize nodelta; #MAP; 2075 normalize nodelta; #MAP; (* 2073 2076 [1: change in ⊢ (? → %) with 2074 2077 ((let 〈result,flags〉 ≝ … … 2078 2081 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 2079 2082 false (DIRECT ARG2)) 2080 ? in ?) = ?) // 2081 [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2: 2082 [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)] 2083 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)] 2083 ? in ?) = ?) 2084 [2,3: %] 2085 change in ⊢ (???% → ?) with 2086 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?) 2087 >get_arg_8_set_clock *) 2088 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ? 2089 [2,4: #abs @⊥ normalize in abs; destruct (abs) 2090 |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)] 2091 [ change in ⊢ (? → %) with 2092 ((let 〈result,flags〉 ≝ 2093 add_8_with_carry 2094 (get_arg_8 ? ps false ACC_A) 2095 (get_arg_8 ? 2096 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 2097 false (DIRECT ARG2)) 2098 ? in ?) = ?) 2099 >get_arg_8_set_low_internal_ram 2100 2101 cases (add_8_with_carry ???) 2102 2103 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)] 2084 2104 #result #flags 2085 2105 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
Note: See TracChangeset
for help on using the changeset viewer.