Refactor models and proofs to use Lean's Int64. (#515)

Signed-off-by: Emina Torlak <[email protected]>
Co-authored-by: Emina Torlak <[email protected]>

cedar-lean/Cedar/Data/Int64.lean

@@ -17,71 +17,54 @@
 import Cedar.Data.LT
 
 /-!
-This file defines a signed 64-bit integer datatype similar to Rust's `i64`.
+This file defines a signed 64-bit integer datatype similar to Rust's `i64`
+by adding checked arithmetic operations to Lean's Int64 datatype.
 -/
 
-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 decide)
-
-
 namespace Int64
 
+def MIN : Int := -9223372036854775808
+def MAX : Int :=  9223372036854775807
+
 ----- Definitions -----
 
-def mk (i : Int) (h : INT64_MIN ≤ i ∧ i ≤ INT64_MAX) : Int64 :=
-  Subtype.mk i h
+def ofIntChecked (i : Int) (_ : MIN ≤ i ∧ i ≤ MAX) : Int64 :=
+  Int64.ofInt i
 
-def mk? (i : Int) : Option Int64 :=
-  if h : INT64_MIN ≤ i ∧ i ≤ INT64_MAX
-  then .some (mk i h)
+def ofInt? (i : Int) : Option Int64 :=
+  if h : MIN ≤ i ∧ i ≤ MAX
+  then .some (ofIntChecked i h)
   else .none
 
-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 := ofInt? (i₁.toInt + i₂.toInt)
 
-def add? (i₁ i₂ : Int64) : Option Int64 := mk? (i₁.1 + i₂.1)
+def sub? (i₁ i₂ : Int64) : Option Int64 := ofInt? (i₁.toInt - i₂.toInt)
 
-def sub? (i₁ i₂ : Int64) : Option Int64 := mk? (i₁.1 - i₂.1)
+def mul? (i₁ i₂ : Int64) : Option Int64 := ofInt? (i₁.toInt * i₂.toInt)
 
-def mul? (i₁ i₂ : Int64) : Option Int64 := mk? (i₁.1 * i₂.1)
+def neg? (i₁ : Int64) : Option Int64 := ofInt? (- i₁.toInt)
 
-def neg? (i₁ : Int64) : Option Int64 := mk? (- i₁.1)
-
-def natAbs (i₁ : Int64) : Nat := i₁.1.natAbs
+def natAbs (i₁ : Int64) : Nat := i₁.toInt.natAbs
 
 ----- 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
 
-theorem ext_iff {i₁ i₂ : Int64} : i₁ = i₂ ↔ i₁.1 = i₂.1 := by
-  cases i₁; cases i₂; simp
+theorem ext_iff {i₁ i₂ : Int64} : i₁ = i₂ ↔ i₁.toInt = i₂.toInt := by
+  constructor <;> intro h₁
+  · simp only [h₁]
+  · cases i₁ ; cases i₂ ; rename_i i₁ i₂
+    simp only [mk.injEq]
+    simp only [toInt, BitVec.toInt_inj, Int64.toBitVec, UInt64.toBitVec_inj] at h₁
+    exact h₁
 
-theorem lt_def {i₁ i₂ : Int64} : i₁ < i₂ ↔ i₁.1 < i₂.1 := by
-  simp [LT.lt, Int64.lt]
+theorem lt_def {i₁ i₂ : Int64} : i₁ < i₂ ↔ i₁.toInt < i₂.toInt := by
+  simp [LT.lt, Int64.lt, BitVec.slt, Int64.toInt]
 
-theorem le_def {i₁ i₂ : Int64} : i₁ ≤ i₂ ↔ i₁.1 ≤ i₂.1 := by
-  simp [LE.le, Int64.le]
+theorem le_def {i₁ i₂ : Int64} : i₁ ≤ i₂ ↔ i₁.toInt ≤ i₂.toInt := by
+  simp [LE.le, Int64.le, BitVec.sle, Int64.toInt]
 
