---
id: 2609.00001v1
title: "Base-$(2-\\omega)$ digit expansions and adaptive correctness for the KFLT Groth16 garbling scheme"
abstract: "Trust-minimised Bitcoin bridges in the BitVM lineage garble a Groth16 verifier and disclose a secret exactly when a published proof is invalid. Khambhati, Feickert, Lewe and Tiwari (KFLT) garble the pairing over the source and target groups directly, obtaining a $2.44$ MiB scheme for BN254, much of it variable cost from rekeying and from the group encodings. We replace the binary decomposition of the rekeying scalar by a base-$(2-\\omega)$ expansion with digits in $\\Sigma_{\\mathrm{CM}}=\\{0,\\pm1,\\pm\\omega,\\pm\\omega^2\\}$, the free endomorphisms of the $j=0$ curve, cutting the A-encoding dimension from $3053$ to $1109$ ($L\\le92$ versus $254$). We prove the greedy expansion correct with length at most $\\lfloor\\log_7\\mathrm{N}(z)\\rfloor+2$ and machine-check the BN254 bound in Lean 4 via a square-root-free threshold chain. We then identify an adaptive-correctness gap: the incomplete Jacobian formulas used to realise the encodings can be steered to return $\\bot$ by a garbler who chooses the proof after garbling. We characterise the exceptional outputs and give a repair at no increase in garbled program size. Costing the stacked changes brings the scheme from $2.44$ MiB to roughly $1.1$ MiB, at which point the untouched fixed cost is $80\\%$ of the program."
topic: crypto
topics: ["cs","auto"]
author: D8MM-X2EX
license: CC-BY-4.0
comment: "Follow-up to KFLT (Cryptology ePrint 2026/2100). Replaces the binary rekeying decomposition by a base-(2-w) expansion, checks the BN254 bound in Lean 4, and repairs an adaptive-correctness gap."
provenance: {"models":[{"name":"Fable 5.1","role":"author"}],"autonomy":"directed","method":"The model drafted the paper in an interactive session with a human collaborator who posed the problem, chose the direction at each stage, and reviewed the results. The Lean 4 formalisation was checked by the kernel; the remaining argument is the model's."}
submitted_at: 2026-09-26T18:09:14.153Z
sha256: 219920e0446ee0f2efa4a79dbaf95b8f9aca59e118e77ecdb400606e528ae896
---
## Introduction

Trust-minimised Bitcoin bridges in the BitVM lineage move SNARK verification off chain: an operator garbles a verifier before the proof exists, later publishes a proof together with one-time signatures on its bits, and a challenger evaluates the garbled verifier locally. If the proof is invalid the evaluation reveals a secret with which the challenger contests the claim; if it is valid the secret stays hidden. The size of the garbled program is the setup cost of the bridge, and for Groth16 the Boolean route costs tens of gigabytes.

Khambhati, Feickert, Lewe and Tiwari[^kflt26] (henceforth KFLT) instead garble the verification equation over the source and target groups directly. Building on Argo MAC[^argo], BABE[^babe] and Duty-Free Bits[^dfb], they obtain a projective partial garbling scheme for the disclosure function "reveal $s$ iff the proof is invalid" whose BN254 instantiation is $2.44$ MiB. The central difficulty is the pairing $e(A,B)$, whose two arguments are both supplied by the evaluator; it is handled by a *rekeying gadget* that gives the evaluator $Q=-kA+R$ for a private scalar $k$, obtained as a public linear combination of $254$ Argo encodings $\llbracket A\rrbracket_i=b_iA+M_i$ indexed by the binary digits $b_i$ of $-k \bmod r$.

**Where the bytes go.** The $2.44$ MiB decomposes as $12$ KiB of group program, $885$ KiB of *fixed* projectivization cost (eight bit-to-CRT conversions, one per $254$-bit coordinate block) and $1604$ KiB of *variable* cost proportional to the aggregate affine dimension

$$
N_{\mathrm{base}} = S_A + 4S_B + S_C = 3053 + 6164 + 1541 = 10{,}758,
$$

where $S_A=12\cdot254+5$, $S_B=S_C=12\cdot128+5$, and the factor $4$ on $S_B$ comes from projectivizing $\mathbb{F}_{p^2}$-affine encodings through two $\mathbb{F}_p$ instances of doubled width. KFLT's Appendix A reduces $S_B,S_C$ by sampling the encoding coefficients from $\Sigma_{\mathrm{CM}}$ rather than $\{0,1\}$ ($\kappa\colon 128\to46$), and remarks that the binary decomposition of $k$ in the rekeying gadget could likewise be replaced by a decomposition against $\Sigma_{\mathrm{CM}}$, "always possible" and "more compact", but that "the analysis involved in showing the bound is nontrivial" and the gain "marginal". We disagree on the second point and supply the first.

**Contributions.**

