fix: model SHA-256 precompile input widths in bits

[DicksonWu654]

Summary

• size the SHA-256 uninterpreted-function input sort in bits instead of bytes
• model empty SHA-256 input with a stable 256-bit symbolic constant
• add concrete, symbolic repeat-consistency, and invariant regression coverage

The previous byte-sized sort does not match the bit width of non-empty EVM input data. Empty input also requires a separate representation because Z3 does not support zero-width bitvectors.

Validation

• git diff --check
• two independent static reviews using the normal Codex load balancer

Tests and project code were not run because this contribution was prepared under a static-review-only constraint.