Documentation

Cedar.Thm.SymCC.Verifier.VerifyEvaluatePair

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

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