namada icon indicating copy to clipboard operation
namada copied to clipboard

Published 20 hours ago • verified publisher icon anoma

test/PoS: setup quint sync test from state machine

Open tzemanovic opened this issue 2 years ago • 2 comments

Adds a test of PoS impl against the Quint model (https://github.com/informalsystems/partnership-heliax/blob/tomas/rust-2-quint/2023/Q2/artifacts/PoS-quint/namada.qnt) using the state machine test that calls into Quint's REPL. The basic approach works but it still needs a bit more work to parametrize more of the data (params in the other actions and the genesis validator set with non-zero stake) currently hard-coded in the Quint model.

tzemanovic avatar Jul 06 '23 16:07 tzemanovic

do we still want to do this @tzemanovic ?

brentstone avatar Jan 02 '24 21:01 brentstone

do we still want to do this @tzemanovic ?

yeah, let's leave this open for now

tzemanovic avatar Jan 04 '24 08:01 tzemanovic