如何检查 16 的对齐块是否u32连续（并且递增）？
例如：[100, 101, 102, ..., 115]是。并且，[100, 99, 3 ...]不是。
我使用的是 AVX512f。这是我到目前为止所拥有的：
算法A：
* predefine DECREASE_U32, a u32x16 of [15,14,13,...0]
* let a = input + DECREASE_32 // wrapping is OK
* compare a to u32x16::splat(first_item(a))
* Return whether all true
替代方案（算法 B）
* let b = copy of A
* permute the elements of b by one position
* let b = a-b
* Is b all 1's (except for 1st position)
我在 Rust 中使用packed_simd板条箱执行此操作，但任何语言/伪代码都可以。（我希望有一个 SIMD 操作来减去相邻项。）
我正在尝试在 Dafny 中调试变量验证时间。我尝试运行verificationLogger，但没有得到任何输出。
我使用的是 Windows（但对 Linux 解决方案很满意）
我将路径设置为 VSCode 加载项安装的 Dafny 版本，如下所示：
设置路径=C:\Users\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%
我跑：
dafny verify --verification-time-limit:15 --cores:6 --boogie -randomSeedIterations:10 --boogie -verificationLogger:csv repro1.dfy
但我没有看到 CSV 输出。
我在 Dafny 中创建了一个经过验证的 SortedMap。它是（键，值）对的序列。键是排序的、不同的整数。我不知道如何表明“KeySet”的长度必须等于序列的长度。
——卡尔
错误：
this is the postcondition that could not be proved
|
7 | ensures |KeySet(sorted_seq)| == |sorted_seq|
简化代码：
predicate SortedSeq(sequence: seq<(int, int)>) {
forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}
function KeySet(sorted_seq: seq<(int, int)>): set<int>
requires SortedSeq(sorted_seq)
ensures |KeySet(sorted_seq)| == |sorted_seq|
{
set i | i in sorted_seq :: i.0
}
method Main()
{
var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
print KeySet(s);
}
我对任何可验证的 CountLessThan 编写方式持开放态度。这是我所拥有的：
function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
set i | i in numbers && i < threshold
}
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
ensures count == |SetLessThan(numbers, threshold)|
{
count := 0;
var shrink := numbers;
var grow := {};
while |shrink | > 0
decreases shrink
invariant shrink + grow == numbers
invariant count == |SetLessThan(grow, threshold)|
{
var i: int :| i in shrink;
shrink := shrink - {i};
grow := grow + {i};
if i < threshold {
count := count + 1;
}
}
}
method Main()
{
var s: set<int> := {1, 2, 3, 4, 5};
var c: int := CountLessThan(s, 4);
print c;
// assert c == 3;
}
这是定义排序集、排序映射、范围集的一小步。
我想计算 Dafny 中设置小于阈值的元素，但我无法弄清楚“确保”。
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
ensures count == |{i in numbers | i < threshold}|
{
count := 0;
var ss := numbers;
while ss != {}
decreases |ss|
{
var i: int :| i in ss;
ss := ss - {i};
if i < threshold {
count := count + 1;
}
}
}
method Main()
{
var s: set<int> := {1, 2, 3, 4, 5};
var c: int := CountLessThan(s, 4);
print c;
// assert c == 3;
}
错误是：this operator chain cannot continue with an ascending operator