0

在最后一段，用户手册 2.5 的第 23 页（我使用的是 2.5.4）：

“类型说明符可以由两个用 .. (<TWO DOTS>) 分隔的表达式给出。这两个表达式都必须计算为常量整数，并且可以包含定义名称和模块形式参数。例如，-1 - P1 .. 5 + D1，其中 P1 指的是模块形式参数，而 D1 指的是定义。P1 和 D1 都必须可以静态评估为整数常量。”

我已经测试了许多不同的示例来运行类似的东西，但我最终不能。这是其中之一：

MODULE main
VAR
    third_party : third_party;
    alice : alice(third_party.n); 

MODULE third_party
FROZENVAR
    p : 0..1000;
    q : 0..1000;
DEFINE 
    n := p * q;

MODULE alice(n)
FROZENVAR
    r :  1 .. n;

或类似的东西：

MODULE main
FROZENVAR
        p : 0..1000;
        q : 0..1000;
VAR
alice : alice(n);
    DEFINE 
        n := p * q;
MODULE alice(n)
    FROZENVAR
        r :  1 .. n;

错误是“无效的子范围 1 .. n”

有谁能够帮我？你能给我例子，类型说明符包含定义和模块形式参数的名称并正确运行吗？

事实上，这段代码是 fiat-shamir 协议的一部分，我正在对不同的 n 值（n 不能是常量整数）测试 ctl，并寻找一个反例。

4

1 回答 1

0

问题是这third_party.n不是静态可评估的。它取决于 和 的值third_party.p，third_party.q它们都是可变的。因此，模块不是用静态可评估表达式实例化的。

一个可能有效的例子是：

MODULE main
VAR
    third_party : third_party;
    alice : alice(third_party.n); 

MODULE third_party
FROZENVAR
    p : 0..1000;
    q : 0..1000;
DEFINE 
    n := 10 * 10;

MODULE alice(n)
FROZENVAR
    r :  1 .. n;
于 2015-09-12T16:17:57.533 回答