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_ir_base::{cmp::CmpOp, felt::Felt, func::FuncIO};
7use std::ops::Range;
8
9pub mod error;
10pub mod lowerable;
11
12pub type Result<T> = std::result::Result<T, error::Error>;
13
14pub trait Lowering: ExprLowering {
15    fn generate_constraint(
16        &self,
17        op: CmpOp,
18        lhs: &Self::CellOutput,
19        rhs: &Self::CellOutput,
20    ) -> Result<()>;
21
22    fn num_constraints(&self) -> usize;
23
24    fn checked_generate_constraint(
25        &self,
26        op: CmpOp,
27        lhs: &Self::CellOutput,
28        rhs: &Self::CellOutput,
29    ) -> Result<()> {
30        let before = self.num_constraints();
31        self.generate_constraint(op, lhs, rhs)?;
32        let after = self.num_constraints();
33        if before >= after {
34            return Err(error::Error::LastConstraintNotGenerated);
35        }
36        Ok(())
37    }
38
39    fn generate_comment(&self, s: String) -> Result<()>;
40
41    fn generate_assume_deterministic(&self, func_io: FuncIO) -> Result<()>;
42
43    fn generate_call(
44        &self,
45        name: &str,
46        selectors: &[Self::CellOutput],
47        outputs: &[FuncIO],
48    ) -> Result<()>;
49
50    fn generate_assert(&self, expr: &Self::CellOutput) -> Result<()>;
51
52    fn generate_post_condition(&self, expr: &Self::CellOutput) -> Result<()>;
53}
54
55pub trait ExprLowering {
56    type CellOutput;
57
58    fn lower_sum(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput)
59    -> Result<Self::CellOutput>;
60
61    fn lower_product(
62        &self,
63        lhs: &Self::CellOutput,
64        rhs: &Self::CellOutput,
65    ) -> Result<Self::CellOutput>;
66
67    fn lower_neg(&self, expr: &Self::CellOutput) -> Result<Self::CellOutput>;
68
69    fn lower_constant(&self, f: Felt) -> Result<Self::CellOutput>;
70
71    fn lower_eq(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
72    fn lower_lt(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
73    fn lower_le(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
74    fn lower_gt(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
75    fn lower_ge(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
76    fn lower_ne(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
77    fn lower_and(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput)
78    -> Result<Self::CellOutput>;
79    fn lower_or(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput) -> Result<Self::CellOutput>;
80    fn lower_not(&self, value: &Self::CellOutput) -> Result<Self::CellOutput>;
81    fn lower_true(&self) -> Result<Self::CellOutput>;
82    fn lower_false(&self) -> Result<Self::CellOutput>;
83    fn lower_det(&self, expr: &Self::CellOutput) -> Result<Self::CellOutput>;
84    fn lower_implies(
85        &self,
86        lhs: &Self::CellOutput,
87        rhs: &Self::CellOutput,
88    ) -> Result<Self::CellOutput>;
89    fn lower_iff(&self, lhs: &Self::CellOutput, rhs: &Self::CellOutput)
90    -> Result<Self::CellOutput>;
91
92    fn lower_function_input(&self, i: usize) -> FuncIO;
93    fn lower_function_output(&self, o: usize) -> FuncIO;
94
95    fn lower_function_inputs(&self, ins: Range<usize>) -> Vec<FuncIO> {
96        ins.map(|i| self.lower_function_input(i)).collect()
97    }
98    fn lower_function_outputs(&self, outs: Range<usize>) -> Vec<FuncIO> {
99        outs.map(|o| self.lower_function_output(o)).collect()
100    }
101
102    fn lower_funcio<IO>(&self, io: IO) -> Result<Self::CellOutput>
103    where
104        IO: Into<FuncIO>;
105}
haloumi_lowering/lib.rs

haloumi_lowering/
lib.rs
