Record productions have exponential behavior

[radumereuta]

Old title: computeOverloadPOSet worst case takes 81s

This worst-case gets activated in one of the definitions @virgil-serbanuta is working on.
Test definition:
https://github.com/radumereuta/verified-smart-contracts/tree/multisig.new/multisig/protocol-correctness/proof/functions
Run as:
kompile -I ../../../ --backend haskell functions-execute.k -v --profile-rule-parsing --debug
kprove proof-count-can-sign.k -v

I'm currently investigating, and I'm making this issue to keep track of progress.
Update 1:

syntax StateCell ::= invariantStateFull(
      numUsers:Usize,
      userIdToAddress:Map,
      addressToUserId:Map,
      numBoardMembers:Usize,
      numProposers:Usize,
      userIdToRole:Map,
      quorum:Usize,
      actionLastIndex:Usize,
      actionData:Map,
      actionSigners:Map,
      callerAddress:KItem,
      stack:Stack,
      variables:Map,
      performedActions:List)  [function, functional]

This is one of the productions that takes a very long time to run computeOverloadPOSet.
Update 2:
This slowdown is because of how we parse record productions.
At parsing time there are 16385 overloads for invariantStateFull (arity 14), 8193 for invariantStateStack (arity 13), 2049 for invariantState (arity 11), 1025 for invariantMultisigState (arity 10), and many others with mere hundreds.

[ehildenb]

Currently, when we have a record production, we generate a bunch of extra syntax for parsing. For example:

syntax Record ::= record(a: Int, b:Int, c:Int)

produces:

syntax Record ::= "record" "(" "..." ")"
                  | "record" "(" a ":" Int "," "..." ")"
                  | "record" "(" b ":" Int "," "..." ")"
                  | "record" "(" a ":" Int ","  b ":" Int "," "..." ")"
....

[ehildenb]

This can be made smarter by changing how to generate productions so we don't generate an exponential number of productions.

Instead, generate extra non-terminals.

[ehildenb]

Some history:

• Originally, we allowed users to write record productions in any order.
• That was factorial, so we switched to only subsets of the existing order (exponential).
• While we're fixing it, we should go back to allowing any order.

We should restrict that:

• You cannot use the incorrect name under a record label.
• You cannot use the same name twice under a record label.

This can likely be done with a grammar transformation (add non-terminal for list of fields specific to that record label), and a post-processing step for checking that the list has no duplicates.