Changeset 1544 for src/ASM


Ignore:
Timestamp:
Nov 23, 2011, 6:01:15 PM (8 years ago)
Author:
sacerdot
Message:

StructuredTraces? inhabited for object code.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/CostsProof.ma

    r1534 r1544  
    22include "ASM/WellLabeled.ma".
    33include "ASM/Status.ma".
    4 
    5 definition is_jump_p ≝
    6   λs.
    7   match s with
    8   [ AJMP _ ⇒ True
    9   | LJMP _ ⇒ True
    10   | SJMP _ ⇒ True
    11   | JMP _ ⇒ False
    12   | RealInstruction ri ⇒
    13     match ri with
    14     [ JZ _ ⇒ True
    15     | JNZ _ ⇒ True
    16     | JC _ ⇒ True
    17     | JNC _ ⇒ True
    18     | JB _ _ ⇒ True
    19     | JNB _ _ ⇒ True
    20     | JBC _ _ ⇒ True
    21     | CJNE _ _ ⇒ True
    22     | DJNZ _ _ ⇒ True
    23     | _ ⇒ False
    24     ]
    25   | _ ⇒ False
    26   ].
     4include "common/StructuredTraces.ma".
     5
     6definition current_instruction ≝
     7  λs: Status.
     8  let pc ≝ program_counter … s in
     9  \fst (\fst (fetch … (code_memory … s) pc)).
     10
     11definition ASM_classify: Status → status_class ≝
     12 λs.
     13  match current_instruction s with
     14   [ RealInstruction pre ⇒
     15     match pre with
     16      [ RET ⇒ cl_return
     17      | JZ _ ⇒ cl_jump
     18      | JNZ _ ⇒ cl_jump
     19      | JC _ ⇒ cl_jump
     20      | JNC _ ⇒ cl_jump
     21      | JB _ _ ⇒ cl_jump
     22      | JNB _ _ ⇒ cl_jump
     23      | JBC _ _ ⇒ cl_jump
     24      | CJNE _ _ ⇒ cl_jump
     25      | DJNZ _ _ ⇒ cl_jump
     26      | _ ⇒ cl_other
     27      ]
     28   | ACALL _ ⇒ cl_call
     29   | LCALL _ ⇒ cl_call
     30   | JMP _ ⇒ cl_call
     31   | AJMP _ ⇒ cl_jump
     32   | LJMP _ ⇒ cl_jump
     33   | SJMP _ ⇒ cl_jump
     34   | _ ⇒ cl_other
     35   ].
     36
     37definition current_instruction_is_labelled ≝
     38  λcost_labels: BitVectorTrie Byte 16.
     39  λs: Status.
     40  let pc ≝ program_counter … s in
     41    match lookup_opt … pc cost_labels with
     42    [ None ⇒ False
     43    | _    ⇒ True
     44    ].
     45
     46definition current_instruction_cost ≝
     47  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
     48
     49definition next_instruction_properly_relates_program_counters ≝
     50  λbefore: Status.
     51  λafter : Status.
     52  let size ≝ current_instruction_cost before in
     53  let pc_before ≝ program_counter … before in
     54  let pc_after ≝ program_counter … after in
     55  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
     56    sum = pc_after.
     57
     58definition ASM_abstract_status: BitVectorTrie Byte 16 → abstract_status ≝
     59 λcost_labels.
     60  mk_abstract_status
     61   Status
     62   (λs,s'. eject … (execute_1 s) = s')
     63   (λs,class. ASM_classify s = class)
     64   (current_instruction_is_labelled cost_labels)
     65   next_instruction_properly_relates_program_counters.
     66
     67(*
     68definition next_instruction_is_labelled ≝
     69  λcost_labels: BitVectorTrie Byte 16.
     70  λs: Status.
     71  let pc ≝ program_counter … (execute_1 s) in
     72    match lookup_opt … pc cost_labels with
     73    [ None ⇒ False
     74    | _    ⇒ True
     75    ].
     76
     77definition current_instruction_cost ≝
     78  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
    2779
    2880definition is_call_p ≝
    … …  
    52104    | _    ⇒ True
    53105    ].
    54 
    55 definition current_instruction_cost ≝
    56   λs: Status.
    57     \snd (fetch (code_memory … s) (program_counter … s)).
    58106
    59107definition next_instruction_properly_relates_program_counters ≝
    … …  
    142190          ¬ (current_instruction_is_labelled cost_labels status_init) →
    143191            trace_label_label_pre cost_labels end_flag status_pre status_end.
    144 
    145 (* XXX: to do later
     192*)
     193
     194(* XXX: not us
    146195definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
    147196
    … …  
    157206
    158207let rec compute_max_trace_label_label_cost
    159   (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     208  (cost_labels: BitVectorTrie Byte 16)
     209   (trace_ends_flag: trace_ends_with_ret)
    160210    (start_status: Status) (final_status: Status)
    161       (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
    162         on the_trace: nat ≝
     211      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     212        start_status final_status) on the_trace: nat ≝
    163213  match the_trace with
    164214  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    165       compute_max_trace_label_label_pre_cost … given_trace
    166   ]
    167 and compute_max_trace_label_label_pre_cost
    168   (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
    169     (start_status: Status) (final_status: Status)
    170       (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
    171         on the_trace: nat ≝
     215      compute_max_trace_any_label_cost … given_trace
     216  ]
     217and compute_max_trace_any_label_cost
     218  (cost_labels: BitVectorTrie Byte 16)
     219  (trace_ends_flag: trace_ends_with_ret)
     220   (start_status: Status) (final_status: Status)
     221     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     222       on the_trace: nat ≝
    172223  match the_trace with
    173   [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒
    174       current_instruction_cost the_status
    175   | tllp_base_return the_status is_return ⇒ current_instruction_cost the_status
    176   | tllp_base_jump the_status is_jump is_cost ⇒
    177       current_instruction_cost the_status
    178   | tllp_step_call end_flag pre_fun_call after_fun_call final is_call
    179         next_intruction_coherence call_trace final_trace ⇒
     224  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
     225  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     226  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     227     _ _ _ call_trace final_trace ⇒
    180228      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    181       let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
    182       let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
     229      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     230      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    183231        call_trace_cost + current_instruction_cost + final_trace_cost
    184   | tllp_step_default end_flag status_pre status_end tail_trace is_not_call
    185         is_not_jump is_not_ret is_not_labelled ⇒
     232  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    186233      let current_instruction_cost ≝ current_instruction_cost status_pre in
    187       let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
     234      let tail_trace_cost ≝
     235       compute_max_trace_any_label_cost cost_labels end_flag
     236        status_init status_end tail_trace
     237      in
    188238        current_instruction_cost + tail_trace_cost
    189239  ]
    190240and compute_max_trace_label_return_cost
    191   (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
    192     (the_trace: trace_label_return cost_labels start_status final_status)
     241  (cost_labels: BitVectorTrie Byte 16)
     242  (start_status: Status) (final_status: Status)
     243    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    193244      on the_trace: nat ≝
    194245  match the_trace with
    … …  
    200251  ].
    201252
     253(* To be moved *)
    202254lemma pred_minus_1:
    203255  ∀m, n: nat.
    … …  
    225277  ∀m: nat.
    226278    S m = m + 1.
    227   #m
    228   elim m
    229   [ %
    230   | #m' #ind_hyp
    231     normalize
    232     <ind_hyp
    233     %
    234   ]
    235 qed.
     279 //
     280qed.
     281
     282include alias "arithmetics/nat.ma".
    236283
    237284lemma minus_m_n_minus_minus_plus_1:
    … …  
    239286  ∀proof: n < m.
    240287    m - n = (m - n - 1) + 1.
    241   #m
    242   elim m
    243   [ #n #proof
    244     cases(lt_to_not_zero … proof)
    245   | #m' #ind_hyp #n
    246     normalize
    247     cases n
    248     [ normalize //
    249     | #n' #proof normalize
    250       <ind_hyp
    251       [ %
    252       | @le_S_S_to_le
    253         assumption
    254       ]
    255     ]
    256   ]
    257 qed.
    258 
    259 include alias "arithmetics/nat.ma".
     288 /3 by lt_plus_to_minus_r, plus_minus/
     289qed.
    260290
    261291lemma plus_minus_rearrangement_1:
    262292  ∀m, n, o: nat.
    263   ∀proof_n_m: n < m.
    264   ∀proof_m_o: m < o.
     293  ∀proof_n_m: n ≤ m.
     294  ∀proof_m_o: m ≤ o.
    265295    (m - n) + (o - m) = o - n.
    266   #m #n #o
    267   elim m
    268   [1: #proof_n_m
    269       cases(lt_to_not_zero … proof_n_m)
    270   |2: #m' #ind_hyp
    271       #proof_n_m' #proof_m_o
    272       >minus_Sn_m
    273       [2: normalize in proof_n_m';
    274           @le_S_S_to_le
    275           assumption
    276       |1: >eq_minus_S_pred
    277           >pred_minus_1
    278           [1: >(succ_m_plus_one (m' - n))
    279               >(associative_plus (m' - n) 1 (o - m' - 1))
    280               <commutative_plus in match (1 + (o - m' - 1));
    281               <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1);
    282               [1: >ind_hyp
    283                 [1: %
    284                 |2: normalize
    285                     normalize in proof_m_o;
    286                     @le_S_S_to_le
    287                     @(le_S ? ? proof_m_o)
    288                 |3: cases daemon (* XXX: problem here *)
    289                 ]
    290               |2: normalize in proof_m_o;
    291                   normalize
    292                   @le_S_S_to_le
    293                   @(le_S (S (S m')) o proof_m_o)
    294               ]
    295           |2: normalize
    296               normalize in proof_m_o;
    297               @le_S_S_to_le
    298               @(le_S (S (S m')) o proof_m_o)
    299           ]
    300       ]
    301   ]
    302 qed.
    303 
    304 axiom plus_minus_rearrangement_2:
    305   ∀m, n, o: nat.
     296  #m #n #o #H1 #H2
     297  lapply (minus_to_plus … H1 (refl …)) #K1 >K1
     298  lapply (minus_to_plus … H2 (refl …)) #K2 >K2
     299  /2 by plus_minus/
     300qed.
     301
     302lemma plus_minus_rearrangement_2:
     303  ∀m, n, o: nat. n ≤ m → o ≤ n →
    306304    (m - n) + (n - o) = m - o.
    307 
    308 example set_program_counter_ignores_clock:
    309   ∀s: Status.
    310   ∀pc: Word.
    311     clock … (set_program_counter … s pc) = clock … s.
    312   #s #pc %
    313 qed.
    314 
    315 example set_low_internal_ram_ignores_clock:
    316   ∀s: Status.
    317   ∀ram: BitVectorTrie Byte 7.
    318     clock … (set_low_internal_ram … s ram) = clock … s.
    319   #s #ram %
    320 qed.
    321 
    322 example set_8051_sfr_ignores_clock:
    323   ∀s: Status.
    324   ∀sfr: SFR8051.
    325   ∀v: Byte.
    326     clock … (set_8051_sfr ? s sfr v) = clock … s.
    327   #s #sfr #v %
    328 qed.
    329 
    330 example clock_set_clock:
    331   ∀s: Status.
    332   ∀v.
    333     clock … (set_clock … s v) = v.
    334   #s #v %
    335 qed.
    336 
    337 example write_at_stack_pointer_ignores_clock:
    338   ∀s: Status.
    339   ∀sp: Byte.
    340     clock … (write_at_stack_pointer … s sp) = clock … s.
    341   #s #sp
    342   change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp); with (
    343       let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
    344         ?);
    345   normalize nodelta;
    346   cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP))
    347   #nu #nl normalize nodelta;
    348   cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
    349   [ normalize nodelta; %
    350   | normalize nodelta; %
    351   ]
    352 qed.
    353 
    354 example status_execution_progresses_processor_clock:
    355   ∀s: Status.
    356     clock … s ≤ clock … (execute 1 s).
    357   #s
    358   change in match (execute 1 s) with (execute_1 s);
    359   change in match (execute_1 s) with (
    360     let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
    361                                (program_counter (BitVectorTrie Byte 16) s)
    362     in 
    363       execute_1_0 s instr_pc_ticks);
    364   normalize nodelta;
    365   whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
    366      (program_counter (BitVectorTrie Byte 16) s)));
    367   normalize nodelta;
    368   cases (fetch (code_memory (BitVectorTrie Byte 16) s)
    369            (program_counter (BitVectorTrie Byte 16) s))
    370   #instruction_pc #ticks
    371   normalize nodelta;
    372   cases instruction_pc
    373   #instruction #pc
    374   cases instruction
    375   [1:
    376     #addr11 cases addr11 #addressing_mode
    377     normalize nodelta; cases addressing_mode
    378     normalize nodelta;
    379     [1,2,3,4,8,9,15,16,17,19:
    380       #assm whd in ⊢ (% → ?)
    381       #absurd cases(absurd)
    382     |5,6,7,10,11,12,13,14:
    383       whd in ⊢ (% → ?)
    384       #absurd cases(absurd)
    385     |18:
    386       #addr11 #irrelevant
    387       normalize nodelta;
    388       >set_program_counter_ignores_clock
    389       normalize nodelta;
    390       >set_program_counter_ignores_clock
    391       >write_at_stack_pointer_ignores_clock
    392       >set_8051_sfr_ignores_clock
    393       >write_at_stack_pointer_ignores_clock
    394       >set_8051_sfr_ignores_clock
    395       >clock_set_clock //
    396     ]
    397   |2:
    398     #addr16 cases addr16 #addressing_mode
    399     normalize nodelta; cases addressing_mode
    400     normalize nodelta;
    401     [1,2,3,4,8,9,15,16,17,18:
    402       #assm whd in ⊢ (% → ?)
    403       #absurd cases(absurd)
    404     |5,6,7,10,11,12,13,14:
    405       whd in ⊢ (% → ?)
    406       #absurd cases(absurd)
    407     |19:
    408       #addr16 #irrelevant
    409       normalize nodelta;
    410       >set_program_counter_ignores_clock
    411       >write_at_stack_pointer_ignores_clock
    412       >set_8051_sfr_ignores_clock
    413       >write_at_stack_pointer_ignores_clock
    414       >set_8051_sfr_ignores_clock
    415       >clock_set_clock
    416       >set_program_counter_ignores_clock //
    417     ]
    418   |3: #addr11 cases addr11 #addressing_mode
    419       normalize nodelta; cases addressing_mode
    420       normalize nodelta;
    421       [1,2,3,4,8,9,15,16,17,19:
    422         #assm whd in ⊢ (% → ?)
    423         #absurd cases(absurd)
    424       |5,6,7,10,11,12,13,14:
    425         whd in ⊢ (% → ?)
    426         #absurd cases(absurd)
    427       |18:
    428         #word11 #irrelevant
    429         normalize nodelta;
    430         >set_program_counter_ignores_clock
    431         >clock_set_clock
    432         >set_program_counter_ignores_clock //
    433       ]
    434   |4: #addr16 cases addr16 #addressing_mode
    435       normalize nodelta; cases addressing_mode
    436       normalize nodelta;
    437       [1,2,3,4,8,9,15,16,17,18:
    438         #assm whd in ⊢ (% → ?)
    439         #absurd cases(absurd)
    440       |5,6,7,10,11,12,13,14:
    441         whd in ⊢ (% → ?)
    442         #absurd cases(absurd)
    443       |19:
    444         #word #irrelevant
    445         normalize nodelta;
    446         >set_program_counter_ignores_clock
    447         >clock_set_clock
    448         >set_program_counter_ignores_clock //
    449       ]
    450   |5: #relative cases relative #addressing_mode
    451       normalize nodelta; cases addressing_mode
    452       normalize nodelta;
    453       [1,2,3,4,8,9,15,16,18,19:
    454         #assm whd in ⊢ (% → ?)
    455         #absurd cases(absurd)
    456       |5,6,7,10,11,12,13,14:
    457         whd in ⊢ (% → ?)
    458         #absurd cases(absurd)
    459       |17:
    460         #byte #irrelevant
    461         normalize nodelta;
    462         >set_program_counter_ignores_clock
    463         >set_program_counter_ignores_clock
    464         >clock_set_clock //
    465       ]
    466   |6: #indirect_dptr cases indirect_dptr #addressing_mode
    467       normalize nodelta; cases addressing_mode
    468       normalize nodelta;
    469       [1,2,3,4,8,9,15,16,17,18,19:
    470         #assm whd in ⊢ (% → ?)
    471         #absurd cases(absurd)
    472       |5,6,7,10,11,12,14:
    473         whd in ⊢ (% → ?)
    474         #absurd cases(absurd)
    475       |13:
    476         #irrelevant
    477         normalize nodelta;
    478         >set_program_counter_ignores_clock
    479         >set_program_counter_ignores_clock
    480         >clock_set_clock //
    481       ]
    482   |8: cases daemon (* XXX: my god *)
    483   |7: #acc_a cases acc_a #addressing_mode
    484       normalize nodelta; cases addressing_mode
    485       normalize nodelta;
    486       [1,2,3,4,8,9,15,16,17,18,19:
    487         #assm whd in ⊢ (% → ?)
    488         #absurd cases(absurd)
    489       |6,7,10,11,12,13,14:
    490         whd in ⊢ (% → ?)
    491         #absurd cases(absurd)
    492       |5:
    493         #irrelevant #acc_dptr_acc_pc
    494         normalize nodelta;
    495         cases daemon (* XXX: my god *)
    496       ]
    497   ]
     305 /2 by plus_minus_rearrangement_1/
    498306qed.
    499307
    … …  
    502310    current_instruction_cost s = clock … (execute 1 s) - clock … s.
    503311  #s
    504   change in match (execute 1 s) with (execute_1 s);
    505   change in match (execute_1 s) with (
     312  change with (execute_1 s) in match (eject … (execute 1 s));
     313  change with (
    506314    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
    507315                               (program_counter (BitVectorTrie Byte 16) s)
    508316    in 
    509       execute_1_0 s instr_pc_ticks);
    510   change in ⊢ (??%?) with (
    511     \snd (fetch (code_memory … s) (program_counter … s)));
     317     eject … (execute_1_0 s instr_pc_ticks)) in match (eject … (execute_1 s));
     318  change with (
     319    \snd (fetch (code_memory … s) (program_counter … s))) in ⊢ (??%?);
    512320  normalize nodelta;
    513321  whd in match (
Note: See TracChangeset for help on using the changeset viewer.