RFC-0:函数签名中的泛型大小数组

该RFC提议在noname中支持常量泛型,泛型参数可以从观察到的参数(如常量、数组或结构体)中解析。这将提高代码的可重用性和模块化,并且是支持具有符号大小的通用数组的先决条件。文章详细介绍了代码示例、内置示例、单态化、实现方法和单态化过程。

RFC-0: 函数签名中的泛型大小数组

概要

此 RFC 提议在 noname 中支持 const generics。泛型参数可以从观察到的参数中解析,例如常量、数组或结构体。这提高了代码的可重用性和模块化。这是支持具有符号大小的泛型数组的先决条件。

代码示例

以下是一些泛型参数如何使用的预览,以及它将解锁哪些功能。

允许函数创建具有符号大小的数组:

// 返回类型由泛型参数决定
// 因此 `init_arr` 可用于创建具有不同大小的数组
fn init_arr(const LEN: Field) -> [Field; LEN] {
    let arr = [0; LEN];
    return arr;
}

fn main() -> [Field; 3] {
    let arr = init_arr(3);
    return arr;
}

从观察到的数组参数中解析泛型值:

fn last(arr: [Field; LEN]) -> Field {
    // 使用泛型参数 LEN 在函数作用域中形成动态表达式
    return arr[LEN - 1];
}

fn main() -> Field {
    let arr = [1, 2, 3, 4, 5];
    // 泛型参数 LEN 可以从参数 `arr` 的数组大小解析
    return last(arr);
}

内置示例

给定内置函数的以下函数签名:

fn to_bits(const LEN: Field, val: Field) -> [Field; LEN]
fn from_bits(bits: [Bool; LEN]) -> Field

在原生代码中调用内置函数:

use std::bits;

const num_bits = 8;

fn main() {
    let val1 = 101;
    // `num_bits` 将被赋值给返回类型中的泛型参数 `LEN`
    // 然后 `bits` 的类型将被单态化为 [Bool; 8]
    let bits = bits::to_bits(num_bits, val); 
    // `LEN` 的值可以在单态化期间从 `bits` 的大小确定
    // 因此内置函数知道要转换多少位
    let val2 = bits::from_bits(bits); 
    assert_eq(val1, val2);
}

泛型参数的值将通过 generics 参数传递给函数:

fn to_bits<B: Backend>(
    compiler: &mut CircuitWriter<B>,
    generics: &GenericParameters,
    vars: &[VarInfo<B::Field, B::Var>],
    span: Span,
) -> Result<Option<Var<B::Field, B::Var>>> {
    ...

    // 从 `generics` 参数中检索泛型值
    let bitlen = generics.get("LEN") as usize;

    ...
}

返回类型和返回的变量都可以在内置函数之外进行检查。返回类型可以像原生函数一样自动检查,原生函数的类型会在特定点传播并收敛,如果在类型不匹配时会抛出错误。

返回的变量可以通过依赖类型进行检查。每个具体类型都有固定数量的变量。通过内置函数的已解析返回类型,我们可以检查大小是否匹配。此外,我们可以使用类型结构递归地检查这些值,但这可能仅限于检查具有明显范围 0 或 1 的布尔类型。因此,自动检查内置函数的实际返回值是一个未来需要改进的方面。

单态化(monomorphization)

泛型值的解析可以通过观察传递给函数的参数来完成。然后,它将解析后的值存储在相关上下文中,以供后续编译器管道进行类型检查和电路综合。我们将解析泛型值和类型检查的过程称为 单态化(Monomorphization)

当前编译 noname 代码的流程是:

  1. 将代码解析为 AST
  2. 将 AST 转换为带有命名解析的 NAST
  3. 将 NAST 转换为带有类型元数据收集和类型检查的 TAST
  4. 电路综合,将 TAST 转换为约束系统

使用泛型参数,当前的 TAST 阶段无法再处理类型检查,因为泛型参数是未知的。例如,如果不解析泛型参数的值,它就无法类型检查具有符号大小的数组。

为了扩展类型检查以支持泛型参数,我们可以在 TAST 阶段之后添加一个 MAST 阶段(单态化 AST),以解析泛型参数的值。电路合成器将依赖于 MAST 而不是 TAST 来编译电路。

