AIR neural networks without range checks

[damip]

Field-Native Algebraically-Bounded Deep Model for STARK AIR

1. Purpose

This specification defines a field-native deep model that can be:

• trained offline with backpropagation,
• executed as an inference trace over a prime field $\mathbb{F}_p$,
• proven in a zkSTARK using only polynomial AIR constraints,
• enforced without range checks,
• and whose row-to-row transition is unique.

This model does not implement bounded signed-integer arithmetic. It implements a field-native dynamical system whose hidden state is constrained to remain inside a low-degree algebraic set.

---

2. Semantics

2.1 What is proved

The proof establishes that:

1. every trace row lies on a fixed algebraic state space,
2. every next row is the unique valid update of the current row under the frozen model parameters,
3. therefore the whole trace is the unique valid inference trace of the model.

2.2 What is not proved

This specification does not prove:

• that values are small signed integers,
• that ordinary integer overflow cannot happen,
• that field operations coincide with integer operations.

There are no range checks. All correctness is purely in $\mathbb{F}_p$.

---

3. State Space

Each hidden feature is represented as a pair of field elements:

$$ g_i = (u_i, v_i) \in \mathbb{F}_p^2 $$

subject to the conic invariant

$$ u_i^2 - \Delta v_i^2 = 1 $$

where:

• $p$ is an odd prime,
• $\Delta \in \mathbb{F}_p^\times$ is a fixed non-square constant.

This defines the norm-one conic / 1-dimensional torus:

$$ C_\Delta = {(u,v) \in \mathbb{F}_p^2 \mid u^2 - \Delta v^2 = 1}. $$

All hidden states must lie in $C_\Delta$.

---

4. Group Law

Define the binary operation

$$ (a,b) \star (s,t) := (as + \Delta bt,; at + bs). $$

If both inputs lie on the conic, then the output also lies on the conic.

The identity element is:

$$ \mathbf{1} := (1,0). $$

The inverse is:

$$ (u,v)^{-1} = (u,-v). $$

So $C_\Delta$ is closed under $\star$.

---

5. Trace Layout

Use two trace columns per feature.

For feature $i$:

$$ x_{2i} = u_i,\qquad x_{2i+1} = v_i. $$

If the current row contains columns $x_c$, then the next row contains $x'_c$.

---

6. Layer Structure

Each layer acts on pairs of features.

Let one block consume two feature-pairs:

• first feature:
  $$
  g_1 = (x_c, x_{c+1})
  $$
• second feature:
  $$
  g_2 = (x_d, x_{d+1})
  $$

with $c,d$ even and typically $d = c + 2$ in the simplest layout.

Each block performs:

1. a fixed nonlinear power map on each feature,
2. coupling through the conic group law,
3. a trainable translation on the conic.

---

7. Nonlinear Power Map

Choose a fixed exponent $e$ such that:

• $e$ is odd,
• $e$ is small,
• $e$ is coprime to $|C_\Delta(\mathbb{F}_p)|$.

For the simplest implementation, choose:

$$ e = 3 $$

and ensure:

$$ \gcd(3,; |C_\Delta(\mathbb{F}_p)|) = 1. $$

For the standard non-square-$\Delta$ conic over $\mathbb{F}_p$, this usually means:

$$ \gcd(3,; p + 1) = 1. $$

The cubic map is:

$$
3 =
\left(
u^3 + 3\Delta u v^2,;
3u^2v + \Delta v^3
\right).
$$

Define:

$$
\operatorname{cube}(u,v) := 3.
$$

---

8. Trainable Parameters

Each output feature has a trainable translation parameter:

$$ \theta = (a,b) $$

which must also lie on the conic:

$$ a^2 - \Delta b^2 = 1. $$

These parameters are learned offline, then frozen for proving.

For one 2-feature block, use two trainable parameters:

$$ \theta_1 = (a_1,b_1),\qquad \theta_2 = (a_2,b_2). $$

---

9. Coupled Block Definition

Let:

$$ g_1 = (x_c, x_{c+1}),\qquad g_2 = (x_d, x_{d+1}). $$

First compute the cubic images:

$$
(A_1,B_1) := 3
$$

$$
(A_2,B_2) := 3
$$

that is,

$$ A_1 = x_c^3 + 3\Delta x_c x_{c+1}^2 $$

$$ B_1 = 3x_c^2x_{c+1} + \Delta x_{c+1}^3 $$

$$ A_2 = x_d^3 + 3\Delta x_d x_{d+1}^2 $$

$$ B_2 = 3x_d^2x_{d+1} + \Delta x_{d+1}^3 $$

Then perform coupling:

