Changeset 1693


Ignore:
Timestamp:
Feb 14, 2012, 4:38:06 PM (8 years ago)
Author:
mulligan
Message:

Changes to ASMCosts and CostsProofs? files to get everything working again.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1692 r1693  
    13381338qed.
    13391339
    1340 definition block_cost ≝
     1340(*
     1341  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
     1342    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     1343      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
     1344        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
     1345          on program_size:
     1346          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
     1347          Σcost_of_block: nat.
     1348          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
     1349            ∀start_status: Status code_memory'.
     1350            ∀final_status: Status code_memory'.
     1351            ∀trace_ends_flag.
     1352            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     1353              program_counter' = program_counter … start_status →
     1354                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     1355                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     1356          else
     1357            (cost_of_block = 0)
     1358*)
     1359
     1360definition block_cost:
     1361    ∀code_memory': BitVectorTrie Byte 16.
     1362    ∀program_counter': Word.
     1363    ∀total_program_size: nat.
     1364    ∀cost_labels: BitVectorTrie costlabel 16.
     1365    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
     1366    ∀good_program_witness: good_program code_memory' total_program_size.
     1367      Σcost_of_block: nat.
     1368        ∀start_status: Status code_memory'.
     1369        ∀final_status: Status code_memory'.
     1370        ∀trace_ends_flag.
     1371        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     1372          program_counter' = program_counter … start_status →
     1373            (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     1374              cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
    13411375  λcode_memory: BitVectorTrie Byte 16.
    13421376  λprogram_counter: Word.
    … …  
    13441378  λcost_labels: BitVectorTrie costlabel 16.
    13451379  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    1346   λgood_program_witness: good_program code_memory total_program_size.
    1347     block_cost' code_memory program_counter total_program_size total_program_size cost_labels
    1348       reachable_program_counter_witness good_program_witness true ?.
    1349   @le_plus_n_r
     1380  λgood_program_witness: good_program code_memory total_program_size. ?.
     1381  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
     1382    reachable_program_counter_witness good_program_witness true ?)
     1383  [1:
     1384    #cost_of_block #block_cost_hyp
     1385    %{cost_of_block}
     1386    cases(lookup_opt … cost_labels) in block_cost_hyp;
     1387    [2: #cost_label] normalize nodelta
     1388    #hyp assumption
     1389  |2:
     1390    @le_plus_n_r
     1391  ]
    13501392qed.
    13511393

  • src/ASM/CostsProof.ma

    r1692 r1693  
    77include alias "basics/logic.ma".
    88
    9 definition current_instruction0 ≝
    10   λcode_memory: BitVectorTrie Byte 16.
    11   λprogram_counter: Word.
    12     \fst (\fst (fetch … code_memory program_counter)).
    13 
    14 definition current_instruction ≝
    15   λcm.
    16   λs: Status cm.
    17     current_instruction0 cm (program_counter … s).
    18 
    19 definition ASM_classify0: instruction → status_class ≝
    20   λi: instruction.
    21   match i with
    22    [ RealInstruction pre ⇒
    23      match pre with
    24       [ RET ⇒ cl_return
    25       | JZ _ ⇒ cl_jump
    26       | JNZ _ ⇒ cl_jump
    27       | JC _ ⇒ cl_jump
    28       | JNC _ ⇒ cl_jump
    29       | JB _ _ ⇒ cl_jump
    30       | JNB _ _ ⇒ cl_jump
    31       | JBC _ _ ⇒ cl_jump
    32       | CJNE _ _ ⇒ cl_jump
    33       | DJNZ _ _ ⇒ cl_jump
    34       | _ ⇒ cl_other
    35       ]
    36    | ACALL _ ⇒ cl_call
    37    | LCALL _ ⇒ cl_call
    38    | JMP _ ⇒ cl_call
    39    | AJMP _ ⇒ cl_jump
    40    | LJMP _ ⇒ cl_jump
    41    | SJMP _ ⇒ cl_jump
    42    | _ ⇒ cl_other
    43    ].
    44 
    45 definition ASM_classify: ∀cm. Status cm → status_class ≝
    46   λcm.
    47   λs: Status cm.
    48     ASM_classify0 (current_instruction cm s).
    49 
    50 definition current_instruction_is_labelled ≝
    51   λcm.
    52   λcost_labels: BitVectorTrie costlabel 16.
    53   λs: Status cm.
    54   let pc ≝ program_counter ? cm s in
    55     match lookup_opt … pc cost_labels with
    56     [ None ⇒ False
    57     | _    ⇒ True
    58     ].
    59 
    60 definition next_instruction_properly_relates_program_counters ≝
    61   λcm.
    62   λbefore: Status cm.
    63   λafter : Status cm.
    64   let size ≝ current_instruction_cost cm before in
    65   let pc_before ≝ program_counter … cm before in
    66   let pc_after ≝ program_counter … cm after in
    67   let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    68     sum = pc_after.
    69 
    70 definition ASM_abstract_status: ∀cm. BitVectorTrie costlabel 16 → abstract_status ≝
    71   λcm.
    72   λcost_labels.
    73   mk_abstract_status
    74    (Status cm)
    75    (λs,s'. (execute_1 cm s) = s')
    76    (λs,class. ASM_classify cm s = class)
    77    (current_instruction_is_labelled cm cost_labels)
    78    (next_instruction_properly_relates_program_counters cm).
    79 
    809let rec compute_max_trace_label_label_cost
    8110  (cm: ?)
    … …  
    9726       on the_trace: nat ≝
    9827  match the_trace with
    99   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
    100   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     28  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost cm the_status
     29  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost cm the_status
    10130  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    10231      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
    … …  
    10736      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
    10837      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    109       let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
     38      let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in
    11039        call_trace_cost + current_instruction_cost + final_trace_cost
    11140  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    11241      let current_instruction_cost ≝ current_instruction_cost cm status_pre in
    11342      let tail_trace_cost ≝
    114        compute_max_trace_any_label_cost cost_labels end_flag
     43       compute_max_trace_any_label_cost cm cost_labels end_flag
    11544        status_init status_end tail_trace
    11645      in
    … …  
    13463
    13564let rec compute_max_trace_label_label_cost_is_ok
     65  (cm: ?)
    13666  (cost_labels: BitVectorTrie costlabel 16)
    13767   (trace_ends_flag: trace_ends_with_ret)
    138     (start_status: Status) (final_status: Status)
    139       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     68    (start_status: Status cm) (final_status: Status cm)
     69      (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    14070        start_status final_status) on the_trace:
    141           clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
     71          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) ≝ ?
    14272and compute_max_trace_any_label_cost_is_ok
     73  (cm: ?)
    14374  (cost_labels: BitVectorTrie costlabel 16)
    14475  (trace_ends_flag: trace_ends_with_ret)
    145    (start_status: Status) (final_status: Status)
    146      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     76   (start_status: Status cm) (final_status: Status cm)
     77     (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    14778       on the_trace:
    148          clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
     79         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) ≝ ?
    14980and compute_max_trace_label_return_cost_is_ok
    150   (cost_labels: BitVectorTrie costlabel 16)
    151   (start_status: Status) (final_status: Status)
    152     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     81  (cm: ?)
     82  (cost_labels: BitVectorTrie costlabel 16)
     83  (start_status: Status cm) (final_status: Status cm)
     84    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    15385      on the_trace:
    154         clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock … start_status ≝ ?.
     86        clock … cm … final_status = (compute_max_trace_label_return_cost cm cost_labels start_status final_status the_trace) + clock … cm … start_status ≝ ?.
    15587  [1:
    15688    cases the_trace
    … …  
    16193    [1,2:
    16294      #start_status #final_status #is_next #is_not_return try (#is_costed)
    163       change with (current_instruction_cost start_status) in ⊢ (???(?%?));
     95      change with (current_instruction_cost cm start_status) in ⊢ (???(?%?));
    16496      cases(is_next) @execute_1_ok
    16597    |3:
     98      #status_pre_fun_call #status_start_fun_call #status_final #is_next
     99      #classifier_assm #after_return_assm #call_trace #costed_assm
     100      whd in match (compute_max_trace_any_label_cost … (tal_base_call …));
     101      >(compute_max_trace_label_return_cost_is_ok … call_trace)
     102      >associative_plus @eq_f cases(is_next)
     103      >execute_1_ok %
     104    |4:
    166105      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    167       #status_final #is_next #is_call #is_after_return #call_trace #final_trace
     106      #status_final #is_next #is_call #is_after_return #call_trace #not_costed #final_trace
    168107      change with (
    169       let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
    170       let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    171       let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
     108      let current_instruction_cost ≝ current_instruction_cost cm status_pre_fun_call in
     109      let call_trace_cost ≝ compute_max_trace_label_return_cost cm … call_trace in
     110      let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in
    172111        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
    173112      normalize nodelta;
    174       >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
     113      >(compute_max_trace_any_label_cost_is_ok … cost_labels end_flag status_after_fun_call
    175114          status_final final_trace)
    176       >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
     115      >(compute_max_trace_label_return_cost_is_ok … cost_labels status_start_fun_call
    177116        status_after_fun_call call_trace)
    178       cases(is_next) in match (clock … status_start_fun_call);
    179       >(execute_1_ok status_pre_fun_call)
     117      cases(is_next) in match (clock … cm status_start_fun_call);
     118      >(execute_1_ok … status_pre_fun_call)
    180119      <associative_plus in ⊢ (??%?);
    181120      <commutative_plus in match (
    182         compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
    183           + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace);
    184       >associative_plus in ⊢ (??%?);
    185       <commutative_plus in match (
    186         compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
    187           + (current_instruction_cost status_pre_fun_call
    188               + clock (BitVectorTrie Byte 16) status_pre_fun_call));
    189       >associative_plus in ⊢ (??%?);
    190       <commutative_plus in match (
    191          clock (BitVectorTrie Byte 16) status_pre_fun_call
    192            + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace);
    193       <(associative_plus (
    194          (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace)))
    195       <associative_plus in ⊢ (??%?); %
    196     |4:
     121        compute_max_trace_any_label_cost cm cost_labels end_flag status_after_fun_call status_final final_trace
     122          + compute_max_trace_label_return_cost cm cost_labels status_start_fun_call status_after_fun_call call_trace);
     123      >associative_plus in ⊢ (??%?); >associative_plus in ⊢ (???%); >associative_plus in ⊢ (???%);
     124      @eq_f >commutative_plus in ⊢ (??%?); >associative_plus in ⊢ (??%?);
     125      @eq_f @commutative_plus
     126    |5:
    197127      #end_flag #status_pre #status_init #status_end #is_next
    198128      #trace_any_label #is_other #is_not_costed
    199129      change with (
    200       let current_instruction_cost ≝ current_instruction_cost status_pre in
     130      let current_instruction_cost ≝ current_instruction_cost cm status_pre in
    201131      let tail_trace_cost ≝
    202        compute_max_trace_any_label_cost cost_labels end_flag
     132       compute_max_trace_any_label_cost cm cost_labels end_flag
    203133        status_init status_end trace_any_label
    204134      in
    205135        current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?));
    206136      normalize nodelta;
    207       >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
     137      >(compute_max_trace_any_label_cost_is_ok cm cost_labels end_flag
    208138         status_init status_end trace_any_label)
    209       cases(is_next) in match (clock … status_init);
    210       >(execute_1_ok status_pre)
     139      cases(is_next) in match (clock … cm status_init);
     140      >(execute_1_ok cm status_pre)
    211141      >commutative_plus >associative_plus >associative_plus @eq_f
    212142      @commutative_plus
    … …  
    220150      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
    221151      normalize
    222       >(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
    223       >(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     152      >(compute_max_trace_label_return_cost_is_ok cm cost_labels status_labelled status_final ret_trace);
     153      >(compute_max_trace_label_label_cost_is_ok cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
    224154      <associative_plus in ⊢ (??%?);
    225155      >commutative_plus in match (
    226         compute_max_trace_label_return_cost cost_labels status_labelled status_final ret_trace
    227           + compute_max_trace_label_label_cost cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     156        compute_max_trace_label_return_cost cm cost_labels status_labelled status_final ret_trace
     157          + compute_max_trace_label_label_cost cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
    228158      %
    229159    ]
    230   ].
    231 qed.
    232 
    233 (* XXX: work below here: *)
    234 
    235 let rec compute_paid_trace_any_label
     160  ]
     161qed.
     162
     163let rec compute_trace_label_label_cost_using_paid
     164  (cm: ?)
     165  (cost_labels: BitVectorTrie costlabel 16)
     166   (trace_ends_flag: trace_ends_with_ret)
     167    (start_status: Status cm) (final_status: Status cm)
     168      (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     169        start_status final_status) on the_trace: nat ≝
     170  match the_trace with
     171  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     172      compute_paid_trace_label_label cm cost_labels … the_trace +
     173      compute_trace_any_label_cost_using_paid … given_trace
     174  ]
     175and compute_trace_any_label_cost_using_paid
     176  (cm: ?)
    236177  (cost_labels: BitVectorTrie costlabel 16)
    237178  (trace_ends_flag: trace_ends_with_ret)
    238    (start_status: Status) (final_status: Status)
    239      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    240        on the_trace: nat ≝
    241   match the_trace with
    242   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
    243   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
    244   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    245      _ _ _ call_trace final_trace ⇒
    246       let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    247       let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
    248         current_instruction_cost + final_trace_cost
    249   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    250       let current_instruction_cost ≝ current_instruction_cost status_pre in
    251       let tail_trace_cost ≝
    252        compute_paid_trace_any_label cost_labels end_flag
    253         status_init status_end tail_trace
    254       in
    255         current_instruction_cost + tail_trace_cost
    256   ].
    257 
    258 definition compute_paid_trace_label_label ≝
    259  λcost_labels: BitVectorTrie costlabel 16.
    260   λtrace_ends_flag: trace_ends_with_ret.
    261    λstart_status: Status.
    262     λfinal_status: Status.
    263      λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    264       start_status final_status.
    265   match the_trace with
    266   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    267       compute_paid_trace_any_label … given_trace
    268   ].
    269 
    270 let rec compute_trace_label_label_cost_using_paid
    271   (cost_labels: BitVectorTrie costlabel 16)
    272    (trace_ends_flag: trace_ends_with_ret)
    273     (start_status: Status) (final_status: Status)
    274       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    275         start_status final_status) on the_trace: nat ≝
    276   match the_trace with
    277   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    278       compute_paid_trace_label_label cost_labels … the_trace +
    279       compute_trace_any_label_cost_using_paid … given_trace
    280   ]
    281 and compute_trace_any_label_cost_using_paid
    282   (cost_labels: BitVectorTrie costlabel 16)
    283   (trace_ends_flag: trace_ends_with_ret)
    284    (start_status: Status) (final_status: Status)
    285      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     179   (start_status: Status cm) (final_status: Status cm)
     180     (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    286181       on the_trace: nat ≝
    287182  match the_trace with
    288183  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
    289184  | tal_base_return the_status _ _ _ ⇒ 0
     185  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     186      compute_trace_label_return_cost_using_paid … call_trace
    290187  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    291      _ _ _ call_trace final_trace ⇒
     188     _ _ _ call_trace _ final_trace ⇒
    292189      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
    293       let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cost_labels end_flag … final_trace in
     190      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cm cost_labels end_flag … final_trace in
    294191        call_trace_cost + final_trace_cost
    295192  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    296      compute_trace_any_label_cost_using_paid cost_labels end_flag
     193     compute_trace_any_label_cost_using_paid cm cost_labels end_flag
    297194      status_init status_end tail_trace
    298195  ]
    299196and compute_trace_label_return_cost_using_paid
    300   (cost_labels: BitVectorTrie costlabel 16)
    301   (start_status: Status) (final_status: Status)
    302     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     197  (cm: ?)
     198  (cost_labels: BitVectorTrie costlabel 16)
     199  (start_status: Status cm) (final_status: Status cm)
     200    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    303201      on the_trace: nat ≝
    304202  match the_trace with
    … …  
    311209
    312210let rec compute_trace_label_label_cost_using_paid_ok
     211  (cm: ?)
    313212  (cost_labels: BitVectorTrie costlabel 16)
    314213   (trace_ends_flag: trace_ends_with_ret)
    315     (start_status: Status) (final_status: Status)
    316       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     214    (start_status: Status cm) (final_status: Status cm)
     215      (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    317216        start_status final_status) on the_trace:
    318  compute_trace_label_label_cost_using_paid cost_labels … the_trace =
     217 compute_trace_label_label_cost_using_paid cm cost_labels … the_trace =
    319218 compute_max_trace_label_label_cost … the_trace ≝ ?
    320219and compute_trace_any_label_cost_using_paid_ok
     220  (cm: ?)
    321221  (cost_labels: BitVectorTrie costlabel 16)
    322222  (trace_ends_flag: trace_ends_with_ret)
    323    (start_status: Status) (final_status: Status)
    324      (the_trace: trace_any_label (ASM_abstract_status cost_labels)
     223   (start_status: Status cm) (final_status: Status cm)
     224     (the_trace: trace_any_label (ASM_abstract_status cm cost_labels)
    325225      trace_ends_flag start_status final_status) on the_trace:     
    326   compute_paid_trace_any_label cost_labels trace_ends_flag … the_trace
    327   +compute_trace_any_label_cost_using_paid cost_labels trace_ends_flag … the_trace
    328   =compute_max_trace_any_label_cost cost_labels trace_ends_flag … the_trace ≝ ?
     226  compute_paid_trace_any_label cm cost_labels trace_ends_flag … the_trace
     227  +compute_trace_any_label_cost_using_paid cm cost_labels trace_ends_flag … the_trace
     228  =compute_max_trace_any_label_cost cm cost_labels trace_ends_flag … the_trace ≝ ?
    329229and compute_trace_label_return_cost_using_paid_ok
    330   (cost_labels: BitVectorTrie costlabel 16)
    331   (start_status: Status) (final_status: Status)
    332     (the_trace: trace_label_return (ASM_abstract_status cost_labels)
     230  (cm: ?)
     231  (cost_labels: BitVectorTrie costlabel 16)
     232  (start_status: Status cm) (final_status: Status cm)
     233    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels)
    333234     start_status final_status) on the_trace:
    334  compute_trace_label_return_cost_using_paid cost_labels … the_trace =
    335  compute_max_trace_label_return_cost cost_labels … the_trace ≝ ?.
     235 compute_trace_label_return_cost_using_paid cm cost_labels … the_trace =
     236 compute_max_trace_label_return_cost cm cost_labels … the_trace ≝ ?.
    336237[ cases the_trace #endsf #ss #es #tr #H normalize
    337238  @compute_trace_any_label_cost_using_paid_ok
    … …  
    339240  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
    340241  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
    341   | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%);
     242  |
     243    #sp #ss #sf #H1 #H2 #tr1 #tr2 #H3
     244    whd in ⊢ (???%); whd in ⊢ (??(??%)?); whd in ⊢ (??(?%?)?);
     245    >compute_trace_label_return_cost_using_paid_ok in ⊢ (??%?);
     246    >commutative_plus in ⊢ (??%?); @eq_f %
     247  | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #H4 #tr2 whd in ⊢ (??(?%%)%);
    342248    <compute_trace_any_label_cost_using_paid_ok
    343249    <compute_trace_label_return_cost_using_paid_ok
    … …  
    374280*)
    375281
     282include alias "ASM/BitVectorTrie.ma".
     283
    376284let rec compute_cost_trace_label_label
     285  (cm: BitVectorTrie Byte 16)
    377286  (cost_labels: BitVectorTrie costlabel 16)
    378287   (trace_ends_flag: trace_ends_with_ret)
    379     (start_status: Status) (final_status: Status)
    380       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     288    (start_status: Status cm) (final_status: Status cm)
     289      (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    381290        start_status final_status) on the_trace:
    382          list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
     291         list (Σk:costlabel. ∃pc: Word. lookup_opt … pc cost_labels = Some … k) ≝
    383292  match the_trace with
    384293  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    385      let pc ≝ program_counter … initial in
     294     let pc ≝ program_counter ? cm initial in
    386295     let label ≝
    387       match lookup_opt … pc cost_labels return λx. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
     296      match lookup_opt … pc cost_labels return λx: option ?. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
    388297      [ None ⇒ λabs. ⊥
    389298      | Some l ⇒ λ_. l ] labelled_proof in
    390      (mk_Sig … label ?)::compute_cost_trace_any_label … given_trace
     299      (mk_Sig ?? label ?)::compute_cost_trace_any_label cm cost_labels ends_flag initial final … given_trace
    391300  ]
    392301and compute_cost_trace_any_label
     302  (cm: BitVectorTrie Byte 16)
    393303  (cost_labels: BitVectorTrie costlabel 16)
    394304  (trace_ends_flag: trace_ends_with_ret)
    395    (start_status: Status) (final_status: Status)
    396      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     305   (start_status: Status cm) (final_status: Status cm)
     306     (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    397307       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    398308  match the_trace with
    399   [ tal_base_not_return the_status _ _ _ _ ⇒ []
    400   | tal_base_return the_status _ _ _ ⇒ []
     309  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
     310  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     311      compute_cost_trace_label_return … call_trace
     312  | tal_base_return the_status _ _ _ ⇒ [ ]
    401313  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    402      _ _ _ call_trace final_trace ⇒
     314     _ _ _ call_trace _ final_trace ⇒
    403315      let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
    404       let final_cost_trace ≝ compute_cost_trace_any_label cost_labels end_flag … final_trace in
     316      let final_cost_trace ≝ compute_cost_trace_any_label cm cost_labels end_flag … final_trace in
    405317        call_cost_trace @ final_cost_trace
    406318  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    407        compute_cost_trace_any_label cost_labels end_flag
     319       compute_cost_trace_any_label cm cost_labels end_flag
    408320        status_init status_end tail_trace
    409321  ]
    410322and compute_cost_trace_label_return
    411   (cost_labels: BitVectorTrie costlabel 16)
    412   (start_status: Status) (final_status: Status)
    413     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     323  (cm: BitVectorTrie Byte 16)
     324  (cost_labels: BitVectorTrie costlabel 16)
     325  (start_status: Status cm) (final_status: Status cm)
     326    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    414327      on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    415328  match the_trace with
    416   [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
     329  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label cm … trace_to_lift
    417330  | tlr_step initial labelled final labelled_trace ret_trace ⇒
    418       let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in
    419       let return_cost ≝ compute_cost_trace_label_return … ret_trace in
     331      let labelled_cost ≝ compute_cost_trace_label_label cm … labelled_trace in
     332      let return_cost ≝ compute_cost_trace_label_return cm … ret_trace in
    420333        labelled_cost @ return_cost
    421334  ].
    … …  
    425338 | // ]
    426339qed.
    427 
    428 (* XXX: zero in base cases (where the trace is a singleton transition) because
    429         we are counting until one from end
    430 *)
    431 let rec trace_any_label_length
    432   (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
    433     (start_status: Status) (final_status: Status)
    434       (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    435         on the_trace: nat ≝
    436   match the_trace with
    437   [ tal_base_not_return the_status _ _ _ _ ⇒ 0
    438   | tal_base_return the_status _ _ _ ⇒ 0
    439   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒
    440       let tail_length ≝ trace_any_label_length … final_trace in
    441       let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
    442         pc_difference + tail_length
    443   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    444       let tail_length ≝ trace_any_label_length … tail_trace in
    445       let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
    446         pc_difference + tail_length       
    447   ].
    448340
    449341(* XXX: commented out in favour of above
    … …  
    586478  ]
    587479qed.
    588    
    589 let rec block_cost_trace_any_label_static_dynamic_ok
    590   (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    591     (trace_ends_flag: ?) (start_status: Status) (final_status: Status)
    592       (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    593         on the_trace:
    594           let code_memory ≝ code_memory … start_status in
    595           let program_counter ≝ program_counter … start_status in
    596             ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
    597             ∀good_program_witness: good_program code_memory total_program_size.
    598               (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
    599                 block_cost code_memory program_counter total_program_size cost_labels reachable_program_counter_witness good_program_witness =
    600                   compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝ ?.
    601     letin code_memory ≝ (code_memory … start_status)
    602     letin program_counter ≝ (program_counter … start_status)
    603     #reachable_program_counter_witness #good_program_witness
    604     generalize in match (refl … final_status);
    605     generalize in match (refl … start_status);
    606     cases the_trace in ⊢ (???% → ???% → %);
    607     [1:
    608       #start_status' #final_status' #execute_hyp #classifier_hyp #costed_hyp
    609       #start_status_refl #final_status_refl destruct
    610       whd in match (trace_any_label_length ? ? ? ? ?);
    611       whd in match (compute_paid_trace_any_label ? ? ? ? ?);
    612       @and_intro_right
    613       [1:
    614         generalize in match reachable_program_counter_witness;
    615         whd in match (reachable_program_counter code_memory total_program_size program_counter);
    616         * #irrelevant #relevant
    617         lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)
    618         #hyp assumption
    619       |2:
    620         * #n #trace_length_hyp
    621         whd in match block_cost; normalize nodelta
    622         generalize in match reachable_program_counter_witness;
    623         generalize in match good_program_witness;
    624         <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
    625         -reachable_program_counter_witness #reachable_program_counter_witness
    626         -good_program_witness #good_program_witness
    627         whd in ⊢ (??%?); @pair_elim
    628       ]
    629     |2:
    630       #start_status' #final_status' #execute_hyp #classified_hyp
    631       #start_status_refl #final_status_refl destruct
    632       whd in match (trace_any_label_length ? ? ? ? ?);
    633       whd in match (compute_paid_trace_any_label ? ? ? ? ?);
    634       @and_intro_right
    635       [1:
    636         generalize in match reachable_program_counter_witness;
    637         whd in match (reachable_program_counter code_memory total_program_size program_counter);
    638         * #irrelevant #relevant
    639         lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)
    640         #hyp assumption
    641       |2:
    642         * #n #trace_length_hyp
    643         whd in match block_cost; normalize nodelta
    644         generalize in match reachable_program_counter_witness;
    645         generalize in match good_program_witness;
    646         <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
    647         -reachable_program_counter_witness #reachable_program_counter_witness
    648         -good_program_witness #good_program_witness
    649         whd in match (0 + S n); whd in ⊢ (??%?);
    650       ]
    651     |3:
    652       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    653       #status_final #execute_hyp #classifier_hyp #after_return_hyp
    654       #trace_label_return #trace_any_label #start_status_refl #final_status_refl
    655       destruct
    656       whd in match (trace_any_label_length ? ? ? ? ?);
    657       whd in match (compute_paid_trace_any_label ? ? ? ? ?);
    658       @and_intro_right
    659       [1:
    660       |2:
    661       ]
    662     |4:
    663       #end_flag #status_pre #status_init #status_end #execute_hyp #trace_any_label
    664       #classifier_hyp #costed_hyp #start_status_refl #final_status_refl
    665       destruct
    666       whd in match (trace_any_label_length ? ? ? ? ?);
    667       whd in match (compute_paid_trace_any_label ? ? ? ? ?);
    668       @and_intro_right
    669       [1:
    670       |2:
    671       ]
    672     ]
    673   ]
    674  
    675 corollary block_cost_trace_label_labelstatic_dynamic_ok:
    676   ∀program_size: nat.
    677   ∀cost_labels: BitVectorTrie costlabel 16.
    678   ∀trace_ends_flag.
    679   ∀start_status: Status.
    680   ∀final_status: Status.
    681   ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    682   let code_memory ≝ code_memory … start_status in
    683   let program_counter ≝ program_counter … start_status in
    684   ∀reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter.
    685   ∀good_program_witness: good_program code_memory program_size.
    686     (∃n: nat. trace_length start_status final_status + n = program_size) ∧
    687       block_cost code_memory program_counter program_size program_size cost_labels reachable_program_counter_witness good_program_witness ? =
    688         compute_paid_trace_label_label cost_labels trace_ends_flag start_status final_status the_trace.
    689   [2:
    690     @le_plus_n_r
    691   |1:
    692     #program_size #cost_labels #trace_ends_flag #start_status #final_status
    693     #the_trace normalize nodelta
    694     #reachable_program_counter_witness #good_program_witness
    695     generalize in match start_status;
    696 qed.
    697480
    698481(*
    … …  
    703486*)
    704487
     488include alias "arithmetics/bigops.ma".
     489
    705490(* This shoudl go in bigops! *)
    706491theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B.
    707492 \big[op,nil]_{i<k1+k2|p i} (f i) =
    708493 op \big[op,nil]_{i<k2|p (i+k1)} (f (i+k1)) \big[op,nil]_{i<k1|p i} (f i).
    709  #k1 #k2 #p #B #nil #op #f >bigop_sum >commutative_plus @same_bigop #i @leb_elim normalize
     494 #k1 #k2 #p #B #nil #op #f >bigop_sum
     495 >commutative_plus @same_bigop #i @leb_elim normalize
    710496 [2,4: //
    711497 | #H1 #H2 <plus_minus_m_m //
    … …  
    751537  with precedence 20
    752538for @{'bigop $n plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f)}.
    753 
    754 axiom code_memory_ro_label_label:
    755  ∀cost_labels. ∀ends_flag.
    756  ∀initial,final. trace_label_label (ASM_abstract_status cost_labels) ends_flag initial final →
    757   code_memory … initial = code_memory … final.
    758 
    759 (*
    760 axiom code_memory_ro_label_return:
    761  ∀cost_labels.
    762  ∀initial,final. trace_label_return (ASM_abstract_status cost_labels) initial final →
    763   code_memory … initial = code_memory … final.
    764 *)
    765539
    766540definition tech_cost_of_label0:
    … …  
    870644
    871645let rec compute_max_trace_label_return_cost_ok_with_trace
     646 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
    872647 (cost_labels: BitVectorTrie costlabel 16)
    873648 (cost_map: identifier_map CostTag nat)
    874  (initial: Status) (final: Status)
    875  (trace: trace_label_return (ASM_abstract_status cost_labels) initial final)
     649 (initial: Status cm) (final: Status cm)
     650 (trace: trace_label_return (ASM_abstract_status cm cost_labels) initial final)
    876651 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    877652 on trace:
    878653 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    879    block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres).
    880   let ctrace ≝ compute_cost_trace_label_return … trace in
    881   compute_max_trace_label_return_cost … trace =
     654   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
     655   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     656  let ctrace ≝ compute_cost_trace_label_return cm … trace in
     657  compute_max_trace_label_return_cost cm … trace =
    882658   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    883659    ≝ ?
    884660and compute_max_trace_label_label_cost_ok_with_trace
     661 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
    885662 (cost_labels: BitVectorTrie costlabel 16)
    886663 (trace_ends_flag: trace_ends_with_ret)
    887664 (cost_map: identifier_map CostTag nat)
    888  (initial: Status) (final: Status)
    889  (trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag initial final)
     665 (initial: Status cm) (final: Status cm)
     666 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
    890667 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    891668 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    892    block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres))
     669   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
     670   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
    893671 on trace:
    894672  let ctrace ≝ compute_cost_trace_label_label … trace in
    … …  
    896674   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    897675    ≝ ?.
    898 cases trace
    899 [ #sb #sa #tr #dom_codom
    900   @compute_max_trace_label_label_cost_ok_with_trace @dom_codom
    901 | #si #sl #sf #tr1 #tr2 #dom_codom whd in ⊢ (let ctrace ≝ % in ??%?);
    902   change with (let ctrace ≝ ? in ? = bigop (|? @ ?|) ?????)
    903   >append_length in ⊢ (let ctrace ≝ ? in ???(?%?????));
    904   change with (?=?) >bigop_sum_rev >commutative_plus @eq_f2
    905   [ >(compute_max_trace_label_return_cost_ok_with_trace … cost_map … codom_dom)
    906     -compute_max_trace_label_return_cost_ok_with_trace     
    907     [2:lapply (code_memory_ro_label_label … tr1) #E2 <E2 @dom_codom]
     676cases trace normalize nodelta
     677[ #sb #sa #tr #dom_codom whd in ⊢ (??%?);
     678  whd in match (compute_cost_trace_label_return ?????);
     679  @(compute_max_trace_label_label_cost_ok_with_trace … good_program_witness) @dom_codom
     680| #si #sl #sf #tr1 #tr2 #dom_codom
     681  whd in ⊢ (??%?);
     682  whd in match (compute_cost_trace_label_return ?????);
     683  >append_length >bigop_sum_rev >commutative_plus @eq_f2
     684  [ >(compute_max_trace_label_return_cost_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     685    -compute_max_trace_label_return_cost_ok_with_trace
    908686    @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
    909   | >(compute_max_trace_label_label_cost_ok_with_trace … cost_map … codom_dom … dom_codom)
     687  | >(compute_max_trace_label_label_cost_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     688    -compute_max_trace_label_return_cost_ok_with_trace
    910689    @same_bigop [//] #i #H #_
    911690]
Note: See TracChangeset for help on using the changeset viewer.