新的流程将是:AST Parser -> NAST -> TAST -> MAST -> 电路综合

实现

为了支持如上例所示的泛型语法,我们需要更改 AST Parser 以支持泛型语法。此外,由于泛型参数无法在 TAST 阶段解析,因此某些类型检查将不那么严格,并将推迟到 MAST 阶段。

新添加的 MAST 阶段将负责从观察到的参数中解析泛型值。它包括对 TAST 阶段中绕过的单态化类型的类型检查。

泛型语法

此 RFC 提出了一种简单的泛型语法,而没有引入常见的 turbofish 语法,因为我们不需要从函数参数中解析泛型参数。相反,可以通过将值与观察到的参数进行比较来直接解析泛型参数的值。

例如,使用 turbofish,我们可以这样做:

fn create_arr<N>(arr: [Field; N + 3]) -> [Field; N + 3] {...}

这是一个罕见的例子,其中泛型参数无法从观察到的参数中轻松解析。为了在没有任何高级推断设置的情况下使其工作,需要通过 turbofish 语法手动将 N 的值传递给函数,例如:

// a 的类型为 [Field, 6]
let a = create_arr::<3>(arr);

但是,在大多数情况下,可以通过简单地观察传递给函数的参数来获得泛型参数的值。此 RFC 旨在保持语法的简单性和直观性。在没有 turbofish 语法的情况下,泛型语法可以简化为如下所示:

// LEN 的值等于传入的参数
fn create_arr(const LEN: Field) -> [typ; LEN]

// 如果参数是数组,则 LEN 的值等于数组的大小
fn last(arr: [typ; LEN]) -> Field

在函数作用域中,可能需要确定一个变量是否是泛型参数。我们将至少包含 2 个字母的字符串(应全部大写)作为泛型参数。

AST Parser

Parser 需要为以下构造 FunctionDef 收集泛型标识符。它将添加一个新的 TyKind,即 GenericSizedArray(type, size)GenericSizedArray 的大小由一个 Symbolic 值表示,该值可以包含泛型参数或具体值。

我们将 generics 字段添加到 FunctionDef,它是一个 GenericParameters 集合,用于在泛型名称和值之间进行映射。

enum Symbolic {
    Concrete(u32), // 字面值
    Generic(GenericParameters), // 泛型参数
    Constant(Ident), // 指向一个常量变量
}

GenericSizedArray {
    ty: TyKind,
    size: Symbolic,
}

更新 FunctionDef

pub struct FunctionDef {
    ...
    // 要添加
    pub generics: HashSet<GenericIdentifier>,
}

带泛型参数的函数示例:

fn create_arr(const LEN: Field) -> [Field; LEN] {...}

解析器应创建如下伪代码的函数定义:

FunctionDef{
    FnSig = {
        ...
        generics = {"LEN": null},
        FnArg = {
            name: 'LEN', 
        }
        // Add / Mul / Generic / Concrete 是 Symbolic 枚举的变体
        return_type: GenericSizedArray(Field, Generic("LEN"))
    }
}

TAST 使用这些泛型参数的元数据来类型检查泛型标识符的一致性。在 MAST 阶段,它们对于从观察到的参数中解析泛型值很有用。

TAST

泛型值从观察到的参数中解析。如果声明了泛型参数,则应在函数体中使用它们。我们需要检查声明的泛型参数是否有意义。

类型检查函数的泛型参数

// 不应该允许这样做,因为 LEN 应该在函数参数中定义
fn foo(n: Field) -> [Field; LEN] {...}

// 如果函数体中没有使用 NN,则不允许
fn foo(const NN: Field) {...} 
fn foo(arr: [Field; NN]) {...} 

禁止在 for 循环中使用泛型函数

for ii in 0..NN {
    // 任何将 for 循环变量作为参数的函数都应该被禁止
    fn_call(ii);
}

为了允许在 for 循环中使用泛型函数,我们需要注意展开循环并使用循环变量的具体值实例化函数。这不在此 RFC 的范围内。

禁止对参数的符号值进行操作

