tasm_lib/verifier/claim/
new_recursive.rs

1use num_traits::ConstZero;
2use triton_vm::isa::op_stack::NUM_OP_STACK_REGISTERS;
3use triton_vm::prelude::*;
4
5use crate::io::InputSource;
6use crate::memory::write_words_to_memory_pop_pointer;
7use crate::prelude::*;
8use crate::verifier::claim::shared::claim_type;
9
10/// Return a pointer to a claim representing the verification of a proof of the program's own
11/// execution. Must be called with an empty stack, as the program digest is read from the bottom
12/// of the stack.
13#[derive(Debug, Copy, Clone)]
14pub struct NewRecursive {
15    input_size: usize,
16    output_size: usize,
17}
18
19impl BasicSnippet for NewRecursive {
20    fn inputs(&self) -> Vec<(DataType, String)> {
21        vec![]
22    }
23
24    fn outputs(&self) -> Vec<(DataType, String)> {
25        vec![(DataType::StructRef(claim_type()), "*claim".to_owned())]
26    }
27
28    fn entrypoint(&self) -> String {
29        "tasmlib_verifier_claim_new_recursive".to_owned()
30    }
31
32    fn code(&self, library: &mut Library) -> Vec<LabelledInstruction> {
33        let entrypoint = self.entrypoint();
34        let claim_size = Claim::new(Digest::default())
35            .with_input(vec![BFieldElement::ZERO; self.input_size])
36            .with_output(vec![BFieldElement::ZERO; self.output_size])
37            .encode()
38            .len();
39        let claim_alloc = library.kmalloc(claim_size.try_into().unwrap());
40        const METADATA_SIZE_FOR_FIELD_WITH_VEC_VALUE: usize = 2;
41        let output_field_pointer = claim_alloc.write_address();
42        let output_field_size: u32 = (1 + self.output_size).try_into().unwrap();
43        let input_field_pointer = output_field_pointer + bfe!(output_field_size + 1);
44        let input_field_size: u32 = (1 + self.input_size).try_into().unwrap();
45        let version_field_pointer = input_field_pointer + bfe!(input_field_size + 1);
46        let version_field_size = 1;
47        let digest_field_pointer = version_field_pointer + bfe!(version_field_size);
48
49        let read_output_value = InputSource::SecretIn.read_words(self.output_size);
50        let write_output_value_and_metadata = write_words_to_memory_pop_pointer(
51            self.output_size + METADATA_SIZE_FOR_FIELD_WITH_VEC_VALUE,
52        );
53        let read_input_value = InputSource::SecretIn.read_words(self.input_size);
54        let write_input_value_and_metadata = write_words_to_memory_pop_pointer(
55            self.input_size + METADATA_SIZE_FOR_FIELD_WITH_VEC_VALUE,
56        );
57        let write_version_to_memory = write_words_to_memory_pop_pointer(version_field_size);
58        let dup_own_program_digest =
59            vec![triton_asm!(dup {NUM_OP_STACK_REGISTERS - 1}); Digest::LEN].concat();
60        let write_digest_to_memory = write_words_to_memory_pop_pointer(Digest::LEN);
61
62        triton_asm!(
63            {entrypoint}:
64                // _
65
66
67                // Write output and its length indicator for the field and the length indicator for
68                // the list to memory
69                {&read_output_value}
70                push {self.output_size}
71                push {output_field_size}
72
73                push {output_field_pointer}
74                // _ [output] output_size output_field_size *output_field_size
75
76                {&write_output_value_and_metadata}
77                // _
78
79                {&read_input_value}
80                push {self.input_size}
81                push {input_field_size}
82                // _ [input] input_size input_field_size
83
84                push {input_field_pointer}
85                // _ [input] input_size input_field_size *input_field_size
86
87                {&write_input_value_and_metadata}
88                // _
89
90                push {triton_vm::proof::CURRENT_VERSION}
91                push {version_field_pointer}
92                {&write_version_to_memory}
93                // _
94
95                // Write own digest to claim. It is assumed that own program digest occupies stack
96                // words stack[15..=11]
97
98                {&dup_own_program_digest}
99                // _ d4 d3 d2 d1 d0
100
101                push {digest_field_pointer}
102                {&write_digest_to_memory}
103                // _
104
105                push {claim_alloc.write_address()}
106                // _ *claim
107
108                return
109        )
110    }
111}
112
113#[cfg(test)]
114pub mod tests {
115    use std::collections::VecDeque;
116
117    use super::*;
118    use crate::test_prelude::*;
119    use crate::verifier::claim::shared::insert_claim_into_static_memory;
120
121    #[test]
122    fn new_recursive_claim_small_params_pbt() {
123        ShadowedProcedure::new(NewRecursive {
124            input_size: Digest::LEN,
125            output_size: 0,
126        })
127        .test()
128    }
129
130    #[proptest(cases = 10)]
131    fn new_recursive_claim_pbt_pbt(
132        #[strategy(0_usize..200)] output_size: usize,
133        #[strategy(0_usize..200)] input_size: usize,
134    ) {
135        ShadowedProcedure::new(NewRecursive {
136            input_size,
137            output_size,
138        })
139        .test()
140    }
141
142    impl Procedure for NewRecursive {
143        fn rust_shadow(
144            &self,
145            stack: &mut Vec<BFieldElement>,
146            memory: &mut HashMap<BFieldElement, BFieldElement>,
147            nondeterminism: &NonDeterminism,
148            _public_input: &[BFieldElement],
149            _sponge: &mut Option<Tip5>,
150        ) -> Vec<BFieldElement> {
151            println!(
152                "nondeterminism.individual_tokens: {}",
153                nondeterminism.individual_tokens.iter().join(",")
154            );
155            let mut individual_tokens: VecDeque<BFieldElement> =
156                nondeterminism.individual_tokens.to_owned().into();
157
158            let mut output = vec![];
159            for _ in 0..self.output_size {
160                output.push(individual_tokens.pop_front().unwrap());
161            }
162            output.reverse();
163
164            let mut input = vec![];
165            for _ in 0..self.input_size {
166                input.push(individual_tokens.pop_front().unwrap());
167            }
168            input.reverse();
169
170            let program_digest = Digest::new([stack[4], stack[3], stack[2], stack[1], stack[0]]);
171
172            let claim = Claim::new(program_digest)
173                .with_input(input)
174                .with_output(output);
175            let (claim_pointer, _claim_size) = insert_claim_into_static_memory(memory, &claim);
176
177            stack.push(claim_pointer);
178
179            vec![]
180        }
181
182        fn pseudorandom_initial_state(
183            &self,
184            _: [u8; 32],
185            _: Option<BenchmarkCase>,
186        ) -> ProcedureInitialState {
187            let output = (0..self.input_size)
188                .map(|x| BFieldElement::new(x as u64))
189                .rev()
190                .collect_vec();
191            let input = (100..(100 + self.output_size))
192                .map(|x| BFieldElement::new(x as u64))
193                .rev()
194                .collect_vec();
195
196            let nondeterminism = NonDeterminism {
197                individual_tokens: [output, input].concat(),
198                ..Default::default()
199            };
200            ProcedureInitialState {
201                stack: self.init_stack_for_isolated_run(),
202                nondeterminism,
203                public_input: vec![],
204                sponge: None,
205            }
206        }
207    }
208}
tasm_lib/verifier/claim/new_recursive.rs

tasm_lib/verifier/claim/
new_recursive.rs
