Xmss sub mtu ipv6

README.md

@@ -31,7 +31,7 @@ Machine: M4 Max 48GB (CPU only)
 ### XMSS aggregation
 
 ```bash
-cargo run --release -- xmss --n-signatures 1400
+cargo run --release -- xmss --n-signatures 1500
 ```
 
 | WHIR rate \ regime | Proven               | Conjectured          |

crates/lean_compiler/snark_lib.py

@@ -67,8 +67,26 @@ def pop(self):
         self._data.pop()
 
 
-def poseidon16_compress(left, right, output, mode):
-    _ = left, right, output, mode
+def poseidon16_compress(left, right, output):
+    _ = left, right, output
+
+
+def poseidon16_compress_half(left, right, output):
+    """Poseidon16 compression outputting only the first 4 FE (last 4 unconstrained)."""
+    _ = left, right, output
+
+
+def poseidon16_compress_hardcoded_left_4(left, right, output, offset):
+    """Poseidon16 compression where the first 4 FE of the left input are read from
+    memory[offset..offset+4] instead of memory[left..left+4]. The last 4 FE of the
+    left input still come from memory[left+4..left+8]. `offset` must be a compile-time
+    constant expression."""
+    _ = left, right, output, offset
+
+
+def poseidon16_compress_half_hardcoded_left_4(left, right, output, offset):
+    """Composition of `poseidon16_compress_half` and `poseidon16_compress_hardcoded_left_4`."""
+    _ = left, right, output, offset
 
 
 def add_be(a, b, result, length=None):

crates/lean_compiler/src/a_simplify_lang.rs

