This file defines the Cedar symbolic compiler.

The symbolic compiler takes as input a Cedar expression and a symbolic environment. Given these inputs, it produces a Term encoding of the expression.

If the compiler returns a Term, this Term represents a sound and complete encoding of the input expression's semantics with respect to the given environment: using this Term for verification will neither miss bugs (soundness) nor produce false positives (completeness).

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

Equations

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

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

Equations

• Cedar.SymCC.compileVar Cedar.Spec.Var.principal req = if req.principal.typeOf.isEntityType = true then Except.ok (⊙req.principal) else Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileVar Cedar.Spec.Var.action req = if req.action.typeOf.isEntityType = true then Except.ok (⊙req.action) else Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileVar Cedar.Spec.Var.resource req = if req.resource.typeOf.isEntityType = true then Except.ok (⊙req.resource) else Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileVar Cedar.Spec.Var.context req = if req.context.typeOf.isRecordType = true then Except.ok (⊙req.context) else Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.compileApp₁ (op₁ : Spec.UnaryOp) (t : Term) : Result Term

Equations

• Cedar.SymCC.compileApp₁ Cedar.Spec.UnaryOp.not t = Except.ok (⊙Cedar.SymCC.Factory.not t)
• Cedar.SymCC.compileApp₁ Cedar.Spec.UnaryOp.neg t = Except.ok (Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvnego t) (Cedar.SymCC.Factory.bvneg t))
• Cedar.SymCC.compileApp₁ (Cedar.Spec.UnaryOp.like p) t = Except.ok (⊙Cedar.SymCC.Factory.string.like t p)
• Cedar.SymCC.compileApp₁ (Cedar.Spec.UnaryOp.is ety₁) t = Except.ok (⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool (decide (ety₁ = ety₂))))
• Cedar.SymCC.compileApp₁ Cedar.Spec.UnaryOp.isEmpty t = Except.ok (⊙Cedar.SymCC.Factory.set.isEmpty t)
• Cedar.SymCC.compileApp₁ op₁✝ t = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.reducibleEq (ty₁ ty₂ : TermType) : Result Bool

Equations

• Cedar.SymCC.reducibleEq ty₁ ty₂ = if ty₁ = ty₂ then Except.ok true else if (ty₁.isPrimType && ty₂.isPrimType) = true then Except.ok false else Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.compileInₑ (t₁ t₂ : Term) (ancs? : Option UnaryFunction) : Term

Equations

• Cedar.SymCC.compileInₑ t₁ t₂ ancs? = Cedar.SymCC.Factory.or (Cedar.SymCC.compileInₑ.isEq t₁ t₂) (Cedar.SymCC.compileInₑ.isIn t₁ t₂ ancs?)

def Cedar.SymCC.compileInₑ.isEq (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.compileInₑ.isEq t₁ t₂ = if t₁.typeOf = t₂.typeOf then Cedar.SymCC.Factory.eq t₁ t₂ else Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

def Cedar.SymCC.compileInₑ.isIn (t₁ t₂ : Term) (ancs? : Option UnaryFunction) : Term

Equations

• Cedar.SymCC.compileInₑ.isIn t₁ t₂ (some ancs) = Cedar.SymCC.Factory.set.member t₂ (Cedar.SymCC.Factory.app ancs t₁)
• Cedar.SymCC.compileInₑ.isIn t₁ t₂ ancs? = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

def Cedar.SymCC.compileInₛ (t ts : Term) (ancs? : Option UnaryFunction) : Term

Equations

• Cedar.SymCC.compileInₛ t ts ancs? = Cedar.SymCC.Factory.or (Cedar.SymCC.compileInₛ.isIn₁ t ts) (Cedar.SymCC.compileInₛ.isIn₂ t ts ancs?)

def Cedar.SymCC.compileInₛ.isIn₁ (t ts : Term) : Term

Equations

• Cedar.SymCC.compileInₛ.isIn₁ t ts = if ts.typeOf = t.typeOf.set then Cedar.SymCC.Factory.set.member t ts else Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

def Cedar.SymCC.compileInₛ.isIn₂ (t ts : Term) (ancs? : Option UnaryFunction) : Term

Equations

• Cedar.SymCC.compileInₛ.isIn₂ t ts (some ancs) = Cedar.SymCC.Factory.set.intersects ts (Cedar.SymCC.Factory.app ancs t)
• Cedar.SymCC.compileInₛ.isIn₂ t ts ancs? = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

def Cedar.SymCC.compileHasTag (entity tag : Term) : Option (Option SymTags) → Result Term

Equations

• Cedar.SymCC.compileHasTag entity tag none = Except.error Cedar.SymCC.Error.noSuchEntityType
• Cedar.SymCC.compileHasTag entity tag (some none) = Except.ok (⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false))
• Cedar.SymCC.compileHasTag entity tag (some (some τs)) = Except.ok (⊙τs.hasTag entity tag)

