inductive Cedar.SymCC.CompiledPolicyError : Type

• validationError (e : Validation.ValidationError) : CompiledPolicyError
• symCCError (e : Error) : CompiledPolicyError

instance Cedar.SymCC.instReprCompiledPolicyError : Repr CompiledPolicyError

Equations

• Cedar.SymCC.instReprCompiledPolicyError = { reprPrec := Cedar.SymCC.instReprCompiledPolicyError.repr }

def Cedar.SymCC.instReprCompiledPolicyError.repr : CompiledPolicyError → Nat → Std.Format

Equations

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

def Cedar.SymCC.instBEqCompiledPolicyError.beq : CompiledPolicyError → CompiledPolicyError → Bool

Equations

• Cedar.SymCC.instBEqCompiledPolicyError.beq (Cedar.SymCC.CompiledPolicyError.validationError a) (Cedar.SymCC.CompiledPolicyError.validationError b) = (a == b)
• Cedar.SymCC.instBEqCompiledPolicyError.beq (Cedar.SymCC.CompiledPolicyError.symCCError a) (Cedar.SymCC.CompiledPolicyError.symCCError b) = (a == b)
• Cedar.SymCC.instBEqCompiledPolicyError.beq x✝¹ x✝ = false

instance Cedar.SymCC.instBEqCompiledPolicyError : BEq CompiledPolicyError

Equations

• Cedar.SymCC.instBEqCompiledPolicyError = { beq := Cedar.SymCC.instBEqCompiledPolicyError.beq }

instance Cedar.SymCC.instToStringCompiledPolicyError : ToString CompiledPolicyError

Equations

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

structure Cedar.SymCC.CompiledPolicy : Type

