Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unit test for LoadWordLeft #2299

Draft
wants to merge 13 commits into
base: master
Choose a base branch
from
Draft

Unit test for LoadWordLeft #2299

wants to merge 13 commits into from

Conversation

querolita
Copy link
Member

@querolita querolita commented Jun 6, 2024

This PR provides a unit test for the `LoadWordLeft` instruction. It matches closely the Cannon definition of the instruction given by
		case 0x22: // lwl
			val := mem << ((rs & 3) * 8)
			mask := uint32(0xFFFFFFFF) << ((rs & 3) * 8)
			return (rt & ^mask) | val

I used this test to realize that our current implementation of the interpreter for that function was not working properly. In particular, bytes were being mapped to different positions. I changed the interpreter code to avoid the confusing (and error prone) use of overwrite_n in favor of a more direct set of variables called mod_n. I included comments to help understand what the above function does and what it expects in each byte position of the destination register.

Old description

This unit test matches what the interpreter of LoadWordLeft is doing. Nonetheless, the constraints still do not pass when trying to make a proof for them. In particular:

"Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)"

Still figuring out why. The obvious answer would be dummy rows initialized to zeros so the -1 will not hold. But we already solved that issue when creating the trace, by padding with a dummy row that is known to be a "real" row.~

@querolita querolita marked this pull request as draft June 11, 2024 15:01
@querolita querolita marked this pull request as ready for review June 11, 2024 16:53
@querolita querolita changed the base branch from master to zkvm/mips/fixme-register-access-underflow June 11, 2024 16:54
@querolita
Copy link
Member Author

After applying #2311 to this PR, I will run the nodes again to see if the constraint holds now.

Base automatically changed from zkvm/mips/fixme-register-access-underflow to master June 13, 2024 14:27
@querolita querolita marked this pull request as draft June 13, 2024 18:12
@querolita
Copy link
Member Author

Demo halts, making the PR a draft until solved

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant