Using opa for abac to check user claims agains defined policies

So I'm trying implement a fairly simple ABAC system for my application and came across open policy agent during my investigations. It seems to be a good fit for my needs but I just can't make it work for my use case where I have an user object that is read from jwt claims that looks something like this: { email: "1@1.com", role: "admin", location: "us" }. I want to check if that user has access rights to a specific path (which is provided as input, same as the user). So for example i want to give access rights to /admin/us if user.role == admin and user.location == us. I've created an example on the rego playground and it is working fine as long as the user has exactly the same claims as written in the policy, but fails if the user has any additional claims:

package play

default allow = false

allow {
    some p
    policy := data.policies[p]
    policy.request_path == input.request_path
    
    # check if all input.user[x] matches to a policy
    policy.user == input.user # works only if objects have the same keys and values
}

I was thinking I could use intersection to get the matching keys and compare that to the policy definition like this:

# check if all input.user[x] matches to a policy
count(intersection(input.user[data.user])) == count(policy.user)

but this isn't working, most likely because the syntax isn't correct.

I also tried to use comprehensions to filter out the keys from user, then comparing that with a full equals against all policies but couldn't get that to work either.

Could someone please push me in the right direction or provide some learning materials for opa/rego (the officials docs are a bit lacking).

Here's the full example on the rego playground: https://play.openpolicyagent.org/p/ijtOjxXRKk

What you've encountered here is Rego's lack of "for all", or "universal quantification". See the docs on the topic here.

As you have noted already there are still quite a few ways of doing this. One would be to use negation in a helper rule (i.e. some key/value in policy.user is not in input.user). Another one would be to use a comprehension and compare the count of all matches to the count of the required attributes:

package play

default allow = false

allow {
    some p
    policy := data.policies[p]
    policy.request_path == input.request_path
    
    required := count(policy.user)
    matches  := count([v |  v := policy.user[k]; v == input.user[k]])
    
    required == matches
}

Future versions of OPA are likely going to make this easier.