Changeset 1935


Ignore:
Timestamp:
May 10, 2012, 5:13:34 PM (7 years ago)
Author:
mulligan
Message:

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1929 r1935  
    44include "ASM/Interpret.ma".
    55include "common/StructuredTraces.ma".
    6    
    7 definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
    8   λcost_labels.
    9     injective … (λx. lookup_opt … x cost_labels).
    10 
    11 definition current_instruction_label ≝
    12   λcode_memory.
    13   λcost_labels: BitVectorTrie costlabel 16.
    14   λs: Status code_memory.
    15   let pc ≝ program_counter … code_memory s in
    16     lookup_opt … pc cost_labels.
    17 
    18 definition next_instruction_properly_relates_program_counters ≝
    19   λcode_memory.
    20   λbefore: Status code_memory.
    21   λafter : Status code_memory.
    22     let program_counter_before ≝ program_counter ? code_memory before in
    23     let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    24       program_counter ? code_memory after = program_counter_after.
    25 
    26 definition word_deqset: DeqSet ≝
    27   mk_DeqSet Word (eq_bv 16) ?.
    28   @refl_iff_eq_bv_true
    29 qed.
    30 
    31 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    32   λcode_memory.
    33   λcost_labels.
    34     mk_abstract_status
    35       (Status code_memory)
    36       (λs,s'. (execute_1 … s) = s')
    37       word_deqset
    38       (program_counter …)
    39       (λs,class. ASM_classify … s = class)
    40       (current_instruction_label code_memory cost_labels)
    41       (next_instruction_properly_relates_program_counters code_memory)
    42       ?.
    43   cases daemon (* XXX: is final predicate *)
    44 qed.
    456
    467definition trace_any_label_length ≝
  • src/ASM/CostsProof.ma

    r1929 r1935  
    268268include alias "ASM/BitVectorTrie.ma".
    269269
     270(*
    270271let rec compute_cost_trace_label_label
    271272  (cm: BitVectorTrie Byte 16)
     
    327328 | cases abs #absurd @absurd % ]
    328329qed.
     330*)
    329331
    330332include alias "arithmetics/nat.ma".
     
    384386
    385387definition tech_cost_of_label0:
     388 ∀code_memory: BitVectorTrie Byte 16.
    386389 ∀cost_labels: BitVectorTrie costlabel 16.
    387390 ∀cost_map: identifier_map CostTag nat.
    388391 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    389  ∀ctrace:list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k).
     392 ∀ctrace:list (Σk:costlabel.∃s: ASM_abstract_status code_memory cost_labels. as_label … s = Some ? k).
    390393 ∀i,p. present … cost_map (nth_safe ? i ctrace p).
    391  #cost_labels #cost_map #codom_dom #ctrace #i #p
     394 #code_memory #cost_labels #cost_map #codom_dom #ctrace #i #p
    392395 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K
    393396 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres)
     
    445448
    446449definition tech_cost_of_label:
     450 ∀code_memory: BitVectorTrie Byte 16.
    447451 ∀cost_labels: BitVectorTrie costlabel 16.
    448452 ∀cost_map: identifier_map CostTag nat.
    449453 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    450  list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k) →
     454 list (Σk:costlabel.∃s: ASM_abstract_status code_memory cost_labels. as_label … s = Some ? k) →
    451455 nat → nat
    452 ≝ λcost_labels,cost_map,codom_dom,ctrace,i.
     456≝ λcode_memory,cost_labels,cost_map,codom_dom,ctrace,i.
    453457 ltb_rect ? i (|ctrace|)
    454458 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?)
     
    485489
    486490lemma tech_cost_of_label_shift:
    487  ∀cost_labels,cost_map,codom_dom,l1,l2,i.
     491 ∀code_memory,cost_labels,cost_map,codom_dom,l1,l2,i.
    488492  i < |l2| →
    489    tech_cost_of_label cost_labels cost_map codom_dom l2 i =
    490    tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
    491  #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
     493   tech_cost_of_label code_memory cost_labels cost_map codom_dom l2 i =
     494   tech_cost_of_label code_memory cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
     495 #code_memory #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
    492496 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    493497 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2
     
    500504   |3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ]
    501505 | #H1 #H2
    502    generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
     506   generalize in match (tech_cost_of_label0 ???? (l1@l2) ??);
    503507   <(shift_nth_safe … H1) #p %
    504508 | // ]
     
    506510
    507511lemma tech_cost_of_label_prefix:
    508  ∀cost_labels,cost_map,codom_dom,l1,l2,i.
     512 ∀code_memory,cost_labels,cost_map,codom_dom,l1,l2,i.
    509513  i < |l1| →
    510    tech_cost_of_label cost_labels cost_map codom_dom l1 i =
    511    tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) i.
    512  #cost_labels #cost_map #codom_dom #l1 #l2 #i #H
     514   tech_cost_of_label code_memory cost_labels cost_map codom_dom l1 i =
     515   tech_cost_of_label code_memory cost_labels cost_map codom_dom (l1@l2) i.
     516 #code_memory #cost_labels #cost_map #codom_dom #l1 #l2 #i #H
    513517 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    514518 [1:
     
    518522 |2:
    519523   #K1 #K2
    520    generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
     524   generalize in match (tech_cost_of_label0 ???? (l1@l2) ??);
    521525   <(shift_nth_prefix … l1 i l2 K1 K2) //
    522526 |3:
     
    535539 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    536540   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    537   let ctrace ≝ compute_cost_trace_label_return cm … trace in
     541  let ctrace ≝ as_compute_cost_trace_label_return (ASM_abstract_status cm cost_labels) … trace in
    538542  compute_trace_label_return_cost_using_paid cm … trace =
    539    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     543   (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
    540544    ≝ ?
    541545and compute_trace_any_label_using_paid_ok_with_trace
     
    550554 on trace:
    551555  ∀unrepeating_witness: tal_unrepeating … trace.
    552   let ctrace ≝ compute_cost_trace_any_label … trace in
     556  let ctrace ≝ as_compute_cost_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in
    553557  compute_trace_any_label_cost_using_paid … trace =
    554    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     558   (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
    555559    ≝ ?
    556560and compute_trace_label_label_using_paid_ok_with_trace
     
    566570 on trace:
    567571 ∀unrepeating_witness: tll_unrepeating … trace.
    568   let ctrace ≝ compute_cost_trace_label_label … trace in
     572  let ctrace ≝ as_compute_cost_trace_label_label (ASM_abstract_status cm cost_labels) … trace in
    569573  compute_trace_label_label_cost_using_paid … trace =
    570    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     574   (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
    571575    ≝ ?.
    572576  cases trace normalize nodelta
    573577  [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
    574     whd in match (compute_cost_trace_label_return ?????);
     578    whd in match (as_compute_cost_trace_label_return ????);
    575579    @compute_trace_label_label_using_paid_ok_with_trace
    576580    assumption
    577581  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    578582    whd in ⊢ (??%?);
    579     whd in match (compute_cost_trace_label_return ?????);
     583    whd in match (as_compute_cost_trace_label_return ????);
    580584    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    581585    [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     
    602606    >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    603607    [1:
     608      whd in match (as_compute_cost_trace_label_label ?????);
    604609      >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
    605610      [1:
    606611        @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
    607         <(tech_cost_of_label_shift ??? [?] ? i) //
     612        <(tech_cost_of_label_shift ???? [?] ? i) try assumption <(plus_n_O i) %
    608613      |2:
    609614        change with (? = lookup_present ? ? ? ? ?)
    610         generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
     615        generalize in match (tech_cost_of_label0 ? ? ? ? ? ? ?);
    611616        normalize in match (nth_safe ? ? ? ?);
    612617        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
     
    682687  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    683688      pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres).
    684         let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
     689        let ctrace ≝ as_compute_cost_trace_label_return … trace in
    685690          clock … code_memory … final =
    686             clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
     691            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label code_memory cost_labels cost_map codom_dom ctrace i)).
    687692  #code_memory #cost_labels #cost_map
    688693  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
     
    703708  ∀unrepeating_witness: tlr_unrepeating … trace.
    704709    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
    705     let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
    706       clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
     710    let ctrace ≝ as_compute_cost_trace_label_return … trace in
     711      clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label code_memory cost_labels cost_map ? ctrace i)).
    707712  [1:
    708713    #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
  • src/ASM/Interpret.ma

    r1928 r1935  
     1include "basics/lists/listb.ma".
    12include "ASM/StatusProofs.ma".
    2 include "common/StructuredTraces.ma".
    33include "ASM/Fetch.ma".
    44
     
    120120include alias "ASM/BitVectorTrie.ma".
    121121
     122inductive status_class : Type[0] ≝
     123| cl_return : status_class
     124| cl_jump   : status_class
     125| cl_call   : status_class
     126| cl_other : status_class.
     127
    122128definition ASM_classify00: ∀a. preinstruction a → status_class ≝
    123129  λa, pre.
     
    159165  λs: Status code_memory.
    160166    current_instruction0 code_memory (program_counter … s).
     167   
     168definition current_instruction_label ≝
     169  λcode_memory.
     170  λcost_labels: BitVectorTrie costlabel 16.
     171  λs: Status code_memory.
     172  let pc ≝ program_counter … code_memory s in
     173    lookup_opt … pc cost_labels.
     174
     175definition next_instruction_properly_relates_program_counters ≝
     176  λcode_memory.
     177  λbefore: Status code_memory.
     178  λafter : Status code_memory.
     179    let program_counter_before ≝ program_counter ? code_memory before in
     180    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
     181      program_counter ? code_memory after = program_counter_after.
     182
     183definition word_deqset: DeqSet ≝
     184  mk_DeqSet Word (eq_bv 16) ?.
     185  @refl_iff_eq_bv_true
     186qed.
    161187   
    162188definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
  • src/common/StructuredTraces.ma

    r1927 r1935  
    44include "common/CostLabel.ma".
    55include "utilities/option.ma".
    6 include "basics/lists/listb.ma".
    76include "ASM/Util.ma".
    8 
    9 inductive status_class : Type[0] ≝
    10 | cl_return : status_class
    11 | cl_jump   : status_class
    12 | cl_call   : status_class
    13 | cl_other : status_class.
     7include "ASM/Interpret.ma".
    148
    159record abstract_status : Type[1] ≝
     
    2418  ; as_final: as_status → Prop
    2519}.
     20
     21definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     22  λcode_memory.
     23  λcost_labels.
     24    mk_abstract_status
     25      (Status code_memory)
     26      (λs,s'. (execute_1 … s) = s')
     27      word_deqset
     28      (program_counter …)
     29      (λs,class. ASM_classify … s = class)
     30      (current_instruction_label code_memory cost_labels)
     31      (next_instruction_properly_relates_program_counters code_memory)
     32      ?.
     33  cases daemon (* XXX: is final predicate *)
     34qed.
    2635
    2736(* temporary alias for backward compatibility *)
     
    432441    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    433442  ].
     443
     444include "ASM/BitVectorTrie.ma".
     445include "ASM/Status.ma".
     446include "ASM/Fetch.ma".
     447
     448let rec as_compute_cost_trace_label_label
     449  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     450    (start_status: S) (final_status: S)
     451      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
     452        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     453  match the_trace with
     454  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     455      let label ≝
     456        match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
     457        [ None ⇒ λabs. ⊥
     458        | Some l ⇒ λ_. l
     459        ] labelled_proof
     460      in
     461        (mk_Sig … label ?)::as_compute_cost_trace_any_label S ends_flag initial final given_trace
     462  ]
     463and as_compute_cost_trace_any_label
     464  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     465    (start_status: S) (final_status: S)
     466      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
     467        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     468  match the_trace with
     469  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
     470  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     471      as_compute_cost_trace_label_return … call_trace
     472  | tal_base_return the_status _ _ _ ⇒ [ ]
     473  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     474    _ _ _ call_trace _ final_trace ⇒
     475    let call_cost_trace ≝ as_compute_cost_trace_label_return … call_trace in
     476    let final_cost_trace ≝ as_compute_cost_trace_any_label … end_flag … final_trace in
     477        call_cost_trace @ final_cost_trace
     478  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     479      as_compute_cost_trace_any_label … tail_trace
     480  ]
     481and as_compute_cost_trace_label_return
     482  (S: abstract_status)
     483    (start_status: S) (final_status: S)
     484      (the_trace: trace_label_return S start_status final_status)
     485        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     486  match the_trace with
     487  [ tlr_base before after trace_to_lift ⇒
     488      as_compute_cost_trace_label_label … trace_to_lift
     489  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     490    let labelled_cost ≝ as_compute_cost_trace_label_label … doesnt_end_with_ret … labelled_trace in
     491    let return_cost ≝ as_compute_cost_trace_label_return … ret_trace in
     492        labelled_cost @ return_cost
     493  ].
     494  [2:
     495    cases abs -abs #abs @abs %
     496  |1:
     497    %{initial} whd in match label;
     498    generalize in match labelled_proof; whd in ⊢ (% → ?);
     499    cases (as_label S initial)
     500    [1:
     501      #absurd @⊥ cases absurd -absurd #absurd @absurd %
     502    |2:
     503      #costlabel normalize nodelta #_ %
     504    ]
     505  ]
     506qed.
Note: See TracChangeset for help on using the changeset viewer.