Project-declaredLean 4.31.0
Type of is sound
Cedar.Thm.type_of_is_sound
Plain-language statement
If an expression is well-typed according to the typechecker, and the input environment and capabilities satisfy some invariants, then either (1) evaluation produces a value of the returned type or (2) it returns an error of type entityDoesNotExist, extensionError, or arithBoundsError. Both options are encoded in the EvaluatesTo predicate.
authorizationprogram verificationsemantics
Source project: Cedar Specification
Person-level attribution pending.