hypercall_state_commitment/
batch_root.rs

1use jmt::RootHash;
2use sha3::{Digest, Keccak256};
3
4use crate::mmr::MmrHash;
5
6/// Compute the batch root that commits to all state.
7///
8/// ```text
9/// batch_root = keccak256(
10///     state_tree_root,
11///     risk_tree_root,
12///     command_mmr_peaks_hash,
13///     obligation_mmr_peaks_hash,
14///     intent_mmr_peaks_hash,
15/// )
16/// ```
17pub fn compute_batch_root(
18    state_root: &RootHash,
19    risk_root: &RootHash,
20    command_mmr_root: &MmrHash,
21    obligation_mmr_root: &MmrHash,
22    intent_mmr_root: &MmrHash,
23) -> [u8; 32] {
24    let mut h = Keccak256::new();
25    h.update(state_root.0);
26    h.update(risk_root.0);
27    h.update(command_mmr_root.0);
28    h.update(obligation_mmr_root.0);
29    h.update(intent_mmr_root.0);
30    h.finalize().into()
31}
32
33/// Decompose and verify a batch root against its components.
34pub fn verify_batch_root(
35    expected: &[u8; 32],
36    state_root: &RootHash,
37    risk_root: &RootHash,
38    command_mmr_root: &MmrHash,
39    obligation_mmr_root: &MmrHash,
40    intent_mmr_root: &MmrHash,
41) -> bool {
42    let computed = compute_batch_root(
43        state_root,
44        risk_root,
45        command_mmr_root,
46        obligation_mmr_root,
47        intent_mmr_root,
48    );
49    &computed == expected
50}
51
52#[cfg(test)]
53mod tests {
54    use super::*;
55
56    #[test]
57    fn fast_batch_root_deterministic() {
58        let state = RootHash([0xAA; 32]);
59        let risk = RootHash([0xBB; 32]);
60        let cmd = MmrHash([0xCC; 32]);
61        let obl = MmrHash([0xDD; 32]);
62        let intent = MmrHash([0xEE; 32]);
63
64        let a = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
65        let b = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
66        assert_eq!(a, b);
67    }
68
69    #[test]
70    fn batch_root_changes_with_any_component() {
71        let state = RootHash([0xAA; 32]);
72        let risk = RootHash([0xBB; 32]);
73        let cmd = MmrHash([0xCC; 32]);
74        let obl = MmrHash([0xDD; 32]);
75        let intent = MmrHash([0xEE; 32]);
76
77        let base = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
78
79        let changed_state = compute_batch_root(&RootHash([0xFF; 32]), &risk, &cmd, &obl, &intent);
80        assert_ne!(base, changed_state);
81
82        let changed_risk = compute_batch_root(&state, &RootHash([0xFF; 32]), &cmd, &obl, &intent);
83        assert_ne!(base, changed_risk);
84
85        let changed_cmd = compute_batch_root(&state, &risk, &MmrHash([0xFF; 32]), &obl, &intent);
86        assert_ne!(base, changed_cmd);
87
88        let changed_obl = compute_batch_root(&state, &risk, &cmd, &MmrHash([0xFF; 32]), &intent);
89        assert_ne!(base, changed_obl);
90
91        let changed_intent = compute_batch_root(&state, &risk, &cmd, &obl, &MmrHash([0xFF; 32]));
92        assert_ne!(base, changed_intent);
93    }
94
95    #[test]
96    fn verify_batch_root_accepts_correct() {
97        let state = RootHash([0x11; 32]);
98        let risk = RootHash([0x22; 32]);
99        let cmd = MmrHash([0x33; 32]);
100        let obl = MmrHash([0x44; 32]);
101        let intent = MmrHash([0x55; 32]);
102
103        let root = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
104        assert!(verify_batch_root(&root, &state, &risk, &cmd, &obl, &intent));
105    }
106
107    #[test]
108    fn verify_batch_root_rejects_tampered() {
109        let state = RootHash([0x11; 32]);
110        let risk = RootHash([0x22; 32]);
111        let cmd = MmrHash([0x33; 32]);
112        let obl = MmrHash([0x44; 32]);
113        let intent = MmrHash([0x55; 32]);
114
115        let root = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
116        assert!(!verify_batch_root(
117            &root,
118            &RootHash([0xFF; 32]),
119            &risk,
120            &cmd,
121            &obl,
122            &intent
123        ));
124    }
125
126    #[test]
127    fn batch_root_is_not_commutative() {
128        let a = RootHash([0x01; 32]);
129        let b = RootHash([0x02; 32]);
130        let c = MmrHash([0x03; 32]);
131        let d = MmrHash([0x04; 32]);
132        let e = MmrHash([0x05; 32]);
133
134        let r1 = compute_batch_root(&a, &b, &c, &d, &e);
135        let r2 = compute_batch_root(&b, &a, &c, &d, &e);
136        assert_ne!(
137            r1, r2,
138            "swapping state/risk roots should produce different batch root"
139        );
140    }
141}
142
143#[cfg(kani)]
144mod kani_proofs {
145    use super::*;
146
147    /// Concrete Keccak smoke proof for the scheduled full Kani workflow.
148    /// Keccak is not PR-fast under Kani, even with fixed inputs.
149    #[kani::proof]
150    fn bounded_batch_root_smoke() {
151        let state = RootHash([0xAA; 32]);
152        let risk = RootHash([0xBB; 32]);
153        let cmd = MmrHash([0xCC; 32]);
154        let obl = MmrHash([0xDD; 32]);
155        let intent = MmrHash([0xEE; 32]);
156
157        let root = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
158        assert!(verify_batch_root(&root, &state, &risk, &cmd, &obl, &intent));
159    }
160
161    /// Prove: compute then verify always succeeds for all inputs.
162    #[kani::proof]
163    fn bounded_compute_verify_round_trip() {
164        let state = RootHash(kani::any());
165        let risk = RootHash(kani::any());
166        let cmd = MmrHash(kani::any());
167        let obl = MmrHash(kani::any());
168        let intent = MmrHash(kani::any());
169
170        let root = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
171        assert!(verify_batch_root(&root, &state, &risk, &cmd, &obl, &intent));
172    }
173
174    /// Prove: compute_batch_root is deterministic for all inputs.
175    #[kani::proof]
176    fn bounded_batch_root_deterministic() {
177        let state = RootHash(kani::any());
178        let risk = RootHash(kani::any());
179        let cmd = MmrHash(kani::any());
180        let obl = MmrHash(kani::any());
181        let intent = MmrHash(kani::any());
182
183        let a = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
184        let b = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
185        assert_eq!(a, b);
186    }
187
188    /// Prove: compute_batch_root never panics.
189    #[kani::proof]
190    fn bounded_batch_root_no_panic() {
191        let state = RootHash(kani::any());
192        let risk = RootHash(kani::any());
193        let cmd = MmrHash(kani::any());
194        let obl = MmrHash(kani::any());
195        let intent = MmrHash(kani::any());
196        let _ = compute_batch_root(&state, &risk, &cmd, &obl, &intent);
197    }
198}
hypercall_state_commitment/batch_root.rs

hypercall_state_commitment/
batch_root.rs
