1 | include "ASM/AssemblyProofSplit.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))) |
---|
100 | (refl …) ? (refl …)) |
---|
101 | try assumption >assembly_refl <EQppc assumption |
---|
102 | check status_of_pseudo_status |
---|
103 | |4: |
---|
104 | #arg1 |
---|
105 | (* XXX: we first work on sigma_increment_commutation *) |
---|
106 | #sigma_increment_commutation |
---|
107 | normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; |
---|
108 | (* XXX: we work on the maps *) |
---|
109 | whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm |
---|
110 | (* XXX: we assume the fetch_many hypothesis *) |
---|
111 | #fetch_many_assm |
---|
112 | (* XXX: we give the existential *) |
---|
113 | %{1} |
---|
114 | whd in match (execute_1_pseudo_instruction0 ?????); |
---|
115 | (* XXX: work on the left hand side of the equality *) |
---|
116 | whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc |
---|
117 | (* XXX: execute fetches some more *) |
---|
118 | whd in match code_memory_of_pseudo_assembly_program; normalize nodelta |
---|
119 | whd in fetch_many_assm; |
---|
120 | >EQassembled in fetch_many_assm; |
---|
121 | cases (fetch ??) * #instr #newpc #ticks normalize nodelta * |
---|
122 | #eq_instr |
---|
123 | #fetch_many_assm whd in fetch_many_assm; |
---|
124 | lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc |
---|
125 | destruct whd in ⊢ (??%?); |
---|
126 | (* XXX: now we start to work on the mk_PreStatus equality *) |
---|
127 | (* XXX: lhs *) |
---|
128 | change with (set_arg_16 ????? = ?) |
---|
129 | >set_program_counter_mk_Status_commutation |
---|
130 | >set_clock_mk_Status_commutation |
---|
131 | >set_arg_16_mk_Status_commutation |
---|
132 | (* XXX: rhs *) |
---|
133 | change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); |
---|
134 | >set_program_counter_mk_Status_commutation |
---|
135 | >set_clock_mk_Status_commutation |
---|
136 | >set_arg_16_mk_Status_commutation in ⊢ (???%); |
---|
137 | (* here we are *) |
---|
138 | @split_eq_status // |
---|
139 | [1: |
---|
140 | assumption |
---|
141 | |2: |
---|
142 | @special_function_registers_8051_set_arg_16 |
---|
143 | [2: % |
---|
144 | |1: // |
---|
145 | ] |
---|
146 | ] |
---|
147 | |5: cases daemon |
---|
148 | ] |
---|
149 | qed. |
---|