Review comments

HerodotusDev · Jun 10, 2024 · 2de105b · 2de105b
1 parent c8df4a2
commit 2de105b
Show file tree

Hide file tree

Showing 12 changed files with 136 additions and 80 deletions.
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -18,4 +18,7 @@ jobs:
         run: scarb fmt --check
 
       - name: Run tests
-        run: scarb test
+        run: scarb test
+
+      - name: Build fact registry
+        run: (cd fact_registry && scarb build)
diff --git a/fact_registry/src/verifier.cairo b/fact_registry/src/verifier.cairo
@@ -39,7 +39,10 @@ mod CairoVerifier {
             cairo_version: CairoVersion
         ) -> (felt252, felt252) {
             stark_proof.verify(SECURITY_BITS);
-            let (program_hash, output_hash) = stark_proof.public_input.verify(cairo_version);
+            let (program_hash, output_hash) = match cairo_version {
+                CairoVersion::Cairo0 => stark_proof.public_input.verify_cairo0(),
+                CairoVersion::Cairo1 => stark_proof.public_input.verify_cairo1(),
+            };
             self.emit(ProofVerified { program_hash, output_hash });
             (program_hash, output_hash)
         }

diff --git a/runner/src/main.rs b/runner/src/main.rs
@@ -59,13 +59,9 @@ fn main() -> anyhow::Result<()> {
     let func = runner.find_function(function).unwrap();
     let proof_arg = Arg::Array(proof.into_iter().map(Arg::Value).collect_vec());
     let cairo_version_arg = Arg::Value(cli.cairo_version.into());
+    let args = &[proof_arg, cairo_version_arg];
     let result = runner
-        .run_function_with_starknet_context(
-            func,
-            &[proof_arg, cairo_version_arg],
-            Some(u32::MAX as usize),
-            Default::default(),
-        )
+        .run_function_with_starknet_context(func, args, Some(u32::MAX as usize), Default::default())
         .unwrap();
     // let profiling_processor =
     //     ProfilingInfoProcessor::new(None, sierra_program.program, UnorderedHashMap::default());

diff --git a/src/air/layouts/dex/public_input.cairo b/src/air/layouts/dex/public_input.cairo
@@ -10,7 +10,7 @@ use cairo_verifier::{
             segments, get_builtins, CPU_COMPONENT_HEIGHT, CPU_COMPONENT_STEP, LAYOUT_CODE,
             PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, ECDSA_BUILTIN_ROW_RATIO
         },
-        public_input::{CairoVersion, PublicInput, PublicInputTrait}
+        public_input::{PublicInput, PublicInputTrait}
     },
     domains::StarkDomains
 };
@@ -19,7 +19,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has
 use poseidon::poseidon_hash_span;
 
 impl DexPublicInputImpl of PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) {
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
@@ -114,6 +114,10 @@ impl DexPublicInputImpl of PublicInputTrait {
         (program_hash, output_hash)
     }
 
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) {
+        panic!("Not implemented")
+    }
+
     fn validate(self: @PublicInput, stark_domains: @StarkDomains) {
         assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS);
         let n_steps = pow(2, *self.log_n_steps);

diff --git a/src/air/layouts/recursive/public_input.cairo b/src/air/layouts/recursive/public_input.cairo
@@ -10,7 +10,7 @@ use cairo_verifier::{
             segments, get_builtins, CPU_COMPONENT_HEIGHT, CPU_COMPONENT_STEP, LAYOUT_CODE,
             PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO
         },
-        public_input::{CairoVersion, PublicInput, PublicInputTrait}
+        public_input::{PublicInput, PublicInputTrait}
     },
     domains::StarkDomains
 };
