愿望单

#wishlist @ 2026-04-01T12:50:05+08:00

学一下 NTT 和 FFT，看看怎么用在 Reed-Solomon decoder 上的。
把 dependent destruction 引入 JMeq 的细节搞明白。
Basic Schnorr signature, EdDSA, 为什么 EdDSA 比 ECC 在常见硬件上更快。有专有指令/加速器的可能吗？
NoC deadlock freedom

初等代数

#alg @ 2026-03-23T03:08:38+08:00

代数课没有好好听，注定度过失败的一生了。

Montgomery 模乘

在真实计算机中，不同带余除法的代价不同：比如除以 power of 2 非常便宜。Naive 的模乘实现需要用模数作为被除数，代价不好控制。Montgomery 模乘可以将计算过程中的除法替换为另一个被除数。

$𝑎, 𝑏 \in ℤ_{𝑞}$ ，需要计算 $𝑎 \cdot 𝑏 \in ℤ_{𝑞}$ ，如果 $ℤ_{𝑞}$ 中的元素都使用最小非负代表元表示，这就是要计算 $(𝑎 \cdot 𝑏) mod 𝑞$ 。假设有另一个常数 $𝑅 \in ℕ$ 满足 $𝑅 > 𝑞$ 而且两者互素。假设除以 $𝑅$ 的代价较小。

称 $𝑥 \in ℤ_{𝑞}$ 的 Montgomery 形式 $\tilde{𝑥} = 𝑥 \cdot 𝑅 \in ℤ_{𝑞}$ 。因为 $𝑅$ 的带余除法代价小，计算 $mod 𝑅$ 的代价很小。需要注意的是 $\cdot$ 和 $mod 𝑞$ 的代价较大。只要能够避免这两个操作，就能得到更快的模乘实现。

$𝑅^{*}$ 是 $𝑅$ 在 $ℤ_{𝑞}$ 里面的逆元， $𝑞^{*}$ 是 $𝑞$ 在 $ℤ_{𝑅}$ 里面的逆元。

\begin{aligned} \tilde{𝑎 \cdot 𝑏} & = \tilde{𝑎} \tilde{𝑏} 𝑅^{*} mod 𝑞 \\ = (\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞) 𝑅^{*} mod 𝑞 \end{aligned}

注意到 $\forall 𝑥 \in ℤ$ ：

(𝑥 - (𝑥 𝑞^{*} mod 𝑅) 𝑞) mod 𝑅 = (𝑥 - (𝑥 𝑞^{*} 𝑞)) mod 𝑅 = 0

所以 $(\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞)$ 一定是 $𝑅$ 的倍数，在 $ℤ$ 中计算 $(-) \cdot 𝑅^{*} mod 𝑞$ 相当于计算 $\frac{-}{𝑅} mod 𝑞$ ：

\begin{aligned} \tilde{𝑎 \cdot 𝑏} & = \tilde{𝑎} \tilde{𝑏} 𝑅^{*} mod 𝑞 \\ = (\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞) 𝑅^{*} mod 𝑞 \\ = \frac{\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞}{𝑅} mod 𝑞 \end{aligned}

最后我们可以通过 Bound $(\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞) / 𝑅$ 来消除最外面的 $mod 𝑞$ ：注意到因为 $𝑅 > 𝑞$ ，这个值一定在 $(- 𝑞, 𝑞)$ 之间。所以我们只需要比较这个值是否是负数，如果是就加上 $𝑞$ 就好了。

实现中的一些细节：

一般来说参数选择是 $𝑅$ 是比 $𝑞$ 大的最小支持高效计算的机器字。比如对于 Dilithium prime $𝑞 = 8380417 < 2^{23}$ ，可以选择 $𝑅 = 2^{32}$ 。
所有除了除以 $𝑅$ 以外的计算都可以在 $ℤ_{𝑅^{2}}$ 内进行。如果 $𝑅 = 2^{32}$ ，只需要有高效的 64 位加、减、乘法。
真实实现中一般不用 $𝑞^{*}$ ，而是用 $- 𝑞$ 在 $ℤ_{𝑅}$ 内的逆元，因为 $ℤ_{2} 𝑅$ 中的加法一般比减法好处理。如果本身就有高效的 $ℤ_{2} 𝑅$ 减法，同时比较正负比比较常数要快，那么应该是用 $𝑞^{*}$ 。

Gemini 给出的伪代码：

#include <stdint.h>

