Skip to content

Cleanup #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ychtao merged 2 commits into from
Jul 9, 2026
Merged

Cleanup #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1f08540
removed weaker soundness lemmas
ychtao Jul 8, 2026
e6164e4
removed some comments
ychtao Jul 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 9 additions & 22 deletions cedar-lean/Cedar/Thm/Translation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,14 +53,11 @@ theorem policy_satisfied_agrees (cp : Cst.Policy) (ap : Spec.Policy)
Cst.satisfied cp req es = satisfied ap req es := by
intro htrans
obtain ⟨ae, hae⟩ := toPolicy?_implies_toAExpr? htrans
have h1 : evaluate ae req es = .ok (↑true : Value) ↔ cp.toExpr.evaluate req es = .ok (↑true : Value) := by
rw [expr_to_expr_sound hae]
have h2 := policy_to_expr_agrees cp ap cp.toExpr ae req es htrans rfl hae (val := (↑true : Value))
have hiff : cp.toExpr.evaluate req es = .ok ↑true ↔ evaluate ap.toExpr req es = .ok ↑true :=
⟨fun hcst => h2.mp (h1.mpr hcst), fun hast => h1.mp (h2.mpr hast)⟩
have heq : cp.toExpr.evaluate req es = evaluate ap.toExpr req es :=
(expr_to_expr_sound hae).symm.trans
(policy_to_expr_sound cp ap cp.toExpr ae req es htrans rfl hae)
unfold Cst.satisfied satisfied
simp only [show (cp.toExpr.evaluate req es = .ok ↑true) = (evaluate ap.toExpr req es = .ok ↑true)
from propext hiff]
rw [heq]

/-- Under a successful translation, `extractScope?` succeeds, so the new scope
guard in `Cst.hasError` is a no-op and it reduces to the plain
Expand All @@ -86,20 +83,11 @@ theorem policy_hasError_agrees (cp : Cst.Policy) (ap : Spec.Policy)
Cst.hasError cp req es = hasError ap req es := by
intro htrans
obtain ⟨ae, hae⟩ := toPolicy?_implies_toAExpr? htrans
have h1 : ∀ v, evaluate ae req es = .ok v ↔ cp.toExpr.evaluate req es = .ok v :=
fun v => by rw [expr_to_expr_sound hae]
have h2 : ∀ v, evaluate ae req es = .ok v ↔ evaluate ap.toExpr req es = .ok v :=
policy_to_expr_agrees cp ap cp.toExpr ae req es htrans rfl hae
have hiff : ∀ v, cp.toExpr.evaluate req es = .ok v ↔ evaluate ap.toExpr req es = .ok v :=
fun v => ⟨fun hcst => (h2 v).mp ((h1 v).mpr hcst), fun hast => (h1 v).mp ((h2 v).mpr hast)⟩
rw [cst_hasError_eq_of_toPolicy htrans]
unfold hasError
cases hcst : cp.toExpr.evaluate req es with
| ok v => rw [(hiff v).mp hcst]
| error e =>
cases hast : evaluate ap.toExpr req es with
| ok v => rw [(hiff v).mpr hast] at hcst; cases hcst
| error e' => rfl
have heq : cp.toExpr.evaluate req es = evaluate ap.toExpr req es :=
(expr_to_expr_sound hae).symm.trans
(policy_to_expr_sound cp ap cp.toExpr ae req es htrans rfl hae)
rw [cst_hasError_eq_of_toPolicy htrans, heq]
rfl

/-- Per-policy agreement of the error check. -/
theorem policy_errored_agrees (cp : Cst.Policy) (ap : Spec.Policy)
Expand Down Expand Up @@ -176,7 +164,6 @@ theorem translation_is_sound (cps : Cst.Policies) (aps : Spec.Policies)
theorem noHasError_translates (cp : Cst.Policy) (req : Request) (es : Entities) :
¬ Cst.hasError cp req es →
∃ ap, cp.toPolicy? = ap := by simp
-- I don't know why simp solves this goal

theorem translation_is_complete (cps : Cst.Policies) (req : Request) (es : Entities) :
∀ cp ∈ cps.ps, cp.id ∉ (Cst.isAuthorized req es cps).erroringPolicies →
Expand Down
Loading