This file defines abstract syntax for Cedar policies.

inductive Cedar.Spec.Effect : Type

• permit : Effect
• forbid : Effect

inductive Cedar.Spec.Scope : Type

• any : Scope
• eq (entity : EntityUID) : Scope
• mem (entity : EntityUID) : Scope
• is (ety : EntityType) : Scope
• isMem (ety : EntityType) (entity : EntityUID) : Scope

inductive Cedar.Spec.PrincipalScope : Type

• principalScope (scope : Scope) : PrincipalScope

inductive Cedar.Spec.ResourceScope : Type

• resourceScope (scope : Scope) : ResourceScope

inductive Cedar.Spec.ActionScope : Type

This definition of the ActionScope is more liberal than what is allowed by Cedar's concrete grammar. In particular, the concrete grammar doesn't allow is constraints in action scopes (e.g., action is ety), while our abstract grammar does. Restricting action scopes in this way is not necessary for proving any properties of Cedar; it is done in the concrete grammar for usability (since is constraints on actions can be expressed using groups instead). We're choosing the more liberal modeling here for uniformity and simplicity.

• actionScope (scope : Scope) : ActionScope
• actionInAny (ls : List EntityUID) : ActionScope

@[reducible, inline]

abbrev Cedar.Spec.PolicyID : Type

Equations

• Cedar.Spec.PolicyID = String

inductive Cedar.Spec.ConditionKind : Type

• when : ConditionKind
• unless : ConditionKind

structure Cedar.Spec.Condition : Type

• kind : ConditionKind
• body : Expr

@[reducible, inline]

abbrev Cedar.Spec.Conditions : Type

Equations

• Cedar.Spec.Conditions = List Cedar.Spec.Condition

structure Cedar.Spec.Policy : Type

• id : PolicyID
• effect : Effect
• principalScope : PrincipalScope
• actionScope : ActionScope
• resourceScope : ResourceScope
• condition : Conditions

@[reducible, inline]

abbrev Cedar.Spec.Policies : Type

Equations

• Cedar.Spec.Policies = List Cedar.Spec.Policy

def Cedar.Spec.PrincipalScope.scope : PrincipalScope → Scope

Equations

• (Cedar.Spec.PrincipalScope.principalScope s).scope = s

def Cedar.Spec.ResourceScope.scope : ResourceScope → Scope

Equations

• (Cedar.Spec.ResourceScope.resourceScope s).scope = s

def Cedar.Spec.Var.eqEntityUID (v : Var) (uid : EntityUID) : Expr

Equations

• v.eqEntityUID uid = Cedar.Spec.Expr.binaryApp Cedar.Spec.BinaryOp.eq (Cedar.Spec.Expr.var v) (Cedar.Spec.Expr.lit (Cedar.Spec.Prim.entityUID uid))

def Cedar.Spec.Var.inEntityUID (v : Var) (uid : EntityUID) : Expr

Equations

• v.inEntityUID uid = Cedar.Spec.Expr.binaryApp Cedar.Spec.BinaryOp.mem (Cedar.Spec.Expr.var v) (Cedar.Spec.Expr.lit (Cedar.Spec.Prim.entityUID uid))

def Cedar.Spec.Var.isEntityType (v : Var) (ety : EntityType) : Expr

Equations

• v.isEntityType ety = Cedar.Spec.Expr.unaryApp (Cedar.Spec.UnaryOp.is ety) (Cedar.Spec.Expr.var v)

def Cedar.Spec.Scope.toExpr (s : Scope) (v : Var) : Expr

Equations

• Cedar.Spec.Scope.any.toExpr v = Cedar.Spec.Expr.lit (Cedar.Spec.Prim.bool true)
• (Cedar.Spec.Scope.eq uid).toExpr v = v.eqEntityUID uid
• (Cedar.Spec.Scope.mem uid).toExpr v = v.inEntityUID uid
• (Cedar.Spec.Scope.is ety).toExpr v = v.isEntityType ety
• (Cedar.Spec.Scope.isMem ety uid).toExpr v = (v.isEntityType ety).and (v.inEntityUID uid)

def Cedar.Spec.PrincipalScope.toExpr : PrincipalScope → Expr

Equations

