This file defines the Cedar validator.

def Cedar.Validation.Schema.environments (schema : Schema) : List TypeEnv

Return every schema-defined environment.

Equations

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

def Cedar.Validation.Schema.environmentsForAction? (schema : Schema) (action : Spec.EntityUID) : Option (List TypeEnv)

Return all the schema-defined environments for a particular action, or none if this action is not declared in the schema.

Note that some ∅ means something different than none -- some ∅ means that the action was declared in the schema, but there are no valid environments for it

Equations

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

def Cedar.Validation.Schema.environment? (schema : Schema) (principal resource : Spec.EntityType) (action : Spec.EntityUID) : Option TypeEnv

Return the environment for the particular (p,a,r) tuple, or none if this is not a valid tuple in this schema

Equations

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

inductive Cedar.Validation.ValidationError : Type

• typeError (pid : Spec.PolicyID) (error : TypeError) : ValidationError
• levelError (pid : Spec.PolicyID) : ValidationError
• impossiblePolicy (pid : Spec.PolicyID) : ValidationError

instance Cedar.Validation.instReprValidationError : Repr ValidationError

Equations

• Cedar.Validation.instReprValidationError = { reprPrec := Cedar.Validation.instReprValidationError.repr }

def Cedar.Validation.instReprValidationError.repr : ValidationError → Nat → Std.Format

Equations

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

def Cedar.Validation.instBEqValidationError.beq : ValidationError → ValidationError → Bool

Equations

• Cedar.Validation.instBEqValidationError.beq (Cedar.Validation.ValidationError.typeError a a_1) (Cedar.Validation.ValidationError.typeError b b_1) = (a == b && a_1 == b_1)
• Cedar.Validation.instBEqValidationError.beq (Cedar.Validation.ValidationError.levelError a) (Cedar.Validation.ValidationError.levelError b) = (a == b)
• Cedar.Validation.instBEqValidationError.beq (Cedar.Validation.ValidationError.impossiblePolicy a) (Cedar.Validation.ValidationError.impossiblePolicy b) = (a == b)
• Cedar.Validation.instBEqValidationError.beq x✝¹ x✝ = false

instance Cedar.Validation.instBEqValidationError : BEq ValidationError

Equations

• Cedar.Validation.instBEqValidationError = { beq := Cedar.Validation.instBEqValidationError.beq }

instance Cedar.Validation.instToStringValidationError : ToString ValidationError

Equations

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

@[reducible, inline]

abbrev Cedar.Validation.ValidationResult : Type

Equations

• Cedar.Validation.ValidationResult = Except Cedar.Validation.ValidationError Unit

Check that all referenced entity types, actions, and enum entities are declared in the schema. The Lean model of typechecking also does this check, but Rust does it only as a separate pass. This means the Rust validator will report undefined entity types that the Lean typechecker ignores due to short-circuiting. We include this validation pass so that the validators behave exactly the same, but we don't need to prove anything about it for soundness.

@[irreducible]

