source: src/ERTL/MoveCorrectness.ma @ 3253

Last change on this file since 3253 was 3253, checked in by piccolo, 7 years ago

some proof obbligation closed of ERTL to LTL proof

File size: 51.7 KB
RevLine 
[3253]1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ERTL/ERTLToLTL.ma".
16include "ERTL/ERTL_semantics.ma".
17include "LTL/LTL_semantics.ma".
18
19definition write_decision :
20ℕ →  decision → beval → state LTL_LIN_state → res (state LTL_LIN_state) ≝
21λlocalss,d,bv,st.
22match d with
23[ decision_spill n ⇒
24  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
25  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
26  ! 〈newaddrl,new_carry〉 ←
27     be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
28  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
29  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
30  ! new_mem ← opt_to_res ? [MSG FailedStore] (bestorev (m … st) ptr bv);
31  return
32   set_m ? new_mem
33   (set_regs LTL_semantics
34    (hwreg_store RegisterDPL newaddrl (hwreg_store RegisterDPH newaddrh (regs … st)))
35     (set_carry ? new_carry' st))
36| decision_colour r ⇒
37   !rgs  ← hw_reg_store r bv (regs … st);
38    return set_regs LTL_LIN_state rgs st
39].
40
41definition read_arg_decision : ℕ  → state LTL_LIN_state → arg_decision →
42res (beval × (state LTL_LIN_state)) ≝
43λlocalss,st,d.
44match d with
45[ arg_decision_colour r ⇒
46    return 〈hwreg_retrieve (regs … st) r,st〉
47| arg_decision_spill n ⇒
48  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
49  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
50  ! 〈newaddrl,new_carry〉 ←
51     be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
52  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
53  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
54  ! bv ← opt_to_res ? [MSG FailedLoad] (beloadv (m … st) ptr);
55  return 〈bv,set_regs LTL_semantics (hwreg_store RegisterDPL newaddrl
56                                     (hwreg_store RegisterDPH newaddrh
57                                       (regs … st))) (set_carry ? new_carry' st)〉
58| arg_decision_imm b ⇒
59   return 〈BVByte b,st〉
60].
61
62include alias "arithmetics/nat.ma".
63
64definition is_zero: nat → Prop ≝
65 λn. match n with [ O ⇒ True | S _ ⇒ False ].
66
67lemma nat_of_register_inj_aux: ∀r,s. eqb (nat_of_register r) (nat_of_register s) → r = s.
68* normalize in ⊢ (∀_. ?(?%?) → ?);
69try ( #x cases x normalize * %) (* 24s *)
70qed.
71
72(* it is true but there are 1296 cases *)
73lemma nat_of_register_inj : ∀r,s.nat_of_register r = nat_of_register s →  r = s.
74#r #s #H @nat_of_register_inj_aux @eqb_elim #H2 try % @(absurd … H H2)
75qed.
76 
77lemma eq_Register_elim : ∀P : bool → Prop.
78∀r,s: Register.(r=s → P true) → (r ≠s → P false) →
79P (eq_Register r s).
80#P #r #s #H1 #H2 whd in match eq_Register; normalize nodelta
81@eqb_elim
82[ #H @H1 @(nat_of_register_inj … H)
83| * #H @H2 % #EQ @H >EQ %
84]
85qed.
86
87lemma hwreg_retrieve_hwregstore_hit :
88∀regs,r,bv.
89hwreg_retrieve (hwreg_store r bv regs) r = bv.
90#regs #r #bv whd in match hwreg_retrieve; whd in match hwreg_store;
91normalize nodelta @lookup_insert_hit
92qed.
93
94axiom bitvector_of_register_inj : ∀r,s.
95bitvector_of_register r = bitvector_of_register s → r =s.
96
97lemma hwreg_retrieve_hwregstore_miss :
98∀regs,r,s,bv.
99r ≠ s →
100hwreg_retrieve (hwreg_store s bv regs) r = hwreg_retrieve regs r.
101#regs #r #s #bv * #H whd in match hwreg_retrieve; whd in match hwreg_store;
102normalize nodelta @lookup_insert_miss @eq_bv_elim
103[ #H1 @H @(bitvector_of_register_inj … H1) ] #_ @I
104qed.
105
106lemma hwreg_retrieve_insensitive_to_set_other :
107∀regs,r,b.
108hwreg_retrieve (hwreg_set_other b regs) r = hwreg_retrieve regs r.
109#regs #r #b %
110qed.
111
112axiom hwreg_store_idempotent : ∀r,bv1,bv2,regs.
113hwreg_store r bv1 (hwreg_store r bv2 regs) =
114hwreg_store r bv1 regs.
115
116axiom hwreg_store_commute : ∀r1,r2,bv1,bv2,regs.
117r1 ≠r2 →
118hwreg_store r1 bv1 (hwreg_store r2 bv2 regs) =
119hwreg_store r2 bv2 (hwreg_store r1 bv1 regs).
120
121axiom other_bit_insensitive_to_reg_store : ∀r,bv,regs.
122other_bit (hwreg_store r bv regs) = other_bit regs.
123
124axiom hwreg_store_retrieve_eq : ∀r,regs.
125hwreg_store r (hwreg_retrieve regs r) regs = regs.
126
127definition invariant_for_move :  arg_decision → Prop ≝
128λsrc.match src with
129[ arg_decision_colour r ⇒ r ≠ RegisterDPL ∧ r ≠ RegisterDPH
130| _ ⇒ True
131].
132
133lemma hwreg_store_set_other_commut : ∀regs,r,bv,b.
134hwreg_store r bv (hwreg_set_other b regs) =
135hwreg_set_other b (hwreg_store r bv regs).
136* #reg_env #other #r #bv #b %
137qed.
138
139include "joint/semantics_blocks.ma".
140
141lemma move_spill_spill_ok : ∀prog.∀stack_size.∀localss : nat.
142∀ carry_lives_after : bool.∀dest : ℕ.∀src : ℕ.
143∀f : ident.
144∀s : state LTL_LIN_state.
145repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
146   (move (prog_names … prog) localss carry_lives_after (decision_spill dest)
147    (arg_decision_spill src)) s =
148 if eqb src dest then return s
149     else ! 〈bv,s'〉 ← (read_arg_decision localss s (arg_decision_spill src));
150          let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
151          ! s'' ← write_decision localss (decision_spill dest) bv news;
152          let regSt1 ≝ (hwreg_store RegisterST1 bv (regs … s'')) in
153          if carry_lives_after then
154            return set_regs LTL_semantics (hwreg_set_other (carry … s) regSt1)
155                    (set_carry ? (carry … s) s'')
156          else
157            return set_regs LTL_semantics regSt1 s''.
158#prog #stack_size #localss #cl #dest #src #f #st
159inversion(repeat_eval_seq_no_pc ?????)
160[ #st' whd in match move; normalize nodelta @eqb_elim
161  [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (??%?? → ?); #EQ destruct(EQ) % ]
162  #_ normalize nodelta whd in match get_stack; whd in match set_stack;
163  normalize nodelta whd in match set_dp_by_offset; whd in match set_stack_a;
164  normalize nodelta whd in match set_stack_not_a; normalize nodelta
165  whd in match repeat_eval_seq_no_pc; normalize nodelta
166  whd in match preserve_carry_bit; normalize nodelta cases cl -cl
167  normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?);
168  inversion (eval_seq_no_pc ??????) [2,4: #e #_ normalize nodelta #EQ destruct(EQ)]
169  #st'' whd in match set_regs; whd in match eval_seq_no_pc in ⊢ (% → ?);
170  normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
171  whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
172  >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
173  whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
174  [2,4: % normalize #EQ destruct] [ >hwreg_retrieve_insensitive_to_set_other]
175  >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
176  whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
177  >hwreg_store_idempotent >m_return_bind whd in match set_carry;
178  whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
179  whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
180  normalize nodelta inversion (eval_seq_no_pc ??????)
181  [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
182  >hwreg_retrieve_hwregstore_hit whd in match eval_seq_no_pc in ⊢ (% → ?);
183  normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
184  whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
185  >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
186  whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
187  [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
188  [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
189  [2,4: normalize % #EQ destruct]  [ >hwreg_retrieve_insensitive_to_set_other]
190  >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
191  whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
192  >hwreg_store_idempotent >(hwreg_store_commute RegisterDPL RegisterA)
193  [2,4: normalize % #EQ destruct] >hwreg_store_idempotent >m_return_bind
194  whd in match set_carry; whd in match set_regs; normalize nodelta
195  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
196  normalize nodelta inversion (eval_seq_no_pc ??????)
197  [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
198  whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta whd in match dph_arg_retrieve;
199  whd in match dpl_arg_retrieve; normalize nodelta whd in ⊢ (??%?% → ?);
200  inversion (pointer_of_address ?) [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
201  #ptr >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
202  [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
203  | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
204  ]
205  [ >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
206  | >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
207  ]
208  >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?); #EQptr normalize nodelta
209  #H @('bind_inversion H) -H #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
210  whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
211  >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
212  >hwreg_store_idempotent >m_return_bind whd in match set_regs; normalize nodelta
213  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
214  normalize nodelta inversion (eval_seq_no_pc ??????)
215  [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
216  >(hwreg_store_commute RegisterST1 RegisterA) [2,4: normalize % #EQ destruct]
217  >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
218  normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
219  whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
220  >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
221  whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
222  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
223  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
224  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
225  [2,4: normalize % #EQ destruct(EQ)]  [ >hwreg_retrieve_insensitive_to_set_other]
226  >m_return_bind #H @('bind_inversion H) -H * #z1 #z2 #EQz1z2
227  whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
228  >hwreg_store_idempotent >m_return_bind whd in match set_carry; whd in match set_regs;
229  normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
230  whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
231  normalize nodelta inversion (eval_seq_no_pc ??????)
232  [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
233  >(hwreg_store_commute RegisterDPL RegisterA) [2,4: normalize % #EQ destruct]
234  >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
235  normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
236  whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
237  >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
238  whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
239  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
240  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
241  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
242  [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
243  [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
244   >m_return_bind #H @('bind_inversion H) -H * #w1 #w2 #EQw1w2 whd in match acca_store;
245   normalize nodelta whd in match (acca_store_ ??????); >hwreg_store_idempotent
246   >m_return_bind whd in match set_regs; whd in match set_carry; normalize nodelta
247   whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
248   normalize nodelta inversion (eval_seq_no_pc ??????)
249   [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
250   [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
251   [2: normalize % #EQ destruct]
252     >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
253   [2: normalize % #EQ destruct]
254   >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
255   [2: normalize % #EQ destruct]
256   >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
257   | >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
258   [2: normalize % #EQ destruct]
259   >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
260        [2: normalize % #EQ destruct]
261        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
262        [2: normalize % #EQ destruct]
263         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
264      ]
265      >hwreg_retrieve_hwregstore_hit >(hwreg_store_commute RegisterDPH RegisterA)
266      [2,4: normalize % #EQ destruct]  >hwreg_store_idempotent
267      whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
268      whd in match dph_arg_retrieve; whd in match dpl_arg_retrieve; normalize nodelta;
269      whd in ⊢ (??%?% → ?); inversion (pointer_of_address ?); [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
270      #ptr1 >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2,4: normalize % #EQ destruct]
271      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
272        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
273        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
274        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);     
275      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
276        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
277        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
278        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
279      ]
280      #EQptr1 normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
281      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
282      >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
283      -H #EQm1 whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?);
284      #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
285      [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
286        >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
287        >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
288        whd in match set_carry; normalize nodelta ]
289      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
290      >m_return_bind >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
291      >m_return_bind >EQptr >m_return_bind >EQbv >m_return_bind
292      whd in match set_regs; whd in match write_decision; normalize nodelta
293      whd in match hw_reg_retrieve; normalize nodelta
294      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
295      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
296         [2: normalize % #EQ destruct]
297        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
298        [2: normalize % #EQ destruct]
299      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
300        [2: normalize % #EQ destruct]
301        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
302        [2: normalize % #EQ destruct]
303      ]
304      >m_return_bind >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
305      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
306      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
307      >m_return_bind >EQz1z2 >m_return_bind
308      >EQw1w2 >m_return_bind >EQptr1 >m_return_bind >EQm1 >m_return_bind
309       whd in match set_m; whd in match set_carry; whd in match set_regs;
310       normalize nodelta
311       @eq_f whd in match (other_bit ?); whd in match set_carry; normalize nodelta
312       @eq_f3 [2,3,5,6: %]
313       [ >(hwreg_store_commute RegisterDPH RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
314         >(hwreg_store_commute RegisterA RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
315         >(hwreg_store_commute RegisterST1 RegisterDPL) in ⊢ (??%?); [2: normalize % #EQ destruct]
316       | >(hwreg_store_commute RegisterDPH RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
317         >(hwreg_store_commute RegisterA RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
318         >(hwreg_store_commute RegisterST1 RegisterDPL) in ⊢ (??%?); [2: normalize % #EQ destruct]           
319       ] [<hwreg_store_set_other_commut] @eq_f3 [1,2,4,5: %]
320       [ >(hwreg_store_commute RegisterA RegisterDPH) in ⊢ (???%); [2: normalize % #EQ destruct]
321         >(hwreg_store_commute RegisterST1 RegisterDPH) in ⊢ (??%?); [2: normalize % #EQ destruct]
322       | >(hwreg_store_commute RegisterA RegisterDPH) in ⊢ (???%); [2: normalize % #EQ destruct]
323         >(hwreg_store_commute RegisterST1 RegisterDPH) in ⊢ (??%?); [2: normalize % #EQ destruct]
324       ] [<hwreg_store_set_other_commut] @eq_f3 [1,2,4,5: %]
325       [ <hwreg_store_set_other_commut <hwreg_store_set_other_commut
326         <hwreg_store_set_other_commut ]
327         >(hwreg_store_commute RegisterA RegisterST1) in ⊢ (???%); [2,4: normalize % #EQ destruct]         
328          @eq_f3 [1,2,4,5: %] @eq_f3 [1,2,4,5: %]
329         [<hwreg_store_set_other_commut ]
330         >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
331         [2,4: normalize % #EQ destruct] %
332| cases daemon (*TODO*)
333]
334qed.
335
336lemma move_spill_colour_ok : ∀prog.∀stack_size.∀localss : nat.
337∀ carry_lives_after : bool.∀dest : Register.∀src : ℕ.
338∀f : ident.
339∀s : state LTL_LIN_state.
340repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
341   (move (prog_names … prog) localss carry_lives_after dest
342    (decision_spill src)) s =
343   if eq_Register dest RegisterA then
344         ! 〈bv,s'〉 ← (read_arg_decision localss s (decision_spill src));
345         ! s'' ← write_decision localss dest bv s';
346         if carry_lives_after then
347           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
348                   (set_carry ? (carry … s) s'')
349         else
350           return s''
351        else
352         ! 〈bv,s'〉 ← (read_arg_decision localss s (decision_spill src));
353         let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
354         ! s'' ← write_decision localss dest bv news;
355         if carry_lives_after then
356           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
357                   (set_carry ? (carry … s) s'')
358         else
359           return s''.   
360#prog #stack_size #localss #cl #dest #src #f #st
361inversion(repeat_eval_seq_no_pc ?????)
362[ #st' whd in match move; normalize nodelta whd in match preserve_carry_bit; normalize nodelta
363  cases cl -cl normalize nodelta
364      whd in match set_stack; normalize nodelta whd in match read_arg_decision;
365      normalize nodelta @eq_Register_elim
366      [1,3: #EQ destruct(EQ) normalize nodelta whd in match set_stack_a;
367            normalize nodelta
368      |*:   * #Hr normalize nodelta
369      ]
370      whd in match set_stack_not_a; whd in match set_dp_by_offset;
371      whd in match repeat_eval_seq_no_pc; normalize nodelta
372      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
373      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ normalize nodelta #EQ destruct]
374      #st1 whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match acca_arg_retrieve;
375      normalize nodelta
376      change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
377      whd in match hw_reg_retrieve; normalize nodelta whd in match set_regs;
378      normalize nodelta >hwreg_retrieve_hwregstore_hit >m_return_bind
379      whd in match snd_arg_retrieve; normalize nodelta
380      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
381      [2,4,6,8: % #ABS whd in ABS : (??%%); destruct(ABS)]
382      (*[1,2: >hwreg_retrieve_hwregstore_miss
383            [2,4: % #ABS whd in ABS : (??%%); destruct(ABS)] ] *)
384      [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
385      #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2 whd in match acca_store;
386      normalize nodelta change with (hw_reg_store ???) in match (acca_store_ ??????);
387      whd in match hw_reg_store; normalize nodelta >hwreg_store_idempotent
388      (*[1,2: >hwreg_retrieve_insensitive_to_set_other ] *) >m_return_bind
389      whd in match set_carry; whd in match set_regs; normalize nodelta
390      whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
391      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)]
392      #st'' whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_hit in ⊢ (% → ?);
393      >(hwreg_store_commute RegisterDPL RegisterA) [2,4,6,8: % normalize #EQ destruct]
394      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
395      whd in match acca_arg_retrieve; normalize nodelta
396      change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????) in ⊢ (% → ?);
397      whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_hit
398      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
399      whd in match (snd_arg_retrieve_ ?????);
400      >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
401      >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
402      (* [1,3: >hwreg_retrieve_hwregstore_miss [2,4: % normalize #EQ destruct(EQ)] ] *)
403      [1,2: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
404      #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2 whd in match acca_store;
405      normalize nodelta whd in match (acca_store_ ??????);
406      >hwreg_store_idempotent >m_return_bind whd in match set_carry;
407      whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ
408      destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
409      inversion (eval_seq_no_pc ??????)
410      [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)] #st''
411      whd in match set_regs; normalize nodelta
412      >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
413      whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match dph_arg_retrieve;
414      normalize nodelta whd in ⊢ (??%?? → ?); inversion(pointer_of_address ?)
415      [2,4,6,8: #e #_ whd in ⊢ (??%?? → ?); #EQ destruct(EQ)] #ptr
416      >hwreg_retrieve_hwregstore_miss in ⊢ (% → ?); [2,4,6,8: normalize % #EQ destruct]
417      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
418        [2: normalize % #EQ destruct]
419        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
420        >hwreg_retrieve_hwregstore_hit
421      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
422        [2: normalize % #EQ destruct]
423        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
424        >hwreg_retrieve_hwregstore_hit
425      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
426        [2: normalize % #EQ destruct]
427        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
428        >hwreg_retrieve_hwregstore_hit
429      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
430        [2: normalize % #EQ destruct]
431        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
432        >hwreg_retrieve_hwregstore_hit
433      ]
434      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
435      whd in match (acca_arg_retrieve_ ?????);
436       #H @('bind_inversion H) -H  #m1 #H lapply(opt_eq_from_res ???? H) -H #EQm1
437       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
438       >(hwreg_store_commute RegisterDPH RegisterA) [2,4,6,8: normalize % #EQ destruct]
439      >hwreg_store_idempotent >m_return_bind whd in match set_regs;
440      normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
441      [2,4: @eq_Register_elim [1,3: #EQ destruct(EQ) @⊥ @Hr %] #_ normalize nodelta
442            whd in ⊢ (??%?? → ?); whd in match set_regs; whd in match set_carry;
443            normalize nodelta
444            [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
445              >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
446              whd in match (other_bit ?); ] >hwreg_retrieve_hwregstore_hit
447      |*: whd in ⊢ (??%?? → ?); whd in match (other_bit ?); whd in match set_carry;
448          normalize nodelta
449      ] #EQ destruct(EQ) @sym_eq >m_return_bind whd in match write_decision;
450      normalize nodelta
451      whd in match hw_reg_retrieve; whd in match set_regs; normalize nodelta
452      >m_return_bind
453      >EQx1x2 >m_return_bind >EQy1y2 >m_return_bind >EQptr
454      >m_return_bind >EQm1 >m_return_bind whd in ⊢ (??%?); @eq_f 
455      @eq_f3 [2,3,5,6,8,9,11,12: %]
456      [1,3: <hwreg_store_set_other_commut <hwreg_store_set_other_commut
457            <hwreg_store_set_other_commut [ <hwreg_store_set_other_commut] ]
458      @eq_f3 [1,2,4,5,7,8,10,11: %]
459      >(hwreg_store_commute RegisterDPH RegisterDPL) [2,4,6,8: % #EQ destruct] %
460| cases daemon (*TODO*)
461]
462qed.
463
464lemma move_colour_spill_ok : ∀prog.∀stack_size.∀localss : nat.
465∀ carry_lives_after : bool.∀dest : ℕ.∀src : Register.
466∀f : ident.
467∀s : state LTL_LIN_state. 
468src ≠ RegisterDPL →  src ≠ RegisterDPH →
469repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
470  (move (prog_names … prog) localss carry_lives_after (decision_spill dest) src) s
471  =
472! 〈bv,s'〉 ← (read_arg_decision localss s src);
473        let rgs ≝ if eq_Register src RegisterA then
474               hwreg_store RegisterST1 (hwreg_retrieve (regs … s') RegisterA)
475                (regs … s')
476              else
477               hwreg_store RegisterA (hwreg_retrieve (regs … s') src) (regs … s') in
478        ! s'' ← write_decision localss (decision_spill dest) bv (set_regs LTL_semantics rgs s');
479        if carry_lives_after then
480           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
481                   (set_carry ? (carry … s) s'')
482         else
483           return s''.
484cases daemon (* problemi con qed!!!
485#prog #stack_size #localss #cl #dest #src #f #st #H1 #H2
486inversion(repeat_eval_seq_no_pc ?????)
487[ #st' whd in match move; whd in match preserve_carry_bit; normalize nodelta
488      cases cl -cl normalize nodelta
489      whd in match set_stack; normalize nodelta whd in match read_arg_decision;
490      normalize nodelta @eq_Register_elim
491      [1,3: #EQ destruct(EQ) normalize nodelta whd in match set_stack_a;
492            normalize nodelta
493      |*:   * #Hr normalize nodelta
494      ]
495      whd in match set_stack_not_a; whd in match set_dp_by_offset;
496      whd in match repeat_eval_seq_no_pc; normalize nodelta
497      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
498      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ normalize nodelta #EQ destruct]
499      #st1 whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match acca_arg_retrieve;
500      normalize nodelta
501      change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
502      whd in match hw_reg_retrieve; normalize nodelta whd in match set_regs;
503      normalize nodelta >hwreg_retrieve_hwregstore_hit >m_return_bind
504      whd in match snd_arg_retrieve; normalize nodelta
505      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
506      [2,4,6,8: % #ABS whd in ABS : (??%%); destruct(ABS)]
507      [1,2: >hwreg_retrieve_hwregstore_miss
508            [2,4: % #ABS whd in ABS : (??%%); destruct(ABS)] ]
509      [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
510      #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2 whd in match acca_store;
511      normalize nodelta change with (hw_reg_store ???) in match (acca_store_ ??????);
512      whd in match hw_reg_store; normalize nodelta >hwreg_store_idempotent
513      [ >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
514      whd in match set_carry; whd in match set_regs; normalize nodelta
515      whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
516      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)]
517      #st'' whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_hit in ⊢ (% → ?);
518      >(hwreg_store_commute RegisterDPL RegisterA) [2,4,6,8: % normalize #EQ destruct]
519      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
520      whd in match acca_arg_retrieve; normalize nodelta
521      change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????) in ⊢ (% → ?);
522      whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_hit
523      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
524      whd in match (snd_arg_retrieve_ ?????);
525      >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
526      >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
527      [1,3: >hwreg_retrieve_hwregstore_miss [2,4: % normalize #EQ destruct(EQ)] ]
528      [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
529      #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2 whd in match acca_store;
530      normalize nodelta whd in match (acca_store_ ??????);
531      >hwreg_store_idempotent >m_return_bind whd in match set_carry;
532      whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ
533      destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
534      inversion (eval_seq_no_pc ??????)
535      [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)] #st''
536      whd in match set_regs; normalize nodelta
537      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
538        [2: normalize % #EQ destruct]
539        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
540        [2: normalize % #EQ destruct]
541        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
542        [2: normalize % #EQ destruct]
543        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
544        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(???%)??))?? → ?);
545      | >hwreg_retrieve_hwregstore_hit
546      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
547        [2: normalize % #EQ destruct]
548        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
549        [2: normalize % #EQ destruct]
550        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?
551        );
552        [2: normalize % #EQ destruct]
553        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
554        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(???%)??))?? → ?);
555      | >hwreg_retrieve_hwregstore_hit
556      ] 
557      whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match dph_arg_retrieve;
558      normalize nodelta whd in ⊢ (??%?? → ?); inversion(pointer_of_address ?)
559      [2,4,6,8: #e #_ whd in ⊢ (??%?? → ?); #EQ destruct(EQ)] #ptr
560      [ >hwreg_retrieve_hwregstore_miss in ⊢ (% → ?); [2: normalize % #EQ destruct]
561        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
562        [2: normalize % #EQ destruct]
563        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
564        [2: normalize % #EQ destruct]
565        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
566        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
567        [2: normalize % #EQ destruct]
568        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
569      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
570        [2: normalize % #EQ destruct]
571        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
572        [2: normalize % #EQ destruct]
573        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
574        [2: normalize % #EQ destruct]
575        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
576        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
577        [2: normalize % #EQ destruct]
578        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
579      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
580        [2: normalize % #EQ destruct]
581        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
582        [2: normalize % #EQ destruct]
583        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
584        [2: normalize % #EQ destruct]
585        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
586        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
587        [2: normalize % #EQ destruct]
588        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
589      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
590        [2: normalize % #EQ destruct]
591        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
592        [2: normalize % #EQ destruct]
593        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
594        [2: normalize % #EQ destruct]
595        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
596        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
597        [2: normalize % #EQ destruct]
598        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
599      ]
600      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
601      whd in match (acca_arg_retrieve_ ?????);
602      [1,3: >hwreg_retrieve_hwregstore_hit >m_return_bind #H @('bind_inversion H) -H
603            #m1 #H lapply(opt_eq_from_res ???? H) -H #EQm1
604      |*: whd in ⊢ (??%?? → ?); inversion (opt_to_res ???)
605          [2,4: #e #_ normalize nodelta #EQ destruct] #m1 #H lapply(opt_eq_from_res ???? H)
606          -H
607          [ >hwreg_retrieve_hwregstore_hit in ⊢ (??(???%)? → ?);
608          | >hwreg_retrieve_hwregstore_hit in ⊢ (??(???%)? → ?);
609          ]
610          >hwreg_retrieve_hwregstore_miss [2,4: assumption]
611          >hwreg_retrieve_hwregstore_miss [2,4: % assumption]
612          >hwreg_retrieve_hwregstore_miss [2,4: assumption]
613          [ >hwreg_retrieve_insensitive_to_set_other ] #EQm1 normalize nodelta
614      ]
615      whd in match set_m; normalize nodelta
616      [1,2: whd in ⊢ (??%% → ?); |*: whd in ⊢ (??%%% → ?);] #EQ destruct(EQ)
617      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
618      [1,3: whd in match set_carry; normalize nodelta
619            >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
620            >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
621            [ >other_bit_insensitive_to_reg_store ]
622            whd in match hwreg_set_other; normalize nodelta
623      ]
624      #EQ destruct(EQ) @sym_eq >m_return_bind whd in match write_decision;
625      normalize nodelta
626      whd in match hw_reg_retrieve; whd in match set_regs; normalize nodelta
627      >hwreg_retrieve_hwregstore_miss [2,4,6,8: normalize % #EQ destruct]
628      >m_return_bind
629      >hwreg_retrieve_hwregstore_miss [2,4,6,8: normalize % #EQ destruct]
630      >m_return_bind
631      >EQx1x2 >m_return_bind >EQy1y2 >m_return_bind >EQptr
632      >m_return_bind >EQm1 >m_return_bind @eq_f whd in match set_m;
633      normalize nodelta @eq_f3 [2,3,5,6,8,9,11,12: %]
634      >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (???(???%));
635      [2,4,6,8: % #EQ destruct]
636      [1,3: >(hwreg_store_idempotent RegisterA)
637              >(hwreg_store_commute RegisterA RegisterDPH) [2,4,6: % #EQ destruct]
638              >(hwreg_store_commute RegisterA RegisterDPL) [2,4,6: % #EQ destruct]
639      |*: >(hwreg_store_commute RegisterDPH RegisterA) [2,4: % #EQ destruct]
640        [ >(hwreg_store_idempotent RegisterA) in ⊢ (???%);
641        | >(hwreg_store_idempotent RegisterA) in ⊢ (???%);
642        ]
643        [2:  >(hwreg_store_commute RegisterA RegisterDPH) [2: % #EQ destruct]
644             >(hwreg_store_commute RegisterA RegisterDPH) [2: % #EQ destruct]
645             >(hwreg_store_commute RegisterA RegisterDPL) [2,4: % #EQ destruct]
646             >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?); [%| % #EQ destruct]
647         |  >(hwreg_store_commute RegisterDPL RegisterA) [2: % #EQ destruct]
648            >(hwreg_store_commute RegisterDPL RegisterDPH) [2: % #EQ destruct]
649            %
650         ]
651      ]
652      [ >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
653      | >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
654      ]  [2,4: % #EQ destruct]
655      >(hwreg_store_commute RegisterA RegisterST1) [2,4: normalize % #EQ destruct]
656      [ <(hwreg_retrieve_insensitive_to_set_other … RegisterA (carry … st)) ]
657      >(hwreg_store_retrieve_eq RegisterA) %
658| cases daemon (*TODO*)
659] *)
660qed.
661
662lemma move_imm_spill_ok : ∀prog.∀stack_size.∀localss : nat.
663∀ carry_lives_after : bool.∀dest : ℕ.∀src : Byte.
664∀f : ident.
665∀s : state LTL_LIN_state. 
666repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
667  (move (prog_names … prog) localss carry_lives_after (decision_spill dest)
668   (arg_decision_imm src)) s
669  =  ! 〈bv,s'〉 ← (read_arg_decision localss s (arg_decision_imm src));
670      let rgs ≝ hwreg_store RegisterA (BVByte src) (regs … s') in
671      ! s'' ← write_decision localss (decision_spill dest) bv
672               (set_regs LTL_semantics rgs s');
673      if carry_lives_after then
674           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
675                   (set_carry ? (carry … s) s'')
676         else
677           return s''. cases daemon (*qed ha problemi
678#prog #stack_size #localss #cl #dest #src #f #st
679inversion(repeat_eval_seq_no_pc ?????)
680[ #st' whd in match move; whd in match preserve_carry_bit; normalize nodelta
681      whd in match set_stack_int; normalize nodelta
682      cases cl -cl normalize nodelta whd in match repeat_eval_seq_no_pc; normalize nodelta     
683      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
684      normalize nodelta inversion (eval_seq_no_pc ??????)
685      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' whd in match eval_seq_no_pc in ⊢ (% → ?);
686      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
687      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
688      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
689      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
690      [2,4: normalize % #EQ destruct] [ >hwreg_retrieve_insensitive_to_set_other]
691      >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
692      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
693      >hwreg_store_idempotent >m_return_bind whd in match set_carry; whd in match set_regs;
694      normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
695      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
696      normalize nodelta inversion (eval_seq_no_pc ??????)
697      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
698      >(hwreg_store_commute RegisterDPL RegisterA) [2,4: normalize % #EQ destruct]
699      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
700      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
701      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
702      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
703      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
704      [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
705      [2,4: normalize % #EQ destruct]  [ >hwreg_retrieve_insensitive_to_set_other]
706      >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
707      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
708      >hwreg_store_idempotent >m_return_bind whd in match set_regs; whd in match set_carry;
709      normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
710      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
711      normalize nodelta inversion (eval_seq_no_pc ??????)
712      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
713      >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
714      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
715      normalize nodelta whd in match dph_arg_retrieve; normalize nodelta
716      whd in ⊢ (??%?% → ?); inversion (pointer_of_address ?) [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
717      #ptr >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
718      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
719        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
720        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
721        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
722      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
723        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
724        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
725        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
726      ]
727      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
728      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
729      >m_return_bind #H @('bind_inversion H) -H #m #H lapply(opt_eq_from_res ???? H) -H
730      #EQm whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
731      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
732      normalize nodelta whd in match set_carry; normalize nodelta
733      [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
734        >other_bit_insensitive_to_reg_store whd in match hwreg_set_other; normalize nodelta ]
735      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
736      >m_return_bind whd in match write_decision; normalize nodelta whd in match set_regs;
737      whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_miss
738      [2,4: % normalize #EQ destruct] >m_return_bind  >hwreg_retrieve_hwregstore_miss
739      [2,4: % normalize #EQ destruct] >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
740      >m_return_bind >EQptr >m_return_bind >EQm >m_return_bind whd in match set_m;
741      whd in match set_regs; normalize nodelta @eq_f whd in match set_carry;
742      normalize nodelta @eq_f3 [2,3,5,6: %]
743      [ >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
744        >(hwreg_store_commute RegisterDPL RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
745      | >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
746        >(hwreg_store_commute RegisterDPL RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
747      ]
748      [2: @eq_f3 [1,2: %] >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
749         [2: % normalize #EQ destruct]
750      |  >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?); [2: % normalize #EQ destruct]
751      ]
752      %
753| cases daemon (*TODO *)
754] *)
755qed.
756
757lemma move_imm_colour_ok : ∀prog.∀stack_size.∀localss : nat.
758∀ carry_lives_after : bool.∀dest : Register.∀src : Byte.
759∀f : ident.
760∀s : state LTL_LIN_state. 
761repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
762  (move (prog_names … prog) localss carry_lives_after dest
763   (arg_decision_imm src)) s =
764 ! 〈bv,s'〉 ← (read_arg_decision localss s (arg_decision_imm src));
765      if eq_Register dest RegisterA then 
766       write_decision localss dest bv s'
767      else
768       write_decision localss dest bv
769        (set_regs LTL_semantics
770         (hwreg_store RegisterA (BVByte src) (regs … s')) s').
771#prog #stack_size #localss #cl #dest #src #f #st
772inversion(repeat_eval_seq_no_pc ?????)
773[ #st whd in ⊢ (??%%? → ?); normalize nodelta @eq_Register_elim [#EQ destruct(EQ) | #H1 ]
774      whd in ⊢ (??%?? → ?); whd in match set_regs; normalize nodelta #EQ destruct(EQ)
775      @sym_eq whd in match read_arg_decision; normalize nodelta >m_return_bind
776      whd in match write_decision; normalize nodelta >m_return_bind
777      @eq_f whd in match set_regs; normalize nodelta [%] @eq_f3 [2,3: %]
778      >hwreg_retrieve_hwregstore_hit %
779| #e whd in ⊢ (??%%? → ?); @eq_Register_elim [#EQ destruct(EQ) | #H1]
780  whd in ⊢ (??%%? → ?); #EQ destruct(EQ)
781]
782qed.       
783
784lemma move_colour_colour_ok : ∀prog.∀stack_size.∀localss : nat.
785∀ carry_lives_after : bool.∀dest : Register.∀src : Register.
786∀f : ident.
787∀s : state LTL_LIN_state.
788src ≠ RegisterDPL →  src ≠ RegisterDPH → 
789repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
790  (move (prog_names … prog) localss carry_lives_after dest src) s =
791 if eq_Register dest src then return s
792         else if eq_Register dest RegisterA then
793               ! 〈bv,s'〉 ← (read_arg_decision localss s src);
794               write_decision localss dest bv s'
795         else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
796               let rgs ≝ (hwreg_store RegisterA (hwreg_retrieve (regs … s) src) (regs … s')) in
797               write_decision localss dest bv (set_regs LTL_semantics rgs s').
798#prog #stack_size #localss #cl #dest #src #f #st #H1 #H2
799inversion(repeat_eval_seq_no_pc ?????)
800[ #st' whd in match move; normalize nodelta whd in ⊢ (??%?? → ?); @eq_Register_elim
801      [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (??%?% → ?); #EQ destruct(EQ) %
802       ]
803      #H3 normalize nodelta @eq_Register_elim normalize nodelta
804      [ #EQ destruct(EQ) whd in match repeat_eval_seq_no_pc; normalize nodelta
805        whd in match (m_fold ??????) in ⊢ (??%?? → ?); #EQ destruct(EQ)
806        @sym_eq whd in match read_arg_decision; normalize nodelta >m_return_bind
807        whd in match write_decision; normalize nodelta >m_return_bind
808        whd in match set_regs; normalize nodelta @eq_f % ]
809      #H4 normalize nodelta @eq_Register_elim
810      [ #EQ destruct(EQ) | #H5] normalize nodelta whd in ⊢ (??%?% → ?);
811      whd in match set_regs; normalize nodelta [2: >hwreg_retrieve_hwregstore_hit ]
812      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
813      >m_return_bind whd in match write_decision; normalize nodelta >m_return_bind
814      @eq_f whd in match set_regs; normalize nodelta cases cl normalize nodelta
815      @eq_f3 try % @eq_f3 [1,2,4,5: %] >hwreg_store_retrieve_eq %
816| #e whd in match move; normalize nodelta @eq_Register_elim
817  [#EQ destruct whd in ⊢ (??%?? → ?); #EQ destruct] #_
818  @eq_Register_elim [#EQ destruct whd in ⊢ (??%?? → ?); #EQ destruct]
819  #_ normalize nodelta whd in ⊢ (??%?? → ?); @eq_Register_elim
820  [#EQ destruct whd in ⊢ (??%?? → ?); #EQ destruct] #_ whd in ⊢ (??%?? → ?); #EQ destruct
821]
822qed.
823
824lemma move_spec : ∀prog.∀stack_size.∀localss : nat.
825∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
826∀f : ident.
827∀s : state LTL_LIN_state.
828invariant_for_move src →
829repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
830   (move (prog_names … prog) localss carry_lives_after dest src) s =
831match src with
832[ arg_decision_spill n ⇒
833  match dest with
834  [ decision_spill n1 ⇒
835     if eqb n n1 then return s
836     else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
837          let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
838          ! s'' ← write_decision localss dest bv news;
839          let regSt1 ≝ (hwreg_store RegisterST1 bv (regs … s'')) in
840          if carry_lives_after then
841            return set_regs LTL_semantics (hwreg_set_other (carry … s) regSt1)
842                    (set_carry ? (carry … s) s'')
843          else
844            return set_regs LTL_semantics regSt1 s''
845   | decision_colour r ⇒
846        if eq_Register r RegisterA then
847         ! 〈bv,s'〉 ← (read_arg_decision localss s src);
848         ! s'' ← write_decision localss dest bv s';
849         if carry_lives_after then
850           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
851                   (set_carry ? (carry … s) s'')
852         else
853           return s''
854        else
855         ! 〈bv,s'〉 ← (read_arg_decision localss s src);
856         let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
857         ! s'' ← write_decision localss dest bv news;
858         if carry_lives_after then
859           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
860                   (set_carry ? (carry … s) s'')
861         else
862           return s''
863   ]
864| arg_decision_colour r ⇒
865      match dest with
866      [ decision_spill _ ⇒
867        ! 〈bv,s'〉 ← (read_arg_decision localss s src);
868        let rgs ≝ if eq_Register r RegisterA then
869               hwreg_store RegisterST1 (hwreg_retrieve (regs … s') RegisterA)
870                (regs … s')
871              else
872               hwreg_store RegisterA (hwreg_retrieve (regs … s') r) (regs … s') in
873        ! s'' ← write_decision localss dest bv (set_regs LTL_semantics rgs s');
874        if carry_lives_after then
875           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
876                   (set_carry ? (carry … s) s'')
877         else
878           return s''
879      | decision_colour r1 ⇒
880         if eq_Register r1 r then return s
881         else if eq_Register r1 RegisterA then
882               ! 〈bv,s'〉 ← (read_arg_decision localss s src);
883               write_decision localss dest bv s'
884         else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
885               let rgs ≝ (hwreg_store RegisterA (hwreg_retrieve (regs … s) r) (regs … s')) in
886               write_decision localss dest bv (set_regs LTL_semantics rgs s')
887      ]     
888| arg_decision_imm b ⇒
889   match dest with
890   [ decision_spill _ ⇒
891      ! 〈bv,s'〉 ← (read_arg_decision localss s src);
892      let rgs ≝ hwreg_store RegisterA (BVByte b) (regs … s') in
893      ! s'' ← write_decision localss dest bv (set_regs LTL_semantics rgs s');
894      if carry_lives_after then
895           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
896                   (set_carry ? (carry … s) s'')
897         else
898           return s''
899   | decision_colour r ⇒
900      ! 〈bv,s'〉 ← (read_arg_decision localss s src);
901      if eq_Register r RegisterA then 
902       write_decision localss dest bv s'
903      else
904       write_decision localss dest bv
905        (set_regs LTL_semantics
906         (hwreg_store RegisterA (BVByte b) (regs … s')) s')
907  ]
908].
909#prog #stack_size #localss #cl #dest #src #f #st #good
910cases src in good;
911[ #r * #H1 #H2 normalize nodelta cases dest
912  [ #n normalize nodelta @move_colour_spill_ok assumption
913  | #r normalize nodelta @move_colour_colour_ok assumption
914  ]
915| #n * cases dest
916  [ #n1 normalize nodelta @move_spill_spill_ok
917  | #r normalize nodelta @move_spill_colour_ok
918  ]
919| #b * cases dest
920  [ #n normalize nodelta @move_imm_spill_ok
921  | #r normalize nodelta @move_imm_colour_ok
922  ]
923]
924qed.
925
926
927
928
Note: See TracBrowser for help on using the repository browser.