• (Cedar.Spec.PrincipalScope.principalScope s).toExpr = s.toExpr Cedar.Spec.Var.principal

def Cedar.Spec.ResourceScope.toExpr : ResourceScope → Expr

Equations

• (Cedar.Spec.ResourceScope.resourceScope s).toExpr = s.toExpr Cedar.Spec.Var.resource

def Cedar.Spec.ActionScope.toExpr : ActionScope → Expr

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Spec.ActionScope.actionScope s).toExpr = s.toExpr Cedar.Spec.Var.action

def Cedar.Spec.Condition.toExpr (c : Condition) : Expr

Equations

• c.toExpr = match c.kind with | Cedar.Spec.ConditionKind.when => c.body | Cedar.Spec.ConditionKind.unless => Cedar.Spec.Expr.unaryApp Cedar.Spec.UnaryOp.not c.body

def Cedar.Spec.Conditions.toExpr (cs : Conditions) : Expr

Equations

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

def Cedar.Spec.Policy.toExpr (p : Policy) : Expr

Equations

• p.toExpr = p.principalScope.toExpr.and (p.actionScope.toExpr.and (p.resourceScope.toExpr.and p.condition.toExpr))

def Cedar.Spec.Scope.bound : Scope → Option EntityUID

Equations

• (Cedar.Spec.Scope.eq uid).bound = some uid
• (Cedar.Spec.Scope.mem uid).bound = some uid
• (Cedar.Spec.Scope.isMem ety uid).bound = some uid
• x✝.bound = none

def Cedar.Spec.Policy.allowAll : Policy

The trivial allow-all policy

Equations

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

def Cedar.Spec.instReprEffect.repr : Effect → Nat → Std.Format

Equations

• Cedar.Spec.instReprEffect.repr Cedar.Spec.Effect.permit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Effect.permit")).group prec✝
• Cedar.Spec.instReprEffect.repr Cedar.Spec.Effect.forbid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Effect.forbid")).group prec✝

instance Cedar.Spec.instReprEffect : Repr Effect

Equations

• Cedar.Spec.instReprEffect = { reprPrec := Cedar.Spec.instReprEffect.repr }

instance Cedar.Spec.instDecidableEqEffect : DecidableEq Effect

Equations

• Cedar.Spec.instDecidableEqEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cedar.Spec.instInhabitedEffect.default : Effect

Equations

• Cedar.Spec.instInhabitedEffect.default = Cedar.Spec.Effect.permit

instance Cedar.Spec.instInhabitedEffect : Inhabited Effect

Equations

• Cedar.Spec.instInhabitedEffect = { default := Cedar.Spec.instInhabitedEffect.default }

def Cedar.Spec.instReprConditionKind.repr : ConditionKind → Nat → Std.Format

Equations

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

instance Cedar.Spec.instReprConditionKind : Repr ConditionKind

Equations

• Cedar.Spec.instReprConditionKind = { reprPrec := Cedar.Spec.instReprConditionKind.repr }

instance Cedar.Spec.instDecidableEqConditionKind : DecidableEq ConditionKind

Equations

• Cedar.Spec.instDecidableEqConditionKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instInhabitedConditionKind : Inhabited ConditionKind

Equations

• Cedar.Spec.instInhabitedConditionKind = { default := Cedar.Spec.instInhabitedConditionKind.default }

def Cedar.Spec.instInhabitedConditionKind.default : ConditionKind

Equations

• Cedar.Spec.instInhabitedConditionKind.default = Cedar.Spec.ConditionKind.when

instance Cedar.Spec.instReprCondition : Repr Condition

Equations

• Cedar.Spec.instReprCondition = { reprPrec := Cedar.Spec.instReprCondition.repr }

def Cedar.Spec.instReprCondition.repr : Condition → Nat → Std.Format

Equations

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

instance Cedar.Spec.instDecidableEqCondition : DecidableEq Condition

Equations

• Cedar.Spec.instDecidableEqCondition = Cedar.Spec.instDecidableEqCondition.decEq

