Changeset 1645 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Jan 13, 2012, 6:11:39 PM (8 years ago)
Author:
mulligan
Message:

more progress on the ASMCosts work: block_costs is now complete (subject to inhabiting the type of the subaddressing_mode eliminator). pushing on through file propagating changes and fixing type errors

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1642 r1645  
    205205      | _ ⇒ λother: False. ⊥
    206206      ] (subaddressing_modein … addr)
    207     | JMP   addr     ⇒ True (* XXX: JMP is used for fptrs and unconstrained *)
     207    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
     208      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     209        nat_of_bitvector … program_counter' < total_program_size
    208210    | MOVC  src trgt ⇒
    209211        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    … …  
    346348qed.
    347349
    348 axiom subaddressing_mode_elim':
     350lemma subaddressing_mode_elim':
     351  ∀T: Type[2].
     352  ∀n: nat.
     353  ∀o: nat.
     354  ∀Q: addressing_mode → T → Prop.
     355  ∀fixed_v: Vector addressing_mode_tag (n + o).
     356  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
     357  ∀v1: Vector addressing_mode_tag n.
     358  ∀v2: Vector addressing_mode_tag o.
     359  ∀fixed_v_proof: fixed_v = v1 @@ v2.
     360  ∀subaddressing_mode_proof.
     361    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
     362      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
     363  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
     364  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
     365  cases daemon
     366qed.
     367
     368axiom subaddressing_mode_elim:
    349369  ∀T: Type[2].
    350370  ∀m: nat.
     371  ∀n: nat.
     372  ∀Q: addressing_mode → T → Prop.
    351373  ∀fixed_v: Vector addressing_mode_tag m.
    352   ∀Q: addressing_mode → T → Prop.
    353374  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    354   ∀n: nat.
    355375  ∀v: Vector addressing_mode_tag n.
    356376  ∀proof.
    357377    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    358378      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    359 (*  #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
    360   elim v
    361   [ #proof normalize
    362    
    363 qed. *)
    364379
    365380(*
    … …  
    406421    n < o → m + n < m + o.
    407422  #m #n #o #assm /2 by monotonic_le_plus_r/
    408 qed.
    409 
    410 (*
    411 axiom blah:
    412   ∀instruction: instruction.
    413   ∀program_counter': Word.
    414   ∀ticks, n: nat.
    415   ∀code_memory: BitVectorTrie Byte 16.
    416     〈instruction,program_counter',ticks〉 = fetch code_memory (fetch_program_counter_n n code_memory (zero 16)) →
    417        program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
    418 *)   
     423qed.   
    419424
    420425let rec block_cost
    … …  
    469474    lapply(good_program_witness program_counter reachable_program_counter_witness)
    470475      <FETCH normalize nodelta <instr normalize nodelta
    471     @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     476    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    472477    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    473478    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    … …  
    489494    lapply(good_program_witness program_counter reachable_program_counter_witness)
    490495      <FETCH normalize nodelta <instr normalize nodelta
    491     @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     496    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    492497    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    493498    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    … …  
    506511    lapply(good_program_witness program_counter reachable_program_counter_witness)
    507512      <FETCH normalize nodelta <instr normalize nodelta
    508     @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     513    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    509514    * * * * #n'
    510515    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
    … …  
    524529    lapply(good_program_witness program_counter reachable_program_counter_witness)
    525530      <FETCH normalize nodelta <instr normalize nodelta
    526     @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     531    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    527532    * * * * #n'
    528533    #_ #_ #program_counter_lt' #program_counter_lt_tps'
    … …  
    535540      assumption
    536541    ]
    537   |6:
    538     cases daemon (* XXX *)
    539   |7:
    540     cases daemon (* XXX *)
    541   |8:
     542  |6,8: (* JMP and MOVC *)
    542543    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    543544    lapply(good_program_witness program_counter reachable_program_counter_witness)
    … …  
    556557        nat_of_bitvector … program_counter')
    557558    assumption
    558   |9:
    559     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    560     lapply(good_program_witness program_counter reachable_program_counter_witness)
    561       <FETCH normalize nodelta <instr normalize nodelta *
     559  |7,9:
     560    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     561    lapply(good_program_witness program_counter reachable_program_counter_witness)
     562    <FETCH normalize nodelta <instr normalize nodelta *
    562563    #program_counter_lt' #program_counter_lt_tps' %
    563     [1:
     564    [1,3:
    564565      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    565566      <FETCH normalize nodelta whd in match ltb; normalize nodelta
    566567      >(le_to_leb_true … program_counter_lt') %
    567     |2:
     568    |2,4:
    568569      assumption
    569570    ]
    … …  
    572573    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    573574    lapply(good_program_witness program_counter reachable_program_counter_witness)
    574       <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
     575    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    575576    #program_counter_lt' #program_counter_lt_tps' %
    576     [1:
     577    try assumption
     578    [*:
    577579      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    578580      <FETCH normalize nodelta whd in match ltb; normalize nodelta
    579581      >(le_to_leb_true … program_counter_lt') %
    580     |2:
    581       assumption
    582582    ]
    583583  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
    … …  
    601601  ]
    602602qed.
    603    
    604    
    605    
    606    
    607    
    608    
    609    
    610   [1: (* ACALL *)
    611     generalize in match good_program_witness;
    612     whd in match good_program; normalize nodelta
    613     cases FETCH normalize nodelta
    614     cases instr normalize nodelta
    615     @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    616     cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta
    617     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    618     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
    619     #assm cases assm #ignore
    620     whd in match good_program_counter; normalize nodelta * #n * *
    621     #program_counter_eq #program_counter_lt_total_program_size
    622     #fetch_n_leq_program_counter
    623     @(transitive_le
    624       total_program_size
    625       ((S program_size') + nat_of_bitvector … program_counter)
    626       (program_size' + nat_of_bitvector … program_counter') recursive_case)
    627     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    628     >plus_n_Sm
    629     @monotonic_le_plus_r
    630     change with (
    631       nat_of_bitvector … program_counter <
    632         nat_of_bitvector … program_counter')
    633     >program_counter_eq in FETCH; #hyp
    634     >(blah … hyp)
    635     <program_counter_eq assumption
    636   |2:
    637     generalize in match good_program_witness;
    638     whd in match good_program; normalize nodelta
    639     cases FETCH normalize nodelta
    640     cases instr normalize nodelta
    641     @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    642     cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta
    643     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    644     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
    645     #assm cases assm #ignore
    646     whd in match good_program_counter; normalize nodelta * #n * *
    647     #program_counter_eq #program_counter_lt_total_program_size
    648     #fetch_n_leq_program_counter
    649 
    650     whd in match good_program; normalize nodelta
    651     @pair_elim #lft #rgt normalize nodelta #fetch_hyp
    652     @pair_elim #instruction #program
    653   |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
    654    54,56,58,60,62:
    655   |3: (* LCALL *)
    656     generalize in match good_program_witness;
    657     whd in match good_program; normalize nodelta
    658     cases FETCH normalize nodelta
    659     cases instr normalize nodelta
    660     @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    661     * #irrelevant
    662     whd in match good_program_counter; normalize nodelta * #n * *
    663     #program_counter_eq #program_counter_lt_total_program_size
    664     #fetch_n_leq_program_counter
    665     @(transitive_le
    666       total_program_size
    667       ((S program_size') + nat_of_bitvector … program_counter)
    668       (program_size' + nat_of_bitvector … program_counter') recursive_case)
    669     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    670     >plus_n_Sm
    671     @monotonic_le_plus_r
    672     change with (
    673       nat_of_bitvector … program_counter <
    674         nat_of_bitvector … program_counter')
    675     >program_counter_eq in FETCH; #hyp
    676     >(blah … hyp)
    677     <program_counter_eq assumption
    678   |5,7: (* JMP and MOVC *)
    679     generalize in match good_program_witness;
    680     whd in match good_program; normalize nodelta
    681     cases FETCH normalize nodelta
    682     cases instr normalize nodelta
    683   |9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,
    684    49,51,53,55,57,59,61,63: (* ADD and similar non-branching instructions *)
    685     generalize in match good_program_witness;
    686     whd in match good_program; normalize nodelta
    687     cases FETCH normalize nodelta
    688     <real_instruction_refl <instr normalize nodelta
     603
     604axiom fetch_program_counter_n_Sn:
     605  ∀instruction: instruction.
     606  ∀program_counter, program_counter': Word.
     607  ∀ticks, n: nat.
     608  ∀code_memory: BitVectorTrie Byte 16.
     609    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
     610      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
     611        Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
     612       
     613let rec traverse_code_internal
     614  (program: list Byte) (code_memory: BitVectorTrie Byte 16)
     615    (cost_labels: BitVectorTrie costlabel 16) (program_counter: Word)
     616      (program_size: nat) (reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter)
     617        (good_program_witness: good_program code_memory program_size)
     618          (n: nat) (fetch_program_counter_proof: Some … program_counter = fetch_program_counter_n n code_memory (zero …))
     619        on program: identifier_map CostTag nat ≝
     620  let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
     621  match program with
     622  [ nil ⇒ empty_map …
     623  | cons hd tl ⇒
     624    match lookup_opt … program_counter cost_labels with
     625    [ None ⇒ traverse_code_internal tl code_memory cost_labels new_program_counter program_size ? good_program_witness (S n) ?
     626    | Some lbl ⇒
     627      let cost ≝ block_cost code_memory program_counter program_size program_size cost_labels ? good_program_witness ? in
     628      let cost_mapping ≝ traverse_code_internal tl code_memory cost_labels new_program_counter program_size ? good_program_witness (S n) ? in
     629        add … cost_mapping lbl cost
     630    ]
     631  ].
     632  [6:
     633    //
     634  |2,4:
     635    @(fetch_program_counter_n_Sn instruction program_counter new_program_counter ticks n)
     636    assumption
     637  |5:
     638    assumption
     639  |1,3:
     640    whd in match reachable_program_counter; normalize nodelta
     641    @conj
     642    [1,3:
     643      %{(S n)}
     644      @(fetch_program_counter_n_Sn instruction program_counter new_program_counter ticks n)
     645      assumption
     646    |2,4:
     647      cases daemon (* XXX ??? *)
     648    ]
    689649  ]
    690     whd in match good_program_counter; normalize nodelta * #n * *
    691     #program_counter_eq #program_counter_lt_total_program_size
    692     #fetch_n_leq_program_counter
    693     @(transitive_le
    694       total_program_size
    695       (S program_size' + nat_of_bitvector … program_counter)
    696       (program_size' + nat_of_bitvector … program_counter')
    697       recursive_case)
    698     normalize in match (S program_size' + nat_of_bitvector … program_counter);
    699     >plus_n_Sm
    700     @monotonic_le_plus_r
    701     change with (
    702       nat_of_bitvector … program_counter <
    703         nat_of_bitvector … program_counter')
    704     >program_counter_eq in FETCH; #hyp
    705     >(blah … hyp)
    706     <program_counter_eq assumption
    707 qed.
    708        
    709 (* XXX: use memoisation here in the future *)
    710 let rec block_cost
    711   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    712     (program_counter: Word) (program_size: nat) (total_program_size: nat)
    713       (size_invariant: total_program_size ≤ code_memory_size)
    714         (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
    715           on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
    716   match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
    717   [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
    718   | S program_size ⇒ λrecursive_case.
    719     let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
    720       match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
    721       [ None ⇒
    722           let classify ≝ ASM_classify0 instr in
    723           match classify return λx. classify = x → ? with
    724           [ cl_jump ⇒ λclassify_refl. ticks
    725           | cl_call ⇒ λclassify_refl. (* ite here *)
    726               ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    727           | cl_return ⇒ λclassify_refl. ticks
    728           | cl_other ⇒ λclassify_refl. (* ite here *)
    729               ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    730           ] (refl … classify)
    731         | Some _ ⇒ ticks
    732       ]
    733   ].
    734 
    735 let rec traverse_code_internal
    736   (program: list Byte) (mem: BitVectorTrie Byte 16)
    737     (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
    738       on program: identifier_map CostTag nat ≝
    739  let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
    740  match program with
    741  [ nil ⇒ empty_map …
    742  | cons hd tl ⇒
    743    match lookup_opt … pc cost_labels with
    744    [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
    745    | Some lbl ⇒
    746      let cost ≝ block_cost mem cost_labels pc program_size in
    747      let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
    748        add … cost_mapping lbl cost ]].
     650qed.
    749651
    750652definition traverse_code ≝
    751653  λprogram: list Byte.
    752   λmem: BitVectorTrie Byte 16.
     654  λcode_memory: BitVectorTrie Byte 16.
    753655  λcost_labels.
    754656  λprogram_size: nat.
    755     traverse_code_internal program mem cost_labels (zero …) program_size.
     657  λprogram_not_empty_proof: 0 < program_size.
     658  λgood_program_witness: good_program code_memory program_size.
     659    traverse_code_internal program code_memory cost_labels (zero …) program_size ? good_program_witness.
     660  normalize @conj
     661  [2:
     662    assumption
     663  |1:
     664    %{0} %
     665  ]
     666qed.
    756667
    757668definition compute_costs ≝
    … …  
    759670  λcost_labels: BitVectorTrie costlabel 16.
    760671  λhas_main: bool.
    761   let program_size ≝ |program| + 1 in
    762   let memory ≝ load_code_memory program in
    763    traverse_code program memory cost_labels program_size.
     672  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
     673  λprogram_not_empty_proof: 0 < |program|.
     674    let program_size ≝ |program| + 1 in
     675    let code_memory ≝ load_code_memory program in
     676      traverse_code program code_memory cost_labels program_size ?.
     677  //
     678qed.
Note: See TracChangeset for help on using the changeset viewer.