def Cedar.Validation.checkEntities (schema : Schema) : Spec.Expr → Except TypeError Unit

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.checkEntities schema (Cedar.Spec.Expr.lit p) = Except.ok ()
• Cedar.Validation.checkEntities schema (Cedar.Spec.Expr.var v) = Except.ok ()
• Cedar.Validation.checkEntities schema (x₁.ite x₂ x₃) = do Cedar.Validation.checkEntities schema x₁ Cedar.Validation.checkEntities schema x₂ Cedar.Validation.checkEntities schema x₃
• Cedar.Validation.checkEntities schema (Cedar.Spec.Expr.binaryApp op x₁ x₂) = do Cedar.Validation.checkEntities schema x₁ Cedar.Validation.checkEntities schema x₂
• Cedar.Validation.checkEntities schema (x₁.and x₂) = do Cedar.Validation.checkEntities schema x₁ Cedar.Validation.checkEntities schema x₂
• Cedar.Validation.checkEntities schema (x₁.or x₂) = do Cedar.Validation.checkEntities schema x₁ Cedar.Validation.checkEntities schema x₂
• Cedar.Validation.checkEntities schema (x₁.getAttr attr) = Cedar.Validation.checkEntities schema x₁
• Cedar.Validation.checkEntities schema (x₁.hasAttr attr) = Cedar.Validation.checkEntities schema x₁
• Cedar.Validation.checkEntities schema (Cedar.Spec.Expr.unaryApp op x₁) = Cedar.Validation.checkEntities schema x₁
• Cedar.Validation.checkEntities schema (Cedar.Spec.Expr.set xs) = xs.attach.forM fun (x : { x : Cedar.Spec.Expr // x ∈ xs }) => have x_1 := ⋯; Cedar.Validation.checkEntities schema x.val

@[irreducible]

def Cedar.Validation.mapOnVars (f : Spec.Var → Spec.Expr) : Spec.Expr → Spec.Expr

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.mapOnVars f (Cedar.Spec.Expr.lit l) = Cedar.Spec.Expr.lit l
• Cedar.Validation.mapOnVars f (Cedar.Spec.Expr.var var) = f var
• Cedar.Validation.mapOnVars f (x₁.ite x₂ x₃) = (Cedar.Validation.mapOnVars f x₁).ite (Cedar.Validation.mapOnVars f x₂) (Cedar.Validation.mapOnVars f x₃)
• Cedar.Validation.mapOnVars f (x₁.and x₂) = (Cedar.Validation.mapOnVars f x₁).and (Cedar.Validation.mapOnVars f x₂)
• Cedar.Validation.mapOnVars f (x₁.or x₂) = (Cedar.Validation.mapOnVars f x₁).or (Cedar.Validation.mapOnVars f x₂)
• Cedar.Validation.mapOnVars f (Cedar.Spec.Expr.unaryApp op₁ x₁) = Cedar.Spec.Expr.unaryApp op₁ (Cedar.Validation.mapOnVars f x₁)
• Cedar.Validation.mapOnVars f (Cedar.Spec.Expr.binaryApp op₂ x₁ x₂) = Cedar.Spec.Expr.binaryApp op₂ (Cedar.Validation.mapOnVars f x₁) (Cedar.Validation.mapOnVars f x₂)
• Cedar.Validation.mapOnVars f (x₁.hasAttr a) = (Cedar.Validation.mapOnVars f x₁).hasAttr a
• Cedar.Validation.mapOnVars f (x₁.getAttr a) = (Cedar.Validation.mapOnVars f x₁).getAttr a

def Cedar.Validation.substituteAction (uid : Spec.EntityUID) (expr : Spec.Expr) : Spec.Expr

Equations

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

def Cedar.Validation.typecheckPolicy (policy : Spec.Policy) (env : TypeEnv) : Except ValidationError TypedExpr

Check that a policy is Boolean-typed.

Equations

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

def Cedar.Validation.typecheckPolicyWithLevel (policy : Spec.Policy) (level : Nat) (env : TypeEnv) : Except ValidationError TypedExpr

Equations

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

def Cedar.Validation.allFalse (txs : List TypedExpr) : Bool

Equations

• Cedar.Validation.allFalse txs = txs.all fun (x : Cedar.Validation.TypedExpr) => x.typeOf == Cedar.Validation.CedarType.bool Cedar.Validation.BoolType.ff

def Cedar.Validation.typecheckPolicyWithEnvironments (tc : Spec.Policy → TypeEnv → Except ValidationError TypedExpr) (policy : Spec.Policy) (schema : Schema) : ValidationResult

Check a policy under multiple environments.

Equations

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

def Cedar.Validation.validate (policies : Spec.Policies) (schema : Schema) : ValidationResult

Analyze a set of policies to check that all are boolean-typed, and that none are guaranteed to be false under all possible environments.

Equations

• Cedar.Validation.validate policies schema = List.forM policies fun (x : Cedar.Spec.Policy) => Cedar.Validation.typecheckPolicyWithEnvironments Cedar.Validation.typecheckPolicy x schema

def Cedar.Validation.validateWithLevel (policies : Spec.Policies) (schema : Schema) (level : Nat) : ValidationResult

Analyze a set of policies to check that all are boolean-typed, and that none are guaranteed to be false under all possible environments.

Equations

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

instance Cedar.Validation.instReprValidationError_1 : Repr ValidationError

Equations

• Cedar.Validation.instReprValidationError_1 = { reprPrec := Cedar.Validation.instReprValidationError_1.repr }

def Cedar.Validation.instReprValidationError_1.repr : ValidationError → Nat → Std.Format

Equations

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

def Cedar.Validation.validationErrorToJson : ValidationError → Lean.Json

Equations

• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.lubErr ty₁ ty₂)) = Lean.Json.str "lubErr"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.unexpectedType ty)) = Lean.Json.str "unexpectedType"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.attrNotFound ty attr)) = Lean.Json.str "attrNotFound"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.tagNotFound ety tag)) = Lean.Json.str "tagNotFound"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.unknownEntity ety)) = Lean.Json.str "unknownEntity"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.extensionErr xs)) = Lean.Json.str "extensionErr"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid Cedar.Validation.TypeError.emptySetErr) = Lean.Json.str "emptySetErr"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.typeError pid (Cedar.Validation.TypeError.incompatibleSetTypes ty)) = Lean.Json.str "incompatibleSetTypes"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.levelError pid) = Lean.Json.str "levelError"
• Cedar.Validation.validationErrorToJson (Cedar.Validation.ValidationError.impossiblePolicy pid) = Lean.Json.str "impossiblePolicy"

instance Cedar.Validation.instToJsonValidationError : Lean.ToJson ValidationError

Equations

• Cedar.Validation.instToJsonValidationError = { toJson := Cedar.Validation.validationErrorToJson }

instance Cedar.Validation.instToJsonExcept_cedar {ε✝ : Type u_1} {α✝ : Type u_2} [Lean.ToJson ε✝] [Lean.ToJson α✝] : Lean.ToJson (Except ε✝ α✝)

Equations

• Cedar.Validation.instToJsonExcept_cedar = { toJson := Cedar.Validation.instToJsonExcept_cedar.toJson }

def Cedar.Validation.instToJsonExcept_cedar.toJson {ε✝ : Type u_1} {α✝ : Type u_2} [Lean.ToJson ε✝] [Lean.ToJson α✝] : Except ε✝ α✝ → Lean.Json

Equations

• Cedar.Validation.instToJsonExcept_cedar.toJson (Except.error a) = Lean.Json.mkObj [("error", Lean.toJson a)]
• Cedar.Validation.instToJsonExcept_cedar.toJson (Except.ok a) = Lean.Json.mkObj [("ok", Lean.toJson a)]

instance Cedar.Validation.instToJsonUnit_cedar : Lean.ToJson Unit

Equations

• Cedar.Validation.instToJsonUnit_cedar = { toJson := fun (x : Unit) => Lean.Json.null }