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

STACK RULES (LOGICAL)

notation:
  next^0(l) = l
  next^(n+1)(l) = next(next^n(l))
  T = (tn;...;t1)
  (tn;...;t1) @ (l:Q) = next^n(l):tn::...next^1(l):t1::l:Q

judgments:
  S => S'
  S |- l + i = l'
  |- Resize(l,S) = S'
  S |- l : t
  S |- l <- t' ~~> S'

judgment: S => S'

  S => S    (S-imp-eq)

  S1 => S2
  S2 => S3
  --------- (S-imp-trans)
  S1 => S3

  S => S'
  --------------------- (S-imp-concat)
  l:(t::S) => l:(t::S')

  l:Q => l:Q'
  -----------------------------------(S-imp-alias)
  l:(Q /\ {lt:t}) => l:(Q' /\ {lt:t})

  l:(t::S) => l:(t::S /\ {l:t}) (S-imp-add-alias)

  l:(t1::lq:(Q /\ {l2:t2})) => l:((t1::lq:Q) /\ {l2:t2}) (S-imp-expand-alias)

  l:(Q /\ {lt:t}) => l:Q (S-imp-drop-alias)

  S => l:(Q /\ {l1:t1})
  S => l:(Q /\ {l2:t2})
  ---------------------------------- (S-imp-merge-alias)
  S => l:((Q /\ {l1:t1}) /\ {l2:t2})

judgment: S |- l + i = l'

  S => T @ (l:Q)
  ----------------------  (S-offset-next)
  S |- l + n = next^n(l)

  S => T @ (l:Q)
  ----------------------  (S-offset-prev)
  S |- next^n(l) - n = l
 
judgment: |- Resize(l,S) = S'

  S => T @ (l:Q)
  -------------------- (S-shrink)
  |- Resize(l,S) = l:Q
 
  |- Resize(next^n(l),l:Q) = (Nonsense_n;...;Nonsense_1) @ (l:Q)  (S-grow)

judgment: S |- l : t

  S => l':(Q /\ {l:t})
  -------------------- (S-lookup)
  S |- l : t

judgment: S |- l <- t' ~~> S'

  S |- l : t
  -------------------- (S-update-weak)
  S |- l <- t ~~> S

  S => T @ (l:t::S')
  ------------------------------- (S-update-strong)
  S |- l <- t' ~~> T @ (l:t'::S')

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

STACK RULES (ALGORITHMIC)

Define:
  O = P | Empty | t::S
  LMap = {...,(l,t),...}
  LMap,(l,t) = LMap U {(l,t)}

judgment: S =>> S' yielding LMap
(syntax-directed, given S and S')

  l:P =>> l:P yielding {}  (S-imp2-P)

  l:Empty =>> l:Empty yielding {}  (S-imp2-empty)

  S1 =>> S2 yielding LMap
  --------------------------------------- (S-imp2-concat)
  l:t::S1 =>> l:t::S2 yielding LMap,(l,t)

  l':Q =>> l':O yielding LMap
  -------------------------------------------- (S-imp2-alias-left)
  l':(Q /\ {l:t}) =>> l':O yielding LMap,(l,t)

  S =>> l':Q yielding LMap,(l,t)
  ----------------------------------------- (S-imp2-alias-right)
  S =>> l':(Q /\ {l:t}) yielding LMap,(l,t)

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

TYPING

judgments:
  G => G'
  D |- l
  D |- t
  D |- G
  D |- S
  |- (h,g,s,b)
  |- h : H          (also: do we need "|- H" separately?)
  D;H |- s : S
  D;H |- g : G
  D;H |- v : t
  D;H;G |- o : t
  |- (G,S){r<-t}(G',S')
  D;H |- (G,S){ins}(G',S')
  D;H;G;S |- b
  H |- block

judgment: G => G'

  G' subsetof G
  ------------- (G-imp)
  G => G'

judgment: D |- l

  {...,L,...} |- L  (wf-l-var)

  D |- base  (wf-l-base)

  D |- l
  ------------ (wf-l-next)
  D |- next(l)

  D |- p  (wf-l-p)

judgment: D |- t

  D |- int  (wf-t-int)

  D |- Nonsense (wf-t-ns)

  D |- t
  --------------- (wf-t-hp)
  D |- HeapPtr(t)

  D |- l
  -------------- (wf-t-single)
  D |- Single(l)

  D,D' |- G'
  D,D' |- S'
  D intersect D' = {}
  ------------------- (wf-t-code)
  D |- All[D'](G',S')

judgment: D |- G

  ... D |- t ...
  ------------------- (wf-G)
  D |- {...,r->t,...}

judgment: D |- S

  D |- l
  ------------ (wf-S-empty)
  D |- l:Empty

  D |- l
  P in D
  -------- (wf-S-P)
  D |- l:P

  D |- l
  D |- t
  D |- lq:Q
  forall lq',t',Q', if lq:Q => lq':(Q' /\ {l:t'}) then t = t'
  ----------------------------------------------------------- (wf-S-alias)
  D |- lq:(Q /\ {l:t})

  D |- l
  D |- t
  D |- S
  forall lq',l',t',Q', if S => lq':(Q' /\ {l':t'}) then l != l'
  ------------------------------------------------------------- (wf-S-concat)
  D |- l:(t::S)

judgment: |- (h,g,s,b)

  |-  h : H   
  {}; H |- s : S
  {}; H |- g : G
  {}; H; G, S |- b
  ----------------------------------------- (m-tp)
  |- (h,g,s,b)     

judgment: |- h : H

  H = {...,p->t,...}
  h = {...,p->v,...}
  ... {};H |- v : t ...
  ------------------------ (h-tp)
  |- h : H

judgment: D;H |- s : S

  D;H |- empty : (base:Empty)   (s-base)

  D;H,{p->HeapPtr(t)} |- s : (l:Q)
  -------------------------------------------(s-alias)
  D;H,{p->HeapPtr(t)} |- s : (l:(Q /\ {p:t}))

  D;H |- s : l:Q
  D;H;{} |- w : t
  ---------------------------- (s-concat)
  D;H |- w::s : next(l):t::l:Q

  D;H |- s : S
  S => S'
  ------------- (s-imp)
  D;H |- s : S'

judgment: D;H |- g : G

  G = {...,r->t,...}
  g = {...,r->w,...}
  ... D;H;{} |- w : t ...
  ----------------------- (g-tp)
  D;H |- g : G

judgment: D;H |- v : t

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

  H |- all[D'](G',S') b
  D |- All[D'](G',S')
  ---------------------------------------- (v-code)
  D;H |- all[D'](G',S') b : All[D'](G',S')

judgment: D;H;G |- o : t

  D;H;G |- r : G(r)  (o-reg)

  D;H;G |- i : int   (o-int)

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

  D;H;G |- p : H(p) (o-p-H)

  D;H;G |- p : Single(p) (o-p)

  D;H;G |- d : Single(d) (o-d)

  D;H;G |- o : All[L,D'](G',S)
  D |- l
  -------------------------------------- (o-inst-l)
  D;H;G |- o[l] : All[D'](G'[l/L],S[l/L])

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

judgment: |- (G,S){r<-t}(G',S')

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

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

judgment: D;H |- (G,S){ins}(G',S')

  D;H;G |- o : t
  |- (G;S){r<-t}(G';S')
  ---------------------------- (i-mov)
  D;H |- (G;S){mov r,o}(G';S')

  G(r) = Single(l)
  S |- l + i = l'
  (G;S) {r <- Single(l')} (G';S')
  -------------------------------- (i-ladd)
  D;H |- (G;S){ladd r,-4*i}(G';S')

  D;H;G |- o : int
  r ! = esp
  G(r) = int
  -------------------------- (i-add)
  D;H |- (G;S){add r,o}(G;S)

  D;H;G |- o : int
  r ! = esp
  G(r) = int
  -------------------------- (i-sub)
  D;H |- (G;S){sub 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')

  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')
  
  G(r1) = HeapPtr(t)
  G(r2) = t
  ---------------------------------- (i-store-p)
  D;H |- (G;S){store [r1+0],r2}(G;S)

  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')
  
  G(r1) = Single(l)
  S |- l : t 
  G(r2) = t
  ------------------------------------- (i-store-aliased)
  D;H |- (G;S){store [r1+0],r2}(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')

  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)

judgment: D;H;G;S |- b

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

  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

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

judgment: H |- block

  D;H;G;S |- b
  ------------------ (block-tp)
  H |- all[D](G,S) b

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

EVALUATION

arithmetic on d:
  d + 0 = d
  d + (n+1) = next(d) + n
  base + (-(n+1)) = base
  next(d) + (-(n+1)) = d + (-n)

size, resize:
  size(empty) = base
  size(w::s) = next(size(s))
  resize(size(s),s) = s
  resize(size(s) + (n+1), s) = nonsense::resize(size(s) + n, s)
  resize(size(s) + (-(n+1)), w::s) = resize(size(s) + (-n), s)

judgments:
  s(d) = w
  s' = s[d<-w]
  g |- o ==> w
  (g,s){r<-w}(g',s')
  (h,g,s,b) --> (h',g',s',b')

judgment: s(d) = w

  (w::s)(size(w::s)) = w   (s-lookup-top)

  s(d) = w
  --------------        (s-lookup)
  (w'::s)(d) = w

judgment: s' = s[d<-w]

  w'::s = (w::s)[size(w::s)<-w']  (s-assign-top)

  s' = s[d<-w]
  ----------------------       (s-assign)
  w'::s' = (w'::s)[d<-w]

judgment: g |- o ==> w

  g |- r ==> g(r)    (eo-r)

  g |- w ==> w	     (eo-w)

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

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

judgment: (g,s){r<-w}(g',s')

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

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

judgment: (h,g,s,b) --> (h',g',s',b')

  g |- o ==> w
  (g,s){r<-w}(g',s')
  ------------------------------------ (e-mov)
  (h,g,s,(mov r,o; b)) --> (h,g',s',b)

  g |- r ==> d
  (g,s){r<-d+i}(g',s')
  ------------------------------------ (e-ladd)
  (h,g,s,(ladd r,-4*i; b)) --> (h,g',s',b)

  g |- r ==> i1
  g |- o ==> i2
  (g,s){r<-i1+i2}(g',s')
  ------------------------------------ (e-add)
  (h,g,s,(add r,o; b)) --> (h,g',s',b)

  g |- r ==> i1
  g |- o ==> i2
  (g,s){r<-i1-i2}(g',s')
  ------------------------------------ (e-sub)
  (h,g,s,(sub r,o; b)) --> (h,g',s',b)

  g |- r2 ==> p
  h(p) = <w>
  (g,s){r1<-w}(g',s')
  ------------------------------------------- (e-load-p)
  (h,g,s,(load r1,[r2+0]; b)) --> (h,g',s',b)

  g |- r2 ==> d
  s(d+i) = w
  (g,s){r1<-w}(g',s')
  ------------------------------------------- (e-load-d)
  (h,g,s,(load r1,[r2+(-4*i)]; b)) --> (h,g',s',b)

  g |- r1 ==> p
  g |- r2 ==> w'
  h(p) = <w>
  ------------------------------------------------- (e-store-p)
  (h,g,s,(store [r1+0],r2; b)) --> (h[p <- <w'>],g,s,b)

  g |- r1 ==> d
  g |- r2 ==> w
  s' = s[d+i<-w]
  ------------------------------------------- (e-store-d)
  (h,g,s,(store [r1+(-4*i)],r2; b)) --> (h,g,s',b)

  g |- o ==> w
  p not in domain(h)
  h' = h,p-><w>
  (g,s){r<-p}(g',s')
  ---------------------------------------------- (e-heapalloc)
  (h,g,s,(heapalloc r = <o>;b)) --> (h',g',s',b)

  g |- r ==> i
  i != 0
  ------------------------------------- (e-jumpif0-false)
  (h,g,s,(jumpif0 r,o;b)) --> (h,g,s,b)

  g |- r ==> 0
  g |- o ==> p[subst]
  h(p) = all[D](G,S) b2
  ------------------------------------------------ (e-jumpif0-true)
  (h,g,s,(jumpif0 r,o;b1)) --> (h,g,s,b2[subst/D])

  g |- o ==> p
  (g,s){r<-p}(g',s')
  -------------------------------------------------- (e-unpack)
  (h,g,s,((L,r) = unpack(o);b)) --> (h,g',s',b[p/L])

  g |- o ==> p[subst]
  h(p) = all[D](G,S) b
  --------------------------------------- (e-jump)
  (h,g,s,(jump o)) --> (h,g,s,b[subst/D])

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