feat: modexp precompile 384 bits #1513

tekkac · 2024-10-19T11:18:12Z

Time spent on this PR:

Pull request type

Please check the type of change your PR introduces:

What is the current behavior?

Running 8 test(s) from src/
[PASS] evm::precompiles::modexp::tests::test_modexp_berlin_empty_input (gas: ~133)
[PASS] evm::precompiles::modexp::tests::test_modexp_eip198_example_1 (gas: ~635)
[PASS] evm::precompiles::modexp::tests::test_modexp_circuit (gas: ~544)
[PASS] evm::precompiles::modexp::tests::test_modexp_edge_case_circuit (gas: ~9)
[PASS] evm::precompiles::modexp::tests::test_modexp_eip198_example_2 (gas: ~312)
[PASS] evm::precompiles::modexp::tests::test_modexp_precompile_input_output_worst (gas: ~953)
[PASS] evm::precompiles::modexp::tests::test_modexp_circuit_worst_case (gas: ~953)
[PASS] evm::precompiles::modexp::tests::test_modexp_precompile_input_output_all_sizes (gas: ~22497)

Resolves #1496

What is the new behavior?

modexp precompiled implemented with circuit up to 384 bits (48 bytes)
passes basic tests and some EIP test vectors
Custom input output needed because of non-standard integer types from circuits.

This change is

ClementWalter · 2024-10-21T08:37:07Z

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

why are some tests commented?

Those tests won't pass as the scope of the issue is to impl modexp for up to 384 bits.
I kept the tests code for reference, let me know how best to handle it.

enitrat · 2024-10-21T15:29:38Z

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

@@ -88,18 +87,158 @@ pub impl ModExp of Precompile {
        let gas = calc_gas(base_len.into(), exp_len.into(), mod_len.into(), exp_highp);

        // Padding is needed if the input does not contain all 3 values.
-        let base = input.slice_right_padded(0, base_len);
-        let exponent = input.slice_right_padded(base_len, exp_len);
-
        let (mod_start_idx, _) = base_len.overflowing_add(exp_len);


note (for us): this should probably not be overflowing_add here. if base_len + exp_len > u32 there's something wrong in the input (which will lead to an OOG prior to that anyway)

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

enitrat

great :)

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

enitrat · 2024-10-21T15:36:09Z

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

+    let mut s_limb0: u128 = Into::<_, felt252>::into(s.limb0).try_into().unwrap();
+    while s_limb0 != 0 {
+        let (q, r) = core::traits::DivRem::div_rem(s_limb0, 2);
+        bits.append(r.into());
+        s_limb0 = q;
+    };
+    let mut s_limb1: u128 = Into::<_, felt252>::into(s.limb1).try_into().unwrap();
+    if s_limb1 != 0 {
+        while bits.len() != 96 {
+            bits.append(0);
+        }
+    }
+    while s_limb1 != 0 {
+        let (q, r) = core::traits::DivRem::div_rem(s_limb1, 2);
+        bits.append(r.into());
+        s_limb1 = q;
+    };
+    let mut s_limb2: u128 = Into::<_, felt252>::into(s.limb2).try_into().unwrap();
+    if s_limb2 != 0 {
+        while bits.len() != 192 {
+            bits.append(0);
+        }
+    }
+    while s_limb2 != 0 {
+        let (q, r) = core::traits::DivRem::div_rem(s_limb2, 2);
+        bits.append(r.into());
+        s_limb2 = q;
+    };
+    let mut s_limb3: u128 = Into::<_, felt252>::into(s.limb3).try_into().unwrap();
+    if s_limb3 != 0 {
+        while bits.len() != 288 {
+            bits.append(0);
+        }
+    }
+    while s_limb3 != 0 {
+        let (q, r) = core::traits::DivRem::div_rem(s_limb3, 2);
+        bits.append(r.into());
+        s_limb3 = q;
+    };


We should use https://github.com/tekkac/kakarot/blob/be550c5812338e8fa727be51efc480b1b6b403e4/cairo/kakarot-ssj/crates/utils/src/traits/integer.cairo#L153-L167

There's an generic impl BitsUsedImpl. Perhaps it can be used directly; otherwise, we can implement the missing traits for the limb type (u96)

I can try again, the main issue is that only TryInto felt252 is impl'd for u96.

Tried again without success, libfuncs are missing for u96

enitrat · 2024-10-21T15:51:02Z

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

