Nonrecursive implementation of `is_justified_checkpoint`

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification

Apache License 2.0

4 stars 0 forks source link

Nonrecursive implementation of `is_justified_checkpoint` #18

Closed Kukovec closed 3 months ago

Kukovec commented 3 months ago

Based on the recursion rules introduced in #17, this PR adds a nonrecursive implementation of is_justified_checkpoint. Justification of iteration values is included in the file comments. Also includes a minor type generalization in the rule itself.

Kukovec commented 3 months ago

Note: changes to MC_ffg were from our live sync.