structure Actus.Abstract.ActusContract : Type 1

An ActusContract bundles a Terms type with a State type.

• Terms : Type
• State : Type

structure Actus.Abstract.StateTransition (c : ActusContract) : Type 1

The operational semantics of an ActusContract: an initial state, a one-step transition relation, and a cashflow extractor.

getCashflow takes a proof that a single step took place and a RiskFactor instance, and returns the resulting Cashflow.

• s₀ : c.State

  Initial state.

• rel : c.State → c.State → Type

  One-step state-transition relation.

• getCashflow {s s' : c.State} : self.rel s s' → Protocol.RiskFactor → Protocol.Cashflow

  Extract the cashflow produced by a single transition.

The reflexive-transitive closure of rel is Star rel, defined in Actus.Closures. Consumers can write Star st.rel s s' for execution traces, where st : StateTransition c.

The following helper is the analogue of the commented-out getCashflows in the Agda source: