Level checking soundness proof

[john-h-kastner-aws]

Proves that level based entity slicing at level n cannot change the authorization decision when using polices that validate at level n.

The main theorem is

theorem validate_with_level_is_sound {ps : Policies} {schema : Schema} {n : Nat} {request : Request} {entities slice : Entities}
  (hr : validateRequest schema request = .ok ())
  (he : validateEntities schema entities = .ok ())
  (hs : slice = entities.sliceAtLevel request n)
  (htl : validateWithLevel ps schema n = .ok ()) :
  isAuthorized request entities ps = isAuthorized request slice ps

[emina]

Looks good to me!

[chaluli]

Looks good.