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

Initial exchange: take on the (unsigned) notional and the nominal rate.

Equations

• Actus.Contract.UMP.stf_IED ct t s = { md := s.md, nt := ct.nt, ipnr := ct.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.UMP.stf_IPCI {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : State α

Interest capitalization (no cash): compound the notional by the interest accrued over [Sd, t], then reset the accrual.

Equations

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

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

Termination: record the interest accrued on the capitalized notional since the last capitalization (settled by pof_TD).

Equations

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

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

STF dispatcher (events outside the UMP schedule just advance the clock).

Equations

• One or more equations did not get rendered due to their size.
• Actus.Contract.UMP.stf ct rf Actus.Protocol.EventType.IED t s = Actus.Contract.UMP.stf_IED ct t s
• Actus.Contract.UMP.stf ct rf Actus.Protocol.EventType.IPCI t s = Actus.Contract.UMP.stf_IPCI rf t s
• Actus.Contract.UMP.stf ct rf Actus.Protocol.EventType.TD t s = Actus.Contract.UMP.stf_TD rf t s

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

Equations

• Actus.Contract.UMP.pof_IED ct = Actus.Util.Conventions.sign ct.cntrl * -1 * ct.nt

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

Termination payoff: buy-back price plus interest accrued since the last capitalization, on the capitalized notional.

Equations

• Actus.Contract.UMP.pof_TD ct rf t s = Actus.Util.Conventions.sign ct.cntrl * (ct.ptd + s.ipac + s.nt * s.ipnr * rf.yf s.sd t)

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

Equations

• Actus.Contract.UMP.pof ct rf Actus.Protocol.EventType.IED t s = Actus.Contract.UMP.pof_IED ct
• Actus.Contract.UMP.pof ct rf Actus.Protocol.EventType.TD t s = Actus.Contract.UMP.pof_TD ct rf t s
• Actus.Contract.UMP.pof ct rf ev t s = 0

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

Pre-IED state at t₀; stf_IED overwrites the monetary fields.

Equations

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

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

One-step UMP transition. The constructor targets the dispatcher stf.

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

@[reducible, inline]

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

Equations

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

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

Equations

• Actus.Contract.UMP.getCashflow ct rf (Actus.Contract.UMP.Step.ev e a) = (((Actus.Contract.UMP.stf ct rf e t s).sd, e), Actus.Contract.UMP.pof ct rf e (Actus.Contract.UMP.stf ct rf e t s).sd s)

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

Equations

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

def Actus.Contract.UMP.UMP_contract : Abstract.ActusContract

Equations

• Actus.Contract.UMP.UMP_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.UMP.UMP_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition UMP_contract

Equations

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

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

UMP cash flows: thread UMP.stf/UMP.pof over the schedule IED, the capitalization (IPCI) cycle strictly before termination, then TD. IPCI is a non-cash capitalization, so its zero payoff is not reported.

Equations

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