EIP-7823: Set upper bounds for MODEXP --- MMU side (#814)

Author: OlivierBBB

mmu/osaka/constants.lisp

@@ -53,8 +53,8 @@
   ;;NB_MICRO_ROWS_TOT_RAM_TO_RAM_SANS_PADDING              variable
   ;;NB_MICRO_ROWS_TOT_ANY_TO_RAM_WITH_PADDING_PURE_PADDING variable
   ;;NB_MICRO_ROWS_TOT_ANY_TO_RAM_WITH_PADDING_SOME_DATA    variable
-  NB_MICRO_ROWS_TOT_MODEXP_ZERO                      32
-  NB_MICRO_ROWS_TOT_MODEXP_DATA                      32
+  NB_MICRO_ROWS_TOT_MODEXP_ZERO                      64
+  NB_MICRO_ROWS_TOT_MODEXP_DATA                      64
   NB_MICRO_ROWS_TOT_BLAKE                            2)
 
 

mmu/osaka/instructions/modexp_data.lisp

@@ -30,19 +30,20 @@
 (defun    (modexp-data---exo-sum)                        macro/EXO_SUM)
 (defun    (modexp-data---phase)                          macro/PHASE)
 (defun    (modexp-data---param-byte-size)                (modexp-data---size))
-(defun    (modexp-data---param-offset)                   (+ (modexp-data---cdo) (modexp-data---src-offset)))
-(defun    (modexp-data---leftover-data-size)             (- (modexp-data---cds) (modexp-data---src-offset)))
-(defun    (modexp-data---num-left-padding-bytes)         (- 512 (modexp-data---param-byte-size)))
+(defun    (modexp-data---param-offset)                   (+   (modexp-data---cdo)                     (modexp-data---src-offset)))
+(defun    (modexp-data---leftover-data-size)             (-   (modexp-data---cds)                     (modexp-data---src-offset)))
+(defun    (modexp-data---num-left-padding-bytes)         (-   EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND   (modexp-data---param-byte-size)))
 (defun    (modexp-data---data-runs-out)                  (shift prprc/WCP_RES 2))
 (defun    (modexp-data---num-right-padding-bytes)        (* (- (modexp-data---param-byte-size) (modexp-data---leftover-data-size)) (modexp-data---data-runs-out)))
 (defun    (modexp-data---right-padding-remainder)        (shift prprc/EUC_REM 2))
 (defun    (modexp-data---totnt-is-one)                   (shift prprc/WCP_RES 3))
 (defun    (modexp-data---middle-sbo)                     (shift prprc/EUC_REM 6)) ;; ""
 
 
-(defconstraint modexp-data---setting-TOT (:guard (* MACRO IS_MODEXP_DATA))
-                 ;; Setting total number of mmio inst
-                 (eq! TOT NB_MICRO_ROWS_TOT_MODEXP_DATA))
+(defconstraint modexp-data---number-of-preprocessing-rows-ie-setting-TOT (:guard (* MACRO IS_MODEXP_DATA))
+               ;; Setting total number of mmio inst
+               (eq!   TOT
+                      NB_MICRO_ROWS_TOT_MODEXP_DATA))
 
 (defconstraint modexp-data---1st-preprocessing-row (:guard (* MACRO IS_MODEXP_DATA))
                (begin
@@ -64,7 +65,8 @@
                               (modexp-data---num-right-padding-bytes)
                               LLARGE)
                  (eq! TOTRZ (shift prprc/EUC_QUOT 2))
-                 (debug (eq! TOTNT (- 32 (+ TOTLZ TOTRZ))))))
+                 (debug (eq! TOTNT (-  NB_MICRO_ROWS_TOT_MODEXP_DATA
+                                       (+ TOTLZ TOTRZ))))))
 
 (defconstraint modexp-data---3rd-preprocessing-row (:guard (* MACRO IS_MODEXP_DATA))
                (begin

mmu/osaka/instructions/modexp_zero.lisp

@@ -16,7 +16,7 @@
 (defconstraint    modexp-zero---setting-the-TOTs (:guard (* MACRO IS_MODEXP_ZERO))
                   (begin
                     (vanishes! TOTLZ)
-                    (eq!       TOTNT NB_MICRO_ROWS_TOT_MODEXP_ZERO)
+                    (eq!       TOTNT   NB_MICRO_ROWS_TOT_MODEXP_ZERO)
                     (vanishes! TOTRZ)))
 
 (defconstraint    modexp-zero---setting-micro-instruction-constant-values (:guard (* MACRO IS_MODEXP_ZERO))