theorem Cedar.Thm.partial_evaluate_policy_is_sound {schema : Validation.Schema} {residual : Spec.Residual} {policy : Spec.Policy} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} : TPE.evaluatePolicy schema policy preq pes = Except.ok residual → TPE.isValidAndConsistent schema req es preq pes = Except.ok () → Except.toOption (Spec.evaluate policy.toExpr req es) = Except.toOption (residual.evaluate req es)

Policy evaluation soundness for TPE: Evaluating a result residual is equivalent to evaluating the input policy, given valid and consistent requests and entities. The equivalence is w.r.t authorization results. That is, the evaluation results are strictly equal when they are .ok or both errors (captured by Except.toOption). We do not care if the error types match because they do not impact authorization results. As a matter of fact, they do not match because all errors encountered during TPE are represented by an error residual, whose interpretation always produces an extensionError.