fix(mmu, mmio): debuging

Makefile

@@ -42,8 +42,9 @@ LOG_INFO := logInfo
 
 MMU := mmu
 
-MMIO := mmio \
-mmio/consistency.lisp
+MMIO := mmio/columns.lisp #TODO enable the MMIO constraint and lookup
+# MMIO := mmio \
+# mmio/consistency.lisp
 
 MXP := mxp
 

constants/constants.lisp

@@ -158,7 +158,6 @@
   EVM_INST_REVERT                              0xFD
   EVM_INST_INVALID                             0xFE
   EVM_INST_SELFDESTRUCT                        0xFF
-  INVALID_CODE_PREFIX_VALUE                    0xEF
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;               ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; GAS CONSTANTS ;;
@@ -200,18 +199,24 @@
   GAS_CONST_G_KECCAK_256_WORD                  6
   GAS_CONST_G_COPY                             3
   GAS_CONST_G_BLOCKHASH                        20
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;           ;;
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;  EVM MISC ;;
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;           ;;
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+  EIP_3541_MARKER                              0xEF
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;               ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; SIZE / LENGTH ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;               ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-  MMEDIUMMO                                    7
   MMEDIUM                                      8
-  LLARGEMO                                     15
+  MMEDIUMMO                                    (- MMEDIUM 1)
   LLARGE                                       16
+  LLARGEMO                                     (- LLARGE 1)
   LLARGEPO                                     (+ LLARGE 1)
-  WORD_SIZE_MO                                 31
   WORD_SIZE                                    32
+  WORD_SIZE_MO                                 (- WORD_SIZE 1)
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;         ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EXO SUM ;;

mmio/columns.lisp

@@ -1,12 +1,12 @@
 (module mmio)
 
 (defcolumns 
-  (CN_A :i32)
-  (CN_B :i32)
-  (CN_C :i32)
-  (INDEX_A :i32)
-  (INDEX_B :i32)
-  (INDEX_C :i32)
+  (CN_A :i64)
+  (CN_B :i64)
+  (CN_C :i64)
+  (INDEX_A :i64)
+  (INDEX_B :i64)
+  (INDEX_C :i64)
   (VAL_A :i128)
   (VAL_B :i128)
   (VAL_C :i128)
@@ -21,15 +21,15 @@
   (ACC_C :i128)
   (MMIO_STAMP :i32)
   (MMIO_INSTRUCTION :i16)
-  (CONTEXT_SOURCE :i32)
-  (CONTEXT_TARGET :i32)
-  (SOURCE_LIMB_OFFSET :i32)
-  (TARGET_LIMB_OFFSET :i32)
+  (CONTEXT_SOURCE :i64)
+  (CONTEXT_TARGET :i64)
+  (SOURCE_LIMB_OFFSET :i64)
+  (TARGET_LIMB_OFFSET :i64)
   (SOURCE_BYTE_OFFSET :i8)
   (TARGET_BYTE_OFFSET :i8)
-  (SIZE :i32)
+  (SIZE :i64)
   (LIMB :i128)
-  (TOTAL_SIZE :i128)
+  (TOTAL_SIZE :i64)
   (EXO_SUM :i32)
   (EXO_ID :i32)
   (KEC_ID :i32)
@@ -57,7 +57,7 @@
   (EXO_IS_ECDATA :binary@prove)
   (EXO_IS_RIPSHA :binary@prove)
   (EXO_IS_BLAKEMODEXP :binary@prove)
-  (INDEX_X :i32)
+  (INDEX_X :i64)
   (BYTE_LIMB :byte@prove)
   (ACC_LIMB :i128)
   (BIT :binary :array [1:5])

mmio/constraints.lisp

@@ -48,9 +48,7 @@
   (force-bool (+ (fast-op-flag-sum) (slow-op-flag-sum))))
 
 (defconstraint no-stamp-no-op ()
-  (if-zero MMIO_STAMP
-           (vanishes! (op-flag-sum))
-           (eq! (op-flag-sum) 1)))
+  (eq! (op-flag-sum) (~ STAMP)))
 
 (defun (weighted-exo-sum)
   (+ (* EXO_SUM_WEIGHT_ROM EXO_IS_ROM)
@@ -62,21 +60,16 @@
      (* EXO_SUM_WEIGHT_BLAKEMODEXP EXO_IS_BLAKEMODEXP)))
 
 (defconstraint exo-sum-decoding ()
-  (eq! EXO_SUM (weighted-exo-sum)))
+  (eq! (weighted-exo-sum) (* (instruction-may-provide-exo-sum) EXO_SUM)))
 
 (defun (instruction-may-provide-exo-sum)
-  (force-bool (+ IS_LIMB_VANISHES
-                 IS_LIMB_TO_RAM_TRANSPLANT
+  (force-bool (+ IS_LIMB_TO_RAM_TRANSPLANT
                  IS_LIMB_TO_RAM_ONE_TARGET
                  IS_LIMB_TO_RAM_TWO_TARGET
                  IS_RAM_TO_LIMB_TRANSPLANT
                  IS_RAM_TO_LIMB_ONE_SOURCE
                  IS_RAM_TO_LIMB_TWO_SOURCE)))
 
-(defconstraint no-exo-when-not-needed ()
-  (if-zero (instruction-may-provide-exo-sum)
-           (vanishes! EXO_SUM)))
-
 ;;
 ;; Heartbeat
 ;;

mmio/lookups/mmio_into_rlptxn.lisp

@@ -3,20 +3,18 @@
   ;reference columns
   (
     rlpTxn.ABS_TX_NUM
+    rlpTxn.LC
     rlpTxn.PHASE_ID
     rlpTxn.INDEX_DATA
     rlpTxn.LIMB
-    rlpTxn.nBYTES
-    rlpTxn.DATA_LO
   )
   ;source columns
   (
     (* mmio.EXO_IS_TXCD mmio.EXO_ID)
+    mmio.EXO_IS_TXCD
     (* mmio.EXO_IS_TXCD mmio.PHASE)
     (* mmio.EXO_IS_TXCD mmio.INDEX_X)
     (* mmio.EXO_IS_TXCD mmio.LIMB)
-    (* mmio.EXO_IS_TXCD mmio.SIZE)
-    (* mmio.EXO_IS_TXCD mmio.TOTAL_SIZE)
   ))
 
 

mmu/columns.lisp

@@ -9,11 +9,11 @@
   (PRPRC :binary@prove)
   (MICRO :binary@prove)
   ;; OUTPUT OF THE PREPROCESSING
-  (TOT :i16)
-  (TOTLZ :i16)
-  (TOTNT :i16)
-  (TOTRZ :i16)
-  (OUT :i32 :array [5])
+  (TOT :i32)
+  (TOTLZ :i32)
+  (TOTNT :i32)
+  (TOTRZ :i32)
+  (OUT :i64 :array [5])
   (BIN :binary :array [5])
   ;; MMU INSTRUCTION FLAG
   (IS_MLOAD :binary@prove)
@@ -45,9 +45,9 @@
   ;; selector
   MACRO
   ((INST :i16)
-   (SRC_ID :i32)
-   (TGT_ID :i32)
-   (AUX_ID :i32)
+   (SRC_ID :i64)
+   (TGT_ID :i64)
+   (AUX_ID :i64)
    (SRC_OFFSET_HI :i128)
    (SRC_OFFSET_LO :i128)
    (TGT_OFFSET_LO :i64)
@@ -84,18 +84,18 @@
   MICRO
   ((INST :i16)
    (SIZE :byte)
-   (SLO :i32)
+   (SLO :i64)
    (SBO :byte)
-   (TLO :i32)
+   (TLO :i64)
    (TBO :byte)
    (LIMB :i128)
-   (CN_S :i32)
-   (CN_T :i32)
+   (CN_S :i64)
+   (CN_T :i64)
    (SUCCESS_BIT :binary)
    (EXO_SUM :i32)
    (PHASE :i32)
    (EXO_ID :i32)
    (KEC_ID :i32)
-   (TOTAL_SIZE :i32)))
+   (TOTAL_SIZE :i64)))
 
 

mmu/constraints.lisp

@@ -395,7 +395,7 @@
          (vanishes! TOTRZ)
          ;; setting prprc row n°1
          (callToEuc 1 macro/SRC_OFFSET_LO LLARGE)
