Changeset 1579


Ignore:
Timestamp:
Dec 1, 2011, 2:11:37 PM (8 years ago)
Author:
mulligan
Message:

Finished proof with simpler statement, making everything a lot nicer

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1577 r1579  
    249249qed.
    250250
    251 axiom clock_execute_1:
    252   ∀s: Status.
    253     clock … (execute_1 s) = current_instruction_cost s + clock … s.
    254 
    255 axiom plus_le_le:
     251lemma m_le_plus_n_m:
     252  ∀m, n: nat.
     253    m ≤ n + m.
     254  #m #n //
     255qed.
     256
     257lemma n_plus_m_le_o_to_m_le_o:
    256258  ∀m, n, o: nat.
    257     m + n ≤ o → n ≤ o.
     259    n + m ≤ o → m ≤ o.
     260  #m #n #o #assm /2 by le_plus_b/
     261qed.
     262
     263lemma m_minus_n_plus_o_m_minus_n_minus_o:
     264  ∀m, n, o: nat.
     265    m - (n + o) = m - n - o.
     266  #m #n #o /2 by /
     267qed.
     268
     269let rec compute_max_trace_label_label_cost_is_ok
     270  (cost_labels: BitVectorTrie costlabel 16)
     271   (trace_ends_flag: trace_ends_with_ret)
     272    (start_status: Status) (final_status: Status)
     273      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     274        start_status final_status) on the_trace:
     275          clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
     276and compute_max_trace_any_label_cost_is_ok
     277  (cost_labels: BitVectorTrie costlabel 16)
     278  (trace_ends_flag: trace_ends_with_ret)
     279   (start_status: Status) (final_status: Status)
     280     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     281       on the_trace:
     282         clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
     283and compute_max_trace_label_return_cost_is_ok
     284  (cost_labels: BitVectorTrie costlabel 16)
     285  (start_status: Status) (final_status: Status)
     286    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     287      on the_trace:
     288        clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock … start_status ≝ ?.
     289  [1:
     290    cases the_trace
     291    #ends_flag #start_status #end_status #any_label_trace #is_costed
     292    normalize @compute_max_trace_any_label_cost_is_ok
     293  |2:
     294    cases the_trace
     295    [1,2:
     296      #start_status #final_status #is_next #is_not_return try (#is_costed)
     297      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
     298      cases(is_next)
     299      cases(execute_1 start_status)
     300      whd in match eject; normalize nodelta;
     301      #the_status #assm >assm %
     302    |3:
     303      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     304      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
     305      change with (
     306      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
     307      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     308      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
     309        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
     310      normalize nodelta;
     311      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
     312          status_final final_trace)
     313      >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
     314        status_after_fun_call call_trace)
     315      cases(is_next) in match (clock … status_start_fun_call);
     316      cases(execute_1 status_pre_fun_call);
     317      #the_status
     318      whd in match eject; normalize nodelta;
     319      #assm >assm
     320      <associative_plus in ⊢ (??%?);
     321      <commutative_plus in match (
     322        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
     323          + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace);
     324      >associative_plus in ⊢ (??%?);
     325      <commutative_plus in match (
     326        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
     327          + (current_instruction_cost status_pre_fun_call
     328              + clock (BitVectorTrie Byte 16) status_pre_fun_call));
     329      >associative_plus in ⊢ (??%?);
     330      <commutative_plus in match (
     331         clock (BitVectorTrie Byte 16) status_pre_fun_call
     332           + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace);
     333      <(associative_plus (
     334         (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace)))
     335      <associative_plus in ⊢ (??%?); %
     336    |4:
     337      #end_flag #status_pre #status_init #status_end #is_next
     338      #trace_any_label #is_other #is_not_costed
     339      change with (
     340      let current_instruction_cost ≝ current_instruction_cost status_pre in
     341      let tail_trace_cost ≝
     342       compute_max_trace_any_label_cost cost_labels end_flag
     343        status_init status_end trace_any_label
     344      in
     345        current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?));
     346      normalize nodelta;
     347      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
     348         status_init status_end trace_any_label)
     349      cases(is_next) in match (clock … status_init);
     350      cases(execute_1 status_pre)
     351      #the_status whd in match eject; normalize nodelta;
     352      #assm >assm <associative_plus in ⊢ (??%?);
     353      >commutative_plus in match (
     354        compute_max_trace_any_label_cost cost_labels end_flag status_init status_end trace_any_label
     355          + current_instruction_cost status_pre);
     356      %
     357    ]
     358  |3:
     359    cases the_trace
     360    [1:
     361      #status_before #status_after #trace_to_lift
     362      normalize @compute_max_trace_label_label_cost_is_ok
     363    |2:
     364      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
     365      normalize
     366      >(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
     367      >(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     368      <associative_plus in ⊢ (??%?);
     369      >commutative_plus in match (
     370        compute_max_trace_label_return_cost cost_labels status_labelled status_final ret_trace
     371          + compute_max_trace_label_label_cost cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     372      %
     373    ]
     374  ].
     375qed.
    258376   
    259377let rec compute_max_trace_label_label_cost_is_ok
     
    291409      cases(is_next)
    292410      @conj
     411      cases(execute_1 start_status)
     412      #the_status #assm
     413      whd in match eject; normalize nodelta
     414      >assm
    293415      [1:
    294         cases(execute_1 start_status)
    295         #the_status #assm
    296         whd in match eject; normalize nodelta
    297         cases(assm)
    298         #eq_hyp #le_hyp
    299         >eq_hyp %
     416        @minus_plus_m_m
    300417      |2:
    301         cases(execute_1 start_status)
    302         #the_status #assm
    303         whd in match eject; normalize nodelta
    304         cases(assm)
    305         #eq_hyp #le_hyp
    306         assumption
     418        @m_le_plus_n_m
    307419      ]
    308420    |2:
     
    311423      cases(is_next)
    312424      @conj
     425      cases(execute_1 start_status)
     426      #the_status #assm
     427      whd in match eject; normalize nodelta
     428      >assm
    313429      [1:
    314         cases(execute_1 start_status)
     430        @minus_plus_m_m
     431      |2:
     432        @m_le_plus_n_m
     433      ]
     434    |3:
     435      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     436      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
     437      change with (
     438      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
     439      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     440      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
     441        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
     442      normalize nodelta;
     443      @conj
     444      [1:
     445        cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
     446          status_after_fun_call call_trace)
     447        #trace_label_return_eq #trace_label_return_le
     448        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
     449          status_final final_trace)
     450        #trace_any_label_eq #trace_any_label_le
     451        >trace_any_label_eq >trace_label_return_eq
     452        cases(is_next)
     453        cases(execute_1 status_pre_fun_call)
    315454        #the_status #assm
    316         whd in match eject; normalize nodelta
    317         cases(assm)
    318         #eq_hyp #le_hyp
    319         >eq_hyp %
     455        whd in match eject; normalize nodelta;
     456        >assm >commutative_plus in match
     457          (current_instruction_cost status_pre_fun_call
     458            + clock (BitVectorTrie Byte 16) status_pre_fun_call);
     459        >m_minus_n_plus_o_m_minus_n_minus_o
     460        <(plus_minus_m_m
     461          (clock (BitVectorTrie Byte 16) status_after_fun_call
     462            - clock (BitVectorTrie Byte 16) status_pre_fun_call)
     463          (current_instruction_cost status_pre_fun_call))
     464        [1:
     465          @plus_minus_rearrangement_1
     466          lapply(transitive_le
     467            (clock … status_pre_fun_call)
     468            (clock … status_start_fun_call)
     469            (clock … status_after_fun_call) ? trace_label_return_le)
     470          [1,3:
     471            cases(is_next)
     472            cases(execute_1 status_pre_fun_call)
     473            whd in match eject; normalize nodelta;
     474            #the_new_status #assm >assm @m_le_plus_n_m
     475          |2,4:
     476            #assm assumption
     477          ]
     478        |2:
     479          cases(is_next)
     480          assumption
    320481      |2:
    321         cases(execute_1 start_status)
     482        cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
     483          status_after_fun_call call_trace)
     484        #trace_label_return_eq
     485        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
     486          status_final final_trace)
     487        #trace_any_label_eq cases(is_next)
     488        cases(execute_1 status_pre_fun_call)
    322489        #the_status #assm
    323         whd in match eject; normalize nodelta
    324         cases(assm)
    325         #eq_hyp #le_hyp
     490        whd in match eject; normalize nodelta;
     491        >assm #after_final_le #pre_after_le
     492        lapply(n_plus_m_le_o_to_m_le_o
     493          (clock … status_pre_fun_call)
     494          (current_instruction_cost status_pre_fun_call)
     495          (clock … status_after_fun_call) pre_after_le);
     496        #pre_after_le'
     497        @(transitive_le
     498          (clock … status_pre_fun_call)
     499          (clock … status_after_fun_call)
     500          (clock … status_final))
    326501        assumption
    327502      ]
    328     |3:
     503    |*: cases daemon (* XXX: for now
    329504      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    330505      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
     
    414589        >clock_execute_1
    415590        @plus_le_le
    416       ]
     591      ]*)
    417592    ]
    418593  |3:
Note: See TracChangeset for help on using the changeset viewer.