Merge remote-tracking branch 'origin/main' into update/cdisselkoen/430

cedar-dafny/def/core.dfy

@@ -155,7 +155,8 @@ module def.core {
   datatype UnaryOp =
     Not |
     Neg | MulBy(i: int) |
-    Like(p: Pattern)
+    Like(p: Pattern) |
+    Is(ety: EntityType)
 
   datatype BinaryOp =
     Eq | In |
@@ -228,13 +229,22 @@ module def.core {
     }
   }
 
-  datatype Scope = Any | Eq(entity: EntityUID) | In(entity: EntityUID)
+  datatype Scope = 
+    Any | 
+    Eq(entity: EntityUID) | 
+    In(entity: EntityUID) | 
+    Is(ety: EntityType) | 
+    IsIn(ety:EntityType, entity: EntityUID)
   {
     function toExpr(v: Var): Expr {
       match this {
         case Any   => PrimitiveLit(Primitive.Bool(true))
         case Eq(e) => BinaryApp(BinaryOp.Eq, Var(v), PrimitiveLit(Primitive.EntityUID(e)))
         case In(e) => BinaryApp(BinaryOp.In, Var(v), PrimitiveLit(Primitive.EntityUID(e)))
+        case Is(ety) => UnaryApp(UnaryOp.Is(ety), Var(v))
+        case IsIn(ety, e) => 
+          And(UnaryApp(UnaryOp.Is(ety), Var(v)),
+              BinaryApp(BinaryOp.In, Var(v), PrimitiveLit(Primitive.EntityUID(e))))
       }
     }
   }

cedar-dafny/def/engine.dfy

@@ -206,6 +206,9 @@ module def.engine {
         case Like(p) =>
           var s :- Value.asString(x);
           Ok(Value.Bool(wildcardMatch(s, p)))
+        case Is(ety) =>
+          var e :- Value.asEntity(x);
+          Ok(Value.Bool(e.ty == ety))
       }
     }
 

cedar-dafny/def/templates.dfy

@@ -126,11 +126,16 @@ module def.templates {
     }
   }
 
-  datatype ScopeTemplate = Any | Eq(entityOrSlot: EntityUIDOrSlot) | In(entityOrSlot: EntityUIDOrSlot)
+  datatype ScopeTemplate = 
+    Any | 
+    Eq(entityOrSlot: EntityUIDOrSlot) | 
+    In(entityOrSlot: EntityUIDOrSlot) |
+    Is(ety: EntityType) | 
+    IsIn(ety: EntityType, entityOrSlot: EntityUIDOrSlot)
   {
     function slotReqs(): SlotReqs {
       match this {
-        case Any => emptySlotReqs
+        case Any | Is(_) => emptySlotReqs
         case _ => entityOrSlot.slotReqs()
       }
     }
@@ -191,6 +196,8 @@ module def.templates {
         case Any => Scope.Any
         case In(e) => Scope.In(linkEntityUIDOrSlot(e))
         case Eq(e) => Scope.Eq(linkEntityUIDOrSlot(e))
+        case Is(ety) => Scope.Is(ety)
+        case IsIn(ety,e) => Scope.IsIn(ety,linkEntityUIDOrSlot(e))
       }
     }
 

cedar-dafny/difftest/main.dfy

@@ -193,6 +193,10 @@ module difftest.main {
         var expr :- deserializeField(body, "expr", exprFromProdJsonRec);
         var pat :- deserializeField(body, "pattern", patternFromProdJson);
         Ok(UnaryApp(Like(pat), expr))
+      case "Is" =>
+        var expr :- deserializeField(body, "expr", exprFromProdJsonRec);
+        var ety :- deserializeField(body, "entity_type", nameFromProdJson);
+        Ok(UnaryApp(UnaryOp.Is(EntityType(ety)), expr))
       case "Set" =>
         var exprs :- deserializeSeq(body, exprFromProdJsonRec);
         Ok(Expr.Set(exprs))
@@ -245,7 +249,13 @@ module difftest.main {
         map[
           "Any" := _ => Ok(ScopeTemplate.Any),
           "In" := bodyDeserializer(entityUIDOrSlotFromProdJson, e => Ok(ScopeTemplate.In(e))),
-          "Eq" := bodyDeserializer(entityUIDOrSlotFromProdJson, e => Ok(ScopeTemplate.Eq(e)))
+          "Eq" := bodyDeserializer(entityUIDOrSlotFromProdJson, e => Ok(ScopeTemplate.Eq(e))),
+          "Is" := bodyDeserializer(nameFromProdJson, ety => Ok(ScopeTemplate.Is(EntityType(ety)))),
+          "IsIn" := tupleDeserializer2Elts(
+                      nameFromProdJson,
+                      entityUIDOrSlotFromProdJson,
+                      (ety, e) => Ok(ScopeTemplate.IsIn(EntityType(ety),e))
+                    )
         ])
   }
 

