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.

Sign up for GitHub

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

Jump to bottom

reconnect MMIO constraints #1388

Open
wants to merge 33 commits into
base: arith-dev
Choose a base branch
from
Open

reconnect MMIO constraints #1388

wants to merge 33 commits into from

Conversation

letypequividelespoubelles
Copy link
Collaborator

@letypequividelespoubelles letypequividelespoubelles commented Oct 8, 2024 •
edited
Loading

Partial debugging of reconnecting the MMIO constraints (inner + all lookup touching the MMIO)

@letypequividelespoubelles
reconnect MMIO constraints
0eb9cac 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles letypequividelespoubelles linked an issue Oct 8, 2024 that may be closed by this pull request
Re-connect RAM (MMU/MMIO) #917
Open
@letypequividelespoubelles
cleaning + fix too much MMIO inst for modexp data if only one MMIO no…
d2911d0 
…n trivil inst

Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
fix no limb for limb vanishes instruction
6efb519 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
fix lookup mmio -> BLKMDXP
03f2e2b 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
fe4276b
@letypequividelespoubelles
clean: kill duplicate constant
1297355 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
fix source CN to extract arg for modexp
733c301 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
fix: generating the limb needs to know TBO
039aeb9 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
558fc9f
@letypequividelespoubelles
fix source Id for Identity PRC MMU call
c32a012 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
fix (again) reading exo Bytes
8e4568b 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
f2a4d0f
@letypequividelespoubelles
some more fixes
3037ade 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles letypequividelespoubelles marked this pull request as ready for review October 10, 2024 13:09
letypequividelespoubelles
letypequividelespoubelles commented Oct 10, 2024
View reviewed changes
arithmetization/src/main/java/net/consensys/linea/zktracer/module/mmu/MmuOperation.java
final int sizeToExtract = mmioInst.size() == 0 ? LLARGE : mmioInst.size();
final Bytes16 exoLimb = readBytes(mmuData.exoBytes(), offset, sizeToExtract);
mmioInst.limb(exoLimb);
for (MmuToMmioInstruction mmioInst : mmuData.mmuToMmioInstructions()) {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is a fix

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⭐

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if the exoBytes is the source, We were extracting the (exo)limb from the SBO which is totally wrong. The exo limb is 16 bytes starting at 16 * SLO? And from this exo limb, we extract from SBO to extract the data. But We weren't reading the right exo(limb) as we were taking 16 bytes from 16*SLO + SBO for the exo bytes

letypequividelespoubelles
letypequividelespoubelles commented Oct 10, 2024
View reviewed changes
...etization/src/main/java/net/consensys/linea/zktracer/module/mmu/instructions/ModexpData.java
@@ -263,7 +263,9 @@ public MmuData setMicroInstructions(MmuData mmuData) {
middleMicroInstruction(mmuData, sourceLimbOffset, targetLimbOffset);
}

lastMicroInstruction(mmuData);
if (initialTotalNonTrivial > 1) {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is a fix

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⭐

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if the nb of non trivial mmio inst is 1, we just have a only mmio inst. We have a last mmio inst only if we have 2 or more non trivial inst. Before the fix, when we had only one non trivial mmio inst, we were writting one only mmio inst and then one last mmio inst.

letypequividelespoubelles
letypequividelespoubelles commented Oct 10, 2024
View reviewed changes
arithmetization/src/main/java/net/consensys/linea/zktracer/types/Bytecodes.java
import org.apache.tuweni.bytes.Bytes;

public class Bytecodes {

public static Bytes16 readBytes(final Bytes data, final long offset, final int sizeToRead) {
if (offset >= data.size()) {
public static Bytes16 readBytes(
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is a fix

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⭐

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we weren't doing the left padding before (this comes from the veridise audit, where we didn't use the SBO for one of the mmio inst). I made a mistake last time when I implemented it (and didn't see it because the MMIO constraint weren't plugged)

letypequividelespoubelles
letypequividelespoubelles commented Oct 10, 2024
View reviewed changes
linea-constraints Outdated
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

just update to the latest master. MMIO constraints are still not plugged

OlivierBBB
OlivierBBB reviewed Oct 11, 2024
View reviewed changes
Copy link
Collaborator

@OlivierBBB OlivierBBB left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still have to understand the changes labeled with ⭐, could you please give a short description of the intended effect ?

...tization/src/main/java/net/consensys/linea/zktracer/module/hub/fragment/imc/mmu/MmuCall.java Show resolved Hide resolved
.../src/main/java/net/consensys/linea/zktracer/module/hub/fragment/imc/mmu/opcode/CodeCopy.java Show resolved Hide resolved
arithmetization/src/main/java/net/consensys/linea/zktracer/types/Bytecodes.java
import org.apache.tuweni.bytes.Bytes;

public class Bytecodes {

public static Bytes16 readBytes(final Bytes data, final long offset, final int sizeToRead) {
if (offset >= data.size()) {
public static Bytes16 readBytes(
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⭐

...etization/src/main/java/net/consensys/linea/zktracer/module/mmu/instructions/ModexpData.java
@@ -263,7 +263,9 @@ public MmuData setMicroInstructions(MmuData mmuData) {
middleMicroInstruction(mmuData, sourceLimbOffset, targetLimbOffset);
}

lastMicroInstruction(mmuData);
if (initialTotalNonTrivial > 1) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⭐

arithmetization/src/main/java/net/consensys/linea/zktracer/module/mmu/MmuOperation.java
final int sizeToExtract = mmioInst.size() == 0 ? LLARGE : mmioInst.size();
final Bytes16 exoLimb = readBytes(mmuData.exoBytes(), offset, sizeToExtract);
mmioInst.limb(exoLimb);
for (MmuToMmioInstruction mmioInst : mmuData.mmuToMmioInstructions()) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⭐

@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
2309d9c
@letypequividelespoubelles
add mmio constraints
f13dec3 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
1c3dd6f
@letypequividelespoubelles
fix: exo Bytes not known when creaing the create MMU cal
934393b 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
17dad7d
@letypequividelespoubelles
constraints
eb15017 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
fix lookup mmio into rom for return from deployment
25d3aff 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
3c28763
@letypequividelespoubelles
fix(invalidCodePrefex): lookup mmio into mmu
448335d 
Signed-off-by: Francois Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
167463f
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
9c5c654
@letypequividelespoubelles
partly fix source ram Bytes for CallDataLoad
dc2cce7 
Signed-off-by: F Bojarski <[email protected]>
@letypequividelespoubelles
target limb ram can be touched twice at transition
70c7e38 
Signed-off-by: F Bojarski <[email protected]>
@letypequividelespoubelles
fix extCodeCopy mmuCall when empty account (and thus no cfi)
d406e26 
Signed-off-by: F Bojarski <[email protected]>
@letypequividelespoubelles
fix callDataLoad when loading from transaction call data
9c6dd34 
Signed-off-by: F Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
c1f2827
@letypequividelespoubelles
fix(ramToRamTwoSource): typo in tracer and constraints
088d032 
Signed-off-by: F Bojarski <[email protected]>
@letypequividelespoubelles
Merge branch 'arith-dev' into feat/issue-917/reconnect-ram
74459d4
@letypequividelespoubelles
initialize callerTargetMemorySpan
16b5de9 
Signed-off-by: F Bojarski <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@OlivierBBB OlivierBBB OlivierBBB left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@letypequividelespoubelles letypequividelespoubelles

Labels
debugging
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Re-connect RAM (MMU/MMIO)
2 participants
@letypequividelespoubelles @OlivierBBB