问题标签 [fstar]

我想使用 Emacs fstar-mode 和 gdb 调试简单的 F* 程序。在 fstar-mode https://github.com/FStarLang/fstar-mode.el的 wiki 的最后是信息：

没有进一步的解释。

在 Emacs 中（假设我正在编辑 Test.fst 文件）我调用fstar-gdb命令并继续到gdb控制台我正在尝试使用命令file Test和run. 他们工作正常，但是break 3（或任何其他行）说它main.c（显然）找不到第 3 行。

如何gdb与 F* 一起使用？

我想编写一个函数，强制它的参数在语法上是一个常量字符串。这是我尝试过的：

但是，我很确定静态引号（带有 `）不是我想要的，而是带有quote. 但这会将我的先决条件置于 Tac 效应中。在目前的情况下，有什么办法可以做我想做的事吗？

我想证明在有限数量的情况下参数化的属性。我想将问题划分为每个案例一个实例，并分别解决每个实例。这是一个清理事情的例子：

在这种情况下，案例由列表 lst 定义。我可以很容易地证明 propHolds：

但我显然不想为每种情况写一个单独的 assert_by_tactic （不是当可能有数千个......）。我想以某种方式为 lst 中的所有元素自动生成上述证明。

我尝试了各种各样的东西，这里是其中之一：

不幸的是，这并没有完全达到我想要的效果，assert_by_tactic 失败了（并且没有以我期望的方式减少）。我想我遗漏了一些关于标准化的明显内容，但是在 F* 中执行此操作的规范方法是什么？如果解决方案指向失败的“案例”/断言（如果存在），则加分。

我正在尝试在 F* 中创建一个函数来确定列表的最小元素，如果列表为空，我想抛出异常。我到目前为止的代码如下：

但是，当我尝试验证文件时，出现以下错误：

我该如何解决这个错误？

我一直在从它的一些论文和 F-star 教程中阅读有关 F-star 的信息，但我发现自己在试图理解它的概念时迷失了方向。例如，依赖类型、Dijkstra monads 等。

正确理解和学习 F-star 的先决条件是什么？对任何资源的链接的任何解释也将有所帮助。

我正在尝试调用另一个模块中的函数，该模块负责确保保留堆上的前置/后置条件。具体来说，它确保在调用 read 之前传入的字符串是“可读的”：

这允许它满足如下定义的读取前提条件：

当我创建一个主函数并调用checkedRead "file"它时工作正常，但是当我尝试在另一个模块中使用这个模块时，它会抱怨以下错误：

如果您尝试read直接调用而不使用checkedRead（在主文件中），这与您将看到的错误相同，这意味着编译器不相信满足前提条件。

如果我在另一个文件中复制checkedRead（并且只有那个函数）它可以正常工作。因此，编译器似乎无法推断这满足跨模块边界的条件。

如何使用checkedRead其他文件中的函数而不必在本地重新定义它？

如何检查 FStar 中的两个集合是否相等？以下表达式的类型Type0不是Tot Prims.bool所以我不确定如何使用它来确定集合是否相等（例如在条件中）。是否应该使用不同的功能来代替Set.equal？

我正在尝试编写两个相互归纳数据类型的声明，它们都将类型参数作为参数，如下所示：

我收到如下错误消息：

LabeledStates.fst(59,0-64,31)：（错误 67）未能解决归纳法的全域不等式 报告了 1 个错误（见上文）

（其中第 59 行是包含“type foo 'a”的行）

这个错误是什么意思，我能做些什么来解决它？

如果我删除类型参数（例如，给 foo.x 提供 int 类型），我就不会再收到错误了。同样，如果我只给其中一种类型一个类型参数而不给另一个类型，我也没有错误。

有时，子类型判断太难让 f-star 自动计算出来，f-star 希望我更详细地说明我的证明。我也遇到了一些情况，我想写一个引理来证明 f-star 可以做出一些类型判断。

一段看起来像它的语法确实可以解析，但它似乎没有做我想要的。我怀疑我误解了这个语法的作用。在这里，我试图证明 x 具有带引理的类型 nat。为什么这不像我认为的那样？

我也很惊讶我可以在那个位置写“x：nat”。如果需要，我如何“证明 x 是 nat”？

这是一个简单的模式生成器，它返回一个1:nat. lemma_1证明生成的任意长度列表的每个位置都有一个 1。必须引入for的lng参数，因为否则会被限制为与in其类型为 的 in发生类型冲突。如果没有额外的参数，如何解决这个问题？nth_1nn:nat{n < length lst}nlemma_1n:nat{n < lng}

似乎问题与gen_1模式不得为零长度的约束有关。有没有更好的方法来表达这个标准？