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..d1f219a69 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp @@ -0,0 +1,43 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CALL_DATA_SIZE analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(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---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 + (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..f7a27ad12 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp @@ -0,0 +1,74 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; bbs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(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-extraction-and-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs)) + MISC_WEIGHT_OOB) + )) + + +(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-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 + ;; 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-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-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-extraction-and-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (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 + 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-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 new file mode 100644 index 000000000..147cb611b --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp @@ -0,0 +1,75 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ebs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(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-extraction-and-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs)) + MISC_WEIGHT_OOB) + )) + + +(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-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 + ;; 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-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-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-extraction-and-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (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 + 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-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 new file mode 100644 index 000000000..32f48eebb --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__04__mbs_extraction_row.lisp @@ -0,0 +1,82 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; mbs extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(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-extraction-and-analysis) + (+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-mbs)) + MISC_WEIGHT_OOB) + )) + + +(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-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 + ;; 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-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-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-extraction-and-analysis---setting-OOB-instruction + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (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-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) + (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..50318fcae --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp @@ -0,0 +1,100 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.Y CALL ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z.4 MODEXP common processing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; leading_word extraction and analysis row ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(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-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) + )) + + +(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-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 + (:guard (precompile-processing---MODEXP---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (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 + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + (+ (precompile-processing---dup-cdo) + 96 + (precompile-processing---MODEXP---bbs-normalized)) ;; 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-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-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 new file mode 100644 index 000000000..2faa93e97 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp @@ -0,0 +1,46 @@ +(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) + 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..6733a8c90 --- /dev/null +++ b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/justifying_hub_predictions.lisp @@ -0,0 +1,32 @@ +(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) (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/common.lisp b/hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/zzz_old.lispX similarity index 79% 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 f8b58381a..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)) @@ -48,13 +49,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 +81,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 +91,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 +138,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 +183,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 +204,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) + ))) -(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) +(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 @@ -225,12 +261,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 +277,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 +291,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)) 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 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..eb01e306b 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 @@ -194,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 @@ -225,9 +227,10 @@ CONTEXT_NUMBER ;; target ID ;; aux_id ;; auxiliary ID ;; src_offset_hi ;; source offset high - (- 512 (precompile-processing---MODEXP---mbs-lo)) ;; 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-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 +251,9 @@ (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 + (- EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND + (precompile-processing---MODEXP---mbs-normalized)) ;; rdo + (precompile-processing---MODEXP---mbs-normalized) ;; rds )) diff --git a/oob/osaka/precompiles/modexp/lead.lisp b/oob/osaka/precompiles/modexp/lead.lisp index d0bde1347..3ea070382 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---result-of-comparison) (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 a8c07fbed..a204106b7 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -8,7 +8,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (defconst EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE (+ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1) @@ -47,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))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -66,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 )) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -83,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-LEQ-EIP-7823-upper-bound) (shift OUTGOING_RES_LO ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND )) -(defun (prc-modexp-xbs---result-of-comparison) (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-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -97,41 +98,37 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (defconstraint prc-modexp-xbs---binarity-sanity-check (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (is-binary (prc-modexp-xbs---compute-max))) -(defconstraint prc-modexp-xbs---justify-hub-predictions---xbs-nonzero - (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (eq! (prc-modexp-xbs---xbs-is-zero) - (- 1 (prc-modexp-xbs---xbs-nonzero)) - )) - -(defconstraint prc-modexp-xbs---justify-hub-predictions---sans-max-computation - (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-zero (prc-modexp-xbs---compute-max) - (vanishes! (prc-modexp-xbs---max-xbs-ybs)) - )) - -(defconstraint prc-modexp-xbs---justify-hub-predictions---with-max-computation - (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (prc-modexp-xbs---compute-max) - (if-zero (prc-modexp-xbs---result-of-comparison) - ;; result-of-comparison ≡ faux case - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---xbs-lo)) - ;; result-of-comparison ≡ true case - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---ybs-lo)) - ))) - -(defconstraint prc-modexp-xbs---justify-hub-predictions---bounds-bits - (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (begin (eq! (prc-modexp-xbs---xbs-within-bounds) (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound)) - (eq! (prc-modexp-xbs---xbs-out-of-bounds) (prc-modexp-xbs---xbs-is-GT-EIP-7823-upper-bound)) - )) +(defconstraint prc-modexp-xbs---justifying-hub-predictions---various-prediction-bits + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin (eq! (prc-modexp-xbs---xbs-nonzero) (- 1 (prc-modexp-xbs---xbs-is-zero)) ) + (eq! (prc-modexp-xbs---xbs-within-bounds) (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-upper-bound) ) + (eq! (prc-modexp-xbs---xbs-out-of-bounds) (prc-modexp-xbs---xbs-is-GT-the-EIP-7823-upper-bound) ) + )) + + +(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) + ;; comupte_max = false + (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + ;; comupte_max = false + (if-zero (prc-modexp-xbs---xbs-is-LE-the-EIP-7823-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)) + ))))