Changeset 1619 for src/ASM


Ignore:
Timestamp:
Dec 15, 2011, 12:02:40 AM (8 years ago)
Author:
sacerdot
Message:

Major advancement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1587 r1619  
    33include "ASM/Status.ma".
    44include "common/StructuredTraces.ma".
     5include "arithmetics/bigops.ma".
     6include alias "arithmetics/nat.ma".
     7include alias "basics/logic.ma".
    58
    69let rec compute_max_trace_label_label_cost
     
    155158      #start_status #final_status #is_next #is_not_return try (#is_costed)
    156159      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
    157       cases(is_next)
    158       cases(execute_1 start_status)
    159       whd in match eject; normalize nodelta;
    160       #the_status #assm >assm %
     160      cases(is_next) @execute_1_ok
    161161    |3:
    162162      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    173173        status_after_fun_call call_trace)
    174174      cases(is_next) in match (clock … status_start_fun_call);
    175       cases(execute_1 status_pre_fun_call);
    176       #the_status
    177       whd in match eject; normalize nodelta;
    178       #assm >assm
     175      >(execute_1_ok status_pre_fun_call)
    179176      <associative_plus in ⊢ (??%?);
    180177      <commutative_plus in match (
     
    207204         status_init status_end trace_any_label)
    208205      cases(is_next) in match (clock … status_init);
    209       cases(execute_1 status_pre)
    210       #the_status whd in match eject; normalize nodelta;
    211       #assm >assm <associative_plus in ⊢ (??%?);
    212       >commutative_plus in match (
    213         compute_max_trace_any_label_cost cost_labels end_flag status_init status_end trace_any_label
    214           + current_instruction_cost status_pre);
    215       %
     206      >(execute_1_ok status_pre)
     207      >commutative_plus >associative_plus >associative_plus @eq_f
     208      @commutative_plus
    216209    ]
    217210  |3:
     
    391384      [ None ⇒ λabs. ⊥
    392385      | Some l ⇒ λ_. l ] labelled_proof in
    393      (dp … label ?)::compute_cost_trace_any_label … given_trace
     386     (mk_Sig … label ?)::compute_cost_trace_any_label … given_trace
    394387  ]
    395388and compute_cost_trace_any_label
     
    452445*)
    453446
    454 include "arithmetics/bigops.ma".
    455 
    456447(* This shoudl go in bigops! *)
    457448theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B.
     
    495486   times ≡ prod ? ? S.
    496487
    497 notation "Σ_{ ident i < n } f"
     488notation > "Σ_{ ident i < n } f"
    498489  with precedence 20
    499490for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
     491
     492notation < "Σ_{ ident i < n } f"
     493  with precedence 20
     494for @{'bigop $n plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f)}.
    500495
    501496axiom code_memory_ro_label_label:
     
    522517 % #abs destruct (abs)
    523518qed.
     519
     520include alias "arithmetics/nat.ma".
     521include alias "basics/logic.ma".
    524522
    525523lemma ltb_rect:
     
    596594  i < |l1| →
    597595   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
    598    tech_cost_of_label cost_labels cost_mnth_safe ? i ctrace H) ?ap codom_dom (l1@l2) (i+|l1|).
    599  #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
    600  cut (ltb i (|l2|) = ltb (i+|l1|) (|l1@l2|))
    601  [ change with (leb ?? = leb ??); @leb_elim
    602    [ #H1 change with (i < ?) in H1; >le_to_leb_true [//] change with (? < ?)
    603      >append_length >commutative_plus @monotonic_lt_plus_r //
    604    | #H1 change with (¬ i < ?) in H1; >not_le_to_leb_false [//]
    605      >append_length >commutative_plus % #H2
    606      change with (? < ?) in H2; @(absurd ?? H1) @(lt_plus_to_lt_r … H2) ]
    607  | #E whd in match tech_cost_of_label; normalize nodelta
    608  @same_ltb_rect [@E]
    609  [ #K1 #K2 lapply (shift_nth_safe ? i l1 l2 K1 K2) #H check eq_f
    610    lapply (eq_f ?? (lookup_present CostTag nat cost_Map) ?? H)
    611 
    612    
    613  
    614   cut (decide_bool (ltb i (|l2|)) = decide_bool (ltb (i+(|l1|)) (|l1@l2|)))
    615   whd in match tech_cost_of_label; normalize nodelta
    616    
     596   tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
     597 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
     598 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
     599 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2
     600   whd in match ltb; normalize nodelta
     601   [1: >le_to_leb_true try assumption applyS le_to_leb_true //
     602   |4: >not_le_to_leb_false try assumption applyS not_le_to_leb_false
     603       change with (¬ ? ≤ ?) in K1; applyS K1
     604   |2: @⊥ @(absurd (i+|l1| < |l1@l2|)) // >length_append
     605       applyS (monotonic_lt_plus_r … (|l1|)) //
     606   |3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ]
     607 | #H1 #H2
     608   generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
     609   <(shift_nth_safe … H1) #p %
     610 | // ]
     611qed.
    617612
    618613let rec compute_max_trace_label_return_cost_ok_with_trace
     
    627622  let ctrace ≝ compute_cost_trace_label_return … trace in
    628623  compute_max_trace_label_return_cost … trace =
    629    Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)
     624   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    630625    ≝ ?.
    631626lapply (refl … initial) cases trace in ⊢ (??%? → %);
     
    640635    |2: @codom_dom
    641636    |4:lapply (code_memory_ro_label_label … tr1) >E #E2 <E2 @dom_codom]
    642     @same_bigop [//] #i #H #_ -dom_codom
    643     generalize in match (compute_cost_trace_label_return cost_labels sl sf tr2); #l1
    644     generalize in match (compute_cost_trace_label_label cost_labels doesnt_end_with_ret si sl tr1);
    645 
    646 i < |l1| →
    647 tech_cost_of_label cost_labels cost_map codom_dom l1 i =
    648 tech_cost_of_label cost_labels cost_map codom_dom (l2@l1) (i+|l1|)
    649 
    650 
    651      whd in ⊢ (??%%);
     637    @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift
     638
    652639  |
    653640  ]
Note: See TracChangeset for help on using the changeset viewer.