freespek / ssf-mc

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

Support Apalache type-checking for specs with mutual recursion #14

Open Kukovec opened 1 month ago

Kukovec commented 1 month ago

Unlike primitive recursion which, while not supported at the model-checking level, remains type-checkable, mutual recursion results in an error in the typechecking pass. (see https://github.com/freespek/ssf-mc/pull/13#discussion_r1686890811)

We should introduce type-checking support for these operators as well.