Cherry-pick #260 to 3.1.x: update for cedar#702 (RFC 57) (#261)

Signed-off-by: Craig Disselkoen <[email protected]>

Author: cdisselkoen

cedar

@@ -33,10 +33,9 @@ def intOrErr : Option Int64 → Result Value
 def apply₁ : UnaryOp → Value → Result Value
   | .not,     .prim (.bool b)        => ok !b
   | .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
+  | .like p,  .prim (.string s)      => .ok (wildcardMatch s p)
+  | .is ety,  .prim (.entityUID uid) => .ok (ety == uid.ty)
+  | _, _                             => .error .typeError
 
 def inₑ (uid₁ uid₂ : EntityUID) (es : Entities) : Bool :=
   uid₁ == uid₂ || (es.ancestorsOrEmpty uid₁).contains uid₂
@@ -52,10 +51,11 @@ def apply₂ (op₂ : BinaryOp) (v₁ v₂ : Value) (es : Entities) : Result Val
   | .lessEq, .prim (.int i), .prim (.int j)                => ok ((i ≤ j): Bool)
   | .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₂)
-  | .mem, .prim (.entityUID uid₁), .prim (.entityUID uid₂) => ok (inₑ uid₁ uid₂ es)
+  | .mul,    .prim (.int i), .prim (.int j)                => intOrErr (i.mul? 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₂)
+  | .mem, .prim (.entityUID uid₁), .prim (.entityUID uid₂) => .ok (inₑ uid₁ uid₂ es)
   | .mem, .prim (.entityUID uid₁), .set (vs)               => inₛ uid₁ vs es
   | _, _, _                                                => error .typeError
 

cedar-lean/Cedar/Spec/Evaluator.lean

@@ -35,7 +35,6 @@ inductive Var where
 inductive UnaryOp where
   | not
   | neg
-  | mulBy (i : Int64)
   | like (p : Pattern)
   | is (ety : EntityType)
 
@@ -46,6 +45,7 @@ inductive BinaryOp where
   | lessEq
   | add
   | sub
+  | mul
   | contains
   | containsAll
   | containsAny

cedar-lean/Cedar/Spec/Expr.lean

@@ -214,7 +214,7 @@ theorem type_of_int_cmp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c
     }
 
 theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : CedarType}
