|
| template<typename AllEntities > |
| static bool | skip (const AllEntities &in) |
| |
| template<typename Accumulator , typename AllEntities > |
| static Accumulator | get_read_selector (const AllEntities &in) |
| | Compute scalar for read term in log derivative lookup argument.
|
| |
| template<typename Accumulator , typename AllEntities , typename Parameters > |
| static Accumulator | compute_table_term (const AllEntities &in, const Parameters ¶ms) |
| | Write term denominator: value + databus_id·β + γ.
|
| |
| template<typename Accumulator , typename AllEntities , typename Parameters > |
| static Accumulator | compute_lookup_term (const AllEntities &in, const Parameters ¶ms) |
| | Read term denominator: w_l + w_r·β + γ. Bus-independent.
|
| |
| template<typename Polynomials > |
| static void | compute_logderivative_inverse (Polynomials &polynomials, auto &relation_parameters, const size_t circuit_size, const size_t start_index=0) |
| | Compute the column's inverse polynomial \(I_i = (L_i · T_i)^{-1}\) at active rows.
|
| |
| template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters > |
| static void | accumulate (ContainerOverSubrelations &accumulator, const AllEntities &in, const Parameters ¶ms, const FF &scaling_factor) |
| | Accumulate this column's four subrelation contributions. (1a) (I*L*T - 1) * is_read = 0 (1b) (I*L*T - 1) * count = 0 (2) (is_read*T - count*L)*I = 0 (linearly dependent — summed across trace) (3) (1 - indicator) * count = 0 (read_counts vanish outside the bus's data rows)
|
| |
template<typename FF_, auto ValueId, auto ReadCountsId, auto InversesId, auto IndicatorId, auto SelectorId>
class bb::SingleBusLookupRelationImpl< FF_, ValueId, ReadCountsId, InversesId, IndicatorId, SelectorId >
Log-derivative lookup argument for a single DataBus column.
Each bus column (kernel_calldata, app_calldata_0, …, returndata) is its own table; this relation establishes that reads from one column are well-formed. The relation is parameterized on the EntityId values for the column's five entities — value, read_counts, inverses, indicator, selector — so the flavor binds a concrete bus at typedef time and the C++ side sees a fixed-shape relation with no bus loop. A flavor with N buses simply lists N independent SingleBusLookupRelation instantiations in its Relations_<FF> tuple.
Per-column subrelations (4 total):
(1a) Inverse correctness on read rows: (I · L · T − 1) · is_read = 0 (per-row, deg 5) (1b) Inverse correctness on write rows: (I · L · T − 1) · count = 0 (per-row, deg 4) (2) Lookup identity (linearly dep'nt): Σ_rows (is_read · T − count · L) · I = 0 (deg 4) (3) Read-count locality: (1 − indicator) · count = 0 (per-row, deg 2)
Where L = w_l + w_r·β + γ (read term) and T = value + databus_id·β + γ (table term). is_read = q_busread · selector. Subrelations (1a)/(1b)/(2) all share length 6 to amortize the common I·L·T − 1 factor across rows; (3) uses length 3 since it has no shared computation.
Definition at line 40 of file databus_lookup_relation.hpp.
1.9.8