(*
   Specification of issuer-driven credential discovery.
*)

(* Use forward-chaining ismem specification *)
#include "ismem_forwards.lo".


entry : entity -> role_name -> role_expr -> o.


expand : list role_expression -> o.
expand (role A Ra::Res),
entry A Ra RE -o 
{!credential A Ra RE, !expand Res}.

(*** Alternative Parallel Expansion ***
expand (role A Ra::Res) -o
{!(entry A Ra RE -o {!credential A Ra RE}), 
 !expand Res
}.
***)


credential A Ra (role B Rb), 
entry B Rb RE -o 
{!credential B Rb RE}. 

credential A Ra (linked_role B Rb R2), 
entry B Rb RE -o 
{!credential B Rb RE}. 

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

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


seed : role_expr -> entity -> 
           entity -> role_name -> role_expr -> o. 
seed (role A R) B A R Re o- entry A R Re.


auth : role_expr -> entity -> o. 
auth R A o- ismem R A, top. 
auth R A o- 
  seed R A B Rb RE, 
  (credential B Rb RE => {auth R A}).