fix

HerodotusDev · Jun 8, 2024 · 58ff77b · 58ff77b
1 parent a29acce
commit 58ff77b
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 78 deletions.
diff --git a/src/air/layouts/recursive/public_input.cairo b/src/air/layouts/recursive/public_input.cairo
@@ -1,3 +1,5 @@
+use core::array::SpanTrait;
+use core::array::ArrayTrait;
 use cairo_verifier::{
     common::{
         math::{pow, Felt252PartialOrd, Felt252Div},
@@ -23,93 +25,32 @@ impl RecursivePublicInputImpl of PublicInputTrait {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
-        let final_pc = *public_segments.at(segments::PROGRAM).stop_ptr;
         let initial_ap = *public_segments.at(segments::EXECUTION).begin_addr;
-        let initial_fp = initial_ap;
         let final_ap = *public_segments.at(segments::EXECUTION).stop_ptr;
         let output_start = *public_segments.at(segments::OUTPUT).begin_addr;
         let output_stop = *public_segments.at(segments::OUTPUT).stop_ptr;
 
+        let output_len: u32 = (output_stop - output_start).try_into().unwrap();
+
         assert(initial_ap < MAX_ADDRESS, 'Invalid initial_ap');
         assert(final_ap < MAX_ADDRESS, 'Invalid final_ap');
 
-        // TODO support more pages?
         assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers');
 
-        let builtins = get_builtins();
-        let memory = self.main_page;
+        let public_memory = self.main_page;
 
         // 1. Program segment
         assert(initial_pc == INITIAL_PC, 'Invalid initial_pc');
-        assert(final_pc == INITIAL_PC + 4, 'Invalid final_pc');
-
-        let mut memory_index: usize = 0;
 
-        let program_end_pc = initial_fp - 2;
-        let program_len = program_end_pc - initial_pc;
-        let program = memory
-            .extract_range(
-                initial_pc.try_into().unwrap(), program_len.try_into().unwrap(), ref memory_index
-            );
+        let program = public_memory
+            .extract_range(initial_pc.try_into().unwrap(), public_memory.len() - output_len);
 
-        assert(
-            *program[0] == 0x40780017fff7fff, 'Invalid program'
-        ); // Instruction: ap += N_BUILTINS.
-        assert(*program[1] == builtins.len().into(), 'Invalid program');
-        assert(*program[2] == 0x1104800180018000, 'Invalid program'); // Instruction: call rel ?.
-        assert(*program[4] == 0x10780017fff7fff, 'Invalid program'); // Instruction: jmp rel 0.
-        assert(*program[5] == 0x0, 'Invalid program');
-
-        let program_hash = poseidon_hash_span(program);
-
-        // 2. Execution segment
-        // 2.1 Initial_fp, initial_pc
-        let fp2 = *memory.at(memory_index);
-        assert(fp2.address == initial_fp - 2, 'Invalid fp2 addr');
-        assert(fp2.value == initial_fp, 'Invalid fp2 val');
-
-        let fp1 = *memory.at(memory_index + 1);
-        assert(fp1.address == initial_fp - 1, 'Invalid fp1 addr');
-        assert(fp1.value == 0, 'Invalid fp1 val');
-        memory_index += 2;
-
-        // 2.2 Main arguments and return values
-        let mut begin_addresses = ArrayTrait::new();
-        let mut stop_addresses = ArrayTrait::new();
-        let mut i = 0;
-        let builtins_len = builtins.len();
-        loop {
-            if i == builtins_len {
-                break;
-            }
-
-            begin_addresses.append(*public_segments.at(2 + i).begin_addr);
-            stop_addresses.append(*public_segments.at(2 + i).stop_ptr);
-
-            i += 1;
-        };
-        memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index);
-        memory
-            .verify_stack(
-                final_ap - builtins_len.into(),
-                stop_addresses.span(),
-                builtins_len,
-                ref memory_index
-            );
+        let program_hash = poseidon_hash_span(program.span());
 
         // 3. Output segment 
-        let output_len = output_stop - output_start;
-        let output = memory
-            .extract_range(
-                output_start.try_into().unwrap(), output_len.try_into().unwrap(), ref memory_index
-            );
-        let output_hash = poseidon_hash_span(output);
-
-        // Check main page len
-        assert(
-            *memory.at(memory_index - 1) == *self.main_page.at(self.main_page.len() - 1),
-            'Invalid main page len'
-        );
+        let output_len: u32 = (output_stop - output_start).try_into().unwrap();
+        let output = public_memory.extract_range(public_memory.len() - output_len, output_len);
+        let output_hash = poseidon_hash_span(output.span());
 
         (program_hash, output_hash)
     }

diff --git a/src/air/public_memory.cairo b/src/air/public_memory.cairo
@@ -45,23 +45,21 @@ impl PageImpl of PageTrait {
         }
     }
 
-    fn extract_range(self: @Page, addr: u32, len: usize, ref offset: usize) -> Span<felt252> {
+    fn extract_range(self: @Page, start: u32, len: usize) -> Array<felt252> {
         let mut arr = ArrayTrait::new();
         let mut i = 0;
 
         loop {
             if i == len {
-                break arr.span();
+                break;
             }
 
-            let current = *self.at(offset);
-
-            // TODO is this needed? If not we can just use slice directly 
-            assert(current.address == (addr + i).into(), 'Invalid address');
+            let current = *self.at(start + i);
             arr.append(current.value);
             i += 1;
-            offset += 1;
-        }
+        };
+
+        arr
     }
 
     fn verify_stack(