Updates to Lean validator spec

cedar-drt/fuzz/src/lib.rs

@@ -177,47 +177,50 @@ pub fn run_val_test(
 
     let definitional_res = custom_impl.validate(&schema, policies, mode);
 
-    match definitional_res {
-        Err(err) => {
-            // TODO(#175): For now, ignore cases where the Lean code returned an error due to
-            // an unknown extension function.
-            if !err.contains("jsonToExtFun: unknown extension function") {
-                panic!(
-                    "Unexpected parse error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}",
-                    &policies, schema
-                );
-            }
-        }
-        Ok(definitional_res) => {
-            // TODO:(#126) Temporary fix to ignore a known mismatch between the spec and `cedar-policy`.
-            // The issue is that the `cedar-policy` will always return an error for an
-            // unrecognized entity or action, even if that part of the expression
-            // should be excluded from typechecking (e.g., `true || Undefined::"foo"`
-            // should be well typed due to short-circuiting).
-            if rust_res.validation_errors().any(|e| {
-                matches!(
-                    e.error_kind(),
-                    ValidationErrorKind::UnrecognizedEntityType(_)
-                        | ValidationErrorKind::UnrecognizedActionId(_)
-                )
-            }) {
-                return;
+    // If `cedar-policy` does not return an error, then the spec should not return an error.
+    // This implies type soundness of the `cedar-policy` validator since type soundness of the
+    // spec is formally proven.
+    //
+    // In particular, we have proven that if the spec validator does not return an error (B),
+    // then there are no authorization-time errors modulo some restrictions (C). So (B) ==> (C).
+    // DRT checks that if the `cedar-policy` validator does not return an error (A), then neither
+    // does the spec validator (B). So (A) ==> (B). By transitivity then, (A) ==> (C).
+
+    if rust_res.validation_passed() {
+        match definitional_res {
+            Err(err) => {
+                // TODO(#175): For now, ignore cases where the Lean code returned an error due to
+                // an unknown extension function.
+                if !err.contains("jsonToExtFun: unknown extension function") {
+                    panic!(
+                        "Unexpected parse error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}",
+                        &policies, schema
+                    );
+                }
             }
+            Ok(definitional_res) => {
+                // Even if the Rust validator succeeds, the definitional validator may
+                // return "impossiblePolicy" due to greater precision. In this case, the
+                // input policy is well-typed, although it is guaranteed to always evaluate
+                // to false.
+                if definitional_res.validation_errors == vec!["impossiblePolicy".to_string()] {
+                    return;
+                }
 
-            // The `validation_passed` decisions should match.
-            assert_eq!(
-                rust_res.validation_passed(),
-                definitional_res.validation_passed(),
-                "Mismatch for Policies:\n{}\nSchema:\n{:?}\ncedar-policy response: {:?}\nTest engine response: {:?}\n",
-                &policies,
-                schema,
-                rust_res,
-                definitional_res,
-            );
+                // But the definitional validator should not return any other error.
+                assert!(
+                    definitional_res.validation_passed(),
+                    "Mismatch for Policies:\n{}\nSchema:\n{:?}\ncedar-policy response: {:?}\nTest engine response: {:?}\n",
+                    &policies,
+                    schema,
+                    rust_res,
+                    definitional_res,
+                );
 
-            // TODO(#69): We currently don't check for a relationship between validation errors.
-            // E.g., the error reported by the definitional validator should be in the list
-            // of errors reported by the production validator, but we don't check this.
+                // TODO(#69): We currently don't check for a relationship between validation errors.
+                // E.g., the error reported by the definitional validator should be in the list
+                // of errors reported by the production validator, but we don't check this.
+            }
         }
     }
 }

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

@@ -46,8 +46,7 @@ theorem type_of_hasAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabili
         simp [h₁]
       }
     case h_2 _ _ =>
-      split at h₁
-      split at h₁ <;> try split at h₁
+      split at h₁ <;> split at h₁ <;> try split at h₁
       all_goals {
         simp [ok] at h₁
         try simp [h₁]
@@ -147,6 +146,22 @@ theorem type_of_hasAttr_is_sound_for_entities {x₁ : Expr} {a : Attr} {c₁ c
     case h₁.true.h_2 =>
       rcases (Map.not_contains_of_empty a) with _
       contradiction
+  case h_2 =>
+    simp [ok] at h₃
+    split at h₃ <;> try simp [err, hasAttrInRecord] at h₃
+    replace ⟨h₃, _⟩ := h₃
+    simp [←h₃]
+    apply InstanceOfType.instance_of_bool
+    unfold Entities.attrsOrEmpty
+    rename_i _ h₇ _ _
+    simp [EntitySchema.attrs?] at h₇
+    replace ⟨_, h₂, _⟩ := h₂
+    cases h₈ : Map.find? entities uid <;> simp
+    simp [Map.not_contains_of_empty, InstanceOfBoolType]
+    replace ⟨_, h₈, _⟩ := h₂ uid _ h₈
+    rw [h₇] at h₈
+    contradiction
+
 
 theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -185,13 +185,19 @@ def hasAttrInRecord (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities)
     else ok (.bool .anyBool) (Capabilities.singleton x a)
   | .none     => ok (.bool .ff)
 
+def actionType? (ety : EntityType) (acts: ActionSchema) : Bool :=
+  acts.keys.any (EntityUID.ty · == ety)
+
 def typeOfHasAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env : Environment) : ResultType :=
   match ty with
   | .record rty => hasAttrInRecord rty x a c true
   | .entity ety =>
     match env.ets.attrs? ety with
     | .some rty => hasAttrInRecord rty x a c false
-    | .none     => err (.unknownEntity ety)
+    | .none     =>
+      if actionType? ety env.acts
+      then ok (.bool .ff) -- action attributes not allowed
+      else err (.unknownEntity ety)
   | _           => err (.unexpectedType ty)
 
 def getAttrInRecord (ty : CedarType) (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) : ResultType :=

cedar-lean/DiffTest/Parser.lean

@@ -450,6 +450,15 @@ def invertJsonActionSchema (acts : JsonActionSchema) : ActionSchema :=
         context := v.context
       })) acts)
 
+-- Add special "unspecified" entity type with no attributes or ancestors
+def addUnspecifiedEntityType (ets : EntitySchema) : EntitySchema :=
+  let unspecifiedEntry : EntitySchemaEntry :=
+  {
+    ancestors := Set.empty
+    attrs := Map.empty
+  }
+  Map.make (ets.toList ++ [({id := "<Unspecified>", path := []}, unspecifiedEntry)])
+
 mutual
 
 partial def jsonToQualifiedCedarType (json : Lean.Json) : ParseResult (Qualified CedarType) := do
@@ -525,7 +534,7 @@ partial def jsonToSchema (json : Lean.Json) : ParseResult Schema := do
   let actionsKVs ← getJsonField json "actionIds" >>= jsonArrayToKVList
   let actions ← mapMKeysAndValues actionsKVs jsonToEuid jsonToActionSchemaEntry
   .ok {
-    ets := invertJsonEntitySchema (Map.make entityTypes),
+    ets := addUnspecifiedEntityType (invertJsonEntitySchema (Map.make entityTypes))
     acts := invertJsonActionSchema (Map.make actions)
   }