From d830e69ab15671ec494a25dbd9ed17baa23fe15f Mon Sep 17 00:00:00 2001 From: Victor Dumitrescu Date: Fri, 29 Nov 2024 17:37:33 +0100 Subject: [PATCH 1/2] RISC-V/ProofGen: Small refactoring of `AccessInfo` --- .../lib/src/state_backend/proof_backend.rs | 12 ++---------- .../src/state_backend/proof_backend/merkle.rs | 18 ++++++++++++++++++ 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/src/riscv/lib/src/state_backend/proof_backend.rs b/src/riscv/lib/src/state_backend/proof_backend.rs index 98da3a33c61f..dc11b0bea9a6 100644 --- a/src/riscv/lib/src/state_backend/proof_backend.rs +++ b/src/riscv/lib/src/state_backend/proof_backend.rs @@ -278,20 +278,12 @@ impl ProofRegion { /// Set the access log to `Read` or, if previously `Write`, to `ReadWrite`. pub fn set_read(&self) { - match self.access.get() { - AccessInfo::NoAccess => self.access.set(AccessInfo::Read), - AccessInfo::Write => self.access.set(AccessInfo::ReadWrite), - _ => (), - } + self.access.set(AccessInfo::and_read(self.access.get())) } /// Set the access log to `Write` or, if previously `Read`, to `ReadWrite`. pub fn set_write(&self) { - match self.access.get() { - AccessInfo::NoAccess => self.access.set(AccessInfo::Write), - AccessInfo::Read => self.access.set(AccessInfo::ReadWrite), - _ => (), - } + self.access.set(AccessInfo::and_write(self.access.get())) } /// Set the access log to `ReadWrite`. diff --git a/src/riscv/lib/src/state_backend/proof_backend/merkle.rs b/src/riscv/lib/src/state_backend/proof_backend/merkle.rs index ea71a85e0e9c..f195db534ab6 100644 --- a/src/riscv/lib/src/state_backend/proof_backend/merkle.rs +++ b/src/riscv/lib/src/state_backend/proof_backend/merkle.rs @@ -137,6 +137,24 @@ impl AccessInfo { Self::ReadWrite => CompressedAccessInfo::ReadWrite(data), } } + + /// Return the updated access information after a read. + pub fn and_read(self) -> Self { + match self { + AccessInfo::NoAccess => AccessInfo::Read, + AccessInfo::Write => AccessInfo::ReadWrite, + access => access, + } + } + + /// Return the updated access information after a write. + pub fn and_write(self) -> Self { + match self { + AccessInfo::NoAccess => AccessInfo::Write, + AccessInfo::Read => AccessInfo::ReadWrite, + access => access, + } + } } /// Intermediary representation obtained when compressing a [`MerkleTree`]. -- GitLab From 8924ad3c629eea771f0527c05e351662a43dbb3f Mon Sep 17 00:00:00 2001 From: Victor Dumitrescu Date: Fri, 29 Nov 2024 17:38:38 +0100 Subject: [PATCH 2/2] RISC-V/ProofGen: Add support for EnrichedCell --- .../lib/src/state_backend/proof_backend.rs | 124 +++++++++++++++--- 1 file changed, 103 insertions(+), 21 deletions(-) diff --git a/src/riscv/lib/src/state_backend/proof_backend.rs b/src/riscv/lib/src/state_backend/proof_backend.rs index dc11b0bea9a6..6b6be0de5b60 100644 --- a/src/riscv/lib/src/state_backend/proof_backend.rs +++ b/src/riscv/lib/src/state_backend/proof_backend.rs @@ -113,30 +113,35 @@ impl ManagerRead for ProofGen { } } - fn enriched_cell_read_stored(_cell: &Self::EnrichedCell) -> V::E + fn enriched_cell_read_stored(cell: &Self::EnrichedCell) -> V::E where V: EnrichedValue, V::E: Copy, { - // TODO: RV-325 Support for `EnrichedCell` in the proof-generating backend - todo!() + cell.set_read(); + match &cell.written { + None => M::enriched_cell_read_stored(&cell.source), + Some(value) => *value, + } } - fn enriched_cell_read_derived(_cell: &Self::EnrichedCell) -> V::D + fn enriched_cell_read_derived(cell: &Self::EnrichedCell) -> V::D where V: EnrichedValueLinked, V::D: Copy, { - // TODO: RV-325 Support for `EnrichedCell` in the proof-generating backend - todo!() + V::derive(Self::enriched_cell_ref_stored(cell)) } - fn enriched_cell_ref_stored(_cell: &Self::EnrichedCell) -> &V::E + fn enriched_cell_ref_stored(cell: &Self::EnrichedCell) -> &V::E where V: EnrichedValue, { - // TODO: RV-325 Support for `EnrichedCell` in the proof-generating backend - todo!() + cell.set_read(); + match &cell.written { + None => M::enriched_cell_ref_stored(&cell.source), + Some(value) => value, + } } } @@ -194,12 +199,12 @@ impl ManagerWrite for ProofGen { } } - fn enriched_cell_write(_cell: &mut Self::EnrichedCell, _value: V::E) + fn enriched_cell_write(cell: &mut Self::EnrichedCell, value: V::E) where V: EnrichedValueLinked, { - // TODO: RV-325 Support for `EnrichedCell` in the proof-generating backend - todo!() + cell.set_write(); + cell.written = Some(value); } } @@ -223,6 +228,7 @@ impl ManagerSerialise for ProofGen { region: &Self::Region, serializer: S, ) -> Result { + // TODO RV-310: Serialise all the data in the region M::serialise_region(®ion.source, serializer) } @@ -230,20 +236,21 @@ impl ManagerSerialise for ProofGen { region: &Self::DynRegion, serializer: S, ) -> Result { + // TODO RV-310: Serialise all the data in the dynamic region M::serialise_dyn_region(®ion.source, serializer) } fn serialise_enriched_cell( - _cell: &Self::EnrichedCell, - _serializer: S, + cell: &Self::EnrichedCell, + serializer: S, ) -> Result where V: EnrichedValue, V::E: serde::Serialize, S: serde::Serializer, { - // TODO: RV-325 Support for `EnrichedCell` in the proof-generating backend - todo!() + // TODO RV-310: Serialise all the data in the enriched cell + M::serialise_enriched_cell(&cell.source, serializer) } } @@ -278,12 +285,12 @@ impl ProofRegion { /// Set the access log to `Read` or, if previously `Write`, to `ReadWrite`. pub fn set_read(&self) { - self.access.set(AccessInfo::and_read(self.access.get())) + self.access.set(self.access.get().and_read()) } /// Set the access log to `Write` or, if previously `Read`, to `ReadWrite`. pub fn set_write(&self) { - self.access.set(AccessInfo::and_write(self.access.get())) + self.access.set(self.access.get().and_write()) } /// Set the access log to `ReadWrite`. @@ -337,16 +344,46 @@ impl ProofDynRegion { } } -// TODO: RV-325 Support for `EnrichedCell` in the proof-generating backend -#[allow(dead_code)] +/// Proof enriched cell which wraps an enriched cell managed by another manager. +/// +/// Similar to [`ManagerBase::Region`], a [`ManagerBase::EnrichedCell`] is never +/// split across multiple leaves when Merkleised. +/// The underlying cell is never mutated, but written values are recorded +/// in order to preserve the integrity of subsequent reads. pub struct ProofEnrichedCell { source: M::EnrichedCell, + written: Option, + access: Cell, } impl ProofEnrichedCell { /// Bind a pre-existing enriched cell. pub fn bind(source: M::EnrichedCell) -> Self { - Self { source } + Self { + source, + written: None, + access: Cell::new(AccessInfo::NoAccess), + } + } + + /// Get a copy of the access log. + pub fn get_access_info(&self) -> AccessInfo { + self.access.get() + } + + /// Set the access log to `Read` or, if previously `Write`, to `ReadWrite`. + pub fn set_read(&self) { + self.access.set(AccessInfo::and_read(self.access.get())) + } + + /// Set the access log to `Write` or, if previously `Read`, to `ReadWrite`. + pub fn set_write(&mut self) { + self.access.set(AccessInfo::and_write(self.access.get())) + } + + /// Set the access log to `ReadWrite`. + pub fn set_read_write(&self) { + self.access.set(AccessInfo::ReadWrite) } } @@ -596,4 +633,49 @@ mod tests { } }); } + + #[test] + fn test_proof_gen_enriched_cell() { + pub struct Enriching; + + impl EnrichedValue for Enriching { + type E = u64; + type D = T; + } + + #[derive(Clone, Copy, Debug, PartialEq)] + pub struct T(u64); + + impl<'a> From<&'a u64> for T { + fn from(value: &'a u64) -> Self { + T(value.wrapping_add(1)) + } + } + + proptest!(|(value_before: u64, value_after: u64)| { + // A read followed by a write + let cell = (value_before, T::from(&value_before)); + let mut proof_cell: ProofEnrichedCell = ProofEnrichedCell::bind(cell); + prop_assert_eq!(proof_cell.get_access_info(), AccessInfo::NoAccess); + let value = ProofGen::::enriched_cell_read_stored(&proof_cell); + prop_assert_eq!(value, value_before); + let derived = ProofGen::::enriched_cell_read_derived(&proof_cell); + prop_assert_eq!(derived, T::from(&value_before)); + prop_assert_eq!(proof_cell.get_access_info(), AccessInfo::Read); + ProofGen::::enriched_cell_write(&mut proof_cell, value_after); + prop_assert_eq!(proof_cell.get_access_info(), AccessInfo::ReadWrite); + + // A write followed by a read + let cell = (value_before, T::from(&value_before)); + let mut proof_cell: ProofEnrichedCell = ProofEnrichedCell::bind(cell); + prop_assert_eq!(proof_cell.get_access_info(), AccessInfo::NoAccess); + ProofGen::::enriched_cell_write(&mut proof_cell, value_after); + prop_assert_eq!(proof_cell.get_access_info(), AccessInfo::Write); + let value = ProofGen::::enriched_cell_read_stored(&proof_cell); + prop_assert_eq!(value, value_after); + let derived = ProofGen::::enriched_cell_read_derived(&proof_cell); + prop_assert_eq!(derived, T::from(&value_after)); + prop_assert_eq!(proof_cell.get_access_info(), AccessInfo::ReadWrite); + }); + } } -- GitLab