def Actus.Contract.ANN.annuityAmount {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (nt ipac ipnr : α) : α

Annuity amount A(t, Md, Nt, Ipac, Ipnr) for the post-reset state.

Equations

• Actus.Contract.ANN.annuityAmount rf t nt ipac ipnr = Actus.Util.Schedule.annuity nt ipac ipnr (rf.annuityYfs t)

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

Rate reset: PAM rate logic, interest accrued on Ipcb, then Prnxt recomputed as the annuity amount.

Equations

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

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

Fixed-rate reset variant: Ipnr := RRNXT, then recompute Prnxt.

Equations

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

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

Equations

• Actus.Contract.ANN.stf ct rf Actus.Protocol.EventType.RR t s = Actus.Contract.ANN.stf_RR ct rf t s
• Actus.Contract.ANN.stf ct rf Actus.Protocol.EventType.RRF t s = Actus.Contract.ANN.stf_RRF ct rf t s
• Actus.Contract.ANN.stf ct rf ev t s = Actus.Contract.NAM.stf ct rf ev t s

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

Payoffs are exactly NAM's (RR/RRF pay nothing; PR uses POF_PR_NAM).

Equations

• Actus.Contract.ANN.pof ct rf ev t s = Actus.Contract.NAM.pof ct rf ev t s

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

Initial state: as NAM (Prnxt = R(CNTRL)·PRNXT; the annuity-derived fallback for an absent PRNXT is recomputed on the first reset).

Equations

• Actus.Contract.ANN.init ct md t₀ = Actus.Contract.NAM.init ct md t₀

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

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

Equations

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

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

Equations

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

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

Equations

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

def Actus.Contract.ANN.ANN_contract : Abstract.ActusContract

Equations

• Actus.Contract.ANN.ANN_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.ANN.ANN_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition ANN_contract

Equations

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