Fix unsimplified bytes2int o int2bytes patterns.

[Stevengre]

No description provided.

[tothtamas28]

IIUC the issue is that this rewrite does not work, and the simplification sequence that should take place is something like:

1. Bytes2Int(Int2Bytes(1, (X +Int Y +Int Z &Int 4294967295) >>Int 8, LE), LE, Unsigned)

0 <=Int 1 ✅
0 <=Int (X +Int Y +Int Z &Int 4294967295) >>Int 8 ✅
by bytes2int-int2bytes:

2. ((X +Int Y +Int Z &Int 4294967295) >>Int 8) &Int (2 ^Int (1 *Int 8) -Int 1)

by constant propagation:

3. (X +Int Y +Int Z &Int 4294967295) >>Int 8) &Int 255

If that's the case, then the problematic part indeed seems to be showing 0 <=Int (X +Int Y +Int Z &Int 4294967295) >>Int 8. Consider adding a dedicated functional test for this.

CC @jberthold

[Stevengre]

If that's the case, then the problematic part indeed seems to be showing 0 <=Int (X +Int Y +Int Z &Int 4294967295) >>Int 8. Consider adding a dedicated functional test for this.

Sorry, but I don't quite understand what does you mean about adding a dedicated functional test for this?

[Stevengre]

This is the simplified pattern for this test (Node 3):

Node 3:

<riscv>
    <instrs>
      #HALT ~> .K
    </instrs>
    <regs>
      26 |-> ( X:Int >>Int 8 ) +Int ( Y:Int >>Int 8 ) +Int ( Z:Int >>Int 8 ) &Int 255
      27 |-> Bytes2Int ( Int2Bytes ( 1 , ( Bytes2Int ( substrBytes ( W3:Bytes , 8 , 12 ) , LE , Unsigned ) +Int Y:Int +Int Z:Int &Int 4294967295 ) >>Int 8 , LE ) , LE , Unsigned )
      28 |-> 1
    </regs>

As you can see, 26 is simplified successfully but 27 keeps unchanged.

[Stevengre]

The failed rewriting is still unchanged after providing the following condition:

andBool 0 <=Int Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned)

and I cannot find this condition in node 3.

[jberthold]

How about the Y and Z, are they constrained in any way?
The rule https://github.com/runtimeverification/riscv-semantics/pull/137/files#diff-686f3abe669ed3a3f63669576b1d85e3f5932c17acaec672cf1a98d637e69bbdR164 requires 0 <= V but that's not immediately clear if for example Y < 0
Well... on the other hand &Int 2 ^Int 32 will indeed make anything positive AFAICT but the related simplification requires andBool: 0 <=Int A &Int B => true requires 0 <=Int A _andBool_ 0 <=Int B

[Stevengre]

 andBool 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z
 andBool 0 <=Int Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned)

[Stevengre]

I changed to this rule [int-and-ineq]: 0 <=Int _ &Int B => true requires 0 <=Int B [simplification], but still doesn't work. Should I make it specific to 4294967295?

[tothtamas28]

Sorry, but I don't quite understand what does you mean about adding a dedicated functional test for this?

If you suspect that a simplification rule does not apply due to a precondition, you can extract a test for the precodition itself. For example:

claim <k> runLemma( 0 <=Int (X +Int Y +Int Z &Int 4294967295) >>Int 8 ) =>
          doneLemma( true ) </k>
  requires 0 <=Int X
   andBool 0 <=Int Y
   andBool 0 <=Int Z

This is how it's done in evm-semantics: https://github.com/runtimeverification/evm-semantics/blob/62c2eaaa73827895362b2f249a139b6d7a65302b/tests/specs/functional/lemmas-spec.k

[Stevengre]

This rewrite works

31 |-> (Bytes2Int(Int2Bytes(1, (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295), LE), LE, Unsigned) => (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 255 ))

does it mean that the problem is caused by >>Int 8?

[Stevengre]

Thank you! This is what I've tested for the precondition:

28 |-> (Bool2Word(0 <=Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned)) => 1)

Therefore, it looks the same for these two patterns:

