source: src/ASM/AssemblyProofSplitSplit.ma @ 2027

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

Got the main lemma to apply in the proof of main theorem again and closed the preinstruction goals.

File size: 7.0 KB
Line 
1include "ASM/AssemblyProofSplit.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)))
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  ]
149qed.
Note: See TracBrowser for help on using the repository browser.