def Cedar.Spec.instDecidableEqCondition.decEq (x✝ x✝¹ : Condition) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqCondition.decEq { kind := a, body := a_1 } { kind := b, body := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Cedar.Spec.instInhabitedCondition : Inhabited Condition

Equations

• Cedar.Spec.instInhabitedCondition = { default := Cedar.Spec.instInhabitedCondition.default }

def Cedar.Spec.instInhabitedCondition.default : Condition

Equations

• Cedar.Spec.instInhabitedCondition.default = { kind := default, body := default }

instance Cedar.Spec.instReprScope : Repr Scope

Equations

• Cedar.Spec.instReprScope = { reprPrec := Cedar.Spec.instReprScope.repr }

def Cedar.Spec.instReprScope.repr : Scope → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.instReprScope.repr Cedar.Spec.Scope.any prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Scope.any")).group prec✝

def Cedar.Spec.instDecidableEqScope.decEq (x✝ x✝¹ : Scope) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqScope.decEq Cedar.Spec.Scope.any Cedar.Spec.Scope.any = isTrue ⋯
• Cedar.Spec.instDecidableEqScope.decEq Cedar.Spec.Scope.any (Cedar.Spec.Scope.eq entity) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq Cedar.Spec.Scope.any (Cedar.Spec.Scope.mem entity) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq Cedar.Spec.Scope.any (Cedar.Spec.Scope.is ety) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq Cedar.Spec.Scope.any (Cedar.Spec.Scope.isMem ety entity) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.eq entity) Cedar.Spec.Scope.any = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.eq a) (Cedar.Spec.Scope.eq b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.eq entity) (Cedar.Spec.Scope.mem entity_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.eq entity) (Cedar.Spec.Scope.is ety) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.eq entity) (Cedar.Spec.Scope.isMem ety entity_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.mem entity) Cedar.Spec.Scope.any = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.mem entity) (Cedar.Spec.Scope.eq entity_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.mem a) (Cedar.Spec.Scope.mem b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.mem entity) (Cedar.Spec.Scope.is ety) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.mem entity) (Cedar.Spec.Scope.isMem ety entity_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.is ety) Cedar.Spec.Scope.any = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.is ety) (Cedar.Spec.Scope.eq entity) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.is ety) (Cedar.Spec.Scope.mem entity) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.is a) (Cedar.Spec.Scope.is b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.is ety) (Cedar.Spec.Scope.isMem ety_1 entity) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.isMem ety entity) Cedar.Spec.Scope.any = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.isMem ety entity) (Cedar.Spec.Scope.eq entity_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.isMem ety entity) (Cedar.Spec.Scope.mem entity_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.isMem ety entity) (Cedar.Spec.Scope.is ety_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqScope.decEq (Cedar.Spec.Scope.isMem a a_1) (Cedar.Spec.Scope.isMem b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Cedar.Spec.instDecidableEqScope : DecidableEq Scope

Equations

• Cedar.Spec.instDecidableEqScope = Cedar.Spec.instDecidableEqScope.decEq

instance Cedar.Spec.instInhabitedScope : Inhabited Scope

Equations

• Cedar.Spec.instInhabitedScope = { default := Cedar.Spec.instInhabitedScope.default }

def Cedar.Spec.instInhabitedScope.default : Scope

Equations

• Cedar.Spec.instInhabitedScope.default = Cedar.Spec.Scope.any

instance Cedar.Spec.instReprPrincipalScope : Repr PrincipalScope

Equations

• Cedar.Spec.instReprPrincipalScope = { reprPrec := Cedar.Spec.instReprPrincipalScope.repr }

def Cedar.Spec.instReprPrincipalScope.repr : PrincipalScope → Nat → Std.Format

Equations

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

def Cedar.Spec.instDecidableEqPrincipalScope.decEq (x✝ x✝¹ : PrincipalScope) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqPrincipalScope.decEq (Cedar.Spec.PrincipalScope.principalScope a) (Cedar.Spec.PrincipalScope.principalScope b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instDecidableEqPrincipalScope : DecidableEq PrincipalScope

Equations

• Cedar.Spec.instDecidableEqPrincipalScope = Cedar.Spec.instDecidableEqPrincipalScope.decEq

def Cedar.Spec.instInhabitedPrincipalScope.default : PrincipalScope

Equations

• Cedar.Spec.instInhabitedPrincipalScope.default = Cedar.Spec.PrincipalScope.principalScope default

instance Cedar.Spec.instInhabitedPrincipalScope : Inhabited PrincipalScope

Equations

• Cedar.Spec.instInhabitedPrincipalScope = { default := Cedar.Spec.instInhabitedPrincipalScope.default }

instance Cedar.Spec.instReprResourceScope : Repr ResourceScope

Equations

• Cedar.Spec.instReprResourceScope = { reprPrec := Cedar.Spec.instReprResourceScope.repr }

def Cedar.Spec.instReprResourceScope.repr : ResourceScope → Nat → Std.Format

Equations

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

instance Cedar.Spec.instDecidableEqResourceScope : DecidableEq ResourceScope

Equations

• Cedar.Spec.instDecidableEqResourceScope = Cedar.Spec.instDecidableEqResourceScope.decEq

def Cedar.Spec.instDecidableEqResourceScope.decEq (x✝ x✝¹ : ResourceScope) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqResourceScope.decEq (Cedar.Spec.ResourceScope.resourceScope a) (Cedar.Spec.ResourceScope.resourceScope b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instInhabitedResourceScope : Inhabited ResourceScope

Equations

• Cedar.Spec.instInhabitedResourceScope = { default := Cedar.Spec.instInhabitedResourceScope.default }

def Cedar.Spec.instInhabitedResourceScope.default : ResourceScope

Equations

• Cedar.Spec.instInhabitedResourceScope.default = Cedar.Spec.ResourceScope.resourceScope default

def Cedar.Spec.instReprActionScope.repr : ActionScope → Nat → Std.Format

Equations

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

instance Cedar.Spec.instReprActionScope : Repr ActionScope

Equations

• Cedar.Spec.instReprActionScope = { reprPrec := Cedar.Spec.instReprActionScope.repr }

instance Cedar.Spec.instDecidableEqActionScope : DecidableEq ActionScope

Equations

• Cedar.Spec.instDecidableEqActionScope = Cedar.Spec.instDecidableEqActionScope.decEq

def Cedar.Spec.instDecidableEqActionScope.decEq (x✝ x✝¹ : ActionScope) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqActionScope.decEq (Cedar.Spec.ActionScope.actionScope a) (Cedar.Spec.ActionScope.actionScope b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqActionScope.decEq (Cedar.Spec.ActionScope.actionScope scope) (Cedar.Spec.ActionScope.actionInAny ls) = isFalse ⋯
• Cedar.Spec.instDecidableEqActionScope.decEq (Cedar.Spec.ActionScope.actionInAny ls) (Cedar.Spec.ActionScope.actionScope scope) = isFalse ⋯
• Cedar.Spec.instDecidableEqActionScope.decEq (Cedar.Spec.ActionScope.actionInAny a) (Cedar.Spec.ActionScope.actionInAny b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instInhabitedActionScope : Inhabited ActionScope

Equations

• Cedar.Spec.instInhabitedActionScope = { default := Cedar.Spec.instInhabitedActionScope.default }

def Cedar.Spec.instInhabitedActionScope.default : ActionScope

Equations

• Cedar.Spec.instInhabitedActionScope.default = Cedar.Spec.ActionScope.actionScope default

def Cedar.Spec.instReprPolicy.repr : Policy → Nat → Std.Format

Equations

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

instance Cedar.Spec.instReprPolicy : Repr Policy

Equations

• Cedar.Spec.instReprPolicy = { reprPrec := Cedar.Spec.instReprPolicy.repr }

instance Cedar.Spec.instDecidableEqPolicy : DecidableEq Policy

Equations

• Cedar.Spec.instDecidableEqPolicy = Cedar.Spec.instDecidableEqPolicy.decEq

def Cedar.Spec.instDecidableEqPolicy.decEq (x✝ x✝¹ : Policy) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.Spec.instInhabitedPolicy : Inhabited Policy

Equations

• Cedar.Spec.instInhabitedPolicy = { default := Cedar.Spec.instInhabitedPolicy.default }

def Cedar.Spec.instInhabitedPolicy.default : Policy

Equations

• Cedar.Spec.instInhabitedPolicy.default = { id := default, effect := default, principalScope := default, actionScope := default, resourceScope := default, condition := default }

instance Cedar.Spec.instToJsonPolicyID : Lean.ToJson PolicyID

Equations

• Cedar.Spec.instToJsonPolicyID = Lean.instToJsonString