$$ (C_1,D_1) := (A_1,B_1) \star (x_d, x_{d+1}) $$

$$ (C_2,D_2) := (A_2,B_2) \star (x_c, x_{c+1}) $$

so

$$ C_1 = A_1 x_d + \Delta B_1 x_{d+1} $$

$$ D_1 = A_1 x_{d+1} + B_1 x_d $$

$$ C_2 = A_2 x_c + \Delta B_2 x_{c+1} $$

$$ D_2 = A_2 x_{c+1} + B_2 x_c $$

Finally apply trainable translations:

$$ (x'_c,; x'_{c+1}) := \theta_1 \star (C_1,D_1) $$

$$ (x'_d,; x'_{d+1}) := \theta_2 \star (C_2,D_2) $$

which gives:

$$ x'_c = a_1 C_1 + \Delta b_1 D_1 $$

$$ x'_{c+1} = a_1 D_1 + b_1 C_1 $$

$$ x'_d = a_2 C_2 + \Delta b_2 D_2 $$

$$ x'_{d+1} = a_2 D_2 + b_2 C_2 $$

This is one nonlinear bijective block.

---

10. AIR Constraints

10.1 State Membership Constraints

For every feature-pair $(x_{2i}, x_{2i+1})$ in every row:

$$ x_{2i}^2 - \Delta x_{2i+1}^2 - 1 = 0 $$

For every corresponding next-row pair:

$$ (x'_{2i})^2 - \Delta (x'_{2i+1})^2 - 1 = 0 $$

These ensure the state remains on the conic.

10.2 Parameter Validity Constraints

For each frozen trainable parameter pair $(a_j,b_j)$:

$$ a_j^2 - \Delta b_j^2 - 1 = 0 $$

If parameters are public constants, this can be checked once outside the trace or treated as setup assumptions.

10.3 Transition Constraints for One 2-Feature Block

Given current row columns:

• $x_c, x_{c+1}$
• $x_d, x_{d+1}$

and next row columns:

• $x'c, x'{c+1}$
• $x'd, x'{d+1}$

enforce the following.

Cubic transforms

$$ A_1 - \left(x_c^3 + 3\Delta x_c x_{c+1}^2\right) = 0 $$

$$ B_1 - \left(3x_c^2x_{c+1} + \Delta x_{c+1}^3\right) = 0 $$

$$ A_2 - \left(x_d^3 + 3\Delta x_d x_{d+1}^2\right) = 0 $$

$$ B_2 - \left(3x_d^2x_{d+1} + \Delta x_{d+1}^3\right) = 0 $$

Coupling

$$ C_1 - \left(A_1 x_d + \Delta B_1 x_{d+1}\right) = 0 $$

$$ D_1 - \left(A_1 x_{d+1} + B_1 x_d\right) = 0 $$

$$ C_2 - \left(A_2 x_c + \Delta B_2 x_{c+1}\right) = 0 $$

$$ D_2 - \left(A_2 x_{c+1} + B_2 x_c\right) = 0 $$

Trainable translations

$$ x'_c - \left(a_1 C_1 + \Delta b_1 D_1\right) = 0 $$

$$ x'_{c+1} - \left(a_1 D_1 + b_1 C_1\right) = 0 $$

$$ x'_d - \left(a_2 C_2 + \Delta b_2 D_2\right) = 0 $$

$$ x'_{d+1} - \left(a_2 D_2 + b_2 C_2\right) = 0 $$

---

11. Fully Inlined Version

If no helper columns are used, the transition can be written directly as:

$$ x'_c - \left( a_1(A_1 x_d + \Delta B_1 x_{d+1}) + \Delta b_1(A_1 x_{d+1} + B_1 x_d) \right) = 0 $$

$$ x'_{c+1} - \left( a_1(A_1 x_{d+1} + B_1 x_d) + b_1(A_1 x_d + \Delta B_1 x_{d+1}) \right) = 0 $$

$$ x'_d - \left( a_2(A_2 x_c + \Delta B_2 x_{c+1}) + \Delta b_2(A_2 x_{c+1} + B_2 x_c) \right) = 0 $$

$$ x'_{d+1} - \left( a_2(A_2 x_{c+1} + B_2 x_c) + b_2(A_2 x_c + \Delta B_2 x_{c+1}) \right) = 0 $$

with

$$ A_1 = x_c^3 + 3\Delta x_c x_{c+1}^2,\qquad B_1 = 3x_c^2x_{c+1} + \Delta x_{c+1}^3 $$

$$ A_2 = x_d^3 + 3\Delta x_d x_{d+1}^2,\qquad B_2 = 3x_d^2x_{d+1} + \Delta x_{d+1}^3 $$

