|
| 1 | +requires "verification.k" |
| 2 | + |
| 3 | +module EQ-FALSE-LT-LOOP-SPEC |
| 4 | + imports VERIFICATION |
| 5 | + |
| 6 | + // Regression exemplar for the SECOND CSE non-termination layer (evm-semantics #2859 / kontrol #1153), |
| 7 | + // the one that remains after `asWord-eq-false` is removed. See `evm-semantics-cse-loop-change-request.md`. |
| 8 | + // |
| 9 | + // HOW THIS WAS FOUND: rebuilding KEVM with `asWord-eq-false` deleted (branch `asword-eq-false-loop-fix`, |
| 10 | + // == kontrol-side "variant A") does NOT stop the CSE proofs hanging — proof #4 |
| 11 | + // `ArithmeticCallTest.test_double_add_sub_external` still spins >25 min in one `execute` request. The |
| 12 | + // loop simply RELOCATES. Server-side context logging of the hanging request shows two rules dominating, |
| 13 | + // ~16-17k attempts each, in two different engines under the same execute request: |
| 14 | + // |
| 15 | + // * booster > execute > simplify > … > [eq-false-lt] > smt (15 865 attempts) |
| 16 | + // rule [eq-false-lt]: A:Int ==Int B:Int => false requires A <Int B [simplification, concrete(B)] |
| 17 | + // * kore > execute > constraint > term:90151e4 > <AccountCellMap #Ceil> > success (17 082 attempts, |
| 18 | + // re-firing on the SAME constraint term) |
| 19 | + // |
| 20 | + // MECHANISM (a two-engine fixpoint failure, NOT a single self-loop like asWord-eq-false): |
| 21 | + // 1. `#Ceil(<accounts> AccountCellMap)` definedness requires the account ids be DISTINCT, i.e. it emits |
| 22 | + // predicates of the form `ACCOUNT_ID ==Int <concrete account address> => false`. |
| 23 | + // 2. `eq-false-lt` (concrete RHS) is invited to discharge each one via its side condition |
| 24 | + // `ACCOUNT_ID <Int <concrete address>`. With ACCOUNT_ID a symbolic account id constrained only to a |
| 25 | + // range (e.g. `[0, pow160)`) that does NOT decide the comparison, SMT returns (Sat,Sat) — |
| 26 | + // UNDETERMINED (2 518 such verdicts captured). The rule cannot fire and the predicate cannot reduce. |
| 27 | + // 3. Because the account-distinctness predicate never simplifies to a stable form, the Kore constraint |
| 28 | + // simplifier never reaches a fixpoint and re-evaluates the AccountCellMap `#Ceil` on the same term |
| 29 | + // thousands of times — each pass paying a fresh ~500 ms undetermined SMT round-trip per account id. |
| 30 | + // |
| 31 | + // The captured concrete address is `645326474426547203313410069153905908525362434349` (a 160-bit value); |
| 32 | + // the symbolic ids were CALLER_ID, ORIGIN_ID, and the deployed-contract ids. |
| 33 | + // |
| 34 | + // SCOPE / CAVEAT — READ BEFORE RELYING ON THIS: |
| 35 | + // The faithful trigger is the INTERACTION of AccountCellMap definedness with `eq-false-lt`, driven by |
| 36 | + // the Kore constraint simplifier's lack of a fixpoint guard. A bare `runLemma(ACCT ==Int <concrete>)` |
| 37 | + // (claim 1 below) reproduces the EXPENSIVE-UNDETERMINED-SMT step but will most likely return the term |
| 38 | + // undetermined ONCE rather than spin, because the AccountCellMap `#Ceil` that re-presents the predicate |
| 39 | + // is absent. Claim 2 adds a two-account `<accounts>` cell so the definedness machinery is in play; this |
| 40 | + // is the closer reproduction, but whether it spins depends on the backend's constraint-simplification |
| 41 | + // fixpoint behaviour, which is the real defect. Please run BOTH on the buggy build and report which |
| 42 | + // actually loops; the primary recommendation to the team is a backend fixpoint/termination guard plus |
| 43 | + // making `eq-false-lt` cheap (or skipped) when `A <Int B` is undetermined — not a lemma deletion. |
| 44 | + |
| 45 | + // Claim 1 — the eq-false-lt undetermined-SMT step in isolation (the per-pass cost of the loop). |
| 46 | + // Exactly the captured comparison: symbolic account id vs the concrete address, range-bounded so that |
| 47 | + // `ACCT_ID <Int 645…349` is undetermined. |
| 48 | + claim [eq-false-lt-undetermined-acctid]: |
| 49 | + <k> runLemma ( ACCT_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) |
| 50 | + => doneLemma ( ?_RESULT:Bool ) ... </k> |
| 51 | + requires 0 <=Int ACCT_ID andBool ACCT_ID <Int pow160 |
| 52 | + |
| 53 | + // Claim 2 — closer reproduction: two symbolic-id accounts in the <accounts> cell, so evaluating the |
| 54 | + // configuration's definedness invokes the AccountCellMap `#Ceil` that emits the account-distinctness |
| 55 | + // predicate `ACCT_ID_1 ==Int ACCT_ID_2 => false`, which `eq-false-lt` then tries (and fails) to discharge. |
| 56 | + // Both ids are range-bounded but unordered, so the distinctness comparison is undetermined — the captured |
| 57 | + // shape. (Adjust the cell context to match the project's VERIFICATION module if `<accounts>` is wrapped.) |
| 58 | + claim [eq-false-lt-acctmap-definedness]: |
| 59 | + <k> runLemma ( .Bytes ) => doneLemma ( .Bytes ) ... </k> |
| 60 | + <accounts> |
| 61 | + <account> <acctID> ACCT_ID_1:Int </acctID> ... </account> |
| 62 | + <account> <acctID> ACCT_ID_2:Int </acctID> ... </account> |
| 63 | + ... |
| 64 | + </accounts> |
| 65 | + requires 0 <=Int ACCT_ID_1 andBool ACCT_ID_1 <Int pow160 |
| 66 | + andBool 0 <=Int ACCT_ID_2 andBool ACCT_ID_2 <Int pow160 |
| 67 | + |
| 68 | +endmodule |
0 commit comments