Changeset 2907


Ignore:
Timestamp:
Mar 19, 2013, 7:48:19 PM (4 years ago)
Author:
sacerdot
Message:
  1. a few bugs fixed
  2. as_return implemented for ASM & OC
Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2899 r2907  
    1 (* JHM: redundant includes
    2 include "ASM/ASM.ma".
    3 include "ASM/Arithmetic.ma".
    4 include "ASM/Fetch.ma".     (* includes ASM/ASM.ma and ASM/Arithmetic.ma *)
    5 *)
    6 
    7 include "ASM/Interpret.ma". (* includes ASM/Fetch.ma and ASM/AbstractStatus.ma *)
    8 
    9 (*include "common/StructuredTraces.ma". (* included by ASM/AbstractStatus.ma *) *)
    10 
    11 definition OC_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    12   λcode_memory.
    13   λcost_labels.
     1include "ASM/Interpret.ma".
     2
     3definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝
     4 [ DIRECT (bitvector_of_nat 8 82);       (* DPL *)
     5   DIRECT (bitvector_of_nat 8 83);       (* DPH *)
     6   REGISTER [[ false; false; false ]];   (* Register00 *)
     7   REGISTER [[ false; false; true ]] ].  (* Register01 *)
     8% qed.
     9
     10definition as_result_of_finaladdr: ∀T:Type[0]. ∀cm:T. PreStatus … cm → Word → option int ≝
     11 λT,cm,st,finaladdr.
     12  if eq_bv ? (program_counter ?? st) finaladdr then
     13   let vals ≝
     14    map [[acc_a;direct;registr]] ? (get_arg_8 ?? st false) (ASMRegisterRets⌈list ? ↦ ?⌉) in
     15   let dummy ≝ zero ? in
     16   let first_byte ≝ λl. match l with [ nil ⇒ 〈dummy,[]〉 | cons hd tl ⇒ 〈hd,tl〉] in
     17   let 〈b1,tl1〉 ≝ first_byte vals in
     18   let 〈b2,tl2〉 ≝ first_byte tl1 in
     19   let 〈b3,tl3〉 ≝ first_byte tl2 in
     20   let 〈b4,tl4〉 ≝ first_byte tl3 in
     21    Some ? (b4 @@ b3 @@ b2 @@ b1)
     22  else
     23   None ?.
     24[ @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % | % ]
     25qed.
     26
     27definition OC_abstract_status: labelled_object_code → abstract_status ≝
     28 λprog.
     29  let code_memory ≝ load_code_memory (oc prog) in
    1430    mk_abstract_status
    1531      (Status code_memory)
     
    1834      (program_counter …)
    1935      (OC_classify …)
    20       (λpc.lookup_opt … pc cost_labels)
     36      (λpc.lookup_opt … pc (costlabels prog))
    2137      (next_instruction_properly_relates_program_counters code_memory)
    22       ? (* (λs.False) *)
     38      (λst. as_result_of_finaladdr … st (final_pc prog))
    2339      ?
    2440      ?.
    25   #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
     41  #x cases daemon (* XXX: (tail)call_ident function *)
    2642qed.
    2743
    2844definition trace_any_label_length ≝
    29   λcode_memory: BitVectorTrie Byte 16.
    30   λcost_labels: BitVectorTrie costlabel 16.
     45  λprog: labelled_object_code.
     46  let code_memory ≝ load_code_memory (oc prog) in
    3147  λtrace_ends_flag: trace_ends_with_ret.
    3248  λstart_status: Status code_memory.
    3349  λfinal_status: Status code_memory.
    34   λthe_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     50  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    3551    as_trace_any_label_length' … the_trace.
    3652
     
    150166
    151167lemma execute_1_and_program_counter_after_other_in_lockstep:
    152   ∀code_memory: BitVectorTrie Byte 16.
    153   ∀cost_labels: BitVectorTrie costlabel 16.
     168  ∀prog: labelled_object_code.
     169  let code_memory ≝ load_code_memory (oc prog) in
    154170  ∀start_status: Status code_memory.
    155     as_classifier (OC_abstract_status code_memory cost_labels) start_status cl_other →
     171    as_classifier (OC_abstract_status prog) start_status cl_other →
    156172      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    157173        program_counter ? ? (execute_1 … start_status) =
    158174          program_counter_after_other pc instruction.
    159   #code_memory #cost_labels #start_status #classify_assm
     175  #prog #start_status #classify_assm
    160176  change with (ASM_classify0 ? = ?) in classify_assm;
    161177  destruct (classify_assm)
     
    164180
    165181lemma sublist_tal_pc_list_all_program_counter_list:
    166   ∀code_memory: BitVectorTrie Byte 16.
    167   ∀cost_labels: BitVectorTrie costlabel 16.
     182  ∀prog: labelled_object_code.
     183  let code_memory ≝ load_code_memory (oc prog) in
    168184  ∀start, final: Status code_memory.
    169185  ∀trace_ends_flag.
    170   ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
     186  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
    171187    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
    172   #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
     188  #prog #start #final #trace_ends_flag #the_trace
    173189  whd in match (sublist ???); #pc #memb_assm
    174190  @lt_bound_mem_all_program_counter_list try %
     
    177193
    178194corollary tal_pc_list_length_leq_total_program_size:
    179   ∀code_memory: BitVectorTrie Byte 16.
    180   ∀cost_labels: BitVectorTrie costlabel 16.
     195  ∀prog: labelled_object_code.
     196  let code_memory ≝ load_code_memory (oc prog) in
    181197  ∀start, final: Status code_memory.
    182198  ∀trace_ends_flag.
    183   ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
     199  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
    184200  ∀unrepeating_witness: tal_unrepeating … the_trace.
    185201    |tal_pc_list … the_trace| ≤ 2^16.
    186   #code_memory #cost_labels #start #final #trace_ends_flag #the_trace #unrepeating_witness
     202  #prog #start #final #trace_ends_flag #the_trace #unrepeating_witness
    187203  <(all_program_counter_list_bound_eq (2^16))
    188204  @sublist_length
     
    197213
    198214let rec compute_paid_trace_any_label
    199   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    200     (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    201       (final_status: Status code_memory)
    202         (the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status)
     215  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
     216   (start_status: Status (load_code_memory (oc prog)))
     217   (final_status: Status (load_code_memory (oc prog)))
     218        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    203219       on the_trace: nat ≝
    204220  match the_trace with
     
    210226     _ _ _ call_trace _ final_trace ⇒
    211227      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
    212       let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
     228      let final_trace_cost ≝ compute_paid_trace_any_label prog end_flag … final_trace in
    213229        current_instruction_cost + final_trace_cost
    214230  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    215231      let current_instruction_cost ≝ current_instruction_cost … status_pre in
    216232      let tail_trace_cost ≝
    217        compute_paid_trace_any_label … cost_labels end_flag
     233       compute_paid_trace_any_label prog end_flag
    218234        status_init status_end tail_trace
    219235      in
     
    222238
    223239definition compute_paid_trace_label_label ≝
    224   λcode_memory: BitVectorTrie Byte 16.
    225   λcost_labels: BitVectorTrie costlabel 16.
     240  λprog: labelled_object_code.
     241  let code_memory ≝ load_code_memory (oc prog) in
    226242  λtrace_ends_flag: trace_ends_with_ret.
    227243  λstart_status: Status code_memory.
    228244  λfinal_status: Status code_memory.
    229   λthe_trace: (trace_label_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     245  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    230246  match the_trace with
    231247  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    234250
    235251lemma trace_compute_paid_trace_cl_other:
    236   ∀code_memory' : (BitVectorTrie Byte 16).
     252  ∀prog : labelled_object_code.
     253  let code_memory' ≝ load_code_memory (oc prog) in
    237254  ∀program_counter' : Word.
    238   ∀cost_labels : BitVectorTrie costlabel 16.
    239255  ∀program_size' : ℕ.
    240256  ∀ticks : ℕ.
     
    246262  ∀final_status : (Status code_memory').
    247263  ∀trace_ends_flag : trace_ends_with_ret.
    248   ∀the_trace : (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     264  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    249265  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    250266  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
    251267  ∀classify_assm: ASM_classify0 instruction = cl_other.
    252268  ∀pi1 : ℕ.
    253    (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
     269   (if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with 
    254270         [None ⇒ true
    255271         |Some _ ⇒ false
     
    259275      ∀final_status0:Status code_memory'.
    260276      ∀trace_ends_flag0:trace_ends_with_ret.
    261       ∀the_trace0:trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
     277      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
    262278        trace_any_label_length … the_trace0 ≤ program_size' →
    263279        program_counter''' = program_counter … start_status0 →
     
    267283   → ticks+pi1
    268284     =compute_paid_trace_any_label … the_trace.
    269   #code_memory' #program_counter' #cost_labels #program_size' #ticks #instruction
     285  #prog #program_counter' #program_size' #ticks #instruction
    270286  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
    271287  #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
     
    299315      whd in costed_assm:(?%);
    300316      generalize in match costed_assm;
    301       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
     317      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog)));
    302318      whd in match (as_label ??);
    303       generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
     319      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog))
    304320        in ⊢ (??%? → % → ?);
    305321      #lookup_assm cases lookup_assm
     
    311327        #None_lookup_opt_assm <None_lookup_opt_assm
    312328        normalize nodelta #new_recursive_assm
    313         cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
     329        cases(new_recursive_assm (execute_1 ? status_pre) status_end
    314330          end_flag trace_any_label ? ?) try (>rewrite_assm %)
    315331        whd in match (current_instruction_cost … status_pre);
    316         cut(ticks = \snd (fetch code_memory'
     332        cut(ticks = \snd (fetch (load_code_memory (oc prog))
    317333           (program_counter … status_pre)))
    318334        [1,3:
     
    340356      whd in costed_assm;
    341357      generalize in match costed_assm;
    342       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
     358      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) ?));
    343359      whd in match (as_label ??);
    344       generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels)
     360      generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) (costlabels prog))
    345361        in ⊢ (??%? → % → ?);
    346362      #lookup_assm cases lookup_assm
     
    357373          #Some_lookup_opt_assm <Some_lookup_opt_assm
    358374          normalize nodelta #new_recursive_assm >new_recursive_assm
    359           cut(ticks = \snd (fetch code_memory'
     375          cut(ticks = \snd (fetch (load_code_memory (oc prog))
    360376             (program_counter … status_start)))
    361377          [1:
     
    392408
    393409lemma trace_compute_paid_trace_cl_jump:
    394   ∀code_memory': BitVectorTrie Byte 16.
     410  ∀prog: labelled_object_code.
     411  let code_memory' ≝ load_code_memory (oc prog) in
    395412  ∀program_counter': Word.
    396   ∀cost_labels: BitVectorTrie costlabel 16.
    397413  ∀first_time_around: bool.
    398414  ∀program_size': ℕ.
     
    404420  ∀final_status: (Status code_memory').
    405421  ∀trace_ends_flag: trace_ends_with_ret.
    406   ∀the_trace: (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     422  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    407423  ∀program_counter_refl: (program_counter' = program_counter … start_status).
    408424  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    409425    ticks
    410426     =compute_paid_trace_any_label … the_trace.
    411   #code_memory' #program_counter' #cost_labels #first_time_around
     427  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #first_time_around
    412428  #program_size' #ticks #instruction #program_counter'' #FETCH
    413429  #start_status #final_status
     
    451467
    452468lemma trace_compute_paid_trace_cl_call:
    453   ∀code_memory' : (BitVectorTrie Byte 16).
     469  ∀prog: labelled_object_code.
     470  let code_memory' ≝ load_code_memory (oc prog) in
    454471  ∀program_counter' : Word.
    455   ∀cost_labels : BitVectorTrie costlabel 16.
    456472  ∀program_size' : ℕ.
    457473  ∀ticks : ℕ.
     
    462478  ∀final_status : (Status code_memory').
    463479  ∀trace_ends_flag : trace_ends_with_ret.
    464   ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     480  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    465481  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    466482  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
    467483  ∀classify_assm: ASM_classify0 instruction = cl_call.
    468484  (∀pi1:ℕ
    469   .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
     485  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
    470486      [None ⇒ true | Some _ ⇒ false] 
    471487   then (∀start_status0:Status code_memory'
     
    473489              .∀trace_ends_flag0:trace_ends_with_ret
    474490               .∀the_trace0:trace_any_label
    475                                         (OC_abstract_status … cost_labels)
     491                                        (OC_abstract_status prog)
    476492                                        trace_ends_flag0 start_status0 final_status0.
    477493                trace_any_label_length … the_trace0
     
    484500   → ticks+pi1
    485501     =compute_paid_trace_any_label … the_trace).
    486   #code_memory' #program_counter' #cost_labels #program_size'
     502  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
    487503  #ticks #instruction #program_counter'' #FETCH
    488504  #start_status #final_status #trace_ends_flag
     
    510526    whd in costed_assm;
    511527    generalize in match costed_assm;
    512     generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
     528    generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog)));
    513529    whd in match (as_label ??);
    514     generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
     530    generalize in match (lookup_opt … (program_counter … status_final) ?)
    515531      in ⊢ (??%? → % → ?);
    516532    #lookup_assm cases lookup_assm
     
    552568    whd in costed_assm:(?%);
    553569    generalize in match costed_assm;
    554     generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
     570    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?)));
    555571    whd in match (as_label ??);
    556     generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
     572    generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog))
    557573      in ⊢ (??%? → % → ?);
    558574    #lookup_assm cases lookup_assm
     
    590606
    591607lemma trace_compute_paid_trace_cl_return:
    592   ∀code_memory' : (BitVectorTrie Byte 16).
     608  ∀prog: labelled_object_code.
     609  let code_memory' ≝ load_code_memory (oc prog) in
    593610  ∀program_counter' : Word.
    594   ∀cost_labels : BitVectorTrie costlabel 16.
    595611  ∀program_size' : ℕ.
    596612  ∀ticks : ℕ.
     
    601617  ∀final_status : (Status code_memory').
    602618  ∀trace_ends_flag : trace_ends_with_ret.
    603   ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     619  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    604620  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    605621  ∀classify_assm: ASM_classify0 instruction = cl_return.
    606622    ticks
    607623     =compute_paid_trace_any_label … the_trace.
    608   #code_memory' #program_counter' #cost_labels #program_size'
     624  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
    609625  #ticks #instruction #program_counter'' #FETCH
    610626  #start_status #final_status #trace_ends_flag
     
    658674
    659675lemma trace_any_label_length_leq_0_to_False:
    660   ∀code_memory: BitVectorTrie Byte 16.
    661   ∀cost_labels: BitVectorTrie costlabel 16.
     676  ∀prog: labelled_object_code.
     677  let code_memory ≝ load_code_memory (oc prog) in
    662678  ∀trace_ends_flag: trace_ends_with_ret.
    663679  ∀start_status: Status code_memory.
    664680  ∀final_status: Status code_memory.
    665   ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     681  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    666682   trace_any_label_length … the_trace ≤ 0 → False.
    667   #code_memory #cost_labels #trace_ends_flag #start_status #final_status
    668   #the_trace
    669   cases the_trace /2/
     683  #prog #trace_ends_flag #start_status #final_status #the_trace
     684  cases the_trace /2 by absurd/
    670685qed.
    671686     
    672687let rec block_cost'
    673   (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    674     (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     688 (prog: labelled_object_code) (program_counter': Word)
     689    (program_size: nat)
    675690      (first_time_around: bool)
    676691        on program_size:
    677692          Σcost_of_block: nat.
    678           if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
    679             ∀start_status: Status code_memory'.
    680             ∀final_status: Status code_memory'.
     693          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
     694            ∀start_status,final_status: Status (load_code_memory (oc prog)).
    681695            ∀trace_ends_flag.
    682             ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     696            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    683697              trace_any_label_length … the_trace ≤ program_size →
    684698              program_counter' = program_counter … start_status →
     
    686700          else
    687701            (cost_of_block = 0) ≝
     702  let code_memory' ≝ load_code_memory (oc prog) in
    688703  match program_size return λx. x = program_size → ? with
    689704  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
    690705  | S program_size' ⇒ λstep_case.
    691     let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
     706    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (load_code_memory (oc prog)) program_counter' in
    692707    let to_continue ≝
    693       match lookup_opt … program_counter' cost_labels with
     708      match lookup_opt … program_counter' (costlabels prog) with
    694709      [ None ⇒ true
    695710      | Some _ ⇒ first_time_around
     
    701716          match real_instruction return λx. x = real_instruction →
    702717          Σcost_of_block: nat.
    703             ∀start_status: Status code_memory'.
    704             ∀final_status: Status code_memory'.
     718            ∀start_status,final_status: Status code_memory'.
    705719            ∀trace_ends_flag.
    706             ∀the_trace: trace_any_label (OC_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
     720            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    707721              trace_any_label_length … the_trace ≤ S program_size' →
    708722              program_counter' = program_counter … start_status →
     
    720734          | DJNZ src_trgt relative ⇒ λinstr. ticks
    721735          | JMP   addr             ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    722               ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     736              ticks + block_cost' prog program_counter'' program_size' false
    723737          | _                      ⇒ λinstr.
    724               ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     738              ticks + block_cost' prog program_counter'' program_size' false
    725739          ] (refl …)
    726740        | ACALL addr     ⇒ λinstr.
    727             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     741            ticks + block_cost' prog program_counter'' program_size' false
    728742        | AJMP  addr     ⇒ λinstr.
    729743          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    730             ticks + block_cost' code_memory' jump_target program_size' cost_labels false
     744            ticks + block_cost' prog jump_target program_size' false
    731745        | LCALL addr     ⇒ λinstr.
    732             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     746            ticks + block_cost' prog program_counter'' program_size' false
    733747        | LJMP  addr     ⇒ λinstr.
    734748          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    735             ticks + block_cost' code_memory' jump_target program_size' cost_labels false
     749            ticks + block_cost' prog jump_target program_size' false
    736750        | SJMP  addr     ⇒ λinstr.
    737751          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    738             ticks + block_cost' code_memory' jump_target program_size' cost_labels false
     752            ticks + block_cost' prog jump_target program_size' false
    739753        | MOVC  src trgt ⇒ λinstr.
    740             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     754            ticks + block_cost' prog program_counter'' program_size' false
    741755        ] (refl …))
    742756      else
    743757        0)
    744758      : Σcost_of_block: nat.
    745           match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
     759          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
    746760          [ true ⇒
    747761            ∀start_status: Status code_memory'.
    748762            ∀final_status: Status code_memory'.
    749763            ∀trace_ends_flag.
    750             ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     764            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    751765              trace_any_label_length … the_trace ≤ S program_size' →
    752766              program_counter' = program_counter … start_status →
     
    781795  |4,46,47:
    782796    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    783     cases(block_cost' ?????) -block_cost'
     797    cases(block_cost' ???) -block_cost'
    784798    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    785799    destruct %
    786800  |43,44,45: (* XXX: unconditional jumps *)
    787801    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    788     cases (block_cost' ?????) -block_cost'
     802    cases (block_cost' ???) -block_cost'
    789803    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    790804    whd in match (program_counter_after_other ??); normalize nodelta destruct
    791805    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
    792806  |25,26,27,28,29,30,31,32,33:
    793     #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl 
    794     @(trace_compute_paid_trace_cl_jump … first_time_around program_size' … FETCH … the_trace program_counter_refl)
    795     destruct %
     807    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     808    @(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl)
     809   destruct %
    796810  |4,33:
    797811  |*:
    798812    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    799     cases(block_cost' ?????) -block_cost'
     813    cases(block_cost' ???) -block_cost'
    800814    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)     
    801815    destruct #assm @assm %
     
    804818
    805819definition block_cost:
    806     ∀code_memory': BitVectorTrie Byte 16.
     820    ∀prog: labelled_object_code.
    807821    ∀program_counter': Word.
    808     ∀cost_labels: BitVectorTrie costlabel 16.
    809822      Σcost_of_block: nat.
    810         ∀start_status: Status code_memory'.
    811         ∀final_status: Status code_memory'.
     823        ∀start_status: Status (load_code_memory (oc prog)).
     824        ∀final_status: Status (load_code_memory (oc prog)).
    812825        ∀trace_ends_flag.
    813         ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     826        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    814827        ∀unrepeating_witness: tal_unrepeating … the_trace.
    815828          program_counter' = program_counter … start_status →
    816             cost_of_block = compute_paid_trace_any_label … the_trace ≝
    817   λcode_memory: BitVectorTrie Byte 16.
    818   λprogram_counter: Word.
    819   λcost_labels: BitVectorTrie costlabel 16. ?.
    820   cases(block_cost' code_memory program_counter (2^16) cost_labels true)
     829            cost_of_block = compute_paid_trace_any_label … the_trace.
     830  #prog #program_counter
     831  cases(block_cost' prog program_counter (2^16) true)
    821832  #cost_of_block #block_cost_hyp
    822833  %{cost_of_block}
    823   cases(lookup_opt … cost_labels) in block_cost_hyp;
     834  cases(lookup_opt … (costlabels prog)) in block_cost_hyp;
    824835  [2: #cost_label] normalize nodelta
    825836  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
  • src/ASM/ASMCostsSplit.ma

    r2899 r2907  
    66
    77let rec traverse_code_internal
    8   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     8  (prog: labelled_object_code)
    99    (program_counter: Word) (program_size: nat)
    1010      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
    1111        on program_size:
    1212          Σcost_map: identifier_map CostTag nat.
    13             (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    14             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
    15                pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
     13            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k) ∧
     14            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc (costlabels prog) = Some … k ∧
     15               pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝
    1616  match program_size return λx. x = program_size → Σcost_map: ?. ? with
    1717  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    1818  | S program_size' ⇒ λprogram_size_refl.
    1919    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
    20     let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    21     match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
     20    let cost_mapping ≝ traverse_code_internal prog new_program_counter' program_size' ? in
     21    match lookup_opt … program_counter (costlabels prog)
     22    return λx. x = lookup_opt … program_counter (costlabels prog) → Σcost_map: ?. ? with
    2223    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    2324    | Some lbl ⇒ λlookup_refl.
    24       let cost ≝ block_cost code_memory program_counter cost_labels in
     25      let cost ≝ block_cost prog program_counter in
    2526        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
    26     ] (refl … (lookup_opt … program_counter cost_labels))
     27    ] (refl … (lookup_opt … program_counter (costlabels prog)))
    2728  ] (refl … program_size).
    2829  [3:
     
    279280 *)
    280281definition traverse_code:
    281   ∀code_memory: BitVectorTrie Byte 16.
    282   ∀cost_labels: BitVectorTrie costlabel 16.
    283   ∀cost_labels_injective:
    284     ∀pc, pc',l.
    285       lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    286         pc = pc'.
     282  ∀prog: labelled_object_code.
     283   let cost_labels ≝ costlabels prog in
    287284    Σcost_map: identifier_map CostTag nat.
    288285      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    289286      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    290           pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    291   λcode_memory: BitVectorTrie Byte 16.
    292   λcost_labels: BitVectorTrie costlabel 16.
    293   λcost_labels_injective.
    294     pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
     287          pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝
     288  λprog.
     289    pi1 ? ? (traverse_code_internal prog (zero …) (2^16) ?).
    295290  [1:
    296291    @or_intror %
    297292  |2:
    298     cases (traverse_code_internal ?????)
     293    cases (traverse_code_internal ???)
    299294    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
    300295    [1:
     
    311306      cases (inductive_hypothesis2 ? k_pres)
    312307      #program_counter' * #lookup_opt_assm' #block_cost_assm
    313       >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
     308      >(oc_injective_costlabels … lookup_opt_assm lookup_opt_assm')
    314309      assumption
    315310    ]
     
    317312qed.
    318313   
    319 definition compute_costs ≝
    320   λprogram: object_code.
    321   λcost_labels: BitVectorTrie costlabel 16.
    322   λcost_labels_injective:
    323     ∀pc, pc',l.
    324       lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    325         pc = pc'.
    326     (* let program_size ≝ |program| in *)
    327     let code_memory ≝ load_code_memory program in
    328       traverse_code code_memory cost_labels cost_labels_injective.
     314definition compute_costs ≝ traverse_code.
    329315
    330316definition ASM_cost_map :
    331317  ∀p: labelled_object_code.
    332318  let code_memory ≝ load_code_memory (oc p) in
    333   let a_s ≝ OC_abstract_status code_memory (costlabels p) in
     319  let a_s ≝ OC_abstract_status p in
    334320  as_cost_map a_s ≝
    335321  λp.
    336   let cost_map ≝ compute_costs (oc p) (costlabels p) (oc_injective_costlabels … p) in
     322  let cost_map ≝ compute_costs p in
    337323  λl_sig.
    338324  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
  • src/ASM/CostsProof.ma

    r2899 r2907  
    99
    1010let rec compute_max_trace_label_label_cost
    11   (cm: ?)
    12   (cost_labels: BitVectorTrie costlabel 16)
     11  (prog: labelled_object_code)
    1312   (trace_ends_flag: trace_ends_with_ret)
    14     (start_status: Status cm) (final_status: Status cm)
    15       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     13    (start_status: Status (load_code_memory (oc prog)))
     14    (final_status: Status (load_code_memory (oc prog)))
     15      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
    1717  match the_trace with
     
    2020  ]
    2121and compute_max_trace_any_label_cost
    22   (cm: ?)
    23   (cost_labels: BitVectorTrie costlabel 16)
     22  (prog: labelled_object_code)
    2423  (trace_ends_flag: trace_ends_with_ret)
    25    (start_status: Status cm) (final_status: Status cm)
    26      (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     24   (start_status: Status (load_code_memory (oc prog)))
     25   (final_status: Status (load_code_memory (oc prog)))
     26     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
    2828  match the_trace with
    29   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost cm the_status
    30   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost cm the_status
     29  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
     30  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
    3131  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    32       let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     32      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    3333      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    3434        call_trace_cost + current_instruction_cost
    3535  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    36       let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     36      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    3737      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    3838        call_trace_cost + current_instruction_cost
    3939  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    4040     _ _ _ call_trace _ final_trace ⇒
    41       let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     41      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    4242      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    43       let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in
     43      let final_trace_cost ≝ compute_max_trace_any_label_cost prog end_flag … final_trace in
    4444        call_trace_cost + current_instruction_cost + final_trace_cost
    4545  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    46       let current_instruction_cost ≝ current_instruction_cost cm status_pre in
     46      let current_instruction_cost ≝ current_instruction_cost status_pre in
    4747      let tail_trace_cost ≝
    48        compute_max_trace_any_label_cost cm cost_labels end_flag
     48       compute_max_trace_any_label_cost prog end_flag
    4949        status_init status_end tail_trace
    5050      in
     
    5252  ]
    5353and compute_max_trace_label_return_cost
    54   (cm: ?)
    55   (cost_labels: BitVectorTrie costlabel 16)
    56   (start_status: Status cm) (final_status: Status cm)
    57     (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
     54  (prog: labelled_object_code)
     55  (start_status: Status (load_code_memory (oc prog)))
     56  (final_status: Status (load_code_memory (oc prog)))
     57    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    5858      on the_trace: nat ≝
    5959  match the_trace with
     
    6868
    6969let rec compute_max_trace_label_label_cost_is_ok
    70   (cm: ?)
    71   (cost_labels: BitVectorTrie costlabel 16)
     70  (prog: labelled_object_code)
    7271   (trace_ends_flag: trace_ends_with_ret)
    73     (start_status: Status cm) (final_status: Status cm)
    74       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     72    (start_status: Status (load_code_memory (oc prog)))
     73    (final_status: Status (load_code_memory (oc prog)))
     74      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    7575        start_status final_status) on the_trace:
    76           clock … cm … final_status = (compute_max_trace_label_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ?
     76          clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?
    7777and compute_max_trace_any_label_cost_is_ok
    78   (cm: ?)
    79   (cost_labels: BitVectorTrie costlabel 16)
     78  (prog: labelled_object_code)
    8079  (trace_ends_flag: trace_ends_with_ret)
    81    (start_status: Status cm) (final_status: Status cm)
    82      (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     80    (start_status: Status (load_code_memory (oc prog)))
     81    (final_status: Status (load_code_memory (oc prog)))
     82     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    8383       on the_trace:
    84          clock … cm … final_status = (compute_max_trace_any_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ?
     84         clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?
    8585and compute_max_trace_label_return_cost_is_ok
    86   (cm: ?)
    87   (cost_labels: BitVectorTrie costlabel 16)
    88   (start_status: Status cm) (final_status: Status cm)
    89     (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
     86  (prog: labelled_object_code)
     87    (start_status: Status (load_code_memory (oc prog)))
     88    (final_status: Status (load_code_memory (oc prog)))
     89    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    9090      on the_trace:
    91         clock … cm … final_status = (compute_max_trace_label_return_cost cm cost_labels start_status final_status the_trace) + clock … cm … start_status ≝ ?.
     91        clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (load_code_memory (oc prog)) … start_status ≝ ?.
    9292  [1:
    9393    cases the_trace
    9494    #ends_flag #start_status #end_status #any_label_trace #is_costed
    95     normalize @compute_max_trace_any_label_cost_is_ok
     95    @compute_max_trace_any_label_cost_is_ok
    9696  |2:
    9797    cases the_trace
    9898    [1,2:
    9999      #start_status #final_status #is_next #is_not_return try (#is_costed)
    100       change with (current_instruction_cost cm start_status) in ⊢ (???(?%?));
     100      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
    101101      cases(is_next) @execute_1_ok_clock
    102102    |3:
     
    104104      #classifier_assm #after_return_assm #call_trace #costed_assm
    105105      whd in match (compute_max_trace_any_label_cost … (tal_base_call …));
    106       >(compute_max_trace_label_return_cost_is_ok … call_trace)
     106      >(compute_max_trace_label_return_cost_is_ok prog … call_trace)
    107107      >associative_plus @eq_f cases(is_next)
    108108      @execute_1_ok_clock
     
    118118      #status_final #is_next #is_call #is_after_return #call_trace #not_costed #final_trace
    119119      change with (
    120       let current_instruction_cost ≝ current_instruction_cost cm status_pre_fun_call in
    121       let call_trace_cost ≝ compute_max_trace_label_return_cost cm … call_trace in
    122       let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in
     120      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
     121      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     122      let final_trace_cost ≝ compute_max_trace_any_label_cost prog end_flag … final_trace in
    123123        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
    124124      normalize nodelta;
    125       >(compute_max_trace_any_label_cost_is_ok … cost_labels end_flag status_after_fun_call
     125      >(compute_max_trace_any_label_cost_is_ok prog end_flag status_after_fun_call
    126126          status_final final_trace)
    127       >(compute_max_trace_label_return_cost_is_ok … cost_labels status_start_fun_call
     127      >(compute_max_trace_label_return_cost_is_ok prog status_start_fun_call
    128128        status_after_fun_call call_trace)
    129       cases(is_next) in match (clock … cm status_start_fun_call);
    130       >(execute_1_ok_clock cm status_pre_fun_call)
     129      cases(is_next) in match (clock … (load_code_memory (oc prog)) status_start_fun_call);
     130      >(execute_1_ok_clock status_pre_fun_call)
    131131      <associative_plus in ⊢ (??%?);
    132132      <commutative_plus in match (
    133         compute_max_trace_any_label_cost cm cost_labels end_flag status_after_fun_call status_final final_trace
    134           + compute_max_trace_label_return_cost cm cost_labels status_start_fun_call status_after_fun_call call_trace);
     133        compute_max_trace_any_label_cost prog end_flag status_after_fun_call status_final final_trace
     134          + compute_max_trace_label_return_cost prog status_start_fun_call status_after_fun_call call_trace);
    135135      >associative_plus in ⊢ (??%?); >associative_plus in ⊢ (???%); >associative_plus in ⊢ (???%);
    136136      @eq_f >commutative_plus in ⊢ (??%?); >associative_plus in ⊢ (??%?);
    137       @eq_f @commutative_plus 
     137      @eq_f @commutative_plus
    138138    |6:
    139139      #end_flag #status_pre #status_init #status_end #is_next
    140140      #trace_any_label #is_other #is_not_costed
    141141      change with (
    142       let current_instruction_cost ≝ current_instruction_cost cm status_pre in
     142      let current_instruction_cost ≝ current_instruction_cost status_pre in
    143143      let tail_trace_cost ≝
    144        compute_max_trace_any_label_cost cm cost_labels end_flag
     144       compute_max_trace_any_label_cost prog end_flag
    145145        status_init status_end trace_any_label
    146146      in
    147147        current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?));
    148148      normalize nodelta;
    149       >(compute_max_trace_any_label_cost_is_ok cm cost_labels end_flag
     149      >(compute_max_trace_any_label_cost_is_ok prog end_flag
    150150         status_init status_end trace_any_label)
    151       cases(is_next) in match (clock … cm status_init);
     151      cases(is_next) in match (clock … (load_code_memory (oc prog)) status_init);
    152152      >(execute_1_ok_clock … status_pre)
    153153      >commutative_plus >associative_plus >associative_plus @eq_f
     
    158158    [1:
    159159      #status_before #status_after #trace_to_lift
    160       normalize @compute_max_trace_label_label_cost_is_ok
     160      @compute_max_trace_label_label_cost_is_ok
    161161    |2:
    162162      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
    163       normalize
    164       >(compute_max_trace_label_return_cost_is_ok cm cost_labels status_labelled status_final ret_trace);
    165       >(compute_max_trace_label_label_cost_is_ok cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     163      >(compute_max_trace_label_return_cost_is_ok prog status_labelled status_final ret_trace);
     164      >(compute_max_trace_label_label_cost_is_ok prog doesnt_end_with_ret status_initial status_labelled labelled_trace);
    166165      <associative_plus in ⊢ (??%?);
    167166      >commutative_plus in match (
    168         compute_max_trace_label_return_cost cm cost_labels status_labelled status_final ret_trace
    169           + compute_max_trace_label_label_cost cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     167        compute_max_trace_label_return_cost prog status_labelled status_final ret_trace
     168          + compute_max_trace_label_label_cost prog doesnt_end_with_ret status_initial status_labelled labelled_trace);
    170169      %
    171170    ]
     
    174173
    175174let rec compute_trace_label_label_cost_using_paid
    176   (cm: ?)
    177   (cost_labels: BitVectorTrie costlabel 16)
     175  (prog:labelled_object_code)
    178176   (trace_ends_flag: trace_ends_with_ret)
    179     (start_status: Status cm) (final_status: Status cm)
    180       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     177    (start_status: Status (load_code_memory (oc prog)))
     178    (final_status: Status (load_code_memory (oc prog)))
     179      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    181180        start_status final_status) on the_trace: nat ≝
    182181  match the_trace with
    183182  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    184       compute_paid_trace_label_label cm cost_labels … the_trace +
     183      compute_paid_trace_label_label prog … the_trace +
    185184      compute_trace_any_label_cost_using_paid … given_trace
    186185  ]
    187186and compute_trace_any_label_cost_using_paid
    188   (cm: ?)
    189   (cost_labels: BitVectorTrie costlabel 16)
     187  (prog:labelled_object_code)
    190188  (trace_ends_flag: trace_ends_with_ret)
    191    (start_status: Status cm) (final_status: Status cm)
    192      (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     189    (start_status: Status (load_code_memory (oc prog)))
     190    (final_status: Status (load_code_memory (oc prog)))
     191     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    193192       on the_trace: nat ≝
    194193  match the_trace with
     
    202201     _ _ _ call_trace _ final_trace ⇒
    203202      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
    204       let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cm cost_labels end_flag … final_trace in
     203      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid prog end_flag … final_trace in
    205204        call_trace_cost + final_trace_cost
    206205  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    207      compute_trace_any_label_cost_using_paid cm cost_labels end_flag
     206     compute_trace_any_label_cost_using_paid prog end_flag
    208207      status_init status_end tail_trace
    209208  ]
    210209and compute_trace_label_return_cost_using_paid
    211   (cm: ?)
    212   (cost_labels: BitVectorTrie costlabel 16)
    213   (start_status: Status cm) (final_status: Status cm)
    214     (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
     210  (prog:labelled_object_code)
     211    (start_status: Status (load_code_memory (oc prog)))
     212    (final_status: Status (load_code_memory (oc prog)))
     213    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    215214      on the_trace: nat ≝
    216215  match the_trace with
     
    223222
    224223let rec compute_trace_label_label_cost_using_paid_ok
    225   (cm: ?)
    226   (cost_labels: BitVectorTrie costlabel 16)
     224  (prog:labelled_object_code)
    227225   (trace_ends_flag: trace_ends_with_ret)
    228     (start_status: Status cm) (final_status: Status cm)
    229       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     226    (start_status: Status (load_code_memory (oc prog)))
     227    (final_status: Status (load_code_memory (oc prog)))
     228      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    230229        start_status final_status) on the_trace:
    231  compute_trace_label_label_cost_using_paid cm cost_labels … the_trace =
     230 compute_trace_label_label_cost_using_paid prog … the_trace =
    232231 compute_max_trace_label_label_cost … the_trace ≝ ?
    233232and compute_trace_any_label_cost_using_paid_ok
    234   (cm: ?)
    235   (cost_labels: BitVectorTrie costlabel 16)
     233  (prog:labelled_object_code)
    236234  (trace_ends_flag: trace_ends_with_ret)
    237    (start_status: Status cm) (final_status: Status cm)
    238      (the_trace: trace_any_label (OC_abstract_status cm cost_labels)
     235    (start_status: Status (load_code_memory (oc prog)))
     236    (final_status: Status (load_code_memory (oc prog)))
     237     (the_trace: trace_any_label (OC_abstract_status prog)
    239238      trace_ends_flag start_status final_status) on the_trace:     
    240   compute_paid_trace_any_label cm cost_labels trace_ends_flag … the_trace
    241   +compute_trace_any_label_cost_using_paid cm cost_labels trace_ends_flag … the_trace
    242   =compute_max_trace_any_label_cost cm cost_labels trace_ends_flag … the_trace ≝ ?
     239  compute_paid_trace_any_label prog trace_ends_flag … the_trace
     240  +compute_trace_any_label_cost_using_paid prog trace_ends_flag … the_trace
     241  =compute_max_trace_any_label_cost prog trace_ends_flag … the_trace ≝ ?
    243242and compute_trace_label_return_cost_using_paid_ok
    244   (cm: ?)
    245   (cost_labels: BitVectorTrie costlabel 16)
    246   (start_status: Status cm) (final_status: Status cm)
    247     (the_trace: trace_label_return (OC_abstract_status cm cost_labels)
     243  (prog:labelled_object_code)
     244    (start_status: Status (load_code_memory (oc prog)))
     245    (final_status: Status (load_code_memory (oc prog)))
     246    (the_trace: trace_label_return (OC_abstract_status prog)
    248247     start_status final_status) on the_trace:
    249  compute_trace_label_return_cost_using_paid cm cost_labels … the_trace =
    250  compute_max_trace_label_return_cost cm cost_labels … the_trace ≝ ?.
     248 compute_trace_label_return_cost_using_paid prog … the_trace =
     249 compute_max_trace_label_return_cost prog … the_trace ≝ ?.
    251250[ cases the_trace #endsf #ss #es #tr #H normalize
    252251  @compute_trace_any_label_cost_using_paid_ok
     
    453452
    454453let rec compute_trace_label_return_using_paid_ok_with_trace
    455  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     454 (prog: labelled_object_code)
    456455 (cost_map: identifier_map CostTag nat)
    457  (initial: Status cm) (final: Status cm)
    458  (trace: trace_label_return (OC_abstract_status cm cost_labels) initial final)
    459  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
     456 (initial: Status (load_code_memory (oc prog)))
     457 (final: Status (load_code_memory (oc prog)))
     458 (trace: trace_label_return (OC_abstract_status prog) initial final)
     459 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
    460460 on trace:
    461461 ∀unrepeating_witness: tlr_unrepeating … trace.
    462  ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    463    pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    464   let ctrace ≝ flatten_trace_label_return (OC_abstract_status cm cost_labels) … trace in
    465   compute_trace_label_return_cost_using_paid cm … trace =
    466    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     462 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     463   pi1 … (block_cost prog pc) = lookup_present … k_pres).
     464  let ctrace ≝ flatten_trace_label_return (OC_abstract_status prog) … trace in
     465  compute_trace_label_return_cost_using_paid prog … trace =
     466   (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
    467467    ≝ ?
    468468and compute_trace_any_label_using_paid_ok_with_trace
    469  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     469 (prog: labelled_object_code)
    470470 (trace_ends_flag: trace_ends_with_ret)
    471471 (cost_map: identifier_map CostTag nat)
    472  (initial: Status cm) (final: Status cm)
    473  (trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
    474  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    475  (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    476    pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres))
     472 (initial: Status (load_code_memory (oc prog)))
     473 (final: Status (load_code_memory (oc prog)))
     474 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
     475 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     476 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     477   pi1 … (block_cost prog pc) = lookup_present … k_pres))
    477478 on trace:
    478479  ∀unrepeating_witness: tal_unrepeating … trace.
    479   let ctrace ≝ flatten_trace_any_label (OC_abstract_status cm cost_labels) … trace_ends_flag … trace in
     480  let ctrace ≝ flatten_trace_any_label (OC_abstract_status prog) … trace_ends_flag … trace in
    480481  compute_trace_any_label_cost_using_paid … trace =
    481    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     482   (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
    482483    ≝ ?
    483484and compute_trace_label_label_using_paid_ok_with_trace
    484  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     485 (prog: labelled_object_code)
    485486 (trace_ends_flag: trace_ends_with_ret)
    486487 (cost_map: identifier_map CostTag nat)
    487  (initial: Status cm) (final: Status cm)
    488  (trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
     488 (initial: Status (load_code_memory (oc prog)))
     489 (final: Status (load_code_memory (oc prog)))
     490 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
    489491 (unrepeating_witness: tll_unrepeating … trace)
    490  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    491  (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    492    pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres))
     492 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     493 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     494   pi1 … (block_cost prog pc) = lookup_present … k_pres))
    493495 on trace:
    494496 ∀unrepeating_witness: tll_unrepeating … trace.
    495   let ctrace ≝ flatten_trace_label_label (OC_abstract_status cm cost_labels) … trace in
     497  let ctrace ≝ flatten_trace_label_label (OC_abstract_status prog) … trace in
    496498  compute_trace_label_label_cost_using_paid … trace =
    497    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     499   (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
    498500    ≝ ?.
    499501  cases trace normalize nodelta
     
    541543        whd in ⊢ (∀p:????%.???(????%?));
    542544        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
    543         inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
     545        inversion (lookup_opt ? ? (program_counter … start_status) (costlabels prog))
    544546        [1:
    545547          #_ #absurd @⊥ cases absurd #absurd @absurd %
     
    547549          normalize nodelta #cost_label #Some_assm #_ #p
    548550          cases (dom_codom ? p ? Some_assm)
    549           cases (block_cost ???)
     551          cases (block_cost ??)
    550552          #cost #block_cost_assm
    551553          cases (block_cost_assm ??? trace_any_label ??)
     
    626628 
    627629lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    628   ∀code_memory: BitVectorTrie Byte 16.
    629   ∀cost_labels: BitVectorTrie costlabel 16.
     630  ∀prog: labelled_object_code.
    630631  ∀cost_map: identifier_map CostTag nat.
    631   ∀initial: Status code_memory.
    632   ∀final: Status code_memory.
    633   ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
     632  ∀initial: Status (load_code_memory (oc prog)).
     633  ∀final: Status (load_code_memory (oc prog)).
     634  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    634635  ∀unrepeating_witness: tlr_unrepeating … trace.
    635   ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    636   ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    637       pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres).
     636  ∀codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k).
     637  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     638      pi1 … (block_cost prog pc) = lookup_present … k_pres).
    638639        let ctrace ≝ flatten_trace_label_return … trace in
    639           clock … code_memory … final =
    640             clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
    641   #code_memory #cost_labels #cost_map
     640          clock … (load_code_memory (oc prog)) … final =
     641            clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
     642  #prog #cost_map
    642643  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    643644  <compute_trace_label_return_using_paid_ok_with_trace try assumption
     
    646647
    647648theorem compute_max_trace_label_return_cost_ok_with_trace:
    648   ∀code_memory: BitVectorTrie Byte 16.
    649   ∀cost_labels: BitVectorTrie costlabel 16.
    650   ∀cost_labels_injective:
    651    (∀pc,pc',l.
    652      lookup_opt costlabel 16 pc cost_labels=Some costlabel l
    653       →lookup_opt costlabel 16 pc' cost_labels=Some costlabel l→pc=pc').
    654   ∀initial: Status code_memory.
    655   ∀final: Status code_memory.
    656   ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
     649  ∀prog: labelled_object_code.
     650  ∀initial: Status (load_code_memory (oc prog)).
     651  ∀final: Status (load_code_memory (oc prog)).
     652  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    657653  ∀unrepeating_witness: tlr_unrepeating … trace.
    658     let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
     654    let cost_map ≝ traverse_code prog in
    659655    let ctrace ≝ flatten_trace_label_return … trace in
    660       clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
     656      clock … (load_code_memory (oc prog)) … final = clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
    661657  [1:
    662     #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
     658    #prog #initial #final #trace #unrepeating_witness
    663659    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    664660  |2:
     
    666662  ]
    667663  normalize nodelta
    668   cases (traverse_code ???)
     664  cases (traverse_code ?)
    669665  #cost_map * #dom_codom #codom_dom try assumption
    670666  #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
     
    682678
    683679lemma costlabel_map_of_as_cost_labels_map_ok:
    684  ∀ccode1,ccode2,cost_labels_injective,tl,Htl,PRF,PRF2.
    685   lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective) tl
     680 ∀prog,tl,Htl,PRF,PRF2.
     681  lookup_present CostTag ℕ (compute_costs prog) tl
    686682  PRF
    687683  =
    688    lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective)
    689    (as_cost_get_label (OC_abstract_status (load_code_memory ccode1) ccode2)
     684   lookup_present CostTag ℕ (compute_costs prog)
     685   (as_cost_get_label (OC_abstract_status prog)
    690686    «tl,Htl») PRF2.
    691687//
     
    695691  ∀compiled_code: labelled_object_code.
    696692  let cost_labels ≝ costlabels compiled_code in
    697   let cost_map ≝ compute_costs (oc compiled_code) (costlabels compiled_code) (oc_injective_costlabels compiled_code) in
     693  let cost_map ≝ compute_costs compiled_code in
    698694  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    699695  ∀trace.
  • src/ASM/Interpret2.ma

    r2905 r2907  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
    41   let cm ≝ load_code_memory (oc c) in
    4241  mk_preclassified_system_of_abstract_status
    4342   labelled_object_code
    44    (OC_abstract_status cm (costlabels c))
     43   (OC_abstract_status c)
    4544   (λst. return (execute_1 … st))
    46    (initialise_status … cm).
     45   (initialise_status … (load_code_memory (oc c))).
    4746
    4847(* Pre-classified system for ASM *)
     
    101100qed.
    102101
     102definition ASM_as_result: ∀prog. PseudoStatus prog → option int ≝
     103 λprog,st.
     104  let finaladdr ≝ address_of_word_labels (code prog) (final_label … prog) in
     105   as_result_of_finaladdr … st finaladdr.
     106
    103107definition ASM_abstract_status:
    104108 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
     
    112116      (ASM_as_label_of_pc prog …)
    113117      (ASM_next_instruction_properly_relates_program_counters prog)
    114       ? (* (λs.False) *)
     118      (ASM_as_result …)
    115119      ?
    116120      ?.
    117   #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
     121  #x cases daemon (* XXX: (tail)call_ident function *)
    118122qed.
    119123
  • src/ASM/Status.ma

    r2770 r2907  
    708708    let memory ≝
    709709      if head' … bit_one then
     710        (high_internal_ram ?? s)
     711      else
    710712        (low_internal_ram ?? s)
    711       else
    712         (high_internal_ram ?? s)
    713713    in
    714714      lookup … seven_bits memory (zero 8).
  • src/compiler.ma

    r2899 r2907  
    135135
    136136definition lift_cost_map_back_to_front :
    137   ∀clight, code_memory, lbls.
    138     let abstat ≝ OC_abstract_status code_memory lbls in
     137  ∀clight, oc.
     138    let abstat ≝ OC_abstract_status oc in
    139139  as_cost_map abstat → clight_cost_map clight ≝
    140   λclight,code_memory,lbls,k,asm_cost_map.
     140  λclight,oc,k,asm_cost_map.
    141141  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    142142    (strong_decidable_in_codomain …) k asm_cost_map.
     
    160160  let k ≝ ASM_cost_map p in
    161161  let k' ≝
    162    lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
     162   lift_cost_map_back_to_front p' p k in
    163163  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracChangeset for help on using the changeset viewer.