feat: support assembly implementation of euc #830
Conversation
This puts in place an assembly implementation of the euc module, thereby replacing the original.
DavePearce
force-pushed
the
829-feat-add-euc-assembly-implementation
branch
from
5852023 to
3f64870
Compare
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Bug: Incomplete Blockdata Causes Euclidean Division Failure
The lookup is missing euc.REMAINDER in the target columns. The new assembly implementation of euc requires REMAINDER as an input parameter (line 5 of euc/euc.zkasm), but blockdata only provides DIVIDEND, DIVISOR, and QUOTIENT. This causes the euclidean division verification to fail or use an undefined value for REMAINDER. The same issue affects blockdata/london and blockdata/paris lookups.
blockdata/cancun/lookups/blockdata_into_euc.lisp#L5-L10
Bug: Missing Remainder Breaks Core Division Verification.
The lookup is missing euc.REMAINDER in the target columns. The new assembly implementation of euc requires REMAINDER as an input parameter, but mxp only provides DIVIDEND, DIVISOR, QUOTIENT, and CEIL. Without REMAINDER, the euclidean division verification in the assembly function cannot correctly validate that DIVIDEND = DIVISOR * QUOTIENT + REMAINDER.
mxp/cancun/lookups/mxp_into_euc.lisp#L8-L14
linea-constraints/mxp/cancun/lookups/mxp_into_euc.lisp
Lines 8 to 14 in 3f64870
Bug: Missing Input Blocks Core Calculation
The lookup is missing euc.REMAINDER in the target columns. The new assembly implementation of euc requires REMAINDER as an input parameter, but txndata/london only provides DIVIDEND, DIVISOR, and QUOTIENT. This prevents proper euclidean division verification. The same issue affects txndata/shanghai.
txndata/london/lookups/txndata_into_euc.lisp#L3-L8
| if val_hi != 0 goto exit_f | ||
| if val_lo != DIVIDEND goto exit_f | ||
| ;; assert remainder < divisor | ||
| b, tmp = DIVISOR - REMAINDER - 1 |
There was a problem hiding this comment.
will it be better to call WCP when wcp will be asm ?
There was a problem hiding this comment.
No, it will not. Its more expensive in terms of columns to do that.
| if b == 1 goto exit_f | ||
| ;; Compute ceiling | ||
| if REMAINDER == 0 goto exit_0 | ||
| c, CEIL = QUOTIENT + 1 |
There was a problem hiding this comment.
do we really need a carry here ?
There was a problem hiding this comment.
Technically yes. You have a u64 with +1 gives u65 which does not go into a u64. However, we know the true value of QUOTIENT is smaller and, hence, the carry will never be 1. But, the tool cannot figure this out. Potentially I could add a cast feature, but not today ;)
This puts in place an assembly implementation of the euc module, thereby replacing the original.
Note
Replace the EUC module with a zkasm implementation and update all related lookups to remove DONE/IOMF wiring and align targets/fields, plus Makefile update.
euc/euc.zkasmimplementing 64-bit Euclidean division withCEIL; enforces non-zero divisor andREMAINDER < DIVISOR.euc/columns.lisp,euc/constraints.lisp, andeuc/lookups/euc_into_wcp.lisp.Makefileto setEUC := euc/euc.zkasm.blockdata/*/lookups/blockdata_into_euc.lisp: target onlyeuc.DIVIDEND,euc.DIVISOR,euc.QUOTIENT; dropeuc.IOMFand constant source.mmu/{london,osaka}/lookups/mmu_into_euc.lisp: mapDIVIDEND/DIVISOR/QUOTIENT/REMAINDER/CEIL; removeeuc.DONE.mxp/cancun/lookups/mxp_into_euc.lisp: targetDIVIDEND/DIVISOR/QUOTIENT/CEIL; removeeuc.DONE.txndata/*/lookups/txndata_into_euc.lisp: targetDIVIDEND/DIVISOR/QUOTIENT(andREMAINDERwhere present); removeeuc.DONEand constant source.Written by Cursor Bugbot for commit 3f64870. This will update automatically on new commits. Configure here.