CST validation soundness

[ychtao]

Extended translation soundness proofs to incorporate errors.
Proved CST policies validation sound -- validated policies don't evaluate to type errors.

[Copilot]

Pull request overview

This PR strengthens CST→AST translation soundness results from “ok-value agreement” to full Except equality (including errors), and uses those stronger bridges to prove a new CST validation soundness theorem: validated CST policies do not evaluate to typeError.

Changes:

• Added full-equality (error-preserving) translation soundness theorem expr_to_expr_sound and supporting mutual soundness lemmas for CST expression translators.
• Added full-equality policy-level bridge policy_to_expr_sound plus supporting evaluation congruence lemmas.
• Added equality versions of several helper lemmas in Aux.lean, and introduced new validation soundness theorems in Translation.lean.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

File	Description
cedar-lean/Cedar/Thm/Translation/PolicyToExpr.lean	Adds full-Except equality lemmas culminating in policy_to_expr_sound.
cedar-lean/Cedar/Thm/Translation/ExprTranslation.lean	Strengthens expression translation soundness to full evaluation equality (including CST-specific errors).
cedar-lean/Cedar/Thm/Translation/Aux.lean	Introduces equality versions of helper lemmas used to keep the new soundness proofs modular.
cedar-lean/Cedar/Thm/Translation.lean	Switches to equality-based soundness lemmas and adds CST validation soundness theorems.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.