isEmpty method

cedar-lean/Cedar/Spec/Evaluator.lean

@@ -33,6 +33,7 @@ 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?
+  | .isEmpty, .set s                 => .ok s.isEmpty
   | .like p,  .prim (.string s)      => .ok (wildcardMatch s p)
   | .is ety,  .prim (.entityUID uid) => .ok (ety == uid.ty)
   | _, _                             => .error .typeError

cedar-lean/Cedar/Spec/Expr.lean

@@ -36,6 +36,7 @@ inductive Var where
 inductive UnaryOp where
   | not
   | neg
+  | isEmpty
   | like (p : Pattern)
   | is (ety : EntityType)
 

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

@@ -128,6 +128,46 @@ theorem type_of_neg_is_sound {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Env
     exact type_is_inhabited CedarType.int
   }
 
+theorem type_of_isEmpty_inversion {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType}
+  (h₁ : typeOf (Expr.unaryApp .isEmpty x₁) c₁ env = Except.ok (ty, c₂)) :
+  c₂ = ∅ ∧
+  ty = .bool .anyBool ∧
+  ∃ c₁' ty₀, typeOf x₁ c₁ env = Except.ok (.set ty₀, 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_isEmpty_is_sound {x₁ : Expr} {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 .isEmpty x₁) c₁ env = Except.ok (ty, c₂))
+  (ih : TypeOfIsSound x₁) :
+  GuardedCapabilitiesInvariant (Expr.unaryApp .isEmpty x₁) c₂ request entities ∧
+  ∃ v, EvaluatesTo (Expr.unaryApp .isEmpty x₁) request entities v ∧ InstanceOfType v ty
+:= by
+  have ⟨h₅, h₆, c₁', h₄⟩ := type_of_isEmpty_inversion h₃
+  subst h₅; subst h₆
+  apply And.intro empty_guarded_capabilities_invariant
+  replace ⟨ty₀, h₄⟩ := h₄
+  have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄
+  simp [EvaluatesTo, evaluate] at *
+  rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆]
+  case inr.inr.inr =>
+    have ⟨s, h₈⟩ := instance_of_set_type_is_set h₇
+    subst h₈
+    simp [apply₁]
+    apply InstanceOfType.instance_of_bool
+    simp [InstanceOfBoolType]
+  all_goals {
+    exact type_is_inhabited (.bool .anyBool)
+  }
+
 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₂ = ∅ ∧
@@ -180,7 +220,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_4 _ _ ety' h₃ =>
+    case h_5 _ _ ety' h₃ =>
       simp only [UnaryOp.is.injEq] at h₃
       subst h₃
       simp [ok] at h₁
@@ -227,6 +267,7 @@ 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
+  | .isEmpty => exact type_of_isEmpty_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/Validation/Typechecker.lean

@@ -112,6 +112,7 @@ def typeOfUnaryApp (op : UnaryOp) (ty : CedarType) : ResultType :=
   match op, ty with
   | .not, .bool x          => ok (.bool x.not)
   | .neg, .int             => ok .int
+  | .isEmpty, .set _       => ok (.bool .anyBool)
   | .like _, .string       => ok (.bool .anyBool)
   | .is ety₁, .entity ety₂ => ok (.bool (if ety₁ = ety₂ then .tt else .ff))
   | _, _                   => err (.unexpectedType ty)

cedar-lean/CedarProto/Expr.lean

@@ -291,6 +291,7 @@ namespace Proto.ExprKind.UnaryApp
 inductive Op where
   | not
   | neg
+  | isEmpty
 deriving Inhabited
 
 namespace Op
@@ -299,6 +300,7 @@ def fromInt (n : Int) : Except String Op :=
   match n with
     | 0 => .ok .not
     | 1 => .ok .neg
+    | 2 => .ok .isEmpty
     | n => .error s!"Field {n} does not exist in enum"
 
 instance : Inhabited Op where
@@ -316,6 +318,7 @@ def mergeOp (result : ExprKind.UnaryApp) (x : Op) : ExprKind.UnaryApp :=
   | .unaryApp _ expr => match x with
     | .not => .unaryApp .not expr
     | .neg => .unaryApp .neg expr
+    | .isEmpty => .unaryApp .isEmpty expr
   | _ => panic!("Expected ExprKind.UnaryApp to be of constructor .unaryApp")
 
 @[inline]

cedar-lean/DiffTest/Parser.lean

@@ -86,6 +86,7 @@ def jsonToUnaryOp (json : Lean.Json) : ParseResult UnaryOp := do
   match op with
   | "Not" => .ok .not
   | "Neg" => .ok .neg
+  | "IsEmpty" => .ok .isEmpty
   | op => .error s!"jsonToUnaryOp: unknown operator {op}"
 
 def jsonToPatElem (json : Lean.Json) : ParseResult PatElem := do

cedar-policy-generators/src/expr.rs

@@ -150,6 +150,9 @@ impl<'a> ExprGenerator<'a> {
                         self.generate_expr(max_depth - 1, u)?,
                         self.generate_expr(max_depth - 1, u)?,
                     )),
+                    1 => Ok(ast::Expr::is_empty(
+                        self.generate_expr(max_depth - 1, u)?,
+                    )),
                     2 => {
                         if self.settings.enable_like {
                             Ok(ast::Expr::like(
@@ -490,6 +493,14 @@ impl<'a> ExprGenerator<'a> {
                                 u,
                             )?,
                         )),
+                        // isEmpty()
+                        1 => Ok(ast::Expr::is_empty(
+                            self.generate_expr_for_type(
+                                &Type::set_of(u.arbitrary()?),
+                                max_depth - 1,
+                                u,
+                            )?,
+                        )),
                         // like
                         2 => {
                             if self.settings.enable_like {