======
Syntax
======

for any item x, I write ~x for a sequence of x's. I write ~x[k] for the
kth element of the sequence.  I write ~x[k=xk] to set the kth element of
the list to xk.  We write length(~x) for the length of the sequence.

r resources
s environment
i instructions
b blocks of instructions
z run time statements (instructions or join points)
n integers
pi fractions
k process id

e ::= x | n | e + e
i ::= i1; i2 | x := e | x := [e] | [e1] := e2 | produce d e | consume d x | assert A | while e i | skip
    | [G1;A1]b1 || [G2;A2]b2
b ::= i; b | exit
z ::= b  |  halted  |  wait k1 k2; b

P ::= (r,s,z)            // a process

c : (Pred * Resource * value list * value list) list
~c[d] = (R, rG, q, hc)

S ::= (~c, ~P)               // ~c = a list of channel states
                             // ~P = processes

G ::= ~x                  // program variables in scope
D ::= ~(k:(G,A)) // list of continuations/process-ids and the environments/resources needed to invoke them

===============================================
Operations on histories:
===============================================

H1 : HistorySet

merge H1 H2 = H3
  s.t. for all h3, h1 in H1, h2 in H2, h3 = (some interleaving of h1 and h2)
        iff h3 is in H3
        

========================
Operations on resources:
========================

// permissions   pi : perm
pi : Share = [0,1]
no permission:      pi = 0
full permission:    pi = 1
partial permission: 0 < pi < 1

Endpoint = {(pi,H) : Share*HistorySet | pi=0 implies H={nil}}

r : { m: Location -> option value,
      p: ChannelName -> option Endpoint,
      c: ChannelName -> option Endpoint,
    }


 r1.m+r2.m = r3.m
 r1.p+r2.p = r3.p
 r1.c+r2.c = r3.c
------------------
    r1+r2 = r3

r.p(d) = (pi, H)
r.c(d) = (pi, H)

emp = \r. forall u, r.m(u)=None /\ forall d, r.p(d)=None /\ r.c(d)=None


Appending to the history
r[p(d)+= v] = r' where r'.m=r.m /\ r'.c=r.c /\ forall d'<>d, r'.p(d)=r.p(d) /\ r.p(d)=Some(pi,H) /\ r'.p(d)=Some(pi,v::H)
r[c(d)+= v] = r' where r'.m=r.m /\ r'.p=r.p /\ forall d'<>d, r'.c(d)=r.c(d) /\ r.c(d)=Some(pi,H) /\ r'.c(d)=Some(pi,v::H)



=====================
Operational Semantics
=====================


~P[k] = (r, s, x := e; b)      x in dom(s)
-------------------------------------------------------------(S-Assign)
(~c, ~P) -k-> (~c, ~P[k=(r,s[x=s[e]],b)])

~P[k] = (r, s, x := [e]; b)      x in dom(s) 
----------------------------------------------------------------(S-Fetch)
(~c, ~P) -k-> (~c, ~P[k=(r,s[x=r.h(s[e])],b)])

~P[k] = (r, s, [e1] := e2; b)
------------------------------------------------------------------(S-Store)
(~c, ~P) -k-> (~c, ~P[k=(r(h: s[e1] = s[e2]),s,b)])

~P[k] = (r, s, while e i; i)    s[e]=true
------------------------------------------------------------------(S-WhileTrue)
(~c, ~P) -k-> (~c, ~P[k=(r,s, i; while e i; b)])

~P[k] = (r, s, while e i; b)    s[e]=false
------------------------------------------------------------------(S-WhileFalse)
(~c, ~P) -k-> (~c, ~P[k=(r,s, b)])


