愿望单

#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 模乘可以将计算过程中的除法替换为另一个被除数。

，需要计算，如果中的元素都使用最小非负代表元表示，这就是要计算。假设有另一个常数满足而且两者互素。假设除以的代价较小。

称的 Montgomery 形式。因为的带余除法代价小，计算的代价很小。需要注意的是和的代价较大。只要能够避免这两个操作，就能得到更快的模乘实现。

是在里面的逆元，是在里面的逆元。

注意到：

所以一定是的倍数，在中计算相当于计算：

最后我们可以通过 Bound 来消除最外面的：注意到因为，这个值一定在之间。所以我们只需要比较这个值是否是负数，如果是就加上就好了。

实现中的一些细节：

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

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 的东西。经典例子：没有非标模型，因为任何模型都有前段，而这个前段套进二阶归纳里面直接得到所有元素都在里。

这直接导致了二阶逻辑甚至没有一个 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. 符号集加一个常元，考虑
如果只考虑 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 。将这一映射称为 .

具有 “Rectangle property”，是一个 Rectangle：

可以理解成，如果有任意两个所有 Party 的私有状态集合满足，那么可以把和任意组合（每个 Party 任意在两者中选一个），那么最终 Transcript 依旧是。

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

这有两个很直接的后果：

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

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

Reed-Solomon 纠错

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

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

Berlekamp-Welch

假设 Underlying polynomial 是，Claim 存在一个多项式，满足。如果不是错误的点，对没有要求。因为最多个错误，所以我们可以要求，并且最高次项系数为，剩下个系数未知。

对所有采样点成立。这给我们提供了个方程，，令，，线性系统一共个方程，个未知数，可以解出和，之后或者 Chien search. 复杂度

Alternatively, 这是一个 Rational polynomial interpolation 问题，经过个点。wo/ FFT 复杂度 , w/ FFT 复杂度。（但我都不会）

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.

令为消息长度，为冗余，为 Codeword 长度。

对于 Generator view 的 RS code，预先选定的是一个 Generator polynomial ，。Underlying field 满足，要求。

Generator polynomial 的常见构造方式是选定一个的 primitive element 和任意 , 。

对于个消息，Message polynomial 是。有两种编码方式得到 Codeword ：

简单编码直接让。解码的时候需要做一次多项式除法
Systematic encoding 令，然后。Systematic encoding 的好处是前个符号就是消息，解码的时候非常简单

Sidenote: 因为消息总能做 Padding，尤其是 Systematic encoding 里面消息 Padding 直接对应 Codeword padding，所以都可以不传这部分 Codeword。因此的限制事实上限制的是最大 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 如果理解成在多项式空间里的函数，都是可逆线性的。因为是一个 degree-m 子空间，因此所有无错误 Codeword 也是一个 degree-m 子空间。错误校验是判定一个多项式是否在这个空间内。

在这个多项式空间上取以下内积结构：系数乘积的和 (i.e. 选取做基映射到 )。。Codeword 空间的正交补空间 degree 是，因此可以通过个多项式来 span 这个正交补空间。

定义 Parity-check polynomial 。，令是的 Reciprocal polynomial。是正交补空间的一组基。

他们是正交补空间的基的简短证明：这组基显然线性无关。同样，是 Codeword 空间的一组基。为了证明他们是正交补，只需要证明两组基中任选向量内积为 0 即可。

注意到，正是表达式的次项系数。而

对于使用 Powers of primitive root 构造的，有更简单的办法给一组基。注意到任何的根都是的根，所以令，那么，因此是一组正交补空间的基。

上述构造出的正交补空间的基不一定正交，但是我们还是可以把投影上去，如果正确的编码是，投影得到的结果是也就是错误项在选定基下的坐标。这一坐标通常被称为 Syndrome 。

在使用 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 )，有更高效的做法。

假设里面实际有个错误，位置分别在次项，也就是：

因此。现在的目标是找到。定义 Error locator polynomial:

的根为。假设展开为，可以证明对于任意给定的正整数 (见 Wikipedia)：

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

BM 算法的直觉是一个一个试，看看目前猜的 LFSR 有没有出错。保存一个上一次出错的时候的 LFSR，以及当时出的错，如果这次出错，那么把上次的 LFSR 减掉就可以用来修这次的错。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 会比较麻烦。