closes #81
This PR changes instrumentation, to the format discussed during our recent meeting. A detailed explanation of the format can be found inside instrument.ts.
To this end, it makes the following changes:
Instrumentation now constructs Init from oldFields, and Next from a conjunction of state-variable updates from fields and transition constraints from method and methodArgs.
Instrumentation adds Gen(1) initializations (in either Init or Next) to all variables declared in the monitor, but absent from the transaction data (in oldFields or fields, respectively). This allows us to avoid Apalache errors on transactions in which data storage changes.
Tests with expecetd instrumentation syntax have been updated to reflect the changes. No semantic changes have been made in those tests
New tests covering the newly-supported initialization paradigm have been added
entry-timelock.json has been fixed to comply with the transition requirements of Claim (last_error' = "contract is not initialized" whenever ~is_initialized)
closes #81 This PR changes instrumentation, to the format discussed during our recent meeting. A detailed explanation of the format can be found inside
instrument.ts
. To this end, it makes the following changes:Init
fromoldFields
, andNext
from a conjunction of state-variable updates fromfields
and transition constraints frommethod
andmethodArgs
.Gen(1)
initializations (in eitherInit
orNext
) to all variables declared in the monitor, but absent from the transaction data (inoldFields
orfields
, respectively). This allows us to avoid Apalache errors on transactions in which data storage changes.entry-timelock.json
has been fixed to comply with the transition requirements ofClaim
(last_error' = "contract is not initialized"
whenever~is_initialized
)