## Predicates

pred org_is_enabled(org_id: Id<Org>);
pred user_in_org(user_id: Id<User>, org_id: Id<Org>);
pred user_in_role(user_id: Id<User>, role_id: Id<RoleId>);
pred is_org_owner(user_id: Id<User>, org_id: Id<Org>);
pred role_in_org(role_id: Id<Role>, org_id: Id<Org>);
pred key_in_role(key_id: Id<Key>, role_id: Id<Role>);
pred role_is_valid(role_id: Id<Role>);
pred role_exists(role_id: Id<Role>);
pred valid_role_in_org(role_id: Id<RoleId>, org_id: Id<Org>) {
    role_exists(role_id) && role_is_valid(role_id) && role_in_org(role_id, org_id)
}

## Effects

### Orgs & Users

effect org_set_enabled(org: &Entity<Org>)
requires is_org_owner($sess_user.id, org.id) && org.id == $sess_org.id
routes PATCH /v0/org/<org_id>

effect org_set_policy(org: &Entity<Org>)
requires is_org_owner($sess_user.id, org.id) && org.id == $sess_org.id
routes PATCH /v0/org/<org_id>
    
effect org_set_name(org: &Entity<Org>)
requires is_org_owner($sess_user.id, org.id) && org.id == $sess_org.id
routes PATCH /v0/org/<org_id>

effect cognito_create_user -> Id<User>
requires org_is_enabled($sess_org.id) && is_org_owner($sess_user.id, $sess_org.id)
routes PATCH /v0/org/<org_id>/invite

effect dynamo_create_user
requires org_is_enabled($sess_org.id) && is_org_owner($sess_user.id, $sess_org.id)
routes PATCH /v0/org/<org_id>/invite

effect create_user_in_org(user_id: Id<User>, org_id: Id<Org>)
requires org_is_enabled(org_id) && is_org_owner($sess_user.id, org_id) && org_id == $sess_org.id
routes PATCH /v0/org/<org_id>/invite

### Keys

effect import_key(user_id: Id<User>, org_id: Id<Org>)
requires org_is_enabled(org_id) && user_in_org(user_id, org_id) 
         && org_id == $sess_org.id && user_id == $sess_org.id
routes PUT /v0/org/<org_id>/keys

effect create_key(user_id: Id<User>, org_id: Id<Org>)
requires org_is_enabled(org_id) && user_in_org(user_id, org_id) 
         && org_id == $sess_org.id && user_id == $sess_org.id
routes POST /v0/org/<org_id>/keys, POST /v1/org/<org_id>/eth2/stake

effect key_update_enabled(key: Relation<Key>)
requires org_is_enabled(key.from) && user_in_org($sess_user.id, key.from)
         && (is_org_owner($sess_user.id, key.from) || key.data.owner == $sess_user.id) 
         && key.from == $sess_org.id
routes PATCH /v0/org/<org_id>/keys/<key_id>

effect key_update_owner(key: Relation<Key>, new_owner_id: Id<User>)
requires org_is_enabled(key.from) && user_in_org($sess_user.id, key.from)
         && (is_org_owner($sess_user.id, key.from) || key.data.owner == $sess_user.id) 
         && key.from == $sess_org.id
         && user_in_org(new_owner_id, key.from)
routes PATCH /v0/org/<org_id>/keys/<key_id>

### Roles

effect create_role
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
routes POST /v0/org/<org_id>/roles

