Skip to content

Commit 1e1c80b

Browse files
john-h-kastner-awsjohn-h-kastner-aws
committed
Split soundness into files
1 parent d1a8a1a commit 1e1c80b

File tree

13 files changed

+1610
-1151
lines changed

13 files changed

+1610
-1151
lines changed

‎cedar-lean/Cedar/Thm/TPE/Soundness.lean‎

Lines changed: 13 additions & 1151 deletions
Large diffs are not rendered by default.

‎cedar-lean/Cedar/Thm/TPE/Soundness/And.lean‎

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,190 @@
1+
/-
2+
Copyright Cedar Contributors
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
18+
import Cedar.TPE
19+
import Cedar.Spec
20+
import Cedar.Validation
21+
import Cedar.Thm.TPE.Input
22+
import Cedar.Thm.TPE.ErrorFree
23+
import Cedar.Thm.TPE.WellTyped
24+
import Cedar.Thm.Validation
25+
import Cedar.Thm.WellTyped
26+
import Cedar.Thm.Data.Control
27+
28+
import Cedar.Thm.TPE.Soundness.Basic
29+
30+
namespace Cedar.Thm
31+
32+
open Cedar.Spec
33+
open Cedar.Validation
34+
open Cedar.TPE
35+
open Cedar.Thm
36+
37+
theorem partial_evaluate_is_sound_and
38+
{x₁ x₂ : Residual}
39+
{req : Request}
40+
{es : Entities}
41+
{preq : PartialRequest}
42+
{pes : PartialEntities}
43+
{env : TypeEnv}
44+
(h₂ : InstanceOfWellFormedEnvironment req es env)
45+
(h₃ : RequestAndEntitiesRefine req es preq pes)
46+
(hᵢ₁ : Residual.WellTyped env x₁)
47+
(hᵢ₂ : Residual.WellTyped env x₂)
48+
(hᵢ₃ : x₁.typeOf = CedarType.bool BoolType.anyBool)
49+
(hᵢ₄ : x₂.typeOf = CedarType.bool BoolType.anyBool)
50+
(hᵢ₅ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate x₁ preq pes).evaluate req es))
51+
(hᵢ₆ : Except.toOption (x₂.evaluate req es) = Except.toOption ((TPE.evaluate x₂ preq pes).evaluate req es)) :
52+
Except.toOption ((x₁.and x₂ (CedarType.bool BoolType.anyBool)).evaluate req es) =
53+
Except.toOption ((TPE.evaluate (x₁.and x₂ (CedarType.bool BoolType.anyBool)) preq pes).evaluate req es)
54+
:= by
55+
simp [TPE.evaluate, TPE.and]
56+
split
57+
case _ ty heq =>
58+
simp [heq, Residual.evaluate] at hᵢ₅
59+
have h₅ := to_option_right_ok' hᵢ₅
60+
simp [Residual.evaluate, h₅, Result.as, Coe.coe, Value.asBool]
61+
split
62+
case _ heq₁ =>
63+
have h₆ := residual_well_typed_is_sound h₂ hᵢ₂ heq₁
64+
rw [hᵢ₄] at h₆
65+
rcases instance_of_anyBool_is_bool h₆ with ⟨_, h₆⟩
66+
replace hᵢ₆ := to_option_left_ok hᵢ₆ heq₁
67+
simp only [h₆, Except.map_ok, hᵢ₆]
68+
case _ heq₁ =>
69+
simp only [Except.map_error]
70+
rw [heq₁] at hᵢ₆
71+
rcases to_option_left_err hᵢ₆ with ⟨_, hᵢ₆⟩
72+
simp only [hᵢ₆, Except.toOption]
73+
case _ heq =>
74+
simp [heq, Residual.evaluate] at hᵢ₅
75+
have h₅ := to_option_right_ok' hᵢ₅
76+
simp [Residual.evaluate, h₅, Result.as, Coe.coe, Value.asBool, Residual.evaluate]
77+
case _ heq =>
78+
simp [heq, Residual.evaluate] at hᵢ₅
79+
rcases to_option_right_err hᵢ₅ with ⟨_, hᵢ₅⟩
80+
simp [Residual.evaluate, hᵢ₅, Result.as, Residual.evaluate, Except.toOption]
81+
case _ heq _ _ _ =>
82+
simp [heq, Residual.evaluate] at hᵢ₆
83+
have h₅ := to_option_right_ok' hᵢ₆
84+
simp [Residual.evaluate]
85+
generalize h₆ : x₁.evaluate req es = res₁
86+
cases res₁
87+
case ok =>
88+
have h₇ := residual_well_typed_is_sound h₂ hᵢ₁ h₆
89+
rw [hᵢ₃] at h₇
90+
rcases instance_of_anyBool_is_bool h₇ with ⟨_, h₇⟩
91+
simp [h₇, Result.as, Coe.coe, Value.asBool]
92+
split
93+
case _ heq₁ =>
94+
subst heq₁
95+
rw [h₇] at h₆
96+
rw [←h₆]
97+
exact hᵢ₅
98+
case _ heq₁ =>
99+
simp [h₅]
100+
simp at heq₁
101+
subst heq₁
102+
subst h₇
103+
rw [←h₆]
104+
exact hᵢ₅
105+
case error =>
106+
simp [h₆] at hᵢ₅
107+
rcases to_option_left_err hᵢ₅ with ⟨_, hᵢ₅⟩
108+
simp only [Except.toOption, Result.as, Except.bind_err, hᵢ₅]
109+
case _ =>
110+
simp [Residual.evaluate]
111+
cases h₅ : x₁.evaluate req es
112+
· simp [Result.as, Except.toOption]
113+
cases h₆ : (TPE.evaluate x₁ preq pes).errorFree <;> simp
114+
· split <;> simp
115+
rename_i h₇
116+
simp [Residual.evaluate] at h₇
117+
rw [h₅] at hᵢ₅
118+
simp [Except.toOption] at hᵢ₅
119+
split at hᵢ₅ <;> try contradiction
120+
clear hᵢ₅ ; rename_i hᵢ₅
121+
simp [hᵢ₅, Result.as] at h₇
122+
· split <;> simp
123+
rename_i h₇
124+
simp [Residual.evaluate] at h₇
125+
subst h₇
126+
rw [Residual.error_free_spec] at h₆
127+
have h₇ : Residual.WellTyped env (TPE.evaluate x₁ preq pes) :=
128+
partial_eval_preserves_well_typed h₂ h₃ hᵢ₁
129+
have h₈ := error_free_evaluate_ok h₂ h₇ h₆
130+
simp [Except.isOk, Except.toBool] at h₈
131+
split at h₈ <;> try contradiction
132+
clear h₈ ; rename_i h₈
133+
rw [h₅, h₈] at hᵢ₅
134+
simp [Except.toOption] at hᵢ₅
135+
· simp [Result.as, Except.toOption, Coe.coe, Value.asBool]
136+
simp [h₅, Except.toOption] at hᵢ₅
137+
split at hᵢ₅ <;> try contradiction
138+
simp at hᵢ₅
139+
subst hᵢ₅
140+
rename_i hᵢ₅
141+
rename_i v _
142+
have ⟨_, hv⟩ : ∃ b, v = .prim (.bool b) := by
143+
have h₇ := residual_well_typed_is_sound h₂ hᵢ₁ h₅
144+
rw [hᵢ₃] at h₇
145+
exact instance_of_anyBool_is_bool h₇
146+
subst hv
147+
simp only
148+
rename_i h₁ _ _ _ _ _
149+
simp [h₁, Except.toOption, Residual.evaluate] at hᵢ₆
150+
split at hᵢ₆ <;> simp at hᵢ₆
151+
subst hᵢ₆
152+
rename_i hᵢ₆
153+
simp [hᵢ₆]
154+
rename_i b _
155+
have hb : (if b = false then (Except.ok (Value.prim (Prim.bool b)) : Except Spec.Error _) else Except.ok (Value.prim (Prim.bool false))) = Except.ok (.prim (.bool false)) := by
156+
split
157+
· rename_i hb
158+
simpa using hb
159+
· simp
160+
simp [hb]
161+
rename_i ty _ _ _ _ _
162+
cases he : (TPE.evaluate x₁ preq pes).errorFree<;> simp [Residual.evaluate, hᵢ₅, Result.as, Coe.coe, Value.asBool]
163+
cases b <;> simp
164+
case _ =>
165+
simp [Residual.evaluate]
166+
generalize h₅ : x₁.evaluate req es = res₁
167+
cases res₁
168+
case ok =>
169+
have h₆ := residual_well_typed_is_sound h₂ hᵢ₁ h₅
170+
rw [hᵢ₃] at h₆
171+
rcases instance_of_anyBool_is_bool h₆ with ⟨_, h₆⟩
172+
subst h₆
173+
replace h₅ := to_option_left_ok hᵢ₅ h₅
174+
simp [Result.as, Coe.coe, h₅, Value.asBool]
175+
generalize h₇ : x₂.evaluate req es = res₂
176+
cases res₂
177+
case _ =>
178+
rw [h₇] at hᵢ₆
179+
rcases to_option_left_err hᵢ₆ with ⟨_, hᵢ₆⟩
180+
simp [hᵢ₆]
181+
split <;> simp [Except.toOption]
182+
case _ =>
183+
replace h₇ := to_option_left_ok hᵢ₆ h₇
184+
rw [h₇]
185+
case error =>
186+
rw [h₅] at hᵢ₅
187+
rcases to_option_left_err hᵢ₅ with ⟨_, hᵢ₅⟩
188+
simp [Result.as, hᵢ₅, Except.toOption]
189+
190+
end Cedar.Thm