// 4236238847 is -q^(-1) mod 2^32
#define QINV_NEG 4236238847u 
#define Q 8380417u

uint32_t montgomery_mul(uint32_t a_mont, uint32_t b_mont) {
  uint64_t prod = (uint64_t)a_mont * b_mont;
  
  // Calculate the multiple of Q needed to clear the lower 32 bits
  uint32_t t = (uint32_t)prod * QINV_NEG;
  
  // Add the multiple of Q and shift out the lower 32 bits (which are now guaranteed to be 0)
  uint64_t u = prod + (uint64_t)t * Q;
  uint32_t res = u >> 32;
  
  if (res >= Q) {
      res -= Q;
  }
  
  return res;
}

逻辑

#logic @ 2026-03-13T08:52:18+08:00

模型大小

一阶逻辑有 Lowenheim-Skolem. 事实上 LS 跟完备性非常相关。Notably，以下两种逻辑因为能够控制模型大小，所以丧失了完备性：

SOL 可以描述模型大小，原因是相比于一阶的理论，二阶理论的二阶量词 Quantify over 的是真的模型里的东西，而不只是 definable 的东西。经典例子： ${𝐏𝐀}^{𝟐}$ 没有非标模型，因为任何 ${𝐏𝐀}^{𝟐}$ 模型都有 $ℕ$ 前段，而 $ℕ$ 这个前段套进二阶归纳里面直接得到所有元素都在 $ℕ$ 里。
${Ind}^{2} ≔ \forall 𝑃 ((𝑃 (0) \land (\forall 𝑛, 𝑃 (𝑛) \to 𝑃 (𝑆 (𝑛)))) \to \forall 𝑛 𝑃 (𝑛))$
这直接导致了二阶逻辑甚至没有一个 sound and complete deduction system。True arithmetic $𝑇 (ℕ)$ 不 RE. 如果 ${𝐏𝐀}^{𝟐}$ 有完备的 deduction system，可以枚举 proof，那么就可以 SOL 里面在 ${𝐏𝐀}^{𝟐}$ 里面的 valid sentences。FOL sentences 是 SOL sentences 的一个 decidable fragment (纯语法性质)，所以这样 $𝑇 (ℕ)$ 也 RE 了。
$𝑇 (ℕ)$ 不 RE 的原因：考虑把 $𝑇 (ℕ)$ 作为公理集的理论。这个理论是一个完备的一阶理论 (syntactical completeness)，而且 consistent （它有个模型），根据 Godel’s incompleteness theorem，他肯定不能 effectively axiomatizable，因此 $𝑇 (ℕ)$ 不 RE。
事实上 ${𝐏𝐀}^{𝟐}$ 可以说明 SOL 不 compact. 符号集加一个常元 $𝑐$ ，考虑
$Γ = {𝐏𝐀}^{𝟐} \cup {𝑐 \neq 𝑆^{𝑛} (0) | 𝑛 \in ℕ}$
如果只考虑 FOL 的有限模型 (finite model theory)， valid FOL sentences is not RE. 与之对比，在任意模型内，根据 Completeness theorem, 枚举 proof 就可以枚举 valid sentences 了。See: Trakhtenbrot’s theorem.
因此，在 FOL 的这种解读下，FOL 也不存在 sound and complete deduction system。

通讯

#communication @ 2026-03-08T16:29:47+08:00

Rectangle property

在 MPC 设定下，如果暂时不考虑 Active malicious adversary 的话，节点的私有状态 $(𝑥_{𝑖}, 𝑟_{𝑖})$ i.e. 输入和随机性可以确定性决定 Transcript $𝑇$ 。将这一映射称为 $Π$ .

$Π^{- 1}$ 具有 “Rectangle property”， $\forall 𝑇 \in 𝒯︀, Π^{- 1} (𝑇)$ 是一个 Rectangle：

Π^{- 1} (𝑇) = \prod_{𝑖 = 1}^{𝑛} 𝜋_{𝑖} (Π^{- 1} (𝑇))

可以理解成，如果有任意两个所有 Party 的私有状态集合 $𝑆_{1}, 𝑆_{2}$ 满足 $Π (𝑆_{1}) = Π (𝑆_{2}) = 𝑇$ ，那么可以把 $𝑆_{1}$ 和 $𝑆_{2}$ 任意组合（每个 Party 任意在两者中选一个），那么最终 Transcript 依旧是 $𝑇$ 。

证明把 T 当成一个消息列，归纳。

这有两个很直接的后果：

