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 219 research declarations. Search 10,000 more complete Mathlib declarations.
219 results
Clear filtersCedar.Thm.verifyMatchesDisjoint_is_ok_and_sound
Plain-language statement
Concrete version of verifyMatchesDisjoint_is_sound.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyMatchesDisjoint_is_sound
Plain-language statement
The verifyMatchesDisjoint analysis is sound: if the assertions verifyMatchesDisjoint p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then the policies cannot both match in any strongly well-formed concrete environment env ∈ᵢ εnv.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyMatchesEquivalent_is_complete
Plain-language statement
The verifyMatchesEquivalent analysis is complete: if the assertions verifyMatchesEquivalent p₁ p₂ εnv are satisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the policies will have different matching behavior (one matche...
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyMatchesEquivalent_is_ok_and_complete
Plain-language statement
Concrete version of verifyMatchesEquivalent_is_complete.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyMatchesEquivalent_is_ok_and_sound
Plain-language statement
Concrete version of verifyMatchesEquivalent_is_sound.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.verifyMatchesEquivalent_is_sound
Plain-language statement
The verifyMatchesEquivalent analysis is sound: if the assertions verifyMatchesEquivalent p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then the policies will have the same matching behavior (both match or both don't match) when applied to any strongly well-formed concrete environmen...
Source project: Cedar Specification
Person-level attribution pending.