Coq TinyRAM emulator setting flag on mull instruction incorrectly

Orbis-Tertius / Orbis

A general-purpose layer 2 zk-rollup scaling solution for Cardano

Apache License 2.0

21 stars 1 forks source link

Closed marcinbugaj closed 2 years ago

marcinbugaj commented 2 years ago

@AHartNtkn , FYI

mull r0, r3, #9121
cmov r0, #38868
answer r0

evaluates to 38868 on Coq TinyRAM emulator. Expected value is 0.

AHartNtkn commented 2 years ago

This has been fixed in the binary-integers branch. https://github.com/Orbis-Tertius/coq-tinyram/pull/13 Also, this should have been an issue in the actual Coq TinyRAM repo.

marcinbugaj commented 2 years ago

I can see that binary-integers branch hasn't been merged to main yet. When can I expect it to be merged then?