`pyk prove` cannot handle claims with `#Equals` in `requires`
Opened this issue · 3 comments
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
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/
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-runtest-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="
}
}
}
]
}
}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.