Changeset 2129


Ignore:
Timestamp:
Jun 27, 2012, 7:14:32 PM (5 years ago)
Author:
mulligan
Message:

Large changes from today trying to complete the main theorem. Again :(

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2128 r2129  
    6464          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
    6565           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
     66  cases daemon
     67(* XXX: commented out as takes ages to typecheck
    6668  #pc #i #code_memory #assembled cases i [8: *]
    6769 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
     
    8385 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
    8486 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
    85  try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl
     87 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
    8688qed.
    8789
     
    936938  ∀i: instruction.
    937939    |(assembly1 i)| < 128.
     940  cases daemon
     941(* XXX: commented out as takes ages to type check
    938942  #i cases i
    939943  try (#assm1 #assm2) try #assm1
     
    10041008    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
    10051009  ]
    1006 qed.
     1010  *)
     1011qed.
  • src/ASM/AssemblyProofSplit.ma

    r2124 r2129  
    400400                      status_of_pseudo_status M' cm s sigma policy).
    401401    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
     402  cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *)
     403  (*
    402404  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    403405  #costs #create_label_cost_refl #newppc
     
    13711373  (* XXX: finally, prove the equality using sigma commutation *)
    13721374  cases daemon
    1373   ]
    1374 qed.
     1375  ] *)
     1376qed.
  • src/ASM/AssemblyProofSplitSplit.ma

    r2127 r2129  
    3838  >(eq_bv_eq … relevant) %
    3939qed.
    40        
     40 
    4141theorem main_thm:
    4242  ∀M, M': internal_pseudo_address_map.
    4343  ∀program: pseudo_assembly_program.
     44  ∀program_in_bounds: |\snd program| ≤ 2^16.
     45  ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16.
    4446  ∀is_well_labelled: is_well_labelled_p (\snd program).
    4547  ∀sigma: Word → Word.
     
    4850  ∀ps: PseudoStatus program.
    4951  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
    50     next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' →
     52    next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
    5153      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    5254        status_of_pseudo_status M' …
    5355          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
    54   #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
    55   letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
    56   change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    57   generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
    58   @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
    59   @pair_elim #assembled #costs' #assembly_refl normalize nodelta
    60   lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
    61   @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
    62   @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
    63   @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    64   whd in match execute_1_pseudo_instruction; normalize nodelta
    65   whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
    66   lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
    67   lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
    68   [1: >fetch_pseudo_refl % |2: skip ]
    69   #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
    70   generalize in match assm1; -assm1 -assm2 -assm3
    71   normalize nodelta
    72   inversion pi
    73   [2,3:
    74     #arg #_
    75     (* XXX: we first work on sigma_increment_commutation *)
    76     #sigma_increment_commutation
    77     normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
    78     (* XXX: we work on the maps *)
    79     whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
    80     (* XXX: we assume the fetch_many hypothesis *)
    81     #fetch_many_assm
    82     (* XXX: we give the existential *)
    83     %{0}
    84     whd in match (execute_1_pseudo_instruction0 ?????);
    85     (* XXX: work on the left hand side of the equality *)
    86     whd in ⊢ (??%?);
    87     @split_eq_status try %
    88     /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
    89   |6: (* Mov *)
    90     #arg1 #arg2 #_
    91     (* XXX: we first work on sigma_increment_commutation *)
    92     #sigma_increment_commutation
    93     normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
    94     (* XXX: we work on the maps *)
    95     whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
    96     (* XXX: we assume the fetch_many hypothesis *)
    97     #fetch_many_assm
    98     (* XXX: we give the existential *)
    99     %{1}
    100     whd in match (execute_1_pseudo_instruction0 ?????);
    101     (* XXX: work on the left hand side of the equality *)
    102     whd in ⊢ (??%?); whd in match (program_counter ???);
    103     (* XXX: execute fetches some more *)
    104     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    105     whd in fetch_many_assm;
    106     >EQassembled in fetch_many_assm;
    107     cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
    108     #eq_instr
    109     #fetch_many_assm whd in fetch_many_assm;
    110     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    111     destruct whd in ⊢ (??%?);
    112     (* XXX: now we start to work on the mk_PreStatus equality *)
    113     (* XXX: lhs *)
    114     change with (set_arg_16 ????? = ?)
    115     >set_program_counter_mk_Status_commutation
    116     >set_clock_mk_Status_commutation
    117     >set_arg_16_mk_Status_commutation
    118     (* XXX: rhs *)
    119     change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
    120     >set_program_counter_mk_Status_commutation
    121     >set_clock_mk_Status_commutation
    122     >set_arg_16_mk_Status_commutation in ⊢ (???%);
    123     (* here we are *)
    124     @split_eq_status try %
    125     [1:
    126       assumption
    127     |2:
    128       @special_function_registers_8051_set_arg_16 %
    129     ]
    130   |1: (* Instruction *)
    131     #instr #_ #EQP #EQnext #fetch_many_assm
    132     @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
    133       ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
    134       EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
    135       (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
    136       (refl …) ? (refl …))
    137     try assumption try % >assembly_refl assumption
    138   |4: (* Jmp *)
    139     #arg1 #pi_refl
    140     (* XXX: we first work on sigma_increment_commutation *)
    141     whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
    142     whd in match (expand_pseudo_instruction ??????);
    143     inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
    144     inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
    145     [2:
    146       inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
    147       inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
    148     ]
    149     #sigma_increment_commutation
    150     normalize in sigma_increment_commutation:(???(???(??%)));
    151     (* XXX: we work on the maps *)
    152     whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
    153     (* XXX: we assume the fetch_many hypothesis *)
    154     * #fetch_refl #fetch_many_assm
    155     (* XXX: we give the existential *)
    156     %{1}
    157     (* XXX: work on the left hand side of the equality *)
    158     whd in ⊢ (??%?); whd in match (program_counter ???);
    159     (* XXX: execute fetches some more *)
    160     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    161     whd in fetch_many_assm;
    162     >EQassembled in fetch_refl; #fetch_refl <fetch_refl
    163     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    164     whd in ⊢ (??%%);
    165     (* XXX: now we start to work on the mk_PreStatus equality *)
    166     (* XXX: lhs *)
    167     (* XXX: rhs *)
    168     (* here we are *)
    169     @split_eq_status try % /demod nohyps/
    170     [1,3,4:
    171       change with (add ???) in match (\snd (half_add ???));
    172       whd in match execute_1_pseudo_instruction0; normalize nodelta
    173       /demod nohyps/ >set_clock_set_program_counter
    174       >program_counter_set_program_counter
    175       whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
    176       lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
    177       normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
     56    #M #M' * #preamble #instr_list #program_in_bounds #addr_of
     57    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
     58    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
     59    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
     60    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
     61    @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
     62    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
     63    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
     64    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
     65    @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
     66    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
     67    whd in match execute_1_pseudo_instruction; normalize nodelta
     68    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
     69    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
     70    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
     71    [1: >fetch_pseudo_refl % |2: skip |3: assumption ]
     72    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
     73    generalize in match assm1; -assm1 -assm2 -assm3
     74    normalize nodelta
     75    inversion pi
     76    [(*2,3:
     77      #arg #_
     78      (* XXX: we first work on sigma_increment_commutation *)
     79      #sigma_increment_commutation
     80      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
     81      (* XXX: we work on the maps *)
     82      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     83      (* XXX: we assume the fetch_many hypothesis *)
     84      #fetch_many_assm
     85      (* XXX: we give the existential *)
     86      %{0}
     87      whd in match (execute_1_pseudo_instruction0 ?????);
     88      (* XXX: work on the left hand side of the equality *)
     89      whd in ⊢ (??%?);
     90      @split_eq_status try %
     91      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
     92    |6: (* Mov *)
     93      #arg1 #arg2 #_
     94      (* XXX: we first work on sigma_increment_commutation *)
     95      #sigma_increment_commutation
     96      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
     97      (* XXX: we work on the maps *)
     98      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     99      (* XXX: we assume the fetch_many hypothesis *)
     100      #fetch_many_assm
     101      (* XXX: we give the existential *)
     102      %{1}
     103      whd in match (execute_1_pseudo_instruction0 ?????);
     104      (* XXX: work on the left hand side of the equality *)
     105      whd in ⊢ (??%?); whd in match (program_counter ???);
     106      (* XXX: execute fetches some more *)
     107      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     108      whd in fetch_many_assm;
     109      >EQassembled in fetch_many_assm;
     110      cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
     111      #eq_instr
     112      #fetch_many_assm whd in fetch_many_assm;
     113      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     114      destruct whd in ⊢ (??%?);
     115      (* XXX: now we start to work on the mk_PreStatus equality *)
     116      (* XXX: lhs *)
     117      change with (set_arg_16 ????? = ?)
     118      >set_program_counter_mk_Status_commutation
     119      >set_clock_mk_Status_commutation
     120      >set_arg_16_mk_Status_commutation
     121      (* XXX: rhs *)
     122      change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
     123      >set_program_counter_mk_Status_commutation
     124      >set_clock_mk_Status_commutation
     125      >set_arg_16_mk_Status_commutation in ⊢ (???%);
     126      (* here we are *)
     127      @split_eq_status try %
    178128      [1:
    179         >EQnewpc
    180         inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
    181         @sym_eq >address_of_word_labels_assm
     129        assumption
     130      |2:
     131        @special_function_registers_8051_set_arg_16 %
     132      ]
     133    |1: (* Instruction *)
     134      #instr #_ #EQP #EQnext #fetch_many_assm
     135      @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
     136        ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
     137        EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
     138        (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
     139        (refl …) ? (refl …))
     140      try assumption try % >assembly_refl assumption
     141    |4: (* Jmp *)
     142      #arg1 #pi_refl
     143      (* XXX: we first work on sigma_increment_commutation *)
     144      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
     145      whd in match (expand_pseudo_instruction ??????);
     146      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
     147      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
     148      [2:
     149        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
     150        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
     151      ]
     152      #sigma_increment_commutation
     153      normalize in sigma_increment_commutation:(???(???(??%)));
     154      (* XXX: we work on the maps *)
     155      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     156      (* XXX: we assume the fetch_many hypothesis *)
     157      * #fetch_refl #fetch_many_assm
     158      (* XXX: we give the existential *)
     159      %{1}
     160      (* XXX: work on the left hand side of the equality *)
     161      whd in ⊢ (??%?); whd in match (program_counter ???);
     162      (* XXX: execute fetches some more *)
     163      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     164      whd in fetch_many_assm;
     165      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
     166      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     167      whd in ⊢ (??%%);
     168      (* XXX: now we start to work on the mk_PreStatus equality *)
     169      (* XXX: lhs *)
     170      (* XXX: rhs *)
     171      (* here we are *)
     172      @split_eq_status try % /demod nohyps/
     173      [1,3,4:
     174        change with (add ???) in match (\snd (half_add ???));
     175        whd in match execute_1_pseudo_instruction0; normalize nodelta
     176        /demod nohyps/ >set_clock_set_program_counter
     177        >program_counter_set_program_counter
     178        whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
     179        lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
     180        normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
    182181        [1:
    183           >EQlookup_labels in mjc_refl; #mjc_refl
    184           @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
    185           >(andb_true_l … mj_possible_refl) @I
     182          >EQnewpc
     183          inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
     184          @sym_eq >address_of_word_labels_assm
     185          [1:
     186            >EQlookup_labels in mjc_refl; #mjc_refl
     187            @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
     188            >(andb_true_l … mj_possible_refl) @I
     189          ]
     190        |3:
     191          >EQlookup_labels normalize nodelta
     192          >address_of_word_labels_assm try %
     193        |5:
     194          >EQnewpc
     195          inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
     196          @sym_eq >address_of_word_labels_assm
     197          [1:
     198            >EQlookup_labels in sjc_refl; #sjc_refl
     199            >(pair_destruct_2 ????? (sym_eq … half_add_refl))
     200            @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
     201            >(andb_true_l … sj_possible_refl) @I
     202          ]
    186203        ]
    187       |3:
    188         >EQlookup_labels normalize nodelta
    189         >address_of_word_labels_assm try %
    190       |5:
    191         >EQnewpc
    192         inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
    193         @sym_eq >address_of_word_labels_assm
    194         [1:
    195           >EQlookup_labels in sjc_refl; #sjc_refl
    196           >(pair_destruct_2 ????? (sym_eq … half_add_refl))
    197           @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
    198           >(andb_true_l … sj_possible_refl) @I
     204        @(is_well_labelled_witness … fetch_pseudo_refl)
     205        >pi_refl %
     206      |2:
     207        whd in ⊢ (??(?%%)%);
     208        cases (bitvector_11_cases address)
     209        * * * * * * #b4 * #b5
     210        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
     211        normalize in match (fetch ??); <plus_n_Sm @eq_f
     212        @commutative_plus
     213      ]
     214    |*)5: (* Call *)
     215      #arg1 #pi_refl
     216      (* XXX: we first work on sigma_increment_commutation *)
     217      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
     218      whd in match (expand_pseudo_instruction ??????);
     219      whd in match (execute_1_pseudo_instruction0 ?????);
     220      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
     221      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
     222      @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) -carry_new_sp_refl #carry_new_sp_refl
     223      @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) -pc_bu_bl_refl #pc_bu_bl_refl
     224      @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') -carry_new_sp_refl' #carry_new_sp_refl'
     225      #sigma_increment_commutation
     226      normalize in sigma_increment_commutation:(???(???(??%)));
     227      (* XXX: we work on the maps *)
     228      whd in ⊢ (??%? → ?);
     229      @pair_elim #callM #accM #Mrefl
     230      @Some_Some_elim #map_refl_assm <map_refl_assm
     231      (* XXX: we assume the fetch_many hypothesis *)
     232      * #fetch_refl #fetch_many_assm
     233      (* XXX: we give the existential *)
     234      %{1}
     235      (* XXX: work on the left hand side of the equality *)
     236      whd in ⊢ (??%?); whd in match (program_counter ???);
     237      (* XXX: execute fetches some more *)
     238      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     239      whd in fetch_many_assm;
     240      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
     241      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     242      whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …));
     243      normalize in match (length ? (assembly1 …)) in EQnewpc;
     244      normalize nodelta
     245      [1:
     246        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
     247        try /demod nohyps/ [1: %]
     248        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
     249        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
     250        try /demod nohyps/ [1: %]
     251        @pair_elim #thr #eig #thr_eig_refl
     252        @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
     253        @split_eq_status try /demod nohyps/ try %
     254        [1,2:
     255          (* XXX: need the commented out axioms from AssemblyProof.ma *)
     256          cases daemon
     257        |3:
     258          >program_counter_set_program_counter
     259          whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
     260          >EQlookup_labels normalize nodelta
     261          @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta
     262          <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
     263          #relevant >fst_5_rest_refl
     264          check absolute_jump_cond
     265          <(vsplit_ok ?????? (sym_eq … thr_eig_refl))
     266          lapply pc_bu_bl_refl' -pc_bu_bl_refl'
     267          >program_counter_set_8051_sfr >set_clock_set_program_counter
     268          >program_counter_set_program_counter >fst_5_rest_pc_refl
     269          cut(fst_5_addr = fst_5_pc)
     270          [1:
     271            cases daemon (* XXX: !! *)
     272          |2:
     273            #relevant2 >relevant2
     274            <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
     275            #relevant3
     276            lapply(vsplit_ok ?????? (sym_eq … relevant3))
     277            >(vector_associative_append bool 5 3 8) #relevant4
     278            cut(fiv = fst_5_pc ∧ thr'@@pc_bl' = rest_pc)
     279            [1:
     280              cases daemon (* XXX: !! *)
     281            |2:
     282              * #relevant5 #relevant6 >relevant5
     283              >(vector_associative_append bool 5 3 8) @eq_f
     284              destruct(relevant)
     285              <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f
     286            ]
     287          ]
     288        |4:
     289          >set_program_counter_mk_Status_commutation in ⊢ (???%);
     290          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
     291          (* XXX: require set_8051_sfr_write_at_stack_pointer and
     292                          special_function_registers_8051_set_8051_sfr
     293          *)
     294          cases daemon
     295        |5,6,7:
     296          >set_program_counter_mk_Status_commutation in ⊢ (???%);
     297          (* XXX: similar to above but for 8052
     298          *)
     299          cases daemon
     300        |8:
     301          whd in match (ticks_of_instruction ?);
     302          cut(\snd  (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2)
     303          [1: //
     304          |2:
     305            normalize in match (assembly1 ?); >thr_eig_refl
     306            @(bitvector_3_elim_prop … thr) %
     307          |3:
     308            #fetch_2_refl >fetch_2_refl >commutative_plus %
     309          ]
     310        |2:
    199311        ]
    200       ]
    201       @(is_well_labelled_witness … fetch_pseudo_refl)
    202       >pi_refl %
    203     |2:
    204       whd in ⊢ (??(?%%)%);
    205       cases (bitvector_11_cases address)
    206       * * * * * * #b4 * #b5
    207       * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
    208       normalize in match (fetch ??); <plus_n_Sm @eq_f
    209       @commutative_plus
    210     ]
    211   |5: (* Call *)
    212     #arg1 #_
    213     (* XXX: we first work on sigma_increment_commutation *)
    214     #sigma_increment_commutation
    215     normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
    216     (* XXX: we work on the maps *)
    217     whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
    218     (* XXX: we assume the fetch_many hypothesis *)
    219     #fetch_many_assm
    220     (* XXX: we give the existential *)
    221     %{1}
    222     whd in match (execute_1_pseudo_instruction0 ?????);
    223     (* XXX: work on the left hand side of the equality *)
    224     whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
    225     (* XXX: execute fetches some more *)
    226     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    227     whd in fetch_many_assm;
    228     >EQassembled in fetch_many_assm;
    229     cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *
    230     #eq_instr
    231     #fetch_many_assm whd in fetch_many_assm;
    232     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    233     destruct whd in ⊢ (??%?);
    234     (* XXX: now we start to work on the mk_PreStatus equality *)
    235     (* XXX: lhs *)
    236     change with (set_arg_16 ????? = ?)
    237     >set_program_counter_mk_Status_commutation
    238     >set_clock_mk_Status_commutation
    239     >set_arg_16_mk_Status_commutation
    240     (* XXX: rhs *)
    241     change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
    242     >set_program_counter_mk_Status_commutation
    243     >set_clock_mk_Status_commutation
    244     >set_arg_16_mk_Status_commutation in ⊢ (???%);
    245     (* here we are *)
    246     @split_eq_status //
    247     [1:
    248       assumption
    249     |2:
    250       @special_function_registers_8051_set_arg_16
    251       [2: %
    252       |1: //
    253312      ]
    254313    ]
  • src/ASM/Interpret.ma

    r2124 r2129  
    10721072          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    10731073            [ ADDR11 a ⇒ λaddr11: True.
     1074              «let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1075              let s ≝ set_8051_sfr … s SFR_SP new_sp in
     1076              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
     1077              let s ≝ write_at_stack_pointer … s pc_bl in
     1078              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1079              let s ≝ set_8051_sfr … s SFR_SP new_sp in
     1080              let s ≝ write_at_stack_pointer … s pc_bu in
     1081              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
     1082              let new_addr ≝ fiv @@ a in
     1083                set_program_counter … s new_addr, ?»
     1084            | _ ⇒ λother: False. ⊥
     1085            ] (subaddressing_modein … addr)
     1086      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
     1087      | LCALL addr ⇒ λinstr_refl.
     1088          let s ≝ set_clock ?? s (ticks + clock … s) in
     1089          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
     1090            [ ADDR16 a ⇒ λaddr16: True.
     1091              «
    10741092              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10751093              let s ≝ set_8051_sfr … s SFR_SP new_sp in
     
    10791097              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10801098              let s ≝ write_at_stack_pointer … s pc_bu in
    1081               let 〈thr, eig〉 ≝ vsplit ? 3 8 a in
    1082               let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
    1083               let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    1084                 set_program_counter … s new_addr
    1085             | _ ⇒ λother: False. ⊥
    1086             ] (subaddressing_modein … addr)
    1087       | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
    1088       | LCALL addr ⇒ λinstr_refl.
    1089           let s ≝ set_clock ?? s (ticks + clock … s) in
    1090           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
    1091             [ ADDR16 a ⇒ λaddr16: True.
    1092               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    1093               let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1094               let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    1095               let s ≝ write_at_stack_pointer … s pc_bl in
    1096               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    1097               let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1098               let s ≝ write_at_stack_pointer … s pc_bu in
    1099                 set_program_counter … s a
     1099                set_program_counter … s a, ?»
    11001100            | _ ⇒ λother: False. ⊥
    11011101            ] (subaddressing_modein … addr)
     
    11061106    try //
    11071107    -s destruct(INSTR_PC) <instr_refl whd
    1108     try (#absurd normalize in absurd; try destruct(absurd) try %) %
     1108    try (#absurd normalize in absurd; try destruct(absurd) try %)
     1109    @pair_elim #carry #new_sp #carry_new_sp_refl
     1110    @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl
     1111    @pair_elim #carry' #new_sp' #carry_new_sp_refl'
     1112    [2:
     1113      /demod nohyps/ %
     1114    |1:
     1115      cases (vsplit ????) #thr #eig normalize nodelta
     1116      cases (vsplit ????) #fiv #thr' normalize nodelta
     1117      /demod by clock_set_program_counter/ /demod nohyps/ %
     1118    ]
    11091119  |9:
    11101120    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
  • src/common/StructuredTraces.ma

    r2044 r2129  
    2525}.
    2626
    27 definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc … (as_pc_of … s).
     27definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
    2828
    2929(* temporary alias for backward compatibility *)
Note: See TracChangeset for help on using the changeset viewer.