-deriving instance Repr, DecidableEq for Int64
+deriving instance Repr for Int64
 
-instance strictLT : StrictLT Int64 where
+instance strictLT : Cedar.Data.StrictLT Int64 where
   asymmetric a b   := by
     simp [Int64.lt_def]
     omega
@@ -92,7 +75,7 @@ instance strictLT : StrictLT Int64 where
     simp [Int64.lt_def, Int64.ext_iff]
     omega
 
-end Int64
-
+instance : Coe Int64 Int where
+  coe i := i.toInt
 
-end Cedar.Data
+end Int64

cedar-lean/Cedar/Spec/Evaluator.lean

@@ -26,7 +26,7 @@ namespace Cedar.Spec
 open Cedar.Data
 open Error
 
-def intOrErr : Option Data.Int64 → Result Value
+def intOrErr : Option Int64 → Result Value
   | .some i => .ok (.prim (.int i))
   | .none   => .error .arithBoundsError
 

cedar-lean/Cedar/Spec/Ext/Datetime.lean

@@ -38,7 +38,7 @@ open Cedar.Data
 
   A duration may be negative. Negative duration strings must begin with `-`.
 -/
-abbrev Duration := Data.Int64
+abbrev Duration := Int64
 
 namespace Datetime
 
@@ -49,11 +49,10 @@ def MILLISECONDS_PER_DAY: Int := 86400000
 
 ----- Definitions -----
 
-def duration? (i : Int) : Option Duration :=
-  Int64.mk? i
+abbrev duration? := Int64.ofInt?
 
 def durationUnits? (n: Nat) (suffix: String) : Option Duration :=
-  match Int64.mk? n with
+  match Int64.ofInt? n with
   | none => none
   | some i =>
     match suffix with

cedar-lean/Cedar/Spec/Ext/Decimal.lean

@@ -32,14 +32,14 @@ We restrict the number of the digits after the decimal point to 4.
 
 def DECIMAL_DIGITS : Nat := 4
 
-abbrev Decimal := Data.Int64
+abbrev Decimal := Int64
 
 namespace Decimal
 
 ----- Definitions -----
 
 def decimal? (i : Int) : Option Decimal :=
-  Int64.mk? i
+  Int64.ofInt? i
 
 def parse (str : String) : Option Decimal :=
   match str.split (· = '.') with
@@ -60,7 +60,7 @@ def parse (str : String) : Option Decimal :=
 
 instance : ToString Decimal where
   toString (d : Decimal) : String :=
-    let neg   := if d < (0 : Int) then "-" else ""
+    let neg   := if d < 0 then "-" else ""
     let d     := d.natAbs
     let left  := d / (Nat.pow 10 DECIMAL_DIGITS)
     let right := d % (Nat.pow 10 DECIMAL_DIGITS)

cedar-lean/Cedar/Spec/Value.lean

@@ -58,7 +58,7 @@ instance : ToString EntityUID where
 
 inductive Prim where
   | bool (b : Bool)
-  | int (i : Data.Int64)
+  | int (i : Int64)
   | string (s : String)
   | entityUID (uid : EntityUID)
 
@@ -88,7 +88,7 @@ def Value.asString : Value →  Result String
   | .prim (.string s) => .ok s
   | _ => .error Error.typeError
 
-def Value.asInt : Value →  Result Data.Int64
+def Value.asInt : Value →  Result Int64
   | .prim (.int i) => .ok i
   | _ => .error Error.typeError
 
@@ -99,7 +99,7 @@ def Result.as {α} (β) [Coe α (Result β)] : Result α → Result β
 instance : Coe Bool Value where
   coe b := .prim (.bool b)
 
-instance : Coe Data.Int64 Value where
+instance : Coe Int64 Value where
   coe i := .prim (.int i)
 
 instance : Coe String Value where
@@ -123,7 +123,7 @@ instance : Coe (Map Attr Value) Value where
 instance : Coe Value (Result Bool) where
   coe v := v.asBool
 
