Integrate the stark verifier code from the miden stdlib into the masm backend

[hackaugusto]

Currently the stark verifier code is split among the VM's stdlib and the codegen in this repo. There are a few places in the stdlib that contains hard coded values [1], which depend on the frame layout.

This issue is to move the code from the stdlib to the codegen backend, and to remove the hard coded constants in favor of computed values from the AIR. The code to evaluate the constraints goes here

1- Example PR updating said constants 0xPolygonMiden/miden-vm#976

[hackaugusto]

It would also be useful to merge the codegen configuration and the file with the address constants, since these need to be kept in sync.

[bobbinth]

I think the parts which are hard-coded right now but would need to be generated based on AirScript definitions are:

1. Number of trace columns, for both main and auxiliary segments (as mentioned in the original post).
   a. This would mean that loading of OOD frame and some other procedures would need to be generated by AirScript MASM.
2. Number of random values used by the prover after commitment to the main trace segment.
   a. This would mean that some of the procedures in random coin MASM module (or maybe the whole module) would need to be generated by AirScript MASM codegen.
3. Shape of public inputs.
   a. This would mean that the procedure which loads public inputs would need to be generated by AirScript MASM codegen.

@Al-Kindi-0 - what do you think? Also, did I miss anything?

[Al-Kindi-0]

I think the parts which are hard-coded right now but would need to be generated based on AirScript definitions are:

1. Number of trace columns, for both main and auxiliary segments (as mentioned in the original post).
   a. This would mean that loading of OOD frame and some other procedures would need to be generated by AirScript MASM.

Indeed, any thing that the DEEP queries computations depend on would be affected by the trace width. This includes the number of random values needed to compute the random linear combinations that make up the DEEP queries.

2. Number of random values used by the prover after commitment to the main trace segment.
   a. This would mean that some of the procedures in random coin MASM module (or maybe the whole module) would need to be generated by AirScript MASM codegen.

This is similar to the previous point and is also the case.

3. Shape of public inputs.
   a. This would mean that the procedure which loads public inputs would need to be generated by AirScript MASM codegen.

This makes sense.

@Al-Kindi-0 - what do you think? Also, did I miss anything?

I don't think so, maybe the proof context could also be included via the seed initialization procedure.