Well-formedness and interpretations #

This file defines well-formedness constraints and relations on concrete and symbolic structures. We prove correctness properties of the symbolic compiler with respect to these defintions.

Well-formedness of a concrete structure is defined with respect to a set of concrete entities es : Entities. A Value, Request, or EntityData structure is well-formed with respect to es if it references only entity UIDs that are in the domain of es; i.e., if the structure references a uid, then uid ∈ es. The set es is well-formed if it consists of well-formed EntityData structures, which amounts to saying that there are no dangling references in the entities set es. Finally, an environment Env consisting of a request req and entities es is well-formed for an expression x if es is well-formed, req is well-formed with respect to es, and es supports x. We say that es supports x if all entity UIDs referenced by x are in the domain of es. If env is well-formed for x, then evaluating x against env cannot result in an entityDoesNotExist error.

Well-formed symbolic structures are defined analagously to well-formed concrete structures. In particular, well-formedness of a symbolic structure is defined with respect to a set of symbolic entity declarations εs : SymEntities. A Term, SymRequest, or SymEntityData structure is well-formed with respect to εs if it references only entity types and UIDs that are in the domain of εs, and if all referenced term types represent valid Cedar types. An entity type ety is in the domain of εs if ety ∈ εs, and entity UID uid is in the domain of εs if εs.isValidEntityUID uid. The set εs is well-formed if it consists of well-formed SymEntityData structures. A symbolic environment SymEnv consisting of a symbolic request ρeq and entities εs is well-formed for an expression x if εs is well-formed, ρeq is well-formed with respect to εs, and εs supports x. We say that εs supports x if εs.isValidEntityUID uid for every entity uid referenced by x.

A well-formed symbolic structure represents a set of well-formed symbolic literal structures, which, in turn, represent corresponding well-formed Cedar structures. A literal symbolic structure contains no term variables or uninterpreted functions. Symbolic structures are related to literals through interpretations. An Interpretation binds term variables to literal terms and uninterpreted functions (UUF) to interpreted ones (UDF). When a well-formed symbolic structure is interpreted with respect to a well-formed Interpretation, the result is a well-formed literal symbolic structure. Interpreting a literal against any Interpretation returns the same literal.

A literal term or symbolic request represent a single corresponding Cedar structure (i.e., a Value, Outcome Value, or Request). A well-formed literal symbolic environment εnv : SymEnv represents a set of well-formed concrete environments that lead to equivalent evaluation outcomes. In particular, if εnv is a literal symbolic environment that is well-formed for an expression x, then x produces the same outcome when evaluated against any concrete environment env ∈ εnv that is well-formed for x. We write env ∈ εnv to denote that exists a well-formed interpretation I such that εnv.interpret I is a literal that represents env.