(***

   RT^2 role membership specification.

   Note that LolliMon types enforce typing component of variable
   "safety" in credentials.

***)

(* less than or equal to *)
leq : int -> int -> o.
leq X X.
leq X Y <= Y > X.

(* core types *)
entity : type.
role_name : type.
role_expr : type.
pconstraint : type.

(* role expression constructors *)
^ : entity -> role_expr.
role : entity -> role_name -> role_expr.
linked_role : entity -> role_name -> role_name -> role_expr.
inter : list role_expr -> role_expr.

(* role name parameter constraint constructors *)
intc : int -> int -> int -> pconstraint.
thisc : entity -> pconstraint.
osetc : entity -> role_expr -> pconstraint.

(* credentials are facts *)

entry : o -> o.
credential : entity -> role_name -> role_expr -> list pconstraint -> o.

(* role name parameter constraint interpretation *)
interp : list pconstraint -> entity -> o.

(* role membership predicates *)
ismem : role_expr -> entity -> o.
ismems : list role_expr -> entity -> o.
auth : role_expr -> entity -> o. 


credential A R (^ B) Cs, 
interp Cs B => 
{!ismem (role A R) B}. 

credential A R0 (role B R1) Cs, 
ismem (role B R1) D,
interp Cs D => 
{!ismem (role A R0) D}. 

credential A R0 (linked_role B R1 R2) Cs, 
ismem (role B R1) D, 
ismem (role D R2) E,
interp Cs E =>
{!ismem (role A R0) E}. 

credential A R (inter Res) Cs, 
ismems Res E,
interp Cs E =>
{!ismem (role A R) E}.


ismems nil B.
ismems (role A R::Res) B <=
  (ismem (role A R) B,
   ismems Res B).


interp nil D.
interp (intc X B T::Ps) D <= 
  leq B X,
  leq X T,
  interp Ps D.
interp (thisc D::Ps) D <= interp Ps D.
interp (osetc E Re::Ps) D <=
  ismem Re E,
  interp Ps D.


(*** Examples ***)

(* L&M example 2 *)
alpha : entity.
evaluator_of : entity -> role_name.
manager_of : entity -> role_name.
ed : entity.
simon : entity.
jonny : entity.

credential alpha (evaluator_of X) (role alpha (manager_of X)) nil.
credential alpha (manager_of simon) (^ ed) nil.

(* L&M example 3 *)
state_u : entity.
founding_alumni: role_name.
diploma : entity -> int -> role_name.
ba : entity.
credential state_u founding_alumni (role state_u (diploma X Y)) 
           (intc Y 1955 1958::nil).
credential state_u (diploma ba 1957) (^ ed) nil. 

(* L&M example 4 *)
pay_raise : role_name.
good_performance : role_name.
credential alpha pay_raise
          (linked_role alpha (evaluator_of X) good_performance) 
          (thisc X::nil).
credential ed good_performance (^ simon) nil.


(*** Example Queries

Ex. 2: 
{ismem (role alpha (evaluator_of simon)) ed}.

Ex. 3:
{ismem (role state_u founding_alumni) ed}.

Ex. 4:
{ismem (role alpha pay_raise) simon}.

***)