Skip to main content

triton_vm/
proof.rs

1use arbitrary::Arbitrary;
2use get_size2::GetSize;
3use isa::program::Program;
4use serde::Deserialize;
5use serde::Serialize;
6use twenty_first::prelude::*;
7
8use crate::error::ProofStreamError;
9use crate::proof_stream::ProofStream;
10
11/// A version tag for the combination of Triton VM's
12/// [instruction set architecture (ISA)][isa] as well as the
13/// [STARK proof system][crate::stark::Stark].
14/// This version changes whenever either of the two changes.
15///
16/// # Rationale
17///
18/// A change in the ISA might give a [`Program`] a new meaning, and an existing
19/// proof might erroneously attest to the “new” program's graceful halt. By
20/// bumping this version when changing the ISA, the old proof is surely invalid
21/// under the new version. If the program's meaning has not changed, or the new
22/// meaning is accepted, a new proof can be generated.
23///
24/// A change in the STARK proof system generally means that the verifier has to
25/// perform different operations to verify a proof. This means that existing
26/// proofs about some program _should_ be accepted as valid, but (generally) are
27/// not. This version helps to make the discrepancy explicit.
28///
29/// Note that proofs remain valid for their matching versions indefinitely.
30///
31/// This version is separate from the crate's semantic version to allow software
32/// upgrades with no semantic changes to both, the ISA and the proof system.
33pub const CURRENT_VERSION: u32 = 5;
34
35/// Contains the necessary cryptographic information to verify a computation.
36/// Should be used together with a [`Claim`].
37#[derive(Debug, Clone, Eq, PartialEq, Serialize, Deserialize, GetSize, BFieldCodec, Arbitrary)]
38pub struct Proof(pub Vec<BFieldElement>);
39
40impl Proof {
41    /// Get the height of the trace used during proof generation.
42    /// This is an upper bound on the length of the computation this proof is
43    /// for. It is one of the main contributing factors to the length of the
44    /// FRI domain.
45    pub fn padded_height(&self) -> Result<usize, ProofStreamError> {
46        let mut log_2_padded_heights = ProofStream::try_from(self)?
47            .items
48            .into_iter()
49            .filter_map(|item| item.try_into_log2_padded_height().ok());
50
51        let log_2_padded_height = log_2_padded_heights
52            .next()
53            .ok_or(ProofStreamError::NoLog2PaddedHeight)?;
54        if log_2_padded_heights.next().is_some() {
55            return Err(ProofStreamError::TooManyLog2PaddedHeights);
56        }
57
58        Ok(1 << log_2_padded_height)
59    }
60}
61
62/// Contains the public information of a verifiably correct computation.
63/// A corresponding [`Proof`] is needed to verify the computation.
64/// One additional piece of public information not explicitly listed in the
65/// [`Claim`] is the `padded_height`, an upper bound on the length of the
66/// computation. It is derivable from a [`Proof`] by calling
67/// [`Proof::padded_height()`].
68#[derive(
69    Debug, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, GetSize, BFieldCodec, Arbitrary,
70)]
71pub struct Claim {
72    /// The hash digest of the program that was executed. The hash function in
73    /// use is [`Tip5`].
74    pub program_digest: Digest,
75
76    /// The version of the Triton VM instruction set architecture the
77    /// [`program_digest`][digest] is about, as well as of the STARK proof
78    /// system in use. See also: [`CURRENT_VERSION`].
79    ///
80    /// [digest]: Self::program_digest
81    pub version: u32,
82
83    /// The public input to the computation.
84    pub input: Vec<BFieldElement>,
85
86    /// The public output of the computation.
87    pub output: Vec<BFieldElement>,
88}
89
90impl Claim {
91    /// Create a new Claim.
92    ///
93    /// Assumes the version to be [`CURRENT_VERSION`]. The version can be
94    /// changed with method [`about_version`][Self::about_version].
95    pub fn new(program_digest: Digest) -> Self {
96        Self {
97            program_digest,
98            version: CURRENT_VERSION,
99            input: vec![],
100            output: vec![],
101        }
102    }
103
104    #[must_use]
105    pub fn about_program(program: &Program) -> Self {
106        Self::new(program.hash())
107    }
108
109    #[must_use]
110    pub fn with_input(mut self, input: impl Into<Vec<BFieldElement>>) -> Self {
111        self.input = input.into();
112        self
113    }
114
115    #[must_use]
116    pub fn with_output(mut self, output: Vec<BFieldElement>) -> Self {
117        self.output = output;
118        self
119    }
120
121    #[must_use]
122    pub fn about_version(mut self, version: u32) -> Self {
123        self.version = version;
124        self
125    }
126}
127
128#[cfg(test)]
129#[cfg_attr(coverage_nightly, coverage(off))]
130mod tests {
131    use assert2::assert;
132    use proptest::collection::vec;
133    use proptest::prelude::*;
134    use proptest_arbitrary_adapter::arb;
135    use rand::prelude::*;
136
137    use crate::prelude::*;
138    use crate::proof_item::ProofItem;
139    use crate::tests::proptest;
140    use crate::tests::test;
141
142    use super::*;
143
144    impl Default for Claim {
145        /// For testing purposes only.
146        fn default() -> Self {
147            Self::new(Digest::default())
148        }
149    }
150
151    #[macro_rules_attr::apply(test)]
152    fn claim_accepts_various_types_for_public_input() {
153        let _claim = Claim::default()
154            .with_input(bfe_vec![42])
155            .with_input(bfe_array![42])
156            .with_input(PublicInput::new(bfe_vec![42]));
157    }
158
159    #[macro_rules_attr::apply(proptest)]
160    fn decode_proof(#[strategy(arb())] proof: Proof) {
161        let encoded = proof.encode();
162        let decoded = *Proof::decode(&encoded).unwrap();
163        prop_assert_eq!(proof, decoded);
164    }
165
166    #[macro_rules_attr::apply(proptest)]
167    fn decode_claim(#[strategy(arb())] claim: Claim) {
168        let encoded = claim.encode();
169        let decoded = *Claim::decode(&encoded).unwrap();
170        prop_assert_eq!(claim, decoded);
171    }
172
173    #[macro_rules_attr::apply(proptest(cases = 10))]
174    fn proof_with_no_padded_height_gives_err(#[strategy(arb())] root: Digest) {
175        let mut proof_stream = ProofStream::new();
176        proof_stream.enqueue(ProofItem::MerkleRoot(root));
177        let proof: Proof = proof_stream.into();
178        let maybe_padded_height = proof.padded_height();
179        assert!(maybe_padded_height.is_err());
180    }
181
182    #[macro_rules_attr::apply(proptest(cases = 10))]
183    fn proof_with_multiple_padded_height_gives_err(#[strategy(arb())] root: Digest) {
184        let mut proof_stream = ProofStream::new();
185        proof_stream.enqueue(ProofItem::Log2PaddedHeight(8));
186        proof_stream.enqueue(ProofItem::MerkleRoot(root));
187        proof_stream.enqueue(ProofItem::Log2PaddedHeight(7));
188        let proof: Proof = proof_stream.into();
189        let maybe_padded_height = proof.padded_height();
190        assert!(maybe_padded_height.is_err());
191    }
192
193    #[macro_rules_attr::apply(proptest)]
194    fn decoding_arbitrary_proof_data_does_not_panic(
195        #[strategy(vec(arb(), 0..1_000))] proof_data: Vec<BFieldElement>,
196    ) {
197        let _proof = Proof::decode(&proof_data);
198    }
199
200    #[macro_rules_attr::apply(test)]
201    fn current_proof_version_is_still_current() {
202        let program = triton_program! {
203            pick 11 pick 12 pick 13 pick 14 pick 15
204            read_io 5 assert_vector halt
205        };
206        let claim = Claim::about_program(&program).with_input(program.hash());
207
208        let input = claim.input.clone().into();
209        let non_determinism = NonDeterminism::default();
210        let (aet, _) = VM::trace_execution(program, input, non_determinism).unwrap();
211
212        let mut rng = StdRng::seed_from_u64(4742841043836029231);
213        let proof = Prover::default()
214            .set_randomness_seed_which_may_break_zero_knowledge(rng.random())
215            .prove(&claim, &aet)
216            .unwrap();
217
218        insta::assert_snapshot!(
219            Tip5::hash(&proof),
220            @"12433316667267448296,\
221            16303325689818214404,\
222            05753433865704583134,\
223            08721639214652157404,\
224            16062979541634131777",
225        );
226    }
227}