This file contains useful lemmas about the Evaluator functions.
producesBool means the expression evaluates to a bool (and not an error)
Equations
- Cedar.Thm.producesBool e request entities = match Cedar.Spec.evaluate e request entities with | Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b)) => true = true | x => false = true
Instances For
producesNonBool means the expression evaluates to a non-bool (and not an error)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.and_bool_operands_is_boolean_and
{b₁ b₂ : Bool}
{e₁ e₂ : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
:
Spec.evaluate e₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool b₁)) →
Spec.evaluate e₂ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool b₂)) →
Spec.evaluate (e₁.and e₂) request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool (b₁ && b₂)))
theorem
Cedar.Thm.left_false_implies_and_false
{e₁ e₂ : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
:
Spec.evaluate e₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false)) →
Spec.evaluate (e₁.and e₂) request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))
theorem
Cedar.Thm.left_bool_right_false_implies_and_false
{e₁ e₂ : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
:
producesBool e₁ request entities →
Spec.evaluate e₂ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false)) →
Spec.evaluate (e₁.and e₂) request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))
theorem
Cedar.Thm.and_true_implies_left_true
{e₁ e₂ : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
:
Spec.evaluate (e₁.and e₂) request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) →
Spec.evaluate e₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))
theorem
Cedar.Thm.and_true_implies_right_true
{e₁ e₂ : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
:
Spec.evaluate (e₁.and e₂) request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) →
Spec.evaluate e₂ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))
theorem
Cedar.Thm.ways_and_can_error
{e₁ e₂ : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
{err : Spec.Error}
:
Spec.evaluate (e₁.and e₂) request entities = Except.error err →
Spec.evaluate e₁ request entities = Except.error err ∨ Spec.evaluate e₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate e₂ request entities = Except.error err ∨ err = Spec.Error.typeError ∧ producesNonBool e₁ request entities ∨ err = Spec.Error.typeError ∧ Spec.evaluate e₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ producesNonBool e₂ request entities
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 .ok true)
theorem
Cedar.Thm.and_produces_bool_or_error
(e₁ e₂ : Spec.Expr)
(request : Spec.Request)
(entities : Spec.Entities)
:
match Spec.evaluate (e₁.and e₂) request entities with
| Except.ok (Spec.Value.prim (Spec.Prim.bool b)) => true = true
| Except.error a => true = true
| x => false = true
Every and expression produces either .ok bool or .error
theorem
Cedar.Thm.policy_produces_bool_or_error
(p : Spec.Policy)
(request : Spec.Request)
(entities : Spec.Entities)
:
match Spec.evaluate p.toExpr request entities with
| Except.ok (Spec.Value.prim (Spec.Prim.bool b)) => true = true
| Except.error a => true = true
| x => false = true
Corollary of the above: Evaluating a policy produces either .ok bool or .error
theorem
Cedar.Thm.record_produces_record_value
{rxs : List (Spec.Attr × Spec.Expr)}
{v : Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
(he : Spec.evaluate (Spec.Expr.record rxs) request entities = Except.ok v)
:
If evaluating a record produces a value, then it always produces a record value.
theorem
Cedar.Thm.record_value_contains_evaluated_attrs
{rxs : List (Spec.Attr × Spec.Expr)}
{rvs : Data.Map Spec.Attr Spec.Value}
{a : Spec.Attr}
{av : Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
(he : Spec.evaluate (Spec.Expr.record rxs) request entities = Except.ok (Spec.Value.record rvs))
(hfv : rvs.find? a = some av)
:
If evaluating a record produces a record value containing an attribute, then that attribute existed in the original record, and corresponding expression evaluates to the same value.