-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Proof that PE on concrete inputs is equivalent to concrete eval (#291)
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
- Loading branch information
1 parent
7369309
commit b0310bb
Showing
19 changed files
with
1,216 additions
and
32 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,17 @@ | ||
| /- | ||
| Copyright Cedar Contributors | ||
| Licensed under the Apache License, Version 2.0 (the "License"); | ||
| you may not use this file except in compliance with the License. | ||
| You may obtain a copy of the License at | ||
| https://www.apache.org/licenses/LICENSE-2.0 | ||
| Unless required by applicable law or agreed to in writing, software | ||
| distributed under the License is distributed on an "AS IS" BASIS, | ||
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| See the License for the specific language governing permissions and | ||
| limitations under the License. | ||
| -/ | ||
|
|
||
| import Cedar.Thm.Partial.Evaluation |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,131 @@ | ||
| /- | ||
| Copyright Cedar Contributors | ||
| Licensed under the Apache License, Version 2.0 (the "License"); | ||
| you may not use this file except in compliance with the License. | ||
| You may obtain a copy of the License at | ||
| https://www.apache.org/licenses/LICENSE-2.0 | ||
| Unless required by applicable law or agreed to in writing, software | ||
| distributed under the License is distributed on an "AS IS" BASIS, | ||
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| See the License for the specific language governing permissions and | ||
| limitations under the License. | ||
| -/ | ||
|
|
||
| import Cedar.Partial.Evaluator | ||
| import Cedar.Spec.Evaluator | ||
| import Cedar.Thm.Partial.Evaluation.And | ||
| import Cedar.Thm.Partial.Evaluation.Basic | ||
| import Cedar.Thm.Partial.Evaluation.Binary | ||
| import Cedar.Thm.Partial.Evaluation.Call | ||
| import Cedar.Thm.Partial.Evaluation.GetAttr | ||
| import Cedar.Thm.Partial.Evaluation.HasAttr | ||
| import Cedar.Thm.Partial.Evaluation.Ite | ||
| import Cedar.Thm.Partial.Evaluation.Or | ||
| import Cedar.Thm.Partial.Evaluation.Record | ||
| import Cedar.Thm.Partial.Evaluation.Set | ||
| import Cedar.Thm.Partial.Evaluation.Unary | ||
| import Cedar.Thm.Partial.Evaluation.Var | ||
| import Cedar.Thm.Data.Control | ||
|
|
||
| /-! This file contains theorems about Cedar's partial evaluator. -/ | ||
|
|
||
| namespace Cedar.Thm.Partial.Evaluation | ||
|
|
||
| open Cedar.Data | ||
| open Cedar.Partial (Unknown) | ||
| open Cedar.Spec (Error Result) | ||
|
|
||
| /-- | ||
| Partial evaluation with concrete inputs gives the same output as | ||
| concrete evaluation with those inputs | ||
| -/ | ||
| theorem on_concrete_eqv_concrete_eval (expr : Spec.Expr) (request : Spec.Request) (entities : Spec.Entities) | ||
| (wf : request.WellFormed) : | ||
| PartialEvalEquivConcreteEval expr request entities | ||
| := by | ||
| unfold PartialEvalEquivConcreteEval | ||
| cases expr | ||
| case lit p => simp [Partial.evaluate, Spec.evaluate, Spec.Expr.asPartialExpr, Except.map] | ||
| case var v => | ||
| have h := Var.on_concrete_eqv_concrete_eval v request entities wf | ||
| unfold PartialEvalEquivConcreteEval at h ; exact h | ||
| case and x₁ x₂ => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| have ih₂ := on_concrete_eqv_concrete_eval x₂ request entities wf | ||
| exact And.on_concrete_eqv_concrete_eval ih₁ ih₂ | ||
| case or x₁ x₂ => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| have ih₂ := on_concrete_eqv_concrete_eval x₂ request entities wf | ||
| exact Or.on_concrete_eqv_concrete_eval ih₁ ih₂ | ||
| case ite x₁ x₂ x₃ => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| have ih₂ := on_concrete_eqv_concrete_eval x₂ request entities wf | ||
| have ih₃ := on_concrete_eqv_concrete_eval x₃ request entities wf | ||
| exact Ite.on_concrete_eqv_concrete_eval ih₁ ih₂ ih₃ | ||
| case unaryApp op x₁ => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| exact Unary.on_concrete_eqv_concrete_eval ih₁ | ||
| case binaryApp op x₁ x₂ => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| have ih₂ := on_concrete_eqv_concrete_eval x₂ request entities wf | ||
| exact Binary.on_concrete_eqv_concrete_eval ih₁ ih₂ | ||
| case getAttr x₁ attr => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| exact GetAttr.on_concrete_eqv_concrete_eval ih₁ | ||
| case hasAttr x₁ attr => | ||
| have ih₁ := on_concrete_eqv_concrete_eval x₁ request entities wf | ||
| exact HasAttr.on_concrete_eqv_concrete_eval ih₁ | ||
| case set xs => | ||
| have ih : ∀ x ∈ xs, PartialEvalEquivConcreteEval x request entities := by | ||
| intro x h₁ | ||
| have := List.sizeOf_lt_of_mem h₁ | ||
| apply on_concrete_eqv_concrete_eval x request entities wf | ||
| exact Set.on_concrete_eqv_concrete_eval ih | ||
| case record attrs => | ||
| have ih : ∀ kv ∈ attrs, PartialEvalEquivConcreteEval kv.snd request entities := by | ||
| intro kv h₁ | ||
| have := List.sizeOf_lt_of_mem h₁ | ||
| apply on_concrete_eqv_concrete_eval kv.snd request entities wf | ||
| exact Record.on_concrete_eqv_concrete_eval ih | ||
| case call xfn args => | ||
| have ih : ∀ arg ∈ args, PartialEvalEquivConcreteEval arg request entities := by | ||
| intro arg h₁ | ||
| have := List.sizeOf_lt_of_mem h₁ | ||
| apply on_concrete_eqv_concrete_eval arg request entities wf | ||
| exact Call.on_concrete_eqv_concrete_eval ih | ||
| termination_by expr | ||
| decreasing_by | ||
| all_goals simp_wf | ||
| all_goals try omega | ||
| case _ => -- record | ||
| have h₂ : sizeOf kv.snd < sizeOf kv := by simp only [sizeOf, Prod._sizeOf_1] ; omega | ||
| apply Nat.lt_trans h₂ | ||
| omega | ||
|
|
||
| /-- | ||
| `Prop` that a given `Result Partial.Value` is either a concrete value or an | ||
| error, not a residual | ||
| -/ | ||
| def isValueOrError : Result Partial.Value → Prop | ||
| | .ok (.value _) => true | ||
| | .ok (.residual _) => false | ||
| | .error _ => true | ||
|
|
||
| /-- | ||
| Corollary to the above: partial evaluation with concrete inputs gives a | ||
| concrete value (or an error) | ||
| -/ | ||
| theorem on_concrete_gives_concrete (expr : Spec.Expr) (request : Spec.Request) (entities : Spec.Entities) | ||
| (wf : request.WellFormed) : | ||
| isValueOrError (Partial.evaluate expr request entities) | ||
| := by | ||
| rw [on_concrete_eqv_concrete_eval expr request entities wf] | ||
| simp only [Except.map, isValueOrError] | ||
| split | ||
| <;> rename_i h | ||
| <;> split at h | ||
| <;> simp only [Except.ok.injEq, Except.error.injEq, Partial.Value.value.injEq] at h | ||
| <;> trivial |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,58 @@ | ||
| /- | ||
| Copyright Cedar Contributors | ||
| Licensed under the Apache License, Version 2.0 (the "License"); | ||
| you may not use this file except in compliance with the License. | ||
| You may obtain a copy of the License at | ||
| https://www.apache.org/licenses/LICENSE-2.0 | ||
| Unless required by applicable law or agreed to in writing, software | ||
| distributed under the License is distributed on an "AS IS" BASIS, | ||
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| See the License for the specific language governing permissions and | ||
| limitations under the License. | ||
| -/ | ||
|
|
||
| import Cedar.Partial.Evaluator | ||
| import Cedar.Spec.Evaluator | ||
| import Cedar.Thm.Data.Control | ||
| import Cedar.Thm.Partial.Evaluation.Basic | ||
|
|
||
| namespace Cedar.Thm.Partial.Evaluation.And | ||
|
|
||
| open Cedar.Data | ||
| open Cedar.Spec (Result) | ||
|
|
||
| /-- | ||
| Inductive argument that partial evaluating a concrete `Partial.Expr.and` | ||
| expression gives the same output as concrete-evaluating the `Spec.Expr.and` | ||
| with the same subexpressions | ||
| -/ | ||
| theorem on_concrete_eqv_concrete_eval {x₁ x₂ : Spec.Expr} {request : Spec.Request} {entities : Spec.Entities} : | ||
| PartialEvalEquivConcreteEval x₁ request entities → | ||
| PartialEvalEquivConcreteEval x₂ request entities → | ||
| PartialEvalEquivConcreteEval (Spec.Expr.and x₁ x₂) request entities | ||
| := by | ||
| unfold PartialEvalEquivConcreteEval | ||
| intro ih₁ ih₂ | ||
| unfold Partial.evaluate Spec.evaluate Spec.Expr.asPartialExpr | ||
| simp only [ih₁, ih₂] | ||
| simp only [Except.map, pure, Except.pure, Result.as, Coe.coe] | ||
| cases h₁ : Spec.evaluate x₁ request entities <;> simp only [Bool.not_eq_true', Except.bind_err, Except.bind_ok] | ||
| case ok v₁ => | ||
| simp only [Spec.Value.asBool] | ||
| cases v₁ <;> try simp only [Except.bind_err] | ||
| case prim p => | ||
| cases p <;> simp only [Except.bind_ok, Except.bind_err] | ||
| case bool b => | ||
| cases b <;> simp only [ite_true, ite_false] | ||
| case true => | ||
| split <;> simp only [Except.bind_ok, Except.bind_err] | ||
| case h_1 e h₂ => simp only [h₂, Except.bind_err] | ||
| case h_2 v h₂ => | ||
| simp only [h₂] | ||
| cases v <;> try simp only [Except.bind_err] | ||
| case prim p => cases p <;> simp | ||
|
|
||
| end Cedar.Thm.Partial.Evaluation.And |
Oops, something went wrong.