Core's bounded evaluator is sound for denoteEval

On a runtime store denoting a semantic store, every value Core's bounded evaluator evalBounded commits to denotes the value of the reference evaluator Lambda.LExpr.denoteEval (BoundedEvalSoundAt), at every modeled factory whose factory meets the conditions of evaluator soundness (Lambda.Factory.EvalSoundWF) and whose short-circuit evaluators commute with re-annotating free variables (Lambda.Factory.ShortCircuitAnnotates): at every modeled factory over a well-formed factory each of whose functions is a function of Core.Factory or a user function meeting UserFuncWF, which userFuncChecked decides for monomorphic user functions; in particular at every modeled factory over Core.Factory.

Key definitions: EvalFactoryWF, fvarsAnnotatedBy, userFuncChecked. Key theorems: boundedEvalSoundAt_of_evalSoundWF, boundedEvalSoundAt_of_evalFactoryWF, evalFactoryWF_of_userFuncs, userFuncWF_of_userFuncChecked, boundedEvalSoundAt_of_userFuncs, evalFactoryWF_coreFactory, boundedEvalSoundAt_coreFactory.

theorem Core.boundedEvalSoundAt_of_evalSoundWF (F : Expression.Factory) (hF : F.factory.EvalSoundWF) (hSC : F.factory.ShortCircuitAnnotates) : Imperative.BoundedEvalSoundAt Expression F

Core's bounded evaluator is sound at a modeled factory F whose factory meets the conditions of evaluator soundness (Lambda.Factory.EvalSoundWF) and whose short-circuit evaluators commute with re-annotating free variables: on a runtime store denoting a semantic store σ, every value evalBounded commits to denotes the value denoteEval gives the expression on σ.

def Core.EvalFactoryWF (f : Lambda.Factory CoreLParams) : Prop

The conditions on a Core factory under which Core's bounded evaluator is sound at every model of it (boundedEvalSoundAt_of_evalFactoryWF): the factory meets the conditions of evaluator soundness (Lambda.Factory.EvalSoundWF: it and a type factory are well formed, and function bodies, at the type substitutions inlining uses and once inlined, and concrete evaluators preserve typing, operator annotations and free-variable annotations), and its short-circuit evaluators commute with re-annotating free variables (Lambda.Factory.ShortCircuitAnnotates).

Equations

• Core.EvalFactoryWF f = (f.EvalSoundWF ∧ f.ShortCircuitAnnotates)

theorem Core.evalFactoryWF_coreFactory : EvalFactoryWF Factory

Core.Factory meets EvalFactoryWF.

theorem Core.boundedEvalSoundAt_of_evalFactoryWF (F : Expression.Factory) (hF : EvalFactoryWF F.factory) : Imperative.BoundedEvalSoundAt Expression F

Core's bounded evaluator is sound at every modeled factory whose factory meets EvalFactoryWF.

theorem Core.boundedEvalSoundAt_coreFactory (F : Expression.Factory) (hF : F.factory = Factory) : Imperative.BoundedEvalSoundAt Expression F

Core's bounded evaluator is sound at Core's built-in factory: at every modeled factory over Core.Factory, on a runtime store denoting a semantic store, every value evalBounded commits to denotes the value denoteEval gives the expression.

def Core.fvarsAnnotatedBy (tyMap : Map CoreIdent Lambda.LMonoTy) : Expression.Expr → Bool

Whether every free variable of e is annotated, with the type tyMap gives it when tyMap gives it one (the decided form of Lambda.fvars_annotated_by).

Equations

• One or more equations did not get rendered due to their size.
• Core.fvarsAnnotatedBy tyMap (Lambda.LExpr.fvar m name none) = false
• Core.fvarsAnnotatedBy tyMap (Lambda.LExpr.app m f a) = (Core.fvarsAnnotatedBy tyMap f && Core.fvarsAnnotatedBy tyMap a)
• Core.fvarsAnnotatedBy tyMap (Lambda.LExpr.abs m prettyName ty body) = Core.fvarsAnnotatedBy tyMap body
• Core.fvarsAnnotatedBy tyMap (Lambda.LExpr.ite m c t f) = (Core.fvarsAnnotatedBy tyMap c && Core.fvarsAnnotatedBy tyMap t && Core.fvarsAnnotatedBy tyMap f)
• Core.fvarsAnnotatedBy tyMap (Lambda.LExpr.eq m a b) = (Core.fvarsAnnotatedBy tyMap a && Core.fvarsAnnotatedBy tyMap b)
• Core.fvarsAnnotatedBy tyMap (Lambda.LExpr.quant m k prettyName ty tr body) = (Core.fvarsAnnotatedBy tyMap tr && Core.fvarsAnnotatedBy tyMap body)
• Core.fvarsAnnotatedBy tyMap x✝ = true

def Core.userFuncChecked (F : Lambda.Factory CoreLParams) (fn : Lambda.LFunc CoreLParams) : Bool

Whether the function fn of the factory F is a monomorphic user function whose body, if any, meets the conditions of UserFuncWF: it has no concrete evaluator, is not a constructor and has no type arguments, and its body type checks at the output type, annotates its free variables with the types of the parameters (fvarsAnnotatedBy), and annotates its operators with instances of their types in F (opsInstantiated).

Equations

• One or more equations did not get rendered due to their size.

theorem Core.userFuncWF_of_userFuncChecked {F : Lambda.Factory CoreLParams} {fn : Lambda.LFunc CoreLParams} (h : userFuncChecked F fn = true) : UserFuncWF F fn

A function userFuncChecked accepts meets UserFuncWF: having no type arguments, it is inlined at the empty type substitution, which leaves its body unchanged.

theorem Core.evalFactoryWF_of_userFuncs (f : Lambda.Factory CoreLParams) (hWF : Lambda.FactoryWF f) (hfns : ∀ (fn : Lambda.LFunc CoreLParams), fn ∈ f.toArray → fn ∈ Factory.toArray ∨ UserFuncWF f fn) : EvalFactoryWF f

A well-formed factory each of whose functions is a function of Core.Factory or a user function meeting UserFuncWF meets EvalFactoryWF.

theorem Core.boundedEvalSoundAt_of_userFuncs (F : Expression.Factory) (hWF : Lambda.FactoryWF F.factory) (hfns : ∀ (fn : Lambda.LFunc CoreLParams), fn ∈ F.factory.toArray → fn ∈ Factory.toArray ∨ UserFuncWF F.factory fn) : Imperative.BoundedEvalSoundAt Expression F

Core's bounded evaluator is sound at program factories: at every modeled factory over a well-formed factory each of whose functions is a function of Core.Factory or a user function meeting UserFuncWF (for instance one userFuncChecked accepts), on a runtime store denoting a semantic store, every value evalBounded commits to denotes the value denoteEval gives the expression.