klab-prove: toggle deterministic functions

[asymmetric]

This fixes the non-determinism we were seeing in some proofs.
The reason was that there was more than one function defined for
sizeWordStack, one of which is problematic, and they were being
chosen non-deterministically.

---

I've created this PR from magit!!! 🚀

[asymmetric]

Quite interesting that there are CI failures for this one.

[d-xo]

rebased on master

[asymmetric]

[Error] Critical: [non-deterministic function definition]: more than one rule can apply to the term:
#if_#then_#else_#fi_K-EQUAL(_andBool_(_andBool_(notBool_(_==K_(Temperature_1790:Int,, _+Int_(ABI_x_1787:Int,, Temperature_1790:Int))),, _==K_(Junk_0_1783:Int,, Temperature_1790:Int)),, _==K_(_+Int_(ABI_x_1787:Int,, Temperature_1790:Int),, Int(#"0"))),, Int(#"15000"),, _+Int_(#if_#then_#else_#fi_K-EQUAL(_andBool_(_andBool_(notBool_(_==K_(Temperature_1790:Int,, _+Int_(ABI_x_1787:Int,, Temperature_1790:Int))),, notBool_(_==K_(Junk_0_1783:Int,, Temperature_1790:Int))),, notBool_(_==K_(Junk_0_1783:Int,, Int(#"0")))),, #if_#then_#else_#fi_K-EQUAL(_==K_(Temperature_1790:Int,, Int(#"0")),, Int(#"-15000"),, #if_#then_#else_#fi_K-EQUAL(_==K_(_+Int_(ABI_x_1787:Int,, Temperature_1790:Int),, Int(#"0")),, Int(#"15000"),, Int(#"0"))),, Int(#"0")),, #if_#then_#else_#fi_K-EQUAL(_andBool_(notBool_(_==K_(Temperature_1790:Int,, _+Int_(ABI_x_1787:Int,, Temperature_1790:Int))),, _==K_(Junk_0_1783:Int,, _+Int_(ABI_x_1787:Int,, Temperature_1790:Int))),, _+Int_(#if_#then_#else_#fi_K-EQUAL(_==K_(Junk_0_1783:Int,, Int(#"0")),, Int(#"15000"),, Int(#"0")),, Int(#"4200")),, Int(#"0"))))

Candidate rules:
    rule #if C1 #then A #else (B +Int #if C2 #then B2 #else B3 #fi) #fi =>
         #if C1 #then A #else B #fi +Int #if (C2 andBool notBool C1) #then B2 #else 0 #fi +Int #if ((notBool C2) andBool (notBool C1)) #then B3 #else 0 #fi
        Source: /home/asymmetric/klab/examples/multipleCalls/out/rules.k Location(319,10,320,156)
  rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C
        Source: /home/asymmetric/klab/evm-semantics/deps/k/k-distribution/target/release/k/include/builtin/domains.k Location(870,8,870,67)

This is saying that this clashes with this on Callee_tempDelta_pass_rough.

@MrChico is the rule there for performance reasons? If so, does it make sense to remove it? Or can we instead mark it concrete?

I'm also wondering about these rules. They will also clash, as the rule in domains.k is extremely generic.

[asymmetric]

40d3201 fixes the issue in Callee_tempDelta_pass_rough.

[d-xo]

rebased on master

[d-xo]

Vat_subui_fail_rough, ConstantTemp_sub_fail_rough, and Callee_add_fail_rough both fail because the following rules clash:

Candidate rules:
    rule (A +Int B) -Int C  => A +Int (B -Int C)
        Source: /home/me/code/dapphub/klab/deterministic-functions/examples/multipleCalls/out/rules.k Location(356,10,356,49)
    rule A -Int A => 0
        Source: /home/me/code/dapphub/klab/deterministic-functions/examples/multipleCalls/out/rules.k Location(455,10,455,23)

[d-xo]

Vat_heal_fail_rough fails because of the following collision:

rule A -Word #unsigned(B) => A -Int B
  requires #rangeUInt(256, A)
  andBool #rangeSInt(256, B)
  andBool #rangeUInt(256, A -Int B)
        Source: /home/me/code/dapphub/klab/deterministic-functions/examples/heal/out/rules.k Location(587,6,590,36)
rule W0 -Word W1 => W0 -Int W1 requires W0 >=Int W1
        Source: /home/me/code/dapphub/klab/deterministic-functions/evm-semantics/.build/defn/java/evm-types.k Location(218,10,218,56)

[d-xo]

@MrChico @mhhf @livnev I don't really have the nescessary context to determine which of the above rules can be removed without causing issues, would really appreciate some input here 🙏 ✨.

Once we have a clean run of the klab test suite, I'll merge this and start working to make k-uniswap deterministic.

[MrChico]

I vote to keep A - A => 0 and rule A -Word #unsigned(B) => A -Int B

[d-xo]

@MrChico rule A -Word #unsigned(B) => A -Int B conflicts with a rule inside evm-types.md and so would require a patch against evm semantics, are you OK with this?

Why is rule A -Word #unsigned(B) => A -Int B required?

[MrChico]

#rangeUInt256(A -Int B) => A >= #unsigned(B)