Unbound variable check when internalising module

[goodlyrottenapple]

Check whether all existential variables are quantified when internalising rules. This is to prevent runtimeverification/haskell-backend#3777, where the rule contains a variable on the RHS which does not appear on the LHS and should therefore be existentially quantified, since this is the assumption that the booster currently makes and we leak internal variable names when this assumption is violated (we could drop using explicit \exist altogether and just infer exist variables automatically).

With this change, sending this request:

{
  "jsonrpc": "2.0",
  "id": 1,
  "method": "add-module",
  "params": {
    "module": "module M-SIMPLE-PROOFS-SPEC-USE-DEPS1-DEPENDS-MODULE\n    import SIMPLE-PROOFS []\n    axiom{} \\rewrites{SortGeneratedTopCell{}}(\\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortStep{}, SortKItem{}}(Lblstart1'Unds'SIMPLE-PROOFS'Unds'Step{}()), dotk{}())), Lbl'-LT-'state'-GT-'{}(Var'Unds'STATE'Unds'CELL : SortMap{}), Lbl'-LT-'generatedCounter'-GT-'{}(Var'Unds'GENERATEDCOUNTER'Unds'CELL'Unds'c84b0b5f : SortInt{})), \\top{SortGeneratedTopCell{}}()), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortStep{}, SortKItem{}}(Lblmid'Unds'SIMPLE-PROOFS'Unds'Step{}()), dotk{}())), Lbl'-LT-'state'-GT-'{}(Var'Unds'STATE'Unds'CELL : SortMap{}), Lbl'-LT-'generatedCounter'-GT-'{}(Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b : SortInt{}))) [priority{}(\"20\"), label{}(\"BASIC-BLOCK-1-TO-2\")]\nendmodule []",
    "name-as-id": true
  }
}

will result in the following error:

{
  "jsonrpc": "2.0",
  "id": 1,
  "error": {
    "code": 8,
    "data": {
      "context": null,
      "error": "Unbound variables Var?_GENERATEDCOUNTER_CELL_6de8d71b:SortInt{} in rule BASIC-BLOCK-1-TO-2"
    },
    "message": "Invalid module"
  }
}