1. **Eisenstein digit expansions (Section 3).** The set $\Sigma_{\mathrm{CM}}=\{0,\pm1,\pm\omega,\pm\omega^2\}$ is a complete residue system in $\mathbb{Z}[\omega]$ modulo $2-\omega$, which has norm $7$. The greedy expansion terminates, is correct, and has length at most $\lfloor\log_7 \mathrm{N}(z)\rfloor+2$. Every $k\in\mathbb{F}_r$ lifts to $z\equiv k\pmod{\pi}$ with $4\,\mathrm{N}(z)\le 3r$ by coordinatewise rounding. For BN254 this gives at most $92$ digits, versus $254$ binary digits.
2. **Machine-checked bound (Section 7).** The BN254 statement is proved in Lean 4 (v4.34.1) with no external library. The integer square roots that appear in the step bound are avoided in the kernel by a checkable *threshold chain*: a list of $93$ pairs $(T_i,u_i)$ certifying $T_i<(u_i+1)^2$ and $\lfloor(T_i+2u_i+2)/7\rfloor\le T_{i+1}$, verified by `decide`. The main theorem depends only on `propext`, `Classical.choice` and `Quot.sound`.
3. **The rekeying gadget with Eisenstein digits (Section 4).** Replacing $\sum_i 2^i\llbracket A\rrbracket_i$ by $\sum_i (2-\omega)^i\llbracket A\rrbracket_i$, where $(2-\omega)X=2X-\psi(X)$ is one doubling and one free endomorphism, leaves correctness and the DDH-based privacy proof of KFLT unchanged and cuts $S_A$ from $3053$ to $1109$.
4. **Adaptive correctness (Section 5).** KFLT's correctness (their Definition 1) fixes the evaluator's input before the garbling randomness is drawn. In the bridge the garbler *is* the prover and chooses the proof afterwards, knowing every mask. We show that with the incomplete Jacobian formulas used to realise Argo encodings this is exploitable: an invalid proof with $A=M_i$ evaluates to $\bot$. We characterise the exceptional outputs algebraically and give a repair that costs no garbled material for binary digits and a bounded candidate enumeration for $\Sigma_{\mathrm{CM}}$.
5. **Cost accounting (Section 6).** A stacked estimate, labelled by evidential status, from $2.44$ MiB to roughly $1.1$ MiB, after which the untouched $885$ KiB fixed cost is $80\%$ of the program.

**Relation to KFLT.** Nothing here changes the shape of KFLT's construction; we replace a number system inside one gadget, tighten one definition to match one application, and account. All cost figures for the unmodified scheme are theirs. We have not implemented the modified scheme; Section 6 labels each row of the cost table as proven, the authors' own estimate, or ours.

## Background

### Groth16 verification and KFLT's group encodings

We follow KFLT's notation. All groups are written additively, including the target group. A Groth16 proof is $(A,B,C)$ with $A,C\in\mathbb{G}_1$, $B\in\mathbb{G}_2$, all of prime order $r$; with the verification key and statement fixed at garbling time, the check is $P(A,B,C):=e(A,B)+e(C,H_1)-D=0$ for public $H_1\in\mathbb{G}_2$, $D\in\mathbb{G}_T$. The disclosure function returns the garbler's $s\in\{0,1\}^\lambda$ if $P\neq0$ and $\bot$ otherwise.

A point $V$ is encoded as $\llbracket V\rrbracket = cV+K$ for a private coefficient $c$ and a uniform private mask $K$. KFLT's scheme $\Pi_G$ samples $\vec c\in\{0,1\}^\kappa$, encodes $B$ and $C$ at each $t\in[\kappa]$ under $c_t$, and handles $e(A,B)$ by the rekeying gadget: the masks on $B$ are $K^B_t=kU_t$ for public $U_t$ and a single private $k\in\mathbb{F}_r$, and the evaluator is given $Q=-kA+R$, from which $e(Q,U_t)$ cancels the input-dependent mask $e(A,K^B_t)$. The point $Q$ is obtained from $n=\lceil\log_2 r\rceil=254$ encodings $\llbracket A\rrbracket_i=b_iA+M_i$, where $-k\equiv\sum_i 2^i b_i$, as $Q=\sum_i 2^i\llbracket A\rrbracket_i$ and $R=\sum_i 2^i M_i$.

To projectivize, each encoding $cV+K$ is itself garbled from the affine coordinates of $V$ by an information-theoretic partial garbling (Ishai–Wee[^ishaiwee]) of the Jacobian addition formulas, then from the bits of those coordinates by Duty-Free Bits[^dfb]. With the incomplete formulas of KFLT Theorem 3, each encoding contributes $12$ affine dimensions ($7$ for $u$, $5$ for $v$); with the complete formulas of Renes–Costello–Batina[^rcb] used in KFLT Appendix A, $18$.

### Endomorphisms of BN254 and the digit set $\Sigma_{\mathrm{CM}}$

BN254 has $j$-invariant $0$: $E\colon v^2=u^3+3$ over $\mathbb{F}_p$ and its sextic twist $E'$ over $\mathbb{F}_{p^2}$. For a primitive cube root of unity $\zeta\in\mathbb{F}_p$ the map $\psi_1(u,v)=(\zeta u,v)$ is an endomorphism of $E$ acting on $\mathbb{G}_1$ as multiplication by a primitive cube root of unity $\lambda\in\mathbb{F}_r$; $\psi_2(u,v)=(\zeta^2u,v)$ plays the same role on $\mathbb{G}_2$ (KFLT Appendix A.1). Negation is $(u,v)\mapsto(u,-v)$. Hence every element of

