From 6d6727f21eef9b5e83b9a2bb5c0ef203a826285e Mon Sep 17 00:00:00 2001 From: John Kastner Date: Fri, 23 Aug 2024 20:51:22 +0000 Subject: [PATCH] instanceOfType attribute map Signed-off-by: John Kastner --- cedar-lean/Cedar/Validation/RequestEntityValidator.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/cedar-lean/Cedar/Validation/RequestEntityValidator.lean b/cedar-lean/Cedar/Validation/RequestEntityValidator.lean index 76fd25320..739522b52 100644 --- a/cedar-lean/Cedar/Validation/RequestEntityValidator.lean +++ b/cedar-lean/Cedar/Validation/RequestEntityValidator.lean @@ -65,6 +65,8 @@ def instanceOfType (v : Value) (ty : CedarType) : Bool := | .some qty => instanceOfType v qty.getType | _ => true))) && rty.keys.all (requiredAttributePresent r rty) + | .record r, .attribute_map aty => + (r.kvs.attach₂.all (λ ⟨(_, v), _⟩ => instanceOfType v aty)) | .ext x, .ext xty => instanceOfExtType x xty | _, _ => false termination_by v @@ -73,7 +75,7 @@ def instanceOfType (v : Value) (ty : CedarType) : Bool := case _ h₁ => have := Set.sizeOf_lt_of_mem h₁ omega - case _ h₁ => + case _ h₁ | _ h₁ => cases r simp only [Map.kvs] at h₁ simp only [Map.mk.sizeOf_spec]