This file proves that verifyEvaluate queries are well-behaved.

theorem Cedar.Thm.value_type_bool_implies_bool {v : Spec.Value} {t : SymCC.Term} : v ∼ t → t.typeOf = SymCC.TermType.bool → ∃ (b : Bool), v = Spec.Value.prim (Spec.Prim.bool b)

theorem Cedar.Thm.verifyNeverErrors_wbeq : WellBehavedEvaluateQuery SymCC.Factory.isSome Except.isOk

theorem Cedar.Thm.verifyAlwaysMatches_wbeq : WellBehavedEvaluateQuery (fun (x : SymCC.Term) => SymCC.Factory.eq x (⊙SymCC.Term.prim (SymCC.TermPrim.bool true))) fun (x : Spec.Result Spec.Value) => x == Except.ok (Spec.Value.prim (Spec.Prim.bool true))

theorem Cedar.Thm.verifyNeverMatches_wbeq : WellBehavedEvaluateQuery (fun (t : SymCC.Term) => SymCC.Factory.not (SymCC.Factory.eq t (⊙SymCC.Term.prim (SymCC.TermPrim.bool true)))) fun (x : Spec.Result Spec.Value) => x != Except.ok (Spec.Value.prim (Spec.Prim.bool true))