air public input and public memory

src/air.cairo

@@ -2,3 +2,4 @@ mod composition;
 mod global_values;
 mod constants;
 mod public_input;
+mod public_memory;

src/air/composition.cairo

@@ -18,7 +18,7 @@ fn eval_composition_polynomial(
     let public_memory_column_size = trace_domain_size / PUBLIC_MEMORY_STEP;
     assert(public_memory_column_size >= 0, 'Invalid column size');
 
-    let public_memory_prod_ratio = public_input.get_public_memory_product_ratio();
+    let public_memory_prod_ratio = public_input.get_public_memory_product_ratio(memory_z, memory_alpha, public_memory_column_size);
 
     // TODO diluted
 
@@ -56,5 +56,6 @@ fn eval_composition_polynomial(
         diluted_check_final_cum_val: 0
     };
 
+    // TODO autogenerated
     0
 }

src/air/public_input.cairo

@@ -1,4 +1,12 @@
+use cairo_verifier::air::public_memory::{Page, PageTrait, ContinuousPageHeader, get_continuous_pages_product};
+use cairo_verifier::common::felt252::{pow, Felt252PartialOrd, Felt252Div};
+
+#[derive(Drop)]
 struct PublicInput {
+    padding_addr: felt252,
+    padding_value: felt252,
+    main_page: Page,
+    continuous_page_headers: Span<ContinuousPageHeader>
 }
 
 #[generate_trait]
@@ -12,6 +20,33 @@ impl PublicInputImpl of PublicInputTrait {
         alpha: felt252,
         public_memory_column_size: felt252
     ) -> felt252 {
-        0
+        let (pages_product, total_length) = self.get_public_memory_product(z, alpha);
+
+        // Pad and divide
+        let numerator = pow(z, public_memory_column_size);
+        let padded = z - (*self.padding_addr + alpha * *self.padding_value);
+
+        assert(total_length <= public_memory_column_size, 'Invalid length');
+        let denominator_pad = pow(padded, public_memory_column_size - total_length);
+
+        numerator / pages_product / denominator_pad
+    }
+
+    // Returns the product of all public memory cells.
+    fn get_public_memory_product(
+        self: @PublicInput,
+        z: felt252,
+        alpha: felt252
+    ) -> (felt252, felt252) {
+        let main_page_prod = self.main_page.get_product(z, alpha);
+
+        let (continuous_pages_prod, continuous_pages_total_length) = get_continuous_pages_product(
+            *self.continuous_page_headers,
+        );
+
+        let prod = main_page_prod * continuous_pages_prod;
+        let total_length = (self.main_page.len()).into() + continuous_pages_total_length;
+
+        (prod, total_length)
     }
 }

src/air/public_memory.cairo

@@ -0,0 +1,65 @@
+#[derive(Drop)]
+struct AddrValue {
+    address: felt252,
+    value: felt252
+}
+
+type Page = Array<AddrValue>;
+
+// Information about a continuous page (a consecutive section of the public memory)..
+// 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])).
+// 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
+//   alpha = interaction_elements.memory_multi_column_perm_hash_interaction_elm0
+#[derive(Drop)]
+struct ContinuousPageHeader {
+    // Start address.
+    //start_address: felt252,
+    // Size of the page.
+    size: felt252,
+    // Hash of the page.
+    //hash: u256
+    // Cumulative product of the page.
+    prod: felt252,
+}
+
+#[generate_trait]
+impl PageImpl of PageTrait {
+    // Returns the product of (z - (addr + alpha * val)) over a single page.
+    fn get_product(
+        self: @Page,
+        z: felt252,
+        alpha: felt252
+    ) -> felt252 {
+        let mut res = 1;
+        let mut i = 0;
+        loop {
+            if i == self.len() {
+                break res;
+            }
+            let current = self.at(i);
+
+            res *= z - (*current.address + alpha * *current.value);
+        }
+    }
+}
+
+fn get_continuous_pages_product(page_headers: Span<ContinuousPageHeader>) -> (felt252, felt252) {
+        let mut res = 1;
+        let mut total_length = 0;
+        let mut i = 0;
+        loop {
+            if i == page_headers.len() {
+                break (res, total_length);
+            }
+            let current = page_headers.at(i);
+
+            res *= *current.prod;
+            total_length += *current.size;
+        }
+}
+