source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2570

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

ERTLtoERTLptr in place

File size: 33.8 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 "ERTLptr/ERTLtoERTLptr.ma".
16include "common/StatusSimulation.ma".   
17include "joint/Traces.ma".
18include "ERTLptr/semantics.ma".
19include "common/ExtraMonads.ma".
20
21definition ERTL_status ≝
22λprog : ertl_program.λstack_sizes.
23joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
24
25definition ERTLptr_status ≝
26λprog : ertlptr_program.λstack_sizes.
27joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
28
29definition sigma_map ≝ λ prog : ertl_program.
30joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.
31
32definition sigma_pc_opt :
33∀ prog : ertl_program.
34sigma_map prog → program_counter → option program_counter ≝
35λprog,sigma,pc.
36  let ge ≝ globalenv_noinit … prog in
37  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
38    return pc
39  else
40    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
41    ! ertl_ptr_point ← sigma fd (point_of_pc ERTL_semantics pc) ;
42    return pc_of_point
43    ERTLptr_semantics (pc_block pc) ertl_ptr_point.
44
45definition well_formed_pc ≝
46λprog,sigma,pc.sigma_pc_opt prog sigma pc ≠ None ?.
47
48definition sigma_pc ≝
49λprog,sigma,pc.λprf : well_formed_pc prog sigma pc. opt_safe … prf.
50
51definition sigma_beval_opt :
52 ∀prog : ertl_program.
53  sigma_map prog →
54  beval → option beval ≝
55λprog,sigma,bv.
56match bv with
57[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt prog sigma pc ; return BVpc pc' prt
58| _ ⇒ return bv
59].
60
61definition sigma_beval :
62 ∀prog,sigma,bv.
63 sigma_beval_opt prog sigma bv ≠ None ? → beval ≝
64 λprog,sigma,bv.opt_safe ….
65
66definition sigma_is_opt :
67 ∀prog : ertl_program.
68  sigma_map prog →
69  internal_stack → option internal_stack ≝
70λprog,sigma,is.
71match is with
72[ empty_is ⇒ return empty_is
73| one_is bv ⇒ ! bv' ← sigma_beval_opt … sigma bv ; return one_is bv'
74| both_is bv1 bv2 ⇒
75  ! bv1' ← sigma_beval_opt … sigma bv1 ;
76  ! bv2' ← sigma_beval_opt … sigma bv2 ;
77  return both_is bv1' bv2'
78].
79
80definition sigma_is :
81 ∀prog,sigma,is.
82 sigma_is_opt prog sigma is ≠ None ? → internal_stack ≝
83 λprog,sigma,is.opt_safe ….
84 
85lemma sigma_is_empty : ∀prog,sigma.
86  ∀prf.sigma_is prog sigma empty_is prf = empty_is.
87#prog #sigma #prf whd in match sigma_is; normalize nodelta
88@opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
89
90lemma sigma_is_pop_commute :
91 ∀prog,sigma,is.
92 ∀prf : sigma_is_opt prog sigma is ≠ None ?.
93 res_preserve …
94  (λpr.sigma_beval_opt prog sigma (\fst pr) ≠ None ? ∧
95       sigma_is_opt prog sigma (\snd pr) ≠ None ?)
96  (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉)
97  (is_pop is) (is_pop (sigma_is … prf)).
98#prog #sigma * [|#bv1|#bv1 #bv2] #prf
99[ @res_preserve_error
100|*:
101 whd in match sigma_is in ⊢ (?????????%); normalize nodelta
102 @opt_safe_elim #is'
103  #H @('bind_inversion H) -H #bv1' #EQ1
104  [2: #H @('bind_inversion H) -H #bv2' #EQ2 ]
105 whd in ⊢ (??%%→?); #EQ destruct(EQ)
106 @mfr_return_eq
107 [1,3: @hide_prf %%
108 |*: whd in match sigma_beval; whd in match sigma_is;
109  normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is''
110 ]
111 [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ]
112  whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
113 [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') %
114]
115qed.
116
117definition well_formed_mem :
118 ∀prog : ertl_program.
119  sigma_map prog →
120 bemem → Prop ≝
121λprog,sigma,m.
122∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
123  sigma_beval_opt prog sigma (contents (blocks m b) z) ≠ None ?.
124
125
126
127definition sigma_mem :
128 ∀prog,sigma,m.
129 well_formed_mem prog sigma m →
130 bemem ≝
131 λprog,sigma,m,prf.
132 mk_mem
133  (λb.
134    If Zltb (block_id b) (nextblock m) then with prf' do   
135      let l ≝ low_bound m b in
136      let h ≝ high_bound m b in
137      mk_block_contents l h
138      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
139        sigma_beval prog sigma (contents (blocks m b) z) ?
140      else BVundef)
141    else empty_block OZ OZ)
142  (nextblock m)
143  (nextblock_pos m).
144@hide_prf
145lapply prf'' lapply prf' -prf' -prf''
146@Zltb_elim_Type0 [2: #_ * ]
147#bid_ok *
148@Zleb_elim_Type0 [2: #_ * ]
149@Zltb_elim_Type0 [2: #_ #_ * ]
150#zh #zl * @(prf … bid_ok zl zh)
151qed.
152
153
154(*DOPPIONI DEI CORRISPONDENTI LEMMI IN LINEARISE_PROOF.MA *)
155lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
156** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed.
157
158axiom mem_ext_eq :
159  ∀m1,m2 : mem.
160  (∀b.let bc1 ≝ blocks m1 b in
161      let bc2 ≝ blocks m2 b in
162      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
163      ∀z.contents bc1 z = contents bc2 z) →
164  nextblock m1 = nextblock m2 → m1 = m2.
165
166lemma beloadv_sigma_commute:
167∀prog,sigma,ptr.
168preserving … opt_preserve …
169 (sigma_mem prog sigma)
170 (sigma_beval prog sigma)
171 (λm.beloadv m ptr)
172 (λm.beloadv m ptr).
173#prog  #sigma #ptr #m #prf #bv
174whd in match beloadv;
175whd in match do_if_in_bounds;
176whd in match sigma_mem;
177normalize nodelta
178@If_elim #block_ok >block_ok normalize nodelta
179[2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]
180@If_elim #H
181[ elim (andb_true … H)
182  #H1 #H2
183  whd in match sigma_beval; normalize nodelta
184  @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta
185  whd in ⊢ (???%→?); #EQ' destruct
186  >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe
187| elim (andb_false … H) -H #H >H
188  [2: >commutative_andb ] normalize nodelta
189  whd in ⊢ (???%→?); #ABS destruct(ABS)
190]
191qed.
192
193include alias "common/GenMem.ma".
194
195lemma bestorev_sigma_commute :
196∀prog,sigma,ptr.
197preserving2 ?? opt_preserve …
198  (sigma_mem prog sigma)
199  (sigma_beval prog sigma)
200  (sigma_mem prog sigma)
201  (λm.bestorev m ptr)
202  (λm.bestorev m ptr).
203#prog #sigma #ptr #m #bv #prf1 #prf2 #m'
204whd in match bestorev;
205whd in match do_if_in_bounds;
206whd in match sigma_mem;
207whd in match update_block;
208 normalize nodelta
209@If_elim #block_ok >block_ok normalize nodelta
210[2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]
211@Zleb_elim_Type0 #H1
212[ @Zltb_elim_Type0 #H2 ]
213[2,3: #ABS normalize in ABS; destruct(ABS) ]
214normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ)
215%
216[2: whd in ⊢ (???%);
217  @eq_f
218  @mem_ext_eq [2: % ]
219  #b @if_elim
220  [2: #B
221    @If_elim #prf1 @If_elim #prf2
222    [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]
223    whd in match low_bound; whd in match high_bound;
224    normalize nodelta
225    cut (Not (bool_to_Prop (eq_block b (pblock ptr))))
226    [ % #ABS >ABS in B; * ]
227    -B #B % [ >B %% ] #z
228    @If_elim #prf3 
229    @If_elim #prf4
230    [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ]
231    whd in match sigma_beval in ⊢ (??%%); normalize nodelta
232    @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
233    >EQ2 #EQ destruct(EQ) %
234  | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ]
235    #EQ destruct(EQ)
236    @If_elim whd in match low_bound; whd in match high_bound;
237    normalize nodelta
238    [2: >block_ok * #ABS elim (ABS I) ]
239    #prf3 % [ >B %% ]
240    #z whd in match update; normalize nodelta
241    @eqZb_elim normalize nodelta #prf4
242    [2: @If_elim #prf5 @If_elim #prf6
243      [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ]
244      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
245      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
246      normalize nodelta >(eqZb_false … prf4) >EQ2
247      #EQ destruct(EQ) %
248    | @If_elim #prf5
249      [2: >B in prf5; normalize nodelta
250        >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]
251      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
252      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
253      normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) %
254    ]
255  ]
256| whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta
257  @eq_block_elim #H normalize nodelta destruct
258  #h2 #h3 whd in match update; normalize nodelta
259  [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]
260  @prf1 assumption
261]
262qed.
263
264include alias "common/Identifiers.ma".
265include alias "common/PositiveMap.ma".
266
267let rec map_inf A B (b : positive_map A) on b :
268        (∀a : A.(Σp:Pos. lookup_opt A p b = Some ? a) → B) →  positive_map B ≝
269λf.       
270(match b return λx.x=b → ? with
271[ pm_leaf ⇒ λ_.pm_leaf ?
272| pm_node a l r ⇒ λprf.pm_node ?
273((match a return λx.a=x→? with
274        [Some x ⇒ λprf1.return f x «one,?» 
275        |None ⇒ λ_.None ?
276        ]) (refl ? a))
277    (map_inf ?? l (λa1,prf1.f a1 «p0 ?,?»))
278    (map_inf ?? r (λa1,prf1.f a1 «p1 ?,?»))
279]) (refl ? b).
280[ @hide_prf <prf normalize assumption
281|*: [1,3: @hide_prf] cases prf1 #tl #H [4,3 : @tl] <prf assumption
282] qed.
283
284
285definition map_inf1 :  ∀A, B: Type[0].
286  ∀tag: String.
287  ∀m:identifier_map tag A.
288   (∀a:A.(Σid. lookup tag A m id = Some A a) → B) →
289  identifier_map tag B ≝
290λA,B,tag,m.
291(match m return λx.(∀a:A.(Σid. lookup tag A x id = Some A a) → B) → ? with
292  [an_id_map b ⇒ λF.an_id_map …
293       (map_inf A B b (λa,prf.F a «an_identifier tag ?,?»))]).
294[@hide_prf] cases prf #pos #H assumption
295qed.
296
297inductive id_is_in (A : Type[0]) : Pos →  positive_map A → Prop ≝
298| is_in_root : ∀l,r,opt_a. id_is_in A (one) (pm_node … opt_a l r)
299| is_in_left : ∀l,r,opt_a,x. id_is_in A x l →
300                                    id_is_in A (p0 x) (pm_node … opt_a l r)
301| is_in_right : ∀l,r,opt_a,x. id_is_in A x r →
302                                    id_is_in A (p1 x) (pm_node … opt_a l r).
303
304definition id_is_in : ∀A : Type[0]. ∀tag : String.
305identifier_map tag A → identifier tag → Prop ≝
306λA,tag,m,id.match id with
307     [an_identifier x ⇒ match m with
308                              [an_id_map p ⇒ id_is_in A x p]
309     ].
310
311lemma lookup_map : ∀A,B : Type[0].
312  ∀tag : String.
313  ∀m : identifier_map tag A.
314  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
315  ∀ id,opt_a. lookup tag A m id =opt_a →
316lookup tag B (map_inf1 A B tag m F) id =
317(match opt_a return λx.opt_a = x→ ? with
318[Some a ⇒ λprf.Some ? (F a «id,?»)
319|None ⇒ λ_.None ?
320])(refl ? (opt_a)).
321[2: @hide_prf //]
322#A #B #tag * #m elim m [2: * [2: #a] #l #r #Hl #Hr] #F ** [1,4,7: |*: #x]
323* [2,4,6,8,10,12,14,16,18: #a1] normalize in ⊢ (% → ?); [1,2,3,8,9,10: #EQ destruct]
324// normalize nodelta
325#EQ
326[1,3: lapply(Hr ? (an_identifier tag x) (Some ? a1) EQ)
327  [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 |*: %{(an_identifier tag (p1 id2))} <id2_spec %]]
328|2,4: lapply(Hl ? (an_identifier tag x) (Some ? a1) EQ)
329  [1,3: #a2 * * #id2 #id2_spec @F [1,3:  @a2 |*: %{(an_identifier tag (p0 id2))} <id2_spec %]]
330|5,7:  lapply(Hr ? (an_identifier tag x) (None ?) EQ)
331  [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 |*: %{(an_identifier tag (p1 id2))} <id2_spec %]]
332|6,8: lapply(Hl ? (an_identifier tag x) (None ?) EQ)
333  [1,3: #a2 * * #id2 #id2_spec @F [1,3:  @a2 |*: %{(an_identifier tag (p0 id2))} <id2_spec %]]
334] normalize #EQ1 <EQ1 %
335qed.
336
337(*
338lemma lookup_map_weak : ∀ A,B : Type[0].
339  ∀tag : String.
340  ∀m : identifier_map tag A.
341  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
342  ∀ id,a,prf.
343 lookup tag B (map_inf1 A B tag m F) id = Some ? (F a «id,prf»).
344#A #B #tag #m #F #id #a #prf >(lookup_map … prf) normalize %
345qed.
346
347
348lemma lookup_map_fail : ∀A,B : Type[0].
349∀tag : String.
350  ∀m : identifier_map tag A.
351  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
352  ∀ id. lookup tag A m id = None ? →
353  lookup tag B (map_inf1 A B tag m F) id = None ?.
354cases daemon
355qed.*)
356
357
358lemma lookup_eq : ∀ A : Type[0].
359∀m,m' : positive_map A.
360(∀id. lookup_opt A id m = lookup_opt A id m'
361      ∧ (id_is_in A id m ↔ id_is_in A id m')) → m=m'.
362#A #m elim m
363[ * [#_ %] #opt_a #l #r #H lapply(H one) normalize * #EQ >EQ * #_ #H1 lapply(H1 ?) [%]
364  -H1 -H <EQ -EQ #H inversion H #l1 #r1 #opt_a1
365  [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
366  |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
367  ]
368| #opt_a #l #r #Hl #Hr *
369  [ #H lapply(H one) normalize * #EQ >EQ * #H1 #_ lapply(H1 ?) [%]
370  -H1 -H -EQ #H inversion H #l1 #r1 #opt_a1
371    [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
372    |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
373    ]
374  | #opt_a1 #l1 #r1 #H lapply(H one) normalize * #EQ >EQ -EQ #_ @eq_f2 [@Hl|@Hr]
375    #id [ lapply(H (p0 id)) | lapply(H (p1 id))] normalize * #H1 * #H2 #H3 %
376    [1,3: assumption] % #H4 [1,3: lapply(H2 ?) |*: lapply(H3 ?)]
377    try %2 try %3 try assumption #H5 inversion H5 #l2 #r2 #opt_a2
378    [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
379               [1,3: cut(p0 id ≠ one) [1,3: @(pos_elim … id) /3/]
380               |*:   cut(p1 id ≠ one) [1,3: @(pos_elim … id) /3/]
381               ] * #H @H assumption
382    |*: #pos #H6 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
383        #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) #_ assumption
384    ]
385  ]
386]
387qed.
388
389lemma update_lookup_previous : ∀ A : Type[0].
390∀ tag : String.
391∀m,m' : identifier_map tag A. ∀id,a.
392update tag A m id a = return m' ↔
393(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
394(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
395     (id_is_in A tag m id' ↔ id_is_in A tag m' id')).
396#A #tag * #m * #m' * #id #a %
397  [ whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
398    #m1 #m1_spec #EQ destruct % [%]
399    [  normalize @(update_lookup_opt_same … m1_spec)
400    |3: * #id' * #id_spec' normalize %
401        [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %]
402        lapply id_spec' lapply m1_spec -id_spec' -m1_spec
403        (*cases id [|*:#x] -id normalize*) lapply m' -m' lapply id lapply id' -id -id'
404        elim m [#id' #id #m' cases id [|*: #x] normalize #EQ destruct]
405        #opt_a #l #r #Hl #Hr #id' #id #m' cases id [|*:#x] -id normalize
406        [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %]
407          #x #_ normalize % #H [1,2: %3 |*: %2]
408          inversion H #l1 #r1 #opt_a1
409          [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥
410                     [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/]
411                     |*:   cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/]
412                     ]
413                     * #H @H >EQ1 //   
414          |*:        #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
415                     #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption
416          ]
417        |*: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map
418            #pos_map_spec #EQ destruct #id_spec' % #H
419            inversion H #l1 #l2 #opt_a1
420            [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
421                       #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
422                       #H1 %
423            |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
424                #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
425                #H2 try %2 try %3 try assumption
426                [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
427                | @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
428                | @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
429                | @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
430                ]
431                assumption
432            ]
433         ]     
434    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
435      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
436      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
437      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
438      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
439    ]
440  | ** normalize in ⊢ (%→%→?); lapply id -id lapply m' -m' elim m
441    [ #m' #id #m_spec' normalize in ⊢ (% → ?); * #EQ @⊥ @EQ %] #opt_a #l #r #Hl #Hr
442    #m' * [|*: #x] normalize in ⊢ (%→%→?); #m_spec'
443    [ cases opt_a -opt_a [* #H @⊥ @H %] #a1 #_ #H normalize @eq_f @eq_f
444      lapply H -H lapply m_spec'; -m_spec' lapply a -a cases m'
445      [#a normalize #EQ destruct] #opt_a1 #l1 #r1 #a
446      normalize in ⊢ (%→?); #EQ >EQ #H @eq_f2 @lookup_eq #id'
447      [ lapply (H (an_identifier tag (p0 id')) ?)
448      | lapply (H (an_identifier tag (p1 id')) ?)
449      ]
450      [1,3:% @(pos_elim … id') [1,3:#H destruct|*: #n #IP #H destruct]]
451      * normalize #H1 * #H2 #H3 % [1,3: >H1 %] % #H4
452      [1,3: lapply(H2 ?) |*: lapply(H3 ?)] try %2 try %3 try assumption
453      #H5 inversion H5 #l2 #r2 #opt_a2
454        [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
455                   [1,3: cut(p0 id' ≠ one) [1,3: /3/]
456                   |*: cut(p1 id' ≠ one) [1,3: /3/]
457                   ] >EQ * #H @H %
458        |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
459            #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) #_ assumption
460        ]
461    |*: #H lapply m_spec' -m_spec' cases m' -m' [1,3: normalize #EQ destruct]
462        #opt_a1 #l1 #r1 normalize in ⊢ (% → ?); #H1 #H2
463        [ lapply(Hr ?? H1 H ?) | lapply(Hl ?? H1 H ?)]
464          [1,3: * #y * #y_spec
465            [lapply(H2 (an_identifier tag (p1 y)) ?) | lapply(H2 (an_identifier tag (p0 y)) ?)]
466            [1,3: % #EQ destruct @y_spec %] * normalize #H3 * #H4 #H5 % // % #H6
467            [1,3: lapply(H4 ?) |*: lapply (H5 ?)] try %2 try %3 try assumption
468            #H7 inversion H7 #l2 #r2 #opt_a2
469              [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
470                   [1,3: cut(p1 y ≠ one) [1,3: /3/]
471                   |*: cut(p0 y ≠ one) [1,3: /3/]
472                   ] >EQ * #H @H %
473              |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
474                 destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
475                 destruct(EQ1) #_ assumption
476              ]
477          |2,4: normalize cases(update A x a ?) normalize [2,4: #pos_map]
478               #EQ destruct @eq_f @eq_f lapply(H2 (an_identifier tag one) ?)
479               [1,3: % #EQ destruct] * normalize #EQ >EQ #_ @eq_f2 [2,3: %]
480               @lookup_eq #id'
481               [lapply (H2 (an_identifier tag (p0 id')) ?) |
482                                   lapply (H2 (an_identifier tag (p1 id')) ?) ]
483               [1,3: % #EQ1 destruct] * normalize #H3 * #H4 #H5 % // % #H6
484               [1,3: lapply(H4 ?) |*: lapply(H5 ?)] try %2 try %3 try assumption
485               #H7 inversion H7 #l2 #r2 #opt_a2
486                  [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
487                    [1,3: cut(p0 id' ≠ one) [1,3: /3/]
488                    |*: cut(p1 id' ≠ one) [1,3: /3/]
489                   ] >EQ * #H @H %
490                  |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
491                      destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
492                      destruct(EQ1) #_ assumption
493                  ]
494            ]
495      ]
496   ]
497qed.   
498               
499                   
500       
501(*
502     
503     
504     
505       -EQ
506      lapply H -H
507      [ lapply l1 -l1 elim l
508        [#l1 #H lapply (H (an_identifier tag (p0 one)) ?) [% #EQ destruct] *
509         normalize in ⊢ (%→?); cases l1 normalize [#_ #_ %] #opt_a #l2 #r2
510         #EQ <EQ * #H1 #H2 lapply (H2 ?) [%2 %] #h inversion h #l3 #r3 #opt_a3
511         [  #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥ cut(p0 one ≠ one) [@(pos_elim … one) /3/]
512         * #H @H >EQ1 //
513         |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
514              #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ1 -H destruct(EQ1) #_
515              -h -H2 inversion H1 #l4 #r4 #opt_a4
516              [ #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
517              |*: #pos #H2 #_ #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
518                  destruct(EQ1)
519              ]
520         ]
521      |
522             -EQ1 #EQ1
523      [ #_ %
524      |#opt_a2 #r2 #l2 #H lapply
525         
526qed.
527*)
528lemma update_lookup_after : ∀ A : Type[0].
529∀ tag : String.
530∀m,m' : identifier_map tag A. ∀id,a.
531update tag A m id a = return m' →
532lookup tag A m' id = Some ? a.
533#A #B #tag * #m1 * #id #a whd in ⊢ (??%% → ?); inversion(update A ???)
534normalize nodelta [#_ #EQ destruct] #pos_map #pos_map_spec #EQ destruct
535@(update_lookup_opt_same … pos_map_spec)
536qed.
537
538lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
539#x /3/
540qed.
541
542lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
543#x /3/
544qed.
545
546lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : String.
547∀m : identifier_map tag A.
548∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
549∀id. id_is_in A tag m id ↔ id_is_in B tag (map_inf1 A B tag m F) id.
550#A #B #tag * #m elim m
551[ #F * #id % normalize #H inversion H #l #r #opt_a
552  [1,4: #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
553  |*: #pos #H1 #_ #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
554  ]
555| * [2:#a] #l #r #Hl #Hr #F ** [1,4: |*:#x] normalize % #H try % try %2 try %3
556  [1,2,5,6: cases(Hr ? (an_identifier tag x)) |*: cases (Hl ? (an_identifier tag x))]
557  [2,4,6,8,10,12,14,16: #a1 ** #id1 #prf1 @F try(@a1)
558                        try(%{(an_identifier tag (p1 id1))} assumption)
559                        try(%{(an_identifier tag (p0 id1))} assumption) ]
560  try(#H1 #_ @H1) try(#_ #H1 @H1) -H1 -Hl -Hr inversion H #l1 #r1 #opt_a1
561  [1,4,7,10,13,16,19,22: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
562             [1,2,3,4: lapply(p1_neq_one x)
563             |*:       lapply(p0_neq_one x)
564             ] * #H @H >EQ %
565  |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
566      #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct #_ assumption
567  ]
568]
569qed.
570
571lemma map_update_commute : ∀ A, B : Type[0].
572∀tag : String.
573∀m1,m2 : identifier_map tag A.
574∀id,a.
575update tag A m1 id a = return m2 →
576∀ F : (∀a:A.(Σid. lookup tag A m1 id = Some A a) → B).
577∀ F': (∀a:A.(Σid. lookup tag A m2 id = Some A a) → B). 
578(∀a',id',prf,prf'. F a' «id',prf» = F' a' «id',prf'») → ∃prf.
579update tag B (map_inf1 A B tag m1 F) id (F' a «id,prf») =
580return map_inf1 A B tag m2 F'.
581#A #B #tag #m1 #m2 #id #a #m2_spec #F #F' #eqFF' %
582[ @hide_prf cases(update_lookup_previous A tag m1 m2 id a) #H1 #_ cases (H1 m2_spec)
583  * #H1 #H2 #H3 assumption
584| cases(update_lookup_previous B tag (map_inf1 A B tag m1 F)
585                             (map_inf1 A B tag m2 F') id (F' a «id,?»))
586  [ #_ #H @H |] cases(update_lookup_previous A tag m1 m2 id a) #H2 #INUTILE
587cases(H2 m2_spec) * #H3 #H4 #H5 % [%]
588[ >(lookup_map … H3) %
589| elim H4 -H4 #H4 % #H5 @H4 lapply H5 cases m1 in F; -m1 #m1 cases id -id
590  elim m1 [ #id #F normalize * %] #a1 #l #r #Hl #Hr * [|*:#x] #F normalize
591  [ cases a1 in F; [2: #a2] #F normalize [2: * %] #EQ destruct
592  |*: #H
593    [@(Hr x ??) | @(Hl x ??)]
594    [1,3:#a ** #id1 #prf1 @F [1,3: @a]
595         [%{(an_identifier tag (p1 id1))}|%{(an_identifier tag (p0 id1))}]
596         normalize assumption
597    |*: normalize @H
598    ]
599  ]
600| #id' #id_spec' lapply(H5 id' id_spec') * #H6 * #H7 #H8 %
601  [ lapply H6 inversion (lookup tag A m2 id')
602    [2: #w] #w_spec #EQ >(lookup_map … EQ) normalize nodelta
603    >(lookup_map … w_spec) normalize nodelta [2: %] @eq_f @eqFF'
604  | cases(id_is_in_map A B tag m1 F id') cases(id_is_in_map A B tag m2 F' id')
605   #H9 #H10 #H11 #H12 % #H13 [ @H9 @H7 @H12 assumption | @H11 @H8 @H10 assumption]
606  ]
607]
608qed.
609
610definition well_formed_register_env :
611∀prog : ertl_program .∀sigma : (sigma_map prog).
612register_env beval → Prop ≝
613λprog,sigma,psd_reg.∀id,bv. lookup ?? psd_reg id = Some ? bv →
614sigma_beval_opt prog sigma bv ≠ None ?.
615
616
617definition sigma_register_env :
618∀prog : ertl_program.∀sigma : (sigma_map prog).
619∀psd_env : register_env beval.
620well_formed_register_env prog sigma psd_env → register_env beval ≝
621λprog,sigma,psd_env,prf.
622map_inf1 ?? ?  psd_env (λbv,prf1.sigma_beval prog sigma bv ?).
623@hide_prf @prf cases prf1 #pi1 #H assumption
624qed.
625
626
627definition well_formed_ertl_psd_env :
628∀prog : ertl_program. ∀sigma : (sigma_map prog).
629ertl_psd_env → Prop≝
630λprog,sigma,psd_env.well_formed_register_env prog sigma (psd_regs psd_env).
631
632definition sigma_ertl_psd_env :
633∀prog : ertl_program. ∀ sigma : (sigma_map prog).
634∀psd : ertl_psd_env.
635well_formed_ertl_psd_env prog sigma psd → ertl_psd_env ≝
636λprog,sigma,psd_env,prf.
637mk_ertl_psd_env
638  (sigma_register_env …  prf)
639  (need_spilled_no psd_env).
640
641let rec well_formed_frames
642(prog : ertl_program) (sigma : (sigma_map prog))
643(l : list ertl_psd_env) on l : Prop ≝
644match l with
645  [nil ⇒ True
646  | cons a tl ⇒ well_formed_ertl_psd_env prog sigma a ∧
647               well_formed_frames prog sigma tl
648  ].
649
650
651let rec sigma_frames (prog : ertl_program) (sigma : (sigma_map prog))
652(l : list ertl_psd_env) (prf : well_formed_frames prog sigma l)
653on l : list ertl_psd_env ≝
654(match l with
655  [nil ⇒ λ_ : (l = nil ?) .nil ?
656  |cons a tl ⇒
657     λx : (l = cons ? a tl).
658       (sigma_ertl_psd_env prog sigma a ?)::
659                                   (sigma_frames prog sigma tl ?)
660     
661  ]) (refl ? l).
662@hide_prf >x in prf; whd in match (well_formed_frames ???); * //
663qed.
664
665lemma sigma_empty_frames_commute :
666∀prog : ertl_program. ∀ sigma : (sigma_map prog).
667∃prf.
668sigma_frames prog sigma [] prf = [].
669#p #s % normalize %
670qed.
671
672
673let rec sigma_bit_vector_trie_opt (prog : ertl_program)
674(sigma : (sigma_map prog)) (n : nat) (t : BitVectorTrie beval n)
675on t : option … (BitVectorTrie beval n) ≝
676match t with
677  [Leaf bv ⇒ ! bv' ← (sigma_beval_opt prog sigma bv);
678                   return Leaf … bv'
679  |Node n1 b1 b2 ⇒ ! b1' ← (sigma_bit_vector_trie_opt prog sigma n1 b1);
680                   ! b2' ← (sigma_bit_vector_trie_opt prog sigma n1 b2);
681                   return Node … n1 b1' b2'
682  |Stub n1 ⇒  return Stub … n1
683  ].
684
685
686definition well_formed_hw_register_env :
687∀ prog : ertl_program. ∀ sigma : (sigma_map prog).
688hw_register_env → Prop ≝
689λprog,sigma,regs.sigma_bit_vector_trie_opt prog sigma 6 (reg_env … regs) ≠ None ?.
690
691definition sigma_hw_register_env :
692∀prog: ertl_program. ∀sigma : (sigma_map prog).
693∀h_reg : hw_register_env. well_formed_hw_register_env prog sigma h_reg →
694hw_register_env ≝
695λprog,sigma,h_reg,prf.mk_hw_register_env
696(opt_safe … prf) (other_bit … h_reg).
697
698definition well_formed_regs :
699∀prog : ertl_program. ∀ sigma : (sigma_map prog).
700ertl_psd_env×hw_register_env → Prop ≝
701λprog,sigma,regs. let 〈x,y〉 ≝ regs in
702well_formed_ertl_psd_env prog sigma x ∧ well_formed_hw_register_env prog sigma y.
703
704definition sigma_regs :
705∀prog : ertl_program. ∀sigma : (sigma_map prog).
706∀regs: ertl_psd_env×hw_register_env.well_formed_regs prog sigma regs →
707ertl_psd_env×hw_register_env ≝
708λprog,sigma,regs.let 〈x,y〉≝ regs in
709λprf : well_formed_regs prog sigma 〈x,y〉.
710      〈sigma_ertl_psd_env prog sigma x (proj1 … prf),
711       sigma_hw_register_env prog sigma y (proj2 … prf)〉.
712
713lemma sigma_empty_regsT_commute :
714∀prog : ertl_program. ∀sigma : (sigma_map prog).
715∀ptr.∃ prf.
716  empty_regsT ERTLptr_semantics ptr =
717  sigma_regs prog sigma (empty_regsT ERTL_semantics ptr) prf.
718#prog #sigma #ptr %
719[ @hide_prf whd in match well_formed_regs; normalize nodelta %
720 [whd in match well_formed_ertl_psd_env; normalize nodelta #id #bv
721  normalize in ⊢ (%→?); #EQ destruct
722 | normalize % #EQ destruct
723 ]
724| % ]
725qed.
726
727axiom sigma_load_sp_commute :
728∀prog : ertl_program.∀sigma : (sigma_map prog).
729∀regs,ptr.
730load_sp ERTL_semantics regs = return ptr
731→ ∃prf.
732load_sp ERTLptr_semantics (sigma_regs prog sigma regs prf) = return ptr.
733
734axiom sigma_save_sp_commute :
735∀prog : ertl_program. ∀sigma : (sigma_map prog).
736∀reg,ptr,prf1. ∃prf2.
737save_sp ERTLptr_semantics (sigma_regs prog sigma reg prf1) ptr =
738sigma_regs prog sigma (save_sp ERTL_semantics reg ptr) prf2.
739
740definition well_formed_state :
741∀prog : ertl_program. ∀sigma : sigma_map prog.
742state ERTL_semantics → Prop ≝
743λprog,sigma,st.
744well_formed_frames prog sigma (st_frms … st) ∧
745sigma_is_opt prog sigma (istack … st) ≠ None ? ∧
746well_formed_regs prog sigma (regs … st) ∧
747well_formed_mem prog sigma (m … st).
748
749definition sigma_state :
750 ∀prog : ertl_program.
751 ∀sigma : sigma_map prog.
752 ∀st : state ERTL_semantics.
753 well_formed_state prog sigma st →
754 state ERTLptr_semantics ≝
755λprog,sigma,st,prf.
756mk_state …
757  (sigma_frames prog sigma (st_frms … st) ?)
758  (sigma_is prog sigma (istack … st) ?)
759  (carry … st)
760  (sigma_regs prog sigma (regs … st) ?)
761  (sigma_mem prog sigma (m … st) ?).
762@hide_prf cases prf ** //
763qed.
764
765definition well_formed_state_pc :
766∀prog : ertl_program .∀ sigma : sigma_map prog.
767  state_pc ERTL_semantics → Prop ≝
768 λprog,sigma,st.
769 well_formed_pc prog sigma (last_pop … st) ∧
770 well_formed_state prog sigma st.
771
772definition sigma_state_pc :
773∀prog : ertl_program. ∀sigma : sigma_map prog.
774∀ st : state_pc ERTL_semantics. well_formed_state_pc prog sigma st →
775state_pc ERTLptr_semantics ≝
776λprog,sigma,st,prf.
777mk_state_pc ? (sigma_state … (proj2 … prf)) (pc … st)
778              (sigma_pc … (proj1 … prf)).
779
780lemma reg_store_sigma_commute :
781∀ prog : ertl_program. ∀sigma : (sigma_map prog).
782∀id. preserving2 … res_preserve …
783       (sigma_beval prog sigma)
784       (sigma_register_env prog sigma)
785       (sigma_register_env prog sigma)
786       (reg_store id)
787       (reg_store id).
788#prog #sigma * #id #bv * #psd_env1 #prf1 #prf2 #psd_env2
789whd in match reg_store; whd in match update; normalize nodelta
790#psd_env2_spec
791% [ @hide_prf whd in psd_env2_spec : (??%%);
792    inversion (update beval ???) in psd_env2_spec; normalize nodelta
793    [#_ #ABS destruct] #pos_map #pos_map_spec #EQ destruct
794    * #id' #bv' cases (decidable_eq_pos id id')
795    [ #EQ <EQ normalize in ⊢ (??%? → ?);
796      >(update_lookup_opt_same ????? pos_map_spec)
797      #EQ1 destruct(EQ1) assumption
798    | #inEQ normalize in ⊢ (??%? → ?);
799      <(update_lookup_opt_other ????? pos_map_spec id' inEQ)
800      @(prf2 (an_identifier ? id') bv')
801    ]
802  | whd in match sigma_register_env; normalize nodelta
803    cases(map_update_commute ??????? psd_env2_spec ???)
804    [ #id_present #EQ <EQ % | | | |]
805    //
806  ]
807qed.
808
809lemma ps_reg_store_commute :
810∀prog : ertl_program. ∀sigma : sigma_map prog.
811∀id. preserving2 ?? res_preserve …
812      (sigma_beval prog sigma)
813      (sigma_regs prog sigma)
814      (sigma_regs prog sigma)
815      (ps_reg_store id)
816      (ps_reg_store id).
817#prog #sigma #id #bv * #psd1 #hw1 #prf1 #prf2
818whd in match ps_reg_store; normalize nodelta
819@mfr_bind [3: @(reg_store_sigma_commute prog sigma id bv ? ? ?) |*:]
820#m #wf_m @mfr_return % [assumption] cases prf2 #_ #H @H
821qed.
822
823lemma ps_reg_retrieve_commute :
824∀prog : ertl_program .∀sigma : sigma_map prog.
825∀r. preserving … res_preserve …
826         (sigma_regs prog sigma)
827         (sigma_beval prog sigma)
828         (λregs.ps_reg_retrieve regs r) 
829         (λregs.ps_reg_retrieve regs r).
830#prog #sigma #r ** #psd_regs #spilled #hw_regs #prf
831whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
832@opt_to_res_preserve #bv #H lapply((proj1 … prf))
833whd in match well_formed_ertl_psd_env; normalize nodelta #H1
834%{(H1 … H)} >(lookup_map … H) %
835qed.
836
837lemma ps_arg_retrieve_commute :
838∀prog : ertl_program. ∀sigma : sigma_map prog.
839∀arg. preserving … res_preserve …
840              (sigma_regs prog sigma)
841              (sigma_beval prog sigma)
842              (λregs.ps_arg_retrieve regs arg)
843              (λregs.ps_arg_retrieve regs arg).
844#prog #ismga * [#r | #b] whd in match ps_arg_retrieve;
845normalize nodelta [@ps_reg_retrieve_commute]
846#regs #wf_regs @mfr_return normalize % #EQ destruct
847qed.
848
849lemma hw_reg_retrieve_commute :
850∀prog: ertl_program. ∀sigma : sigma_map prog.
851∀r. preserving … res_preserve …
852         (sigma_regs prog sigma)
853         (sigma_beval prog sigma)
854         (λregs.hw_reg_retrieve regs r)
855         (λregs.hw_reg_retrieve regs r).
856cases daemon
857qed. (*help for bit_vector_trie*)
858
859check hw_reg_store
860
861lemma hw_reg_store_commute :
862∀prog : ertl_program. ∀sigma : sigma_map prog.
863∀r. preserving2 … res_preserve …
864         (sigma_beval prog sigma)
865         (sigma_regs prog sigma)
866         (sigma_regs prog sigma)
867         (hw_reg_store r)
868         (hw_reg_store r).
869cases daemon
870qed.
871
872
873lemma ertl_eval_move_commute :
874∀prog : ertl_program.∀sigma : sigma_map prog.
875∀move. preserving … res_preserve …
876         (sigma_regs prog sigma)
877         (sigma_regs prog sigma)
878         (λregs.ertl_eval_move regs move)
879         (λregs.ertl_eval_move regs move).
880#prog #sigma * #mv_dst #arg_mv #regs #wf_regs
881whd in match ertl_eval_move; normalize nodelta
882@mfr_bind
883  [2: #bv @sigma_beval assumption |
884  |   cases arg_mv [#mv_dst1 | #b] normalize nodelta
885    [ cases mv_dst1 [#r | #b] normalize nodelta
886      [@ps_reg_retrieve_commute | @hw_reg_retrieve_commute]
887    | @mfr_return normalize % #EQ destruct
888    ]
889  | #bv #prf cases mv_dst [#r | #r] normalize nodelta
890    [@ps_reg_store_commute | @hw_reg_store_commute ]
891  ]
892qed.
893
894
895
896
897       
898definition ERTLptrStatusSimulation :
899∀ prog : ertl_program.
900let trans_prog ≝ ertl_to_ertlptr prog in
901∀stack_sizes.
902sigma_map prog →
903status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝
904λprog,stack_sizes,sigma.mk_status_rel …
905    (* sem_rel ≝ *) (λ
Note: See TracBrowser for help on using the repository browser.