Ignore:
Timestamp:
Jul 13, 2012, 5:03:15 PM (9 years ago)
Author:
mulligan
Message:

More progress on main lemma proof.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2181 r2183  
    191191qed.
    192192
     193lemma match_nat_status_of_pseudo_status:
     194  ∀M, cm, sigma, policy, s, s', s'', s'''.
     195  ∀n, n': nat.
     196    n = n' →
     197    status_of_pseudo_status M cm s' sigma policy = s →
     198    status_of_pseudo_status M cm s''' sigma policy = s'' →
     199      match n with [ O ⇒ s | S n' ⇒ s'' ] =
     200        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''']) sigma policy.
     201  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
     202  #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'
     203  cases n normalize nodelta try % #n' %
     204qed.
     205
    193206(* XXX: copied from Test.ma *)
    194207lemma let_pair_in_status_of_pseudo_status:
    … …  
    210223  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
    211224  destruct(destruct_refl) /2/
     225qed.
     226
     227lemma match_nat_replace:
     228  ∀l, o, p, r, o', p': nat.
     229    l ≃ r →
     230    o ≃ o' →
     231    p ≃ p' →
     232      match l with [ O ⇒ o | S n ⇒ p ] = match r with [ O ⇒ o' | S n' ⇒ p' ].
     233  #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl %
    212234qed.
    213235
    … …  
    238260  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
    239261  ∀ticks: nat × nat.
    240   ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr).
     262  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
    241263  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
    242264  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
    … …  
    669691  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    670692  whd in match execute_1_preinstruction; normalize nodelta
    671 
    672 (*  [31,32: (* DJNZ *)
    673   (* XXX: work on the right hand side *)
    674   >p normalize nodelta >p1 normalize nodelta
    675   (* XXX: switch to the left hand side *)
    676   >EQP -P normalize nodelta
    677   #sigma_increment_commutation #maps_assm #fetch_many_assm
    678   whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    679   <EQppc in fetch_many_assm;
    680   whd in match (short_jump_cond ??);
    681   @pair_elim #sj_possible #disp
    682   @pair_elim #result #flags #sub16_refl
    683   @pair_elim #upper #lower #vsplit_refl
    684   inversion (get_index' bool ???) #get_index_refl' normalize nodelta
    685   #sj_possible_pair destruct(sj_possible_pair)
    686   >p1 normalize nodelta
    687   [1,3:
    688     >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    689     >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    690     normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    691     whd in ⊢ (??%?);
    692     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    693     lapply maps_assm whd in ⊢ (??%? → ?);
    694     inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
    695     [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
    696     (* XXX: work on the left hand side *)
    697     @(pair_replace ?????????? p) normalize nodelta
    698     [1,3:
    699       >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
    700       [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    701       >(get_arg_8_set_program_counter … true addr1)
    702       [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    703       @get_arg_8_pseudo_addressing_mode_ok assumption
    704     |2,4:
    705       >p1 normalize nodelta >EQs
    706       alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
    707       >set_program_counter_status_of_pseudo_status
    708        whd in ⊢ (??%%);
    709       @split_eq_status
    710       [1,10:
    711         whd in ⊢ (??%%); >set_arg_8_set_program_counter
    712         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    713         >low_internal_ram_set_program_counter
    714         [1:
    715           >low_internal_ram_set_program_counter
    716           (* XXX: ??? *)
    717         |2:
    718           >low_internal_ram_set_clock
    719           (* XXX: ??? *)
    720         ]
    721       |2,11:
    722         whd in ⊢ (??%%); >set_arg_8_set_program_counter
    723         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    724         >high_internal_ram_set_program_counter
    725         [1:
    726           >high_internal_ram_set_program_counter
    727           (* XXX: ??? *)
    728         |2:
    729           >high_internal_ram_set_clock
    730           (* XXX: ??? *)
    731         ]
    732       |3,12:
    733         whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
    734         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    735         >(external_ram_set_arg_8 ??? addr1)
    736         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
    737       |4,13:
    738         whd in ⊢ (??%%); >EQaddr_of normalize nodelta
    739         [1:
    740           >program_counter_set_program_counter
    741           >set_arg_8_set_program_counter
    742           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    743           >set_clock_set_program_counter >program_counter_set_program_counter
    744           change with (add ??? = ?)
    745           (* XXX: ??? *)
    746         |2:
    747           >set_arg_8_set_program_counter
    748           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    749           >program_counter_set_program_counter
    750           >set_arg_8_set_program_counter
    751           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    752           >set_clock_set_program_counter >program_counter_set_program_counter
    753           >sigma_increment_commutation <EQppc
    754           whd in match (assembly_1_pseudoinstruction ??????);
    755           whd in match (expand_pseudo_instruction ??????);
    756           (* XXX: ??? *)
    757         ]
    758       |5,14:
    759         whd in match (special_function_registers_8051 ???);
    760         [1:
    761           >special_function_registers_8051_set_program_counter
    762           >special_function_registers_8051_set_clock
    763           >set_arg_8_set_program_counter in ⊢ (???%);
    764           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    765           >special_function_registers_8051_set_program_counter
    766           >set_arg_8_set_program_counter
    767           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    768           >special_function_registers_8051_set_program_counter
    769           @special_function_registers_8051_set_arg_8 assumption
    770         |2:
    771           >special_function_registers_8051_set_clock
    772           >set_arg_8_set_program_counter
    773           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    774           >set_arg_8_set_program_counter
    775           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    776           >special_function_registers_8051_set_program_counter
    777           >special_function_registers_8051_set_program_counter
    778           @special_function_registers_8051_set_arg_8 assumption
    779         ]
    780       |6,15:
    781         whd in match (special_function_registers_8052 ???);
    782         whd in match (special_function_registers_8052 ???) in ⊢ (???%);
    783         [1:
    784           >set_arg_8_set_program_counter
    785           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    786           >set_arg_8_set_program_counter
    787           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    788           >special_function_registers_8052_set_program_counter
    789           >special_function_registers_8052_set_program_counter
    790           @special_function_registers_8052_set_arg_8 assumption
    791         |2:
    792           whd in ⊢ (??%%);
    793           >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
    794         ]
    795         (* XXX: we need special_function_registers_8052_set_arg_8 *)
    796       |7,16:
    797         whd in match (p1_latch ???);
    798         whd in match (p1_latch ???) in ⊢ (???%);
    799         (* XXX: we need p1_latch_8052_set_arg_8 *)
    800       |8,17:
    801         whd in match (p3_latch ???);
    802         whd in match (p3_latch ???) in ⊢ (???%);
    803         (* XXX: we need p3_latch_8052_set_arg_8 *)
    804       |9:
    805         >clock_set_clock
    806         >clock_set_program_counter in ⊢ (???%); >clock_set_clock
    807         >EQticks <instr_refl @eq_f2
    808         [1:
    809           whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
    810         |2:
    811           (* XXX: we need clock_set_arg_8 *)
    812         ]
    813       |18:
    814       ]
    815     ]
    816     (* XXX: switch to the right hand side *)
    817     normalize nodelta >EQs -s >EQticks -ticks
    818     cases (¬ eq_bv ???) normalize nodelta
    819     whd in ⊢ (??%%);
    820     (* XXX: finally, prove the equality using sigma commutation *)
    821     @split_eq_status try %
    822     [1,2,3,19,20,21,28,29,30:
    823       cases daemon (* XXX: axioms as above *)
    824     |4,13,22,31:
    825     |5,14,23,32:
    826     |6,15,24,33:
    827     |7,16,25,34:
    828     |8,17,26,35:
    829       whd in ⊢ (??%%);maps_assm
    830      
    831     |9,18,27,36:
    832       whd in ⊢ (??%%);
    833       whd in match (ticks_of_instruction ?); <instr_refl
    834       cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
    835     ]
    836   |2,4:
    837     >(? : eq_v bool 9 eq_b upper (zero 9) = false)
    838     [2, 4:
    839       cases daemon (* XXX: !!! *)
    840     ]
    841     normalize nodelta >EQppc
    842     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    843     * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    844     * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    845     #fetch_many_assm whd in fetch_many_assm; %{2}
    846     change with (execute_1 ?? = ?)
    847     @(pose … (execute_1 ? (status_of_pseudo_status …)))
    848     #status_after_1 #EQstatus_after_1
    849     <(?: ? = status_after_1)
    850     [3,6:
    851       >EQstatus_after_1 in ⊢ (???%);
    852       whd in ⊢ (???%);
    853       [1:
    854         <fetch_refl in ⊢ (???%);
    855       |2:
    856         <fetch_refl in ⊢ (???%);
    857       ]
    858       whd in ⊢ (???%);
    859       @(pair_replace ?????????? p)
    860       [1,3:
    861         cases daemon
    862       |2,4:
    863         normalize nodelta
    864         whd in match (addr_of_relative ????);
    865         cases (¬ eq_bv ???) normalize nodelta
    866         >set_clock_mk_Status_commutation
    867         whd in ⊢ (???%);
    868         change with (add ???) in match (\snd (half_add ???));
    869         >set_arg_8_set_program_counter in ⊢ (???%);
    870         [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    871         >program_counter_set_program_counter in ⊢ (???%);
    872         >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    873         [2,4,6,8:
    874           >bitvector_of_nat_sign_extension_equivalence
    875           [1,3,5,7:
    876             >EQintermediate_pc' %
    877           |*:
    878             repeat @le_S_S @le_O_n
    879           ]
    880         ]
    881         [1,3: % ]
    882       ]
    883     |1,4:
    884       skip
    885     ]
    886     [3,4:
    887       -status_after_1
    888       @(pose … (execute_1 ? (mk_PreStatus …)))
    889       #status_after_1 #EQstatus_after_1
    890       <(?: ? = status_after_1)
    891       [3,6:
    892         >EQstatus_after_1 in ⊢ (???%);
    893         whd in ⊢ (???%);
    894         (* XXX: matita bug with patterns across multiple goals *)
    895         [1:
    896           <fetch_refl'' in ⊢ (???%);
    897         |2:
    898           <fetch_refl'' in ⊢ (???%);
    899         ]
    900         [2: % |1: whd in ⊢ (???%); % ]
    901       |1,4:
    902         skip
    903       ]
    904       -status_after_1 whd in ⊢ (??%?);
    905       (* XXX: switch to the right hand side *)
    906       normalize nodelta >EQs -s >EQticks -ticks
    907       normalize nodelta whd in ⊢ (??%%);
    908     ]
    909     (* XXX: finally, prove the equality using sigma commutation *)
    910     @split_eq_status try %
    911     whd in ⊢ (??%%);
     693  [4,5,6,7,8,9: (* INC and DEC *)
    912694    cases daemon
    913   ]
    914   |30: (* CJNE *)
    915   (* XXX: work on the right hand side *)
    916   cases addr1 -addr1 #addr1 normalize nodelta
    917   cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
    918   (* XXX: switch to the left hand side *)
    919   >EQP -P normalize nodelta
    920   #sigma_increment_commutation #maps_assm #fetch_many_assm
    921 
    922   whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    923   <EQppc in fetch_many_assm;
    924   whd in match (short_jump_cond ??);
    925   @pair_elim #sj_possible #disp
    926   @pair_elim #result #flags #sub16_refl
    927   @pair_elim #upper #lower #vsplit_refl
    928   inversion (get_index' bool ???) #get_index_refl' normalize nodelta
    929   #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
    930   [1,3:
    931     >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    932     >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    933     normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    934     whd in ⊢ (??%?);
    935     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    936     inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
    937     lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
    938     @(if_then_else_replace ???????? eq_bv_refl)
    939     [1,3,5,7:
    940       cases daemon
    941     |2,4,6,8:
    942       (* XXX: switch to the right hand side *)
    943       normalize nodelta >EQs -s >EQticks -ticks
    944       whd in ⊢ (??%%);
    945       (* XXX: finally, prove the equality using sigma commutation *)
    946       @split_eq_status try %
    947       [3,7,11,15:
    948         whd in ⊢ (??%?);
    949         [1,3:
    950           cases daemon
    951         |2,4:
    952           cases daemon
    953         ]
    954       ]
    955       cases daemon (* XXX *)
    956     ]
    957   |2,4:
    958     >(? : eq_v bool 9 eq_b upper (zero 9) = false)
    959     [2, 4:
    960       cases daemon (* XXX: !!! *)
    961     ]
    962     normalize nodelta >EQppc
    963     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    964     * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    965     * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    966     #fetch_many_assm whd in fetch_many_assm; %{2}
    967     change with (execute_1 ?? = ?)
    968     @(pose … (execute_1 ? (status_of_pseudo_status …)))
    969     #status_after_1 #EQstatus_after_1
    970     <(?: ? = status_after_1)
    971     [2,5:
    972       inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
    973     |3,6:
    974       >EQstatus_after_1 in ⊢ (???%);
    975       whd in ⊢ (???%);
    976       [1: <fetch_refl in ⊢ (???%);
    977       |2: <fetch_refl in ⊢ (???%);
    978       ]
    979       whd in ⊢ (???%);
    980       inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
    981       whd in ⊢ (???%);
    982       whd in match (addr_of_relative ????);
    983       change with (add ???) in match (\snd (half_add ???));
    984       >set_clock_set_program_counter in ⊢ (???%);
    985       >program_counter_set_program_counter in ⊢ (???%);
    986       >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    987       [2,4,6,8:
    988         >bitvector_of_nat_sign_extension_equivalence
    989         [1,3,5,7:
    990           >EQintermediate_pc' %
    991         |*:
    992           repeat @le_S_S @le_O_n
    993         ]
    994       |1,5:
    995         %
    996       ]
    997     |1,4: skip
    998     ]
    999     [1,2,3,4:
    1000       -status_after_1
    1001       @(pose … (execute_1 ? (mk_PreStatus …)))
    1002       #status_after_1 #EQstatus_after_1
    1003       <(?: ? = status_after_1)
    1004       [3,6,9,12:
    1005         >EQstatus_after_1 in ⊢ (???%);
    1006         whd in ⊢ (???%);
    1007         (* XXX: matita bug with patterns across multiple goals *)
    1008         [1: <fetch_refl'' in ⊢ (???%);
    1009         |2: <fetch_refl'' in ⊢ (???%);
    1010         |3: <fetch_refl'' in ⊢ (???%);
    1011         |4: <fetch_refl'' in ⊢ (???%);
    1012         ] %
    1013       |1,4,7,10:
    1014         skip
    1015       ]
    1016       -status_after_1 whd in ⊢ (??%?);
    1017       (* XXX: switch to the right hand side *)
    1018       normalize nodelta >EQs -s >EQticks -ticks
    1019       whd in ⊢ (??%%);
    1020     ]
    1021     (* XXX: finally, prove the equality using sigma commutation *)
    1022     @split_eq_status try %
    1023     cases daemon
    1024   ]
    1025   |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
    1026   (* XXX: work on the right hand side *)
    1027   >p normalize nodelta
    1028   (* XXX: switch to the left hand side *)
    1029   >EQP -P normalize nodelta
    1030   #sigma_increment_commutation #maps_assm #fetch_many_assm
    1031  
    1032   whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    1033   <EQppc in fetch_many_assm;
    1034   whd in match (short_jump_cond ??);
    1035   @pair_elim #sj_possible #disp
    1036   @pair_elim #result #flags #sub16_refl
    1037   @pair_elim #upper #lower #vsplit_refl
    1038   inversion (get_index' bool ???) #get_index_refl' normalize nodelta
    1039   #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
    1040   [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1041     >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    1042     >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    1043     normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    1044     whd in ⊢ (??%?);
    1045     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    1046     (* XXX: work on the left hand side *)
    1047     @(if_then_else_replace ???????? p) normalize nodelta
    1048     [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1049       cases daemon
    1050     ]
    1051     (* XXX: switch to the right hand side *)
    1052     normalize nodelta >EQs -s >EQticks -ticks
    1053     whd in ⊢ (??%%);
    1054     (* XXX: finally, prove the equality using sigma commutation *)
    1055     @split_eq_status try %
    1056     cases daemon
    1057   |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1058     >(? : eq_v bool 9 eq_b upper (zero 9) = false)
    1059     [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1060       cases daemon (* XXX: !!! *)
    1061     ]
    1062     normalize nodelta >EQppc
    1063     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    1064     * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    1065     * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    1066     #fetch_many_assm whd in fetch_many_assm; %{2}
    1067     change with (execute_1 ?? = ?)
    1068     @(pose … (execute_1 ? (status_of_pseudo_status …)))
    1069     #status_after_1 #EQstatus_after_1
    1070     <(?: ? = status_after_1)
    1071     [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
    1072       >EQstatus_after_1 in ⊢ (???%);
    1073       whd in ⊢ (???%);
    1074       [1: <fetch_refl in ⊢ (???%);
    1075       |2: <fetch_refl in ⊢ (???%);
    1076       |3: <fetch_refl in ⊢ (???%);
    1077       |4: <fetch_refl in ⊢ (???%);
    1078       |5: <fetch_refl in ⊢ (???%);
    1079       |6: <fetch_refl in ⊢ (???%);
    1080       |7: <fetch_refl in ⊢ (???%);
    1081       |8: <fetch_refl in ⊢ (???%);
    1082       |9: <fetch_refl in ⊢ (???%);
    1083       |10: <fetch_refl in ⊢ (???%);
    1084       |11: <fetch_refl in ⊢ (???%);
    1085       |12: <fetch_refl in ⊢ (???%);
    1086       |13: <fetch_refl in ⊢ (???%);
    1087       |14: <fetch_refl in ⊢ (???%);
    1088       ]
    1089       whd in ⊢ (???%);
    1090       @(if_then_else_replace ???????? p)
    1091       [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1092         cases daemon
    1093       |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1094         normalize nodelta
    1095         whd in match (addr_of_relative ????);
    1096         >set_clock_mk_Status_commutation
    1097         [9,10:
    1098           (* XXX: demodulation not working in this case *)
    1099           >program_counter_set_arg_1 in ⊢ (???%);
    1100           >program_counter_set_program_counter in ⊢ (???%);
    1101         |*:
    1102           /demod/
    1103         ]
    1104         whd in ⊢ (???%);
    1105         change with (add ???) in match (\snd (half_add ???));
    1106         >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    1107         [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1108           >bitvector_of_nat_sign_extension_equivalence
    1109           [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1110             >EQintermediate_pc' %
    1111           |*:
    1112             repeat @le_S_S @le_O_n
    1113           ]
    1114         ]
    1115         %
    1116       ]
    1117     |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    1118       skip
    1119     ]
    1120     -status_after_1
    1121     @(pose … (execute_1 ? (mk_PreStatus …)))
    1122     #status_after_1 #EQstatus_after_1
    1123     <(?: ? = status_after_1)
    1124     [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
    1125       >EQstatus_after_1 in ⊢ (???%);
    1126       whd in ⊢ (???%);
    1127       (* XXX: matita bug with patterns across multiple goals *)
    1128       [1: <fetch_refl'' in ⊢ (???%);
    1129       |2: <fetch_refl' in ⊢ (???%);
    1130       |3: <fetch_refl'' in ⊢ (???%);
    1131       |4: <fetch_refl' in ⊢ (???%);
    1132       |5: <fetch_refl'' in ⊢ (???%);
    1133       |6: <fetch_refl' in ⊢ (???%);
    1134       |7: <fetch_refl'' in ⊢ (???%);
    1135       |8: <fetch_refl' in ⊢ (???%);
    1136       |9: <fetch_refl'' in ⊢ (???%);
    1137       |10: <fetch_refl' in ⊢ (???%);
    1138       |11: <fetch_refl'' in ⊢ (???%);
    1139       |12: <fetch_refl' in ⊢ (???%);
    1140       |13: <fetch_refl'' in ⊢ (???%);
    1141       |14: <fetch_refl' in ⊢ (???%);
    1142       ]
    1143       whd in ⊢ (???%);
    1144       [9,10:
    1145       |*:
    1146         /demod/
    1147       ] %
    1148     |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    1149       skip
    1150     ]
    1151     -status_after_1 whd in ⊢ (??%?);
    1152     (* XXX: switch to the right hand side *)
    1153     normalize nodelta >EQs -s >EQticks -ticks
    1154     whd in ⊢ (??%%);
    1155     (* XXX: finally, prove the equality using sigma commutation *)
    1156     @split_eq_status try %
    1157     [3,11,19,27,36,53,61:
    1158       >program_counter_set_program_counter >set_clock_mk_Status_commutation
    1159       [5: >program_counter_set_program_counter ]
    1160       >EQaddr_of normalize nodelta
    1161       whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
    1162       >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
    1163       @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
    1164       >create_label_cost_refl normalize nodelta #relevant @relevant
    1165       whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
    1166       try assumption whd in match instruction_has_label; normalize nodelta
    1167       <instr_refl normalize nodelta %
    1168     |7,15,23,31,45,57,65:
    1169       >set_clock_mk_Status_commutation >program_counter_set_program_counter
    1170       whd in ⊢ (??%?); normalize nodelta
    1171       >EQppc in fetch_many_assm; #fetch_many_assm
    1172       [5:
    1173         >program_counter_set_arg_1 >program_counter_set_program_counter
    1174       ]
    1175       <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
    1176       <bitvector_of_nat_sign_extension_equivalence
    1177       [1,3,5,7,9,11,13:
    1178         whd in ⊢ (???%); cases (half_add ???) normalize //
    1179       |2,4,6,8,10,12,14:
    1180         @assembly1_lt_128
    1181         @le_S_S @le_O_n
    1182       ]
    1183     |*:
    1184       cases daemon
    1185     ]
    1186   ]
    1187   |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
    1188   (* XXX: work on the right hand side *)
    1189   lapply (subaddressing_modein ???)
    1190   <EQaddr normalize nodelta #irrelevant
    1191   try (>p normalize nodelta)
    1192   try (>p1 normalize nodelta)
    1193   (* XXX: switch to the left hand side *)
    1194   >EQP -P normalize nodelta
    1195   #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1196   whd in ⊢ (??%?);
    1197   whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    1198   <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    1199   (* XXX: work on the left hand side *)
    1200   [1,2,3,4,5:
    1201     generalize in ⊢ (??(???(?%))?);
    1202   |6,7,8,9,10,11:
    1203     generalize in ⊢ (??(???(?%))?);
    1204   |12:
    1205     generalize in ⊢ (??(???(?%))?);
    1206   ]
    1207   <EQaddr normalize nodelta #irrelevant
    1208   try @(jmpair_as_replace ?????????? p)
    1209   [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
    1210   (* XXX: switch to the right hand side *)
    1211   normalize nodelta >EQs -s >EQticks -ticks
    1212   whd in ⊢ (??%%);
    1213   (* XXX: finally, prove the equality using sigma commutation *)
    1214   try @split_eq_status try % whd in ⊢ (??%%);
    1215   cases daemon
    1216   |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
    1217   (* XXX: work on the right hand side *)
    1218   >p normalize nodelta
    1219   try (>p1 normalize nodelta)
    1220   (* XXX: switch to the left hand side *)
    1221   -instr_refl >EQP -P normalize nodelta
    1222   #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1223   whd in ⊢ (??%?);
    1224   <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    1225   (* XXX: work on the left hand side *)
    1226   @(pair_replace ?????????? p)
    1227   [1,3,5,7,9,11,13,15,17:
    1228     >set_clock_set_program_counter >set_clock_mk_Status_commutation
    1229     >set_program_counter_mk_Status_commutation >clock_set_program_counter
    1230     cases daemon
    1231   |14,16,18:
    1232     normalize nodelta
    1233     @(pair_replace ?????????? p1)
    1234     [1,3,5:
    1235       >set_clock_mk_Status_commutation
    1236       cases daemon
    1237     ]
    1238   ]
    1239   (* XXX: switch to the right hand side *)
    1240   normalize nodelta >EQs -s >EQticks -ticks
    1241   whd in ⊢ (??%%);
    1242   (* XXX: finally, prove the equality using sigma commutation *)
    1243   try @split_eq_status try %
    1244   cases daemon *)
    1245   [42,44: (* RL and RR *)
     695  |42,44: (* RL and RR *)
    1246696    (* XXX: work on the right hand side *)
    1247697    (* XXX: switch to the left hand side *)
    … …  
    1411861        @sym_eq @set_clock_status_of_pseudo_status
    1412862        [1:
    1413           >sigma_increment_commutation
     863          @sym_eq @set_program_counter_status_of_pseudo_status %
    1414864        |2:
    1415865          %
    … …  
    1436886      ]
    1437887    ]
    1438   |4,5,6,7,8,9: (* INC and DEC *)
    1439     (* XXX: work on the right hand side *)
    1440     (* XXX: switch to the left hand side *)
    1441     >EQP -P normalize nodelta
    1442     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    1443     whd in maps_assm:(??%%);
    1444     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
    1445     [2,4,6,8,10,12: normalize nodelta #absurd destruct(absurd) ]
    1446     normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1447     whd in ⊢ (??%?);
    1448     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1449     @(subaddressing_mode_elim … addr) try #w whd in ⊢ (??%?); normalize nodelta
    1450     [1:
    1451       @(jmpair_as_replace ?????????? p)
    1452       [1:
    1453         @eq_f2 try % normalize nodelta
    1454         XXX
    1455       |2:
    1456         @(jmpair_as_replace ?????????? p)
    1457       ]
    1458888  |10: (* MUL *)
    1459889    (* XXX: work on the right hand side *)
    … …  
    1474904      @sym_eq
    1475905      [1:
    1476         @(get_8051_sfr_status_of_pseudo_status … policy) #_
    1477         @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
     906        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     907        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
     908        %
    1478909      |2:
    1479         @(get_8051_sfr_status_of_pseudo_status M' … policy)
    1480         @sym_eq @set_clock_status_of_pseudo_status [2: % ]
    1481         @sym_eq @set_program_counter_status_of_pseudo_status %
     910        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
    1482911      ]
    1483912    ]
    … …  
    1488917      @sym_eq
    1489918      [1:
    1490         @(get_8051_sfr_status_of_pseudo_status … policy) #_
    1491         @(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
     919        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     920        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    1492921      |2:
    1493         @(get_8051_sfr_status_of_pseudo_status M' … policy)
    1494         @sym_eq @set_clock_status_of_pseudo_status [2: % ]
    1495         @sym_eq @set_program_counter_status_of_pseudo_status %
     922        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
    1496923      ]
    1497924    ]
    … …  
    1514941    whd in ⊢ (??%?);
    1515942    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     943    whd in ⊢ (??%?); normalize nodelta
     944    cases daemon (* XXX: need match_nat_replace but is not working! *)
     945  |13: (* DA *)
     946    (* XXX: work on the right hand side *)
     947    (* XXX: switch to the left hand side *)
     948    >EQP -P normalize nodelta
     949    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     950    whd in maps_assm:(??%%);
     951    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     952    [2: normalize nodelta #absurd destruct(absurd) ]
     953    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    1516954    whd in ⊢ (??%?);
    1517     @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm #pose_refl @sym_eq
    1518     @(pose … (nat_of_bitvector ??)) #nat_of_bitvector_assm' #pose_refl'
    1519     cut(nat_of_bitvector_assm = nat_of_bitvector_assm')
    1520     [1,3:
    1521     |2,4:
    1522       #cut_assm <cut_assm cases nat_of_bitvector_assm try #n' normalize nodelta
    1523       @set_flags_status_of_pseudo_status
    1524     ]
    1525    
    1526    
     955    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     956    whd in ⊢ (??%?); normalize nodelta
     957    @(pair_replace ?????????? p)
     958    [1:
     959      @eq_f normalize nodelta >EQs >EQticks <instr_refl
     960      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     961      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     962    |2:
     963      @(pair_replace ?????????? p)
     964      [1:
     965        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
     966      |2:
     967        @(if_then_else_replace ???????? p1) normalize nodelta
     968        [1:
     969          cases (gtb ? 9)
     970          [1:
     971            %
     972          |2:
     973            change with (get_ac_flag ??? = get_ac_flag ???)
     974            (* XXX: requires get_ac_flag_status_of_pseudo_status *)
     975            cases daemon
     976          ]
     977        |2:
     978          @(if_then_else_replace ???????? p1) normalize nodelta try %
     979          @(pair_replace ?????????? p2)
     980          [1:
     981            @eq_f3 try % normalize nodelta
     982            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
     983            whd in ⊢ (??%?);
     984            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     985          |2:
     986            @(pair_replace ?????????? p2) try %
     987            @(pair_replace ?????????? p3) try %
     988            @(pair_replace ?????????? p3) try %
     989            @(if_then_else_replace ???????? p4) try % normalize nodelta
     990            @(if_then_else_replace ???????? p4) try % normalize nodelta
     991            @(pair_replace ?????????? p5) try %
     992            @(pair_replace ?????????? p5) try %
     993            @set_flags_status_of_pseudo_status try %
     994            [1:
     995              @eq_f @sym_eq cases daemon
     996              (* XXX: get_ac_flag_status_of_pseudo_status *)
     997            |2:
     998              @sym_eq cases daemon
     999              (* XXX: get_ov_flag_status_of_pseudo_status *)
     1000            |3:
     1001              @sym_eq @set_8051_sfr_status_of_pseudo_status
     1002              [1:
     1003                @sym_eq @set_clock_status_of_pseudo_status
     1004                [1:
     1005                  >EQs
     1006                  @sym_eq @set_program_counter_status_of_pseudo_status %
     1007                |2:
     1008                  >EQs >EQticks <instr_refl %
     1009                ]
     1010              |2:
     1011                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1012              ]
     1013            ]
     1014          ]
     1015        ]
     1016      ]
     1017    ]
     1018  |14: (* DA *)
     1019    (* XXX: work on the right hand side *)
     1020    (* XXX: switch to the left hand side *)
     1021    >EQP -P normalize nodelta
     1022    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1023    whd in maps_assm:(??%%);
     1024    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1025    [2: normalize nodelta #absurd destruct(absurd) ]
     1026    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1027    whd in ⊢ (??%?);
     1028    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1029    whd in ⊢ (??%?); normalize nodelta
     1030    @(pair_replace ?????????? p)
     1031    [1:
     1032      @eq_f normalize nodelta >EQs >EQticks <instr_refl
     1033      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1034      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1035    |2:
     1036      @(pair_replace ?????????? p)
     1037      [1:
     1038        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
     1039      |2:
     1040        @(if_then_else_replace ???????? p1) normalize nodelta
     1041        [1:
     1042          cases (gtb ? 9)
     1043          [1:
     1044            %
     1045          |2:
     1046            change with (get_ac_flag ??? = get_ac_flag ???)
     1047            (* XXX: requires get_ac_flag_status_of_pseudo_status *)
     1048            cases daemon
     1049          ]
     1050        |2:
     1051          @(if_then_else_replace ???????? p1) normalize nodelta try %
     1052          @(pair_replace ?????????? p2)
     1053          [1:
     1054            @eq_f3 try % normalize nodelta
     1055            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
     1056            whd in ⊢ (??%?);
     1057            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1058          |2:
     1059            @(pair_replace ?????????? p2) try %
     1060            @(pair_replace ?????????? p3) try %
     1061            @(pair_replace ?????????? p3) try %
     1062            @(if_then_else_replace ???????? p4) try % normalize nodelta
     1063            @(if_then_else_replace ???????? p4) try % normalize nodelta
     1064            @set_clock_status_of_pseudo_status
     1065            [1:
     1066              >EQs
     1067              @sym_eq @set_program_counter_status_of_pseudo_status %
     1068            |2:
     1069              >EQs >EQticks <instr_refl %
     1070            ]
     1071          ]
     1072        ]
     1073      ]
     1074    ]
     1075  |15: (* DA *)
     1076    (* XXX: work on the right hand side *)
     1077    (* XXX: switch to the left hand side *)
     1078    >EQP -P normalize nodelta
     1079    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1080    whd in maps_assm:(??%%);
     1081    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1082    [2: normalize nodelta #absurd destruct(absurd) ]
     1083    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1084    whd in ⊢ (??%?);
     1085    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1086    whd in ⊢ (??%?); normalize nodelta
     1087    @(pair_replace ?????????? p)
     1088    [1:
     1089      @eq_f normalize nodelta >EQs >EQticks <instr_refl
     1090      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
     1091      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1092    |2:
     1093      @(pair_replace ?????????? p)
     1094      [1:
     1095        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
     1096      |2:
     1097        @(if_then_else_replace ???????? p1) normalize nodelta
     1098        [1:
     1099          cases (gtb ? 9)
     1100          [1:
     1101            %
     1102          |2:
     1103            change with (get_ac_flag ??? = get_ac_flag ???)
     1104            (* XXX: requires get_ac_flag_status_of_pseudo_status *)
     1105            cases daemon
     1106          ]
     1107        |2:
     1108          @(if_then_else_replace ???????? p1) normalize nodelta try %
     1109          @set_clock_status_of_pseudo_status
     1110          [1:
     1111            >EQs
     1112            @sym_eq @set_program_counter_status_of_pseudo_status %
     1113          |2:
     1114            >EQs >EQticks <instr_refl %
     1115          ]
     1116        ]
     1117      ]
     1118    ]
     1119  |16: (* JC *)
     1120    (* XXX: work on the right hand side *)
     1121    (* XXX: switch to the left hand side *)
     1122    >EQP -P normalize nodelta
     1123    #sigma_increment_commutation #maps_assm
     1124    whd in match expand_pseudo_instruction; normalize nodelta
     1125    whd in match expand_relative_jump; normalize nodelta
     1126    whd in match expand_relative_jump_internal; normalize nodelta
     1127    @pair_elim #sj_possible #disp #sj_possible_disp_refl normalize nodelta
     1128    inversion sj_possible #sj_possible_refl
     1129    [1:
     1130      #fetch_many_assm %{1}
     1131      whd in maps_assm:(??%%);
     1132      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1133      whd in ⊢ (??%?); normalize nodelta
     1134      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1135      whd in ⊢ (??%?); normalize nodelta
     1136      @(if_then_else_replace ???????? p) normalize nodelta
     1137      [1:
     1138        >EQs @(get_cy_flag_status_of_pseudo_status M')
     1139        @sym_eq @set_program_counter_status_of_pseudo_status %
     1140      |2:
     1141        @(if_then_else_replace ???????? p) normalize nodelta try %
     1142        >EQs >EQticks <instr_refl
     1143        @set_program_counter_status_of_pseudo_status
     1144        [1:
     1145          >EQaddr_of normalize nodelta
     1146          whd in match addr_of_relative; normalize nodelta
     1147          whd in match (program_counter ???);
     1148          >sigma_increment_commutation
     1149          whd in match assembly_1_pseudoinstruction; normalize nodelta
     1150          whd in match expand_pseudo_instruction; normalize nodelta
     1151          whd in match expand_relative_jump; normalize nodelta
     1152          whd in match expand_relative_jump_internal; normalize nodelta
     1153          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1154          [1:
     1155            >EQppc %
     1156          |2:
     1157            >sj_possible_refl normalize nodelta normalize in match (length ??);
     1158            cases daemon
     1159            (* XXX: missing invariant? *)
     1160          ]
     1161        |2:
     1162          @sym_eq @set_clock_status_of_pseudo_status try %
     1163          @eq_f2 try % whd in ⊢ (??%%);
     1164          whd in match ticks_of0; normalize nodelta lapply sigma_increment_commutation
     1165          whd in match assembly_1_pseudoinstruction; normalize nodelta
     1166          whd in match expand_pseudo_instruction; normalize nodelta
     1167          whd in match expand_relative_jump; normalize nodelta
     1168          whd in match expand_relative_jump_internal; normalize nodelta
     1169          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1170          [1:
     1171            @eq_f2 try % >EQppc %
     1172          |2:
     1173            @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1174            [1:
     1175              @eq_f2 try % (* XXX: finish, use Jaap's invariant *)
     1176              cases daemon
     1177            |2:
     1178              #_ >sj_possible_refl %
     1179            ]
     1180          ]
     1181        ]
     1182      ]
     1183    |2:
     1184      normalize nodelta >EQppc
     1185      * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     1186      * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     1187      * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     1188      #fetch_many_assm whd in fetch_many_assm; %{2}
     1189      change with (execute_1 ?? = ?)
     1190      @(pose … (execute_1 ? (status_of_pseudo_status …)))
     1191      #status_after_1 #EQstatus_after_1
     1192      cases daemon (* XXX: ??? *)
     1193    ]
     1194  ]
     1195qed.
     1196
     1197(*
    15271198  (* XXX: work on the left hand side *)
    15281199  (* XXX: switch to the right hand side *)
    … …  
    16381309  cases daemon
    16391310  ]
    1640 qed.
     1311*)
     1312
     1313
     1314(*  [31,32: (* DJNZ *)
     1315  (* XXX: work on the right hand side *)
     1316  >p normalize nodelta >p1 normalize nodelta
     1317  (* XXX: switch to the left hand side *)
     1318  >EQP -P normalize nodelta
     1319  #sigma_increment_commutation #maps_assm #fetch_many_assm
     1320  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     1321  <EQppc in fetch_many_assm;
     1322  whd in match (short_jump_cond ??);
     1323  @pair_elim #sj_possible #disp
     1324  @pair_elim #result #flags #sub16_refl
     1325  @pair_elim #upper #lower #vsplit_refl
     1326  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     1327  #sj_possible_pair destruct(sj_possible_pair)
     1328  >p1 normalize nodelta
     1329  [1,3:
     1330    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     1331    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     1332    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
     1333    whd in ⊢ (??%?);
     1334    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1335    lapply maps_assm whd in ⊢ (??%? → ?);
     1336    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
     1337    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
     1338    (* XXX: work on the left hand side *)
     1339    @(pair_replace ?????????? p) normalize nodelta
     1340    [1,3:
     1341      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
     1342      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1343      >(get_arg_8_set_program_counter … true addr1)
     1344      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1345      @get_arg_8_pseudo_addressing_mode_ok assumption
     1346    |2,4:
     1347      >p1 normalize nodelta >EQs
     1348      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
     1349      >set_program_counter_status_of_pseudo_status
     1350       whd in ⊢ (??%%);
     1351      @split_eq_status
     1352      [1,10:
     1353        whd in ⊢ (??%%); >set_arg_8_set_program_counter
     1354        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1355        >low_internal_ram_set_program_counter
     1356        [1:
     1357          >low_internal_ram_set_program_counter
     1358          (* XXX: ??? *)
     1359        |2:
     1360          >low_internal_ram_set_clock
     1361          (* XXX: ??? *)
     1362        ]
     1363      |2,11:
     1364        whd in ⊢ (??%%); >set_arg_8_set_program_counter
     1365        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1366        >high_internal_ram_set_program_counter
     1367        [1:
     1368          >high_internal_ram_set_program_counter
     1369          (* XXX: ??? *)
     1370        |2:
     1371          >high_internal_ram_set_clock
     1372          (* XXX: ??? *)
     1373        ]
     1374      |3,12:
     1375        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
     1376        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1377        >(external_ram_set_arg_8 ??? addr1)
     1378        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1379      |4,13:
     1380        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
     1381        [1:
     1382          >program_counter_set_program_counter
     1383          >set_arg_8_set_program_counter
     1384          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1385          >set_clock_set_program_counter >program_counter_set_program_counter
     1386          change with (add ??? = ?)
     1387          (* XXX: ??? *)
     1388        |2:
     1389          >set_arg_8_set_program_counter
     1390          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1391          >program_counter_set_program_counter
     1392          >set_arg_8_set_program_counter
     1393          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1394          >set_clock_set_program_counter >program_counter_set_program_counter
     1395          >sigma_increment_commutation <EQppc
     1396          whd in match (assembly_1_pseudoinstruction ??????);
     1397          whd in match (expand_pseudo_instruction ??????);
     1398          (* XXX: ??? *)
     1399        ]
     1400      |5,14:
     1401        whd in match (special_function_registers_8051 ???);
     1402        [1:
     1403          >special_function_registers_8051_set_program_counter
     1404          >special_function_registers_8051_set_clock
     1405          >set_arg_8_set_program_counter in ⊢ (???%);
     1406          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1407          >special_function_registers_8051_set_program_counter
     1408          >set_arg_8_set_program_counter
     1409          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1410          >special_function_registers_8051_set_program_counter
     1411          @special_function_registers_8051_set_arg_8 assumption
     1412        |2:
     1413          >special_function_registers_8051_set_clock
     1414          >set_arg_8_set_program_counter
     1415          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1416          >set_arg_8_set_program_counter
     1417          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1418          >special_function_registers_8051_set_program_counter
     1419          >special_function_registers_8051_set_program_counter
     1420          @special_function_registers_8051_set_arg_8 assumption
     1421        ]
     1422      |6,15:
     1423        whd in match (special_function_registers_8052 ???);
     1424        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
     1425        [1:
     1426          >set_arg_8_set_program_counter
     1427          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1428          >set_arg_8_set_program_counter
     1429          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1430          >special_function_registers_8052_set_program_counter
     1431          >special_function_registers_8052_set_program_counter
     1432          @special_function_registers_8052_set_arg_8 assumption
     1433        |2:
     1434          whd in ⊢ (??%%);
     1435          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
     1436        ]
     1437        (* XXX: we need special_function_registers_8052_set_arg_8 *)
     1438      |7,16:
     1439        whd in match (p1_latch ???);
     1440        whd in match (p1_latch ???) in ⊢ (???%);
     1441        (* XXX: we need p1_latch_8052_set_arg_8 *)
     1442      |8,17:
     1443        whd in match (p3_latch ???);
     1444        whd in match (p3_latch ???) in ⊢ (???%);
     1445        (* XXX: we need p3_latch_8052_set_arg_8 *)
     1446      |9:
     1447        >clock_set_clock
     1448        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
     1449        >EQticks <instr_refl @eq_f2
     1450        [1:
     1451          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
     1452        |2:
     1453          (* XXX: we need clock_set_arg_8 *)
     1454        ]
     1455      |18:
     1456      ]
     1457    ]
     1458    (* XXX: switch to the right hand side *)
     1459    normalize nodelta >EQs -s >EQticks -ticks
     1460    cases (¬ eq_bv ???) normalize nodelta
     1461    whd in ⊢ (??%%);
     1462    (* XXX: finally, prove the equality using sigma commutation *)
     1463    @split_eq_status try %
     1464    [1,2,3,19,20,21,28,29,30:
     1465      cases daemon (* XXX: axioms as above *)
     1466    |4,13,22,31:
     1467    |5,14,23,32:
     1468    |6,15,24,33:
     1469    |7,16,25,34:
     1470    |8,17,26,35:
     1471      whd in ⊢ (??%%);maps_assm
     1472     
     1473    |9,18,27,36:
     1474      whd in ⊢ (??%%);
     1475      whd in match (ticks_of_instruction ?); <instr_refl
     1476      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
     1477    ]
     1478  |2,4:
     1479    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
     1480    [2, 4:
     1481      cases daemon (* XXX: !!! *)
     1482    ]
     1483    normalize nodelta >EQppc
     1484    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     1485    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     1486    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     1487    #fetch_many_assm whd in fetch_many_assm; %{2}
     1488    change with (execute_1 ?? = ?)
     1489    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     1490    #status_after_1 #EQstatus_after_1
     1491    <(?: ? = status_after_1)
     1492    [3,6:
     1493      >EQstatus_after_1 in ⊢ (???%);
     1494      whd in ⊢ (???%);
     1495      [1:
     1496        <fetch_refl in ⊢ (???%);
     1497      |2:
     1498        <fetch_refl in ⊢ (???%);
     1499      ]
     1500      whd in ⊢ (???%);
     1501      @(pair_replace ?????????? p)
     1502      [1,3:
     1503        cases daemon
     1504      |2,4:
     1505        normalize nodelta
     1506        whd in match (addr_of_relative ????);
     1507        cases (¬ eq_bv ???) normalize nodelta
     1508        >set_clock_mk_Status_commutation
     1509        whd in ⊢ (???%);
     1510        change with (add ???) in match (\snd (half_add ???));
     1511        >set_arg_8_set_program_counter in ⊢ (???%);
     1512        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1513        >program_counter_set_program_counter in ⊢ (???%);
     1514        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     1515        [2,4,6,8:
     1516          >bitvector_of_nat_sign_extension_equivalence
     1517          [1,3,5,7:
     1518            >EQintermediate_pc' %
     1519          |*:
     1520            repeat @le_S_S @le_O_n
     1521          ]
     1522        ]
     1523        [1,3: % ]
     1524      ]
     1525    |1,4:
     1526      skip
     1527    ]
     1528    [3,4:
     1529      -status_after_1
     1530      @(pose … (execute_1 ? (mk_PreStatus …)))
     1531      #status_after_1 #EQstatus_after_1
     1532      <(?: ? = status_after_1)
     1533      [3,6:
     1534        >EQstatus_after_1 in ⊢ (???%);
     1535        whd in ⊢ (???%);
     1536        (* XXX: matita bug with patterns across multiple goals *)
     1537        [1:
     1538          <fetch_refl'' in ⊢ (???%);
     1539        |2:
     1540          <fetch_refl'' in ⊢ (???%);
     1541        ]
     1542        [2: % |1: whd in ⊢ (???%); % ]
     1543      |1,4:
     1544        skip
     1545      ]
     1546      -status_after_1 whd in ⊢ (??%?);
     1547      (* XXX: switch to the right hand side *)
     1548      normalize nodelta >EQs -s >EQticks -ticks
     1549      normalize nodelta whd in ⊢ (??%%);
     1550    ]
     1551    (* XXX: finally, prove the equality using sigma commutation *)
     1552    @split_eq_status try %
     1553    whd in ⊢ (??%%);
     1554    cases daemon
     1555  ]
     1556  |30: (* CJNE *)
     1557  (* XXX: work on the right hand side *)
     1558  cases addr1 -addr1 #addr1 normalize nodelta
     1559  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
     1560  (* XXX: switch to the left hand side *)
     1561  >EQP -P normalize nodelta
     1562  #sigma_increment_commutation #maps_assm #fetch_many_assm
     1563
     1564  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     1565  <EQppc in fetch_many_assm;
     1566  whd in match (short_jump_cond ??);
     1567  @pair_elim #sj_possible #disp
     1568  @pair_elim #result #flags #sub16_refl
     1569  @pair_elim #upper #lower #vsplit_refl
     1570  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     1571  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
     1572  [1,3:
     1573    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     1574    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     1575    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
     1576    whd in ⊢ (??%?);
     1577    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1578    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
     1579    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
     1580    @(if_then_else_replace ???????? eq_bv_refl)
     1581    [1,3,5,7:
     1582      cases daemon
     1583    |2,4,6,8:
     1584      (* XXX: switch to the right hand side *)
     1585      normalize nodelta >EQs -s >EQticks -ticks
     1586      whd in ⊢ (??%%);
     1587      (* XXX: finally, prove the equality using sigma commutation *)
     1588      @split_eq_status try %
     1589      [3,7,11,15:
     1590        whd in ⊢ (??%?);
     1591        [1,3:
     1592          cases daemon
     1593        |2,4:
     1594          cases daemon
     1595        ]
     1596      ]
     1597      cases daemon (* XXX *)
     1598    ]
     1599  |2,4:
     1600    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
     1601    [2, 4:
     1602      cases daemon (* XXX: !!! *)
     1603    ]
     1604    normalize nodelta >EQppc
     1605    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     1606    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     1607    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     1608    #fetch_many_assm whd in fetch_many_assm; %{2}
     1609    change with (execute_1 ?? = ?)
     1610    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     1611    #status_after_1 #EQstatus_after_1
     1612    <(?: ? = status_after_1)
     1613    [2,5:
     1614      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
     1615    |3,6:
     1616      >EQstatus_after_1 in ⊢ (???%);
     1617      whd in ⊢ (???%);
     1618      [1: <fetch_refl in ⊢ (???%);
     1619      |2: <fetch_refl in ⊢ (???%);
     1620      ]
     1621      whd in ⊢ (???%);
     1622      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
     1623      whd in ⊢ (???%);
     1624      whd in match (addr_of_relative ????);
     1625      change with (add ???) in match (\snd (half_add ???));
     1626      >set_clock_set_program_counter in ⊢ (???%);
     1627      >program_counter_set_program_counter in ⊢ (???%);
     1628      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     1629      [2,4,6,8:
     1630        >bitvector_of_nat_sign_extension_equivalence
     1631        [1,3,5,7:
     1632          >EQintermediate_pc' %
     1633        |*:
     1634          repeat @le_S_S @le_O_n
     1635        ]
     1636      |1,5:
     1637        %
     1638      ]
     1639    |1,4: skip
     1640    ]
     1641    [1,2,3,4:
     1642      -status_after_1
     1643      @(pose … (execute_1 ? (mk_PreStatus …)))
     1644      #status_after_1 #EQstatus_after_1
     1645      <(?: ? = status_after_1)
     1646      [3,6,9,12:
     1647        >EQstatus_after_1 in ⊢ (???%);
     1648        whd in ⊢ (???%);
     1649        (* XXX: matita bug with patterns across multiple goals *)
     1650        [1: <fetch_refl'' in ⊢ (???%);
     1651        |2: <fetch_refl'' in ⊢ (???%);
     1652        |3: <fetch_refl'' in ⊢ (???%);
     1653        |4: <fetch_refl'' in ⊢ (???%);
     1654        ] %
     1655      |1,4,7,10:
     1656        skip
     1657      ]
     1658      -status_after_1 whd in ⊢ (??%?);
     1659      (* XXX: switch to the right hand side *)
     1660      normalize nodelta >EQs -s >EQticks -ticks
     1661      whd in ⊢ (??%%);
     1662    ]
     1663    (* XXX: finally, prove the equality using sigma commutation *)
     1664    @split_eq_status try %
     1665    cases daemon
     1666  ]
     1667  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
     1668  (* XXX: work on the right hand side *)
     1669  >p normalize nodelta
     1670  (* XXX: switch to the left hand side *)
     1671  >EQP -P normalize nodelta
     1672  #sigma_increment_commutation #maps_assm #fetch_many_assm
     1673 
     1674  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     1675  <EQppc in fetch_many_assm;
     1676  whd in match (short_jump_cond ??);
     1677  @pair_elim #sj_possible #disp
     1678  @pair_elim #result #flags #sub16_refl
     1679  @pair_elim #upper #lower #vsplit_refl
     1680  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     1681  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
     1682  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     1683    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     1684    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     1685    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
     1686    whd in ⊢ (??%?);
     1687    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1688    (* XXX: work on the left hand side *)
     1689    @(if_then_else_replace ???????? p) normalize nodelta
     1690    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     1691      cases daemon
     1692    ]
     1693    (* XXX: switch to the right hand side *)
     1694    normalize nodelta >EQs -s >EQticks -ticks
     1695    whd in ⊢ (??%%);
     1696    (* XXX: finally, prove the equality using sigma commutation *)
     1697    @split_eq_status try %
     1698    cases daemon
     1699  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1700    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
     1701    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1702      cases daemon (* XXX: !!! *)
     1703    ]
     1704    normalize nodelta >EQppc
     1705    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     1706    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     1707    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     1708    #fetch_many_assm whd in fetch_many_assm; %{2}
     1709    change with (execute_1 ?? = ?)
     1710    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     1711    #status_after_1 #EQstatus_after_1
     1712    <(?: ? = status_after_1)
     1713    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
     1714      >EQstatus_after_1 in ⊢ (???%);
     1715      whd in ⊢ (???%);
     1716      [1: <fetch_refl in ⊢ (???%);
     1717      |2: <fetch_refl in ⊢ (???%);
     1718      |3: <fetch_refl in ⊢ (???%);
     1719      |4: <fetch_refl in ⊢ (???%);
     1720      |5: <fetch_refl in ⊢ (???%);
     1721      |6: <fetch_refl in ⊢ (???%);
     1722      |7: <fetch_refl in ⊢ (???%);
     1723      |8: <fetch_refl in ⊢ (???%);
     1724      |9: <fetch_refl in ⊢ (???%);
     1725      |10: <fetch_refl in ⊢ (???%);
     1726      |11: <fetch_refl in ⊢ (???%);
     1727      |12: <fetch_refl in ⊢ (???%);
     1728      |13: <fetch_refl in ⊢ (???%);
     1729      |14: <fetch_refl in ⊢ (???%);
     1730      ]
     1731      whd in ⊢ (???%);
     1732      @(if_then_else_replace ???????? p)
     1733      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     1734        cases daemon
     1735      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1736        normalize nodelta
     1737        whd in match (addr_of_relative ????);
     1738        >set_clock_mk_Status_commutation
     1739        [9,10:
     1740          (* XXX: demodulation not working in this case *)
     1741          >program_counter_set_arg_1 in ⊢ (???%);
     1742          >program_counter_set_program_counter in ⊢ (???%);
     1743        |*:
     1744          /demod/
     1745        ]
     1746        whd in ⊢ (???%);
     1747        change with (add ???) in match (\snd (half_add ???));
     1748        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     1749        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1750          >bitvector_of_nat_sign_extension_equivalence
     1751          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     1752            >EQintermediate_pc' %
     1753          |*:
     1754            repeat @le_S_S @le_O_n
     1755          ]
     1756        ]
     1757        %
     1758      ]
     1759    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
     1760      skip
     1761    ]
     1762    -status_after_1
     1763    @(pose … (execute_1 ? (mk_PreStatus …)))
     1764    #status_after_1 #EQstatus_after_1
     1765    <(?: ? = status_after_1)
     1766    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
     1767      >EQstatus_after_1 in ⊢ (???%);
     1768      whd in ⊢ (???%);
     1769      (* XXX: matita bug with patterns across multiple goals *)
     1770      [1: <fetch_refl'' in ⊢ (???%);
     1771      |2: <fetch_refl' in ⊢ (???%);
     1772      |3: <fetch_refl'' in ⊢ (???%);
     1773      |4: <fetch_refl' in ⊢ (???%);
     1774      |5: <fetch_refl'' in ⊢ (???%);
     1775      |6: <fetch_refl' in ⊢ (???%);
     1776      |7: <fetch_refl'' in ⊢ (???%);
     1777      |8: <fetch_refl' in ⊢ (???%);
     1778      |9: <fetch_refl'' in ⊢ (???%);
     1779      |10: <fetch_refl' in ⊢ (???%);
     1780      |11: <fetch_refl'' in ⊢ (???%);
     1781      |12: <fetch_refl' in ⊢ (???%);
     1782      |13: <fetch_refl'' in ⊢ (???%);
     1783      |14: <fetch_refl' in ⊢ (???%);
     1784      ]
     1785      whd in ⊢ (???%);
     1786      [9,10:
     1787      |*:
     1788        /demod/
     1789      ] %
     1790    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
     1791      skip
     1792    ]
     1793    -status_after_1 whd in ⊢ (??%?);
     1794    (* XXX: switch to the right hand side *)
     1795    normalize nodelta >EQs -s >EQticks -ticks
     1796    whd in ⊢ (??%%);
     1797    (* XXX: finally, prove the equality using sigma commutation *)
     1798    @split_eq_status try %
     1799    [3,11,19,27,36,53,61:
     1800      >program_counter_set_program_counter >set_clock_mk_Status_commutation
     1801      [5: >program_counter_set_program_counter ]
     1802      >EQaddr_of normalize nodelta
     1803      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
     1804      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
     1805      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
     1806      >create_label_cost_refl normalize nodelta #relevant @relevant
     1807      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
     1808      try assumption whd in match instruction_has_label; normalize nodelta
     1809      <instr_refl normalize nodelta %
     1810    |7,15,23,31,45,57,65:
     1811      >set_clock_mk_Status_commutation >program_counter_set_program_counter
     1812      whd in ⊢ (??%?); normalize nodelta
     1813      >EQppc in fetch_many_assm; #fetch_many_assm
     1814      [5:
     1815        >program_counter_set_arg_1 >program_counter_set_program_counter
     1816      ]
     1817      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
     1818      <bitvector_of_nat_sign_extension_equivalence
     1819      [1,3,5,7,9,11,13:
     1820        whd in ⊢ (???%); cases (half_add ???) normalize //
     1821      |2,4,6,8,10,12,14:
     1822        @assembly1_lt_128
     1823        @le_S_S @le_O_n
     1824      ]
     1825    |*:
     1826      cases daemon
     1827    ]
     1828  ]
     1829  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
     1830  (* XXX: work on the right hand side *)
     1831  lapply (subaddressing_modein ???)
     1832  <EQaddr normalize nodelta #irrelevant
     1833  try (>p normalize nodelta)
     1834  try (>p1 normalize nodelta)
     1835  (* XXX: switch to the left hand side *)
     1836  >EQP -P normalize nodelta
     1837  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1838  whd in ⊢ (??%?);
     1839  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     1840  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1841  (* XXX: work on the left hand side *)
     1842  [1,2,3,4,5:
     1843    generalize in ⊢ (??(???(?%))?);
     1844  |6,7,8,9,10,11:
     1845    generalize in ⊢ (??(???(?%))?);
     1846  |12:
     1847    generalize in ⊢ (??(???(?%))?);
     1848  ]
     1849  <EQaddr normalize nodelta #irrelevant
     1850  try @(jmpair_as_replace ?????????? p)
     1851  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
     1852  (* XXX: switch to the right hand side *)
     1853  normalize nodelta >EQs -s >EQticks -ticks
     1854  whd in ⊢ (??%%);
     1855  (* XXX: finally, prove the equality using sigma commutation *)
     1856  try @split_eq_status try % whd in ⊢ (??%%);
     1857  cases daemon
     1858  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
     1859  (* XXX: work on the right hand side *)
     1860  >p normalize nodelta
     1861  try (>p1 normalize nodelta)
     1862  (* XXX: switch to the left hand side *)
     1863  -instr_refl >EQP -P normalize nodelta
     1864  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1865  whd in ⊢ (??%?);
     1866  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1867  (* XXX: work on the left hand side *)
     1868  @(pair_replace ?????????? p)
     1869  [1,3,5,7,9,11,13,15,17:
     1870    >set_clock_set_program_counter >set_clock_mk_Status_commutation
     1871    >set_program_counter_mk_Status_commutation >clock_set_program_counter
     1872    cases daemon
     1873  |14,16,18:
     1874    normalize nodelta
     1875    @(pair_replace ?????????? p1)
     1876    [1,3,5:
     1877      >set_clock_mk_Status_commutation
     1878      cases daemon
     1879    ]
     1880  ]
     1881  (* XXX: switch to the right hand side *)
     1882  normalize nodelta >EQs -s >EQticks -ticks
     1883  whd in ⊢ (??%%);
     1884  (* XXX: finally, prove the equality using sigma commutation *)
     1885  try @split_eq_status try %
     1886  cases daemon *)
Note: See TracChangeset for help on using the changeset viewer.