Bytes2Int(Int2Bytes(1, (X +Int Y +Int Z &Int 4294967295) >>Int 8, LE), LE, Unsigned)

Bytes2Int(Int2Bytes(1, (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295) >>Int 8, LE), LE, Unsigned)

[jberthold]

Probably we could say 0 <=Int A &Int B => true requires 0 <=Int B here?
K uses 2-s complement in infinite precision so if A is negative it starts with an "infinite" sequence of ...11111... that would get removed if B is not also negative.

[Stevengre]

Sure! Let me try this. Additionally, do we need to add preserve-definedness attribute to this simp rule?

[Stevengre]

updated this simp rule and k version. still doesnt' work.

[tothtamas28]

So if the simplification rule is:

rule [bytes2int-int2bytes]:
  Bytes2Int(Int2Bytes(LEN, V, LE), LE, Unsigned) =>
  V &Int (2 ^Int (LEN *Int 8) -Int 1)
requires 0 <=Int LEN
 andBool 0 <=Int V [simplification(45), preserves-definedness]

and the LHS is:

Bytes2Int(Int2Bytes(1, (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295) >>Int 8, LE), LE, Unsigned)

then:

LEN |-> 1
V   |-> (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295) >>Int 8

and the preconditions are the following:

0 <=Int 1
0 <=Int (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295) >>Int 8

Out of the two preconditions, the first one is trivial. Do you have a test for the second preconditon?

Once you have that, and you've confirmed that it indeed fails, you can start decomposing the problem by abstracting subterms to figure out which one is problematic. For example, does

0<=Int X >>Int 8 => true
  requires 0 <=Int X

hold? If not, you have a new lemma, If so, let's continue with X. Does

0 <=Int Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295 => true
  requires 0 <=Int Y andBool 0 <=Int Z

hold? Etc.

[Stevengre]

Thank you! Let me try!

[Stevengre]

3 |-> (Bool2Word(0 <=Int (Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295) >>Int 8) => 1) // fail
4 |-> (Bool2Word(0 <=Int X >>Int 8) => 1) // pass
5 |-> (Bool2Word(0 <=Int Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295) => 1) // pass

[tothtamas28]

Okay, this looks like the root cause. To simplify exposition, we basically have

(3) 0 <=Int complex-term >>Int 8 => true                     // fail
(4) 0 <=Int X            >>Int 8 => true requires 0 <=Int X  // pass
(5) 0 <=Int complex-term         => true                     // pass

The backend is obviously not clever enough to infer (3) from (4) and (5), it's not how it works. But @jberthold, what is the workaround in such a case? Is there a way to utilize theory reasoning by marking some of the simplifications smt-lemma-s?

[Stevengre]

It's confused for me that why (5) is passed and (30) is failed, because complex-term is already complex.

Another fact confuses me is that the (Bytes2Int(Int2Bytes(1, (X +Int Y +Int Z &Int 4294967295) >>Int 8, LE), LE, Unsigned) => (X +Int Y +Int Z &Int 4294967295 ) >>Int 8 &Int 255) is passed, but the more complex one doesn't. However, the main difference between them is just the fact that 0 <=Int Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned).

BTW, terms passed with condition 0 <=Int ( Bytes2Int ( substrBytes ( W3:Bytes , 8 , 12 ) , LE , Unsigned ) +Int Y:Int +Int Z:Int &Int 4294967295 ) >>Int 8

[Stevengre]

Add smt-lemma doesn't work.

[Stevengre]

I'm thinking that why must we have 0 <=Int V for Bytes2Int(Int2Bytes(LEN, V, LE), LE, Unsigned) => V &Int (2 ^Int (LEN *Int 8) -Int 1)? In fact the following is passed:

6 |-> (-1 &Int 255 => 255) // passed

Even if not correct, we can add more process for the RHS's V to make it align with the concrete execution result.

[tothtamas28]

Yes, I think it's safe to drop 0 <=Int V from the requires clause of bytes2int-int2bytes.

[tothtamas28]

Add smt-lemma doesn't work.

Adding it to which simplification rule(s)?

[Stevengre]

To all the <=Int rules.