Skip to content

Commit d1a8a1a

Browse files
john-h-kastner-awsjohn-h-kastner-aws
committed
Split TPE WellTyped Proof into files
1 parent 1596c6c commit d1a8a1a

File tree

15 files changed

+1914
-1598
lines changed

15 files changed

+1914
-1598
lines changed

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@ import Cedar.Thm.TPE.PreservesTypeOf
2525
import Cedar.Thm.TPE.Policy
2626
import Cedar.Thm.TPE.Authorizer
2727
import Cedar.Thm.TPE.WellTyped
28-
import Cedar.Thm.TPE.WellTypedCases
2928
import Cedar.Thm.TPE.ErrorFree
3029
import Cedar.Thm.Validation
3130
import Cedar.Thm.Authorization

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

Lines changed: 18 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,23 @@
1717
import Cedar.TPE
1818
import Cedar.Thm.TPE.Input
1919
import Cedar.Thm.TPE.PreservesTypeOf
20-
import Cedar.Thm.TPE.WellTypedCases
2120
import Cedar.Thm.WellTyped.Residual.Definition
2221
import Cedar.Thm.Data.List
2322
import Cedar.Thm.Data.Map
2423

24+
import Cedar.Thm.TPE.WellTyped.Basic
25+
import Cedar.Thm.TPE.WellTyped.And
26+
import Cedar.Thm.TPE.WellTyped.Binary
27+
import Cedar.Thm.TPE.WellTyped.Call
28+
import Cedar.Thm.TPE.WellTyped.GetAttr
29+
import Cedar.Thm.TPE.WellTyped.HasAttr
30+
import Cedar.Thm.TPE.WellTyped.IfThenElse
31+
import Cedar.Thm.TPE.WellTyped.Or
32+
import Cedar.Thm.TPE.WellTyped.Record
33+
import Cedar.Thm.TPE.WellTyped.Set
34+
import Cedar.Thm.TPE.WellTyped.Unary
35+
import Cedar.Thm.TPE.WellTyped.Var
36+
2537
/-!
2638
This file contains theorems about partial evaluation preserving well-typedness of residuals.
2739
-/
@@ -63,7 +75,11 @@ theorem partial_eval_preserves_well_typed
6375

6476
cases hᵣ : res <;> rw [hᵣ] at h_wt
6577
case val v ty =>
66-
exact partial_eval_well_typed_val h_wf h_ref h_wt
78+
simp only [TPE.evaluate]
79+
exact h_wt
80+
case error ty =>
81+
simp only [TPE.evaluate]
82+
exact h_wt
6783
case var v ty =>
6884
exact partial_eval_well_typed_var h_wf h_ref h_wt
6985
case and a b ty =>
@@ -101,10 +117,7 @@ theorem partial_eval_preserves_well_typed
101117
| binaryApp h_expr1 h_expr2 h_op =>
102118
have ih1 : Residual.WellTyped env (TPE.evaluate expr1 preq pes) := partial_eval_preserves_well_typed h_wf h_ref h_expr1
103119
have ih2 : Residual.WellTyped env (TPE.evaluate expr2 preq pes) := partial_eval_preserves_well_typed h_wf h_ref h_expr2
104-
105120
apply partial_eval_well_typed_app₂ ih1 ih2 h_wf h_ref h_wt₂
106-
case error ty =>
107-
exact partial_eval_well_typed_error h_wf h_ref h_wt
108121
case set ls ty =>
109122
let h_wt₂ := h_wt
110123
cases h_wt₂

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

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
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+
import Cedar.TPE
18+
import Cedar.Thm.TPE.Input
19+
import Cedar.Thm.TPE.PreservesTypeOf
20+
import Cedar.Thm.WellTyped.Residual.Definition
21+
import Cedar.Thm.Data.List
22+
import Cedar.Thm.Data.Map
23+
24+
import Cedar.Thm.TPE.WellTyped.Basic
25+
26+
namespace Cedar.Thm
27+
28+
open Cedar.Thm
29+
open Cedar.Data
30+
open Cedar.Spec
31+
open Cedar.Validation
32+
open Cedar.TPE
33+
34+
theorem partial_eval_well_typed_and {env : TypeEnv} {a b : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} :
35+
Residual.WellTyped env (TPE.evaluate a preq pes) →
36+
Residual.WellTyped env (TPE.evaluate b preq pes) →
37+
PEWellTyped env (Residual.and a b ty) (TPE.evaluate (Residual.and a b ty) preq pes) req preq es pes
38+
:= by
39+
intros h_a_wt h_b_wt h_wf h_ref h_wt
40+
simp only [TPE.evaluate]
41+
cases h_wt with
42+
| and h_a h_b h_ty_a h_ty_b =>
43+
unfold TPE.and
44+
split
45+
. exact h_b_wt
46+
. exact well_typed_bool
47+
. apply Residual.WellTyped.error
48+
. exact h_a_wt
49+
· split
50+
· exact well_typed_bool
51+
· rename_i bty h_eval_b _ _ _ _
52+
replace h_ty_b : bty = CedarType.bool BoolType.anyBool := by
53+
replace h_ty_b' := partial_eval_preserves_typeof _ h_b preq pes
54+
simp only [h_eval_b, h_ty_b] at h_ty_b'
55+
simpa [Residual.typeOf] using h_ty_b'
56+
apply Residual.WellTyped.and
57+
· exact h_a_wt
58+
· rw [h_ty_b]
59+
exact well_typed_bool
60+
· rw [partial_eval_preserves_typeof _ h_a]
61+
exact h_ty_a
62+
· simp [h_ty_b, Residual.typeOf]
63+
. apply Residual.WellTyped.and
64+
· exact h_a_wt
65+
· exact h_b_wt
66+
· rw [partial_eval_preserves_typeof _ h_a]
67+
exact h_ty_a
68+
· rw [partial_eval_preserves_typeof _ h_b]
69+
exact h_ty_b

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

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
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+
import Cedar.TPE
18+
import Cedar.Thm.TPE.Input
19+
import Cedar.Thm.TPE.PreservesTypeOf
20+
import Cedar.Thm.WellTyped.Residual.Definition
21+
import Cedar.Thm.Data.List
22+
import Cedar.Thm.Data.Map
23+
24+
/-!
25+
This file contains theorems about partial evaluation preserving well-typedness of residuals.
26+
-/
27+
28+
namespace Cedar.Thm
29+
30+
open Cedar.Thm
31+
open Cedar.Data
32+
open Cedar.Spec
33+
open Cedar.Validation
34+
open Cedar.TPE
35+
36+
abbrev PEWellTyped (env : TypeEnv)
37+
(r₁ r₂ : Residual)
38+
(req : Request)
39+
(preq : PartialRequest)
40+
(es : Entities)
41+
(pes : PartialEntities) : Prop :=
42+
InstanceOfWellFormedEnvironment req es env →
43+
RequestAndEntitiesRefine req es preq pes →
44+
Residual.WellTyped env r₁ →
45+
Residual.WellTyped env r₂
46+
47+
theorem well_typed_bool { env : TypeEnv} {b : Bool}:
48+
Residual.WellTyped env (.val (.prim (.bool b)) (CedarType.bool BoolType.anyBool))
49+
:= by
50+
apply Residual.WellTyped.val
51+
apply InstanceOfType.instance_of_bool
52+
simp [InstanceOfBoolType]

0 commit comments

Comments
 (0)