Lean: Specify authz response includes ids of erroring policies

[cdisselkoen]

Description of changes:

The main change is at Spec/Response.lean and Spec/Authorizer.lean. isAuthorized now reports the set of ids of policies which encountered an error.

I created Thm/SlicingDefs.lean to hold the definition of "sound policy slice" (which was previously inlined everywhere). Importantly, I adjusted this definition to include that all sliced-out policies evaluate without errors.

This required substantial changes to proofs. I hesitate to call this proof repair -- really, it imposed an entire new proof obligation for the slicing results (in Thm/Slicing.lean): we have to prove that with scope-based policy slicing, all sliced-out policies evaluate without errors.

When possible, I added general-purpose lemmas to Data/List.lean, Data/Set.lean, etc rather than just inlining them where needed.

This is my first nontrivial Lean PR, suggestions and style corrections are very welcome. :)

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[emina]

Very nice first Lean PR :))

Left some comments on code style and one suggestion for making the model shorter. (If it's too hard to use the shorter model because it breaks too many proofs, please ignore, and we can address it in a separate PR.)

The main piece of style feedback is to get rid of the separate SlicingDefs file and merging its sole definition back into Slicing. The merged structure fits better with how Lean projects organize code (more in the comments).

[khieta]

Looks great! Left some small comments, but approving as-is.