Merge pull request #753 from powdr-labs/write-once-memory

Write-Once Memory

compiler/src/verify.rs

@@ -10,7 +10,12 @@ use std::{
 
 use crate::compile_asm_string;
 
-pub fn verify_asm_string<T: FieldElement>(file_name: &str, contents: &str, inputs: Vec<T>) {
+pub fn verify_asm_string<T: FieldElement>(
+    file_name: &str,
+    contents: &str,
+    inputs: Vec<T>,
+    external_witness_values: Vec<(&str, Vec<T>)>,
+) {
     let temp_dir = mktemp::Temp::new_dir().unwrap();
     let (_, result) = compile_asm_string(
         file_name,
@@ -20,7 +25,7 @@ pub fn verify_asm_string<T: FieldElement>(file_name: &str, contents: &str, input
         &temp_dir,
         true,
         Some(BackendType::PilStarkCli),
-        vec![],
+        external_witness_values,
     )
     .unwrap();
 

compiler/tests/asm.rs

@@ -4,14 +4,22 @@ use std::fs;
 use test_log::test;
 
 fn verify_asm<T: FieldElement>(file_name: &str, inputs: Vec<T>) {
+    verify_asm_with_external_witness(file_name, inputs, vec![]);
+}
+
+fn verify_asm_with_external_witness<T: FieldElement>(
+    file_name: &str,
+    inputs: Vec<T>,
+    external_witness_values: Vec<(&str, Vec<T>)>,
+) {
     let file_name = format!(
         "{}/../test_data/asm/{file_name}",
         env!("CARGO_MANIFEST_DIR")
     );
 
     let contents = fs::read_to_string(&file_name).unwrap();
 
-    verify_asm_string(&file_name, &contents, inputs)
+    verify_asm_string(&file_name, &contents, inputs, external_witness_values);
 }
 
 fn gen_estark_proof(file_name: &str, inputs: Vec<GoldilocksField>) {
@@ -71,6 +79,24 @@ fn secondary_block_machine_add2() {
     gen_estark_proof(f, vec![]);
 }
 
+#[test]
+fn mem_write_once() {
+    let f = "mem_write_once.asm";
+    verify_asm::<GoldilocksField>(f, vec![]);
+    gen_halo2_proof(f, vec![]);
+    gen_estark_proof(f, vec![]);
+}
+
+#[test]
+fn mem_write_once_external_write() {
+    let f = "mem_write_once_external_write.asm";
+    let mut mem = vec![GoldilocksField::from(0); 256];
+    mem[17] = GoldilocksField::from(42);
+    mem[62] = GoldilocksField::from(123);
+    mem[255] = GoldilocksField::from(-1);
+    verify_asm_with_external_witness::<GoldilocksField>(f, vec![], vec![("main.v", mem)]);
+}
+
 #[test]
 fn block_machine_cache_miss() {
     let f = "block_machine_cache_miss.asm";

compiler/tests/powdr_std.rs

@@ -11,7 +11,7 @@ fn verify_asm<T: FieldElement>(file_name: &str, inputs: Vec<T>) {
 
     let contents = fs::read_to_string(&file_name).unwrap();
 
-    verify_asm_string(&file_name, &contents, inputs)
+    verify_asm_string(&file_name, &contents, inputs, vec![])
 }
 
 fn gen_estark_proof(file_name: &str, inputs: Vec<GoldilocksField>) {

executor/src/witgen/machines/block_machine.rs

@@ -15,6 +15,7 @@ use crate::witgen::{machines::Machine, EvalError, EvalValue, IncompleteCause};
 use crate::witgen::{MutableState, QueryCallback};
 use ast::analyzed::{
     AlgebraicExpression as Expression, AlgebraicReference, Identity, IdentityKind, PolyID,
+    PolynomialType,
 };
 use ast::parsed::SelectedExpressions;
 use number::{DegreeType, FieldElement};
@@ -72,6 +73,17 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> {
         global_range_constraints: &GlobalConstraints<T>,
     ) -> Option<Self> {
         for id in connecting_identities {
+            for r in id.right.expressions.iter() {
+                if let Some(poly) = try_to_simple_poly(r) {
+                    if poly.poly_id.ptype == PolynomialType::Constant {
+                        // It does not really make sense to have constant polynomials on the RHS
+                        // of a block machine lookup, as all constant polynomials are periodic, so
+                        // it would always return the same value.
+                        return None;
+                    }
+                }
+            }
+
             // TODO we should check that the other constraints/fixed columns are also periodic.
             if let Some(block_size) = try_to_period(&id.right.selector, fixed_data) {
                 assert!(block_size <= fixed_data.degree as usize);

executor/src/witgen/machines/machine_extractor.rs

@@ -8,6 +8,7 @@ use super::FixedData;
 use super::KnownMachine;
 use crate::witgen::generator::Generator;
 use crate::witgen::global_constraints::GlobalConstraints;
+use crate::witgen::machines::write_once_memory::WriteOnceMemory;
 use ast::analyzed::{AlgebraicExpression as Expression, Identity, IdentityKind, PolyID};
 use ast::parsed::visitor::ExpressionVisitable;
 use ast::parsed::SelectedExpressions;
@@ -107,6 +108,11 @@ pub fn split_out_machines<'a, T: FieldElement>(
         {
             log::info!("Detected machine: memory");
             machines.push(KnownMachine::DoubleSortedWitnesses(machine));
+        } else if let Some(machine) =
+            WriteOnceMemory::try_new(fixed, &connecting_identities, &machine_identities)
+        {
+            log::info!("Detected machine: write-once memory");
+            machines.push(KnownMachine::WriteOnceMemory(machine));
         } else if let Some(machine) = BlockMachine::try_new(
             fixed,
             &connecting_identities,

executor/src/witgen/machines/mod.rs

@@ -9,6 +9,7 @@ use self::block_machine::BlockMachine;
 use self::double_sorted_witness_machine::DoubleSortedWitnesses;
 pub use self::fixed_lookup_machine::FixedLookup;
 use self::sorted_witness_machine::SortedWitnesses;
+use self::write_once_memory::WriteOnceMemory;
 use ast::analyzed::IdentityKind;
 
 use super::affine_expression::AffineExpression;
@@ -23,6 +24,7 @@ mod double_sorted_witness_machine;
 mod fixed_lookup_machine;
 pub mod machine_extractor;
 mod sorted_witness_machine;
+mod write_once_memory;
 
 /// A machine is a set of witness columns and identities where the columns
 /// are used on the right-hand-side of lookups. It can process plookups.
@@ -54,6 +56,7 @@ pub trait Machine<'a, T: FieldElement>: Send + Sync {
 pub enum KnownMachine<'a, T: FieldElement> {
     SortedWitnesses(SortedWitnesses<'a, T>),
     DoubleSortedWitnesses(DoubleSortedWitnesses<T>),
+    WriteOnceMemory(WriteOnceMemory<'a, T>),
     BlockMachine(BlockMachine<'a, T>),
     Vm(Generator<'a, T>),
 }
@@ -71,6 +74,7 @@ impl<'a, T: FieldElement> Machine<'a, T> for KnownMachine<'a, T> {
             KnownMachine::DoubleSortedWitnesses(m) => {
                 m.process_plookup(mutable_state, kind, left, right)
             }
+            KnownMachine::WriteOnceMemory(m) => m.process_plookup(mutable_state, kind, left, right),
             KnownMachine::BlockMachine(m) => m.process_plookup(mutable_state, kind, left, right),
             KnownMachine::Vm(m) => m.process_plookup(mutable_state, kind, left, right),
         }
@@ -88,6 +92,9 @@ impl<'a, T: FieldElement> Machine<'a, T> for KnownMachine<'a, T> {
             KnownMachine::DoubleSortedWitnesses(m) => {
                 m.take_witness_col_values(fixed_lookup, query_callback)
             }
+            KnownMachine::WriteOnceMemory(m) => {
+                m.take_witness_col_values(fixed_lookup, query_callback)
+            }
             KnownMachine::BlockMachine(m) => {
                 m.take_witness_col_values(fixed_lookup, query_callback)
             }