def Actus.Contract.LAX.accr {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : α

Interest accrued over [Sd, t] on the current notional.

Equations

• Actus.Contract.LAX.accr rf t s = s.ipac + s.nt * s.ipnr * rf.yf s.sd t

def Actus.Contract.LAX.stf_IED {α : Type} [Amount α] (ct : Terms α) (t : Protocol.Time) (s : State α) : State α

Initial exchange: take on the signed notional and the nominal rate.

Equations

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

def Actus.Contract.LAX.stf_IP {α : Type} [Amount α] (t : Protocol.Time) (s : State α) : State α

Interest payment: pay the accrued interest, reset the accrual.

Equations

• Actus.Contract.LAX.stf_IP t s = { md := s.md, nt := s.nt, ipnr := s.ipnr, ipac := 0, feac := s.feac, nsc := s.nsc, isc := s.isc, prnxt := s.prnxt, ipcb := s.ipcb, prf := s.prf, sd := t }

def Actus.Contract.LAX.stf_PR {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (x : α) (t : Protocol.Time) (s : State α) : State α

Principal redemption: reduce the notional by the (signed) instalment x, capitalizing the interest accrued so far.

Equations

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

def Actus.Contract.LAX.stf_PI {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (x : α) (t : Protocol.Time) (s : State α) : State α

Principal increase (draw): grow the notional by the (signed) draw x.

Equations

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

def Actus.Contract.LAX.stf_MD {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : State α

Maturity: pay out the residual notional.

Equations

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

def Actus.Contract.LAX.stf_reset {α : Type} [Amount α] (rf : RiskFactorEnv α) (x : α) (t : Protocol.Time) (s : State α) : State α

Rate reset (RR/RRF): set the rate to the payload x (already resolved by schedule generation: the fixed rate for RRF, the observed market rate for RR).

Equations

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

def Actus.Contract.LAX.stf {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (e : Protocol.EventType) (x : α) (t : Protocol.Time) (s : State α) : State α

STF dispatcher. Out-of-schedule events accrue and advance the clock.

Equations

• One or more equations did not get rendered due to their size.
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.IED x t s = Actus.Contract.LAX.stf_IED ct t s
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.IP x t s = Actus.Contract.LAX.stf_IP t s
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.PR x t s = Actus.Contract.LAX.stf_PR ct rf x t s
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.PI x t s = Actus.Contract.LAX.stf_PI ct rf x t s
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.MD x t s = Actus.Contract.LAX.stf_MD rf t s
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.RRF x t s = Actus.Contract.LAX.stf_reset rf x t s
• Actus.Contract.LAX.stf ct rf Actus.Protocol.EventType.RR x t s = Actus.Contract.LAX.stf_reset rf x t s

def Actus.Contract.LAX.pof_IED {α : Type} [Amount α] (ct : Terms α) : α

Equations

• Actus.Contract.LAX.pof_IED ct = Actus.Util.Conventions.sign ct.cntrl * -1 * (ct.nt + ct.premiumDiscountAtIED.getD 0)

def Actus.Contract.LAX.pof_IP {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : α

Equations

• Actus.Contract.LAX.pof_IP rf t s = Actus.Contract.LAX.accr rf t s

def Actus.Contract.LAX.pof_PR {α : Type} [Amount α] (ct : Terms α) (x : α) : α

Equations

• Actus.Contract.LAX.pof_PR ct x = Actus.Util.Conventions.sign ct.cntrl * x

def Actus.Contract.LAX.pof_PI {α : Type} [Amount α] (ct : Terms α) (x : α) : α

Equations

• Actus.Contract.LAX.pof_PI ct x = Actus.Util.Conventions.sign ct.cntrl * -1 * x

def Actus.Contract.LAX.pof_MD {α : Type} (s : State α) : α

Equations

• Actus.Contract.LAX.pof_MD s = s.nt

def Actus.Contract.LAX.pof {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (e : Protocol.EventType) (x : α) (t : Protocol.Time) (s : State α) : α

Equations

• Actus.Contract.LAX.pof ct rf Actus.Protocol.EventType.IED x t s = Actus.Contract.LAX.pof_IED ct
• Actus.Contract.LAX.pof ct rf Actus.Protocol.EventType.IP x t s = Actus.Contract.LAX.pof_IP rf t s
• Actus.Contract.LAX.pof ct rf Actus.Protocol.EventType.PR x t s = Actus.Contract.LAX.pof_PR ct x
• Actus.Contract.LAX.pof ct rf Actus.Protocol.EventType.PI x t s = Actus.Contract.LAX.pof_PI ct x
• Actus.Contract.LAX.pof ct rf Actus.Protocol.EventType.MD x t s = Actus.Contract.LAX.pof_MD s
• Actus.Contract.LAX.pof ct rf e x t s = 0

def Actus.Contract.LAX.init {α : Type} [Amount α] (ct : Terms α) (iedT : Protocol.Time) : State α

State just before the IED event (which stf_IED re-establishes).

Equations

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

inductive Actus.Contract.LAX.Step {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

One-step LAX transition. The constructor carries the event e and its schedule payload x, and targets the dispatcher stf.

• ev {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) (x : α) {t : Protocol.Time} : s.sd ≤ t → Step ct rf s (stf ct rf e x t s)

@[reducible, inline]

abbrev Actus.Contract.LAX.Trace {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

Equations

• Actus.Contract.LAX.Trace ct rf = Actus.Closures.Star (Actus.Contract.LAX.Step ct rf)

def Actus.Contract.LAX.getCashflow {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} (h : Step ct rf s s') : Protocol.Event × α

Equations

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

def Actus.Contract.LAX.getCashflows {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} : Trace ct rf s s' → List (Protocol.Event × α)

Equations

• Actus.Contract.LAX.getCashflows ct rf Actus.Closures.Star.refl = []
• Actus.Contract.LAX.getCashflows ct rf (Actus.Closures.Star.step h rest) = Actus.Contract.LAX.getCashflow ct rf h :: Actus.Contract.LAX.getCashflows ct rf rest

def Actus.Contract.LAX.LAX_contract : Abstract.ActusContract

Equations

• Actus.Contract.LAX.LAX_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.LAX.LAX_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition LAX_contract

Equations

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

def Actus.Contract.Execution.getI {α : Type} (l : List α) (i : ℕ) (d : α) : α

Indexed lookup with a default.

Equations

• Actus.Contract.Execution.getI l i d = l[i]?.getD d

def Actus.Contract.Execution.laxRun (ct : Terms Float) (rf : RiskFactorEnv Float) : State Float → List (Protocol.Time × Protocol.EventType × Float) → Protocol.Cashflows

Fold LAX.stf/LAX.pof over a payloaded event list (time, event, x), where x is the redemption amount (PR/PI) or new rate (RR/RRF).

Equations

• One or more equations did not get rendered due to their size.
• Actus.Contract.Execution.laxRun ct rf x✝ [] = []

def Actus.Contract.Execution.laxCashflows (ct : Terms Float) (rf : RiskFactorEnv Float) : Protocol.Cashflows

LAX — build the array-derived event list (principal segments, interest cycle, rate resets) and fold LAX.stf/LAX.pof over it.

Equations

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

@[irreducible]

def Actus.Contract.Execution.laxCashflows.buildPrin (ct : Terms Float) (ied : Protocol.LocalTime) (cfg : Protocol.ScheduleConfig) (prAnchors : List Protocol.LocalTime) (prCycles : List (Option Protocol.Cycle)) (prAmts : List Float) (prDirs : List String) (nseg i : ℕ) (run : Float) : List (Protocol.Time × Bool × Float) × Option Protocol.LocalTime

Equations

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