pub trait Procedure: BasicSnippet {
// Required methods
fn rust_shadow(
&self,
stack: &mut Vec<BFieldElement>,
memory: &mut HashMap<BFieldElement, BFieldElement>,
nondeterminism: &NonDeterminism,
public_input: &[BFieldElement],
sponge: &mut Option<VmHasher>,
) -> Vec<BFieldElement>;
fn pseudorandom_initial_state(
&self,
seed: [u8; 32],
bench_case: Option<BenchmarkCase>,
) -> ProcedureInitialState;
// Provided methods
fn preprocess<T: BFieldCodec>(
_meta_input: T,
_nondeterminism: &mut NonDeterminism,
) { ... }
fn corner_case_initial_states(&self) -> Vec<ProcedureInitialState> { ... }
}
Expand description
A trait that can modify all parts of the VM state.
A Procedure is a piece of tasm code that can do almost anything: modify stack, read from and write to memory, take in nondeterminism, and read and write from standard input/output. What it cannot do is stand alone. In other words, it is still wrapped in a function (lower case f, as in ‘labelled scope’); and cannot be proved as a standalone program.
See also: closure, function, algorithm, read_only_algorithm, accessor, mem_preserver
Required Methods§
Sourcefn rust_shadow(
&self,
stack: &mut Vec<BFieldElement>,
memory: &mut HashMap<BFieldElement, BFieldElement>,
nondeterminism: &NonDeterminism,
public_input: &[BFieldElement],
sponge: &mut Option<VmHasher>,
) -> Vec<BFieldElement>
fn rust_shadow( &self, stack: &mut Vec<BFieldElement>, memory: &mut HashMap<BFieldElement, BFieldElement>, nondeterminism: &NonDeterminism, public_input: &[BFieldElement], sponge: &mut Option<VmHasher>, ) -> Vec<BFieldElement>
Returns standard output
fn pseudorandom_initial_state( &self, seed: [u8; 32], bench_case: Option<BenchmarkCase>, ) -> ProcedureInitialState
Provided Methods§
fn preprocess<T: BFieldCodec>( _meta_input: T, _nondeterminism: &mut NonDeterminism, )
fn corner_case_initial_states(&self) -> Vec<ProcedureInitialState>
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.