Airscript bug

[skaller]

There is a bug in airscript typing a method when we have auxilliary constraints:

error[E0308]: mismatched types
  --> examples/tests/winterfell/src/example.rs:93:9
   |
90 | ...n get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxTraceRandElements<E>) -> Vec<Assertion<E>...
   |                         - this type parameter                                                                     ----------------- expected `Vec<Assertion<E>>` because of return type
91 | ...   let mut result = Vec::new();
92 | ...   result.push(Assertion::single(0, 0, self.inputs[4]));
   |                   --------------------------------------- this is of type `Assertion<winter_math::fields::f64::BaseElement>`, which causes `result` to be inferred as `Vec<Assertion<winter_math::fields::f64::BaseElement>>`
93 | ...   result
   |       ^^^^^^ expected `Vec<Assertion<E>>`, found `Vec<Assertion<BaseElement>>`
   |
   = note: expected struct `Vec<Assertion<E>>`
              found struct `Vec<Assertion<winter_math::fields::f64::BaseElement>>`

For more information about this error, try `rustc --explain E0308`.
error: could not compile `winterfell` due to previous error

Unfortunately I don't understand Rust's junky type system so I don't know how to fix this. I will note the generator also generates this correct code in another example:

    fn get_assertions(&self) -> Vec<Assertion<Felt>> {
        let mut result = Vec::new();
        result.push(Assertion::single(0, 0, self.inputs[0]));
        result.push(Assertion::single(1, 0, self.inputs[1]));
        result.push(Assertion::single(2, 0, self.inputs[2]));
        result.push(Assertion::single(3, 0, self.inputs[3]));
        result.push(Assertion::single(0, self.last_step(), self.outputs[0]));
        result.push(Assertion::single(1, self.last_step(), self.outputs[1]));
        result.push(Assertion::single(2, self.last_step(), self.outputs[2]));
        result.push(Assertion::single(3, self.last_step(), self.outputs[3]));
        result
    }

    fn get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxTraceRandElements<E>) -> Vec<Assertion<E>> {
        let mut result = Vec::new();
        result
    }

    fn evaluate_transition<E: FieldElement<BaseField = Felt>>(&self, frame: &EvaluationFrame<E>, periodic_values: &[E], result: &mut [E]) {
        let main_current = frame.current();
        let main_next = frame.next();
        result[0] = main_current[0].exp(E::PositiveInteger::from(2_u64)) - main_current[0];
        result[1] = periodic_values[0] * (main_next[0] - main_current[0]) - E::ZERO;
        result[2] = (E::ONE - main_current[0]) * (main_current[3] - main_current[1] - main_current[2]) - E::ZERO;
        result[3] = main_current[0] * (main_current[3] - main_current[1] * main_current[2]) - E::ZERO;
    }

    fn evaluate_aux_transition<F, E>(&self, main_frame: &EvaluationFrame<F>, aux_frame: &EvaluationFrame<E>, _periodic_values: &[F], aux_rand_elements: &AuxTraceRandElements<E>, result: &mut [E])
    where F: FieldElement<BaseField = Felt>,
          E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
    {
        let main_current = main_frame.current();
        let main_next = main_frame.next();
        let aux_current = aux_frame.current();
        let aux_next = aux_frame.next();
    }

The difference is that there are no aux assertions, and the stupid thing doesn't return anything (t SHOULD return an empty vector), the evaluate uses the same parameter encoding but doesn't return anything, but the main assertions uses a completely different type encoding since it has no extra arguments.

I don't understand the difference between BaseField and FieldElement nor the assignment BaseField=Felt where Felt is a synonym for winter_math::fields::f64::BaseElement.

Anyhow the bug in Airscript has to be fixed in the code generator which i can probably do if only I knew what to fix it to. It's clear the reason for the signature is that the E is required to constrain a parameter.

This bug roadblocks further progress with auxiliary constraints. I expected issues, because there is a conflct between the public inputs needed to initialise the auxiliary trace and the fact the VM just packs the aux trace in with the main trace. I also don't understand where the random values come from. At the moment the VM just reads them from an input file. The public output of the VM is the last row, which now includes the aux trace. Anyhow the airscript bug prevents reaching the bug I expected Winterfell to generate because the mainline code doesn't yet know about aux traces.

[skaller]

So this gets rid of the type error:

        result.push(Assertion::<E>::single(0, 0, self.inputs[4].into()));

I basically force the assertion type to be based on E, then coerce the argument to something or other and it worked (the compiler gave the hint to use into().

[skaller]

Hacked airscript to fix the type error: This fixes the probem:

fn get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxTraceRandElements<E>) -> Vec<Assertion<E>> {
        let mut result = Vec::new();
        result.push(Assertion::<E>::single(0, 0, self.inputs[4].into()));
        result
    }

but it creates another problem, that get_assertions doesn't have a generic parameter so I did this:

fn get_assertions(&self) -> Vec<Assertion<Felt>> {
        type E = Felt;
        let mut result = Vec::new();
        result.push(Assertion::<E>::single(0, 0, self.inputs[0].into()));
        result.push(Assertion::<E>::single(1, 0, self.inputs[1].into()));
        result.push(Assertion::<E>::single(2, 0, self.inputs[2].into()));
        result.push(Assertion::<E>::single(3, 0, self.inputs[3].into()));
        result.push(Assertion::<E>::single(0, self.last_step(), self.outputs[0].into()));
        result.push(Assertion::<E>::single(1, self.last_step(), self.outputs[1].into()));
        result.push(Assertion::<E>::single(2, self.last_step(), self.outputs[2].into()));
        result.push(Assertion::<E>::single(3, self.last_step(), self.outputs[3].into()));
        result
    }

because a single function is used to generate getting assertions, and since it now forces the type to E, and get_assertions won't accept a generic, I had to add the line

        type E = Felt;

to it so E is defined. It compiles now!