Changeset 1561


Ignore:
Timestamp:
Nov 25, 2011, 1:13:15 PM (8 years ago)
Author:
sacerdot
Message:

More dependent types to accomodate the statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1558 r1561  
    33include "ASM/Status.ma".
    44include "common/StructuredTraces.ma".
    5 
    6 definition current_instruction ≝
    7   λs: Status.
    8   let pc ≝ program_counter … s in
    9   \fst (\fst (fetch … (code_memory … s) pc)).
    10 
    11 definition ASM_classify: Status → status_class ≝
    12  λs.
    13   match current_instruction s with
    14    [ RealInstruction pre ⇒
    15      match pre with
    16       [ RET ⇒ cl_return
    17       | JZ _ ⇒ cl_jump
    18       | JNZ _ ⇒ cl_jump
    19       | JC _ ⇒ cl_jump
    20       | JNC _ ⇒ cl_jump
    21       | JB _ _ ⇒ cl_jump
    22       | JNB _ _ ⇒ cl_jump
    23       | JBC _ _ ⇒ cl_jump
    24       | CJNE _ _ ⇒ cl_jump
    25       | DJNZ _ _ ⇒ cl_jump
    26       | _ ⇒ cl_other
    27       ]
    28    | ACALL _ ⇒ cl_call
    29    | LCALL _ ⇒ cl_call
    30    | JMP _ ⇒ cl_call
    31    | AJMP _ ⇒ cl_jump
    32    | LJMP _ ⇒ cl_jump
    33    | SJMP _ ⇒ cl_jump
    34    | _ ⇒ cl_other
    35    ].
    36 
    37 definition current_instruction_is_labelled ≝
    38   λcost_labels: BitVectorTrie costlabel 16.
    39   λs: Status.
    40   let pc ≝ program_counter … s in
    41     match lookup_opt … pc cost_labels with
    42     [ None ⇒ False
    43     | _    ⇒ True
    44     ].
    45 
    46 definition label_of_current_instruction:
    47  BitVectorTrie costlabel 16 → Status → list costlabel
    48  ≝
    49   λcost_labels,s.
    50   let pc ≝ program_counter … s in
    51     match lookup_opt … pc cost_labels with
    52     [ None ⇒ []
    53     | Some l ⇒ [l]
    54     ].
    55 
    56 definition next_instruction_properly_relates_program_counters ≝
    57   λbefore: Status.
    58   λafter : Status.
    59   let size ≝ current_instruction_cost before in
    60   let pc_before ≝ program_counter … before in
    61   let pc_after ≝ program_counter … after in
    62   let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    63     sum = pc_after.
    64 
    65 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
    66  λcost_labels.
    67   mk_abstract_status
    68    Status
    69    (λs,s'. eject … (execute_1 s) = s')
    70    (λs,class. ASM_classify s = class)
    71    (current_instruction_is_labelled cost_labels)
    72    next_instruction_properly_relates_program_counters.
    735
    746(*
     
    290222include alias "arithmetics/nat.ma".
    291223
    292 (*
     224(*Useless now?
    293225lemma minus_m_n_minus_minus_plus_1:
    294226  ∀m, n: nat.
     
    297229 /3 by lt_plus_to_minus_r, plus_minus/
    298230qed.
    299 *)
    300231
    301232lemma plus_minus_rearrangement_1:
     
    314245    (m - n) + (n - o) = m - o.
    315246 /2 by plus_minus_rearrangement_1/
    316 qed.
     247qed.*)
    317248
    318249(*
     
    345276    normalize @compute_max_trace_any_label_cost_is_ok
    346277  |2:
    347     cases the_trace
    348     [1:
    349       #start_status #final_status #is_next #is_not_return #is_costed
    350       normalize nodelta;
    351       change with (
    352         let current_instruction_cost ≝ current_instruction_cost start_status in 
    353         let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 
    354         let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 
    355         call_trace_cost+current_instruction_cost+final_trace_cost
    356       ) in ⊢ (??%?);
    357     |2:
    358       #start_status #final_status #is_next #is_return
    359     |3:
    360       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    361       #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace
    362       change with (
    363         let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 
    364         let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 
    365         let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in 
    366           call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);
    367       normalize nodelta;
    368       >compute_max_trace_label_return_cost_is_ok
    369       >compute_max_trace_any_label_cost_is_ok
    370     |4:
    371     ]
    372278  |3:
    373279    cases the_trace
     
    379285      normalize >compute_max_trace_label_label_cost_is_ok
    380286      >compute_max_trace_label_return_cost_is_ok
    381       >plus_minus_rearrangement_1
    382       [1: %
    383       |2:
    384       |3:
    385       ]
    386287    ]
    387288  ].
     
    536437    (start_status: Status) (final_status: Status)
    537438      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    538         start_status final_status) on the_trace: list costlabel ≝
     439        start_status final_status) on the_trace:
     440         list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    539441  match the_trace with
    540442  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    544446      [ None ⇒ λabs. ⊥
    545447      | Some l ⇒ λ_. l ] labelled_proof in
    546      label::compute_cost_trace_any_label … given_trace
     448     (dp … label ?)::compute_cost_trace_any_label … given_trace
    547449  ]
    548450and compute_cost_trace_any_label
     
    551453   (start_status: Status) (final_status: Status)
    552454     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    553        on the_trace: list costlabel
     455       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k)
    554456  match the_trace with
    555457  [ tal_base_not_return the_status _ _ _ _ ⇒ []
     
    568470  (start_status: Status) (final_status: Status)
    569471    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    570       on the_trace: list costlabel
     472      on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k)
    571473  match the_trace with
    572474  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
     
    576478        labelled_cost @ return_cost
    577479  ].
    578 //
     480 [ %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
     481  cases (lookup_opt costlabel … pc cost_labels) normalize
     482  [ #abs cases abs | // ]
     483 | // ]
    579484qed.
    580485
     
    595500   start_status final_status the_trace.
    596501
    597 include "arithmetics/bigops.ma".
    598 
    599 lemma foo:
     502(* To be moved elsewhere*)
     503lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m.
     504 #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) //
     505qed.
     506
     507(* Here I would like to use arithmetics/bigops.ma, but it requires the
     508   function f to be total on nat, which is not the case here *)
     509let rec bigplus0 (b:nat) (f: ∀n:nat. n < b → nat) (n:nat) on n ≝
     510  match n return λn.n < b → nat with
     511   [ O ⇒ λ_. 0
     512   | S k ⇒ λH. f k ? + bigplus0 b f k ?
     513   ].
     514 @(le_S_n_m_to_le_n_m … H)
     515qed.
     516
     517definition bigplus ≝
     518 λn,f.
     519 match n return λx. x = n → nat with
     520 [ O ⇒ λ_. 0
     521 | S m ⇒ λH. bigplus0 n f m ? ] (refl … n).
     522 //
     523qed.
     524
     525lemma compute_max_trace_label_return_cost_ok_with_trace:
    600526 ∀cost_labels: BitVectorTrie costlabel 16.
    601  ∀cost_labels_inv: identifier_map CostTag Word.
     527 ∀cost_map: identifier_map CostTag nat.
    602528 ∀initial,final.
    603529 ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final.
    604   let dummy ≝ an_identifier ? one in
     530 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     531 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     532   block_cost (code_memory … initial) cost_labels pc 2^16 =
     533   lookup_present … k_pres).
    605534  let ctrace ≝ compute_cost_trace_label_return … trace in
    606535  compute_max_trace_label_return_cost … trace =
    607    \big [ plus, 0 ]_{ i < |ctrace| }
    608     (block_cost (code_memory … initial) cost_labels
    609      (lookup_present … cost_labels_inv (nth i ? ctrace dummy) ?) 2^16).
    610  [2: cases daemon (* ALL LABELS MUST BE PRESENT *)
    611  | #cost_labels #cost_labels_inv #initial #final #trace
    612    letin dummy ≝ (an_identifier CostTag one) normalize nodelta
    613    whd in match
     536   bigplus (|ctrace|) (λi,H.lookup_present … cost_map (nth_safe ? i ctrace H) ?).
     537 [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K
     538   lapply (codom_dom … K) #k_pres //
     539 | #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom normalize nodelta
     540   whd in match
    614541
    615542lemma
Note: See TracChangeset for help on using the changeset viewer.