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

Rate reset: install the clamped market floating rate.

Equations

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

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

STF dispatcher. The floating leg advances the period boundary Sd; the fixed leg (and any other event) leaves the state untouched.

Equations

• One or more equations did not get rendered due to their size.
• Actus.Contract.SWPPV.stf ct rf Actus.Protocol.EventType.RR t s = Actus.Contract.SWPPV.stf_RR ct rf t s
• Actus.Contract.SWPPV.stf ct rf e t s = s

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

Equations

• Actus.Contract.SWPPV.pof_IPFX ct rf t s = s.nt * ct.ipnr * rf.yf s.sd t

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

Equations

• Actus.Contract.SWPPV.pof_IPFL rf t s = -1 * s.nt * s.ipnr * rf.yf s.sd t

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

Equations

• Actus.Contract.SWPPV.pof ct rf Actus.Protocol.EventType.IPFX t s = Actus.Contract.SWPPV.pof_IPFX ct rf t s
• Actus.Contract.SWPPV.pof ct rf Actus.Protocol.EventType.IPFL t s = Actus.Contract.SWPPV.pof_IPFL rf t s
• Actus.Contract.SWPPV.pof ct rf e t s = 0

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

Initial state: signed notional, floating rate at nominalInterestRate2, period start at IED.

Equations

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

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

One-step SWPPV transition. t is explicit (a period may emit two legs at the same t, so the cash-flow time is taken from t rather than Sd).

• 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.SWPPV.Trace {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

Equations

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

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

Equations

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

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

Equations

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

def Actus.Contract.SWPPV.SWPPV_contract : Abstract.ActusContract

Equations

• Actus.Contract.SWPPV.SWPPV_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.SWPPV.SWPPV_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition SWPPV_contract

Equations

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

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

SWPPV cash flows. Each interest period emits a fixed (IPFX) and floating (IPFL) leg; rate resets (RR) update the floating rate. The events are folded through SWPPV.stf/SWPPV.pof; at a shared timestamp they are ordered IPFX, IPFL, then RR, so both legs read the pre-reset rate and the same period year-fraction. Gross (D) keeps both legs; net (S) sums them per period into one IP.

Equations

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

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

Cash flows of a single (child) contract, dispatched on its type.

Equations

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

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

SWAPS — a parent contract over two legs (contractStructure). The FIL leg runs in the parent's role direction, the SEL leg in the opposite one; each leg is generated by the ordinary engine and the cash flows combined: gross/delivery (deliverySettlement = D) emits both legs' flows, while net (S) sums same-(date, event-type) flows. A parent terminationDate truncates the combined flows and settles TD; a parent purchaseDate drops pre-purchase flows and settles PRD (both at the parent's clean price).

Equations

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