Changeset 1511 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 16, 2011, 5:35:24 PM (8 years ago)
Author:
mulligan
Message:

proofs, added, changes to execute_1_0 function therefore required to remove excess lets

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1509 r1511  
    5555definition current_instruction_cost ≝
    5656  λs: Status.
    57   let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in
    58     cost.
     57    \snd (fetch (code_memory … s) (program_counter … s)).
    5958
    6059definition next_instruction_properly_relates_program_counters ≝
     
    6463  let pc_before ≝ program_counter … before in
    6564  let pc_after ≝ program_counter … after in
    66   let 〈carry, sum〉 ≝ half_add … pc_before (bitvector_of_nat … size) in
     65  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    6766    sum = pc_after.
    6867
     
    7069  λs: Status.
    7170  let pc ≝ program_counter … s in
    72   let 〈instruction, new_pc, cost〉 ≝ fetch … (code_memory … s) pc in
    73     instruction.
     71  \fst (\fst (fetch … (code_memory … s) pc)).
    7472
    7573definition current_instruction_is_labelled ≝
     
    302300qed.
    303301
    304 lemma status_execution_progresses_processor_clock:
     302example set_program_counter_ignores_clock:
     303  ∀s: Status.
     304  ∀pc: Word.
     305    clock … (set_program_counter … s pc) = clock … s.
     306  #s #pc %
     307qed.
     308
     309example set_low_internal_ram_ignores_clock:
     310  ∀s: Status.
     311  ∀ram: BitVectorTrie Byte 7.
     312    clock … (set_low_internal_ram … s ram) = clock … s.
     313  #s #ram %
     314qed.
     315
     316example set_8051_sfr_ignores_clock:
     317  ∀s: Status.
     318  ∀sfr: SFR8051.
     319  ∀v: Byte.
     320    clock … (set_8051_sfr ? s sfr v) = clock … s.
     321  #s #sfr #v %
     322qed.
     323
     324example clock_set_clock:
     325  ∀s: Status.
     326  ∀v.
     327    clock … (set_clock … s v) = v.
     328  #s #v %
     329qed.
     330
     331example write_at_stack_pointer_ignores_clock:
     332  ∀s: Status.
     333  ∀sp: Byte.
     334    clock … (write_at_stack_pointer … s sp) = clock … s.
     335  #s #sp
     336  change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with (
     337      let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
     338        ?);
     339  normalize nodelta;
     340  cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP))
     341  #nu #nl normalize nodelta;
     342  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
     343  [ normalize nodelta; %
     344  | normalize nodelta; %
     345  ]
     346qed.
     347
     348example status_execution_progresses_processor_clock:
    305349  ∀s: Status.
    306350    clock … s ≤ clock … (execute 1 s).
    307   #status
    308   cases status
    309   #ignore1 #ignore2 #ignore3 #ignore4 #ignore5 #ignore6 #ignore7 #ignore8
    310   #ignore9 #clock
    311  
     351  #s
     352  change in match (execute 1 s) with (execute_1 s);
     353  change in match (execute_1 s) with (
     354    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
     355                               (program_counter (BitVectorTrie Byte 16) s)
     356    in 
     357      execute_1_0 s instr_pc_ticks);
     358  normalize nodelta;
     359  whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
     360     (program_counter (BitVectorTrie Byte 16) s)));
     361  normalize nodelta;
     362  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
     363           (program_counter (BitVectorTrie Byte 16) s))
     364  #instruction_pc #ticks
     365  normalize nodelta;
     366  cases instruction_pc
     367  #instruction #pc
     368  cases instruction
     369  [1:
     370    #addr11 cases addr11 #addressing_mode
     371    normalize nodelta; cases addressing_mode
     372    normalize nodelta;
     373    [1,2,3,4,8,9,15,16,17,19:
     374      #assm whd in ⊢ (% → ?)
     375      #absurd cases(absurd)
     376    |5,6,7,10,11,12,13,14:
     377      whd in ⊢ (% → ?)
     378      #absurd cases(absurd)
     379    |18:
     380      #addr11 #irrelevant
     381      normalize nodelta;
     382      >set_program_counter_ignores_clock
     383      normalize nodelta;
     384      >set_program_counter_ignores_clock
     385      >write_at_stack_pointer_ignores_clock
     386      >set_8051_sfr_ignores_clock
     387      >write_at_stack_pointer_ignores_clock
     388      >set_8051_sfr_ignores_clock
     389      >clock_set_clock //
     390    ]
     391  |2:
     392    #addr16 cases addr16 #addressing_mode
     393    normalize nodelta; cases addressing_mode
     394    normalize nodelta;
     395    [1,2,3,4,8,9,15,16,17,18:
     396      #assm whd in ⊢ (% → ?)
     397      #absurd cases(absurd)
     398    |5,6,7,10,11,12,13,14:
     399      whd in ⊢ (% → ?)
     400      #absurd cases(absurd)
     401    |19:
     402      #addr16 #irrelevant
     403      normalize nodelta;
     404      >set_program_counter_ignores_clock
     405      >write_at_stack_pointer_ignores_clock
     406      >set_8051_sfr_ignores_clock
     407      >write_at_stack_pointer_ignores_clock
     408      >set_8051_sfr_ignores_clock
     409      >clock_set_clock
     410      >set_program_counter_ignores_clock //
     411    ]
     412  |3: #addr11 cases addr11 #addressing_mode
     413      normalize nodelta; cases addressing_mode
     414      normalize nodelta;
     415      [1,2,3,4,8,9,15,16,17,19:
     416        #assm whd in ⊢ (% → ?)
     417        #absurd cases(absurd)
     418      |5,6,7,10,11,12,13,14:
     419        whd in ⊢ (% → ?)
     420        #absurd cases(absurd)
     421      |18:
     422        #word11 #irrelevant
     423        normalize nodelta;
     424        >set_program_counter_ignores_clock
     425        >clock_set_clock
     426        >set_program_counter_ignores_clock //
     427      ]
     428  |4: #addr16 cases addr16 #addressing_mode
     429      normalize nodelta; cases addressing_mode
     430      normalize nodelta;
     431      [1,2,3,4,8,9,15,16,17,18:
     432        #assm whd in ⊢ (% → ?)
     433        #absurd cases(absurd)
     434      |5,6,7,10,11,12,13,14:
     435        whd in ⊢ (% → ?)
     436        #absurd cases(absurd)
     437      |19:
     438        #word #irrelevant
     439        normalize nodelta;
     440        >set_program_counter_ignores_clock
     441        >clock_set_clock
     442        >set_program_counter_ignores_clock //
     443      ]
     444  |5: #relative cases relative #addressing_mode
     445      normalize nodelta; cases addressing_mode
     446      normalize nodelta;
     447      [1,2,3,4,8,9,15,16,18,19:
     448        #assm whd in ⊢ (% → ?)
     449        #absurd cases(absurd)
     450      |5,6,7,10,11,12,13,14:
     451        whd in ⊢ (% → ?)
     452        #absurd cases(absurd)
     453      |17:
     454        #byte #irrelevant
     455        normalize nodelta;
     456        >set_program_counter_ignores_clock
     457        >set_program_counter_ignores_clock
     458        >clock_set_clock //
     459      ]
     460  |6: #indirect_dptr cases indirect_dptr #addressing_mode
     461      normalize nodelta; cases addressing_mode
     462      normalize nodelta;
     463     
     464
     465lemma current_instruction_cost_is_ok:
     466  ∀s: Status.
     467    current_instruction_cost s = clock … (execute 1 s) - clock … s.
     468  #s
     469  change in match (execute 1 s) with (execute_1 s);
     470  change in match (execute_1 s) with (
     471    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
     472                               (program_counter (BitVectorTrie Byte 16) s)
     473    in 
     474      execute_1_0 s instr_pc_ticks);
     475  change in ⊢ (??%?) with (
     476    \snd (fetch (code_memory … s) (program_counter … s)));
     477  normalize nodelta;
    312478
    313479let rec compute_max_trace_label_label_cost_is_ok
     
    348514  |2: cases the_trace
    349515    [1: #the_status #not_return #not_jump #not_cost
     516        change in ⊢ (??%?) with (current_instruction_cost the_status);
     517        @current_instruction_cost_is_ok
    350518    |2: #the_status #is_return
     519        change in ⊢ (??%?) with (current_instruction_cost the_status);
     520        @current_instruction_cost_is_ok
    351521    |3: #the_status #is_jump #is_cost
     522        change in ⊢ (??%?) with (current_instruction_cost the_status);
     523        @current_instruction_cost_is_ok
    352524    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
    353         #next_intruction_coherence #call_trace #final_trace
     525        #next_instruction_coherence #call_trace #final_trace
     526        change in ⊢ (??%?) with (
     527          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     528          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
     529          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
     530            call_trace_cost + current_instruction_cost + final_trace_cost)
     531        normalize nodelta;
     532        >current_instruction_cost_is_ok
     533        >compute_max_trace_label_return_cost_is_ok
     534        >compute_max_trace_label_label_pre_cost_is_ok
     535        generalize in match next_instruction_coherence;
     536        change in ⊢ (% → ?) with (
     537          let size ≝ current_instruction_cost pre_fun_call in
     538          let pc_before ≝ program_counter … pre_fun_call in
     539          let pc_after ≝ program_counter … after_fun_call in
     540          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
     541            sum = pc_after)
     542        normalize nodelta;
     543        >(plus_minus_rearrangement
     544          (clock (BitVectorTrie Byte 16) after_fun_call)
     545          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
     546          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
    354547    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
    355548        #is_not_jump #is_not_ret #is_not_labelled
    356         @current_instruction_cost
     549        change in ⊢ (??%?) with (
     550          let current_instruction_cost ≝ current_instruction_cost status_pre in
     551          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
     552            current_instruction_cost + tail_trace_cost)
     553        normalize nodelta;
     554        >compute_max_trace_label_label_pre_cost_is_ok
     555        >current_instruction_cost_is_ok
    357556    ]
    358557  ]
Note: See TracChangeset for help on using the changeset viewer.