Documentation

Cedar.Validation.Levels

This file defines a level checking of a type-annotated AST. Level checking should behave as defined in RFC#76, although the implementation here is different from what was proposed because this implementation operates over a type-annotated AST instead of being built into the primary typechecking algorithm.

source
@[irreducible]
def Cedar.Validation.TypedExpr.checkEntityAccessLevel (tx : TypedExpr) (env : TypeEnv) (n nmax : Nat) (path : List Spec.Attr) :
Bool

Check that an expression is valid as the argument to an entity dereferencing expression at a level. This functions assumes that tx either evaluates to an entity value or to a record value containing a entity value via path.

Note that this function intentionally returns false for entity literals at any level. This is necessary because entity literals are not one of the "roots" used by the slicing algorithm.

This functions takes two additional arguments not required by checkLevel

  • nmax specifies the maximum level allowed for any expression. E.g., for an .ite expression, the maximum level permissible for the guard is independent of any .getAttr expressions it might be nested inside of.
  • path is a sequence of attributes specifying an access path through a record value, eventually reaching an attribute that has an entity value. This allows allows more permissive level checking on record attributes that aren't accessed.
Equations
Instances For
    source
    @[irreducible]
    def Cedar.Validation.TypedExpr.checkLevel (tx : TypedExpr) (env : TypeEnv) (n : Nat) :
    Bool

    Main entry point for level checking an expression. For most expressions, this is a simple recursive traversal of the AST. For entity dereferencing expressions, it calls to checkEntityAccessLevel which ensures that expression is valid specifically in an entity access position

    Equations
    Instances For
      source
      def Cedar.Validation.typecheckAtLevel (policy : Spec.Policy) (env : TypeEnv) (n : Nat) :
      Bool
      Equations
      Instances For