Changeset 876


Ignore:
Timestamp:
Jun 3, 2011, 4:03:00 PM (8 years ago)
Author:
sacerdot
Message:

...

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r875 r876  
    439439 ∀P. instruction_elim P = true → ∀i. P i = true.
    440440
    441 definition eq_instruction ≝
     441(*definition eq_instruction ≝
    442442  λi, j: instruction.
    443     true.
    444    
    445 let rec list_addressing_mode_tags_elim_prop
    446   (n: nat) (l: Vector addressing_mode_tag (S n))
    447   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    448   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    449   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    450   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    451   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    452   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    453   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    454   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    455   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    456   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    457   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    458   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    459   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    460   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    461   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    462   (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
    463   (if is_in ? l relative then ∀x. P (RELATIVE x) else True) →
    464   (if is_in ? l addr11 then ∀x. P (ADDR11 x) else True) →
    465   (if is_in ? l addr16 then ∀x. P (ADDR16 x) else True) →
    466   (P: addressing_mode → Prop) (x: l)
    467    on l : P x ≝
    468   match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
    469    (l → bool) → bool ] with
    470   [ VEmpty      ⇒  true 
    471   | VCons len hd tl ⇒ λP.
    472     let process_hd ≝
    473       match hd return λhd. ∀P: hd:::tl → bool. bool with
    474       [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
    475       | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
    476       | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
    477       | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
    478       | acc_a ⇒ λP.P ACC_A
    479       | acc_b ⇒ λP.P ACC_B
    480       | dptr ⇒ λP.P DPTR
    481       | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
    482       | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
    483       | acc_dptr ⇒ λP.P ACC_DPTR
    484       | acc_pc ⇒ λP.P ACC_PC
    485       | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
    486       | indirect_dptr ⇒ λP.P INDIRECT_DPTR
    487       | carry ⇒ λP.P CARRY
    488       | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
    489       | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
    490       | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
    491       | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
    492       | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
    493       ]
    494     in
    495       andb (process_hd P)
    496        (match len return λx. x = len → bool with
    497          [ O ⇒ λprf. true
    498          | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
    499   ].
    500   try %
    501   [ 2: cases (sym_eq ??? prf); @tl
    502   | generalize in match H; generalize in match tl; cases prf;
    503     (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    504     #tl
    505     normalize in ⊢ (∀_: %. ?)
    506     # H
    507     whd
    508     normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    509     cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
    510 qed.
     443    true.*)
     444axiom eq_instruction: instruction → instruction → bool.
    511445
    512446(*
     
    522456 ]*)
    523457
     458lemma BitVectorTrie_O:
     459 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
     460 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     461  [ #w #_ %1 %[@w] %
     462  | #n #l #r #abs @⊥ //
     463  | #n #EQ %2 >EQ %]
     464qed.
     465
     466lemma BitVectorTrie_Sn:
     467 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
     468 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     469  [ #m #abs @⊥ //
     470  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
     471  | #m #EQ %2 // ]
     472qed.
     473
     474lemma lookup_prepare_trie_for_insertion_hit:
     475 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
     476  lookup … b (prepare_trie_for_insertion … b v) a = v.
     477 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     478qed.
     479 
     480lemma lookup_insert_hit:
     481 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     482  lookup … b (insert … b v t) a = v.
     483 #A #a #v #n #b elim b -b -n //
     484 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
     485  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
     486  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     487qed.
     488
     489lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     490 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     491 #n #hd #tl #abs @⊥ //
     492qed.
     493
     494lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
     495 ∃hd.∃tl.v ≃ VCons bool n hd tl.
     496 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     497 [ #abs @⊥ //
     498 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     499qed.
     500
     501coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     502
     503lemma lookup_prepare_trie_for_insertion_miss:
     504 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
     505  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
     506 #A #a #v #n #c elim c
     507  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     508  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     509    cases hd cases hd' normalize
     510    [2,3: #_ cases tl' //
     511    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
     512qed.
     513 
     514lemma lookup_insert_miss:
     515 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     516  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
     517 #A #a #v #n #c elim c -c -n
     518  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     519  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     520    #t cases(BitVectorTrie_Sn … t)
     521    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     522     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     523    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     524     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     525     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
     526qed.
     527
     528definition load_code_memory_aux ≝
     529 fold_left_i_aux … (
     530   λi, mem, v.
     531     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
     532
     533axiom split_elim:
     534 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
     535  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
     536
     537axiom half_add_SO:
     538 ∀pc.
     539 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     540
     541axiom not_eqvb_S:
     542 ∀pc.
     543 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
     544
     545axiom not_eqvb_SS:
     546 ∀pc.
     547 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
     548
    524549lemma test:
    525   ∀i.
    526       (let assembled ≝ assembly1 i in
    527       let code_memory ≝ load_code_memory assembled in
    528       let fetched ≝ fetch code_memory ? in
     550  ∀pc,i.
     551     (let assembled ≝ assembly1 i in
     552      let code_memory ≝ load_code_memory_aux pc assembled in
     553      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
    529554      let 〈instr_pc, ticks〉 ≝ fetched in
    530555        eq_instruction (\fst instr_pc)) i = true.
    531  [ #i cases i #arg try #arg2 whd in ⊢ (??%?)
    532    [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?)
     556 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
     557   [2,4: whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
    533558       cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
    534        whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?)
     559       whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX;
     560       [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX
     561       |*:@split_elim #b1 #b2 #EQ >EQ -EQ;
     562        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     563        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     564        >lookup_insert_miss //
     565        >lookup_insert_miss //
     566        >lookup_insert_hit
     567        whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?)
     568        whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
     569        >half_add_SO >half_add_SO
     570        >lookup_insert_miss [2,4: @not_eqvb_S]
     571        >lookup_insert_hit >lookup_insert_hit]
     572   |
     573       
     574       
     575         
    535576 
    536577   [2: #addr whd in ⊢ (??%?)
     
    630671qed.
    631672
    632 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    633 
    634673lemma index_of_internal_None: ∀i,id,instr_list,n.
    635674 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     
    665704    → False.
    666705
    667 lemma BitVectorTrie_O:
    668  ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
    669  #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
    670   [ #w #_ %1 %[@w] %
    671   | #n #l #r #abs @⊥ //
    672   | #n #EQ %2 >EQ %]
    673 qed.
    674 
    675 lemma BitVectorTrie_Sn:
    676  ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    677  #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
    678   [ #m #abs @⊥ //
    679   | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    680   | #m #EQ %2 // ]
    681 qed.
    682 
    683 lemma lookup_prepare_trie_for_insertion_hit:
    684  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
    685   lookup … b (prepare_trie_for_insertion … b v) a = v.
    686  #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
    687 qed.
    688  
    689 lemma lookup_insert_hit:
    690  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
    691   lookup … b (insert … b v t) a = v.
    692  #A #a #v #n #b elim b -b -n //
    693  #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
    694   [ * #l * #r #JMEQ >JMEQ cases hd normalize //
    695   | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
    696 qed.
    697 
    698 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    699  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    700  #n #hd #tl #abs @⊥ //
    701 qed.
    702 
    703 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
    704  ∃hd.∃tl.v ≃ VCons bool n hd tl.
    705  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    706  [ #abs @⊥ //
    707  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    708 qed.
    709 
    710 lemma lookup_prepare_trie_for_insertion_miss:
    711  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
    712   (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
    713  #A #a #v #n #c elim c
    714   [ #b >(BitVector_O … b) normalize #abs @⊥ //
    715   | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    716     cases hd cases hd' normalize
    717     [2,3: #_ cases tl' //
    718     |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
    719 qed.
    720  
    721 lemma lookup_insert_miss:
    722  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    723   (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
    724  #A #a #v #n #c elim c -c -n
    725   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
    726   | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    727     #t cases(BitVectorTrie_Sn … t)
    728     [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    729      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    730     | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    731      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
    732      [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    733 qed.
    734706
    735707definition build_maps' ≝
  • src/ASM/Fetch.ma

    r856 r876  
    66 λpmem: BitVectorTrie Byte 16.
    77 λpc: Word.
    8  let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in
    9    〈res, lookup … pc pmem (zero 8)〉.
     8  〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup … pc pmem (zero 8)〉.
    109
    1110(* timings taken from SIEMENS *)
    1211
    13 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
     12definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝
    1413 λpmem: BitVectorTrie Byte 16.
    15  λpc: Word.
    16   let 〈pc,v〉 ≝ next pmem pc in
     14 λpc_v.
     15  let 〈pc,v〉 ≝ pc_v in
    1716   let 〈b,v〉 ≝ head … v in if b then
    1817    let 〈b,v〉 ≝ head … v in if b then
     
    390389  %.
    391390qed.
     391
     392definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
     393 λpmem: BitVectorTrie Byte 16.
     394 λpc: Word.
     395  fetch0 pmem (next pmem pc).
Note: See TracChangeset for help on using the changeset viewer.