Changeset 1650 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Jan 19, 2012, 4:56:17 PM (7 years ago)
Author:
mulligan
Message:

changes over the last couple of days: stuck due to matita producing terms so large that the program cannot print them out!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1648 r1650  
    1818definition ASM_classify0: instruction → status_class ≝
    1919  λi: instruction.
    20     match i with
    21      [ RealInstruction pre ⇒
    22        match pre with
    23         [ RET ⇒ cl_return
    24         | JZ _ ⇒ cl_jump
    25         | JNZ _ ⇒ cl_jump
    26         | JC _ ⇒ cl_jump
    27         | JNC _ ⇒ cl_jump
    28         | JB _ _ ⇒ cl_jump
    29         | JNB _ _ ⇒ cl_jump
    30         | JBC _ _ ⇒ cl_jump
    31         | CJNE _ _ ⇒ cl_jump
    32         | DJNZ _ _ ⇒ cl_jump
    33         | _ ⇒ cl_other
    34         ]
    35      | ACALL _ ⇒ cl_call
    36      | LCALL _ ⇒ cl_call
    37      | JMP _ ⇒ cl_call
    38      | AJMP _ ⇒ cl_jump
    39      | LJMP _ ⇒ cl_jump
    40      | SJMP _ ⇒ cl_jump
    41      | _ ⇒ cl_other
    42      ].
     20  match i with
     21   [ RealInstruction pre ⇒
     22     match pre with
     23      [ RET ⇒ cl_return
     24      | JZ _ ⇒ cl_jump
     25      | JNZ _ ⇒ cl_jump
     26      | JC _ ⇒ cl_jump
     27      | JNC _ ⇒ cl_jump
     28      | JB _ _ ⇒ cl_jump
     29      | JNB _ _ ⇒ cl_jump
     30      | JBC _ _ ⇒ cl_jump
     31      | CJNE _ _ ⇒ cl_jump
     32      | DJNZ _ _ ⇒ cl_jump
     33      | _ ⇒ cl_other
     34      ]
     35   | ACALL _ ⇒ cl_call
     36   | LCALL _ ⇒ cl_call
     37   | JMP _ ⇒ cl_call
     38   | AJMP _ ⇒ cl_jump
     39   | LJMP _ ⇒ cl_jump
     40   | SJMP _ ⇒ cl_jump
     41   | _ ⇒ cl_other
     42   ].
    4343
    4444definition ASM_classify: Status → status_class ≝
    45  λs: Status.
    46    ASM_classify0 (current_instruction s).
     45  λs: Status.
     46    ASM_classify0 (current_instruction s).
     47
     48definition current_instruction_is_labelled ≝
     49  λcost_labels: BitVectorTrie costlabel 16.
     50  λs: Status.
     51  let pc ≝ program_counter … s in
     52    match lookup_opt … pc cost_labels with
     53    [ None ⇒ False
     54    | _    ⇒ True
     55    ].
     56
     57definition next_instruction_properly_relates_program_counters ≝
     58  λbefore: Status.
     59  λafter : Status.
     60  let size ≝ current_instruction_cost before in
     61  let pc_before ≝ program_counter … before in
     62  let pc_after ≝ program_counter … after in
     63  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
     64    sum = pc_after.
     65
     66definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
     67 λcost_labels.
     68  mk_abstract_status
     69   Status
     70   (λs,s'. (execute_1 s) = s')
     71   (λs,class. ASM_classify s = class)
     72   (current_instruction_is_labelled cost_labels)
     73   next_instruction_properly_relates_program_counters.
    4774
    4875let rec compute_max_trace_label_label_cost
     
    92119  ].
    93120
    94 (*Useless now?
    95 (* To be moved *)
    96 lemma pred_minus_1:
    97   ∀m, n: nat.
    98   ∀proof: n < m.
    99     pred (m - n) = m - n - 1.
    100   #m #n
    101   cases m
    102   [ #proof
    103     cases(lt_to_not_zero … proof)
    104   | #m' #proof
    105     normalize in ⊢ (???%);
    106     cases n
    107     [ normalize //
    108     | #n' normalize
    109       cases(m' - n')
    110       [ %
    111       | #Sm_n'
    112         normalize //
    113       ]
    114     ]
    115   ]
    116 qed.
    117 
    118 lemma succ_m_plus_one:
    119   ∀m: nat.
    120     S m = m + 1.
    121  //
    122 qed.*)
    123 
    124121include alias "arithmetics/nat.ma".
    125 
    126 (*
    127 lemma minus_m_n_minus_minus_plus_1:
    128   ∀m, n: nat.
    129   ∀proof: n < m.
    130     m - n = (m - n - 1) + 1.
    131  /3 by lt_plus_to_minus_r, plus_minus/
    132 qed.
    133 
    134 lemma plus_minus_rearrangement_1:
    135   ∀m, n, o: nat.
    136   ∀proof_n_m: n ≤ m.
    137   ∀proof_m_o: m ≤ o.
    138     (m - n) + (o - m) = o - n.
    139   #m #n #o #H1 #H2
    140   lapply (minus_to_plus … H1 (refl …)) #K1 >K1
    141   lapply (minus_to_plus … H2 (refl …)) #K2 >K2
    142   /2 by plus_minus/
    143 qed.
    144 
    145 lemma plus_minus_rearrangement_2:
    146   ∀m, n, o: nat. n ≤ m → o ≤ n →
    147     (m - n) + (n - o) = m - o.
    148  /2 by plus_minus_rearrangement_1/
    149 qed.
    150 
    151 lemma m_le_plus_n_m:
    152   ∀m, n: nat.
    153     m ≤ n + m.
    154   #m #n //
    155 qed.
    156 
    157 lemma n_plus_m_le_o_to_m_le_o:
    158   ∀m, n, o: nat.
    159     n + m ≤ o → m ≤ o.
    160   #m #n #o #assm /2 by le_plus_b/
    161 qed.
    162 
    163 lemma m_minus_n_plus_o_m_minus_n_minus_o:
    164   ∀m, n, o: nat.
    165     m - (n + o) = m - n - o.
    166   #m #n #o /2 by /
    167 qed.
    168 *)
    169122
    170123let rec compute_max_trace_label_label_cost_is_ok
     
    461414qed.
    462415
    463 (* ??????????????????????? *)
    464 axiom block_cost_static_dynamic_ok:
    465  ∀cost_labels: BitVectorTrie costlabel 16.
    466  ∀trace_ends_flag.
    467  ∀start_status: Status.
    468  ∀final_status: Status.
    469  ∀the_trace:
    470   trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    471    start_status final_status.
    472  let mem ≝ code_memory … start_status in
    473  let pc ≝ program_counter … start_status in
    474  let program_size ≝ 2^16 in
    475   block_cost mem cost_labels pc program_size =
    476   compute_paid_trace_label_label cost_labels trace_ends_flag
    477    start_status final_status the_trace.
     416(* XXX: zero in base cases (where the trace is a singleton transition) because
     417        we are counting until one from end
     418*)
     419let rec trace_any_label_length
     420  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
     421    (start_status: Status) (final_status: Status)
     422      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     423        on the_trace: nat ≝
     424  match the_trace with
     425  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
     426  | tal_base_return the_status _ _ _ ⇒ 0
     427  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒
     428      let tail_length ≝ trace_any_label_length … final_trace in
     429      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
     430        pc_difference + tail_length
     431  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     432      let tail_length ≝ trace_any_label_length … tail_trace in
     433      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
     434        pc_difference + tail_length       
     435  ].
     436
     437(* XXX: commented out in favour of above
     438let rec trace_label_label_length
     439  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
     440    (start_status: Status) (final_status: Status)
     441      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     442        on the_trace: nat ≝
     443  match the_trace with
     444  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
     445  ]
     446and trace_any_label_length
     447  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
     448    (start_status: Status) (final_status: Status)
     449      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     450        on the_trace: nat ≝
     451  match the_trace with
     452  [ tal_base_not_return the_status _ _ _ _ ⇒ ?
     453  | tal_base_return the_status _ _ _ ⇒ ?
     454  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒ ?
     455  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ ?
     456  ]
     457and trace_label_return_length
     458  (cost_labels: BitVectorTrie costlabel 16) (start_status: Status) (final_status: Status)
     459    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     460      on the_trace: nat ≝
     461  match the_trace with
     462  [ tlr_base before after trace_to_lift ⇒ ?
     463  | tlr_step initial labelled final labelled_trace ret_trace ⇒ ?
     464  ].
     465  cases daemon
     466qed.
     467*)
     468
     469(* Experiments with block_cost first!
     470lemma reachable_program_counter_to_compute_trace_any_label_length_le_program_size:
     471  ∀start_status, final_status: Status.
     472  ∀code_memory: BitVectorTrie Byte 16.
     473  ∀program_size: nat.
     474  ∀cost_labels: BitVectorTrie costlabel 16.
     475  ∀trace_ends_flag: trace_ends_with_ret.
     476  ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
     477  let start_program_counter ≝ program_counter … start_status in
     478  let final_program_counter ≝ program_counter … final_status in
     479    reachable_program_counter code_memory program_size start_program_counter →
     480      nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter).
     481  cases daemon
     482qed.
     483
     484lemma reachable_program_counter_to_compute_trace_label_label_length_le_program_size:
     485  ∀start_status, final_status: Status.
     486  ∀code_memory: BitVectorTrie Byte 16.
     487  ∀program_size: nat.
     488  ∀cost_labels: BitVectorTrie costlabel 16.
     489  ∀trace_ends_flag: trace_ends_with_ret.
     490  ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
     491  let start_program_counter ≝ program_counter … start_status in
     492  let final_program_counter ≝ program_counter … final_status in
     493    reachable_program_counter code_memory program_size start_program_counter →
     494      nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter).
     495  #start_status #final_status #code_memory #program_size #cost_labels #trace_ends_flag #the_trace
     496  cases daemon
     497qed.
     498
     499corollary reachable_program_counter_to_compute_trace_length_le_program_size:
     500  ∀start_status, final_status: Status.
     501  ∀code_memory: BitVectorTrie Byte 16.
     502  ∀program_size: nat.
     503  ∀cost_labels: BitVectorTrie costlabel 16.
     504  ∀trace_ends_flag: trace_ends_with_ret.
     505  ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
     506  let program_counter ≝ program_counter … start_status in
     507    reachable_program_counter code_memory program_size program_counter →
     508      trace_length start_status final_status ≤ program_size.
     509  cases daemon
     510qed. *)
     511
     512include alias "arithmetics/nat.ma".
     513include alias "basics/logic.ma".
     514
     515lemma and_intro_right:
     516  ∀a, b: Prop.
     517    a → (a → b) → a ∧ b.
     518  #a #b /3/
     519qed.
     520
     521lemma lt_m_n_to_exists_o_plus_m_n:
     522  ∀m, n: nat.
     523    m < n → ∃o: nat. m + o = n.
     524  #m #n
     525  cases m
     526  [1:
     527    #irrelevant
     528    %{n} %
     529  |2:
     530    #m' #lt_hyp
     531    %{(n - S m')}
     532    >commutative_plus in ⊢ (??%?);
     533    <plus_minus_m_m
     534    [1:
     535      %
     536    |2:
     537      @lt_S_to_lt
     538      assumption
     539    ]
     540  ]
     541qed.
     542
     543lemma lt_O_n_to_S_pred_n_n:
     544  ∀n: nat.
     545    0 < n → S (pred n) = n.
     546  #n
     547  cases n
     548  [1:
     549    #absurd
     550    cases(lt_to_not_zero 0 0 absurd)
     551  |2:
     552    #n' #lt_hyp %
     553  ]
     554qed.
     555
     556lemma exists_plus_m_n_to_exists_Sn:
     557  ∀m, n: nat.
     558    m < n → ∃p: nat. S p = n.
     559  #m #n
     560  cases m
     561  [1:
     562    #lt_hyp %{(pred n)}
     563    @(lt_O_n_to_S_pred_n_n … lt_hyp)
     564  |2:
     565    #m' #lt_hyp %{(pred n)}
     566    @(lt_O_n_to_S_pred_n_n)
     567    @(transitive_le … (S m') …)
     568    [1:
     569      //
     570    |2:
     571      @lt_S_to_lt
     572      assumption
     573    ]
     574  ]
     575qed.
     576   
     577
     578let rec block_cost_trace_any_label_static_dynamic_ok
     579  (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     580    (trace_ends_flag: ?) (start_status: Status) (final_status: Status)
     581      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     582        on the_trace:
     583          let code_memory ≝ code_memory … start_status in
     584          let program_counter ≝ program_counter … start_status in
     585            ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
     586            ∀good_program_witness: good_program code_memory total_program_size.
     587              (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     588                block_cost code_memory program_counter total_program_size cost_labels reachable_program_counter_witness good_program_witness =
     589                  compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝ ?.
     590    letin code_memory ≝ (code_memory … start_status)
     591    letin program_counter ≝ (program_counter … start_status)
     592    #reachable_program_counter_witness #good_program_witness
     593    generalize in match (refl … final_status);
     594    generalize in match (refl … start_status);
     595    cases the_trace in ⊢ (???% → ???% → %);
     596    [1:
     597      #start_status' #final_status' #execute_hyp #classifier_hyp #costed_hyp
     598      #start_status_refl #final_status_refl destruct
     599      whd in match (trace_any_label_length ? ? ? ? ?);
     600      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
     601      @and_intro_right
     602      [1:
     603        generalize in match reachable_program_counter_witness;
     604        whd in match (reachable_program_counter code_memory total_program_size program_counter);
     605        * #irrelevant #relevant
     606        lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)
     607        #hyp assumption
     608      |2:
     609        * #n #trace_length_hyp
     610        whd in match block_cost; normalize nodelta
     611        generalize in match reachable_program_counter_witness;
     612        generalize in match good_program_witness;
     613        <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?); (*
     614        -reachable_program_counter_witness #reachable_program_counter_witness
     615        -good_program_witness #good_program_witness
     616        whd in ⊢ (??%?); @pair_elim *)
     617      ]
     618    |2:
     619      #start_status' #final_status' #execute_hyp #classified_hyp
     620      #start_status_refl #final_status_refl destruct
     621      whd in match (trace_any_label_length ? ? ? ? ?);
     622      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
     623      @and_intro_right
     624      [1:
     625        generalize in match reachable_program_counter_witness;
     626        whd in match (reachable_program_counter code_memory total_program_size program_counter);
     627        * #irrelevant #relevant
     628        lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)
     629        #hyp assumption
     630      |2:
     631        * #n #trace_length_hyp
     632        whd in match block_cost; normalize nodelta
     633        generalize in match reachable_program_counter_witness;
     634        generalize in match good_program_witness;
     635        <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
     636        -reachable_program_counter_witness #reachable_program_counter_witness
     637        -good_program_witness #good_program_witness
     638        whd in match (0 + S n); whd in ⊢ (??%?);
     639      ]
     640    |3:
     641      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     642      #status_final #execute_hyp #classifier_hyp #after_return_hyp
     643      #trace_label_return #trace_any_label #start_status_refl #final_status_refl
     644      destruct
     645      whd in match (trace_any_label_length ? ? ? ? ?);
     646      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
     647      @and_intro_right
     648      [1:
     649      |2:
     650      ]
     651    |4:
     652      #end_flag #status_pre #status_init #status_end #execute_hyp #trace_any_label
     653      #classifier_hyp #costed_hyp #start_status_refl #final_status_refl
     654      destruct
     655      whd in match (trace_any_label_length ? ? ? ? ?);
     656      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
     657      @and_intro_right
     658      [1:
     659      |2:
     660      ]
     661    ]
     662  ]
     663 
     664corollary block_cost_trace_label_labelstatic_dynamic_ok:
     665  ∀program_size: nat.
     666  ∀cost_labels: BitVectorTrie costlabel 16.
     667  ∀trace_ends_flag.
     668  ∀start_status: Status.
     669  ∀final_status: Status.
     670  ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
     671  let code_memory ≝ code_memory … start_status in
     672  let program_counter ≝ program_counter … start_status in
     673  ∀reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter.
     674  ∀good_program_witness: good_program code_memory program_size.
     675    (∃n: nat. trace_length start_status final_status + n = program_size) ∧
     676      block_cost code_memory program_counter program_size program_size cost_labels reachable_program_counter_witness good_program_witness ? =
     677        compute_paid_trace_label_label cost_labels trace_ends_flag start_status final_status the_trace.
     678  [2:
     679    @le_plus_n_r
     680  |1:
     681    #program_size #cost_labels #trace_ends_flag #start_status #final_status
     682    #the_trace normalize nodelta
     683    #reachable_program_counter_witness #good_program_witness
     684    generalize in match start_status;
     685qed.
    478686
    479687(*
Note: See TracChangeset for help on using the changeset viewer.