如果至少有 3 个 Party，那么不存在在纯广播信道上的 $𝑡 \geq 1$ 的计算元素和的协议。原因是如果存在，假设 Party 1 semi-honest，Fix $(𝑥_{1}, 𝑟_{1})$ ，注意到只要 $\sum_{{𝑖 \geq 2}} 𝑥_{𝑖}$ 不变，那么 Party 1 的 View 也不变。这是纯广播，因此 Transcript 不变。只要有限域大小大于 2, 总能选出来两个不同的元素 $𝑒_{0}, 𝑒_{1}$ ，假设他们是 Party 2 和 Party 3 的输入，那么交换他们，Party 1 View 不变，所以把 Party 3 的输入从 $𝑒_{1}$ 改成 $𝑒_{0}$ ，Party 1 View 依旧不变，但是结果变了，矛盾。
不存在 2-Party 计算 AND 的协议。如果存在， $𝑥_{1} = 0, 𝑥_{2} = 1$ 和 $𝑥_{1} = 1, 𝑥_{2} = 0$ 都会输出 $0$ , 所以 Adversary View 相同，只有两个 Party 所以 View 包含整个 Transcript，整个 Transcript 也就相同。所以 $𝑥_{1} = 𝑥_{2} = 1$ 也应该产生一样的 Transcript，但是这会产生不同的输出，矛盾。

相关历史综述见 Gemini DeepResearch。AI 幻觉有风险，4.6 Opus 就给我幻觉了几个 Ref。不过 DeepResearch 至少给链接了。

Reed-Solomon 纠错

Reed-Solomon 如果有 $2 𝑡$ 冗余可以纠 $𝑡$ 个错 (Also, Shamir Secret Sharing).

考虑有限域 $GF (𝑞)$ 上的 Reed-Solomon 码，共 $𝑛 - 2 𝑡$ 个数据， $2 𝑡$ 个冗余，总共采样点 $𝑛$ 个。现在要找出来其中最多 $𝑡$ 个错的点。如果我们忽略多项式的其他结构，认为这些采样点是任选的，下面陈述的方法是找到这些错误点的标准方法 Berlekamp-Welch algorithm。

Berlekamp-Welch

假设 Underlying polynomial 是 $𝐹 (𝑥)$ ，Claim 存在一个多项式 $𝐸 (𝑥)$ ，满足 $𝑥_{𝑖} incorrect \Leftrightarrow 𝐹 (𝑥_{𝑖}) \neq 𝑦_{𝑖} \Rightarrow 𝐸 (𝑥_{𝑖}) = 0$ 。如果 $𝑥_{𝑖}$ 不是错误的点，对 $𝐸 (𝑥_{𝑖})$ 没有要求。因为最多 $𝑡$ 个错误，所以我们可以要求 $deg 𝐸 (𝑥) = 𝑡$ ，并且最高次项系数为 $1$ ， $𝐸 (𝑥)$ 剩下 $𝑡$ 个系数未知。

$𝐸 (𝑥_{𝑖}) 𝐹 (𝑥_{𝑖}) = 𝐸 (𝑥_{𝑖}) 𝑦_{𝑖}$ 对所有采样点成立。这给我们提供了 $𝑛$ 个方程， $deg 𝐹 (𝑥) = 𝑛 - 2 𝑡 - 1$ ，令 $𝑄 (𝑥) = 𝐸 (𝑥) 𝐹 (𝑥)$ ， $deg 𝑄 (𝑥) = 𝑛 - 𝑡 - 1$ ，线性系统 $𝑄 (𝑥_{𝑖}) - 𝐸 (𝑥_{𝑖}) 𝑦_{𝑖}$ 一共 $𝑛$ 个方程， $𝑛$ 个未知数，可以解出 $𝑄 (𝑥)$ 和 $𝐸 (𝑥)$ ，之后 $𝐹 (𝑥) = \frac{𝑄 (𝑥)}{𝐸 (𝑥)}$ 或者 Chien search. 复杂度 $𝒪︀ (𝑛^{3})$

Alternatively, 这是一个 Rational polynomial interpolation 问题， $\frac{𝑄 (𝑥_{𝑖})}{𝐸 (𝑥_{𝑖})}$ 经过 $𝑛$ 个点。wo/ FFT 复杂度 $𝒪︀ (𝑛^{2})$ , w/ FFT 复杂度 $𝒪︀ (𝑛 {log}^{2} 𝑛)$ 。（但我都不会）

Generator view vs. evaluation view

