Changeset 1921


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

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

Location:
src
Files:
4 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
  • src/ASM/ASMCostsSplit.ma

    r1919 r1921  
    4040       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    4141        λ${ident E}.$s ] ] (refl ? $t) }.
     42
     43definition nat_of_bool: bool → nat ≝
     44  λb: bool.
     45  match b with
     46  [ true ⇒ 1
     47  | false ⇒ 0
     48  ].
     49
     50lemma blah:
     51  ∀n: nat.
     52  ∀bv: BitVector n.
     53  ∀buffer: nat.
     54    nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
     55  #n #bv elim bv
     56  [1:
     57    #buffer elim buffer try %
     58    #buffer' #inductive_hypothesis
     59    normalize <times_n_1 %
     60  |2:
     61    #n' #hd #tl #inductive_hypothesis
     62    #buffer cases hd normalize
     63    >inductive_hypothesis
     64    >inductive_hypothesis
     65    [1:
     66      change with (
     67        ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
     68      change with (
     69        ? + buffer * (2 * 2^n')) in ⊢ (???%);
     70      cases daemon
     71    ]
     72  ]
     73  cases daemon
     74qed.
     75
     76lemma nat_of_bitvector_aux_hd_tl:
     77  ∀n: nat.
     78  ∀tl: BitVector n.
     79  ∀hd: bool.
     80    nat_of_bitvector (S n) (hd:::tl) =
     81      nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
     82  #n #tl elim tl
     83  [1:
     84    #hd cases hd %
     85  |2:
     86    #n' #hd' #tl' #inductive_hypothesis #hd
     87    cases hd whd in ⊢ (??%?); normalize nodelta
     88    >inductive_hypothesis cases hd' normalize nodelta
     89    normalize in match (nat_of_bool ?);
     90    normalize in match (nat_of_bool ?);
     91    [4:
     92      normalize in match (2 * ?);
     93      <plus_n_O <plus_n_O %
     94    |3:
     95      normalize in match (2 * ?);
     96      normalize in match (0 + 1);
     97      <plus_n_O
     98      normalize in match (1 * ?);
     99      <plus_n_O
     100      cases daemon
     101      (* XXX: lemma *)
     102    |*:
     103      cases daemon
     104    ]
     105  ]
     106qed.
    42107
    43108lemma succ_nat_of_bitvector_aux_half_add_1:
     
    74139qed.
    75140   
     141include alias "arithmetics/nat.ma".
     142include alias "basics/logic.ma".
     143   
    76144let rec traverse_code_internal
    77145  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    89157            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
    90158              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    91                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     159                pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    92160  match program_size return λx. x = program_size → Σcost_map: ?. ? with
    93161  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
     
    98166    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    99167    | Some lbl ⇒ λlookup_refl.
    100       let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
     168      let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in
    101169        add … cost_mapping lbl cost
    102170    ] (refl … (lookup_opt … program_counter cost_labels))
     
    395463      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    396464        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
    397           pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     465          pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    398466  λcode_memory: BitVectorTrie Byte 16.
    399467  λcost_labels: BitVectorTrie costlabel 16.
  • src/ASM/CostsProof.ma

    r1919 r1921  
    594594(* XXX: here *)
    595595let rec compute_trace_label_return_using_paid_ok_with_trace
    596  (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     596 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
     597 (good_program_witness: good_program cm total_program_size)
    597598 (cost_labels: BitVectorTrie costlabel 16)
    598599 (cost_map: identifier_map CostTag nat)
     
    601602 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    602603 on trace:
     604 ∀unrepeating_witness: tlr_unrepeating … trace.
    603605 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    604606   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    605    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     607   pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
    606608  let ctrace ≝ compute_cost_trace_label_return cm … trace in
    607609  compute_trace_label_return_cost_using_paid cm … trace =
     
    609611    ≝ ?
    610612and compute_trace_any_label_using_paid_ok_with_trace
    611  (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     613 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
     614 (good_program_witness: good_program cm total_program_size)
    612615 (cost_labels: BitVectorTrie costlabel 16)
    613616 (trace_ends_flag: trace_ends_with_ret)
     
    618621 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    619622   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    620    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     623   pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
    621624 on trace:
     625  ∀unrepeating_witness: tal_unrepeating … trace.
    622626  let ctrace ≝ compute_cost_trace_any_label … trace in
    623627  compute_trace_any_label_cost_using_paid … trace =
     
    625629    ≝ ?
    626630and compute_trace_label_label_using_paid_ok_with_trace
    627  (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     631 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
     632 (good_program_witness: good_program cm total_program_size)
    628633 (cost_labels: BitVectorTrie costlabel 16)
    629634 (trace_ends_flag: trace_ends_with_ret)
     
    631636 (initial: Status cm) (final: Status cm)
    632637 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     638 (unrepeating_witness: tll_unrepeating … trace)
    633639 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    634640 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    635641   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    636    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     642   pi1 … (block_cost cm pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
    637643 on trace:
     644 ∀unrepeating_witness: tll_unrepeating … trace.
    638645  let ctrace ≝ compute_cost_trace_label_label … trace in
    639646  compute_trace_label_label_cost_using_paid … trace =
     
    641648    ≝ ?.
    642649  cases trace normalize nodelta
    643   [ #sb #sa #tr #dom_codom whd in ⊢ (??%?);
     650  [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
    644651    whd in match (compute_cost_trace_label_return ?????);
    645     @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness) @dom_codom
    646   | #si #sl #sf #tr1 #tr2 #dom_codom
     652    @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness)
     653    assumption
     654  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    647655    whd in ⊢ (??%?);
    648656    whd in match (compute_cost_trace_label_return ?????);
    649657    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    650     [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     658    [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
    651659      -compute_trace_label_return_using_paid_ok_with_trace
    652       @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
     660      [1:
     661        @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
     662      |2:
     663        inversion unrepeating_witness
     664        #tll_unrepeating #tlr_unrepeating #_ assumption
     665      ]
    653666    | >(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    654667      -compute_trace_label_label_using_paid_ok_with_trace
    655       @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H)
     668      [1:
     669        @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H)
     670      |2,3:
     671        inversion unrepeating_witness
     672        #tll_unrepeating #tlr_unrepeating #_ assumption
     673      ]
    656674    ]
    657675  |8:
    658676    #end_flag #start_status #end_status #trace_any_label #costed_assm
     677    #unrepeating_witness
    659678    whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
    660679    >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    661     >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
    662680    [1:
    663       @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
    664       <(tech_cost_of_label_shift ??? [?] ? i) //
     681      >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
     682      [1:
     683        @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
     684        <(tech_cost_of_label_shift ??? [?] ? i) //
     685      |2:
     686        change with (? = lookup_present ? ? ? ? ?)
     687        generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
     688        normalize in match (nth_safe ? ? ? ?);
     689        whd in costed_assm; lapply costed_assm -costed_assm   
     690        inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
     691        [1:
     692          #_ #absurd cases absurd
     693        |2:
     694          normalize nodelta #cost_label #Some_assm #_ #p
     695          cases (dom_codom ? p ? Some_assm)
     696          #reachable_witness #block_cost_assm <block_cost_assm
     697          cases (block_cost ???????)
     698          #cost -block_cost_assm #block_cost_assm
     699          cases (block_cost_assm ??? trace_any_label ???)
     700          try @refl
     701          [1:
     702            assumption
     703          |2:
     704            (* XXX: !!! *)
     705            cases daemon
     706          ]
     707        ]
     708      ]
    665709    |2:
    666       change with (? = lookup_present ? ? ? ? ?)
    667       generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    668       normalize in match (nth_safe ? ? ? ?);
    669       whd in costed_assm; lapply costed_assm -costed_assm   
    670       inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
    671       [1:
    672         #_ #absurd cases absurd
    673       |2:
    674         normalize nodelta #cost_label #Some_assm #_ #p
    675         cases (dom_codom ? p ? Some_assm)
    676         #reachable_witness #block_cost_assm <block_cost_assm
    677         cases (block_cost ? ? ? ? ? ?)
    678         #cost -block_cost_assm #block_cost_assm
    679         cases (block_cost_assm ? ? ? trace_any_label ? (refl …))
    680         try % (* XXX: assumption about length of trace *) cases daemon
    681       ]
     710      assumption
    682711    ]
    683712  |3:
    684713    #start_status #final_status #execute_assm #classifier_assm #costed_assm
     714    #unrepeating_witness
    685715    %
    686716  |4:
    687     #start_status #final_status #execute_assm #classifier_assm %
     717    #start_status #final_status #execute_assm #classifier_assm #unrepeating_witness
     718    %
    688719  |5:
    689720    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    690     #classifier_assm #after_return_assm #trace_label_return #costed_assm
     721    #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness
    691722    whd in ⊢ (??%?);
    692     @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     723    @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     724    assumption
    693725  |6:
    694726    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    695727    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    696     #costed_assm #trace_any_label
     728    #costed_assm #trace_any_label #unrepeating_witness
    697729    whd in ⊢ (??%?);
    698     >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
    699     >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    700     >length_append >bigop_sum_rev >commutative_plus @eq_f2
    701     [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
    702                   |1: #i #H % ]
    703     | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     730    >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom ? dom_codom)
     731    [1:
     732      >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     733      [1:
     734        >length_append >bigop_sum_rev >commutative_plus @eq_f2
     735        [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
     736                      |1: #i #H % ]
     737        | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     738        ]
     739      |2:
     740        inversion unrepeating_witness
     741        * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
     742      ]
     743    |2:
     744      inversion unrepeating_witness
     745      * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
    704746    ]
    705747  |7:
    706748    #end_flag #status_pre_fun_call #status_start_fun_call #status_final
    707     #execute_assm #trace_any_label #classifier_assm #costed_assm
     749    #execute_assm #trace_any_label #classifier_assm #costed_assm #unrepeating_witness
    708750    whd in ⊢ (??%?);
    709751    @(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     752    inversion unrepeating_witness
     753    #memb_1 #tal_unrepeating #_ assumption
    710754  ]
    711755qed.
     
    714758  ∀code_memory: BitVectorTrie Byte 16.
    715759  ∀total_program_size: nat.
     760  ∀total_program_size_limit: total_program_size ≤ 2^16.
    716761  ∀good_program_witness: good_program code_memory total_program_size.
    717762  ∀cost_labels: BitVectorTrie costlabel 16.
     
    720765  ∀final: Status code_memory.
    721766  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     767  ∀unrepeating_witness: tlr_unrepeating … trace.
    722768  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    723769  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    724770    ∃reachable_witness: reachable_program_counter code_memory total_program_size pc.
    725       pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     771      pi1 … (block_cost code_memory pc total_program_size total_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
    726772        let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
    727773          clock … code_memory … final =
    728774            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
    729   #code_memory #total_program_size #good_program_witness #cost_labels #cost_map
    730   #initial #final #trace #codom_dom #dom_codom normalize nodelta
     775  #code_memory #total_program_size #total_program_size_limit
     776  #good_program_witness #cost_labels #cost_map
     777  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    731778  <compute_trace_label_return_using_paid_ok_with_trace try assumption
    732779  >commutative_plus >compute_trace_label_return_cost_using_paid_ok //
     
    751798  ∀final: Status code_memory.
    752799  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     800  ∀unrepeating_witness: tlr_unrepeating … trace.
    753801    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant
    754802      reachable_program_counter_witness good_program_witness in
     
    758806    #code_memory #total_program_size #total_program_size_invariant #good_program_witness
    759807    #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace
     808    #unrepeating_witness
    760809    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    761810  |2:
  • src/common/StructuredTraces.ma

    r1918 r1921  
    1212
    1313record abstract_status : Type[1] ≝
    14   { as_status :> Type[0]
     14{   
     15    as_status :> Type[0]
    1516  ; as_execute : as_status → as_status → Prop
    1617  ; as_pc : DeqSet
     
    112113 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
    113114 ].
     115 
     116definition as_trace_any_label_length':
     117    ∀S: abstract_status.
     118    ∀trace_ends_flag: trace_ends_with_ret.
     119    ∀start_status: S.
     120    ∀final_status: S.
     121    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
     122      nat ≝
     123  λS: abstract_status.
     124  λtrace_ends_flag: trace_ends_with_ret.
     125  λstart_status: S.
     126  λfinal_status: S.
     127  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
     128    |tal_pc_list … the_trace|.
    114129
    115130let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
     
    131146    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    132147    tal_unrepeating … tl
     148  | tal_base_call status_pre_fun_call status_start_fun_call status_final _ _ _
     149      fun_call_trace _ ⇒ tlr_unrepeating … fun_call_trace
    133150  | _ ⇒ True
    134151  ].
Note: See TracChangeset for help on using the changeset viewer.