TritonVM / triton-vm

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.
https://triton-vm.org
Apache License 2.0
247 stars 37 forks source link

Output values are multiplied by `2**32-1` #307

Closed chancehudson closed 4 months ago

chancehudson commented 4 months ago

Hi, I've run into a strange thing. I'm proving the following program:

push 0
push 1337
write_io 1
halt

I get the following:

Stark { security_level: 160, fri_expansion_factor: 4, num_trace_randomizers: 166, num_collinearity_checks: 80, num_combination_codeword_checks: 160 }
Claim { program_digest: Digest([BFieldElement(11255392571129683947), BFieldElement(13719496134677853561), BFieldElement(14136027283438667658), BFieldElement(13258940694832340512), BFieldElement(6761981634964174787)]), input: [], output: [BFieldElement(5742371273415)] }

Note that the output is a single element 5742371273415 which == 1337 * (2^32-1). When I test outputing a larger value like 2^50 + 1337 the output is ((2^50 + 1337)*(2^32-1)) % (2^64 - 2^32 + 1) = 5742371011271. I think it's possible to generally unwrap the output by multiplying by the modular inverse of 2^32 - 1.

I want to confirm if this is intended behavior, or if I'm improperly handling output.

Thanks

aszepieniec commented 4 months ago

BFieldElements are internally represented in Montgomery form. You see the Montgomery form with debug formatting. However, BFieldElement also implements Display, which produces a string which hides the Montgomery cofactor. Alternatively, you can use .value() which divides out the Montgomery factor before returning the u64 you would expect.

chancehudson commented 4 months ago

Ah gotcha, thanks!