Change Cedar semantics to use bounded integers (Int64) and error-on-o…

…verflow behavior.

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