Changeset 1966 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 May 17, 2012, 5:45:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1963 r1966 3 3 include alias "basics/logic.ma". 4 4 5 axiom add_commutative: 6 ∀n: nat. 7 ∀l, r: BitVector n. 8 add … l r = add … r l. 5 lemma set_arg_16_mk_Status_commutation: 6 ∀M: Type[0]. 7 ∀cm: M. 8 ∀s: PreStatus M cm. 9 ∀w: Word. 10 ∀d: [[dptr]]. 11 set_arg_16 M cm s w d = 12 mk_PreStatus M cm 13 (low_internal_ram … s) 14 (high_internal_ram … s) 15 (external_ram … s) 16 (program_counter … s) 17 (special_function_registers_8051 … (set_arg_16 M cm s w d)) 18 (special_function_registers_8052 … s) 19 (p1_latch … s) 20 (p3_latch … s) 21 (clock … s). 22 #M #cm #s #w #d 23 whd in match set_arg_16; normalize nodelta 24 whd in match set_arg_16'; normalize nodelta 25 @(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ] 26 cases (split bool 8 8 w) #bu #bl normalize nodelta 27 whd in match set_8051_sfr; normalize nodelta % 28 qed. 29 30 lemma set_program_counter_mk_Status_commutation: 31 ∀M: Type[0]. 32 ∀cm: M. 33 ∀s: PreStatus M cm. 34 ∀w: Word. 35 set_program_counter M cm s w = 36 mk_PreStatus M cm 37 (low_internal_ram … s) 38 (high_internal_ram … s) 39 (external_ram … s) 40 w 41 (special_function_registers_8051 … s) 42 (special_function_registers_8052 … s) 43 (p1_latch … s) 44 (p3_latch … s) 45 (clock … s). 46 // 47 qed. 48 49 lemma set_clock_mk_Status_commutation: 50 ∀M: Type[0]. 51 ∀cm: M. 52 ∀s: PreStatus M cm. 53 ∀c: nat. 54 set_clock M cm s c = 55 mk_PreStatus M cm 56 (low_internal_ram … s) 57 (high_internal_ram … s) 58 (external_ram … s) 59 (program_counter … s) 60 (special_function_registers_8051 … s) 61 (special_function_registers_8052 … s) 62 (p1_latch … s) 63 (p3_latch … s) 64 c. 65 // 66 qed. 67 68 69 lemma special_function_registers_8051_set_arg_16: 70 ∀M, M': Type[0]. 71 ∀cm: M. 72 ∀cm': M'. 73 ∀s: PreStatus M cm. 74 ∀s': PreStatus M' cm'. 75 ∀w, w': Word. 76 ∀d, d': [[dptr]]. 77 (∀sfr: SFR8051. 78 sfr ≠ SFR_DPH → sfr ≠ SFR_DPL → 79 get_8051_sfr M cm s sfr = get_8051_sfr M' cm' s' sfr) → 80 w = w' → 81 special_function_registers_8051 ?? (set_arg_16 … s w d) = 82 special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d'). 83 #M #M' #cm #cm' #s #s' #w #w' #d 84 cases daemon 85 qed. 86 9 87 10 88 theorem main_thm: 11 89 ∀M. 12 90 ∀M'. 13 ∀cm. 14 ∀ps. 15 ∀sigma. 16 ∀policy. 17 next_internal_pseudo_address_map M cm ps = Some … M' → 91 ∀program: pseudo_assembly_program. 92 ∀sigma: Word → Word. 93 ∀policy: Word → bool. 94 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 95 ∀ps: PseudoStatus program. 96 next_internal_pseudo_address_map M program ps = Some … M' → 18 97 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 19 98 status_of_pseudo_status M' … 20 (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.21 #M #M' * #preamble #instr_list # ps #sigma #policy99 (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. 100 #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps 22 101 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 23 102 @(pose … (program_counter ?? ps)) #ppc #EQppc 24 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?; 25 @pair_elim #labels #costs #H0 normalize nodelta 26 @pair_elim #assembled #costs' #EQ1 normalize nodelta 27 @pair_elim #pi #newppc #EQ2 normalize nodelta 103 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?; 104 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta 105 @pair_elim #assembled #costs' #assembly_refl normalize nodelta 106 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled 107 @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta 28 108 @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels 29 109 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 30 110 whd in match execute_1_pseudo_instruction; normalize nodelta 31 whd in match ticks_of; normalize nodelta <EQppc >EQ2 normalize nodelta 32 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc 33 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?) 34 [1: >EQ2 % 35 2: 36 3: normalize nodelta 111 whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta 112 lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc 113 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?) 114 [1: >fetch_pseudo_refl % ] 115 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; 116 generalize in match assm1; assm1 assm2 assm3 117 normalize nodelta 37 118 cases pi 38 119 [2,3: 39 #ARG 40 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3; 41 #H2 42 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP 120 #arg 121 (* XXX: we first work on sigma_increment_commutation *) 122 #sigma_increment_commutation 123 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 124 (* XXX: we work on the maps *) 125 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 126 (* XXX: we assume the fetch_many hypothesis *) 127 #fetch_many_assm 128 (* XXX: we give the existential *) 129 %{0} 43 130 whd in match (execute_1_pseudo_instruction0 ?????); 44 %{0} @split_eq_status // 45 [1,2: /demod/ >EQnewppc >H3 <add_zero % (*CSC: auto not working, why? *) ] 46 6: (* Mov *) #arg1 #arg2 131 (* XXX: work on the left hand side of the equality *) 132 whd in ⊢ (??%?); 133 @split_eq_status // 134 [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ] 135 6: (* Mov *) 136 #arg1 #arg2 137 (* XXX: we first work on sigma_increment_commutation *) 138 #sigma_increment_commutation 139 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 140 (* XXX: we work on the maps *) 141 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 142 (* XXX: we assume the fetch_many hypothesis *) 143 #fetch_many_assm 144 (* XXX: we give the existential *) 145 %{1} 146 whd in match (execute_1_pseudo_instruction0 ?????); 147 (* XXX: work on the left hand side of the equality *) 148 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 149 (* XXX: execute fetches some more *) 150 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 151 whd in fetch_many_assm; 152 >EQassembled in fetch_many_assm; 153 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 154 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 155 #fetch_many_assm whd in fetch_many_assm; 156 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 157 >(eq_instruction_to_eq … eq_instr) instr whd in ⊢ (??%?); 158 (* XXX: now we start to work on the mk_PreStatus equality *) 159 change with (set_arg_16 ????? = ?) 160 >set_program_counter_mk_Status_commutation 161 >set_clock_mk_Status_commutation 162 >set_arg_16_mk_Status_commutation 163 164 change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??) 165 >set_program_counter_mk_Status_commutation 166 >set_clock_mk_Status_commutation 167 >set_arg_16_mk_Status_commutation in ⊢ (???%); 168 169 170 @split_eq_status // 171 [1: 172 assumption 173 2: 174 @special_function_registers_8051_set_arg_16 175 [2: 176 >EQlookup_datalabels % 177 1: 178 * 179 #absurd1 #absurd2 180 try (@⊥ cases absurd1 absurd #absurd1 @absurd1 %) 181 try (@⊥ cases absurd2 absurd #absurd2 @absurd2 %) 182 whd in ⊢ (??%%); cases daemon (* XXX: not nice! manipulation of vectors; true though *) 183 ] 184 ] 185 186 (* 187 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1 whd in ⊢ (??%?); 188 whd in match (get_arg_16 ????); whd in match (set_arg_16' ?????); 189 190 @split_eq_status 191 192 193 #fetch_many_assm 194 >assembly_refl in fetch_many_assm; 195 196 cases (fetch ??) * #instr #newppc' #ticks normalize nodelta 197 whd in ⊢ (??%?); 198 199 47 200 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3; 48 201 #H2 … … 70 223 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % 71 224 72 225 *) 73 226 74 227 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?); … … 130 283 @low_internal_ram_write_at_stack_pointer 131 284 [ >EQ0 @pol  %  % 132  @( pair_destruct_2… EQ1)285  @( … EQ1) 133 286  @(pair_destruct_2 … EQ2) 134 287  >(pair_destruct_1 ????? EQpc)
Note: See TracChangeset
for help on using the changeset viewer.