search

franck44 / evm-dis

An EVM bytecode disassembler/assembler
Apache License 2.0
29 stars 6 forks source link

SLT/SGT Proof Object Mismatch with evm-dafny's Definition #47

Open gaxiiiiiiiiiiii opened 6 months ago

gaxiiiiiiiiiiii commented 6 months ago

Problem Description

When generating Dafny Proof Objects for opcodes SLT/SGT, I encountered an inconsistency with the function defined in evm-dafny's bytecode.dfy.

Suggested Area for Correction

This is speculative as I do not have a complete understanding of the entire project, but I suspect there might be a typo in src/dafny/prettyprinters/PrettyInstruction.dfy. Below is the relevant section of the code.

Current Codd:

case SLT    => "var s" + DecToString(tgt) + " := Slt(s" + DecToString(src) + ");"
case SGT    => "var s" + DecToString(tgt) + " := Sgt(s" + DecToString(src) + ");"

Proposed Improvement:

case SLT    => "var s" + DecToString(tgt) + " := SLt(s" + DecToString(src) + ");"
case SGT    => "var s" + DecToString(tgt) + " := SGt(s" + DecToString(src) + ");"

Changed Slt/Sgt to SLt/SGt

This inconsistency could affect Proof Object generation. Your review and any necessary adjustments would be appreciated.