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

Interest accrual Ipac_{t-} + Y(Sd_{t-}, t)·Ipnr_{t-}·Nt_{t-}.

Equations

• Actus.Contract.PAM.ipacAccr rf t s = s.ipac + rf.yf s.sd t * s.ipnr * s.nt

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

Fee accrual Feac_{t+} (§7.1). The FEB_N branch is exact; the absolute (FEB_A) branch's proration over the fee period is omitted because the state does not carry the fee-period boundaries t^{FP±}.

Equations

• Actus.Contract.PAM.feacNext ct rf t s = match ct.feb with | Actus.Protocol.FeeBasis.FEB_N => s.feac + rf.yf s.sd t * s.nt * ct.fer | Actus.Protocol.FeeBasis.FEB_A => s.feac

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Rate reset: Ipnr_{t+} = clamp_{[RRLF,RRLC]}(Ipnr+Δr) with Δr = clamp_{[RRPF,RRPC]}(Oʳᶠ(RRMO,t)·RRMLT + RRSP − Ipnr). Absent caps / floors impose no bound (clampHi/clampLo with none).

Equations

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

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

Equations

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

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

Scaling (§7.1): Nsc/Isc are reset to Oʳᶠ(SCMO,t)/SCIED for the dimensions the SCEF code scales (notional and/or interest).

Equations

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

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

Credit event uses STF_AD_PAM().

Equations

• Actus.Contract.PAM.stf_CE rf t s = Actus.Contract.PAM.stf_AD rf t s

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

STF dispatcher by event type (events not in the PAM schedule just advance the status date).

Equations

• One or more equations did not get rendered due to their size.
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.AD t s = Actus.Contract.PAM.stf_AD rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.IED t s = Actus.Contract.PAM.stf_IED ct t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.MD t s = Actus.Contract.PAM.stf_MD t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.PP t s = Actus.Contract.PAM.stf_PP ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.PY t s = Actus.Contract.PAM.stf_PY ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.FP t s = Actus.Contract.PAM.stf_FP rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.PRD t s = Actus.Contract.PAM.stf_PRD ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.TD t s = Actus.Contract.PAM.stf_TD t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.IP t s = Actus.Contract.PAM.stf_IP ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.IPCI t s = Actus.Contract.PAM.stf_IPCI ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.RR t s = Actus.Contract.PAM.stf_RR ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.RRF t s = Actus.Contract.PAM.stf_RRF ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.SC t s = Actus.Contract.PAM.stf_SC ct rf t s
• Actus.Contract.PAM.stf ct rf Actus.Protocol.EventType.CE t s = Actus.Contract.PAM.stf_CE rf t s

def Actus.Contract.PAM.pof_AD {α : Type} [Amount α] : α

Equations

• Actus.Contract.PAM.pof_AD = 0

