From 688306098cc434874559fb9f2f5bfb5a3903f094 Mon Sep 17 00:00:00 2001 From: MaksymMalicki Date: Thu, 23 Jan 2025 19:37:08 +0100 Subject: [PATCH] Implement inline casm for segment arena --- integration_tests/.env | 2 +- .../proofmode_segment_arena__small.cairo | 45 ++++++++++++++++++ .../proofmode_with_builtins__small.cairo | 47 +++++++++++++++++++ integration_tests/cairo_vm_test.go | 14 +++--- pkg/runner/runner.go | 30 +++++++++--- 5 files changed, 125 insertions(+), 13 deletions(-) create mode 100644 integration_tests/cairo_1_programs/with_input/proofmode_segment_arena__small.cairo create mode 100644 integration_tests/cairo_1_programs/with_input/proofmode_with_builtins__small.cairo diff --git a/integration_tests/.env b/integration_tests/.env index 8c90ed93f..5448ff22e 100644 --- a/integration_tests/.env +++ b/integration_tests/.env @@ -1,2 +1,2 @@ # Set to run some specific file tests (ex. fib.cairo,alloc.cairo) -INTEGRATION_TESTS_FILTERS=proofmode__small.cairo \ No newline at end of file +INTEGRATION_TESTS_FILTERS= \ No newline at end of file diff --git a/integration_tests/cairo_1_programs/with_input/proofmode_segment_arena__small.cairo b/integration_tests/cairo_1_programs/with_input/proofmode_segment_arena__small.cairo new file mode 100644 index 000000000..6c7ea1e2b --- /dev/null +++ b/integration_tests/cairo_1_programs/with_input/proofmode_segment_arena__small.cairo @@ -0,0 +1,45 @@ +use array::ArrayTrait; +use array::SpanTrait; +use dict::Felt252DictTrait; +use pedersen::PedersenTrait; + +fn main(mut vals: Array) -> Array { + // Create a dictionary using segment arena + let mut dict = felt252_dict_new::(); + + // Store each value in the dictionary with its index + let mut index: felt252 = 0; + loop { + match vals.pop_front() { + Option::Some(v) => { + dict.insert(index, v); + index += 1; + }, + Option::None(_) => { + break; + } + }; + }; + + // Create result array + let mut res: Array = ArrayTrait::new(); + + // Read values back from dictionary and hash them + let mut i: felt252 = 0; + loop { + let i_u128: u128 = i.try_into().unwrap(); + let index_u128: u128 = index.try_into().unwrap(); + + if i_u128 >= index_u128 { + break; + } + + let value = dict.get(i); + let hash = pedersen::pedersen(value, i); + res.append(hash); + + i += 1; + }; + + res +} \ No newline at end of file diff --git a/integration_tests/cairo_1_programs/with_input/proofmode_with_builtins__small.cairo b/integration_tests/cairo_1_programs/with_input/proofmode_with_builtins__small.cairo new file mode 100644 index 000000000..f61d484ff --- /dev/null +++ b/integration_tests/cairo_1_programs/with_input/proofmode_with_builtins__small.cairo @@ -0,0 +1,47 @@ +use array::ArrayTrait; +use array::SpanTrait; +use pedersen::PedersenTrait; +use core::num::traits::Bounded; + +fn check_and_sum(mut vals: Array) -> felt252 { + let mut sum: felt252 = 0; + let upper_bound: u128 = 1000000; // Example bound + + loop { + match vals.pop_front() { + Option::Some(v) => { + // Convert felt252 to u128 for range check + let v_u128: u128 = v.try_into().unwrap(); + // This will ensure v is non-negative and within u128 bounds + assert(v_u128 <= upper_bound, 'Value exceeds bound'); + + sum += v; + }, + Option::None(_) => { + break sum; + } + }; + } +} + +fn main(mut vals: Array) -> Array { + // Calculate sum with range checks + let sum = check_and_sum(vals); + + // Hash the sum using Pedersen + let hash = pedersen::pedersen(sum, 0); + + // Create result array + let mut res: Array = ArrayTrait::new(); + + // Add original sum + res.append(sum); + // Add hash of sum + res.append(hash); + + // Add a u128 conversion to demonstrate more range checks + let sum_u128: u128 = sum.try_into().unwrap(); + res.append(sum_u128.into()); + + res +} \ No newline at end of file diff --git a/integration_tests/cairo_vm_test.go b/integration_tests/cairo_vm_test.go index eca3f1bfe..e79f47f92 100644 --- a/integration_tests/cairo_vm_test.go +++ b/integration_tests/cairo_vm_test.go @@ -187,12 +187,14 @@ func TestCairoFiles(t *testing.T) { } inputArgsMap := map[string]string{ - "cairo_1_programs/with_input/array_input_sum__small.cairo": "2 [111 222 333] 1 [444 555 666 777]", - "cairo_1_programs/with_input/array_length__small.cairo": "[1 2 3 4 5 6] [7 8 9 10]", - "cairo_1_programs/with_input/branching.cairo": "123", - "cairo_1_programs/with_input/dict_with_input__small.cairo": "[1 2 3 4]", - "cairo_1_programs/with_input/tensor__small.cairo": "[1 4] [1 5]", - "cairo_1_programs/with_input/proofmode__small.cairo": "[1 2 3 4 5]", + "cairo_1_programs/with_input/array_input_sum__small.cairo": "2 [111 222 333] 1 [444 555 666 777]", + "cairo_1_programs/with_input/array_length__small.cairo": "[1 2 3 4 5 6] [7 8 9 10]", + "cairo_1_programs/with_input/branching.cairo": "123", + "cairo_1_programs/with_input/dict_with_input__small.cairo": "[1 2 3 4]", + "cairo_1_programs/with_input/tensor__small.cairo": "[1 4] [1 5]", + "cairo_1_programs/with_input/proofmode__small.cairo": "[1 2 3 4 5]", + "cairo_1_programs/with_input/proofmode_with_builtins__small.cairo": "[1 2 3 4 5]", + "cairo_1_programs/with_input/proofmode_segment_arena__small.cairo": "[1 2 3 4 5]", } // filter is for debugging purposes diff --git a/pkg/runner/runner.go b/pkg/runner/runner.go index 82f082dc3..22b322a3e 100644 --- a/pkg/runner/runner.go +++ b/pkg/runner/runner.go @@ -661,7 +661,8 @@ func GetEntryCodeInstructions(function starknet.EntryPointByFunction, proofmode for i, b := range function.Builtins { // assert [fp + i] == [fp - builtin_offset] offset := builtinsOffsetsMap[b] - ctx.AddInlineCASM(fmt.Sprintf("[fp+%d] = [ap-%d];", i, offset)) + // increment the offset by 1 to account for the skipped output builtin + ctx.AddInlineCASM(fmt.Sprintf("[fp+%d] = [ap-%d];", i+1, offset)) } outputs := []string{} @@ -709,7 +710,7 @@ func GetEntryCodeInstructions(function starknet.EntryPointByFunction, proofmode ctx.AddInlineCASM( fmt.Sprintf(` - [%s] = [ap] + %s, ap++; + %s = [ap] + %s, ap++; [ap-1] = [[ap-2]]; [ap] = [ap-1], ap++; [ap] = %s, ap++; @@ -719,9 +720,9 @@ func GetEntryCodeInstructions(function starknet.EntryPointByFunction, proofmode [ap] = [[ap-2]], ap++; [ap-1] = [[ap-2]]; - [ap-4] = [ap] + 1, ap++; - [ap] = [ap-4] + 1, ap++; - [ap] = [ap-4] + 1; + [ap-4] = [ap]+1, ap++; + [ap] = [ap-4]+1, ap++; + [ap] = [ap-4]+1; jmp rel -8 if [ap-3] != 0; `, arrayEndPtr, arrayStartPtr, arrayStartPtr), ) @@ -733,7 +734,24 @@ func GetEntryCodeInstructions(function starknet.EntryPointByFunction, proofmode if gotSegmentArena { offset := 2 + len(function.Builtins) segmentArenaPtr := fmt.Sprintf("[fp + %d]", offset) - fmt.Println(segmentArenaPtr) + ctx.AddInlineCASM(fmt.Sprintf(` + [ap]=[%s-2], ap++; + [ap]=[%s-1], ap++; + [ap-1]=[ap-2]; + jmp rel 4 if [ap-2] != 0; + jpm rel 19; + [ap]=[[%s-3], ap++; + [ap-3] = [ap]+1; + jmp rel 4 if [ap-1] != 0; + jmp rel 12; + [ap]=[[ap-2]+1], ap++; + [ap] = [[ap-3]+3], ap++; + [ap-1] = [ap-2] + 1; + [ap] = [ap-4] + 3, ap++; + [ap-4] = [ap] + 1, ap++; + jmp rel -12; + `, segmentArenaPtr, segmentArenaPtr, segmentArenaPtr, + )) } // Copying the final builtins from locals into the top of the stack.