effect add_role_to_org(org_id: Id<Org>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && org_id == $sess_org.id
routes POST /v0/org/<org_id>/roles
         
effect add_user_to_role(role_id: Id<Role>, user_id: Id<User>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && user_in_org(user_id, $sess_org.id)
         && (user_id == $sess_user.id || is_org_owner($sess_user.id, $sess_org.id) || user_in_role($sess_user.id, role_id))
         && role_is_valid(role_id) && role_in_org(role_id, $sess_user.id)
routes POST /v0/org/<org_id>/roles, PUT /v0/org/<org_id>/roles/<role_id>/add_user/<user_id>
      
effect role_update_enabled(role_id: Id<Role>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && role_exists(role_id) && role_in_org(role_id, $sess_org.id) 
         && (user_in_role($sess_user.id, $role_id) || is_org_owner($sess_user.id, $sess_org.id)
routes PATCH /v0/org/<org_id>/roles/<role_id>

effect delete_role(role_id: Id<Role>, org_id: Id<Org>)
requires org_is_enabled(org_id) && is_org_owner($sess_user.id, org_id)
         && valid_role_in_org(role_id, org_id)
routes DELETE /v0/org/<org_id>/roles/<role_id>

### Mfa

effect mfa_set_status(mfa: Relation<MfaRequest>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, org_id)
         && valid_role_in_org(role_id, org_id)
         && (user_in_role($sess_user.id, mfa.from) || is_org_owner($sess_user.id, $sess_org.id)
         && allowed_approver($sess_user.id, mfa.data.to)
routes PATCH /v0/org/<org_id>/roles/<role_id>/mfa/<mfa_id>

effect mfa_set_approved(mfa: Relation<MfaRequest>, user_id: Id<User>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, org_id)
         && valid_role_in_org(role_id, org_id)
         && (user_in_role($sess_user.id, mfa.from) || is_org_owner($sess_user.id, $sess_org.id)
         && allowed_approver($sess_user.id, mfa.data.to)
         && user_id = $sess_user.id 
routes PATCH /v0/org/<org_id>/roles/<role_id>/mfa/<mfa_id>

### Keys in Role

effect add_keys_to_role_checked(org_id: Id<Org>, role_id: Id<Role>, policy: KeyInRole, keys: impl Iterator<Id<Key>>)
requires org_is_enabled(org_id) && user_in_org($sess_user.id, org_id)
         && valid_rules(policy.rules)
         && valid_role_in_org(role_id, org_id)
         && (is_org_owner($sess_user.id, org_id) || (user_in_role($sess_user.id, role_id) && for key_id in keys { is_key_owner($sess_user.id, key_id) } ))
         && org_id == $sess_org.id
    
effect remove_key_from_role(role_id: Id<Role>, key_id: Id<Key>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && valid_role_in_org(role_id, org_id)
         && key_in_role(key_id, role_id)
         && (is_org_owner($sess_user.id, $sess_org.id) || user_in_role($sess_user.id, role_id))
         && (is_org_owner($sess_user.id, $sess_org.id) || is_key_owner($sess_user.id, key_id))
routes DELETE /v0/org/<org_id>/roles/<role_id>/keys/<key_id>

### Tokens

effect create_session_token(role_id: Id<Role>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && valid_role_in_org(role_id, org_id)
         && (user_in_role($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
route POST /v0/org/<org_id>/roles/<role_id>/tokens
    
effect revoke_all(role_id: Id<Role>)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && valid_role_in_org(role_id, org_id)
         && (user_in_role($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
routes DELETE /v0/org/<org_id>/roles/<role_id>/tokens
   
effect revoke(session: Session)
requires org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
         && valid_role_in_org(role_id, org_id)
         && (user_in_role($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
route DELETE /v0/org/<org_id>/roles/<role_id>/tokens/<session_id>

## Routes

### About me

[about_me] GET /v0/about_me
    READS: $user.orgs

### Orgs

[get_org] GET /v0/org/<org_id>
    ASSUMES: in_org($sess_user.id, $sess_org.id)
    
[update_org] PATCH /v0/org/<org_id>
    ASSUMES: is_org_owner($sess_user.id, $sess_org.id)         
    EFFECT: org_set_enabled($sess_org); org_set_name($sess_org); org_set_rules($sess_org)
    
[invite] POST /v0/org/<org_id>/ivite
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    EFFECT: let user_id = cognito_create_user in dynamo_create_user; create_user_in_org(user_id, $sess_org.id)

### Keys

    
[import_key] PUT /v0/org/<org_id>/keys
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    EFFECT: import_key($sess_user.id, $sess_org.id)
    
[create_key] POST /v0/org/<org_id>/keys
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    EFFECT: create_key($user, $org)
    
[list_keys] GET /v0/org/<org_id>/keys?<key_type>
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    
[get_key] GET /v0/org/<org_id>/keys/<key_id>
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    ASSERT: user_in_org(key_id, $sess_org.id)

[update_key] PATCH /v0/org/<org_id>/keys/<key_id>
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    ASSERT: is_org_owner($sess_user.id, $sess_org.id) || is_key_owner($sess_user.id, key_id) && if let Some(owner) = body.owner {  user_in_org(owner, $sess_org.id) }
    EFFECT: key_update_enabled(key_id); if let Some(owner) = body.owner { key_update_owner(key_id, owner) }

### Roles

[create_role] POST /v0/org/<org_id>/roles
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($user.id, $sess_org.id)
    EFFECT: let role_id = create_role in add_role_to_org($sess_org.id); add_user_to_role(role_id, $sess_org.id)
    
[list_roles] GET /v0/org/<org_id>/roles
    ASSUMES: org_is_enabled($sess_org.id) && user_in_org($sess_user.id, $sess_org.id)
    ASSERT: for role_id in $sess_org { is_org_owner($sess_user.id, $sess_org.id) || user_is_in_role($sess_user.id, role_id) }
    
[get_role] GET /v0/org/<org_id>/roles/<role_id>
    ASSUMES: org_is_enabled($sess_org) && user_in_org($sess_user.id, $sess_org.id)
    ASSERT: role_exists(role_id) && role_in_org(role_id, $sess_org.id) && (user_in_role($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
    
[update_role] PUT /v0/org/<org_id>/roles/<role_id>
    ASSUMES: org_is_enabled($sess_org) && in_org($sess_user.id, $sess_org.id)
    ASSERT: role_exists(role_id) && role_in_org(role_id, $sess_org.id) && (user_in_role($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
    EFFECTS: role_update_enabled(role_id)
    
[delete_role] DELETE /v0/org/<org_id>/roles/<role_id>
    ASSUMES: org_is_enabled($sess_org) && is_org_owner($sess_user.id, $sess_org.id)
    ASSERT: let role = role_exists(role_id) in role_is_valid(role) && role_in_org(role_id, $sess_org.id)
    EFFECTS: delete_role(role_id, $sess_org.id)

### MFA

[approve] PATCH /v0/org/<org_id>/roles/<role_id>/mfa/<mfa_id>
    ASSUMES: org_is_enabled($sess_org) && user_in_org($sess_user.id, $sess_org.id)
    ASSERT: (let role = role_exists(role_id) in role_is_valid(role) && role_in_org(role_id, $sess_org.id)) && (user_in_org($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
    ASSERT: (let mfa = mfa_exists(mfa_id) in $mfa.allowed_approvers.contains($user.id))
    EFFECT: mfa_update_status(mfa), mfa_update_approve(mfa)
    
[get_mfa] PATCH /v0/org/<org_id>/roles/<role_id>/mfa/<mfa_id>
    ASSUMES: org_is_enabled($sess_org) && user_in_org($sess_user.id, $sess_org.id)
    ASSERT: (let role = role_exists(role_id) in role_is_valid(role) && role_in_org(role_id, $sess_org.id)) && (user_in_org($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
    ASSERT: (let mfa = mfa_exists(mfa_id) in mfa.allowed_approvers.contains($sess_user.id))

### Keys in Roles

[add_keys_to_role] PUT /v0/org/<org_id>/roles/<role_id>/add_keys
    ASSUMES: org_is_enabled($sess_org) && user_in_org($user.id, $sess_org.id)
    ASSERT: validate_policies($sess_org)
    ASSERT: (let role = role_exists(role_id) in role_is_valid(role) && role_in_org(role_id, $sess_org.id)) 
            && (is_org_owner($sess_user.id, $sess_org.id) || (user_in_role($sess_org.id, $sess_user.id) && for key_id in body.keys() { is_key_owner($sess_user.id, key_id) })
    EFFECT: add_keys_to_role_checked($sess_org.id, role_id, body.keys())
    
[remove_key_from_role] DELTE /v0/org/<org_id>/roles/<role_id>/keys/<key_id>
   ASSUMES: org_is_enabled($sess_org) && user_in_org($sess_user.id, $sess_org.id)
   ASSERT: (let $role = role_exists($role) in role_is_valid($role) && role_in_org($role.id, $org.id))
           && key_in_role($key_id, $role_id) 
           && (user_in_role($sess_user.id, $role_id) || is_org_owner($user.id, $org.id)) 
           && (is_key_owner($sess_user.id, $key_id) || is_org_owner($user.id, $org.id))
   EFFECT: delete_key_from_role($role_id, $key_id)

[add_user_to_role] PUT /v0/org/<org_id>/roles/<role_id>/add_user/<user_id>
   ASSUMES: org_is_enabled($sess_org) AND user_in_org($sess_user.id, $sess_org.id)
   ASSERT: user_in_org($user_id, $sess_org.id) 
           && (let role = role_exists(role_id) in role_is_valid(role)) && (role_in_org(role_id, sess_org.id))
           && (user_in_role($sess_user.id, role_id) || is_org_owner($sess_user.id, $sess_org.id))
   EFFECT: create_user_in_role(role_id, $sess_user.id)

### Tokens

[list] GET /v0/org/<org_id>/roles/<role_id>/tokens
   ASSUMES: org_is_enabled($sess_org) AND user_in_org($)
   ASSERT: (let $role = role_exists($role_id) in role_is_valid($role)) && (role_in_org($role_id, sess_org.id))
           && (user_in_role($sess_user.id, $role_id) || is_org_owner($sess_user.id, $sess_org.id))

[create] POST /v0/org/<org_id>/roles/<role_id>/tokens
   ASSUMES: org_is_enabled($sess_org) AND user_in_org($sess_user.id, $sess_org.id)
   ASSERT: (let $role = role_exists($role_id) in role_is_valid($role)) && (role_in_org($role_id, sess_org.id))
           && (user_in_role($sess_user.id, $role_id) || is_org_owner($sess_user.id, $sess_org.id))
   EFFECT: create_session($role_id)
    
[revoke_all] DELETE /v0/org/<org_id>/roles/<role_id>/tokens
   ASSUMES: org_is_enabled($sess_org) && user_in_org($sess_user.id, $sess_org.id)
   ASSERT: (let $role = role_exists($role_id) in role_is_valid($role)) && (role_in_org($role_id, sess_org.id))
           && (user_in_role($sess_user.id, $role_id) || is_org_owner($sess_user.id, $sess_org.id))
   EFFECT: revoke_all($role_id)
   
[revoke] DELETE /v0/org/<org_id>/roles/<role_id>/tokens/<session_id>
   ASSUMES: org_is_enabled($sess_org) AND user_in_org($)
   ASSERT: (let $role = role_exists($role_id) in role_is_valid($role)) && (role_in_org($role_id, sess_org.id))
           && (user_in_role($sess_user.id, $role_id) || is_org_owner($sess_user.id, $sess_org.id))
   EFFECT: let $session = session_exists($session) in revoke_session($session)