source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2666

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

bug fixed in blocks.ma

File size: 133.8 KB
Line 
1
2(**************************************************************************)
3(*       ___                                                              *)
4(*      ||M||                                                             *)
5(*      ||A||       A project by Andrea Asperti                           *)
6(*      ||T||                                                             *)
7(*      ||I||       Developers:                                           *)
8(*      ||T||         The HELM team.                                      *)
9(*      ||A||         http://helm.cs.unibo.it                             *)
10(*      \   /                                                             *)
11(*       \ /        This file is distributed under the terms of the       *)
12(*        v         GNU General Public License Version 2                  *)
13(*                                                                        *)
14(**************************************************************************)
15
16include "ERTLptr/ERTLtoERTLptr.ma".
17include "common/StatusSimulation.ma".   
18include "joint/Traces.ma".
19include "ERTLptr/ERTLptr_semantics.ma".
20include "common/ExtraMonads.ma".
21
22definition ERTL_status ≝
23λprog : ertl_program.λstack_sizes.
24joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
25
26definition ERTLptr_status ≝
27λprog : ertlptr_program.λstack_sizes.
28joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
29
30definition sigma_map ≝ λ prog : ertl_program.
31joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.
32
33
34definition sigma_pc_opt :
35∀ prog : ertl_program.
36sigma_map prog → program_counter → option program_counter ≝
37λprog,sigma,pc.
38  let ge ≝ globalenv_noinit … prog in
39  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
40    return pc
41  else
42    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
43    ! ertl_ptr_point ← sigma fd (point_of_pc ERTL_semantics pc) ;
44    return pc_of_point
45    ERTLptr_semantics (pc_block pc) ertl_ptr_point.
46
47definition sigma_stored_pc ≝
48λprog,sigma,pc. match sigma_pc_opt prog sigma pc with
49      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
50     
51     
52definition sigma_beval :
53 ∀prog : ertl_program.
54  sigma_map prog →
55  beval → beval ≝
56λprog,sigma,bv.
57match bv with
58[ BVpc pc prt ⇒ match sigma_pc_opt prog sigma pc with
59                 [None ⇒ BVundef | Some x ⇒ BVpc x prt]
60| _ ⇒ bv
61].
62
63(*
64definition sigma_beval :
65 ∀prog,sigma,bv.
66 sigma_beval_opt prog sigma bv ≠ None ? → beval ≝
67 λprog,sigma,bv.opt_safe ….
68*)
69definition sigma_is :
70 ∀prog : ertl_program.
71  sigma_map prog →
72  internal_stack → internal_stack ≝
73λprog,sigma,is.
74match is with
75[ empty_is ⇒ empty_is
76| one_is bv ⇒ one_is (sigma_beval prog sigma bv)
77| both_is bv1 bv2 ⇒
78  both_is (sigma_beval prog sigma bv1) (sigma_beval prog sigma bv2)
79].
80
81lemma sigma_is_empty : ∀prog,sigma.
82  sigma_is prog sigma empty_is = empty_is.
83#prog #sigma %
84qed.
85
86definition sigma_mem :
87 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝
88 λprog,sigma,m.
89 mk_mem
90  (λb.
91    If Zltb (block_id b) (nextblock m) then with prf' do   
92      let l ≝ low_bound m b in
93      let h ≝ high_bound m b in
94      mk_block_contents l h
95      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
96        sigma_beval prog sigma (contents (blocks m b) z)
97      else BVundef)
98    else empty_block OZ OZ)
99  (nextblock m)
100  (nextblock_pos m).
101
102(*DOPPIONE ASSIOMA IN LINEARISE_PROOF.MA *)
103axiom mem_ext_eq :
104  ∀m1,m2 : mem.
105  (∀b.let bc1 ≝ blocks m1 b in
106      let bc2 ≝ blocks m2 b in
107      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
108      ∀z.contents bc1 z = contents bc2 z) →
109  nextblock m1 = nextblock m2 → m1 = m2.
110
111
112
113inductive id_is_in (A : Type[0]) : Pos →  positive_map A → Prop ≝
114| is_in_root : ∀l,r,opt_a. id_is_in A (one) (pm_node … opt_a l r)
115| is_in_left : ∀l,r,opt_a,x. id_is_in A x l →
116                                    id_is_in A (p0 x) (pm_node … opt_a l r)
117| is_in_right : ∀l,r,opt_a,x. id_is_in A x r →
118                                    id_is_in A (p1 x) (pm_node … opt_a l r).
119
120definition id_is_in : ∀A : Type[0]. ∀tag : identifierTag.
121identifier_map tag A → identifier tag → Prop ≝
122λA,tag,m,id.match id with
123     [an_identifier x ⇒ match m with
124                              [an_id_map p ⇒ id_is_in A x p]
125     ].
126     
127lemma lookup_eq : ∀ A : Type[0].
128∀m,m' : positive_map A.
129(∀id. lookup_opt A id m = lookup_opt A id m'
130      ∧ (id_is_in A id m ↔ id_is_in A id m')) → m=m'.
131#A #m elim m
132[ * [#_ %] #opt_a #l #r #H lapply(H one) normalize * #EQ >EQ * #_ #H1 lapply(H1 ?) [%]
133  -H1 -H <EQ -EQ #H inversion H #l1 #r1 #opt_a1
134  [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
135  |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
136  ]
137| #opt_a #l #r #Hl #Hr *
138  [ #H lapply(H one) normalize * #EQ >EQ * #H1 #_ lapply(H1 ?) [%]
139  -H1 -H -EQ #H inversion H #l1 #r1 #opt_a1
140    [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
141    |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
142    ]
143  | #opt_a1 #l1 #r1 #H lapply(H one) normalize * #EQ >EQ -EQ #_ @eq_f2 [@Hl|@Hr]
144    #id [ lapply(H (p0 id)) | lapply(H (p1 id))] normalize * #H1 * #H2 #H3 %
145    [1,3: assumption] % #H4 [1,3: lapply(H2 ?) |*: lapply(H3 ?)]
146    try %2 try %3 try assumption #H5 inversion H5 #l2 #r2 #opt_a2
147    [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
148               [1,3: cut(p0 id ≠ one) [1,3: @(pos_elim … id) /3/]
149               |*:   cut(p1 id ≠ one) [1,3: @(pos_elim … id) /3/]
150               ] * #H @H assumption
151    |*: #pos #H6 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
152        #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) #_ assumption
153    ]
154  ]
155]
156qed.
157
158include alias "common/Identifiers.ma".
159include alias "common/PositiveMap.ma".
160
161
162lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
163#x /3/
164qed.
165
166lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
167#x /3/
168qed.
169
170lemma lookup_ok_to_update : ∀ A : Type[0].
171∀ tag : identifierTag.
172∀m,m' : identifier_map tag A. ∀id,a.
173(lookup tag A m' id = Some ? a)  → lookup tag A m id ≠ None ? →
174(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
175     (id_is_in A tag m id' ↔ id_is_in A tag m' id')) →
176update tag A m id a = return m'.
177#A #tag * #m * #m' * #id #a
178normalize in ⊢ (%→%→?); lapply id -id lapply m' -m' elim m
179    [ #m' #id #m_spec' normalize in ⊢ (% → ?); * #EQ @⊥ @EQ %] #opt_a #l #r #Hl #Hr
180    #m' * [|*: #x] normalize in ⊢ (%→%→?); #m_spec'
181    [ cases opt_a -opt_a [* #H @⊥ @H %] #a1 #_ #H normalize @eq_f @eq_f
182      lapply H -H lapply m_spec'; -m_spec' lapply a -a cases m'
183      [#a normalize #EQ destruct] #opt_a1 #l1 #r1 #a
184      normalize in ⊢ (%→?); #EQ >EQ #H @eq_f2 @lookup_eq #id'
185      [ lapply (H (an_identifier tag (p0 id')) ?)
186      | lapply (H (an_identifier tag (p1 id')) ?)
187      ]
188      [1,3:% @(pos_elim … id') [1,3:#H destruct|*: #n #IP #H destruct]]
189      * normalize #H1 * #H2 #H3 % [1,3: >H1 %] % #H4
190      [1,3: lapply(H2 ?) |*: lapply(H3 ?)] try %2 try %3 try assumption
191      #H5 inversion H5 #l2 #r2 #opt_a2
192        [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
193                   [1,3: cut(p0 id' ≠ one) [1,3: /3/]
194                   |*: cut(p1 id' ≠ one) [1,3: /3/]
195                   ] >EQ * #H @H %
196        |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
197            #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) #_ assumption
198        ]
199    |*: #H lapply m_spec' -m_spec' cases m' -m' [1,3: normalize #EQ destruct]
200        #opt_a1 #l1 #r1 normalize in ⊢ (% → ?); #H1 #H2
201        [ lapply(Hr ?? H1 H ?) | lapply(Hl ?? H1 H ?)]
202          [1,3: * #y * #y_spec
203            [lapply(H2 (an_identifier tag (p1 y)) ?) | lapply(H2 (an_identifier tag (p0 y)) ?)]
204            [1,3: % #EQ destruct @y_spec %] * normalize #H3 * #H4 #H5 % // % #H6
205            [1,3: lapply(H4 ?) |*: lapply (H5 ?)] try %2 try %3 try assumption
206            #H7 inversion H7 #l2 #r2 #opt_a2
207              [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
208                   [1,3: cut(p1 y ≠ one) [1,3: /3/]
209                   |*: cut(p0 y ≠ one) [1,3: /3/]
210                   ] >EQ * #H @H %
211              |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
212                 destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
213                 destruct(EQ1) #_ assumption
214              ]
215          |2,4: normalize cases(update A x a ?) normalize [2,4: #pos_map]
216               #EQ destruct @eq_f @eq_f lapply(H2 (an_identifier tag one) ?)
217               [1,3: % #EQ destruct] * normalize #EQ >EQ #_ @eq_f2 [2,3: %]
218               @lookup_eq #id'
219               [lapply (H2 (an_identifier tag (p0 id')) ?) |
220                                   lapply (H2 (an_identifier tag (p1 id')) ?) ]
221               [1,3: % #EQ1 destruct] * normalize #H3 * #H4 #H5 % // % #H6
222               [1,3: lapply(H4 ?) |*: lapply(H5 ?)] try %2 try %3 try assumption
223               #H7 inversion H7 #l2 #r2 #opt_a2
224                  [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
225                    [1,3: cut(p0 id' ≠ one) [1,3: /3/]
226                    |*: cut(p1 id' ≠ one) [1,3: /3/]
227                   ] >EQ * #H @H %
228                  |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
229                      destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
230                      destruct(EQ1) #_ assumption
231                  ]
232            ]
233      ]
234qed.
235
236lemma update_ok_to_lookup : ∀ A : Type[0].
237∀ tag : identifierTag.
238∀m,m' : identifier_map tag A. ∀id,a.
239update tag A m id a = return m' →
240(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
241(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
242     (id_is_in A tag m id' ↔ id_is_in A tag m' id')).
243#A #tag * #m * #m' * #id #a
244whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
245    #m1 #m1_spec #EQ destruct % [%]
246    [  normalize @(update_lookup_opt_same … m1_spec)
247    |3: * #id' * #id_spec' normalize %
248        [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %]
249        lapply id_spec' lapply m1_spec -id_spec' -m1_spec
250        (*cases id [|*:#x] -id normalize*) lapply m' -m' lapply id lapply id' -id -id'
251        elim m [#id' #id #m' cases id [|*: #x] normalize #EQ destruct]
252        #opt_a #l #r #Hl #Hr #id' #id #m' cases id [|*:#x] -id normalize
253        [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %]
254          #x #_ normalize % #H [1,2: %3 |*: %2]
255          inversion H #l1 #r1 #opt_a1
256          [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥
257                     [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/]
258                     |*:   cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/]
259                     ]
260                     * #H @H >EQ1 //   
261          |*:        #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
262                     #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption
263          ]
264        |*: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map
265            #pos_map_spec #EQ destruct #id_spec' % #H
266            inversion H #l1 #l2 #opt_a1
267            [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
268                       #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
269                       #H1 %
270            |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
271                #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
272                #H2 try %2 try %3 try assumption
273                [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
274                | @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
275                | @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
276                | @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
277                ]
278                assumption
279            ]
280         ]     
281    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
282      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
283      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
284      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
285      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
286    ]
287qed.
288
289
290(*
291               
292lemma update_lookup_after : ∀ A : Type[0].
293∀ tag : identifierTag.
294∀m,m' : identifier_map tag A. ∀id,a.
295update tag A m id a = return m' →
296lookup tag A m' id = Some ? a.
297#A #B #tag * #m1 * #id #a whd in ⊢ (??%% → ?); inversion(update A ???)
298normalize nodelta [#_ #EQ destruct] #pos_map #pos_map_spec #EQ destruct
299@(update_lookup_opt_same … pos_map_spec)
300qed.
301
302lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
303#x /3/
304qed.
305
306lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
307#x /3/
308qed.
309
310lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : identifierTag.
311∀m : identifier_map tag A.
312∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
313∀id. id_is_in A tag m id ↔ id_is_in B tag (map_inf1 A B tag m F) id.
314#A #B #tag * #m elim m
315[ #F * #id % normalize #H inversion H #l #r #opt_a
316  [1,4: #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
317  |*: #pos #H1 #_ #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
318  ]
319| * [2:#a] #l #r #Hl #Hr #F ** [1,4: |*:#x] normalize % #H try % try %2 try %3
320  [1,2,5,6: cases(Hr ? (an_identifier tag x)) |*: cases (Hl ? (an_identifier tag x))]
321  [2,4,6,8,10,12,14,16: #a1 ** #id1 #prf1 @F try(@a1)
322                        try(%{(an_identifier tag (p1 id1))} assumption)
323                        try(%{(an_identifier tag (p0 id1))} assumption) ]
324  try(#H1 #_ @H1) try(#_ #H1 @H1) -H1 -Hl -Hr inversion H #l1 #r1 #opt_a1
325  [1,4,7,10,13,16,19,22: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
326             [1,2,3,4: lapply(p1_neq_one x)
327             |*:       lapply(p0_neq_one x)
328             ] * #H @H >EQ %
329  |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
330      #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct #_ assumption
331  ]
332]
333qed.
334
335lemma map_update_commute : ∀ A, B : Type[0].
336∀tag : identifierTag.
337∀m1,m2 : identifier_map tag A.
338∀id,a.
339update tag A m1 id a = return m2 →
340∀ F : (∀a:A.(Σid. lookup tag A m1 id = Some A a) → B).
341∀ F': (∀a:A.(Σid. lookup tag A m2 id = Some A a) → B). 
342(∀a',id',prf,prf'. F a' «id',prf» = F' a' «id',prf'») → ∃prf.
343update tag B (map_inf1 A B tag m1 F) id (F' a «id,prf») =
344return map_inf1 A B tag m2 F'.
345#A #B #tag #m1 #m2 #id #a #m2_spec #F #F' #eqFF' %
346[ @hide_prf cases(update_lookup_previous A tag m1 m2 id a) #H1 #_ cases (H1 m2_spec)
347  * #H1 #H2 #H3 assumption
348| cases(update_lookup_previous B tag (map_inf1 A B tag m1 F)
349                             (map_inf1 A B tag m2 F') id (F' a «id,?»))
350  [ #_ #H @H |] cases(update_lookup_previous A tag m1 m2 id a) #H2 #INUTILE
351cases(H2 m2_spec) * #H3 #H4 #H5 % [%]
352[ >(lookup_map … H3) %
353| elim H4 -H4 #H4 % #H5 @H4 lapply H5 cases m1 in F; -m1 #m1 cases id -id
354  elim m1 [ #id #F normalize * %] #a1 #l #r #Hl #Hr * [|*:#x] #F normalize
355  [ cases a1 in F; [2: #a2] #F normalize [2: * %] #EQ destruct
356  |*: #H
357    [@(Hr x ??) | @(Hl x ??)]
358    [1,3:#a ** #id1 #prf1 @F [1,3: @a]
359         [%{(an_identifier tag (p1 id1))}|%{(an_identifier tag (p0 id1))}]
360         normalize assumption
361    |*: normalize @H
362    ]
363  ]
364| #id' #id_spec' lapply(H5 id' id_spec') * #H6 * #H7 #H8 %
365  [ lapply H6 inversion (lookup tag A m2 id')
366    [2: #w] #w_spec #EQ >(lookup_map … EQ) normalize nodelta
367    >(lookup_map … w_spec) normalize nodelta [2: %] @eq_f @eqFF'
368  | cases(id_is_in_map A B tag m1 F id') cases(id_is_in_map A B tag m2 F' id')
369   #H9 #H10 #H11 #H12 % #H13 [ @H9 @H7 @H12 assumption | @H11 @H8 @H10 assumption]
370  ]
371]
372qed.
373
374(*
375definition well_formed_register_env :
376∀prog : ertl_program .∀sigma : (sigma_map prog).
377register_env beval → Prop ≝
378λprog,sigma,psd_reg.∀id,bv. lookup ?? psd_reg id = Some ? bv →
379sigma_beval_opt prog sigma bv ≠ None ?.
380*)
381*)
382
383definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
384λtag,A,B,m,f.match m with
385[an_id_map p ⇒ an_id_map … (map ?? f p)].
386
387lemma lookup_map : ∀A,B : Type[0].
388  ∀tag : identifierTag.
389  ∀m : identifier_map tag A.
390  ∀ f:A → B.
391  ∀ id.
392lookup tag B (map tag A B m f) id =
393! a ← lookup tag A m id; return f a.
394#A #B #tag * #m #f * #id normalize >lookup_opt_map %
395qed.
396
397lemma update_leaf_fail: ∀tag,A,i,v.
398 update tag A (empty_map ??) i v = Error ? [MSG MissingId; CTX … i].
399#ta #A ** [|*: #x] #v normalize %
400qed.
401
402lemma update_def : ∀tag,A,m,i,v.
403  update tag A m i v =
404  match lookup tag A m i with
405  [ Some _ ⇒ OK ? (add tag A m i v)
406  | None ⇒ Error ? [MSG MissingId; CTX … i]
407  ].
408#tag #A #m #i #v inversion(update tag A m i v)
409[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
410 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
411 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i
412 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
413 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
414 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
415 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
416 [3: cases opt_a normalize [2: #y] #EQ destruct %
417 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
418     [<(Hr … EQm'') | <(Hl … EQm'')] %
419 ]
420| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m']
421  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
422  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
423 [3: cases opt_a [2:#w] normalize #EQ destruct %
424 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
425     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a]
426     normalize #EQ destruct %
427 ]
428]
429qed.
430
431lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
432map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
433#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
434[ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?)
435  normalize // cases x normalize [2,3,5,6: #y] #EQ destruct
436| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize cases opt_a normalize [2: #a %]
437  cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize
438  //] #v normalize cases opt_a [2,4: #a] normalize //
439  [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize
440    [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y]
441    normalize #EQ destruct
442  | >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb]
443    inversion (pm_set B x ? ?) normalize //
444    [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct]
445    #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r)
446    normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ %
447]
448qed.
449
450
451definition restrict : ∀tag.∀A,B.
452identifier_map tag A → identifier_map tag B → identifier_map tag A ≝
453λtag,A,B,m1,m2.an_id_map …
454           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
455                  (match m1 with [an_id_map p1 ⇒ p1])
456                  (match m2 with [an_id_map p2 ⇒ p2])).
457
458interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).
459
460unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
461 
462lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
463update tag B (map tag A B m f) id (f v) =
464!m' ← update tag A m id v; return map tag A B m' f.
465#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
466cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
467whd in ⊢ (???%); @eq_f @sym_eq @map_add
468qed.
469
470definition is_leaf ≝ λA.λpm : positive_map A.
471match pm with [ pm_leaf ⇒ true | _ ⇒ false ].
472(*
473let rec pm_clean A (pm : positive_map A) on pm : positive_map A ≝
474match pm with
475[ pm_leaf ⇒ pm_leaf ?
476| pm_node o l r ⇒
477  let l' ≝ pm_clean … l in
478  let r' ≝ pm_clean … r in
479  match o with
480  [ Some _ ⇒ pm_node … o l' r'
481  | None ⇒
482    if is_leaf … l' ∧ is_leaf … r' then pm_leaf ? else
483    pm_node … o l' r'
484  ]
485].
486 
487definition clean ≝ λtag,A.λm : identifier_map tag A.
488  match m with [ an_id_map pm ⇒ an_id_map tag A (pm_clean … pm) ].
489*)
490
491definition sigma_register_env :
492∀prog : ertl_program.∀sigma : (sigma_map prog).
493register_env beval → list register →  register_env beval ≝
494λprog,sigma,psd_env,ids.
495let m' ≝  map ??? psd_env (λbv.sigma_beval prog sigma bv) in
496m' ∖ ids.
497
498(*
499definition well_formed_ertl_psd_env :
500∀prog : ertl_program. ∀sigma : (sigma_map prog).
501ertl_psd_env → Prop≝
502λprog,sigma,psd_env.well_formed_register_env prog sigma (psd_regs psd_env).
503*)
504(*
505let rec well_formed_frames
506(prog : ertl_program) (sigma : (sigma_map prog))
507(l : list ertl_psd_env) on l : Prop ≝
508match l with
509  [nil ⇒ True
510  | cons a tl ⇒ well_formed_ertl_psd_env prog sigma a ∧
511               well_formed_frames prog sigma tl
512  ].                           
513*)
514
515
516lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
517∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
518#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
519[2: #b] normalize % qed.
520
521
522lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B.
523∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i.
524#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
525[2: #b] % qed.
526
527(*
528lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v.
529#tag #A * #m * #i #v normalize @eq_f
530lapply m -m
531elim i -i
532[ * [%]
533  * [2: #x] #l #r [%] normalize
534  cases (pm_clean A l) normalize // cases (pm_clean A r) //
535|*: #i #IH * normalize
536  [1,3: >IH cases i // ]
537  * [2,4: #x] #l #r normalize
538  [1,2: >IH % ]
539  >IH cases i cases (pm_clean A l) cases (pm_clean A r) normalize //
540]
541qed.
542
543lemma clean_lookup : ∀tag,A,m,i.lookup … (clean tag A m) i = lookup … m i.
544#tag #A * #m * #i normalize lapply i -i elim m
545[#i %] * [2: #a] #l #r #Hl #Hr * [2,3,5,6: #x] normalize in ⊢ (???%);
546[1,3:<Hr|2,4:<Hl] normalize try % [3: @if_elim #_ %]
547cases(pm_clean A l) in Hl; normalize
548[2: #opt_a1 #l1 #r1 #_ %
549|3: #H cases(pm_clean A r) normalize //
550| #H cases(pm_clean A r) in Hr; normalize //
551| #opt_a1 #l1 #r1 #H cases x normalize //
552]
553qed.   
554
555 
556lemma clean_update : ∀tag,A,m,i,v.
557! m' ← update tag A m i v; return clean … m' =
558update tag A (clean … m) i v.
559#tag #A #m #i #v
560>update_def >update_def >clean_lookup cases (lookup tag A m i)
561[ % ]
562#m' >m_return_bind normalize nodelta >clean_add %
563qed.
564*)
565lemma lookup_eq_id_map : ∀tag : identifierTag. ∀ A : Type[0].
566∀m,m' : identifier_map tag A.
567(∀id. lookup … m id = lookup … m' id
568      ∧ (id_is_in A tag m id ↔ id_is_in A tag m' id)) → m=m'.
569#tag #A * #m * #m' #H @eq_f @lookup_eq #id lapply(H (an_identifier tag id))
570* #H1 #H2 % // assumption
571qed.
572
573(*
574lemma clean_leaf : ∀tag : identifierTag . ∀ A : Type[0].
575∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) →
576clean ?? m = empty_map ??.
577#tag #A * #m elim m [#_ %] #opt_a #l #r #Hl #Hr #H normalize @eq_f
578lapply(H (an_identifier tag one)) normalize #EQ >EQ -EQ normalize
579lapply(Hl ?) [2: lapply(Hr ?)]
580  [1,3: * #id [lapply(H (an_identifier tag (p1 id))) | lapply(H (an_identifier tag (p0 id)))]
581       #H assumption
582  | normalize #EQ #EQ1 destruct >e0 >e1 normalize %
583  ]
584qed.
585*)
586lemma id_is_in_lookup : ∀tag,A,m,id,v.
587 lookup tag A m id = Some ? v → id_is_in A tag m id.
588#tag #A * #m * #id #a normalize lapply m -m elim id
589[|*: #x #IH] * normalize [1,3,5: #EQ destruct] #opt_a #l #r [ #_ %] #H [%3 |%2]
590@IH assumption
591qed.
592(*
593lemma pm_clean_leaf : ∀ A : Type[0].
594∀m : positive_map A. (∀ id. lookup_opt … id m = None ?) →
595pm_clean ? m = pm_leaf ….
596#A #m elim m [ #id %] #opt_a #l #r #Hl #Hr #H normalize lapply(H one) normalize
597#EQ >EQ normalize >Hl [normalize >Hr [ %]] #id [@(H (p1 id))|@(H (p0 id))]
598qed.
599
600
601lemma pm_clean_canonic : ∀A,m,n.(∀i.lookup_opt A i m = lookup_opt A i n) →
602  pm_clean ? m = pm_clean ? n.
603#A #m #n lapply m -m elim n
604[ @pm_clean_leaf ]
605* [2: #x] #l #r #IHl #IHr *
606  [1,3: #H @sym_eq @pm_clean_leaf #id @sym_eq @H ] #opt #l' #r' #H
607 lapply (H one) normalize in ⊢ (%→?); #EQ destruct
608 whd in ⊢ (??%%);
609 >(IHl l') [1,3: >(IHr r') [1,3 : % ]] #i
610 [1,2: @(H (p1 i)) |*: @(H (p0 i)) ] qed.
611
612
613lemma clean_canonic : ∀tag,A,m,n.(∀i.lookup tag A m i = lookup tag A n i) →
614  clean ?? m = clean ?? n.
615#tag #A * #m * #n #H normalize @eq_f @pm_clean_canonic #i
616lapply(H (an_identifier tag i))
617normalize //
618qed.
619*)
620lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 
621  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
622#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
623#EQ destruct % //
624qed.
625
626lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 
627  ∃m'.update tag A m i v = OK ? m'.
628#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
629normalize %|]
630qed.
631
632lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 
633  update … m i v = Error … [MSG MissingId; CTX … i].
634#tag #A #m #i #v #EQ >update_def >EQ normalize %
635qed.
636
637lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
638  i ∈ m.
639#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
640#EQ destruct >EQ normalize @I
641qed.
642
643lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
644  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
645#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
646normalize nodelta #EQ1 destruct @eq_identifier_elim
647[ #H normalize nodelta >H @lookup_add_hit
648| #H normalize nodelta @lookup_add_miss assumption
649]
650qed.
651
652lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
653∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
654#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
655[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
656qed.
657(*
658lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge
659*)
660(*
661lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B.
662∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b.
663#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) normalize [#_ *]
664#v1 #EQv1 * @eq_f lapply EQv1 lapply v1 lapply a lapply b -a -b -v1 elim i normalize
665[ * normalize [#b #v #EQ destruct] #opt_a #l #r *
666  [#v #EQ destruct normalize %] #opt_b #l1 #r1 #v #EQ destruct normalize cases opt_b
667  normalize [2: #x %] cases(merge A B A ? l1 l) normalize [2: #opt_a2 #l2 #r2 %]
668  cases(merge A B A ? r1 r) //
669|*: #x #IH * [2,4: #opt_b #l1 #r1] #p1 normalize [3,4: #i #EQ destruct] cases p1 -p1
670    [2,4: #opt_a #l2 #r2] normalize #v #H cases opt_b [2,4,6,8: #b] normalize
671    [1,2,5,6: <IH try assumption [1,2: cases opt_a [2,4: #a] normalize try %]
672     cases(merge A B A ? l2 l1) normalize // lapply H [1,4: cases r1 |*: cases l1]
673     normalize [1,3,5,7,9,11: #EQ destruct] #opt_b4 #l4 #r4 cases x normalize
674     [1,4,7,10,13,16: #EQ destruct normalize // cases(merge A B A ? ? ?) normalize //]
675     #x #H normalize cases(merge A B A ? ? ?) normalize //
676    |*: <IH try assumption
677       [1,3: cases(map_opt ? ? ? l1) normalize // lapply H cases r1 normalize
678            [1,3: #EQ destruct] #opt_b2 #l2 #r2 cases x [1,4: //] #x normalize //
679       |*: lapply H cases x normalize [2,3,5,6: #y] cases l1 normalize
680          [1,3,5,7,9,11: #EQ destruct] #opt_b2 #l2 #r2 #H //
681       ]
682   ]
683]
684qed.
685
686lemma update_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
687∀i,v.i ∈ b → update ?? (a ∩ b) i v =
688  ! a' ← update ?? a i v ; return a' ∩ b.
689#tag #A #B #a #b #id #v #H
690lapply (in_map_domain … b id) >H * #ignore #EQ_lookup_b
691(*<clean_update*)
692inversion (update tag A a id v)
693[2: #e #EQ cases (update_fail_lookup ?????? EQ) #EQ1 #EQ2 destruct
694  >lookup_miss_update [%]
695  >lookup_restrict >H assumption ]
696#m' #EQ >m_return_bind
697cases (lookup_hit_update ?? (a∩b) id v ?)
698[2: >mem_set_restrict >H >(update_ok_old_lookup ?????? EQ) % ]
699#m'' >update_def >update_def in EQ; >lookup_restrict >H normalize nodelta
700cases(lookup tag A a id) normalize nodelta [#ABS destruct] #v1 #EQ #EQ'' destruct
701whd in ⊢ (??%%); @eq_f @add_restrict assumption
702qed.
703*)
704lemma add_set_minus  : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
705∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b.
706#tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *]
707@if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *]
708#H * * * * @eq_f lapply H -H lapply v -v lapply b -b lapply a -a elim i
709[  *
710  [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %]
711  normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r)
712  normalize //
713  | * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct
714    normalize [3: % |1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //]
715    cases(map_opt ??? l) normalize // cases(map_opt ??? r) //
716  ]
717|2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v
718      normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%);
719      whd in match (merge ??????) in ⊢ (???%);
720      [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?);
721                whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize
722                [2,4,6,8: #b] [5,6: cases opt_a normalize //]
723                [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2]
724                          // cases (merge ???? r r1) normalize
725                          [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????)
726                          normalize // cases x
727                          [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
728                          normalize #EQ destruct
729                |*: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] //
730                    cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3]
731                    inversion(pm_set ????) normalize // cases x
732                    [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
733                    normalize #EQ destruct
734                ]
735     |*: whd in match (pm_set ????) in ⊢ (??%?);
736         whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]]
737         normalize
738         [1,2: @eq_f2 [1,4:%] | cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize
739         | cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize]       
740         [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v)
741         |2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v)
742         |*: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v)
743         ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %]
744           cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize
745           inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y]
746           normalize #EQ1 destruct
747     ]
748]
749qed.     
750
751lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
752∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v =
753  ! a' ← update ?? a i v ; return a' ∖ b.
754#tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim
755[ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def
756cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
757qed.
758
759
760record good_state_transformation
761(prog : ertl_program)
762(def_in : joint_closed_internal_function ERTL (prog_var_names ?? prog)) :
763Type[0] ≝
764{ f_lbls : label → option (list label)
765; f_regs : label → option (list register)
766; part_partition_f_lbls : partial_partition … f_lbls
767; part_partion_f_regs : partial_partition … f_regs
768; freshness_lab : let def_out ≝ translate_internal … def_in in
769     (∀l.opt_All … (All …
770    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
771           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
772; freshness_regs : let def_out ≝ translate_internal … def_in in
773  (∀l.opt_All … (All …
774    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
775           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
776; multi_fetch_ok : let def_out ≝ translate_internal … def_in in
777  let f_step ≝ translate_step ? in
778  let f_fin ≝  translate_fin_step ? in
779  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
780  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
781  match s with
782  [ sequential s' nxt ⇒
783    l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
784  | final s' ⇒
785    l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
786  | FCOND abs _ _ _ ⇒ Ⓧabs
787  ]
788}.
789
790definition get_internal_function_from_ident :
791∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
792ident → option (joint_closed_internal_function p globals) ≝
793λp,globals,ge,id.
794! bl  ← (find_symbol (joint_function p globals) ge id);
795! bl' ← (code_block_of_block bl);
796! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
797return fn.
798
799definition get_sigma_from_good_state :
800∀prog : ertl_program.
801(∀ fn : joint_closed_internal_function ERTL (prog_var_names ?? prog).
802good_state_transformation prog fn) → sigma_map prog ≝
803λprog,good,fn,searched.
804!〈res,s〉 ← find ?? (joint_if_code … fn)
805                (λlbl.λ_. match (f_lbls … (good fn)) lbl with
806                          [None ⇒ false
807                          |Some lbls ⇒
808                             match lbls with
809                                [nil ⇒ eq_identifier … searched lbl
810                                |cons hd tl ⇒ let last ≝ last_ne … «hd::tl,I» in
811                                          eq_identifier … searched last
812                                ]
813                          ]);
814return res.
815
816
817definition sigma_frames : ∀prog : ertl_program.
818(∀fn.good_state_transformation prog fn) →
819list (register_env beval × ident) → (list (register_env beval × ident)) ≝
820λprog,good,frms.
821let sigma ≝ get_sigma_from_good_state … good in
822foldr ??
823(λx,tl.let 〈reg_env,id〉 ≝ x in
824       match get_internal_function_from_ident
825                  ERTL_semantics (prog_var_names … prog)
826                  (globalenv_noinit … prog) id with
827       [Some fn ⇒
828  〈(sigma_register_env prog sigma reg_env
829       (added_registers … fn (f_regs … (good fn)))),id〉 :: tl
830       |None ⇒ [ ]
831       ]) ([ ]) frms.
832
833
834(*
835lemma sigma_empty_frames_commute :
836∀prog : ertl_program. ∀ sigma : (sigma_map prog).
837∃prf.
838sigma_frames prog sigma [] prf = [].
839#p #s % normalize %
840qed.
841
842
843let rec sigma_bit_vector_trie_opt (prog : ertl_program)
844(sigma : (sigma_map prog)) (n : nat) (t : BitVectorTrie beval n)
845on t : option … (BitVectorTrie beval n) ≝
846match t with
847  [Leaf bv ⇒ ! bv' ← (sigma_beval_opt prog sigma bv);
848                   return Leaf … bv'
849  |Node n1 b1 b2 ⇒ ! b1' ← (sigma_bit_vector_trie_opt prog sigma n1 b1);
850                   ! b2' ← (sigma_bit_vector_trie_opt prog sigma n1 b2);
851                   return Node … n1 b1' b2'
852  |Stub n1 ⇒  return Stub … n1
853  ].
854
855
856definition well_formed_hw_register_env :
857∀ prog : ertl_program. ∀ sigma : (sigma_map prog).
858hw_register_env → Prop ≝
859λprog,sigma,regs.sigma_bit_vector_trie_opt prog sigma 6 (reg_env … regs) ≠ None ?.
860*)
861
862
863include "common/BitVectorTrieMap.ma".
864
865definition sigma_hw_register_env :
866∀prog: ertl_program. ∀sigma : (sigma_map prog).
867hw_register_env → hw_register_env ≝
868λprog,sigma,h_reg.mk_hw_register_env
869(map ? ? (sigma_beval prog sigma) 6 (reg_env … h_reg)) (other_bit … h_reg).
870
871
872definition sigma_regs :
873∀prog : ertl_program. ∀sigma : (sigma_map prog).
874(register_env beval)×hw_register_env→ list register →
875(register_env beval)×hw_register_env ≝
876λprog,sigma,regs,ids.let 〈x,y〉≝ regs in
877      〈sigma_register_env prog sigma x ids,
878       sigma_hw_register_env prog sigma y〉.
879(*
880lemma sigma_empty_regsT_commute :
881∀prog : ertl_program. ∀sigma : (sigma_map prog).
882∀ptr.∃ prf.
883  empty_regsT ERTLptr_semantics ptr =
884  sigma_regs prog sigma (empty_regsT ERTL_semantics ptr) prf.
885#prog #sigma #ptr %
886[ @hide_prf whd in match well_formed_regs; normalize nodelta %
887 [whd in match well_formed_ertl_psd_env; normalize nodelta #id #bv
888  normalize in ⊢ (%→?); #EQ destruct
889 | normalize % #EQ destruct
890 ]
891| % ]
892qed.
893
894axiom sigma_load_sp_commute :
895∀prog : ertl_program.∀sigma : (sigma_map prog).
896∀regs,ptr.
897load_sp ERTL_semantics regs = return ptr
898→ ∃prf.
899load_sp ERTLptr_semantics (sigma_regs prog sigma regs prf) = return ptr.
900
901axiom sigma_save_sp_commute :
902∀prog : ertl_program. ∀sigma : (sigma_map prog).
903∀reg,ptr,prf1. ∃prf2.
904save_sp ERTLptr_semantics (sigma_regs prog sigma reg prf1) ptr =
905sigma_regs prog sigma (save_sp ERTL_semantics reg ptr) prf2.
906
907definition well_formed_state :
908∀prog : ertl_program. ∀sigma : sigma_map prog.
909state ERTL_semantics → Prop ≝
910λprog,sigma,st.
911well_formed_frames prog sigma (st_frms … st) ∧
912sigma_is_opt prog sigma (istack … st) ≠ None ? ∧
913well_formed_regs prog sigma (regs … st) ∧
914well_formed_mem prog sigma (m … st).
915*)
916
917definition sigma_state : ∀prog : ertl_program.
918(∀fn.good_state_transformation prog fn) →
919 state ERTLptr_semantics → list register →
920 state ERTL_semantics ≝
921λprog,good,st,ids.
922let sigma ≝ get_sigma_from_good_state … good in
923mk_state ?
924  (sigma_frames prog good (st_frms ERTLptr_semantics st))
925  (sigma_is ? sigma (istack … st))
926  (carry … st)
927  (sigma_regs ? sigma (regs … st) ids)
928  (sigma_mem ? sigma (m … st)).
929
930
931definition dummy_state : state ERTL_semantics ≝
932mk_state ERTL_semantics
933   [ ] empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
934   
935definition dummy_state_pc : state_pc ERTL_semantics ≝
936mk_state_pc ? dummy_state (null_pc one) (null_pc one).
937
938definition sigma_state_pc :
939∀prog : ertl_program.
940(∀fn.good_state_transformation prog fn) →
941state_pc ERTLptr_semantics →
942 state_pc ERTL_semantics ≝
943λprog,good,st.
944  let sigma ≝ get_sigma_from_good_state … good in
945  let ge ≝ globalenv_noinit … prog in
946  if eqZb       (block_id (pc_block (pc … st))) (-1) then (* check for dummy pc *)
947    dummy_state_pc
948  else
949  match (fetch_internal_function (joint_closed_internal_function ERTL
950         (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with
951   [OK x ⇒ let 〈i,fd〉 ≝ x in
952      mk_state_pc ?
953       (sigma_state prog good st (added_registers … fd (f_regs … (good fd))))
954       (pc … st) (sigma_stored_pc prog sigma (last_pop … st))
955   |Error msg ⇒ dummy_state_pc].
956
957
958definition ERTLptrStatusSimulation :
959∀ prog : ertl_program.
960let trans_prog ≝ ertl_to_ertlptr prog in
961∀stack_sizes.(∀fn.good_state_transformation prog fn) →
962status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝
963λprog,stack_sizes,good.
964  let trans_prog ≝ ertl_to_ertlptr prog in
965    mk_status_rel ??
966    (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes
967       .λs2:ERTLptr_status trans_prog stack_sizes
968        .s1=sigma_state_pc prog good s2)
969    (* call_rel ≝ *) 
970          (λs1:Σs:ERTL_status prog stack_sizes
971               .as_classifier (ERTL_status prog stack_sizes) s cl_call
972       .λs2:Σs:ERTLptr_status trans_prog stack_sizes
973                .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call
974        .let sigma ≝ get_sigma_from_good_state … good in
975        pc (mk_prog_params ERTL_semantics prog stack_sizes) s1
976         =sigma_stored_pc prog sigma
977          (pc
978           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes)
979           s2))
980    (* sim_final ≝ *) ?.
981cases daemon
982qed.
983
984lemma fetch_function_no_minus_one :
985  ∀F,V,i,p,bl.
986  block_id (pi1 … bl) = -1 →
987  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
988    bl = Error … [MSG BadFunction].
989 #F#V#i#p ** #r #id #EQ1 destruct
990  whd in match fetch_function; normalize nodelta
991  >globalenv_no_minus_one
992  cases (symbol_for_block ???) normalize //
993qed.
994 
995lemma fetch_function_no_zero :
996 ∀F,V,i,p,bl.
997  block_id (pi1 … bl) = 0 →
998  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
999    bl = Error … [MSG BadFunction].
1000 #F#V#i#p ** #r #id #EQ1 destruct
1001  whd in match fetch_function; normalize nodelta
1002  >globalenv_no_zero
1003  cases (symbol_for_block ???) normalize //
1004qed.
1005
1006(*DOPPIONI dei LEMMI in LINEARISE_PROOF*)
1007lemma symbol_for_block_match:
1008    ∀M:matching.∀initV,initW.
1009     (∀v,w. match_var_entry M v w →
1010      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
1011    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
1012    ∀MATCH:match_program … M p p'.
1013    ∀b: block.
1014    symbol_for_block … (globalenv … initW p') b =
1015    symbol_for_block … (globalenv … initV p) b.
1016* #A #B #V #W #match_fn #match_var #initV #initW #H
1017#p #p' * #Mvars #Mfn #Mmain
1018#b
1019whd in match symbol_for_block; normalize nodelta
1020whd in match globalenv in ⊢ (???%); normalize nodelta
1021whd in match (globalenv_allocmem ????);
1022change with (add_globals ?????) in match (foldl ?????);
1023>(proj1 … (add_globals_match … initW … Mvars))
1024[ % |*:]
1025[ * #idr #v * #idr' #w #MVE %
1026  [ inversion MVE
1027    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
1028  | @(H … MVE)
1029  ]
1030| @(matching_fns_get_same_blocks … Mfn)
1031  #f #g @match_funct_entry_id
1032]
1033qed.
1034
1035lemma symbol_for_block_transf :
1036 ∀A,B,V,init.∀prog_in : program A V.
1037 ∀trans : ∀vars.A vars → B vars.
1038 let prog_out ≝ transform_program … prog_in trans in
1039 ∀bl.
1040 symbol_for_block … (globalenv … init prog_out) bl =
1041 symbol_for_block … (globalenv … init prog_in) bl.
1042#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
1043#v0 #w0 * //
1044qed.
1045
1046lemma fetch_function_transf :
1047 ∀A,B,V,init.∀prog_in : program A V.
1048 ∀trans : ∀vars.A vars → B vars.
1049 let prog_out ≝ transform_program … prog_in trans in
1050 ∀bl,i,f.
1051 fetch_function … (globalenv … init prog_in) bl =
1052  return 〈i, f〉
1053→ fetch_function … (globalenv … init prog_out) bl =
1054  return 〈i, trans … f〉.
1055#A #B #V #init #prog_in #trans #bl #i #f
1056 whd in match fetch_function; normalize nodelta
1057 #H lapply (opt_eq_from_res ???? H) -H
1058 #H @('bind_inversion H) -H #id #eq_symbol_for_block
1059 #H @('bind_inversion H) -H #fd #eq_find_funct
1060 whd in ⊢ (??%?→?); #EQ destruct(EQ)
1061 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
1062 >(find_funct_ptr_transf A B …  eq_find_funct) %
1063qed.
1064
1065
1066lemma fetch_internal_function_transf :
1067 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
1068 ∀trans : ∀vars.A vars → B vars.
1069 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
1070 ∀bl,i,f.
1071 fetch_internal_function … (globalenv_noinit … prog_in) bl =
1072  return 〈i, f〉
1073→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
1074  return 〈i, trans … f〉.
1075#A #B #prog #trans #bl #i #f
1076 whd in match fetch_internal_function; normalize nodelta
1077 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
1078 whd in ⊢ (??%%→?); #EQ destruct(EQ)
1079 >(fetch_function_transf … EQfetch) %
1080qed.
1081
1082(*
1083definition good_local_sigma :
1084  ∀globals.
1085  ∀g:codeT ERTLptr globals.
1086  (Σl.bool_to_Prop (code_has_label … g l)) →
1087  codeT ERTL globals →
1088  (label → option label) → Prop ≝
1089  λglobals,g,c,sigma.
1090    ∀l,l'.sigma l = Some ? l' →
1091      ∃s. stmt_at … g l = Some ? s ∧
1092          All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
1093          (match s with
1094           [ sequential s' nxt ⇒
1095             match s' with
1096             [ step_seq _ ⇒
1097               (stmt_at … c n = Some ? (sequential … s' it)) ∧
1098                  ((sigma nxt = Some ? (S n)) ∨
1099                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
1100             | COND a ltrue ⇒
1101               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
1102               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
1103             ]
1104           | final s' ⇒
1105             stmt_at … c n = Some ? (final … s')
1106           | FCOND abs _ _ _ ⇒ Ⓧabs
1107           ]).
1108 
1109*)
1110
1111lemma ps_reg_retrieve_ok :  ∀prog : ertl_program.
1112∀sigma : sigma_map prog. ∀r,restr.
1113preserving1 ?? res_preserve1 …
1114     (λregs.sigma_regs prog sigma regs restr)
1115     (sigma_beval prog sigma)
1116     (λregs.ps_reg_retrieve regs r)
1117     (λregs.ps_reg_retrieve regs r).
1118#prog #sigma #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve;
1119whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
1120whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
1121>lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
1122>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
1123#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
1124qed.
1125
1126lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
1127∀sigma : sigma_map prog. ∀r,restr.
1128preserving1 ?? res_preserve1 …
1129    (λregs.sigma_regs prog sigma regs restr)
1130    (sigma_beval prog sigma)
1131    (λregs.hw_reg_retrieve regs r)
1132    (λregs.hw_reg_retrieve regs r).
1133#prog #sigma #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
1134whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
1135whd in match sigma_hw_register_env; normalize nodelta
1136change with (sigma_beval prog sigma BVundef) in ⊢ (???????(??(?????%))?);
1137#bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct
1138%{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
1139% //
1140qed.
1141
1142
1143lemma ps_reg_store_ok : ∀prog : ertl_program.
1144∀sigma : sigma_map prog. ∀r,restr.
1145preserving21 ?? res_preserve1 …
1146   (sigma_beval prog sigma)
1147   (λregs.sigma_regs prog sigma regs restr)
1148   (λregs.sigma_regs prog sigma regs restr)
1149   (ps_reg_store r)
1150   (ps_reg_store r).
1151#prog #sigma #r #restr whd in match ps_reg_store; normalize nodelta
1152#bv * #psd_r #hw_r @mfr_bind1
1153[ @(λr.sigma_register_env prog sigma r restr)
1154| whd in match reg_store; whd in match sigma_regs; normalize nodelta
1155  #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
1156  lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
1157  normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
1158  #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
1159  #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
1160  whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
1161| #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
1162  whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
1163]
1164qed.
1165
1166
1167lemma hw_reg_store_ok : ∀prog : ertl_program.
1168∀sigma : sigma_map prog. ∀r,restr.
1169preserving21 ?? res_preserve1 …
1170   (sigma_beval prog sigma)
1171   (λregs.sigma_regs prog sigma regs restr)
1172   (λregs.sigma_regs prog sigma regs restr)
1173   (hw_reg_store r)
1174   (hw_reg_store r).
1175#prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
1176#bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs; normalize nodelta
1177whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r'
1178* #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % |]
1179qed.
1180
1181
1182lemma ertl_eval_move_ok : ∀prog : ertl_program.
1183∀sigma : sigma_map prog. ∀ restr,pm.
1184preserving1 ?? res_preserve1 …
1185     (λregs.sigma_regs prog sigma regs restr)
1186     (λregs.sigma_regs prog sigma regs restr)
1187     (λregs.ertl_eval_move regs pm)
1188     (λregs.ertl_eval_move regs pm).
1189#prog #sigma #restr * #mv_dst #arg_dst #pm whd in match ertl_eval_move;
1190normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
1191| cases arg_dst normalize nodelta
1192  [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
1193      @mfr_return1]
1194  * #r normalize nodelta [@ps_reg_retrieve_ok| @hw_reg_retrieve_ok]
1195| #bv cases mv_dst #r normalize nodelta [@ps_reg_store_ok | @hw_reg_store_ok]
1196]
1197qed.
1198
1199lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
1200∀sigma : sigma_map prog. ∀a,restr.
1201preserving1 ?? res_preserve1 …
1202    (λregs.sigma_regs prog sigma regs restr)
1203    (sigma_beval prog sigma)
1204    (λregs.ps_arg_retrieve regs a)
1205    (λregs.ps_arg_retrieve regs a).
1206#prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
1207normalize nodelta [#r | #b ] #regs
1208[ @ps_reg_retrieve_ok
1209| change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
1210  @mfr_return1
1211]
1212qed.
1213
1214lemma pop_ok :
1215∀prog : ertl_program.
1216∀good : (∀fn.good_state_transformation prog fn).
1217∀restr.
1218preserving1 ?? res_preserve1 ????
1219   (λst.sigma_state prog good st restr)
1220   (λx.let 〈bv,st〉 ≝ x in
1221      〈let sigma ≝ get_sigma_from_good_state … good in
1222       sigma_beval prog sigma bv,
1223       sigma_state prog good st restr〉)
1224   (pop ERTL_semantics)
1225   (pop ERTLptr_semantics).
1226#prog #good #restr whd in match pop; normalize nodelta #st @mfr_bind1
1227[@(λx.let 〈bv,is〉 ≝ x in
1228      let sigma ≝ get_sigma_from_good_state … good in
1229     〈sigma_beval prog sigma bv,
1230      sigma_is prog sigma is 〉)
1231| whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta
1232  cases(istack ? st) normalize nodelta
1233  [@res_preserve_error1
1234  |2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
1235        % [2,4: % [1,3: %|*: %] |*:]
1236  ]
1237| * #bv #is * #bv1 #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] %|]
1238]
1239qed.
1240
1241lemma push_ok :
1242∀prog : ertl_program.
1243∀good : (∀fn.good_state_transformation prog fn).
1244∀restr.
1245preserving21 ?? res_preserve1 …
1246     (λst.sigma_state prog good st restr)
1247     (let sigma ≝ get_sigma_from_good_state … good in sigma_beval prog sigma)
1248     (λst.sigma_state prog good st restr)
1249     (push ERTL_semantics)
1250     (push ERTLptr_semantics).
1251#prog #good #restr whd in match push; normalize nodelta #st #bv @mfr_bind1
1252[ @(let sigma ≝ get_sigma_from_good_state … good in sigma_is ? sigma)
1253| whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta
1254 cases (istack ? st) [2,3: #bv [2: #bv']]  whd in match sigma_is in ⊢ (???????%?);
1255 normalize nodelta [@res_preserve_error1] @mfr_return_eq1 %
1256| #is @mfr_return_eq1 %
1257]
1258qed.
1259
1260lemma be_opaccs_ok :
1261∀prog : ertl_program. ∀sigma : sigma_map prog.
1262∀ op.
1263preserving21 ?? res_preserve1 ??????
1264    (sigma_beval prog sigma)
1265    (sigma_beval prog sigma)
1266    (λx.let 〈bv1,bv2〉 ≝ x in
1267           〈sigma_beval prog sigma bv1,
1268            sigma_beval prog sigma bv2〉)
1269    (be_opaccs op)
1270    (be_opaccs op).
1271#prog #sigma #op #bv #bv1
1272whd in match be_opaccs; normalize nodelta @mfr_bind1
1273[ @(λx.x)
1274| cases bv
1275  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1276  whd in match Byte_of_val; normalize nodelta
1277  try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
1278  whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
1279  normalize nodelta [2: #pc] @res_preserve_error1
1280| #by @mfr_bind1
1281  [ @(λx.x)
1282  | cases bv1
1283    [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1284    whd in match Byte_of_val; normalize nodelta
1285    try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
1286    whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
1287    normalize nodelta [2: #pc] @res_preserve_error1
1288 | #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta
1289   whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
1290qed.
1291
1292lemma be_op1_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1293∀ op.
1294preserving1 ?? res_preserve1 …
1295     (sigma_beval prog sigma)
1296     (sigma_beval prog sigma)
1297     (be_op1 op)
1298     (be_op1 op).
1299#prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1
1300[ @(λx.x)
1301| cases bv
1302  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1303  whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta
1304  try @res_preserve_error1 [ @mfr_return_eq1 %]
1305  cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta
1306  @res_preserve_error1
1307| #by @mfr_return_eq1 %
1308]
1309qed.
1310
1311lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
1312res_preserve1 X Y F n (Error … e).
1313#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
1314qed.
1315
1316
1317lemma be_op2_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1318∀ b,op.
1319preserving21 ?? res_preserve1 …
1320     (sigma_beval prog sigma)
1321     (sigma_beval prog sigma)
1322     (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog sigma bv,b〉)
1323     (be_op2 b op)
1324     (be_op2 b op).
1325#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
1326cases bv
1327[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1328normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
1329normalize nodelta
1330cases bv1
1331[1,2,8,9,15,16,22,23,29,30,36,37:
1332|3,10,17,24,31,38: #ptr1' #ptr2' #p'
1333|4,11,18,25,32,39: #by'
1334|5,12,19,26,33,40: #p'
1335|6,13,20,27,34,41: #ptr' #p'
1336|7,14,21,28,35,42: #pc1' #p1'
1337]
1338normalize nodelta try @res_preserve_error1
1339[4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 %
1340   [2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 %
1341   |*:]
1342|*: cases op normalize nodelta
1343    try @res_preserve_error1 try( @mfr_return_eq1 %)
1344    [1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1
1345                         try( @mfr_return_eq1 %)
1346                         [ @if_elim #_ @mfr_return_eq1 %
1347                         | cases(ptype ptr) normalize nodelta
1348                           [2: @res_preserve_error1] @mfr_bind1
1349                           [ @(λx.x)
1350                           | whd in match Bit_of_val; normalize nodelta
1351                             cases b [#bo|| #bo #ptr'' #p'' #bit_v]
1352                             normalize nodelta [2,3: @res_preserve_error1]
1353                             @mfr_return_eq1 %
1354                           | #bi cases(op2 ?????) #by #bi1 normalize nodelta
1355                             @mfr_return_eq1 %
1356                           ]
1357                         | cases(ptype ptr) normalize nodelta @res_preserve_error1
1358                         ]
1359    |3,4,5,6,7,8: @mfr_bind1
1360        [1,4,7,10,13,16: @(λx.x)
1361        |2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta
1362                         cases b [1,4,7,10,13,16: #bo|
1363                                 |2,5,8,11,14,17:
1364                                 |3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v
1365                                 ] normalize nodelta try @res_preserve_error1
1366                                 @mfr_return_eq1 %
1367       |3,6,9,12,15,18: #bi cases(op2 ?????) #by #bi1 normalize nodelta
1368                        @mfr_return_eq1 %
1369       ]
1370    |*: whd in match be_add_sub_byte; normalize nodelta
1371        [1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1]
1372                cases p * [2,4,6: #p_no] #prf normalize nodelta
1373                [@res_preserve_error1
1374                |2,3: cases b [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
1375                      normalize nodelta [1,2,3,4: @res_preserve_error1]
1376                      @if_elim #_ [2,4: @res_preserve_error1]
1377                      @If_elim #INUTILE [2,4: @res_preserve_error1]
1378                      @pair_elim #a1 #a2 #_ normalize nodelta
1379                      @mfr_return_eq1 %
1380                |*: @mfr_bind1
1381                  [1,4,7: @(λx.x)
1382                  |2,5,8: whd in match Bit_of_val; normalize nodelta
1383                          [@mfr_return_eq1 %] cases b
1384                          [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
1385                          normalize nodelta [3,4,5,6: @res_preserve_error1]
1386                          @mfr_return_eq1 %
1387                  |3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1]
1388                          cases(op2 ?????) #a1 #a2 normalize nodelta
1389                          @mfr_return_eq1 %
1390                  ]
1391               ]
1392         |*: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1]
1393             cases p' * [2,4: #part_no] #prf normalize nodelta
1394             [ @res_preserve_error1
1395             | cases b [#bo|| #bo #ptr'' #p'' #bit_v]
1396               normalize nodelta [1,2: @res_preserve_error1] @if_elim #_
1397               [2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1]
1398               @pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 %
1399             |*: @mfr_bind1
1400                [1,4: @(λx.x)
1401                |2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %]
1402                      cases b [#bo|| #bo #ptr'' #p'' #bit_v] normalize nodelta
1403                      [2,3: @res_preserve_error1] @mfr_return_eq1 %
1404                |3,6: * normalize nodelta [1,3: @res_preserve_error1]   
1405                      cases(op2 ?????) #a1 #a2 normalize nodelta
1406                      @mfr_return_eq1 %
1407                ]
1408              ]
1409          ]
1410      ]
1411]
1412qed.
1413
1414lemma pointer_of_address_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1415preserving1 … res_preserve1 …
1416     (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1,
1417           sigma_beval prog sigma bv2〉)
1418     (λx.x)
1419     pointer_of_address pointer_of_address.
1420#prog #sigma * #bv1 #bv2 whd in match pointer_of_address;
1421whd in match pointer_of_bevals; normalize nodelta
1422cases bv1 normalize nodelta
1423[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1424try @res_preserve_error1
1425[ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
1426  normalize nodelta
1427  [1,2,3,4,5: @res_preserve_error1
1428  | @if_elim #_ [ @mfr_return_eq1 % | @res_preserve_error1]
1429  ]
1430] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
1431  [2,4: #pc4] normalize nodelta @res_preserve_error1
1432qed.
1433
1434lemma beloadv_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1435∀ptr.
1436preserving1 … opt_preserve1 …
1437     (sigma_mem prog sigma)
1438     (sigma_beval prog sigma)
1439     (λm.beloadv m ptr)
1440     (λm.beloadv m ptr).
1441#prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds;
1442normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
1443whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
1444@if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
1445normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim
1446[2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta
1447@mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb
1448@If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %]
1449* %
1450qed.
1451
1452lemma bestorev_ok : ∀prog : ertl_program.∀sigma : sigma_map prog.
1453∀ptr.
1454preserving21 … opt_preserve1 …
1455    (sigma_mem prog sigma)
1456    (sigma_beval prog sigma)
1457    (sigma_mem prog sigma)
1458    (λm.bestorev m ptr)
1459    (λm.bestorev m ptr).
1460#prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds;
1461normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
1462whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
1463@if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
1464whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb
1465@If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb
1466>Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq
1467[ #bl normalize nodelta % [%]
1468  [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] *
1469    whd in match update_block; normalize nodelta @if_elim
1470    [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %]
1471      * whd in match low_bound; normalize nodelta @if_elim [ #_ %]
1472      @eq_block_elim #_ * %
1473    | @eq_block_elim [#_ *] * #Hbl * @If_elim
1474      [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
1475        normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl
1476        assumption
1477      | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
1478      ]
1479   ]
1480 | whd in match update_block; whd in match sigma_mem; normalize nodelta
1481   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ @If_elim
1482   [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] *
1483        whd in match high_bound; normalize nodelta @if_elim [#_ %]
1484        @eq_block_elim [ #_ *] * #H @⊥ @H %
1485   | #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound;
1486     normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *]
1487     #H @⊥ @Hbl assumption
1488  | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
1489  ]
1490 | #z whd in match update_block; whd in match sigma_mem; normalize nodelta
1491   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_
1492   [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim
1493     @if_elim [2: #_ *] #Hzleb' #Hzlb'''
1494     [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta
1495       @If_elim @andb_elim @if_elim [2: #_ *] @if_elim
1496       [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' *
1497       whd in match high_bound; normalize nodelta @if_elim
1498       [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
1499       [ * %] * #H @⊥ @H %
1500     | @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta
1501       @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_
1502       >Hzleb' whd in match high_bound; normalize nodelta @if_elim
1503       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
1504       @If_elim [2: #_ %] *
1505     | @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim
1506       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_
1507       whd in match low_bound in Hzleb'; normalize nodelta in Hzleb';
1508       whd in match high_bound; normalize nodelta @if_elim
1509       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %]
1510       @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
1511     ]
1512   | whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * |4: *] #Hz *
1513       [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim
1514          [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_
1515          whd in match low_bound; normalize nodelta @eq_block_elim
1516          [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound;
1517          normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %]
1518          #_ normalize nodelta
1519          [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %]
1520                #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %]
1521                @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption
1522          | @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
1523          ]
1524       | >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
1525         normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta
1526         whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
1527         normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_
1528         whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ %
1529       ]
1530    ]
1531 ]
1532| %
1533]
1534qed.
1535
1536lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
1537∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
1538(∀ prf : r = Code.P (g prf)) →
1539P ((match r return λx.(r = x → ?) with
1540    [XData ⇒ f | Code ⇒ g])(refl ? r)).
1541#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
1542qed.
1543
1544
1545lemma sp_ok : ∀prog : ertl_program.
1546∀good : (∀fn.good_state_transformation prog fn).
1547∀restr.
1548   preserving1 … res_preserve1 …
1549      (λst.sigma_state prog good st restr)
1550      (λx.x)
1551      (sp ERTL_semantics)
1552      (sp ERTLptr_semantics).
1553#prog #good #restr #st whd in match sp; normalize nodelta
1554whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
1555normalize nodelta whd in match sigma_regs; normalize nodelta
1556cases(regs ? st) #psd_r #hw_r normalize nodelta
1557inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1]
1558#pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta
1559whd in match sigma_hw_register_env; normalize nodelta
1560change with (sigma_beval ? (get_sigma_from_good_state … good) BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
1561>lookup_map >lookup_map
1562cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
1563[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1564whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta
1565[1,2,3,4,5: #ABS destruct
1566| cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef)
1567  [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
1568  whd in match sigma_beval; normalize nodelta
1569  [1,2,3,4,5: #ABS destruct
1570  | @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct
1571    normalize nodelta @match_reg_elim #INUTILE
1572    [ @mfr_return_eq1 % | @res_preserve_error1 ]
1573  | cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct
1574  ]
1575| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
1576 normalize nodelta [2: #x] #EQ destruct
1577]
1578qed.
1579
1580lemma set_sp_ok :  ∀prog : ertl_program.
1581∀good : (∀fn.good_state_transformation prog fn).
1582∀restr.∀ptr,st.
1583set_sp ? ptr (sigma_state prog good st restr) =
1584sigma_state prog good (set_sp ? ptr st) restr.
1585#prog #good #restr #ptr #st whd in match set_sp; whd in match sigma_state;
1586normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???);
1587whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
1588cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
1589whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env;
1590normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %]
1591>insert_map @eq_f >insert_map %
1592qed.
1593
1594lemma eval_seq_no_pc_no_call_ok :
1595∀prog : ertl_program.
1596let trans_prog ≝ (ertl_to_ertlptr prog) in
1597∀good : (∀fn.good_state_transformation prog fn).
1598∀stack_size. ∀id. ∀fn : (joint_closed_internal_function ??) .∀seq.
1599   preserving1 ?? res_preserve1 ????
1600      (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1601      (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1602      (eval_seq_no_pc ERTL_semantics
1603             (globals (mk_prog_params ERTL_semantics prog stack_size))
1604             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
1605      (eval_seq_no_pc ERTLptr_semantics
1606  (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
1607  (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (seq_embed … seq)).
1608#prog #good #stack_size #f #fn *
1609whd in match eval_seq_no_pc; normalize nodelta
1610[ #c #st @mfr_return1
1611| #c #st @mfr_return1
1612| #pm #st whd in match pair_reg_move; normalize nodelta
1613  @mfr_bind1
1614  [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
1615  | | #regs  @mfr_return_eq1 %
1616  ]
1617| #r #st @mfr_bind1
1618  [2:  @pop_ok |
1619  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
1620    [2: @ps_reg_store_ok |
1621    | #regs  @mfr_return_eq1 %
1622    ]
1623  ]
1624| #r #st @mfr_bind1
1625  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1626  | #bv @push_ok
1627  ]
1628| #i
1629  #i_spec
1630  change with ((dpl_reg ERTL) → ?)
1631  #dpl
1632  change with ((dph_reg ERTL) → ?)
1633  #dph #st @mfr_bind1
1634  [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1635  | whd in match dpl_store; normalize nodelta @mfr_bind1
1636    [2: @opt_safe_elim #bl #EQbl
1637       @opt_safe_elim #bl'
1638       >(find_symbol_transf …
1639          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
1640       >EQbl #EQ destruct whd in match sigma_state; normalize nodelta       
1641       change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …))
1642                                               in ⊢ (???????(?????%?)?);
1643       @ps_reg_store_ok |
1644    | #regs  @mfr_return_eq1 %
1645    ]
1646  | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
1647    >(find_symbol_transf …
1648          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
1649    >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
1650    [2: whd in match sigma_state; normalize nodelta       
1651       change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …))
1652                                               in ⊢ (???????(?????%?)?);
1653      @ps_reg_store_ok |
1654    | #regs  @mfr_return_eq1 %
1655    ]
1656  ]
1657| #op #a #b #arg1 #arg2 #st @mfr_bind1
1658  [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
1659     @ps_arg_retrieve_ok |
1660  | #bv1 @mfr_bind1
1661   [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
1662      @ps_arg_retrieve_ok |
1663   | #bv2 @mfr_bind1
1664     [2: @be_opaccs_ok |
1665     | * #bv3 #bv4 normalize nodelta @mfr_bind1
1666       [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1667       | whd in match acca_store; normalize nodelta @mfr_bind1
1668         [2: @ps_reg_store_ok |
1669         | #regs  @mfr_return_eq1 %
1670         ]
1671       | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
1672         [2: whd in match sigma_state; normalize nodelta
1673            @ps_reg_store_ok |
1674         | #regs  @mfr_return_eq1 %
1675         ]         
1676       ]
1677     ]
1678   ]
1679  ] 
1680| #op #r1 #r2 #st @mfr_bind1
1681  [ @(sigma_beval prog (get_sigma_from_good_state … good))
1682  | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
1683  | #bv1 @mfr_bind1
1684    [ @(sigma_beval prog (get_sigma_from_good_state … good))
1685    | @be_op1_ok
1686    | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
1687      [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
1688      | #regs  @mfr_return_eq1 %
1689      ]
1690    ]
1691  ]
1692| #op2 #r1 #r2 #arg #st @mfr_bind1
1693  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1694  | #bv @mfr_bind1
1695    [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1696    | #bv1 @mfr_bind1
1697      [2: @be_op2_ok |
1698      | * #bv2 #b @mfr_bind1
1699        [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1700        | whd in match acca_store; normalize nodelta @mfr_bind1
1701          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
1702          | #regs  @mfr_return_eq1 %
1703          ]
1704        | #st1 @mfr_return_eq1 %
1705        ]
1706      ]
1707    ]
1708  ]
1709| #st  @mfr_return_eq1 %
1710| #st  @mfr_return_eq1 %
1711| #r1 #dpl #dph #st @mfr_bind1
1712  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1713  | #bv @mfr_bind1
1714    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1715    | #bv1 @mfr_bind1
1716      [ @(λx.x)
1717      | @(pointer_of_address_ok ? ? 〈bv1,bv〉)
1718      | #ptr @mfr_bind1
1719        [2: @opt_to_res_preserve1 @beloadv_ok |
1720        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
1721          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
1722          | #regs  @mfr_return_eq1 %
1723          ]
1724        ] 
1725      ]
1726    ]
1727  ] 
1728| #dpl #dph #r #st @mfr_bind1
1729  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1730  | #bv @mfr_bind1
1731    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1732    | #bv1 @mfr_bind1
1733      [ @(λx.x)
1734      |  @(pointer_of_address_ok ? ? 〈bv1,bv〉)
1735      | #ptr @mfr_bind1
1736        [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1737        | #bv2 @mfr_bind1
1738          [2: @opt_to_res_preserve1 @bestorev_ok |
1739          | #m @mfr_return_eq1 %
1740          ]
1741        ]
1742      ]
1743    ]
1744  ]
1745| #ext #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
1746  normalize nodelta
1747  [ @res_preserve_error1
1748  | #n cases ext normalize nodelta
1749    [1,2: @mfr_bind1
1750      [1,4: @(λx.x)
1751      |2,5: @sp_ok
1752      |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
1753      ]
1754    | #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
1755      [2: whd in match sigma_state; normalize nodelta
1756          change with (sigma_beval ? (get_sigma_from_good_state … good) (BVByte ?))
1757               in ⊢ (???????(??%?)?);
1758          @ps_reg_store_ok
1759      |
1760      | #regs @mfr_return_eq1 %
1761      ]
1762    ]
1763  ]     
1764]
1765qed.
1766
1767lemma partial_inj_sigma : ∀ prog : ertl_program.
1768∀good : (∀fn.good_state_transformation prog fn).
1769let sigma ≝ (get_sigma_from_good_state … good) in
1770∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2.
1771#prog #good #fn #lbl1 #lbl2 inversion(get_sigma_from_good_state … lbl1)
1772[#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma_from_good_state; normalize nodelta
1773#H @('bind_inversion H) -H * #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct
1774#_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
1775whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
1776lapply(find_predicate ?????? H2) cases(f_lbls ????) normalize nodelta [*]
1777* normalize nodelta
1778[@eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % ]
1779#lb #tl @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
1780qed.
1781
1782lemma pc_of_label_eq :
1783  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
1784  ∀globals,ge,bl,i_fn,lbl.
1785  fetch_internal_function ? ge bl = return i_fn →
1786  pc_of_label pars globals ge bl lbl =
1787    OK ? (pc_of_point ERTL_semantics bl lbl).
1788#p #p' #globals #ge #bl #i_fn #lbl #EQf
1789whd in match pc_of_label;
1790normalize nodelta >EQf >m_return_bind %
1791qed.
1792
1793lemma pop_ra_ok :
1794∀prog : ertl_program.
1795∀good : (∀fn.good_state_transformation prog fn).
1796∀restr.
1797preserving1 … res_preserve1 …
1798     (λst.sigma_state prog good st restr)
1799     (λx.let 〈st,pc〉 ≝ x in
1800         let sigma ≝ (get_sigma_from_good_state … good) in
1801       〈sigma_state prog good st restr,
1802        sigma_stored_pc ? sigma pc〉)
1803     (pop_ra ERTL_semantics)
1804     (pop_ra ERTLptr_semantics).
1805#prog #good #restr #st whd in match pop_ra; normalize nodelta @mfr_bind1
1806[ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
1807[ @(sigma_stored_pc ? (get_sigma_from_good_state … good))
1808| whd in match pc_of_bevals; normalize nodelta
1809  cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
1810  whd in match sigma_beval; normalize nodelta try @res_preserve_error1
1811  inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
1812  #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
1813  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1814  normalize nodelta try @res_preserve_error1
1815  inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
1816  #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
1817  @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
1818  #_ #H >H @eq_program_counter_elim [2: #_ *]
1819  #EQspc * @eq_program_counter_elim
1820  [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
1821   >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
1822   whd in match sigma_pc_opt; normalize nodelta @if_elim
1823  [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
1824    #H3 #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
1825    cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
1826  | #H2 @if_elim
1827    [ #H3 #H @('bind_inversion H) -H #x1 #_ #H @('bind_inversion H) -H #lbl1 #_
1828      cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?);
1829      #EQ destruct >H3 in H2; *
1830    | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
1831     [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ #x #x_spec
1832     lapply(res_eq_from_opt ??? x_spec) -x_spec #x_spec #H @('bind_inversion H) * #lbl
1833     #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1
1834     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2
1835     #H @('bind_inversion H) -H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) -x1_spec #x1_spec
1836     #H @('bind_inversion H) -H * #lbl2 #lbl2_spec
1837     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
1838     <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct
1839     lapply(partial_inj_sigma … EQsig)
1840     [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta
1841     whd in match (point_of_offset ??); whd in match (point_of_offset ??);
1842     #EQ destruct cases pc1 #bl #p %
1843    ]
1844  ]
1845| #pc @mfr_return_eq1 %
1846]
1847qed.
1848
1849lemma pc_block_eq : ∀prog : ertl_program.
1850∀sigma : sigma_map prog.
1851∀pc,id,fn.
1852fetch_internal_function (joint_closed_internal_function ERTL
1853  (prog_var_names (joint_function ERTL) ℕ prog))
1854  (globalenv_noinit (joint_function ERTL) prog) (pc_block … pc)
1855  = return 〈id,fn〉→
1856sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? →
1857 pc_block … pc = pc_block … (sigma_stored_pc prog sigma pc).
1858#prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc;
1859normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %]
1860#_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind %
1861qed.
1862
1863inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
1864    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
1865(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
1866
1867include "joint/semantics_blocks.ma".
1868
1869lemma fetch_internal_function_no_zero :
1870∀F,V,i,p,bl.
1871  block_id (pi1 … bl) = 0 →
1872  fetch_internal_function ?
1873 
1874  (globalenv (λvars.fundef (F vars)) V i p) bl =
1875  Error ? [MSG BadFunction].
1876#F #V #i #p #bl #EQbl whd in match fetch_internal_function;
1877normalize nodelta >fetch_function_no_zero [2: assumption] %
1878qed.
1879
1880lemma fetch_internal_function_no_minus_one :
1881∀F,V,i,p,bl.
1882  block_id (pi1 … bl) = -1 →
1883  fetch_internal_function ?
1884 
1885  (globalenv (λvars.fundef (F vars)) V i p) bl =
1886  Error ? [MSG BadFunction].
1887#F #V #i #p #bl #EQbl whd in match fetch_internal_function;
1888normalize nodelta >fetch_function_no_minus_one [2: assumption] %
1889qed.
1890
1891lemma fetch_statement_no_zero :
1892∀pars,prog,stack_size,pc.
1893block_id(pi1 … (pc_block pc)) = 0 →
1894fetch_statement pars (prog_var_names … prog)
1895(ev_genv (mk_prog_params pars prog stack_size)) pc =
1896Error ? [MSG BadFunction].
1897#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
1898>fetch_internal_function_no_zero [2: assumption] %
1899qed.
1900
1901lemma fetch_statement_no_minus_one :
1902∀pars,prog,stack_size,pc.
1903block_id(pi1 … (pc_block pc)) = -1 →
1904fetch_statement pars (prog_var_names … prog)
1905(ev_genv (mk_prog_params pars prog stack_size)) pc =
1906Error ? [MSG BadFunction].
1907#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
1908>fetch_internal_function_no_minus_one [2: assumption] %
1909qed.
1910
1911
1912
1913lemma foo :
1914 ∀P1_unser,P2_unser: unserialized_params.
1915 ∀P1_sem_unser,P2_sem_unser.
1916 let P1_sem ≝ make_sem_graph_params P1_unser P1_sem_unser in
1917 let P2_sem ≝ make_sem_graph_params P2_unser P2_sem_unser in
1918 ∀init,translate_step.
1919 ∀translate_fin_step.
1920 ∀closed_graph_translate.
1921 let translate_internal :
1922  ∀globals.
1923   joint_closed_internal_function P1_sem globals →
1924   joint_closed_internal_function P2_sem globals
1925  ≝
1926  λglobals,fun.
1927   «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals
1928    (init globals)
1929    (translate_step globals)
1930    (translate_fin_step globals)
1931    (pi1 … fun), closed_graph_translate globals fun» in
1932 ∀prog.
1933 let trans_prog ≝ transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)) in
1934 ∀stack_size.
1935 ∀sigma_state_pc.
1936 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) →
1937 ∀st : state_pc P2_sem.
1938 ∀st' : state_pc P1_sem.
1939 ∀f.
1940 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)).
1941 luniverse_ok … fn →
1942 ∀stmt,nxt.
1943 ∀P : (state_pc P2_sem) → Prop.
1944 (∀pre_Instrs',last_Instrs',dst.
1945   ∃st''.∃st'''.∃st''''.
1946    repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size)
1947     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
1948    eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size))
1949                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
1950    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
1951     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧
1952    P st'' (*st' = sigma_state_pc st''*) ∧
1953    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
1954    let P2_globals ≝ globals P2_prog_params in
1955     All
1956      (joint_seq … P2_globals)
1957      (no_cost_label … P2_globals)
1958      (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) →
1959 fetch_statement …
1960  (prog_var_names (joint_function P1_sem) ℕ prog)
1961  (ev_genv (mk_prog_params P1_sem prog stack_size))
1962  (pc … (sigma_state_pc st)) =
1963    return 〈f, fn,  sequential … (step_seq P1_sem … stmt) nxt〉 →
1964 eval_state …
1965 (prog_var_names (joint_function P1_sem) ℕ prog)
1966 (ev_genv … (mk_prog_params P1_sem prog stack_size))
1967 (sigma_state_pc st) = return st' →
1968 ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*)
1969 P st'' ∧
1970 ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''.
1971(if taaf_non_empty … taf then True else
1972(¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) ∨
1973 ¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) st'))
1974 (* the length of taf is the same of the length of ??? *).
1975#P1_unser #P2_unser #P1_sem_unser #P2_sem_unser
1976letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser)
1977letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser)
1978#init #translate_step #translate_fin_step #closed_graph_translate.
1979letin translate_internal ≝
1980 (λglobals,fun.
1981   «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals
1982    (init globals)
1983    (translate_step globals)
1984    (translate_fin_step globals)
1985    (pi1 … fun), closed_graph_translate globals fun»)
1986#prog
1987letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)))
1988#stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #P
1989#Hpass #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
1990cases
1991 (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok)
1992#_ * #MK_fresh_labels * #MK_fresh_registers **** #_ #_ #_ #_ (*CSC: useful things thrown out here *)
1993#MULTI_FETCH_OK cases (MULTI_FETCH_OK … EQstmt)
1994#list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers
1995normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
1996@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
1997#EQeval
1998cut((list
1999   (code_point P2_sem
2000    →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)]
2001#pre_Instrs'
2002cut((code_point P2_sem
2003   →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)]
2004#last_Instrs'
2005cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *))
2006#st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED
2007lapply(produce_trace_any_any_free … NO_COSTED … REPEAT)
2008[ cases daemon (* should be @Multi_fetch *)
2009| <sigma_state_pc_ok @(fetch_internal_function_transf … (λvars.translate_internal vars))
2010  assumption
2011| @dst
2012| @list_b_last (*wrong, should dst be destination or the last of list_b_last *)
2013] #TAAF
2014lapply
2015  (produce_step_trace (mk_prog_params P2_sem trans_prog stack_size)
2016    (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
2017       st''' (pc_of_point P2_sem (pc_block (pc … st)) dst) (last_pop … st))
2018    f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' … EVAL_NO_PC_Last)
2019[ cases daemon (* should be @STEP_In_code *)
2020| <sigma_state_pc_ok
2021  @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ]
2022#LAST_STEP
2023cases daemon
2024qed.
2025
2026lemma eval_seq_no_call_ok :
2027 ∀prog.
2028 let trans_prog ≝ ertl_to_ertlptr prog in
2029 ∀good : (∀fn.good_state_transformation prog fn).     
2030 ∀stack_sizes.
2031 (*? →*)
2032 ∀st : state_pc ERTLptr_semantics.
2033 ∀st' : state_pc ERTL_semantics.
2034 ∀f,fn,stmt,nxt.
2035   fetch_statement ERTL_semantics
2036     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2037    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
2038    (pc … (sigma_state_pc ? good st)) =
2039      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
2040   eval_state ERTL_semantics
2041   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2042   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2043   (sigma_state_pc ? good st) =
2044    return st' →
2045 ∃st''. st' = sigma_state_pc ? good st'' ∧
2046 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2047  st
2048  st''.
2049 bool_to_Prop (taaf_non_empty … taf).
2050#prog #good #stack_size #st #st' #f #fn #stmt #nxt #EQfetch #EQeval
2051cases (foo … translate_step translate_fin_step … EQfetch EQeval)
2052[2,3: cases daemon (* first one, take out init definition from ERTLtoERTLptr;
2053                      second one to be taken from somewhere *)
2054|4: #x cases daemon (* TO BE DONE, EASY *)
2055|5: cases daemon (* to be taken in input *)
2056|6: @(λst''.st' = sigma_state_pc ? good st'')
2057|7: cases daemon
2058| #st'' * #EQ destruct * change with ERTL_uns in match (mk_unserialized_params ???????????????);
2059  change with ERTLptr_uns in match (mk_unserialized_params ???????????????);
2060  (* change with ERTL_semantics in match (make_sem_graph_params ??);
2061  change with ERTLptr_semantics in match (make_sem_graph_params ??); *)
2062#taaf #Htaaf %{st''}
2063 % [%] cases daemon
2064 qed.
2065
2066lemma lookup_opt_none_transf :
2067∀prog : ertl_program.
2068let trans_prog ≝ ertl_to_ertlptr prog in
2069∀x.lookup_opt
2070    (fundef
2071     (joint_closed_internal_function ERTL
2072      (prog_var_names (joint_function ERTL) ℕ prog))) x
2073     (functions
2074       (fundef
2075        (joint_closed_internal_function ERTL
2076         (prog_var_names (joint_function ERTL) ℕ prog)))
2077       (globalenv_noinit (joint_function ERTL) prog)) =None ? →
2078lookup_opt
2079    (fundef
2080     (joint_closed_internal_function ERTLptr
2081      (prog_var_names (joint_function ERTLptr) ℕ trans_prog))) x
2082     (functions
2083       (fundef
2084        (joint_closed_internal_function ERTLptr
2085         (prog_var_names (joint_function ERTLptr) ℕ trans_prog)))
2086       (globalenv_noinit (joint_function ERTLptr) trans_prog)) =None ?.
2087#prog #x #EQlookup
2088whd in match ertl_to_ertlptr in ⊢ (??(???(??%))?); whd in match transform_program;
2089whd in match transf_program; normalize nodelta whd in match globalenv_noinit;
2090whd in match globalenv; whd in match globalenv_allocmem;
2091whd in match add_globals; normalize nodelta
2092cases daemon
2093qed.
2094
2095 
2096 
2097lemma fetch_function_none :
2098∀prog : ertl_program.
2099let trans_prog ≝ ertl_to_ertlptr prog in
2100∀bl.
2101fetch_function
2102        (fundef
2103         (joint_closed_internal_function ERTL
2104          (prog_var_names (joint_function ERTL) ℕ prog)))
2105        (globalenv_noinit (joint_function ERTL) prog) bl = Error ? [MSG BadFunction] →
2106fetch_function
2107        (fundef
2108         (joint_closed_internal_function ERTLptr
2109          (prog_var_names (joint_function ERTLptr) ℕ trans_prog)))
2110        (globalenv_noinit (joint_function ERTLptr) trans_prog) bl = Error ? [MSG BadFunction].
2111#prog #bl whd in match fetch_function in ⊢ (% → ?); normalize nodelta
2112<(symbol_for_block_transf … (λn:ℕ.[Init_space n]) prog …
2113                         (λvars.transf_fundef … (translate_internal …)) bl)
2114change with (symbol_for_block
2115              (fundef
2116                (joint_closed_internal_function ERTLptr
2117                  (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog))))
2118               (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog)) bl)
2119               in match (symbol_for_block ???);
2120whd in match fetch_function; normalize nodelta cases(symbol_for_block ???) [#_ %]
2121#id >m_return_bind inversion(find_funct_ptr ???)
2122[2: #x #_ whd in ⊢ (??%% → ?); #EQ destruct] whd in match find_funct_ptr;
2123normalize nodelta cases(block_region bl) normalize nodelta [ #_ #_ >m_return_bind %]
2124cases(block_id bl) normalize nodelta [1,2: [2: #x] #_ #_ >m_return_bind %]
2125#x whd in match globalenv_noinit; whd in match globalenv; normalize nodelta
2126whd in match globalenv_allocmem; normalize nodelta #EQlookup
2127>(lookup_opt_none_transf … EQlookup) #_ %
2128qed.
2129
2130lemma fetch_function_err :
2131∀F,ge,bl,e. fetch_function F ge bl = Error ? e → e = [MSG BadFunction].
2132#F #ge #bl #e whd in match fetch_function; normalize nodelta
2133cases(symbol_for_block ???) [ normalize #EQ destruct %]
2134#id >m_return_bind cases(find_funct_ptr ???) normalize [2: #x]
2135#EQ destruct %
2136qed.
2137
2138 
2139lemma fetch_internal_function_none :
2140∀ prog : ertl_program.
2141let trans_prog ≝ ertl_to_ertlptr prog in
2142∀bl.
2143fetch_internal_function
2144   (joint_closed_internal_function ERTL
2145    (prog_var_names (joint_function ERTL) ℕ prog))
2146   (globalenv_noinit (joint_function ERTL) prog) bl = Error ? [MSG BadFunction] →
2147fetch_internal_function
2148   (joint_closed_internal_function ERTLptr
2149    (prog_var_names (joint_function ERTLptr) ℕ trans_prog))
2150   (globalenv_noinit (joint_function ERTLptr) trans_prog) bl = Error ? [MSG BadFunction].
2151#prog #bl whd in match fetch_internal_function; normalize nodelta
2152inversion(fetch_function ???)
2153[2: #err_msg #EQfetch lapply(fetch_function_err … EQfetch) #EQ destruct #_
2154    >(fetch_function_none … EQfetch) %] * #f * #fn #EQfetch >m_return_bind
2155normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct
2156>(fetch_function_transf … (λvars.transf_fundef … (translate_internal …)) … EQfetch)
2157>m_return_bind %
2158qed.
2159 
2160lemma fetch_internal_function_err :
2161∀F,ge,bl,e. fetch_internal_function F ge bl = Error ? e → e = [MSG BadFunction].
2162#F #ge #bl #e whd in match fetch_internal_function; normalize nodelta
2163inversion(fetch_function ???)
2164[2: #e #EQf lapply(fetch_function_err … EQf) #EQ destruct whd in ⊢ (??%? → ?);
2165    #EQ destruct %] * #id * #fn #EQf >m_return_bind normalize nodelta
2166whd in ⊢ (??%? → ?); #EQ destruct %
2167qed.
2168
2169 
2170   
2171 
2172lemma as_label_ok : ∀ prog : ertl_program.
2173let trans_prog ≝ ertl_to_ertlptr prog in
2174∀ good,stack_sizes,st.
2175as_label (ERTLptr_status trans_prog stack_sizes) st = as_label
2176(ERTL_status prog stack_sizes) (sigma_state_pc prog good st).
2177#prog #good #stack_size #st whd in match as_label; normalize nodelta
2178whd in match (as_pc_of ? ?); whd in match (as_pc_of ? ?);
2179whd in match sigma_state_pc; normalize nodelta @if_elim
2180[ @eqZb_elim [2: #_ *] #EQbl * whd in match (as_label_of_pc ??);
2181  >fetch_statement_no_minus_one [2: assumption] normalize nodelta
2182  whd in match (as_label_of_pc ??); >fetch_statement_no_zero [2: %] %]
2183#_ inversion(fetch_internal_function ???)
2184[2: #e #EQf lapply(fetch_internal_function_err … EQf) #EQ destruct normalize nodelta
2185    whd in match (as_label_of_pc ??); whd in match fetch_statement; normalize nodelta
2186    >(fetch_internal_function_none … EQf) whd in ⊢ (??%%);
2187    >fetch_statement_no_zero [2: %] % ] * #f #fn #EQf normalize nodelta
2188whd in match (as_label_of_pc ??) in ⊢ (???%); whd in match fetch_statement;
2189normalize nodelta >EQf >m_return_bind inversion(stmt_at ????) [cases daemon (*to discuss with Paolo*)]
2190* [ * [ * [ #id | #addr ] #args #dst | #acc_r #lbl | #seq ] #nxt | #fin | *]
2191#EQstmt_at >m_return_bind normalize nodelta
2192cases(multi_fetch_ok … (good fn) … EQstmt_at)
2193#labs * #regs ** #EQlabs #EQregs normalize nodelta whd in match translate_step;
2194normalize nodelta
2195[1,3,4: * #step_block * whd in match (bind_new_instantiates ?????);
2196        cases regs in EQregs; [2,4,6: #r #tl #EQ normalize nodelta *]
2197        #EQregs normalize nodelta #EQ destruct * #dst *
2198        whd in match (step_list_in_code ???????); cases labs in EQlabs;
2199        [2,4,6: #lb #tl #EQ normalize nodelta *] #EQlabs normalize nodelta
2200        #EQ destruct * #nxt1 * #EQ_s_stmt #EQ destruct
2201        whd in match (as_label_of_pc ??); whd in match fetch_statement;
2202        normalize nodelta
2203        >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
2204        >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta [1,2: %]
2205        cases seq
2206        [#str % | #c % | #H1 % | #H3 % | #x % | #H5 #H6 #H7 #H8 %
2207        | #H10 #H11 #H12 #H13 #H14 % | #H16 #H17 #H18 % | #H20 #H21 #H22 #H23 %
2208        | % | % | #H25 #H26 #H27 % | #H29 #H30 #H31 % | #H33 %]
2209| * #step_block whd in match (bind_new_instantiates ?????);
2210  cases regs in EQregs; [ #EQ normalize nodelta **] #reg #tl #EQregs
2211  normalize nodelta whd in match (bind_new_instantiates ?????);
2212  cases tl in EQregs; [2: #reg1 #tl1 #EQ normalize nodelta **]
2213  #EQreg normalize nodelta * #EQ destruct * #dst *
2214  whd in match (step_list_in_code ???????); cases labs in EQlabs;
2215  [ #_ normalize nodelta *] #lbl #tl #EQlabs normalize nodelta *
2216  * #nxt1 * #EQ_s_stmt #_ #_ #_ whd in match (as_label_of_pc ??);
2217  whd in match fetch_statement; normalize nodelta
2218   >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
2219   >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta %
2220| (whd in match translate_fin_step; normalize nodelta) *
2221  #fin_block * whd in match (bind_new_instantiates ?????); cases regs in EQregs;
2222  [2: #r #tl #_ normalize nodelta *] #EQregs normalize nodelta #EQ destruct
2223  * #list_l * #lbl ** #EQ destruct whd in match (step_list_in_code ???????);
2224  normalize nodelta cases list_l in EQlabs; [2: #lbl1 #tl #_ normalize nodelta *]
2225  #EQlabs normalize nodelta #EQ destruct whd in match fin_step_in_code;
2226  normalize nodelta #EQ_s_stmt whd in match (as_label_of_pc ??);
2227   whd in match fetch_statement; normalize nodelta
2228   >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
2229   >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta %
2230]
2231qed.
2232
2233(*
2234#H1 #H2 #H3 *
2235
2236 ∀P1_unser,P2_unser: unserialized_params.
2237 ∀P1_sem_unser,P2_sem_unser.
2238 ∀init,translate_step.
2239 ∀translate_fin_step.
2240 ∀closed_graph_translate.
2241 ∀prog.
2242 ∀stack_size.
2243 ∀sigma_state_pc.
2244 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) →
2245 ∀st : state_pc P2_sem.
2246 ∀st' : state_pc P1_sem.
2247 ∀f.
2248 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)).
2249 luniverse_ok … fn →
2250 ∀stmt,nxt.
2251 (∀pre_Instrs',last_Instrs',dst.
2252   ∃st''.∃st'''.∃st''''.
2253    repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size)
2254     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
2255    eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size))
2256                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
2257    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
2258     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧
2259    st' = sigma_state_pc st'' ∧
2260    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
2261    let P2_globals ≝ globals P2_prog_params in
2262     All
2263      (joint_seq … P2_globals)
2264      (no_cost_label … P2_globals)
2265      (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) →
2266
2267
2268 
2269whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
2270[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2271#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st))) normalize nodelta
2272[2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2273* #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch)
2274* >EQfn #EQ destruct normalize nodelta #EQstmt
2275cases(multi_fetch_ok … (good fn) ?? EQstmt)
2276#list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers
2277normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
2278@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
2279#EQeval
2280cut((list
2281   (code_point ERTLptr
2282    →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)]
2283#pre_Instrs'
2284cut((code_point ERTLptr
2285   →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)]
2286#last_Instrs'
2287letin list_map ≝ cic:/matita/basics/lists/list/map.fix(0,3,1)
2288cut(∃st''.∃st'''.∃st''''.
2289    repeat_eval_seq_no_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2290     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
2291    eval_seq_no_pc ? (prog_var_names … (ertl_to_ertlptr prog)) (ev_genv … (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size))
2292                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
2293    st'' = (mk_state_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2294     st'''' (pc_of_point ERTLptr_semantics (pc_block (pc … st)) dst)
2295                                 (last_pop … st)) ∧
2296    st' = sigma_state_pc ? good st'')
2297     [ cases daemon (*to be generalized and TO be moved into an other lemma *)]
2298* #st'' * #st''' * #st'''' *** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' %{st''} % [assumption]
2299lapply(produce_trace_any_any_free … REPEAT)
2300[ cases daemon (* Pass dependent *)
2301| cases daemon (* should be @Multi_fetch *)
2302| @(fetch_internal_function_transf … (λvars. translate_internal …) … EQfn)
2303| @dst
2304| @list_b_last (*wrong, should dst be destination or the last of list_b_last *)
2305] #TAAF
2306lapply(produce_step_trace (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2307       (mk_state_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2308     st''' (pc_of_point ERTLptr_semantics (pc_block (pc … st)) dst)
2309                                 (last_pop … st)) f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' (fetch_internal_function_transf … (λvars. translate_internal …) … EQfn)
2310       ? EVAL_NO_PC_Last) [cases daemon (* should be @STEP_in_code *)]
2311#LAST_STEP
2312letin taaf_last ≝ (taaf_step ???? TAAF LAST_STEP)
2313
2314        cut(dst = (point_of_pc
2315                           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2316                           (pc … st))) [cases daemon (*TODO it is true since pre_Instr is empty *)]
2317                #EQ <EQ whd in match step_in_code; normalize nodelta
2318                cases STEP_in_code #x * #x_spec #x_spec' %{x} %
2319                [ >x_spec in ⊢ (??%?); @eq_f @eq_f2 [2: %] cases daemon (*should be % *) |
2320                 [<EVAL_NO_PC_Last in ⊢ (???%); @eq_f %
2321
2322
2323
2324whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
2325lapply EQfetch -EQfetch whd in match sigma_state_pc in ⊢ (% → ?);
2326normalize nodelta @if_elim
2327[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2328#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st))) normalize nodelta
2329[2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2330* #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch)
2331* >EQfn #EQ destruct normalize nodelta #EQstmt
2332whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
2333[#H >H in EQbl; *] #_ >EQfn normalize nodelta whd in match eval_statement_no_pc;
2334normalize nodelta #H @('bind_inversion H) -H #ex_st_nopc
2335#H lapply (err_eq_from_io ????? H) -H #EQnopc whd in match eval_statement_advance;
2336normalize nodelta whd in match set_no_pc; normalize nodelta
2337whd in ⊢ (??%% → ?); #EQ destruct cases(eval_seq_no_pc_no_call_ok … EQnopc)
2338#sigma_st_nopc * #EQsigma_st_nopc #sem_rel %
2339[ % [@sigma_st_nopc
2340    | @(succ_pc ERTL_semantics (pc ERTLptr_semantics st) nxt)
2341    | @(last_pop … st)
2342    ]
2343] % whd in match sigma_state_pc;
2344
2345
2346
2347qed.*)
2348
2349lemma ertl_to_ertlptr_ok:
2350∀prog.
2351let trans_prog ≝ ertl_to_ertlptr prog in
2352∀good : (∀fn.good_state_transformation prog fn).     
2353∀stack_sizes.
2354   ex_Type1 … (λR.
2355   status_simulation
2356    (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R).
2357#prog #good #stack_size % [@ERTLptrStatusSimulation assumption]
2358whd in match status_simulation; normalize nodelta
2359whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
2360whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
2361change with
2362  (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) 
2363#EQeval @('bind_inversion EQeval)
2364** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
2365#_  whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct
2366cases stmt in EQfetch; -stmt
2367[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch
2368change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2369[ (*CALL*) cases daemon
2370| (*COND*) cases daemon
2371| (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
2372          normalize nodelta cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
2373          #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
2374          % [% //] whd >as_label_ok [2:assumption] %
2375
2376
2377lapply(produce_trace_any_any_free
2378      (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2379      st2 id (translate_internal ? fn)) #PRODUCE_TAAF
2380cases stmt in EQfetch; -stmt
2381[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch
2382normalize nodelta
2383
2384     
2385lapply EQfetch -EQfetch whd in match sigma_state_pc in ⊢ (% → ?);
2386normalize nodelta @if_elim
2387[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2388#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st2))) normalize nodelta
2389[2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2390* #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch)
2391* >EQfn #EQ destruct normalize nodelta #EQstmt     
2392     
2393      ? ? ?? ? ???)
2394
2395
2396
2397cases stmt in EQfetch; -stmt
2398[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQstmt
2399change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2400whd in match joint_classify; normalize nodelta >EQstmt >m_return_bind
2401normalize nodelta lapply(fetch_statement_inv … EQstmt) * #fn_spec
2402#stmt_spec
2403cases(multi_fetch_ok … (good fn) ?? stmt_spec) #f_labs * #f_regs ** #f_labs_spec
2404#f_regs_spec normalize nodelta * #list_instr * #b_new_f_regs
2405whd in ⊢ (% → ?); normalize nodelta
2406[1,2,3: @pair_elim #list_instr1 #rgt #last_ne_spec * #last_lab *
2407       #list_instr1_spec #last_step
2408       lapply(fetch_internal_function_transf …
2409                                       (λvars. translate_internal …) … fn_spec)
2410       change with ((fetch_internal_function
2411                    (joint_closed_internal_function ? (prog_var_names … (ertl_to_ertlptr prog)))
2412                    (globalenv_noinit … (ertl_to_ertlptr prog)) ?) = ?  → ?)
2413       #EQtrans_fn
2414       check prog_params
2415       lapply(produce_trace_any_any_free
2416       (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
2417        ? id (translate_internal ? fn) ? ? ?? EQtrans_fn ???) [2: @EQtrans_fn
2418
2419
2420
2421
2422
2423lapply EQstmt whd in match sigma_state_pc in ⊢ (% → ?);
2424normalize nodelta @if_elim
2425[1,3: #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2426#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st2))) normalize nodelta
2427[2,4: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
2428* #id1 #fn1 #EQfn1 normalize nodelta #EQstmt1 lapply(fetch_statement_inv … EQstmt1)
2429* >EQfn1 #EQ destruct normalize nodelta #EQstmtat
2430
2431
2432
2433
2434[ (*CALL*)
2435  cases daemon (*TODO*)
2436| whd in match joint_classify; normalize nodelta
2437 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2438  normalize nodelta
2439 #n_cost
2440 cases (eval_cond_ok … EQfetch EQeval n_cost)
2441 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf}
2442 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok %
2443| whd in match joint_classify; normalize nodelta
2444 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2445  normalize nodelta
2446  cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
2447  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
2448  % [% //] whd >as_label_ok [2:assumption] %
2449| (*FIN*)
2450  cases fin_step in EQfetch;
2451  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
2452  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
2453    cases (eval_goto_ok … EQfetch EQeval)
2454    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
2455    % [% //] whd >as_label_ok [2:assumption] %
2456  | (*RETURN*) #EQfetch
2457     whd in match joint_classify; normalize nodelta
2458    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
2459    cases (eval_return_ok … EQfetch EQeval) #is_ret
2460    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
2461    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
2462    % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption]
2463    % assumption
2464  | (*TAILCALL*) #fl #called #args #EQfetch
2465    cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall
2466    * #is_tailcall' *  #eq_call #EQeval' >is_tailcall normalize nodelta
2467    #prf  %{«?, is_tailcall'»} %{eq_call}
2468    % [2: % [2: %{(taa_base …)} %{(taa_base …)}  % [ %{EQeval'} % |] | ] | ]
2469    whd >as_label_ok %
2470  ]
2471]
2472qed.
2473
2474@('bind_inversion EQfetch) * #id1 #fn1 #EQfn #H @('bind_inversion H) -H
2475#stmt1 #H lapply(opt_eq_from_res ???? H) -H #EQstmt whd in ⊢ (??%% → ?);
2476#EQ destruct
2477
2478(*
2479lemma push_ra_ok : ∀prog : ertl_program.
2480∀good :  (∀fn.good_state_transformation prog fn).∀restr.
2481preserving21 … res_preserve1 …
2482     (sigma_state_pc prog good)
2483     (\l
2484     (λst.sigma_state prog good st restr)
2485     (push_ra ERTL_semantics)
2486     (push_ra ERTLptr_semantics).
2487#prog #good #restr #st #pc whd in match push_ra; normalize nodelta @mfr_bind1
2488[2: whd in match sigma_stored_pc; normalize nodelta
2489
2490[2: #x
2491
2492
2493lemma ertlptr_save_frame_ok : ∀prog : ertl_program.
2494∀good : (∀fn.good_state_transformation prog fn).
2495∀id.
2496    preserving1 … res_preserve1 …
2497        (sigma_state_pc prog good)
2498        (λst. match get_internal_function_from_ident
2499                  ERTL_semantics (prog_var_names … prog)
2500                  (globalenv_noinit … prog) id with
2501             [None ⇒ dummy_state
2502             |Some fd ⇒
2503                sigma_state prog good st (added_registers … fd (f_regs … (good fd)))
2504             ])
2505        (ertl_save_frame ID it id)
2506        (ertlptr_save_frame ID it id).
2507#prog #good #id #st whd in match ertl_save_frame; whd in match ertlptr_save_frame;
2508normalize nodelta @mfr_bind1
2509[2: whd in match push_ra; normalize nodelta @mfr_bind1
2510xxxxxxxxxxxx
2511
2512
2513
2514lemma fetch_statement_commute :
2515∀prog : ertl_program.
2516let trans_prog ≝ (ertl_to_ertlptr prog) in
2517∀sigma : sigma_map trans_prog.
2518∀stack_sizes,id,fn,stmt,pc.
2519fetch_statement ERTL_semantics
2520(globals (mk_prog_params ERTL_semantics prog stack_sizes))
2521(ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
2522pc = return 〈id,fn,stmt〉 →
2523match stmt with
2524[ sequential seq nxt ⇒
2525    match seq with
2526    [ CALL ids args dest ⇒
2527        match ids with
2528        [ inl i ⇒
2529          fetch_statement ERTLptr_semantics
2530          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2531          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2532          pc =
2533          return 〈id,
2534          translate_internal … fn,
2535          sequential ?? (CALL ERTLptr ? (inl ?? i) args dest) nxt〉
2536        | inr p ⇒ ?(*
2537          ∃reg,lbl.
2538          fetch_statement ERTLptr_semantics
2539          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2540          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2541           pc = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (LOW_ADDRESS reg lbl)) nxt〉
2542           ∧ ∃ nxt'.
2543           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2544                 id nxt;
2545           fetch_statement ERTLptr_semantics
2546          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2547          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2548           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'〉
2549           ∧ ∃ nxt''.
2550           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2551                 id nxt';
2552           fetch_statement ERTLptr_semantics
2553          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2554          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2555           pc' = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (HIGH_ADDRESS reg lbl)) nxt''〉
2556           ∧ ∃ nxt'''.
2557           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2558                 id nxt'';
2559           fetch_statement ERTLptr_semantics
2560          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2561          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2562           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'''〉
2563           ∧ ∃ nxt''''.
2564           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2565                 id nxt''';
2566           fetch_statement ERTLptr_semantics
2567          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2568          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2569           pc' = return 〈id,translate_internal … fn,sequential ?? (CALL ERTLptr ? (inr ?? p) args dest) nxt''''〉
2570           ∧ sigma (translate_internal … fn) nxt''' =  return point_of_pc ERTL_semantics pc *)
2571        ]
2572    | COND r lbl ⇒
2573          fetch_statement ERTLptr_semantics
2574          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2575          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2576          pc =
2577          return 〈id,
2578          translate_internal … fn,
2579          sequential ?? (COND ERTLptr ? r lbl) nxt〉
2580    | step_seq s ⇒
2581          fetch_statement ERTLptr_semantics
2582          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2583          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2584          pc =
2585          return 〈id,
2586          translate_internal … fn,
2587          sequential ?? (step_seq ERTLptr … (translate_step_seq ? s)) nxt〉
2588    ]                   
2589| final fin ⇒
2590     fetch_statement ERTLptr_semantics
2591     (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2592     (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2593     pc = return 〈id,(translate_internal … fn),final … (joint_fin_step_id fin)〉
2594| FCOND abs _ _ _ ⇒ Ⓧabs
2595].
2596cases daemon
2597qed.
2598
2599lemma eval_seq_no_call_ok :
2600 ∀prog.
2601 let trans_prog ≝ ertl_to_ertlptr prog in
2602 ∀sigma : sigma_map trans_prog.∀stack_sizes.
2603 (*? →*)
2604 ∀st,st',f,fn,stmt,nxt.
2605   fetch_statement ERTL_semantics
2606     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2607    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
2608    (pc … (sigma_state_pc ? sigma st)) =
2609      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
2610   eval_state ERTL_semantics
2611   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2612   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2613   (sigma_state_pc ? sigma st) =
2614    return st' →
2615 ∃st''. st' = sigma_state_pc ? sigma st'' ∧
2616 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2617  st
2618  st''.
2619 bool_to_Prop (taaf_non_empty … taf).
2620#prog #sigma #stack_size #st1 #st2 #f #fn #stmt #nxt #EQf whd in match eval_state;
2621normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance;
2622whd in match eval_statement_no_pc; normalize nodelta
2623 #H @('bind_inversion H) -H #st_no_pc #EQ lapply(err_eq_from_io ????? EQ) -EQ
2624#EQeval whd in ⊢ (??%% → ?); #EQ destruct lapply EQf
2625whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
2626[ #EQbl
2627| #pc_st1_spec inversion(fetch_internal_function ???) [2: #e #_]
2628]
2629[1,2: whd in match dummy_state_pc; whd in match null_pc;
2630  whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
2631  normalize nodelta lapply(fetch_function_no_zero ??????)
2632  [2,9: @( «mk_block Code OZ,refl region Code»)
2633    |1,8: % |3,10: @prog |7,14: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2634* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2635whd in match fetch_statement; normalize nodelta >fn1_spec
2636>m_return_bind #H @('bind_inversion H) -H #stmt1 #EQ
2637lapply(opt_eq_from_res ???? EQ) -EQ #stmt1_spec whd in ⊢ (??%% → ?); #EQ destruct
2638lapply EQeval -EQeval whd in match sigma_state_pc in ⊢ (% → ?);
2639normalize nodelta @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec
2640normalize nodelta #EQeval cases(eval_seq_no_pc_no_call_ok ???????? EQeval)
2641#st_no_pc' * #EQeval' #EQst_no_pc'
2642whd in match set_no_pc; normalize nodelta
2643% [ % [@st_no_pc'|@(succ_pc ERTL_semantics (pc ERTL_semantics (sigma_state_pc prog sigma st1))
2644   nxt)| @(last_pop ? st1)]]
2645% [ whd in match sigma_state_pc; normalize nodelta
2646    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
2647    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
2648    >EQst_no_pc' %]
2649%{(taaf_step … (taa_base …) …)}
2650[3: //] lapply(fetch_statement_commute ? sigma ????? EQf) normalize nodelta
2651whd in match sigma_state_pc; normalize nodelta
2652@if_elim [1,3:#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
2653#EQf1
2654[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
2655  >EQf1 normalize nodelta %
2656| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
2657  >EQf1 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
2658  >EQeval' >m_return_bind %
2659]
2660qed.
2661
2662
2663lemma eval_goto_ok :
2664 ∀prog : ertl_program.
2665 let trans_prog ≝ ertl_to_ertlptr prog in
2666 ∀stack_sizes.
2667 ∀sigma : sigma_map trans_prog.
2668 ∀st,st',f,fn,nxt.
2669   fetch_statement ERTL_semantics …
2670    (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2671      return 〈f, fn,  final … (GOTO ERTL … nxt)〉 →
2672   eval_state ERTL_semantics
2673   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2674   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2675   (sigma_state_pc ? sigma st) =
2676    return st' →
2677    ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2678 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2679  st
2680  st''.
2681 bool_to_Prop (taaf_non_empty … taf).
2682#prog #stack_sizes #sigma #st #st' #f #fn #nxt
2683whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2684@if_elim
2685[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2686  whd in match fetch_statement; whd in match fetch_internal_function;
2687  normalize nodelta lapply(fetch_function_no_zero ??????)
2688  [2: @( «mk_block Code OZ,refl region Code»)
2689    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2690#Hbl inversion(fetch_internal_function ???)
2691[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2692   whd in match fetch_statement; whd in match fetch_internal_function;
2693  normalize nodelta lapply(fetch_function_no_zero ??????)
2694  [2: @( «mk_block Code OZ,refl region Code»)
2695    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2696* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2697#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2698>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2699#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2700@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta whd in match eval_state;
2701normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance;
2702whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
2703whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) -H
2704#H @('bind_inversion H) -H #pc' whd in match set_no_pc; normalize nodelta
2705>(pc_of_label_eq … fn1_spec) whd in ⊢ (???% → ?); #EQ whd in ⊢ (??%% → ?); #EQ1
2706destruct lapply (fetch_statement_commute … sigma … stack_sizes … EQf)
2707normalize nodelta #EQf' %
2708[ % [ @st
2709    | @(mk_program_counter
2710         (pc_block (pc ERTLptr_semantics st))
2711         (offset_of_point ERTL_semantics nxt))
2712    | @(last_pop … st)
2713    ]
2714] %
2715[ whd in match sigma_state_pc; normalize nodelta @if_elim [#H >H in Hbl; *]
2716  >fn1_spec normalize nodelta #_ % ]
2717%{(taaf_step … (taa_base …) …)}
2718[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
2719  >EQf' normalize nodelta %
2720| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
2721  >EQf' >m_return_bind whd in match eval_statement_no_pc;
2722  whd in match eval_statement_advance; normalize nodelta >m_return_bind
2723  whd in match goto; normalize nodelta whd in match pc_of_label; normalize nodelta
2724  lapply(fetch_internal_function_transf ??????? fn1_spec)
2725  [ #vars @translate_internal |] #EQ >EQ >m_return_bind %
2726| %
2727]
2728qed.
2729*)
2730
2731
2732                       
2733
2734 
2735lemma eval_return_ok :
2736∀prog : ertl_program.
2737let trans_prog ≝ ertl_to_ertlptr prog in
2738∀stack_sizes.
2739∀sigma : sigma_map trans_prog.
2740∀st,st',f,fn.
2741 fetch_statement ERTL_semantics …
2742  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2743    return 〈f, fn,  final … (RETURN ERTL … )〉 →
2744 eval_state ERTL_semantics
2745   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2746   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2747   (sigma_state_pc ? sigma st) =
2748  return st' →
2749joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)
2750  st = Some ? cl_return ∧
2751∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2752∃st2_after_ret.
2753∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2754st2_after_ret
2755st''.
2756(if taaf_non_empty … taf then
2757  ¬as_costed (ERTLptr_status trans_prog stack_sizes)
2758    st2_after_ret
2759 else True) ∧
2760eval_state … (ev_genv …  (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st =
2761return st2_after_ret ∧
2762ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes sigma) st' st2_after_ret.
2763#prog #stack_size #sigma #st #st' #f #fn
2764whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2765@if_elim
2766[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2767  whd in match fetch_statement; whd in match fetch_internal_function;
2768  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
2769  whd in ⊢ (??%% → ?); #EQ destruct ]
2770#Hbl inversion(fetch_internal_function ???)
2771[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2772   whd in match fetch_statement; whd in match fetch_internal_function;
2773  normalize nodelta lapply(fetch_function_no_zero ??????)
2774  [2: @( «mk_block Code OZ,refl region Code»)
2775    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2776* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2777#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2778>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2779#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2780@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
2781whd in match eval_state; normalize nodelta >EQf >m_return_bind
2782whd in match eval_statement_no_pc; whd in match eval_statement_advance;
2783normalize nodelta >m_return_bind
2784#H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
2785* #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta
2786>m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn1 * normalize nodelta
2787[ * [ #c_id #args #dest | #r #lbl | #seq ] #nxt | #fin | * ]
2788#EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct]
2789>m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
2790lapply (fetch_statement_commute prog sigma stack_size … EQf)
2791normalize nodelta #EQf'
2792% [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %]
2793change with (pop_ra ?? = ?) in EQpop; whd in match set_no_pc in EQpop;
2794normalize nodelta in EQpop;
2795cases(pop_ra_ok ? sigma  stack_size fn ?? EQpop) * #st3 #pc3 * #st3_spec
2796normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc;
2797normalize nodelta whd in match (point_of_succ ???);
2798 % [ % [ @st3 | @(pc_of_point ERTL_semantics (pc_block … pc3) nxt) | @pc3] ]
2799 % [  @('bind_inversion EQf1) * #f3 #fn3 whd in match sigma_stored_pc;
2800      normalize nodelta inversion(sigma_pc_opt ???) normalize nodelta
2801      [ #_ #H @('bind_inversion H) -H #x whd in match null_pc; normalize nodelta
2802        >fetch_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct
2803      | #pc4 whd in match sigma_pc_opt; normalize nodelta @if_elim
2804        [ #bl3_spec @('bind_inversion EQf1) #x #H @('bind_inversion H) -H
2805          #x1 >fetch_function_no_minus_one [ whd in ⊢ (???% → ?); #EQ destruct]
2806          lapply bl3_spec @eqZb_elim #EQ * whd in match sigma_stored_pc;
2807          normalize nodelta whd in match sigma_pc_opt; normalize nodelta
2808           >bl3_spec normalize nodelta assumption
2809        | #bl3_spec #H @('bind_inversion H) -H * #id4 #fn4
2810          #H lapply(res_eq_from_opt ??? H) -H #fn4_spec
2811          #H @('bind_inversion H) -H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ
2812          destruct #fn3_spec #H @('bind_inversion H) -H #stmt1 #_
2813          whd in ⊢ (??%% → ?); #EQ destruct
2814          >(fetch_internal_function_transf … fn3_spec) in fn4_spec;
2815          whd in ⊢ (??%% → ?); #EQ destruct
2816        ]
2817      ]
2818      whd in match sigma_state_pc; normalize nodelta @if_elim
2819      [ >(pc_block_eq prog sigma ????) in bl3_spec;
2820       [2: >lbl4_spec % #ABS destruct
2821       |3: >(fetch_internal_function_transf … fn3_spec) % |*:]
2822       #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; *
2823      | #_ cases daemon
2824      ]
2825  ] cases daemon
2826qed.
2827
2828(*
2829lemma ertl_allocate_local_ok : ∀ prog : ertl_program.
2830let trans_prog ≝ ertl_to_ertlptr prog in
2831∀sigma : sigma_map.
2832∀stack_size.
2833∀id,regs.
2834ertl_allocate_local id (sigma_regs ? sigma getLocalsFromId(
2835*)
2836
2837lemma eval_tailcall_ok :
2838∀prog.
2839let trans_prog ≝ ertl_to_ertlptr prog in
2840∀stack_sizes.
2841∀sigma : sigma_map trans_prog.
2842∀st,st',f,fn,fl,called,args.
2843 fetch_statement ERTL_semantics …
2844  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2845    return 〈f, fn,  final … (TAILCALL ERTL … fl called args)〉 →
2846 eval_state ERTL_semantics
2847   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2848   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2849   (sigma_state_pc ? sigma st) =
2850  return st' →
2851  ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2852  ∃is_tailcall, is_tailcall'.
2853  joint_tailcall_ident (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) «st, is_tailcall'» =
2854  joint_tailcall_ident (mk_prog_params ERTL_semantics prog stack_sizes) «(sigma_state_pc ? sigma st), is_tailcall» ∧
2855  eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2856    st = return st''.
2857#prog #stack_size #sigma #st #st' #f #fn #fl #called #args
2858whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2859@if_elim
2860[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2861  whd in match fetch_statement; whd in match fetch_internal_function;
2862  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
2863  whd in ⊢ (??%% → ?); #EQ destruct ]
2864#Hbl inversion(fetch_internal_function ???)
2865[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2866   whd in match fetch_statement; whd in match fetch_internal_function;
2867  normalize nodelta lapply(fetch_function_no_zero ??????)
2868  [2: @( «mk_block Code OZ,refl region Code»)
2869    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2870* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2871#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2872>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2873#EQ destruct  whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2874@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
2875whd in match eval_state; normalize nodelta >EQf >m_return_bind
2876whd in match eval_statement_no_pc; whd in match eval_statement_advance;
2877normalize nodelta >m_return_bind whd in match eval_tailcall;
2878normalize nodelta #H @('bind_inversion H) -H #bl whd in match set_no_pc;
2879normalize nodelta #bl_spec #H @('bind_inversion H) -H * #id1 * [#int_f | #ext_f] 
2880#H lapply(err_eq_from_io ????? H) -H #id1_spec normalize nodelta
2881[2: #H @('bind_inversion H) -H #st1 whd in match eval_external_call; normalize nodelta
2882    #H @('bind_inversion H) -H #l_val #_ #H @('bind_inversion H) -H #le #_
2883    #H @('bind_inversion H) -H #x whd in match do_io; normalize nodelta
2884    whd in ⊢ (???% → ?); #EQ destruct ]
2885#H lapply(err_eq_from_io ????? H) -H  #H @('bind_inversion H) -H #st1
2886whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????);
2887#H @('bind_inversion H) -H #n #H lapply(opt_eq_from_res ???? H) -H #n_spec
2888whd in match(setup_call ???????); >m_return_bind
2889whd in ⊢ (??%% → ?); #EQ destruct whd in match sigma_state in ⊢ (% → ?);
2890normalize  nodelta whd in ⊢ (??%% → ?); #EQ destruct
2891% [ %
2892    [ %
2893      [ @(st_frms ERTLptr_semantics st)
2894      | @(istack ERTLptr_semantics st)
2895      | @(carry ERTLptr_semantics st)
2896      | cases daemon
2897      | @(m ERTLptr_semantics st)
2898      ]
2899    | @(mk_program_counter bl
2900            (offset_of_point ERTL_semantics
2901              (joint_if_entry ERTL_semantics
2902                  (prog_var_names (joint_function ERTL_semantics) ℕ prog) int_f)))
2903    | @(last_pop ERTLptr_semantics st)
2904    ]
2905  ]
2906% [ whd in match sigma_state_pc; normalize nodelta @if_elim whd in match pc_of_point;
2907    normalize nodelta
2908    [ #Hbl >fetch_function_no_minus_one in id1_spec;
2909       [2: lapply Hbl @eqZb_elim -Hbl #Hbl * @Hbl] whd in ⊢ (???% → ?);
2910       #EQ destruct(EQ)
2911    ] #_ whd in match fetch_internal_function; normalize nodelta >id1_spec
2912      >m_return_bind normalize nodelta cases daemon (*TO BE COmpleted *)
2913  ] cases daemon (*TO BE COMPLETED*)
2914qed.
2915   
2916   
2917   
2918   
2919lemma as_label_ok : ∀ prog : ertl_program.
2920let trans_prog ≝ ertl_to_ertlptr prog in
2921∀ sigma : sigma_map trans_prog.
2922∀stack_sizes.
2923∀ st.
2924as_label (ERTLptr_status trans_prog stack_sizes) st = as_label
2925(ERTL_status prog stack_sizes) (sigma_state_pc prog sigma st).
2926#prog #sigma #stack_size * #st #pc #lp
2927whd in match as_label; normalize nodelta whd in match (as_pc_of ??) in ⊢ (??%%);
2928whd in match (as_label_of_pc ??) in ⊢ (??%%);
2929
2930
2931(*
2932
2933whd in match fetch_statement; normalize nodelta
2934whd in match sigma_state_pc; normalize nodelta @if_elim
2935[ #EQbl whd in match fetch_internal_function; normalize nodelta >m_bind_bind
2936 lapply(fetch_function_no_minus_one ??????) [2: @(pc_block pc) | lapply EQbl
2937 @eqZb_elim #H * @H| @(ertl_to_ertlptr prog) |7: #EQ >EQ |*:] normalize nodelta
2938 whd in match dummy_state_pc; whd in match (as_label_of_pc ??); whd in match null_pc;
2939 whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
2940 normalize nodelta >m_bind_bind
2941 lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
2942 | % | @prog |7: #EQ >EQ |*:] %
2943| inversion ( fetch_internal_function
2944     (joint_closed_internal_function ERTL
2945      (prog_var_names (joint_function ERTL) ℕ prog))
2946     (globalenv_noinit (joint_function ERTL) prog) (pc_block pc))
2947 [ * #id #fn #fn_spec #_ lapply(fetch_internal_function_transf ??????? fn_spec)
2948   [ @(λvars,fn.translate_internal … fn) |] #EQ >EQ >m_return_bind normalize nodelta
2949     whd in match (as_label_of_pc ??);
2950     whd in match fetch_statement; normalize nodelta >fn_spec >m_return_bind
2951     cases daemon (*serve specifica su sigma TODO*)
2952   | #err #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fetch_err #_ normalize nodelta
2953     whd in match dummy_state_pc;
2954     whd in match (as_label_of_pc ??); whd in match null_pc;
2955     whd in match fetch_statement; normalize nodelta
2956     whd in match fetch_internal_function in ⊢ (???%);
2957     normalize nodelta
2958     lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
2959     | % | @prog |7: #EQ >EQ in ⊢ (???%); |*:] normalize nodelta -EQ
2960     lapply fetch_err -fetch_err whd in match fetch_internal_function; normalize nodelta
2961     inversion(fetch_function ???)
2962     [* #id * #fn #fn_spec >m_return_bind normalize nodelta [whd in ⊢ (??%? → ?); #EQ destruct]
2963     #EQ destruct  lapply(jmeq_to_eq ??? fn_spec) -fn_spec #fn_spec
2964     lapply(fetch_function_transf ????????? fn_spec) [ #v  @transf_fundef [2:@translate_internal |]|]
2965     #EQ >EQ >m_return_bind %
2966   | #err1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQfetch whd in ⊢ (??%? → ?); #EQ destruct
2967     normalize nodelta lapply EQfetch -EQfetch whd in match fetch_function;
2968     normalize nodelta check joint_function
2969      lapply(symbol_for_block_transf  ? ? ? ? prog (λvars.?)  (pc_block pc))
2970      [@transf_fundef [2: @translate_internal|] |4: #EQ >EQ in ⊢ (? → %); |*:] 
2971     cases(symbol_for_block ???) [ whd in ⊢ (??%% → ?); #EQ destruct %]
2972     #id >m_return_bind inversion(find_funct_ptr ???)
2973     [2: #fn1 #_ >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct]
2974     #EQf whd in ⊢ (??%? → ?); #EQ destruct
2975     lapply(find_funct_ptr_none ??????? EQf) (*forse e' falso*)
2976     [#vars @transf_fundef [2: @translate_internal|]|]
2977     #EQ >EQ %
2978     ]
2979  ]
2980]*)
2981cases daemon
2982qed.
2983
2984lemma bool_of_beval_ok : ∀prog : ertlptr_program.
2985∀sigma : sigma_map prog.
2986preserving1 … res_preserve1 …
2987    (sigma_beval prog sigma)
2988    (λx.x)
2989    (bool_of_beval)
2990    (bool_of_beval).
2991#prog #sigma whd in match bool_of_beval; normalize nodelta
2992* normalize nodelta
2993 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
2994try @res_preserve_error1 #x
2995[1,2,3,4: whd in ⊢ (???% → ?); #EQ destruct
2996          [1,4: %{true} % //
2997          |3: %{false} % //
2998          | %{(eq_bv 8 (zero 8) by)} % //
2999          ]
3000| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
3001  normalize nodelta [2: #pc1] whd in ⊢ (???% → ?); #EQ destruct
3002]
3003qed.
3004
3005lemma eval_cond_ok :
3006∀prog.
3007let trans_prog ≝ ertl_to_ertlptr prog in
3008∀stack_sizes.
3009∀sigma : sigma_map trans_prog.
3010∀st,st',f,fn,a,ltrue,lfalse.
3011 fetch_statement ERTL_semantics …
3012  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
3013    return 〈f, fn,  sequential … (COND ERTL … a ltrue) lfalse〉 →
3014 eval_state ERTL_semantics
3015   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
3016   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
3017   (sigma_state_pc ? sigma st) =
3018  return st' →
3019as_costed (ERTL_status prog stack_sizes)
3020  st' →
3021∃ st''. st' = sigma_state_pc ? sigma st'' ∧
3022∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
3023st st''.
3024bool_to_Prop (taaf_non_empty … taf).
3025#prog #stack_size #sigma #st #st' #f #fn #a #lb_t #lb_f
3026whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
3027@if_elim
3028[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
3029  whd in match fetch_statement; whd in match fetch_internal_function;
3030  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
3031  whd in ⊢ (??%% → ?); #EQ destruct ]
3032#Hbl inversion(fetch_internal_function ???)
3033[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
3034   whd in match fetch_statement; whd in match fetch_internal_function;
3035  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
3036 whd in ⊢ (??%% → ?); #EQ destruct]
3037* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
3038#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
3039>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
3040#EQ destruct whd in match eval_state; whd in match eval_statement_no_pc;
3041whd in match eval_statement_advance; whd in match sigma_state_pc in ⊢ (% → ?);
3042normalize nodelta @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
3043>EQf >m_return_bind normalize nodelta >m_return_bind
3044#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv
3045change with (ps_reg_retrieve ?? = ? → ?) whd in match set_no_pc;
3046whd in match sigma_state in ⊢ (??(?%?)? → ?); normalize nodelta #bv_spec
3047#H @('bind_inversion H) -H * #EQbv normalize nodelta
3048[ whd in match goto; normalize nodelta >pc_of_label_eq [2: assumption |3:]
3049  >m_return_bind whd in match pc_of_point; normalize nodelta whd in ⊢ (??%% → ?);
3050  whd in match set_pc; normalize nodelta #EQ destruct
3051| whd in match next; whd in match set_pc; normalize nodelta whd in match (succ_pc ???);
3052  whd in match (point_of_succ ???); whd in ⊢ (??%% → ?); #EQ destruct
3053]
3054whd in match as_costed; normalize nodelta * #n_cost %
3055[1,3: % [1,4: @st
3056        |2,5: @(mk_program_counter
3057                  (pc_block (pc ERTLptr_semantics st))
3058                  (offset_of_point ERTL_semantics ?)) [ @lb_t | @lb_f]
3059        |3,6: @(last_pop ? st)
3060        ]
3061]
3062% [1,3: whd in match sigma_state_pc; normalize nodelta @if_elim
3063       [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %]
3064%{(taaf_step_jump … (taa_base …) …) I}
3065lapply (fetch_statement_commute prog sigma … stack_size … EQf)
3066normalize nodelta #EQf'
3067[1,4: whd in match as_costed; normalize nodelta >as_label_ok [2,4: @sigma]
3068      % #H @n_cost <H whd in match sigma_state_pc; normalize nodelta
3069      @if_elim [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %
3070|2,5: whd in match as_classifier; normalize nodelta  whd in match (as_classify ??);
3071      normalize nodelta >EQf' %
3072|*:  whd in match (as_execute ???); whd in match eval_state; normalize nodelta
3073     >EQf' >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
3074     >m_return_bind whd in match eval_statement_advance; normalize nodelta 
3075     change with (ps_reg_retrieve ??) in ⊢ (??(????(????%?))?);
3076     cases(ps_reg_retrieve_ok ????? ? bv_spec) #bv' * #bv_spec' #bv_bv'
3077     >bv_spec' >m_return_bind >bv_bv' in EQbv; #EQbv
3078     cases(bool_of_beval_ok ? sigma ? ? EQbv) #b1 * #b1_spec #EQ destruct
3079     >b1_spec >m_return_bind normalize nodelta [2: %] whd in match goto;
3080     normalize nodelta whd in match set_no_pc; normalize nodelta
3081     >pc_of_label_eq
3082     [ %
3083     | lapply(fetch_internal_function_transf ????????)
3084       [3: @f |2: @fn | whd in ⊢ (???%); <fn1_spec in ⊢ (???%); %
3085       | | #vars @translate_internal |9: #EQ >EQ in ⊢ (??%?); % |*:]
3086       |
3087     ]
3088]
3089qed.
3090       
3091
3092lemma
3093  find_funct_ptr_none:
3094    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
3095    ∀b: block.
3096    find_funct_ptr ? (globalenv … iV p) b = None ? →
3097    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?.
3098#A #B #V #i #p #transf #b
3099whd in match find_funct_ptr; normalize nodelta
3100cases b -b * normalize nodelta [#x #_ %] * normalize nodelta
3101[1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta
3102whd in match globalenv_allocmem; normalize nodelta
3103cases daemon (*forse e' falso *)
3104qed.
3105
3106
3107
3108
3109
3110
3111
Note: See TracBrowser for help on using the repository browser.