Added u512_divmod_by_u256.

[orizi]

Stack:

• Added get coordinates syscall for secp. #3141
• Added implementations for secp hints. #3125
• Added u512_divmod_by_u256. #3112 ⬅

⚠️ Part of a stack created by spr. Do not merge manually using the UI - doing so may have unexpected results.

---

This change is 

[yuvalsw]

Reviewed 13 of 16 files at r1, 3 of 3 files at r2, 1 of 1 files at r3, all commit messages.
Reviewable status: all files reviewed, 25 unresolved discussions (waiting on @orizi and @spapinistarkware)

---

corelib/src/integer.cairo line 1120 at r2 (raw file):

}

extern fn u512_safe_divmod_by_u256(

please doc both. For the first - mostly the return types. For the second - what it does. I also think the order should be the other way around as the user function is the interface that should be used, but I don't feel strongly about it.

---

corelib/src/test/integer_test.cairo line 708 at r2 (raw file):

#[test]
fn test_u512_safe_div_rem_by_u256() {

same as in the previous PR - I suggest to change the error messages to have != instead of ==.

---

corelib/src/test/integer_test.cairo line 721 at r2 (raw file):

    assert(r == 0, '0 % 1 == 0');
    let (q, r) = u512_safe_div_rem_by_u256(one, u256_as_non_zero(1));
    assert(q == one, '1 / 1 == 0');

Suggestion:

assert(q == one, '1 / 1 == 1');

---

crates/cairo-lang-casm/src/hints/mod.rs line 142 at r2 (raw file):

    },
    /// Divides dividend (represented by 4 128bit limbs) by divisor (represented by 2 128bit
    /// limbs). Returns the quotient (represented by 4 128bit limbs) and remainder (represented

Worth noting that limb0 is the least-significant

---

crates/cairo-lang-sierra/src/extensions/modules/int/unsigned512.rs line 19 at r2 (raw file):

define_libfunc_hierarchy! {
    pub enum Uint512Libfunc {
        DivModU256(Uint521DivmodU256Libfunc),

Suggestion:

(Uint512DivmodU256Libfunc

---

crates/cairo-lang-sierra/src/extensions/modules/int/unsigned512.rs line 54 at r2 (raw file):

                OutputVarInfo {
                    ty: guarantee_ty.clone(),
                    ref_info: OutputVarReferenceInfo::SimpleDerefs,

export to a var and clone 4 times

---

crates/cairo-lang-sierra/src/extensions/modules/int/unsigned512.rs line 76 at r2 (raw file):

/// Helper for u512 type def.
fn get_u512_type(

please move to crates/cairo-lang-sierra/src/extensions/modules/mod.rs

---

crates/cairo-lang-sierra-gas/src/core_libfunc_cost_base.rs line 556 at r2 (raw file):

fn u512_libfunc_cost(libfunc: &Uint512Concrete) -> Vec<ConstCost> {
    match libfunc {
        Uint512Concrete::DivModU256(_) => vec![ConstCost { steps: 51, holes: 0, range_checks: 14 }],

I count 15 range checks
(But as Written in another comment, I think there is one RC missing, so maybe a total of 16)

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 22 at r2 (raw file):

/// Generates casm instructions for `u512_safe_divmod_by_u256()`.
fn build_u512_divmod_by_u256(

add "safe"

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 32 at r2 (raw file):

    let mut casm_builder = CasmBuilder::default();
    add_input_variables! {casm_builder,
        buffer(16) range_check;

I count 15, so it should be 14 here.
(But as Written in another comment, I think there is one RC missing, so maybe a total of 16 and here should be 15)

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 45 at r2 (raw file):

        const one = 1;
        const i16_upper_limiter = u128::MAX - i16::MAX as u128;
        const i16_lower_limiter = -BigInt::from(i16::MIN);

Suggestion:
s/limiter/limit/

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 47 at r2 (raw file):

        const i16_lower_limiter = -BigInt::from(i16::MIN);
        const u128_bound_minus_u64_bound = u128::MAX - u64::MAX as u128;
        const u128_limit = (BigInt::from(u128::MAX) + 1) as BigInt;

I suggest consistent naming (other consistent namings are also OK)

Or another suggestion for u128_limit/u128_bound: exp128.

Suggestion:

        const u128_bound_minus_i16_upper_bound = u128::MAX - i16::MAX as u128;
        const i16_lower_bound = -BigInt::from(i16::MIN);
        const u128_bound_minus_u64_bound = u128::MAX - u64::MAX as u128;
        const u128_bound = (BigInt::from(u128::MAX) + 1) as BigInt;

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 87 at r2 (raw file):

        tempvar diff1 = divisor1 - remainder1;
        tempvar diff0 = divisor0 - remainder0;
        tempvar diff0_min_1 = diff0 - one;

compute this only after the jump

Code quote:

        tempvar diff0 = divisor0 - remainder0;
        tempvar diff0_min_1 = diff0 - one;

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 96 at r2 (raw file):

    }
    // Do basic calculations.
    casm_build_extend! {casm_builder,

Why is it divided to 3 casm_build_extends?

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 97 at r2 (raw file):

    // Do basic calculations.
    casm_build_extend! {casm_builder,
        ap += 10;

why do you need ap+= here but not in other places?

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 116 at r2 (raw file):

    casm_build_extend! {casm_builder,
        // Validating `quotient * divisor + remainder - dividend = 0`.
        // Validate limb0.

You don't assert the equality in limbs 0,1,2.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 149 at r2 (raw file):

        // We know that limb4 and limb5 are 0.
        // So we know that quotient3 or divisor1 are 0.
        // We also know that divisor1*quotient2 and divisor0*quotient3 are smaller than 2**128.

You don't know this. This is what you expect and thus it's sufficient to assert this.
Am I missing something?

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 149 at r2 (raw file):

        // We know that limb4 and limb5 are 0.
        // So we know that quotient3 or divisor1 are 0.
        // We also know that divisor1*quotient2 and divisor0*quotient3 are smaller than 2**128.

suggestion for consistency - always quotient before divisor

Suggestion:

/ We also know that quotient2*divisor1 and quotient3*divisor0 are smaller than 2**

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 154 at r2 (raw file):

        tempvar qd3_large;
        jump DIVISOR1_EQ_ZERO if quotient3 != 0;
        // quotient3 is 0 - no need to multiply it by the divisor.

I think you missed q1d1_high in that case.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 182 at r2 (raw file):

        tempvar qd3 = qd3_small * qd3_large;
        tempvar part0 = leftover + q2d0_high;
        assert dividend3 = part0 + qd3;

Are you sure this should always be true? Can't we have negative carry from the remainder?
(We need to assert qd3 = (dividend-remainder)3, which is mostly dividend3, but could be dividend3-1 with the carry from the remainder).

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 183 at r2 (raw file):

        tempvar part0 = leftover + q2d0_high;
        assert dividend3 = part0 + qd3;
    };

I think you still need to assert limb4 is 0. You did for limb5, but
limb4 = q2d1_high+q3d0_high+q3d1_low. You asserted that q3d1_low is 0, so you still need to assert that q2d1_high+q3d0_high = 0.
In the case q3 is 0, you need to assert q2d1_high = 0.
In the case d1 is 0, you need to assert q3d0_high = 0.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 178 at r3 (raw file):

        assert qd3_large = divisor0;
    MERGE:
        tempvar qd3_small_fixed = qd3_small + u128_bound_minus_u64_bound;

Don't you also need to range check qd3_small to check it's >0?

---

tests/e2e_test_data/libfuncs/u512 line 1 at r2 (raw file):

//! > u512_safe_divmod_by_u256 libfunc

change to u512_safe_div_rem_by_u256? This is the function you call

---

tests/e2e_test_data/libfuncs/u512 line 3 at r2 (raw file):

//! > u512_safe_divmod_by_u256 libfunc

//! > test_comments

remove

---

tests/e2e_test_data/libfuncs/u512 line 10 at r2 (raw file):

//! > cairo
use integer::u512;
fn foo(a: u512, b: NonZero::<u256>) -> (u512, u256) {

"::" needed?

Code quote:

 NonZero::<u256>

[orizi]

Reviewable status: all files reviewed, 15 unresolved discussions (waiting on @spapinistarkware and @yuvalsw)

---

corelib/src/integer.cairo line 1120 at r2 (raw file):

Previously, yuvalsw wrote…

please doc both. For the first - mostly the return types. For the second - what it does. I also think the order should be the other way around as the user function is the interface that should be used, but I don't feel strongly about it.

Done

---

crates/cairo-lang-sierra/src/extensions/modules/int/unsigned512.rs line 54 at r2 (raw file):

Previously, yuvalsw wrote…

export to a var and clone 4 times

not clonable - and rather not do this at this pr.

---

crates/cairo-lang-sierra/src/extensions/modules/int/unsigned512.rs line 76 at r2 (raw file):

Previously, yuvalsw wrote…

please move to crates/cairo-lang-sierra/src/extensions/modules/mod.rs

i rather do that only if and when it actually is used out of file.

---

crates/cairo-lang-sierra-gas/src/core_libfunc_cost_base.rs line 556 at r2 (raw file):

Previously, yuvalsw wrote…

I count 15 range checks
(But as Written in another comment, I think there is one RC missing, so maybe a total of 16)

it is automatically counted - you probably counted 2 branches.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 32 at r2 (raw file):

Previously, yuvalsw wrote…

I count 15, so it should be 14 here.
(But as Written in another comment, I think there is one RC missing, so maybe a total of 16 and here should be 15)

ditto

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 45 at r2 (raw file):

Previously, yuvalsw wrote…

Suggestion:
s/limiter/limit/

it isn't a limit - it is a limiter to be used by the range check.
but done with the next suggestion.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 87 at r2 (raw file):

Previously, yuvalsw wrote…

compute this only after the jump

we do not remove cost from just a single side of the branch, as it requires alignments later.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 96 at r2 (raw file):

Previously, yuvalsw wrote…

Why is it divided to 3 casm_build_extends?

just preventing max macro resolve depth. (since the macro is unwrapped recursively)

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 97 at r2 (raw file):

Previously, yuvalsw wrote…

why do you need ap+= here but not in other places?

since we allocate a lot of values filled by hints and don't have enough instructions that do not allocate variables to cover it up.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 116 at r2 (raw file):

Previously, yuvalsw wrote…

You don't assert the equality in limbs 0,1,2.

i make sure the leftover is small until the last limb - so yes i do.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 149 at r2 (raw file):

Previously, yuvalsw wrote…

You don't know this. This is what you expect and thus it's sufficient to assert this.
Am I missing something?

we know it is so for any valid calculation - so there's no need to validate it.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 154 at r2 (raw file):

Previously, yuvalsw wrote…

I think you missed q1d1_high in that case.

good catch - though i should add it to everything.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 182 at r2 (raw file):

Previously, yuvalsw wrote…

Are you sure this should always be true? Can't we have negative carry from the remainder?
(We need to assert qd3 = (dividend-remainder)3, which is mostly dividend3, but could be dividend3-1 with the carry from the remainder).

this is the final limb - we must have full equality at this step - so we may have previously had a negative carry - but it is cancelled out by this point.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 183 at r2 (raw file):

Previously, yuvalsw wrote…

I think you still need to assert limb4 is 0. You did for limb5, but
limb4 = q2d1_high+q3d0_high+q3d1_low. You asserted that q3d1_low is 0, so you still need to assert that q2d1_high+q3d0_high = 0.
In the case q3 is 0, you need to assert q2d1_high = 0.
In the case d1 is 0, you need to assert q3d0_high = 0.

since i know qd3_small * qd3_large is smaller than 192 bits - this validates that the high limb is 0 when i sum everything.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 178 at r3 (raw file):

Previously, yuvalsw wrote…

Don't you also need to range check qd3_small to check it's >0?

all was rangechecked right after the hint.

---

tests/e2e_test_data/libfuncs/u512 line 1 at r2 (raw file):

Previously, yuvalsw wrote…

change to u512_safe_div_rem_by_u256? This is the function you call

it tests that libfunc - it just carries the costs of the guarantees as well.

[yuvalsw]

Reviewed 8 of 9 files at r4, all commit messages.
Reviewable status: 15 of 16 files reviewed, 10 unresolved discussions (waiting on @orizi and @spapinistarkware)

---

corelib/src/integer.cairo line 1120 at r4 (raw file):

}

/// Calculates division and remainder of a u512 by a non-zero u256.

or "quotient and remainder".

Same below.

Suggestion:

Calculates division with remainder

---

crates/cairo-lang-sierra/src/extensions/modules/int/unsigned512.rs line 76 at r2 (raw file):

Previously, orizi wrote…

i rather do that only if and when it actually is used out of file.

I see your point, but it's a bit strange that we have the exact same function for 256 and they are in different places.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 97 at r2 (raw file):

Previously, orizi wrote…

since we allocate a lot of values filled by hints and don't have enough instructions that do not allocate variables to cover it up.

WDYM by "cover it up"?

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 154 at r2 (raw file):

Previously, orizi wrote…

good catch - though i should add it to everything.

You don't need to add it in the case d1 is zero as q1d1 would be 0.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 178 at r3 (raw file):

Previously, orizi wrote…

all was rangechecked right after the hint.

quotient2/quotient3 were rangechecked. divisor0/divisor1 (inputs) weren't. Actually I am not sure - don't we also need to range check the inputs anyway to make sure they are u128?

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 44 at r4 (raw file):

        const zero = 0;
        const one = 1;
        const u128_bound_minus_i64_upper_bound = u128::MAX - i16::MAX as u128;

Suggestion:

nst u128_bound_minus_i16_upper_bound = u128:

---

tests/e2e_test_data/libfuncs/u512 line 3 at r2 (raw file):

Previously, yuvalsw wrote…

remove

Still there.

---

tests/e2e_test_data/libfuncs/u512 line 10 at r2 (raw file):

Previously, yuvalsw wrote…

"::" needed?

Still there.

[orizi]

Reviewable status: 15 of 16 files reviewed, 7 unresolved discussions (waiting on @spapinistarkware and @yuvalsw)

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 97 at r2 (raw file):

Previously, yuvalsw wrote…

WDYM by "cover it up"?

the builder automatically uses commands that allow for ap++ but do not need it for allocating a new var to allocate space on ap without a special ap += * command.
this time we just do not have enough space.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 154 at r2 (raw file):

Previously, yuvalsw wrote…

You don't need to add it in the case d1 is zero as q1d1 would be 0.

true - but again - all optimisations that do not improve all branches are ignored.

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 178 at r3 (raw file):

Previously, yuvalsw wrote…

quotient2/quotient3 were rangechecked. divisor0/divisor1 (inputs) weren't. Actually I am not sure - don't we also need to range check the inputs anyway to make sure they are u128?

they are "range checked" due to the type system.

---

tests/e2e_test_data/libfuncs/u512 line 3 at r2 (raw file):

Previously, yuvalsw wrote…

Still there.

probably something about updating during test running.
Done

[yuvalsw]

Reviewed 4 of 4 files at r5, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @orizi and @spapinistarkware)

---

crates/cairo-lang-sierra-to-casm/src/invocations/int/unsigned512.rs line 150 at r5 (raw file):

        // So we know that quotient3 or divisor1 are 0.
        // We also know that quotient2*divisor1 and quotient3*divisor0 are smaller than 2**128.
        // Therefore the smaller of each pair must be smaller than 2**64, and if we check this we can avoid wraparound on the prime.

Suggestion:

        // We know that limb4 and limb5 should be 0.
        // Therfore quotient3 or divisor1 should also be 0.
        // We also know that quotient2*divisor1 and quotient3*divisor0 should be smaller than 2**128.
        // Therefore the smaller of each pair must be smaller than 2**64.
        // So by checking this we can avoid wraparound on the prime.

[orizi]

Reviewed 1 of 1 files at r6, all commit messages.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @spapinistarkware)