Changeset 1650


Ignore:
Timestamp:
Jan 19, 2012, 4:56:17 PM (6 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!

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1648 r1650  
    106106  cases other
    107107qed.
    108 
    109 lemma is_in_tl_to_is_in_cons_hd_tl:
    110   ∀n: nat.
    111   ∀the_vect: Vector addressing_mode_tag n.
    112   ∀h: addressing_mode_tag.
    113   ∀element: addressing_mode.
    114     is_in n the_vect element → is_in (S n) (h:::the_vect) element.
    115   #n #the_vect #h #element #assm
    116   normalize cases (is_a h element) normalize nodelta
    117   //
    118 qed.
    119 
    120 lemma is_in_singleton_to_is_a:
    121   ∀tag.
    122   ∀element.
    123     is_in … [[tag]] element → is_a tag element.
    124   #tag #element
    125   normalize in ⊢ (% → ?);
    126   cases (is_a tag element)
    127   [1:
    128     normalize nodelta #irrelevant
    129     @I
    130   |2:
    131     normalize nodelta #absurd
    132     cases absurd
    133   ]
    134 qed.
    135108       
    136109lemma is_a_decidable:
     
    150123qed.
    151124
    152 (*
    153 lemma is_in_cons_hd_tl_to_is_in_tl:
     125lemma eq_a_elim:
     126  ∀tag.
     127  ∀hd.
     128  ∀P: bool → Prop.
     129    (tag = hd → P (true)) →
     130      (tag ≠ hd → P (false)) →
     131        P (eq_a tag hd).
     132  #tag #hd #P
     133  cases tag
     134  cases hd
     135  #true_hyp #false_hyp
     136  try @false_hyp
     137  try @true_hyp
     138  try %
     139  #absurd destruct(absurd)
     140qed.
     141 
     142lemma is_a_true_to_is_in:
    154143  ∀n: nat.
    155   ∀the_vect: Vector addressing_mode_tag n.
    156   ∀h: addressing_mode_tag.
    157   ∀element: addressing_mode.
    158     is_in (S n) (h:::the_vect) element →
    159       is_in n the_vect element. *)
     144  ∀x: addressing_mode.
     145  ∀tag: addressing_mode_tag.
     146  ∀supervector: Vector addressing_mode_tag n.
     147  mem addressing_mode_tag eq_a n supervector tag →
     148    is_a tag x = true →
     149      is_in … supervector x.
     150  #n #x #tag #supervector
     151  elim supervector
     152  [1:
     153    #absurd cases absurd
     154  |2:
     155    #n' #hd #tl #inductive_hypothesis
     156    whd in match (mem … eq_a (S n') (hd:::tl) tag);
     157    @eq_a_elim normalize nodelta
     158    [1:
     159      #tag_hd_eq #irrelevant
     160      whd in match (is_in (S n') (hd:::tl) x);
     161      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
     162      @I
     163    |2:
     164      #tag_hd_neq
     165      whd in match (is_in (S n') (hd:::tl) x);
     166      change with (
     167        mem … eq_a n' tl tag)
     168          in match (fold_right … n' ? false tl);
     169      #mem_hyp #is_a_hyp
     170      cases(is_a hd x)
     171      [1:
     172        normalize nodelta //
     173      |2:
     174        normalize nodelta
     175        @inductive_hypothesis assumption
     176      ]
     177    ]
     178  ]
     179qed.
    160180
    161181lemma is_in_subvector_is_in_supervector:
     
    166186    subvector_with … eq_a subvector supervector →
    167187      is_in m subvector element → is_in n supervector element.
    168   (*
    169188  #m #n #subvector #supervector #element
    170189  elim subvector
     
    173192    cases is_in_proof
    174193  |2:
    175     #n #hd #tl #inductive_hypothesis
    176     cases supervector
     194    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
     195    whd in match (is_in … (hd':::tl') element);
     196    cases (is_a_decidable hd' element)
    177197    [1:
    178       #subvector_with_proof #is_in_proof
    179       cases subvector_with_proof
    180     |2:
    181       #n' #hd' #tl' #subvector_with_proof #is_in_proof
    182       whd in match (is_in … (hd':::tl') element);
    183       cases (is_a_decidable hd' element)
    184       [1:
    185         #is_a_true >is_a_true normalize nodelta
    186         @I
    187       |2:
    188         #is_a_false >is_a_false normalize nodelta
    189         @inductive_hypothesis'
    190         [2:
    191           assumption
    192         |1:
    193         ]
    194       ]     
    195     ]
    196   ]
    197 qed.
    198   |3:
    199     #n #hd #tl #inductive_hypothesis
    200     #subvector_with_proof #is_in_proof
    201     @inductive_hypothesis
    202     [1:
    203       assumption
    204   |4:
    205   ]
    206 qed.
    207  
    208  
    209  
    210   [1:
    211     #n #supervector #subvector_proof #is_in_proof
    212     cases is_in_proof
    213   |2:
    214     #m' #hd #tl #inductive_hypothesis #n' #supervector
    215     #subvector_proof #is_in_proof
    216     generalize in match is_in_proof;
    217     cases(is_a_decidable hd element)
    218     whd in match (is_in … (hd:::tl) element);
    219     [1:
    220       #is_a_true >is_a_true normalize nodelta
     198      #is_a_true >is_a_true
    221199      #irrelevant
     200      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
     201      @(is_a_true_to_is_in … is_a_true)
     202      lapply(subvector_with_proof)
     203      cases(mem … eq_a n supervector hd') //
    222204    |2:
    223205      #is_a_false >is_a_false normalize nodelta
     
    225207      @inductive_hypothesis
    226208      [1:
    227         generalize in match subvector_proof;
    228         whd in match (subvector_with … eq_a (hd:::tl) supervector);
    229         cases(mem_decidable n' supervector hd)
     209        generalize in match subvector_with_proof;
     210        whd in match (subvector_with … eq_a (hd':::tl') supervector);
     211        cases(mem_decidable n supervector hd')
    230212        [1:
    231213          #mem_true >mem_true normalize nodelta
     
    239221      ]
    240222    ]
    241    
    242    
    243    
    244    
    245     generalize in match subvector_proof;
    246     whd in match (subvector_with … eq_a (hd:::tl) supervector);
    247     cases(mem_decidable n' supervector hd)
    248     [1:
    249       #mem_true >mem_true normalize nodelta
    250       #subvector_with_proof
    251       @inductive_hypothesis
    252       [1:
    253         assumption
    254       |2:
    255         generalize in match is_in_proof;
    256         whd in match (is_in (S m') (hd:::tl) element);
    257         cases(is_a_decidable hd element)
    258         [1:
    259           #is_a_true >is_a_true normalize nodelta
    260           #irrelevant
    261           whd whd in match (is_in … tl element);
    262         |2:
    263           #is_a_false >is_a_false normalize nodelta
    264           #assm assumption
    265         ]
    266       ]
    267     |2:
    268       #mem_false >mem_false normalize nodelta
    269       #absurd cases absurd
    270     ]
    271     |1:
    272       normalize nodelta #subvector_with_assm
    273       cases(is_a_decidable hd element)
    274       [1:
    275         #is_a_hd
    276         generalize in match subvector_proof;
    277         whd in match (subvector_with … eq_a (hd:::tl) supervector);
    278       |2:
    279         #not_is_a_hd
    280       ]
    281     ]
    282   ] *)
    283   cases daemon
     223  ]
    284224qed.
    285225
     
    417357      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    418358
    419 (*
    420 lemma subaddressing_mode_elim:
    421   ∀T:Type[2].
    422   ∀P1: Word11 → T.
    423   ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
    424   ∀addr: addressing_mode.
    425   ∀p: is_in 1 [[ addr11 ]] addr.
    426   ∀Q: addressing_mode → T → Prop.
    427     (∀w. Q (ADDR11 w) (P1 w)) →
    428       Q addr (
    429         match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 
    430         [ ADDR11 (x:Word11) ⇒ λH:True. P1 x
    431         | ADDR16 _ ⇒ λH:False. P2 H
    432         | DIRECT _ ⇒ λH:False. P3 H
    433         | INDIRECT _ ⇒ λH:False. P4 H
    434         | EXT_INDIRECT _ ⇒ λH:False. P5 H
    435         | ACC_A ⇒ λH:False. P6 H
    436         | REGISTER _ ⇒ λH:False. P7 H
    437         | ACC_B ⇒ λH:False. P8 H
    438         | DPTR ⇒ λH:False. P9 H
    439         | DATA _ ⇒ λH:False. P10 H
    440         | DATA16 _ ⇒ λH:False. P11 H
    441         | ACC_DPTR ⇒ λH:False. P12 H
    442         | ACC_PC ⇒ λH:False. P13 H
    443         | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
    444         | INDIRECT_DPTR ⇒ λH:False. P15 H
    445         | CARRY ⇒ λH:False. P16 H
    446         | BIT_ADDR _ ⇒ λH:False. P17 H
    447         | N_BIT_ADDR _ ⇒ λH:False. P18 H   
    448         | RELATIVE _ ⇒ λH:False. P19 H
    449         ] p).
    450   #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    451   #P14 #P15 #P16 #P17 #P18 #P19
    452   * try #x1 try #x2 try #x3 try #x4
    453   try (@⊥ assumption) normalize @x4
    454 qed. *)
    455 
    456359include alias "arithmetics/nat.ma".
    457360
    458 let rec block_cost
     361let rec block_cost'
    459362  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    460363    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    461364      (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter)
    462         (good_program_witness: good_program code_memory total_program_size)
     365        (good_program_witness: good_program code_memory total_program_size) (first_time_around: bool)
    463366          on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
    464367  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
     
    466369  | S program_size' ⇒ λrecursive_case.
    467370    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
    468       match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
    469       [ None   ⇒
     371    let to_continue ≝
     372      match lookup_opt … program_counter' cost_labels with
     373      [ None ⇒ true
     374      | Some _ ⇒ first_time_around
     375      ]
     376    in
     377      if to_continue then
    470378        match instruction return λx. x = instruction → ? with
    471379        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
     
    482390          | DJNZ src_trgt relative ⇒ λinstr. ticks
    483391          | _                      ⇒ λinstr.
    484               ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     392              ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    485393          ] (refl … real_instruction)
    486394        | ACALL addr     ⇒ λinstr.
    487             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     395            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    488396        | AJMP  addr     ⇒ λinstr. ticks
    489397        | LCALL addr     ⇒ λinstr.
    490             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     398            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    491399        | LJMP  addr     ⇒ λinstr. ticks
    492400        | SJMP  addr     ⇒ λinstr. ticks
    493401        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    494             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     402            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    495403        | MOVC  src trgt ⇒ λinstr.
    496             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     404            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    497405        ] (refl … instruction)
    498       | Some _ ⇒ ticks
    499       ]
     406      else
     407        0
    500408  ].
    501409  [1:
     
    635543qed.
    636544
     545definition block_cost ≝
     546  λcode_memory: BitVectorTrie Byte 16.
     547  λprogram_counter: Word.
     548  λtotal_program_size: nat.
     549  λcost_labels: BitVectorTrie costlabel 16.
     550  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
     551  λgood_program_witness: good_program code_memory total_program_size.
     552    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
     553      reachable_program_counter_witness good_program_witness true ?.
     554  @le_plus_n_r
     555qed.
     556
    637557lemma fetch_program_counter_n_Sn:
    638558  ∀instruction: instruction.
     
    672592    [ None ⇒ λlookup_refl. cost_mapping
    673593    | Some lbl ⇒ λlookup_refl.
    674       let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size cost_labels ? good_program_witness ? in
     594      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
    675595        add … cost_mapping lbl cost
    676596    ] (refl … (lookup_opt … program_counter cost_labels))
     
    680600    assumption
    681601  |2:
    682     //
    683   |3:
    684602    assumption
    685603  ]
  • 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.