Changeset 1639


Ignore:
Timestamp:
Jan 10, 2012, 5:27:41 PM (8 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1625 r1639  
    9292qed.
    9393   
    94 definition good_program_counter: BitVectorTrie Byte 16 → Word → nat → Prop ≝
     94definition good_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
    9595  λcode_memory: BitVectorTrie Byte 16.
     96  λprogram_size: nat.
    9697  λprogram_counter: Word.
    97   λprogram_size: nat.
    9898    ∃n: nat.
    9999      let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in
     
    102102            nat_of_bitvector 16 tail_program_counter < nat_of_bitvector 16 program_counter.
    103103
     104axiom half_add_zero:
     105  ∀n: nat.
     106  ∀b: BitVector n.
     107    \snd (half_add n (zero …) b) = b.
     108
     109lemma fetch_program_counter_n_half_add:
     110  ∀n: nat.
     111  ∀code_memory: BitVectorTrie Byte 16.
     112    fetch_program_counter_n (S n) code_memory (zero …) =
     113      let program_counter ≝ fetch_program_counter_n n code_memory (zero …) in
     114      let 〈instr, new_program_counter, cost〉 ≝ fetch code_memory program_counter in
     115        \snd (half_add … program_counter new_program_counter).
     116  #n #code_memory elim n
     117  [1:
     118    whd in match (fetch_program_counter_n 1 code_memory (zero …));
     119    normalize in match (fetch_program_counter_n 0 code_memory (zero …));
     120    change with (
     121      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory (zero …) in
     122        program_counter
     123    ) in ⊢ (??%?);
     124    cases (fetch code_memory (zero …)) #instr #program_counter normalize nodelta
     125    generalize in match instr; #instr
     126    cases instr #instr #program_counter normalize nodelta
     127    >half_add_zero %
     128  |2:
     129    #n' #ind_hyp
     130    whd in match (fetch_program_counter_n (S (S n')) code_memory (zero …));
     131    >ind_hyp (* XXX: things start going wrong here!
     132    generalize in match (let (program_counter:Word) ≝
     133                  fetch_program_counter_n n' code_memory (zero 16) in 
     134           let 〈eta40050,cost〉 ≝fetch code_memory program_counter in 
     135           let 〈instr,new_program_counter〉 ≝eta40050 in 
     136           \snd  (half_add 16 program_counter new_program_counter));
     137    #B normalize nodelta
     138    cases (fetch code_memory B) #instr_program_counter #cost normalize nodelta
     139    cases instr_program_counter #instr #program_counter normalize nodelta *)
     140    cases daemon
     141  ]
     142qed.
     143   
    104144definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
    105145  λcode_memory: BitVectorTrie Byte 16.
     
    121161      | DJNZ src_trgt relative ⇒ True
    122162      | _                      ⇒
    123           good_program_counter code_memory program_counter total_program_size
     163          good_program_counter code_memory total_program_size program_counter
    124164      ]
    125165    | LCALL addr         ⇒
    126166      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    127167      [ 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
     168          good_program_counter code_memory total_program_size addr
     169            good_program_counter code_memory total_program_size program_counter
    130170      | _ ⇒ λother: False. ⊥
    131171      ] (subaddressing_modein … addr)
     
    137177        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
    138178        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
     179          good_program_counter code_memory total_program_size new_program_counter
     180            good_program_counter code_memory total_program_size program_counter
    141181      | _ ⇒ λother: False. ⊥
    142182      ] (subaddressing_modein … addr)
     
    150190        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    151191        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)
     192          (good_program_counter code_memory total_program_size new_program_counter) ∧
     193            (good_program_counter code_memory total_program_size program_counter)
    154194      | _ ⇒ λother: False. ⊥
    155195      ] (subaddressing_modein … addr)
     
    157197      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    158198      [ 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
     199          good_program_counter code_memory total_program_size addr
     200            good_program_counter code_memory total_program_size program_counter
    161201      | _ ⇒ λother: False. ⊥
    162202      ] (subaddressing_modein … addr)
     
    165205      [ RELATIVE addr ⇒ λrelative: True.
    166206        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
     207          good_program_counter code_memory total_program_size new_program_counter
     208            good_program_counter code_memory total_program_size program_counter
    169209      | _ ⇒ λother: False. ⊥
    170210      ] (subaddressing_modein … addr)
    171211    | JMP   addr     ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
    172212    | MOVC  src trgt ⇒
    173         good_program_counter code_memory program_counter total_program_size
     213        good_program_counter code_memory total_program_size program_counter
    174214    ].
    175215  cases other
     
    298338qed.
    299339
    300 lemma subaddressing_mode_elim':
     340axiom subaddressing_mode_elim':
    301341  ∀T: Type[2].
    302342  ∀m: nat.
     
    305345  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    306346  ∀n: nat.
    307  
    308347  ∀v: Vector addressing_mode_tag n.
    309348  ∀proof.
    310349    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    311350      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    312   #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
     351(*  #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
    313352  elim v
    314353  [ #proof normalize
    315354   
    316 qed.
     355qed. *)
    317356
    318357(*
     
    362401
    363402axiom fetch_program_counter_n_technical:
     403  ∀n: nat.
    364404  ∀code_memory: BitVectorTrie Byte 16.
    365405  ∀program_counter, program_counter': Word.
    366   ∀instruction: instruction.
    367   ∀ticks, n: nat.
    368   program_counter' = \snd (\fst (fetch code_memory program_counter)) →
    369     program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
     406  program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
     407    program_counter' = \snd (\fst (fetch code_memory program_counter)) →
    370408      program_counter = fetch_program_counter_n n code_memory (zero …).
    371409   
     
    382420      [ None   ⇒
    383421        match instruction return λx. x = instruction → ? with
    384         [ RealInstruction instruction ⇒ λreal_instruction.
    385           match instruction return λx. x = instruction → ? with
     422        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
     423          match real_instruction return λx. x = real_instruction → ? with
    386424          [ RET                    ⇒ λinstr. ticks
    387425          | JC   relative          ⇒ λinstr. ticks
     
    396434          | _                      ⇒ λinstr.
    397435              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
    398           ] (refl … instruction)
     436          ] (refl … real_instruction)
    399437        | ACALL addr     ⇒ λinstr.
    400438            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     
    412450      ]
    413451  ].
    414   [1:
     452  [1: (* ACALL *)
    415453    generalize in match good_program_witness;
    416454    whd in match good_program; normalize nodelta
    417455    cases FETCH normalize nodelta
    418456    cases instr normalize nodelta
    419     @(subaddressing_mode_elim … [[ addr11 ]]) #new_addr
     457    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    420458    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    421459    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     
    434472        program_size' + (nat_of_bitvector … program_counter'))
    435473    @lt_n_o_to_plus_m_n_lt_plus_m_o
    436     >(fetch_program_counter_n_technical code_memory program_counter
    437       program_counter' instruction ticks n)
     474    >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
    438475    /2 by pair_destruct_2/
    439   |7:
     476  |2:
     477    generalize in match good_program_witness;
     478    whd in match good_program in ⊢ (? → %); normalize nodelta
     479    cases FETCH normalize nodelta
     480    cases instr normalize nodelta
     481    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     482    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     483    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     484    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
     485    * #ignore #good_program_counter_assm
     486    cases (fetch code_memory program_counter') #instruction_program_counter #cost normalize nodelta
     487    cases instruction_program_counter #instruction #program_counter normalize nodelta
     488    cases instruction
     489    [1:
     490      #addr11 normalize nodelta
     491      cases addr11 #addressing_mode
     492      cases addressing_mode
     493      try (#assm #proof normalize in proof; cases proof)
     494      try (#proof normalize in proof; cases proof)
     495      normalize nodelta
     496  |3: (* LCALL *)
    440497    generalize in match good_program_witness;
    441498    whd in match good_program; normalize nodelta
    442499    cases FETCH normalize nodelta
    443500    cases instr normalize nodelta
    444     @(subaddressing_mode_elim … [[ acc_dptr; acc_pc ]]) #new_addr
    445     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    446     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    447     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
     501    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    448502    #assm cases assm #ignore
    449503    whd in match good_program_counter; normalize nodelta * #n * *
     
    459513        program_size' + (nat_of_bitvector … program_counter'))
    460514    @lt_n_o_to_plus_m_n_lt_plus_m_o
    461     >(fetch_program_counter_n_technical code_memory program_counter
    462       program_counter' instruction ticks n)
     515    >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
    463516    /2 by pair_destruct_2/
    464   |3,5,7,9,11:
    465     (* XXX etc. need the subaddressing_mode_elim generalizing *)
    466   |2:
     517  |5: (* JMP *)
    467518    generalize in match good_program_witness;
    468     whd in match (good_program code_memory program_counter total_program_size);
     519    whd in match good_program; normalize nodelta
    469520    cases FETCH normalize nodelta
    470521    cases instr normalize nodelta
    471     @subaddressing_mode_elim #new_addr
    472     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    473     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    474     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
    475     #assm cases assm #ignore #good_program_counter
    476     whd in match (good_program code_memory program_counter' total_program_size);
    477     cases(fetch code_memory program_counter') #instruction_program_counter'' #ticks''
    478     cases(instruction_program_counter'') #instruction'' #program_counter'' normalize nodelta
    479    
    480   [2:
    481     (* generalize in match good_program_witness; *)
     522    cases daemon (* XXX ??? *)
     523  |7: (* MOVC *)
     524    generalize in match good_program_witness;
    482525    whd in match good_program; normalize nodelta
    483526    cases FETCH normalize nodelta
    484     cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta
    485     cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta
    486     cases acall normalize nodelta
    487     cases addr #subaddressing_mode cases subaddressing_mode
    488     try (#assm #absurd normalize in absurd; cases absurd)
    489     try (#absurd normalize in absurd; cases absurd)
    490     normalize nodelta
    491     cases instruction'
    492     try (#assm normalize nodelta)
    493     [7:
    494       #irrelevant
    495       whd in match good_program_counter; normalize nodelta
     527    cases instr normalize nodelta
     528    cases daemon (* XXX ??? *)
     529  |9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,
     530   49,51,53,55,57,59,61,63: (* ADD and similar non-branching instructions *)
     531    generalize in match good_program_witness;
     532    whd in match good_program; normalize nodelta
     533    cases FETCH normalize nodelta
     534    cases real_instruction_refl
     535    cases instr normalize nodelta
     536    whd in match good_program_counter; normalize nodelta
     537    * #the_n * *
     538    #program_counter_fetch_program_counter_n' #program_counter_lt_total_program_size'
     539    #fetch_program_n_lt_program_counter'
     540    @(transitive_le
     541      total_program_size
     542      (S program_size' + nat_of_bitvector … program_counter)
     543      (program_size' + nat_of_bitvector … program_counter')
     544      recursive_case)
     545    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     546    >plus_n_Sm
     547    @monotonic_le_plus_r
     548    change with (
     549      nat_of_bitvector … program_counter <
     550        nat_of_bitvector … program_counter')
     551    generalize in match (
     552      fetch_program_counter_n_technical the_n code_memory
     553        program_counter program_counter' program_counter_fetch_program_counter_n');
     554    #hyp >hyp
     555    >program_counter_fetch_program_counter_n'
     556  ]
     557qed.
    496558     
    497559     
Note: See TracChangeset for help on using the changeset viewer.