Need help with porting from Ivy to Veil

Stream: Veil

[Asgeir Eiriksson]

Hi I'm trying to port the Apple open-source ord_live.ivy ordering model to Veil and I'm running into some issues

I'm attaching a distilled test case (Main.lean in attachment) that reproduces the problem, and I modified the code to produce an artificial failure (negative testing). The model checkin part produces the correct behavior, but something goes wrong on the proof side. I only get a WP, but no TR CTI is produced

The header in the following file gives some references to the model and has the distilled test case, and it mentions some CTI RFE (which are not crucial at this point)

Main.lean

Thanks

[George Pîrlea]

@Asgeir Eiriksson I'm taking a look now and will get back to you as soon possible.

[George Pîrlea]

I've identified the root cause and am working on a fix.

[George Pîrlea]

@Asgeir Eiriksson I've pushed a fix.

If you're running in a repository based on the veil-usage-example template, run lake update && lake build. If you're operating in a clone of the Veil repo on the veil-2.0-preview branch, run git pull first.

[George Pîrlea]

The comment in the file also mentions:

in other cases seen wrong TR CTI

Could you please expand on that? What is the issue?

[Qiyuan Zhao]

@Asgeir Eiriksson Hi, do you plan to port the liveness proofs?

Previously we've verified some of the proof rules from that paper using our LTL library. Their proofs are currently in a private GitHub repo, but we'd be happy to give you access if that would be useful.

Since we're planning to add liveness support to Veil, it could be a good opportunity to work together on porting the liveness proofs if you're interested.

[George Pîrlea]

@Asgeir Eiriksson

CTI print numeric values of enum e.g. 0 instead of symbolic name e.g. write

I've made it such that CTIs now show the symbolic name for enums, rather than a numeric value.

CTI don't trace the execution with line numbers

Getting line-by-line execution traces would be a lot more involved, unfortunately. We're not currently planning to add that.

CTI don't print T0, T1

I think this should already work. It's perhaps a bit confusing because the "Extra values" panel is collapsed by default. (Please let me know if that's indeed what's going on.)

image.png

[George Pîrlea]

I also noticed the Lean server crashes due to the #model_check InfoView widget, apparently when the widget unloads, with errors like this:

Watchdog error: Got param with wrong structure: {"refs":[{"p":1},{"p":0},{"p":"0"},{"p":"0"},{"p":"0"},{"p":"0"},{"p":"0"}],"sessionId":"15898261356649562253","uri":"file:///src/veil/Examples/Main.lean"}
Lean.Lsp.RpcReleaseParams.refs: Lean.Lsp.RpcRef.p: String expected

I'll have to look more deeply into what's going on there, but probably won't have time for it very soon. We're still waiting for the upstream refreshable widget component to get merged (we have a custom version of that vendored inside the Veil repo for now).

Later edit: Codex identified the issue. It's a bug in the Lean InfoView. It treats any subobject {'p': v} as an RPC reference. Since this spec has actions with a parameter named p, the JSON traces we send to the InfoView get treated as RPC objects :man_facepalming:

I've submitted the issue upstream: https://github.com/leanprover/vscode-lean4/issues/712

[George Pîrlea]

As a workaround for now, you can rename the parameter p of step_north... :dizzy:

[Asgeir Eiriksson]

@George Pîrlea
Thanks for the quick response!

There is one issue remaining having to do with the "assert! ¬ prevents min_arr" that I've commented out in the test file. When I comment out the "if prevents min_arr" instead and remove the comment on the assert, then bad things happen

The bad TR CTI I mentioned probably had something to do with the issue that you fixed

I now plan to continue the port of the ord_live.ivy safety properties to lean

[Asgeir Eiriksson]

@Qiyuan Zhao

Yes, I'm hoping to port the liveness proofs too, and it's great you already have some of the proof rules working, and I'd be happy to try to port them once you think they're stable

The ord_live2.ivy (same directory in ivy repository as ord_live.ivy) has the ranking tactic that I find very useful, and at this point we primarily use that tactic and l2s_auto4 when the ranking tactic is not a fit

[George Pîrlea]

Thanks for the quick response!

You're very welcome!

Please do keep getting back to us with issues you encounter. We're happy to fix them.

When I comment out the "if prevents min_arr" instead and remove the comment on the assert, then bad things happen

Ah, I see what you mean. This is a bug. As a workaround for now, you can inline the definition of the ghost relation, e.g.:

assert ¬ (∀ T, lt LClock.zero min_arr ∧ (lt T ltime → ¬ (evs_loc T = dramc_l ∧ lt min_arr T)))

[Qiyuan Zhao]

I just pushed a fix and hopefully it resolves the error could not synthesize default value for parameter 'st' using tactics, if that's the bad thing you are referring to.

I'm hoping to port the liveness proofs too, and it's great you already have some of the proof rules working, and I'd be happy to try to port them once you think they're stable

That sounds great! At the moment, since Veil doesn't yet have built-in support for liveness reasoning, using those rules still requires manual setup, so I wouldn't quite call the development "stable" in that sense. I'll get back to you once things are in a better shape.