kore-rpc - Return branch rule id and condition

[goodlyrottenapple]

This PR adds new fields to the next-states objects, namely:

• new rule-id and rule-predicate field
• rename substitution to rule-substitution (should not break anything because the substitution field is optional and most likely always empty)

The rule-predicate term is a subterm of predicate and signals the requires clause predicate that was undecidable and thus caused branching. Note that variables inside rule-predicate may not always be present in the configuration. E.g. consider the following two rules

rule [AB]: <k> a => b ... </k> <val> V </val> requires V ==Int 0
rule [AC]: <k> a => c ... </k> <val> V </val> requires notBool (V ==Int 0)

With <T><k> a ~> . </k> <val> X </val></T> sent to the server. The response will be the following:

{
  "jsonrpc": "2.0",
  "id": 1,
  "result": {
    "reason": "branching",
    "depth": 0,
    "state": <T><k> a ~> . </k> <val> X </val></T>
    "next-states": [
      {
        "term": <T><k> c ~> . </k> <val> X </val></T>,
        "predicate": #Not (X #Equals 0),
        "rule-id": "6974170fb1496dc2cae5b77afce0c12386d66ce73a4b2344c6512681ba06c70d",
        "rule-predicate": #Not (X #Equals 0),
        "rule-substitution": {...}
      },
      {
        "term": <T><k> b ~> . </k> <val> 0 </val></T>,
        "rule-id": "79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b",
        "rule-predicate": X #Equals 0,
        "substitution": VarV #Equals X #And X #Equals 0 #And ...
      }
    ]
  }
}

Notice that the backend eagerly applies substitutions, so on the branch where X ==Int 0 holds, the backend simply substitutes X for 0.

[goodlyrottenapple]

Will add changes to the RPC serever doc, once I confirm with @ehildenb and @tothtamas28 if the format above works.

[tothtamas28]

I'm not sure whether we want to try to change this behaviour, because we would either have to stop the backend from applying the substitution or else return a condition X ==Int 0 where X would no longer be in the configuration

So if I understand correctly, in all the design alternatives, rule-id, rule-substitution and predicate are the same, and the open questions are the following.

1. Should rule-predicate be provided, even if it refers to variables not present in term?
2. Should rule-substitution be applied to term?

Question 1

Is X |-> 0 still present in therule-substitution for the X ==Int 0 branch? Because in that case, I don't think the variable missing from the term is a problem, as the client still can correlate things based on the substitution. Also, the rule-predicate is not something we can easily reproduce on the client side, so it'd be important to have it in the response.

Question 2

Doing the substitution is fine I think, as reproducing the unapplied term is possible on the client side based on the rule-substitution. But suppose the substitution is not applied. Is there still enough information in the term so that the client can feed it back and continue search from where the backend left off? In that case, I think not doing the substitution is okay too.

[goodlyrottenapple]

@tothtamas28 I went with option 1, i.e. X|-> 0 appearing in both the rule-substitution and the rule-predicate. Btw, given we are renaming the substitution field, should we change the structure to previously discussed #3608 ?

[tothtamas28]

I went with option 1, i.e. X|-> 0 appearing in both the rule-substitution and the rule-predicate

Sounds good.

Note however that "yes/no to (1)" and "yes/no to (2)" are independent design choices, so (2) still needs to be addressed somehow. I personally do not have a strong opinion at this point, but don't have perfect understanding either (see the question above regarding term).

Btw, given we are renaming the substitution field, should we change the structure to previously discussed #3608 ?

Can we do the renaming and the structural change in a subsequent PR? So basically, split the change into a non breaking and a breaking part.

[goodlyrottenapple]

Hmm there is maybe some misunderstanding on my part what exactly substitution is meant to be. Atm it is basically always empty as far as i can tell. This PR populates it (or rather the renamed rule-substitution) with the result of unifying the previous state with the LHS of the given rule, so it will contain rule variables mapped to subterms of the configuration. In the case above, the substitution will additionally contain mapping of variables from the configuration to concrete values, learned from the rule side condition, i.e. in the example above the map will contain VarV |-> X, X |-> 0. The rule-substitution is always applied to RHS of the rule and returned as a next state.

[goodlyrottenapple]

Can we do the renaming and the structural change in a subsequent PR? So basically, split the change into a non breaking and a breaking part.

Sure, I won't introduce the format change and can keep substitution instead of rule-substitution, but just wanted to ask/confirm what pyk currently does with this field.

[tothtamas28]

just wanted to ask/confirm what pyk currently does with this field

Besides parsing the field into a pattern object nothing meaningful I think.

[goodlyrottenapple]

Besides parsing the field into a pattern object nothing meaningful I think.

Great, I will revert the filed name for now

[geo2a]

👍

[goodlyrottenapple]

I ran the kevm test suite with no real differences. The kontrol tests still seem broken:

Test	sam-branching-rule-conditions time	master-1562646 time	(sam-branching-rule-conditions/master-1562646) time
bihu/forwardToHotWallet-failure-1-spec.k	26.63	33.47	0.7956378846728414
mcd/vat-muluu-pass-spec.k	107.47	112.14	0.9583556268949527
erc20/hkg/transferFrom-failure-2-spec.k	25.1	26.04	0.9639016897081414
erc20/hkg/transfer-failure-2-spec.k	24.99	25.89	0.9652375434530706
erc20/ds/allowance-spec.k	33.05	31.65	1.0442338072669826
bihu/forwardToHotWallet-success-2-spec.k	34.73	26.96	1.2882047477744805
TOTAL	251.97	256.15000000000003	0.983681436658208

[goodlyrottenapple]

Test	sam-branching-rule-conditions time	master-1562646 time	(sam-branching-rule-conditions/master-1562646) time
LabelTest.testLabel()	33.52	37.41	0.8960171077252074
LoopsTest.sum_N(uint256)	191.46	209.33	0.9146323986050733
BlockParamsTest.testWarp(uint256)	39.73	42.5	0.9348235294117646
AssumeTest.test_assume_true(uint256,uint256)	41.85	44.56	0.9391831238779174
AssumeTest.testFail_assume_false(uint256,uint256)	60.34	63.41	0.9515849235136414
UintTypeTest.test_uint256(uint256)	31.37	32.84	0.9552375152253348
ChainIdTest.test_chainid_setup()	70.76	74.04	0.95569962182604
RollTest.test_roll_setup()	68.25	71.15	0.9592410400562191
Setup2Test.testFail_setup()	93.01	96.93	0.95955844423811
StoreTest.testStoreLoadNonExistent()	56.92	59.31	0.9597032540886865
BlockParamsTest.testRoll(uint256)	40.76	42.47	0.9597362844360725
BMCLoopsTest.test_countdown_symbolic(uint256)	138.58	144.24	0.9607598447032724
MethodDisambiguateTest.test_method_call()	24.66	25.65	0.9614035087719299
SymbolicStorageTest.testEmptyInitialStorage(uint256)	45.0	46.78	0.9619495510902095
PlainPrankTest.test_startPrank_zeroAddress_true()	159.73	166.03	0.9620550502921158
BlockParamsTest.testCoinBase()	36.26	37.66	0.9628252788104089
CounterTest.testIncrement()	167.4	173.85	0.9628990509059535
SetUpDeployTest.test_extcodesize()	99.69	103.51	0.96309535310598
StoreTest.testStoreLoad()	74.13	76.97	0.963102507470443
PlainPrankTest.test_startPrank_true()	152.76	158.55	0.9634815515610217
StoreTest.testLoadNonExistent()	44.12	45.79	0.9635291548373007
PrankTestMsgSender.test_msgsender_setup()	143.3	148.71	0.9636204693699146
PlainPrankTest.test_stopPrank_notExistent()	38.78	40.22	0.964196916956738
PlainPrankTest.test_prank_zeroAddress_true()	178.02	184.62	0.9642508937276568
PrankTestOrigin.test_origin_setup()	139.77	144.95	0.9642635391514317
PlainPrankTest.testFail_startPrank_internalCall()	54.07	56.06	0.9645023189439885
StoreTest.testGasLoadWarmUp()	77.74	80.56	0.964995034756703
StartPrankTestMsgSender.test_startprank_msgsender_setup()	140.78	145.85	0.9652382584847446
PlainPrankTest.test_prank_expectRevert()	112.11	116.14	0.9653004993972791
StartPrankTestOrigin.test_startprank_origin_setup()	141.68	146.74	0.9655172413793104
BytesTypeTest.test_bytes4(bytes4)	28.17	29.17	0.9657182036338704
PlainPrankTest.test_startPrankWithOrigin_true()	152.54	157.89	0.9661156501361707
TOTAL	2877.26	3003.89	0.9578446614223558