This file defines the Cedar symbolic authorizer.

The symbolic authorizer takes as input a set of policies and a symbolic environment. Given these inputs, it produces a Term encoding of the authorization decision for those policies. The output term is of type boolean. If this boolean term evaluates to true, then access is allowed. Otherwise, access is denied.

def Cedar.SymCC.compileWithEffect (effect : Spec.Effect) (policy : Spec.Policy) (εnv : SymEnv) : Result (Option Term)

Equations

• Cedar.SymCC.compileWithEffect effect policy εnv = if (policy.effect == effect) = true then do let a ← Cedar.SymCC.compile policy.toExpr εnv pure (some a) else Except.ok none

def Cedar.SymCC.satisfiedPolicies (effect : Spec.Effect) (policies : Spec.Policies) (εnv : SymEnv) : Result Term

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.isAuthorized (policies : Spec.Policies) (εnv : SymEnv) : Result Term

Equations

• One or more equations did not get rendered due to their size.