~P[k] = (r, s, consume d x; b)
x in dom(s)
~c[d] = (R,rG+r',q@[v],hc)
rG;. |= R(q,v::hc)
--------------------------------------------------------------------(S-Consume)
(~c, ~P) -k-> (~c[d=(R,rG,q,v::hc)], ~P[k=((r+r')[c: d+=v],s[x=v], b)])

~P[k] = (r, s, consume d x; b)
~c[d] = (R,rG,nil,hc)
--------------------------------------------------------------------(S-BlockingConsume)
(~c, ~P) -k-> (~c, ~P)


~P[k] = (r, s, produce d e; b)
~c[d] = (R,rG,q,hc)
s[e] = v
r[p(d)+=v] = r1 + r2
rG+r1;. |= R(v::q,hc)
-------------------------------------------------------------------------------(S-Produce)
(~c, ~P) -k-> (~c[d=(R,rG+r1,v::q,hc)], ~P[k=(r2,s,b)])


~P[k] = (r, s, assert A; b)
r;s |= A*true
----------------------------------------------------------------------(S-Assert)
(~c, ~P) -k-> (~c, ~P[k=(r,s,b)])

~P[k] = (r, s, skip; b)
----------------------------------------------------------------------(S-Skip)
(~c, ~P) -k-> (~c, ~P[k=(r,s,b)])


~P[k] = (r, s, ([G1;A1]b1 || [G2;A2]b2); b]))
r = r1 + r2
s = s1 + s2
s1 disjoint s2
G1 = dom(s1)
G2 = dom(s2)
r1; s1 |= A1*true
r2; s2 |= A2
k1 = length(~P)
k2 = length(~P)+1
-----------------------------------------------------------------------(S-Fork)
(~c, ~P) -k-> (~c, ~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))

~P[k1] = (r1,s1, exit)
~P[k2] = (r2,s2, exit)
~P[k] = (.,., wait k1 k2; b))
--------------------------------------------------------------------------------(S-Wait)
(~c, ~P) -k-> (~c, ~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)]))

~P[k2] = (r2,s2,b2)
~P[k1] = (r1,s1,b1)
~P[k] = (.,., wait k1 k2; b)
b1 <> exit OR b2 <> exit
--------------------------------------------------------------------------------(S-BlockingWait)
(~c, ~P) -k-> (~c, ~P)

~P[k] = (r,s, (i1; i2); b)
--------------------------------------------------------------------------------(S-Seq)
(~c, ~P) -k-> (~c, ~P[k=(r,s, i1; (i2; b))])


~P[k] = (r,s, exit)
--------------------------------------------------------------------------------(S-Exit)
(~c, ~P) -k-> (~c, ~P)



============
Hoare Rules
============

x in G
-------------------------------(H-Assign)
~R;G |-i {A[e/x]} x := e {A}

x in G
-----------------------------------------------------------------------(H-Fetch)
~R;G |-i {exists x1.(e -> x1) * ((e -> x1) -* A[x1/x])} x := [e] {A}


----------------------------------------------------------------------(H-Store)
~R;G |-i {e1 -> - * ((e1 -> e2) -* A)} [e1] := e2 {A}

~R;G |-i {A/\e} i {A}
----------------------------------------------------------------------(H-While)
~R;G |-i {A} while e i {A/\!e}


(forall lq lc, SubIn pi (lq++lc) H -> B * ~R[d](lq,lc) |- ~R[d](v::lq,lc)
(d,pi,v::H)! =* B*A |- PNoHist d
-----------------------------------------------------------------------------------------(H-Produce)
~R;G |-i {(d,pi,H)! * ((d,pi,v::H)! =* B*A) /\ e|:v} produce d e {A}


x in G
forall lq v lc, SubIn pi lc H -> ~R[d](lq++v::nil,lc) |- B(v) * ~R[d](lq,v::lc)
forall v, ((d,pi,H)? * B(v))[c:d+=v] =* A[v/x]) |- CNoHist d
------------------------------------------------------------------------------- (H-Consume)
~R;G |-i {(d,pi,H)? * (forall v, ((d,pi,H)? * B(v))[c:d+=v] =* A[v/x])} consume d x {A}


-----------------------------(H-Assert)
~R;G |-i {A} assert A {A}

~R;G |-i {A} i1 {B}
~R;G |-i {B} i2 {C}
------------------------(H-Seq)
~R;G |-i {A} i1; i2 {C}

