Comment by jacobjwalters
10 hours ago
Is the plan to build a new separation logic framework, or use e.g. iris-lean or splean as a base?
And even if fuel isn’t exposed in the program logic, I’d imagine you’d still want step indexing to allow reasoning around cyclic heap structures. My experience with getting Claude (even fable) to do step indexed logical relations/SL proofs autonomously is that it struggles hard even on toy examples, particularly around the index shuffling. Do you have a setup in mind that can scale to larger programs?
Fun project in any case! I look forward to seeing how it develops :)
> 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)