Steps towards RPC prover (#112)

These changes are what I needed to have a first working version of
KProve implemented fully here:
runtimeverification/evm-semantics#1443. In
particular:

- Some KAst <-> Kore problems are addressed:
- If the same variable shows up multiple times in
`KDefinition.sort_vars`, but with different sorts, instead of just
giving up we'll check if one sort is a subsort of the other. If so,
we'll return the smaller sort. Test added to `test_kast_to_kore`.
- The conversions for `Exists` are added. Test added to
`test_bidirectional`.
- `KProve.execute` method now returns `CTerm` instead of `KInner`, as it
shouldn't be able to return `mlTop()` or `mlBottom()` anyway.
- `KCFG.create_cover` now allows you to specify a witness manually
instead of trying to compute it for you. (De)Serialization requires that
we can do `Subst.{from_dict,to_dict}`, so that functionality is added
too.
- `KProve.implies` method is added as a wrapper around the `implies` RPC
endpoint. Tests are added that make sure it's giving back sane results.
By default, we much existentially bind variables in the consequent that
are not present in the antecedent to get anything useful out of the
endpoint. Tests added to `test_implies` in `test_kprove`.

Co-authored-by: devops <[email protected]>

Author: ehildenb

k-files/simple-proofs.k

@@ -18,6 +18,7 @@ module SIMPLE-PROOFS
     syntax Baz ::= "foo-bar" | "baz" [klabel(baz), symbol]
 
     syntax BarHolder ::= hold ( Foo , Bar ) [klabel(barholder), symbol]
+                       | hold2 ( Bar , Baz ) [klabel(barholder2), symbol]
 
     rule <k> foo => bar ... </k>
          <state> ... 3 |-> N ... </state>

package/version

@@ -1 +1 @@
-0.1.68
+0.1.69

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.68"
+version = "0.1.69"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/integration_tests/test_kore_to_kast.py

@@ -1,5 +1,5 @@
 from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable
-from pyk.kore.syntax import DV, And, App, Ceil, Equals, EVar, LeftAssoc, Not, RightAssoc, SortApp, String
+from pyk.kore.syntax import DV, And, App, Ceil, Equals, EVar, Exists, LeftAssoc, Not, RightAssoc, SortApp, String
 from pyk.ktool import KompileBackend
 from pyk.ktool.kprint import SymbolTable
 from pyk.prelude.kbool import TRUE
@@ -108,6 +108,22 @@ def test_bidirectional(self) -> None:
                     [KVariable('X', sort=KSort('Bool'))],
                 ),
             ),
+            (
+                'ml-exists',
+                KSort('Bool'),
+                Exists(
+                    SortApp('SortBool'),
+                    EVar('VarX', SortApp('SortBool')),
+                    EVar('VarX', SortApp('SortBool')),
+                ),
+                KApply(
+                    KLabel('#Exists', [KSort('Bool')]),
+                    [
+                        KVariable('X', sort=KSort('Bool')),
+                        KVariable('X', sort=KSort('Bool')),
+                    ],
+                ),
+            ),
             (
                 'ml-not',
                 KSort('Bool'),
@@ -222,6 +238,19 @@ def test_kast_to_kore(self) -> None:
                 ),
                 KApply('barholder', [KApply('foo', [KVariable('B', sort=KSort('Baz'))]), KVariable('B')]),
             ),
+            (
+                'variable-with-multi-sort',
+                KSort('BarHolder'),
+                App(
+                    'Lblbarholder2',
+                    [],
+                    [
+                        App('inj', [SortApp('SortBaz'), SortApp('SortBar')], [EVar('VarX', SortApp('SortBaz'))]),
+                        EVar('VarX', SortApp('SortBaz')),
+                    ],
+                ),
+                KApply('barholder2', [KVariable('X', sort=KSort('Baz')), KVariable('X', sort=KSort('Bar'))]),
+            ),
         )
         for name, sort, kore, kast in kore_kast_pairs:
             with self.subTest(name):

src/integration_tests/test_kprove.py

@@ -1,12 +1,13 @@
 from typing import List, Tuple
 
 from pyk.cterm import CTerm
-from pyk.kast.inner import KApply, KAtt, KSequence, KToken, KVariable
+from pyk.kast.inner import KApply, KAtt, KSequence, KSort, KToken, KVariable, Subst
 from pyk.kast.manip import get_cell
 from pyk.kast.outer import KClaim, KRule
 from pyk.ktool import KompileBackend
 from pyk.ktool.kprint import SymbolTable
 from pyk.prelude.kbool import BOOL
