source: src/ASM/AssemblyProofSplitSplit.ma @ 2026

Last change on this file since 2026 was 2026, checked in by mulligan, 7 years ago

Added a new file to house the main theorem as the type checking time for the main lemma is ridiculous.

File size: 6.9 KB
Line 
1include "ASM/AssemblyProofSplitSplit.ma".
2
3theorem 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  ]
147qed.
Note: See TracBrowser for help on using the repository browser.