Public input verification

.tool-versions

@@ -1 +1 @@
-scarb 2.4.1
+scarb 2.4.2

src/air/composition.cairo

@@ -1,17 +1,14 @@
 use cairo_verifier::air::global_values::{EcPoint, InteractionElements, GlobalValues};
 use cairo_verifier::air::constants::{
     PUBLIC_MEMORY_STEP, DILUTED_N_BITS, DILUTED_SPACING, PEDERSEN_BUILTIN_RATIO,
-    PEDERSEN_BUILTIN_REPETITIONS, segments
+    PEDERSEN_BUILTIN_REPETITIONS, segments, SHIFT_POINT_X, SHIFT_POINT_Y
 };
 use cairo_verifier::air::public_input::{PublicInput, PublicInputTrait};
 use cairo_verifier::air::diluted::get_diluted_product;
 use cairo_verifier::air::pedersen::{eval_pedersen_x, eval_pedersen_y};
 use cairo_verifier::air::autogenerated::eval_composition_polynomial_inner;
 use cairo_verifier::common::math::{Felt252Div, Felt252PartialOrd, pow, assert_range_u128};
 
-const SHIFT_POINT_X: felt252 = 0x49ee3eba8c1600700ee1b87eb599f16716b0b1022947733551fde4050ca6804;
-const SHIFT_POINT_Y: felt252 = 0x3ca0cfe4b3bc6ddf346d49d06ea0ed34e621062c0e056c1d0405d266e10268a;
-
 fn eval_composition_polynomial(
     interaction_elements: InteractionElements,
     public_input: PublicInput,

src/air/constants.cairo

@@ -38,3 +38,15 @@ mod segments {
     const BITWISE: usize = 5;
     const N_SEGMENTS: usize = 6;
 }
+
+// Pedersen builtin
+const SHIFT_POINT_X: felt252 = 0x49ee3eba8c1600700ee1b87eb599f16716b0b1022947733551fde4050ca6804;
+const SHIFT_POINT_Y: felt252 = 0x3ca0cfe4b3bc6ddf346d49d06ea0ed34e621062c0e056c1d0405d266e10268a;
+
+const SECURITY_BITS: felt252 = 128;
+const MAX_ADDRESS: felt252 = 0xffffffffffffffff;
+const INITIAL_PC: felt252 = 1;
+
+fn get_builtins() -> Array<felt252> {
+    array!['output', 'pedersen', 'range_check', 'bitwise']
+}

src/air/public_input.cairo

@@ -5,6 +5,8 @@ use cairo_verifier::{
     },
     air::public_memory::{Page, PageTrait, ContinuousPageHeader, get_continuous_pages_product}
 };
+use cairo_verifier::common::hash::hash_felts;
+use cairo_verifier::air::constants::{segments, MAX_ADDRESS, get_builtins, INITIAL_PC};
 use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Hash}};
 
 #[derive(Drop, Copy)]
@@ -148,4 +150,88 @@ impl PublicInputImpl of PublicInputTrait {
 
         (prod, total_length)
     }
+
+    fn verify(self: @PublicInput) -> (felt252, felt252) {
+        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;
+
+        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;
+
+        // 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, program_len);
+        memory_index += program_len.try_into().unwrap();
+
+        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 = hash_felts(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
+        memory
+            .verify_stack(
+                initial_ap, *public_segments.at(2).begin_addr, builtins.span(), memory_index.into()
+            );
+        memory_index += builtins.len();
+
+        memory
+            .verify_stack(
+                final_ap - builtins.len().into(),
+                *public_segments.at(2).stop_ptr,
+                builtins.span(),
+                memory_index.into()
+            );
+        memory_index += builtins.len();
+
+        // 3. Output segment 
+        let output = memory
+            .extract_range(memory_index.into() + output_start, output_stop - output_start);
+        memory_index += (output_stop - output_start).try_into().unwrap();
+        let output_hash = hash_felts(output);
+
+        // Check main page len
+        assert(
+            *memory.at(memory_index) == *self.main_page.at(self.main_page.len() - 1),
+            'Invalid main page len'
+        );
+
+        (program_hash, output_hash)
+    }
 }
