Changeset 1927 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 9, 2012, 1:05:21 PM (8 years ago)
Author:
mulligan
Message:

Reduced complexity of good_program predicate, ported to new notion of as_label, reintroduced some deleted code from common/StructuredTraces.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1924 r1927  
    6363      ]
    6464    | LCALL addr         ⇒
    65       match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
     65      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     66        nat_of_bitvector … program_counter' < total_program_size
     67      (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    6668      [ ADDR16 addr ⇒ λaddr16: True.
    6769          reachable_program_counter code_memory total_program_size addr ∧
     
    6971              nat_of_bitvector … program_counter' < total_program_size
    7072      | _ ⇒ λother: False. ⊥
    71       ] (subaddressing_modein … addr)
     73      ] (subaddressing_modein … addr) *)
    7274    | ACALL addr         ⇒
    73       match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
     75      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     76        nat_of_bitvector … program_counter' < total_program_size
     77      (* match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
    7478      [ ADDR11 addr ⇒ λaddr11: True.
    7579        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
     
    8185              nat_of_bitvector … program_counter' < total_program_size
    8286      | _ ⇒ λother: False. ⊥
    83       ] (subaddressing_modein … addr)
     87      ] (subaddressing_modein … addr) *)
    8488    | AJMP  addr         ⇒
    8589      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
     
    98102          nat_of_bitvector … program_counter' < total_program_size
    99103    ].
    100   cases other
    101 qed.
    102 
    103 definition current_instruction_is_labelled
     104(*  cases other
     105qed. *)
     106
     107definition current_instruction_label
    104108  λcode_memory.
    105109  λcost_labels: BitVectorTrie costlabel 16.
    106110  λs: Status code_memory.
    107111  let pc ≝ program_counter … code_memory s in
    108     match lookup_opt … pc cost_labels with
    109     [ None ⇒ False
    110     | _    ⇒ True
    111     ].
     112    lookup_opt … pc cost_labels.
    112113
    113114definition next_instruction_properly_relates_program_counters ≝
     
    159160      (program_counter …)
    160161      (λs,class. ASM_classify … s = class)
    161       (current_instruction_is_labelled … cost_labels)
     162      (current_instruction_label code_memory cost_labels)
    162163      (next_instruction_properly_relates_program_counters code_memory)
    163164      ?.
     
    373374    try (#assm1 #absurd destruct(absurd) @I)
    374375    try (#absurd destruct(absurd) @I)
    375     [1:
     376    (* [1:
    376377      #addr #_
    377378      @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ]
     
    385386    |3:
    386387      #addr #_ *
    387     ]
    388     #relevant #pc_tps_assm'
     388    ] *)
     389    #_ #_ * #relevant #pc_tps_assm'
    389390    whd cases reachable_program_counter_witness * #n
    390391    #Some_assm #_ % try assumption
     
    553554    #new_pc @ltn_to_ltO
    554555  ]
     556qed.
     557
     558lemma not_Some_neq_None_to_False:
     559  ∀a: Type[0].
     560  ∀e: a.
     561    ¬ (Some a e ≠ None a) → False.
     562  #a #e #absurd cases absurd -absurd
     563  #absurd @absurd @nmk -absurd
     564  #absurd destruct(absurd)
    555565qed.
    556566
     
    612622      generalize in match costed_assm;
    613623      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
     624      whd in match (as_label ??);
    614625      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
    615         in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     626        in ⊢ (??%? → % → ?);
    616627      #lookup_assm cases lookup_assm
    617628      [1:
     
    642653        ]
    643654      |2:
    644         #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
    645         #absurd cases absurd #absurd cases(absurd I)
     655        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
     656        #absurd
     657        cases (not_Some_neq_None_to_False ?? absurd)
    646658      ]
    647659    |1:
     
    654666      generalize in match costed_assm;
    655667      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
     668      whd in match (as_label ??);
    656669      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
    657         in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     670        in ⊢ (??%? → % → ?);
    658671      #lookup_assm cases lookup_assm
    659672      [1:
    660         #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
    661         #absurd cases absurd
     673        #None_lookup_opt_assm
     674        #absurd @⊥ cases absurd -absurd #absurd @absurd %
    662675      |2:
    663676        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
     
    841854    generalize in match costed_assm;
    842855    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
     856    whd in match (as_label ??);
    843857    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
    844       in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     858      in ⊢ (??%? → % → ?);
    845859    #lookup_assm cases lookup_assm
    846860    [1:
    847861      #None_lookup_opt normalize nodelta #absurd cases absurd
     862      -absurd #absurd @⊥ @absurd %
    848863    |2:
    849864      #costlabel #Some_lookup_opt normalize nodelta #ignore
     
    876891    generalize in match costed_assm;
    877892    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
     893    whd in match (as_label ??);
    878894    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
    879       in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     895      in ⊢ (??%? → % → ?);
    880896    #lookup_assm cases lookup_assm
    881897    [1:
     
    899915      ]
    900916    |2:
    901       #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
    902       cases absurd #absurd cases (absurd I)
     917      #cost_label #Some_lookup_opt_assm #absurd
     918      cases (not_Some_neq_None_to_False ?? absurd)
    903919    ]
    904920  ]
     
    11211137  ]
    11221138  -block_cost'
    1123   [32:
    1124     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1125     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1126     <FETCH normalize nodelta <instr normalize nodelta
    1127     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    1128     * * * * #n'
    1129     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1130     %
    1131     [1:
    1132       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1133       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1134       >(le_to_leb_true … program_counter_lt') %
    1135     |2:
    1136       assumption
    1137     ]
    1138   |33:
    1139     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1140     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1141     <FETCH normalize nodelta <instr normalize nodelta
    1142     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    1143     cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    1144     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    1145     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    1146     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    1147     %
    1148     [1:
    1149       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1150       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1151       >(le_to_leb_true … program_counter_lt') %
    1152     |2:
    1153       assumption
    1154     ]
    1155   |27,28:
    1156     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1157     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1158     <FETCH normalize nodelta <instr normalize nodelta *
    1159     #program_counter_lt' #program_counter_lt_tps' %
    1160     [1,3:
    1161       %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1162       <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1163       >(le_to_leb_true … program_counter_lt') %
    1164     |2,4:
    1165       assumption
    1166     ]
    1167   |1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26:
    1168     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    1169     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    1170     <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    1171     #program_counter_lt' #program_counter_lt_tps' %
    1172     try assumption
    1173     %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
    1174     <FETCH normalize nodelta whd in match ltb; normalize nodelta
    1175     >(le_to_leb_true … program_counter_lt') %
    1176   |29,30,31: (* XXX: unconditional jumps *)
     1139  [29,30,31: (* XXX: unconditional jumps *)
    11771140    normalize nodelta
    11781141    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    11791142    lapply (good_program_witness program_counter' reachable_program_counter_witness)
    11801143    <FETCH normalize nodelta <instr normalize nodelta #assm assumption
     1144  |*:
     1145    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     1146    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     1147    <FETCH normalize nodelta destruct normalize nodelta
     1148    * #program_counter_lt' #program_counter_lt_tps'
     1149    % try assumption
     1150    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     1151    <FETCH normalize nodelta whd in match ltb; normalize nodelta
     1152    >(le_to_leb_true … program_counter_lt') %
    11811153  ]
    11821154qed.
Note: See TracChangeset for help on using the changeset viewer.