Changeset 2999 for src/ASM


Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (7 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

Location:
src/ASM
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2767 r2999  
    11561156}.
    11571157
    1158 definition object_code ≝ list Byte.
     1158definition object_code ≝ list Byte.
     1159
     1160include alias "ASM/BitVectorTrie.ma".
     1161include alias "ASM/Arithmetic.ma".
     1162
     1163definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
     1164  λpmem: BitVectorTrie Byte 16.
     1165  λpc: Word.
     1166    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
     1167
     1168definition load_code_memory0:
     1169 ∀program: object_code. Σres: BitVectorTrie Byte 16.
     1170  let program_size ≝ |program| in
     1171   program_size ≤ 2^16 →
     1172    ∀pc. ∀pc_ok: pc < program_size.
     1173     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
     1174
     1175 λprogram. \snd
     1176  (foldl_strong ?
     1177   (λprefix.
     1178     Σres: nat × (BitVectorTrie Byte 16).
     1179      let 〈i,mem〉 ≝ res in
     1180      i = |prefix| ∧
     1181      (i ≤ 2^16 →
     1182        ∀pc. ∀pc_ok: pc < |prefix|.
     1183         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
     1184   program
     1185   (λprefix,v,tl,prf,i_mem.
     1186     let 〈i,mem〉 ≝ i_mem in
     1187      〈S i,insert … (bitvector_of_nat … i) v mem〉)
     1188  〈0,Stub Byte 16〉).
     1189[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
     1190| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
     1191| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
     1192  [ >length_append >H1 normalize //
     1193  | #LE #pc #pc_ok
     1194    cases (le_to_or_lt_eq … pc_ok)
     1195    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
     1196      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
     1197      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
     1198      <H1 <plus_n_O whd in ⊢ (???%); //
     1199    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     1200      >H2 [2: @(transitive_le … LE) //]
     1201      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
     1202      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     1203      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
     1204      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
     1205qed.
     1206
     1207definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
     1208 λprogram.load_code_memory0 program.
     1209
     1210lemma load_code_memory_ok:
     1211 ∀program: object_code.
     1212  let program_size ≝ |program| in
     1213   program_size ≤ 2^16 →
     1214    ∀pc. ∀pc_ok: pc < program_size.
     1215     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     1216whd in match load_code_memory; normalize nodelta #program @pi2
     1217qed.
     1218
     1219
    11591220definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *)
    11601221definition symboltable_type ≝ BitVectorTrie ident 16.  (* XXX *)
    11611222record labelled_object_code : Type[0] ≝
    11621223{ oc : object_code
     1224; cm: BitVectorTrie Byte 16
     1225; cm_def: cm = load_code_memory oc
    11631226; costlabels : costlabel_map
    11641227; symboltable : symboltable_type
     
    11681231  partial_injection … (λpc.lookup_opt … pc costlabels)
    11691232}.
    1170 
    1171 
    1172 
  • src/ASM/ASMCosts.ma

    r2993 r2999  
    3737definition OC_abstract_status: labelled_object_code → abstract_status ≝
    3838 λprog.
    39   let code_memory ≝ load_code_memory (oc prog) in
    4039    mk_abstract_status
    41       (Status code_memory)
     40      (Status (cm prog))
    4241      (λs1,s2. execute_1 … s1 = s2)
    4342      word_deqset
    44       (program_counter … code_memory)
    45       (OC_classify code_memory)
     43      (program_counter …)
     44      (OC_classify )
    4645      (λpc.lookup_opt … pc (costlabels prog))
    47       (next_instruction_properly_relates_program_counters code_memory)
    48       (λst. as_result_of_finaladdr … code_memory … st (final_pc prog))
    49       (OC_as_call_ident prog code_memory)
     46      (next_instruction_properly_relates_program_counters )
     47      (λst. as_result_of_finaladdr … st (final_pc prog))
     48      (OC_as_call_ident prog )
    5049      ?.
    5150 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
     
    5554definition trace_any_label_length ≝
    5655  λprog: labelled_object_code.
    57   let code_memory ≝ load_code_memory (oc prog) in
    5856  λtrace_ends_flag: trace_ends_with_ret.
    59   λstart_status: Status code_memory.
    60   λfinal_status: Status code_memory.
     57  λstart_status: Status (cm prog).
     58  λfinal_status: Status (cm prog).
    6159  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    6260    as_trace_any_label_length' … the_trace.
     
    178176lemma execute_1_and_program_counter_after_other_in_lockstep:
    179177  ∀prog: labelled_object_code.
    180   let code_memory ≝ load_code_memory (oc prog) in
    181   ∀start_status: Status code_memory.
     178  ∀start_status: Status (cm prog).
    182179    as_classifier (OC_abstract_status prog) start_status cl_other →
    183       let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     180      let 〈instruction, pc, ticks〉 ≝ fetch (cm prog) (program_counter … start_status) in
    184181        program_counter ? ? (execute_1 … start_status) =
    185182          program_counter_after_other pc instruction.
     
    192189lemma sublist_tal_pc_list_all_program_counter_list:
    193190  ∀prog: labelled_object_code.
    194   let code_memory ≝ load_code_memory (oc prog) in
    195   ∀start, final: Status code_memory.
     191  ∀start, final: Status (cm prog).
    196192  ∀trace_ends_flag.
    197193  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
     
    205201corollary tal_pc_list_length_leq_total_program_size:
    206202  ∀prog: labelled_object_code.
    207   let code_memory ≝ load_code_memory (oc prog) in
    208   ∀start, final: Status code_memory.
     203  ∀start, final: Status (cm prog).
    209204  ∀trace_ends_flag.
    210205  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
     
    225220let rec compute_paid_trace_any_label
    226221  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
    227    (start_status: Status (load_code_memory (oc prog)))
    228    (final_status: Status (load_code_memory (oc prog)))
     222   (start_status: Status (cm prog))
     223   (final_status: Status (cm prog))
    229224        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    230225       on the_trace: nat ≝
     
    250245definition compute_paid_trace_label_label ≝
    251246  λprog: labelled_object_code.
    252   let code_memory ≝ load_code_memory (oc prog) in
    253247  λtrace_ends_flag: trace_ends_with_ret.
    254   λstart_status: Status code_memory.
    255   λfinal_status: Status code_memory.
     248  λstart_status: Status (cm prog).
     249  λfinal_status: Status (cm prog).
    256250  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    257251  match the_trace with
     
    262256lemma trace_compute_paid_trace_cl_other:
    263257  ∀prog : labelled_object_code.
    264   let code_memory' ≝ load_code_memory (oc prog) in
    265258  ∀program_counter' : Word.
    266259  ∀program_size' : ℕ.
     
    268261  ∀instruction : instruction.
    269262  ∀program_counter'' : Word.
    270   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     263  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
    271264  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
    272   ∀start_status : (Status code_memory').
    273   ∀final_status : (Status code_memory').
     265  ∀start_status : (Status (cm prog)).
     266  ∀final_status : (Status (cm prog)).
    274267  ∀trace_ends_flag : trace_ends_with_ret.
    275268  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
     
    283276         ] 
    284277    then
    285       ∀start_status0:Status code_memory'.
    286       ∀final_status0:Status code_memory'.
     278      ∀start_status0:Status (cm prog).
     279      ∀final_status0:Status (cm prog).
    287280      ∀trace_ends_flag0:trace_ends_with_ret.
    288281      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
     
    341334          end_flag trace_any_label ? ?) try (>rewrite_assm %)
    342335        whd in match (current_instruction_cost … status_pre);
    343         cut(ticks = \snd (fetch (load_code_memory (oc prog))
    344            (program_counter … status_pre)))
     336        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre)))
    345337        [1,3:
    346338          <FETCH %
     
    384376          #Some_lookup_opt_assm <Some_lookup_opt_assm
    385377          normalize nodelta #new_recursive_assm >new_recursive_assm
    386           cut(ticks = \snd (fetch (load_code_memory (oc prog))
    387              (program_counter … status_start)))
     378          cut(ticks = \snd (fetch (cm prog) (program_counter … status_start)))
    388379          [1:
    389380            <FETCH %
     
    420411lemma trace_compute_paid_trace_cl_jump:
    421412  ∀prog: labelled_object_code.
    422   let code_memory' ≝ load_code_memory (oc prog) in
    423413  ∀program_counter': Word.
    424414  ∀first_time_around: bool.
     
    427417  ∀instruction: instruction.
    428418  ∀program_counter'': Word.
    429   ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
    430   ∀start_status: (Status code_memory').
    431   ∀final_status: (Status code_memory').
     419  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch (cm prog) program_counter'.
     420  ∀start_status: (Status (cm prog)).
     421  ∀final_status: (Status (cm prog)).
    432422  ∀trace_ends_flag: trace_ends_with_ret.
    433423  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
     
    436426    ticks
    437427     =compute_paid_trace_any_label … the_trace.
    438   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #first_time_around
     428  #prog #program_counter' #first_time_around
    439429  #program_size' #ticks #instruction #program_counter'' #FETCH
    440430  #start_status #final_status
     
    479469lemma trace_compute_paid_trace_cl_call:
    480470  ∀prog: labelled_object_code.
    481   let code_memory' ≝ load_code_memory (oc prog) in
    482471  ∀program_counter' : Word.
    483472  ∀program_size' : ℕ.
     
    485474  ∀instruction : instruction.
    486475  ∀program_counter'' : Word.
    487   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    488   ∀start_status : (Status code_memory').
    489   ∀final_status : (Status code_memory').
     476  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
     477  ∀start_status : (Status (cm prog)).
     478  ∀final_status : (Status (cm prog)).
    490479  ∀trace_ends_flag : trace_ends_with_ret.
    491480  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    496485  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
    497486      [None ⇒ true | Some _ ⇒ false] 
    498    then (∀start_status0:Status code_memory'
    499              .∀final_status0:Status code_memory'
     487   then (∀start_status0:Status (cm prog)
     488             .∀final_status0:Status (cm prog)
    500489              .∀trace_ends_flag0:trace_ends_with_ret
    501490               .∀the_trace0:trace_any_label
     
    511500   → ticks+pi1
    512501     =compute_paid_trace_any_label … the_trace).
    513   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
     502  #prog #program_counter' #program_size'
    514503  #ticks #instruction #program_counter'' #FETCH
    515504  #start_status #final_status #trace_ends_flag
     
    555544        #program_counter_assm >program_counter_assm <Some_lookup_opt
    556545        normalize nodelta #new_recursive_assm >new_recursive_assm
    557         cut(ticks = \snd (fetch code_memory' (program_counter … status_pre_fun_call)))
     546        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call)))
    558547        [1:
    559548          <FETCH %
     
    618607lemma trace_compute_paid_trace_cl_return:
    619608  ∀prog: labelled_object_code.
    620   let code_memory' ≝ load_code_memory (oc prog) in
    621609  ∀program_counter' : Word.
    622610  ∀program_size' : ℕ.
     
    624612  ∀instruction : instruction.
    625613  ∀program_counter'' : Word.
    626   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    627   ∀start_status : (Status code_memory').
    628   ∀final_status : (Status code_memory').
     614  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
     615  ∀start_status : (Status (cm prog)).
     616  ∀final_status : (Status (cm prog)).
    629617  ∀trace_ends_flag : trace_ends_with_ret.
    630618  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    633621    ticks
    634622     =compute_paid_trace_any_label … the_trace.
    635   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
     623  #prog #program_counter' #program_size'
    636624  #ticks #instruction #program_counter'' #FETCH
    637625  #start_status #final_status #trace_ends_flag
     
    686674lemma trace_any_label_length_leq_0_to_False:
    687675  ∀prog: labelled_object_code.
    688   let code_memory ≝ load_code_memory (oc prog) in
    689676  ∀trace_ends_flag: trace_ends_with_ret.
    690   ∀start_status: Status code_memory.
    691   ∀final_status: Status code_memory.
     677  ∀start_status: Status (cm prog).
     678  ∀final_status: Status (cm prog).
    692679  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    693680   trace_any_label_length … the_trace ≤ 0 → False.
     
    703690          Σcost_of_block: nat.
    704691          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
    705             ∀start_status,final_status: Status (load_code_memory (oc prog)).
     692            ∀start_status,final_status: Status (cm prog).
    706693            ∀trace_ends_flag.
    707694            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    711698          else
    712699            (cost_of_block = 0) ≝
    713   let code_memory' ≝ load_code_memory (oc prog) in
    714700  match program_size return λx. x = program_size → ? with
    715701  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
    716702  | S program_size' ⇒ λstep_case.
    717     let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (load_code_memory (oc prog)) program_counter' in
     703    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in
    718704    let to_continue ≝
    719705      match lookup_opt … program_counter' (costlabels prog) with
     
    727713          match real_instruction return λx. x = real_instruction →
    728714          Σcost_of_block: nat.
    729             ∀start_status,final_status: Status code_memory'.
     715            ∀start_status,final_status: Status (cm prog).
    730716            ∀trace_ends_flag.
    731717            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    770756          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
    771757          [ true ⇒
    772             ∀start_status: Status code_memory'.
    773             ∀final_status: Status code_memory'.
     758            ∀start_status: Status (cm prog).
     759            ∀final_status: Status (cm prog).
    774760            ∀trace_ends_flag.
    775761            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    832818    ∀program_counter': Word.
    833819      Σcost_of_block: nat.
    834         ∀start_status: Status (load_code_memory (oc prog)).
    835         ∀final_status: Status (load_code_memory (oc prog)).
     820        ∀start_status: Status (cm prog).
     821        ∀final_status: Status (cm prog).
    836822        ∀trace_ends_flag.
    837823        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
  • src/ASM/ASMCostsSplit.ma

    r2907 r2999  
    316316definition ASM_cost_map :
    317317  ∀p: labelled_object_code.
    318   let code_memory ≝ load_code_memory (oc p) in
    319318  let a_s ≝ OC_abstract_status p in
    320319  as_cost_map a_s ≝
  • src/ASM/Assembly.ma

    r2899 r2999  
    872872      〈(zero ?), [ ]〉)
    873873    in
     874     let code ≝ reverse … revcode in
    874875     mk_labelled_object_code
    875      (reverse … revcode)
     876     code (load_code_memory code) (refl …)
    876877     (fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??))
    877878     (foldl ??
  • src/ASM/CostsProof.ma

    r2907 r2999  
    1111  (prog: labelled_object_code)
    1212   (trace_ends_flag: trace_ends_with_ret)
    13     (start_status: Status (load_code_memory (oc prog)))
    14     (final_status: Status (load_code_memory (oc prog)))
     13    (start_status: Status (cm prog))
     14    (final_status: Status (cm prog))
    1515      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
     
    2222  (prog: labelled_object_code)
    2323  (trace_ends_flag: trace_ends_with_ret)
    24    (start_status: Status (load_code_memory (oc prog)))
    25    (final_status: Status (load_code_memory (oc prog)))
     24   (start_status: Status (cm prog))
     25   (final_status: Status (cm prog))
    2626     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
     
    5353and compute_max_trace_label_return_cost
    5454  (prog: labelled_object_code)
    55   (start_status: Status (load_code_memory (oc prog)))
    56   (final_status: Status (load_code_memory (oc prog)))
     55  (start_status: Status (cm prog))
     56  (final_status: Status (cm prog))
    5757    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    5858      on the_trace: nat ≝
     
    7070  (prog: labelled_object_code)
    7171   (trace_ends_flag: trace_ends_with_ret)
    72     (start_status: Status (load_code_memory (oc prog)))
    73     (final_status: Status (load_code_memory (oc prog)))
     72    (start_status: Status (cm prog))
     73    (final_status: Status (cm prog))
    7474      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    7575        start_status final_status) on the_trace:
    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) ≝ ?
     76          clock … (cm prog) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ?
    7777and compute_max_trace_any_label_cost_is_ok
    7878  (prog: labelled_object_code)
    7979  (trace_ends_flag: trace_ends_with_ret)
    80     (start_status: Status (load_code_memory (oc prog)))
    81     (final_status: Status (load_code_memory (oc prog)))
     80    (start_status: Status (cm prog))
     81    (final_status: Status (cm prog))
    8282     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    8383       on the_trace:
    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) ≝ ?
     84         clock … (cm prog) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ?
    8585and compute_max_trace_label_return_cost_is_ok
    8686  (prog: labelled_object_code)
    87     (start_status: Status (load_code_memory (oc prog)))
    88     (final_status: Status (load_code_memory (oc prog)))
     87    (start_status: Status (cm prog))
     88    (final_status: Status (cm prog))
    8989    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    9090      on the_trace:
    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 ≝ ?.
     91        clock … (cm prog) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (cm prog) … start_status ≝ ?.
    9292  [1:
    9393    cases the_trace
     
    127127      >(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 … (load_code_memory (oc prog)) status_start_fun_call);
     129      cases(is_next) in match (clock … (cm prog) status_start_fun_call);
    130130      >(execute_1_ok_clock … status_pre_fun_call)
    131131      <associative_plus in ⊢ (??%?);
     
    149149      >(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 … (load_code_memory (oc prog)) status_init);
     151      cases(is_next) in match (clock … (cm prog) status_init);
    152152      >(execute_1_ok_clock … status_pre)
    153153      >commutative_plus >associative_plus >associative_plus @eq_f
     
    175175  (prog:labelled_object_code)
    176176   (trace_ends_flag: trace_ends_with_ret)
    177     (start_status: Status (load_code_memory (oc prog)))
    178     (final_status: Status (load_code_memory (oc prog)))
     177    (start_status: Status (cm prog))
     178    (final_status: Status (cm prog))
    179179      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    180180        start_status final_status) on the_trace: nat ≝
     
    187187  (prog:labelled_object_code)
    188188  (trace_ends_flag: trace_ends_with_ret)
    189     (start_status: Status (load_code_memory (oc prog)))
    190     (final_status: Status (load_code_memory (oc prog)))
     189    (start_status: Status (cm prog))
     190    (final_status: Status (cm prog))
    191191     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    192192       on the_trace: nat ≝
     
    209209and compute_trace_label_return_cost_using_paid
    210210  (prog:labelled_object_code)
    211     (start_status: Status (load_code_memory (oc prog)))
    212     (final_status: Status (load_code_memory (oc prog)))
     211    (start_status: Status (cm prog))
     212    (final_status: Status (cm prog))
    213213    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    214214      on the_trace: nat ≝
     
    224224  (prog:labelled_object_code)
    225225   (trace_ends_flag: trace_ends_with_ret)
    226     (start_status: Status (load_code_memory (oc prog)))
    227     (final_status: Status (load_code_memory (oc prog)))
     226    (start_status: Status (cm prog))
     227    (final_status: Status (cm prog))
    228228      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    229229        start_status final_status) on the_trace:
     
    233233  (prog:labelled_object_code)
    234234  (trace_ends_flag: trace_ends_with_ret)
    235     (start_status: Status (load_code_memory (oc prog)))
    236     (final_status: Status (load_code_memory (oc prog)))
     235    (start_status: Status (cm prog))
     236    (final_status: Status (cm prog))
    237237     (the_trace: trace_any_label (OC_abstract_status prog)
    238238      trace_ends_flag start_status final_status) on the_trace:     
     
    242242and compute_trace_label_return_cost_using_paid_ok
    243243  (prog:labelled_object_code)
    244     (start_status: Status (load_code_memory (oc prog)))
    245     (final_status: Status (load_code_memory (oc prog)))
     244    (start_status: Status (cm prog))
     245    (final_status: Status (cm prog))
    246246    (the_trace: trace_label_return (OC_abstract_status prog)
    247247     start_status final_status) on the_trace:
     
    454454 (prog: labelled_object_code)
    455455 (cost_map: identifier_map CostTag nat)
    456  (initial: Status (load_code_memory (oc prog)))
    457  (final: Status (load_code_memory (oc prog)))
     456 (initial: Status (cm prog))
     457 (final: Status (cm prog))
    458458 (trace: trace_label_return (OC_abstract_status prog) initial final)
    459459 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     
    470470 (trace_ends_flag: trace_ends_with_ret)
    471471 (cost_map: identifier_map CostTag nat)
    472  (initial: Status (load_code_memory (oc prog)))
    473  (final: Status (load_code_memory (oc prog)))
     472 (initial: Status (cm prog))
     473 (final: Status (cm prog))
    474474 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
    475475 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     
    486486 (trace_ends_flag: trace_ends_with_ret)
    487487 (cost_map: identifier_map CostTag nat)
    488  (initial: Status (load_code_memory (oc prog)))
    489  (final: Status (load_code_memory (oc prog)))
     488 (initial: Status (cm prog))
     489 (final: Status (cm prog))
    490490 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
    491491 (unrepeating_witness: tll_unrepeating … trace)
     
    630630  ∀prog: labelled_object_code.
    631631  ∀cost_map: identifier_map CostTag nat.
    632   ∀initial: Status (load_code_memory (oc prog)).
    633   ∀final: Status (load_code_memory (oc prog)).
     632  ∀initial: Status (cm prog).
     633  ∀final: Status (cm prog).
    634634  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    635635  ∀unrepeating_witness: tlr_unrepeating … trace.
     
    638638      pi1 … (block_cost prog pc) = lookup_present … k_pres).
    639639        let ctrace ≝ flatten_trace_label_return … trace in
    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)).
     640          clock … (cm prog) … final =
     641            clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
    642642  #prog #cost_map
    643643  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
     
    648648theorem compute_max_trace_label_return_cost_ok_with_trace:
    649649  ∀prog: labelled_object_code.
    650   ∀initial: Status (load_code_memory (oc prog)).
    651   ∀final: Status (load_code_memory (oc prog)).
     650  ∀initial: Status (cm prog).
     651  ∀final: Status (cm prog).
    652652  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    653653  ∀unrepeating_witness: tlr_unrepeating … trace.
    654654    let cost_map ≝ traverse_code prog in
    655655    let ctrace ≝ flatten_trace_label_return … trace in
    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)).
     656      clock … (cm prog) … final = clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
    657657  [1:
    658658    #prog #initial #final #trace #unrepeating_witness
  • src/ASM/Fetch.ma

    r2770 r2999  
    173173definition code_memory_size ≝ bitvector_max_nat 16.
    174174
    175 include alias "ASM/BitVectorTrie.ma".
    176 include alias "ASM/Arithmetic.ma".
    177 
    178 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
    179   λpmem: BitVectorTrie Byte 16.
    180   λpc: Word.
    181     〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    182 
    183 definition load_code_memory0:
    184  ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185   let program_size ≝ |program| in
    186    program_size ≤ 2^16 →
    187     ∀pc. ∀pc_ok: pc < program_size.
    188      nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
    189 
    190  λprogram. \snd
    191   (foldl_strong ?
    192    (λprefix.
    193      Σres: nat × (BitVectorTrie Byte 16).
    194       let 〈i,mem〉 ≝ res in
    195       i = |prefix| ∧
    196       (i ≤ 2^16 →
    197         ∀pc. ∀pc_ok: pc < |prefix|.
    198          nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
    199    program
    200    (λprefix,v,tl,prf,i_mem.
    201      let 〈i,mem〉 ≝ i_mem in
    202       〈S i,insert … (bitvector_of_nat … i) v mem〉)
    203   〈0,Stub Byte 16〉).
    204 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
    205 | % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
    206 | cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
    207   [ >length_append >H1 normalize //
    208   | #LE #pc #pc_ok
    209     cases (le_to_or_lt_eq … pc_ok)
    210     [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
    211       [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
    212       #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
    213       <H1 <plus_n_O whd in ⊢ (???%); //
    214     | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
    215       >H2 [2: @(transitive_le … LE) //]
    216       cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
    217       whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
    218       #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
    219       @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
    220 qed.
    221 
    222 definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223  λprogram.load_code_memory0 program.
    224 
    225 lemma load_code_memory_ok:
    226  ∀program: object_code.
    227   let program_size ≝ |program| in
    228    program_size ≤ 2^16 →
    229     ∀pc. ∀pc_ok: pc < program_size.
    230      nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
    231 whd in match load_code_memory; normalize nodelta #program @pi2
    232 qed.
    233 
    234175lemma Prod_inv_rect_Type0:
    235176 ∀A,B. ∀P: A × B → Type[0].∀ab.
  • src/ASM/Interpret2.ma

    r2993 r2999  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
    41   let lcm ≝ load_code_memory … (oc c) in
    4241  mk_preclassified_system_of_abstract_status
    4342   labelled_object_code
    4443   (OC_abstract_status c)
    45    (λst. return (execute_1 lcm … st))
    46    (initialise_status … (load_code_memory (oc c))).
     44   (λst. return (execute_1 (cm c) … st))
     45   (initialise_status … (cm c)).
    4746
    4847(* Pre-classified system for ASM *)
Note: See TracChangeset for help on using the changeset viewer.