@[irreducible]
theorem
Cedar.Thm.level_based_slicing_is_sound_expr
{e : Spec.Expr}
{n : Nat}
{tx : Validation.TypedExpr}
{c c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf e c env = Except.ok (tx, c₁))
(hl : Validation.TypedExpr.AtLevel env tx n)
:
theorem
Cedar.Thm.typecheck_policy_with_level_is_sound
{p : Spec.Policy}
{tx : Validation.TypedExpr}
{n : Nat}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hr : InstanceOfWellFormedEnvironment request entities env)
(htl : Validation.typecheckPolicyWithLevel p n env = Except.ok tx)
:
Spec.evaluate p.toExpr request entities = Spec.evaluate p.toExpr request (entities.sliceAtLevel request n)
theorem
Cedar.Thm.typecheck_policy_at_level_with_environments_is_sound
{p : Spec.Policy}
{schema : Validation.Schema}
{n : Nat}
{request : Spec.Request}
{entities : Spec.Entities}
(he : ∃ (env : Validation.TypeEnv), env ∈ schema.environments ∧ InstanceOfWellFormedEnvironment request entities env)
(htl :
Validation.typecheckPolicyWithEnvironments (fun (x : Spec.Policy) => Validation.typecheckPolicyWithLevel x n) p
schema = Except.ok ())
:
Spec.evaluate p.toExpr request entities = Spec.evaluate p.toExpr request (entities.sliceAtLevel request n)
theorem
Cedar.Thm.validate_with_level_is_sound_wf
{ps : Spec.Policies}
{schema : Validation.Schema}
{n : Nat}
{request : Spec.Request}
{entities : Spec.Entities}
(hwf : InstanceOfWellFormedSchema schema request entities)
(htl : Validation.validateWithLevel ps schema n = Except.ok ())
:
Spec.isAuthorized request entities ps = Spec.isAuthorized request (entities.sliceAtLevel request n) ps