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 200 research declarations. Search 10,000 more complete Mathlib declarations.
200 results
Clear filtersCedar.Thm.verifyNeverMatches_is_complete'
Plain-language 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
Plain-language statement
Concrete version of verifyNeverMatches_is_complete.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyNeverMatches_is_ok_and_sound
Plain-language statement
Concrete version of verifyNeverMatches_is_sound.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyNeverMatches_is_sound'
Plain-language 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
Plain-language 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
Plain-language statement
TypedExpr.WellTyped implies well-formedness of the type (CedarType.WellFormed).
Source project: Cedar Specification
Person-level attribution pending.