~R;G1 |-b {A1} b1 {B1}
~R;G2 |-b {A2} b2 {B2}
G1 disjoint G2
G1 + G2 subset G
FV(A1) subset G1
FV(A2) subset G2
A2 is precise
-----------------------------------------------------------------(H-Parallel)
~R;G |-i {A1*A2} [G1;A1]b1 || [G2;A2]b2 {B1*B2}


---------------------- (H-Skip)
~R;G |-i {A} skip {A}

~R;G,v |-i {A} i {B}    v not in G
-----------------------------------(H-Exists)
~R;G |-i {exists v. A} i {B}

~R;G |-i {A'} i {B'}    A |- A'   B' |- B   
-------------------------------------------- (H-Consequence)
~R;G |-i {A} i {B}


~R;G |-i {A} i {B}
FV(i) intersect FV(C) = empty
forall d in FV(i), C |- PNoHist d
forall d in FV(i), C |- CNoHist d
---------------------------------------------------------- (H-Frame)
~R;G |-i {A*C} i {B*C}


-----------------------------(H-Exit)
~R;G |-b  {A} exit {A}

~R;G |-i  {A} i {B}
~R;G |-b  {B} b {C} 
---------------------------(H-SeqBlock)
~R;G |-b  {A} i; b {C}

~R;G |-b  {A} b {C}
----------------------(H-BlockZ)
~R;G;D |-z  {A} b {C}


-----------------------------(H-HaltedZ)
~R;.;D |-z  {emp} halted {False}

D(k1) = (G1,B1)
D(k2) = (G2,B2)
G1 disjoint G2
~R;G1+G2 |-b  {B1 * B2} b {C}
-----------------------------------------------------------(H-ContZ)
~R;.;D |-z  {emp} wait k1 k2; b {C}



==========================
Well-formedness of states
==========================

 
Definition: total-res r  iff permissions sum to either 1/full or 0/none


rG;. |= R(q,hc)
forall lq lc, R(lq,lc) is precise and closed
forall lc, R(nil,lc) |- emp
emp |- R(nil,nil)
---------------------------------------------
d |- (R,rG,q,hc) ok


forall d. d |- ~c[d] ok
rt = forall+ k. ~P[k].r + forall+ d. ~c[d].rG
total-res rt                                   // all permissions are either 1 or 0, etc
forall d.  ~R[d] = ~c[d].R
forall k.  exists Ak. ~R;D;k |- ~P[k] : Ak
forall k1 k2.  k1!=k2  implies  dom(~P[k1].s) disjoint dom(~P[k2].s)
forall d R rG q hc.  ~c[d]=(R,rG,q,hc)  implies  (q@hc in rt.p(d).H)  and  (hc in rt.c(d).H)
|- ~P cont-ok
------------------------------------------------------------------
|- (~c, ~P) well-formed



forall k k1 k2 ... . ~P[k] = (.,., wait k1 k2; b)
   implies  k < k1 < k2  and  k2 < length(~P)
forall k1 k2 ... . ~P[k1] = (.,., wait k11 k12; b1) and ~P[k2] = (.,., wait k21 k22; b2) and k1<>k2
   implies  k11 <> k12 <> k21 <> k22
-------------------------------------------------------------------------
|- ~P cont-ok
 

r;s |= A
~R;dom(s);D |-z {A}z{B}
D(k) = (dom(s),B)
----------------------------------------------------------------------------(Process-Okay)
~R;D;k |- (r,s,z) : A



=====================
Semantics of Formulae
=====================

r;s |= (d,pi,e)!     iff r.p(d)=Some(pi,s[H]) /\ forall d'<>d, r.p(d')=None /\ forall d, r.c(d)=None /\ forall u, r.m(u)=None
r;s |= (d,pi,e)?     iff r.c(d)=Some(pi,s[H]) /\ forall d'<>d, r.c(d')=None /\ forall d, r.p(d)=None /\ forall u, r.m(u)=None

