search

freespek / ssf-mc

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

Frontload computation for recursively defined predicates #19

Closed Kukovec closed 2 weeks ago

Kukovec commented 3 months ago

In many parts of the spec, we evaluate predicates with varying levels of complexity, such as is_ancestor_descendant_relationship or is_justified_checkpoint, which are defined recursively in the original python code, and via fold in the spec. To ease model checking, it might be simpler to compute the entire predicate (e.g. as a function) at once, and refer to that singular function everywhere else in the spec where the predicate is used. In the case that we extend the spec with protocol behavior (e.g. sending a message), we could update these predicates after each step (e.g. each new vote message may extend the set of justified predicates by all checkpoints between its source and target)

konnov commented 2 weeks ago

@thpani you did it, right?

thpani commented 2 weeks ago

Yes, this was done a long time ago in #38