From 2e5118a2c03c958f20f68530332587ded1ff5f96 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 24 Oct 2025 02:31:40 +0200 Subject: [PATCH 01/10] wip --- .../call/precompiles/modexp/common.lisp | 107 ++++++++++++------ 1 file changed, 75 insertions(+), 32 deletions(-) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp index f8b58381a..e1fcd2be4 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp @@ -48,13 +48,17 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-analysis) (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs)) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-analysis) (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset CONTEXT_NUMBER ;; source ID @@ -76,7 +80,9 @@ (defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) (defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset (precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs @@ -84,6 +90,9 @@ 0 ;; bit indicating whether to compute max(xbs, ybs) or not )) +(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) +(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) ;; "" + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -128,6 +137,9 @@ 0 ;; bit indicating whether to compute max(xbs, ybs) or not )) +(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) +(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) ;; "" + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -170,12 +182,19 @@ (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs - 1 ;; bit indicating whether to compute max(xbs, ybs) or not + (precompile-processing---MODEXP---bbs-within-bounds) ;; bit indicating whether to compute max(xbs, ybs) or not )) -(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) -(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" + +(defun (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) (* (precompile-processing---MODEXP---bbs-within-bounds) + (precompile-processing---MODEXP---ebs-within-bounds) + (precompile-processing---MODEXP---mbs-within-bounds) + )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -184,28 +203,44 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) - (+ (* MISC_WEIGHT_EXP (precompile-processing---MODEXP---load-lead)) - (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---load-lead)) - MISC_WEIGHT_OOB) - )) +(defun (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift misc/OOB_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) -(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset - (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) - (precompile-processing---dup-cds) ;; call data size - (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) - )) -(defun (precompile-processing---MODEXP---load-lead) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (precompile-processing---MODEXP---load-lead) ) + (eq! (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (precompile-processing---MODEXP---load-lead) ) + (eq! (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) + (eq! (+ (shift misc/MXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) + (shift misc/STP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) + 0) + )) + + +(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) + (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset + (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) + (precompile-processing---dup-cds) ;; call data size + (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) + ))) +(defun (precompile-processing---MODEXP---load-lead) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) + +(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (set-MMU-instruction---mload precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset CONTEXT_NUMBER ;; source ID ;; tgt_id ;; target ID @@ -225,12 +260,14 @@ ;; phase ;; phase ))) -(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---load-lead) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---load-lead) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-EXP-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) - (if-not-zero (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) +(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-EXP-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (set-EXP-instruction-MODEXP-lead-log precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; row offset (precompile-processing---MODEXP---raw-lead-hi) ;; raw leading word where exponent starts, high part @@ -239,8 +276,12 @@ (precompile-processing---MODEXP---ebs-cutoff) ;; min{ebs, 32} ))) -(defun (precompile-processing---MODEXP---lead-log) (* (precompile-processing---MODEXP---load-lead) (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) (* 8 (precompile-processing---MODEXP---sub-ebs-32)))) +(defun (precompile-processing---MODEXP---lead-log) (* (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) + (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) + (* 16 (precompile-processing---MODEXP---sub-ebs-32)))) + +;; @OLIVIER: on reprend ici; pas sûr que modexp-full-log soit bien défini (filtres différents) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -249,9 +290,11 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---pricing) - MISC_WEIGHT_OOB + (* (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) MISC_WEIGHT_OOB) )) (defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) From 659dfd2e85968913528df8a543d00cbe4aab1ef1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 6 Nov 2025 00:21:34 +0100 Subject: [PATCH 02/10] feat: splitting of the MODEXP/common constraints file --- .../__01__call_data_size_analysis_row.lisp | 37 +++++++ .../common/__02__bbs_extraction_row.lisp | 69 ++++++++++++ .../common/__03__ebs_extraction_row.lisp | 63 +++++++++++ .../common/__04__mbs_extraction_row.lisp | 71 ++++++++++++ ...ding_word_extraction_and_analysis_row.lisp | 104 ++++++++++++++++++ .../modexp/common/__06__pricing_row.lisp | 43 ++++++++ .../modexp/common/generalities.lisp | 25 +++++ .../common/justifying_hub_predictions.lisp | 30 +++++ .../{common.lisp => common/zzz_old.lispX} | 1 + 9 files changed, 443 insertions(+) create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp create mode 100644 hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp rename hub/osaka/constraints/instruction-handling/call/precompiles/modexp/{common.lisp => common/zzz_old.lispX} (99%) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp new file mode 100644 index 000000000..10c9a82f0 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp @@ -0,0 +1,37 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CALL_DATA_SIZE analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis) + MISC_WEIGHT_OOB)) + +(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + (set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset + (precompile-processing---dup-cds))) ;; call data size + +(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) +(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) +(defun (precompile-processing---MODEXP---extract-mbs) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp new file mode 100644 index 000000000..67d356336 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp @@ -0,0 +1,69 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; bbs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs)) + MISC_WEIGHT_OOB) + )) + +(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 0 ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + (precompile-processing---dup-cdo) ;; reference offset + (precompile-processing---dup-cds) ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) +(defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) + +(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset + (precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs + 0 ;; low part of some {b,e,m}bs + 0 ;; bit indicating whether to compute max(xbs, ybs) or not + )) + +(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) +(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp new file mode 100644 index 000000000..f2ca069e2 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp @@ -0,0 +1,63 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ebs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs)) + MISC_WEIGHT_OOB) + )) + +(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 32 ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + (precompile-processing---dup-cdo) ;; reference offset + (precompile-processing---dup-cds) ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) +(defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) + +(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset + (precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs + 0 ;; low part of some {b,e,m}bs + 0 ;; bit indicating whether to compute max(xbs, ybs) or not + )) + +(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) +(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp new file mode 100644 index 000000000..0453e5009 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp @@ -0,0 +1,71 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; mbs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---mbs-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-mbs)) + MISC_WEIGHT_OOB) + )) + +(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---mbs-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 64 ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + (precompile-processing---dup-cdo) ;; reference offset + (precompile-processing---dup-cds) ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defun (precompile-processing---MODEXP---mbs-hi) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) +(defun (precompile-processing---MODEXP---mbs-lo) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) + +(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset + (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-within-bounds) ;; bit indicating whether to compute max(xbs, ybs) or not + )) + + +(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" + +(defun (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) (* (precompile-processing---MODEXP---bbs-within-bounds) + (precompile-processing---MODEXP---ebs-within-bounds) + (precompile-processing---MODEXP---mbs-within-bounds) + )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp new file mode 100644 index 000000000..045749045 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp @@ -0,0 +1,104 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; leading_word analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift misc/OOB_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) + + +(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (precompile-processing---MODEXP---load-lead) ) + (eq! (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (precompile-processing---MODEXP---load-lead) ) + (eq! (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) + (eq! (+ (shift misc/MXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) + (shift misc/STP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) + 0) + )) + + +(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) + (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset + (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) + (precompile-processing---dup-cds) ;; call data size + (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) + ))) + +(defun (precompile-processing---MODEXP---load-lead) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" + + +(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) + (set-MMU-instruction---mload precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset + CONTEXT_NUMBER ;; source ID + ;; tgt_id ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + (+ (precompile-processing---dup-cdo) + 96 + (precompile-processing---MODEXP---bbs-lo)) ;; source offset low + ;; tgt_offset_lo ;; target offset low + ;; size ;; size + ;; ref_offset ;; reference offset + ;; ref_size ;; reference size + ;; success_bit ;; success bit + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) + + +(defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-EXP-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) + (set-EXP-instruction-MODEXP-lead-log + precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; row offset + (precompile-processing---MODEXP---raw-lead-hi) ;; raw leading word where exponent starts, high part + (precompile-processing---MODEXP---raw-lead-lo) ;; raw leading word where exponent starts, low part + (precompile-processing---MODEXP---cds-cutoff) ;; min{max{cds - 96 - bbs, 0}, 32} + (precompile-processing---MODEXP---ebs-cutoff) ;; min{ebs, 32} + ))) + +(defun (precompile-processing---MODEXP---lead-log) (* (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) + (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) + (* 16 (precompile-processing---MODEXP---sub-ebs-32)))) + +;; @OLIVIER: on reprend ici; pas sûr que modexp-full-log soit bien défini (filtres différents) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp new file mode 100644 index 000000000..f7517986b --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp @@ -0,0 +1,43 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; pricing analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---pricing) + (* (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) MISC_WEIGHT_OOB) + )) + +(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + (set-OOB-instruction---modexp-pricing precompile-processing---MODEXP---misc-row-offset---pricing ;; offset + (precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile + (precompile-processing---dup-r@c) ;; return at capacity + (precompile-processing---MODEXP---modexp-full-log) ;; leading (≤) word log of exponent + (precompile-processing---MODEXP---max-mbs-bbs) ;; call data size + )) + +(defun (precompile-processing---MODEXP---ram-success) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---pricing)) +(defun (precompile-processing---MODEXP---return-gas) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---pricing)) +(defun (precompile-processing---MODEXP---r@c-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---pricing)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp new file mode 100644 index 000000000..41d70f7bf --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/generalities.lisp @@ -0,0 +1,25 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (precompile-processing---MODEXP---standard-precondition) (* PEEK_AT_SCENARIO scenario/PRC_MODEXP)) + +(defconstraint precompile-processing---MODEXP---excluding-execution-scenarios + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! scenario/PRC_FAILURE_KNOWN_TO_HUB)) + diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp new file mode 100644 index 000000000..7d8aa9600 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp @@ -0,0 +1,30 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Justifying precompile success / failure scenarios ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint precompile-processing---MODEXP---justifying-success-failure-scenarios (:guard (precompile-processing---MODEXP---standard-precondition)) + (begin + (eq! (scenario-shorthand---PRC---success) (precompile-processing---MODEXP---ram-success)) + (eq! (precompile-processing---prd-return-gas) (precompile-processing---MODEXP---return-gas)) + )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/zzz_old.lispX similarity index 99% rename from hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp rename to hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/zzz_old.lispX index e1fcd2be4..3a06a2f75 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/zzz_old.lispX @@ -28,6 +28,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (defconstraint precompile-processing---MODEXP---cds-misc-row---setting-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis) MISC_WEIGHT_OOB)) From b2435c4125060ba96bb6d494a78a1145e97ff703 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 6 Nov 2025 20:42:11 +0100 Subject: [PATCH 03/10] ras: formatting --- .../__01__call_data_size_analysis_row.lisp | 14 ++++++++++---- .../modexp/common/__02__bbs_extraction_row.lisp | 3 +++ .../modexp/common/__03__ebs_extraction_row.lisp | 16 +++++++++++++--- .../modexp/common/__04__mbs_extraction_row.lisp | 15 ++++++++++++--- .../modexp/common/__06__pricing_row.lisp | 5 ++++- .../common/justifying_hub_predictions.lisp | 4 +++- 6 files changed, 45 insertions(+), 12 deletions(-) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp index 10c9a82f0..148467c45 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp @@ -24,14 +24,20 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis) MISC_WEIGHT_OOB)) -(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + +(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset (precompile-processing---dup-cds))) ;; call data size -(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) -(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) + +(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" +(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" (defun (precompile-processing---MODEXP---extract-mbs) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp index 67d356336..a4b0a534e 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp @@ -31,6 +31,7 @@ MISC_WEIGHT_OOB) )) + (defconstraint precompile-processing---MODEXP---bbs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -55,6 +56,7 @@ (defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) (defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) + (defconstraint precompile-processing---MODEXP---bbs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -65,5 +67,6 @@ 0 ;; bit indicating whether to compute max(xbs, ybs) or not )) + (defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) (defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp index f2ca069e2..5fd5ca9d6 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp @@ -23,13 +23,18 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-analysis) (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs)) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + +(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-analysis) (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset CONTEXT_NUMBER ;; source ID @@ -48,10 +53,14 @@ ;; phase ;; phase ))) + (defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) (defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + +(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset (precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs (precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs @@ -59,5 +68,6 @@ 0 ;; bit indicating whether to compute max(xbs, ybs) or not )) + (defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) (defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) ;; "" diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp index 0453e5009..66172fb5e 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp @@ -23,13 +23,18 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-misc-module-flags + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---mbs-analysis) (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-mbs)) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + +(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-MMU-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---mbs-analysis) (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset CONTEXT_NUMBER ;; source ID @@ -48,10 +53,14 @@ ;; phase ;; phase ))) + (defun (precompile-processing---MODEXP---mbs-hi) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) (defun (precompile-processing---MODEXP---mbs-lo) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + +(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp index f7517986b..2ee2012ad 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp @@ -30,7 +30,10 @@ (* (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) + +(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (set-OOB-instruction---modexp-pricing precompile-processing---MODEXP---misc-row-offset---pricing ;; offset (precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile (precompile-processing---dup-r@c) ;; return at capacity diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp index 7d8aa9600..8b3d5c235 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp @@ -23,7 +23,9 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---justifying-success-failure-scenarios (:guard (precompile-processing---MODEXP---standard-precondition)) +(defconstraint precompile-processing---MODEXP---justifying-success-failure-scenarios + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin (eq! (scenario-shorthand---PRC---success) (precompile-processing---MODEXP---ram-success)) (eq! (precompile-processing---prd-return-gas) (precompile-processing---MODEXP---return-gas)) From 1939d1613766ccaa38e8f72ad04f155dc476dc0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 6 Nov 2025 22:49:00 +0100 Subject: [PATCH 04/10] feat: done with HUB (?) --- .../__01__call_data_size_analysis_row.lisp | 4 +- .../common/__02__bbs_extraction_row.lisp | 28 ++++---- .../common/__03__ebs_extraction_row.lisp | 28 ++++---- .../common/__04__mbs_extraction_row.lisp | 40 ++++++------ ...ding_word_extraction_and_analysis_row.lisp | 65 +++++++++---------- .../modexp/common/__06__pricing_row.lisp | 2 +- .../common/justifying_hub_predictions.lisp | 4 +- .../call/precompiles/modexp/constants.lisp | 6 +- 8 files changed, 90 insertions(+), 87 deletions(-) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp index 148467c45..d1f219a69 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp @@ -24,14 +24,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-module-flags +(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis) MISC_WEIGHT_OOB)) -(defconstraint precompile-processing---MODEXP---cds-misc-row---setting-OOB-instruction +(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp index a4b0a534e..f7a27ad12 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp @@ -23,20 +23,20 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-misc-module-flags +(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-analysis) + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs)) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-MMU-instruction +(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-analysis) - (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset CONTEXT_NUMBER ;; source ID ;; tgt_id ;; target ID ;; aux_id ;; auxiliary ID @@ -47,20 +47,20 @@ (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE ;; exo_sum ;; weighted exogenous module flag sum ;; phase ;; phase ))) -(defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) -(defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-analysis))) +(defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis))) +(defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis))) -(defconstraint precompile-processing---MODEXP---bbs-analysis---setting-OOB-instruction +(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-analysis ;; offset + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset (precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs 0 ;; low part of some {b,e,m}bs @@ -68,5 +68,7 @@ )) -(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) -(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---bbs-normalized) (* (precompile-processing---MODEXP---bbs-lo) + (precompile-processing---MODEXP---bbs-within-bounds))) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp index 5fd5ca9d6..147cb611b 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp @@ -23,20 +23,20 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-misc-module-flags +(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-analysis) + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs)) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-MMU-instruction +(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-analysis) - (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset CONTEXT_NUMBER ;; source ID ;; tgt_id ;; target ID ;; aux_id ;; auxiliary ID @@ -47,21 +47,21 @@ (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE ;; exo_sum ;; weighted exogenous module flag sum ;; phase ;; phase ))) -(defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) -(defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-analysis))) +(defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis))) +(defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis))) -(defconstraint precompile-processing---MODEXP---ebs-analysis---setting-OOB-instruction +(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-analysis ;; offset + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset (precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs (precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs 0 ;; low part of some {b,e,m}bs @@ -69,5 +69,7 @@ )) -(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) -(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)) +(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---ebs-normalized) (* (precompile-processing---MODEXP---ebs-lo) + (precompile-processing---MODEXP---ebs-within-bounds))) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp index 66172fb5e..32f48eebb 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp @@ -23,20 +23,20 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-misc-module-flags +(defconstraint precompile-processing---MODEXP---mbs-extraction-and-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---mbs-analysis) + (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-mbs)) MISC_WEIGHT_OOB) )) -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-MMU-instruction +(defconstraint precompile-processing---MODEXP---mbs-extraction-and-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---mbs-analysis) - (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset + (if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) + (set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis ;; offset CONTEXT_NUMBER ;; source ID ;; tgt_id ;; target ID ;; aux_id ;; auxiliary ID @@ -47,32 +47,34 @@ (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit - (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE - (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE + (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE ;; exo_sum ;; weighted exogenous module flag sum ;; phase ;; phase ))) -(defun (precompile-processing---MODEXP---mbs-hi) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) -(defun (precompile-processing---MODEXP---mbs-lo) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-analysis))) +(defun (precompile-processing---MODEXP---mbs-hi) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis))) +(defun (precompile-processing---MODEXP---mbs-lo) (* (precompile-processing---MODEXP---extract-mbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis))) -(defconstraint precompile-processing---MODEXP---mbs-analysis---setting-OOB-instruction +(defconstraint precompile-processing---MODEXP---mbs-extraction-and-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---mbs-analysis ;; offset - (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs - (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs - (precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs - (precompile-processing---MODEXP---bbs-within-bounds) ;; bit indicating whether to compute max(xbs, ybs) or not + (set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis ;; offset + (precompile-processing---MODEXP---mbs-hi) ;; high part of some {b,e,m}bs + (precompile-processing---MODEXP---mbs-lo) ;; low part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-normalized) ;; low part of some {b,e,m}bs + (precompile-processing---MODEXP---bbs-within-bounds) ;; bit indicating whether to compute max(xbs, ybs) or not )) -(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" -(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" -(defun (precompile-processing---MODEXP---mbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" -(defun (precompile-processing---MODEXP---mbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---mbs-analysis)) ;; "" +(defun (precompile-processing---MODEXP---max-mbs-bbs) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis)) ;; "" +(defun (precompile-processing---MODEXP---mbs-normalized) (* (precompile-processing---MODEXP---mbs-lo) + (precompile-processing---MODEXP---mbs-within-bounds))) (defun (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) (* (precompile-processing---MODEXP---bbs-within-bounds) (precompile-processing---MODEXP---ebs-within-bounds) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp index 045749045..2c2ec6bc5 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp @@ -16,25 +16,25 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; leading_word analysis row ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; leading_word extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) -(defun (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) -(defun (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift misc/OOB_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-OOB-on-leading-word-row) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) (defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin - (eq! (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) (precompile-processing---MODEXP---load-lead) ) - (eq! (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (precompile-processing---MODEXP---load-lead) ) - (eq! (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) + (eq! (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (precompile-processing---MODEXP---extract-leading-word) ) + (eq! (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (precompile-processing---MODEXP---extract-leading-word) ) + (eq! (precompile-processing---MODEXP---call-OOB-on-leading-word-row) 1 ) (eq! (+ (shift misc/MXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis) (shift misc/STP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) 0) @@ -46,21 +46,21 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-not-zero (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset - (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) + (precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size) (precompile-processing---dup-cds) ;; call data size - (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) + (precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size) ))) -(defun (precompile-processing---MODEXP---load-lead) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defun (precompile-processing---MODEXP---extract-leading-word) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" +(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" (defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) + (if-not-zero (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (set-MMU-instruction---mload precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset CONTEXT_NUMBER ;; source ID ;; tgt_id ;; target ID @@ -68,7 +68,7 @@ ;; src_offset_hi ;; source offset high (+ (precompile-processing---dup-cdo) 96 - (precompile-processing---MODEXP---bbs-lo)) ;; source offset low + (precompile-processing---MODEXP---bbs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low ;; size ;; size ;; ref_offset ;; reference offset @@ -80,25 +80,22 @@ ;; phase ;; phase ))) -(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) -(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---call-MMU-module-for-modexp-lead) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---raw-lead-hi) (* (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) +(defun (precompile-processing---MODEXP---raw-lead-lo) (* (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) (defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-EXP-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) - (set-EXP-instruction-MODEXP-lead-log - precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; row offset - (precompile-processing---MODEXP---raw-lead-hi) ;; raw leading word where exponent starts, high part - (precompile-processing---MODEXP---raw-lead-lo) ;; raw leading word where exponent starts, low part - (precompile-processing---MODEXP---cds-cutoff) ;; min{max{cds - 96 - bbs, 0}, 32} - (precompile-processing---MODEXP---ebs-cutoff) ;; min{ebs, 32} - ))) - -(defun (precompile-processing---MODEXP---lead-log) (* (precompile-processing---MODEXP---call-EXP-module-for-modexp-lead) - (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) - (* 16 (precompile-processing---MODEXP---sub-ebs-32)))) + (if-not-zero (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) + (set-EXP-instruction-MODEXP-lead-log precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; row offset + (precompile-processing---MODEXP---raw-lead-hi) ;; raw leading word where exponent starts, high part + (precompile-processing---MODEXP---raw-lead-lo) ;; raw leading word where exponent starts, low part + (precompile-processing---MODEXP---cds-cutoff) ;; min{max{cds - 96 - bbs, 0}, 32} + (precompile-processing---MODEXP---ebs-cutoff) ;; min{ebs, 32} + ))) + +(defun (precompile-processing---MODEXP---lead-log) (shift [misc/EXP_DATA 5] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---modexp-full-log) (+ (precompile-processing---MODEXP---lead-log) (* 16 (precompile-processing---MODEXP---sub-ebs-32)))) ;; @OLIVIER: on reprend ici; pas sûr que modexp-full-log soit bien défini (filtres différents) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp index 2ee2012ad..2faa93e97 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp @@ -27,7 +27,7 @@ (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---pricing) - (* (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) MISC_WEIGHT_OOB) + MISC_WEIGHT_OOB )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp index 8b3d5c235..2030aaeac 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp @@ -27,6 +27,6 @@ (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin - (eq! (scenario-shorthand---PRC---success) (precompile-processing---MODEXP---ram-success)) - (eq! (precompile-processing---prd-return-gas) (precompile-processing---MODEXP---return-gas)) + (eq! (scenario-shorthand---PRC---success) (* (precompile-processing---MODEXP---ram-success) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) + (eq! (precompile-processing---prd-return-gas) (* (precompile-processing---MODEXP---return-gas) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) )) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp index f9b7545f0..1ef0064d2 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/constants.lisp @@ -11,9 +11,9 @@ (defconst precompile-processing---MODEXP---misc-row-offset---cds-analysis 1 - precompile-processing---MODEXP---misc-row-offset---bbs-analysis 2 - precompile-processing---MODEXP---misc-row-offset---ebs-analysis 3 - precompile-processing---MODEXP---misc-row-offset---mbs-analysis 4 + precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis 2 + precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis 3 + precompile-processing---MODEXP---misc-row-offset---mbs-extraction-and-analysis 4 precompile-processing---MODEXP---misc-row-offset---leading-word-analysis 5 precompile-processing---MODEXP---misc-row-offset---pricing 6 precompile-processing---MODEXP---misc-row-offset---base-extraction 7 From f35d9b478d82c1aa42a02973a41f2eb95ed387da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 6 Nov 2025 22:53:05 +0100 Subject: [PATCH 05/10] fix: make it compile --- ...ding_word_extraction_and_analysis_row.lisp | 23 +++++++++---------- .../common/justifying_hub_predictions.lisp | 4 ++-- 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp index 2c2ec6bc5..50318fcae 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp @@ -25,7 +25,7 @@ (defun (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (shift misc/EXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) (defun (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) -(defun (precompile-processing---MODEXP---call-OOB-on-leading-word-row) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) +(defun (precompile-processing---MODEXP---call-OOB-on-leading-word-row) (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) (defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-misc-module-flags @@ -44,17 +44,16 @@ (defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) - (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset - (precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size) - (precompile-processing---dup-cds) ;; call data size - (precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size) - ))) - -(defun (precompile-processing---MODEXP---extract-leading-word) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defun (precompile-processing---MODEXP---cds-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defun (precompile-processing---MODEXP---ebs-cutoff) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" -(defun (precompile-processing---MODEXP---sub-ebs-32) (* (precompile-processing---MODEXP---call-OOB-module-for-modexp-lead) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))) ;; "" + (set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset + (precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size) + (precompile-processing---dup-cds) ;; call data size + (precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size) + )) + +(defun (precompile-processing---MODEXP---extract-leading-word) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---cds-cutoff) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---ebs-cutoff) (shift [misc/OOB_DATA 7] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" +(defun (precompile-processing---MODEXP---sub-ebs-32) (shift [misc/OOB_DATA 8] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; "" (defconstraint precompile-processing---MODEXP---lead-word-analysis---setting-MMU-instruction diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp index 2030aaeac..6733a8c90 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp @@ -27,6 +27,6 @@ (:guard (precompile-processing---MODEXP---standard-precondition)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin - (eq! (scenario-shorthand---PRC---success) (* (precompile-processing---MODEXP---ram-success) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) - (eq! (precompile-processing---prd-return-gas) (* (precompile-processing---MODEXP---return-gas) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) + (eq! (scenario-shorthand---PRC---success) (* (precompile-processing---MODEXP---ram-success) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) ) + (eq! (precompile-processing---prd-return-gas) (* (precompile-processing---MODEXP---return-gas) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) ) ) )) From 839e3d615ed4bd82c4bdfe3892fa4eb8705d2b04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 6 Nov 2025 23:32:34 +0100 Subject: [PATCH 06/10] ras --- .../call/precompiles/modexp/success.lisp | 28 ++++++++++--------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp index e8339c966..31546f014 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp @@ -44,9 +44,9 @@ (defconstraint precompile-processing---MODEXP---success-case---base-extraction-row---setting-the-OOB-instruction-which-decides-which-actual-parameters-to-extract (:guard (precompile-processing---MODEXP---success-case)) (set-OOB-instruction---modexp-extract precompile-processing---MODEXP---misc-row-offset---base-extraction ;; offset (precompile-processing---dup-cds) ;; call data size - (precompile-processing---MODEXP---bbs-lo) ;; low part of bbs (base byte size) - (precompile-processing---MODEXP---ebs-lo) ;; low part of ebs (exponent byte size) - (precompile-processing---MODEXP---mbs-lo) ;; low part of mbs (modulus byte size) + (precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size) + (precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size) + (precompile-processing---MODEXP---mbs-normalized) ;; low part of mbs (modulus byte size) )) ;; Note: we deduce some shorthands AT THE END OF THE FILE. @@ -79,7 +79,7 @@ ;; src_offset_hi ;; source offset high 96 ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---bbs-lo) ;; size + (precompile-processing---MODEXP---bbs-normalized) ;; size (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit @@ -127,9 +127,9 @@ (+ 1 HUB_STAMP) ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (+ 96 (precompile-processing---MODEXP---bbs-lo)) ;; source offset low + (+ 96 (precompile-processing---MODEXP---bbs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---ebs-lo) ;; size + (precompile-processing---MODEXP---ebs-normalized) ;; size (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit @@ -157,12 +157,14 @@ ;; extract_modulus == 1 case: (set-MMU-instruction---modexp-data precompile-processing---MODEXP---misc-row-offset---modulus-extraction ;; offset CONTEXT_NUMBER ;; source ID - (+ 1 HUB_STAMP) ;; target ID + (+ 1 HUB_STAMP) ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (+ 96 (precompile-processing---MODEXP---bbs-lo) (precompile-processing---MODEXP---ebs-lo)) ;; source offset low + (+ 96 + (precompile-processing---MODEXP---bbs-normalized) + (precompile-processing---MODEXP---ebs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---mbs-lo) ;; size + (precompile-processing---MODEXP---mbs-normalized) ;; size (precompile-processing---dup-cdo) ;; reference offset (precompile-processing---dup-cds) ;; reference size ;; success_bit ;; success bit @@ -225,9 +227,9 @@ CONTEXT_NUMBER ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (- 512 (precompile-processing---MODEXP---mbs-lo)) ;; source offset low + (- 512 (precompile-processing---MODEXP---mbs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low - (precompile-processing---MODEXP---mbs-lo) ;; size + (precompile-processing---MODEXP---mbs-normalized) ;; size (precompile-processing---dup-r@o) ;; reference offset (precompile-processing---dup-r@c) ;; reference size ;; success_bit ;; success bit @@ -248,8 +250,8 @@ (provide-return-data precompile-processing---MODEXP---context-row-offset---success ;; row offset CONTEXT_NUMBER ;; receiver context (+ 1 HUB_STAMP) ;; provider context - (- 512 (precompile-processing---MODEXP---mbs-lo)) ;; rdo - (precompile-processing---MODEXP---mbs-lo) ;; rds + (- 512 (precompile-processing---MODEXP---mbs-normalized)) ;; rdo + (precompile-processing---MODEXP---mbs-normalized) ;; rds )) From ad8e35b088d25da4346527b7f96e5f0dd0b4b410 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 6 Nov 2025 23:53:36 +0100 Subject: [PATCH 07/10] ras: replace (deprectated) 512 of MODEXP with 1024 macro --- constants/constants.lisp | 1 + .../call/precompiles/modexp/success.lisp | 8 +++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/constants/constants.lisp b/constants/constants.lisp index a03e1bd55..1ce16cecb 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -269,6 +269,7 @@ HISTORY_STORAGE_ADDRESS_HI 0x0000f908 HISTORY_STORAGE_ADDRESS_LO 0x27f1c53a10cb7a02335b175320002935 EIP_7825_TRANSACTION_GAS_LIMIT_CAP 0x1000000 ;; 2^24 == 16777216 appears in OSAKA + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1024 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; LINEA MISC ;; diff --git a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp index 31546f014..eb01e306b 100644 --- a/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/success.lisp @@ -196,7 +196,7 @@ ;; src_offset_hi ;; source offset high ;; src_offset_lo ;; source offset low ;; tgt_offset_lo ;; target offset low - 512 ;; size + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND ;; size ;; ref_offset ;; reference offset ;; ref_size ;; reference size ;; success_bit ;; success bit @@ -227,7 +227,8 @@ CONTEXT_NUMBER ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (- 512 (precompile-processing---MODEXP---mbs-normalized)) ;; source offset low + (- EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND + (precompile-processing---MODEXP---mbs-normalized)) ;; source offset low ;; tgt_offset_lo ;; target offset low (precompile-processing---MODEXP---mbs-normalized) ;; size (precompile-processing---dup-r@o) ;; reference offset @@ -250,7 +251,8 @@ (provide-return-data precompile-processing---MODEXP---context-row-offset---success ;; row offset CONTEXT_NUMBER ;; receiver context (+ 1 HUB_STAMP) ;; provider context - (- 512 (precompile-processing---MODEXP---mbs-normalized)) ;; rdo + (- EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND + (precompile-processing---MODEXP---mbs-normalized)) ;; rdo (precompile-processing---MODEXP---mbs-normalized) ;; rds )) From 4f70e049d170f0c7ff7b5b2a1590752162d3926f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 7 Nov 2025 00:58:28 +0100 Subject: [PATCH 08/10] fix: MODEXP related OOB instructions --- oob/osaka/precompiles/modexp/lead.lisp | 6 +- oob/osaka/precompiles/modexp/xbs.lisp | 103 +++++++++++++++++-------- 2 files changed, 75 insertions(+), 34 deletions(-) diff --git a/oob/osaka/precompiles/modexp/lead.lisp b/oob/osaka/precompiles/modexp/lead.lisp index d02040e00..0a2c267c0 100644 --- a/oob/osaka/precompiles/modexp/lead.lisp +++ b/oob/osaka/precompiles/modexp/lead.lisp @@ -10,7 +10,7 @@ (defun (prc-modexp-lead---standard-precondition) IS_MODEXP_LEAD) (defun (prc-modexp-lead---bbs) [DATA 1]) (defun (prc-modexp-lead---ebs) [DATA 3]) -(defun (prc-modexp-lead---load-lead) [DATA 4]) +(defun (prc-modexp-lead---extract-leading-word) [DATA 4]) (defun (prc-modexp-lead---cds-cutoff) [DATA 6]) (defun (prc-modexp-lead---ebs-cutoff) [DATA 7]) (defun (prc-modexp-lead---sub-ebs_32) [DATA 8]) @@ -19,6 +19,8 @@ (defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2)) (defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3)) +;; "" + (defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) (call-to-ISZERO 0 0 (prc-modexp-lead---ebs))) @@ -37,7 +39,7 @@ 32))) (defconstraint prc-modexp-lead---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (begin (eq! (prc-modexp-lead---load-lead) + (begin (eq! (prc-modexp-lead---extract-leading-word) (* (prc-modexp-lead---call-data-contains-exponent-bytes) (- 1 (prc-modexp-lead---ebs-is-zero)))) (if-zero (prc-modexp-lead---call-data-contains-exponent-bytes) diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index fbaaf481a..70dee1a74 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -7,35 +7,74 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) -(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) -(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) -(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) -(defun (prc-modexp-xbs---compute-max) [DATA 4]) -(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) -(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) - -(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-LT 0 (prc-modexp-xbs---xbs-hi) (prc-modexp-xbs---xbs-lo) 0 513)) - -(defconstraint prc-modexp-xbs---compare-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo))) - -(defconstraint prc-modexp-xbs---check-xbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo))) - -(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) - -(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (if-zero (prc-modexp-xbs---compute-max) - (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) - (vanishes! (prc-modexp-xbs---xbs-nonzero))) - (begin (eq! (prc-modexp-xbs---xbs-nonzero) - (- 1 (shift OUTGOING_RES_LO 2))) - (if-zero (prc-modexp-xbs---comp) - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---xbs-lo)) - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---ybs-lo)))))) +(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) +(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) +(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) +(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) +(defun (prc-modexp-xbs---compute-max) [DATA 4]) +(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) +(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) +(defun (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---xbs-is-LT-ybs) (next OUTGOING_RES_LO)) ;; "" + +(defconstraint prc-modexp-xbs---compare-xbs-against-MODEXP-upper-byte-size-bound + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + (call-to-LT 0 + (prc-modexp-xbs---xbs-hi) + (prc-modexp-xbs---xbs-lo) + 0 + (+ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1) + )) + + +(defconstraint prc-modexp-xbs---compare-xbs-against-ybs + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo))) + + +(defconstraint prc-modexp-xbs---check-xbs-is-zero + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo))) + + +(defconstraint additional-prc-modexp-xbs + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) + (eq! (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) 1))) + + +(defconstraint prc-modexp-xbs---justifying-hub-predictions---nonzeroness-bit + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero (prc-modexp-xbs---compute-max) + ;; comupte max = false + (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + (vanishes! (prc-modexp-xbs---xbs-nonzero))) + ;; comupte max = false + (begin (eq! (prc-modexp-xbs---xbs-nonzero) + (- 1 (shift OUTGOING_RES_LO 2))) + ))) + + +(defconstraint prc-modexp-xbs---justifying-hub-predictions---value-of-max + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero (prc-modexp-xbs---compute-max) + ;; comupte_max = false + (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + ;; comupte_max = false + (if-zero (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) + ;; false case + (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + ;; true case + (if-zero (prc-modexp-xbs---xbs-is-LT-ybs) + ;; false case + (eq! (prc-modexp-xbs---max-xbs-ybs) + (prc-modexp-xbs---xbs-lo)) + ;; true case + (eq! (prc-modexp-xbs---max-xbs-ybs) + (prc-modexp-xbs---ybs-lo)) + )))) From 0117e1e59a8917aeeb84b781bde08e7a4ff0f959 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 7 Nov 2025 01:36:40 +0100 Subject: [PATCH 09/10] fix: OOB instructions ... xbs was all wrong ? or did I change the spec that radically ? --- oob/osaka/precompiles/modexp/xbs.lisp | 53 +++++++++++++++++---------- 1 file changed, 33 insertions(+), 20 deletions(-) diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index 70dee1a74..0e58f7f07 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -8,14 +8,19 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) -(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) -(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) -(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) -(defun (prc-modexp-xbs---compute-max) [DATA 4]) -(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) OUTGOING_RES_LO) -(defun (prc-modexp-xbs---xbs-is-LT-ybs) (next OUTGOING_RES_LO)) ;; "" +(defun (prc-modexp-xbs---xbs-hi) [ DATA 1 ]) +(defun (prc-modexp-xbs---xbs-lo) [ DATA 2 ]) +(defun (prc-modexp-xbs---ybs-lo) [ DATA 3 ]) +(defun (prc-modexp-xbs---compute-max) [ DATA 4 ]) +(defun (prc-modexp-xbs---max-xbs-ybs) [ DATA 7 ]) +(defun (prc-modexp-xbs---xbs-nonzero) [ DATA 8 ]) +(defun (prc-modexp-xbs---xbs-within-bounds) [ DATA 9 ]) +(defun (prc-modexp-xbs---xbs-out-of-bounds) [ DATA 10 ]) + +(defun (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) (shift OUTGOING_RES_LO 0)) ;; "" +(defun (prc-modexp-xbs---xbs-is-LT-ybs) (shift OUTGOING_RES_LO 1)) ;; "" +(defun (prc-modexp-xbs---xbs-lo-is-zero) (shift OUTGOING_RES_LO 2)) ;; "" + (defconstraint prc-modexp-xbs---compare-xbs-against-MODEXP-upper-byte-size-bound (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) @@ -27,16 +32,28 @@ )) +(defun (prc-modexp-xbs---xbs-normalized) (* (prc-modexp-xbs---xbs-lo) (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) ) ) +(defun (prc-modexp-xbs---ybs-normalized) (* (prc-modexp-xbs---ybs-lo) (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) ) ) + + (defconstraint prc-modexp-xbs---compare-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo))) + (call-to-LT 1 + 0 + (prc-modexp-xbs---xbs-normalized) + 0 + (prc-modexp-xbs---ybs-normalized) + )) (defconstraint prc-modexp-xbs---check-xbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo))) + (call-to-ISZERO 2 + 0 + (prc-modexp-xbs---xbs-normalized) + )) (defconstraint additional-prc-modexp-xbs @@ -46,20 +63,16 @@ (eq! (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) 1))) -(defconstraint prc-modexp-xbs---justifying-hub-predictions---nonzeroness-bit +(defconstraint prc-modexp-xbs---justifying-hub-predictions---various-prediction-bits (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-zero (prc-modexp-xbs---compute-max) - ;; comupte max = false - (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) - (vanishes! (prc-modexp-xbs---xbs-nonzero))) - ;; comupte max = false - (begin (eq! (prc-modexp-xbs---xbs-nonzero) - (- 1 (shift OUTGOING_RES_LO 2))) - ))) + (begin (eq! (prc-modexp-xbs---xbs-nonzero) (- 1 (prc-modexp-xbs---xbs-lo-is-zero) )) + (eq! (prc-modexp-xbs---xbs-within-bounds) (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) ) + (eq! (prc-modexp-xbs---xbs-out-of-bounds) (- 1 (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound)) ) + )) -(defconstraint prc-modexp-xbs---justifying-hub-predictions---value-of-max +(defconstraint prc-modexp-xbs---justifying-hub-predictions---setting-the-value-of-max-xbs-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (if-zero (prc-modexp-xbs---compute-max) From 6bcb9fc372f83e9e533db2a296628f44c59f1283 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 7 Nov 2025 14:57:07 +0100 Subject: [PATCH 10/10] ras: formatting --- oob/osaka/precompiles/modexp/xbs.lisp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index b3a5779b7..a204106b7 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -46,6 +46,9 @@ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE )) +(defun (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND )) +(defun (prc-modexp-xbs---xbs-is-GT-the-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -65,6 +68,8 @@ (prc-modexp-xbs---ybs-lo) )) +(defun (prc-modexp-xbs---xbs-is-LT-ybs) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_YBS )) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -82,11 +87,8 @@ (prc-modexp-xbs---xbs-lo) )) +(defun (prc-modexp-xbs---xbs-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_ISZERO_CHECK )) -(defun (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND )) -(defun (prc-modexp-xbs---xbs-is-LT-ybs) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_YBS )) -(defun (prc-modexp-xbs---xbs-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_ISZERO_CHECK )) -(defun (prc-modexp-xbs---xbs-is-GT-the-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;