This file proves that level checking for .extHasAttr expressions is sound.
Core helper lemmas #
theorem
Cedar.Thm.reachable_implies_find_agree
(entities : Spec.Entities)
(request : Spec.Request)
(uid : Spec.EntityUID)
(n : Nat)
(hr : ReachableIn entities request.sliceEUIDs uid (n + 1))
:
If uid is reachable at level n+1, then its find? agrees between
entities and the slice at level n+1.
The main soundness theorem #
theorem
Cedar.Thm.hasAttrs_loop_entity_sound
{uid : Spec.EntityUID}
{ety : Spec.EntityType}
{attrs : List Spec.Attr}
{sliceLevel : Nat}
{entities : Spec.Entities}
{request : Spec.Request}
{env : Validation.TypeEnv}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(huidty : InstanceOfEntityType uid ety env)
(hcost : Validation.extHasAttrChainCost env (Validation.CedarType.entity ety) attrs < sliceLevel)
(hreach :
ReachableIn entities request.sliceEUIDs uid
(sliceLevel - Validation.extHasAttrChainCost env (Validation.CedarType.entity ety) attrs))
:
Spec.hasAttrs.loop (Spec.Value.prim (Spec.Prim.entityUID uid)) attrs entities = Spec.hasAttrs.loop (Spec.Value.prim (Spec.Prim.entityUID uid)) attrs (entities.sliceAtLevel request sliceLevel)
Core lemma: hasAttrs.loop on an entity uid agrees between full and sliced
stores when the uid is reachable and the chain cost budget is sufficient.
theorem
Cedar.Thm.hasAttrs_loop_record_sound
{r : Data.Map Spec.Attr Spec.Value}
{rty : Validation.RecordType}
{attrs : List Spec.Attr}
{sliceLevel : Nat}
{entities : Spec.Entities}
{request : Spec.Request}
{env : Validation.TypeEnv}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(hinst : InstanceOfType env (Spec.Value.record r) (Validation.CedarType.record rty))
(hcost : Validation.extHasAttrChainCost env (Validation.CedarType.record rty) attrs ≤ sliceLevel)
(hreach :
∀ (path : List Spec.Attr),
Validation.extHasAttrFirstEntityPath? env (Validation.CedarType.record rty) attrs = some path →
∀ (uid : Spec.EntityUID),
Value.EuidViaPath (Spec.Value.record r) path uid →
ReachableIn entities request.sliceEUIDs uid
(sliceLevel - Validation.extHasAttrChainCost env (Validation.CedarType.record rty) attrs + 1))
:
Spec.hasAttrs.loop (Spec.Value.record r) attrs entities = Spec.hasAttrs.loop (Spec.Value.record r) attrs (entities.sliceAtLevel request sliceLevel)
theorem
Cedar.Thm.level_based_slicing_is_sound_ext_has_attr
{e : Spec.Expr}
{tx : Validation.TypedExpr}
{a : Spec.Attr}
{attrs : List Spec.Attr}
{n : Nat}
{c₀ c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c₀ request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf (e.extHasAttr a attrs) c₀ env = Except.ok (tx, c₁))
(hl : Validation.TypedExpr.AtLevel env tx n)
(ihe : TypedAtLevelIsSound e)
:
Spec.evaluate (e.extHasAttr a attrs) request entities = Spec.evaluate (e.extHasAttr a attrs) request (entities.sliceAtLevel request n)