‎cedar-lean/Cedar/Thm/TPE/Soundness/Basic.lean‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
/-
2+
Copyright Cedar Contributors
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
18+
import Cedar.TPE
19+
import Cedar.Spec
20+
import Cedar.Validation
21+
import Cedar.Thm.TPE.Input
22+
import Cedar.Thm.TPE.ErrorFree
23+
import Cedar.Thm.TPE.WellTyped
24+
import Cedar.Thm.Validation
25+
import Cedar.Thm.WellTyped
26+
import Cedar.Thm.Data.Control
27+
28+
/-!
29+
This file contains basic utility theorems used in the TPE soundness proof.
30+
-/
31+
32+
namespace Cedar.Thm
33+
34+
open Cedar.Spec
35+
open Cedar.Validation
36+
open Cedar.TPE
37+
open Cedar.Thm
38+
39+
theorem as_value_some {r : Residual} {v : Value} :
40+
r.asValue = .some v → (∃ ty, r = .val v ty)
41+
:= by
42+
intro h
43+
simp only [Residual.asValue] at h
44+
split at h <;> simp at h
45+
subst h
46+
simp only [Residual.val.injEq, true_and, exists_eq']
47+
48+
theorem anyM_some_implies_any {α} {xs : List α} {b : Bool} (f : α → Option Bool) (g : α → Bool) :
49+
(∀ x b, f x = some b → g x = b) → List.anyM f xs = some b → xs.any g = b
50+
:= by
51+
intro h₁ h₂
52+
induction xs generalizing b
53+
case nil =>
54+
simp only [List.anyM, Option.pure_def, Option.some.injEq, Bool.false_eq] at h₂
55+
simp only [List.any_nil, h₂]
56+
case cons head tail hᵢ =>
57+
simp only [List.any_cons]
58+
simp only [List.anyM, Option.pure_def, Option.bind_eq_bind] at h₂
59+
generalize h₃ : f head = res
60+
cases res <;> simp [h₃] at h₂
61+
case some =>
62+
split at h₂
63+
case _ =>
64+
simp only [Option.some.injEq, Bool.true_eq] at h₂
65+
subst h₂
66+
specialize h₁ head true h₃
67+
simp only [h₁, Bool.true_or]
68+
case _ =>
69+
specialize hᵢ h₂
70+
simp only [hᵢ, Bool.or_eq_right_iff_imp]
71+
specialize h₁ head false h₃
72+
simp only [h₁, Bool.false_eq_true, false_implies]
73+
74+
theorem to_option_eq_do₁ {α β ε} {res₁ res₂: Except ε α} (f : α → Except ε β) :
75+
Except.toOption res₁ = Except.toOption res₂ →
76+
Except.toOption (do let x ← res₁; f x) = Except.toOption (do let x ← res₂; f x)
77+
:= by
78+
intro h₁
79+
simp [Except.toOption] at *
80+
split at h₁ <;>
81+
split at h₁ <;>
82+
simp at h₁
83+
case _ => subst h₁; simp only [Except.bind_ok]
84+
case _ => simp only [Except.bind_err]
85+
86+
theorem to_option_eq_map {α β ε} {res₁ res₂: Except ε α} (f : α → β) :
87+
Except.toOption res₁ = Except.toOption res₂ →
88+
Except.toOption (f <$> res₁) = Except.toOption (f <$> res₂)
89+
:= by
90+
intro h₁
91+
simp [Except.toOption] at *
92+
split at h₁ <;>
93+
split at h₁ <;>
94+
simp at h₁
95+
case _ => subst h₁; simp only
96+
case _ => simp only [Except.map_error]
97+
98+
theorem to_option_eq_do₂ {α ε} {res₁ res₂ res₃ res₄: Except ε α} (f : α → α → Except ε α) :
99+
Except.toOption res₁ = Except.toOption res₃ →
100+
Except.toOption res₂ = Except.toOption res₄ →
101+
Except.toOption (do let x ← res₁; let y ← res₂; f x y) = Except.toOption (do let x ← res₃; let y ← res₄; f x y)
102+
:= by
103+
intro h₁ h₂
104+
simp [Except.toOption] at *
105+
split at h₁ <;>
106+
split at h₁ <;>
107+
split at h₂ <;>
108+
split at h₂ <;>
109+
simp at h₁ <;>
110+
simp at h₂
111+
case _ => subst h₁; subst h₂; simp only [Except.bind_ok]
112+
case _ => simp only [Except.bind_err, Except.bind_ok]
113+
case _ => simp only [Except.bind_ok, Except.bind_err]
114+
case _ => simp only [Except.bind_err]
115+
116+
theorem to_option_eq_mapM {α β ε} {ls : List α} (f g: α → Except ε β) :
117+
(∀ x,
118+
x ∈ ls →
119+
Except.toOption (f x) = Except.toOption (g x)) →
120+
Except.toOption (List.mapM f ls) =
121+
Except.toOption (List.mapM g ls)
122+
:= by
123+
induction ls
124+
case nil => simp only [List.not_mem_nil, false_implies, implies_true, List.mapM_nil]
125+
case cons head tail hᵢ =>
126+
simp only [List.mem_cons, forall_eq_or_imp, List.mapM_cons, bind_pure_comp, and_imp]
127+
intro h
128+
simp only [Except.toOption] at h
129+
split at h <;> split at h <;> simp at h
130+
case _ heq₁ _ _ heq₂ =>
131+
subst h
132+
simp only [heq₁, Except.bind_ok, heq₂]
133+
intro h
134+
specialize hᵢ h
135+
simp only [Except.toOption] at hᵢ
136+
split at hᵢ <;> split at hᵢ <;> simp at hᵢ
137+
case _ heq₃ _ _ heq₄ =>
138+
subst hᵢ
139+
simp only [heq₃, Except.map_ok, heq₄]
140+
case _ heq₃ _ _ heq₄ =>
141+
simp only [Except.toOption, heq₃, Except.map_error, heq₄]
142+
case _ heq₁ _ _ heq₂ =>
143+
simp only [Except.toOption, heq₁, Except.bind_err, heq₂, implies_true]
144+
145+
end Cedar.Thm

0 commit comments

Comments
 (0)