Changeset 1921 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 8, 2012, 3:29:25 PM (8 years ago)
Author:
mulligan
Message:

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1919 r1921  
    113113      program_counter ? code_memory after = program_counter_after.
    114114
     115lemma eq_bv_true_to_refl:
     116  ∀n: nat.
     117  ∀x: BitVector n.
     118  ∀y: BitVector n.
     119    eq_bv n x y = true → x = y.
     120  #n #x #y
     121  cases daemon (* XXX: !!! *)
     122qed.
     123
     124lemma refl_to_eq_bv_true:
     125  ∀n: nat.
     126  ∀x: BitVector n.
     127  ∀y: BitVector n.
     128    x = y → eq_bv n x y = true.
     129  #n #x #y #refl destruct /2/
     130qed.
     131
     132corollary refl_iff_eq_bv_true:
     133  ∀n: nat.
     134  ∀x: BitVector n.
     135  ∀y: BitVector n.
     136    eq_bv n x y = true ↔ x = y.
     137  #n #x #y whd in match iff; normalize nodelta
     138  @conj /2/
     139qed.
     140
     141definition word_deqset: DeqSet ≝
     142  mk_DeqSet Word (eq_bv 16) ?.
     143  @refl_iff_eq_bv_true
     144qed.
     145
    115146definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    116147  λcode_memory.
     
    119150      (Status code_memory)
    120151      (λs,s'. (execute_1 … s) = s')
    121       ?
    122       ?
     152      word_deqset
     153      (program_counter …)
    123154      (λs,class. ASM_classify … s = class)
    124155      (current_instruction_is_labelled … cost_labels)
    125156      (next_instruction_properly_relates_program_counters code_memory)
    126157      ?.
    127   cases daemon (* XXX: new additions to abstract status record *)
     158  cases daemon (* XXX: is final predicate *)
    128159qed.
    129160
     
    156187  λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status.
    157188    as_trace_any_label_length' … the_trace.
     189
     190let rec all_program_counter_list
     191  (n: nat)
     192    on n ≝
     193  match n with
     194  [ O ⇒ [ ]
     195  | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
     196  ].
     197
     198lemma all_program_counter_list_bound_eq:
     199  ∀bound: nat.
     200    |all_program_counter_list bound| = bound.
     201  #bound elim bound try %
     202  #bound' #inductive_hypothesis normalize
     203  >inductive_hypothesis %
     204qed.
     205
     206axiom nat_of_bitvector_bitvector_of_nat_inverse:
     207  ∀n: nat.
     208  ∀b: nat.
     209    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
     210
     211axiom bitvector_of_nat_inverse_nat_of_bitvector:
     212  ∀n: nat.
     213  ∀b: BitVector n.
     214    bitvector_of_nat n (nat_of_bitvector n b) = b.
     215
     216lemma mem_all_program_counter_list_lt_bound:
     217  ∀bound: nat.
     218  ∀bound_proof: bound ≤ 2^16.
     219  ∀e: Word.
     220    memb word_deqset e (all_program_counter_list bound) = true →
     221      nat_of_bitvector … e < bound.
     222  #bound elim bound
     223  [1:
     224    #bound_proof #e
     225    normalize #absurd destruct(absurd)
     226  |2:
     227    #bound' #inductive_hypothesis
     228    #bound_proof #e
     229    change with (if eq_bv ??? then ? else ? = ? → ?)
     230    @eq_bv_elim
     231    [1:
     232      #eq_assm
     233      normalize nodelta destruct #_
     234      >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     235      normalize %
     236    |2:
     237      #neq_assm normalize nodelta
     238      #memb_assm %2 @inductive_hypothesis
     239      try assumption
     240      @(transitive_le bound' (S bound'))
     241      try assumption %2 %
     242    ]
     243  ]
     244qed.
     245
     246lemma lt_bound_mem_all_program_counter_list:
     247  ∀bound: nat.
     248  ∀bound_proof: bound ≤ 2^16.
     249  ∀e: Word.
     250    nat_of_bitvector … e < bound →
     251      memb word_deqset e (all_program_counter_list bound) = true.
     252  #bound elim bound
     253  [1:
     254    #bound_proof #e normalize
     255    #absurd cases (lt_to_not_zero … absurd)
     256  |2:
     257    #bound' #inductive_hypothesis
     258    #bound_proof #e
     259    change with (? → if eq_bv ??? then ? else ? = ?)
     260    #assm
     261    cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
     262    [1:
     263      #e_lt_assm
     264      @eq_bv_elim
     265      [1:
     266        #eq_assm normalize nodelta %
     267      |2:
     268        #neq_assm normalize nodelta
     269        @inductive_hypothesis try assumption
     270        @(transitive_le bound' (S bound')) try assumption
     271        %2 %
     272      ]
     273    |2:
     274      #relevant >eq_eq_bv normalize nodelta try %
     275      destruct >bitvector_of_nat_inverse_nat_of_bitvector %
     276    |3:
     277      normalize in assm;
     278      @le_S_S_to_le assumption
     279    ]
     280  ]
     281qed.
     282
     283include alias "arithmetics/nat.ma".
     284
     285lemma fetch_program_counter_n_Sn:
     286  ∀instruction: instruction.
     287  ∀program_counter, program_counter': Word.
     288  ∀ticks, n: nat.
     289  ∀code_memory: BitVectorTrie Byte 16.
     290    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
     291      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
     292        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
     293          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
     294  #instruction #program_counter #program_counter' #ticks #n #code_memory
     295  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
     296  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
     297  <fetch_program_counter_n_hyp normalize nodelta
     298  <fetch_hyp normalize nodelta
     299  change with (
     300    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
     301  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
     302  >(le_to_leb_true … lt_hyp) %
     303qed.
     304
     305(* XXX: indexing bug *)
     306lemma execute_1_and_program_counter_after_other_in_lockstep:
     307  ∀code_memory: BitVectorTrie Byte 16.
     308  ∀start_status: Status code_memory.
     309    ASM_classify code_memory start_status = cl_other →
     310      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     311        program_counter ? ? (execute_1 … start_status) =
     312          program_counter_after_other pc instruction.
     313  #code_memory #start_status #classify_assm
     314  whd in match execute_1; normalize nodelta
     315  cases (execute_1' code_memory start_status) #the_status
     316  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
     317  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
     318  #classify_assm #classify_assm' @classify_assm' assumption
     319qed-.
     320
     321let rec tal_pc_list_lt_total_program_size
     322  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     323    (total_program_size: nat) (total_program_size_invariant: total_program_size ≤ 2^16)
     324      (good_program_witness: good_program code_memory total_program_size)
     325        (start: Status code_memory) (final: Status code_memory) (trace_ends_flag: trace_ends_with_ret)
     326          (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final)
     327            (pc: as_pc (ASM_abstract_status code_memory cost_labels))
     328              on the_trace:
     329  reachable_program_counter code_memory total_program_size (program_counter … start) →
     330    memb word_deqset pc (tal_pc_list (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace) = true →
     331      nat_of_bitvector 16 pc<total_program_size ≝
     332  match the_trace with
     333  [ tal_base_not_return the_status _ _ _ _ ⇒ ?
     334  | tal_base_return the_status _ _ _ ⇒ ?
     335  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ ?
     336  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     337     _ classifier after_return call_trace _ final_trace ⇒ ?
     338  | tal_step_default end_flag status_pre status_init status_end execute tail_trace classifier _ ⇒ ?
     339  ].
     340  #reachable_program_counter_witness
     341  whd in ⊢ (??%? → ?); @(bool_inv_ind … (pc==as_pc_of (ASM_abstract_status code_memory cost_labels) ?))
     342  normalize nodelta #eq_assm cases reachable_program_counter_witness
     343  [1,3,5,7,9:
     344    >(eq_bv_eq … eq_assm) #_ #relevant #_
     345    assumption
     346  |2,4,6:
     347    #_ #_ #absurd
     348    normalize in absurd; destruct(absurd)
     349  |8:
     350    #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption
     351    whd in after_return;
     352    lapply after_return
     353    @pair_elim * normalize nodelta #instruction #pc' #ticks
     354    #fetch_eq #pc_assm' >pc_assm'
     355    lapply (good_program_witness ? reachable_program_counter_witness)
     356    whd in classifier; whd in classifier:(??%?);
     357    whd in match (current_instruction ??) in classifier;
     358    whd in match current_instruction0 in classifier;
     359    >fetch_eq in classifier;
     360    normalize nodelta cases instruction
     361    normalize nodelta -tal_pc_list_lt_total_program_size
     362    [8:
     363      #preinstruction elim preinstruction
     364      normalize in match (? = cl_call);
     365    ]
     366    try (#assm1 #assm2 #absurd destruct(absurd) @I)
     367    try (#assm1 #absurd destruct(absurd) @I)
     368    try (#absurd destruct(absurd) @I)
     369    [1:
     370      #addr #_
     371      @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ]
     372      #w
     373      @pair_elim #lft #rgt @pair_elim #lft' #rgt' @pair_elim #lft'' #rgt''
     374      #_ #_ #_ * * #_
     375    |2:
     376      #addr #_
     377      @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ]
     378      #w * * #_
     379    |3:
     380      #addr #_ *
     381    ]
     382    #relevant #pc_tps_assm'
     383    whd cases reachable_program_counter_witness * #n
     384    #Some_assm #_ % try assumption
     385    %{(S n)}
     386    @(fetch_program_counter_n_Sn … Some_assm (sym_eq … fetch_eq))
     387    assumption
     388  |10:
     389    #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption -tal_pc_list_lt_total_program_size
     390    lapply (execute_1_and_program_counter_after_other_in_lockstep … status_pre classifier)
     391    @pair_elim * #instruction #pc #ticks normalize nodelta
     392    #fetch_eq whd in match program_counter_after_other; normalize nodelta
     393    lapply (good_program_witness … reachable_program_counter_witness)
     394    whd in classifier; whd in classifier:(??%?);
     395    whd in match (current_instruction ??) in classifier;
     396    whd in match current_instruction0 in classifier;
     397    >fetch_eq in classifier; normalize nodelta cases instruction
     398    normalize nodelta
     399    [8:
     400      #preinstruction elim preinstruction
     401      normalize in match (? = cl_other);
     402    ]
     403    try (#assm1 #assm2 #absurd destruct(absurd) @I)
     404    try (#assm1 #absurd destruct(absurd) @I)
     405    try (#absurd destruct(absurd) @I) normalize nodelta
     406    [27,28,29:
     407      #addr #_ #reachable
     408      #program_counter_execute_1_refl
     409      whd in execute; <execute
     410      >program_counter_execute_1_refl assumption
     411    |*:
     412      try (#assm1 #assm2 #_ * #relevant #pc_lt_assm)
     413      try (#assm1 #_ * #relevant #pc_lt_assm)
     414      try (#_ * #relevant #pc_lt_assm) #pc_refl
     415      cases reachable_program_counter_witness * #n
     416      #Some_assm #tps_lt_assm
     417      whd in match reachable_program_counter; normalize nodelta %
     418      try %{(S n)}
     419      whd in execute; <execute
     420      try (@(fetch_program_counter_n_Sn instruction ?? ticks ?? Some_assm ?) >execute >fetch_eq <pc_refl >execute try %)
     421      <pc_refl in relevant; <execute #assm
     422      >pc_refl >pc_refl in assm; #assm assumption
     423    ]
     424  ]
     425qed.
     426
     427lemma sublist_tal_pc_list_all_program_counter_list:
     428  ∀code_memory: BitVectorTrie Byte 16.
     429  ∀cost_labels: BitVectorTrie costlabel 16.
     430  ∀total_program_size: nat.
     431  ∀total_program_size_invariant: total_program_size ≤ 2^16.
     432  ∀good_program_witness: good_program code_memory total_program_size.
     433  ∀start, final: Status code_memory.
     434  ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
     435    (program_counter (BitVectorTrie Byte 16) code_memory start).
     436  ∀trace_ends_flag.
     437  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
     438    sublist ? (tal_pc_list … the_trace) (all_program_counter_list total_program_size).
     439  #code_memory #cost_labels #total_program_size #total_program_size_invariant
     440  #good_program_witness #start #final #reachable_program_counter_witness
     441  #trace_ends_flag #the_trace
     442  whd in match (sublist ???); #pc #memb_assm
     443  @lt_bound_mem_all_program_counter_list
     444  try assumption destruct
     445  lapply memb_assm -memb_assm
     446  @tal_pc_list_lt_total_program_size
     447  assumption
     448qed.
     449
     450corollary tal_pc_list_length_leq_total_program_size:
     451  ∀code_memory: BitVectorTrie Byte 16.
     452  ∀cost_labels: BitVectorTrie costlabel 16.
     453  ∀total_program_size: nat.
     454  ∀total_program_size_invariant: total_program_size ≤ 2^16.
     455  ∀good_program_witness: good_program code_memory total_program_size.
     456  ∀start, final: Status code_memory.
     457  ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
     458    (program_counter (BitVectorTrie Byte 16) code_memory start).
     459  ∀trace_ends_flag.
     460  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
     461  ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace.
     462    |tal_pc_list … the_trace| ≤ total_program_size.
     463  #code_memory #cost_labels #total_program_size #total_program_size_invariant
     464  #good_program_witness #start #final #reachable_program_counter_witness
     465  #trace_ends_flag #the_trace #unrepeating_witness
     466  <(all_program_counter_list_bound_eq total_program_size)
     467  @sublist_length
     468  [1:
     469    @tal_unrepeating_uniqueb
     470    assumption
     471  |2:
     472    @sublist_tal_pc_list_all_program_counter_list
     473    assumption
     474  ]
     475qed.
    158476
    159477let rec compute_paid_trace_any_label
     
    214532  #m #n #proof /2 by plus_minus/
    215533qed.
    216 
    217 (* XXX: indexing bug *)
    218 lemma execute_1_and_program_counter_after_other_in_lockstep:
    219   ∀code_memory: BitVectorTrie Byte 16.
    220   ∀start_status: Status code_memory.
    221     ASM_classify code_memory start_status = cl_other →
    222       let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    223         program_counter ? ? (execute_1 … start_status) =
    224           program_counter_after_other pc instruction.
    225   #code_memory #start_status #classify_assm
    226   whd in match execute_1; normalize nodelta
    227   cases (execute_1' code_memory start_status) #the_status
    228   * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
    229   cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
    230   #classify_assm #classify_assm' @classify_assm' assumption
    231 qed-.
    232534
    233535lemma reachable_program_counter_to_0_lt_total_program_size:
     
    8781180    ∀program_counter': Word.
    8791181    ∀total_program_size: nat.
     1182    ∀total_program_size_invariant: total_program_size ≤ 2^16.
    8801183    ∀cost_labels: BitVectorTrie costlabel 16.
    8811184    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
     
    8861189        ∀trace_ends_flag.
    8871190        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    888           trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    889             ≤ total_program_size →
     1191        ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size (program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     1192        ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace.
    8901193          program_counter' = program_counter … start_status →
    8911194            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
     
    8931196  λprogram_counter: Word.
    8941197  λtotal_program_size: nat.
     1198  λtotal_program_size_invariant: total_program_size ≤ 2^16.
    8951199  λcost_labels: BitVectorTrie costlabel 16.
    8961200  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
     
    9021206  cases(lookup_opt … cost_labels) in block_cost_hyp;
    9031207  [2: #cost_label] normalize nodelta
    904   #hyp assumption
    905 qed.
    906 
    907 lemma fetch_program_counter_n_Sn:
    908   ∀instruction: instruction.
    909   ∀program_counter, program_counter': Word.
    910   ∀ticks, n: nat.
    911   ∀code_memory: BitVectorTrie Byte 16.
    912     Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
    913       〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
    914         nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
    915           Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
    916   #instruction #program_counter #program_counter' #ticks #n #code_memory
    917   #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
    918   whd in match (fetch_program_counter_n (S n) code_memory (zero …));
    919   <fetch_program_counter_n_hyp normalize nodelta
    920   <fetch_hyp normalize nodelta
    921   change with (
    922     leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
    923   ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
    924   >(le_to_leb_true … lt_hyp) %
     1208  #hyp #start_status #final_status #trace_ends_flag #the_trace
     1209  #reachable_program_counter_witness #unrepeating_witness
     1210  @hyp @tal_pc_list_length_leq_total_program_size try assumption
    9251211qed.
    9261212
Note: See TracChangeset for help on using the changeset viewer.