Prove residuals from TPE satisfy Symcc preconditions

[john-h-kastner-aws]

Category

Lean formalization

Describe the feature you'd like to request

It should be possible to take the residual resulting from TPE and symbolically compile it with symcc, but we have not proven it.

The main precondition here should be that the residual are well-typed, which we do prove, but the symcc compiler works over Expr not Residual. This is problematic because Expr doesn't have type annotations, so it can't represent a typed empty set, but well-typed residual may contain an empty set.

We need to refactor symcc to work on TypedExprs, write a conversion from Residual back to TypedExpr, and prove that those expressions are well typed, satisfying the symcc precondition. We'll presumably also want to prove that it preserves semantics.

That should let us write some top level theorems stating that tpe + symcc gives results consistent with a compatible concrete authorization request, but I haven't thought through exactly what that property is yet.

Describe alternatives you've considered

.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change