Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 385 to 390 of 2,569 results.

Project-declaredLean 4.31.0

Unchanged determining when add policy and decision unchanged

Cedar.Thm.unchanged_determining_when_add_policy_and_decision_unchanged

Mathematical statement

If P is a determining policy, then adding a new policy resulting in the same decision won't change that.

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Unchanged erroring when add policy

Cedar.Thm.unchanged_erroring_when_add_policy

Mathematical statement

If P is an erroring policy, then adding another policy won’t change that (even if the decision changes).

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Validation is sound

Cedar.Thm.validation_is_sound

Mathematical statement

If a set of policies is well-typed (valid) with respect to the schema according to the validator, and the input request and entities are consistent with the schema, then evaluating a policy in this set either produces a boolean value, or throws an error of type entityDoesNotExist, extensionError, or arithBoundsError. These errors cannot be protected...

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Validation is sound response

Cedar.Thm.validation_is_sound_response

Mathematical statement

Response-level form of validation_is_sound: for a validated policy set with unique policy ids, every policy in the authorizer's erroringPolicies errored with one of the three errors validation cannot rule out (entityDoesNotExist, extensionError, arithBoundsError). Uniqueness of ids (PolicyIdsUnique, as in `determining_erroring_disjoint_when_...