def Actus.Contract.PAM.pof_IED {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (t : Protocol.Time) : α

Equations

• Actus.Contract.PAM.pof_IED ct rf t = rf.curs t * Actus.Util.Conventions.sign ct.cntrl * -1 * (ct.nt + ct.pdied)

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

Equations

• Actus.Contract.PAM.pof_MD rf t s = rf.curs t * (s.nsc * s.nt + s.isc * s.ipac + s.feac)

def Actus.Contract.PAM.pof_PP {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) : α

Equations

• Actus.Contract.PAM.pof_PP rf t = rf.curs t * rf.prepayment t

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

Equations

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

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

Equations

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

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

Equations

• Actus.Contract.PAM.pof_PRD ct rf t s = rf.curs t * Actus.Util.Conventions.sign ct.cntrl * -1 * (ct.pprd + s.ipac + rf.yf s.sd t * s.ipnr * s.nt)

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

Equations

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

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

Equations

• Actus.Contract.PAM.pof_IP _ct rf t s = rf.curs t * s.isc * (s.ipac + rf.yf s.sd t * s.ipnr * s.nt)

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

POF dispatcher by event type.

Equations

• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.IED t s = Actus.Contract.PAM.pof_IED ct rf t
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.MD t s = Actus.Contract.PAM.pof_MD rf t s
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.PP t s = Actus.Contract.PAM.pof_PP rf t
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.PY t s = Actus.Contract.PAM.pof_PY ct rf t s
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.FP t s = Actus.Contract.PAM.pof_FP ct rf t s
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.PRD t s = Actus.Contract.PAM.pof_PRD ct rf t s
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.TD t s = Actus.Contract.PAM.pof_TD ct rf t s
• Actus.Contract.PAM.pof ct rf Actus.Protocol.EventType.IP t s = Actus.Contract.PAM.pof_IP ct rf t s
• Actus.Contract.PAM.pof ct rf ev t s = 0

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

Initial state per the §7.1 initialization table. md is the maturity date on the Time axis (caller supplies it from genSchedule); t₀ is the status date.

Equations

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

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

One-step state-transition relation for PAM: Step ct rf s s' holds when the contract advances from s to s' by one scheduled event at time t ≥ Sd. Each constructor's target is the corresponding functional stf_*.

• ad {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_AD rf t s
• ied {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_IED ct t s
• md {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_MD t s
• pp {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_PP ct rf t s
• py {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_PY ct rf t s
• fp {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_FP rf t s
• prd {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_PRD ct rf t s
• td {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_TD t s
• ip {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_IP ct rf t s
• ipci {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_IPCI ct rf t s
• rr {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_RR ct rf t s
• rrf {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_RRF ct rf t s
• sc {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_SC ct rf t s
• ce {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} : s.sd ≤ t → s ↝[ct, rf] stf_CE rf t s

def Actus.Contract.PAM.«term_↝[_,_]_» : Lean.TrailingParserDescr

One-step state-transition relation for PAM: Step ct rf s s' holds when the contract advances from s to s' by one scheduled event at time t ≥ Sd. Each constructor's target is the corresponding functional stf_*.

Equations

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

@[reducible, inline]

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

Execution trace: zero-or-more PAM steps.

Equations

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

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

The cashflow of one PAM step: event time is the post-state status date (= t), the payoff is the matching pof_* applied to the pre-state.

Equations

• One or more equations did not get rendered due to their size.
• Actus.Contract.PAM.getCashflow ct rf (Actus.Contract.PAM.Step.ad a) = (((Actus.Contract.PAM.stf_AD rf t s).sd, Actus.Protocol.EventType.AD), Actus.Contract.PAM.pof_AD)
• Actus.Contract.PAM.getCashflow ct rf (Actus.Contract.PAM.Step.ipci a) = (((Actus.Contract.PAM.stf_IPCI ct rf t s).sd, Actus.Protocol.EventType.IPCI), 0)
• Actus.Contract.PAM.getCashflow ct rf (Actus.Contract.PAM.Step.rr a) = (((Actus.Contract.PAM.stf_RR ct rf t s).sd, Actus.Protocol.EventType.RR), 0)
• Actus.Contract.PAM.getCashflow ct rf (Actus.Contract.PAM.Step.rrf a) = (((Actus.Contract.PAM.stf_RRF ct rf t s).sd, Actus.Protocol.EventType.RRF), 0)
• Actus.Contract.PAM.getCashflow ct rf (Actus.Contract.PAM.Step.sc a) = (((Actus.Contract.PAM.stf_SC ct rf t s).sd, Actus.Protocol.EventType.SC), 0)
• Actus.Contract.PAM.getCashflow ct rf (Actus.Contract.PAM.Step.ce a) = (((Actus.Contract.PAM.stf_CE rf t s).sd, Actus.Protocol.EventType.CE), 0)

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

Collect cashflows along a full execution trace.

Equations

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

def Actus.Contract.PAM.PAM_contract : Abstract.ActusContract

Equations

• Actus.Contract.PAM.PAM_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.PAM.PAM_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition PAM_contract

Witness that PAM satisfies the abstract StateTransition interface.

Equations

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