Incorrect RPC Ref Detection on { 'p': ... } JSON Objects

[dranov]

Description

The comment on registerRefs says:

The function implements a form of "conservative garbage collection" where it treats any subobject {'p': v} as a potential RPC reference. Therefore p should not be used as a field name on the Lean side to prevent false positives.

It is unclear if the false positives will become a big issue.

I just ran into Lean server crashes due to this in our project, Veil.

Context

I am one of the maintainers of Veil. A Veil user on Zulip (#Veil > Need help with porting from Ivy to Veil @ 💬) shared a specification with us. Among other issues (related to Veil itself), the InfoView widget we have for #model_check crashes the Lean server, with errors that look 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

What's going on is that the traces returned by #model_check contain arbitrary JSON from model states and transition labels. In particular, if you have an action like this, with a single parameter named p :

action step_north (p : Proc)

... the obtained trace will look like this (simplified):

{
  "result": {
    "trace": {
      "states": [
        { "transition": { "step_north": { "p": 1 } } }
      ]
    }
  }
}

As a mitigation in Veil, we can rpcEncode our actual JSON objects as strings and parse the strings as JSON objects on rpcDecode, but this seems insane.

Expected Behavior

Only true RPC references should be tracked/released. Regular JSON objects should not be interpreted as RPC refs solely due to containing a field named p.

If that's too complicated to implement, at least the field name shouldn't be p, but something hard to collide with, like __lean_infoview_internal_rpc_ref_p__.

Versions

Lean: v4.27.0
Infoview dependency: @leanprover/infoview ~0.11.0