Finish proof about updateSchema

[khieta]

Category

Lean formalization

Describe the feature you'd like to request

As discussed in #414, the updateSchema primitive added as a part of entity/request validation is a potential source of incorrect behavior. It would be ideal to fully formalize that this function is doing what we want.

Current progress is in https://github.com/cedar-policy/cedar-spec/tree/bhakti/update-schema-proof.

Describe alternatives you've considered

No response

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