 Timestamp:
 Jun 29, 2012, 10:09:10 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2138 r2142 406 406 [1: #j #H <load_code_memory_ok 407 407 [ @assembly_ok 408  cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))) ≤ assembled') 409 [ cases sigma_policy_witness #_ #sigma_ok cases daemon 410 (*CSC: True, propagate already proved invariant*) 411  #LE @(lt_to_le_to_lt … LE) 412 @lt_to_lt_nat_of_bitvector_add 413 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 414 / by / 415  @(transitive_le ???? assembly_ok1) change with (? < ?) cases daemon 416 (*CSC: Same as before*) 417  assumption 418 ] 408  cases (le_to_or_lt_eq … assembly_ok1) 409 [ #assembly_ok1' 410 cut (nat_of_bitvector 16 (sigma ppc)+assembled≤assembled') 411 [ <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok 412 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 413 #sigma_ok1 #sigma_ok2 414 cases daemon (*CSC: True, apply lemma above + monotonicity of sigma *) 415  #LE2 416 cut (assembled < 2^16) 417 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) / by /] #LTassembled 418 cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))) ≤ assembled') 419 [ >nat_of_bitvector_add 420 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 421 @(le_to_lt_to_lt … LE2 assembly_ok1') 422  #LE @(lt_to_le_to_lt … LE) 423 @lt_to_lt_nat_of_bitvector_add 424 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 425 / by / 426  @(le_to_lt_to_lt ???? assembly_ok1') @LE2 427  assumption 428 ] 429 ] 430 ] 431  #assembly_ok1' >assembly_ok1' / by / 419 432 ] 420 433 ]
Note: See TracChangeset
for help on using the changeset viewer.