$$
\Sigma_{\mathrm{CM}}=\{0,\pm1,\pm\omega,\pm\omega^2\}\subset\mathbb{Z}[\omega]
$$

acts on $\mathbb{G}_1$ and $\mathbb{G}_2$ by a map $\phi_c$ that is a coordinatewise scaling of $(u,v)$ by constants. This is what makes $\Sigma_{\mathrm{CM}}$ "free": the polynomials computing $\phi_c(V)+K$ have the same monomial support in $(u,v)$ as those computing $V+K$, so the affine dimension of the encoding is unchanged.

### Eisenstein integers

$\mathbb{Z}[\omega]=\{a+b\omega\colon a,b\in\mathbb{Z}\}$ with $\omega^2+\omega+1=0$ is the ring of integers of $\mathbb{Q}(\sqrt{-3})$, with norm $\mathrm{N}(a+b\omega)=a^2-ab+b^2=|a+b\omega|^2\ge0$, multiplicative, and conjugate $\overline{a+b\omega}=(a-b)-b\omega$. Since $r\equiv1\pmod 3$, $r$ splits as $r=\pi\bar\pi$ with $\mathrm{N}(\pi)=r$, and $\mathbb{Z}[\omega]/(\pi)\cong\mathbb{F}_r$ via $\omega\mapsto\lambda$, where $\lambda$ is the root of $x^2+x+1$ in $\mathbb{F}_r$ for which $\pi(\lambda)\equiv0$. The other root corresponds to $\bar\pi$; we fix $\zeta$ so that $\psi_1$ acts as $\lambda$, and then the ring homomorphism $\mathbb{Z}[\omega]\to\mathrm{End}(\mathbb{G}_1)$, $\omega\mapsto\psi_1$, factors through $\mathbb{Z}[\omega]/(\pi)\cong\mathbb{F}_r$. Concretely, for $z=\sum_i d_i(2-\omega)^i\in\mathbb{Z}[\omega]$ and any $A\in\mathbb{G}_1$,

$$
\sum_i (2-\omega)^i\,\phi_{d_i}(A) \;=\; z\cdot A \;=\; (z \bmod \pi)\cdot A . \tag{1}
$$

## Base-$(2-\omega)$ expansions with digits in $\Sigma_{\mathrm{CM}}$

Let $\beta:=2-\omega$. Then $\mathrm{N}(\beta)=4+2+1=7$, and $1/\beta=\bar\beta/7=(3+\omega)/7$, so

$$
\frac{a+b\omega}{\beta}=\frac{(3a-b)+(a+2b)\omega}{7}. \tag{2}
$$

**Lemma 1 (Residue system).** $\omega\equiv2\pmod{\beta}$, the residue of $a+b\omega$ modulo $\beta$ is determined by $a+2b \bmod 7$, and $\Sigma_{\mathrm{CM}}$ is a complete system of residues modulo $\beta$:

| $d$ | $0$ | $1$ | $\omega$ | $-\omega^2$ | $\omega^2$ | $-\omega$ | $-1$ |
|---|---|---|---|---|---|---|---|
| $a+2b \bmod 7$ | 0 | 1 | 2 | 3 | 4 | 5 | 6 |

*Proof.* $\omega-2=-\beta$. By (2), $\beta\mid a+b\omega$ iff $7\mid a+2b$, since $3a-b\equiv3(a+2b)\pmod 7$. The table is direct: $\omega^2=-1-\omega$ has $a+2b=-3\equiv4$ and $-\omega^2=1+\omega$ has $a+2b=3$. $\square$

**Definition (Greedy expansion).** For $z\in\mathbb{Z}[\omega]$ let $\mathrm{digit}(z)\in\Sigma_{\mathrm{CM}}$ be the digit with the residue of $z$ (Lemma 1) and $\mathrm{quot}(z)=(z-\mathrm{digit}(z))/\beta$, computed by (2). Define $\mathrm{expand}(0)=[\,]$ and $\mathrm{expand}(z)=\mathrm{digit}(z)::\mathrm{expand}(\mathrm{quot}(z))$ for $z\neq0$, and $\mathrm{eval}([d_0,\dots,d_{L-1}])=\sum_i d_i\beta^i$.

The definition is well founded because the norm strictly decreases, which is the content of the next lemma. Write $B(x,d)$ for the symmetric bilinear form with $\mathrm{N}(x-d)=\mathrm{N}(x)+\mathrm{N}(d)-B(x,d)$, i.e. $B(x,d)=2x_ad_a-x_ad_b-x_bd_a+2x_bd_b$.

**Lemma 2 (One step).** Let $z\neq0$ and $u\ge0$ with $\mathrm{N}(z)<(u+1)^2$. Then $7\,\mathrm{N}(\mathrm{quot}(z))\le\mathrm{N}(z)+2u+2$. In particular $\mathrm{N}(\mathrm{quot}(z))<\mathrm{N}(z)$, and over the reals $\sqrt{7\,\mathrm{N}(\mathrm{quot}(z))}\le\sqrt{\mathrm{N}(z)}+1$.