r;s |= e1 -> e2      iff r.m(s[e1])=s[e2] /\ forall u<>s[e1], r.m(u)=None /\ forall d, r.p(d)=r.c(d)=None

r;s |= A1 * A2       iff exists r1 r2. r=r1+r2 and r1;s |= A1 and r2;s |= A2
r;s |= A1 =* A2      iff forall r', (r disjoint r') implies r';s |= A1 implies r+r';s |= A2

r;s |= A ==> B       iff (r;s |= A) implies (r;s |= B)
r;s |= A /\ B        iff (r;s |= A) /\ (r;s |= B)
r;s |= A \/ B        iff (r;s |= A) \/ (r;s |= B)
r;s |= exists x. A   iff exists v. (r;s[x=v] |= A) (and x is not in dom(s) for <==)
r;s |= forall x. A   iff forall v. (r;s[x=v] |= A) (and x is not in dom(s) for <==)
.;s |= e1 = e2       iff s[e1]=s[e2]



Definition step:
(~c, ~P) --> (~c, ~P) := forall k, (~c, ~P) -k-> (~c, ~P)


----------(StartStep1)
 S -->* S

 S --> S'  S' -->* S''
-----------------------(StarStep2)
 S -->* S''

=====================
Useful Lemmas
=====================
 


Lemma Preservation: forall S S' k.
  If |- S well-formed and S -k-> S' then |- S' well-formed.

Definition: halted S k
  forall ~cont ~j ~~hp ~~hc r s contk, S = (~c, ~P) implies
    ~P[k] = (r,s,exit) or ~P[k] = (.,.,halted)


Definition:  Stuck State:
  A state S is *not* stuck when either
  (1) S --> S', or
  (2) forall k. halted S k
  
Definition: Safe State:
  A state S is ``safe'' when for all k, either
  (1) exists S', S -k-> S'
  (2) halted S k

Lemma Progress:
  If |- S well-formed then S is safe




Lemma Fresh-Var: forall s. exists x. x not in dom(s)

Lemma ihoare_inv: forall R A B i, R;G |-i {A} i {B} -> exists A' B' C,
      A |- A'*C /\ B'*C |- B /\ (FV(i) intersect FV(C) = empty) /\ R;G |-i {A'} i {B'} /\
      forall d in FV(i), C |- PNoHist d /\
      forall d in FV(i), C |- CNoHist d
      /\ F(C) subset G.
    And:
      if i = x:=e, then A' = AA[e/x], B'= AA, x in G
      if i = x:=[e], then A' = exists x1.(e -> x1) * ((e -> x1) -* AA[x1/x]), B'=AA, x in G
      if i = ..., A' =, B'=, ...
Proved by induction on R |-i {A} i {B}.


Lemma histfree_ppush_star:
  B|-PNoHist d implies r;s |= A*B implies r[p: d+=v];s|= A[p:d+=v] * B
Lemma histfree_cpush_star:
  B|-CNoHist d implies r;s |= A*B implies r[c: d+=v];s|= A[c:d+=v] * B

Lemma subst_free_star:
  x not in FV(F)  implies  r;s|=A[e/x]*F  implies  r;s[x=s[e]] |= A*F

Lemma heap_upd_frame: r;s |= e -> - * B  implies  r[h(l) = v];s |= e -> v * B

Lemma block_consequence:
  ~R;G |-b {A'} b {B'}  implies  A |- A'  implies  B' |- B  implies  ~R;G |-b {A} b {B}
Proof: By induction on b.

Lemma block_frame: ~R;G |-b {A} b {B}  implies  FV(b) intersect FV(C) = empty  implies
    forall d in FV(b), C |- PNoHist d  implies  forall d in FV(b), C |- CNoHist d  implies
  ~R;G |-b {A*C} b {B*C}.
Proof: by induction on b


Lemma shrink_env: forall r s s' G A. r;s |= A implies FV(A) subset dom(s') implies s' subset s implies r;s' |= A

Lemma grow_env: forall r s s'. r;s |= A implies dom(s) disjoint dom(s') implies r;s+s' |= A