有两种 (somewhat equivalent) 看待 Reed-Solomon code 的方式。

SSS 里常见的构造对应 RS code 的 Evaluation view，这也是 Reed & Solomon’s original view: 数据在 pre-defined points of evaluation. RS code 目前实现中常见的方法是 Generator view (BCH view): 数据在 polynomial coefficients 上。两者之间的转换就是一次 NTT.

令 $𝑚$ 为消息长度， $2 𝑡$ 为冗余， $𝑛 = 𝑚 + 2 𝑡$ 为 Codeword 长度。

对于 Generator view 的 RS code，预先选定的是一个 Generator polynomial $𝐺 (𝑥)$ ， $deg 𝐺 (𝑥) = 2 𝑡$ 。Underlying field $𝔽$ 满足 $| 𝔽 | = 𝑛 + 1$ ，要求 $𝐺 (𝑥) ∣ 𝑥^{𝑛} - 1$ 。

Generator polynomial 的常见构造方式是选定一个 $𝔽$ 的 primitive element $𝛼$ 和任意 $𝑟 \in ℕ$ , $𝐺 (𝑥) = \prod_{𝑖 = 1}^{2 𝑡} (𝑥 - 𝛼^{𝑖 + 𝑟})$ 。

对于 $𝑚$ 个消息 $𝑟_{0}, \dots, 𝑟_{𝑚 - 1}$ ，Message polynomial 是 $𝑀 (𝑥) = \sum_{𝑖 = 0}^{𝑚 - 1} 𝑟_{𝑖} 𝑥^{𝑖}$ 。有两种编码方式得到 Codeword $𝐶 (𝑥)$ ：

