pyk prove cannot handle claims with #Equals in requires

[nwatson22]

pyk prove crashes with an error when trying to prove a spec claim with #Equals in the requires clause when trying to resolve sorts for the rule.

Steps to reproduce:

test.k

module TEST
  imports BOOL
  imports INT

  configuration 
  <test>
    <k> $PGM:K </k>
  </test>
endmodule

test-spec.k

module TEST-SPEC
  imports TEST
  claim <k> 0 </k>
    requires { true #Equals 1 <Int 2 }
endmodule

pyk kompile test.k --backend haskell
pyk prove test-spec.k

Desired result:

The claim can be proven similarly to if the same files are used with kompile test.k --backend haskell; kprove test-spec.k.

Actual result:

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/noah/dev/k/pyk/src/pyk/__main__.py", line 97, in main
    execute(options)
  File "/home/noah/dev/k/pyk/src/pyk/__main__.py", line 272, in exec_prove
    proofs = prove_rpc.prove_rpc(options=options)
  File "/home/noah/dev/k/pyk/src/pyk/ktool/prove_rpc.py", line 48, in prove_rpc
    return [
  File "/home/noah/dev/k/pyk/src/pyk/ktool/prove_rpc.py", line 49, in <listcomp>
    self._prove_claim_rpc(
  File "/home/noah/dev/k/pyk/src/pyk/ktool/prove_rpc.py", line 92, in _prove_claim_rpc
    prover.advance_proof(proof, max_iterations=max_iterations)
  File "/home/noah/dev/k/pyk/src/pyk/proof/proof.py", line 505, in advance_proof
    self.init_proof(proof)
  File "/home/noah/dev/k/pyk/src/pyk/proof/reachability.py", line 703, in init_proof
    _inject_module(proof.circularities_module_name, proof.dependencies_module_name, [circularity_rule])
  File "/home/noah/dev/k/pyk/src/pyk/proof/reachability.py", line 686, in _inject_module
    _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, _module)
  File "/home/noah/dev/k/pyk/src/pyk/konvert/_kast_to_kore.py", line 247, in kflatmodule_to_kore
    kore_axioms.append(krule_to_kore(definition, sent))
  File "/home/noah/dev/k/pyk/src/pyk/konvert/_kast_to_kore.py", line 213, in krule_to_kore
    kore_lhs: Pattern = kast_to_kore(definition, krule_lhs, sort=top_level_k_sort)
  File "/home/noah/dev/k/pyk/src/pyk/konvert/_kast_to_kore.py", line 66, in kast_to_kore
    kast = _add_sort_injections(definition, kast, sort)
  File "/home/noah/dev/k/pyk/src/pyk/konvert/_kast_to_kore.py", line 137, in _add_sort_injections
    stack.append(_argument_sorts(definition, term))
  File "/home/noah/dev/k/pyk/src/pyk/konvert/_kast_to_kore.py", line 167, in _argument_sorts
    _, argument_sorts = definition.resolve_sorts(term.label)
  File "/home/noah/dev/k/pyk/src/pyk/kast/outer.py", line 1336, in resolve_sorts
    sorts = dict(zip(prod.params, label.params, strict=True))
ValueError: zip() argument 2 is shorter than argument 1

[ehildenb]

requires { X #Equals Y } actually does not make sense though.

The sort of requires is Bool, and the semantics is that it should be equal to true. But { ... #Equals ... } is a matching logic connective, which has the semantics that if the LHS and RHS represent the same ML sets, then the entire thing is the entire sort. So if { ... #Equals ... } holds, then it actually represents the set true #Or false, not just the singleton true.

So we almost certainly don't want { ... #Equals ... } in a requires clause. You likely just want true ==K 1 <Int 2, or even just 1 <Int 2, which when turning it into a CTerm will be stored as { true #Equals 1 <Int 2 } as you want above. That's because, in a CTerm, the constraints are of sort GeneratedTopCell, and so CONFIG #And { true #Equals 1 <Int 2 } means "all things that CONFIG could be where we also have { true #Equals 1 <Int 2 }.

For more information, review the Matching Logic paper: https://fsl.cs.illinois.edu/publications/rosu-2017-lmcs.html, and the website: http://www.matching-logic.org/

[tothtamas28]

The root cause is that kprove emits the .json file without sort parameters on #Equals:

$ kprove test-spec.k --emit-json-spec test-spec.json --dry-run

test-spec.json

{
  "format": "KAST",
  "version": 3,
  "term": {
    "node": "KFlatModuleList",
    "mainModule": "TEST-SPEC",
    "term": [
      {
        "node": "KFlatModule",
        "name": "TEST-SPEC",
        "imports": [
          {
            "node": "KImport",
            "name": "TEST",
            "isPublic": true
          }
        ],
        "localSentences": [
          {
            "node": "KClaim",
            "body": {
              "node": "KApply",
              "label": {
                "node": "KLabel",
                "name": "<generatedTop>",
                "params": []
              },
              "arity": 2,
              "args": [
                {
                  "node": "KApply",
                  "label": {
                    "node": "KLabel",
                    "name": "<test>",
                    "params": []
                  },
                  "arity": 1,
                  "args": [
                    {
                      "node": "KApply",
                      "label": {
                        "node": "KLabel",
                        "name": "<k>",
                        "params": []
                      },
                      "arity": 1,
                      "args": [
                        {
                          "node": "KToken",
                          "sort": {
                            "node": "KSort",
                            "name": "Int"
                          },
                          "token": "0"
                        }
                      ]
                    }
                  ]
                },
                {
                  "node": "KApply",
                  "label": {
                    "node": "KLabel",
                    "name": "<generatedCounter>",
                    "params": []
                  },
                  "arity": 1,
                  "args": [
                    {
                      "node": "KRewrite",
                      "lhs": {
                        "node": "KVariable",
                        "name": "_Gen0",
                        "sort": {
                          "node": "KSort",
                          "name": "Int"
                        }
                      },
                      "rhs": {
                        "node": "KVariable",
                        "name": "?_Gen1",
                        "sort": {
                          "node": "KSort",
                          "name": "Int"
                        }
                      }
                    }
                  ]
                }
              ]
            },
            "requires": {
              "node": "KApply",
              "label": {
                "node": "KLabel",
                "name": "#Equals",
                "params": []
              },
              "arity": 2,
              "args": [
                {
                  "node": "KToken",
                  "sort": {
                    "node": "KSort",
                    "name": "Bool"
                  },
                  "token": "true"
                },
                {
                  "node": "KApply",
                  "label": {
                    "node": "KLabel",
                    "name": "_<Int_",
                    "params": []
                  },
                  "arity": 2,
                  "args": [
                    {
                      "node": "KToken",
                      "sort": {
                        "node": "KSort",
                        "name": "Int"
                      },
                      "token": "1"
                    },
                    {
                      "node": "KToken",
                      "sort": {
                        "node": "KSort",
                        "name": "Int"
                      },
                      "token": "2"
                    }
                  ]
                }
              ]
            },
            "ensures": {
              "node": "KToken",
              "sort": {
                "node": "KSort",
                "name": "Bool"
              },
              "token": "true"
            },
            "att": {
              "node": "KAtt",
              "att": {
                "org.kframework.attributes.Location": [
                  3,
                  9,
                  4,
                  39
                ],
                "org.kframework.attributes.Source": "/home/ttoth/git/k/pyk/test-spec.k",
                "org.kframework.definition.Production": {
                  "node": "KProduction",
                  "klabel": {
                    "node": "KLabel",
                    "name": "#ruleRequires",
                    "params": []
                  },
                  "productionItems": [
                    {
                      "node": "KNonTerminal",
                      "sort": {
                        "node": "KSort",
                        "name": "#RuleBody"
                      }
                    },
                    {
                      "node": "KTerminal",
                      "value": "requires"
                    },
                    {
                      "node": "KNonTerminal",
                      "sort": {
                        "node": "KSort",
                        "name": "Bool"
                      }
                    }
                  ],
                  "params": [],
                  "sort": {
                    "node": "KSort",
                    "name": "#RuleContent"
                  },
                  "att": {
                    "node": "KAtt",
                    "att": {
                      "klabel": "#ruleRequires",
                      "symbol": "",
                      "org.kframework.attributes.Location": [
                        346,
                        27,
                        346,
                        102
                      ],
                      "org.kframework.attributes.Source": "/home/ttoth/git/k/k-distribution/target/release/k/include/kframework/builtin/kast.md"
                    }
                  }
                },
                "UNIQUE_ID": "8dc0e1d873088f3cfb273cf138f2b279914672cbcca7c71a8d04c25b3360ccd2"
              }
            }
          }
        ],
        "att": {
          "node": "KAtt",
          "att": {
            "org.kframework.attributes.Location": [
              1,
              1,
              5,
              10
            ],
            "org.kframework.attributes.Source": "/home/ttoth/git/k/pyk/test-spec.k",
            "digest": "ha2k2aFsVNWhTxJB0GEX2k9yTwIiKVHGTACQyuDV2Ks="
          }
        }
      }
    ]
  }
}

[virgil-serbanuta]

FWIW, using #Equals in requires is sometimes useful when the terms may not be defined, e.g.:

requires true #And {M[K] #Equals N[K]}

for testing that two maps either have the same value for K, or K is missing from both maps. Of course, in this particular case, this could also be written as:

requires K in_keys(M) andBool K in_keys(N) andBool M[K] orDefault true ==K N[K] orDefault true

but the latter is significantly more verbose, and does not generalize (not all undefined functions have an "orDefault" version).

Of course, while true #And {M[K] #Equals N[K]} is of sort Bool, it is either true or #Bottom (or, in general, it's true, false or #Bottom) instead of just true or false. However, that's already the case when the requires clause contains partial functions, so it should not be an issue.