Changeset 870


Ignore:
Timestamp:
May 31, 2011, 5:54:34 PM (8 years ago)
Author:
mulligan
Message:

more changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r869 r870  
    364364    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
    365365    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))).
    375385   
    376386   
     
    383393    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧
    384394    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)) ∧
    389395    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧
    390396    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧
     
    400406 
    401407
    402 definition instruction_elim: ∀P: instruction → bool. bool.
     408axiom instruction_elim: ∀P: instruction → bool. bool.
    403409 
    404410 
     
    544550   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
    545551    → 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 -n
    594   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
    595   | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    596     #t cases(BitVectorTrie_Sn … t)
    597     [ * #l * #r #JMEQ >JMEQ cases hd #H CSC
    598      normalize in H;
    599      
    600       normalize //
    601     | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
    602 qed.
    603552
    604553definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.