main PE soundness theorems

[cdisselkoen]

This PR includes the main soundness theorems for partial authorization (in Thm/Partial/Authorization.lean) and partial evaluation (in Thm/Partial/Evaluation.lean). Draft for now because although it contains over 5K lines of proof (!), it also still contains approximately 52 sorrys (!)

This PR also fixes a few soundness problems which otherwise prevent the theorems from holding (!):

• Error residuals in Partial.Response no longer carry a copy of the specific error, just the ID of the policy that errored, so that structural equality of Partial.Response has the intended semantics (matching how the spec authorizer is specified; see Lean: Specify authz response includes ids of erroring policies #206).
• Partial-evaluating true && residual cannot return residual in all cases. Consider the case where residual is a single unknown, and that we substitute it with 37. We need the substitute-and-reevaluate operation to return type-error, not 37. This PR has partial evaluation just return true && residual in all these cases. More precision is possible in the future, but not required for soundness.
• Everything in the above bullet also applies to false || residual.
• Everything in the above two bullets applies to both Partial.evaluate and Partial.evaluateValue.
• When the partial evaluator evaluates a request variable (principal, context, etc) or a GetAttr getting an entity attribute, instead of returning the partial value directly, it needs to evaluateValue it, in case the partial value contains a residual that could be (fully) evaluated (e.g., because a substitution operation was recently performed on it).

[aaronjeline]

Everything in the above bullet also applies to false || residual.

We need typed unknowns :)