trident/os/neptune/recursive.tri

module os.neptune.recursive

use os.neptune.xfield

use vm.io.io

use vm.core.assert

// Recursive STARK Verification Primitives for Triton VM
//
// These functions implement the core building blocks for verifying
// a STARK proof inside a Triton VM program. This enables proof
// composition: a program can verify that another program executed
// correctly, creating recursive proof chains.
//
// The key operations are:
//   - Inner product accumulation (xx_dot_step, xb_dot_step)
//   - FRI layer folding
//   - Merkle root authentication of codeword commitments
//
// Architecture:
//   The inner proof's Claim (program_digest + public I/O) is read
//   from public input. The proof data (FRI layers, Merkle paths,
//   out-of-domain values) is supplied via divine input. The verifier
//   circuit checks all algebraic and combinatorial constraints.
// Accumulate an inner product of two extension field vectors in RAM.
// Processes `count` pairs starting at ptr_a and ptr_b.
// Each step: acc += a[i] * b[i], pointers advance by 3 fields.
// Returns the accumulated XField value as a Digest (3 coefficients + 2 pointers).
pub fn xfe_inner_product(ptr_a: Field, ptr_b: Field, count: Field) -> Digest {
    let mut acc0: Field = 0
    let mut acc1: Field = 0
    let mut acc2: Field = 0
    let mut cur_a: Field = ptr_a
    let mut cur_b: Field = ptr_b
    for i in 0..count bounded 1024 {
        let (r0, r1, r2, r3, r4) = xfield.xx_dot_step(
            acc0,
            acc1,
            acc2,
            cur_a,
            cur_b
        )
        acc0 = r0
        acc1 = r1
        acc2 = r2
        cur_a = r3
        cur_b = r4
    }
    (acc0, acc1, acc2, cur_a, cur_b)
}

// Accumulate an inner product of XField * BField vectors in RAM.
// Processes `count` pairs where a[i] is XField (3 elements) and
// b[i] is BField (1 element). Pointers advance accordingly.
pub fn xb_inner_product(ptr_a: Field, ptr_b: Field, count: Field) -> Digest {
    let mut acc0: Field = 0
    let mut acc1: Field = 0
    let mut acc2: Field = 0
    let mut cur_a: Field = ptr_a
    let mut cur_b: Field = ptr_b
    for i in 0..count bounded 1024 {
        let (r0, r1, r2, r3, r4) = xfield.xb_dot_step(
            acc0,
            acc1,
            acc2,
            cur_a,
            cur_b
        )
        acc0 = r0
        acc1 = r1
        acc2 = r2
        cur_a = r3
        cur_b = r4
    }
    (acc0, acc1, acc2, cur_a, cur_b)
}

// Read the inner program's Claim from public input.
// Returns (program_digest, num_pub_inputs, num_pub_outputs).
// The actual public I/O values follow in subsequent pub_read calls.
pub fn read_claim() -> (Digest, Field, Field) {
    let program_digest: Digest = io.read5()
    let num_inputs: Field = io.read()
    let num_outputs: Field = io.read()
    (program_digest, num_inputs, num_outputs)
}

// Verify that a divined Digest matches an expected commitment.
// Used to authenticate FRI codeword Merkle roots.
pub fn verify_commitment(expected: Digest) {
    let divined: Digest = io.divine5()
    assert.digest(divined, expected)
}