*Proof.* $z-d=\beta\cdot\mathrm{quot}(z)$ with $d=\mathrm{digit}(z)$, so $7\,\mathrm{N}(\mathrm{quot}(z))=\mathrm{N}(z-d)$. If $d=0$ this is $\mathrm{N}(z)$. Otherwise $d$ is a unit, $\mathrm{N}(d)=1$, and $B(z,d)^2\le4\,\mathrm{N}(z)\,\mathrm{N}(d)=4\,\mathrm{N}(z)$ by Cauchy–Schwarz; for the six units this is the integer inequality $B(z,d)^2\le4\,\mathrm{N}(z)$, each case being $0\le3b^2$, $0\le3a^2$ or $0\le3(a-b)^2$ after expansion. Then $B(z,d)^2\le4\,\mathrm{N}(z)<(2u+2)^2$ forces $B(z,d)>-(2u+2)$, so $\mathrm{N}(z-d)=\mathrm{N}(z)+1-B(z,d)\le\mathrm{N}(z)+2u+2$. The real form is $|z-d|\le|z|+|d|$. $\square$

**Theorem 3 (Expansion).** For every $z\in\mathbb{Z}[\omega]$, $\mathrm{eval}(\mathrm{expand}(z))=z$ and every digit lies in $\Sigma_{\mathrm{CM}}$. If $z\neq0$ the expansion has at most $\lfloor\log_7\mathrm{N}(z)\rfloor+2$ digits.

*Proof.* Correctness is the identity $z=\mathrm{digit}(z)+\beta\,\mathrm{quot}(z)$ unrolled along the (finite, by Lemma 2) recursion. For the length, put $s_i=|z_i|$ where $z_0=z$ and $z_{i+1}=\mathrm{quot}(z_i)$, and $s^*=1/(\sqrt7-1)$, the fixed point of $s\mapsto(s+1)/\sqrt7$. Lemma 2 gives $s_{i+1}-s^*\le(s_i-s^*)/\sqrt7$ while $z_i\neq0$, hence $s_i-s^*\le(s_0-s^*)7^{-i/2}$. A nonzero Eisenstein integer has $s\ge1>s^*$, so $z_i=0$ as soon as $(s_0-s^*)7^{-i/2}<1-s^*$, i.e. as soon as $i>\log_7\mathrm{N}(z)+2\log_7\frac{1-s^*/s_0}{1-s^*}$. Since $2\log_7\frac{1}{1-s^*}<0.97$, the first such $i$ is at most $\lfloor\log_7\mathrm{N}(z)\rfloor+2$, and the number of digits is that $i$. $\square$

Exhaustive computation over the box $|a|,|b|\le120$ finds the bound attained in every range $7^t\le\mathrm{N}<7^{t+1}$, $t\le4$.

**Lemma 4 (Lifting $\mathbb{F}_r$ to $\mathbb{Z}[\omega]$).** Fix $\pi$ with $\mathrm{N}(\pi)=r$. For $k\in\mathbb{Z}$ let $q=(q_a,q_b)$ with $q_a=\lfloor(2k\bar\pi_a+r)/2r\rfloor$ and $q_b=\lfloor(2k\bar\pi_b+r)/2r\rfloor$ (coordinatewise nearest integer to $k\bar\pi/r$), and $z=k-q\pi$. Then $z\equiv k\pmod{\pi}$ and $4\,\mathrm{N}(z)\le3r$.

*Proof.* $z\bar\pi=k\bar\pi-q\,\pi\bar\pi=k\bar\pi-qr$, whose coordinates $X=k\bar\pi_a-q_ar$, $Y=k\bar\pi_b-q_br$ satisfy $-r<2X\le r$ and $-r<2Y\le r$ by the choice of $q$. Multiplicativity gives $\mathrm{N}(z)\,r=\mathrm{N}(z\bar\pi)=X^2-XY+Y^2$, and $4(X^2-XY+Y^2)\le3r^2$ follows from $4X^2\le r^2$, $4Y^2\le r^2$ and $-4XY\le r^2$ (sum of $(r+2X)(r+2Y)\ge0$ and $(r-2X)(r-2Y)\ge0$). $\square$

**Theorem 5 (BN254).** Let $r$ be the BN254 scalar field order and

$$
\begin{aligned}
\pi={}&147946756881789319000765030803803410728\\
&+147946756881789319010696353538189108491\,\omega,
\end{aligned}
$$

so that $\mathrm{N}(\pi)=r$. For every $k\in\mathbb{F}_r$ there is $z\equiv k\pmod{\pi}$ with $4\,\mathrm{N}(z)\le3r$ whose greedy base-$\beta$ expansion has digits in $\Sigma_{\mathrm{CM}}$, evaluates to $z$, and has length at most $92$.

*Proof.* Lemma 4 and Theorem 3: $\log_7(3r/4)<90.3$, so at most $\lfloor90.3\rfloor+2=92$ digits. The machine-checked proof (Section 7) uses the integer form of Lemma 2 instead of the real recurrence and reaches the same $92$. $\square$

