Lemmas Used in Progress and Preservation





==========================================================================================================


S-Update-Size Lemma:
-------------------------

If s' = s[d <- w] then size(s) = size(s').

Proof: By induction on the structure of s[d <- w].



==========================================================================================================

Canonical Forms Lemma:
-------------------------

If  {};H;G |- o : t  and  |- h:H   and  {};H |- g : G 
then if t = int   then  Exists i.  g |- o  ==> i
     if t = HeapPtr(t') then  Exists p,w.  g |- o ==> p  and  h(p) = <w>  and H(p) = t  and  {};H;{} |- w : t'
     if t = Single(l) then either Exists d. g |- o ==> d   or  Exists p.  g |- o ==> p    (this line may not be necessary...)
     if t = Single(d) then g |- o ==> d
     if t = Single(p) then g |- o ==> p
     if t = Nonsense then g |- o ==> nonsense
     if t = All[D1](G1,S1) then Exists p, subst, D2, G3, S3.  g |- o ==> p[subst]  and  h(p) = all[D1,D2](G3,S3) 
							      and G1 = G3[subst/D2]  and S1 = S3[subst/D2] 

Proof: By induction on the structure of {};H;G |- o : t

a1. {};H;G |- o : t
a2. |- h : H
a3. {}; H |- g : G


Induction on the structure of a1. 


case o-reg:

  ------------------ (o-reg)
  {};H;G |- r : G(r)

1a. {};H;{} |- g(r) : G(r)				[ Inversion of g-tp, a3 ] 
2a. if t = ... Exists w_t. g |- g(r) ==> w_t...		[ Canonical Forms, 1a, a2, a3 ]
3a. Exists w. g(r) = w 					[ def of g ]
4a. results in 2a all using eo-w			[ 3a, 2a ]
5a. if t = ... Exists w. g |- r ==> w_t...		[ 2a, 4a, eo-r ]
*



case o-int:

  ----------------- (o-int)
  {};H;G |- i : int 

1b. g |- i ==> i					[ eo-w ]
2b. if t=int then Exists i. g |- o ==> i		[ 1b ]
*



case o-ns:

  ----------------------------- (o-ns)
  {};H;G |- nonsense : Nonsense 

1c. g |- nonsense ==> nonsense				[ eo-w ]
2c. if t = Nonsense then g |- o ==> nonsense		[ 1c ]
*



case o-p-H:

  ------------------ (o-p-H)
  {};H;G |- p : H(p)

1d. g |- p ==> p					[ eo-w ]
2d. Forall p'. {}; H |- h(p') : H(p')			[ Inversion of h-tp, a2 ]
3d. {};H |- h(p) : H(p)					[ 2d, assumption ]

subcase on the structure of 3d.

subcase o-p-H-1:

  {};H;{} |- w : t
  -------------------------- (v-hp)
  {};H |- <w> : HeapPtr(t')

3d1. t = H(p) = HeapPtr(t')				[ case/subcase assumption ]
4d1. {}; H |- h(p) : HeapPtr(t')			[ 2d, 3d1 ]
5d1. h(p) = <w>						[ Inspection of v-hp, 4d1 ]
6d1. {};H;{} |- w : t'					[ Inversion of v-hp, 4d1, 5d1 ]
7d1. if t = HeapPtr(t') 				[ 1d, 5d1, 3d1 ]
     then  Exists p.  g |- o ==> p  and  h(p) = <w>  and H(p) = t  and D;H;{} |- w : t'
*

subcase o-p-H-2:

  H |- all[D1](G1,S1) b
  {} |- All[D1](G1,S1)
  ------------------------------------------ (v-code)
  {};H |- all[D1](G1,S1) b : All[D1](G1,S1)

3d2. t = H(p) = All[D1](G1,S1) 				[ case/subcase assumption ]
4d2. {};H |- h(p) : All[D1](G1,S1)			[ 2d, 3d2 ]
5d2. h(p) = all[D1](G1,S1) b'				[ Inspection of v-code, 4d2 ]
6d2. if t = All[D1](G1,S1) 				[ 1d, 5d2, 3d2 ]
     then  g |- o ==> p[{}]  and h(p) = all[{}](G3,S3) b'  and G1 = G3[{}/{}]  and S1 = S3[{}/{}]
*



case o-p:

  ----------------------- (o-p)
  {};H;G |- p : Single(p)
  
1e. g |- p ==> p  					[ eo-w ]
2e. if t = Single(p) then g |- o ==> p			[ 1e ]
    if t = Single(l) then Exists p. g |- o ==> p	[ 1e ]
*



case o-d:

  ----------------------- (o-d)
  {};H;G |- d : Single(d)
 
 1f. g |- d ==> d					[ eo-w ]
 2f. if t = Single(d) then g |- o ==> d			[ 1f ]
     if t = Single(l) then Exists d. g |- o ==> d	[ 1f ]
 *    
 
     
     
case o-inst-l

  {};H;G |- o : All[L,D1](G1,S1)
  {} |- l
  -------------------------------------- (o-inst-l)
  {};H;G |- o[l] : All[D1](G1[l/L],S1[l/L])

1g. Exists p, subst, D2, G3, S3.  g |- o ==> p[subst]			[ Canonical Forms, ap1, a2, a3 ]
2g. h(p) = all[D1,L,D2](G3,S3) 
3g. G1 = G3[subst/D2]  and S1 = S3[Dsubst/D2]  

4g. g |- o[l] ==> p[subst,l]						[ eo-inst-l, 1g ]

5g. G1[l/L] = G3[subst/D2][l/L]	and S1[l/L] = S1[subst/D2][l/L] 	[ 3g ]
6g. G1[l/L] = G3[(subst,l)/(D2,L)] and S1[l/L] = S1[(subst,l)/(D2,L)]	[ 5g, properties of subst? ]
7g. g |- o[l] ==> p[subst,l]  and  h(p) = all[D1,L,D2](G3,S3) 
    and  G1[l/L] = G3[(subst,l)/(D2,L)] and S1[l/L] = S1[(subst,l)/(D2,L)]
*




case o-inst-Q:

  {};H;G |- o : All[P,D'](G,S)
  {} |- Q
  -------------------------------------- (o-inst-Q)
  {};H;G |- o[Q] : All[D'](G[Q/P],S[Q/P])

as in case o-inst-l.
*



==========================================================================================================

Substitution Lemma:
-------------------

1. If (D,L);H;G |- o : t and D |- l then D;H;G[l/L] |- o[l/L] : t[l/L]
2. If (D,L);H |- (G,S){ins}(G',S') and D |- l  then D;H |- (G[l/L];S[l/L]){ins[l/L]}{G'[l/L];S'[l/L])
3. If (D,L);H;G;S |- b  and D |- l  then D;H;G[l/L];S[l/L] |- b[l/L]

Equivalent lemmas hold for P and Q.

Proof: each by induction on the respective typing derivation, using the preceeding lemmas.


==========================================================================================================

Deterministic-EO Lemma:
-------------------------

If g |- o ==> w  and  g |- o ==> w'  then w = w'.

Proof: By induction on the structure of g |- o ==> w.




==========================================================================================================


Unnecessary-G Lemma:
-------------------------

If {};H;G |- w : t  then {};H;{} |- w : t

Proof: By induction on the structure of {};H;G |- w : t.


==========================================================================================================


Lemma EO-Type-Preservation
----------------------------

If  {};H;G |- o : t  and  {};H |- g : G  and g |- o ==> w  then {};H;{} |- w : t

Proof: by induction on the structure of g |- o ==> w :


a1. {};H;G |- o : t
a2. {};H |- g : G
a3. g |- o ==> w

case eo-r:

  --------------- (eo-r)
  g |- r ==> g(r) 
  
1a. {};H;G |- r : t						[ a1, case assumption ]
2a. G(r) = t							[ Inspection of o-reg, 1a ]
3a. Forall r' in dom(g) or dom(G). {};H;{} |- g(r') : G(r')	[ Inversion of g-tp, a2 ]
4a. {};H;{} |- g(r) : t						[ 2a, 3a ]
5a. {};H;G |- g(r) : t						[ weakening on G, 4a ]
6a. {};H;{} |- g(r) : t						[ Unnecessary-G Lemma, 5a ]
*

case eo-w:

  ------------ (eo-w)
  g |- w ==> w
  
1b. {};H;G |- w : t						[ a1, case assumption ]
2b. {};H;{} |- w : t						[ Unnecessary-G Lemma, 5a ]
*


case eo-inst-l:

  g |- o ==> w
  ------------------ (eo-inst-l)
  g |- o[l] ==> w[l]

1c. {};H;G |- o[l] : All[D'](G[l/L],S[l/L])			[ a1, case assumption, inspection of o-inst-l ]
2c. {};H;G |- o : All[L,D'](G,S)				[ Inversion of o-inst-l, 1c ]
3c. {};H;G |- w : All[L,D'](G,S)				[ I.H., 2c, a2, pc1 ]
4c. {} |- l							[ Inversion of o-inst-l, 1c ]
5c. {};H;G |- w[l] : All[D'](G[l/L],S[l/L])			[ o-inst-l, 3c, 4c ]
6c. {};H;{} |- w[l] : All[D'](G[l/L],S[l/L])			[ Unnecessary-G Lemma, 5c ]
*


case eo-inst-Q:

  g |- o ==> w
  ------------------ (eo-inst-Q)
  g |- o[Q] ==> w[Q]

as in case eo-inst-l.
*




==========================================================================================================

Lemma A-U-Progress
--------------------

If  |- (G,S) {r1 <- t} (G';S')  and  {};H;G |- o : t  and  g |- o ==> w  
and  |- h:H  and  {};H |- g : G  and  {};H |- s : S 
then Exists g',s'. (g,s) {r1 <- w} (g',s') 


Proof: by case analysis on the structure of |- (G,S) {r1 <- t} (G';S')

a1. |- (G,S) {r1 <- t} (G';S')
a2. {};H;G |- o : t
a3. g |- o ==> w
a4. {};H |- g : G
a5. {};H |- s : S
a6. |- h : H


case on the structure of a1

case a-not-esp:

  r1 != esp
  --------------------------------------- (a-not-esp)
  |- (G,S){r1 <- t}(G[r1 <- t],S)

2a. (g,s) {r1 <- w} (g[r1<-w],s)				[ u-not-esp, pa1 ]
*



case a-esp:

  |- Resize(l,S) = S'
  ---------------------------------------------- (a-esp)
  |- (G,S){esp<-Single(l)}(G[esp<-Single(l)],S')

2b. {};H;G |- o : Single(l)					[ a1, case assumption ]
3b. Exists d. l = d						[ Lemma S-resize-d, pb1, a5 ]
4b. {};H;G |- o : Single(d)					[ 2b, 3b ]
5b. g |- o ==> d						[ Canonical Forms, 4b, a4, a6 ]
6b. w = d							[ a3, 5b ]
7b. (g,s) {esp <- d} (g[esp<-d],resize(w,s))			[ u-esp, 6b ]
*







==========================================================================================================


Lemma A-U-Preservation
-------------------------

If  |- (G,S) {r1 <- t} (G';S')  and  {};H;G |- o : t  and  g |- o ==> w  and  (g,s) {r1<-w} (g',s')  
and  |- h:H  and  {};H |- g : G  and  {};H |- s : S 
then {};H |- g' : G'  and {};H |- s' : S'

Proof: by case analysis on the structure of |- (G,S) {r1 <- t} (G';S')


a1. |- (G,S) {r1 <- t} (G';S')
a2. {};H;G |- o : t
a3. g |- o ==> w
a4. (g,s) {r1 <- w} (g',s')  
a5. |- h: H
a6. {};H |- s : S
a7. {};H |- g : G


case on the structure of a3

case u-not-esp:

  r1 != esp
  ---------------------- (u-not-esp)
  (g,s){r1<-w}(g[r1<-w],s)


3a. {};H;G |- w : t						[ Lemma EO-Type-Preservation, a2, a7, a3 ]
4a. {};H;G[r1<-t] |- w : (G[r1<-t])(r1)				[ 3a, def of G[r<-t], G(r) ] 

5a. Forall r' in dom(g) or dom(G). {};H;{} |- g(r') : G(r')	[ Inversion of g-tp, a7 ]
6a. {};H |- g[r1<-w] : G[r1<-t]					[ g-tp, 5a, 4a ] 

7a. G' = G[r1<-t]  and  S' = S					[ Inversion of a-not-esp, a1, p1 ]
8a. {};H |- g':G' and {};H |- s':S' 				[ 4a, 6a, 7a ]
*



case u-esp:

  -------------------------------------- (u-esp)
  (g,s){esp<-d}(g[esp<-d],resize(d,s))  

ab1. r1 = esp
ab2. w = d

2b. |- (G,S){esp<-Single(l)}(G[esp<-Single(l)],S')		[ Inspection of a-not-esp, a1, ab1 ]
3b. t = Single(l)						[ a1, 2b ]
4b. |- Resize(l,S) = S'						[ Inversion of a-not-esp, 2b ]

5b. {};H;G |- o : Single(l)					[ a2, 3b ]
6b. Exists d'. l = d'						[ Lemma S-resize-d, 4b, a6 ]

7b. {};H;G |- o : Single(d')					[ 5b, 6b ]
8b. {};H;G |- d : Single(d')					[ Lemma EO-Type-Preservation, 6b, a6, a3, ab2 ]
9b. d = d'							[ Inspection of o-d, 8b ]

10b. {};H |- g[esp<-d] : G[esp<-Single(l)]			[ g-tp, a7, 8b, 6b ]

11b. {};H |- resize(d,s) : S'					[ Lemma S-s-Resize, a6, (4b, 6b, 9b) ]

12b. {};H |- g[esp<-d]:G[esp<-Single(l)] and {};H |- resize(d,s):S' 	[ 10b, 11b ]
*



==========================================================================================================

Lemma Stack-Weakening
----------------------

If D;H;G;S |- b and S1 => S then D;H;G;S1 |- b

PROOF: By induction on the structure of D;H;G;S' |- b

a1. D;H;G;S |- b
a2. S1 => S

CASE b-ins:

  D;H |- (G;S){ins}(G';S')
  D;H;G';S' |- b
  ------------------------ (b-ins)
  D;H;G;S |- ins; b

1. Exists S1'. D;H |- (G;S1){ins}(G';S1') and S1' => S'		[ Lemma Stack-Weakening-Ins, p1, a2 ]
2. D;H;G';S1' |- b						[ I.H., p1, 1 ]
3. D;H;G;S1 |- ins;b						[ b-ins, 1, 2 ]
*


CASE b-unpack:

  D;H;G |- o : HeapPtr(t)
  r != esp
  L not in D
  (D,L);H;G[r<-Single(L)];l:(Q/\{L:t}) |- b
  ------------------------------------------- (b-unpack)
  D;H;G;l:Q |- (L,r) = unpack(o);b

1. Exists Q1. S1 = l:Q1						[ Lemma S-imp-label-eq, a2 ]
2. l:(Q1/\{L:t}) => l:(Q/\{L:t})				[ S-imp-alias, a2, 1 ]
3. (D,L);H;G[r<-Single(L)];l:(Q1/\{L:t}) |- b			[ I.H. p4, 2 ]
4. D;H;G;S1 |- (L,r) = unpack(o);b				[ b-unpack, p1, p2, p3, 3, 1 ]
* 


CASE b-jump:

  D;H;G |- o : All[](G',S')
  G => G'
  S => S'
  ------------------------ (b-jump)
  D;H;G;S |- jump o

1. S1 => S'							[ S-imp-trans, a2, p3 ]
2. D;H;G,S1 |- jump o						[ b-jump, p1, p2, 1 ]
*



==========================================================================================================

Lemma Stack-Weakening-Ins
--------------------------

If D;H |- (G,S){ins}(G',S') and S1 => S then Exists S1'. S1' => S' and D;H |- (G,S1){ins}(G',S1')


PROOF: By case analysis on the structure of D;H |- (G,S){ins}(G',S')


CASES i-add, i-sub, i-store-p :

  D;H;G |- o : int
  r ! = esp
  G(r) = int
  -------------------------- (i-add/sub)
  D;H |- (G;S){add/sub r,o}(G;S)
  
  G(r1) = HeapPtr(t)
  G(r2) = t
  ---------------------------------- (i-store-p)
  D;H |- (G;S){store [r1+0],r2}(G;S)  
  
S = S', S1 = S1'
Result hold immediately using a2 and rebuilding each rule using S1
*


CASES i-mov, i-load-p, i-store-p i-heapalloc : 

  D;H;G |- o : t
  |- (G;S){r<-t}(G';S')
  ---------------------------- (i-mov)
  D;H |- (G;S){mov r,o}(G';S')
  
  G(r2) = HeapPtr(t)
  |- (G,S){r1<-t}(G',S')
  ----------------------------------- (i-load-p)
  D;H |- (G;S){load r1,[r2+0]}(G';S')
  
  D;H;G |- o : t
  |- (G,S){r<-HeapPtr(t)}(G',S')
  -------------------------------------- (i-heapalloc)
  D;H |- (G;S){heapalloc r = <o>}(G';S')

For each rule, use Lemma Stack-Weakening-A and a2 to show that
Exists S1'. S1' => S'  and  |- (G,S1){r<-t}(G',S1')	
Then rebuild each rule using this result.
*


CASE i-add-l:

  G(r) = Single(l)
  S |- l + i = l'
  (G;S) {r <- Single(l')} (G';S')
  -------------------------------- (i-add-l)
  D;H |- (G;S){add r,-4*i}(G';S')
  
  G(r2) = Single(l)
  S |- l + i = l'
  S |- l' : t
  |- (G,S){r1<-t}(G',S')
  ---------------------------------------- (i-load-concat)
  D;H |- (G;S){load r1,[r2+(-4*i)]}(G';S')


  G(r2) = Single(l)      
  S |- l : t
  |- (G,S){r1<-t}(G',S')
  ------------------------------------------------ (i-load-aliased)
  D;H |- (G;S){load r1,[r2+0]}(G';S')
  
  
By Lemma Stack-Weakening-A, a2, and the appropriate premise Exists S1'. S1' => S'  and  |- (G,S1){r<-t}(G',S1').
Transitivity of => to show that S-lookup and S-offset hold for S1.
Rebuild each rule using modified premises.
*

  
  
  
CASE i-store-concat:
  
  G(r1) = Single(l)
  G(r2) = t
  S |- l + i = l'
  S |- l' <- t ~~> S'
  ---------------------------------------- (i-store-concat)
  D;H |- (G;S){store [r1+(-4*i)],r2}(G;S')

By transitivity of =>, S1 |- l+i = l'
By transitivity of =>, S1 |- l' <-t ~~> S'
Rebuild rule using modified premises and S' => S'
*

  
CASE i-store-aliased:
  
  G(r1) = Single(l)
  S |- l : t 
  G(r2) = t
  ------------------------------------- (i-store-aliased)
  D;H |- (G;S){store [r1+0],r2}(G;S)
  
By transitivity of =>, S1 |- l : t
Rebuild rule using modified premise and S1 => S
*  

  

CASE i-jumpif0:

  G(r) = int
  D;H;G |- o : All[](G',S')
  G => G'
  S => S'
  ------------------------------ (i-jumpif0)
  D;H |- (G;S){jumpif0 r,o}(G;S)

1. S1 => S'							[ S-imp-trans, a2, p4 ]
2. D;H;G,S1 |- jump o						[ b-jump, p1, p2, p3, 1 ]
*




==========================================================================================================

Lemma Stack-Weakening-A
-------------------------

If |- (G;S){r<-t}(G';S')  and S1 => S  then Exists S1'. S1' => S'  and  |- (G,S1){r<-t}(G',S1')

PROOF: By case analysis on the structure of |- (G;S){r<-t}(G';S')


CASE a-not-esp:

  r != esp
  ------------------------- (a-not-esp)
  |- (G,S){r<-t}(G[r<-t],S)

1. S' = S						[ case assumption ]
2. |- (G,S1){r<-t}((G[r<-t],S1)				[ a-not-esp, p1 ]
3. S1 => S and |- (G,S1){r<-t}((G[r<-t],S1)		[ a2, 2]
*

CASE a-esp:

  |- Resize(l,S) = S'
  ---------------------------------------------- (a-esp)
  |- (G,S){esp<-Single(l)}(G[esp<-Single(l)],S')

1. Exists S1'. S1' => S' and |- Resize(l,S1) = S1'	[ Lemma S-Resize-imp, p1, a1 ]
2. |- (G,S1){esp<-Single(l)}(G[esp<-Single(l)],S1')	[ a-esp, 1 ]
3. S1' => S' and |- (G,S1){r<-t}(G',S1')		[ 1, 2 ]
*




==========================================================================================================

Lemma RegFile-Weakening
------------------------

If D;H;G;S |- b and G1 => G then D;H;G1;S |- b

PROOF:

Inspection of rules involved in D;H;G;S |- b. All rules only lookup/modify regs in dom(G). 
None require a register to not be in dom(G).
G is a subset of G1, so G1 can be used instead.
Rules i-jumpif0 and b-jump require transitivity of G => G
*