Assert 250 Bits and SPLIT_FELT (#233)

* [WIP] Assert 250 Bits and SPLIT_FELT

* Add tests for ASSERT_250_BIT

* Implement SPLIT_FELT

* Add tests for SPLIT_FELT

* Incorporate the GetConst function

* Skip checking for the common library path first

* Remove redundant nil check

cairo_programs/assert_250_bit_element_array.cairo

@@ -0,0 +1,31 @@
+%builtins range_check
+
+from starkware.cairo.common.math import assert_250_bit
+from starkware.cairo.common.alloc import alloc
+
+func assert_250_bit_element_array{range_check_ptr: felt}(
+    array: felt*, array_length: felt, iterator: felt
+) {
+    if (iterator == array_length) {
+        return ();
+    }
+    assert_250_bit(array[iterator]);
+    return assert_250_bit_element_array(array, array_length, iterator + 1);
+}
+
+func fill_array(array: felt*, base: felt, step: felt, array_length: felt, iterator: felt) {
+    if (iterator == array_length) {
+        return ();
+    }
+    assert array[iterator] = base + step * iterator;
+    return fill_array(array, base, step, array_length, iterator + 1);
+}
+
+func main{range_check_ptr: felt}() {
+    alloc_locals;
+    tempvar array_length = 10;
+    let (array: felt*) = alloc();
+    fill_array(array, 70000000000000000000, 300000000000000000, array_length, 0);
+    assert_250_bit_element_array(array, array_length, 0);
+    return ();
+}

cairo_programs/split_felt.cairo

@@ -0,0 +1,42 @@
+%builtins range_check
+
+from starkware.cairo.common.math import assert_le
+from starkware.cairo.common.math import split_felt
+
+func split_felt_manual_implemetation{range_check_ptr}(value) -> (high: felt, low: felt) {
+    // Note: the following code works because PRIME - 1 is divisible by 2**128.
+    const MAX_HIGH = (-1) / 2 ** 128;
+    const MAX_LOW = 0;
+
+    // Guess the low and high parts of the integer.
+    let low = [range_check_ptr];
+    let high = [range_check_ptr + 1];
+    let range_check_ptr = range_check_ptr + 2;
+
+    %{
+        from starkware.cairo.common.math_utils import assert_integer
+        assert ids.MAX_HIGH < 2**128 and ids.MAX_LOW < 2**128
+        assert PRIME - 1 == ids.MAX_HIGH * 2**128 + ids.MAX_LOW
+        assert_integer(ids.value)
+        ids.low = ids.value & ((1 << 128) - 1)
+        ids.high = ids.value >> 128
+    %}
+
+    assert value = high * (2 ** 128) + low;
+    if (high == MAX_HIGH) {
+        assert_le(low, MAX_LOW);
+    } else {
+        assert_le(high, MAX_HIGH - 1);
+    }
+    return (high=high, low=low);
+}
+
+func main{range_check_ptr: felt}() {
+    let (m, n) = split_felt_manual_implemetation(5784800237655953878877368326340059594760);
+    assert m = 17;
+    assert n = 8;
+    let (x, y) = split_felt(5784800237655953878877368326340059594760);
+    assert x = 17;
+    assert y = 8;
+    return ();
+}

pkg/hints/hint_codes/math_hint_codes.go

@@ -18,3 +18,7 @@ else:
 const ASSERT_NOT_EQUAL = "from starkware.cairo.lang.vm.relocatable import RelocatableValue\nboth_ints = isinstance(ids.a, int) and isinstance(ids.b, int)\nboth_relocatable = (\n    isinstance(ids.a, RelocatableValue) and isinstance(ids.b, RelocatableValue) and\n    ids.a.segment_index == ids.b.segment_index)\nassert both_ints or both_relocatable, \\\n    f'assert_not_equal failed: non-comparable values: {ids.a}, {ids.b}.'\nassert (ids.a - ids.b) % PRIME != 0, f'assert_not_equal failed: {ids.a} = {ids.b}.'"
 
 const SQRT = "from starkware.python.math_utils import isqrt\nvalue = ids.value % PRIME\nassert value < 2 ** 250, f\"value={value} is outside of the range [0, 2**250).\"\nassert 2 ** 250 < PRIME\nids.root = isqrt(value)"
+
+const ASSERT_250_BITS = "from starkware.cairo.common.math_utils import as_int\n\n# Correctness check.\nvalue = as_int(ids.value, PRIME) % PRIME\nassert value < ids.UPPER_BOUND, f'{value} is outside of the range [0, 2**250).'\n\n# Calculation for the assertion.\nids.high, ids.low = divmod(ids.value, ids.SHIFT)"
+
+const SPLIT_FELT = "from starkware.cairo.common.math_utils import assert_integer\nassert ids.MAX_HIGH < 2**128 and ids.MAX_LOW < 2**128\nassert PRIME - 1 == ids.MAX_HIGH * 2**128 + ids.MAX_LOW\nassert_integer(ids.value)\nids.low = ids.value & ((1 << 128) - 1)\nids.high = ids.value >> 128"

pkg/hints/hint_processor.go

@@ -74,6 +74,10 @@ func (p *CairoVmHintProcessor) ExecuteHint(vm *vm.VirtualMachine, hintData *any,
 		return memcpy_enter_scope(data.Ids, vm, execScopes)
 	case VM_ENTER_SCOPE:
 		return vm_enter_scope(execScopes)
+	case ASSERT_250_BITS:
+		return Assert250Bit(data.Ids, vm, constants)
+	case SPLIT_FELT:
+		return SplitFelt(data.Ids, vm, constants)
 	default:
 		return errors.Errorf("Unknown Hint: %s", data.Code)
 	}

pkg/hints/math_hints.go

@@ -151,3 +151,99 @@ func sqrt(ids IdsManager, vm *VirtualMachine) error {
 	ids.Insert("root", NewMaybeRelocatableFelt(root_felt), vm)
 	return nil
 }
+
+// Implements hint:
+//
+//	from starkware.cairo.common.math_utils import as_int
+//	# Correctness check.
+//	value = as_int(ids.value, PRIME) % PRIME
+//	assert value < ids.UPPER_BOUND, f'{value} is outside of the range [0, 2**250).'
+//	# Calculation for the assertion.
+//	ids.high, ids.low = divmod(ids.value, ids.SHIFT)
+func Assert250Bit(ids IdsManager, vm *VirtualMachine, constants *map[string]Felt) error {
+	upperBound, err := ids.GetConst("UPPER_BOUND", constants)
+	if err != nil {
+		return err
+	}
+
+	shift, err := ids.GetConst("SHIFT", constants)
+	if err != nil {
+		return err
+	}
+
+	value, err := ids.GetFelt("value", vm)
+
+	if err != nil {
+		return err
+	}
+
+	if Felt.Cmp(value, upperBound) == 1 {
+		return errors.New("Value outside of 250 bit Range")
+	}
+
+	high, low := value.DivRem(shift)
+
+	err = ids.Insert("high", NewMaybeRelocatableFelt(high), vm)
+	if err != nil {
+		return err
+	}
+
+	err = ids.Insert("low", NewMaybeRelocatableFelt(low), vm)
+	if err != nil {
+		return err
+	}
+
+	return nil
+}
+
+// Implements hint:
+//
+//	%{
+//	    from starkware.cairo.common.math_utils import assert_integer
+//	    assert ids.MAX_HIGH < 2**128 and ids.MAX_LOW < 2**128
+//	    assert PRIME - 1 == ids.MAX_HIGH * 2**128 + ids.MAX_LOW
+//	    assert_integer(ids.value)
+//	    ids.low = ids.value & ((1 << 128) - 1)
+//	    ids.high = ids.value >> 128
+//
+// %}
+func SplitFelt(ids IdsManager, vm *VirtualMachine, constants *map[string]Felt) error {
+	maxHigh, err := ids.GetConst("MAX_HIGH", constants)
+	if err != nil {
+		return err
+	}
+
+	maxLow, err := ids.GetConst("MAX_LOW", constants)
+	if err != nil {
+		return err
+	}
+
+	if maxHigh.Bits() > 128 || maxLow.Bits() > 128 {
+		return errors.New("Assertion Failed: assert ids.MAX_HIGH < 2**128 and ids.MAX_LOW < 2**128")
+	}
+
+	twoToTheOneTwentyEight := lambdaworks.FeltOne().Shl(128)
+	if lambdaworks.FeltFromDecString("-1") != maxHigh.Mul(twoToTheOneTwentyEight).Add(maxLow) {
+		return errors.New("Assertion Failed: assert PRIME - 1 == ids.MAX_HIGH * 2**128 + ids.MAX_LOW")
+	}
+
+	value, err := ids.GetFelt("value", vm)
+	if err != nil {
+		return err
+	}
+
+	low := value.And(twoToTheOneTwentyEight.Sub(lambdaworks.FeltOne()))
+	high := value.Shr(128)
+
+	err = ids.Insert("high", NewMaybeRelocatableFelt(high), vm)
+	if err != nil {
+		return err
+	}
+
+	err = ids.Insert("low", NewMaybeRelocatableFelt(low), vm)
+	if err != nil {
+		return err
+	}
+
+	return nil
+}