feat: Handle aux boundary values

[Leo-Besancon]

This PR aims to close #17.
It adds the access of aux final values in the MidenAirBuilder.

Currently, the tests in Plonky3 fails as the FibPermAir Air is not built on the same assumptions than the AirScript codegen.

Notes:

• This work is based on the branch corresponding to PR feat: add fri params suitable for miden proving #19, so it also contains its commits.
• We assume that whenever we work with buses, the Air contains constraints to make sure that the values given by the prover are the correct one. For instance, for each bus, we should have a constraint such as:

  builder.when_last_row().assert_zero_ext(AB::ExprEF::from(aux_current[0].clone().into()) - aux_bus_boundary_values[0].into());

This means that it should not be needed to commit to the values. If the prover lies on values it provides, the constraints should not be verified.

• For now, we do not handle variable-length public inputs.

[Al-Kindi-0]

Looks great!
As you said, it would be great to add support for variable-length public inputs.
A couple of things worth thinking about:

1. Since we are focusing on the Miden use-case for now, should we make the addition of the boundary constraints, using the provided boundary values, automatic ?
2. I believe we should include the values sent by the prover to the verifier into the Fiat-Shamir transcript.
3. The equality check is not necessary for soundness, at least in the current setup, as long as we have the boundary constraints from point 1 above.

[Leo-Besancon]

Hi @Al-Kindi-0, putting it in review as I now have:

• existing tests that pass on Plonky3 (basically, bus boundary values are not checked if we do not provide bus_types in the Air. We could also toggle this behaviour from an argument to the verify function instead if you think it's better practice
• include the aux_finals values in the transcript (afff307)
• handle variable length public inputs in 38ef4fa. On this front, I've tested them on Add bus types and variable length public inputs to Plonky3 backend tests air-script#525 (and in particular the following test that provides var len pub inputs that are checked: https://github.com/0xMiden/air-script/blob/c01c7ea3d63863efaecf208b2ec9b6747eca9402/air-script/src/tests/buses/test_air_plonky3_varlen_boundary_last.rs)

Since we are focusing on the Miden use-case for now, should we make the addition of the boundary constraints, using the provided boundary values, automatic ?

This is already handled in the AirScript codegen: for each bus, two constraints are automatically included in the graph:

• that the bus is empty in the first row
• that the bus equals the corresponding aux_bus_boundary_values value in the last row

I'll check what can be done in the prover / verifier side.

[Leo-Besancon]

Hello again @Al-Kindi-0

1. Since we are focusing on the Miden use-case for now, should we make the addition of the boundary constraints, using the provided boundary values, automatic ?

I have not yet put it on the branch of this PR, but could you look at this commit: 0a5752b

It basically wraps the air provided in the prove and verify functions into a MidenAir that delegates everything to the air, but adds the bus boundary constraintss automatically.

I've tested it in AirScript and it works well (in the test_air_plonky3_varlen_boundary_last.rs test, if I remove the codegen boundary constraints but provide inconsistant variable length public inputs, the verification fails as expected).

Some caveats is that we could have duplicated constraints (so we would need to remove the boundary handling from the codegen). What do you think?

[adr1anh]

Looks good!

[Al-Kindi-0]

Looks great, thank you Leo!
Left a few questions and nits (but I think I found the answer by the end of the review for the most important one)