-  (h₁ : op₂ = .add ∨ op₂ = .sub)
+  (h₁ : op₂ = .add ∨ op₂ = .sub ∨ op₂ = .mul)
   (h₂ : typeOf (Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (ty, c')) :
   c' = ∅ ∧
   ty = .int ∧
@@ -224,7 +224,7 @@ theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c'
   simp [typeOf] at *
   cases h₃ : typeOf x₁ c env <;> simp [h₃] at h₂
   cases h₄ : typeOf x₂ c env <;> simp [h₄] at h₂
-  rcases h₁ with h₁ | h₁
+  rcases h₁ with h₁ | h₁ | h₁
   all_goals {
     subst h₁
     simp [typeOfBinaryApp, err, ok] at h₂
@@ -238,7 +238,7 @@ theorem type_of_int_arith_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c'
   }
 
 theorem type_of_int_arith_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities}
-  (h₀ : op₂ = .add ∨ op₂ = .sub)
+  (h₀ : op₂ = .add ∨ op₂ = .sub ∨ op₂ = .mul)
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
   (h₃ : typeOf (Expr.binaryApp op₂ x₁ x₂) c₁ env = Except.ok (ty, c₂))
@@ -266,15 +266,19 @@ theorem type_of_int_arith_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c
     have ⟨i₁, ih₁⟩ := instance_of_int_is_int ih₃
     have ⟨i₂, ih₂⟩ := instance_of_int_is_int ih₄
     subst ih₁ ih₂
-    rcases h₀ with h₀ | h₀ <;> subst h₀ <;> simp [apply₂, intOrErr]
+    rcases h₀ with h₀ | h₀ | h₀ <;> subst h₀ <;> simp [apply₂, intOrErr]
     case inl =>
       cases h₄ : Int64.add? i₁ i₂ <;> simp [h₄]
       case none => exact type_is_inhabited CedarType.int
       case some => simp [InstanceOfType.instance_of_int]
-    case inr =>
+    case inr.inl =>
       cases h₄ : Int64.sub? i₁ i₂ <;> simp [h₄]
       case none => exact type_is_inhabited CedarType.int
       case some => simp [InstanceOfType.instance_of_int]
+    case inr.inr =>
+      cases h₄ : Int64.mul? i₁ i₂ <;> simp [h₄]
+      case none => exact type_is_inhabited CedarType.int
+      case some => simp [InstanceOfType.instance_of_int]
 
 theorem type_of_contains_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : CedarType}
   (h₁ : typeOf (Expr.binaryApp .contains x₁ x₂) c env = Except.ok (ty, c')) :
@@ -838,7 +842,8 @@ theorem type_of_binaryApp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c
   | .less
   | .lessEq      => exact type_of_int_cmp_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂
   | .add
-  | .sub         => exact type_of_int_arith_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂
+  | .sub
+  | .mul         => exact type_of_int_arith_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂
   | .contains    => exact type_of_contains_is_sound h₁ h₂ h₃ ih₁ ih₂
   | .containsAll
   | .containsAny => exact type_of_containsA_is_sound (by simp) h₁ h₂ h₃ ih₁ ih₂

cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean

@@ -133,53 +133,6 @@ theorem type_of_neg_is_sound {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Env
       exact type_is_inhabited CedarType.int
     }
 
-theorem type_of_mulBy_inversion {x₁ : Expr} {k : Int64} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType}
-  (h₁ : typeOf (Expr.unaryApp (.mulBy k) x₁) c₁ env = Except.ok (ty, c₂)) :
-  c₂ = ∅ ∧
-  ty = .int ∧
-  ∃ c₁', typeOf x₁ c₁ env = Except.ok (.int, c₁')
-:= by
-  simp [typeOf] at h₁
-  cases h₂ : typeOf x₁ c₁ env <;> simp [h₂] at h₁
-  case ok res =>
-    have ⟨ty₁, c₁'⟩ := res
-    simp [typeOfUnaryApp] at h₁
-    split at h₁ <;> try contradiction
-    simp [ok] at h₁
-    simp [h₁]
-
-theorem type_of_mulBy_is_sound {x₁ : Expr} {k : Int64} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities}
-  (h₁ : CapabilitiesInvariant c₁ request entities)
-  (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
-  (h₃ : typeOf (Expr.unaryApp (.mulBy k) x₁) c₁ env = Except.ok (ty, c₂))
-  (ih : TypeOfIsSound x₁) :
-  GuardedCapabilitiesInvariant (Expr.unaryApp (.mulBy k) x₁) c₂ request entities ∧
-  ∃ v, EvaluatesTo (Expr.unaryApp (.mulBy k) x₁) request entities v ∧ InstanceOfType v ty
-:= by
-  have ⟨h₅, h₆, c₁', h₄⟩ := type_of_mulBy_inversion h₃
-  subst h₅; subst h₆
-  apply And.intro
-  case left => exact empty_guarded_capabilities_invariant
-  case right =>
-    have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄ -- IH
-    simp [EvaluatesTo] at h₆
-    simp [EvaluatesTo, evaluate]
-    rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆]
-    case inr.inr.inr =>
-      have ⟨i, h₈⟩ := instance_of_int_is_int h₇
-      subst h₈
-      simp [apply₁, intOrErr]
-      cases h₉ : k.mul? i
-      case none =>
-        simp only [or_false, or_true, true_and]
-        exact type_is_inhabited CedarType.int
-      case some i' =>
-        simp only [Except.ok.injEq, false_or, exists_eq_left']
-        apply InstanceOfType.instance_of_int
-    all_goals {
-      exact type_is_inhabited CedarType.int
-    }
-
 theorem type_of_like_inversion {x₁ : Expr} {p : Pattern} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType}
   (h₁ : typeOf (Expr.unaryApp (.like p) x₁) c₁ env = Except.ok (ty, c₂)) :
   c₂ = ∅ ∧
