Implement SPLIT_FELT

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_processor.go

@@ -71,6 +71,8 @@ func (p *CairoVmHintProcessor) ExecuteHint(vm *vm.VirtualMachine, hintData *any,
 		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_hint_codes.go

@@ -20,3 +20,5 @@ const ASSERT_NOT_EQUAL = "from starkware.cairo.lang.vm.relocatable import Reloca
 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/math_hints.go

@@ -202,8 +202,67 @@ func Assert250Bit(ids IdsManager, vm *VirtualMachine, constants *map[string]Felt
 
 	high, low := value.DivRem(shift)
 
-	ids.Insert("high", NewMaybeRelocatableFelt(high), vm)
-	ids.Insert("low", NewMaybeRelocatableFelt(low), vm)
+	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 := GetConstantFromVarName("MAX_HIGH", constants)
+	if err != nil {
+		return err
+	}
+
+	maxLow, err := GetConstantFromVarName("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
 }

pkg/lambdaworks/lib/lambdaworks/src/lib.rs

@@ -257,7 +257,7 @@ pub unsafe extern "C" fn free_string(ptr: *mut c_char) {
 pub extern "C" fn felt_shr(a: Limbs, b: usize, result: Limbs) {
     let felt_a = limbs_to_felt(a).representative();
 
-    let res = felt_a << b;
+    let res = felt_a >> b;
 
     felt_to_limbs(Felt::from(&res), result)
 }

pkg/vm/cairo_run/cairo_run_test.go

@@ -210,3 +210,11 @@ func TestAssert250BitHint(t *testing.T) {
 		t.Errorf("Program execution failed with error: %s", err)
 	}
 }
+
+func TestSplitFeltHint(t *testing.T) {
+	cairoRunConfig := cairo_run.CairoRunConfig{DisableTracePadding: false, Layout: "all_cairo", ProofMode: false}
+	_, err := cairo_run.CairoRun("../../../cairo_programs/split_felt.json", cairoRunConfig)
+	if err != nil {
+		t.Errorf("Program execution failed with error: %s", err)
+	}
+}