@@ -19,7 +19,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has
 use poseidon::poseidon_hash_span;
 
 impl RecursivePublicInputImpl of PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) {
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
@@ -39,85 +39,104 @@ impl RecursivePublicInputImpl of PublicInputTrait {
         let builtins = get_builtins();
         let memory = self.main_page;
 
-        let offset = match cairo_version {
-            CairoVersion::Cairo0 => 0,
-            CairoVersion::Cairo1 => 1,
-        };
-
         // 1. Program segment
         assert(initial_pc == INITIAL_PC, 'Invalid initial_pc');
-        assert(final_pc == INITIAL_PC + 4 + offset, 'Invalid final_pc');
+        assert(final_pc == INITIAL_PC + 4, 'Invalid final_pc');
 
         let mut memory_index: usize = 0;
 
-        let program_end_pc = initial_fp - (2 + offset);
+        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
             );
 
-        if cairo_version == CairoVersion::Cairo0 {
-            // Instruction: ap += N_BUILTINS.
-            assert(*program[0] == 0x40780017fff7fff, 'Invalid program');
-            assert(*program[1] == builtins.len().into(), 'Invalid program');
-            // Instruction: call rel ?.
-            assert(*program[2] == 0x1104800180018000, 'Invalid program');
-            // Instruction: jmp rel 0.
-            assert(*program[4] == 0x10780017fff7fff, 'Invalid program');
-            assert(*program[5] == 0x0, 'Invalid 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 = array![];
-            let mut stop_addresses = array![];
-            let mut i = 0;
-            let builtins_len = builtins.len();
-            while i != builtins_len {
-                let segment = *public_segments.at(2 + i);
-                begin_addresses.append(segment.begin_addr);
-                stop_addresses.append(segment.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
-                );
-        }
+        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
+            );
 
         // 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);
 
-        if cairo_version == CairoVersion::Cairo0 {
-            // Check main page len
-            assert(
-                *memory.at(memory_index - 1) == *memory.at(memory.len() - 1),
-                'Invalid main page len'
-            );
-        }
+        // Check main page len
+        assert(
+            *memory.at(memory_index - 1) == *memory.at(memory.len() - 1), 'Invalid main page len'
+        );
+
+        (program_hash, output_hash)
+    }
+
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) {
+        let public_segments = self.segments;
 
+        let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
+        let initial_ap = *public_segments.at(segments::EXECUTION).begin_addr;
+        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');
+        assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers');
+        let memory = self.main_page;
+
+        // 1. Program segment
+        assert(initial_pc == INITIAL_PC, 'Invalid initial_pc');
+        let program = memory
+            .extract_range_unchecked(initial_pc.try_into().unwrap(), memory.len() - output_len);
         let program_hash = poseidon_hash_span(program);
-        let output_hash = poseidon_hash_span(output);
 
+        // 2. Output segment 
+        let output = memory.extract_range_unchecked(memory.len() - output_len, output_len);
+        let output_hash = poseidon_hash_span(output);
         (program_hash, output_hash)
     }
 

diff --git a/src/air/layouts/recursive_with_poseidon/public_input.cairo b/src/air/layouts/recursive_with_poseidon/public_input.cairo
@@ -11,7 +11,7 @@ use cairo_verifier::{
             PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO,
             POSEIDON_ROW_RATIO
         },
-        public_input::{CairoVersion, PublicInput, PublicInputTrait}
+        public_input::{PublicInput, PublicInputTrait}
     },
     domains::StarkDomains
 };
@@ -20,7 +20,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has
 use poseidon::poseidon_hash_span;
 
 impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) {
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
@@ -115,6 +115,10 @@ impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait {
         (program_hash, output_hash)
     }
 
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) {
+        panic!("Not implemented")
+    }
+
     fn validate(self: @PublicInput, stark_domains: @StarkDomains) {
         assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS);
         let n_steps = pow(2, *self.log_n_steps);

diff --git a/src/air/layouts/small/public_input.cairo b/src/air/layouts/small/public_input.cairo
@@ -10,7 +10,7 @@ use cairo_verifier::{
             segments, get_builtins, CPU_COMPONENT_HEIGHT, CPU_COMPONENT_STEP, LAYOUT_CODE,
             PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, ECDSA_BUILTIN_ROW_RATIO
         },
-        public_input::{CairoVersion, PublicInput, PublicInputTrait}
+        public_input::{PublicInput, PublicInputTrait}
     },
     domains::StarkDomains
 };