cedar-dafny/thm/pslicing.dfy

@@ -134,8 +134,8 @@ module pslicing {
 
   function headBasedTarget(p: Policy): Target {
     Target(
-      if p.principalScope.scope.Any? then None else Some(p.principalScope.scope.entity),
-      if p.resourceScope.scope.Any? then None else Some(p.resourceScope.scope.entity))
+      if p.principalScope.scope.Any? || p.principalScope.scope.Is? then None else Some(p.principalScope.scope.entity),
+      if p.resourceScope.scope.Any? || p.resourceScope.scope.Is? then None else Some(p.resourceScope.scope.entity))
   }
 
   function headBasedPolicySlice(request: Request, store: Store): PolicyStore {

cedar-dafny/validation/thm/model.dfy

@@ -715,6 +715,35 @@ module validation.thm.model {
     ensures IsSafe(r,s,UnaryApp(Like(p),e),Type.Bool(AnyBool))
   {
     reveal IsSafe();
+  }      
+
+  lemma IsOpSafe(r: Request, s: EntityStore, e: Expr, ety: EntityType)
+    requires IsSafe(r,s,e,Type.Entity(AnyEntity))
+    ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(AnyBool))
+  {
+    reveal IsSafe();
+  }
+
+  lemma IsOpSafeTrue(r: Request, s: EntityStore, e: Expr, ety: EntityType, lub: EntityLUB)
+    requires IsSafe(r,s,e,Type.Entity(lub))
+    requires lub.EntityLUB?
+    requires ety in lub.tys && |lub.tys| == 1
+    ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(True))
+  {
+    assert lub.tys == {ety} by {
+      def.util.EntityTypeLeqIsTotalOrder();
+      var _ := def.util.SetToSortedSeq(lub.tys,def.util.EntityTypeLeq);
+    }
+    reveal IsSafe();
+  }
+
+  lemma IsOpSafeFalse(r: Request, s: EntityStore, e: Expr, ety: EntityType, lub: EntityLUB)
+    requires IsSafe(r,s,e,Type.Entity(lub))
+    requires lub.EntityLUB?
+    requires ety !in lub.tys
+    ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(False))
+  {
+    reveal IsSafe();
   }
 
   lemma SetConstrSafe(r: Request, s: EntityStore, es: seq<Expr>, t: Type)

cedar-dafny/validation/thm/soundness.dfy

@@ -663,6 +663,57 @@ module validation.thm.soundness {
       }
     }
 
+    lemma SoundIs(e: Expr, ety: EntityType, t: Type, effs: Effects)
+      decreases UnaryApp(UnaryOp.Is(ety),e) , 0
+      requires WellFormedRequestAndStore()
+      requires EffectsInvariant(effs)
+      requires Typesafe(UnaryApp(UnaryOp.Is(ety),e),effs,t)
+      ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t)
+      ensures getEffects(UnaryApp(UnaryOp.Is(ety),e),effs) == Effects.empty()
+    {
+      var t' :| getType(UnaryApp(UnaryOp.Is(ety),e),effs) == t' && subty(t',t,ValidationMode.Permissive);
+      assert TC.inferIs(ety,e,effs) == types.Ok(t');
+
+      assert TC.ensureEntityType(e,effs).Ok?;
+      var t1 := getType(e,effs);
+      assert t1.Entity?;
+
+      assert IsSafe(r,s,e,t1) by { Sound(e,t1,effs); }
+      match t1 {
+        case Entity(AnyEntity) =>
+          assert t' == Type.Bool(AnyBool);
+          assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(AnyBool)) by {
+            IsOpSafe(r,s,e,ety);
+          }
+        case Entity(EntityLUB(tys)) =>
+          if ety !in tys {
+            assert t' == Type.Bool(False);
+            assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t') by { 
+              IsOpSafeFalse(r,s,e,ety,EntityLUB(tys)); 
+            }
+            assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t) by {
+              SubtyCompat(t',t);
+              SemSubtyTransport(r,s,UnaryApp(UnaryOp.Is(ety),e),t',t);
+            }
+          } else if ety in tys && |tys| == 1 {
+            assert t' == Type.Bool(True);
+            assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t') by { 
+              IsOpSafeTrue(r,s,e,ety,EntityLUB(tys)); 
+            }
+            assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t) by {
+              SubtyCompat(t',t);
+              SemSubtyTransport(r,s,UnaryApp(UnaryOp.Is(ety),e),t',t);
+            }
+          } else {
+            assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(AnyBool)) by {
+              assert subty(t1,Type.Entity(AnyEntity),ValidationMode.Permissive);
+              assert IsSafe(r,s,e,Type.Entity(AnyEntity)) by { Sound(e,Type.Entity(AnyEntity),effs); }
+              IsOpSafe(r,s,e,ety);
+            }
+          }
+      }
+    }
+
     const unspecifiedEntityType := Type.Entity(EntityLUB({EntityType.UNSPECIFIED}))
 
     // Take advantage of the fact that in the current implementation, an
