diff --git a/Makefile b/Makefile index c75b0a4e..3b233dfd 100644 --- a/Makefile +++ b/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 diff --git a/constants/constants.lisp b/constants/constants.lisp index a4b82e38..81b25812 100644 --- a/constants/constants.lisp +++ b/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 ;; diff --git a/mmio/columns.lisp b/mmio/columns.lisp index 67d13a6a..989d2c18 100644 --- a/mmio/columns.lisp +++ b/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]) diff --git a/mmio/constraints.lisp b/mmio/constraints.lisp index e88aa67d..e5e88c1c 100644 --- a/mmio/constraints.lisp +++ b/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 ;; diff --git a/mmio/lookups/mmio_into_rlptxn.lisp b/mmio/lookups/mmio_into_rlptxn.lisp index 4ecfc089..547cb27c 100644 --- a/mmio/lookups/mmio_into_rlptxn.lisp +++ b/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) )) diff --git a/mmu/columns.lisp b/mmu/columns.lisp index 23fc3743..6347bc5d 100644 --- a/mmu/columns.lisp +++ b/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))) diff --git a/mmu/constraints.lisp b/mmu/constraints.lisp index 3daa13f8..0203ee29 100644 --- a/mmu/constraints.lisp +++ b/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)