+from pyk.prelude.kint import intToken
 
 from .kprove_test import KProveTest
 
@@ -72,13 +73,13 @@ def _config(k: str, state: str) -> CTerm:
                 actual_depth, _actual_state, _actual_next_states = self.kprove.execute(
                     _config(pre_k, pre_state), depth=depth
                 )
-                actual_k = self.kprove.pretty_print(get_cell(_actual_state, 'K_CELL'))
-                actual_state = self.kprove.pretty_print(get_cell(_actual_state, 'STATE_CELL'))
+                actual_k = self.kprove.pretty_print(get_cell(_actual_state.kast, 'K_CELL'))
+                actual_state = self.kprove.pretty_print(get_cell(_actual_state.kast, 'STATE_CELL'))
 
                 actual_next_states = [
                     (
-                        self.kprove.pretty_print(get_cell(s, 'K_CELL')),
-                        self.kprove.pretty_print(get_cell(s, 'STATE_CELL')),
+                        self.kprove.pretty_print(get_cell(s.kast, 'K_CELL')),
+                        self.kprove.pretty_print(get_cell(s.kast, 'STATE_CELL')),
                     )
                     for s in _actual_next_states
                 ]
@@ -233,13 +234,13 @@ def _config(k: str, state: str) -> CTerm:
                 actual_depth, _actual_state, _actual_next_states = self.kprove.execute(
                     _config(pre_k, pre_state), depth=depth
                 )
-                actual_k = self.kprove.pretty_print(get_cell(_actual_state, 'K_CELL'))
-                actual_state = self.kprove.pretty_print(get_cell(_actual_state, 'STATE_CELL'))
+                actual_k = self.kprove.pretty_print(get_cell(_actual_state.kast, 'K_CELL'))
+                actual_state = self.kprove.pretty_print(get_cell(_actual_state.kast, 'STATE_CELL'))
 
                 actual_next_states = [
                     (
-                        self.kprove.pretty_print(get_cell(s, 'K_CELL')),
-                        self.kprove.pretty_print(get_cell(s, 'STATE_CELL')),
+                        self.kprove.pretty_print(get_cell(s.kast, 'K_CELL')),
+                        self.kprove.pretty_print(get_cell(s.kast, 'STATE_CELL')),
                     )
                     for s in _actual_next_states
                 ]
@@ -249,3 +250,54 @@ def _config(k: str, state: str) -> CTerm:
                 self.assertEqual(actual_state, expected_state)
                 self.assertEqual(actual_depth, expected_depth)
                 self.assertCountEqual(actual_next_states, expected_next_states)
+
+    def test_implies(self) -> None:
+        def _config(k: str, state: str) -> CTerm:
+            _k_parsed = self.kprove.parse_token(KToken(k, 'Pgm'), as_rule=True)
+            _state_parsed = self.kprove.parse_token(KToken(state, 'Map'), as_rule=True)
+            return CTerm(
+                KApply(
+                    '<generatedTop>',
+                    [
+                        KApply(
+                            '<T>',
+                            (
+                                KApply('<k>', [KSequence([_k_parsed])]),
+                                KApply('<state>', [_state_parsed]),
+                            ),
+                        ),
+                        KVariable('GENERATED_COUNTER_CELL'),
+                    ],
+                )
+            )
+
+        # Given
+        test_data = (
+            (
+                'constant-subst',
+                ('int $n , $s ; $n = X ;', '.Map'),
+                ('int $n , $s ; $n = 3 ;', '.Map'),
+                Subst({'X': intToken(3)}),
+            ),
+            (
+                'variable-subst',
+                ('int $n , $s ; $n = X ;', '.Map'),
+                ('int $n , $s ; $n = Y ;', '.Map'),
+                Subst({'X': KVariable('Y', sort=KSort('AExp'))}),
+            ),
+        )
+
+        for (
+            name,
+            (antecedent_k, antecedent_map),
+            (consequent_k, consequent_map),
+            expected_subst,
+        ) in test_data:
+            with self.subTest(name):
+                antecedent = _config(antecedent_k, antecedent_map)
+                consequent = _config(consequent_k, consequent_map)
+                # When
+                actual_subst = self.kprove.implies(antecedent, consequent)
+
+                # Then
+                self.assertEqual(actual_subst, expected_subst)

src/pyk/kast/inner.py

