Changeset 1710


Ignore:
Timestamp:
Feb 20, 2012, 10:04:54 AM (8 years ago)
Author:
mulligan
Message:

changes from friday afternoon

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1709 r1710  
    474474  #code_memory #start_status #classify_assm
    475475  whd in match execute_1; normalize nodelta
    476   whd in match execute_1'; normalize nodelta
    477   whd in match execute_1_0; normalize nodelta
    478   generalize in match (refl … (fetch code_memory
    479     (program_counter (BitVectorTrie Byte 16) code_memory start_status)));
    480   cases (fetch code_memory
    481     (program_counter (BitVectorTrie Byte 16) code_memory start_status)) in ⊢ (??%? → ?);
    482   #instr_pc #ticks #fetch_rewrite <fetch_rewrite
    483   cases
     476  cases (execute_1' code_memory start_status) #the_status
     477  * #_ #classify_assm' @classify_assm' assumption
    484478qed-.
    485479
     
    572566        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
    573567        [1:
    574           <fetch_twice_fetch_execute_1 <FETCH %
     568          <fetch_twice_fetch_execute_1
     569          [1:
     570            <FETCH %
     571          |2:
     572            >classifier_assm %
     573          ]
    575574        |2:
    576575          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
     
    621620        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
    622621        [1:
    623           <fetch_twice_fetch_execute_1 <FETCH %
     622          <fetch_twice_fetch_execute_1
     623          [1:
     624            <FETCH %
     625          |2:
     626            cases classifier_assm
     627            [1:
     628              whd in ⊢ (% → ?);
     629              whd in ⊢ (??%? → ?);
     630              whd in match (current_instruction code_memory' status_start);
     631              <FETCH generalize in match classify_assm;
     632              cases instruction
     633              [8:
     634                #preinstruction normalize nodelta
     635                whd in match ASM_classify0; normalize nodelta
     636                #contradiction >contradiction #absurd destruct(absurd)
     637              ]
     638              try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
     639              try(#addr normalize nodelta #ignore #absurd destruct(absurd))
     640              normalize in ignore; destruct(ignore)
     641            |2:
     642              #classifier_assm' >classifier_assm' %
     643            ]
     644          ]
    624645        |2:
    625646          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
     
    908929qed.
    909930
     931lemma trace_compute_paid_trace_cl_return:
     932  ∀code_memory' : (BitVectorTrie Byte 16).
     933  ∀program_counter' : Word.
     934  ∀total_program_size : ℕ.
     935  ∀cost_labels : (BitVectorTrie costlabel 16).
     936  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
     937  ∀good_program_witness : (good_program code_memory' total_program_size).
     938  ∀program_size' : ℕ.
     939  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
     940  ∀ticks : ℕ.
     941  ∀instruction : instruction.
     942  ∀program_counter'' : Word.
     943  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     944  ∀start_status : (Status code_memory').
     945  ∀final_status : (Status code_memory').
     946  ∀trace_ends_flag : trace_ends_with_ret.
     947  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     948  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     949  ∀classify_assm: ASM_classify0 instruction = cl_return.
     950    (∃n:ℕ
     951     .trace_any_label_length code_memory' cost_labels trace_ends_flag
     952      start_status final_status the_trace
     953      +S n
     954      =total_program_size)
     955    ∧ticks
     956     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     957      start_status final_status the_trace.
     958  #code_memory' #program_counter' #total_program_size #cost_labels
     959  #reachable_program_counter_witness #good_program_witness #program_size'
     960  #recursive_case #ticks #instruction #program_counter'' #FETCH
     961  #start_status #final_status #trace_ends_flag
     962  #the_trace #program_counter_refl #classify_assm
     963  @(trace_any_label_inv_ind … the_trace)
     964  [1:
     965    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     966    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     967    destruct @⊥
     968  |2:
     969    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
     970    #start_status_refl #final_status_refl #the_trace_refl destruct
     971    whd in match (trace_any_label_length … (tal_base_return …));
     972    whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
     973    [1:
     974      %{(pred total_program_size)} whd in ⊢ (??%?);
     975      @S_pred
     976      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     977    |2:
     978      <FETCH %
     979    ]
     980  |3:
     981    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     982    #classifier_assm #after_return_assm #trace_label_return #costed_assm
     983    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     984    destruct @⊥
     985  |4:
     986    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     987    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     988    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     989    #final_status_refl #the_trace_refl
     990    destruct @⊥
     991  |5:
     992    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     993    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
     994    #final_status_refl #the_trace_refl destruct @⊥
     995  ]
     996  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     997  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
     998  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     999  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     1000  <FETCH in classifier_assm; >classify_assm
     1001  #absurd try (destruct(absurd))
     1002  cases absurd
     1003  #absurd destruct(absurd)
     1004qed.
     1005     
     1006     
    9101007let rec block_cost'
    9111008  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
     
    9491046                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
    9501047          [ RET                    ⇒ λinstr. ticks
     1048          | RETI                   ⇒ λinstr. ticks
    9511049          | JC   relative          ⇒ λinstr. ticks
    9521050          | JNC  relative          ⇒ λinstr. ticks
     
    9901088          ])
    9911089  ].
    992   cases daemon (*
    9931090  [1:
    9941091    cases reachable_program_counter_witness #_ #hyp
     
    10021099    change with (if to_continue then ? else (0 = 0))
    10031100    >p normalize nodelta %
    1004   |98,104,107:
     1101  |7,8:
     1102    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     1103    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     1104    destruct %
     1105  |96,102,105:
    10051106    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    10061107    cases(block_cost' ?????????) -block_cost'
    10071108    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
    10081109    destruct %
    1009   |4,7,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
    1010    92,95:
     1110  |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87,
     1111   90,93:
    10111112    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    10121113    cases(block_cost' ?????????) -block_cost'
    10131114    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    10141115    destruct %
    1015   |62,63,64,65,66,67,68,69,101,102,103:
     1116  |62,63,64,65,66,67,68,69,99,101,102:
    10161117    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    10171118    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
    10181119    destruct %
    1019   |96,99:
    1020     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1021     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1022     <FETCH normalize nodelta <instr normalize nodelta *
    1023     #program_counter_lt' #program_counter_lt_tps' %
    1024     [1,3:
    1025       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1026       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1027       >(le_to_leb_true … program_counter_lt') %
    1028     |2,4:
    1029       assumption
    1030     ]
    1031   |105:
     1120  |103:
    10321121    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10331122    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10441133      assumption
    10451134    ]
    1046   |106:
     1135  |104:
    10471136    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10481137    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10621151        nat_of_bitvector … program_counter'')
    10631152    assumption
    1064   |108:
     1153  |106:
    10651154    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10661155    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10791168      assumption
    10801169    ]
    1081   |109:
     1170  |107:
    10821171    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    10831172    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    10991188        nat_of_bitvector … program_counter'')
    11001189    assumption
    1101   |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
    1102    78,81,84,87,90,93:
     1190  |94,97:
     1191    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1192    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1193    <FETCH normalize nodelta <instr normalize nodelta *
     1194    #program_counter_lt' #program_counter_lt_tps' %
     1195    [1,3:
     1196      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1197      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1198      >(le_to_leb_true … program_counter_lt') %
     1199    |2,4:
     1200      assumption
     1201    ]
     1202  |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73,
     1203   76,79,82,85,88,91:
    11031204    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    11041205    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    11091210    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    11101211    >(le_to_leb_true … program_counter_lt') %
     1212    (* XXX: got to here *)
    11111213  |6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91,
    11121214   94:
     
    11271229        nat_of_bitvector … program_counter'')
    11281230    assumption
    1129   |10:
    1130     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    1131     cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
    1132       reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
    1133     [1:
    1134       #recursive_block_cost #recursive_assm
    1135       @(trace_any_label_inv_ind … the_trace)
    1136       [1:
    1137         #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
    1138         #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1139         destruct @⊥
    1140       |2:
    1141         #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
    1142         #start_status_refl #final_status_refl #the_trace_refl destruct
    1143         whd in match (trace_any_label_length … (tal_base_return …));
    1144         whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
    1145         [1:
    1146           %{(pred total_program_size)} whd in ⊢ (??%?);
    1147           @S_pred
    1148           @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
    1149         |2:
    1150           <FETCH %
    1151         ]
    1152       |3:
    1153         #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    1154         #classifier_assm #after_return_assm #trace_label_return #costed_assm
    1155         #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    1156         destruct @⊥
    1157       |4:
    1158         #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    1159         #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    1160         #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    1161         #final_status_refl #the_trace_refl
    1162         destruct @⊥
    1163       |5:
    1164         #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    1165         #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    1166         #final_status_refl #the_trace_refl destruct @⊥
    1167       ]
    1168       try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
    1169       try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    1170       whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    1171       whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    1172       <FETCH in classifier_assm;
    1173       try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
    1174       whd in ⊢ (?(??%?)(??%?) → ?); #absurd
    1175       cases absurd #absurd destruct(absurd)
    1176     |2:
    1177       cases daemon (* XXX: ??? *)
    1178     ]
    11791231  |62,63,64,65,66,67,68,69,70,101,102,103:
    11801232    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     
    12871339        nat_of_bitvector … program_counter'')
    12881340    assumption
    1289   ] *)
     1341  ]
    12901342qed.
    12911343
  • src/ASM/Interpret.ma

    r1709 r1710  
    120120include alias "ASM/BitVectorTrie.ma".
    121121
     122definition ASM_classify00: ∀a. preinstruction a → status_class ≝
     123  λa, pre.
     124  match pre with
     125  [ RET ⇒ cl_return
     126  | RETI ⇒ cl_return
     127  | JZ _ ⇒ cl_jump
     128  | JNZ _ ⇒ cl_jump
     129  | JC _ ⇒ cl_jump
     130  | JNC _ ⇒ cl_jump
     131  | JB _ _ ⇒ cl_jump
     132  | JNB _ _ ⇒ cl_jump
     133  | JBC _ _ ⇒ cl_jump
     134  | CJNE _ _ ⇒ cl_jump
     135  | DJNZ _ _ ⇒ cl_jump
     136  | _ ⇒ cl_other
     137  ].
     138
    122139definition ASM_classify0: instruction → status_class ≝
    123   λi: instruction.
     140  λi.
    124141  match i with
    125    [ RealInstruction pre ⇒
    126      match pre with
    127       [ RET ⇒ cl_return
    128       | JZ _ ⇒ cl_jump
    129       | JNZ _ ⇒ cl_jump
    130       | JC _ ⇒ cl_jump
    131       | JNC _ ⇒ cl_jump
    132       | JB _ _ ⇒ cl_jump
    133       | JNB _ _ ⇒ cl_jump
    134       | JBC _ _ ⇒ cl_jump
    135       | CJNE _ _ ⇒ cl_jump
    136       | DJNZ _ _ ⇒ cl_jump
    137       | _ ⇒ cl_other
    138       ]
     142   [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
    139143   | ACALL _ ⇒ cl_call
    140144   | LCALL _ ⇒ cl_call
     
    163167definition execute_1_preinstruction':
    164168  ∀ticks: nat × nat.
    165   ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
     169  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
    166170  ∀s: PreStatus m cm.
    167171    Σs': PreStatus m cm.
    168172      And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
    169         (ASM_classify cm s' = cl_other → program_counter … s' = \fst (\snd (fetch … s))) ≝
     173        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝
    170174  λticks: nat × nat.
    171175  λa, m: Type[0]. λcm.
     
    175179  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
    176180  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
    177   match instr in preinstruction return λx. Σs': ?. ? with
    178         [ ADD addr1 addr2 ⇒
     181  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
     182    And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     183      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with
     184        [ ADD addr1 addr2 ⇒ λinstr_refl.
    179185            let s ≝ add_ticks1 s in
    180186            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
     
    185191            let s ≝ set_arg_8 … s ACC_A result in
    186192              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
    187         | ADDC addr1 addr2 ⇒
     193        | ADDC addr1 addr2 ⇒ λinstr_refl.
    188194            let s ≝ add_ticks1 s in
    189195            let old_cy_flag ≝ get_cy_flag ?? s in
     
    195201            let s ≝ set_arg_8 … s ACC_A result in
    196202              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
    197         | SUBB addr1 addr2 ⇒
     203        | SUBB addr1 addr2 ⇒ λinstr_refl.
    198204            let s ≝ add_ticks1 s in
    199205            let old_cy_flag ≝ get_cy_flag ?? s in
     
    205211            let s ≝ set_arg_8 … s ACC_A result in
    206212              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
    207         | ANL addr ⇒
     213        | ANL addr ⇒ λinstr_refl.
    208214          let s ≝ add_ticks1 s in
    209215          match addr with
     
    224230               set_flags … s and_val (None ?) (get_ov_flag ?? s)
    225231            ]
    226         | ORL addr ⇒
     232        | ORL addr ⇒ λinstr_refl.
    227233          let s ≝ add_ticks1 s in
    228234          match addr with
     
    243249               set_flags … s or_val (None ?) (get_ov_flag … s)
    244250            ]
    245         | XRL addr ⇒
     251        | XRL addr ⇒ λinstr_refl.
    246252          let s ≝ add_ticks1 s in
    247253          match addr with
     
    255261                set_arg_8 … s addr1 xor_val
    256262            ]
    257         | INC addr ⇒
    258             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     263        | INC addr ⇒ λinstr_refl.
     264            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
    259265              [ ACC_A ⇒ λacc_a: True.
    260266                let s' ≝ add_ticks1 s in
     
    281287              | _ ⇒ λother: False. ⊥
    282288              ] (subaddressing_modein … addr)
    283         | NOP ⇒
     289        | NOP ⇒ λinstr_refl.
    284290           let s ≝ add_ticks2 s in
    285291            s
    286         | DEC addr ⇒
     292        | DEC addr ⇒ λinstr_refl.
    287293           let s ≝ add_ticks1 s in
    288294           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
    289295             set_arg_8 … s addr result
    290         | MUL addr1 addr2 ⇒
     296        | MUL addr1 addr2 ⇒ λinstr_refl.
    291297           let s ≝ add_ticks1 s in
    292298           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     
    298304           let s ≝ set_8051_sfr … s SFR_ACC_A low in
    299305             set_8051_sfr … s SFR_ACC_B high
    300         | DIV addr1 addr2 ⇒
     306        | DIV addr1 addr2 ⇒ λinstr_refl.
    301307           let s ≝ add_ticks1 s in
    302308           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
     
    311317                   set_flags … s false (None Bit) false
    312318               ]
    313         | DA addr ⇒
     319        | DA addr ⇒ λinstr_refl.
    314320            let s ≝ add_ticks1 s in
    315321            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     
    327333              else
    328334                s
    329         | CLR addr ⇒
    330           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     335        | CLR addr ⇒ λinstr_refl.
     336          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
    331337            [ ACC_A ⇒ λacc_a: True.
    332338              let s ≝ add_ticks1 s in
     
    340346            | _ ⇒ λother: False. ⊥
    341347            ] (subaddressing_modein … addr)
    342         | CPL addr ⇒
    343           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     348        | CPL addr ⇒ λinstr_refl.
     349          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
    344350            [ ACC_A ⇒ λacc_a: True.
    345351                let s ≝ add_ticks1 s in
     
    359365            | _ ⇒ λother: False. ?
    360366            ] (subaddressing_modein … addr)
    361         | SETB b ⇒
     367        | SETB b ⇒ λinstr_refl.
    362368            let s ≝ add_ticks1 s in
    363369            set_arg_1 … s b false
    364         | RL _ ⇒ (* DPM: always ACC_A *)
     370        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    365371            let s ≝ add_ticks1 s in
    366372            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    367373            let new_acc ≝ rotate_left … 1 old_acc in
    368374              set_8051_sfr … s SFR_ACC_A new_acc
    369         | RR _ ⇒ (* DPM: always ACC_A *)
     375        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    370376            let s ≝ add_ticks1 s in
    371377            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    372378            let new_acc ≝ rotate_right … 1 old_acc in
    373379              set_8051_sfr … s SFR_ACC_A new_acc
    374         | RLC _ ⇒ (* DPM: always ACC_A *)
     380        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    375381            let s ≝ add_ticks1 s in
    376382            let old_cy_flag ≝ get_cy_flag ?? s in
     
    380386            let s ≝ set_arg_1 … s CARRY new_cy_flag in
    381387              set_8051_sfr … s SFR_ACC_A new_acc
    382         | RRC _ ⇒ (* DPM: always ACC_A *)
     388        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    383389            let s ≝ add_ticks1 s in
    384390            let old_cy_flag ≝ get_cy_flag ?? s in
     
    388394            let s ≝ set_arg_1 … s CARRY new_cy_flag in
    389395              set_8051_sfr … s SFR_ACC_A new_acc
    390         | SWAP _ ⇒ (* DPM: always ACC_A *)
     396        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
    391397            let s ≝ add_ticks1 s in
    392398            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
     
    394400            let new_acc ≝ nl @@ nu in
    395401              set_8051_sfr … s SFR_ACC_A new_acc
    396         | PUSH addr ⇒
    397             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
     402        | PUSH addr ⇒ λinstr_refl.
     403            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
    398404              [ DIRECT d ⇒ λdirect: True.
    399405                let s ≝ add_ticks1 s in
     
    403409              | _ ⇒ λother: False. ⊥
    404410              ] (subaddressing_modein … addr)
    405         | POP addr ⇒
     411        | POP addr ⇒ λinstr_refl.
    406412            let s ≝ add_ticks1 s in
    407413            let contents ≝ read_at_stack_pointer ?? s in
     
    409415            let s ≝ set_8051_sfr … s SFR_SP new_sp in
    410416              set_arg_8 … s addr contents
    411         | XCH addr1 addr2 ⇒
     417        | XCH addr1 addr2 ⇒ λinstr_refl.
    412418            let s ≝ add_ticks1 s in
    413419            let old_addr ≝ get_arg_8 … s false addr2 in
     
    415421            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
    416422              set_arg_8 … s addr2 old_acc
    417         | XCHD addr1 addr2 ⇒
     423        | XCHD addr1 addr2 ⇒ λinstr_refl.
    418424            let s ≝ add_ticks1 s in
    419425            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     
    421427            let new_acc ≝ acc_nu @@ arg_nl in
    422428            let new_arg ≝ arg_nu @@ acc_nl in
    423             let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     429            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
    424430              set_arg_8 … s addr2 new_arg
    425         | RET ⇒
     431        | RET ⇒ λinstr_refl.
    426432            let s ≝ add_ticks1 s in
    427433            let high_bits ≝ read_at_stack_pointer ?? s in
     
    433439            let new_pc ≝ high_bits @@ low_bits in
    434440              set_program_counter … s new_pc
    435         | RETI ⇒
     441        | RETI ⇒ λinstr_refl.
    436442            let s ≝ add_ticks1 s in
    437443            let high_bits ≝ read_at_stack_pointer ?? s in
     
    443449            let new_pc ≝ high_bits @@ low_bits in
    444450              set_program_counter … s new_pc
    445         | MOVX addr ⇒
     451        | MOVX addr ⇒ λinstr_refl.
    446452          let s ≝ add_ticks1 s in
    447453          (* DPM: only copies --- doesn't affect I/O *)
     
    454460                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
    455461            ]
    456         | MOV addr ⇒
     462        | MOV addr ⇒ λinstr_refl.
    457463          let s ≝ add_ticks1 s in
    458464          match addr with
     
    488494               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
    489495            ]
    490           | JC addr ⇒
     496          | JC addr ⇒ λinstr_refl.
    491497                  if get_cy_flag ?? s then
    492498                    let s ≝ add_ticks1 s in
     
    495501                    let s ≝ add_ticks2 s in
    496502                      s
    497             | JNC addr ⇒
     503            | JNC addr ⇒ λinstr_refl.
    498504                  if ¬(get_cy_flag ?? s) then
    499505                   let s ≝ add_ticks1 s in
     
    502508                   let s ≝ add_ticks2 s in
    503509                    s
    504             | JB addr1 addr2 ⇒
     510            | JB addr1 addr2 ⇒ λinstr_refl.
    505511                  if get_arg_1 … s addr1 false then
    506512                   let s ≝ add_ticks1 s in
     
    509515                   let s ≝ add_ticks2 s in
    510516                    s
    511             | JNB addr1 addr2 ⇒
     517            | JNB addr1 addr2 ⇒ λinstr_refl.
    512518                  if ¬(get_arg_1 … s addr1 false) then
    513519                   let s ≝ add_ticks1 s in
     
    516522                   let s ≝ add_ticks2 s in
    517523                    s
    518             | JBC addr1 addr2 ⇒
     524            | JBC addr1 addr2 ⇒ λinstr_refl.
    519525                  let s ≝ set_arg_1 … s addr1 false in
    520526                    if get_arg_1 … s addr1 false then
     
    524530                     let s ≝ add_ticks2 s in
    525531                      s
    526             | JZ addr ⇒
     532            | JZ addr ⇒ λinstr_refl.
    527533                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
    528534                     let s ≝ add_ticks1 s in
     
    531537                     let s ≝ add_ticks2 s in
    532538                      s
    533             | JNZ addr ⇒
     539            | JNZ addr ⇒ λinstr_refl.
    534540                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
    535541                     let s ≝ add_ticks1 s in
     
    538544                     let s ≝ add_ticks2 s in
    539545                      s
    540             | CJNE addr1 addr2 ⇒
     546            | CJNE addr1 addr2 ⇒ λinstr_refl.
    541547                  match addr1 with
    542548                    [ inl l ⇒
     
    563569                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
    564570                    ]
    565             | DJNZ addr1 addr2 ⇒
     571            | DJNZ addr1 addr2 ⇒ λinstr_refl.
    566572              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
    567573              let s ≝ set_arg_8 … s addr1 result in
     
    572578                 let s ≝ add_ticks2 s in
    573579                  s
    574  |_ ⇒ ?            ]. (*15s*)
     580            ] (refl … instr).
    575581    try (cases(other))
    576582    try assumption (*20s*)
    577583    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    578584    try (
    579       @ (execute_1_technical … (subaddressing_modein …))
    580       @ I
     585      @(execute_1_technical … (subaddressing_modein …))
     586      @I
    581587    ) (*66s*)
    582     normalize nodelta /2 by or_introl, or_intror/ (*35s*)
    583     (*CSC: the times are now much longer. I suspect because the inclusion of
    584       all StatusProofs makes the search space larger :-( *)
     588    normalize nodelta %
     589    try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
     590    try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd))
     591    try (@or_introl //)
     592    try (@or_intror //)
     593    #_ /demod/ %
    585594qed.
    586595
     
    592601lemma execute_1_preinstruction_ok:
    593602 ∀ticks,a,m,cm,f,i,s.
    594   clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
    595   clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s.
     603  (clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
     604  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
     605    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
    596606 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
    597607qed.
     
    707717    #absurd normalize in absurd; try destruct(absurd) try %
    708718  |9:
    709    
    710     [1,2,3,4,5,7: @pi2 (*35s*)
    711     |8: cases daemon (*
    712     lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] …
     719    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
    713720        (λx. λs.
    714721        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    715722        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
    716723        | _ ⇒ λabsd. ⊥
    717         ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H *)
    718       (*XXX : propagate further *)
    719     |28,48,68,88,108,128: skip
    720     |*:
    721       try assumption
    722        normalize nodelta
    723        try // >clock_set_program_counter %
    724        try // destruct destruct (* XXX: for wilmer! *) >e1
    725        whd in match ASM_classify; normalize nodelta
    726        whd in match current_instruction; normalize nodelta
    727        whd in match current_instruction0; normalize nodelta
    728     [||||||||*:try assumption]
    729     |*: normalize nodelta try // (*17s*)
    730         >clock_set_program_counter // (* Andrea:??*) ]
     724        ] (subaddressing_modein … x)) instr' s) try @absd
     725    #clock_proof #classify_proof %
     726    [1:
     727      cases clock_proof #clock_proof' >clock_proof'
     728      destruct(INSTR_PC_TICKS) %
     729    |2:
     730      #classify_assm -clock_proof >classify_proof -classify_proof
     731      [1:
     732        normalize nodelta normalize <INSTR_PC_TICKS
     733        destruct(INSTR_PC) %
     734      |2:
     735        <classify_assm <INSTR_PC_TICKS destruct <e0 %
     736      ]
     737    ]
     738  ]
    731739qed.
    732740
     
    736744
    737745definition execute_1': ∀cm.∀s:Status cm.
    738   Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝
     746  Σs':Status cm.
     747    And (clock ?? s' = current_instruction_cost cm s + clock … s)
     748      (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝
    739749  λcm. λs: Status cm.
    740     let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    741      execute_1_0 cm s instr_pc_ticks.
     750  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     751    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
     752  %
     753  [1:
     754    cases(execute_1_0 cm s instr_pc_ticks)
     755    #the_status * #clock_assm #_ @clock_assm
     756  |2:
     757    cases(execute_1_0 cm s instr_pc_ticks)
     758    #the_status * #_ #classify_assm #classify_assm'
     759    lapply(classify_assm ?)
     760    [1:
     761      change with (
     762        ASM_classify cm s = cl_other
     763      )
     764      assumption
     765    |2:
     766      #program_counter_refl >program_counter_refl %
     767    ]
     768  ]
     769qed.
    742770
    743771definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
    744772
    745 lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     773lemma execute_1_ok: ∀cm.∀s.
     774  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     775    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)).
    746776 #cm #s whd in match execute_1; normalize nodelta @pi2
    747777qed-. (*x Andrea: indexing takes ages here *)
  • src/ASM/StatusProofs.ma

    r1666 r1710  
    333333qed.
    334334
     335axiom program_counter_set_bit_addressable_sfr:
     336  ∀m, cm, s, addr, v.
     337   program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s.
     338
     339(* XXX: to be moved elsewhere *)
     340lemma program_counter_set_arg_8:
     341  ∀m, cm, s, addr, v.
     342   program_counter m cm (set_arg_8 m cm s addr v) = program_counter m cm s.
     343  #m #cm #s #addr #byte
     344  whd in match set_arg_8; normalize nodelta
     345  whd in match set_arg_8'; normalize nodelta
     346  cases addr #subaddressing_modein_proof
     347  cases subaddressing_modein_proof
     348  try (#addr normalize in addr; cases addr)
     349  try (#ignore #addr normalize in addr; cases addr)
     350  normalize nodelta try #_ try /demod/ try %
     351  cases (split bool 4 4 ?) #nu #nl normalize nodelta
     352  cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     353  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
     354qed.
     355
     356lemma program_counter_set_arg_1:
     357  ∀m, cm, s, addr, v.
     358   program_counter m cm (set_arg_1 m cm s addr v) = program_counter m cm s.
     359  #m #cm #s #addr #v
     360  whd in match set_arg_1; normalize nodelta
     361  whd in match set_arg_1'; normalize nodelta
     362  cases addr #subaddressing_modein_proof
     363  cases subaddressing_modein_proof
     364  try (#ignore #addr normalize in addr; cases addr)
     365  try (#addr normalize in addr; cases addr)
     366  normalize nodelta
     367  cases (split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
     368  cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     369  cases (get_index_v bool 4 nu ??) normalize nodelta try /demod/ try %
     370qed.
     371
     372lemma program_counter_set_arg_16:
     373  ∀m, cm, s, addr, v.
     374   program_counter m cm (set_arg_16 m cm s v addr) = program_counter m cm s.
     375  #m #cm #s #addr #v
     376  whd in match set_arg_16; normalize nodelta
     377  whd in match set_arg_16'; normalize nodelta
     378  cases addr #subaddressing_modein_proof
     379  cases subaddressing_modein_proof
     380  try (#ignore #addr normalize in addr; cases addr)
     381  try (#addr normalize in addr; cases addr)
     382  normalize nodelta
     383  cases (split bool 8 8 v) #bu #bl normalize nodelta /demod/ %
     384qed.
     385
     386lemma program_counter_set_low_internal_ram:
     387  ∀m, cm, s, v.
     388   program_counter m cm (set_low_internal_ram m cm s v) = program_counter m cm s.
     389  #m #cm #s #v
     390  whd in match set_low_internal_ram; normalize nodelta %
     391qed.
     392
     393lemma program_counter_set_high_internal_ram:
     394  ∀m, cm, s, v.
     395   program_counter m cm (set_high_internal_ram m cm s v) = program_counter m cm s.
     396  #m #cm #s #v
     397  whd in match set_high_internal_ram; normalize nodelta %
     398qed.
     399
     400lemma program_counter_write_at_stack_pointer:
     401  ∀m, cm, s, v.
     402   program_counter m cm (write_at_stack_pointer m cm s v) = program_counter m cm s.
     403  #m #cm #s #v
     404  whd in match write_at_stack_pointer; normalize nodelta
     405  cases (split bool 4 4 ?) #nu #nl normalize nodelta
     406  cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
     407qed.
     408
    335409axiom get_arg_8_set_low_internal_ram:
    336  ∀M,cm,s,x,b,z. get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
     410  ∀M,cm,s,x,b,z.
     411    get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
    337412
    338413lemma split_eq_status:
Note: See TracChangeset for help on using the changeset viewer.