harness: public data about air-script

[skaller]

There is a design fault in airscript that it propagates public variable names:

public_inputs:
    stack_inputs: [16]
    stack_outputs: [16]

The actual Rust IR contains these names.

pub enum Value {
    BoundConstant(SymbolAccess),
    InlineConstant(u64),
    TraceElement(TraceAccess),
    PeriodicColumn(usize, usize),

    /// An identifier for a public input declared by the specified name and accessed at the
    /// specified index.
    PublicInput(String, usize), // <<----------------------------------

    RandomValue(usize),
}

The generated rust verifier contains

pub struct PublicInputs {
    stack_inputs: [Felt; 16],
    stack_outputs: [Felt; 16],
}

impl PublicInputs {
    pub fn new(stack_inputs: [Felt; 16], stack_outputs: [Felt; 16]) -> Self {
        Self { stack_inputs, stack_outputs }
    }
}

pub struct ExampleAir {
    context: AirContext<Felt>,
    stack_inputs: [Felt; 16],
    stack_outputs: [Felt; 16],
}

These are then used in the constraint evaluation:

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

However Winterfell itself cannot know these, instead, the public values are a single vector:

impl Serializable for PublicInputs {
    fn write_into<W: ByteWriter>(&self, target: &mut W) {
        target.write(self.stack_inputs.as_slice());
        target.write(self.stack_outputs.as_slice());
    }
}

impl ToElements<Felt> for PublicInputs {
    fn to_elements(&self) -> Vec<Felt> {
        let mut result = Vec::new();
        result.extend_from_slice(&self.stack_inputs);
        result.extend_from_slice(&self.stack_outputs);
        result
    }
}

The hand written Winterfell mainline uses fixed sample public values:

    fn get_pub_inputs(&self, trace: &Self::Trace) -> PublicInputs {
        // based on air, c = a * b and therefore all 1s
        let inputs = [Felt::ONE; 16];
        let mut outputs = [Felt::ONE; 16];
        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)
    }

THIS CODE WILL BE MODIFIED as part of this issue to actually read the public input data from a file.
Keep track of this .. read on...

The generated verifier is called:

verify::<ExampleAir, Blake3_192<Felt>, DefaultRandomCoin<Blake3_192<Felt>>>(proof, pub_inputs)

However the prover does NOT seem to require the public inputs. How can it? Winterfell itself is fixed Rust code, it cannot know about stack_inputs and stack_output names. It just gets a single vector of values (if that?). Actually the method get_pub_inputs called here:

    let pub_inputs = prover.get_pub_inputs(&trace);

is NOT used by the prover at all. i know because I changed it's interface and everything still compiled.

So the issue is we want to REMOVE these names, names have no place in the calculations.
Airscript is a compiler its JOB is to REPLACE NAMES WITH NUMBERS.

It is not doing its job correctly. This is because of the non-professional mindset of Rust developers.
Winterfell should be a BINARY PROGRAM not a text library that has to be recompiled with every different input, and the airscript IR similarly should contain NO NAMES except for debugging (for example the Air name itself).

It's OK to generated code, in fact the constraint evaluator has to be generated, but it should be compiled to binary and linked to Winterfell.

Everything else is done by numbers. For examples constraints are not named, they're numbered (implicitly) and located in the AirGraph by number. Public values should be identified the same way.

This applies to "constants" too. We don't want any names, we just want the numbers.

Now the RELEVANCE of all this is that I have to generated a file containing the public inputs to be used for a test run (as well as the trace) because the constraint evaluation at least depends on them, and the Winterfell proof/verification at least needs a hash of them.

The problem is, the public.values can ONLY contain numbers, so the fixed routine which reads them cannot have any knowledge of names.

So to make the existing code work correctly, a generated "unpacker" is needed.

Eventually airscipt should be fixed.

[skaller]

So .. i'll output multiple rows of numbers like this:

1 2 3 4
6 7 8 9 23

corresponding in sequence to the airscript decls. That fixes the file format.

[skaller]

Full automation now.