InteractionTrees 库 - ASM 上的简单程序

Question

我正在尝试在本教程中的 ASM（一种简单的控制流图语言）上编写简单的程序： 交互树 -> ASM.v

我的最终目标是使用库的功能

证明其正确性

我正在尝试编写的函数：

如果 current_i （即 42）小于或等于 val （函数参数） - 我们返回 current_i，即 42 否则我们返回 current_i + 1，所以我们返回 43

我们将使用的寄存器： 2 - 当前_i ; 3 - i_leq_val

这是下面的伪代码，它包含标签、指令和跳转：

function asm_forty_two (val : operand) {                 (* val is parameter *)
0 :                                                      (* entry label 0 *)
  Istore ("current_i") (Oimm 42)                         (* %current_i = 42 *)
  Bjmp 1                                                 (* jump to label 1 *)

1 :                                        (* internal label 1 *)
  Iload 2 current_i                        (* we load current_i into register #2 *)
  ILe 3 2 val                              (* we load into register #3 result of comparison
                                              of current_i (which is in register 2 and val) *)
  Bbrz 3 3 2                               (* if in register 3 we have 1 - go to label 3 else
                                              go to label 2 *)


2 :                                        (* internal label 2 *)
  
  Iadd 2 2 (Oimm 1)                        (* we add 1 to current_i (which is in register #2) 
                                              and put it back into register #2  *)
  Bjmp 3                                   (* jump to label 3 *)

3 :                                        (* exit point 3 *)
  Bhalt                                    (* return current_i which is 42 or 43 (depends on val)
}

现在我正在定义asm（即记录）。因为我们有 1 个入口点和 1 个出口点，所以类型为

asm 1 1

是否正确？

下面的代码我试图在文件中的库中编译 ASM.v

Definition asm_forty_two (val : operand) : asm 1 1 :=
  {|
    internal := 2;
    (* in our case fina = 3 : one entry point and 2 internal points *)
    code := fun fina => match fina with
                     | (exist _ 0 _) => 
                          bbi (Istore ("current_i"%string) (Oimm 42))
                               (bbb (Bjmp ((exist (fun j : nat => (j < 1 + 1)) 1 _))))
                     | (exist _ 1 _) => bbi (Iload 2 "current_i"%string)
                                               (bbi (ILe 3 2 val)
                                                  (bbb (Bbrz 3
                                                          (exist (fun j : nat => _) 3 _)
                                                          (exist (fun j : nat => _) 2 _)
                                               )))
                     | (exist _ 2 _) => bbi (Iadd 2 2 (Oimm 1))
                                            (bbb (Bjmp (exist (fun j : nat => _) 3 _)))
                     | (exist _ 3 _) => bbb Bhalt
                     end
  |}.

但是它不会编译...“非详尽的模式匹配”或“未解析的隐式参数”...

我可以在 ASM 上提供这样简单的函数的示例吗？它可以编译吗？标签应该从0开始吗？这里如何使用 fi' 表示法？

Answer 1

• match

  的详尽检查器非常基本。它没有利用

  nat

  场有界这一事实。最简单的解决方案是使最后一个子句成为包罗万象的子句。 （让 Coq 相信其余分支不可访问是乏味且不必要的。如果你真的想这样做，使用

  Equations

  库会比

  match

  更好。）

• 没有输出标签（你的标签3是内部标签），有3个内部标签。所以类型是

  asm 1 0

  。输出跳跃中的不等式证明应该是

  j < 3

  。

• 首先对内部标签进行编号，然后对外部标签进行编号。这隐含在

  asm

  的定义中、操作数

  internal + A

  和

  internal + B

  的排序中。

  Record asm (A B: nat) : Type :=
  {
    internal : nat;
    code     : bks (internal + A) (internal + B)
  }.
  

  在您的 asm 代码中，条目标签

  0

  是外部的，而标签

  1

  、

  2

  、

  3

  是内部的，因此索引会移位。

  ASM labels | Coq labels
  0          | 3    (external)
  1          | 0    (internal)
  2          | 1    (internal)
  3          | 2    (internal)
  

• 由于所有标签都是文字，因此不等式证明

  j < 3

  可以使用策略

  simpl; auto

  来解决。您可以使用符号

  ltac:(simpl; auto)

  代替

  0 < 3

  、

  1 < 3

  、

  2 < 3

  类型的证明项。还要确保填写

  exist

  第一个参数中的任何漏洞，以使这些类型明确（否则

  simpl; auto

  将具有未知的目标）。

Definition asm_forty_two (val : operand) : asm 1 0 :=
  {|
    internal := 3;
    code := fun fina => match fina with
                     | (exist _ 0 _) => bbi (Iload 2 "current_i"%string)
                                               (bbi (ILe 3 2 val)
                                                  (bbb (Bbrz 3
                                                          (exist (fun j : nat => j < 3) 2 ltac:(simpl; auto))
                                                          (exist (fun j : nat => j < 3) 1 ltac:(simpl; auto))
                                               )))
                     | (exist _ 1 _) => bbi (Iadd 2 2 (Oimm 1))
                                            (bbb (Bjmp (exist (fun j : nat => j < 3) 2 ltac:(simpl; auto))))
                     | (exist _ 2 _) => bbb Bhalt
                     | (exist _ _ _) => 
                          bbi (Istore ("current_i"%string) (Oimm 42))
                               (bbb (Bjmp ((exist (fun j : nat => (j < 3)) 0 ltac:(simpl; auto)))))
                     end
  |}.