From 5fd24c1ea9b69cdd15a57a186addbe8ad7462d24 Mon Sep 17 00:00:00 2001 From: Emina Torlak Date: Tue, 7 Nov 2023 09:34:17 -0800 Subject: [PATCH 1/2] Add formalization of Int64 data type. --- cedar-lean/Cedar/Data/Int64.lean | 82 ++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 cedar-lean/Cedar/Data/Int64.lean diff --git a/cedar-lean/Cedar/Data/Int64.lean b/cedar-lean/Cedar/Data/Int64.lean new file mode 100644 index 000000000..922f1af33 --- /dev/null +++ b/cedar-lean/Cedar/Data/Int64.lean @@ -0,0 +1,82 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + 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 Std + +/-! +This file defines a signed 64-bit integer datatype similar to Rust's `i64`. +-/ + +namespace Cedar.Data + +def INT64_MIN : Int := -9223372036854775808 +def INT64_MAX : Int := 9223372036854775807 + +abbrev Int64 := { i : Int // INT64_MIN ≤ i ∧ i ≤ INT64_MAX } + +instance : Inhabited Int64 where + default := Subtype.mk 0 (by simp) + + +namespace Int64 + +----- Definitions ----- + +def mk (i : Int) (h : INT64_MIN ≤ i ∧ i ≤ INT64_MAX) : Int64 := + Subtype.mk i h + +def mk? (i : Int) : Option Int64 := + if h : INT64_MIN ≤ i ∧ i ≤ INT64_MAX + then .some (mk i h) + else .none + +def mk! (i : Int) : Int64 := + if h : INT64_MIN ≤ i ∧ i ≤ INT64_MAX + then mk i h + else panic! s!"not a signed 64-bit integer {i}" + +def lt (i₁ i₂ : Int64) : Bool := i₁.1 < i₂.1 + +def le (i₁ i₂ : Int64) : Bool := i₁.1 ≤ i₂.1 + +def add? (i₁ i₂ : Int64) : Option Int64 := mk? (i₁.1 + i₂.1) + +def sub? (i₁ i₂ : Int64) : Option Int64 := mk? (i₁.1 - i₂.1) + +def mul? (i₁ i₂ : Int64) : Option Int64 := mk? (i₁.1 * i₂.1) + +def neg? (i₁ : Int64) : Option Int64 := mk? (- i₁.1) + +----- Derivations ----- +instance : LT Int64 where + lt := fun i₁ i₂ => Int64.lt i₁ i₂ + +instance : LE Int64 where + le := fun i₁ i₂ => Int64.le i₁ i₂ + +instance int64Lt (i₁ i₂ : Int64) : Decidable (i₁ < i₂) := +if h : Int64.lt i₁ i₂ then isTrue h else isFalse h + +instance int64Le (i₁ i₂ : Int64) : Decidable (i₁ ≤ i₂) := +if h : Int64.le i₁ i₂ then isTrue h else isFalse h + +deriving instance Repr for Int64 +deriving instance DecidableEq for Int64 + +end Int64 + + +end Cedar.Data From a4bf9808d868c23165c23171e4dc06c40e9324d8 Mon Sep 17 00:00:00 2001 From: Emina Torlak Date: Tue, 7 Nov 2023 10:58:55 -0800 Subject: [PATCH 2/2] Change Cedar semantics to use bounded integers (Int64) and error-on-overflow behavior. --- cedar-lean/Cedar/Data.lean | 1 + cedar-lean/Cedar/Spec/Evaluator.lean | 14 +++++++++----- cedar-lean/Cedar/Spec/Expr.lean | 5 ++++- cedar-lean/Cedar/Spec/Value.lean | 16 +++++----------- cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean | 19 ++++++++++++------- 5 files changed, 31 insertions(+), 24 deletions(-) diff --git a/cedar-lean/Cedar/Data.lean b/cedar-lean/Cedar/Data.lean index 9ee23729e..b714ee8b7 100644 --- a/cedar-lean/Cedar/Data.lean +++ b/cedar-lean/Cedar/Data.lean @@ -14,5 +14,6 @@ limitations under the License. -/ +import Cedar.Data.Int64 import Cedar.Data.Set import Cedar.Data.Map diff --git a/cedar-lean/Cedar/Spec/Evaluator.lean b/cedar-lean/Cedar/Spec/Evaluator.lean index f989b0bff..348379260 100644 --- a/cedar-lean/Cedar/Spec/Evaluator.lean +++ b/cedar-lean/Cedar/Spec/Evaluator.lean @@ -26,10 +26,14 @@ open Cedar.Data open Except open Error +def intOrErr : Option Int64 → Result Value + | .some i => ok (.prim (.int i)) + | .none => error .arithBoundsError + def apply₁ : UnaryOp → Value → Result Value | .not, .prim (.bool b) => ok !b - | .neg, .prim (.int i) => ok ((- i) : Int) - | .mulBy c, .prim (.int i) => ok (c * i) + | .neg, .prim (.int i) => intOrErr i.neg? + | .mulBy c, .prim (.int i) => intOrErr (c.mul? i) | .like p, .prim (.string s) => ok (wildcardMatch s p) | .is ety, .prim (.entityUID uid) => ok (ety == uid.ty) | _, _ => error .typeError @@ -46,8 +50,8 @@ def apply₂ (op₂ : BinaryOp) (v₁ v₂ : Value) (es : Entities) : Result Val | .eq, _, _ => ok (v₁ == v₂) | .less, .prim (.int i), .prim (.int j) => ok ((i < j): Bool) | .lessEq, .prim (.int i), .prim (.int j) => ok ((i ≤ j): Bool) - | .add, .prim (.int i), .prim (.int j) => ok (i + j) - | .sub, .prim (.int i), .prim (.int j) => ok (i - j) + | .add, .prim (.int i), .prim (.int j) => intOrErr (i.add? j) + | .sub, .prim (.int i), .prim (.int j) => intOrErr (i.sub? j) | .contains, .set vs₁, _ => ok (vs₁.contains v₂) | .containsAll, .set vs₁, .set vs₂ => ok (vs₂.subset vs₁) | .containsAny, .set vs₁, .set vs₂ => ok (vs₁.intersects vs₂) @@ -114,4 +118,4 @@ def evaluate (x : Expr) (req : Request) (es : Entities) : Result Value := let vs ← xs.mapM₁ (fun ⟨x₁, _⟩ => evaluate x₁ req es) call xfn vs -end Cedar.Spec \ No newline at end of file +end Cedar.Spec diff --git a/cedar-lean/Cedar/Spec/Expr.lean b/cedar-lean/Cedar/Spec/Expr.lean index 1e5f7e7fa..5a04a2634 100644 --- a/cedar-lean/Cedar/Spec/Expr.lean +++ b/cedar-lean/Cedar/Spec/Expr.lean @@ -14,6 +14,7 @@ limitations under the License. -/ +import Cedar.Data import Cedar.Spec.ExtFun import Cedar.Spec.Wildcard @@ -21,6 +22,8 @@ import Cedar.Spec.Wildcard namespace Cedar.Spec +open Cedar.Data + ----- Definitions ----- inductive Var where @@ -32,7 +35,7 @@ inductive Var where inductive UnaryOp where | not | neg - | mulBy (i : Int) + | mulBy (i : Int64) | like (p : Pattern) | is (ety : EntityType) diff --git a/cedar-lean/Cedar/Spec/Value.lean b/cedar-lean/Cedar/Spec/Value.lean index f08470763..a08f4ddfd 100644 --- a/cedar-lean/Cedar/Spec/Value.lean +++ b/cedar-lean/Cedar/Spec/Value.lean @@ -31,6 +31,7 @@ inductive Error where | entityDoesNotExist | attrDoesNotExist | typeError + | arithBoundsError | extensionError abbrev Result (α) := Except Error α @@ -49,7 +50,7 @@ structure EntityUID where inductive Prim where | bool (b : Bool) - | int (i : Int) + | int (i : Int64) | string (s : String) | entityUID (uid : EntityUID) @@ -79,7 +80,7 @@ def Value.asString : Value → Result String | .prim (.string s) => ok s | _ => error Error.typeError -def Value.asInt : Value → Result Int +def Value.asInt : Value → Result Int64 | .prim (.int i) => ok i | _ => error Error.typeError @@ -90,7 +91,7 @@ def Result.as {α} (β) [Coe α (Result β)] : Result α → Result β instance : Coe Bool Value where coe b := .prim (.bool b) -instance : Coe Int Value where +instance : Coe Int64 Value where coe i := .prim (.int i) instance : Coe String Value where @@ -114,7 +115,7 @@ instance : Coe (Map Attr Value) Value where instance : Coe Value (Result Bool) where coe v := v.asBool -instance : Coe Value (Result Int) where +instance : Coe Value (Result Int64) where coe v := v.asInt instance : Coe Value (Result String) where @@ -230,9 +231,6 @@ instance : LT Name where instance Name.decLt (n m : Name) : Decidable (n < m) := if h : Name.lt n m then isTrue h else isFalse h --- lol for some reason eta reduction breaks this (can't handle the implicit arguments) -instance : Ord EntityType where - compare a b := compareOfLessAndEq a b def EntityUID.lt (a b : EntityUID) : Bool := (a.ty < b.ty) ∨ (a.ty = b.ty ∧ a.eid < b.eid) @@ -317,10 +315,6 @@ instance : LT Value where instance Value.decLt (n m : Value) : Decidable (n < m) := if h : Value.lt n m then isTrue h else isFalse h -instance : Ord Value where - compare a b := compareOfLessAndEq a b - - deriving instance Inhabited for Value end Cedar.Spec diff --git a/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean b/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean index 451755238..09b3bb5c5 100644 --- a/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean +++ b/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean @@ -105,24 +105,29 @@ def RequestAndEntitiesMatchEnvironment (env : Environment) (request : Request) ( /-- The type soundness property says that if the typechecker assigns a type to an expression, then it must be the case that the expression `EvaluatesTo` a value -of that type. The `EvaluatesTo` predicate covers the (obvious) case where evaluation -has no errors, but it also allows for errors of type `entityDoesNotExist` and -`extensionError`. +of that type. The `EvaluatesTo` predicate covers the (obvious) case where +evaluation has no errors, but it also allows for errors of type +`entityDoesNotExist`, `extensionError`, and `arithBoundsError`. -The typechecker cannot protect against these errors because they depend on runtime -information (i.e., the entities passed into the authorization request, and -extension function applications on authorization-time data). All other errors -(`attrDoesNotExist` and `typeError`) can be prevented statically. +The typechecker cannot protect against these errors because they depend on +runtime information (i.e., the entities passed into the authorization request, +extension function applications on authorization-time data, and arithmetic +overflow errors). All other errors (`attrDoesNotExist` and `typeError`) can be +prevented statically. _Note_: Currently, `extensionError`s can also be ruled out at validation time because the only extension functions that can error are constructors, and all constructors are required to be applied to string literals, meaning that they can be fully evaluated during validation. This is not guaranteed to be the case in the future. + +_Note_: We plan to implement a range analysis that will be able to rule out +`arithBoundsError`s. -/ def EvaluatesTo (e: Expr) (request : Request) (entities : Entities) (v : Value) : Prop := evaluate e request entities = .error .entityDoesNotExist ∨ evaluate e request entities = .error .extensionError ∨ + evaluate e request entities = .error .arithBoundsError ∨ evaluate e request entities = .ok v /--