Documentation

Cedar.Thm.TPE.Input

This file defines theorems related to the inputs of TPE.

source
theorem Cedar.Thm.decide_eq_implies_eq {α : Sort u_1} [DecidableEq α] {y : α} (x : α) :
decide (x = y) = true → x = y
source
inductive Cedar.Thm.PartialIsValid {α : Type u_1} (p : α → Prop) (o : Option α) :
Prop
Instances For
    source
    @[simp]
    theorem Cedar.Thm.PartialIsValid.some_inv {α : Type u_1} {p : α → Prop} {x : α} :
    PartialIsValid p (Option.some x) ↔ p x
    source
    theorem Cedar.Thm.partial_is_valid_rfl {α : Type u_1} {f : α → Bool} {p : α → Prop} {o : Option α} :
    (∀ (x : α), f x = true → p x) → TPE.partialIsValid o f = true → PartialIsValid p o
    source
    def Cedar.Thm.RequestRefines (req : Spec.Request) (preq : TPE.PartialRequest) :
    Prop
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Cedar.Thm.EntitiesRefine (es : Spec.Entities) (pes : TPE.PartialEntities) :
      Prop
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cedar.Thm.RequestAndEntitiesRefine (req : Spec.Request) (es : Spec.Entities) (preq : TPE.PartialRequest) (pes : TPE.PartialEntities) :
        Prop

        Concrete request req and entities es refine their partial counterparts peq and pes.

        Equations
        Instances For
          source
          theorem Cedar.Thm.validatePartialRequest_ok_environment? {schema : Validation.Schema} {req : TPE.PartialRequest} {env : Validation.TypeEnv} :
          TPE.validatePartialRequest schema req = Except.ok env → schema.environment? req.principal.ty req.resource.ty req.action = some env
          source
          theorem Cedar.Thm.entitiesIsConsistent_implies_refines {es : Spec.Entities} {pes : TPE.PartialEntities} :
          TPE.entitiesIsConsistent es pes = true → EntitiesRefine es pes
          source
          theorem Cedar.Thm.requestIsConsistent_implies_refines {req : Spec.Request} {preq : TPE.PartialRequest} :
          TPE.requestIsConsistent req preq = true → RequestRefines req preq
          source
          theorem Cedar.Thm.consistent_checks_ensure_refinement {schema : Validation.Schema} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} :
          TPE.isValidAndConsistent schema req es preq pes = Except.ok () → RequestAndEntitiesRefine req es preq pes

          Requests and entities that pass isValidAndConsistent satisfy RequestAndEntitiesRefine.