Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system.
It would be very convenient if it was somehow possible to extract a FRI proof, or probably a FRI proof stream from a STARK proof (or a STARK proof stream).
I wrote this functionality in order to be able to derive the correct non-deterministic digests from a STARK-proof. So I guess it's possible to think of this problem in a more generic way: Is it possible to derive NonDeterminism from a STARK proof? This derived NonDeterminism would of course be specific to a function (Program in the TASM sense) since each program can decide where to get its cryptographic data: from initialized memory, from the digests input, or from the individual_tokens input. So perhaps it actually belongs wherever the relevant program is being written? In that case, this functionality belongs in tasm-lang where we are currently developing the recursive verifier.
See 404b1688 for my current work-around to this problem.
It would be very convenient if it was somehow possible to extract a FRI proof, or probably a FRI proof stream from a STARK proof (or a STARK proof stream).
I wrote this functionality in order to be able to derive the correct non-deterministic digests from a STARK-proof. So I guess it's possible to think of this problem in a more generic way: Is it possible to derive
NonDeterminismfrom a STARK proof? This derivedNonDeterminismwould of course be specific to a function (Programin the TASM sense) since each program can decide where to get its cryptographic data: from initialized memory, from thedigestsinput, or from theindividual_tokensinput. So perhaps it actually belongs wherever the relevant program is being written? In that case, this functionality belongs intasm-langwhere we are currently developing the recursive verifier.See 404b1688 for my current work-around to this problem.