如何让Spoq为LLVM IR函数生成Coq高层规范而非AST

• 我正在尝试用Spoq框架将C代码转换为Coq代码，但目前只能得到函数的低层规范（仅AST结构），无法生成带参数、包含不动点（fixpoint）的高层规范。
• 已完成操作：成功将测试C代码编译为LLVM IR，通过命令 python3 AutoV/main.py build TestFactorialProof/proof.v 生成了Coq项目，但怀疑配置文件proof.v存在不足。
• 已知需要手动编写不动点定义，例如：

  Definition rank (i: nat) := MAX_PAGE - i.(*user input*)
  

  但不清楚这类定义应该写在何处（是否放在proof.v中）。
• 额外问题：找不到包含简单演示示例的Spoq官方文档，缺乏参考案例。

我已准备好以下材料：测试用C代码、proof.v配置文件、生成的Code.v内容、未生成有效高层规范的Spec.v内容，希望能得到针对性的帮助。

内容的提问来源于stack exchange，提问作者Natasha Klaus