This file defines what it means for a policy slice to be sound.

We prove two main theorems:

• Authorization returns the same response for a sound policy slice as for the original collection of policies (isAuthorized_eq_for_sound_policy_slice).
• It is sound to slice policies based on scope constraints (see isAuthorized_eq_for_scope_based_policy_slice). The proof is based on a more general lemma (sound_bound_analysis_produces_sound_slices) that covers all forms of slicing that are based on identifying "bound" principal and resource entities (if any) for a policy, such that the policy evaluates to true on an input only if the request principal and resource are descendents of the corresponding bound entities. Currently, we are extracting bounds only from the scope constraints. The general lemma also covers more sophisticated analyses that can extract bounds from policy conditions as well.