Research proof index

The lemma shows that the symbolic compiler (compile) behaves like the concrete evaluator (evaluate) on literal inputs. In particular, let x be an expression, εnv a well-formed symbolic environment for x, and env a well-formed concrete environment for x that is equivalent to εnv. Then, the result produced by the symbolic compiler on x and...

The lemma shows that interpret and compile can be applied in any order to get the same result. In particular, let x be an expression, εnv a well-formed symbolic environment for x, and I a well-formed interpretion for εnv. Then, compiling x with respect to (εnv.interpret I) gives the same result as interpreting the output of compiling x...

Let x be a Cedar expression and εnv a symbolic environment, where x and εnv are a well-formed input to the symbolic compiler, i.e., εnv.WellFormedFor x. Let t the outcome of compiling x to a Term with respect to εnv, and o a concrete outcome represented by t. Then, the completeness theorem says that there exists a concrete environment...

Requests and entities that pass isValidAndConsistent satisfy RequestAndEntitiesRefine.

Theorem stating that converting a TypedExpr to a Residual preserves evaluation semantics. That is, evaluating the original TypedExpr (converted to Expr) gives the same result as evaluating the converted Residual.

This theorem covers the "happy path" -- showing that if optimized policy compilation with CompiledPolicy.compile succeeds, then satAsserts? and satAssertsOpt? are equivalent.