Changeset 2197 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jul 17, 2012, 3:23:51 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2195 r2197 241 241 (nat_of_bitvector … 242 242 (add … (sigma ppc) (bitvector_of_nat … j)))))) 243 [1: #j #H <load_code_memory_ok 244 [ @assembly_ok 245  cut (0=assembled' → False) 246 [ #abs <abs in assembly_ok4; >EQlen #abs' 247 @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY 248 cases assembly_ok3 assembly_ok3 249 [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ] 250 #EQlen_assembled' <EQlen_assembled' 251 cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok 252 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 253 whd in match instruction_size; normalize nodelta 254 >create_label_cost_refl 255 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 256 [>eq_assembly_1_pseudoinstruction 2: skip] #OK >OK <EQlen * 257 [2: * #EQ1 #EQ2 258 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))))) 259 [1: @lt_to_lt_nat_of_bitvector_add try assumption 260 cases daemon (* XXX: two cases to prove, both true *) 261 2: cases daemon (* XXX: use monotonicity of sigma *) 262 ] 263 ] 264 cases (le_to_or_lt_eq … instr_list_ok) 265 [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero 266 assumption ] 267 #instr_list_ok' #NO_OVERFLOW 268 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))))) 269 [ @lt_to_lt_nat_of_bitvector_add 270 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 271 / by / 272  <EQlen assumption 273  assumption 274 ] 275  <EQlen <OK 276 cases (monotone_sigma ???? sigma_policy_witness 277 (add … ppc (bitvector_of_nat … 1)) 278 (bitvector_of_nat … (instr_list)) ??) try assumption 279 [ #H @H 280 3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse 281 try % assumption 282 4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption 283 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption 284 @(transitive_le … instr_list_ok') @le_S_S assumption 285  #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]] 243 [1: #j #H cases (assembly_ok … H) #K assembly_ok #assembly_ok <load_code_memory_ok 244 [ @assembly_ok  skip ] 286 245 2: 287 246 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len
Note: See TracChangeset
for help on using the changeset viewer.