Changeset 870
 Timestamp:
 May 31, 2011, 5:54:34 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r869 r870 364 364 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧ 365 365 P (DA ? ACC_A) ∧ 366 P (JC ? ?) ∧ 367 P (JNC ? ?) ∧ 368 P (JZ ? ?) ∧ 369 P (JNZ ? ?) ∧ 370 bitvector_elim 8 (λx. P (JB ? (BIT_ADDR x))). ∧ 371 P (JNB ? [[ bit_addr ]] ?) ∧ 372 P (JBC ? [[ bit_addr ]] ?) ∧ 373 P (RL ? ACC_A). 374 366 bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧ 367 bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧ 368 bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧ 369 bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧ 370 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧ 371 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧ 372 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧ 373 list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧ 374 P (RL ? ACC_A) ∧ 375 P (RLC ? ACC_A) ∧ 376 P (RR ? ACC_A) ∧ 377 P (RRC ? ACC_A) ∧ 378 P (SWAP ? ACC_A) ∧ 379 P (RET ?) ∧ 380 P (RETI ?) ∧ 381 P (NOP ?) ∧ 382 list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧ 383 bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧ 384 bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))). 375 385 376 386 … … 383 393 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧ 384 394 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧ 385 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RL ? addr)) ∧386 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RLC ? addr)) ∧387 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RR ? addr)) ∧388 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RRC ? addr)) ∧389 395 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧ 390 396 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧ … … 400 406 401 407 402 definitioninstruction_elim: ∀P: instruction → bool. bool.408 axiom instruction_elim: ∀P: instruction → bool. bool. 403 409 404 410 … … 544 550 construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None … 545 551 → False. 546 547 lemma BitVectorTrie_O:548 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.549 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))550 [ #w #_ %1 %[@w] %551  #n #l #r #abs @⊥ //552  #n #EQ %2 >EQ %]553 qed.554 555 lemma BitVectorTrie_Sn:556 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).557 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)558 [ #m #abs @⊥ //559  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //560  #m #EQ %2 // ]561 qed.562 563 lemma lookup_prepare_trie_for_insertion_hit:564 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.565 lookup … b (prepare_trie_for_insertion … b v) a = v.566 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //567 qed.568 569 lemma lookup_insert_hit:570 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.571 lookup … b (insert … b v t) a = v.572 #A #a #v #n #b elim b b n //573 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)574 [ * #l * #r #JMEQ >JMEQ cases hd normalize //575  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]576 qed.577 578 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.579 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //580 #n #hd #tl #abs @⊥ //581 qed.582 583 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).584 ∃hd.∃tl.v ≃ VCons bool n hd tl.585 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))586 [ #abs @⊥ //587  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]588 qed.589 590 lemma lookup_insert_miss:591 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.592 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.593 #A #a #v #n #c elim c c n594 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //595  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ596 #t cases(BitVectorTrie_Sn … t)597 [ * #l * #r #JMEQ >JMEQ cases hd #H CSC598 normalize in H;599 600 normalize //601  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]602 qed.603 552 604 553 definition build_maps' ≝
Note: See TracChangeset
for help on using the changeset viewer.