Standalone Lean project
Formal semantics and machine-checked results for the Cedar authorization language, with differential testing against the production implementation.
Flagship declarations
Cedar.Data.Map.find?_ext
Plain-language statement
Two well-formed maps are equal if they have the same find? for every key.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.find?_notmem_keys
Plain-language statement
Inverse of find?_mem_toList, except that this requires wf
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.find?_some_iff_in_values
Plain-language statement
The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.in_list_iff_find?_some
Plain-language statement
The mpr direction of this does not need the wf precondition and, in fact, is available separately as find?_mem_toList above
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.map_make_append_find_disjoint
Plain-language statement
If a key exists in l₂ but not in l₁, then Map.make (l₁ ++ l₂) contains that key.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.map_make_append_find_disjoint'
Plain-language statement
A variant of map_make_append_find_disjoint.
Source project: Cedar Specification
Person-level attribution pending.
Project index
Showing 8 of 194 additional declarations. Use project search for the complete index.
Cedar.Data.Map.mapMOnValues_ok_implies_all_ok
Plain-language statement
Note that the converse is not true: counterexample m₁ is [(1, false)], m₂ is [(1, false), (2, true)], f is Except.ok But for a limited converse, see all_ok_implies_mapMOnValues_ok
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_preserves_keys
Plain-language statement
This is not stated in terms of Map.keys because Map.keys produces a Set, and we want the even stronger property that it not only preserves the key-set, but also the key-order. (We'll use this to prove mapMOnValues_some_wf.)
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_some_implies_all_from_some_alt_proof
Plain-language statement
alternate proof of mapMOnValues_some_implies_all_from_some, which instead of relying on mapMOnValues_some_implies_forall₂, relies on List.mapM_some_implies_all_from_some. Which do we prefer?
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_some_implies_all_some_alt_proof
Plain-language statement
alternate proof of mapMOnValues_some_implies_all_some, which instead of relying on mapMOnValues_some_implies_forall₂, relies on List.mapM_some_implies_all_some. Which do we prefer?
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_some_wf_alt_proof
Plain-language statement
Alternate proof of mapMOnValues_some_wf, that relies on List.mapM_some_eq_filterMap instead of mapMOnValues_preserves_keys. Which do we prefer?
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mem_values_make
Plain-language statement
Very similar to mem_make_mem_list above
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.action_scope_produces_boolean
Plain-language statement
Lemma: evaluating the actionScope of any policy produces a boolean (and does not error)
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.allowed_iff_explicitly_permitted_and_not_denied
Plain-language statement
A request is allowed if and only if it is explicitly permitted and is not explicitly forbidden.
Source project: Cedar Specification
Person-level attribution pending.