Fix protobuf parsing for unrecognized extension functions (#517)

Signed-off-by: John Kastner <[email protected]>

Author: john-h-kastner-aws

cedar-drt/fuzz/src/lib.rs

@@ -84,7 +84,7 @@ pub fn run_pe_test(
         TestResult::Failure(err) => {
             // TODO(#175): Ignore cases where the definitional code returned an error due to
             // an unknown extension function.
-            if err.contains("jsonToExtFun: unknown extension function") {
+            if err.contains("unknown extension function") {
                 return;
             }
             // No other errors are expected
@@ -139,7 +139,7 @@ pub fn run_eval_test(
         TestResult::Failure(err) => {
             // TODO(#175): Ignore cases where the definitional code returned an error due to
             // an unknown extension function.
-            if err.contains("jsonToExtFun: unknown extension function") {
+            if err.contains("unknown extension function") {
                 return;
             }
             // No other errors are expected
@@ -176,7 +176,7 @@ pub fn run_auth_test(
         TestResult::Failure(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") {
+            if err.contains("unknown extension function") {
                 rust_res
             } else {
                 panic!(
@@ -249,7 +249,9 @@ pub fn run_val_test(
         TestResult::Failure(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") {
+            if !err.contains("unknown extension function")
+                && !err.contains("unknown extension type")
+            {
                 panic!(
                     "Unexpected error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}",
                     &policies, schema

cedar-drt/src/lean_impl.rs

@@ -38,7 +38,7 @@ use lean_sys::{
     lean_alloc_sarray, lean_dec, lean_dec_ref, lean_finalize_thread,
     lean_initialize_runtime_module_locked, lean_initialize_thread, lean_io_mark_end_initialization,
     lean_io_mk_world, lean_io_result_is_ok, lean_io_result_show_error, lean_sarray_object,
-    lean_string_cstr,
+    lean_set_exit_on_panic, lean_string_cstr,
 };
 use log::info;
 use miette::miette;
@@ -167,6 +167,8 @@ impl LeanDefinitionalEngine {
                     panic!("Failed to initialize Lean");
                 }
                 lean_io_mark_end_initialization();
+                // If we don't explicitly set this, Lean does not abort after hitting a panic
+                lean_set_exit_on_panic(true);
             };
         });
         unsafe { lean_initialize_thread() };

cedar-lean/CedarProto/ActionConstraint.lean

@@ -73,7 +73,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope.In) := do
   match t.fieldNum with
     | 1 =>
       let x : Repeated EntityUID ← Field.guardedParse t
-      pure (mergeEuids · x)
+      pure (pure $ mergeEuids · x)
     | _ =>
       t.wireType.skip
       pure ignore
@@ -105,7 +105,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope.Eq) := do
   match t.fieldNum with
     | 1 =>
       let x : EntityUID ← Field.guardedParse t
-      pure (mergeEuid · x)
+      pure (pure $ mergeEuid · x)
     | _ =>
       t.wireType.skip
       pure ignore
@@ -157,13 +157,13 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope) := do
   match t.fieldNum with
     | 1 =>
       let x : Proto.ActionScope.Ty ← Field.guardedParse t
-      pure (mergeTy · x)
+      pure (pure $ mergeTy · x)
     | 2 =>
       let x : Proto.ActionScope.In ← Field.guardedParse t
-      pure (mergeIn · x)
+      pure (pure $ mergeIn · x)
     | 3 =>
       let x : Proto.ActionScope.Eq ← Field.guardedParse t
-      pure (mergeEq · x)
+      pure (pure $ mergeEq · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/AuthorizationRequest.lean

@@ -62,13 +62,13 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn AuthorizationRequest) := do
   match t.fieldNum with
     | 1 =>
       let x : Request ← Field.guardedParse t
-      pure (mergeRequest · x)
+      pure (pure $ mergeRequest · x)
     | 2 =>
       let x : Policies ← Field.guardedParse t
-      pure (mergePolicies · x)
+      pure (pure $ mergePolicies · x)
     | 3 =>
       let x : Entities ← Field.guardedParse t
-      pure (mergeEntities · x)
+      pure (pure $ mergeEntities · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/Context.lean

@@ -48,7 +48,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn Context) := do
   match t.fieldNum with
     | 1 =>
       let x : Value ← Field.guardedParse t
-      pure (mergeValue · x)
+      pure (pure $ mergeValue · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/Entities.lean

@@ -51,7 +51,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntitiesProto) := do
   match t.fieldNum with
     | 1 =>
       let x : Repeated EntityProto ← Field.guardedParse t
-      pure (mergeEntities · x)
+      pure (pure $ mergeEntities · x)
     -- Ignoring 3 | mode
     | _ =>
       t.wireType.skip

cedar-lean/CedarProto/Entity.lean

@@ -79,16 +79,16 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntityProto) := do
   match t.fieldNum with
     | 1 =>
       let x : EntityUID ← Field.guardedParse t
-      pure (mergeUid · x)
+      pure (pure $ mergeUid · x)
     | 2 =>
       let x : Proto.Map String Value ← Field.guardedParse t
-      pure (mergeAttrs · x)
+      pure (pure $ mergeAttrs · x)
     | 3 =>
       let x : Repeated EntityUID ← Field.guardedParse t
-      pure (mergeAncestors · x)
+      pure (pure $ mergeAncestors · x)
     | 4 =>
       let x : Proto.Map String Value ← Field.guardedParse t
-      pure (mergeTags · x)
+      pure (pure $ mergeTags · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/EntityReference.lean

@@ -74,10 +74,10 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUIDOrSlot) := do
   match t.fieldNum with
     | 1 =>
       let x : Proto.EntityReferenceType ← Field.guardedParse t
-      pure (mergeTy · x)
+      pure (pure $ mergeTy · x)
     | 2 =>
       let x : EntityUID ← Field.guardedParse t
-      pure (mergeEuid · x)
+      pure (pure $ mergeEuid · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/EntityType.lean

@@ -47,7 +47,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntityTypeProto) := do
   match t.fieldNum with
     | 1 =>
       let x : Name ← Field.guardedParse t
-      pure (mergeName · x)
+      pure (pure $ mergeName · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/EntityUID.lean

@@ -55,10 +55,10 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUID) := do
   match t.fieldNum with
     | 1 =>
       let x : EntityTypeProto ← Field.guardedParse t
-      pure (mergeTy · x)
+      pure (pure $ mergeTy · x)
     | 2 =>
       let x : String ← Field.guardedParse t
-      pure (mergeEid · x)
+      pure (pure $ mergeEid · x)
     | _ =>
       t.wireType.skip
       pure ignore

cedar-lean/CedarProto/EntityUIDEntry.lean

@@ -42,7 +42,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUIDEntry) := do
   match t.fieldNum with
     | 1 =>
       let x : EntityUID ← Field.guardedParse t
-      pure (mergeEuid · x)
+      pure (pure $ mergeEuid · x)
     | _ =>
       t.wireType.skip
       pure ignore