+impl U8SpanTryIntoU384 of TryInto<Span<u8>, u384> {
+    fn try_into(self: Span<u8>) -> Option<u384> {
+        if self.len() != 48 {
+            return Option::None;
+        }
+        let limb3_128: u128 = self.slice(0, 12).pad_left_with_zeroes(16).from_be_bytes().unwrap();
+        let limb2_128: u128 = self.slice(12, 12).pad_left_with_zeroes(16).from_be_bytes().unwrap();
+        let limb1_128: u128 = self.slice(24, 12).pad_left_with_zeroes(16).from_be_bytes().unwrap();
+        let limb0_128: u128 = self.slice(36, 12).pad_left_with_zeroes(16).from_be_bytes().unwrap();
+        let limb0: u96 = Into::<_, felt252>::into(limb0_128).try_into().unwrap();
+        let limb1: u96 = Into::<_, felt252>::into(limb1_128).try_into().unwrap();
+        let limb2: u96 = Into::<_, felt252>::into(limb2_128).try_into().unwrap();
+        let limb3: u96 = Into::<_, felt252>::into(limb3_128).try_into().unwrap();
+        Option::Some(u384 { limb0, limb1, limb2, limb3 })
+    }
+}



nit: this should probably be https://github.com/tekkac/kakarot/blob/be550c5812338e8fa727be51efc480b1b6b403e4/cairo/kakarot-ssj/crates/utils/src/traits/bytes.cairo#L326-L367

obatirou · 2024-10-22T08:03:12Z

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo

-        Result::Ok((gas.into(), return_data))
+// Compute the modular exponentiation
+// x^y mod n
+pub fn modexp_circuit(x: u384, y: u384, n: u384) -> u384 {


Please explain the algorithm in high level + add resources to get up to speed in docstring.
For example (and from my understanding of your implementation) this one: Repeated square-and-multiply algorithm for exponentiation
from Handbook of Applied Cryptography - Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone (Algo 2.143)
Feel free to put the resource you used.
Explain the implementation details where necessary for example the exponent is taken in little endian to process bits from LSB to MSB
This algo/implementation is not trivial and other devs (or future auditors) need context.

Let me know if the docstring is correct and sufficiently explicit

Doesn't it miss the check Assert :: (modulus - 1) * (modulus - 1) does not overflow base in the implementation ?

It's not needed in our case since the circuit already does all the operations with modular arithmetic.

tekkac added 3 commits October 19, 2024 13:11

🔥 remove old version

59f12ef

🧪 add test data visibility

8a01b32

✨ circuit implementation of modexp + test cases

be550c5

ClementWalter reviewed Oct 21, 2024

View reviewed changes

enitrat reviewed Oct 21, 2024

View reviewed changes

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo Outdated Show resolved Hide resolved

enitrat reviewed Oct 21, 2024

View reviewed changes

cairo/kakarot-ssj/crates/evm/src/precompiles/modexp.cairo Outdated Show resolved Hide resolved

enitrat reviewed Oct 21, 2024

View reviewed changes

obatirou reviewed Oct 22, 2024

View reviewed changes

tekkac added 2 commits October 23, 2024 20:45

🩹 fix edge case + comments

d13f960

🧪 fix test and remove unused imports

834f946

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: modexp precompile 384 bits #1513

feat: modexp precompile 384 bits #1513

tekkac commented Oct 19, 2024 •

edited

Loading

ClementWalter Oct 21, 2024

tekkac Oct 21, 2024

enitrat Oct 21, 2024

enitrat left a comment

enitrat Oct 21, 2024

tekkac Oct 22, 2024

tekkac Oct 23, 2024

enitrat Oct 21, 2024

obatirou Oct 22, 2024 •

edited

Loading

tekkac Oct 23, 2024

obatirou Oct 25, 2024 •

edited

Loading

tekkac Oct 25, 2024

feat: modexp precompile 384 bits #1513

Are you sure you want to change the base?

feat: modexp precompile 384 bits #1513

Conversation

tekkac commented Oct 19, 2024 • edited Loading

Pull request type

What is the current behavior?

What is the new behavior?

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

enitrat left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

obatirou Oct 22, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

obatirou Oct 25, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tekkac commented Oct 19, 2024 •

edited

Loading

obatirou Oct 22, 2024 •

edited

Loading

obatirou Oct 25, 2024 •

edited

Loading