Read symbolic value at symbolic address

[Stevengre]

No description provided.

[tothtamas28]

Consider DROP > I. In that case, WriteBytes(I -Int DROP, ...) is .SparseBytes.

[Stevengre]

WriteBytes and #WB have different behaviors. #WB currently doesn't handle index < 0.

I'll be adding a rule to #WB so that I < 0 acts as a no-op (only written bytes are kept).

[tothtamas28]

That doesn't seem to be sufficient. Consider a case where I <Int DROP <Int I +Int NUM:

I = 0
NUM = 2
DROP = 1
V = 65535
B = b"=\x00\x00"  // I will treat SparseBytes as Bytes for simplicity
FLAG = true

LHS:
dropFront(DROP, #WB(FLAG, I, V, NUM, B)) =>
dropFront(1, #WB(true, 0, 65535, 2, b"\x00\x00")) =>
dropFront(1, b"\xff\xff") =>
b"\xff"

RHS:
#WB(FLAG, I -Int DROP, V, NUM, dropFront(DROP, B)) =>
#WB(true, 0 -Int 1, 65535, 2, dropFront(1, b"\x00\x00")) =>
#WB(true, -1, 65535, 2, b"x00")) =>
b"x00"

[tothtamas28]

effectively dropping the first N bytes from the sparse byte structure while maintaining the integer value semantics of the remaining bytes

Can you give an example? E.g., using syntax somewhat freely, given a bytes value

0x01 0x02 0x03 0x04

dropFront 1 gives

0x02 0x03 0x04

What does >>SparseBytes 1 evaluate to? Is it

0x00 0x01 0x02 0x03

[Stevengre]

On concrete, dropFront and >>SparseBytes behave identically. The only difference arises during symbolic writes to the queue, specifically for #WB. This distinction is crucial for the pickFront rule, which handles cases like writing a small num followed by a large num (e.g., as seen in our test specs: 5 |->).

[tothtamas28]

So this is an alias for dropFront used in simplification rules? I want to rule out the case that the symbolic and concrete semantics of >>SparseBytes differ.

[Stevengre]

Yes, you can understand >>Sparse as being specifically for handling a special case of #WB under pickFront that the previous dropFront simplification rule couldn't handle. And the dropFront simplification rule is indeed correct.

[tothtamas28]

That doesn't seem to be sufficient. Consider a case where I <Int DROP <Int I +Int NUM:

I = 0
NUM = 2
DROP = 1
V = 65535
B = b"=\x00\x00"  // I will treat SparseBytes as Bytes for simplicity
FLAG = true

LHS:
dropFront(DROP, #WB(FLAG, I, V, NUM, B)) =>
dropFront(1, #WB(true, 0, 65535, 2, b"\x00\x00")) =>
dropFront(1, b"\xff\xff") =>
b"\xff"

RHS:
#WB(FLAG, I -Int DROP, V, NUM, dropFront(DROP, B)) =>
#WB(true, 0 -Int 1, 65535, 2, dropFront(1, b"\x00\x00")) =>
#WB(true, -1, 65535, 2, b"x00")) =>
b"x00"

[tothtamas28]

I think there is a similar counterexample here for the I <Int SHIFT <Int I +Int NUM case.

[tothtamas28]

In fact, these two simplifications look analogous on the LHS but differ on the RHS:

LHS
dropFront(DROP, #WB(FLAG, I, V, NUM, B:SparseBytes))
vs
#WB(FLAG, I, V, NUM, B:SparseBytes) >>SparseBytes SHIFT

RHS
#WB(FLAG, I -Int DROP, V, NUM, dropFront(DROP, B))
vs
#WB(FLAG, maxInt(0, I -Int SHIFT), V >>Int (SHIFT *Int 8), NUM, B >>SparseBytes SHIFT)

If B >>SparseBytes X and dropFront(X, B) are the same, what's the reason for this discrepancy? If they are not, I still would like to see an example for >>SparseBytes applied on concrete values.

[Stevengre]

  rule dropFront(DROP, #WB(FLAG, I, V, NUM, B:SparseBytes)) => #WB(FLAG, maxInt(0, I -Int SHIFT), V >>Int (SHIFT *Int 8), NUM -Int DROP, dropFront(DROP, B)) 
    [simplification(45)]

Found that the dropFront and >>SparseBytes should be the same, so why I provide >>SparseBytes is that the previous simp rule for dropFront is wrong.

Quick idea to fix this issue:

1. provide a correct simp rule for dropFront
2. delete the >>SparseBytes
3. check if the #WB have the correct implementation when index <=0 && num <=0.
4. Verifying the implementation's correctness using a decision tree with a truth table.