AIR Composibility
struct AirComponent {
trace: TraceTable,
constraints: Vec<RationalExpression>,
labels: Vec<(String, RationalExpression)>
}
Note. Having labels on expressions allows direct labeling of trace cells using Trace(i, j)
. But it also allows labeling derived values, for example if the constraints are written such that the 'real' value is the difference of two columns, the labeled output can be Trace(i, j) - Trace(i, k)
.
Trace generation
Alternative. Instead of having the components supply the full trace table, we could also have them return a sparse table of (i, j, value) tuples. The constraints would then be used to fill out the table. This may (or not) be more performant, but seems harder to implement. Perhaps instead we can provide helper functions to generate a trace table from constraints and sparse values.
Air component combinators
fn compose_horizontal(A: AirComponent, B: AirComponent) -> AirComponent {
require(A.rows == B.rows);
}
fn compose_vertical(A: AirComponent, B: AirComponent) -> AirComponent {
require(A.rows == B.rows);
require(A.cols == B.cols);
require(A.constraints == B.constraints)
}
fn compose_interleaved(A: AirComponent, B: AirComponent) -> AirComponent {
require(A.rows == B.rows);
require(A.cols == B.cols);
}
fn fold(A: AirComponent) -> AirComponent {
require(A.cols % 2 == 0);
}
To do. We can skip renaming if there are no collisions. This will have to be done on a global basis, not a per name, basis. This can lead to breakage when a subcomponent adds a new name.
Further combinators
It's useful to add a helper function creating no-op components. This allows doing things like fold(compose_horizontal(A, empty(A.rows, 1))
to do a fold where A
has an odd number of columns.
fn empty(rows: usize, cols: usize) -> AirComponent;
Using these, we can implement more complex operations:
fn fold_padded(A: AirComponent, repeats: usize) -> AirComponent {
}
fn fit_horizontal(A: AirComponent, B: AirComponent) -> AirComponent {
}
Example
fn transaction(
initial_balances: Balances,
txs: Vec<Transaction>
) -> (Balances, AirComponent) {
let mut air = fit_horizontal(
compose_vertical(
compose_vertical(
compose_horizontal(
merkle_proof()
.relabel("root", "old_maker_buy_root")
.relabel("leaf", "old_maker_buy_leaf"),
merkle_proof()
.relabel("root", "new_maker_buy_root")
.relabel("leaf", "new_maker_buy_leaf"),
),
compose_horizontal(
merkle_proof()
.relabel("root", "old_maker_sell_root")
.relabel("leaf", "old_maker_sell_leaf"),
merkle_proof()
.relabel("root", "new_maker_sell_root")
.relabel("leaf", "new_maker_sell_leaf"),
),
),
compose_vertical(
compose_horizontal(
merkle_proof(),
merkle_proof(),
),
compose_horizontal(
merkle_proof(),
merkle_proof(),
),
),
),
);
air.add_constraint(
(air["old_maker_buy_root"]
- air["old_maker_sell_root"]
) * air.on_row(0)
);
air.relabel("old_maker_buy_root", "initial_balance_root");
air.relabel("new_maker_sell_root", "final_balance_root");
}
fn starkdex(
initial_balances: Balances,
txs: Vec<Transaction>
) -> (Balances, AirComponent) {
let mut component = txs
.pad_to_power_of_two(EMPTY_TRANSACTION)
.map(transaction)
.binary_tree(compose_vertical)
}
struct Projection {
}
impl Projection {
fn trace(usize, isize) -> RationalExpression;
}
trait Component {
type Claim;
type Witness;
fn dimensions(&self) -> [usize];
fn set_projection(projection: &[(usize, (usize, isize))]);
fn constraints(&self, claim: &Claim) -> Vec<RationalExpression>;
fn witness() -> Claim;
}