freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
4 stars 0 forks source link

Add SMT-based spec #49

Closed thpani closed 1 month ago

thpani commented 2 months ago

Add a hand-written SMT-based specification of 3SF.

This spec takes a constraint-based approach to encode 3SF and accountable safety. It uses the decision procedure for finite sets and cardinality constraints in CVC5.

It was produced as a byproduct of the model-checking work for 3SF, to rule out performance issues caused by Apalache's SMT encoding.

thpani commented 2 months ago

I initially forgot to add the cardinality check for 1/3 in AccountableSafety. This has been fixed in 96c86f3.

@konnov @Kukovec PTAL