Changeset 1554


Ignore:
Timestamp:
Nov 24, 2011, 4:49:15 PM (8 years ago)
Author:
sacerdot
Message:

Major progress in the proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1549 r1554  
    3636
    3737definition current_instruction_is_labelled ≝
    38   λcost_labels: BitVectorTrie Byte 16.
     38  λcost_labels: BitVectorTrie costlabel 16.
    3939  λs: Status.
    4040  let pc ≝ program_counter … s in
     
    4242    [ None ⇒ False
    4343    | _    ⇒ True
     44    ].
     45
     46definition label_of_current_instruction:
     47 BitVectorTrie costlabel 16 → Status → list costlabel
     48 ≝
     49  λcost_labels,s.
     50  let pc ≝ program_counter … s in
     51    match lookup_opt … pc cost_labels with
     52    [ None ⇒ []
     53    | Some l ⇒ [l]
    4454    ].
    4555
     
    5363    sum = pc_after.
    5464
    55 definition ASM_abstract_status: BitVectorTrie Byte 16 → abstract_status ≝
     65definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
    5666 λcost_labels.
    5767  mk_abstract_status
     
    203213
    204214let rec compute_max_trace_label_label_cost
    205   (cost_labels: BitVectorTrie Byte 16)
     215  (cost_labels: BitVectorTrie costlabel 16)
    206216   (trace_ends_flag: trace_ends_with_ret)
    207217    (start_status: Status) (final_status: Status)
     
    213223  ]
    214224and compute_max_trace_any_label_cost
    215   (cost_labels: BitVectorTrie Byte 16)
     225  (cost_labels: BitVectorTrie costlabel 16)
    216226  (trace_ends_flag: trace_ends_with_ret)
    217227   (start_status: Status) (final_status: Status)
     
    236246  ]
    237247and compute_max_trace_label_return_cost
    238   (cost_labels: BitVectorTrie Byte 16)
     248  (cost_labels: BitVectorTrie costlabel 16)
    239249  (start_status: Status) (final_status: Status)
    240250    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     
    305315qed.*)
    306316
     317(*
    307318let rec compute_max_trace_label_label_cost_is_ok
    308319  (cost_labels: BitVectorTrie Byte 16)
     
    344355    ]
    345356  ].
     357*)
     358
     359(* XXX: work below here: *)
     360
     361let rec compute_paid_trace_any_label
     362  (cost_labels: BitVectorTrie costlabel 16)
     363  (trace_ends_flag: trace_ends_with_ret)
     364   (start_status: Status) (final_status: Status)
     365     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     366       on the_trace: nat ≝
     367  match the_trace with
     368  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
     369  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     370  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     371     _ _ _ call_trace final_trace ⇒
     372      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     373      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
     374        current_instruction_cost + final_trace_cost
     375  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     376      let current_instruction_cost ≝ current_instruction_cost status_pre in
     377      let tail_trace_cost ≝
     378       compute_paid_trace_any_label cost_labels end_flag
     379        status_init status_end tail_trace
     380      in
     381        current_instruction_cost + tail_trace_cost
     382  ].
     383
     384definition compute_paid_trace_label_label ≝
     385 λcost_labels: BitVectorTrie costlabel 16.
     386  λtrace_ends_flag: trace_ends_with_ret.
     387   λstart_status: Status.
     388    λfinal_status: Status.
     389     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     390      start_status final_status.
     391  match the_trace with
     392  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     393      compute_paid_trace_any_label … given_trace
     394  ].
     395
     396let rec compute_trace_label_label_cost_using_paid
     397  (cost_labels: BitVectorTrie costlabel 16)
     398   (trace_ends_flag: trace_ends_with_ret)
     399    (start_status: Status) (final_status: Status)
     400      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     401        start_status final_status) on the_trace: nat ≝
     402  match the_trace with
     403  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     404      compute_paid_trace_label_label cost_labels … the_trace +
     405      compute_trace_any_label_cost_using_paid … given_trace
     406  ]
     407and compute_trace_any_label_cost_using_paid
     408  (cost_labels: BitVectorTrie costlabel 16)
     409  (trace_ends_flag: trace_ends_with_ret)
     410   (start_status: Status) (final_status: Status)
     411     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     412       on the_trace: nat ≝
     413  match the_trace with
     414  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
     415  | tal_base_return the_status _ _ _ ⇒ 0
     416  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     417     _ _ _ call_trace final_trace ⇒
     418      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
     419      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cost_labels end_flag … final_trace in
     420        call_trace_cost + final_trace_cost
     421  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     422     compute_trace_any_label_cost_using_paid cost_labels end_flag
     423      status_init status_end tail_trace
     424  ]
     425and compute_trace_label_return_cost_using_paid
     426  (cost_labels: BitVectorTrie costlabel 16)
     427  (start_status: Status) (final_status: Status)
     428    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     429      on the_trace: nat ≝
     430  match the_trace with
     431  [ tlr_base before after trace_to_lift ⇒ compute_trace_label_label_cost_using_paid … trace_to_lift
     432  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     433      let labelled_cost ≝ compute_trace_label_label_cost_using_paid … labelled_trace in
     434      let return_cost ≝ compute_trace_label_return_cost_using_paid … ret_trace in
     435        labelled_cost + return_cost
     436  ].
     437
     438let rec compute_trace_label_label_cost_using_paid_ok
     439  (cost_labels: BitVectorTrie costlabel 16)
     440   (trace_ends_flag: trace_ends_with_ret)
     441    (start_status: Status) (final_status: Status)
     442      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     443        start_status final_status) on the_trace:
     444 compute_trace_label_label_cost_using_paid cost_labels … the_trace =
     445 compute_max_trace_label_label_cost … the_trace ≝ ?
     446and compute_trace_any_label_cost_using_paid_ok
     447  (cost_labels: BitVectorTrie costlabel 16)
     448  (trace_ends_flag: trace_ends_with_ret)
     449   (start_status: Status) (final_status: Status)
     450     (the_trace: trace_any_label (ASM_abstract_status cost_labels)
     451      trace_ends_flag start_status final_status) on the_trace:     
     452  compute_paid_trace_any_label cost_labels trace_ends_flag … the_trace
     453  +compute_trace_any_label_cost_using_paid cost_labels trace_ends_flag … the_trace
     454  =compute_max_trace_any_label_cost cost_labels trace_ends_flag … the_trace ≝ ?
     455and compute_trace_label_return_cost_using_paid_ok
     456  (cost_labels: BitVectorTrie costlabel 16)
     457  (start_status: Status) (final_status: Status)
     458    (the_trace: trace_label_return (ASM_abstract_status cost_labels)
     459     start_status final_status) on the_trace:
     460 compute_trace_label_return_cost_using_paid cost_labels … the_trace =
     461 compute_max_trace_label_return_cost cost_labels … the_trace ≝ ?.
     462[ cases the_trace #endsf #ss #es #tr #H normalize
     463  @compute_trace_any_label_cost_using_paid_ok
     464| cases the_trace
     465  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
     466  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
     467  | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%);
     468    <compute_trace_any_label_cost_using_paid_ok
     469    <compute_trace_label_return_cost_using_paid_ok
     470    -compute_trace_label_label_cost_using_paid_ok
     471    -compute_trace_label_return_cost_using_paid_ok
     472    -compute_trace_any_label_cost_using_paid_ok
     473    >commutative_plus in ⊢ (???(?%?));
     474    >commutative_plus in ⊢ (??(??%)?);
     475    >associative_plus >associative_plus in ⊢ (???%); @eq_f2 try %
     476    <associative_plus <commutative_plus %
     477  | #ef #sp #si #se #H1 #tr #H2 #H3 whd in ⊢ (??(?%%)%); >associative_plus @eq_f2
     478    [ % | @compute_trace_any_label_cost_using_paid_ok ]
     479  ]
     480| cases the_trace
     481  [ #sb #sa #tr normalize @compute_trace_label_label_cost_using_paid_ok
     482  | #si #sl #sf #tr1 #tr2 normalize @eq_f2
     483    [ @compute_trace_label_label_cost_using_paid_ok
     484    | @compute_trace_label_return_cost_using_paid_ok ]]]
     485qed.
    346486
    347487(*
    348 let rec compute_max_trace_label_label_cost_is_ok
    349   (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     488let rec compute_paid_trace_label_return
     489  (cost_labels: BitVectorTrie costlabel 16)
     490  (start_status: Status) (final_status: Status)
     491    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     492      on the_trace: nat ≝
     493 match the_trace with
     494  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label … trace_to_lift
     495  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     496      let labelled_cost ≝ compute_paid_trace_label_label … labelled_trace in
     497      let return_cost ≝ compute_paid_trace_label_return … ret_trace in
     498        labelled_cost + return_cost
     499  ].
     500*)
     501
     502let rec compute_cost_trace_label_label
     503  (cost_labels: BitVectorTrie costlabel 16)
     504   (trace_ends_flag: trace_ends_with_ret)
    350505    (start_status: Status) (final_status: Status)
    351       (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
    352       on the_trace:
    353         compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    354           (clock … final_status) - (clock … start_status) ≝ ?
    355 and compute_max_trace_any_label_pre_cost_is_ok
    356   (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     506      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     507        start_status final_status) on the_trace: list costlabel ≝
     508  match the_trace with
     509  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     510     let pc ≝ program_counter … initial in
     511     let label ≝
     512      match lookup_opt … pc cost_labels return λx. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
     513      [ None ⇒ λabs. ⊥
     514      | Some l ⇒ λ_. l ] labelled_proof in
     515     label::compute_cost_trace_any_label … given_trace
     516  ]
     517and compute_cost_trace_any_label
     518  (cost_labels: BitVectorTrie costlabel 16)
     519  (trace_ends_flag: trace_ends_with_ret)
     520   (start_status: Status) (final_status: Status)
     521     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     522       on the_trace: list costlabel ≝
     523  match the_trace with
     524  [ tal_base_not_return the_status _ _ _ _ ⇒ []
     525  | tal_base_return the_status _ _ _ ⇒ []
     526  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     527     _ _ _ call_trace final_trace ⇒
     528      let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
     529      let final_cost_trace ≝ compute_cost_trace_any_label cost_labels end_flag … final_trace in
     530        call_cost_trace @ final_cost_trace
     531  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     532       compute_cost_trace_any_label cost_labels end_flag
     533        status_init status_end tail_trace
     534  ]
     535and compute_cost_trace_label_return
     536  (cost_labels: BitVectorTrie costlabel 16)
     537  (start_status: Status) (final_status: Status)
     538    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     539      on the_trace: list costlabel ≝
     540  match the_trace with
     541  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
     542  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     543      let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in
     544      let return_cost ≝ compute_cost_trace_label_return … ret_trace in
     545        labelled_cost @ return_cost
     546  ].
     547//
     548qed.
     549
     550include "arithmetics/bigops.ma".
     551
     552lemma foo:
     553 ∀cost_label: BitVectorTrie costlabel 16.
     554 ∀initial,final.
     555 ∀trace: trace_label_return (ASM_abstract_status cost_label) initial final.
     556  let ctrace ≝ compute_cost_trace_label_return … trace in
     557  compute_max_trace_label_return_cost … trace =
     558   \big [ plus, 0 ]_{ i < |ctrace| } (? (nth i ? ctrace ?)).
     559 
     560  compute_cost_trace_label_return trace =
     561 
     562 
     563
     564
     565lemma
     566 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
     567  final_status the_trace =
     568 
     569
     570let rec compute_paid_trace_label_label_cost
     571  (cost_labels: BitVectorTrie Byte 16)
     572   (trace_ends_flag: trace_ends_with_ret)
    357573    (start_status: Status) (final_status: Status)
    358       (the_trace: trace_any_label cost_labels trace_ends_flag start_status final_status)
    359         on the_trace:
    360           compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    361             (clock … final_status) - (clock … start_status) ≝ ?
    362 and compute_max_trace_label_return_cost_is_ok
    363   (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
    364     (the_trace: trace_label_return cost_labels start_status final_status)
    365       on the_trace:
    366         compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
    367           (clock … final_status) - (clock … start_status) ≝ ?.
    368   [1:
    369     cases the_trace
    370     #ends_flag #start_status #end_status #label_label_pre_trace
    371     #labelled_proof
    372     normalize
    373     @compute_max_trace_label_label_pre_cost_is_ok
    374   |3:
    375     cases the_trace
    376     [1:
    377       #status_before #status_after #trace_to_lift
    378       @compute_max_trace_label_label_cost_is_ok
    379     |2:
    380       #status_initial #status_labelled #status_final #labelled_trace #return_trace
    381       >compute_max_trace_label_return_cost_is_ok %
    382     ]
    383   |2: cases the_trace
    384     [1: #the_status #not_return #not_jump #not_cost
    385         change in ⊢ (??%?) with (current_instruction_cost the_status);
    386         @current_instruction_cost_is_ok
    387     |2: #the_status #is_return
    388         change in ⊢ (??%?) with (current_instruction_cost the_status);
    389         @current_instruction_cost_is_ok
    390     |3: #the_status #is_jump #is_cost
    391         change in ⊢ (??%?) with (current_instruction_cost the_status);
    392         @current_instruction_cost_is_ok
    393     |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
    394         #next_instruction_coherence #call_trace #final_trace
    395         change in ⊢ (??%?) with (
    396           let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    397           let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
    398           let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
    399             call_trace_cost + current_instruction_cost + final_trace_cost)
    400         normalize nodelta;
    401         >current_instruction_cost_is_ok
    402         >compute_max_trace_label_return_cost_is_ok
    403         >compute_max_trace_label_label_pre_cost_is_ok
    404         generalize in match next_instruction_coherence;
    405         change in ⊢ (% → ?) with (
    406           let size ≝ current_instruction_cost pre_fun_call in
    407           let pc_before ≝ program_counter … pre_fun_call in
    408           let pc_after ≝ program_counter … after_fun_call in
    409           let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    410             sum = pc_after)
    411         normalize nodelta; #relation_pre_after_fun_call
    412         >plus_minus_rearrangement_2 in match (
    413           (clock (BitVectorTrie Byte 16) after_fun_call
    414             -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
    415           +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
    416             -clock (BitVectorTrie Byte 16) pre_fun_call)));
    417         >(plus_minus_rearrangement
    418           (clock (BitVectorTrie Byte 16) after_fun_call)
    419           (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
    420           (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
    421     |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
    422         #is_not_jump #is_not_ret #is_not_labelled
    423         change in ⊢ (??%?) with (
    424           let current_instruction_cost ≝ current_instruction_cost status_pre in
    425           let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
    426             current_instruction_cost + tail_trace_cost)
    427         normalize nodelta;
    428         >compute_max_trace_label_label_pre_cost_is_ok
    429         >current_instruction_cost_is_ok
    430     ]
    431   ]
    432 qed. *)
    433 
    434 (* XXX: work below here: *)
    435 
    436 let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
    437  match p with
    438  [ call ⇒ DO NOT ADD ANYTHING
    439  | _ ⇒ DO ADD ].
     574      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     575        start_status final_status) on the_trace: nat ≝
     576  match the_trace with
     577  [ tll_base _ _ _ given_trace _ ⇒
     578      compute_paid_trace_any_label_cost … given_trace
     579  ]
     580and compute_paid_trace_any_label_cost
     581  (cost_labels: BitVectorTrie Byte 16)
     582  (trace_ends_flag: trace_ends_with_ret)
     583   (start_status: Status) (final_status: Status)
     584     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     585       on the_trace: nat ≝
     586  match the_trace with
     587  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
     588  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     589  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     590     _ _ _ call_trace final_trace ⇒
     591      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     592      let final_trace_cost ≝ compute_paid_trace_any_label_cost cost_labels end_flag … final_trace in
     593        current_instruction_cost + final_trace_cost
     594  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     595      let current_instruction_cost ≝ current_instruction_cost status_pre in
     596      let tail_trace_cost ≝
     597       compute_paid_trace_any_label_cost cost_labels end_flag
     598        status_init status_end tail_trace
     599      in
     600        current_instruction_cost + tail_trace_cost
     601  ]
     602and compute_paid_trace_label_return_cost
     603  (cost_labels: BitVectorTrie Byte 16)
     604  (start_status: Status) (final_status: Status)
     605    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     606      on the_trace: nat ≝
     607  match the_trace with
     608  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label_cost … trace_to_lift
     609  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     610      let labelled_cost ≝ compute_paid_trace_label_label_cost … labelled_trace in
     611      let return_cost ≝ compute_paid_trace_label_return_cost … ret_trace in
     612        labelled_cost + return_cost
     613  ].
    440614
    441615let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
Note: See TracChangeset for help on using the changeset viewer.