Entity Attribute Maps Lean Model

[john-h-kastner-aws]

Models entity attribute maps as described in RFC 68.

[emina]

Can we rename this to attributeMap?

We use the Mathlib / Lean naming convention where snake_case is reserved for theorem names.

See https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/GUIDE.md#casing

[emina]

Curious: why not define the lub? to be .none when either of the types is an attribute map, instead of special-casing it in every operator that depends on the lub?

If it was defined as .none, then the .none case for these operators should do the right thing and correctly disallow the use of attribute maps in any of these positions (equality, control constructs, etc.).

Would something break if we define lub? x y to be .none if either x or y is an attribute map?

[emina]

(Ah, I see that it has to be special-cased anyway for set and record literals, no getting around that.)

[emina]

This PR takes the approach of modeling AttributeMaps as regular types in the sense that we're adding a variant for it in the CedarType definition.

This makes compositional typechecking possible since they can be assigned as types to subexpressions. But the downside is that it requires special-casing various places in the code to ensure that the values of these types are not usable as first-class values (e.g., typechecking of equal, ite, set literals, and record literals).

An alternative approach is to not add AttributeMaps to the CedarType definition. Instead, we modify EntitySchemaEntry to have a third field, tags: Map Attr AttributeMap, which maps names of tag sets to AttributeMaps.

With this modeling, we only change how getAttr and hasAttr operators are typechecked, because they are the only operators that need to deal with tags. Everything else is unaffected.

The downside is that the typechecking of getAttr and hasAttr becomes more complicated. (Maybe proofs too?) Specifically, it will not be fully compositional because we have to special-case the handling of tags along these lines:

def typeOf (x : Expr) (c : Capabilities) (env : Environment) : ResultType :=
  match x with
  ... 
  | .hasAttr (getAttr x₁ a1) a2 => do
    let (ty₁, _) ← typeOf x₁ c env
    typeOfHasAttr' ty₁ x₁ a1 a2 c env -- handles the case when a1 is the name of a tag set
  | .hasAttr x₁ a => do
    let (ty₁, _) ← typeOf x₁ c env
    typeOfHasAttr ty₁ x₁ a c env
   | .getAttr (.getAttr x₁ a1) a2 => do
    let (ty₁, _) ← typeOf x₁ c env
    typeOfGetAttr' ty₁ x₁ a1 a2 c env -- handles the case when a1 is the name of a tag set
  | .getAttr x₁ a => do
    let (ty₁, _) ← typeOf x₁ c env
    typeOfGetAttr ty₁ x₁ a c env

This handling should be sufficient since the only valid syntactic positions for tags should be (getAttr (getAttr x tags) attr) and (hasAttr (getAttr x tags) attr). And, of course, typeOfGetAttr' and typeOfHasAttr' have to account for the case when a1 is the name of a tag set, and when a1 is the name of a regular attribute.

I'm curious to know if we considered the alternative approach and if so, why we decided against it?

[john-h-kastner-aws]

Curious: why not define the lub? to be .none when either of the types is an attribute map, instead of special-casing it in every operator that depends on the lub?

(Ah, I see that it has to be special-cased anyway for set and record literals, no getting around that.)

Correct. I did most the change in that style but on getting to set literals, I decided it was nicer to special case it everywhere. It was also just a bit annoying to update the some of the proof to not depend on subtype reflexivity. The proof update in the current revision was entirely straightforward.

An alternative approach is to not add AttributeMaps to the CedarType definition. Instead, we modify EntitySchemaEntry to have a third field, tags: Map Attr AttributeMap, which maps names of tag sets to AttributeMaps.

I considered something like this, but then if principal is User then principal.userTags else principal.otherTags wouldn't be accepted, which is inconsistent with how short-circuiting works elsewhere (e.g, if principal is User then principal.longAttr else principal.stringAttr is accepted by the typechecker). Should this not work like this for attribute maps?

[emina]

Should this not work like this for attribute maps?

Good point. This example does seem like it should work.

Unfortunately, our current approach also allows more confusing examples you shared offline, like this one:

(if true then principal.authTags else principal.authTags).write

This one is particularly troublesome because it's saying that we allow tags to be treated as first-class values in some contexts (like this one) but not in others. I worry that this will be really confusing to users.

Another concern with adding AttributeMaps into CedarType is that, without more assumptions or more checks in the typechecker, we won't be able to prove that if the typechecker accepts a policy, then the symbolic compiler will succeed in reducing to SMT.

To see why, note that the current modeling makes it possible to programmatically construct types A with attributes {foo : Set<AttributeMap<Integer>>} and B with attributes { bar: AttributeMap<Integer> }.

Therefore, the typechecker will accept this expression, which is not translatable to SMT: principal.foo.contains(resource.bar), where principal is of type A and resource is of type B. Similarly, the typechecker will also accept the literals [ principal.foo ] and {baz : principal.foo}.

Now, the above types aren't expressible syntactically in the schema, but there is nothing in the model that enforces this restriction. And it would need to be enforced somewhere in order to prove that successful typechecking ensures successful symbolic compilation.

[john-h-kastner-aws]

Now, the above types aren't expressible syntactically in the schema, but there is nothing in the model that enforces this restriction.

I see. This is annoying.

[emina]

I see. This is annoying.

Yes :(

I don't see any particularly elegant way to handle it. I can think of kludgy solutions.

[john-h-kastner-aws]

Closing due to cedar-policy/rfcs#82