package octez-protocol-017-PtNairob-libs
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=aa2f5bc99cc4ca2217c52a1af2a2cdfd3b383208cb859ca2e79ca0903396ca1d
sha512=d68bb3eb615e3dcccc845fddfc9901c95b3c6dc8e105e39522ce97637b1308a7fa7aa1d271351d5933febd7476b2819e1694f31198f1f0919681f1f9cc97cb3a
doc/octez-protocol-017-PtNairob-libs.test-helpers/Tezos_017_PtNairob_test_helpers/Liquidity_baking_machine/ValidationMachine/index.html
Module Liquidity_baking_machine.ValidationMachine
Source
type t =
ConcreteMachine.t
* Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t state
The state of the ValidationMachine
.
A collections of functions to introspect the symbolic part of the ValidationMachine
state.
A collections of functions to introspect the concrete part of the ValidationMachine
state.
val build :
?invariant:
(Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t env ->
t ->
bool Tezos_base.TzPervasives.tzresult Lwt.t) ->
?subsidy:xtz ->
specs ->
(t * Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t env)
Tezos_base.TzPervasives.tzresult
Lwt.t
build specs
asynchronously computes (1) an initial state for the ValidationMachine
, and (2) the environment associated to this state.
The machine enforces the resulting state is consistent with the specs
given as inputs, and raises an Assert_failure
exception if it does not. It also enforces that the machines used underneath remain in sync.
One can use the optional argument subsidy
to set the subsidy amount to a given value (by default, we use the same as the main chain). Additionally, the invariant
optional argument can be used to verify that a given invariant holds at the end of the initialization.
val step :
?invariant:
(Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t env ->
t ->
bool Tezos_base.TzPervasives.tzresult Lwt.t) ->
Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t step ->
Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t env ->
t ->
t Tezos_base.TzPervasives.tzresult Lwt.t
step s env state
asynchronously executes a single step s
from state
.
The invariant
optional argument can be used to verify that a given invariant holds after each baked block.
val run :
?invariant:
(Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t env ->
t ->
bool Tezos_base.TzPervasives.tzresult Lwt.t) ->
contract_id step list ->
Tezos_protocol_017_PtNairob.Protocol.Alpha_context.Contract.t env ->
t ->
t Tezos_base.TzPervasives.tzresult Lwt.t
run lss env state
asynchronously executes a list of steps from state
.
The invariant
optional argument can be used to verify that a given invariant holds after each baked block.