Annotating rules that preserve definedness

[PetarMax]

This PR aims to annotate all of the KEVM rules for which we know that they preserve definedness, but the backend is not able to prove this on its own.

[PetarMax]

By moving this account creation here, the [owise] guarantees that ACCT is not in the <accounts> map, and the rule preserves definedness. Previosly, with the account creation isolated inside #newFreshAccount, which could be in principle called from anywhere, this would not hold.

[PetarMax]

@jberthold Is there a systematic way of understanding all of the rules for which the backend cannot establish preservation of definedness?

[jberthold]

@jberthold Is there a systematic way of understanding all of the rules for which the backend cannot establish preservation of definedness?

We have plans to make this available as a log level or with a CLI option, runtimeverification/hs-backend-booster#459 but there might be higher-priority things getting in the way (and I will be away to another funeral in my family :-| next week).
We have the output in a dev tool parsetest which you could use if you build hs-backend-booster from source.

[palinatolmach]

@ehildenb @PetarMax the kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k fails in the booster CI job consistently with the smt solver error, which the backend team recommended to interpret as an SMT timeout. It also fails locally on my machine, unless I increase the solver timeout in test_pyk_prove significantly — 1.6 seconds is the smallest one that makes the test pass on my machine. So we can either

• bump the timeout in test_pyk_prove to 1.6s, or
• skip this test in the Booster integration CI job

but I wanted to ask for your opinion first.

This might also indicate that we should bump the default timeout in KEVM and Kontrol.

[PetarMax]

I would like to know what the SMT query in question is.

[jberthold]

I would like to know what the SMT query in question is.

We can take a transcript of the SMT interactions with the --solver-transcript <PATH> option (to clarify, it will write two transcripts for the two solver bindings when using booster).
@palinatolmach if this fails locally on your machine, you could maybe add that option via kore-rpc-command (if that's supported by the test runner)?

[palinatolmach]

These are the transcripts of SMT interactions, and I also attached the error message with the term:
timeout-smtlib.kore.txt
timeout-smtlib.txt
timeout-term.txt

If I understand correctly, here's the relevant part of the SMT logs:

; /* T Fn D Sfa */ ConfigVarVV0'Unds'a'Unds'114b9705:SortInt{} -> <0>
(declare-fun <0> () Int )
; success

; /* T Fn D Sfa */ ConfigVarVV1'Unds'b'Unds'114b9705:SortInt{} -> <1>
(declare-fun <1> () Int )
; success

; /* Sfa */
; \equals{SortBool{}, _}(
;     /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"),
;     /* Fn Sfa */
;     Lbl'Unds-LT-'Int'Unds'{}(
;         /* Fn Sfa */
;         Lbl'UndsSlsh'Word'UndsUnds'EVM-TYPES'Unds'Int'Unds'Int'Unds'Int{}(
;             /* T Fn D Sfa Cl */
;             \dv{SortInt{}}("115792089237316195423570985008687907853269984665640564039457584007913129639935"),
;             /* Fn Sfa */
;             Lbl'UndsSlsh'Int'Unds'{}(
;                 /* T Fn D Sfa */
;                 Lbl'UndsStar'Int'Unds'{}(
;                     /* T Fn D Sfa */
;                     ConfigVarVV0'Unds'a'Unds'114b9705:SortInt{},
;                     /* T Fn D Sfa */ ConfigVarVV1'Unds'b'Unds'114b9705:SortInt{}
;                 ),
;                 /* T Fn D Sfa Cl */ \dv{SortInt{}}("1000000000000000000")
;             )
;         ),
;         /* T Fn D Sfa Cl */ \dv{SortInt{}}("1000000000000000000")
;     )
; ) -> <2>
(declare-fun <2> () Bool )
; success

; /* T Fn D Sfa */ ConfigVarCALLER'Unds'ID:SortInt{} -> <3>
(declare-fun <3> () Int )
; success

; /* T Fn D Sfa */ ConfigVarORIGIN'Unds'ID:SortInt{} -> <4>
(declare-fun <4> () Int )
; success

; /* T Fn D Sfa */ ConfigVarNUMBER'Unds'CELL:SortInt{} -> <5>
(declare-fun <5> () Int )
; success

(assert (and (and (and (= false (and (not (= <0> 0 ) ) (< (div 115792089237316195423570985008687907853269984665640564039457584007913129639935 <0> ) <1> ) ) ) (and <2> (= true (< 0 <0> ) ) ) ) (and (= true (< 0 <1> ) ) (and (= true (< <3> 1461501637330902918203684832716283019655932542976 ) ) (and (= true (< <4> 1461501637330902918203684832716283019655932542976 ) ) (= true (< <0> 115792089237316195423570985008687907853269984665640564039457584007913129639936 ) ) ) ) ) ) (and (= true (< <1> 115792089237316195423570985008687907853269984665640564039457584007913129639936 ) ) (and (and (= true (<= 0 <3> ) ) (and (= true (<= 0 <5> ) ) (= true (<= 0 <4> ) ) ) ) (and (= true (<= 0 <0> ) ) (and (= true (<= 0 <1> ) ) (and (= true (<= <5> 57896044618658097711785492504343953926634992332820282019728792003956564819967 ) ) (and (= true (<= <1> (div 115792089237316195423570985008687907853269984665640564039457584007913129639935 <0> ) ) ) (and (not (= 0 (div (* <0> <1> ) 1000000000000000000 ) ) ) (not (= <0> 0 ) ) ) ) ) ) ) ) ) ) )
; success

(check-sat )
; unknown

(get-info :reason-unknown )
; (:reason-unknown "canceled")

[palinatolmach]

@ehildenb said that he's fine with keeping the timeout of 1.6s and that we can also increase the default timeout in KEVM and Kontrol (I can do it, if we all agree on it).

[palinatolmach]

After a discussion with @PetarMax, we decided to skip the failing test on booster and keep the 300ms timeout since it's sufficient for all other tests; I created an issue to track the investigation on the skipped test: #2314.

[palinatolmach]

@PetarMax shall we get it merged, or are we waiting for some more feedback from the reviewers?