def Cedar.SymCC.compileGetTag (entity tag : Term) : Option (Option SymTags) → Result Term

Equations

• Cedar.SymCC.compileGetTag entity tag none = Except.error Cedar.SymCC.Error.noSuchEntityType
• Cedar.SymCC.compileGetTag entity tag (some none) = Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileGetTag entity tag (some (some τs)) = Except.ok (τs.getTag entity tag)

def Cedar.SymCC.compileApp₂ (op₂ : Spec.BinaryOp) (t₁ t₂ : Term) (εs : SymEntities) : Result Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.less t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.Factory.bvslt t₁ t₂)
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.less t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.Factory.bvslt (Cedar.SymCC.Factory.ext.datetime.val t₁) (Cedar.SymCC.Factory.ext.datetime.val t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.less t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.Factory.bvslt (Cedar.SymCC.Factory.ext.duration.val t₁) (Cedar.SymCC.Factory.ext.duration.val t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.lessEq t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.Factory.bvsle t₁ t₂)
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.lessEq t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.Factory.bvsle (Cedar.SymCC.Factory.ext.datetime.val t₁) (Cedar.SymCC.Factory.ext.datetime.val t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.lessEq t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.Factory.bvsle (Cedar.SymCC.Factory.ext.duration.val t₁) (Cedar.SymCC.Factory.ext.duration.val t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.add t₁ t₂ εs = Except.ok (Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvsaddo t₁ t₂) (Cedar.SymCC.Factory.bvadd t₁ t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.sub t₁ t₂ εs = Except.ok (Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvssubo t₁ t₂) (Cedar.SymCC.Factory.bvsub t₁ t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.mul t₁ t₂ εs = Except.ok (Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvsmulo t₁ t₂) (Cedar.SymCC.Factory.bvmul t₁ t₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.contains t₁ t₂ εs = if ty₁ = t₂.typeOf then Except.ok (⊙Cedar.SymCC.Factory.set.member t₂ t₁) else Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.containsAll t₁ t₂ εs = if ty₁ = ty₂ then Except.ok (⊙Cedar.SymCC.Factory.set.subset t₂ t₁) else Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.containsAny t₁ t₂ εs = if ty₁ = ty₂ then Except.ok (⊙Cedar.SymCC.Factory.set.intersects t₁ t₂) else Except.error Cedar.SymCC.Error.typeError
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.mem t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.compileInₑ t₁ t₂ (εs.ancestorsOfType ety₁ ety₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.mem t₁ t₂ εs = Except.ok (⊙Cedar.SymCC.compileInₛ t₁ t₂ (εs.ancestorsOfType ety₁ ety₂))
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.hasTag t₁ t₂ εs = Cedar.SymCC.compileHasTag t₁ t₂ (εs.tags ety)
• Cedar.SymCC.compileApp₂ Cedar.Spec.BinaryOp.getTag t₁ t₂ εs = Cedar.SymCC.compileGetTag t₁ t₂ (εs.tags ety)
• Cedar.SymCC.compileApp₂ op₂✝ t₁ t₂ εs = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.compileAttrsOf (t : Term) (εs : SymEntities) : Result Term

Equations

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

def Cedar.SymCC.compileHasAttr (t : Term) (a : Spec.Attr) (εs : SymEntities) : Result Term

Equations

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

def Cedar.SymCC.compileGetAttr (t : Term) (a : Spec.Attr) (εs : SymEntities) : Result Term

Equations

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

def Cedar.SymCC.compileIf (t₁ : Term) (r₂ r₃ : Result Term) : Result Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.compileIf (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true)).some r₂ r₃ = r₂
• Cedar.SymCC.compileIf (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)).some r₂ r₃ = r₃
• Cedar.SymCC.compileIf t₁✝ r₂ r₃ = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.compileAnd (t₁ : Term) (r₂ : Result Term) : Result Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.compileAnd (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)).some r₂ = Except.ok (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)).some
• Cedar.SymCC.compileAnd t₁✝ r₂ = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.compileOr (t₁ : Term) (r₂ : Result Term) : Result Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.compileOr (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true)).some r₂ = Except.ok (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true)).some
• Cedar.SymCC.compileOr t₁✝ r₂ = Except.error Cedar.SymCC.Error.typeError

def Cedar.SymCC.compileExtHasAttr (t : Term) (as : List Spec.Attr) (εs : SymEntities) : Result Term

This is an iterative implementation of the compilation of extended has. We also define a proved equivalent recursive implementation in Cedar.Thm.SymCC.Compiler.ExtHasAttrRec that is easier to use in proofs.

Equations

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

def Cedar.SymCC.compileExtHasAttr.loop (εs : SymEntities) (current : Term) (as : List Spec.Attr) (acc : List Term) : Result (List Term)

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.compileExtHasAttr.loop εs current [] acc = Except.ok acc.reverse

def Cedar.SymCC.compileSet (ts : List Term) : Result Term

Equations

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

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

Equations

• Cedar.SymCC.compileRecord ats = Cedar.SymCC.Factory.ifAllSome (List.map Prod.snd ats) (⊙Cedar.SymCC.Factory.recordOf (List.map (Prod.map id Cedar.SymCC.Factory.option.get) ats))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Cedar.SymCC.compileCallₙ (xty : Validation.ExtType) (enc : Term → List Term → Term) (t : Term) (ts : List Term) : Result Term

Variadic version of compileCall₂ for a non-erroring call whose target t and all arguments ts share extension type xty. Errors (.typeError) unless every term has type .option (.ext xty); otherwise encodes enc under nested ifSome guards so that a .none in any position propagates as .none, mirroring the concrete evaluator's error propagation.

Equations

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

def Cedar.SymCC.compileCall (xfn : Spec.ExtFun) (ts : List Term) : Result Term

Equations

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

@[irreducible]

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

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.compile (Cedar.Spec.Expr.lit l) εnv = Cedar.SymCC.compilePrim l εnv.entities
• Cedar.SymCC.compile (Cedar.Spec.Expr.var v) εnv = Cedar.SymCC.compileVar v εnv.request
• Cedar.SymCC.compile (x₁.ite x₂ x₃) εnv = do let __do_lift ← Cedar.SymCC.compile x₁ εnv Cedar.SymCC.compileIf __do_lift (Cedar.SymCC.compile x₂ εnv) (Cedar.SymCC.compile x₃ εnv)
• Cedar.SymCC.compile (x₁.and x₂) εnv = do let __do_lift ← Cedar.SymCC.compile x₁ εnv Cedar.SymCC.compileAnd __do_lift (Cedar.SymCC.compile x₂ εnv)
• Cedar.SymCC.compile (x₁.or x₂) εnv = do let __do_lift ← Cedar.SymCC.compile x₁ εnv Cedar.SymCC.compileOr __do_lift (Cedar.SymCC.compile x₂ εnv)
• Cedar.SymCC.compile (x_2.extHasAttr a as) εnv = do let t ← Cedar.SymCC.compile x_2 εnv Cedar.SymCC.compileExtHasAttr t (a :: as) εnv.entities