// 禁止对函数参数的符号值进行算术运算,
// 例如本例中的 NN * 2。
// 因为解析 NN 的值具有挑战性。
fn last(arr: [Field; NN * 2]) -> Field {
    return arr[NN - 1];
}

推迟类型检查 任何涉及泛型参数的内容都应推迟到 MAST 阶段。我们需要推迟对具有泛型大小的数组的类型检查。

在 MAST 阶段,可以解析泛型参数的值,因此可以评估符号值。因此,可以类型检查所有带有泛型参数的类型,因为数组大小变为具体值。

MAST

在 TAST 阶段之后,MAST 阶段可以通过传播主函数 AST 中的常量值来从观察到的参数中解析泛型值。

解析算法

该算法需要处理以下两类:

  • 从常量参数解析
  • 从数组参数解析

从常量参数解析的示例:

// 常量泛型
// - LEN 的值可以从观察到的传播的常量值解析
// - 将值存储在函数体作用域中
fn gen_arr(const LEN: Field) -> [Field; LEN] {
    let arr = [Field; LEN];
    return arr;
}

从数组参数解析的示例:

// 首先,这是一个简单的例子。
// - LEN 可以从参数 `arr` 的数组大小解析
// - 将 N 的值存储在上下文中
fn last(arr: [Field; LEN]) -> Field {
    return arr[LEN - 1];
}
// 然后,这是一个更具挑战性的例子,需要像 SMT 这样的技术来求解泛型参数的唯一值。
// 即使 LEN * 2 看起来很容易求解,但求解它可能需要像 rust 中的(计算机代数系统)CAS。
// 使用已求解的泛型值很容易评估符号值。但反过来却很难。
fn last(arr: [Field; LEN * 2]) -> Field {
    return arr[LEN - 1];
}

在此 RFC 中,我们只想强制执行语法以足以支持简单的情况。也就是说,禁止对函数参数的泛型参数进行算术运算。

回顾一下,以下是函数解析算法的伪代码

// 在函数调用者作用域中
// 收集观察到的参数
//  在函数被调用者作用域中
//    对于每个参数
//      如果参数涉及泛型参数
//        从观察到的参数中解析泛型值
//    对于每个语句
//      使用已解析的泛型值计算类型
//      类型检查
//  返回类型

函数调用实例化

函数定义为 FunctionDef,它是一个 AST,包含函数的签名和主体。主体是一个语句向量,每个语句都是一个表达式节点树。当这些函数的内容没有改变时,不同的函数调用指向这些函数的原始 AST 是可以的,表达式节点也是如此。

但是,当函数接受泛型参数时,实际参数可能会导致不同的表达式节点。例如:

fn last(arr: [Field; LEN]) -> Field {
    return arr[LEN - 1];
}

fn main() {
    let arr1 = [1, 2, 3, 4, 5];
    let arr2 = [6, 7, 8, 9];

    let last1 = last(arr1); // with LEN = 5
    let last2 = last(arr2); // with LEN = 4
}

last(arr1) 的单态化函数体是 return arr[5 - 1],而 last(arr2) 的单态化函数体是 return arr[4 - 1]。因此,我们不能有一个单一的表达式节点来表示 arr[5 - 1]arr[4 - 1] 表达式节点。这些函数应该使用新的 AST 实例,这些 AST 是从原始 AST 单态化的。它们将使用已解析为具体值的泛型参数重新生成。对 last 的两次调用应指向两个不同的单态化函数实例。

为了确保为这些实例化的函数重新生成的节点 ID 没有冲突,主函数作为入口点的 AST 将被重新生成。单态化 AST 保留了 span 信息,以指向 noname 源代码以实现现有的调试功能。

与之前一样,这些实例化的函数可以由表达式节点 ExprKind::FnCall 指向。在支持泛型参数的情况下,我们需要更改加载函数 AST 的方式,因为当前的完全限定名称模式不包含区分具有不同泛型值的实例化函数的信息。

因此,我们可以生成单态化函数名称,并使用它来存储单态化函数 AST,而不是原始函数名称。存储单态化函数 AST 的新字符串模式可以是: fn_full_qualified_name#generic1=value1#generic2=value2

