Comment by mfornet

> Is the plan to build a new separation logic framework, or use e.g. iris-lean or splean as a base?

We plan to build our own, though we are currently evaluating what is the current state of iris-lean. Thanks for pointing to splean, I wasn't aware of it before.

> I’d imagine you’d still want step indexing to allow reasoning around cyclic heap structures

We have some APIs around loops and function calls that hides the "fuel-detail" and instead asks you to provide a well-founded relation that is used to prove that the behavior of the program is correct for "some" fuel.

The GCD example make use of this primitive to provide the invariants of the loop plus the argument that loop will terminate.

> Fun project in any case! I look forward to seeing how it develops :)

Feel free to join the telegram dev chat (link in github)