- Timestamp:
- Jun 29, 2012, 10:09:10 AM (9 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.