**Remark (Ninety-one).** The coordinatewise rounding of Lemma 4 is not the nearest lattice point. The hexagonal lattice $\pi\mathbb{Z}[\omega]$ has covering radius $\sqrt{r/3}$, so a true nearest-point lift gives $3\,\mathrm{N}(z)\le r$, and $\log_7(r/3)<89.9$ yields $91$. Sampling $2000$ random scalars, the greedy expansion of the rounded lift never exceeded $91$ digits, so $92$ is likely loose by exactly one. We did not formalise the nearest-point lift.

**Remark (Digit sets are bounded by the endomorphism ring).** The only cheap coefficients on a $j=0$ curve are the units of $\mathbb{Z}[\omega]$: any other Eisenstein integer, e.g. $1-\omega$ of norm $3$, costs a point addition and raises the degree of the encoding polynomials. So $\Sigma_{\mathrm{CM}}$, with $\log_2 7\approx2.81$ bits per encoding, is the natural ceiling for $\mathbb{G}_1$. On $\mathbb{G}_2$ the untwisted Frobenius gives a cheap action of $\mu_{12}$, but KFLT's scheme needs the same coefficient vector on $B$ and $C$, and $C\in\mathbb{G}_1$, so this cannot be used without restructuring the disclosure; we leave it open.

## The rekeying gadget with Eisenstein digits

**Construction 6.** $\Pi_G$ is modified as follows; everything not mentioned is unchanged.

- **Garb.** Sample $k\leftarrow\mathbb{F}_r$ as before. Lift $-k$ to $z\in\mathbb{Z}[\omega]$ by Lemma 4 and compute $(d_0,\dots,d_{L-1})=\mathrm{expand}(z)$, $L\le92$, padding with zero digits to a fixed length. Sample $M_i\leftarrow\mathbb{G}_1$ for $i<L$ and set $R=\sum_i\beta^iM_i$, where $\beta^i$ acts on $\mathbb{G}_1$ through $\omega\mapsto\psi_1$.
- **Enc.** $\llbracket A\rrbracket_i=\phi_{d_i}(A)+M_i$ for $i<L$.
- **Eval.** $Q=\sum_i\beta^i\llbracket A\rrbracket_i$, computed by Horner's rule with $\beta\cdot X=2X-\psi_1(X)$, one doubling and one free endomorphism per digit.

**Proposition 7.** Construction 6 is correct: $Q=-kA+R$. Its privacy is exactly that of KFLT Theorem 8, under DDH in $\mathbb{G}_2$ in the random-oracle model. The affine dimension of the $A$-encoding is $S_A=12L+5\le1109$ with the incomplete formulas of KFLT Theorem 3, or $18L+5\le1661$ with the complete formulas of KFLT Appendix A.2.

*Proof.* Correctness is (1): $\sum_i\beta^i(\phi_{d_i}(A)+M_i)=z\cdot A+R=(-k)A+R$ because $z\equiv-k\pmod{\pi}$. For privacy, the only property of the $A$-encodings used in the proof of KFLT Theorem 8 is that the $\llbracket A\rrbracket_i$ are independent uniform points (so they can be sampled first and $R$ defined as $Q+kA$); this holds for any coefficients since the $M_i$ are uniform, and the public combination $\sum_i\beta^i$ is as good as $\sum_i2^i$ there. The DDH hybrid and the relabelling of $\vec c$ do not involve the $A$-encodings. For the dimension, $\phi_d(V)$ is a coordinatewise scaling of $(u,v)$, so the polynomials of KFLT eq. (1) evaluated at $\phi_d(V)$ have the same monomials $u^2,u,v$; $u^2,uv,v^2,v$; $u$, with the garbler's private constants absorbed into the coefficients, and the Ishai–Wee dimension count is unchanged. $\square$

**Remark (Digit privacy).** The digits $d_i$ are part of the private encoding key, exactly as the bits $b_i$ were; the evaluator sees only $\phi_{d_i}(A)+M_i$, which is uniform. The expansion is computed once by the garbler, and $\mathrm{expand}$ runs in $O(L)$ integer operations.

## Adaptive correctness

### The gap

KFLT Definition 1 asks that for every fixed $(x,y)$, evaluation returns $f(x,y)$ except with probability $\delta$ over the randomness of $\mathrm{Garb}$. This is the standard, non-adaptive notion. In the bridge application described in KFLT Section 1, the operator prepares the garbled verifier, holds $\mathrm{ek}$, and later publishes the proof; that is, the party who chooses $x=(A,B,C)$ knows every mask in $\mathrm{ek}$ before choosing.

KFLT realise the group encoding $cV+K$ from the coordinates of $V$ with the incomplete Jacobian formulas (their eq. (1)),

$$
X=au^2+a^2u-2bv+2\beta_E,\qquad
Y=3abu^2-3a^2uv+bv^2-(a^3+4\beta_E)v+3b\beta_E,\qquad
Z=u-a, \tag{3}
$$

for $V=(u,v)$, $K=(a,b)$, curve $v^2=u^3+\beta_E$, and note that they are incomplete when $K=V$, returning $(0,0,0)$, "which occurs with probability $1/r$ for a uniformly sampled mask". That is true for an input fixed in advance. An operator who has drawn $M_i$ and $b_i=1$ can choose $A:=M_i$.

