Changeset 1511


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

Location:
src/ASM
Files:
2 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  ]
  • src/ASM/Interpret.ma

    r1494 r1511  
    545545          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    546546            [ ADDR11 a ⇒ λaddr11: True.
    547               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     547              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    548548              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    549               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     549              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
     550              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
    550551              let s ≝ write_at_stack_pointer ? s pc_bl in
    551               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     552              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    552553              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    553554              let s ≝ write_at_stack_pointer ? s pc_bu in
    554               let 〈thr, eig〉 ≝ split ? 3 8 a in
    555               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     555              let thr ≝ \fst (split ? 3 8 a) in
     556              let eig ≝ \snd (split ? 3 8 a) in
     557              let fiv ≝ \fst (split ? 5 3 pc_bu) in
     558              let thr' ≝ \snd (split ? 5 3 pc_bu) in
    556559              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    557560                set_program_counter ? s new_addr
     
    562565          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    563566            [ ADDR16 a ⇒ λaddr16: True.
    564               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     567              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    565568              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    566               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     569              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
     570              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
    567571              let s ≝ write_at_stack_pointer ? s pc_bl in
    568               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     572              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    569573              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    570574              let s ≝ write_at_stack_pointer ? s pc_bu in
     
    596600          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    597601          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    598           let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    599           let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
     602          let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
     603          let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
    600604            set_program_counter ? s new_pc
    601605        | LJMP addr ⇒
     
    610614          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    611615            [ RELATIVE r ⇒ λrelative: True.
    612                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     616                let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
    613617                  set_program_counter ? s new_pc
    614618            | _ ⇒ λother: False. ⊥
     
    618622          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    619623            [ ADDR11 a ⇒ λaddr11: True.
    620               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    621               let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     624              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
     625              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
     626              let nu ≝ \fst (split ? 4 4 pc_bu) in
     627              let nl ≝ \snd (split ? 4 4 pc_bu) in
    622628              let bit ≝ get_index' ? O ? nl in
    623               let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     629              let relevant1 ≝ \fst (split ? 3 8 a) in
     630              let relevant2 ≝ \snd (split ? 3 8 a) in
    624631              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    625               let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
     632              let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
    626633                set_program_counter ? s new_pc
    627634            | _ ⇒ λother: False. ⊥
Note: See TracChangeset for help on using the changeset viewer.