starkoracles / air-script Goto Github PK

To make them work, constraint evaluation expressions have been decomposed into 3 address code and single assignment form which is hard to read and associate with the original airscript formulae.

Add a comment with the constraint compactly expressed in a form similar to the original source code.

This requires rejigging the test setup, the new version uses a different kind of "toml" file.

Protostar is currently out of date. In addition it is not clear how it finds the files to process.
In order to run multiple test cases it would be useful if we could control this with a command
line parameter rather than copying files about.

Decide how to do this and do it.
Will require deciding

1. file layout
2. file name
3. modify test VM to output it
4. modify Winterfell main to read it

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.

The test\input\example_vm.flx file needs to output public value file.

This is a problem because it also needs to input the input values.

This particular VM is only a small test hack, but in general, a VM needs to

1. input the input public values
2. Output the trace
3. Output the result values

In some cases we could separate the input and output public values into two files,
so the VM doesn't have to duplicate them. However in this test case the inputs
are hard coded (at the moment). So the VM has to write the input file.

Previously the trace used standard output. That won't work for multiple files
so we have to now use command line arguments.

The VM has two inputs:

1. the public input file
2. Command line switches

We could run the VM for multiple trace lengths using a command line switch.

1. Add @starkoracles library.
2. Convert computations to use it.

Currently, Winterfell prover requires extracting the public data from the trace.
For this to be possible, the map from public inputs to the first row, and map
of outputs to the last row, must each be invertible.

The simplest case of this is probably the ONLY reasonable one: each public input
must correspond to one trace column, similarly for outputs. Possible some input
columns are not mapped to so they must be hard initialised. Some outputs
columns may be of no interest.

The correspondences can be specified like this:

0-2 1-3 2-0

which says public input 0 goes to column 2, input1 goes to 3, and input 2 goes to 0.
So we can use this information to completely automate get_pub_inputs which currently looks like this:

   fn get_pub_inputs(&self, trace: &Self::Trace) -> PublicInputs {
        let mut inputs = [Felt::ONE; 3];
        inputs[0] = trace.get(1, 0); // a
        inputs[1] = trace.get(2, 0); // b
        inputs[2] = trace.get(3, 0); // c

        let mut outputs = [Felt::ONE; 3];
        let last_step = trace.length() - 1; // why is this 2?
        outputs[0] = trace.get(1, last_step); // a
        outputs[1] = trace.get(2, last_step); // b
        outputs[2] = trace.get(3, last_step); // c
        PublicInputs::new(inputs, outputs)
    }

Notice this code does not need to know the names of the variables in PublicInputs: inputs and outputs are local variables.

This function:

  /// Builds an execution trace of the air
    pub fn build_trace(&self, table_f: &str) -> TraceTable<Felt> {

        let table_data = load_file(table_f);
        let vwords = parse_lines(table_data); 
        let nrows = vwords.len();
        let ncols = vwords[0].len();

        println!("Trace length {:?}",nrows);
        assert!(
            nrows.is_power_of_two(),
            "sequence length must be a power of 2"
        );

        println!("Trace width {:?}",ncols);
        println!("DATA {:?}",vwords);
        let mut tab = Vec::<Vec::<Felt>>::new();
        for colix in 0..ncols {
          let mut col = Vec::<Felt>::new();
          for rowix in 0..nrows {
            col.push(Felt::from(vwords[rowix][colix]));   
          }
          tab.push(col);
        }
        TraceTable::init(tab)
    }

is already invariant (i.e. the same function will work in all cases).

It remains to find any further variants such as the AirName, and then make the test harness
generate this file.

• Demarcate differences between prover, codegen, verifier and which values they can share

This file