类型检查 泛型函数的实例化将解析泛型类型为具体类型。与 TAST 阶段类似,在单态化函数体期间,计算出的具体类型可以传播并与函数签名的返回类型进行比较。

此阶段的类型检查将始终采用具体类型。任何未解析的泛型类型都将导致类型检查失败。

单态化过程

以下是单态化过程的概述:

  1. 以类型检查器相同的方式传播类型,但也包括常量值,这些常量值将用于解析泛型参数。

  2. 同时,它也传播 AST 节点。当它不是泛型函数的一部分时,节点应保持不变。否则,应重新生成节点。

  3. 每当遇到泛型函数调用时,它会根据参数实例化函数,并将其存储为具有单态化名称的新函数,然后遍历实例化的函数 AST。函数调用 AST 节点将被修改为单态化名称,同时保留相同的节点 ID 和 span。

  4. 在函数实例化过程中,将重新生成所有 AST 节点。此新 AST 将存储在单态化函数名称下。

  5. 单态化函数后,应将原始函数的名称添加到列表中,该列表记录了最终要删除的函数 AST。我们不能立即删除原始函数 AST,因为它可能在不同的地方被调用。

  6. 在每个函数块作用域中,它应该通过比较传播的返回类型和定义的返回类型来类型检查返回类型。所有这些类型都应采用具体形式,而不涉及泛型参数。

  7. 最后,它使用单态化版本覆盖主函数 AST,并根据列表删除泛型函数。

所有更新都已完成对 TAST 中现有存储的更新。

  • 实例化的函数已添加到 HashMap<FullyQualified, FnInfo<B>>
  • 单态化节点的类型存储在 HashMap<usize, TyKind> 中(请记住,节点类型的存储 HashMap<usize, TyKind> 也可以包含已删除函数的节点类型。我们可能需要找到一种安全删除属于已删除函数的节点类型的方法)
  • 应从 HashMap<FullyQualified, FnInfo<B>> 中删除泛型函数。

电路合成器

电路合成器将依赖于单态化 AST 来编译电路。要进行合成,工作流程将与以前相同,但使用单态化 AST。它不需要知道与泛型相关的新添加的支持。与以下部分中描述的替代方法相比,添加的 MAST 阶段简化了在电路合成器中支持泛型功能所需完成的工作。

替代方法

上述单态化的 一种替代方法 是直接在电路编写器中传播泛型值,而无需添加 MAST 阶段。

电路编写器通过 compile_expr 函数遍历原始 AST。此函数传播来自主函数参数和常量的值,并将 VarOrRef 计算为结果。VarOrRef 不返回正在计算的类型结构。

在此过程中,当需要确定表达式节点后面的类型结构时,它依赖于 size_of 函数来确定表示该类型的变量数量。size_of 依赖于表达式的节点 ID 来查找类型。当类型是具体的时,这不是问题。

当表达式节点后面的类型是泛型时,通过 size_of 查找类型大小的方式不再适用,因为表达式节点可以是泛型类型。

要解决此问题,应该有一种新的方法来确定表达式节点的类型大小,而无需依赖节点 ID。一种方法是(如 ComputedExpr 中所述)通过 compute_expr 中的传播来保留类型的结构。compute_expr 不再传递 VarOrRef,而是返回 ComputedExpr,其中包含类型结构和底层变量 VarOrRef

例如,当它为 ExprKind::ArrayAccess 计算时,它可以使用 array 表达式节点的 ComputedExpr 来确定数组的大小,从而对访问索引进行一些边界检查。

这种方法需要对电路编写器的编译过程进行重大重构。它需要更改从使用 VarOrRef 到结构化 ComputedExpr 的假设。它还需要依赖 ComputedExpr 来进行一些额外的检查,而不仅仅是依赖类型。这将需要在 ComputedExpr、实际类型和泛型参数之间进行大量额外的假设。

因此,考虑到编译器的流程,我们认为单态化方法更直接且更易于长期维护。

  • 原文链接: github.com/zksecurity/no...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
zksecurity
zksecurity
Security audits, development, and research for ZKP, FHE, and MPC applications, and more generally advanced cryptography.