Improvements to Alan's new traits

[Sword-Smith]

@aszepieniec's traits BasicSnippet, Closure Function etc. gets a lot of things right, and is an improvement over the trait that is now called DeprecatedSnippet by deriving the snippet's net-effect on the stack, by better annotation of input and outputs (on stack), by returning Vec<LabeledInstruction> instead of String and by more clearly defining what part of the VM state that the snippet may change (as differentiated by Closure, Function, Algorithm, and Procedure).

The new traits, however, do not allow for extensive corner-case testing, where the rust_shadowing and the Triton VM execution are verified to be equivalent. The problem is that the implementer of the trait can only define stochastic initial states or define just a single initial state. Very often the implementer would want to define multiple initial states that function as corner-case testing, as well as auto-generated initial states.

How do we adjust the traits to allow this?

[Sword-Smith]

My suggestion is to add a trait function unit_test_initial_states that returns a collection of initial states that can then all be used to verify rust-shadowing/TVM equivalence. But there might be other ways of achieving the same.

[aszepieniec]

I would propose to rewrite the current function

    fn pseudorandom_initial_state(
        &self,
        seed: [u8; 32],
        bench_case: Option<BenchmarkCase>,
    ) -> (
        Vec<BFieldElement>,
        HashMap<BFieldElement, BFieldElement>,
        NonDeterminism<BFieldElement>,
        Vec<BFieldElement>,
        VmHasherState,
    );

as

    fn generate_initial_states(
        &self,
        test_case: TestCase,
    ) -> Vec<Procedure::InitialState>;

where

• Procedure should be generalized across {Procedure, Algorithm, Closure, Function}.
• Procedure::InitialState is a trait member type and wraps the rather complex current return tuple. Algorithm::InitialState, Closure::InitialState, etc. define different tuples.
• The return type has been upgraded from a single tuple to a vector of tuples.
• TestCase is an enum with members:
  • Pseudorandom([u8;32]) where the associated data is the seed
  • Corner
  • AverageBench
  • WorstBench.

[aszepieniec]

My suggestion is to add a trait function unit_test_initial_states that returns a collection of initial states that can then all be used to verify rust-shadowing/TVM equivalence.

I dislike this proposal because it adds a new function for logic that is very similar to what is already there. There is already special-casing based on whether BenchCase is Some and which variant it is if it is Some. This proposal strikes an ugly middle point on a spectrum whose two end points are architecturally sound, namely:

• keep similar logic inside one function and special case within that one function as needed; and
• special case into different functions to keep functions small and maintainable.

[Sword-Smith]

The drawback of the TestCase suggestion is that the bench variants of the TestCase enum should only return a single initial state, whereas Corner should return a collection. And Pseudorandom? Probably just one, right?

So you take information that could be checked at compile-time with a different trait and force the wrapper-code to make these checks at run-time -- that generate_initial_states returns a single initial state when called with the TestCase::AverageBench argument.

To me, your suggestion confuses what we want the trait to do with internal logic -- that a lot of initial state building will share logic, what might seem convenient for the developer. The latter fact should not influence the trait definition, I believe.

If e.g. the Closure trait was expanded with a corner_case_initial_states function with a default implementation, the paranoid tester (me) could add corner-case tests without a big rewrite. But it's also a possibility that we don't have a default implementation and that the developer can just have the function return the empty vector if they so wish.

[Sword-Smith]

To show an example:

With the above suggestion of adding a corner_case_initial_states with a default implementation to the Closure trait, the Closure implementation of u32's safepow could look like this:

impl Closure for Safepow {
    fn rust_shadow(&self, stack: &mut Vec<triton_vm::BFieldElement>) {
        let exp: u32 = stack.pop().unwrap().try_into().unwrap();
        let base: u32 = stack.pop().unwrap().try_into().unwrap();
        stack.push(BFieldElement::new(base.pow(exp) as u64));
    }

    fn pseudorandom_initial_state(
        &self,
        seed: [u8; 32],
        bench_case: Option<crate::snippet_bencher::BenchmarkCase>,
    ) -> Vec<triton_vm::BFieldElement> {
        let (base, exponent): (u32, u32) = match bench_case {
            Some(BenchmarkCase::CommonCase) => (10, 5),
            Some(BenchmarkCase::WorstCase) => (2, 31),
            None => {
                let mut seeded_rng = StdRng::from_seed(seed);
                let base: u32 = seeded_rng.gen_range(0..0x10);
                let exponent: u32 = seeded_rng.gen_range(0..0x8);
                (base, exponent)
            }
        };

        [
            empty_stack(),
            vec![
                BFieldElement::new(base as u64),
                BFieldElement::new(exponent as u64),
            ],
        ]
        .concat()
    }

    fn corner_case_initial_states(&self) -> Vec<Vec<BFieldElement>> {
        let zero_pow_zero = [
            empty_stack(),
            vec![BFieldElement::new(0), BFieldElement::new(0)],
        ]
        .concat();

        vec![zero_pow_zero]
    }
}

A few open questions remain though:

• Do we want to be able to use the trait functions to declare initial states that should crash the VM? If so, how?
• If we add corner_case_initial_states, do we then want to keep the benchmark generation in pseudorandom_initial_state? I'm actually leaning towards a "yes" since both the pseudo-random initial states and the benchmarking initial states should just return a single initial state, whereas you should be able to declare multiple corner-case initial states.

[Sword-Smith]

This was implemented for Closure on a branch here: https://github.com/TritonVM/tasm-lib/commit/57d580ffc816150606a96e6795da4f1cc6faf246

[aszepieniec]

Arguing from general and weakly held subjective opinions: encoding special-casing into traits based on whether a segment of code should return one thing or a collection of things, is a criterion that strikes me as introducing unnecessary complexity. It is not a big deal to operate with lists of things when those lists are known to contain only one item. As a rule, traits should be as simple as possible.

That said,

• general principles can have exceptions,
• extending a trait definition with a function that has a default implementation returning vec![] is a robust way to tame complexity.

Let's go with your suggestion.