(https://github.com/ZeroSync/ZeroSync/blob/main/src/stark_verifier/air/air_instance.cairo)

contains a function air_instance_new which is cairo specific. We need to generate this function for the airscript we are working on. Our function must be called instead of the one in that file. The rest of the code in the file appears generic.

So how do these work?

combine all constraint evaluations into a single value

The test script now runs multiple tests but all the output just gets dumped to standard output.
Also annoyingly cargo/rust builds dump crap to standard error.

What we want to see is just a list of tests as they're run, and if they're successful or failed.
If they failed, some indication at what stage. Then we consult the appropriate log.

The test harness may not currently able to run an arbitrary test case.
We need to add extra test cases and be able to select which one to run.

In https://github.com/starkoracles/winterfell/blob/air-script/air/src/air/divisor.rs#L67
the following comment:

    /// Builds a divisor for a boundary constraint described by the assertion.
    ///
    /// For boundary constraints, the divisor polynomial is defined as:
    ///
    /// $$
    /// z(x) = x^k - g^{a \cdot k}
    /// $$
    ///
    /// where $g$ is the generator of the trace domain, $k$ is the number of asserted steps, and
    /// $a$ is the step offset in the trace domain. Specifically:
    /// * For an assertion against a single step, the polynomial is $(x - g^a)$, where $a$ is the
    ///   step on which the assertion should hold.

specified the divisor polynomial for boundary constraints.

Our test constraints assert only one step, so the special case applies.
SInce we have 8 trace rows, a=7 and the polymomial becomes:

(x-g^7)

Our g has value

trace_domain_generator: 16777216

which is taken from the Winterfell Rust test log.
x is given by"

x: 3883415319251994391

also from those logs. Using Python:

>>> g = 16777216
>>> f64 = pow(2,64) - pow(2,32) + 1
>>> x = 3883415319251994391
>>> g7 = pow(g,7) % f64
>>> p = (x - g7) % f64
>>> p
3883416418763621911

Note Python uses the correct Euclidean division operation (unlike most other languages including C and Rust which round the quotient towards 0).

Unfortunately, our tests fail to agree with Winterfell logs, unless we do:

s = s + "let last_z =  3883696794228705047;\n";

in https://github.com/starkoracles/air-script/blob/main/codegen/cairo0/src/lib.rs#L208

The actual Rust code used to calculate the divisor polynomial is at
https://github.com/starkoracles/winterfell/blob/air-script/air/src/air/divisor.rs#L98

            let trace_offset = num_steps * assertion.first_step;
            let offset = get_trace_domain_value_at::<B>(trace_length, trace_offset);
            Self::new(vec![(num_steps, offset)], vec![])

which agrees with the comments. In particular offset is just g^7. See
https://github.com/starkoracles/winterfell/blob/air-script/air/src/air/divisor.rs#L11
for a description of the encoding schema.

My cairo code evaluated the polynomial directly:

       s = s + "  let v1 = sub_g(trace_length, 1);\n";
       s = s + "  let v2 = pow_g(g, v1);\n";
       s = s + "  let last_z = sub_g(x, v2);\n"; // (x - g^(trace_length-1))
       s = s + "  %{\n";
       s = s + "    print('CAIRO DIVISORS (simple)',ids.first_z, ids.last_z)\n";
       s = s + "  %}\n";

which agrees with the Python result. Winterfell actually uses the more efficient and general calculation:

    pub fn evaluate_at<E: FieldElement<BaseField = B>>(&self, x: E) -> E {
        // compute the numerator value
        let mut numerator = E::ONE;
        for (degree, constant) in self.numerator.iter() {
            let v = x.exp((*degree as u32).into());
            let v = v - E::from(*constant);
            numerator *= v;
        }

        // compute the denominator value
        let denominator = self.evaluate_exemptions_at(x);

        numerator / denominator
    }

which can be found at
https://github.com/starkoracles/winterfell/blob/air-script/air/src/air/divisor.rs#L130

Note the REALLY BAD coding where numerator is the local variable and self.numerator comes from the trait.
However the code seems correct and should yield the same value as the naive calculation when the number of steps is one. The representation should be [1,g^7] for the numerator and [] for the denominator.

I have no idea at this time what the problem is. To me it looks like a bug in Winterfell. The only
computation i have not checked is the evaluation of the generator g (since I used the supplied one).