Taint Tracking Inconsistency with COND Contract

[OleksiiOleksenko]

Environment

• dev branch of Revizor
• OS: Ubuntu 24.04.2 LTS
• Kernel: 6.8.0-53

Issue Description

When running Revizor with a COND contract, the taint tracking system produces inconsistent results between fast path contract traces and full traces. This suggests a potential logic error in the taint propagation algorithm when operating under COND contract constraints.

Steps to Reproduce

Execute the following command:

./revizor.py reproduce -s base.json -c demo/detecting-v1-var.yaml -t program.asm -i ./input_0000.bin ./input_0001.bin ./input_0002.bin

The output contains the warning message: WARNING: [fuzzer] Fast path contract traces do not match the full traces

Possible Root Cause

Under investigation

program.asm.txt
input_0000.bin.txt
input_0001.bin.txt
input_0002.bin.txt

[sharp30]

I was able to reproduce the issue in my environment as well.

It seems that the model starts using "Cond" speculation only during the taint_mistake stage, not before. I reviewed the logs while in dbg_model and noticed that the model only begins checking the transient path at that point.

So, it doesn’t appear to be something specific to tainting.

I’ve attached the ctraces for stage 3 and stage 4.
Even with the same inputs, the CTrace changes between the stages.

[OleksiiOleksenko]

Closed by mistake; revert