+

src/air/public_memory.cairo

@@ -1,4 +1,4 @@
-#[derive(Drop, Copy)]
+#[derive(Drop, Copy, PartialEq)]
 struct AddrValue {
     address: felt252,
     value: felt252
@@ -43,6 +43,48 @@ impl PageImpl of PageTrait {
             i += 1;
         }
     }
+
+    fn extract_range(self: @Page, addr: felt252, len: felt252) -> Span<felt252> {
+        let mut arr = ArrayTrait::new();
+        let mut i = 0;
+
+        loop {
+            if i == len {
+                break arr.span();
+            }
+
+            let current = *self.at((addr + i).try_into().unwrap());
+
+            // TODO is this needed? If not we can just use slice directly 
+            assert(current.address == addr + i, 'Invalid address');
+            arr.append(current.value);
+            i += 1;
+        }
+    }
+
+    fn verify_stack(
+        self: @Page,
+        start_ap: felt252,
+        segment_address: felt252,
+        builtins: Span<felt252>,
+        memory_index: felt252
+    ) {
+        let mut i = 0;
+
+        // TODO size of SegmentInfo
+        let size = 2;
+        loop {
+            if i == builtins.len() {
+                break;
+            }
+
+            let current = *self.at(memory_index.try_into().unwrap() + i);
+
+            assert(current.address == start_ap + i.into(), 'Invalid address');
+            assert(current.value == segment_address + size * (i.into() + 1), 'Invalid builtin');
+            i += 1;
+        };
+    }
 }
 
 fn get_continuous_pages_product(page_headers: Span<ContinuousPageHeader>) -> (felt252, felt252) {

src/common.cairo

@@ -10,6 +10,7 @@ mod flip_endianness;
 mod from_span;
 mod horner_eval;
 mod math;
+mod hash;
 mod merge_sort;
 mod bit_reverse;
 mod powers_array;

src/common/hash.cairo

@@ -0,0 +1,15 @@
+use pedersen::PedersenTrait;
+use hash::HashStateTrait;
+
+fn hash_felts(s: Span<felt252>) -> felt252 {
+    let mut hash_state = PedersenTrait::new(0);
+    let mut i = 0;
+
+    loop {
+        if i == s.len() {
+            break hash_state.finalize();
+        }
+
+        hash_state.update(*s.at(i));
+    }
+}

src/input_structs.cairo

@@ -0,0 +1,5 @@
+mod public_input;
+mod stark_config;
+mod stark_proof;
+mod stark_unsent_commitment;
+mod stark_witness;

src/input_structs/public_input.cairo

@@ -0,0 +1,16 @@
+#[derive(Drop, Serde)]
+struct PublicInput {
+    log_n_steps: felt252,
+    range_check_min: felt252,
+    range_check_max: felt252,
+    layout: felt252,
+    dynamic_params: Array<felt252>,
+    n_segments: felt252,
+    segments: Array<felt252>,
+    padding_addr: felt252,
+    padding_value: felt252,
+    main_page_len: felt252,
+    main_page: Array<felt252>,
+    n_continuous_pages: felt252,
+    continuous_page_headers: Array<felt252>,
+}

src/input_structs/stark_config.cairo

@@ -0,0 +1,55 @@
+#[derive(Drop, Serde)]
+struct StarkConfig {
+    traces: TracesConfig,
+    composition: TableCommitmentConfig,
+    fri: FriConfig,
+    proof_of_work: ProofOfWorkConfig,
+    // Log2 of the trace domain size.
+    log_trace_domain_size: felt252,
+    // Number of queries to the last component, FRI.
+    n_queries: felt252,
+    // Log2 of the number of cosets composing the evaluation domain, where the coset size is the
+    // trace length.
+    log_n_cosets: felt252,
+    // Number of layers that use a verifier friendly hash in each commitment.
+    n_verifier_friendly_commitment_layers: felt252,
+}
+
+#[derive(Drop, Serde)]
+struct TracesConfig {
+    original: TableCommitmentConfig,
+    interaction: TableCommitmentConfig,
+}
+
+#[derive(Drop, Serde)]
+struct TableCommitmentConfig {
+    columns: felt252,
+    vector: VectorCommitmentConfig
+}
+
+#[derive(Drop, Serde)]
+struct VectorCommitmentConfig {
+    height: felt252,
+    verifier_friendly_commitment_layers: felt252,
+}
+
+#[derive(Drop, Serde)]
+struct FriConfig {
+    // Log2 of the size of the input layer to FRI.
+    log_input_size: felt252,
+    // Number of layers in the FRI. Inner + last layer.
+    n_layers: felt252,
+    // Array of size n_layers - 1, each entry is a configuration of a table commitment for the
+    // corresponding inner layer.
+    inner_layers: Array<felt252>,
+    // Array of size n_layers, each entry represents the FRI step size,
+    // i.e. the number of FRI-foldings between layer i and i+1.
+    fri_step_sizes: Array<felt252>,
+    log_last_layer_degree_bound: felt252,
+}
+
+#[derive(Drop, Serde)]
+struct ProofOfWorkConfig {
+    // Proof of work difficulty (number of bits required to be 0).
+    n_bits: felt252,
+}

src/input_structs/stark_proof.cairo

@@ -0,0 +1,13 @@
+use cairo_verifier::input_structs::{
+    stark_config::StarkConfig, public_input::PublicInput,
+    stark_unsent_commitment::StarkUnsentCommitment, stark_witness::StarkWitness,
+};
+
+
+#[derive(Drop, Serde)]
+struct StarkProof {
+    config: StarkConfig,
+    public_input: PublicInput,
+    unsent_commitment: StarkUnsentCommitment,
+    witness: StarkWitness,
+}

src/input_structs/stark_unsent_commitment.cairo

@@ -0,0 +1,25 @@
+#[derive(Drop, Serde)]
+struct StarkUnsentCommitment {
+    traces: TracesUnsentCommitment,
+    composition: felt252,
+    oods_values: Array<felt252>,
+    fri: FriUnsentCommitment,
+    proof_of_work: ProofOfWorkUnsentCommitment,
+}
+
+#[derive(Drop, Serde)]
+struct TracesUnsentCommitment {
+    original: felt252,
+    interaction: felt252,
+}
+
+#[derive(Drop, Serde)]
+struct FriUnsentCommitment {
+    inner_layers: Array<felt252>,
+    last_layer_coefficients: Array<felt252>,
+}
+
+#[derive(Drop, Serde)]
+struct ProofOfWorkUnsentCommitment {
+    nonce: felt252,
+}

src/input_structs/stark_witness.cairo

@@ -0,0 +1,42 @@
+#[derive(Drop, Serde)]
+struct StarkWitness {
+    traces_decommitment: TracesDecommitment,
+    traces_witness: TracesWitness,
+    interaction: TableCommitmentWitness,
+    composition_decommitment: TableDecommitment,
+    composition_witness: TableCommitmentWitness,
+    fri_witness: FriWitness,
+}
+
+#[derive(Drop, Serde)]
+struct TracesDecommitment {
+    original: TableDecommitment,
+    interaction: TableDecommitment,
+}
+
+#[derive(Drop, Serde)]
+struct TableDecommitment {
+    n_values: felt252,
+    values: Array<felt252>,
+}
+
+#[derive(Drop, Serde)]
+struct TracesWitness {
+    original: TableCommitmentWitness,
+}
+
+#[derive(Drop, Serde)]
+struct TableCommitmentWitness {
+    vector: VectorCommitmentWitness,
+}
+
+#[derive(Drop, Serde)]
+struct VectorCommitmentWitness {
+    n_authentications: felt252,
+    authentications: Array<felt252>,
+}
+
+#[derive(Drop, Serde)]
+struct FriWitness {
+    layers: Array<felt252>,
+}