[2026] | 1 | include "ASM/AssemblyProofSplitSplit.ma". |
---|
| 2 | |
---|
| 3 | theorem main_thm: |
---|
| 4 | ∀M, M': internal_pseudo_address_map. |
---|
| 5 | ∀program: pseudo_assembly_program. |
---|
| 6 | ∀sigma: Word → Word. |
---|
| 7 | ∀policy: Word → bool. |
---|
| 8 | ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. |
---|
| 9 | ∀ps: PseudoStatus program. |
---|
| 10 | ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) ≤ |\snd program|. |
---|
| 11 | next_internal_pseudo_address_map M program ps = Some … M' → |
---|
| 12 | ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = |
---|
| 13 | status_of_pseudo_status M' … |
---|
| 14 | (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. |
---|
| 15 | #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds |
---|
| 16 | change with (next_internal_pseudo_address_map0 ????? = ? → ?) |
---|
| 17 | @(pose … (program_counter ?? ps)) #ppc #EQppc |
---|
| 18 | generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?; |
---|
| 19 | @pair_elim #labels #costs #create_label_cost_refl normalize nodelta |
---|
| 20 | @pair_elim #assembled #costs' #assembly_refl normalize nodelta |
---|
| 21 | lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled |
---|
| 22 | @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta |
---|
| 23 | @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels |
---|
| 24 | @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels |
---|
| 25 | whd in match execute_1_pseudo_instruction; normalize nodelta |
---|
| 26 | whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta |
---|
| 27 | lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc |
---|
| 28 | lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?) |
---|
| 29 | [1: >fetch_pseudo_refl % |2: >EQppc assumption ] |
---|
| 30 | #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; |
---|
| 31 | generalize in match assm1; -assm1 -assm2 -assm3 |
---|
| 32 | normalize nodelta |
---|
| 33 | cases pi |
---|
| 34 | [2,3: |
---|
| 35 | #arg |
---|
| 36 | (* XXX: we first work on sigma_increment_commutation *) |
---|
| 37 | #sigma_increment_commutation |
---|
| 38 | normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; |
---|
| 39 | (* XXX: we work on the maps *) |
---|
| 40 | whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm |
---|
| 41 | (* XXX: we assume the fetch_many hypothesis *) |
---|
| 42 | #fetch_many_assm |
---|
| 43 | (* XXX: we give the existential *) |
---|
| 44 | %{0} |
---|
| 45 | whd in match (execute_1_pseudo_instruction0 ?????); |
---|
| 46 | (* XXX: work on the left hand side of the equality *) |
---|
| 47 | whd in ⊢ (??%?); |
---|
| 48 | @split_eq_status // |
---|
| 49 | [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ] |
---|
| 50 | |6: (* Mov *) |
---|
| 51 | #arg1 #arg2 |
---|
| 52 | (* XXX: we first work on sigma_increment_commutation *) |
---|
| 53 | #sigma_increment_commutation |
---|
| 54 | normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; |
---|
| 55 | (* XXX: we work on the maps *) |
---|
| 56 | whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm |
---|
| 57 | (* XXX: we assume the fetch_many hypothesis *) |
---|
| 58 | #fetch_many_assm |
---|
| 59 | (* XXX: we give the existential *) |
---|
| 60 | %{1} |
---|
| 61 | whd in match (execute_1_pseudo_instruction0 ?????); |
---|
| 62 | (* XXX: work on the left hand side of the equality *) |
---|
| 63 | whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc |
---|
| 64 | (* XXX: execute fetches some more *) |
---|
| 65 | whd in match code_memory_of_pseudo_assembly_program; normalize nodelta |
---|
| 66 | whd in fetch_many_assm; |
---|
| 67 | >EQassembled in fetch_many_assm; |
---|
| 68 | cases (fetch ??) * #instr #newpc #ticks normalize nodelta * |
---|
| 69 | #eq_instr |
---|
| 70 | #fetch_many_assm whd in fetch_many_assm; |
---|
| 71 | lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc |
---|
| 72 | destruct whd in ⊢ (??%?); |
---|
| 73 | (* XXX: now we start to work on the mk_PreStatus equality *) |
---|
| 74 | (* XXX: lhs *) |
---|
| 75 | change with (set_arg_16 ????? = ?) |
---|
| 76 | >set_program_counter_mk_Status_commutation |
---|
| 77 | >set_clock_mk_Status_commutation |
---|
| 78 | >set_arg_16_mk_Status_commutation |
---|
| 79 | (* XXX: rhs *) |
---|
| 80 | change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); |
---|
| 81 | >set_program_counter_mk_Status_commutation |
---|
| 82 | >set_clock_mk_Status_commutation |
---|
| 83 | >set_arg_16_mk_Status_commutation in ⊢ (???%); |
---|
| 84 | (* here we are *) |
---|
| 85 | @split_eq_status // |
---|
| 86 | [1: |
---|
| 87 | assumption |
---|
| 88 | |2: |
---|
| 89 | @special_function_registers_8051_set_arg_16 |
---|
| 90 | [2: % |
---|
| 91 | |1: // |
---|
| 92 | ] |
---|
| 93 | ] |
---|
| 94 | |1: (* Instruction *) |
---|
| 95 | -pi #instr #EQP #EQnext #fetch_many_assm |
---|
| 96 | @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness |
---|
| 97 | ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels |
---|
| 98 | EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …) |
---|
| 99 | (λ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))) (refl …)) |
---|
| 100 | cases daemon |
---|
| 101 | |4: |
---|
| 102 | #arg1 |
---|
| 103 | (* XXX: we first work on sigma_increment_commutation *) |
---|
| 104 | #sigma_increment_commutation |
---|
| 105 | normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; |
---|
| 106 | (* XXX: we work on the maps *) |
---|
| 107 | whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm |
---|
| 108 | (* XXX: we assume the fetch_many hypothesis *) |
---|
| 109 | #fetch_many_assm |
---|
| 110 | (* XXX: we give the existential *) |
---|
| 111 | %{1} |
---|
| 112 | whd in match (execute_1_pseudo_instruction0 ?????); |
---|
| 113 | (* XXX: work on the left hand side of the equality *) |
---|
| 114 | whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc |
---|
| 115 | (* XXX: execute fetches some more *) |
---|
| 116 | whd in match code_memory_of_pseudo_assembly_program; normalize nodelta |
---|
| 117 | whd in fetch_many_assm; |
---|
| 118 | >EQassembled in fetch_many_assm; |
---|
| 119 | cases (fetch ??) * #instr #newpc #ticks normalize nodelta * |
---|
| 120 | #eq_instr |
---|
| 121 | #fetch_many_assm whd in fetch_many_assm; |
---|
| 122 | lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc |
---|
| 123 | destruct whd in ⊢ (??%?); |
---|
| 124 | (* XXX: now we start to work on the mk_PreStatus equality *) |
---|
| 125 | (* XXX: lhs *) |
---|
| 126 | change with (set_arg_16 ????? = ?) |
---|
| 127 | >set_program_counter_mk_Status_commutation |
---|
| 128 | >set_clock_mk_Status_commutation |
---|
| 129 | >set_arg_16_mk_Status_commutation |
---|
| 130 | (* XXX: rhs *) |
---|
| 131 | change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); |
---|
| 132 | >set_program_counter_mk_Status_commutation |
---|
| 133 | >set_clock_mk_Status_commutation |
---|
| 134 | >set_arg_16_mk_Status_commutation in ⊢ (???%); |
---|
| 135 | (* here we are *) |
---|
| 136 | @split_eq_status // |
---|
| 137 | [1: |
---|
| 138 | assumption |
---|
| 139 | |2: |
---|
| 140 | @special_function_registers_8051_set_arg_16 |
---|
| 141 | [2: % |
---|
| 142 | |1: // |
---|
| 143 | ] |
---|
| 144 | ] |
---|
| 145 | |5: cases daemon |
---|
| 146 | ] |
---|
| 147 | qed. |
---|