haloumi_lowering/
lib.rs

1#![doc = include_str!("../README.md")]
2#![deny(rustdoc::broken_intra_doc_links)]
3#![deny(missing_debug_implementations)]
4#![deny(missing_docs)]
5
6use haloumi_core::{cmp::CmpOp, felt::Felt, slot::Slot};
7
8pub mod error;
9pub mod lowerable;
10
11/// Result type for lowering related operations.
12pub type Result<T> = std::result::Result<T, error::Error>;
13
14/// Defines the interface code generators expose for generating code in their corresponding IR.
15pub trait Lowering: ExprLowering {
16    /// Generates a constraint.
17    fn generate_constraint(
18        &self,
19        op: CmpOp,
20        lhs: &Self::CellOutput,
21        rhs: &Self::CellOutput,
22    ) -> Result<()>;
23
24    /// Returns the number of generated constraints.
25    fn num_constraints(&self) -> usize;
26
27    /// Attempts to generate a constraint and fails if it couldn't be generated.
28    fn checked_generate_constraint(
29        &self,
30        op: CmpOp,
31        lhs: &Self::CellOutput,
32        rhs: &Self::CellOutput,
33    ) -> Result<()> {
34        let before = self.num_constraints();
35        self.generate_constraint(op, lhs, rhs)?;
36        let after = self.num_constraints();
37        if before >= after {
38            return Err(error::Error::LastConstraintNotGenerated);
39        }
40        Ok(())
41    }
42
43    /// Generates IR representing a comment with the given text.
44    fn generate_comment(&self, s: String) -> Result<()>;
45
46    /// Generates an statement that hints that the given [`Slot`] must be assumed to be
47    /// deterministic.
48    fn generate_assume_deterministic(&self, slot: Slot) -> Result<()>;
49
50    /// Generates a call to another group.
51    fn generate_call(
52        &self,
53        name: &str,
54        selectors: &[Self::CellOutput],
55        outputs: &[Slot],
56    ) -> Result<()>;
57
58    /// Generates an assertion using the given expression.
59    ///
60    /// How exactly this assertion is represented is backend dependant.
61    fn generate_assert(&self, expr: &Self::CellOutput) -> Result<()>;
62
63    /// Generates an assertion using the given expression that is treated as a post-condition.
64    ///
65    /// How exactly this assertion is represented is backend dependant.
66    fn generate_post_condition(&self, expr: &Self::CellOutput) -> Result<()>;
67}
68
69/// Defines the interface code generators expose for generating expressions in their corresponding IR.
70pub trait ExprLowering {
71    /// The type representing a generated expression.
72    type CellOutput;
73
74    /// Emits an expression representing addition.
75    fn lower_sum(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput)
76    -> Result<Self::CellOutput>;
77
78    /// Emits an expression representing multiplication.
79    fn lower_product(
80        &self,
81        lhs: &Self::CellOutput,
82        rhs: &Self::CellOutput,
83    ) -> Result<Self::CellOutput>;
84
85    /// Emits an expression representing negation.
86    fn lower_neg(&self, expr: &Self::CellOutput) -> Result<Self::CellOutput>;
87
88    /// Emits a constant value.
89    fn lower_constant(&self, f: Felt) -> Result<Self::CellOutput>;
90
91    /// Emits a boolean expression representing equality between the operands.
92    fn lower_eq(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
93
94    /// Emits a boolean expression representing a less-than relation between the operands.
95    fn lower_lt(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
96
97    /// Emits a boolean expression representing a less-than or equal relation between the operands.
98    fn lower_le(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
99
100    /// Emits a boolean expression representing a greater-than relation between the operands.
101    fn lower_gt(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
102
103    /// Emits a boolean expression representing a greater-than or equal relation between the operands.
104    fn lower_ge(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
105
106    /// Emits a boolean expression representing the negation of equality between the operands.
107    fn lower_ne(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
108
109    /// Emits a logical AND between the two operands.
110    fn lower_and(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput)
111    -> Result<Self::CellOutput>;
112
113    /// Emits a logical OR between the two operands.
114    fn lower_or(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
115
116    /// Emits a logical NOT between the two operands.
117    fn lower_not(&self, value: &Self::CellOutput) -> Result<Self::CellOutput>;
118
119    /// Emits a literal `true` value.
120    fn lower_true(&self) -> Result<Self::CellOutput>;
121
122    /// Emits a literal `false` value.
123    fn lower_false(&self) -> Result<Self::CellOutput>;
124
125    /// Emits an expression that hints that the given expression must be proven deterministic.
126    ///
127    /// The concrete semantics of this expression are backend dependant but it must return an
128    /// expression of boolean type.
129    fn lower_det(&self, expr: &Self::CellOutput) -> Result<Self::CellOutput>;
130
131    /// Emits a logical implication between the two operands.
132    fn lower_implies(
133        &self,
134        lhs: &Self::CellOutput,
135        rhs: &Self::CellOutput,
136    ) -> Result<Self::CellOutput>;
137
138    /// Emits a logical double-implication between the two operands.
139    fn lower_iff(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput)
140    -> Result<Self::CellOutput>;
141
142    /// Returns a [`Slot`] representing the `i`-th input.
143    fn lower_function_input(&self, i: usize) -> Slot;
144
145    /// Returns a [`Slot`] representing the `o`-th output.
146    fn lower_function_output(&self, o: usize) -> Slot;
147
148    /// Returns a list of [`Slot`] representing the input indices in the iterator.
149    fn lower_function_inputs(&self, ins: impl IntoIterator<Item = usize>) -> Vec<Slot> {
150        ins.into_iter()
151            .map(|i| self.lower_function_input(i))
152            .collect()
153    }
154
155    /// Returns a list of [`Slot`] representing the output indices in the iterator.
156    fn lower_function_outputs(&self, outs: impl IntoIterator<Item = usize>) -> Vec<Slot> {
157        outs.into_iter()
158            .map(|o| self.lower_function_output(o))
159            .collect()
160    }
161
162    /// Emits an expression representing the given IO.
163    fn lower_funcio<IO>(&self, io: IO) -> Result<Self::CellOutput>
164    where
165        IO: Into<Slot>;
166}
haloumi_lowering/lib.rs

haloumi_lowering/
lib.rs
