Documentation

Cedar.Thm.SymCC.Verifier.VerifyEvaluate

This file proves the soundness and completeness of Cedar.SymCC.verifyEvaluate for well-behaved verification queries. This enables proving soundness and completeness of analyses built on verifyEvaluate by proving that their queries are well-behaved. #

source
def Cedar.Thm.WellBehavedEvaluateQuery (φ : SymCC.Term → SymCC.Term) (f : Spec.Result Spec.Value → Bool) :
Prop
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Cedar.Thm.WellBehavedEvaluateQuery.WellFormedInput (t : SymCC.Term) (εs : SymCC.SymEntities) :
    Prop
    Equations
    Instances For
      source
      def Cedar.Thm.WellBehavedEvaluateQuery.WellFormedOutput (φ : SymCC.Term → SymCC.Term) :
      Prop
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cedar.Thm.WellBehavedEvaluateQuery.Interpretable (φ : SymCC.Term → SymCC.Term) :
        Prop
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cedar.Thm.WellBehavedEvaluateQuery.Same (φ : SymCC.Term → SymCC.Term) (f : Spec.Result Spec.Value → Bool) :
          Prop
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Cedar.Thm.verifyEvaluate_is_sound {φ : SymCC.Term → SymCC.Term} {f : Spec.Result Spec.Value → Bool} {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} :
            WellBehavedEvaluateQuery φ f → εnv.StronglyWellFormedForPolicy p → SymCC.verifyEvaluate φ p εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p → f (Spec.evaluate p.toExpr env.request env.entities) = true
            source
            theorem Cedar.Thm.verifyEvaluate_is_complete {φ : SymCC.Term → SymCC.Term} {f : Spec.Result Spec.Value → Bool} {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} :
            WellBehavedEvaluateQuery φ f → εnv.StronglyWellFormedForPolicy p → SymCC.verifyEvaluate φ p εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p ∧ SymCC.Env.EnumCompleteFor env εnv ∧ f (Spec.evaluate p.toExpr env.request env.entities) = false