fix the last panic

Signed-off-by: Craig Disselkoen <[email protected]>
cedar-policy · Nov 25, 2024 · 5259003 · 5259003
1 parent f69c70f
commit 5259003
Show file tree

Hide file tree

Showing 9 changed files with 29 additions and 28 deletions.
diff --git a/cedar-lean/Cedar/Spec/Template.lean b/cedar-lean/Cedar/Spec/Template.lean
@@ -72,40 +72,41 @@ structure TemplateLinkedPolicy where
   id : PolicyID
   templateId : TemplateID
   slotEnv : SlotEnv
+deriving Repr
 
 abbrev TemplateLinkedPolicies := List TemplateLinkedPolicy
 
-def EntityUIDOrSlot.link? (slotEnv : SlotEnv) : EntityUIDOrSlot → Option EntityUID
-  | entityUID entity => .some entity
-  | slot id => slotEnv.find? id
+def EntityUIDOrSlot.link? (slotEnv : SlotEnv) : EntityUIDOrSlot → Except String EntityUID
+  | entityUID entity => .ok entity
+  | slot id => slotEnv.findOrErr id s!"missing binding for slot {id}"
 
-def ScopeTemplate.link? (slotEnv : SlotEnv) : ScopeTemplate → Option Scope
-  | .any => .some .any
+def ScopeTemplate.link? (slotEnv : SlotEnv) : ScopeTemplate → Except String Scope
+  | .any => .ok .any
   | .eq entityOrSlot => do
     let entity ← entityOrSlot.link? slotEnv
-    .some (.eq entity)
+    .ok (.eq entity)
   | .mem entityOrSlot => do
     let entity ← entityOrSlot.link? slotEnv
-    .some (.mem entity)
-  | .is ety => .some (.is ety)
+    .ok (.mem entity)
+  | .is ety => .ok (.is ety)
   | .isMem ety entityOrSlot => do
     let entity ← entityOrSlot.link? slotEnv
-    .some (.isMem ety entity)
+    .ok (.isMem ety entity)
 
-def PrincipalScopeTemplate.link? (slotEnv : SlotEnv) : PrincipalScopeTemplate → Option PrincipalScope
+def PrincipalScopeTemplate.link? (slotEnv : SlotEnv) : PrincipalScopeTemplate → Except String PrincipalScope
   | .principalScope s => do
     let s ← s.link? slotEnv
-    .some (.principalScope s)
+    .ok (.principalScope s)
 
-def ResourceScopeTemplate.link? (slotEnv : SlotEnv) : ResourceScopeTemplate → Option ResourceScope
+def ResourceScopeTemplate.link? (slotEnv : SlotEnv) : ResourceScopeTemplate → Except String ResourceScope
   | .resourceScope s => do
     let s ← s.link? slotEnv
-    .some (.resourceScope s)
+    .ok (.resourceScope s)
 
-def Template.link? (template : Template) (id : PolicyID) (slotEnv : SlotEnv) : Option Policy := do
+def Template.link? (template : Template) (id : PolicyID) (slotEnv : SlotEnv) : Except String Policy := do
   let principalScope ← template.principalScope.link? slotEnv
   let resourceScope ← template.resourceScope.link? slotEnv
-  .some {
+  .ok {
     id := id,
     effect := template.effect,
     principalScope := principalScope,

diff --git a/cedar-lean/CedarProto/LiteralPolicy.lean b/cedar-lean/CedarProto/LiteralPolicy.lean
@@ -47,13 +47,13 @@ def mergeTemplateId (result : TemplateLinkedPolicy) (x : String) : TemplateLinke
 @[inline]
 def mergePrincipalEuid (result : TemplateLinkedPolicy) (x : EntityUID) : TemplateLinkedPolicy :=
   {result with
-    slotEnv := Cedar.Data.Map.mk (("principal", x) :: result.slotEnv.kvs)
+    slotEnv := Cedar.Data.Map.mk (("?principal", x) :: result.slotEnv.kvs)
   }
 
 @[inline]
 def mergeResourceEuid (result : TemplateLinkedPolicy) (x : EntityUID) : TemplateLinkedPolicy :=
   {result with
-    slotEnv := Cedar.Data.Map.mk (("resource", x) :: result.slotEnv.kvs)
+    slotEnv := Cedar.Data.Map.mk (("?resource", x) :: result.slotEnv.kvs)
   }
 
 @[inline]

diff --git a/cedar-lean/CedarProto/LiteralPolicySet.lean b/cedar-lean/CedarProto/LiteralPolicySet.lean
@@ -77,8 +77,8 @@ def fromLiteralPolicySet (x : LiteralPolicySet) : Policies :=
   let templates := Cedar.Data.Map.make x.templates.toList
   let links := x.links.map (λ ⟨id, p⟩ => (p.mergeId id).mkWf)
   match link? templates links.toList with
-  | .some policies => policies
-  | .none => panic!("fromLiteralPolicySet: failed to link templates")
+  | .ok policies => policies
+  | .error e => panic!(s!"fromLiteralPolicySet: failed to link templates: {e}\n  templates: {repr templates}\n  links: {repr links.toList}}")
 
 @[inline]
 private def merge (x y : Policies) : Policies :=

diff --git a/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/record.protodata
@@ -1,10 +1,10 @@
 
 WzU
-)
-eggs!
-
-{ ham: 3, eggs: 7 }
 (
 ham!
 
-{ ham: 3, eggs: 7 }{ ham: 3, eggs: 7 }
+{ ham: 3, eggs: 7 }
+)
+eggs!
+
+{ ham: 3, eggs: 7 }{ ham: 3, eggs: 7 }
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata
@@ -1,8 +1,8 @@
 #!
 
-
-ham
-
 
 eggs
-
+
+
+ham
+