Formalize the use of bounded integers and error-on-overflow semantics

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

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

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
+end Cedar.Spec

cedar-lean/Cedar/Spec/Expr.lean

@@ -14,13 +14,16 @@
  limitations under the License.
 -/
 
+import Cedar.Data
 import Cedar.Spec.ExtFun
 import Cedar.Spec.Wildcard
 
 /-! This file defines abstract syntax for Cedar expressions. -/
 
 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)
 

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

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
 
 /--