(***

   Higher-order RT^2 certificate chain discovery 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}.

***)



(*** Issuer driven discovery ***)

test : o -> o -> o.
test (pi P) Q <= test (P X) Q.
test P P.

expand : list role_expr -> list pconstraint -> o.

cnstrDisc : list pconstraint -> o.

seed : role_expr -> entity -> o -> list pconstraint -> o.
seed (role A R) B Cred Cs o- entry Cred, test Cred (credential A R Re Cs).

credential A Ra (role B Rb) Cs1, 
entry Cred,
test Cred (credential B Rb RE Cs2) -o 
{!Cred, cnstrDisc Cs1}. 

credential A Ra (linked_role B Rb R2) Cs1, 
entry Cred,
test Cred (credential B Rb RE Cs2) -o 
{!Cred, cnstrDisc Cs1 }. 

credential A Ra (linked_role B Rb Rc) Cs1, 
ismem (role B Rb) C, 
entry Cred,
test Cred (credential C Rc RE Cs2) -o 
{!Cred, cnstrDisc Cs1}. 

credential A R (inter Res) Cs -o 
{!expand Res Cs}. 

expand (role A Ra::Res) Cs, 
entry Cred,
test Cred (credential A Ra RE Cs) -o 
{!Cred, !expand Res Cs}.

expand nil Cs -o
{cnstrDisc Cs}.


(* Discover new credentials needed for osetc constraints. *)
cnstrDisc nil.
cnstrDisc (osetc E Re::Cs) -o {auth Re E, cnstrDisc Cs}.
cnstrDisc (intc X Y Z::Cs) -o {cnstrDisc Cs}.
cnstrDisc (thisc E::Cs) -o {cnstrDisc Cs}.


auth R A, 
ismem R A -o 
{one}.

auth R A,
seed R A Cred Cs -o
{!Cred, cnstrDisc Cs, auth R A}. 

authorize : role_expr -> entity -> o. 
authorize Re A o-
  auth Re A -o {ismem Re A, top}.

(* L&M example 5 *)
file_ac : entity -> entity -> role_name.
read : entity.
proj1 : entity.
file_a : entity.
team : entity -> role_name.
documents : entity -> role_name.
#linear entry 
  (pi X  pi Y \ credential alpha (file_ac read X) (role alpha (team Y)) (osetc X (role alpha (documents Y))::nil)).
#linear entry (credential alpha (documents proj1) (^ file_a) nil).
#linear entry (credential alpha (team proj1) (^ jonny) nil).
(***

Ex. 5: put whole auth in monad to allow initialization of distributed entries.
authorize (role alpha (file_ac read file_a)) jonny.

***)