This is simpler to read but higher degree in AIR.

---

12. Recommended Low-Degree Implementation

To keep AIR degree low, use helper columns.

12.1 Helper Columns for One Feature-Pair

For pair $(x_c, x_{c+1})$, add:

$$ s_c,; t_c,; m_c,; A_c,; B_c $$

with constraints:

$$ s_c - x_c^2 = 0 $$

$$ t_c - x_{c+1}^2 = 0 $$

$$ m_c - x_c x_{c+1} = 0 $$

$$ A_c - \left(x_c s_c + 3\Delta x_c t_c\right) = 0 $$

$$ B_c - \left(3 s_c x_{c+1} + \Delta x_{c+1} t_c\right) = 0 $$

Do the same for $(x_d, x_{d+1})$.

Then use:

$$ A_1 := A_c,\quad B_1 := B_c,\quad A_2 := A_d,\quad B_2 := B_d. $$

This keeps most constraints quadratic.

12.2 Helper Columns for Coupling

Add:

$$ C_1,; D_1,; C_2,; D_2 $$

with constraints exactly as in Section 10.3.

This makes the transition mostly bilinear.

---

13. Why the Transition Is Unique

The transition is unique because it is a composition of bijections on $C_\Delta$:

1. the cubic map $[3]$ is bijective if $3$ is invertible modulo the group order,
2. the group law with a fixed valid feature is bijective,
3. translation by a valid parameter $\theta = (a,b) \in C_\Delta$ is bijective.

Therefore each block defines a bijection from valid input state to valid output state.

As a result:

• for each valid current row, there is exactly one valid next row,
• the prover may supply next-row values nondeterministically,
• but the AIR constraints force them to equal the unique valid update.

---

14. Why There Are No Range Checks

This construction uses no range checks.

The reason is:

• the state is bounded algebraically by the conic equation,
• not bounded numerically as a small integer interval.

So the invariant is:

$$ u^2 - \Delta v^2 = 1 $$

not:

$$ u \in [-B,B]. $$

All correctness is field-native.

---

15. Model Stacking

A deep network is formed by stacking multiple blocks with permutations between them.

Let the hidden state have $2n$ columns:

$$ (x_0,x_1),; (x_2,x_3),; \dots,; (x_{2n-2},x_{2n-1}). $$

A layer consists of:

1. partition these feature-pairs into disjoint adjacent pairs,
2. apply one 2-feature block to each pair,
3. permute feature-pairs,
4. repeat.

A permutation layer is just column relabeling or copy constraints, for example:

$$ x'_c - x_d = 0. $$

---

16. Input and Output Encoding

16.1 Input

Inputs must be embedded into conic points.

A simple implementation is:

• preprocess inputs offline into valid conic points,
• place those points into the first trace row,
• prove that the first row matches the claimed encoded input.

16.2 Output

Outputs may be:

• the final conic coordinates directly,
• or a deterministic projection from the final conic state.

If using a projection, define it as a polynomial map over the final row and prove it with AIR constraints.

---

17. Offline Training

17.1 What is trainable

Recommended trainable objects:

• conic translation parameters $\theta_j = (a_j,b_j)$,
• optional scalar gates if constrained algebraically,
• optional mixing schedules chosen from a small discrete family outside the proof.

Recommended fixed objects:

• $p$,
• $\Delta$,
• the exponent $e=3$,
• the pairing/permutation structure,
• the number of layers.

17.2 Parameterization during training

To ensure trainable parameters remain on the conic, use one of:

Option A: projected parameters

Train unconstrained values $(\tilde a,\tilde b)$, then periodically project onto:

$$ a^2 - \Delta b^2 = 1. $$

Option B: intrinsic parameterization

Parameterize $(a,b)$ by repeated valid conic compositions from a seed point.

Option C: penalty method

Add training loss term:

$$ \lambda \cdot (a^2 - \Delta b^2 - 1)^2 $$

then project once after training.

At proof time, only the final frozen values matter.

17.3 Surrogate arithmetic for training

Training is done offline with ordinary differentiable computation over floating point or high-precision arithmetic, using the same algebraic formulas as the inference model.

After training:

1. quantize / map learned parameters into $\mathbb{F}_p$,
2. enforce $a^2 - \Delta b^2 = 1$,
3. freeze parameters,
4. use the frozen field-valued model for inference and proof.

---

18. Minimal AIR Template

For each row and each feature-pair index $i$:

Membership

$$ x_{2i}^2 - \Delta x_{2i+1}^2 - 1 = 0 $$

