miden_core/program/
claim.rs

1//! The execution claim: the statement a Miden VM proof attests, and its canonical commitment.
2//!
3//! An execution claim binds four fields: the program digest `P`, the kernel commitment `K`, the
4//! stack inputs `I`, and the stack outputs `O`. The deferred root `D` produced by execution is
5//! *not* part of the claim: it is the obligation a verified claim hands back, bound separately
6//! into the transcript seed.
7//!
8//! # Canonical encoding
9//!
10//! The claim encodes as exactly [`NUM_CLAIM_ELEMENTS`] = 40 field elements:
11//!
12//! ```text
13//! offset  0..8    P ‖ K                       (program digest, kernel commitment)
14//! offset  8..24   I  StackInputs, 16 felts    (canonical zero-padded, native order)
15//! offset 24..40   O  StackOutputs, 16 felts   (canonical zero-padded, native order)
16//! ```
17//!
18//! The code context comes first so that callsites that pin `(P, K)` can resume the claim hash
19//! from a precomputed chaining value. Forty elements is exactly five Eidos blocks, so no partial
20//! block is synthesized and both read points (the `(P, K)` prefix state and the claim commitment)
21//! fall on compression boundaries.
22//!
23//! # Claim commitment
24//!
25//! `CLAIM_HASH = Eidos::hash_elements_in_domain(P ‖ K ‖ I ‖ O, CLAIM_DOMAIN_TAG)`. The initial
26//! chaining value binds both the registered domain and the exact logical length (`40`), after
27//! which Eidos processes five compression blocks in sequence.
28
29use miden_crypto::hash::eidos::EidosDomain;
30
31use super::{KernelDescriptor, ProgramInfo, StackInputs, StackOutputs};
32use crate::{Felt, Word, ZERO, chiplets::hasher};
33
34// CONSTANTS
35// ================================================================================================
36
37/// Number of field elements in the canonical claim encoding: `P ‖ K ‖ I ‖ O`.
38pub const NUM_CLAIM_ELEMENTS: usize = 40;
39
40/// Registered domain tag for the claim commitment.
41pub const CLAIM_DOMAIN_TAG: Felt = super::domain::ExecutionClaimDomain::TAG.as_felt();
42
43// EXECUTION CLAIM
44// ================================================================================================
45
46/// The external statement a Miden VM proof attests: the program root and kernel identify the
47/// executed code and its syscall authorization set; the stack inputs and outputs are the
48/// execution's public I/O.
49///
50/// Stack inputs and stack outputs are both stored top-of-stack first: the first value in each
51/// slice is the top of the operand stack. The claim stores both in their canonical zero-padded
52/// 16-element form.
53///
54/// The deferred root is deliberately absent: verification returns it as an obligation.
55#[derive(Debug, Clone, PartialEq, Eq)]
56pub struct ExecutionClaim {
57    program_root: Word,
58    kernel: KernelDescriptor,
59    stack_inputs: StackInputs,
60    stack_outputs: StackOutputs,
61}
62
63impl ExecutionClaim {
64    /// Creates a new execution claim from the program root, kernel, and stack I/O.
65    pub const fn new(
66        program_root: Word,
67        kernel: KernelDescriptor,
68        stack_inputs: StackInputs,
69        stack_outputs: StackOutputs,
70    ) -> Self {
71        Self {
72            program_root,
73            kernel,
74            stack_inputs,
75            stack_outputs,
76        }
77    }
78
79    /// Creates a new execution claim from the program info and the stack I/O.
80    pub fn from_program_info(
81        program_info: ProgramInfo,
82        stack_inputs: StackInputs,
83        stack_outputs: StackOutputs,
84    ) -> Self {
85        let (program_root, kernel) = program_info.into_parts();
86        Self::new(program_root, kernel, stack_inputs, stack_outputs)
87    }
88
89    /// Returns the MAST root of the executed program.
90    pub const fn program_root(&self) -> Word {
91        self.program_root
92    }
93
94    /// Returns the kernel descriptor of this claim.
95    pub const fn kernel(&self) -> &KernelDescriptor {
96        &self.kernel
97    }
98
99    /// Returns the program info (program root + kernel) of this claim.
100    ///
101    /// This constructs a new [`ProgramInfo`], cloning the kernel descriptor.
102    pub fn to_program_info(&self) -> ProgramInfo {
103        ProgramInfo::new(self.program_root, self.kernel.clone())
104    }
105
106    /// Returns the stack inputs of this claim.
107    pub const fn stack_inputs(&self) -> &StackInputs {
108        &self.stack_inputs
109    }
110
111    /// Returns the stack outputs of this claim.
112    pub const fn stack_outputs(&self) -> &StackOutputs {
113        &self.stack_outputs
114    }
115
116    /// Splits this claim into its program root, kernel, and stack I/O.
117    pub fn into_parts(self) -> (Word, KernelDescriptor, StackInputs, StackOutputs) {
118        (self.program_root, self.kernel, self.stack_inputs, self.stack_outputs)
119    }
120
121    /// Returns the canonical 40-element encoding `P ‖ K ‖ I ‖ O` of this claim.
122    pub fn to_elements(&self) -> [Felt; NUM_CLAIM_ELEMENTS] {
123        let mut elements = [ZERO; NUM_CLAIM_ELEMENTS];
124        elements[0..4].copy_from_slice(self.program_root.as_elements());
125        elements[4..8].copy_from_slice(self.kernel.commitment().as_elements());
126        elements[8..24].copy_from_slice(&self.stack_inputs[..]);
127        elements[24..40].copy_from_slice(&self.stack_outputs[..]);
128        elements
129    }
130
131    /// Returns the canonical commitment to this claim (`CLAIM_HASH`).
132    ///
133    /// This is the verifier-independent name of the claim: the value used to request proof
134    /// packages and to bind verified claims into a consumer's own statement.
135    pub fn commitment(&self) -> Word {
136        claim_commitment(&self.to_elements())
137    }
138}
139
140/// Returns the canonical claim commitment over an already-encoded claim.
141///
142/// This is the single implementation of `CLAIM_HASH`; every native computation of the claim
143/// commitment (including the transcript observation in `miden-air`) must go through it.
144pub fn claim_commitment(elements: &[Felt; NUM_CLAIM_ELEMENTS]) -> Word {
145    hasher::hash_elements_in_domain(elements, super::domain::EXECUTION_CLAIM)
146}
147
148// TESTS
149// ================================================================================================
150
151#[cfg(test)]
152mod tests {
153    use super::{
154        super::{KernelDescriptor, domain},
155        *,
156    };
157
158    fn test_claim() -> ExecutionClaim {
159        let word = |a: u64| -> Word {
160            [
161                Felt::new_unchecked(a),
162                Felt::new_unchecked(a + 1),
163                Felt::new_unchecked(a + 2),
164                Felt::new_unchecked(a + 3),
165            ]
166            .into()
167        };
168        let kernel = KernelDescriptor::from_hashes(vec![word(100)]).unwrap();
169        let program_info = ProgramInfo::new(word(1), kernel);
170        let inputs = StackInputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(6)]).unwrap();
171        let outputs = StackOutputs::new(&[Felt::new_unchecked(7)]).unwrap();
172        ExecutionClaim::from_program_info(program_info, inputs, outputs)
173    }
174
175    /// The commitment must bind every field and the I/O order, be domain-separated, and use
176    /// the registered domain tag.
177    #[test]
178    fn commitment_binds_fields_order_and_domain() {
179        let base = test_claim();
180        let base_commitment = base.commitment();
181        let base_elements = base.to_elements();
182
183        // mutate P
184        let mut mutated = base.clone();
185        mutated.program_root = [Felt::new_unchecked(999), ZERO, ZERO, ZERO].into();
186        assert_ne!(mutated.commitment(), base_commitment, "P not bound");
187
188        // mutate K (different kernel)
189        let mut mutated = base.clone();
190        mutated.kernel = KernelDescriptor::from_hashes(vec![
191            [Felt::new_unchecked(200), ZERO, ZERO, ZERO].into(),
192        ])
193        .unwrap();
194        assert_ne!(mutated.commitment(), base_commitment, "K not bound");
195
196        // mutate one element of I
197        let mut mutated = base.clone();
198        mutated.stack_inputs =
199            StackInputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(60)]).unwrap();
200        assert_ne!(mutated.commitment(), base_commitment, "I not bound");
201
202        // mutate one element of O
203        let mut mutated = base.clone();
204        mutated.stack_outputs = StackOutputs::new(&[Felt::new_unchecked(70)]).unwrap();
205        assert_ne!(mutated.commitment(), base_commitment, "O not bound");
206
207        // swap I and O (order binding): same multiset of felts, different positions
208        let mut mutated = base;
209        mutated.stack_inputs = StackInputs::new(&[Felt::new_unchecked(7)]).unwrap();
210        mutated.stack_outputs =
211            StackOutputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(6)]).unwrap();
212        assert_ne!(mutated.commitment(), base_commitment, "I/O order not bound");
213
214        // domain separation: differs from the untagged hash and from another registered tag
215        let elements = base_elements;
216        assert_ne!(
217            base_commitment,
218            hasher::hash_elements(&elements),
219            "claim commitment must differ from the untagged hash"
220        );
221        assert_ne!(
222            base_commitment,
223            hasher::hash_elements_in_domain(&elements, domain::KERNEL_COMMITMENT),
224            "claim commitment must differ from a kernel-tagged hash of the same data"
225        );
226
227        assert_eq!(CLAIM_DOMAIN_TAG, domain::ExecutionClaimDomain::TAG.as_felt());
228    }
229}
miden_core/program/claim.rs

miden_core/program/
claim.rs
