Changeset 1621


Ignore:
Timestamp:
Dec 15, 2011, 10:22:59 AM (8 years ago)
Author:
mulligan
Message:

to prevent conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1606 r1621  
    9191  //
    9292qed.
    93  
    94 axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
    95   ∀m, n, o: nat.
    96     m - n ≤ m - S o → S m - n ≤ m - o.
    97 (* XXX: ^^^ false without some preconditions *)
    98 
    99 axiom m_leq_n_to_m_eq_n_or_m_lt_n:
    100   ∀n, m: nat.
    101     m ≤ n → m = n ∨ m < n.
    102 
    103 lemma strengthened_invariant:
    104   ∀code_memory: BitVectorTrie Byte 16.
    105   ∀total_program_size: nat.
    106   ∀new_program_counter: Word.
    107   ∀program_counter: Word.
    108     total_program_size ≤ code_memory_size →
    109       let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    110         Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
    111           new_program_counter = \snd (\fst (fetch … code_memory program_counter)) →
    112             nat_of_bitvector … program_counter ≤ total_program_size →
    113               nat_of_bitvector … new_program_counter ≤ total_program_size.
    114   #code_memory #total_program_size #new_program_counter #program_counter
    115   #relation_total_program_code_memory_size #end_instruction_is_ok
    116   #new_program_counter_from_fetch #program_counter_within_program
    117   >new_program_counter_from_fetch
    118   lapply (fetch code_memory program_counter) #assm
    119   cases daemon
     93   
     94definition good_program_counter: BitVectorTrie Byte 16 → Word → nat → Prop ≝
     95  λcode_memory: BitVectorTrie Byte 16.
     96  λprogram_counter: Word.
     97  λprogram_size: nat.
     98    ∃n: nat.
     99      let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in
     100        program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧
     101          nat_of_bitvector 16 program_counter ≤ program_size ∧
     102            nat_of_bitvector 16 tail_program_counter ≤ nat_of_bitvector 16 program_counter.
     103
     104definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
     105  λcode_memory: BitVectorTrie Byte 16.
     106  λprogram_counter: Word.
     107  λtotal_program_size: nat.
     108  let 〈instruction, program_counter, ticks〉 ≝ fetch code_memory program_counter in
     109    match instruction with
     110    [ RealInstruction instr ⇒
     111      match instr with
     112      [ RET                    ⇒ True
     113      | JC   relative          ⇒ True (* XXX: see below *)
     114      | JNC  relative          ⇒ True (* XXX: see below *)
     115      | JB   bit_addr relative ⇒ True
     116      | JNB  bit_addr relative ⇒ True
     117      | JBC  bit_addr relative ⇒ True
     118      | JZ   relative          ⇒ True
     119      | JNZ  relative          ⇒ True
     120      | CJNE src_trgt relative ⇒ True
     121      | DJNZ src_trgt relative ⇒ True
     122      | _                      ⇒
     123          good_program_counter code_memory program_counter total_program_size
     124      ]
     125    | LCALL addr         ⇒
     126      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
     127      [ ADDR16 addr ⇒ λaddr16: True.
     128          good_program_counter code_memory addr total_program_size ∧
     129            good_program_counter code_memory program_counter total_program_size
     130      | _ ⇒ λother: False. ⊥
     131      ] (subaddressing_modein … addr)
     132    | ACALL addr         ⇒
     133      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
     134      [ ADDR11 addr ⇒ λaddr11: True.
     135        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
     136        let 〈thr, eig〉 ≝ split … 3 8 addr in
     137        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
     138        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
     139          good_program_counter code_memory new_program_counter total_program_size ∧
     140            good_program_counter code_memory program_counter total_program_size
     141      | _ ⇒ λother: False. ⊥
     142      ] (subaddressing_modein … addr)
     143    | AJMP  addr         ⇒
     144      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
     145      [ ADDR11 addr ⇒ λaddr11: True.
     146        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
     147        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
     148        let bit ≝ get_index' … O ? nl in
     149        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
     150        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
     151        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
     152          (good_program_counter code_memory new_program_counter total_program_size) ∧
     153            (good_program_counter code_memory program_counter total_program_size)
     154      | _ ⇒ λother: False. ⊥
     155      ] (subaddressing_modein … addr)
     156    | LJMP  addr         ⇒
     157      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
     158      [ ADDR16 addr ⇒ λaddr16: True.
     159          good_program_counter code_memory addr total_program_size ∧
     160            good_program_counter code_memory program_counter total_program_size
     161      | _ ⇒ λother: False. ⊥
     162      ] (subaddressing_modein … addr)
     163    | SJMP  addr     ⇒
     164      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
     165      [ RELATIVE addr ⇒ λrelative: True.
     166        let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in
     167          good_program_counter code_memory new_program_counter total_program_size ∧
     168            good_program_counter code_memory program_counter total_program_size
     169      | _ ⇒ λother: False. ⊥
     170      ] (subaddressing_modein … addr)
     171    | JMP   addr     ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
     172    | MOVC  src trgt ⇒
     173        good_program_counter code_memory program_counter total_program_size
     174    ].
     175  cases other
    120176qed.
    121    
     177
     178axiom dubious:
     179  ∀m, n, o, p: nat.
     180    1 ≤ p → n ≤ m → m - n ≤ S o → m - (n + p) ≤ o.
     181
     182lemma subaddressing_mod_elim:
     183 ∀T:Type[2].
     184 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19,addr,p.
     185 ∀Q: addressing_mode → T → Prop.
     186 (∀w. Q (ADDR11 w) (P1 w)) →
     187  Q addr (match addr
     188     in addressing_mode
     189     return λx:addressing_mode.(is_in 1 [[addr11]] x→T)
     190     with 
     191    [ADDR11 (x:Word11) ⇒ λH:True. P1 x
     192    |ADDR16 _ ⇒ λH:False. P2 H
     193    |DIRECT _ ⇒ λH:False. P3 H
     194    |INDIRECT _ ⇒ λH:False. P4 H
     195    |EXT_INDIRECT _ ⇒ λH:False. P5 H
     196    |ACC_A ⇒ λH:False. P6 H
     197    |REGISTER _ ⇒ λH:False. P7 H
     198    |ACC_B ⇒ λH:False. P8 H
     199    |DPTR ⇒ λH:False. P9 H
     200    |DATA _ ⇒ λH:False. P10 H
     201    |DATA16 _ ⇒ λH:False. P11 H
     202    |ACC_DPTR ⇒ λH:False. P12 H
     203    |ACC_PC ⇒ λH:False. P13 H
     204    |EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
     205    |INDIRECT_DPTR ⇒ λH:False. P15 H
     206    |CARRY ⇒ λH:False. P16 H
     207    |BIT_ADDR _ ⇒ λH:False. P17 H
     208    |N_BIT_ADDR _ ⇒ λH:False. P18 H   
     209    |RELATIVE _ ⇒ λH:False. P19 H
     210    ] p).
     211 #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
     212 #P14 #P15 #P16 #P17 #P18 #P19
     213 * try #x1 try #x2 try #x3 try #x4
     214 try (@⊥ assumption) normalize @x4
     215qed.
     216
     217let rec block_cost
     218  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
     219    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     220      (good_program_witness: good_program code_memory program_counter total_program_size)
     221        on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
     222  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
     223  [ O ⇒ λbase_case. 0
     224  | S program_size' ⇒ λrecursive_case.
     225    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
     226      match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
     227      [ None   ⇒
     228        match instruction return λx. x = instruction → ? with
     229        [ RealInstruction instruction ⇒ λreal_instruction.
     230          match instruction return λx. x = instruction → ? with
     231          [ RET                    ⇒ λret.  ticks
     232          | JC   relative          ⇒ λjc.   ticks
     233          | JNC  relative          ⇒ λjnc.  ticks
     234          | JB   bit_addr relative ⇒ λjb.   ticks
     235          | JNB  bit_addr relative ⇒ λjnb.  ticks
     236          | JBC  bit_addr relative ⇒ λjbc.  ticks
     237          | JZ   relative          ⇒ λjz.   ticks
     238          | JNZ  relative          ⇒ λjnz.  ticks
     239          | CJNE src_trgt relative ⇒ λcjne. ticks
     240          | DJNZ src_trgt relative ⇒ λdjnz. ticks
     241          | _                      ⇒ λalt.
     242              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     243          ] (refl … instruction)
     244        | ACALL addr     ⇒ λacall.
     245            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     246        | AJMP  addr     ⇒ λajmp. ticks
     247        | LCALL addr     ⇒ λlcall.
     248            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     249        | LJMP  addr     ⇒ λljmp. ticks
     250        | SJMP  addr     ⇒ λsjmp. ticks
     251        | JMP   addr     ⇒ λjmp. (* XXX: actually a call due to use with fptrs *)
     252            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     253        | MOVC  src trgt ⇒ λmovc.
     254            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     255        ] (refl … instruction)
     256      | Some _ ⇒ ticks
     257      ]
     258  ].
     259  [1: -block_cost -eta62747 -program_size
     260    generalize in match good_program_witness;
     261    whd in match good_program; normalize nodelta
     262    cases FETCH normalize nodelta
     263    cases acall normalize nodelta
     264    @(subaddressing_mod_elim Prop ??????????????????? addr
     265       (subaddressing_modein ? [[addr11]] addr)
     266       (λ_.λP. P → total_program_size-nat_of_bitvector 16 program_counter'≤program_size'))
     267       
     268    cases addr #subaddressing_mode cases subaddressing_mode
     269    try (#assm #absurd normalize in absurd; cases absurd)
     270    try (#absurd normalize in absurd; cases absurd)
     271    normalize nodelta
     272    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     273    cases (split … 3 8 assm) #thr #eig normalize nodelta
     274    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
     275    #assm cases assm #ignore
     276    whd in match good_program_counter; normalize nodelta * #n * *
     277    #program_counter_eq' #program_counter_lt_total_program_size
     278    #fetch_n_leq_program_counter'
     279    lapply(dubious total_program_size (nat_of_bitvector … program_counter')
     280      program_size' ? ? ? ?)
     281    [2: assumption ]
     282  [2:
     283    (* generalize in match good_program_witness; *)
     284    whd in match good_program; normalize nodelta
     285    cases FETCH normalize nodelta
     286    cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta
     287    cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta
     288    cases acall normalize nodelta
     289    cases addr #subaddressing_mode cases subaddressing_mode
     290    try (#assm #absurd normalize in absurd; cases absurd)
     291    try (#absurd normalize in absurd; cases absurd)
     292    normalize nodelta
     293    cases instruction'
     294    try (#assm normalize nodelta)
     295    [7:
     296      #irrelevant
     297      whd in match good_program_counter; normalize nodelta
     298     
     299     
     300     
     301     
     302     
     303     
     304     
     305     
     306     
    122307(* XXX: use memoisation here in the future *)
    123308let rec block_cost
    … …  
    126311      (size_invariant: total_program_size ≤ code_memory_size)
    127312        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
    128           (final_instr_invariant:
    129             let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    130               Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
    131                 on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
     313          on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
    132314  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
    133315  [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
    134316  | S program_size ⇒ λrecursive_case.
    135     let ticks ≝ \snd (fetch … code_memory program_counter) in
    136     let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in
    137     let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in
    138     match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
    139     [ None ⇒
    140         match ASM_classify0 instr with
    141         [ cl_jump ⇒ ticks
    142         | cl_call ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    143         | cl_return ⇒ ticks
    144         | cl_other ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    145         ]
    146     | Some _ ⇒ ticks
    147     ]
     317    let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
     318      match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
     319      [ None ⇒
     320          let classify ≝ ASM_classify0 instr in
     321          match classify return λx. classify = x → ? with
     322          [ cl_jump ⇒ λclassify_refl. ticks
     323          | cl_call ⇒ λclassify_refl. (* ite here *)
     324              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
     325          | cl_return ⇒ λclassify_refl. ticks
     326          | cl_other ⇒ λclassify_refl. (* ite here *)
     327              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
     328          ] (refl … classify)
     329        | Some _ ⇒ ticks
     330      ]
    148331  ].
    149   [1,3:
    150     lapply(sig2 ? ? (fetch code_memory program_counter))
    151     change with (
    152       nat_of_bitvector … newpc
    153     ) in ⊢ (??% → ?);
    154  
    155  
    156  
    157   [1:
    158     cases(lt_to_not_zero … absurd)
    159   |2,4:
    160     cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)
    161     [1,3:
    162       normalize nodelta in match newpc;
    163       lapply(sig2 ? ? (fetch code_memory program_counter))
    164       [*: #assm assumption ]
    165     |2,4:
    166       #first_lt_assm
    167     ]
    168    
    169    
    170   |3,5:
    171     lapply(sig2
    172       normalize in recursive_case;
    173       change with (
    174         S (total_program_size - nat_of_bitvector … newpc) ≤ program_size)
    175       lapply (le_S_S_to_le … recursive_case)
    176       change with (
    177         initial_program_size - (nat_of_bitvector … pc) ≤ program_size
    178       ) in ⊢ (% → ?);
    179       #second_le_assm
    180       @(transitive_le
    181         (S (initial_program_size-nat_of_bitvector 16 newpc))
    182         (initial_program_size-nat_of_bitvector_aux 16 O pc)
    183         program_size ? second_le_assm)
    184       change with (
    185         initial_program_size - nat_of_bitvector … pc
    186       ) in ⊢ (??%);
    187       lapply (minus_Sn_m (nat_of_bitvector … newpc) initial_program_size)
    188       #assm <assm in ⊢ (?%?);
    189       [1,3:
    190         @minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o
    191         @monotonic_le_minus_r
    192         assumption
    193       |2,4:
    194         @(strengthened_invariant mem initial_program_size newpc pc size_invariant final_instr_invariant)
    195         [1,3:
    196           %
    197         |2,4:
    198           assumption
    199         ]
    200       ]
    201     ]
    202   |3,5:
    203   ]
    204 qed.
    205332
    206333let rec traverse_code_internal
Note: See TracChangeset for help on using the changeset viewer.