$$ (x'_{2i})^2 - \Delta (x'_{2i+1})^2 - 1 = 0 $$

Transition

If $(2i,2i+1)$ and $(2j,2j+1)$ are paired in this layer, enforce the block constraints from Section 10.3.

Permutation layer

If the next layer changes pairing, add copy/permutation constraints.

---

19. Concrete Example with 4 State Columns

Let the row state be:

• feature 1:
  $$
  (x_0,x_1)
  $$
• feature 2:
  $$
  (x_2,x_3)
  $$

Next row:

• $(x'_0,x'_1)$
• $(x'_2,x'_3)$

Trainable parameters:

$$ \theta_1 = (a_1,b_1),\qquad \theta_2 = (a_2,b_2). $$

Membership constraints

$$ x_0^2 - \Delta x_1^2 - 1 = 0 $$

$$ x_2^2 - \Delta x_3^2 - 1 = 0 $$

$$ (x'_0)^2 - \Delta (x'_1)^2 - 1 = 0 $$

$$ (x'_2)^2 - \Delta (x'_3)^2 - 1 = 0 $$

Parameter constraints

$$ a_1^2 - \Delta b_1^2 - 1 = 0 $$

$$ a_2^2 - \Delta b_2^2 - 1 = 0 $$

Cubic helper definitions

$$ A_1 - (x_0^3 + 3\Delta x_0 x_1^2) = 0 $$

$$ B_1 - (3x_0^2x_1 + \Delta x_1^3) = 0 $$

$$ A_2 - (x_2^3 + 3\Delta x_2 x_3^2) = 0 $$

$$ B_2 - (3x_2^2x_3 + \Delta x_3^3) = 0 $$

Coupling helpers

$$ C_1 - (A_1 x_2 + \Delta B_1 x_3) = 0 $$

$$ D_1 - (A_1 x_3 + B_1 x_2) = 0 $$

$$ C_2 - (A_2 x_0 + \Delta B_2 x_1) = 0 $$

$$ D_2 - (A_2 x_1 + B_2 x_0) = 0 $$

Output definitions

$$ x'_0 - (a_1 C_1 + \Delta b_1 D_1) = 0 $$

$$ x'_1 - (a_1 D_1 + b_1 C_1) = 0 $$

$$ x'_2 - (a_2 C_2 + \Delta b_2 D_2) = 0 $$

$$ x'_3 - (a_2 D_2 + b_2 C_2) = 0 $$

This is a complete one-layer AIR block.

---

20. Field Selection Rules

Choose the field prime $p$ such that:

1. $p$ is odd,
2. $\Delta$ is a non-square in $\mathbb{F}_p$,
3. the chosen exponent $e$ is coprime to the group order,
4. all constants used by the model are represented in $\mathbb{F}_p$.

For the cubic map, ensure:

$$ \gcd(3,; p + 1) = 1. $$

If this fails, choose another odd exponent such as $e=5$, provided:

$$ \gcd(5,; p + 1) = 1. $$

---

21. Soundness Statement

Given:

• a valid initial row,
• valid frozen parameters,
• the AIR constraints from this specification,
• and the fixed layer schedule,

the proof establishes that:

$$ \forall t,\quad X_{t+1} = F_\theta(X_t) $$

where:

• $X_t$ is the row state at time $t$,
• $F_\theta$ is the composed layer update over $C_\Delta^n$,
• and $F_\theta$ is bijective on the valid state space.

Hence the trace is the unique valid inference trace of the frozen field-native model.

---

22. Implementation Checklist

• Choose odd prime $p$
• Choose non-square $\Delta \in \mathbb{F}_p$
• Choose exponent $e$ with $\gcd(e, p+1)=1$
• Define number of features $n$
• Allocate 2 trace columns per feature
• Define layer pairing schedule
• Define permutation schedule
• Train conic translation parameters offline
• Freeze parameters $(a_j,b_j)$
• Verify $a_j^2 - \Delta b_j^2 = 1$
• Generate inference trace row by row
• Add membership constraints
• Add helper columns for low AIR degree
• Add block transition constraints
• Add boundary constraints for input/output claims

---

23. Summary

This specification gives a deep model with the following properties:

• field-native
• nonlinear
• bijective per layer
• unique next-row witness
• algebraically bounded
• no range checks
• simple polynomial AIR constraints
• trainable offline

The core invariant is not numerical boundedness, but algebraic boundedness:

$$ u^2 - \Delta v^2 = 1. $$

The core transition is a composition of:

• a bijective nonlinear power map,
• conic-group coupling,
• trainable conic translation.

This is the intended implementation target.