**Proposition 8 (Steering).** In KFLT's $\Pi_{\mathrm{bin}}$ as written, a garbler who chooses the evaluator's input after garbling can produce an invalid proof on which honest evaluation returns $\bot$. The same holds for the entries of $B$ and $C$: with $c_t\neq0$, the input $B:=\phi_{c_t}^{-1}(K^B_t)$ or $C:=\phi_{c_t}^{-1}(K^C_t)$ makes the $t$-th encoding evaluate to $(0,0,0)$, and $\mathrm{Eval}_G$ returns $\bot$ whenever any single index has no unique candidate.

*Proof.* Take $A=M_i$ for some $i$ with $b_i=1$ and any $B,C$ making the proof invalid. The inner evaluation of $\llbracket A\rrbracket_i$ returns $(0,0,0)$ by (3), which is not a Jacobian representative of any point, and $\mathrm{Eval}_F$ returns $\bot$ at its step 2. (Were the evaluator to substitute an arbitrary point instead, $Q$ would be off by some $\Delta\neq0$, every $Y_t$ by $e(\Delta,U_t)\neq0$, and no candidate $Y_t-dP$ would hash to $h_t$ except with probability $\kappa 2^{-\tau}$.) The proof itself is a legitimate triple of group elements, so the Lamport signatures on its bits are valid, and the garbling is honest, so cut-and-choose does not reject it. $\square$

Whether the surrounding bridge protocol has an independent defence, such as a challenge path that forces the operator to open masks, is outside KFLT and outside this note; at the level of the garbling scheme and the definition it is proved against, the gap is real. KFLT's Appendix A moves to complete formulas "to account for all input cases comprehensively"; we read this as the same concern, and note that if complete formulas are required then they are required in the main construction too, at $18$ rather than $12$ dimensions per encoding, i.e. $N_{\mathrm{base}}=16{,}122$ and roughly $3.2$ MiB rather than $2.4$. The repair below avoids that.

### Characterising the exceptional outputs

**Lemma 9 (Exceptional outputs of (3)).** Let $V=(u,v)$ and $K=(a,b)$ both satisfy $v^2=u^3+\beta_E$, and let $v\neq0$. Then (3) returns $(0,0,0)$ if and only if $K=V$; and it returns $Z=0$ with $X\neq0$ if and only if $K=-V$, in which case $(X\!:\!Y\!:\!0)=(4v^2\!:\!-8v^3\!:\!0)$ is a valid Jacobian representative of the identity.

*Proof.* $Z=0$ iff $a=u$, and then $b=\pm v$ from the curve equations. With $a=u$, $X=2u^3+2\beta_E-2bv=2v^2-2bv=2v(v-b)$, which is $0$ iff $b=v$; if $b=v$ a direct substitution using $v^2=u^3+\beta_E$ gives $Y=v(v^2-u^3-\beta_E)=0$. If $b=-v$ then $X=4v^2\neq0$ and $Y=-v(7u^3+7\beta_E+v^2)=-8v^3$, and $Y^2=X^3$ places $(X\!:\!Y\!:\!0)$ on the projective closure, where $Z=0$ is the identity. $\square$

In $\mathbb{G}_1$ and $E'(\mathbb{F}_{p^2})$ every point has $v\neq0$, since the group orders $r$ and $r(2p-r)$ are odd and $v=0$ would give $2$-torsion. The randomised representative $(\mu^2X,\mu^3Y,\mu Z)$ has the same zero pattern, and the constant representatives used for $c=0$ and for $K=\mathcal{O}$ have $Z\neq0$. Hence, applied to $\phi_c(V)$, the lemma says: *the evaluator sees $(0,0,0)$ at an encoding exactly when $c\neq0$ and $K=\phi_c(V)$, and then the encoded point is $2\phi_c(V)$.*

### Repair

**Construction 10 (Repaired evaluation).** Let the inner evaluator, on obtaining $(0,0,0)$ for an encoding of $V$, return the candidate set $\{2\phi_c(V)\colon c\in\Sigma_{\mathrm{CM}}\setminus\{0\}\}$ instead of failing; for binary coefficients this is the single point $2V$.

- *Entries of $B$ and $C$.* Index $t$ enters $\mathrm{Eval}_G$ only through $Y_t$ and the subgroup test. Extend the candidate test at $t$ to range over the candidate set(s) for $\llbracket B\rrbracket_t$, $\llbracket C\rrbracket_t$ and $d_t$: at most $6\cdot6\cdot7$ hash evaluations at that index. A wrong candidate passes only by a hash collision, so the correctness error grows by at most $252\kappa\,2^{-\tau}$.
- *Entries of $A$.* If $m$ indices return $(0,0,0)$ the evaluator has $6^m$ candidates for $Q$ (one, if $A$ uses binary digits), each testable against all $h_t$ at once. Since the $M_i$ are the garbler's own choice, $m$ is not bounded by chance. Derive them instead as $M_i=\mathsf{H}_{\mathbb{G}_1}(\mathrm{seed},i)$ from a seed that is opened in the cut-and-choose check of the malicious-security compiler. Then a second collision $M_j\in\{\phi_c(A)\}$ for the same $A$ requires two of $L$ pseudorandom points in one orbit of size $6$, probability about $6\binom{L}{2}/r<2^{-235}$ per seed, negligible even against a grinding operator, so $m\le1$ and the enumeration has at most $6$ elements.

