move things around

cedar-lean/Cedar/Thm/Authorization/Authorizer.lean

@@ -16,9 +16,9 @@
 
 import Cedar.Spec
 import Cedar.Spec.Authorizer
+import Cedar.Thm.Authorization.Basic
 import Cedar.Thm.Authorization.Evaluator
 import Cedar.Thm.Core.LT
-import Cedar.Thm.SlicingDefs
 import Cedar.Thm.Validation.Typechecker.BinaryApp -- mapM'_asEntityUID_eq_entities
 
 /-!

cedar-lean/Cedar/Thm/Authorization/Basic.lean

@@ -0,0 +1,68 @@
+
+import Cedar.Spec
+
+namespace Cedar.Thm
+
+open Cedar.Spec
+
+/--
+A policy slice is a subset of a collection of policies.  This slice is sound for
+a given request and entities if every policy in the collection that is not in
+the slice is also not satisfied with respect to the request and entities, and
+doesn't produce an error when evaluated.
+-/
+def IsSoundPolicySlice (req : Request) (entities : Entities) (slice policies : Policies) : Prop :=
+  slice ⊆ policies ∧
+  ∀ policy ∈ policies,
+    policy ∉ slice →
+    ¬ satisfied policy req entities ∧ ¬ hasError policy req entities
+
+/--
+A policy bound consists of optional `principal` and `resource` entities.
+-/
+structure PolicyBound where
+  principalBound : Option EntityUID
+  resourceBound  : Option EntityUID
+
+def inSomeOrNone (uid : EntityUID) (opt : Option EntityUID) (entities : Entities) : Bool :=
+  match opt with
+  | .some uid' => inₑ uid uid' entities
+  | .none      => true
+
+/--
+A bound is satisfied by a request and store if the request principal and
+resource fields are descendents of the corresponding bound fields (or if those
+bound fields are `none`).
+-/
+def satisfiedBound (bound : PolicyBound) (request : Request) (entities : Entities) : Bool :=
+  inSomeOrNone request.principal bound.principalBound entities ∧
+  inSomeOrNone request.resource bound.resourceBound entities
+
+/--
+A bound is sound for a given policy if the bound is satisfied for every request
+and entities for which the policy is satisfied or for which the policy produces
+an error.
+-/
+def IsSoundPolicyBound (bound : PolicyBound) (policy : Policy) : Prop :=
+  ∀ (request : Request) (entities : Entities),
+  (satisfied policy request entities →
+  satisfiedBound bound request entities) ∧
+  (hasError policy request entities →
+  satisfiedBound bound request entities)
+
+/--
+A bound analysis takes as input a policy and returns a PolicyBound.
+-/
+abbrev BoundAnalysis := Policy → PolicyBound
+
+def BoundAnalysis.slice (ba : BoundAnalysis) (request : Request) (entities : Entities) (policies : Policies) : Policies :=
+  policies.filter (fun policy => satisfiedBound (ba policy) request entities)
+
+/--
+A bound analysis is sound if it produces sound bounds for all policies.
+-/
+def IsSoundBoundAnalysis (ba : BoundAnalysis) : Prop :=
+  ∀ (policy : Policy), IsSoundPolicyBound (ba policy) policy
+
+
+end Cedar.Thm

cedar-lean/Cedar/Thm/Slicing.lean

@@ -16,7 +16,7 @@
 
 import Cedar.Spec
 import Cedar.Thm.Authorization.Authorizer
-import Cedar.Thm.SlicingDefs
+import Cedar.Thm.Authorization.Basic
 
 /-!
 This file defines what it means for a policy slice to be sound.
@@ -57,53 +57,6 @@ theorem isAuthorized_eq_for_sound_policy_slice (req : Request) (entities : Entit
     errorPolicies_eq_for_sound_policy_slice req entities slice policies h₀
   simp [isAuthorized, hf, hp, he]
 
-/--
-A policy bound consists of optional `principal` and `resource` entities.
--/
-structure PolicyBound where
-  principalBound : Option EntityUID
-  resourceBound  : Option EntityUID
-
-def inSomeOrNone (uid : EntityUID) (opt : Option EntityUID) (entities : Entities) : Bool :=
-  match opt with
-  | .some uid' => inₑ uid uid' entities
-  | .none      => true
-
-/--
-A bound is satisfied by a request and store if the request principal and
-resource fields are descendents of the corresponding bound fields (or if those
-bound fields are `none`).
--/
-def satisfiedBound (bound : PolicyBound) (request : Request) (entities : Entities) : Bool :=
-  inSomeOrNone request.principal bound.principalBound entities ∧
-  inSomeOrNone request.resource bound.resourceBound entities
-
-/--
-A bound is sound for a given policy if the bound is satisfied for every request
-and entities for which the policy is satisfied or for which the policy produces
-an error.
--/
-def IsSoundPolicyBound (bound : PolicyBound) (policy : Policy) : Prop :=
-  ∀ (request : Request) (entities : Entities),
-  (satisfied policy request entities →
-  satisfiedBound bound request entities) ∧
-  (hasError policy request entities →
-  satisfiedBound bound request entities)
-
-/--
-A bound analysis takes as input a policy and returns a PolicyBound.
--/
-abbrev BoundAnalysis := Policy → PolicyBound
-
-def BoundAnalysis.slice (ba : BoundAnalysis) (request : Request) (entities : Entities) (policies : Policies) : Policies :=
-  policies.filter (fun policy => satisfiedBound (ba policy) request entities)
-
-/--
-A bound analysis is sound if it produces sound bounds for all policies.
--/
-def IsSoundBoundAnalysis (ba : BoundAnalysis) : Prop :=
-  ∀ (policy : Policy), IsSoundPolicyBound (ba policy) policy
-
 /--
 A sound bound analysis produces sound policy slices.
 -/