Represents a symbolically compiled policy. This can be fed into the various functions in SymCCOpt.lean for efficient solver queries (that don't have to repeat symbolic compilation).

• term : Term

  typechecked policy compiled to a Term of type .option bool

• εnv : SymEnv

  SymEnv representing the environment this policy was compiled for

• policy : Spec.Policy

  typechecked policy

• footprint : Data.Set Term

  footprint of the policy

• acyclicity : Data.Set Term

  acyclicity constraints for this policy

instance Cedar.SymCC.instReprCompiledPolicy : Repr CompiledPolicy

Equations

• Cedar.SymCC.instReprCompiledPolicy = { reprPrec := Cedar.SymCC.instReprCompiledPolicy.repr }

def Cedar.SymCC.instReprCompiledPolicy.repr : CompiledPolicy → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instInhabitedCompiledPolicy : Inhabited CompiledPolicy

Equations

• Cedar.SymCC.instInhabitedCompiledPolicy = { default := Cedar.SymCC.instInhabitedCompiledPolicy.default }

def Cedar.SymCC.instInhabitedCompiledPolicy.default : CompiledPolicy

Equations

• Cedar.SymCC.instInhabitedCompiledPolicy.default = { term := default, εnv := default, policy := default, footprint := default, acyclicity := default }

def Cedar.SymCC.instDecidableEqCompiledPolicy.decEq (x✝ x✝¹ : CompiledPolicy) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.SymCC.instDecidableEqCompiledPolicy : DecidableEq CompiledPolicy

Equations

• Cedar.SymCC.instDecidableEqCompiledPolicy = Cedar.SymCC.instDecidableEqCompiledPolicy.decEq

def Cedar.SymCC.CompiledPolicy.compile (p : Spec.Policy) (Γ : Validation.TypeEnv) : Except CompiledPolicyError CompiledPolicy

Compile a policy p for the given environment Γ. This function calls the Cedar typechecker to obtain a policy p' that is semantically equivalent to p and well-typed with respect to Γ. Then, it runs the symbolic compiler to produce a compiled policy.

Equations

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

structure Cedar.SymCC.CompiledPolicySet : Type

Represents a symbolically compiled policyset. This can be fed into the various functions in SymCCOpt.lean for efficient solver queries (that don't have to repeat symbolic compilation).

• term : Term

  typechecked policies compiled to a single Term of type .bool representing the authorization decision

• εnv : SymEnv

  SymEnv representing the environment these policies were compiled for

• policies : Spec.Policies

  typechecked policies

• footprint : Data.Set Term

  footprint of the policies

• acyclicity : Data.Set Term

  acyclicity constraints for these policies

instance Cedar.SymCC.instReprCompiledPolicySet : Repr CompiledPolicySet

Equations

• Cedar.SymCC.instReprCompiledPolicySet = { reprPrec := Cedar.SymCC.instReprCompiledPolicySet.repr }

def Cedar.SymCC.instReprCompiledPolicySet.repr : CompiledPolicySet → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instInhabitedCompiledPolicySet : Inhabited CompiledPolicySet

Equations

• Cedar.SymCC.instInhabitedCompiledPolicySet = { default := Cedar.SymCC.instInhabitedCompiledPolicySet.default }

def Cedar.SymCC.instInhabitedCompiledPolicySet.default : CompiledPolicySet

Equations

• Cedar.SymCC.instInhabitedCompiledPolicySet.default = { term := default, εnv := default, policies := default, footprint := default, acyclicity := default }

instance Cedar.SymCC.instDecidableEqCompiledPolicySet : DecidableEq CompiledPolicySet

Equations

• Cedar.SymCC.instDecidableEqCompiledPolicySet = Cedar.SymCC.instDecidableEqCompiledPolicySet.decEq

def Cedar.SymCC.instDecidableEqCompiledPolicySet.decEq (x✝ x✝¹ : CompiledPolicySet) : Decidable (x✝ = x✝¹)

Equations

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

def Cedar.SymCC.CompiledPolicySet.compile (ps : Spec.Policies) (Γ : Validation.TypeEnv) : Except CompiledPolicyError CompiledPolicySet

Compile a set of policies ps for the given environment Γ. This function calls the Cedar typechecker on each p ∈ ps to obtain a policy p' that is semantically equivalent to p and well-typed with respect to Γ. Then, it runs the symbolic compiler to produce a compiled policy.

Equations

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

def Cedar.SymCC.CompiledPolicySet.allowAll (εnv : SymEnv) : CompiledPolicySet

A CompiledPolicySet that represents the policyset that allows all requests in the εnv.

Equations

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

def Cedar.SymCC.CompiledPolicySet.denyAll (εnv : SymEnv) : CompiledPolicySet

A CompiledPolicySet that represents the policyset that denies all requests in the εnv.

Equations

• Cedar.SymCC.CompiledPolicySet.denyAll εnv = { term := Cedar.SymCC.Term.bool false, εnv := εnv, policies := [], footprint := Cedar.Data.Set.empty, acyclicity := Cedar.Data.Set.empty }

def Cedar.SymCC.CompiledPolicy.intoCompiledPolicySet (cp : CompiledPolicy) : CompiledPolicySet

Convert a CompiledPolicy to a CompiledPolicySet representing a singleton policyset with just that policy.

This function is intended to be much more efficient than re-compiling with CompiledPolicySet.compile.

Equations

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

inductive Cedar.SymCC.CompiledPolicies : Type

Represents a CompiledPolicy or a CompiledPolicySet, for APIs that don't care which one they get.

• policy (cp : CompiledPolicy) : CompiledPolicies
• pset (cpset : CompiledPolicySet) : CompiledPolicies

def Cedar.SymCC.CompiledPolicies.allPolicies : CompiledPolicies → Spec.Policies

Equations

• (Cedar.SymCC.CompiledPolicies.policy cp).allPolicies = [cp.policy]
• (Cedar.SymCC.CompiledPolicies.pset cpset).allPolicies = cpset.policies

def Cedar.SymCC.CompiledPolicies.footprint : CompiledPolicies → Data.Set Term

Equations

• (Cedar.SymCC.CompiledPolicies.policy cp).footprint = cp.footprint
• (Cedar.SymCC.CompiledPolicies.pset cpset).footprint = cpset.footprint

def Cedar.SymCC.CompiledPolicies.εnv : CompiledPolicies → SymEnv

Equations

• (Cedar.SymCC.CompiledPolicies.policy cp).εnv = cp.εnv
• (Cedar.SymCC.CompiledPolicies.pset cpset).εnv = cpset.εnv