-instance : Coe Value (Result Data.Int64) where
+instance : Coe Value (Result Int64) where
   coe v := v.asInt
 
 instance : Coe Value (Result String) where

cedar-lean/Cedar/Thm/Data/LT.lean

@@ -133,10 +133,7 @@ instance Ext.strictLT : StrictLT Ext where
     cases a <;> cases b <;> simp [LT.lt, Ext.lt] <;>
     rename_i x₁ x₂ <;> intro h₁
     case decimal =>
-      have h₂ := Data.Int64.strictLT.asymmetric x₁ x₂
-      simp [LT.lt] at h₂
-      cases h₃ : Data.Int64.lt x₁ x₂ <;>
-      simp [h₃] at h₁ h₂ ; simp [h₂]
+      exact Int64.strictLT.asymmetric x₁ x₂ h₁
     case ipaddr =>
       have h₂ := IPNet.strictLT.asymmetric x₁ x₂
       simp [LT.lt] at h₂
@@ -146,11 +143,7 @@ instance Ext.strictLT : StrictLT Ext where
     cases a <;> cases b <;> cases c <;> simp [LT.lt, Ext.lt] <;>
     rename_i x₁ x₂ x₃ <;> intro h₁ h₂
     case decimal =>
-      have h₃ := Data.Int64.strictLT.transitive x₁ x₂ x₃
-      simp [LT.lt] at h₃
-      cases h₄ : Data.Int64.lt x₁ x₂ <;> simp [h₄] at *
-      cases h₅ : Data.Int64.lt x₂ x₃ <;> simp [h₅] at *
-      simp [h₃]
+      exact Int64.strictLT.transitive x₁ x₂ x₃ h₁ h₂
     case ipaddr =>
       have h₃ := IPNet.strictLT.transitive x₁ x₂ x₃
       simp [LT.lt] at h₃
@@ -161,9 +154,7 @@ instance Ext.strictLT : StrictLT Ext where
     cases a <;> cases b <;> simp [LT.lt, Ext.lt] <;>
     rename_i x₁ x₂ <;> intro h₁
     case decimal =>
-      have h₂ := Data.Int64.strictLT.connected x₁ x₂
-      simp [LT.lt, h₁] at h₂
-      rcases h₂ with h₂ | h₂ <;> simp [h₂]
+      exact Int64.strictLT.connected x₁ x₂ h₁
     case ipaddr =>
       have h₂ := IPNet.strictLT.connected x₁ x₂
       simp [LT.lt, h₁] at h₂
@@ -261,7 +252,7 @@ theorem Prim.lt_asymm {a b : Prim} :
   cases a <;> cases b <;> simp [LT.lt] <;>
   simp [Prim.lt]
   case bool b₁ b₂          => exact Bool.strictLT.asymmetric b₁ b₂
-  case int i₁ i₂           => exact (Data.Int64.strictLT.asymmetric i₁ i₂)
+  case int i₁ i₂           => exact (Int64.strictLT.asymmetric i₁ i₂)
   case string s₁ s₂        => exact (String.strictLT.asymmetric s₁ s₂)
   case entityUID uid₁ uid₂ => exact (EntityUID.strictLT.asymmetric uid₁ uid₂)
 
@@ -271,7 +262,7 @@ theorem Prim.lt_trans {a b c : Prim} :
   cases a <;> cases b <;> cases c <;> simp [LT.lt] <;>
   simp [Prim.lt]
   case bool b₁ b₂ b₃            => exact (Bool.strictLT.transitive b₁ b₂ b₃)
-  case int i₁ i₂ i₃             => exact (Data.Int64.strictLT.transitive i₁ i₂ i₃)
+  case int i₁ i₂ i₃             => exact (Int64.strictLT.transitive i₁ i₂ i₃)
   case string s₁ s₂ s₃          => exact (String.strictLT.transitive s₁ s₂ s₃)
   case entityUID uid₁ uid₂ uid₃ => exact (EntityUID.strictLT.transitive uid₁ uid₂ uid₃)
 
@@ -281,7 +272,7 @@ theorem Prim.lt_conn {a b : Prim} :
   cases a <;> cases b <;> simp [LT.lt] <;>
   simp [Prim.lt]
   case bool b₁ b₂          => exact (Bool.strictLT.connected b₁ b₂)
-  case int i₁ i₂           => exact (Data.Int64.strictLT.connected i₁ i₂)
+  case int i₁ i₂           => exact (Int64.strictLT.connected i₁ i₂)
   case string s₁ s₂        => exact (String.strictLT.connected s₁ s₂)
   case entityUID uid₁ uid₂ => exact (EntityUID.strictLT.connected uid₁ uid₂)
 

cedar-lean/CedarProto/ActionConstraint.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 import Protobuf.Enum
 
 -- Message Dependencies

cedar-lean/CedarProto/AuthorizationRequest.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 
 -- Message Dependencies
 import CedarProto.Request

cedar-lean/CedarProto/Context.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 import Protobuf.Message
 import Protobuf.Map
 import Protobuf.String

cedar-lean/CedarProto/Entities.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 
 -- Message Dependencies
 import CedarProto.Entity

cedar-lean/CedarProto/Entity.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 
 -- Message Dependencies
 import CedarProto.EntityUID

cedar-lean/CedarProto/EntityReference.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 import Protobuf.Enum
 
 -- Message Dependencies

cedar-lean/CedarProto/EntityType.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 import Protobuf.Message
 
 -- Message Dependencies

cedar-lean/CedarProto/EntityUID.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 import Protobuf.Message
 import Protobuf.String
 

cedar-lean/CedarProto/EntityUIDEntry.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 import Protobuf.Message
 import Protobuf.String
 

cedar-lean/CedarProto/Expr.lean

@@ -14,7 +14,8 @@
  limitations under the License.
 -/
 
-import Cedar
+import Cedar.Spec
+import Cedar.Data.Int64
 import Protobuf.Message
 import Protobuf.Enum
 import Protobuf.Map
@@ -45,17 +46,17 @@ def merge_bool (p : Prim) (b2 : Bool) : Prim :=
 @[inline]
 def merge_int (_ : Prim) (pi : Proto.Int64) : Prim :=
   have i : Int := pi
-  if H1 : i < Cedar.Data.INT64_MIN then
+  if H1 : i < Int64.MIN then
     panic!("Integer less than INT64_MIN")
-  else if H2 : i > Cedar.Data.INT64_MAX then
+  else if H2 : i > Int64.MAX then
     panic!("Integer greater than INT64_MAX")
   else
-    have h1 : Cedar.Data.INT64_MIN ≤ i ∧ i ≤ Cedar.Data.INT64_MAX := by
+    have h1 : Int64.MIN ≤ i ∧ i ≤ Int64.MAX := by
       unfold Proto.Int64 at *
       omega
 
     -- Override semantics
-    Prim.int (Cedar.Data.Int64.mk i h1)
+    Prim.int (Int64.ofIntChecked i h1)
 
 @[inline]
 def merge_string (p : Prim) (s2 : String) : Prim :=
@@ -74,7 +75,7 @@ def merge (p1 : Prim) (p2 : Prim) : Prim :=
   match p2 with
     | .bool b2 => merge_bool p1 b2
     | .int i2 =>
-      let i2₁ : Int := i2
+      let i2₁ : Int := i2.toInt
       let i2₂ : Proto.Int64 := i2₁
       merge_int p1 i2₂
     | .string s2 => merge_string p1 s2

cedar-lean/CedarProto/LiteralPolicy.lean

@@ -13,7 +13,7 @@
  See the License for the specific language governing permissions and
  limitations under the License.
 -/
-import Cedar
+import Cedar.Spec
 
 -- Message Dependencies
 import CedarProto.EntityUID