@@ -19,7 +19,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has
 use poseidon::poseidon_hash_span;
 
 impl SmallPublicInputImpl of PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) {
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
@@ -114,6 +114,10 @@ impl SmallPublicInputImpl of PublicInputTrait {
         (program_hash, output_hash)
     }
 
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) {
+        panic!("Not implemented")
+    }
+
     fn validate(self: @PublicInput, stark_domains: @StarkDomains) {
         assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS);
         let n_steps = pow(2, *self.log_n_steps);

diff --git a/src/air/layouts/starknet/public_input.cairo b/src/air/layouts/starknet/public_input.cairo
@@ -11,7 +11,7 @@ use cairo_verifier::{
             PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO,
             ECDSA_BUILTIN_ROW_RATIO, EC_OP_BUILTIN_ROW_RATIO, POSEIDON_ROW_RATIO
         },
-        public_input::{CairoVersion, PublicInput, PublicInputTrait}
+        public_input::{PublicInput, PublicInputTrait}
     },
     domains::StarkDomains
 };
@@ -20,7 +20,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has
 use poseidon::poseidon_hash_span;
 
 impl StarknetPublicInputImpl of PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) {
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
@@ -115,6 +115,10 @@ impl StarknetPublicInputImpl of PublicInputTrait {
         (program_hash, output_hash)
     }
 
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) {
+        panic!("Not implemented")
+    }
+
     fn validate(self: @PublicInput, stark_domains: @StarkDomains) {
         assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS);
         let n_steps = pow(2, *self.log_n_steps);

diff --git a/src/air/layouts/starknet_with_keccak/public_input.cairo b/src/air/layouts/starknet_with_keccak/public_input.cairo
@@ -11,7 +11,7 @@ use cairo_verifier::{
             PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO,
             ECDSA_BUILTIN_ROW_RATIO, EC_OP_BUILTIN_ROW_RATIO, POSEIDON_ROW_RATIO, KECCAK_ROW_RATIO
         },
-        public_input::{CairoVersion, PublicInput, PublicInputTrait}
+        public_input::{PublicInput, PublicInputTrait}
     },
     domains::StarkDomains
 };
@@ -20,7 +20,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has
 use poseidon::poseidon_hash_span;
 
 impl StarknetWithKeccakPublicInputImpl of PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) {
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) {
         let public_segments = self.segments;
 
         let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr;
@@ -115,6 +115,10 @@ impl StarknetWithKeccakPublicInputImpl of PublicInputTrait {
         (program_hash, output_hash)
     }
 
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) {
+        panic!("Not implemented")
+    }
+
     fn validate(self: @PublicInput, stark_domains: @StarkDomains) {
         assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS);
         let n_steps = pow(2, *self.log_n_steps);

diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo
@@ -41,7 +41,8 @@ enum CairoVersion {
 }
 
 trait PublicInputTrait {
-    fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252);
+    fn verify_cairo0(self: @PublicInput) -> (felt252, felt252);
+    fn verify_cairo1(self: @PublicInput) -> (felt252, felt252);
     fn validate(self: @PublicInput, stark_domains: @StarkDomains);
 }
 

diff --git a/src/air/public_memory.cairo b/src/air/public_memory.cairo
@@ -11,7 +11,7 @@ type Page = Array<AddrValue>;
 // Each such page must be verified externally to the verifier:
 //   hash = Hash(
 //     memory[start_address], memory[start_address + 1], ..., memory[start_address + size - 1]).
-//   prod = prod_i (z - ((start_address + i) + alpha * (memory[start_address + i])).
+//   prod = prod_i (z - ((start_address + i) + alpha * (memory[start_address + i]))).
 // z, alpha are taken from the interaction values, and can be obtained directly from the
 // StarkProof object.
 //   z     = interaction_elements.memory_multi_column_perm_perm__interaction_elm
@@ -64,6 +64,17 @@ impl PageImpl of PageTrait {
         }
     }
 
+    fn extract_range_unchecked(self: @Page, addr: u32, len: usize) -> Span<felt252> {
+        let mut arr = ArrayTrait::new();
+        let mut slice = self.span().slice(addr, len);
+        while !slice
+            .is_empty() {
+                let current = *slice.pop_front().unwrap();
+                arr.append(current.value);
+            };
+        arr.span()
+    }
+
     fn verify_stack(
         self: @Page,
         start_ap: felt252,