@@ -234,7 +187,7 @@ theorem type_of_is_inversion {x₁ : Expr} {ety : EntityType} {c₁ c₂ : Capab
     have ⟨ty₁, c₁'⟩ := res
     simp [typeOfUnaryApp] at h₁
     split at h₁ <;> try contradiction
-    case h_5 _ _ ety' h₃ =>
+    case h_4 _ _ ety' h₃ =>
       simp only [UnaryOp.is.injEq] at h₃
       subst h₃
       simp [ok] at h₁
@@ -284,7 +237,6 @@ theorem type_of_unaryApp_is_sound {op₁ : UnaryOp} {x₁ : Expr} {c₁ c₂ : C
   match op₁ with
   | .not     => exact type_of_not_is_sound h₁ h₂ h₃ ih
   | .neg     => exact type_of_neg_is_sound h₁ h₂ h₃ ih
-  | .mulBy k => exact type_of_mulBy_is_sound h₁ h₂ h₃ ih
   | .like p  => exact type_of_like_is_sound h₁ h₂ h₃ ih
   | .is ety  => exact type_of_is_is_sound h₁ h₂ h₃ ih
 

cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean

@@ -106,7 +106,6 @@ def typeOfUnaryApp (op : UnaryOp) (ty : CedarType) : ResultType :=
   match op, ty with
   | .not, .bool x          => ok (.bool x.not)
   | .neg, .int             => ok .int
-  | .mulBy _, .int         => ok .int
   | .like _, .string       => ok (.bool .anyBool)
   | .is ety₁, .entity ety₂ => ok (.bool (if ety₁ = ety₂ then .tt else .ff))
   | _, _                   => err (.unexpectedType ty)
@@ -172,6 +171,7 @@ def typeOfBinaryApp (op₂ : BinaryOp) (ty₁ ty₂ : CedarType) (x₁ x₂ : Ex
   | .lessEq, .int, .int                     => ok (.bool .anyBool)
   | .add,    .int, .int                     => ok .int
   | .sub,    .int, .int                     => ok .int
+  | .mul,    .int, .int                     => ok .int
   | .contains, .set ty₃, _                  => ifLubThenBool ty₂ ty₃
   | .containsAll, .set ty₃, .set ty₄        => ifLubThenBool ty₃ ty₄
   | .containsAny, .set ty₃, .set ty₄        => ifLubThenBool ty₃ ty₄

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -117,6 +117,7 @@ def jsonToBinaryOp (json : Lean.Json) : ParseResult BinaryOp := do
   | "LessEq" => .ok .lessEq
   | "Add" => .ok .add
   | "Sub" => .ok .sub
+  | "Mul" => .ok .mul
   | "Contains" => .ok .contains
   | "ContainsAll" => .ok .containsAll
   | "ContainsAny" => .ok .containsAny
@@ -181,10 +182,6 @@ partial def jsonToExpr (json : Lean.Json) : ParseResult Expr := do
     let op ← getJsonField body "op" >>= jsonToUnaryOp
     let arg ← getJsonField body "arg" >>= jsonToExpr
     .ok (.unaryApp op arg)
-  | "MulByConst" => do
-    let c ← getJsonField body "constant" >>= jsonToInt64
-    let arg ← getJsonField body "arg" >>= jsonToExpr
-    .ok (.unaryApp (.mulBy c) arg)
   | "Like" => do
     let pat ← getJsonField body "pattern" >>= jsonToPattern
     let expr ← getJsonField body "expr" >>= jsonToExpr

cedar-lean/DiffTest/Parser.lean

@@ -108,13 +108,10 @@ impl<'a> ExprGenerator<'a> {
                         self.generate_expr(max_depth - 1, u)?,
                         self.generate_expr(max_depth - 1, u)?,
                     )),
-                    1 => {
-                        // arbitrary expression, which may be a constant
-                        let expr = self.generate_expr(max_depth - 1, u)?;
-                        // arbitrary constant integer
-                        let c = self.constant_pool.arbitrary_int_constant(u)?;
-                        Ok(ast::Expr::mul(expr, c))
-                    },
+                    1 => Ok(ast::Expr::mul(
+                        self.generate_expr(max_depth - 1, u)?,
+                        self.generate_expr(max_depth - 1, u)?,
+                    )),
                     1 => {
                         // negation expression
                         Ok(ast::Expr::neg(self.generate_expr(max_depth - 1, u)?))
@@ -641,17 +638,18 @@ impl<'a> ExprGenerator<'a> {
                             )?,
                         )),
                         // * expression
-                        1 => {
-                            // arbitrary expression, which may be a constant
-                            let expr = self.generate_expr_for_type(
+                        1 => Ok(ast::Expr::mul(
+                            self.generate_expr_for_type(
                                 &Type::long(),
                                 max_depth - 1,
                                 u,
-                            )?;
-                            // arbitrary integer constant
-                            let c = self.constant_pool.arbitrary_int_constant(u)?;
-                            Ok(ast::Expr::mul(expr, c))
-                        },
+                            )?,
+                            self.generate_expr_for_type(
+                                &Type::long(),
+                                max_depth - 1,
+                                u,
+                            )?,
+                        )),
                         // negation expression
                         1 => Ok(ast::Expr::neg(self.generate_expr_for_type(
                             &Type::long(),