MXP redesign
#103
MXP redesign
#103
Conversation
Signed-off-by: F Bojarski <[email protected]>
| \item \If $\locPerspectiveSum _{i} = 0$ \Then | ||
| \[ | ||
| \left\{ \begin{array}{lcl} | ||
| \maxCt_{i} & = & 0 \\ |
There was a problem hiding this comment.
trash constraint
| \[ | ||
| \left\{ \begin{array}{lcl} | ||
| \maxCt_{i} & = & 0 \\ | ||
| \ct _{i} & = & 0 \\ |
There was a problem hiding this comment.
trash constraint
There was a problem hiding this comment.
The way the constraints work atm is that we unconditionally define the counter stuff
Given that I don't want to cut out too much. For instance I don't want our traces to be allowed to start with CT[0] = CT_MAX[0] = 13.
In general I don't particularly like the idea of cutting constraints with the justification that "you can't produce a valid trace if you broke that constraint". These implicit restrictions rely on other constraints that may change at a future point. I prefer things to be explicit, even if it means some clutter constraints. I also believe that these extra "making expectations explicit"-type constraints will help with formal verification tools.
| ▶ some_data ◀ | ||
|
|
||
| In the case of MLOAD, MSTORE, MSTORE8 it is supposed to draw attention to the fact that the size parameters are set in stone and must be written as such in the HUB module. | ||
| In the case of MCOPY we highlight the fact that the HUB must duplicate the values in the SIZE_1_HI/LO columns in the SIZE_2_HI/LO columns. |
There was a problem hiding this comment.
for both case I would insist that the constraint is in the MXP module, not in the HUB. So the HUB has to write the right value in order to make the lookup working, but not for inner constraint. The first time I read this, I thought the constraint were in the HUB (which is, I agree, non-sense)
There was a problem hiding this comment.
The constraints will be on both sides: in setting the MXP instruction in the HUB and within the MXP module enforcing the correct size (32, 32 or 1) based on the instruction.
There was a problem hiding this comment.
IMHO we could trash the constraint duplication in the HUB (for MCOPY for exemple, enforcing the instruction in the HUB should be enough, and should be fully constrained in MXP)
There was a problem hiding this comment.
I will echo my previous point. The MXP module should be able to work in isolation. Relying on assumptions about how the HUB produces its MXP instructions leaves us open to changes on one side not being reflected on the other. In particular if we start out under-constrained on one side to save 2 constraints.
It's always going to be a delicate dance to find the right balance. I again prefer to pay the price of a few extra constraints to make sure that even in isolation the MXP module functions as expected.
| \end{center} | ||
| We impose exclusivity on the (binary) module flags | ||
| \begin{enumerate} | ||
| \item $\mxpComputationWcpFlag _{i} \cdot \mxpComputationEucFlag _{i} = 0$ |
There was a problem hiding this comment.
trash constraint. It will make the lookup failing, but we don't need this constraint.
mxp_v3/computations/msize.tex
Outdated
| \begin{description} | ||
| \item[\underline{\underline{First computation row:}}] we impose | ||
| \begin{enumerate} | ||
| \item $\mxpComputationWcpFlag _{i + \rowNum} = 0$ |
There was a problem hiding this comment.
Why impose this ? trash constraint
There was a problem hiding this comment.
The fact that we don't need the lookup doesn't mean we need to not have the lookup.
There was a problem hiding this comment.
We don't need these, I agree.
mxp_v3/computations/non_msize.tex
Outdated
| and given the definitions of section~(\ref{mxp: columns: scenario: shorthands}) and standing assumptions of this section, | ||
| we are also (implicitly) setting | ||
| \[ | ||
| \locMxpScenarioNotMsizeNorTrivial _{i} = 1 - |
There was a problem hiding this comment.
I think this is wrong. In the case MSIZE we don't impose anything on the value of ARG1HI/LO.
I would rather NOtMSizeNonTrivial = 1 - MSize - Trivial
There was a problem hiding this comment.
and standing assumptions of this section
This refers to the assumptions box at the start of the section, which is among others:
SCNRI/not_msize = 1So we cannot be in the MSIZE case.
There was a problem hiding this comment.
BTW I agree that this is a convoluted way of stating things.
There was a problem hiding this comment.
I moved that comment to be a note in the constraint fixing scenario/TRIVIAL.
| The present section describes the computation for the $\locMxpScenarioNotMsizeNorTrivial$ case. | ||
| We need the following constant: | ||
| \[ | ||
| \mxpxThreshold \define 256^\mxpxThresholdExponent - 1 |
There was a problem hiding this comment.
I may be wrong, but shouldn't it be without -1 ? We call LT after, not LEQ.
IU would be in favor of keeping the -1 here, but calling LEQ, not LT in WCP (1 less row)
There was a problem hiding this comment.
second size arg and offset has to be LEQ too.
And the LeqCall is not defined in 4.5.2, only LtCall
There was a problem hiding this comment.
Indeed. Fixing this right now.
| @@ -0,0 +1,74 @@ | |||
| We define several simple constraint systems to simplify the writing of constraints. | |||
There was a problem hiding this comment.
Wouldn't it make sense to be able to have on the same row a WCP and a EUC call ? It would save up to three rows (nb of EUC calls), and won't make the MXP wider as the computation perspective is not the widest one.
There was a problem hiding this comment.
We could indeed do this.
There was a problem hiding this comment.
Issue for future reference #141
Note. We have chosen a design that has a unique computation path for
GAS_MXP. The trade off is essentially (everything is estimations)20 + 60 constraints estimated - 10% of instructions will take up 3 + 1 rows - 90% of instructions will take up 3 + 10 rows average 9.4 rows per opcodeBut I could change things up and instead have two computational paths (depending on whether the
DECODER/SINGLE_MAX_OFFSETorDECODER/DOUBLE_MAX_OFFSETis on):Basically trading constraints for cells. We could pivot would basically take me the rest of the day so it's not like starting from scratch.
Note. The above is a total guesstimate. It neglects instructions using WORD vs BYTE pricing (which would also change the number of rows by +1 in the WORDS case etc ...)