@@ -1439,6 +1490,7 @@ module validation.thm.soundness {
         case UnaryApp(Neg,e') => SoundNeg(e',t,effs);
         case UnaryApp(MulBy(i),e') => SoundMulBy(i,e',t,effs);
         case UnaryApp(Like(p),e') => SoundLike(e',p,t,effs);
+        case UnaryApp(Is(ety),e') => SoundIs(e',ety,t,effs);
         case BinaryApp(Eq,e1,e2) => SoundEq(e1,e2,t,effs);
         case BinaryApp(Less,e1,e2) => SoundIneq(Less,e1,e2,t,effs);
         case BinaryApp(LessEq,e1,e2) => SoundIneq(BinaryOp.LessEq,e1,e2,t,effs);

cedar-dafny/validation/thm/strict_inf_strict.dfy

@@ -152,6 +152,7 @@ module validation.thm.strict_inf_strict {
         case UnaryApp(Neg,e') =>
         case UnaryApp(MulBy(i),e') =>
         case UnaryApp(Like(p),e') =>
+        case UnaryApp(Is(ety),e') =>
         case BinaryApp(Eq,e1,e2) =>
         case BinaryApp(Less,e1,e2) =>
         case BinaryApp(LessEq,e1,e2) =>

cedar-dafny/validation/thm/strict_soundness.dfy

@@ -121,6 +121,17 @@ module validation.thm.strict_soundness {
       }
     }
 
+    lemma StrictIs(ety: EntityType, e: Expr, effs: Effects)
+      decreases UnaryApp(UnaryOp.Is(ety), e), 0
+      requires S_TC.infer(UnaryApp(UnaryOp.Is(ety), e), effs).Ok?
+      ensures P_TC.infer(UnaryApp(UnaryOp.Is(ety), e), effs) == S_TC.infer(UnaryApp(UnaryOp.Is(ety), e), effs)
+    {
+      assert S_TC.ensureEntityType(e, effs).Ok?;
+      assert P_TC.ensureEntityType(e, effs) == S_TC.ensureEntityType(e, effs) by { 
+        StrictTypecheckingIsStrict(e, effs); 
+      }
+    }
+
     lemma StrictArith2Ineq(o: BinaryOp, e1: Expr, e2: Expr, effs: Effects)
       decreases BinaryApp(o, e1, e2), 0
       requires o.Add? || o.Sub? || o.Less? || o.LessEq?
@@ -361,6 +372,7 @@ module validation.thm.strict_soundness {
         case UnaryApp(Neg,e') => StrictArith1(Neg, e', effs);
         case UnaryApp(MulBy(i),e') => StrictArith1(MulBy(i), e', effs);
         case UnaryApp(Like(p),e') => StrictLike(p, e', effs);
+        case UnaryApp(Is(ety),e') => StrictIs(ety, e', effs);
         case BinaryApp(Eq,e1,e2) => StrictEq(e1, e2, effs);
         case BinaryApp(Less,e1,e2) => StrictArith2Ineq(Less, e1, e2, effs);
         case BinaryApp(LessEq,e1,e2) => StrictArith2Ineq(LessEq, e1, e2, effs);

cedar-dafny/validation/typechecker.dfy

@@ -557,6 +557,21 @@ module validation.typechecker {
       Ok(Type.Bool(AnyBool))
     }
 
+    function inferIs(ety: EntityType, e: Expr, effs: Effects): Result<Type>
+      decreases UnaryApp(UnaryOp.Is(ety),e) , 0
+    {
+      var elub :- ensureEntityType(e,effs);
+      match elub {
+        case AnyEntity => Ok(Type.Bool(AnyBool))
+        case EntityLUB(tys) =>
+          if ety !in tys
+          then Ok(Type.Bool(False))
+          else if ety in tys && |tys| == 1
+          then Ok(Type.Bool(True))
+          else Ok(Type.Bool(AnyBool))
+      }
+    }
+
     function inferArith1(ghost op: UnaryOp, e: Expr, effs: Effects): Result<Type>
       requires op.Neg? || op.MulBy?
       decreases UnaryApp(op,e) , 0
@@ -667,6 +682,7 @@ module validation.typechecker {
         case UnaryApp(Neg,e1) => wrap(inferArith1(Neg,e1,effs))
         case UnaryApp(MulBy(i),e1) => wrap(inferArith1(MulBy(i),e1,effs))
         case UnaryApp(Like(p),e1) => wrap(inferLike(p,e1,effs))
+        case UnaryApp(Is(ety),e1) => wrap(inferIs(ety,e1,effs))
         case BinaryApp(Eq,e1,e2) => wrap(inferEq(e1,e2,effs))
         case BinaryApp(Less,e1,e2) => wrap(inferIneq(Less,e1,e2,effs))
         case BinaryApp(LessEq,e1,e2) => wrap(inferIneq(LessEq,e1,e2,effs))

cedar-policy-generators/src/policy.rs

@@ -292,7 +292,7 @@ impl PrincipalOrResourceConstraint {
                     1 => Ok(Self::IsTypeInSlot(hierarchy.arbitrary_entity_type(u)?))
                 )
             } else {
-                // 32% Eq, 32% In (16% with and without Is), 32% Is (16% with and without In)
+                // 32% Eq, 16% In, 16% Is, 16% IsIn
                 let uid = hierarchy.arbitrary_uid(u)?;
                 gen!(u,
                     2 => Ok(Self::Eq(uid)),

cedar-policy-generators/src/schema.rs

@@ -1037,15 +1037,22 @@ impl Schema {
         hierarchy: &Hierarchy,
         u: &mut Unstructured<'_>,
     ) -> Result<PrincipalOrResourceConstraint> {
-        // 20% of the time, NoConstraint; 40%, Eq; 40%, In
-        gen!(u,
-        2 => Ok(PrincipalOrResourceConstraint::NoConstraint),
-        4 => Ok(PrincipalOrResourceConstraint::Eq(
-            self.exprgenerator(Some(hierarchy)).arbitrary_principal_uid(u)?,
-        )),
-        4 => Ok(PrincipalOrResourceConstraint::In(
-            self.exprgenerator(Some(hierarchy)).arbitrary_principal_uid(u)?,
-        )))
+        // 20% of the time, NoConstraint
+        if u.ratio(1, 5)? {
+            Ok(PrincipalOrResourceConstraint::NoConstraint)
+        } else {
+            // 32% Eq, 16% In, 16% Is, 16% IsIn
+            let uid = self
+                .exprgenerator(Some(hierarchy))
+                .arbitrary_principal_uid(u)?;
+            let ety = u.choose(self.entity_types())?.clone();
+            gen!(u,
+                2 => Ok(PrincipalOrResourceConstraint::Eq(uid)),
+                1 => Ok(PrincipalOrResourceConstraint::In(uid)),
+                1 => Ok(PrincipalOrResourceConstraint::IsType(ety)),
+                1 => Ok(PrincipalOrResourceConstraint::IsTypeIn(ety, uid))
+            )
+        }
     }
     fn arbitrary_principal_constraint_size_hint(depth: usize) -> (usize, Option<usize>) {
         arbitrary::size_hint::and(
@@ -1063,15 +1070,22 @@ impl Schema {
         hierarchy: &Hierarchy,
         u: &mut Unstructured<'_>,
     ) -> Result<PrincipalOrResourceConstraint> {
-        // 20% of the time, NoConstraint; 40%, Eq; 40%, In
-        gen!(u,
-        2 => Ok(PrincipalOrResourceConstraint::NoConstraint),
-        4 => Ok(PrincipalOrResourceConstraint::Eq(
-            self.exprgenerator(Some(hierarchy)).arbitrary_resource_uid(u)?,
-        )),
-        4 => Ok(PrincipalOrResourceConstraint::In(
-            self.exprgenerator(Some(hierarchy)).arbitrary_resource_uid(u)?,
-        )))
+        // 20% of the time, NoConstraint
+        if u.ratio(1, 5)? {
+            Ok(PrincipalOrResourceConstraint::NoConstraint)
+        } else {
+            // 32% Eq, 16% In, 16% Is, 16% IsIn
+            let uid = self
+                .exprgenerator(Some(hierarchy))
+                .arbitrary_resource_uid(u)?;
+            let ety = u.choose(self.entity_types())?.clone();
+            gen!(u,
+                2 => Ok(PrincipalOrResourceConstraint::Eq(uid)),
+                1 => Ok(PrincipalOrResourceConstraint::In(uid)),
+                1 => Ok(PrincipalOrResourceConstraint::IsType(ety)),
+                1 => Ok(PrincipalOrResourceConstraint::IsTypeIn(ety, uid))
+            )
+        }
     }
     fn arbitrary_resource_constraint_size_hint(depth: usize) -> (usize, Option<usize>) {
         arbitrary::size_hint::and(