This file defines the main theorem of TPE soundness and its associated lemmas.

theorem Cedar.Thm.conversion_preserves_evaluation_forall2 {req : Spec.Request} {es : Spec.Entities} {ls : List Validation.TypedExpr} : List.Forall₂ (fun (x y : Validation.TypedExpr) => Spec.evaluate x.toExpr req es = y.toResidual.evaluate req es) ls ls

theorem Cedar.Thm.conversion_preserves_evaluation_forall2_map {req : Spec.Request} {es : Spec.Entities} {map : List (Spec.Attr × Validation.TypedExpr)} : List.Forall₂ (fun (x y : Spec.Attr × Validation.TypedExpr) => Prod.mk x.fst <$> Spec.evaluate x.snd.toExpr req es = Prod.mk y.fst <$> y.snd.toResidual.evaluate req es) map map

theorem Cedar.Thm.conversion_preserves_evaluation (te : Validation.TypedExpr) (req : Spec.Request) (es : Spec.Entities) : Spec.evaluate te.toExpr req es = te.toResidual.evaluate req es

Theorem stating that converting a TypedExpr to a Residual preserves evaluation semantics. That is, evaluating the original TypedExpr (converted to Expr) gives the same result as evaluating the converted Residual.

theorem Cedar.Thm.conversion_preserves_typeof (e : Validation.TypedExpr) : e.typeOf = e.toResidual.typeOf

@[irreducible]

theorem Cedar.Thm.conversion_preserves_typedness {env : Validation.TypeEnv} {expr : Validation.TypedExpr} : TypedExpr.WellTyped env expr → Residual.WellTyped env expr.toResidual