// -*- apollo -*-



//-- bind-top.p
bind x = 1 {top} in true

sugar =   bind x = 1 {top} in true
src   =   bind x = 1 {top} in true
type  =   bool {top}
eval  =   true



//-- bind-trust.p
def alice, bob. fun c:cert.
if c => 'alice #> 'declassify then
  if c => 'bob #> 'declassify then
    <bind x = 1{T alice bob} in \x,
    bind y = 1{T alice} in \y,
    bind z = 1{T bob} in \z>
  else 2
else 3

sugar =  def alice,bob. fun c : cert. if c => 'alice #> 'declassify  then if c => 'bob #> 'declassify  then <bind x = 1 {T alice bob} in \ x,bind y = 1 {T alice} in \ y,bind z = 1 {T bob} in \ z> else 2 else 3
src   =  def alice,bob. fun c : cert. if c => 'alice #> 'declassify bot then if c => 'bob #> 'declassify bot then <bind x = 1 {T alice#bob} in \ x,bind y = 1 {T alice} in \ y,bind z = 1 {T bob} in \ z> else 2 else 3
bind-trust.p:04:34: Escape: checking env |- m : t where
bind-trust.p:04:34:   env =  alice<:top, bob<:top, c:cert, alice<:declassify bot, bob<:declassify bot, x:int
bind-trust.p:04:34:    m  =  x
bind-trust.p:04:15:    t  =  int
bind-trust.p:05:29: Escape: checking env |- m : t where
bind-trust.p:05:29:   env =  alice<:top, bob<:top, c:cert, alice<:declassify bot, bob<:top, y:int
bind-trust.p:05:29:    m  =  y
bind-trust.p:05:14:    t  =  int
bind-trust.p:06:27: Escape: checking env |- m : t where
bind-trust.p:06:27:   env =  alice<:top, bob<:top, c:cert, alice<:top, bob<:declassify bot, z:int
bind-trust.p:06:27:    m  =  z
bind-trust.p:06:14:    t  =  int
type  =  def alice,bob. cert -> top
eval  =  def alice,bob. fun c : cert. if c => 'alice #> 'declassify bot then if c => 'bob #> 'declassify bot then <bind x = 1 {T alice#bob} in \ x,bind y = 1 {T alice} in \ y,bind z = 1 {T bob} in \ z> else 2 else 3



//-- cert-acq.p
def alice,bob.
(fun c:cert. if c => 'alice #> '(delegate bob) then 1 else 2)
(acquire 'alice #> '(delegate bob))

sugar =  def alice,bob. ( fun c : cert. if c => 'alice #> '( delegate bob ) then 1 else 2 ) ( acquire 'alice #> '( delegate bob ) )
src   =  def alice,bob. fun c : cert. if c => 'alice #> 'delegate bob then 1 else 2 acquire 'alice #> 'delegate bob
type  =  def alice,bob. int
cert-acq.p:03:02: Acquiring alice #> delegate bob...
eval  =  def alice,bob.1



//-- cert-dcls.p
def alice.
poly p. fun pid:'p, c:cert, x:bool{R p top}.
  if c => pid #> 'declassify then
    declassify x as bool{R p alice}
  else
    true{R p alice}

sugar =  def alice. poly p. fun pid : 'p,c : cert,x : bool {R p top}. if c => pid #> 'declassify  then declassify x as bool {R p alice} else true {R p alice}
src   =  def alice. poly p<:top. fun pid : 'p. fun c : cert. fun x : bool {R p top}. if c => pid #> 'declassify bot then declassify x as bool {R p alice} else true {R p alice}
type  =  def alice. all p<:top. 'p -> cert -> bool {R p top} -> bool {R p alice}
eval  =  def alice. poly p<:top. fun pid : 'p. fun c : cert. fun x : bool {R p top}. if c => pid #> 'declassify bot then declassify x as bool {R p alice} else true {R p alice}



//-- cert-dcls2.p
def alice,bob,eve.
fun c:cert, x:bool{R alice}.
if c => 'alice #> '(declassify bob&eve) then
  <declassify x as bool{R alice bob},
   declassify x as bool{R alice eve}>
else
  error "fail"

sugar =  def alice,bob,eve. fun c : cert,x : bool {R alice}. if c => 'alice #> '( declassify bob&eve ) then <declassify x as bool {R alice bob},declassify x as bool {R alice eve}> else error "fail"
src   =  def alice,bob,eve. fun c : cert. fun x : bool {R alice top}. if c => 'alice #> 'declassify bob&eve then <declassify x as bool {R alice bob},declassify x as bool {R alice eve}> else error "fail"
type  =  def alice,bob,eve. cert -> bool {R alice top} -> <bool {R alice bob},bool {R alice eve}>
eval  =  def alice,bob,eve. fun c : cert. fun x : bool {R alice top}. if c => 'alice #> 'declassify bob&eve then <declassify x as bool {R alice bob},declassify x as bool {R alice eve}> else error "fail"



//-- cert-del.p
def alice,bob.
fun c1:cert, c2:cert, x:bool{R alice top}.
  if c1 => 'alice #> '(delegate bob) then
    delegate 'alice <: 'bob in
    if c2 => 'bob #> 'declassify then
      declassify x as bool{R bob bot}
    else
      true{R bob bot}
  else
    true{R bob bot}

sugar =  def alice,bob. fun c1 : cert,c2 : cert,x : bool {R alice top}. if c1 => 'alice #> '( delegate bob ) then delegate 'alice<:'bob in if c2 => 'bob #> 'declassify  then declassify x as bool {R bob bot} else true {R bob bot} else true {R bob bot}
src   =  def alice,bob. fun c1 : cert. fun c2 : cert. fun x : bool {R alice top}. if c1 => 'alice #> 'delegate bob then delegate 'alice<:'bob in if c2 => 'bob #> 'declassify bot then declassify x as bool {R bob bot} else true {R bob bot} else true {R bob bot}
type  =  def alice,bob. cert -> cert -> bool {R alice top} -> bool {R bob bot}
eval  =  def alice,bob. fun c1 : cert. fun c2 : cert. fun x : bool {R alice top}. if c1 => 'alice #> 'delegate bob then delegate 'alice<:'bob in if c2 => 'bob #> 'declassify bot then declassify x as bool {R bob bot} else true {R bob bot} else true {R bob bot}



//-- effect-hl.p
def h, l<:h. (fun x:{h}int. true) ({l} return 3)


sugar =  def h,l<:h. ( fun x : {h} int. true ) ( {l} return 3 )
src   =  def h,l<:h. fun x : {h} int. true {l} return 3
effect-hl.p:01:14: Subtype error: fail to prove m1:t1<:t2 when checking env |- m0 where
effect-hl.p:01:14:   env =  h<:top, l<:h
effect-hl.p:01:14:    m0 =  fun x : {h} int. true {l} return 3
effect-hl.p:01:36:    m1 =  {l} return 3
effect-hl.p:01:36:    t1 =  {l&top} int
effect-hl.p:01:21:    t2 =  {h} int



//-- effect-lh.p
def h, l<:h. (fun x:{l}int. true) ({h} return 3)

sugar =  def h,l<:h. ( fun x : {l} int. true ) ( {h} return 3 )
src   =  def h,l<:h. fun x : {l} int. true {h} return 3
type  =  def h,l<:h. bool
eval  =  def h,l<:h. true



//-- effect-print1.p
def h, l<:h. fun print : all a. (int{a}) -> ({a}<>).
  fun x: int{h}. ({h} run y = print [h] x in return <>)

sugar =  def h,l<:h. fun print : all a. ( int {a} ) -> ( {a} <> ). fun x : int {h}. ( {h} run y = print [h] x in return <> )
src   =  def h,l<:h. fun print : all a<:top. int {a} -> {a} <>. fun x : int {h}. {h} run y = print [h] x in return <>
type  =  def h,l<:h. all a<:top. int {a} -> {a} <> -> int {h} -> {h&h&top} <>
eval  =  def h,l<:h. fun print : all a<:top. int {a} -> {a} <>. fun x : int {h}. {h} run y = print [h] x in return <>



//-- effect-print2.p
def h, l<:h. fun print : all a. (int{a}) -> ({a}<>).
  let f = fun x: int{h}. {h} run y = print [h] x in return <> in
  let g = fun w: (int{h})->({l}<>). w (3{l}) in
  g f

sugar =  def h,l<:h. fun print : all a. ( int {a} ) -> ( {a} <> ). let f = fun x : int {h}. {h} run y = print [h] x in return <> in let g = fun w : ( int {h} ) -> ( {l} <> ). w ( 3 {l} ) in g f
src   =  def h,l<:h. fun print : all a<:top. int {a} -> {a} <>. let f = fun x : int {h}. {h} run y = print [h] x in return <> in let g = fun w : int {h} -> {l} <>. w 3 {l} in g f
type  =  def h,l<:h. all a<:top. int {a} -> {a} <> -> {l} <>
eval  =  def h,l<:h. fun print : all a<:top. int {a} -> {a} <>. let f = fun x : int {h}. {h} run y = print [h] x in return <> in let g = fun w : int {h} -> {l} <>. w 3 {l} in g f



//-- effect-run.p
def e1, e2.
run x = 
  {e2} run y = {e1} return 1 in 
    return y+2 in
  return x+3

sugar =  def e1,e2. run x = {e2} run y = {e1} return 1 in return y + 2 in return x + 3
src   =  def e1,e2. run x = {e2} run y = {e1} return 1 in return y + 2 in return x + 3
type  =  def e1,e2. {e2&e1&top&top&top} int
effect-run.p:03:16: Running effect: e1
effect-run.p:03:03: Running effect: e2
eval  =  def e1,e2. return 6



//-- escape.p
bind x = \((1+2) {top}) in true

sugar =   bind x = \ ( ( 1 + 2 ) {top} ) in true
src   =   bind x = \ 1 + 2 {top} in true
escape.p:01:12: Escape: checking env |- m : t where
escape.p:01:12:   env =  
escape.p:01:12:    m  =  1 + 2 {top}
escape.p:01:12:    t  =  int {top}
type  =   bool {top}
escape.p:01:12: Escape: evaluating env |- m -> v where
escape.p:01:12:   env =  
escape.p:01:12:    m  =  1 + 2 {top}
escape.p:01:12:    v  =  3 {top}
eval  =   true



//-- index-open.p
// open-term substitution
def y. (fun x:'y. fun z:int. x) ('y)

sugar =  def y. ( fun x : 'y. fun z : int. x ) ( 'y )
src   =  def y. fun x : 'y. fun z : int. x 'y
type  =  def y. int -> 'y
eval  =  def y. fun z : int. 'y



//-- label-bind.p
def h,l<:h. (fun x:int{h}. bind y=x in (y+1){h}) (4{l})

sugar =  def h,l<:h. ( fun x : int {h}. bind y = x in ( y + 1 ) {h} ) ( 4 {l} )
src   =  def h,l<:h. fun x : int {h}. bind y = x in y + 1 {h} 4 {l}
type  =  def h,l<:h. int {h}
eval  =  def h,l<:h.5 {h}



//-- label-flow.p
def h,l<:h. (fun x:int{l}. bind y=x in (y+1){h}) (4{h})

sugar =  def h,l<:h. ( fun x : int {l}. bind y = x in ( y + 1 ) {h} ) ( 4 {h} )
src   =  def h,l<:h. fun x : int {l}. bind y = x in y + 1 {h} 4 {h}
label-flow.p:01:13: Subtype error: fail to prove m1:t1<:t2 when checking env |- m0 where
label-flow.p:01:13:   env =  h<:top, l<:h
label-flow.p:01:13:    m0 =  fun x : int {l}. bind y = x in y + 1 {h} 4 {h}
label-flow.p:01:51:    m1 =  4 {h}
label-flow.p:01:51:    t1 =  int {h}
label-flow.p:01:20:    t2 =  int {l}



//-- label-hash.p
def h,l<:h. fun x:int{h}. bind y=x in (y+1){l}

sugar =  def h,l<:h. fun x : int {h}. bind y = x in ( y + 1 ) {l}
src   =  def h,l<:h. fun x : int {h}. bind y = x in y + 1 {l}
type  =  def h,l<:h. int {h} -> int {h}
eval  =  def h,l<:h. fun x : int {h}. bind y = x in y + 1 {l}



//-- label-ifsub1.p
poly a,b. fun x:'a, y:'b, z:a, w:b. if x<:y then z else w

sugar =   poly a,b. fun x : 'a,y : 'b,z : a,w : b. if x<:y then z else w
src   =   poly a<:top. poly b<:top. fun x : 'a. fun y : 'b. fun z : a. fun w : b. if x<:y then z else w
type  =   all a<:top. all b<:top. 'a -> 'b -> a -> b -> b
eval  =   poly a<:top. poly b<:top. fun x : 'a. fun y : 'b. fun z : a. fun w : b. if x<:y then z else w



//-- label-ifsub2.p
(poly a,b. fun x:'a, y:'b, z:a, w:b. if x<:y then z else w) [int,int] ('int) ('int) 3 4

sugar =   ( poly a,b. fun x : 'a,y : 'b,z : a,w : b. if x<:y then z else w ) [int,int] ( 'int ) ( 'int ) 3 4
src   =   poly a<:top. poly b<:top. fun x : 'a. fun y : 'b. fun z : a. fun w : b. if x<:y then z else w [int][int] 'int 'int 3 4
type  =   int
eval  =   3



//-- label-ifsub3.p
(poly a,b. fun x:'a, y:'b, z:a, w:b. if x<:y then z else w) [int,bool] ('int) ('bool) 3 true
sugar =   ( poly a,b. fun x : 'a,y : 'b,z : a,w : b. if x<:y then z else w ) [int,bool] ( 'int ) ( 'bool ) 3 true
src   =   poly a<:top. poly b<:top. fun x : 'a. fun y : 'b. fun z : a. fun w : b. if x<:y then z else w [int][bool] 'int 'bool 3 true
type  =   bool
eval  =   true



//-- label-ifsub4.p
def root. poly user.
fun uid : 'user.
fun print : (int{user}) -> <>. 
fun x : int{root}.
  if 'root <: uid then 
    print x
  else
    <>

sugar =  def root. poly user. fun uid : 'user. fun print : ( int {user} ) -> <>. fun x : int {root}. if 'root<:uid then print x else <>
src   =  def root. poly user<:top. fun uid : 'user. fun print : int {user} -> <>. fun x : int {root}. if 'root<:uid then print x else <>
type  =  def root. all user<:top. 'user -> int {user} -> <> -> int {root} -> <>
eval  =  def root. poly user<:top. fun uid : 'user. fun print : int {user} -> <>. fun x : int {root}. if 'root<:uid then print x else <>



//-- label-join.p
def h,l<:h. if true then 1{l} else 1{h}

sugar =  def h,l<:h. if true then 1 {l} else 1 {h}
src   =  def h,l<:h. case true of  fun $x : <>.1 {l}|fun $x : <>.1 {h}
type  =  def h,l<:h. int {h}
eval  =  def h,l<:h.1 {l}



//-- label-join2.p
def h,l<:h. if true then fun x:int{l}. 1 else fun x:int{h}. 1

sugar =  def h,l<:h. if true then fun x : int {l}.1 else fun x : int {h}.1
src   =  def h,l<:h. case true of  fun $x : <>. fun x : int {l}.1|fun $x : <>. fun x : int {h}.1
type  =  def h,l<:h. int {l} -> int
eval  =  def h,l<:h. fun x : int {l}.1



//-- parse-app.p
(fun x:'int. 1) 'int

Parse error: missing parenthesis in function application?



//-- parse-error.p
open x = 1 with 3

parse-error.p:01:12: Parse error
  prefix:  Open: 'open'x '='m 'with'
  rule  :  Open: 'open'x '='m 'with'a ++ ',''in'm



//-- parse-prefix.p
if 1

parse-prefix.p:01:01: Parse error
  prefix:  Ifcert: 'if'm
  rule  :  Ifcert: 'if'm '=>'m '#>'m 'then'm 'else'm
or
  prefix:  Ifsub: 'if'm
  rule  :  Ifsub: 'if'm '<:'m 'then'm 'else'm



//-- sugar-fun.p
poly x. fun a:x, b:x, c:x. 1

sugar =   poly x. fun a : x,b : x,c : x.1
src   =   poly x<:top. fun a : x. fun b : x. fun c : x.1
type  =   all x<:top. x -> x -> x -> int
eval  =   poly x<:top. fun a : x. fun b : x. fun c : x.1



//-- sugar-if.p
(fun k:int. if true then k else k) 1

sugar =   ( fun k : int. if true then k else k ) 1
src   =   fun k : int. case true of  fun $x : <>. k|fun $x : <>. k 1
type  =   int
eval  =   1



//-- sugar-let.p
let x = fun x:int. x in x 3

sugar =   let x = fun x : int. x in x 3
src   =   let x = fun x : int. x in x 3
type  =   int
eval  =   3



//-- sugar-match.p
let <x,y,z> = <1,2,3> in x

sugar =   let <x,y,z> = <1,2,3> in x
src   =   let x = <1,2,3>.1 in let y = <1,2,3>.2.1 in let z = <1,2,3>.2.2.1 in x
type  =   int
eval  =   1



//-- sugar-open.p
open x = 1 with c,d in x [c,d]

sugar =   open x = 1 with c,d in x [c,d]
src   =   open $x = 1 with c in open x = $x with d in x [c][d]
sugar-open.p:01:01: Form error: m:t is not a some when checking env |- m0 where
sugar-open.p:01:01:    m0 =  open $x = 1 with c in open x = $x with d in x [c][d]
sugar-open.p:01:10:    m  =  1
sugar-open.p:01:10:    t  =  int



//-- sugar-open2.p
open x = pack pack 1 with int as some a. a with bool as some a,b. b with b,b2 in 2

sugar =   open x = pack pack 1 with int as some a. a with bool as some a,b. b with b,b2 in 2
src   =   open $x = pack pack 1 with int as some a<:top. a with bool as some a<:top. some b<:top. b with b in open x = $x with b2 in 2
type  =   int
eval  =   2



//-- sugar-poly.p
poly a,b<:a,c<:a,d<:b,e<:d. 1

sugar =   poly a,b<:a,c<:a,d<:b,e<:d.1
src   =   poly a<:top. poly b<:a. poly c<:a. poly d<:b. poly e<:d.1
type  =   all a<:top. all b<:a. all c<:a. all d<:b. all e<:d. int
eval  =   poly a<:top. poly b<:a. poly c<:a. poly d<:b. poly e<:d.1



//-- sugar-prj.p
<<1,"a",3,4>.1, <1,"a",3,4>.2, <1,"a",3,4>.3>
sugar =   <<1,"a",3,4>.1,<1,"a",3,4>.2,<1,"a",3,4>.3>
src   =   <<1,"a",3,4>.1,<1,"a",3,4>.2.1,<1,"a",3,4>.2.2.1>
type  =   <int,string,int>
eval  =   <1,"a",3>



//-- sugar-shadow.p
def y. (fun x:'y. fun y:int. x) ('y)

sugar =  def y. ( fun x : 'y. fun y : int. x ) ( 'y )
sugar-shadow.p:01:19: Shadow error: binder variable yequals to toplevel type variable



//-- sugar-shadow2.p
fun x:int. fun x:int. 1

sugar =   fun x : int. fun x : int.1
src   =   fun x : int. fun x : int.1
type  =   int -> int -> int
eval  =   fun x : int. fun x : int.1



//-- sugar-sub.p
(poly a. fun x:a, y:int. <x,y>) [int] 1

sugar =   ( poly a. fun x : a,y : int. <x,y> ) [int] 1
src   =   poly a<:top. fun x : a. fun y : int. <x,y> [int] 1
type  =   int -> <int,int>
eval  =   fun y : int. <1,y>



//-- type-form.p
case 1@1 as int+int of 1 | (fun x:int. x)

sugar =   case 1 @ 1 as int + int of  1|( fun x : int. x )
src   =   case 1 @ 1 as int + int of  1|fun x : int. x
type-form.p:01:01: Form error: m:t is not a function when checking env |- m0 where
type-form.p:01:01:    m0 =  case 1 @ 1 as int + int of  1|fun x : int. x
type-form.p:01:24:    m  =  1
type-form.p:01:24:    t  =  int



//-- type-promote.p
poly a<:int->int. fun x:a. x 1

sugar =   poly a<:int -> int. fun x : a. x 1
src   =   poly a<:int -> int. fun x : a. x 1
type  =   all a<:int -> int. a -> int
eval  =   poly a<:int -> int. fun x : a. x 1



//-- type-promote2.p
// do not promote
def a. (fun x:a->a. fun y:a. x y) (fun z:a. z)

sugar =  def a. ( fun x : a -> a. fun y : a. x y ) ( fun z : a. z )
src   =  def a. fun x : a -> a. fun y : a. x y fun z : a. z
type  =  def a. a -> a
eval  =  def a. fun y : a. fun z : a. z y



//-- type-scope.p
open x = pack 11 with int as some a. a with b in x

sugar =   open x = pack 11 with int as some a. a with b in x
src   =   open x = pack 11 with int as some a<:top. a with b in x
type-scope.p:01:01: Scope error: m:t is not closed when checking env |- m0 where
type-scope.p:01:01:   env =  
type-scope.p:01:01:    m0 =  open x = pack 11 with int as some a<:top. a with b in x
type-scope.p:01:50:    m  =  x
type-scope.p:01:01:    t  =  b



//-- index-open2.pp
fun z:(some a,b. <a,b>).
  open y=z with c,d in   
  y; 1

sugar =   fun z : ( some a,b. <a,b> ). open y = z with c,d in y ; 1
src   =   fun z : some a<:top. some b<:top. <a1,b0>. open $x = z0 with c in open y = $x0 with d in y0 ; 1
index-open2.pp:03:03: Subtype warning: fail to prove m1:t1<:t2 when checking env |- m0 where
index-open2.pp:03:03:   env =  z:some a<:top. some b<:top. <a1,b0>, c<:top, $x:some b<:top. <c1,b0>, d<:top, y:<c2,d0>
index-open2.pp:03:03:    m0 =  y0 ; 1
index-open2.pp:03:03:    m1 =  y0
index-open2.pp:01:18:    t1 =  <c3,d1>
index-open2.pp:03:03:    t2 =  <>
type  =   some a<:top. some b<:top. <a1,b0> -> int
eval  =   fun z : some a<:top. some b<:top. <a1,b0>. open $x = z0 with c in open y = $x0 with d in y0 ; 1



//-- eg-bank.pp
def atm,alice,bank,prt.
def withdraw.
fun login : <> -> <some user. 'user,cert>{R atm atm}.
fun request : all agent,user. 
  <'agent,'user,cert,cert>{R bank bank} -> int{R agent agent, T agent}.
fun listen : <> -> (some agent,user. <'agent,'user,cert,cert,
  (int{R agent agent} -> <>)>){R bank bank, T bank}.
fun print : int{R atm prt} -> <>.
fun get : all user. ('user) -> int{R user&bank bank}.
fun set : all user. ('user) -> int{R user&bank bank} -> <>.

< 
  fun u:<>.
  if (acquire 'atm #> '(declassify bank)) 
    => 'atm #> '(declassify bank) then
    bind x = login <> in
    let <y,cdel> = x in
    open userid = y with user in
    let creq = acquire userid #> withdraw in
    let msg = <'atm, userid, cdel, creq> in
    let dmsg = declassify msg as <'atm,'user,cert,cert>{R bank bank} in
    bind balance = request [atm,user] dmsg in
    if (acquire 'atm #> '(declassify prt)) 
      => 'atm #> '(declassify prt) then
      let dbalance = declassify balance as int{R atm prt} in    
      print dbalance
    else <>
  else error "insecure network"
,
  fun u:<>.
  bind x0 = listen <>, x=x0 in
  open y = x with agent, user in
  if (acquire 'bank #> '(declassify user))
    => 'bank #> '(declassify user) then
    let <agentid,userid,cdel,creq,reply> = y in
    if cdel => userid #> '(delegate agent) then
      delegate userid <: agentid in
      if creq => userid #> 'withdraw then
        let old = get [user] userid in
        let balance = bind x = old in x - 100 in
        let y = set [user] userid balance in
        let dbalance = declassify balance as int{R user user} in
        reply dbalance
      else <>
    else error "insecure atm"
  else error "insecure network"
>

sugar =  def atm,alice,bank,prt. def withdraw. 
fun login : <> -> <some user. 'user,cert> {R atm atm}. 
fun request : all agent,user. <'agent,'user,cert,cert> {R bank bank} -> int {R agent agent,T agent}. 
fun listen : <> -> ( some agent,user. <'agent,'user,cert,cert,( int {R agent agent} -> <> )> ) {R bank bank,T bank}. 
fun print : int {R atm prt} -> <>. 
fun get : all user. ( 'user ) -> int {R user&bank bank}. 
fun set : all user. ( 'user ) -> int {R user&bank bank} -> <>. <
fun u : <>. 
if ( acquire 'atm #> '( declassify bank ) ) => 'atm #> '( declassify bank ) then 
bind x = login <> in let <y,cdel> = x in 
open userid = y with user in 
let creq = acquire userid #> withdraw in 
let msg = <'atm,userid,cdel,creq> in 
let dmsg = declassify msg as <'atm,'user,cert,cert> {R bank bank} in 
bind balance = request [atm,user] dmsg in 
if ( acquire 'atm #> '( declassify prt ) ) => 'atm #> '( declassify prt ) then 
let dbalance = declassify balance as int {R atm prt} in print dbalance else <> else error "insecure network",
fun u : <>. 
bind x0 = listen <>,x = x0 in 
open y = x with agent,user in 
if ( acquire 'bank #> '( declassify user ) ) => 'bank #> '( declassify user ) then let <agentid,userid,cdel,creq,reply> = y in 
if cdel => userid #> '( delegate agent ) then delegate userid<:agentid in 
if creq => userid #> 'withdraw then 
let old = get [user] userid in 
let balance = 
bind x = old in x - 100 in 
let y = set [user] userid balance in 
let dbalance = declassify balance as int {R user user} in reply dbalance else <> else error "insecure atm" else error "insecure network">

****

src   =  def atm,alice,bank,prt. def withdraw. 
fun login : <> -> <some user<:top. 'user,cert> {R atm atm}. 
fun request : all agent<:top. all user<:top. <'agent,'user,cert,cert> {R bank bank} -> int {R agent agent} {T agent}. 
fun listen : <> -> some agent<:top. some user<:top. <'agent,'user,cert,cert,int {R agent agent} -> <>> {R bank bank} {T bank}. 
fun print : int {R atm prt} -> <>. 
fun get : all user<:top. 'user -> int {R user&bank bank}. 
fun set : all user<:top. 'user -> int {R user&bank bank} -> <>. <
fun u : <>. 
if acquire 'atm #> 'declassify bank => 'atm #> 'declassify bank then 
bind x = login <> in 
let y = x.1 in 
let cdel = x.2.1 in 
open userid = y with user in 
let creq = acquire userid #> withdraw in 
let msg = <'atm,userid,cdel,creq> in 
let dmsg = declassify msg as <'atm,'user,cert,cert> {R bank bank} in 
bind balance = request [atm][user] dmsg in 
if acquire 'atm #> 'declassify prt => 'atm #> 'declassify prt then 
let dbalance = declassify balance as int {R atm prt} in print dbalance else <> else error "insecure network",
fun u : <>. 
bind x0 = listen <> in 
bind x = x0 in 
open $x = x with agent in 
open y = $x with user in 
if acquire 'bank #> 'declassify user => 'bank #> 'declassify user then 
let agentid = y.1 in 
let userid = y.2.1 in 
let cdel = y.2.2.1 in 
let creq = y.2.2.2.1 in 
let reply = y.2.2.2.2.1 in 
if cdel => userid #> 'delegate agent then delegate userid<:agentid in 
if creq => userid #> 'withdraw then 
let old = get [user] userid in 
let balance = 
bind x = old in x - 100 in 
let y = set [user] userid balance in 
let dbalance = declassify balance as int {R user user} in reply dbalance else <> else error "insecure atm" else error "insecure network">

****

type  =  def atm,alice,bank,prt. def withdraw. <> -> <some user<:top. 'user,cert> {R atm atm} -> all agent<:top. all user<:top. <'agent,'user,cert,cert> {R bank bank} -> int {R agent agent} {T agent} -> <> -> some agent<:top. some user<:top. <'agent,'user,cert,cert,int {R agent agent} -> <>> {R bank bank} {T bank} -> int {R atm prt} -> <> -> all user<:top. 'user -> int {R user&bank bank} -> all user<:top. 'user -> int {R user&bank bank} -> <> -> <<> -> <>,<> -> <>>

****

eval  =  def atm,alice,bank,prt. def withdraw. 
fun login : <> -> <some user<:top. 'user,cert> {R atm atm}. 
fun request : all agent<:top. all user<:top. <'agent,'user,cert,cert> {R bank bank} -> int {R agent agent} {T agent}. 
fun listen : <> -> some agent<:top. some user<:top. <'agent,'user,cert,cert,int {R agent agent} -> <>> {R bank bank} {T bank}. 
fun print : int {R atm prt} -> <>. 
fun get : all user<:top. 'user -> int {R user&bank bank}. 
fun set : all user<:top. 'user -> int {R user&bank bank} -> <>. <
fun u : <>. 
if acquire 'atm #> 'declassify bank => 'atm #> 'declassify bank then 
bind x = login <> in 
let y = x.1 in 
let cdel = x.2.1 in 
open userid = y with user in 
let creq = acquire userid #> withdraw in 
let msg = <'atm,userid,cdel,creq> in 
let dmsg = declassify msg as <'atm,'user,cert,cert> {R bank bank} in 
bind balance = request [atm][user] dmsg in 
if acquire 'atm #> 'declassify prt => 'atm #> 'declassify prt then 
let dbalance = declassify balance as int {R atm prt} in print dbalance else <> else error "insecure network",
fun u : <>. 
bind x0 = listen <> in 
bind x = x0 in 
open $x = x with agent in 
open y = $x with user in 
if acquire 'bank #> 'declassify user => 'bank #> 'declassify user then 
let agentid = y.1 in 
let userid = y.2.1 in 
let cdel = y.2.2.1 in 
let creq = y.2.2.2.1 in 
let reply = y.2.2.2.2.1 in 
if cdel => userid #> 'delegate agent then delegate userid<:agentid in 
if creq => userid #> 'withdraw then 
let old = get [user] userid in 
let balance = 
bind x = old in x - 100 in 
let y = set [user] userid balance in 
let dbalance = declassify balance as int {R user user} in reply dbalance else <> else error "insecure atm" else error "insecure network">