-         (callToEq 1 0 (shift micro/LIMB NB_PP_ROWS_INVALID_CODE_PREFIX_PO) INVALID_CODE_PREFIX_VALUE)
+         (callToEq 1 0 (shift micro/LIMB NB_PP_ROWS_INVALID_CODE_PREFIX_PO) EIP_3541_MARKER)
          ;; setting the success bit
          (eq! macro/SUCCESS_BIT
               (- 1 (next prprc/WCP_RES)))
@@ -412,7 +412,7 @@
 ;; RIGHT PADDED WORD EXTRACTION
 ;;
 (defun (right-pad-word-extract-second-limb-padded)
-  (- 1 (next prprc/WCP_RES)))
+  (force-bool (- 1 (next prprc/WCP_RES))))
 
 (defun (right-pad-word-extract-extract-size)
   (+ (* (right-pad-word-extract-second-limb-padded) (- macro/REF_SIZE macro/SRC_OFFSET_LO))
@@ -495,25 +495,25 @@
          (vanishes! (shift micro/TBO NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PO))
          (eq! (shift micro/LIMB NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PO) macro/LIMB_1)
          ;; setting second mmio inst
-         (if-zero (right-pad-word-extract-second-limb-void)
-                  (if-zero (right-pad-word-extract-second-limb-single-source)
-                           (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
-                                MMIO_INST_RAM_TO_LIMB_TWO_SOURCE)
-                           (if-zero (right-pad-word-extract-second-limb-padded)
-                                    (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
-                                         MMIO_INST_RAM_TO_LIMB_TRANSPLANT)
-                                    (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
-                                         MMIO_INST_RAM_TO_LIMB_ONE_SOURCE)))
-                  (begin (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
-                              MMIO_INST_LIMB_VANISHES)
-                         (vanishes! macro/LIMB_2)))
+         (if-eq-else (right-pad-word-extract-second-limb-void) 1
+                     (begin (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
+                                 MMIO_INST_LIMB_VANISHES)
+                            (vanishes! macro/LIMB_2))
+                     (if-eq-else (right-pad-word-extract-second-limb-single-source) 1
+                                 (if-zero (right-pad-word-extract-second-limb-padded)
+                                          (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
+                                               MMIO_INST_RAM_TO_LIMB_TRANSPLANT)
+                                          (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
+                                               MMIO_INST_RAM_TO_LIMB_ONE_SOURCE))
+                                 (eq! (shift micro/INST NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
+                                      MMIO_INST_RAM_TO_LIMB_TWO_SOURCE)))
          (eq! (shift micro/SIZE NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
               (right-pad-word-extract-second-limb-byte-size))
          (eq! (shift micro/SLO NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT)
               (+ (right-pad-word-extract-slo) 1))
          (eq! (shift micro/SBO NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT) (right-pad-word-extract-sbo))
          (vanishes! (shift micro/TBO NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT))
-         (eq! (shift micro/LIMB NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT) macro/LIMB_1)))
+         (eq! (shift micro/LIMB NB_PP_ROWS_RIGHT_PADDED_WORD_EXTRACTION_PT) macro/LIMB_2)))
 
 ;;
 ;; RAM TO EXO WITH PADDING
@@ -562,7 +562,7 @@
          (callToLt 2 0 macro/SIZE macro/REF_SIZE)
          (callToEuc 2 (ram-exo-wpad-padding-size) LLARGE)
          ;; setting prprc row n°3
-         (callToIszero 3 0 prprc/EUC_REM)
+         (callToIszero 3 0 (shift prprc/EUC_REM 3))
          (callToEuc 3 (ram-exo-wpad-extraction-size) LLARGE)
          ;; setting prprc row n°4
          (callToLt 4
@@ -611,7 +611,7 @@
               (shift (ram-exo-wpad-initial-sbo) (- 0 NB_PP_ROWS_RAM_TO_EXO_WITH_PADDING_PO)))))
 
 (defconstraint ram-to-exo-with-padding-last-or-only-common (:guard (* IS_RAM_TO_EXO_WITH_PADDING
-      (force-bool (+ NT_LAST NT_MDDL))))
+      (force-bool (+ NT_LAST NT_ONLY))))
   (begin (eq! micro/SIZE [OUT 1])
          (if-zero [BIN 2]
                   (eq! micro/INST MMIO_INST_RAM_TO_LIMB_TWO_SOURCE)