Skip to content

Commit c5a0c94

Browse files
committed
feat(traits): Add new trait mem_preserver
This trait makes it easier to reason about code, as there is a snippet (verify_mmr_successor) which can read from ND but does not modify memory. In order to reason about the soundness of that snippet, this trait `MemPreserver` is added. It makes it easier to clarify that the field-access of `verify_mmr_successor` is safe.
1 parent 7c86811 commit c5a0c94

File tree

7 files changed

+215
-5
lines changed

7 files changed

+215
-5
lines changed

tasm-lib/src/traits.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,6 @@ pub mod closure;
55
pub mod compiled_program;
66
pub mod deprecated_snippet;
77
pub mod function;
8+
pub mod mem_preserver;
89
pub mod procedure;
910
pub mod rust_shadow;

tasm-lib/src/traits/accessor.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,13 @@ use super::rust_shadow::RustShadow;
2323
/// stack but can only read from memory. Note that it cannot write to static
2424
/// memory. It cannot read from any inputs or write to standard out. It cannot
2525
/// modify the sponge state.
26-
/// See also: [closure], [function], [procedure], [algorithm]
26+
/// See also: [closure], [function], [procedure], [algorithm], [mem_preserver]
2727
///
2828
/// [closure]: crate::traits::closure::Closure
2929
/// [function]: crate::traits::function::Function
3030
/// [procedure]: crate::traits::procedure::Procedure
3131
/// [algorithm]: crate::traits::algorithm::Algorithm
32+
/// [mem_preserver]: crate::traits::mem_preserver::MemPreserver
3233
pub trait Accessor: BasicSnippet {
3334
fn rust_shadow(
3435
&self,

tasm-lib/src/traits/algorithm.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,13 @@ use super::rust_shadow::RustShadow;
2323
/// the dynamic memory allocator, and can take nondeterministic input. It cannot read from
2424
/// standard in or write to standard out.
2525
///
26-
/// See also: [closure], [function], [procedure], [accessor]
26+
/// See also: [closure], [function], [procedure], [accessor], [mem_preserver]
2727
///
2828
/// [closure]: crate::traits::closure::Closure
2929
/// [function]: crate::traits::function::Function
3030
/// [procedure]: crate::traits::procedure::Procedure
3131
/// [accessor]: crate::traits::accessor::Accessor
32+
/// [mem_preserver]: crate::traits::mem_preserver::MemPreserver
3233
pub trait Algorithm: BasicSnippet {
3334
fn rust_shadow(
3435
&self,

tasm-lib/src/traits/closure.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,13 @@ use super::rust_shadow::RustShadow;
1818
/// A Closure is a piece of tasm code that modifies the top of the stack without access to
1919
/// memory or nondeterminism or standard input/output.
2020
///
21-
/// See also: [function], [algorithm], [procedure], [accessor]
21+
/// See also: [function], [algorithm], [procedure], [accessor], [mem_preserver]
2222
///
2323
/// [function]: crate::traits::function::Function
2424
/// [algorithm]: crate::traits::algorithm::Algorithm
2525
/// [procedure]: crate::traits::procedure::Procedure
2626
/// [accessor]: crate::traits::accessor::Accessor
27+
/// [mem_preserver]: crate::traits::mem_preserver::MemPreserver
2728
pub trait Closure: BasicSnippet {
2829
fn rust_shadow(&self, stack: &mut Vec<BFieldElement>);
2930

tasm-lib/src/traits/function.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,13 @@ use super::rust_shadow::RustShadow;
2323
/// larger than the dynamic memory allocator and the dynamic memory allocator value has to
2424
/// be updated accordingly.
2525
///
26-
/// See also: [closure], [algorithm], [procedure], [accessor]
26+
/// See also: [closure], [algorithm], [procedure], [accessor], [mem_preserver]
2727
///
2828
/// [closure]: crate::traits::closure::Closure
2929
/// [algorithm]: crate::traits::algorithm::Algorithm
3030
/// [procedure]: crate::traits::procedure::Procedure
3131
/// [accessor]: crate::traits::accessor::Accessor
32+
/// [mem_preserver]: crate::traits::mem_preserver::MemPreserver
3233
pub trait Function: BasicSnippet {
3334
fn rust_shadow(
3435
&self,
Lines changed: 204 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
1+
use std::cell::RefCell;
2+
use std::collections::HashMap;
3+
use std::collections::VecDeque;
4+
use std::rc::Rc;
5+
6+
use rand::prelude::*;
7+
use triton_vm::prelude::*;
8+
9+
use crate::linker::execute_bench;
10+
use crate::linker::link_for_isolated_run;
11+
use crate::snippet_bencher::write_benchmarks;
12+
use crate::snippet_bencher::BenchmarkCase;
13+
use crate::snippet_bencher::NamedBenchmarkResult;
14+
use crate::test_helpers::test_rust_equivalence_given_complete_state;
15+
use crate::InitVmState;
16+
use crate::VmHasher;
17+
18+
use super::basic_snippet::BasicSnippet;
19+
use super::rust_shadow::RustShadow;
20+
21+
/// A MemPreserver cannot modify memory
22+
///
23+
/// An MemPreserver is a piece of tasm code that can do pretty much everything
24+
/// except modify memory, including static memory. It can read from any input
25+
/// and write to standard out. It can also modify the sponge state.
26+
/// See also: [closure], [function], [procedure], [algorithm], [accessor]
27+
///
28+
/// [closure]: crate::traits::closure::Closure
29+
/// [function]: crate::traits::function::Function
30+
/// [procedure]: crate::traits::procedure::Procedure
31+
/// [algorithm]: crate::traits::algorithm::Algorithm
32+
/// [accessor]: crate::traits::accessor::Accessor
33+
pub trait MemPreserver: BasicSnippet {
34+
fn rust_shadow(
35+
&self,
36+
stack: &mut Vec<BFieldElement>,
37+
memory: &HashMap<BFieldElement, BFieldElement>,
38+
nd_tokens: VecDeque<BFieldElement>,
39+
nd_digests: VecDeque<Digest>,
40+
sponge: &mut Option<VmHasher>,
41+
) -> Vec<BFieldElement>;
42+
43+
fn pseudorandom_initial_state(
44+
&self,
45+
seed: [u8; 32],
46+
bench_case: Option<BenchmarkCase>,
47+
) -> MemPreserverInitialState;
48+
49+
fn corner_case_initial_states(&self) -> Vec<MemPreserverInitialState> {
50+
vec![]
51+
}
52+
}
53+
54+
#[derive(Debug, Clone, Default)]
55+
pub struct MemPreserverInitialState {
56+
pub stack: Vec<BFieldElement>,
57+
pub nondeterminism: NonDeterminism,
58+
pub public_input: VecDeque<BFieldElement>,
59+
pub sponge_state: Option<Tip5>,
60+
}
61+
62+
impl From<MemPreserverInitialState> for InitVmState {
63+
fn from(value: MemPreserverInitialState) -> Self {
64+
Self {
65+
stack: value.stack,
66+
nondeterminism: value.nondeterminism,
67+
public_input: value.public_input.into(),
68+
sponge: value.sponge_state,
69+
}
70+
}
71+
}
72+
73+
pub struct ShadowedMemPreserver<T: MemPreserver + 'static> {
74+
mem_preserver: Rc<RefCell<T>>,
75+
}
76+
77+
impl<T: MemPreserver + 'static> ShadowedMemPreserver<T> {
78+
pub fn new(algorithm: T) -> Self {
79+
Self {
80+
mem_preserver: Rc::new(RefCell::new(algorithm)),
81+
}
82+
}
83+
}
84+
85+
impl<T> RustShadow for ShadowedMemPreserver<T>
86+
where
87+
T: MemPreserver + 'static,
88+
{
89+
fn inner(&self) -> Rc<RefCell<dyn BasicSnippet>> {
90+
self.mem_preserver.clone()
91+
}
92+
93+
fn rust_shadow_wrapper(
94+
&self,
95+
_stdin: &[BFieldElement],
96+
nondeterminism: &NonDeterminism,
97+
stack: &mut Vec<BFieldElement>,
98+
memory: &mut HashMap<BFieldElement, BFieldElement>,
99+
sponge: &mut Option<VmHasher>,
100+
) -> Vec<BFieldElement> {
101+
self.mem_preserver.borrow().rust_shadow(
102+
stack,
103+
memory,
104+
nondeterminism.individual_tokens.to_owned().into(),
105+
nondeterminism.digests.to_owned().into(),
106+
sponge,
107+
)
108+
}
109+
110+
fn test(&self) {
111+
for (i, corner_case) in self
112+
.mem_preserver
113+
.borrow()
114+
.corner_case_initial_states()
115+
.into_iter()
116+
.enumerate()
117+
{
118+
println!(
119+
"testing {} corner case number {i}",
120+
self.mem_preserver.borrow().entrypoint(),
121+
);
122+
123+
let stdin: Vec<_> = corner_case.public_input.into();
124+
125+
test_rust_equivalence_given_complete_state(
126+
self,
127+
&corner_case.stack,
128+
&stdin,
129+
&corner_case.nondeterminism,
130+
&corner_case.sponge_state,
131+
None,
132+
);
133+
}
134+
135+
let num_states = 10;
136+
let seed: [u8; 32] = thread_rng().gen();
137+
let mut rng: StdRng = SeedableRng::from_seed(seed);
138+
for _ in 0..num_states {
139+
let seed: [u8; 32] = rng.gen();
140+
println!(
141+
"testing {} common case with seed: {:#4x?}",
142+
self.mem_preserver.borrow().entrypoint(),
143+
seed
144+
);
145+
let MemPreserverInitialState {
146+
stack,
147+
public_input,
148+
sponge_state,
149+
nondeterminism: non_determinism,
150+
} = self
151+
.mem_preserver
152+
.borrow()
153+
.pseudorandom_initial_state(seed, None);
154+
155+
let stdin: Vec<_> = public_input.into();
156+
test_rust_equivalence_given_complete_state(
157+
self,
158+
&stack,
159+
&stdin,
160+
&non_determinism,
161+
&sponge_state,
162+
None,
163+
);
164+
}
165+
}
166+
167+
fn bench(&self) {
168+
let mut rng: StdRng = SeedableRng::from_seed(
169+
hex::decode("73a24b6b8b32e4d7d563a4d9a85f476573a24b6b8b32e4d7d563a4d9a85f4765")
170+
.unwrap()
171+
.try_into()
172+
.unwrap(),
173+
);
174+
let mut benchmarks = Vec::with_capacity(2);
175+
176+
for bench_case in [BenchmarkCase::CommonCase, BenchmarkCase::WorstCase] {
177+
let MemPreserverInitialState {
178+
stack,
179+
public_input,
180+
sponge_state,
181+
nondeterminism: non_determinism,
182+
} = self
183+
.mem_preserver
184+
.borrow()
185+
.pseudorandom_initial_state(rng.gen(), Some(bench_case));
186+
let program = link_for_isolated_run(self.mem_preserver.clone());
187+
let benchmark = execute_bench(
188+
&program,
189+
&stack,
190+
public_input.into(),
191+
non_determinism,
192+
sponge_state,
193+
);
194+
let benchmark = NamedBenchmarkResult {
195+
name: self.mem_preserver.borrow().entrypoint(),
196+
benchmark_result: benchmark,
197+
case: bench_case,
198+
};
199+
benchmarks.push(benchmark);
200+
}
201+
202+
write_benchmarks(benchmarks);
203+
}
204+
}

tasm-lib/src/traits/procedure.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,13 @@ use crate::VmHasher;
3030
/// in a function (lower case f, as in 'labelled scope'); and cannot be proved as
3131
/// a standalone program.
3232
///
33-
/// See also: [closure], [function], [algorithm], [accessor]
33+
/// See also: [closure], [function], [algorithm], [accessor], [mem_preserver]
3434
///
3535
/// [closure]: crate::traits::closure::Closure
3636
/// [function]: crate::traits::function::Function
3737
/// [algorithm]: crate::traits::algorithm::Algorithm
3838
/// [accessor]: crate::traits::accessor::Accessor
39+
/// [mem_preserver]: crate::traits::mem_preserver::MemPreserver
3940
pub trait Procedure: BasicSnippet {
4041
/// Returns standard output
4142
fn rust_shadow(

0 commit comments

Comments
 (0)