- Timestamp:
- Jun 13, 2012, 5:00:35 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2051 r2062 27 27 λinstr_list. 28 28 ∀id: Identifier. 29 ∀ppc. 29 ∀ppc. ∀ppc_ok. 30 30 ∀i. 31 fetch_pseudo_instruction instr_list ppc = i →31 fetch_pseudo_instruction instr_list ppc ppc_ok = i → 32 32 instruction_has_label id (\fst i) → 33 33 occurs_exactly_once ASMTag pseudo_instruction id instr_list. … … 105 105 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 106 106 ∀ps: PseudoStatus program. 107 ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) ≤|\snd program|.108 next_internal_pseudo_address_map M program ps = Some … M' →107 ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|. 108 next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' → 109 109 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 110 110 status_of_pseudo_status M' … 111 (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. 112 #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds 111 (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy. 112 #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps 113 letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds 113 114 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 114 @(pose … (program_counter ?? ps)) #ppc #EQppc 115 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?; 115 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?; 116 116 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta 117 117 @pair_elim #assembled #costs' #assembly_refl normalize nodelta … … 121 121 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 122 122 whd in match execute_1_pseudo_instruction; normalize nodelta 123 whd in match ticks_of; normalize nodelta <EQppc>fetch_pseudo_refl normalize nodelta124 lapply (snd_fetch_pseudo_instruction instr_list ppc ) >fetch_pseudo_refl #EQnewppc >EQnewppc123 whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta 124 lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc 125 125 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?) 126 [1: >fetch_pseudo_refl % |2: >EQppc assumption]126 [1: >fetch_pseudo_refl % |2: skip ] 127 127 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; 128 128 generalize in match assm1; -assm1 -assm2 -assm3 … … 144 144 whd in ⊢ (??%?); 145 145 @split_eq_status try % 146 /demod/ > EQnewppc >sigma_increment_commutation<add_zero % (*CSC: auto not working, why? *)146 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) 147 147 |6: (* Mov *) 148 148 #arg1 #arg2 #_ … … 158 158 whd in match (execute_1_pseudo_instruction0 ?????); 159 159 (* XXX: work on the left hand side of the equality *) 160 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc160 whd in ⊢ (??%?); whd in match (program_counter ???); 161 161 (* XXX: execute fetches some more *) 162 162 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta … … 189 189 #instr #_ #EQP #EQnext #fetch_many_assm 190 190 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness 191 ps ppc EQppclabels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels191 ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels 192 192 EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …) 193 193 (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) 194 194 (refl …) ? (refl …)) 195 try assumption >assembly_refl <EQppcassumption196 |4: 195 try assumption try % >assembly_refl assumption 196 |4: (* Jmp *) 197 197 #arg1 #pi_refl 198 198 (* XXX: we first work on sigma_increment_commutation *) … … 214 214 %{1} 215 215 (* XXX: work on the left hand side of the equality *) 216 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc216 whd in ⊢ (??%?); whd in match (program_counter ???); 217 217 (* XXX: execute fetches some more *) 218 218 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta … … 272 272 ] 273 273 |5: (* Call *) 274 #arg1 274 #arg1 #_ 275 275 (* XXX: we first work on sigma_increment_commutation *) 276 276 #sigma_increment_commutation -
src/ASM/Interpret.ma
r2056 r2062 1222 1222 1223 1223 definition execute_1_pseudo_instruction: 1224 (Word → nat × nat) → ∀cm.∀s:PseudoStatus cm.1224 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm. 1225 1225 nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd cm| → 1226 1226 PseudoStatus cm 1227 1227 ≝ 1228 λ ticks_of,cm,s,pc_ok.1228 λcm,ticks_of,s,pc_ok. 1229 1229 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in 1230 let ticks ≝ ticks_of (program_counter … s) in1230 let ticks ≝ ticks_of (program_counter … s) pc_ok in 1231 1231 execute_1_pseudo_instruction0 ticks cm s instr pc. 1232 1232
Note: See TracChangeset
for help on using the changeset viewer.