This file defines an optimized Cedar symbolic compiler, which computes the actual compiled Term and the footprint simultaneously, avoiding the inefficiencies in the footprint function in SymCC/Enforcer.lean, which repeatedly calls compile on certain subexpressions, making it quadratic or worse in policy size, at least for certain policies.

For notes on the meaning of compile or footprint, see SymCC/Compiler.lean and SymCC/Enforcer.lean, which have clearer, unoptimized implementations.

structure Cedar.SymCC.Opt.CompileResult : Type

Structure returned by the optimized compiler, as opposed to the unoptimized compiler which just produces a Term

• term : Term

  Well-formed term of the appropriate type, representing the compiled expression

• footprint : Data.Set Term

  The "footprint" of the compiled expression.

  This is the terms corresponding to subexpressions of the compiled expression of the following form:

  • A variable term with an entity type
  • An entity reference literal
  • An attribute access expression with an entity type
  • A binary (getTag) expression with an entity type

  These are the only basic expressions in Cedar that may evaluate to an entity. All other expressions that evaluate to an entity are built up from the above basic expresions.

  All terms in the footprint are of type TermType.option .entity.

def Cedar.SymCC.Opt.CompileResult.mapTerm (f : Term → Term) : CompileResult → CompileResult

Map on the Term, leaving the footprint unchanged

Equations

• Cedar.SymCC.Opt.CompileResult.mapTerm f { term := term, footprint := footprint } = { term := f term, footprint := footprint }

def Cedar.SymCC.Opt.directFootprint (t : Term) : Data.Set Term

Return the footprint of this compiled term itself (not counting its subexpressions). Only terms of option-entity type have any direct footprint.

This corresponds to ofEntity in the footprint function in SymCC/Enforcer.lean, except that we only call it when compiling to Term was successful, so it takes a Term argument rather than Result Term.

Equations

• Cedar.SymCC.Opt.directFootprint t = if t.typeOf.isOptionEntityType = true then Cedar.Data.Set.singleton t else Cedar.Data.Set.empty

def Cedar.SymCC.Opt.compilePrim (p : Spec.Prim) (εs : SymEntities) : Result CompileResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compilePrim (Cedar.Spec.Prim.bool b) εs = Except.ok { term := ⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool b), footprint := ∅ }
• Cedar.SymCC.Opt.compilePrim (Cedar.Spec.Prim.int i) εs = Except.ok { term := ⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec i.toBitVec), footprint := ∅ }
• Cedar.SymCC.Opt.compilePrim (Cedar.Spec.Prim.string s) εs = Except.ok { term := ⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.string s), footprint := ∅ }

def Cedar.SymCC.Opt.compileVar (v : Spec.Var) (req : SymRequest) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileApp₁ (op₁ : Spec.UnaryOp) (arg : CompileResult) : Result CompileResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compileApp₁ Cedar.Spec.UnaryOp.not arg = Except.ok (Cedar.SymCC.Opt.CompileResult.mapTerm (fun (term : Cedar.SymCC.Term) => ⊙Cedar.SymCC.Factory.not term) arg)
• Cedar.SymCC.Opt.compileApp₁ Cedar.Spec.UnaryOp.isEmpty arg = Except.ok (Cedar.SymCC.Opt.CompileResult.mapTerm (fun (term : Cedar.SymCC.Term) => ⊙Cedar.SymCC.Factory.set.isEmpty term) arg)
• Cedar.SymCC.Opt.compileApp₁ op₁✝ arg = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.Opt.compileApp₂ (op₂ : Spec.BinaryOp) (arg₁ arg₂ : CompileResult) (εs : SymEntities) : Result CompileResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compileApp₂ op₂✝ arg₁ arg₂ εs = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.Opt.compileHasAttr (arg : CompileResult) (a : Spec.Attr) (εs : SymEntities) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileGetAttr (arg : CompileResult) (a : Spec.Attr) (εs : SymEntities) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileIf (arg₁ : CompileResult) (arg₂ arg₃ : Result CompileResult) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileAnd (arg₁ : CompileResult) (arg₂ : Result CompileResult) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileOr (arg₁ : CompileResult) (arg₂ : Result CompileResult) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileSet (args : List CompileResult) : Result CompileResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compileSet [] = Except.error Cedar.SymCC.Error.unsupportedError

def Cedar.SymCC.Opt.compileRecord (ats : List (Spec.Attr × CompileResult)) : CompileResult

Equations

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

def Cedar.SymCC.Opt.compileCall₀ {α : Type u_1} [Coe α Spec.Ext] (mk : String → Option α) : CompileResult → Result CompileResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compileCall₀ mk x✝ = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.Opt.compileCallWithError₁ (xty : Validation.ExtType) (enc : Term → Term) (arg₁ : CompileResult) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileCall₁ (xty : Validation.ExtType) (enc : Term → Term) (arg₁ : CompileResult) : Result CompileResult

Equations

• Cedar.SymCC.Opt.compileCall₁ xty enc arg₁ = Cedar.SymCC.Opt.compileCallWithError₁ xty (fun (t₁ : Cedar.SymCC.Term) => ⊙enc t₁) arg₁

def Cedar.SymCC.Opt.compileCallWithError₂ (xty₁ xty₂ : Validation.ExtType) (enc : Term → Term → Term) (arg₁ arg₂ : CompileResult) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.compileCall₂ (xty : Validation.ExtType) (enc : Term → Term → Term) (arg₁ arg₂ : CompileResult) : Result CompileResult

Equations

• Cedar.SymCC.Opt.compileCall₂ xty enc arg₁ arg₂ = Cedar.SymCC.Opt.compileCallWithError₂ xty xty (fun (t₁ t₂ : Cedar.SymCC.Term) => ⊙enc t₁ t₂) arg₁ arg₂

def Cedar.SymCC.Opt.compileCall (xfn : Spec.ExtFun) (args : List CompileResult) : Result CompileResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.decimal [t₁] = Cedar.SymCC.Opt.compileCall₀ Cedar.Spec.Ext.Decimal.decimal t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.lessThan [t₁, t₂] = Cedar.SymCC.Opt.compileCall₂ Cedar.Validation.ExtType.decimal Cedar.SymCC.Decimal.lessThan t₁ t₂
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.lessThanOrEqual [t₁, t₂] = Cedar.SymCC.Opt.compileCall₂ Cedar.Validation.ExtType.decimal Cedar.SymCC.Decimal.lessThanOrEqual t₁ t₂
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.greaterThan [t₁, t₂] = Cedar.SymCC.Opt.compileCall₂ Cedar.Validation.ExtType.decimal Cedar.SymCC.Decimal.greaterThan t₁ t₂
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.greaterThanOrEqual [t₁, t₂] = Cedar.SymCC.Opt.compileCall₂ Cedar.Validation.ExtType.decimal Cedar.SymCC.Decimal.greaterThanOrEqual t₁ t₂
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.ip [t₁] = Cedar.SymCC.Opt.compileCall₀ Cedar.Spec.Ext.IPAddr.ip t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.isIpv4 [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.ipAddr Cedar.SymCC.IPAddr.isIpv4 t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.isIpv6 [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.ipAddr Cedar.SymCC.IPAddr.isIpv6 t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.isLoopback [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.ipAddr Cedar.SymCC.IPAddr.isLoopback t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.isMulticast [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.ipAddr Cedar.SymCC.IPAddr.isMulticast t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.isInRange [t₁, t₂] = Cedar.SymCC.Opt.compileCall₂ Cedar.Validation.ExtType.ipAddr Cedar.SymCC.IPAddr.isInRange t₁ t₂
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.datetime [t₁] = Cedar.SymCC.Opt.compileCall₀ Cedar.Spec.Ext.Datetime.datetime t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.duration [t₁] = Cedar.SymCC.Opt.compileCall₀ Cedar.Spec.Ext.Datetime.duration t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toDate [t₁] = Cedar.SymCC.Opt.compileCallWithError₁ Cedar.Validation.ExtType.datetime Cedar.SymCC.Datetime.toDate t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toTime [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.datetime Cedar.SymCC.Datetime.toTime t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toMilliseconds [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.duration Cedar.SymCC.Duration.toMilliseconds t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toSeconds [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.duration Cedar.SymCC.Duration.toSeconds t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toMinutes [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.duration Cedar.SymCC.Duration.toMinutes t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toHours [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.duration Cedar.SymCC.Duration.toHours t₁
• Cedar.SymCC.Opt.compileCall Cedar.Spec.ExtFun.toDays [t₁] = Cedar.SymCC.Opt.compileCall₁ Cedar.Validation.ExtType.duration Cedar.SymCC.Duration.toDays t₁
• Cedar.SymCC.Opt.compileCall xfn args = Except.error Cedar.SymCC.Error.typeError

@[irreducible]

def Cedar.SymCC.Opt.compile (x : Spec.Expr) (εnv : SymEnv) : Result CompileResult

Given an expression x that has type τ with respect to a type environment Γ, and given a well-formed symbolic environment εnv that conforms to Γ, compile x εnv succeeds and produces a well-formed term of type .option τ.toTermType.

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Opt.compile (Cedar.Spec.Expr.lit l) εnv = Cedar.SymCC.Opt.compilePrim l εnv.entities
• Cedar.SymCC.Opt.compile (Cedar.Spec.Expr.var v) εnv = Cedar.SymCC.Opt.compileVar v εnv.request
• Cedar.SymCC.Opt.compile (x₁.and x₂) εnv = do let __do_lift ← Cedar.SymCC.Opt.compile x₁ εnv Cedar.SymCC.Opt.compileAnd __do_lift (Cedar.SymCC.Opt.compile x₂ εnv)
• Cedar.SymCC.Opt.compile (x₁.or x₂) εnv = do let __do_lift ← Cedar.SymCC.Opt.compile x₁ εnv Cedar.SymCC.Opt.compileOr __do_lift (Cedar.SymCC.Opt.compile x₂ εnv)