@@ -5,8 +5,9 @@ use crate::{
 };
 use backend::PrimeCharacteristicRing;
 use lean_vm::{
-    Boolean, BooleanExpr, CustomHint, ExtensionOpMode, FunctionName, PrecompileArgs, PrecompileCompTimeArgs,
-    SourceLocation, Table, TableT,
+    Boolean, BooleanExpr, CustomHint, ExtensionOpMode, FunctionName, POSEIDON16_HALF_HARDCODED_LEFT_4_NAME,
+    POSEIDON16_HALF_NAME, POSEIDON16_HARDCODED_LEFT_4_NAME, PrecompileArgs, PrecompileCompTimeArgs, SourceLocation,
+    Table, TableT,
 };
 use std::{
     collections::{BTreeMap, BTreeSet},
@@ -2193,28 +2194,54 @@ fn simplify_lines(
                             continue;
                         }
 
-                        // Special handling for poseidon16 precompile
-                        if function_name == Table::poseidon16().name() {
+                        // Special handling for poseidon16 precompile (4 variants)
+                        if function_name == Table::poseidon16().name()
+                            || function_name == POSEIDON16_HALF_NAME
+                            || function_name == POSEIDON16_HARDCODED_LEFT_4_NAME
+                            || function_name == POSEIDON16_HALF_HARDCODED_LEFT_4_NAME
+                        {
+                            let half_output = function_name == POSEIDON16_HALF_NAME
+                                || function_name == POSEIDON16_HALF_HARDCODED_LEFT_4_NAME;
+                            let is_hardcoded = function_name == POSEIDON16_HARDCODED_LEFT_4_NAME
+                                || function_name == POSEIDON16_HALF_HARDCODED_LEFT_4_NAME;
                             if !targets.is_empty() {
                                 return Err(format!(
                                     "Precompile {function_name} should not return values, at {location}"
                                 ));
                             }
-                            if args.len() != 3 {
+                            let expected_args = if is_hardcoded { 4 } else { 3 };
+                            if args.len() != expected_args {
+                                let signature = if is_hardcoded {
+                                    "(ptr_a, ptr_b, ptr_res, offset)"
+                                } else {
+                                    "(ptr_a, ptr_b, ptr_res)"
+                                };
                                 return Err(format!(
-                                    "Precompile {function_name} expects 3 arguments (ptr_a, ptr_b, ptr_res), got {}, at {location}",
+                                    "Precompile {function_name} expects {expected_args} arguments {signature}, got {}, at {location}",
                                     args.len()
                                 ));
                             }
                             let simplified_args = args
                                 .iter()
                                 .map(|arg| simplify_expr(ctx, state, const_malloc, arg, &mut res))
                                 .collect::<Result<Vec<_>, _>>()?;
+                            let hardcoded_left_4 = if is_hardcoded {
+                                Some(simplified_args[3].as_constant().ok_or_else(|| {
+                                    format!(
+                                        "{function_name}: offset argument must be a compile-time constant, at {location}"
+                                    )
+                                })?)
+                            } else {
+                                None
+                            };
                             res.push(SimpleLine::Precompile(PrecompileArgs {
                                 arg_0: simplified_args[0].clone(),
                                 arg_1: simplified_args[1].clone(),
                                 res: simplified_args[2].clone(),
-                                data: PrecompileCompTimeArgs::Poseidon16,
+                                data: PrecompileCompTimeArgs::Poseidon16 {
+                                    half_output,
+                                    hardcoded_left_4,
+                                },
                             }));
                             continue;
                         }

crates/lean_compiler/src/instruction_encoder.rs

@@ -48,7 +48,17 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
         }
         Instruction::Precompile(precompile) => {
             let precompile_data = match &precompile.data {
-                PrecompileCompTimeArgs::Poseidon16 => POSEIDON_PRECOMPILE_DATA,
+                PrecompileCompTimeArgs::Poseidon16 {
+                    half_output,
+                    hardcoded_left_4,
+                } => {
+                    let flag = hardcoded_left_4.is_some() as usize;
+                    let offset = hardcoded_left_4.unwrap_or(0);
+                    POSEIDON_PRECOMPILE_DATA
+                        + POSEIDON_HALF_OUTPUT_SHIFT * (*half_output as usize)
+                        + POSEIDON_HARDCODED_LEFT_4_FLAG_SHIFT * flag
+                        + POSEIDON_HARDCODED_LEFT_4_OFFSET_SHIFT * offset
+                }
                 PrecompileCompTimeArgs::ExtensionOp { size, mode } => {
                     assert!(*size >= 1, "invalid extension_op size={size}");
                     mode.flag_encoding() + EXT_OP_LEN_MULTIPLIER * size

crates/lean_compiler/src/parser/parsers/function.rs

@@ -9,7 +9,10 @@ use crate::{
         grammar::{ParsePair, Rule},
     },
 };
-use lean_vm::{CUSTOM_HINTS, ExtensionOpMode, POSEIDON16_NAME};
+use lean_vm::{
+    CUSTOM_HINTS, ExtensionOpMode, POSEIDON16_HALF_HARDCODED_LEFT_4_NAME, POSEIDON16_HALF_NAME,
+    POSEIDON16_HARDCODED_LEFT_4_NAME, POSEIDON16_NAME,
+};
 
 /// Reserved function names that users cannot define.
 pub const RESERVED_FUNCTION_NAMES: &[&str] = &[
@@ -35,7 +38,11 @@ fn is_reserved_function_name(name: &str) -> bool {
         return true;
     }
     // Check precompile names (poseidon16, extension_op functions)
-    if name == POSEIDON16_NAME {
+    if name == POSEIDON16_NAME
+        || name == POSEIDON16_HALF_NAME
+        || name == POSEIDON16_HARDCODED_LEFT_4_NAME
+        || name == POSEIDON16_HALF_HARDCODED_LEFT_4_NAME
+    {
         return true;
     }
     if ExtensionOpMode::from_name(name).is_some() {

crates/lean_prover/src/test_zkvm.rs

@@ -12,11 +12,43 @@ DIM = 5
 N = 11
 M = 3
 DIGEST_LEN = 8
+HALF_DIGEST_LEN = 4
 
 def main():
     pub_start = 0
     poseidon16_compress(pub_start + 4 * DIGEST_LEN, pub_start + 5 * DIGEST_LEN, pub_start + 6 * DIGEST_LEN)
 
+    # poseidon16_compress_half: only first 4 FE constrained
+    full_out = pub_start + 6 * DIGEST_LEN
+    half_out = pub_start + 80
+    poseidon16_compress_half(pub_start + 4 * DIGEST_LEN, pub_start + 5 * DIGEST_LEN, half_out)
+    for i in unroll(0, HALF_DIGEST_LEN):
+        assert full_out[i] == half_out[i]
+
+    # poseidon16_compress_hardcoded_left_4: with the new convention, only 4 FE are read
+    # at the left pointer (the 4-element data digest at pub_start + 1496) and the first
+    # 4 FE of the left input come from memory[pub_start + 1500 .. pub_start + 1504]
+    # (the hardcoded prefix).
+    hardcoded_left = pub_start + 1496
+    hardcoded_full_out = pub_start + 1504
+    poseidon16_compress_hardcoded_left_4(
+        hardcoded_left,
+        pub_start + 5 * DIGEST_LEN,
+        hardcoded_full_out,
+        pub_start + 1500
+    )
+
+    # Same, but only first 4 FE of the output are constrained.
+    hardcoded_half_out = pub_start + 1512
+    poseidon16_compress_half_hardcoded_left_4(
+        hardcoded_left,
+        pub_start + 5 * DIGEST_LEN,
+        hardcoded_half_out,
+        pub_start + 1500
+    )
+    for i in unroll(0, HALF_DIGEST_LEN):
+        assert hardcoded_full_out[i] == hardcoded_half_out[i]
+
     base_ptr = pub_start + 88
     ext_a_ptr = pub_start + 88 + N
     ext_b_ptr = pub_start + 88 + N * (DIM + 1)
@@ -58,9 +90,46 @@ def main():
     // Poseidon test data
     let poseidon_16_compress_input: [F; 16] = rng.random();
     public_input[32..48].copy_from_slice(&poseidon_16_compress_input);
-    public_input[48..56].copy_from_slice(&poseidon16_compress(poseidon_16_compress_input)[..8]);
+    let poseidon_output = poseidon16_compress(poseidon_16_compress_input);
+    public_input[48..56].copy_from_slice(&poseidon_output[..8]);
     let poseidon_24_input: [F; 24] = rng.random();
     public_input[56..80].copy_from_slice(&poseidon_24_input);
+    // poseidon16_compress_half output at offset 80: first 4 = hash, last 4 = arbitrary pre-existing data
+    public_input[80..84].copy_from_slice(&poseidon_output[..4]);
+    public_input[84..88].copy_from_slice(&[
+        F::from_usize(111),
+        F::from_usize(222),
+        F::from_usize(333),
+        F::from_usize(444),
+    ]);
+
+    // Hardcoded-left-4 test data, placed at public_input[1496..1520].
+    // - The 4-element data digest lives at offset 1496..1500 (the "left" pointer).
+    // - The 4-element hardcoded prefix lives at offset 1500..1504.
+    // The hardcoded variant computes
+    //   Poseidon(prefix(4) || data(4), original_input[8..16])
+    // i.e. only 4 elements are read at the left pointer (matching the new convention
+    // where flag_hardcoded_left_4 = 1 reads m[index_a..index_a+4] for the second half
+    // of the left input and m[offset..offset+4] for the first half).
+    let hardcoded_data: [F; 4] = rng.random();
+    let hardcoded_prefix: [F; 4] = rng.random();
+    public_input[1496..1500].copy_from_slice(&hardcoded_data);
+    public_input[1500..1504].copy_from_slice(&hardcoded_prefix);
+    let mut hardcoded_input = [F::ZERO; 16];
+    hardcoded_input[..4].copy_from_slice(&hardcoded_prefix);
+    hardcoded_input[4..8].copy_from_slice(&hardcoded_data);
+    hardcoded_input[8..16].copy_from_slice(&poseidon_16_compress_input[8..16]);
+    let hardcoded_output = poseidon16_compress(hardcoded_input);
+    // Full output at 1504..1512
+    public_input[1504..1512].copy_from_slice(&hardcoded_output);
+    // Half output at 1512..1520: first 4 = hash, last 4 = arbitrary pre-existing data
+    public_input[1512..1516].copy_from_slice(&hardcoded_output[..4]);
+    public_input[1516..1520].copy_from_slice(&[
+        F::from_usize(555),
+        F::from_usize(666),
+        F::from_usize(777),
+        F::from_usize(888),
+    ]);
 
     // Extension op operands: base[N], ext_a[N], ext_b[N]
     let base_slice: [F; N] = rng.random();

crates/lean_prover/src/trace_gen.rs

@@ -108,6 +108,24 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
     let poseidon_trace = traces.get_mut(&Table::poseidon16()).unwrap();
     fill_trace_poseidon_16(&mut poseidon_trace.columns);
 
+    // For half_output rows, override last 4 output columns with actual memory values
+    // (the AIR doesn't constrain them, but the lookup checks against memory)
+    {
+        let half_output_col = poseidon_trace.columns[POSEIDON_16_COL_FLAG_HALF_OUTPUT].clone();
+        let res_col = poseidon_trace.columns[POSEIDON_16_COL_INDEX_INPUT_RES].clone();
+        for j in HALF_DIGEST_LEN..DIGEST_LEN {
+            poseidon_trace.columns[POSEIDON_16_COL_OUTPUT_START + j]
+                .par_iter_mut()
+                .zip(&half_output_col)
+                .zip(&res_col)
+                .for_each(|((out, &half), &res)| {
+                    if half == F::ONE {
+                        *out = memory_padded[res.to_usize() + j];
+                    }
+                });
+        }
+    }
+
     let extension_op_trace = traces.get_mut(&Table::extension_op()).unwrap();
     fill_trace_extension_op(extension_op_trace, &memory_padded);
 

crates/lean_vm/src/isa/instruction.rs

@@ -63,21 +63,35 @@ pub struct PrecompileArgs<V, S> {
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum PrecompileCompTimeArgs<S> {
-    Poseidon16,
-    ExtensionOp { size: S, mode: ExtensionOpMode },
+    Poseidon16 {
+        half_output: bool,
+        /// `None` = standard variant. `Some(offset)` = the first 4 elements of the left input
+        /// are read from `memory[offset..offset+4]` instead of `memory[index_left..index_left+4]`.
+        hardcoded_left_4: Option<S>,
+    },
+    ExtensionOp {
+        size: S,
+        mode: ExtensionOpMode,
+    },
 }
 
 impl<S> PrecompileCompTimeArgs<S> {
     pub fn table(&self) -> Table {
         match self {
-            Self::Poseidon16 => Table::poseidon16(),
+            Self::Poseidon16 { .. } => Table::poseidon16(),
             Self::ExtensionOp { .. } => Table::extension_op(),
         }
     }
 
-    pub fn map_size<T>(self, f: impl FnOnce(S) -> T) -> PrecompileCompTimeArgs<T> {
+    pub fn map_size<T>(self, mut f: impl FnMut(S) -> T) -> PrecompileCompTimeArgs<T> {
         match self {
-            Self::Poseidon16 => PrecompileCompTimeArgs::Poseidon16,
+            Self::Poseidon16 {
+                half_output,
+                hardcoded_left_4,
+            } => PrecompileCompTimeArgs::Poseidon16 {
+                half_output,
+                hardcoded_left_4: hardcoded_left_4.map(&mut f),
+            },
             Self::ExtensionOp { size, mode } => PrecompileCompTimeArgs::ExtensionOp { size: f(size), mode },
         }
     }
@@ -233,9 +247,18 @@ impl<V: Display, S: Display> Display for PrecompileArgs<V, S> {
             data,
         } = self;
         match data {
-            PrecompileCompTimeArgs::Poseidon16 => {
-                write!(f, "{POSEIDON16_NAME}({arg_0}, {arg_1}, {res})")
-            }
+            PrecompileCompTimeArgs::Poseidon16 {
+                half_output,
+                hardcoded_left_4,
+            } => match (*half_output, hardcoded_left_4) {
+                (false, None) => write!(f, "{POSEIDON16_NAME}({arg_0}, {arg_1}, {res})"),
+                (true, None) => write!(f, "{POSEIDON16_NAME}({arg_0}, {arg_1}, {res}, half)"),
+                (false, Some(off)) => write!(f, "{POSEIDON16_NAME}({arg_0}, {arg_1}, {res}, hardcoded_left_4={off})"),
+                (true, Some(off)) => write!(
+                    f,
+                    "{POSEIDON16_NAME}({arg_0}, {arg_1}, {res}, half, hardcoded_left_4={off})"
+                ),
+            },
             PrecompileCompTimeArgs::ExtensionOp { size, mode } => {
                 write!(f, "{}({arg_0}, {arg_1}, {res}, {size})", mode.name())
             }