source: src/ERTL/MoveCorrectness.ma @ 3371

Last change on this file since 3371 was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

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