- Timestamp:
- Jun 28, 2012, 10:41:59 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2131 r2132 180 180 ]. 181 181 182 lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels: 183 ∀lookup_labels,sigma,policy,ppc,pi. 184 ∀lookup_datalabels1,lookup_datalabels2. 185 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) = 186 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi). 187 #lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2 188 cases pi // 189 qed. 190 191 lemma fst_snd_assembly_1_pseudoinstruction: 192 ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled. 193 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi 194 = 〈len,assembled〉 → 195 len = |assembled|. 196 #lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled 197 inversion (assembly_1_pseudoinstruction ??????) #len' #assembled' 198 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct % 199 qed. 200 182 201 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *) 183 202 lemma assembly_ok: … … 224 243 #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f 225 244 >eq_fetch_pseudo_instruction whd in match instruction_size; 226 normalize nodelta (*CSC: TRUE, NEEDS LEMMA *) 227 cases daemon 245 normalize nodelta >create_label_cost_refl 246 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 247 [>eq_assembly_1_pseudoinstruction % | skip] 228 248 | lapply (load_code_memory_ok assembled' ?) [ assumption ] 229 249 #load_code_memory_ok 230 cut (len=|assembled|) 231 [1: (*CSC: provable before cleaning *) 232 cases daemon 233 ] 234 #EQlen 250 lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen 235 251 (* Nice statement here *) 236 252 cut (∀j. ∀H: j < |assembled|.
Note: See TracChangeset
for help on using the changeset viewer.