Source-pinned research
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.
Showing 433 to 438 of 2,569 results.
Cedar.Thm.verifyNeverMatches_is_complete'
Mathematical statement
Alternate definition of completeness for neverMatches: For a singleton policyset, if symcc says the policy does not neverMatch, then there exists a concrete environment where the policy appears in determiningPolicies.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyNeverMatches_is_ok_and_complete
Mathematical statement
Concrete version of verifyNeverMatches_is_complete.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyNeverMatches_is_ok_and_sound
Mathematical statement
Concrete version of verifyNeverMatches_is_sound.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyNeverMatches_is_sound'
Mathematical statement
Alternate definition of soundness for neverMatches: For a singleton policyset, if symcc says the policy neverMatches, then the spec authorizer should say it never appears in determiningPolicies.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.ways_and_can_error
Mathematical statement
If an and expression results in an error, it's because either: - the left subexpression had that error - the right subexpression had that error (and the left subexpression evaluated to .ok true) - the left subexpression evaluated to .ok with a non-bool - the right subexpression evaluated to .ok with a non-bool (and the left subexpression evaluated to .o...
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.well_typed_implies_wf_type
Mathematical statement
TypedExpr.WellTyped implies well-formedness of the type (CedarType.WellFormed).
Source project: Cedar Specification
Person-level attribution pending.