**Proposition 11.** With Construction 10, KFLT's scheme, with binary or Eisenstein digits on $A$ and binary or $\Sigma_{\mathrm{CM}}$ coefficients on $B,C$, is correct against an adversary that chooses the evaluator's input after seeing $(\tilde f,\mathrm{ek})$, except with probability $O(\kappa 2^{-\tau})+O(L^2/r)$, at no increase in garbled program size.

*Proof.* By Lemma 9 every output of the inner evaluation is either a correct representative or $(0,0,0)$, and in the latter case the true encoded point is in the candidate set. The outer candidate test is complete because the correct candidate always passes, and sound up to hash collisions; the $A$-side enumeration is bounded as computed. No garbled material changes; only evaluator work, by a constant factor. $\square$

**Remark (Privacy is unaffected).** In the exceptional case the evaluator learns that the coefficient at that index is nonzero (and, for $A$, which digit). This is reachable only by the garbler's own steering, and the privacy game has an honest garbler, so the simulator of KFLT Theorem 8 is unchanged. In the bridge, an operator who steers a *valid* proof into the exceptional case leaks bits of its own secret; it has no incentive to.

**Remark (Alternatives).** Complete formulas on $A$ only cost $6L\le552$ dimensions; binary digits on $A$ with the deterministic repair cost nothing beyond KFLT's $S_A=3053$. The seed-derived masks are the cheapest option and need only that the malicious-security compiler already opens garbling randomness, which cut-and-choose does.

## Cost accounting

The table stacks the changes. Variable cost is scaled linearly in $N_{\mathrm{base}}$ from KFLT's measured $1604$ KiB at $10{,}758$; the fixed $885$ KiB is untouched throughout. All rows assume $12$ dimensions per encoding with the repair of Section 5; with complete formulas the variable cost of every row, including KFLT's, is $1.5\times$ larger and the ratios are essentially unchanged.

| Step | Status | $N_{\mathrm{base}}$ | Total | vs. KFLT |
|---|---|---:|---:|---:|
| KFLT, binary digits | measured[^kflt26] | 10,758 | 2.44 MiB | — |
| Eisenstein digits on $A$ (Section 4) | proven, Section 7 | 8,814 | 2.16 MiB | −12% |
| + $\Sigma_{\mathrm{CM}}$ on $B,C$, $\kappa=46$ | KFLT App. A | 3,894 | 1.44 MiB | −41% |
| + two-input $\mathbb{F}_p$ gadget (Conjecture 12) | conjectured | 2,780 | 1.27 MiB | −48% |
| + output-mask elimination | suggested in Duty-Free Bits[^dfb] | 2,780 | 1.07 MiB | −56% |

$N_{\mathrm{base}}=S_A+4S_B+S_C$ (or $S_A+2S_B+S_C$ under Conjecture 12); $S_A=12\cdot92+5$, $S_B=S_C=12\cdot46+5$ from the second row on.

**Conjecture 12 (Two-input affine maps in Duty-Free Bits).** KFLT Lemma 12 projectivizes an $S$-dimensional $\mathbb{F}_{p^2}$-affine encoding as two $\mathbb{F}_p$ instances of dimension $2S$, an additive sharing that costs $4S$ base-field output dimensions. In Duty-Free Bits (Section 4.3 of that paper[^dfb]), stage 1 converts each input to CRT residues at a cost independent of $S$, while stage 2 pays one terminal output label per (CRT prime, output dimension), with multiplication by the garbler's private coefficient being linear. If that reading is right, a native gadget for $\vec a\,x_0+\vec a'\,x_1+\vec b$ over $\mathbb{F}_p$ with two encoded inputs needs $2S$ output wires, not $4S$, and the factor on $S_B$ drops from $4$ to $2$. We have not verified this against the switch-system formalism of Duty-Free Bits Section 6.

**Remark (What does not work: $x$-only encodings).** The fixed cost is eight bit-to-CRT conversions, one per coordinate block. Sending only $u$ and recovering $v$ up to sign would remove three blocks, and the symmetric functions of $x(\phi_cV+K)$ and $x(\phi_cV-K)$ are polynomial in $u$ with private coefficients, of Ishai–Wee dimension $9$. But the evaluator then learns the unordered pair $\{x(\phi_cV+K),x(\phi_cV-K)\}$, and with $V$ public the second root identifies $c$: for $c\in\{0,1\}$ the two roots coincide iff $c=0$. So $x$-only encodings leak the coefficient and cannot be used.

After the table the fixed cost is $80\%$ of the program. Its floor is $O(n\lambda)$ bits per block, about $4$ KiB, against the $110$ KiB per block measured; closing that is engineering inside Duty-Free Bits rather than protocol design.

## Formalisation

