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 parameters(&self) -> Vec<(DataType, String)> {
21        vec![]
22    }
23
24    fn return_values(&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    #[macro_rules_attr::apply(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    #[macro_rules_attr::apply(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        ) -> Result<Vec<BFieldElement>, RustShadowError> {
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                let front_token = individual_tokens
161                    .pop_front()
162                    .ok_or(RustShadowError::StackUnderflow)?;
163                output.push(front_token);
164            }
165            output.reverse();
166
167            let mut input = vec![];
168            for _ in 0..self.input_size {
169                let front_token = individual_tokens
170                    .pop_front()
171                    .ok_or(RustShadowError::StackUnderflow)?;
172                input.push(front_token);
173            }
174            input.reverse();
175
176            let program_digest = Digest::new([stack[4], stack[3], stack[2], stack[1], stack[0]]);
177
178            let claim = Claim::new(program_digest)
179                .with_input(input)
180                .with_output(output);
181            let (claim_pointer, _claim_size) = insert_claim_into_static_memory(memory, &claim);
182
183            stack.push(claim_pointer);
184
185            Ok(Vec::new())
186        }
187
188        fn pseudorandom_initial_state(
189            &self,
190            _: [u8; 32],
191            _: Option<BenchmarkCase>,
192        ) -> ProcedureInitialState {
193            let output = (0..self.input_size)
194                .map(|x| BFieldElement::new(x as u64))
195                .rev()
196                .collect_vec();
197            let input = (100..(100 + self.output_size))
198                .map(|x| BFieldElement::new(x as u64))
199                .rev()
200                .collect_vec();
201
202            let nondeterminism = NonDeterminism {
203                individual_tokens: [output, input].concat(),
204                ..Default::default()
205            };
206            ProcedureInitialState {
207                stack: self.init_stack_for_isolated_run(),
208                nondeterminism,
209                public_input: vec![],
210                sponge: None,
211            }
212        }
213    }
214}
tasm_lib/verifier/claim/new_recursive.rs

tasm_lib/verifier/claim/
new_recursive.rs
