proofs of source-target translation


========================================================================
tranlation of types

Lemma [transTy]
if (1) ||GS, V, sz, f|| = (D,H,G,S,_), 
   (2) GS |- v: t *s, t != t' *S
then (3) ||t *S, G, S, V, v|| = single(l') and
     (4) S |- l' : ||t||

Proof:
By type rules of values, v must be a variable x.
By translation rules of t *S, ||t *S, G, S, V, x|| = t' where G(r_fp) = single(l) and 
S |- l + V(x) : t'.
By [transEnv], t' = single(l+V(x)-1) and S |- l+V(x)-1 : ||t||.


Lemma [funTy]
If (1) GS(f') = (t1, ..., tn) -> t
   (2) ||GS, V, 0, f|| = (D,H,G,S,_)
then (3) H(p_f') = ||(t1, ..., tn)->t||

Proof: by translation rule of environments.

========================================================================
instantiation of locations

Lemma [ins-id]
if D;H;G |- o: All[D](G,S), then D;H;G |-o[D]: All[](G,S)

Proof: by o-inst-l and o-inst-Q

========================================================================
translation of values

Lemma [transV]
If (1) ||GS |- v:t|| V r = I_v, 
   (2) ||GS, V, sz, f|| = (D,H,G,S,l),
   (3) G' supersetof G. r not in domain(G'), r != sp,
   (4) D;H';G'[r->t'];S |- b where t' = ||t,G,S,V,v|| 
       and H' supersetof H
then (5) D;H';G';S |- I_v; b

Proof:
case n:
******

t = int,
I_v = mov r, n
t' = int
                                              
------- (o-int)   ----------------- (a-not-esp)   
D;H';G' |- n:int  |- (G';S){r<-int}(G'[r->int];S) (4) D;H';G'[r->int];S |- b
-------------------------------------------------------- (i-mov & b-ins)
(5) D;H';G';S |- mov r, n; b

case x:
******

t = GS(x)
I_v = (mov r, r_fp; ladd r, -4*V(x); load r, [r+0])

From [transEnv], exists l0 such that 
(6) G(r_fp) = single(l0),
(7) S |- l0 + V(x) = l_x, and
(8) S |- l_x: t'

D;H';G'[r->single(l_x)] |- r:single(l_x)  from (o-reg)
(8) S |- l_x : t'
|- (G'[r->single(l_x), S]{r<-t'}{G'[r->t'],S}  from (a-not-esp)
(4) D;H';G'[r->t'];S |- b 
---------------------------------------- (i-load-aliased & b-ins)
D;H';G'[r->single(l_x)]; S |- load r, [r+0]; b
(6) G'(r_fp) = single(l0) 
(7) S |- l0+V(x) = l_x from [transEnv]   
|- (G'[r->G(r_fp)];S){r<-single(l_x)}(G'[r<-single(l_x)],S) from (a-not-esp)
-------------------------------------------------------- (i-ladd & b-ins)
D;H';G'[r->G'(r_fp)];S |- ladd r, -4* V(x); load r, [r+0]; b
D;H';G' |- r_fp:G'(r_fp) from (o-reg) 
|-(G';S){r<-G'(r_fp)}(G'[r->G'(r_fp)];S) from (a-not-esp)
-------------------------------------------------------- (i-mov & b-ins)
(5) D;H';G';S |- mov r, r_fp; ladd r, -4*V(x); load r, [r+0]; b

========================================================================
translation of local declarations

Lemma [transLd]
If (1) ||GS |- ld: GS'|| V sz = (V', sz', I_ld)
  and (2) ||GS, V, sz, f|| = (D, H, G, S, l)
  and (3) ||GS', V', sz', f|| = (D1, H1, G1, S1, _)

then forall b, forall H0, if D1;(H1,H0);G1;S1 |- b 
       then D;(H,H0);G;S |- I_ld; b  

Proof:

case trans-ld-v:
***************
ld = (t x = v)
GS' = GS[x:t]
V' = V[x->sz+1]
sz' = sz+1
I_ld = (I; push r1)
||GS |- v:t|| V r1 = I

Let t' = ||t, G, S, V, v||

By translation rules of environments transEnv,
D1 = D, H1 = H, G1 = G[sp->single(next(l))],
S1 = next(l):t'::S

D;(H,H0);G1;S1 |- b from premise    r1 not in domain(G1) from [transEnv]
----------------------------------------------------------- (RegFile-Weakening)
D;(H,H0);G1[r1->t'];S1 |- b           G[r1->t'](r1) = t'
-------------------------------------------------- ([push])
D;(H,H0);G[r1->t'];S |- push r1; b
||GS |- v:t|| V r1 = I
(2) ||GS, V, sz, f|| = (D, H, G, S, _)
--------------------------------------------- ([transV])
D;(H,H0);G;S |- I; push r1; b
----------------------------------------------- (if-introduction)
if D1;(H1,H0);G1;S1 |- b, then D;(H,H0);G;S |- I_ld; b


case trans-ld-s:
***************
lds = (t x = new_S v)
GS' = GS[x:t]
V' = V[x->sz+2]
sz' = sz+2
I_ld = I; push r1; mov r2, sp; push r2
t = t' *S
||GS |- v:t'|| V r1 = I

Let t" = ||t', G, S, V, v||

By translation rules of environments transEnv,
D1 = D, H1 = H, G1 = G[sp->Next(l,2)], 
S1 = Next(l,2):single(next(l))::next(l):t'::S


D1;(H1,H0);G1;S1 |- b   r1, r2 not in domain(G1) from [transEnv]
------------------------------------------ (RegFile-Weakening)
D;(H,H0);G1[r1->t",r2->single(next(l))];S1 |- b
G[r1->t",r2->single(next(l)),sp->single(next(l))](r2) = singel(next(l))
----------------------------------------------------------------------- ([push])
D;(H,H0);G[r1->t",r2->single(next(l)),sp->single(next(l))];next(l):t'::S
  |- push r2; b
D;(H,H0);G[r1->t",sp->single(next(l))] |- sp: single(next(l))
|- (G[r1->t",sp->single(next(l))],next(l):t'::S){r2<-single(next(l))}
  (G[r1->t",r2->single(next(l)),sp->single(next(l))],next(l):t'::S)
----------------------------------------------------------------- (i-mov & b-ins)
D;(H,H0);G[r1->t",sp->single(next(l)];next(l):t'::S |- mov r2,sp;push r2;b
G[r1->t"](r1) = t"
------------------------------------------------- ([push])
D;(H,H0);G[r1->t"];S |- push r1; mov r2, sp; push r2; b
||GS |- v:t'|| V r1 = I
(2) ||GS, V, sz, f|| = (D, H, G, S, _)
----------------------------------------------- ([transV])
D;(H,H0);G;S |- I; push r1; mov r2, sp; push r2; b
----------------------------------------------- (if-introduction)
if D1;(H1,H0);G1;S1 |- b, then D;(H,H0);G;S |- I_ld; b


case trans-ld-h:
***************
ld = (t x = new_H v)
GS' = GS[x:t]
V' = V[x->sz+1]
sz' = sz+1
I_ld = (I; heapalloc r1 = <r1>; push r1)
t = t' *H
||GS |- v:t'|| V r1 = I

Let t" = ||t', G, S, V, v||

By translation rules of environments transEnv,
D1 = D, H1 = H, G1 = G[sp->single(next(l))],
S1 = next(l):HeapPtr(t")::S

D;(H,H0);G1;S1 |- b from premise    r1 not in domain(G1) from [transEnv]
----------------------------------------------------------- (RegFile-Weakening)
D;(H,H0);G1[r1->HeapPtr(t')];S1 |- b     
G[r1->HeapPtr(t")](r1) = HeapPtr(t")
-------------------------------------------------- ([push])
D;(H,H0);G[r1->HeapPtr(t")];S |- push r1; b
D;(H,H0);G[r1->t"] |- r1: t"
|-(G[r1->t"]S){r1<-HeapPtr(t")}(G[r1->HeapPtr(t")],S)
--------------------------------------------------- ([i-heapalloc])
D;(H,H0);G[r1->t"];S |- heapalloc r1 = <r1>; push r1; b
||GS |- v:t'|| V r1 = I
(2) ||GS, V, sz, f|| = (D, H, G, S, _)
--------------------------------------------- ([transV])
D;(H,H0);G;S |- I; heapalloc r1 = <r1>; push r1; b
----------------------------------------------- (if-introduction)
if D1;(H1,H0);G1;S1 |- b, then D;(H,H0);G;S |- I_ld; b


========================================================================
translation of environments

Lemma [transEnv]
If ||GS, V, sz, f|| L P = (D, H, G, S) and GS(f) = (t1, ..., tn) -> t
then (1) r1, r2 not in domain(G)
     (2) G(r_fp) = Next(L, n) if sz>0
     (3) forall x in domain(V), if GS |- x : t, then
          S |- Next(L,n)+V(x) = l_x,
         then S |- l_x : ||t, G, S, V, x||
     (4) . |- All[D](G,S)
     (5) G(sp) = Next(L, sz+n)
     (6) G(r_ra) = All[](G_ra, S_ra) where
         G_ra = sp->single(next(L)) and
         S_ra = next(L):||t||::L:Q
     (7) if GS(f') = t_f' then H(p_f') = ||t_f'||
     (8) size(S) = Next(L, sz+n)
Proof: (1), (2), (5), (6), and (7): by insepction of translation rules of environments
      (3), (4), and (8) by induction on translation rules of environments


========================================================================
translation of arguments

Lemma [transArgs]

If (1) ||GS |- v:t|| V r1 l l0 = (Is, sub), 
   (2) ||GS, V, sz, f|| L P = (D,H,G,S)
   (3) G(sp) = single(l), l0 + sz = l
   (4) D;H;G[sp->next(l)];next(l):t_0 :: S |- b where t_0 = ||t, G, S, V,v||
then (5) D;H;G;S |- Is; b

Proof:


case 1: t != t" *S and Is = I; push r1
and (7) ||GS |- v:t|| V r1 = I

(4) D;H;G[sp->next(l)];next(l):t_0 :: S |- b
---------------------------------------------- (RegFile-Weakening)
D;H;G[r1->t_0,esp->single(next(l))];next(l):t_0::S |- b
------------------------------------------------(push)
D;H;G[r1->t_0];S |- push r1; b
--------------------------(transV)
(5) D;H;G;S |- Is; b

case 2: t = t' *S, v = x, Is = (I; I', push r1)
and (7) ||GS |- x:GS(x)|| V r1 = I
and (8) ||GS(x)|| (t' *S) x V l0 f r1 = (I', sub)

Let t_0' = ||GS(x), G, S, V, x||,

(4) D;H;G[sp->next(l)];next(l):t_0 :: S |- b
--------------------------------------- (RegFile-Weakening)
D;H;G[r1->t_0, sp->next(l)];next(l):t_0::S |- b
------------------------------------- (push)
D;H;G[r1->t_0];S |- push r1; b
(8) ||GS(x)|| (t' *S) x V l0 f r1 = (I', sub)
---------------------------------(transArgTy)
D;H;G[r1->t_0'];S |- I'; push r1; b
--------------------------(transV)
(5) D;H;G;S |- Is; b


========================================================================
update 

Lemma [update-x]
If (1) GS |- x:t and t != t' *S, 
   (2) ||GS, V, sz, f|| = (D,H,G,S,l),
   (3) D;H';G[r1->||t||];s |- b and H' supersetof H 
then (4) D;H';G[r1->||t||];S |- update x; b

Proof:

By [transEnv], G(r_fp) = single(l0) and S |- l0 + V(x) = l_x
and S |- l_x :

Let G1 = G[r1->||t||] and G2 = G1[r2->G(r_fp)] and G3 = G1[r2->single(l_x)]

--------------- (o-reg)        ------------------ (a-not-esp)
D;H';G1 |- r_fp:G(r_fp)        |-(G1;S){r2<-G(r_fp)}(G2;S)
(5) D;H';G2;S |- ladd r2, -4*V(x); store [r2+0], r1; b
-------------------------------------------------------- (i-mov & b-ins)
(4) D;H';G1;S |- mov r2, r_fp; ladd r2, -4*V(x); store [r2+0], r1; b


----------- (o-reg)                       ----------------- (a-not-esp)
D;G2;S|-r2:single(l0)  S|- l0+V(x) = l_x  |-(G2;S){r2<-single(l_x)}(G3;S)
(6) D;H';G3:S |- store [r2+0],r1; b
------------------------------------------------------- (i-ladd & b-ins)
(5) D;H';G2;S |- ladd r2, -4*V(x); store [r2+0], r1; b

                                                  (2) D;H';G1 |-b
                                                   --------- (RegFile-Weakening)
G3(r2)=single(l_x)  S |- l_x:||t||  G3(r1) = ||t||  D;H';G3;t |- b
----------------------------------------------- (i-store-aliased & b-ins)
(6) D;H';G3:S |- store [r2+0],r1; b

========================================================================
push

Lemma [push]
If (1) D;H;G[sp->single(next(l))];next(l):G(r) :: S|- b,
   (2) S = l:Q
   (3) G(sp) = single(l)
then (4) D;H;G;S |- push r; b

Proof:

(1)D;H;G[sp->single(next(l)];next(l):G(r)::S |- b
G[sp->single(next(l))](sp) = single(next(l)) 
next(l):Nonsense::S |- next(l) : Nonsense  from (s-lookup) & (s-imp-add-alias)
next(l):Nonsense::S |- next(l) + 0 : next(l) from (s-offset-next) & (s-imp-eq)
next(l):Nonsense::S |- next(l) <- G(r) ~~> next(l):G(r)::S  
    from (s-update-strong) & (s-imp-eq)
--------------------------------------------------- (i-store-concat & b-ins)
D;H;G[sp->single(next(l))];next(l):Nonsense::S |- store [sp], r; b
D;H;G |- sp:single(l) from (o-reg)   S |- l+1 : next(l) from (s-offset-next)
|-(G;S){sp<-single(next(l))}(G[sp->single(next(l))],next(l):Nonsense::S)
----------------------------------------- (i-ladd & b-ins)
D;H;G;S |- ladd sp, -4; store [sp], r; b

=========================================================================
pop

Lemma [pop]
If (1) D;H;G[sp->single(l), r->t];S |- b,  S = l:Q
   (2) r != sp, r not in domain(G)
then D;H;G';S' |- pop r;b where G'=G[sp->single(next(l))] and S'=next(l):t::S

Proof:

S' => next(l):t::S from (s-imp-eq)
----------------------------- (S-shrink)
|- Resize(single(l),S') = S
----------------------------------------------------------- (a-sp)
(3) |-(G'[r->t];S'){sp<-single(l)}(G[sp->single(l),r->t];S)
(1) D;H;G[sp->single(l), r->t];S |- b
G'[r->t](sp) = single(next(l))
S |- next(l) - 1 = l   from (s-offset-prev) & (s-imp-eq)
-------------------------------------------------- (i-ladd & b-ins)
D;H;G'[r->t];S' |- ladd sp, 4; b
G'(sp) =single(next(l))
S' |- next(l) : t      from (s-lookup) and (s-imp-add-alias)
|- (G',S'){r<-t}(G'[r->t], S')    from (a-not-esp)
--------------------------------------------------- (i-load-aliased & b-ins)
D;H;G';S' |- load r,[sp]; ladd sp,4; b

========================================================================
translation of statements

Lemma [transS]
If (1) ||GS |- st|| V sz f C0 H1 cb I = (C1, H2, cb', I')
  and (2) |- C0 : H1\cb
  and (3) ||GS, V, sz, f|| L P = (D, H, G, S)
  and (4) H1(cb) = All[D1](G1, S1) and H2(cb') = All[D2](G2, S2)
  and (5) forall b, forall H0, let H' = (H, H0) and H1' = (H1, H0),
          if D;H';G;S |- b then D1;H1';G1;S1 |- I; b  
then (6) |- C1 : H2\cb'
  and (7) forall b, forall H0, let H' = (H, H0) and H2' = (H2, H0),
         if D;H';G;S |- b then D2;H2';G2;S2 |- I'; b
  and (8) C0 subsetof C1 and H1 subsetof H2

Proof:

case trans-mov:
**************

st = (x = v),
C1 = C0,
H2 = H1,
cb' = cb,
D1 = D2, G1 = G2, and S1 = S2,
I' = I; I_v; update x,
(9) GS |- x: t,
(10) ||GS |- v: t|| V r1 = I_v
(11) t != t' *S

(6) |- C1 : H2\cb' from (2) |- C0 : H1\cb

                             (3) ||GS, V, sz, f|| L P = (D, H, G, S)
                             ------------------------ ([transEnv])
D; H'; G; S |- b (premise)     r1, r2 not in domain(G)
------------------------------------------------ (RegFile-Weakening)
D; H'; G[r1->||t||]; S |- b
(9) GS |- x:t  (11) t != t' *S  (3) ||GS, V, sz, f|| L P = (D, H, G, S)
--------------------------------------------------------------- ([update-x])
D; H'; G[r1->||t||]; S |- update x; b
(10) ||GS |- v: t|| V r1 = I_v  (3) ||GS, V, sz, f|| L P = (D, H, G, S)
--------------------------------------------------------------- ([transV])
D; H'; G; S |- I_v; update x; b
-------------------------------- (5)
D1; H1'; G1; S1 |- I; I_v; update x; b
---------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b


(8) C0 subsetof C0 and H1 subsetof H1.

case trans-add:
**************

st = (x = v1 + v2),
C1 = C0,
H2 = H1,
cb' = cb,
D1 = D2, G1 = G2, and S1 = S2,
I' = I; I_v1; I_v2; add r1, r2; update x
(9) GS |- x: int,
(10) ||GS |- v1: int|| V r1 = I_v1
(11) ||GS |- v2: int|| V r2 = I_v2

(6) |- C1 : H2\cb' from (2) |- C0 : H1\cb

                             (3) ||GS, V, sz, f|| L P = (D, H, G, S)
                             ------------------------------ ([transEnv])
D; H'; G; S |- b (premise)     r1, r2 not in domain(G)
------------------------------------------------ (RegFile-Weakening)
D; H'; G[r1->int]; S |- b      
(9) GS |- x: int   (3) ||GS, V, sz, f|| L P = (D, H, G, S)
-------------------------------------------([update-x])
D; H'; G[r1->int]; S |- update x; b                      r2 not in domain(G)
------------------------------------------- (RegFile-Weakening) 
D; H'; G[r1->int, r2->int]; S |- update x; b
D;H';G[r1->int,r2->int] |- r2:int from (o-reg)
r1 != sp     G[r1->int,r2->int](r1) = int
---------------------------------------------- (i-add & b-ins)
D; H'; G[r1->int, r2->int]; S |- add r1, r2; update x; b
(10) ||GS |- v2: int|| V r2 = I_v2
(3) ||GS, V, sz, f|| L P = (D, H, G, S)
G[r1->int] supersetof G  and r2 not in domain(G[r1->int])
----------------------------------------------------- ([transV])
D; H'; G[r1->int]; S |- I_v2; add r1, r2; update x; b
(10) ||GS |- v1: int|| V r1 = I_v1
(3) ||GS, V, sz, f|| L P = (D, H, G, S)
r1 not in domain(G)
---------------------------------------------- ([transV])
D; H'; G; S |- I_v1; I_v2; add r1, r2; update x; b
-------------------------------------------------- (5)
D1; H1'; G1; S1 |- I; I_v1; I_v2; add r1, r2; update x; b
---------------------------------------------- (if-introduction)
(7) forall b,forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b

(8) C0 subsetof C0 and H1 subsetof H1.


case trans-sub: similar to trans-add


case trans-deref:
****************

st = (x = !v),
C1 = C0,
H2 = H1,
cb' = cb,
D1 = D2, G1 = G2, and S1 = S2,
I' = I; I_v; load r1, [r1]; update x
(9) GS |- x: t,
(10) ||GS |- v: t *q|| V r1 = I_v
(11) t != t' *S


(6) |- C1 : H2\cb' from (2) |- C0 : H1\cb


if (10-H) ||GS |- v: t *H|| V r1 = I_v:

                             (3) ||GS, V, sz, f|| L P = (D, H, G, S)
                             ------------------------------ (transEnv (1))
D; H'; G; S |- b (premise)     r1 not in domain(G)
------------------------------------------------ (RegFile-Weakening)
D; H'; G[r1->||t||]; S |- b
(9) GS |- x: t    (11) t != t' *S
(3) ||GS, V, sz, f|| L P = (D, H, G, S)
----------------------([update-x])
D; H'; G[r1->||t||]; S |- update x; b
G[r1->||t*H||](r1) = HeapPtr(||t||)   from translation of types
|-(G[r1->||t*H||], S){r1<-||t||}(G[r1->||t||],S) from (a-not-esp)
---------------------------------------------- (i-load-p & b-ins)
D; H'; G[r1->||t *H||]; S |- load r1, [r1]; update x; b
(10-H) ||GS |- v: t *H|| V r1 = I_v
(3) ||GS, V, sz, f|| L P= (D, H, G, S)
r1 not in domain(G)
---------------------------------------------- (transV)
D; H'; G; S |- I_v; load r1, [r1]; update x; b
-------------------------------------------------- (5)
D1; H1'; G1; S1 |- I; I_v; load r1, [r1]; update x; b
---------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b


if (10-S) ||GS |- v: t *S|| V r1 = I_v:
Let t' = ||t *S, G, S, V, v|| 

                             (3) ||GS, V, sz, f|| L P = (D, H, G, S)
                             ------------------------------ (transEnv (1))
D; H'; G; S |- b (premise)     r1 not in domain(G)
------------------------------------------------ (RegFile-Weakening)
D; H'; G[r1->||t||]; S |- b
(9) GS |- x: t    (11) t != t' *S
(3) ||GS, V, sz, f|| L P = (D, H, G, S)
----------------------([update-x])
D; H'; G[r1->||t||]; S |- update x; b
G[r1->t'](r1) = single(l')    S |- l':||t||  from [transTy]
|-(G[r1->t'], S){r1<-||t||}(G[r1->||t||],S) from (a-not-esp)
---------------------------------------------- (i-load-aliased & b-ins)
D; H'; G[r1->t']; S |- load r1, [r1]; update x; b
(10-S ) ||GS |- v: t *S|| V r1 = I_v
(3) ||GS, V, sz, f|| L P= (D, H, G, S)
r1 not in domain(G)
---------------------------------------------- (transV)
D; H'; G; S |- I_v; load r1, [r1]; update x; b
-------------------------------------------------- (5)
D1; H1'; G1; S1 |- I; I_v; load r1, [r1]; update x; b
---------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b


C0 subsetof C0 and H1 subsetof H1.


case trans-assign:
*****************

st = (v1 := v2),
C1 = C0,
H2 = H1,
cb' = cb,
D1 = D2, G1 = G2, and S1 = S2,
I' = I; I1; I2; store [r1], r2
(10) ||GS |- v1: t *q|| V r1 = I1
(12) ||GS |- v2: t|| V r2 = I2
(13) t != t' *S


(6) |- C1 : H2\cb' from (2) |- C0 : H1\cb


(10-H) ||GS |- v1: t *H|| V r1 = I1


                             (3) ||GS, V, sz, f|| L P = (D, H, G, S)
                             ------------------------------ (transEnv (1))
D; H'; G; S |- b (premise)     r1, r2 not in domain(G)
------------------------------------------------ (RegFile-Weakening)
D; H'; G[r1->||t *H||, r2->||t||]; S |- b
G[r1->||t *H||, r2->||t||](r1) = ||t *H|| = HeapPtr(||t||)
G[r1->||t *H||, r2->||t||](r2) = ||t||    
---------------------------------------------- (i-store-p & b-ins)
D; H'; G[r1->||t *H||, r2->||t||]; S |- store [r1], r2; b
(12) ||GS |- v2: t|| V r2 = I2    
G[r1->||t *H||] supersetof G and r1 not in domain (G)
(3) ||GS, V, sz, f|| L P = (D, H, G, S)   r2 not in domain(G)
------------------------------------------------------------------- (transV)
D; H'; G[r1->||t *H||]; S |- I2; store [r1], r2; b
(10-H) ||GS |- v1: t *H|| V r1 = I1
(3) ||GS, V, sz, f|| L P= (D, H, G, S)   r1 not in domain(G)
----------------------------------------------------- (transV)
D; H'; G; S |- I1; I2; store [r1], r2; b
---------------------------------------------- (5)
D1; H1'; G1; S1 |- I; I1; I2; store [r1], r2; b
---------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b



(10-S) ||GS |- v1: t *S|| V r1 = I1
Let t' = || t *S, G, S, V, v1||


                             (3) ||GS, V, sz, f|| L P = (D, H, G, S)
                             ------------------------------ (transEnv (1))
D; H'; G; S |- b (premise)     r1, r2 not in domain(G)
------------------------------------------------ (RegFile-Weakening)
D; H'; G[r1->t', r2->||t||]; S |- b
G[r1->t', r2->||t||](r1) = t'= single(l') and S |- l' : ||t|| from [transTy]
G[r1->t', r2->||t||](r2) = ||t||    
---------------------------------------------- (i-store-aliased & b-ins)
D; H'; G[r1->t', r2->||t||]; S |- store [r1], r2; b
(12) ||GS |- v2: t|| V r2 = I2    
G[r1->t'] supersetof G and r1 not in domain (G)
(3) ||GS, V, sz, f|| L P = (D, H, G, S)   r2 not in domain(G)
------------------------------------------------------------------- (transV)
D; H'; G[r1->t']; S |- I2; store [r1], r2; b
(10-H) ||GS |- v1: t *S|| V r1 = I1
(3) ||GS, V, sz, f|| L P = (D, H, G, S)   r1 not in domain(G)
----------------------------------------------------- (transV)
D; H'; G; S |- I1; I2; store [r1], r2; b
---------------------------------------------- (5)
D1; H1'; G1; S1 |- I; I1; I2; store [r1], r2; b
---------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b

C0 subsetof C0 and H1 subsetof H1.


case trans-if:
*************

st = (if v then sts1 else sts2),
C1 = (C_t \/ C_f), cb_t->All[D](G,S)(I_t; jump cb_cont[D]),
                   cb_f->All[D](G,S)(I_f; jump cb_cont[D]),
                   cb ->All[D1](G1,S1)(I; I_v; jumpif0 r1, cb_f[D]; 
                                       jump cb_t[D])
H2 = (H_t \/ H_f), cb_cont->All[D](G,S)
cb' = cb_cont,
D2 = D, G2 = G, and S2 = S,
I' = emptyset
(9) ||GS |- v: int|| V r1 = I_v
(11) ||GS |- sts1|| V sz f C0 (H1, cb_t->All[D](G,S)) cb_t emptyset = 
      (C_t, H_t, cb_t, I_t)
(12) ||GS |- sts2|| V sz f C0 (H1, cb_f->All[D](G,S)) cb_f emptyset = 
      (C_f, H_f, cb_f, I_f)



(13) |- C_t:H_t\cb_t  (14) |- C_f:H_f\cb_f 
(15) .;H2 |- All[D](G,S)(I_t; jump cb_cont[D]) : H_t(cb_t)
(16) .;H2 |- All[D](G,S)(I_f; jump cb_cont[D]) : H_f(cb_f)
(17) .;H2 |- All[D1](G1,S1)(I; I_v; jumpif0 r1, cb_f[D]; 
                                    jump cb_t[D]) 
                    : (H_t \/ H_f)(cb)
--------------------------------------------------------- (h-tp)
|- (C_t \/ C_f), cb_t->All[D](G,S)(I_t; jump cb_cont[D]),
                 cb_f->All[D](G,S)(I_f; jump cb_cont[D]),
                 cb->All[D1](G1,S1)(I; I_v; jumpif0 r1, cb_f[D]; 
                                    jump cb_t[D]) : H_t \/ H_f
----------------------------------------------------- (definition)
(6) |- C1 : H2\cb'

By induction hypothesis and
(11) ||GS |- sts1|| V sz f C0 (H1, cb_t->All[D](G,S)) cb_t emptyset = 
      (C_t, H_t, cb_t, I_t)
(2) |- C0 : H1, and
forall b, forall H0, if D;(H,H0);G;S |- b then D;(H,H0);G;S |- emptyset;b 
     from emptyset;b = b,
we have (13) |- C_t:H_t\cb_t
        (18) forall b, forall H0, if D;(H,H0);G;S |- b, then D;(H_t,H0);G;S |- I_t;b
        (19) C0 subsetof C_t
        (20) (H1, cb_t->All[D](G,S)) subsetof H_t


By induction hypothesis and
(12) ||GS |- sts2|| V sz f C0 (H1, cb_f->All[D](G,S)) cb_f emptyset = 
      (C_f, H_f, cb_f, I_f)
(2) |- C0 : H1, and
forall b, forall H0, if D;(H,H0);G;S |- b then D;(H,H0);G;S |- emptyset;b 
      from emptyset;b = b,
we have (14) |- C_f:H_f\cb_f  
        (21) forall b, forall H0, if D;(H,H0);G;S |- b, then D;(H_f,H0);G;S |- I_f;b
        (22) C0 subsetof C_f
        (23) (H1, cb_f->All[D](G,S)) subsetof H_f


(24) D;(H, cb_cont->All[D](G,S));G;S |- jump cb_cont[D]
-------------------------- (18)
D;(H_t,cb_cont->All[D](G,S));G;S |- I_t; jump cb_cont[D]
-------------------------- (h-weakening)
D;H2;G;S |- I_t; jump cb_cont[D]
-------------------------------------- (block-tp)   --- ([transEnv])
H2 |- All[D](G,S)(I_t; jump cb_cont[D])             . |- All[D](G,S)
---------------------------------------------------------- (v-code)
.;H2 |- All[D](G,S)(I_t; jump cb_cont[D]) : All[D](G,S)
-------------------------------------------------------------------
(15) .;H2 |- All[D](G,S)(I_t; jump cb_cont[D]) : H_t(cb_t)


-------------------------------------------- (o-p-H)
D;(H,cb_cont->All[D](G,S));G |- cb_cont : All[D](G,S)
-------------------------------------------- ([ins-id])
D;(H,cb_cont->All[D](G,S));G |- cb_cont[D] : All[](G,S)
G => G from (g-imp)      S => S from (s-imp-eq)
--------------------------------------------- (b-jump)
(24) D;(H,cb_cont->All[D](G,S));G;S |- jump cb_cont[D]



(24) D;(H,cb_cont->All[D](G,S));G;S |- jump cb_cont[D]
--------------------------------------------------- (21)
D;(H_f,cb_cont->All[D](G,S));G;S |- I_f; jump cb_cont[D]
-------------------------- (h-weakening)
D;H2;G;S |- I_f; jump cb_cont[D]
-------------------------------------- (block-tp)   --- ([transEnv])
H2 |- All[D](G,S)(I_f; jump cb_cont[D])            . |- All[D](G,S)
---------------------------------------------------------- (v-code)
.;H2 |- All[D](G,S)(I_f; jump cb_cont[D]) : All[D](G,S)
-------------------------------------------------------------------
(16) .;H2 |- All[D](G,S)(I_f; jump cb_cont[D]) : H_f(cb_f)


Let H1_tf = (H1, cb_t->All[D](G,S), cb_f->All[D](G,S)) and
    H_tf = (H, cb_t->All[D](G,S), cb_f->All[D](G,S)).
Then H1_tf subsetof H2 from (H1, cb_t->All[D](G,S)) subsetof H_t and
(H1, cb_f->All[D](G,S)) subsetof H_f


                      ------------------------- (o-p-H)
                      D;H_tf;G[r1->int] |- cb_f : All[D](G,S)
                      ------------------------------ [ins-id]
G[r1->int](r1) = int  D;H_tf;G[r1->int] |- cb_f[D]: All[](G,S)
G[r1->int] => G from g-imp     S => S from s-imp-id
(18) D;H_tf;G[r1->int];S |- jump cb_t[D]
------------------------------------------------------ (i-jumpif0)
D;H_tf;G[r1->int];S |- jumpif0 r1, cb_f[D]; jump cb_t[D]
(9) ||GS |- v: int|| V r1 = I_v
(3) ||GS, V, sz, f|| L P = (D, H, G, S)
r1 not in domain(G) from transEnv and (3)
------------------------------------------------ (transV)
D;H_tf;G;S |- I_v; jumpif0 r1, cb_f[D]; jump cb_t[D]
-------------------------------------------------- (5)
D1;H1_tf;G1;S1 |- I; I_v; jumpif0 r1, cb_f[D]; jump cb_t[D]
--------------------------------------------------- (h-weakening)
D1;H2;G1;S1 |- I; I_v; jumpif0 r1, cb_f[D]; jump cb_t[D]
--------------------------------------------------------------- (block-tp)
.;H2 |- All[D1](G1,S1)(I; I_v; jumpif0 r1, cb_f[D]; jump cb_t[D])
.|- All[D1](G1,S1)
----------------------------------------------------------- (v-code)
.;H2 |- All[D1](G1,S1)(I; I_v; jumpif0 r1, cb_f[D]; jump cb_t[D])
        : All[D1](G1, S1)
------------------------------------------------------------ 
(17) .;H2 |- All[D1](G1,S1)(I; I_v; jumpif0 r1, cb_f[D]; jump cb_t[D]) 
               : (H_t \/ H_f)(cb)


------------------------- (o-p-H)
D;H_tf;G[r1->int] |- cb_t : All[D](G,S)
------------------------------ [ins-id]
D;H_tf;G[r1->int] |- cb_t[D]: All[](G,S)
G[r1->int] => G from g-imp     S => S from s-imp-id
-------------------------------- (b-jump)
(18) D;H_tf;G[r1->int];S |- jump cb_t[D]

D, H', G, S |- b (premise)
---------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D; H'; G; S |- b then D2; H2'; G2; S2 |- I'; b


(8) C0 subsetof C1 from C0 subsetof C_t and C_t subsetof C1
    H1 subsetof H2 from definition of H2

case trans-call:
***************

st = (x = f'(v1, ..., vn)),
C1 = C0, cb ->all[D1](G1,S1)(I; push r_fp; push r_ra; Is;
                             mov r_ra, cb_cont; jump p_f'[sub, Next(l,2), Q])
H2 = H1, cb_cont->All[D](G,Next(l,3):||t|| :: Next(l,2):Q)
Q = G(r_ra)::next(l):G(r_fp)::S
cb' = cb_cont,
D2 = D, G2 = G[sp->single(Next(l,3))], and S2 = Next(l,3):||t|| :: Next(l,2):Q,
I' = (pop r1; update x; pop r_ra; pop r_fp)
(9)||GS |- (v1, ..., vn) : (t1, ..., tn)|| V r1 = (Is, sub),
(10) GS(f') = (t1, ..., tn) -> t
(11) GS |- x:t and t != t' *S,
(12) GS(sp) = single(l)

Let sub' = sub, Next(l,2), Q.

                    (13) H2 |- C1(cb)   
                    H2(cb) = H1(cb) = All[D1](G1, S1)
                    .|- All[D1](G1, S1) from [CodeLabel]
                    ------------------------------ (v-code)
(2) |- C0: H1\cb    .;H2 |- C1(cb) : H2(cb)
---------------------------------------------- (h-tp)
(6) |- C1: H2\cb'


Let ti' = ||ti, G, S, V, vi|| forall i = 1, ..., n
and S_call = Next(l,n+2)::t1':: ...:: Next(l,3):tn'::Next(l,2):Q
and G_call = G[sp->single(Next(l,n+2)), r1->t1']

From translation of types, ||(t1, ..., tn)->t|| = All[D_f](G_f,S_f) 
where ||{t1, ..., tn}|| L P = (S_f, D_f')
and D_f = {D_f', L, P}
and G_f = {sp -> single(Next(L,n)),
           r_ra -> All[](sp -> single(next(L)), next(L):||t||::L:P)}


(10) GS(f') = (t1, ..., tn) -> t
(3) ||GS, V, sz, f|| L P = (D,H,G,S)
-------------------------------- ([funcTy])
H(p_f') = All[D_f](G_f,S_f)
--------------------------------------------------------------(o-p-H)
D;(H,cb_cont->All[D](G2,S2));G_call[r_ra->All[](G2,S2)] |- p_f': All[D_f](G_f,S_f)
----------------------------------------------------------------(o-inst-l & o-inst-Q)
D;(H,cb_cont->All[D](G2,S2));G_call[r_ra->All[](G2,S2)] |-
            p_f'[sub']: (All[D_f](G_f,S_f))[sub']
All[D_f](G_f,S_f)[sub'] = All[](G_f[sub'/D_f], S_f[sub'/D_f])
G_call[r_ra->All[](G2,S2)] => G_f[sub'/D_f] from g-imp
S_call => S_f[sub'/D_f] from [call]
----------------------------------------------------------------- (b-jump)
D;(H,cb_cont->All[D](G2,S2));G_call[r_ra->All[](G2,S2)];S_call |- jump p_f'[sub']
D;(H,cb_cont->All[D](G2,S2));G_call |- cb_cont[D] : All[](G2,S2) from (o-p) and [inst-id]
|-(G_call,S_call){r_ra<-All[](G2,S2)}(G_call[r_ra->All[](G2,S2)],S_call) from (a-not-esp)
-------------------------------------------------------------  (i-mov & b-ins)
D;(H,cb_cont->All[D](G2,S2));G_call;S_call |- move r_ra, cb_cont[D]; jump p_f'[sub']
||GS |- (v1, ..., vn) : (t1, ..., tn)|| = (Is, sub)
------------------------------------------------------------------ (transArgs)
D;(H,cb_cont->All[D](G2,S2));G[sp->single(Next(l,2))];
Next(l,2):G(r_ra)::Next(l,1):G(r_fp)::S |- Is; mov r_ra, cb_cont[D]; jump p_f'[sub']
------------------------------------------------------------------ (push)
D;(H,cb_cont->All[D](G2,S2));G[sp->single(Next(l,1))];Next(l,1):G(r_fp)::S |- 
 push r_ra; Is; mov r_ra, cb_cont[D]; jump p_f'[sub']
---------------------------------------------------------- ([push])
D;(H,cb_cont->All[D](G2,S2));G;S |- push r_fp; push r_ra; Is; 
                                  mov r_ra, cb_cont[D]; jump p_f'[sub']
--------------------------------------------------------------------------- (5)
D1; H2; G1; S1 |- (I; push r_fp; push r_ra; Is; 
                   mov r_ra, cb_cont[D]; jump p_f'[sub'])
------------------------------------------------------------- (block-tp)
(13) H2 |- all[D1](G1,S1)(I; push r_fp; push r_ra; Is; 
                          mov r_ra, cb_cont[D]; jump p_f'[sub'])


Let S2' = Next(l,2):G(r_ra)::next(l):G(r_fp)::S


                     (3) ||GS, V, sz, f|| L P = (D, H, G, S)
------ (premise)    ----------------------------- ([transEnv])
D;H';G;S |- b           r1 not in domain(G)
-------------------------------------- (RegFile-Weakening)
D;H';G[r1->||t||];S |- b
---------------------------------------------- ([pop])
D;H';G[r1->||t||,sp->single(next(l))];(next(l):G(r_fp)::S) |- pop r_fp; b
-------------------------------------------- ([pop])
D;H';G[r1->||t||,sp->single(Next(l,2))];S2' |- pop r_ra; pop r_fp; b
(10) GS |- x:t and t != t' *S
(3) ||GS, V, sz, f|| L P = (D, H, G, S)
----------------------------------------------------- ([update-x])
D;H';G[r1->||t||,sp->single(Next(l,2))];S2' |- update x; pop r_ra; pop r_fp; b
-------------------------------------------------------- ([pop])
D;H'; G2; S2 |- pop r1; update x; pop r_ra; pop r_fp; b
------------------------------------------------------- (if-introduction)
(7) forall b, forall H0, if D;H';G;S |- b then D2;H2';G2;S2 |- I';b




(8) C0 subsetof C1 and H1 subsetof H2 


========================================================================
translation of blocks

Lemma [transB]
If (1) ||GS |-t B|| f C0 H1 = (C1, H2) and
   (2) |- C0 : H1\p_f
then (3) |- C1 : H2
	and C0 subsetof C1 and H1 subsetof H2

Proof: 

By translation rule of blocks [trans-B],
B = (lds; sts; return v)
and (4) ||GS |- lds: GS'|| V 0 = (V', sz', I_ld)
and (5) ||GS' |- v:t|| V' r1 = I_v
and (6) ||GS' |- sts|| V' sz' f C0 H1 p_f (mov r_fp, sp; I_ld) 
       = (C0', H2, cb', I')
and (7) GS(f) = (t1, ..., tn) -> t
and H2(cb')  = All[D2](G2,S2)
and C1 = (C0', cb' -> b')
and b' = All[D2](G2,S2)(I'; I_v; pop r2; ...; pop r2; push r1; jump r_ra))
                                 \------ sz'+n -----/


Let ||GS', V', sz', f|| L P = (D, H, G, S), 
and ||GS, V, 0, f|| L P = (D1, H1, G1, S1) 

D;(H,H0);G;S |- b from (premise)
(4) ||GS |- lds: GS'|| V 0 = (V', sz', I_ld)
---------------------------------------------([transLd])
D1;(H1,H0);G1;S1 |- I_ld; b
(G1\r_fp)(sp) = single(Next(L,n)) and G1(r_fp) = single(Next(L,n)) from [transEnv]
|-(G1\r_fp;S1){r_fp<-single(l)}(G1;S1) 
------------------------------------(i-mov & b-ins)
D1;(H1,H0);G1\r_fp;S1 |- mov r_fp, sp;I_ld;b      r_fp not in domain(G1\r_fp)  
----------------------------------------------------- (RegFile-Weakening)
D1;(H1,H0);G1;S1 |- mov r_fp, sp; I_ld; b
--------------------------------------------------------- (if-introduction)
forall b, forall H0, if D;(H,H0);G;S |- b 
       then D1;(H1,H0);G1;S1 |- mov r_fp, sp; I_ld; b 


(2) |- C0: H1\p_f
By [transS], we have
    (8) |- C0' : H2\cb' 
    (9) forall b, forall H0, if D;(H,H0);G;S |- b
         then D2;(H2;H0);G2;S2 |- I';b    


(8) |- C0' : H2\cb'   (10).;H2 |- b': H2(cb')
----------------------------------- (h-tp)
(4) |- C1 : H2

By [transEnv] S = Next(L, sz'+n):...::L:Q
and G(r_ra) = All[](G_ra, S_ra) where
    G_ra = sp->single(next(L)) and
    S_ra = next(L):||t||::L:Q

G(r_ra) = All[](G_ra, S_ra) 
G[r1->||t||, r2->_, sp->single(next(L)] => G_ra  from (g-imp)
next(L)::||t||::L:Q => S_ra from (s-imp-id)
------------------------------------------------ (b-jump)
D;H;G[r1->||t||, r2->_, sp->single(next(L)]; next(L):||t||::L:Q |- jump r_ra
------------------------------------------------ ([push])
D;H;G[r1->||t||,r2->_, sp->single(L)];L:Q|- push r1; jump r_ra
------------------------------------------------ ([pop])
D;H;G[r1->||t||];S |- pop r2; ...; pop r2; push r1; jump r_ra
(5) ||GS' |- v:t|| V' r1 = I_v
(7) ||GS', V', sz', f|| L P = (D, H, G, S)
----------------------------------------------------- (transV)
D;H;G;S |- I_v; pop r2; ...; pop r2; push r1; jump r_ra
-------------------------------------------------------- (9)
D2;H2;G2;S2 |-I'; I_v: pop r2; ...; pop r2; push r1; jump r_ra
-------------------------------------------------- (block-tp)
.;H2 |- b'
. |- All[D2](G2,S2) from [CodeLabel]
--------------------------------------------------- (v-code)
(10) .;H2 |- b: H2(cb')


========================================================================
translation of functions

Lemma[transF]
If    (1) ||GS |- fd : GS'|| C H = (C', H') 
  and (2) |- C : H
then  (3) |- C' : H'
  and C subsetof C' and H subsetof H'

Proof:

By translation rule of functions [trans-f],
 fd = t f(t1 x1, ..., tn xn) rb, and
(4) ||GS' |-t rb|| f C H[p_f -> ||tf||] = (C',H') 
where tf = (t1, ..., tn) -> t and GS' = GS[f:tf, x1:t1, ..., xn:tn]


(4) ||GS' |-t rb|| f C H[p_f -> ||tf||] = (C',H')    (2) |- C : H 
---------------------------------------------------------- (transB)
(3) |- C' : H'


========================================================================
translation of programs

Lemma[transP]
If    (1) |||-(fds, rb)|| = (C', H', b) 
then  (2) |- (C', {sp -> base}, empty, b)

Proof: 
By translation rule of programs [trans-p], 
  b = (mov r_ra, p_halt; jump p_main[base, empty]) 
  and (3) ||.|- fds : GS|| {p_halt -> block_halt} {p_halt -> t_halt} = (C, H)
  and (4) ||GS |- rb || main C (H, p_main -> t_main) = (C', H')
where t_halt = All[]({sp -> single(next(base))}, next(base):int :: base:Empty)
  and t_main = All[L,P]({sp -> single(L), 
                         r_ra -> ALL[]({sp -> single(next(L))}, 
                                        next(L):int :: L:P)},
                        L:P)

Let G = {sp -> single(base)}, S = base : Empty.			
			
                ---------------- (o-d)
                |- base : single(base)
                -------------------- (h-tp)  --- (s-base)
(5) |- C' : H'   |-{sp -> base} : G	     |- empty: S    (6) (.,H',G,S) |- b
-------------------------------------------------------------------------- (prog)
              (2) |-(C', {sp -> base}, empty, b)


 (8) |- C : H   ||GS |- rb || main C (H, p_main -> t_main) = (C', H')   
---------------------------------------------------------------------- (tranB)
    (5) |- C' : H'     (7) (H, p_main -> t_main) subsetof H'
	

(3)||.|-fds:GS|| {p_halt -> block_halt} {p_halt -> t_halt} = (C,H) 
(10) |-{p_halt -> block_halt}:{p_halt -> t_halt} 
---------------------------------------------------------------------(transF)									  
         (8) |- C : H        (9) {p_halt -> t_halt} subsetof H


|-block_halt : t_halt
---------------------------------------------(h-tp)
(10)|-{p_halt -> block_halt}:{p_halt -> t_halt}


(9) {p_halt -> t_halt} subsetof H
(7) (H, p_main -> t_main) subsetof H' 
-------------------------------- (transitivity)
{p_halt -> t_halt} subsetof H'
------------------------ 
(11) H'(p_halt) = t_halt
----------------- (o-p-H)  --------------------------------- (a-not-esp)
.;H';G |- p_halt: t_halt   |-(G;S){r_ra <- t_halt}(G[r_ra:t_halt];S)
------------------------------------------------------------- (i-mov)
(.; H') |- (G;S){mov r_ra, p_halt}(G[r_ra:t_halt]; S)      
    (12) (.; H'; G[r_ra:t_halt]; S) |- jump p_main[base, empty] 
--------------------------------------------------------------------- (b-ins)
(6) (.;H';G;S) |- b


Let G' = {sp -> single(base), r_ra -> t_halt}

(7) (H, p_main -> t_main) subsetof H' 
------------------------------------
H'(p_main) = t_main
--------------------------------------- (o-p-H)
.;H';G[r_ra -> t_halt] |- p_main:t_main
------------------------------------- (o-inst-l)
.;H';G[r_ra -> t_halt] |- p_main[base]: t_main[base/L]
-------------------------------------------- (o-inst-Q)                            
.;H'; G[r_ra -> t_halt] |- p_main[base,empty] : All[](G', S) 
G[r_ra:t_halt]=>G' by (G-imp)
S=>S  by (s-imp-eq)
-------------------------------------------------------------------(b-jump)
(12) (.; H'; G[r_ra:t_halt]; S) |- jump p_main[base, empty]