Winterfell main automation

[skaller]

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.

[skaller]

Note: it would be better again if the same file exactly could be used, for this would allow Winterfell to be compiled to binary once and for all.

[skaller]

OK so to simplify things here's the plan:

1. Airscript name has to be AirType.
2. Public inputs and outputs must be named inputs and outputs
3. inputs and outputs must be the first and last row in order
4. The AirType will use vectors not arrays.

This means the main.rs will be the same for all tests so there is no need (or possibility) of writing it by hand. It remains to confirm this works.

Public values that aren't the first and last rows are nonsense anyhow. For some VM some columns might be initialised to fixed values, so just use the right values. The public inputs will now be the same as the values required to initialise the VM, and the outputs will be the last row,

So "No RUST REQUIRED".

The actual subroutines are of course still generated so Winterfell still has to be recompiled at this point.

[skaller]

Done