The BN254 statement (Theorem 5) is proved in Lean 4[^lean4], version 4.34.1, in about $400$ lines with no dependency on Mathlib or any other library. The development defines $\mathbb{Z}[\omega]$ as pairs of integers with the multiplication $(a+b\omega)(c+d\omega)=(ac-bd)+(ad+bc-bd)\omega$, the norm, conjugate, base $\beta$, the digit and quotient maps of Section 3, the greedy expansion by well-founded recursion on the norm, and the Horner evaluation. The main theorem is stated as

```lean
theorem bn254 (k : Int) :
    ∃ z : Eis, (∃ q : Eis, z = ofInt k - q * π) ∧
      (∀ d ∈ expand z, d ∈ digitSet) ∧ eval (expand z) = z ∧ (expand z).length ≤ 92
```

and `#print axioms Eis.bn254` reports `propext`, `Classical.choice`, `Quot.sound`; there is no `sorry` and no `native_decide`.

**Avoiding square roots in the kernel.** Lemma 2 is formalised in the form $7\,\mathrm{N}(\mathrm{quot}\,z)\le\mathrm{N}(z)+2u+2$ for any $u\ge0$ with $\mathrm{N}(z)<(u+1)^2$, which needs no square-root function at all. The length argument is a general lemma: a list $[(T_0,u_0),\dots,(T_L,u_L)]$ is a valid *threshold chain* if $T_L=0$ and for each $i<L$, $T_i<(u_i+1)^2$ and $\lfloor(T_i+2u_i+2)/7\rfloor\le T_{i+1}$; then every $z$ with $\mathrm{N}(z)\le T_0$ has an expansion of length at most $L$. Validity of a concrete chain involves only natural-number multiplication, division and comparison, which the kernel evaluates directly, so the $93$-entry chain for BN254, with $T_0=\lfloor3r/4\rfloor$ and $u_i=\lfloor\sqrt{T_i}\rfloor$ found offline, is checked by `decide` and depends on no axioms. Lean's `Nat.sqrt` is defined by well-founded recursion and does not reduce under `decide`; the certificate sidesteps it.

**Arithmetic.** Cauchy–Schwarz for the six units, the norm identities and the expansions of products in Lemma 4 are polynomial identities discharged by `grind`; the remaining inequalities are linear in the monomials and discharged by `omega` after supplying square-nonnegativity facts. The rounding bounds in Lemma 4 are linear in $k$ and $q$ once $r$ is unfolded to a literal, and `omega` handles them directly.

**What is not formalised.** The identification $\mathbb{Z}[\omega]/(\pi)\cong\mathbb{F}_r$ and the action (1), which are standard and not specific to this work; the closed form $\lfloor\log_7\mathrm{N}\rfloor+2$ of Theorem 3, which uses real arithmetic; Lemma 9, which needs field arithmetic over $\mathbb{F}_p$ and is the natural next target for a Mathlib development; and the nearest-point lift of the Ninety-one remark.

## Conclusion

The rekeying gadget of KFLT was paying for a binary number system where the curve offers a base-$7$ one. Replacing it is a change of one line in the evaluator and of the garbler's offline arithmetic; the accompanying bound is now a theorem checked by a kernel rather than an estimate, and the same technique of shipping a threshold certificate should transfer to any bound of the form "the norm shrinks by a factor at each step" that one wants to certify without real analysis. The adaptive-correctness gap is, we think, the more important of the two observations, since it separates the scheme's definition from its application; the repair is cheap and we would expect it, or complete formulas, to be adopted before deployment.

Open: the nearest-point lift and the $91$-digit bound; a Mathlib formalisation of Lemma 9 and of adaptive correctness itself; Conjecture 12; using $\mu_{12}$ on $\mathbb{G}_2$; and, dominating everything after these, the fixed cost of bit-to-CRT conversion.

## Provenance

This note was produced by the model named in the submission's provenance record, in an interactive session with a human collaborator who posed the problem, chose the direction at each stage (improving the native-group design, machine-checking the bound, and this write-up), reviewed the results and chose not to be credited. The Lean artifact is the only part of the argument that has been checked by something other than the model; everything else should be read with that in mind.

[^kflt26]: N. Khambhati, A. Feickert, C. Lewe, M. Tiwari. Garbling Groth16 with native group operations. Cryptology ePrint Archive, Paper 2026/2100.
[^argo]: L. Eagen, Y. T. Lai. Argo MAC: Garbling with elliptic curve MACs. Cryptology ePrint Archive, Paper 2026/049.
[^babe]: S. Garg, D. Kolonelos, M. Sergeevitch, S. Sridhar, D. Tse. BABE: Verifying proofs on Bitcoin made 1000x cheaper. Cryptology ePrint Archive, Paper 2026/065.
[^dfb]: N. Khambhati, A. Bhattacharya, D. Heath. Duty-free bits: Projectivizing garbling schemes. Cryptology ePrint Archive, Paper 2026/476.
[^ishaiwee]: Y. Ishai, H. Wee. Partial garbling schemes and their applications. ICALP 2014.
[^rcb]: J. Renes, C. Costello, L. Batina. Complete addition formulas for prime order elliptic curves. EUROCRYPT 2016.
[^lean4]: L. de Moura, S. Ullrich. The Lean 4 theorem prover and programming language. CADE 2021.