Changeset 1567


Ignore:
Timestamp:
Nov 25, 2011, 6:17:13 PM (8 years ago)
Author:
mulligan
Message:

more work on big proof, 2.5 cases left

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1564 r1567  
    222222include alias "arithmetics/nat.ma".
    223223
    224 (*Useless now?
     224(*
    225225lemma minus_m_n_minus_minus_plus_1:
    226226  ∀m, n: nat.
     
    229229 /3 by lt_plus_to_minus_r, plus_minus/
    230230qed.
     231*)
    231232
    232233lemma plus_minus_rearrangement_1:
     
    245246    (m - n) + (n - o) = m - o.
    246247 /2 by plus_minus_rearrangement_1/
    247 qed.*)
    248 
    249 (*
     248qed.
     249
     250axiom current_instruction_cost_non_zero:
     251  ∀s: Status.
     252    current_instruction_cost s > 0.
     253   
     254axiom minus_m_n_gt_o_0_le_n_m:
     255  ∀m, n, o.
     256  m - n = o → o > 0 → n ≤ m.
     257
    250258let rec compute_max_trace_label_label_cost_is_ok
    251   (cost_labels: BitVectorTrie Byte 16)
     259  (cost_labels: BitVectorTrie costlabel 16)
    252260   (trace_ends_flag: trace_ends_with_ret)
    253261    (start_status: Status) (final_status: Status)
    254262      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    255263        start_status final_status) on the_trace:
    256           compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    257             (clock … final_status) - (clock … start_status) ≝ ?
     264          And (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
     265            (clock … final_status) - (clock … start_status)) (clock … start_status ≤ clock … final_status) ≝ ?
    258266and compute_max_trace_any_label_cost_is_ok
    259   (cost_labels: BitVectorTrie Byte 16)
     267  (cost_labels: BitVectorTrie costlabel 16)
    260268  (trace_ends_flag: trace_ends_with_ret)
    261269   (start_status: Status) (final_status: Status)
    262270     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    263271       on the_trace:
    264          compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    265            (clock … final_status) - (clock … start_status) ≝ ?
     272         (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
     273           (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?
    266274and compute_max_trace_label_return_cost_is_ok
    267   (cost_labels: BitVectorTrie Byte 16)
     275  (cost_labels: BitVectorTrie costlabel 16)
    268276  (start_status: Status) (final_status: Status)
    269277    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    270278      on the_trace:
    271         compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
    272           (clock … final_status) - (clock … start_status) ≝ ?.
     279        (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
     280          (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?.
    273281  [1:
    274282    cases the_trace
     
    276284    normalize @compute_max_trace_any_label_cost_is_ok
    277285  |2:
     286    cases the_trace
     287    [1:
     288      #start_status #final_status #is_next #is_not_return #is_costed
     289      change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
     290      cases(is_next)
     291      @conj
     292      [1:
     293        cases(execute_1 start_status)
     294        #the_status #assm
     295        whd in match eject; normalize nodelta
     296        >assm %
     297      |2:
     298        cases(execute_1 start_status)
     299        #the_status #assm
     300        whd in match eject; normalize nodelta
     301        @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
     302        [1: assumption
     303        |2: @current_instruction_cost_non_zero
     304        ]
     305      ]
     306    |2:
     307      #start_status #final_status #is_next #is_return
     308      change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
     309      cases(is_next)
     310      @conj
     311      [1:
     312        cases(execute_1 start_status)
     313        #the_status #assm
     314        whd in match eject; normalize nodelta
     315        >assm %
     316      |2:
     317        cases(execute_1 start_status)
     318        #the_status #assm
     319        whd in match eject; normalize nodelta
     320        @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
     321        [1: assumption
     322        |2: @current_instruction_cost_non_zero
     323        ]
     324      ]
     325    |3:
     326      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     327      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
     328      change with (
     329      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
     330      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     331      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
     332        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
     333      normalize nodelta;
     334      @conj
     335      [1:
     336        cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
     337          status_after_fun_call call_trace)
     338        #trace_label_return_eq #trace_label_return_le
     339        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
     340          status_final final_trace)
     341        #trace_any_label_eq #trace_any_label_le
     342        >trace_label_return_eq >trace_any_label_eq
     343        cases daemon (* XXX: complete me *)
     344      |2:
     345        cases daemon (* XXX: complete me *)
     346      ]
     347    |4:
     348      #end_flag #status_pre #status_init #status_end #is_next
     349      #trace_any_label #is_other #is_not_costed
     350      cases daemon (* XXX: complete me *)
     351    ]
    278352  |3:
    279353    cases the_trace
     
    283357    |2:
    284358      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
    285       normalize >compute_max_trace_label_label_cost_is_ok
    286       >compute_max_trace_label_return_cost_is_ok
     359      normalize
     360      cases(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     361      #label_label_trace_equality #label_label_trace_leq
     362      cases(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
     363      #label_return_trace_equality #label_return_trace_leq
     364      >label_label_trace_equality >label_return_trace_equality
     365      @conj
     366      [2: @(transitive_le (clock (BitVectorTrie (Vector bool 8) 16) status_initial)
     367            (clock (BitVectorTrie Byte 16) status_labelled)
     368            (clock (BitVectorTrie (Vector bool 8) 16) status_final))
     369      |1: @plus_minus_rearrangement_1
     370      ]
     371      assumption
    287372    ]
    288   ].
    289 *)
     373  ]
     374qed.
    290375
    291376(* XXX: work below here: *)
Note: See TracChangeset for help on using the changeset viewer.