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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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    ]
Note: See TracChangeset for help on using the changeset viewer.