This file contains the symbolic encoding (factory functions) for extension operators.

The extension functions are total. If given well-formed and type-correct arguments, an extension function will return a well-formed and type-correct output. Otherwise, the output is an arbitrary term.

This design lets us minimize the number of error paths in the overall specification of symbolic compilation, which makes for nicer code and proofs, and it more closely tracks the specification of the concrete evaluator.

See Compiler.lean to see how the symbolic compiler uses this API. See also Factory.lean.

def Cedar.SymCC.Decimal.lessThan (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Decimal.lessThan t₁ t₂ = Cedar.SymCC.Factory.bvslt (Cedar.SymCC.Factory.ext.decimal.val t₁) (Cedar.SymCC.Factory.ext.decimal.val t₂)

def Cedar.SymCC.Decimal.lessThanOrEqual (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Decimal.lessThanOrEqual t₁ t₂ = Cedar.SymCC.Factory.bvsle (Cedar.SymCC.Factory.ext.decimal.val t₁) (Cedar.SymCC.Factory.ext.decimal.val t₂)

def Cedar.SymCC.Decimal.greaterThan (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Decimal.greaterThan t₁ t₂ = Cedar.SymCC.Decimal.lessThan t₂ t₁

def Cedar.SymCC.Decimal.greaterThanOrEqual (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Decimal.greaterThanOrEqual t₁ t₂ = Cedar.SymCC.Decimal.lessThanOrEqual t₂ t₁

def Cedar.SymCC.IPAddr.isIpv4 (t : Term) : Term

Equations

• Cedar.SymCC.IPAddr.isIpv4 t = Cedar.SymCC.Factory.ext.ipaddr.isV4 t

def Cedar.SymCC.IPAddr.isIpv6 (t : Term) : Term

Equations

• Cedar.SymCC.IPAddr.isIpv6 t = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.ext.ipaddr.isV4 t)

def Cedar.SymCC.IPAddr.subnetWidth (w : Nat) (ipPre : Term) : Term

Equations

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

def Cedar.SymCC.IPAddr.range (w : Nat) (ipAddr ipPre : Term) : Term × Term

Equations

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

def Cedar.SymCC.IPAddr.rangeV4 (t : Term) : Term × Term

Equations

• Cedar.SymCC.IPAddr.rangeV4 t = Cedar.SymCC.IPAddr.range 5 (Cedar.SymCC.Factory.ext.ipaddr.addrV4 t) (Cedar.SymCC.Factory.ext.ipaddr.prefixV4 t)

def Cedar.SymCC.IPAddr.rangeV6 (t : Term) : Term × Term

Equations

• Cedar.SymCC.IPAddr.rangeV6 t = Cedar.SymCC.IPAddr.range 7 (Cedar.SymCC.Factory.ext.ipaddr.addrV6 t) (Cedar.SymCC.Factory.ext.ipaddr.prefixV6 t)

def Cedar.SymCC.IPAddr.inRange (range : Term → Term × Term) (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.IPAddr.inRange range t₁ t₂ = Cedar.SymCC.Factory.and (Cedar.SymCC.Factory.bvule (range t₁).snd (range t₂).snd) (Cedar.SymCC.Factory.bvule (range t₂).fst (range t₁).fst)

def Cedar.SymCC.IPAddr.inRangeV (isIp : Term → Term) (range : Term → Term × Term) (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.IPAddr.inRangeV isIp range t₁ t₂ = Cedar.SymCC.Factory.and (isIp t₁) (Cedar.SymCC.Factory.and (isIp t₂) (Cedar.SymCC.IPAddr.inRange range t₁ t₂))

def Cedar.SymCC.IPAddr.isInRange (t₁ t₂ : Term) : Term

Equations

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

def Cedar.SymCC.IPAddr.inRangeVs (isIp : Term → Term) (range : Term → Term × Term) (t : Term) (ts : List Term) : Term

Variadic inRangeV: t is isIp and in range of any of ts (each of which must also be isIp). Left-folds the per-range checks with or.

Equations

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

def Cedar.SymCC.IPAddr.isInRangeV (t₁ : Term) (ts : List Term) : Term

Variadic isInRange: t₁ is in range of any of ts. A single top-level or of the ipv4 and ipv6 inRangeVs checks, each folding over all ranges. With a single range this reduces to the binary isInRange.

Equations

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

def Cedar.SymCC.IPAddr.ipTerm (ip : Spec.IPAddr) : Term

Equations

• Cedar.SymCC.IPAddr.ipTerm ip = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.ext (Cedar.Spec.Ext.ipaddr ip))

def Cedar.SymCC.IPAddr.inRangeLit (t : Term) (cidr₄ : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH) (cidr₆ : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH) : Term

Equations

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

def Cedar.SymCC.IPAddr.isLoopback (t : Term) : Term

Equations

• Cedar.SymCC.IPAddr.isLoopback t = Cedar.SymCC.IPAddr.inRangeLit t Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V4 Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V6

def Cedar.SymCC.IPAddr.isMulticast (t : Term) : Term

Equations

• Cedar.SymCC.IPAddr.isMulticast t = Cedar.SymCC.IPAddr.inRangeLit t Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V4 Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V6

def Cedar.SymCC.Duration.toMilliseconds (t : Term) : Term

Equations

• Cedar.SymCC.Duration.toMilliseconds t = Cedar.SymCC.Factory.ext.duration.val t

def Cedar.SymCC.Duration.toSeconds (t : Term) : Term

Equations

• Cedar.SymCC.Duration.toSeconds t = Cedar.SymCC.Factory.bvsdiv (Cedar.SymCC.Duration.toMilliseconds t) (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec (Int64.toBitVec 1000)))

def Cedar.SymCC.Duration.toMinutes (t : Term) : Term

Equations

• Cedar.SymCC.Duration.toMinutes t = Cedar.SymCC.Factory.bvsdiv (Cedar.SymCC.Duration.toSeconds t) (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec (Int64.toBitVec 60)))

def Cedar.SymCC.Duration.toHours (t : Term) : Term

Equations

• Cedar.SymCC.Duration.toHours t = Cedar.SymCC.Factory.bvsdiv (Cedar.SymCC.Duration.toMinutes t) (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec (Int64.toBitVec 60)))

def Cedar.SymCC.Duration.toDays (t : Term) : Term

Equations

• Cedar.SymCC.Duration.toDays t = Cedar.SymCC.Factory.bvsdiv (Cedar.SymCC.Duration.toHours t) (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec (Int64.toBitVec 24)))

def Cedar.SymCC.Datetime.offset (dt dur : Term) : Term

Equations

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

def Cedar.SymCC.Datetime.durationSince (dt₁ dt₂ : Term) : Term

Equations

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

def Cedar.SymCC.Datetime.toDate (dt : Term) : Term

Equations

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

def Cedar.SymCC.Datetime.toTime (dt : Term) : Term

Equations

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