Skip to main content

hekate_program/
lib.rs

1// SPDX-License-Identifier: Apache-2.0
2// This file is part of the hekate project.
3// Copyright (C) 2026 Andrei Kochergin <andrei@oumuamua.dev>
4// Copyright (C) 2026 Oumuamua Labs <info@oumuamua.dev>. All rights reserved.
5//
6// Licensed under the Apache License, Version 2.0 (the "License");
7// you may not use this file except in compliance with the License.
8// You may obtain a copy of the License at
9//
10//     http://www.apache.org/licenses/LICENSE-2.0
11//
12// Unless required by applicable law or agreed to in writing, software
13// distributed under the License is distributed on an "AS IS" BASIS,
14// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15// See the License for the specific language governing permissions and
16// limitations under the License.
17
18#![cfg_attr(not(feature = "std"), no_std)]
19
20extern crate alloc;
21extern crate core;
22
23use alloc::string::{String, ToString};
24use alloc::vec::Vec;
25use constraint::{BoundaryConstraint, Constraint, ConstraintAst};
26use core::marker::PhantomData;
27use expander::VirtualExpander;
28use hekate_core::errors;
29use hekate_core::trace::{ColumnTrace, ColumnType, Trace, TraceCompatibleField};
30use hekate_math::{Flat, HardwareField, TowerField};
31use permutation::PermutationCheckSpec;
32
33pub mod chiplet;
34pub mod constraint;
35pub mod expander;
36pub mod permutation;
37pub mod schema;
38
39// =================================================================
40// AIR TRAIT:
41// Core Algebraic Intermediate Representation
42// =================================================================
43
44/// Defines the algebraic structure, trace
45/// layout, and constraints of an AIR table.
46///
47/// Implemented by both standalone
48/// programs and independent chiplets.
49pub trait Air<F: TowerField>: Sized + Clone + Sync {
50    fn name(&self) -> String {
51        "HekateAir".to_string()
52    }
53
54    fn num_columns(&self) -> usize {
55        self.virtual_column_layout().len()
56    }
57
58    /// Flat expansion of `constraint_ast()`.
59    fn constraints(&self) -> Vec<Constraint<F>> {
60        self.constraint_ast().to_constraints()
61    }
62
63    /// Returns the list of boundary constraints. Each
64    /// constraint ties a specific trace cell to a public
65    /// input value. By default, returns an empty list.
66    fn boundary_constraints(&self) -> Vec<BoundaryConstraint<F>> {
67        Vec::new()
68    }
69
70    /// Returns the physical layout
71    /// of the columns in the trace.
72    ///
73    /// This describes the storage type
74    /// (Bit, B8, B32, etc.) of each column.
75    fn column_layout(&self) -> &[ColumnType];
76
77    /// Returns the virtual layout of the columns
78    /// (after unpacking). Defaults to the expander's
79    /// layout if present, else the physical layout.
80    fn virtual_column_layout(&self) -> &[ColumnType] {
81        match self.virtual_expander() {
82            Some(e) => e.virtual_layout(),
83            None => self.column_layout(),
84        }
85    }
86
87    /// Returns the permutation check
88    /// specifications for this AIR table.
89    ///
90    /// Each tuple contains:
91    /// - `String`:
92    ///   Unique bus identifier (e.g., `RomChiplet::BUS_ID`)
93    /// - `PermutationCheckSpec`:
94    ///   The GPA specification (sources, selector)
95    ///
96    /// Default:
97    /// No permutation checks.
98    fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)> {
99        Vec::new()
100    }
101
102    /// Columns pinned to a fixed shape, bound by MLE
103    /// equality at `r_final`. Each shape must be a pure
104    /// function of the row index, not the witness.
105    fn fixed_columns(&self) -> Vec<FixedColumn<F>> {
106        Vec::new()
107    }
108
109    /// Returns the `VirtualExpander` for chiplets
110    /// with physical to virtual column expansion.
111    /// Non-reuse entries must tile `column_layout()`
112    /// exactly; an uncovered column is bound by nothing.
113    fn virtual_expander(&self) -> Option<&VirtualExpander> {
114        None
115    }
116
117    /// Parses a raw physical row (bytes) into
118    /// the full Virtual Row (fields). Used by
119    /// the Verifier to reconstruct the virtual
120    /// trace from committed data.
121    ///
122    /// Delegates to `virtual_expander().parse_row()`
123    /// when present. Falls back to 1:1 parsing
124    /// from `column_layout()`.
125    fn parse_virtual_row(&self, bytes: &[u8], res: &mut Vec<Flat<F>>)
126    where
127        F: TraceCompatibleField,
128    {
129        res.clear();
130
131        if let Some(e) = self.virtual_expander() {
132            e.parse_row(bytes, res)
133                .expect("committed row byte length must match physical_row_bytes");
134            return;
135        }
136
137        let mut offset = 0;
138        for col_type in self.column_layout() {
139            let size = col_type.byte_size();
140            if offset + size <= bytes.len() {
141                res.push(col_type.parse_from_bytes(&bytes[offset..offset + size]));
142                offset += size;
143            }
144        }
145    }
146
147    /// Returns the constraint system as an AST-DAG.
148    fn constraint_ast(&self) -> ConstraintAst<F>;
149
150    /// Chiplet defs used only for kernel dispatch.
151    fn inline_chiplets(&self) -> errors::Result<Vec<chiplet::ChipletDef<F>>> {
152        Ok(Vec::new())
153    }
154
155    /// Each hint's `chiplet_idx` indexes into `inline_chiplets()`.
156    fn inline_chiplet_kernels(&self) -> Vec<InlineKernelHint> {
157        Vec::new()
158    }
159}
160
161// =================================================================
162// PROGRAM TRAIT — Composition over Air
163// =================================================================
164
165/// Extends `Air<F>` with multi-table composition:
166/// independent chiplets, GKR gadgets, and public inputs.
167///
168/// The top-level prover and verifier require `Program<F>`.
169/// Internal sub-protocols (ZeroCheck, chiplet verification)
170/// operate on `Air<F>` alone.
171pub trait Program<F: TowerField>: Air<F> {
172    /// Number of public inputs for this program.
173    fn num_public_inputs(&self) -> usize {
174        0
175    }
176
177    /// Returns independent AIR chiplet definitions.
178    /// Each chiplet gets its own trace, commitment,
179    /// ZeroCheck, and evaluation argument.
180    /// Connected to the main trace via GPA bus.
181    fn chiplet_defs(&self) -> errors::Result<Vec<chiplet::ChipletDef<F>>> {
182        Ok(Vec::new())
183    }
184}
185
186/// Represents a reference to a trace cell within
187/// the program's execution trace. Points to a specific
188/// column and relative row offset (current or next).
189#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
190pub struct ProgramCell {
191    pub col_idx: usize,
192
193    /// false = current row (i),
194    /// true = next row (i+1)
195    pub next_row: bool,
196}
197
198impl ProgramCell {
199    /// Reference to a cell in the current row.
200    pub fn current(col_idx: usize) -> Self {
201        Self {
202            col_idx,
203            next_row: false,
204        }
205    }
206
207    /// Reference to a cell in the next row.
208    pub fn next(col_idx: usize) -> Self {
209        Self {
210            col_idx,
211            next_row: true,
212        }
213    }
214}
215
216// =================================================================
217// INSTANCE & WITNESS
218// =================================================================
219
220/// Public Instance (Common inputs)
221/// of the program execution.
222#[derive(Clone, Debug)]
223pub struct ProgramInstance<F: TowerField> {
224    num_rows: usize,
225    public_inputs: Vec<F>,
226}
227
228impl<F: TowerField> ProgramInstance<F> {
229    pub fn new(num_rows: usize, public_inputs: Vec<F>) -> Self {
230        assert!(
231            num_rows.is_power_of_two(),
232            "Program trace height must be power of 2"
233        );
234
235        Self {
236            num_rows,
237            public_inputs,
238        }
239    }
240
241    #[inline(always)]
242    pub fn num_rows(&self) -> usize {
243        self.num_rows
244    }
245
246    /// Public inputs in canonical basis.
247    #[inline(always)]
248    pub fn public_inputs(&self) -> &[F] {
249        &self.public_inputs
250    }
251
252    #[inline(always)]
253    pub fn public_input(&self, idx: usize) -> Option<F> {
254        self.public_inputs.get(idx).copied()
255    }
256}
257
258/// Secret Witness (The Execution Trace) of the program.
259/// Holds the trace data. Generic over T to support both
260/// raw ColumnTrace and specialized wrappers.
261pub struct ProgramWitness<F: TowerField, T: Trace = ColumnTrace> {
262    pub trace: T,
263    pub chiplet_traces: Vec<ColumnTrace>,
264    _marker: PhantomData<F>,
265}
266
267impl<F: TowerField, T: Trace> ProgramWitness<F, T> {
268    pub fn new(trace: T) -> Self {
269        Self {
270            trace,
271            chiplet_traces: Vec::new(),
272            _marker: PhantomData,
273        }
274    }
275
276    /// Attach independent chiplet traces.
277    /// Each entry corresponds by index to `chiplet_defs()`.
278    pub fn with_chiplets(mut self, chiplet_traces: Vec<ColumnTrace>) -> Self {
279        self.chiplet_traces = chiplet_traces;
280        self
281    }
282}
283
284/// Locates a chiplet's inlined sub-AST in
285/// the program's merged `constraint_ast()`
286/// so the prover can dispatch its kernel.
287#[derive(Clone, Copy, Debug)]
288pub struct InlineKernelHint {
289    /// Index into `Air::inline_chiplets()`.
290    pub chiplet_idx: usize,
291
292    /// Absolute index of the chiplet's
293    /// first root in the program's `roots`.
294    pub root_offset: usize,
295
296    /// Absolute column index where
297    /// the chiplet's columns start.
298    pub column_offset: usize,
299}
300
301// =================================================================
302// FIXED COLUMNS
303// =================================================================
304
305/// Row-index-determined shape a fixed column is
306/// pinned to. `FirstRow`/`LastRow`/`Custom` are
307/// single-row indicators; `Periodic`/`Sparse`/`Dense`
308/// are arbitrary row-indexed patterns.
309#[derive(Clone, Debug, PartialEq, Eq)]
310pub enum FixedShape<F> {
311    LastRow,
312    FirstRow,
313    Custom(Vec<bool>),
314    Periodic { period: usize, values: Vec<F> },
315    Sparse(Vec<(usize, F)>),
316    Dense(Vec<F>),
317}
318
319impl<F: HardwareField> FixedShape<F> {
320    /// MLE of the shape at point `r` (LSB-first),
321    /// in flat basis. `r.len()` must equal `num_vars`.
322    pub fn evaluate(&self, r: &[Flat<F>]) -> Flat<F> {
323        let one = Flat::from_raw(F::ONE);
324        match self {
325            FixedShape::LastRow => {
326                let mut prod = one;
327                for &r_k in r {
328                    prod *= r_k;
329                }
330
331                one - prod
332            }
333            FixedShape::FirstRow => {
334                let mut prod = one;
335                for &r_k in r {
336                    prod *= one - r_k;
337                }
338
339                prod
340            }
341            FixedShape::Custom(bits) => {
342                debug_assert_eq!(bits.len(), r.len(), "Custom point bit width != r.len()");
343
344                let mut prod = one;
345                for (k, &b) in bits.iter().enumerate() {
346                    let factor = if b { r[k] } else { one - r[k] };
347                    prod *= factor;
348                }
349
350                prod
351            }
352            FixedShape::Periodic { period, values } => {
353                // Low p = log2(period) coords only;
354                // high coords each sum to 1.
355                let p = period.trailing_zeros() as usize;
356
357                let mut acc = Flat::from_raw(F::ZERO);
358                for (j, &v) in values.iter().enumerate() {
359                    acc += v.to_hardware() * eq_index(&r[..p], j);
360                }
361
362                acc
363            }
364            FixedShape::Sparse(entries) => {
365                let mut acc = Flat::from_raw(F::ZERO);
366                for &(row, v) in entries {
367                    acc += v.to_hardware() * eq_index(r, row);
368                }
369
370                acc
371            }
372            FixedShape::Dense(values) => {
373                let mut acc = Flat::from_raw(F::ZERO);
374                for (i, &v) in values.iter().enumerate() {
375                    acc += v.to_hardware() * eq_index(r, i);
376                }
377
378                acc
379            }
380        }
381    }
382
383    /// Shape value at integer row `row`. O(1);
384    /// prefer over `evaluate` at a vertex,
385    /// which is O(N) for `Dense`.
386    pub fn value_at_row(&self, row: usize, num_vars: usize) -> Flat<F> {
387        let one = Flat::from_raw(F::ONE);
388        let zero = Flat::from_raw(F::ZERO);
389
390        match self {
391            FixedShape::FirstRow => {
392                if row == 0 {
393                    one
394                } else {
395                    zero
396                }
397            }
398            FixedShape::LastRow => {
399                if row == (1usize << num_vars) - 1 {
400                    zero
401                } else {
402                    one
403                }
404            }
405            FixedShape::Custom(bits) => {
406                let target = bits
407                    .iter()
408                    .enumerate()
409                    .fold(0usize, |acc, (k, &b)| acc | ((b as usize) << k));
410
411                if row == target { one } else { zero }
412            }
413            FixedShape::Periodic { period, values } => values[row % period].to_hardware(),
414            FixedShape::Sparse(entries) => {
415                let mut acc = zero;
416                for &(r, v) in entries {
417                    if r == row {
418                        acc += v.to_hardware();
419                    }
420                }
421
422                acc
423            }
424            FixedShape::Dense(values) => values[row].to_hardware(),
425        }
426    }
427}
428
429fn eq_index<F: HardwareField>(r: &[Flat<F>], index: usize) -> Flat<F> {
430    let one = Flat::from_raw(F::ONE);
431
432    let mut prod = one;
433    for (k, &r_k) in r.iter().enumerate() {
434        let factor = if (index >> k) & 1 == 1 {
435            r_k
436        } else {
437            one - r_k
438        };
439        prod *= factor;
440    }
441
442    prod
443}
444
445/// One committed column pinned to a fixed shape.
446#[derive(Clone, Debug, PartialEq, Eq)]
447pub struct FixedColumn<F> {
448    pub col_idx: usize,
449    pub shape: FixedShape<F>,
450}
451
452impl<F> FixedColumn<F> {
453    pub fn last_row(col_idx: usize) -> Self {
454        Self {
455            col_idx,
456            shape: FixedShape::LastRow,
457        }
458    }
459
460    pub fn first_row(col_idx: usize) -> Self {
461        Self {
462            col_idx,
463            shape: FixedShape::FirstRow,
464        }
465    }
466
467    pub fn custom(col_idx: usize, bits: Vec<bool>) -> Self {
468        Self {
469            col_idx,
470            shape: FixedShape::Custom(bits),
471        }
472    }
473
474    pub fn periodic(col_idx: usize, period: usize, values: Vec<F>) -> Self {
475        Self {
476            col_idx,
477            shape: FixedShape::Periodic { period, values },
478        }
479    }
480
481    pub fn sparse(col_idx: usize, entries: Vec<(usize, F)>) -> Self {
482        Self {
483            col_idx,
484            shape: FixedShape::Sparse(entries),
485        }
486    }
487
488    pub fn dense(col_idx: usize, values: Vec<F>) -> Self {
489        Self {
490            col_idx,
491            shape: FixedShape::Dense(values),
492        }
493    }
494}
495
496/// Declares a fixed column from a shape.
497pub fn fix<F>(col_idx: usize, shape: FixedShape<F>) -> FixedColumn<F> {
498    FixedColumn { col_idx, shape }
499}
500
501/// Rejects out-of-range `col_idx`, duplicate pins,
502/// malformed shapes, and out-of-domain values
503/// (`Bit` columns require values in {0, 1}).
504pub fn validate_fixed_columns<F: TowerField>(
505    fixed: &[FixedColumn<F>],
506    layout: &[ColumnType],
507    num_vars: Option<usize>,
508) -> errors::Result<()> {
509    for (i, fc) in fixed.iter().enumerate() {
510        if fc.col_idx >= layout.len() {
511            return Err(errors::Error::Protocol {
512                protocol: "fixed_column",
513                message: "col_idx out of range",
514            });
515        }
516
517        validate_shape(&fc.shape, layout[fc.col_idx], num_vars)?;
518
519        for prior in &fixed[..i] {
520            if prior.col_idx == fc.col_idx {
521                return Err(errors::Error::Protocol {
522                    protocol: "fixed_column",
523                    message: "duplicate pin on same column",
524                });
525            }
526        }
527    }
528
529    Ok(())
530}
531
532fn validate_shape<F: TowerField>(
533    shape: &FixedShape<F>,
534    col_type: ColumnType,
535    num_vars: Option<usize>,
536) -> errors::Result<()> {
537    match shape {
538        FixedShape::LastRow | FixedShape::FirstRow => Ok(()),
539        FixedShape::Custom(bits) => match num_vars {
540            Some(nv) if bits.len() != nv => Err(errors::Error::Protocol {
541                protocol: "fixed_column",
542                message: "Custom point bit width != num_vars",
543            }),
544            _ => Ok(()),
545        },
546        FixedShape::Periodic { period, values } => {
547            if !period.is_power_of_two() {
548                return Err(errors::Error::Protocol {
549                    protocol: "fixed_column",
550                    message: "Periodic period must be a power of two",
551                });
552            }
553
554            if values.len() != *period {
555                return Err(errors::Error::Protocol {
556                    protocol: "fixed_column",
557                    message: "Periodic values length != period",
558                });
559            }
560
561            if let Some(nv) = num_vars
562                && *period > (1usize << nv)
563            {
564                return Err(errors::Error::Protocol {
565                    protocol: "fixed_column",
566                    message: "Periodic period exceeds trace height",
567                });
568            }
569
570            check_bit_domain(values.iter().copied(), col_type)
571        }
572        FixedShape::Sparse(entries) => {
573            if let Some(nv) = num_vars {
574                let n = 1usize << nv;
575                for &(row, _) in entries {
576                    if row >= n {
577                        return Err(errors::Error::Protocol {
578                            protocol: "fixed_column",
579                            message: "Sparse row index exceeds trace height",
580                        });
581                    }
582                }
583            }
584
585            for (i, &(row, _)) in entries.iter().enumerate() {
586                if entries[..i].iter().any(|&(prior, _)| prior == row) {
587                    return Err(errors::Error::Protocol {
588                        protocol: "fixed_column",
589                        message: "duplicate Sparse row",
590                    });
591                }
592            }
593
594            check_bit_domain(entries.iter().map(|&(_, v)| v), col_type)
595        }
596        FixedShape::Dense(values) => {
597            if let Some(nv) = num_vars
598                && values.len() != (1usize << nv)
599            {
600                return Err(errors::Error::Protocol {
601                    protocol: "fixed_column",
602                    message: "Dense values length != trace height",
603                });
604            }
605
606            check_bit_domain(values.iter().copied(), col_type)
607        }
608    }
609}
610
611fn check_bit_domain<F: TowerField>(
612    values: impl Iterator<Item = F>,
613    col_type: ColumnType,
614) -> errors::Result<()> {
615    if col_type != ColumnType::Bit {
616        return Ok(());
617    }
618
619    for v in values {
620        if v != F::ZERO && v != F::ONE {
621            return Err(errors::Error::Protocol {
622                protocol: "fixed_column",
623                message: "Bit fixed column value not in {0,1}",
624            });
625        }
626    }
627
628    Ok(())
629}