This file proves the compilation lemmas for .hasAttr and .getAttr expressions.

theorem Cedar.Thm.compile_evaluate_hasAttr_record {a : Spec.Attr} {v₁ : Spec.Value} {es : Spec.Entities} {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty₁ : SymCC.TermType} {rty rty' : Data.Map Spec.Attr SymCC.TermType} (hwφ₁ : SymCC.Term.WellFormed εs t₁) (hty₁ : t₁.typeOf = ty₁.option) (hwo : SymCC.Term.WellFormed εs (SymCC.Factory.option.get t₁) ∧ (SymCC.Factory.option.get t₁).typeOf = SymCC.TermType.record rty') (hwφ₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.bool.option) (ha : RecordHasAttr t₂ (SymCC.Factory.option.get t₁) rty a) (ih : Except.ok v₁ ∼ t₁) : Spec.hasAttr v₁ a es ∼ SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.compile_evaluate_hasAttr_entity {a : Spec.Attr} {v₁ : Spec.Value} {es : Spec.Entities} {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {fₐ : SymCC.UnaryFunction} {ety : Spec.EntityType} {rty : Data.Map Spec.Attr SymCC.TermType} (heq : SymCC.SameEntities es εs) (hwε : εs.WellFormed) (hwf₁ : Spec.Value.WellFormed es v₁) (hwφ₁ : SymCC.Term.WellFormed εs t₁) (hty₁ : t₁.typeOf = (SymCC.TermType.entity ety).option) (hwo : SymCC.Term.WellFormed εs (SymCC.Factory.option.get t₁) ∧ (SymCC.Factory.option.get t₁).typeOf = SymCC.TermType.entity ety) (hwφ₂ : SymCC.Term.WellFormed εs t₂ ∧ t₂.typeOf = SymCC.TermType.bool.option) (hf : εs.attrs ety = some fₐ) (ha : RecordHasAttr t₂ (SymCC.Factory.app fₐ (SymCC.Factory.option.get t₁)) rty a) (ih : Except.ok v₁ ∼ t₁) : Spec.hasAttr v₁ a es ∼ SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.compile_evaluate_hasAttr {x₁ : Spec.Expr} {a : Spec.Attr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (heq : env ∼ εnv) (hwe : env.WellFormedFor (x₁.hasAttr a)) (hwε : εnv.WellFormedFor (x₁.hasAttr a)) (hok : SymCC.compile (x₁.hasAttr a) εnv = Except.ok t) (ih : CompileEvaluate x₁) : Spec.evaluate (x₁.hasAttr a) env.request env.entities ∼ t

theorem Cedar.Thm.interpret_compileHasAttr {t t₁ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} {I : SymCC.Interpretation} (hwε : εs.WellFormed) (hI : I.WellFormed εs) (hwt : SymCC.Term.WellFormed εs t₁) (hok : SymCC.compileHasAttr t₁ a εs = Except.ok t) : SymCC.compileHasAttr (SymCC.Term.interpret I t₁) a (SymCC.SymEntities.interpret I εs) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.compileHasAttr_false_of_getAttr_error_typeOf_eq {t₁ t₂ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} {e : SymCC.Error} (hwε : εs.WellFormed) (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty : t₁.typeOf = t₂.typeOf) (hha : SymCC.compileHasAttr t₁ a εs = Except.ok (⊙SymCC.Term.prim (SymCC.TermPrim.bool false))) (hga : SymCC.compileGetAttr t₁ a εs = Except.error e) : SymCC.compileHasAttr t₂ a εs = Except.ok (⊙SymCC.Term.prim (SymCC.TermPrim.bool false))

theorem Cedar.Thm.compileGetAttr_noSuchAttribute_of_error_typeOf_eq {t₁ t₂ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} {e : SymCC.Error} (hwε : εs.WellFormed) (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty : t₁.typeOf = t₂.typeOf) (hha : SymCC.compileHasAttr t₁ a εs = Except.ok (⊙SymCC.Term.prim (SymCC.TermPrim.bool false))) (hga : SymCC.compileGetAttr t₁ a εs = Except.error e) : SymCC.compileGetAttr t₂ a εs = Except.error SymCC.Error.noSuchAttribute

theorem Cedar.Thm.interpret_compileGetAttr_error_of_compileHasAttr_false {t₁ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {e : SymCC.Error} (hwε : εs.WellFormed) (hI : I.WellFormed εs) (hwt : SymCC.Term.WellFormed εs t₁) (hha : SymCC.compileHasAttr t₁ a εs = Except.ok (⊙SymCC.Term.prim (SymCC.TermPrim.bool false))) (hga : SymCC.compileGetAttr t₁ a εs = Except.error e) : SymCC.compileGetAttr (SymCC.Term.interpret I t₁) a (SymCC.SymEntities.interpret I εs) = Except.error SymCC.Error.noSuchAttribute

theorem Cedar.Thm.interpret_option_get_aux {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {ty : SymCC.TermType} (hI : I.WellFormed εs) (hwt : SymCC.Term.WellFormed εs t) (hty : t.typeOf = ty.option) : SymCC.Term.WellFormed (SymCC.SymEntities.interpret I εs) (SymCC.Term.interpret I (SymCC.Factory.option.get t)) ∧ SymCC.Term.WellFormed (SymCC.SymEntities.interpret I εs) (SymCC.Factory.option.get (SymCC.Term.interpret I t)) ∧ (SymCC.Term.interpret I (SymCC.Factory.option.get t)).typeOf = (SymCC.Factory.option.get (SymCC.Term.interpret I t)).typeOf

theorem Cedar.Thm.compileHasAttr_interpret_ok {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t_ha : SymCC.Term} {a : Spec.Attr} {ty : SymCC.TermType} (hI : I.WellFormed εs) (hwε : εs.WellFormed) (hwt : SymCC.Term.WellFormed εs t₁) (hty : t₁.typeOf = ty.option) (hi : SymCC.compileHasAttr (SymCC.Term.interpret I (SymCC.Factory.option.get t₁)) a (SymCC.SymEntities.interpret I εs) = Except.ok (SymCC.Term.interpret I t_ha)) : ∃ (t' : SymCC.Term), SymCC.compileHasAttr (SymCC.Factory.option.get (SymCC.Term.interpret I t₁)) a (SymCC.SymEntities.interpret I εs) = Except.ok t'

theorem Cedar.Thm.compile_interpret_hasAttr {x₁ : Spec.Expr} {a : Spec.Attr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (hI : I.WellFormed εnv.entities) (hwε : εnv.WellFormedFor (x₁.hasAttr a)) (hok : SymCC.compile (x₁.hasAttr a) εnv = Except.ok t) (ih : CompileInterpret x₁) : SymCC.compile (x₁.hasAttr a) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.compile_evaluate_getAttr_record {a : Spec.Attr} {v₁ : Spec.Value} {es : Spec.Entities} {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty₁ tyₐ : SymCC.TermType} {rty rty' : Data.Map Spec.Attr SymCC.TermType} (hwφ₁ : SymCC.Term.WellFormed εs t₁) (hty₁ : t₁.typeOf = ty₁.option) (hwo : SymCC.Term.WellFormed εs (SymCC.Factory.option.get t₁) ∧ (SymCC.Factory.option.get t₁).typeOf = SymCC.TermType.record rty') (hwφ₂ : SymCC.Term.WellFormed εs t₂) (htyₐ : t₂.typeOf = tyₐ.option) (ha : RecordGetAttr t₂ (SymCC.Factory.option.get t₁) rty a) (ih : Except.ok v₁ ∼ t₁) : Spec.getAttr v₁ a es ∼ SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.compile_evaluate_getAttr_entity {a : Spec.Attr} {v₁ : Spec.Value} {es : Spec.Entities} {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {fₐ : SymCC.UnaryFunction} {ety : Spec.EntityType} {tyₐ : SymCC.TermType} {rty : Data.Map Spec.Attr SymCC.TermType} (heq : SymCC.SameEntities es εs) (hwε : εs.WellFormed) (hwf₁ : Spec.Value.WellFormed es v₁) (hwφ₁ : SymCC.Term.WellFormed εs t₁) (hty₁ : t₁.typeOf = (SymCC.TermType.entity ety).option) (hwo : SymCC.Term.WellFormed εs (SymCC.Factory.option.get t₁) ∧ (SymCC.Factory.option.get t₁).typeOf = SymCC.TermType.entity ety) (hwφ₂ : SymCC.Term.WellFormed εs t₂) (htyₐ : t₂.typeOf = tyₐ.option) (hf : εs.attrs ety = some fₐ) (ha : RecordGetAttr t₂ (SymCC.Factory.app fₐ (SymCC.Factory.option.get t₁)) rty a) (ih : Except.ok v₁ ∼ t₁) : Spec.getAttr v₁ a es ∼ SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.compile_evaluate_getAttr {x₁ : Spec.Expr} {a : Spec.Attr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (heq : env ∼ εnv) (hwe : env.WellFormedFor (x₁.getAttr a)) (hwε : εnv.WellFormedFor (x₁.getAttr a)) (hok : SymCC.compile (x₁.getAttr a) εnv = Except.ok t) (ih : CompileEvaluate x₁) : Spec.evaluate (x₁.getAttr a) env.request env.entities ∼ t

theorem Cedar.Thm.interpret_compileGetAttr {t t₁ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} {I : SymCC.Interpretation} (hwε : εs.WellFormed) (hI : I.WellFormed εs) (hwt : SymCC.Term.WellFormed εs t₁) (hok : SymCC.compileGetAttr t₁ a εs = Except.ok t) : SymCC.compileGetAttr (SymCC.Term.interpret I t₁) a (SymCC.SymEntities.interpret I εs) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.compileGetAttr_interpret_ok {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t₁ t_ga : SymCC.Term} {a : Spec.Attr} {ty : SymCC.TermType} (hI : I.WellFormed εs) (hwε : εs.WellFormed) (hwt : SymCC.Term.WellFormed εs t₁) (hty : t₁.typeOf = ty.option) (hi : SymCC.compileGetAttr (SymCC.Term.interpret I (SymCC.Factory.option.get t₁)) a (SymCC.SymEntities.interpret I εs) = Except.ok (SymCC.Term.interpret I t_ga)) : ∃ (t' : SymCC.Term), SymCC.compileGetAttr (SymCC.Factory.option.get (SymCC.Term.interpret I t₁)) a (SymCC.SymEntities.interpret I εs) = Except.ok t'

theorem Cedar.Thm.compileGetAttr_ok_typeOf_eq {t t₁ t₂ t₃ : SymCC.Term} {a : Spec.Attr} {εs : SymCC.SymEntities} (hwε : εs.WellFormed) (hw₁ : SymCC.Term.WellFormed εs t₁) (hw₂ : SymCC.Term.WellFormed εs t₂) (hty : t₁.typeOf = t₂.typeOf) (hok₁ : SymCC.compileGetAttr t₁ a εs = Except.ok t) (hok₂ : SymCC.compileGetAttr t₂ a εs = Except.ok t₃) : t₃.typeOf = t.typeOf

theorem Cedar.Thm.compile_interpret_getAttr {x₁ : Spec.Expr} {a : Spec.Attr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (hI : I.WellFormed εnv.entities) (hwε : εnv.WellFormedFor (x₁.getAttr a)) (hok : SymCC.compile (x₁.getAttr a) εnv = Except.ok t) (ih : CompileInterpret x₁) : SymCC.compile (x₁.getAttr a) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)