[kprove] intermediate claim modules not included in output of --emit-json-spec

[ehildenb]

Given the following K definition:

module TEST
    imports BOOL
    imports INT
    configuration <k> $PGM:Int </k>
    rule <k> 1 => 2 ... </k>
endmodule

module SOME-OTHER
    imports TEST
endmodule

module TEST-INTERMEDIATE
    imports TEST
    claim <k> 3 => 4 ... </k>
endmodule

module TEST-SPEC
    imports TEST-INTERMEDIATE 
    claim <k> 4 => 5 ... </k>
endmodule

You can run the following commands:

$ kompile --backend haskell test.k --main-module TEST --syntax-module TEST

$ kprovex test.k --spec-module TEST-SPEC --dry-run --emit-json-spec spec.json
kore-exec /home/dev/src/k/./test-kompiled/definition.kore --module TEST --prove /home/dev/src/k/./.kprove-2022-04-30-04-50-34-081-d9e7acef-013b-41e2-ad32-6a0bb24d4dad/spec.kore --spec-module TEST-SPEC --output /home/dev/src/k/./.kprove-2022-04-30-04-50-34-081-d9e7acef-013b-41e2-ad32-6a0bb24d4dad/result.kore

$ cat spec.json | jq .
{
  "format": "KAST",
  "version": 1,
  "term": {
    "node": "KFlatModule",
    "name": "TEST-SPEC",
    "imports": [
      {
        "node": "KImport",
        "name": "TEST-INTERMEDIATE",
        "isPublic": true
      }
    ],
    "localSentences": [
      {
        "node": "KClaim",
        "body": {
          "node": "KApply",
          "label": "<generatedTop>",
          "variable": false,
          "arity": 2,
          "args": [
            {
              "node": "KApply",
              "label": "<k>",
              "variable": false,
              "arity": 1,
              "args": [
                {
                  "node": "KSequence",
                  "arity": 2,
                  "items": [
                    {
                      "node": "KRewrite",
                      "lhs": {
                        "node": "KToken",
                        "sort": "Int",
                        "token": "4"
                      },
                      "rhs": {
                        "node": "KToken",
                        "sort": "Int",
                        "token": "5"
                      },
                      "att": ""
                    },
                    {
                      "node": "KVariable",
                      "name": "_DotVar1",
                      "originalName": "_DotVar1"
                    }
                  ]
                }
              ]
            },
            {
              "node": "KVariable",
              "name": "_DotVar0",
              "originalName": "_DotVar0"
            }
          ]
        },
        "requires": {
          "node": "KToken",
          "sort": "Bool",
          "token": "true"
        },
        "ensures": {
          "node": "KToken",
          "sort": "Bool",
          "token": "true"
        },
        "att": {
          "node": "KAtt",
          "att": {
            "org.kframework.attributes.Location": "Location(24,11,24,30)",
            "org.kframework.attributes.Source": "Source(/home/dev/src/k/test.k)",
            "org.kframework.definition.Production": "syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"
          }
        }
      }
    ],
    "att": {
      "node": "KAtt",
      "att": {
        "org.kframework.attributes.Location": "Location(21,1,26,10)",
        "org.kframework.attributes.Source": "Source(/home/dev/src/k/test.k)"
      }
    }
  }
}

The key here is that we see only one claim (the one from module TEST-SPEC), but not the claim from the included module TEST-INTERMEDIATE. This is because we are only outputting a single module in JSON. I propose we instead output every module imported by the --spec-module but not already included in the --main-module, that we there is enough information to reconstruct an entire definition.

This is annoying for the summarizer, because it means that we can only have one module full of claims at a time.

[ehildenb]

This is now blocking the Foundry verification project.