@@ -92,6 +92,13 @@ def __mul__(self, other: 'Subst') -> 'Subst':
     def __call__(self, term: KInner) -> KInner:
         return self.apply(term)
 
+    @staticmethod
+    def from_dict(d: Dict[str, Any]) -> 'Subst':
+        return Subst({k: KInner.from_dict(v) for k, v in d.items()})
+
+    def to_dict(self) -> Dict[str, Any]:
+        return {k: v.to_dict() for k, v in self.items()}
+
     def minimize(self) -> 'Subst':
         return Subst({k: v for k, v in self.items() if v != KVariable(k)})
 

src/pyk/kast/outer.py

@@ -1007,10 +1007,14 @@ def sort_vars_subst(self, kast: KInner) -> Subst:
                     for v in voccurrences[1:]:
                         if vsort is None and v.sort is not None:
                             vsort = v.sort
-                        elif vsort is not None and v.sort is not None and vsort != v.sort:
-                            raise ValueError(
-                                f'Could not find common subsort among variable occurrences: {voccurrences}'
-                            )
+                        elif vsort is not None and v.sort is not None:
+                            if vsort != v.sort:
+                                if v.sort in self.subsorts(vsort):
+                                    vsort = v.sort
+                                elif vsort not in self.subsorts(v.sort):
+                                    raise ValueError(
+                                        f'Could not find common subsort among variable occurrences: {voccurrences}'
+                                    )
                 subst[vname] = KVariable(vname, sort=vsort)
         return Subst(subst)
 

src/pyk/kcfg.py

@@ -14,6 +14,7 @@
 from .kast.manip import ml_pred_to_bool, mlAnd, remove_source_attributes, simplify_bool
 from .kast.outer import KClaim, KRule
 from .ktool import KPrint
+from .prelude.ml import mlTop
 from .utils import add_indent, compare_short_hashes, shorten_hash
 
 
@@ -95,20 +96,35 @@ class Cover(EdgeLike):
         subst: Subst
         constraint: KInner
 
-        def __init__(self, source: 'KCFG.Node', target: 'KCFG.Node'):
+        def __init__(
+            self,
+            source: 'KCFG.Node',
+            target: 'KCFG.Node',
+            subst: Optional[Subst] = None,
+            constraint: Optional[KInner] = None,
+        ):
             object.__setattr__(self, 'source', source)
             object.__setattr__(self, 'target', target)
 
-            match_res = target.cterm.match_with_constraint(source.cterm)
-            if not match_res:
-                raise ValueError(f'No matching between: {source.id} and {target.id}')
+            if subst is None and constraint is not None:
+                subst = Subst({})
+            elif subst is not None and constraint is None:
+                constraint = mlTop()
+            elif subst is None and constraint is None:
+                match_res = target.cterm.match_with_constraint(source.cterm)
+                if not match_res:
+                    raise ValueError(f'No matching between: {source.id} and {target.id}')
+                subst, constraint = match_res
 
-            subst, constraint = match_res
             object.__setattr__(self, 'subst', subst)
             object.__setattr__(self, 'constraint', constraint)
 
         def to_dict(self) -> Dict[str, Any]:
-            return {'source': self.source.id, 'target': self.target.id}
+            return {
+                'source': self.source.id,
+                'target': self.target.id,
+                'witness': {'subst': self.subst.to_dict(), 'constraint': self.constraint.to_dict()},
+            }
 
         def pretty(self, kprint: KPrint) -> Iterable[str]:
             return [
@@ -255,7 +271,13 @@ def resolve(node_id: str) -> str:
         for cover_dict in dct.get('covers') or []:
             source_id = resolve(cover_dict['source'])
             target_id = resolve(cover_dict['target'])
-            cfg.create_cover(source_id, target_id)
+            subst = None
+            constraint = None
+            if 'subst' in cover_dict:
+                subst = Subst.from_dict(cover_dict['subst'])
+            if 'constraint' in cover_dict:
+                constraint = KInner.from_dict(cover_dict['constraint'])
+            cfg.create_cover(source_id, target_id, subst=subst, constraint=constraint)
 
         for init_id in dct.get('init') or []:
             cfg.add_init(resolve(init_id))
@@ -600,7 +622,9 @@ def contains_cover(self, cover: Cover) -> bool:
             return cover == other
         return False
 
-    def create_cover(self, source_id: str, target_id: str) -> Cover:
+    def create_cover(
+        self, source_id: str, target_id: str, subst: Optional[Subst] = None, constraint: Optional[KInner] = None
+    ) -> Cover:
         source = self.node(source_id)
         target = self.node(target_id)
 
@@ -610,7 +634,7 @@ def create_cover(self, source_id: str, target_id: str) -> Cover:
         if source.id not in self._covers:
             self._covers[source.id] = {}
 
-        cover = KCFG.Cover(source, target)
+        cover = KCFG.Cover(source, target, subst=subst, constraint=constraint)
         self._covers[source.id][target.id] = cover
         return cover
 

src/pyk/kore/rpc.py

@@ -110,7 +110,7 @@ def request(self, method: str, **params: Any) -> Dict[str, Any]:
         _LOGGER.info(f'Sending request to {server_addr}: {req}')
         self._sock.sendall(req.encode())
         _LOGGER.info(f'Waiting for response from {server_addr}...')
-        resp = self._file.readline()
+        resp = self._file.readline().rstrip()
         _LOGGER.info(f'Received response from {server_addr}: {resp}')
 
         data = json.loads(resp)

src/pyk/ktool/kprint.py

@@ -30,7 +30,7 @@
     read_kast_definition,
 )
 from ..kore.parser import KoreParser
-from ..kore.syntax import DV, And, App, Assoc, Ceil, Equals, EVar, Not, Pattern, SortApp, String
+from ..kore.syntax import DV, And, App, Assoc, Ceil, Equals, EVar, Exists, Not, Pattern, SortApp, String
 from ..prelude.bytes import BYTES, bytesToken
 from ..prelude.k import DOTS, EMPTY_K
 from ..prelude.kbool import TRUE
@@ -324,6 +324,13 @@ def _kore_to_kast(self, kore: Pattern) -> Optional[KInner]:
             if arg is not None:
                 return KApply(KLabel('#Not', [psort]), [arg])
 
+        elif type(kore) is Exists:
+            psort = KSort(kore.sort.name[4:])
+            var = self._kore_to_kast(kore.var)
+            body = self._kore_to_kast(kore.pattern)
+            if var is not None and type(var) is KVariable and body is not None:
+                return KApply(KLabel('#Exists', [psort]), [var, body])
+
         elif type(kore) is Equals:
             osort = KSort(kore.op_sort.name[4:])
             psort = KSort(kore.sort.name[4:])
@@ -418,6 +425,7 @@ def _get_sort(_ki: KInner) -> Optional[KSort]:
 
             elif len(kast.label.params) == 1:
                 psort = kast.label.params[0]
+
                 if kast.label.name == '#And' and kast.arity == 2:
                     larg = self._kast_to_kore(kast.args[0], sort=psort)
                     rarg = self._kast_to_kore(kast.args[1], sort=psort)
@@ -426,6 +434,7 @@ def _get_sort(_ki: KInner) -> Optional[KSort]:
                         if sort is not None:
                             _and = self._add_sort_injection(_and, psort, sort)
                         return _and
+
                 elif kast.label.name == '#Not' and kast.arity == 1:
                     arg = self._kast_to_kore(kast.args[0], sort=psort)
                     if arg is not None:
@@ -434,6 +443,15 @@ def _get_sort(_ki: KInner) -> Optional[KSort]:
                             _not = self._add_sort_injection(_not, psort, sort)
                         return _not
 
+                elif kast.label.name == '#Exists' and kast.arity == 2 and type(kast.args[0]) is KVariable:
+                    var = self._kast_to_kore(kast.args[0])
+                    body = self._kast_to_kore(kast.args[1], sort=psort)
+                    if var is not None and type(var) is EVar and body is not None:
+                        _exists: Pattern = Exists(SortApp('Sort' + psort.name), var, body)
+                        if sort is not None:
+                            _exists = self._add_sort_injection(_exists, psort, sort)
+                        return _exists
+
             elif len(kast.label.params) == 2:
                 osort = kast.label.params[0]
                 psort = kast.label.params[1]
@@ -474,7 +492,9 @@ def _add_sort_injection(self, pat: Pattern, isort: KSort, osort: KSort) -> Patte
         if isort == osort:
             return pat
         if isort not in self.definition.subsorts(osort):
-            raise ValueError(f'Could not find injection from subsort to supersort: {isort} -> {osort}')
+            raise ValueError(
+                f'Could not find injection from subsort to supersort {isort} -> {osort} for pattern: {pat}'
+            )
         return App('inj', [SortApp('Sort' + isort.name), SortApp('Sort' + osort.name)], [pat])
 
     def pretty_print(self, kast: KAst) -> str: