Backend fails to simplify complex shift expressions with bitwise AND operations

Problem Description

We've encountered an issue where the K backend fails to simplify certain complex expressions involving bit shifts and logical operations, even when simpler variants of the same expressions work correctly.

Failing Case

The following simplification rule fails:

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

Working Cases

However, these similar expressions work correctly:

// This works when X is a simple variable
0 <=Int X >>Int 8 => true
  requires 0 <=Int X

// This works for the complex term without the shift
0 <=Int Bytes2Int(substrBytes(W3, 8, 12), LE, Unsigned) +Int Y +Int Z &Int 4294967295 => true

Root Cause Analysis

The backend cannot infer the complex case from the combination of the two working cases. This suggests a limitation in the theorem prover's ability to compose logical reasoning across multiple steps.

Attempted Solutions

1. SMT Lemmas: Adding smt-lemma annotations to the <=Int rules didn't resolve the issue.

Questions

1. Is there a recommended workaround for cases where the backend cannot perform multi-step logical inference?
2. What's the best way to utilize theory reasoning for complex expressions like this?

Environment

• Related to PR #137: Fix unsimplified bytes2int o int2bytes patterns
• File: src/tests/integration/test-data/specs/xx.k

Expected Behavior

The complex shift expression should simplify to true just like its simpler components do.

Additional Context

This issue is blocking the completion of PR #137, which aims to fix unsimplified bytes2int o int2bytes patterns in the RISC-V semantics. But we have another way to solve this issue.

Start with the failing case in src/tests/integration/test-data/specs/xx.k and compare it with the two working expressions shown in the issue. Investigate how the backend combines the shift, bitwise AND, and arithmetic reasoning, including the attempted smt-lemma annotations. Done means the complex expression simplifies to true and the integration case passes.