From 605b79266dcf1425bc6ac3833384acd174cb62df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 15:54:05 +0200 Subject: [PATCH 1/9] ras --- todo | 29 ----------------------------- 1 file changed, 29 deletions(-) delete mode 100644 todo diff --git a/todo b/todo deleted file mode 100644 index b98536f9..00000000 --- a/todo +++ /dev/null @@ -1,29 +0,0 @@ -✅ hub/columns/scenarios/precompiles.tex -✅ hub/scenario/generalities/precompiles.tex -✅ hub/scenario/shorthands/precompile.tex -✅ hub/instruction_handling/call/precompiles/common/generalities.tex -❌ hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/success.tex -✅ hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing_bls/failure_KTR.tex -✅ hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing_bls/success.tex -❌ hub/instruction_handling/call/precompiles/nsr_and_flagsum.tex -✅ hub/instruction_handling/call/precompiles/nsr_and_flagsum_I.tex -✅ hub/instruction_handling/call/precompiles/nsr_and_flagsum_II.tex - - - - - - - - - - -❌ Lisp erase -⚠️ Lisp todo -✅ Lisp done - - - -❌ Lisp ràf -⚠️ Lisp unclear -✅ Lisp done From c6e8c340dcd5a531146e085c857176be999d0f64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 13 Oct 2025 20:25:16 +0200 Subject: [PATCH 2/9] ras --- oob/cancun/precompiles/modexp/xbs.lisp | 4 ++-- oob/london/precompiles/modexp/xbs.lisp | 4 ++-- oob/osaka/precompiles/modexp/lead.lisp | 4 ++-- oob/prague/precompiles/modexp/xbs.lisp | 4 ++-- oob/shanghai/precompiles/modexp/xbs.lisp | 4 ++-- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/oob/cancun/precompiles/modexp/xbs.lisp b/oob/cancun/precompiles/modexp/xbs.lisp index fbaaf481..2a0e83e9 100644 --- a/oob/cancun/precompiles/modexp/xbs.lisp +++ b/oob/cancun/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-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))) @@ -28,7 +28,7 @@ (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))) + (eq! (prc-modexp-xbs---comparison-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) diff --git a/oob/london/precompiles/modexp/xbs.lisp b/oob/london/precompiles/modexp/xbs.lisp index fbaaf481..2a0e83e9 100644 --- a/oob/london/precompiles/modexp/xbs.lisp +++ b/oob/london/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-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))) @@ -28,7 +28,7 @@ (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))) + (eq! (prc-modexp-xbs---comparison-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) diff --git a/oob/osaka/precompiles/modexp/lead.lisp b/oob/osaka/precompiles/modexp/lead.lisp index d02040e0..d0bde134 100644 --- a/oob/osaka/precompiles/modexp/lead.lisp +++ b/oob/osaka/precompiles/modexp/lead.lisp @@ -17,7 +17,7 @@ (defun (prc-modexp-lead---ebs-is-zero) OUTGOING_RES_LO) (defun (prc-modexp-lead---ebs-less-than_32) (next OUTGOING_RES_LO)) (defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2)) -(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3)) +(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))) @@ -42,7 +42,7 @@ (- 1 (prc-modexp-lead---ebs-is-zero)))) (if-zero (prc-modexp-lead---call-data-contains-exponent-bytes) (vanishes! (prc-modexp-lead---cds-cutoff)) - (if-zero (prc-modexp-lead---comp) + (if-zero (prc-modexp-lead---result-of-comparison) (eq! (prc-modexp-lead---cds-cutoff) 32) (eq! (prc-modexp-lead---cds-cutoff) (- (prc---cds) (+ 96 (prc-modexp-lead---bbs)))))) diff --git a/oob/prague/precompiles/modexp/xbs.lisp b/oob/prague/precompiles/modexp/xbs.lisp index fbaaf481..2a0e83e9 100644 --- a/oob/prague/precompiles/modexp/xbs.lisp +++ b/oob/prague/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-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))) @@ -28,7 +28,7 @@ (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))) + (eq! (prc-modexp-xbs---comparison-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) diff --git a/oob/shanghai/precompiles/modexp/xbs.lisp b/oob/shanghai/precompiles/modexp/xbs.lisp index fbaaf481..2a0e83e9 100644 --- a/oob/shanghai/precompiles/modexp/xbs.lisp +++ b/oob/shanghai/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-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))) @@ -28,7 +28,7 @@ (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))) + (eq! (prc-modexp-xbs---comparison-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) From eeaa0f94838d54566c9c41220201d7d108d6d1bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 13 Oct 2025 20:26:34 +0200 Subject: [PATCH 3/9] feat: OOB_INST_modexp_xbs instruction update --- constants/constants.lisp | 1 + oob/osaka/precompiles/modexp/xbs.lisp | 113 ++++++++++++++++++-------- 2 files changed, 82 insertions(+), 32 deletions(-) diff --git a/constants/constants.lisp b/constants/constants.lisp index a03e1bd5..1ce16cec 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/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index fbaaf481..47ff49fc 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -7,35 +7,84 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(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)))))) + + +(defconst + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE (+ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1) + ) + + +(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) (force-bin [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) (force-bin [DATA 9])) +(defun (prc-modexp-xbs---xbs-out-of-bounds) (force-bin [DATA 10])) +(defun (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---xbs-is-GT-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound))) +(defun (prc-modexp-xbs---result-of-comparison) (next OUTGOING_RES_LO)) ;; "" + +(defconstraint prc-modexp-xbs---compare-xbs-against-EIP-7823-upper-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_PLUS_ONE + )) + +(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))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (is-binary (prc-modexp-xbs---compute-max))) + +(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) + (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + (vanishes! (prc-modexp-xbs---xbs-nonzero)) + ))) + +(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) + (begin (eq! (prc-modexp-xbs---xbs-nonzero) + (- 1 (shift OUTGOING_RES_LO 2))) + (if-zero (prc-modexp-xbs---result-of-comparison) + ;; result-of-comparison ≡ false 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)) + )) + From 4caa0a350f5cbddc63c142f32775bdf7ff1c1a14 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 22 Oct 2025 20:44:08 +0200 Subject: [PATCH 4/9] ras --- oob/cancun/precompiles/modexp/xbs.lisp | 2 +- oob/london/precompiles/modexp/xbs.lisp | 2 +- oob/prague/precompiles/modexp/xbs.lisp | 2 +- oob/shanghai/precompiles/modexp/xbs.lisp | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/oob/cancun/precompiles/modexp/xbs.lisp b/oob/cancun/precompiles/modexp/xbs.lisp index 2a0e83e9..fda951ec 100644 --- a/oob/cancun/precompiles/modexp/xbs.lisp +++ b/oob/cancun/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-to-512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-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))) diff --git a/oob/london/precompiles/modexp/xbs.lisp b/oob/london/precompiles/modexp/xbs.lisp index 2a0e83e9..fda951ec 100644 --- a/oob/london/precompiles/modexp/xbs.lisp +++ b/oob/london/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-to-512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-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))) diff --git a/oob/prague/precompiles/modexp/xbs.lisp b/oob/prague/precompiles/modexp/xbs.lisp index 2a0e83e9..fda951ec 100644 --- a/oob/prague/precompiles/modexp/xbs.lisp +++ b/oob/prague/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-to-512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-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))) diff --git a/oob/shanghai/precompiles/modexp/xbs.lisp b/oob/shanghai/precompiles/modexp/xbs.lisp index 2a0e83e9..fda951ec 100644 --- a/oob/shanghai/precompiles/modexp/xbs.lisp +++ b/oob/shanghai/precompiles/modexp/xbs.lisp @@ -14,7 +14,7 @@ (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---comparison-to-512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comparison-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))) From 2e2d3598d730160573a724c07d0eb27a58808e4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 22 Oct 2025 23:18:09 +0200 Subject: [PATCH 5/9] ras: reflecting spec changes --- oob/osaka/precompiles/modexp/xbs.lisp | 125 ++++++++++++++------------ 1 file changed, 70 insertions(+), 55 deletions(-) diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index 47ff49fc..628961fc 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -11,6 +11,10 @@ (defconst EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE (+ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1) + + ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND 0 + ROFF___MODEXP_XBS___XBS_VS_YBS 1 + ROFF___MODEXP_XBS___XBS_ISZERO_CHECK 2 ) @@ -23,68 +27,79 @@ (defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) (defun (prc-modexp-xbs---xbs-within-bounds) (force-bin [DATA 9])) (defun (prc-modexp-xbs---xbs-out-of-bounds) (force-bin [DATA 10])) -(defun (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound) OUTGOING_RES_LO) -(defun (prc-modexp-xbs---xbs-is-GT-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound))) -(defun (prc-modexp-xbs---result-of-comparison) (next OUTGOING_RES_LO)) ;; "" - -(defconstraint prc-modexp-xbs---compare-xbs-against-EIP-7823-upper-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_PLUS_ONE - )) +;; "" -(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 +(defconstraint prc-modexp-xbs---compare-xbs-against-EIP-7823-upper-bound + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND + (prc-modexp-xbs---xbs-hi) + (prc-modexp-xbs---xbs-lo) + 0 + EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE + )) + +(defconstraint prc-modexp-xbs---compare-xbs-against-ybs + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_XBS___XBS_VS_YBS 0 (prc-modexp-xbs---xbs-lo) + 0 + (prc-modexp-xbs---ybs-lo) )) -(defconstraint additional-prc-modexp-xbs - (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (is-binary (prc-modexp-xbs---compute-max))) - -(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) - (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) - (vanishes! (prc-modexp-xbs---xbs-nonzero)) - ))) - -(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) - (begin (eq! (prc-modexp-xbs---xbs-nonzero) - (- 1 (shift OUTGOING_RES_LO 2))) - (if-zero (prc-modexp-xbs---result-of-comparison) - ;; result-of-comparison ≡ false case +(defconstraint prc-modexp-xbs---check-xbs-is-zero + (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO ROFF___MODEXP_XBS___XBS_ISZERO_CHECK + 0 + (prc-modexp-xbs---xbs-lo) + )) + + +(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))) + + + +(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---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)) + )) From f43d5d17cb7c5c59744ee4a0c11cfd587c16d9c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 22 Oct 2025 23:23:49 +0200 Subject: [PATCH 6/9] ras --- oob/osaka/precompiles/modexp/xbs.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index 628961fc..5316adfd 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -24,7 +24,7 @@ (defun (prc-modexp-xbs---ybs-lo) [DATA 3]) (defun (prc-modexp-xbs---compute-max) (force-bin [DATA 4])) (defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) +(defun (prc-modexp-xbs---xbs-nonzero) (force-bin [DATA 8])) (defun (prc-modexp-xbs---xbs-within-bounds) (force-bin [DATA 9])) (defun (prc-modexp-xbs---xbs-out-of-bounds) (force-bin [DATA 10])) ;; "" From 24e287b23831e0a8b7bc2335fb6629ad21a79511 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 23 Oct 2025 01:38:00 +0200 Subject: [PATCH 7/9] feat: MODEXP pricing instruction in the OOB module --- constants/constants.lisp | 1 + oob/osaka/precompiles/modexp/pricing.lisp | 225 ++++++++++++++++++---- 2 files changed, 184 insertions(+), 42 deletions(-) diff --git a/constants/constants.lisp b/constants/constants.lisp index 1ce16cec..7b621ca0 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -227,6 +227,7 @@ GAS_CONST_IDENTITY 15 GAS_CONST_IDENTITY_WORD 3 GAS_CONST_MODEXP 200 + GAS_CONST_MODEXP_EIP_7823 500 GAS_CONST_ECADD 150 GAS_CONST_ECMUL 6000 GAS_CONST_ECPAIRING 45000 diff --git a/oob/osaka/precompiles/modexp/pricing.lisp b/oob/osaka/precompiles/modexp/pricing.lisp index 6efc2556..f0e850db 100644 --- a/oob/osaka/precompiles/modexp/pricing.lisp +++ b/oob/osaka/precompiles/modexp/pricing.lisp @@ -7,47 +7,188 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (prc-modexp-pricing---standard-precondition) IS_MODEXP_PRICING) + +(defconst + ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK 0 + ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK 1 + ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8 2 + ROFF___MODEXP_PRICING___MAX_VS_32 3 + ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST 4 + ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST 5 + ) + + +(defun (prc-modexp-pricing---standard-precondition) (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) (defun (prc-modexp-pricing---exponent-log) [DATA 6]) -(defun (prc-modexp-pricing---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-pricing---exponent-log-is-zero) (next OUTGOING_RES_LO)) -(defun (prc-modexp-pricing---f-of-max) (* (shift OUTGOING_RES_LO 2) (shift OUTGOING_RES_LO 2))) -(defun (prc-modexp-pricing---big-quotient) (shift OUTGOING_RES_LO 3)) -(defun (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) (shift OUTGOING_RES_LO 4)) -(defun (prc-modexp-pricing---big-numerator) (if-zero (prc-modexp-pricing---exponent-log-is-zero) - (* (prc-modexp-pricing---f-of-max) (prc-modexp-pricing---exponent-log)) - (prc-modexp-pricing---f-of-max))) -(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) - (prc-modexp-pricing---big-quotient) - GAS_CONST_MODEXP)) - -(defconstraint prc-modexp-pricing---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-ISZERO 0 0 (prc---r@c))) - -(defconstraint prc-modexp-pricing---check-exponent-log-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-ISZERO 1 0 (prc-modexp-pricing---exponent-log))) - -(defconstraint prc-modexp-pricing---div-max-xbs-ybs-plus-7-by-8 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-DIV 2 - 0 - (+ (prc-modexp-pricing---max-xbs-ybs) 7) - 0 - 8)) - -(defconstraint prc-modexp-pricing---div-big-numerator-by-quaddivisor (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-DIV 3 0 (prc-modexp-pricing---big-numerator) 0 G_QUADDIVISOR)) - -(defconstraint prc-modexp-pricing---compare-big-quotient-against-GAS_CONST_MODEXP (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-LT 4 0 (prc-modexp-pricing---big-quotient) 0 GAS_CONST_MODEXP)) - -(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-LT 5 0 (prc---callee-gas) 0 (prc-modexp-pricing---precompile-cost))) - -(defconstraint prc-modexp-pricing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (begin (eq! (prc---ram-success) - (- 1 (shift OUTGOING_RES_LO 5))) - (if-zero (prc---ram-success) - (vanishes! (prc---return-gas)) - (eq! (prc---return-gas) (- (prc---callee-gas) (prc-modexp-pricing---precompile-cost)))) - (eq! (prc---r@c-nonzero) (- 1 OUTGOING_RES_LO)))) +(defun (prc-modexp-pricing---max-mbs-bbs) [DATA 7]) +;; "" + + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 0 ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + +(defconstraint prc-modexp-pricing---r@c-iszero-check + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK + 0 + (prc---r@c) + )) + +(defun (prc-modex-pricing---r@c-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK )) + + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 1 ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-pricing---check-exponent-log-is-zero + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-ISZERO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK + 0 + (prc-modexp-pricing---exponent-log) + )) + +(defun (prc-modexp-pricing---exponent-log-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK)) + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 2 ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + + + +(defconstraint prc-modexp-pricing---computing-ceiling-of-max-mbs-bbs-over-8 + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-DIV ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8 + 0 + (+ (prc-modexp-pricing---max-mbs-bbs) 7) + 0 + 8 + )) + +(defun (prc-modexp-pricing---ceiling-of-max-over-8) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8)) + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 3 ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-pricing---max-mbs-bbs-vs-32 + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_PRICING___MAX_VS_32 + 0 + WORD_SIZE + 0 + (prc-modexp-pricing---max-mbs-bbs) + )) + +(defun (prc-modexp-pricing---word-cost-dominates) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___MAX_VS_32)) +(defun (prc-modexp-pricing---f-of-max) (* (prc-modexp-pricing---ceiling-of-max-over-8) + (prc-modexp-pricing---ceiling-of-max-over-8))) +(defun (prc-modexp-pricing---multiplication-complexity) (if-zero (force-bin (prc-modexp-pricing---word-cost-dominates)) + 16 + (* 2 (prc-modexp-pricing---f-of-max)))) +(defun (prc-modexp-pricing---iteration-count-or-1) (if-zero (force-bin (prc-modexp-pricing---exponent-log-is-zero)) + (prc-modexp-pricing---exponent-log) + 1)) +(defun (prc-modexp-pricing---raw-cost) (* (prc-modexp-pricing---multiplication-complexity) + (prc-modexp-pricing---iteration-count-or-1))) + + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 4 ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + + + +(defconstraint prc-modexp-pricing---compare-raw-cost-against-GAS_CONST_MODEXP-of-EIP-7823 + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST + 0 + (prc-modexp-pricing---raw-cost) + 0 + GAS_CONST_MODEXP_EIP_7823 + )) + +(defun (prc-modexp-pricing---raw-cost-LT-min-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST))) +(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---raw-cost-LT-min-cost) + ;; raw_cost_LT_min_cost ≡ faux + (prc-modexp-pricing---raw-cost) + ;; raw_cost_LT_min_cost ≡ true + GAS_CONST_MODEXP_EIP_7823)) + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 5 ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + + + +(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (call-to-LT ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST + 0 + (prc---callee-gas) + 0 + (prc-modexp-pricing---precompile-cost) + )) + +(defun (prc-modexp-pricing---callee-gas-LT-precompile-cost) (borce-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; justifying HUB predictions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint prc-modexp-pricing---justify-hub-predictions---ram-success + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (prc---ram-success) + (- 1 (prc-modexp-pricing---callee-gas-LT-precompile-cost)) + )) + +(defconstraint prc-modexp-pricing---justify-hub-predictions---return-gas + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero (force-bin (prc---ram-success)) + ;; ram_success ≡ faux + (vanishes! (prc---return-gas)) + ;; ram_success ≡ true + (eq! (prc---return-gas) + (- (prc---callee-gas) + (prc-modexp-pricing---precompile-cost))) + )) + +(defconstraint prc-modexp-pricing---justify-hub-predictions---r@c-nonzero + (:guard (prc-modexp-pricing---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (prc---r@c-nonzero) + (- 1 (prc-modex-pricing---r@c-is-zero)) + )) From 53eaa71604af7cf28daa398996ccc8342c1da209 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 23 Oct 2025 01:51:14 +0200 Subject: [PATCH 8/9] fix: make it compile --- oob/osaka/precompiles/modexp/pricing.lisp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/oob/osaka/precompiles/modexp/pricing.lisp b/oob/osaka/precompiles/modexp/pricing.lisp index f0e850db..a15ff5e8 100644 --- a/oob/osaka/precompiles/modexp/pricing.lisp +++ b/oob/osaka/precompiles/modexp/pricing.lisp @@ -18,7 +18,7 @@ ) -(defun (prc-modexp-pricing---standard-precondition) (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) +(defun (prc-modexp-pricing---standard-precondition) (* (assumption---fresh-new-stamp) IS_MODEXP_PRICING)) (defun (prc-modexp-pricing---exponent-log) [DATA 6]) (defun (prc-modexp-pricing---max-mbs-bbs) [DATA 7]) ;; "" @@ -39,7 +39,7 @@ (prc---r@c) )) -(defun (prc-modex-pricing---r@c-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK )) +(defun (prc-modex-pricing---r@c-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK)) @@ -157,7 +157,7 @@ (prc-modexp-pricing---precompile-cost) )) -(defun (prc-modexp-pricing---callee-gas-LT-precompile-cost) (borce-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST))) +(defun (prc-modexp-pricing---callee-gas-LT-precompile-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; From b73e42302ac373df489e01f2d3e18dffc82bb871 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 23 Oct 2025 19:27:55 +0200 Subject: [PATCH 9/9] ras: "documentation" --- oob/osaka/precompiles/modexp/pricing.lisp | 60 +++++++++++------------ oob/osaka/precompiles/modexp/xbs.lisp | 38 ++++++++++++-- 2 files changed, 65 insertions(+), 33 deletions(-) diff --git a/oob/osaka/precompiles/modexp/pricing.lisp b/oob/osaka/precompiles/modexp/pricing.lisp index a15ff5e8..5dcf062f 100644 --- a/oob/osaka/precompiles/modexp/pricing.lisp +++ b/oob/osaka/precompiles/modexp/pricing.lisp @@ -25,11 +25,11 @@ -;;;;;;;;;;;;;;;;;;; -;; ;; -;; row i + 0 ;; -;; ;; -;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 0: r@c.isZero() check ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint prc-modexp-pricing---r@c-iszero-check (:guard (prc-modexp-pricing---standard-precondition)) @@ -43,11 +43,11 @@ -;;;;;;;;;;;;;;;;;;; -;; ;; -;; row i + 1 ;; -;; ;; -;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 1: exponentLog.isZero() check ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint prc-modexp-pricing---check-exponent-log-is-zero @@ -61,11 +61,11 @@ (defun (prc-modexp-pricing---exponent-log-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK)) -;;;;;;;;;;;;;;;;;;; -;; ;; -;; row i + 2 ;; -;; ;; -;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 2: ⌈ max(mbs, bbs) / 8 ⌉ compututation ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -82,11 +82,11 @@ (defun (prc-modexp-pricing---ceiling-of-max-over-8) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8)) -;;;;;;;;;;;;;;;;;;; -;; ;; -;; row i + 3 ;; -;; ;; -;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 3: comparing max(mbs, bbs) and 32 ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint prc-modexp-pricing---max-mbs-bbs-vs-32 @@ -113,11 +113,11 @@ -;;;;;;;;;;;;;;;;;;; -;; ;; -;; row i + 4 ;; -;; ;; -;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 4: comparing raw_price to 500 ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -139,11 +139,11 @@ GAS_CONST_MODEXP_EIP_7823)) -;;;;;;;;;;;;;;;;;;; -;; ;; -;; row i + 5 ;; -;; ;; -;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 5: comparing callee_gas to precopile_cost ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/oob/osaka/precompiles/modexp/xbs.lisp b/oob/osaka/precompiles/modexp/xbs.lisp index 5316adfd..a8c07fbe 100644 --- a/oob/osaka/precompiles/modexp/xbs.lisp +++ b/oob/osaka/precompiles/modexp/xbs.lisp @@ -30,7 +30,14 @@ ;; "" -(defconstraint prc-modexp-xbs---compare-xbs-against-EIP-7823-upper-bound +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 0: comparing xbs against 1024 ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---comparing-xbs-against-EIP-7823-upper-bound (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (call-to-LT ROFF___MODEXP_XBS___XBS_VS_EIP_7823_UPPER_BOUND @@ -40,7 +47,16 @@ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND_PLUS_ONE )) -(defconstraint prc-modexp-xbs---compare-xbs-against-ybs + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 1: comparing xbs against ybs ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---comparing-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (call-to-LT ROFF___MODEXP_XBS___XBS_VS_YBS @@ -50,7 +66,16 @@ (prc-modexp-xbs---ybs-lo) )) -(defconstraint prc-modexp-xbs---check-xbs-is-zero + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; row i + 2: zeroness check for xbs ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint prc-modexp-xbs---is-zero-check-for-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (call-to-ISZERO ROFF___MODEXP_XBS___XBS_ISZERO_CHECK @@ -65,6 +90,13 @@ (defun (prc-modexp-xbs---xbs-is-GT-EIP-7823-upper-bound) (- 1 (prc-modexp-xbs---xbs-is-LEQ-EIP-7823-upper-bound))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; justifying HUB predictions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + (defconstraint prc-modexp-xbs---binarity-sanity-check (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))