Constraints with an existential variable produced by `kmxwasm` cannot be internalised by Booster

Executing a proof test_change_quorum-int2val-spec.json) using the current version of kore-rpc-booster produces s number of warnings that boil down to Booster's inability to internalize constraints with existential variables.

The pretty-printed constraint looks like this:

#And #Not ( #Exists CODE:ModuleDecl . { AbstractCode_1:Code #Equals CODE:ModuleDecl } )

and seems to be introduced by abstracting the contents of the <code> cell (I'll need @virgil-serbanuta input on this to confirm).

I cannot say if the proof is hindered in any way by the Booster's inability to internalize these. I think Kore can still deal with them if necessary.

I'm attaching a minimized bug report that contains:

• the Haskell and LLVM definition.kore
• an execute request that leads to a three-way branch, the third branch containing an existential;
• a simplify request with the predicate from the third branch that contains the existential;
• responses to the requests for kore-rpc-booster, booster-dev and kore-rpc-dev

kmxwasm_bug_report_existential.tar.gz

booster-dev fails with:

[NotSupported (KJExists {sort = SortApp {name = Id {getId = "SortGeneratedTopCell"}, args = []}, var = Id {getId = "VarCODE"}, ...

while kore-rpc-dev and kore-rpc-booster return the predicate as-is (that is fine).

I do not think there's an immediate action needed. @virgil-serbanuta please let us know your views on this.

Start with kmxwasm_bug_report_existential.tar.gz and reproduce the simplify request containing the existential predicate. Compare booster-dev's KJExists NotSupported response with kore-rpc-dev and kore-rpc-booster, using the attached Haskell and LLVM definition.kore files and execute request. Done means determining whether the constraint must be internalized and resolving or explicitly accepting the differing behavior.