简单编码直接让 $𝐶 (𝑥) = 𝐺 (𝑥) \cdot 𝑀 (𝑥)$ 。解码的时候需要做一次多项式除法
Systematic encoding 令 $𝐶^{'} (𝑥) = 𝑀 (𝑥) \cdot 𝑥^{2} 𝑡$ ，然后 $𝐶 (𝑥) = 𝐶^{'} (𝑥) - (𝐶^{'} (𝑥) mod 𝐺 (𝑥))$ 。Systematic encoding 的好处是前 $𝑚$ 个符号就是消息，解码的时候非常简单

Sidenote: 因为消息总能做 Padding，尤其是 Systematic encoding 里面消息 Padding 直接对应 Codeword padding，所以都可以不传这部分 Codeword。因此 $𝑛 = | 𝔽 | - 1$ 的限制事实上限制的是最大 Block length。Evaluation view 也有类似的限制，这个限制来自于 Evaluation point 的个数。但是因为可以选任意 $𝔽$ 元素当作 evaluation point，所以限制比 Generator view 要大 1. (Related: Extended RS & Doubly-extended RS，但是我没看懂这些)

Generator view decoding

在 Generator view 构造中，Berlekamp-Welch 无法直接使用。Berlekamp-Massey 是一个求最小 LFSR 的算法，在 RS code 中可以用于在 generator view 的构造中替代 Berlekamp-Welch 做错误定位。

注意到，两种 encoding 如果理解成 $𝑀 (𝑥) \mapsto 𝐶 (𝑥)$ 在 ${𝔽 [𝑥]}_{\leq 𝑚 + 2 𝑡 - 1}$ 多项式空间里的函数，都是可逆线性的。因为 $𝑀 (𝑥)$ 是一个 degree-m 子空间，因此所有无错误 Codeword 也是一个 degree-m 子空间。错误校验是判定一个多项式是否在这个空间内。

在这个多项式空间上取以下内积结构：系数乘积的和 (i.e. 选取 ${𝑥^{𝑖}}$ 做基映射到 $𝔽^{𝑛}$ )。 $𝐶 (𝑥)$ 。Codeword 空间的正交补空间 degree 是 $𝑚 + 2 𝑡 - 𝑚 = 2 𝑡$ ，因此可以通过 $2 𝑡$ 个多项式来 span 这个正交补空间。

定义 Parity-check polynomial $𝐻 (𝑥) = \frac{𝑥^{𝑛} - 1}{𝐺 (𝑥)}$ 。 $deg 𝐻 (𝑥) = 𝑛 - 2 𝑡 = 𝑚$ ，令 $𝐻^{*} (𝑥) = 𝑥^{deg 𝐻 (𝑥)} 𝐻 (𝑥^{- 1})$ 是 $𝐻 (𝑥)$ 的 Reciprocal polynomial。 ${𝐻^{*} (𝑥) \cdot 𝑥^{0}, 𝐻^{*} (𝑥) \cdot 𝑥, \dots, 𝐻^{*} (𝑥) \cdot 𝑥^{2 𝑡 - 1}}$ 是正交补空间的一组基。

他们是正交补空间的基的简短证明：这组基显然线性无关。同样， ${𝐺 (𝑥) \cdot 𝑥^{0}, 𝐺 (𝑥) \cdot 𝑥, \dots, 𝐺 (𝑥) \cdot 𝑥^{𝑚 - 1}}$ 是 Codeword 空间的一组基。为了证明他们是正交补，只需要证明两组基中任选向量内积为 0 即可。
注意到， $⟨ 𝐺 (𝑥) \cdot 𝑥^{𝑖}, 𝐻^{*} (𝑥) \cdot 𝑥^{𝑗} ⟩$ 正是表达式 $𝐺 (𝑥) \cdot 𝐻 (𝑥) mod (𝑥^{𝑛} - 1)$ 的 $deg 𝐻 (𝑥) + 𝑗 - 𝑖$ 次项系数。而 $𝐺 (𝑥) \cdot 𝐻 (𝑥) = 𝑥^{𝑛} - 1$

对于使用 Powers of primitive root 构造的 $𝐺 (𝑥)$ ，有更简单的办法给一组基。注意到任何 $𝐺 (𝑥)$ 的根 $𝛼^{𝑖}$ 都是 $𝐶 (𝑥)$ 的根，所以令 $𝐻_{𝑖} (𝑥) = \sum_{𝑗 = 0}^{2 𝑡} 𝑎^{𝑖 𝑗} 𝑥^{𝑗}$ ，那么 $⟨ 𝐻_{𝑖} (𝑥), 𝐶 (𝑥) ⟩ = 𝐶 (𝛼^{𝑖}) = 0$ ，因此 ${𝐻_{𝑖} (𝑥)}_{{𝑖 = 𝑟 + 1 \dots 𝑟 + 2 𝑡}}$ 是一组正交补空间的基。

上述构造出的正交补空间的基不一定正交，但是我们还是可以把 $𝐶 (𝑥)$ 投影上去，如果正确的编码是 $𝐶_{0} (𝑥)$ ，投影得到的结果是 $𝐸 (𝑥) = 𝐶 (𝑥) - 𝐶_{0} (𝑥)$ 也就是错误项在选定基下的坐标。这一坐标通常被称为 Syndrome ${𝑆_{𝑖}}_{𝑖 = 1 \dots 2 𝑡}$ 。

在使用 Power of primitive root 构造的 $𝐺 (𝑥)$ 的情况下，投影直接就是求值，因此不用存储 $𝐻$ 矩阵。

对于一般的 Parity-check matrix 构造，使用 Syndrome 进行错误定位可以利用 Meggitt Decoder: 一个查找表，加上 RS code 在 generator view construction 下是一个 Cyclic code 的特性检查。

Berlekamp-Massey

如果我们使用 Powers of primitive root 构造 $𝐺 (𝑥)$ 和 parity-check matrix $𝐻$ (as a Vandermond matrix of $𝛼, 𝛼^{2} \dots 𝛼^{2 𝑡}$ )，有更高效的做法。

假设 $𝐸 (𝑥)$ 里面实际有 $𝜈 \leq 𝑡$ 个错误 ${𝑒_{𝑗}}_{𝑗 = 1 \dots 𝜈}$ ，位置分别在 $𝑖_{1}, \dots, 𝑖_{𝜈}$ 次项，也就是：

𝐸 (𝑥) = \sum_{𝑗 = 1}^{𝜈} 𝑒_{𝑖_{𝑗}} 𝑥^{𝑖_{𝑗}}

因此 $𝑆_{𝑖} = 𝐸 (𝛼^{𝑖})$ 。现在的目标是找到 ${𝑖_{𝑗}}_{𝑗 = 1 \dots 𝜈}$ 。定义 Error locator polynomial:

Λ (𝑥) = \prod_{𝑗 = 1}^{𝜈} (1 - 𝑥 𝛼^{𝑖_{𝑗}})

$Λ (𝑥)$ 的根为 ${𝛼^{- 𝑖_{𝑗}}}_{{𝑗 = 1 \dots 𝜈}}$ 。假设 $Λ (𝑥)$ 展开为 $1 + Λ_{1} 𝑥 + Λ_{2} 𝑥^{2} + \dots + Λ_{𝜈} 𝑥^{𝜈}$ ，可以证明对于任意给定的正整数 $𝑗 \leq 2 𝑡 - 𝜈$ (见 Wikipedia)：

𝑆_{𝑗 + 𝜈} + Λ_{1} 𝑆_{𝑗 + 𝜈 - 1} + Λ_{2} 𝑆_{𝑗 + 𝜈 - 2} + \dots + Λ_{𝜈} 𝑆_{𝑗} = 0

注意到这等价于一个需要找到一个最短的 $𝜈$ -stage LFSR 生成 $𝑆_{1}, 𝑆_{2}, \dots, 𝑆_{2 𝑡}$ 。注意：对于一个 Recurrent sequence，如果我们知道他的 Generating LFSR has degree $\leq 𝑡$ ，那么可以通过前 $2 𝑡$ 项确定 Generating LFSR。但是反过来不成立： 存在 $2 𝑡$ 个元素序列无法被一个 degree $\leq 𝑡$ 的 LFSR 生成。

BM 算法的直觉是一个一个试，看看目前猜的 LFSR 有没有出错。保存一个上一次出错的时候的 LFSR，以及当时出的错 $𝑏$ ，如果这次出错 $𝑑$ ，那么把上次的 LFSR $\times \frac{𝑑}{𝑏}$ 减掉就可以用来修这次的错。Pseudocode in Rust format:

// Input: S: Vec<Field> of length 2t
let mut lambda = poly!(1); // C in most texts about BM
let mut last_lambda = poly!(1); // B in most texts about BM
let mut last_update = -1;
let mut last_dis_inv = 1;

for k in 0..2t {
  // Loop invariant:
  // last_lambda when evaluates by S[..last_update
  // will generate discrepancy last_dis_inv^(-1)
  let discrepancy = S.rev().skip(2 * t - k - 1) // Start from S[k]
    .zip(lambda.coeffs()) // Coeffs from lowest degree to highest
    .map(|(s, l)| s * l)  // Field multiplication
    .sum();               // Field addition
  if discrepancy == 0 { continue; }
  let tmp = lambda.clone();
  let update = (discrepancy * last_dis_inv)
    * last_lambda * poly!(x^(k - last_update));
  // Because of the invariant, the update polynomial
  // will evaluates to exactly discrepancy at S[..k]
  lambda -= update;

  if lambda.degree() > tmp.degree() {
    // Degree updated
    last_lambda = tmp;
    last_update = k;
    last_dis_inv = 1 / discrepancy;
  }
}

lambda / lambda.coeffs().first()
// So that the constant term is always 1

Loop invariant -> 算法正确性。找到的 LFSR 肯定是一个成立的。最小性原因是我们在 Degree 上升的时候更新用来修 Discrepancy 的多项式，证明待补充（我还没看懂，乐）

Other notes

现代解读中会把 BM 当成 Padé approximation 的一个特例，在这个解读下它的对面是扩展欧几里得。现代 RS decoder 也有很多通过 EEA 实现的。可能需要继续阅读以下内容：

Forney algorithm: 在已知错误位置后计算错误值。在其中定义的 Error evaluator 是将 RS decoding 建模为 Padé approximation 问题的基础。
Modified Euclidean Algorithms for Decoding Reed-Solomon Codes

Hello, World!

#hello-world @ 2026-03-07T16:20:35+08:00

Hello! 这是 [喵喵](@CircuitCoder) 的笔记本。这里记录了我一些未经整理的笔记和想法，反映我的小脑瓜里在想什么，因此绝大多数内容会使用最接近我思考的中英混杂写成，请见谅。

制作这个笔记的动机是想有一个类似[杰哥](@jiegec)的知识库，但是考虑到我的知识一点都没有结构性，所以正好就做成了这样一个杂乱无章的 UI，非常合适。

这里的想法成熟之后可能会整理变成我的博客的帖子，内容也可能会随便删改修订，如果需要 Permalink 的话请复制每个 Section 标题下方更新日期的那个链接，那个链接带有 Commit Hash，可以保证不变。

这里没有评论区，可以直接在 Repo 的 Issue section 发 issue。

Git Repo: CircuitCoder/scribble

类型体操

#type @ 2026-03-07T16:14:32+08:00

Rocq 和 Agda 的 Inductive type 的 Elimination 都是 pattern matching as intrinsic, induction principle 是生成出来的。因此去有的时候为了写明白 motive 会比较麻烦。