如何在Coq中实现支持标签的汇编程序表示方案？

我正在Coq中实现汇编程序到字节序列的表示与编译流程，目前已完成汇编语言定义、解码器、编译器，并证明了良类型指令的解码器是编译器的逆过程。

现在需要设计更易读写的汇编表示，核心需求是支持标签（label）功能，避免在分支/跳转指令中手动计算指令长度和偏移量（这是该表示与现有asm类型的核心区别）。整体数据流转如下：

带标签的汇编表示（当前待实现）
                |
                V
汇编器（已有雏形）
                |
                V
完整汇编（即现有`asm`类型）
                |
                V
        编译器（已完成）
                |
                V
              字节序列
                |
                V
        解码器（已完成）
                |
                V
完整汇编（即现有`asm`类型）

现有实现片段 #

以下是已完成的部分代码：

Require Import NArith.

Inductive asm : Type :=
  | ADD (rd rs1 rs2:N)
  | BEQ (rs1 rs2:N) (si:Z)
  (* 其他汇编指令 *)
.

(* 用于查找标签位置的临时函数 *)
Require Import String.
Require Import List.
Import ListNotations.

Open Scope string.
Open Scope N.
Definition insn_length (a:asm) : N := 4.

Fixpoint label_loc (label:string) (base_addr:N) (code:list (sum string asm)) : option N :=
  match code with
  | nil => None
  | inl label' :: t => if (label =? label')%string then Some base_addr 
      else label_loc label base_addr t
  | inr insn :: t => label_loc label (base_addr + (insn_length insn)) t
  end.

(* 理想的程序表示：标签与指令混合的列表，指令可通过标签位置计算立即数 *)
Definition ideal_example (base_address : N) : list (sum string asm) :=
  [ inr (ADD 0 0 0) ;
    inl "label" ;
    inr (BEQ 0 0 (label_loc "label" base_address (ideal_example base_address)))
  ].

尝试过的方案与问题 #

我曾尝试用互递归定点函数实现，但Coq报错：A fixpoint needs at least one parameter，且该方案存在额外间接层，并非理想的定点实现：

Fixpoint mutual_recursion_example : list (sum string asm) :=
  [ inr (ADD 0 0 0) ;
    inl "label" ;
    inr (BEQ 0 0 klabel)
  ]
with klabel := label_loc "label" 0 mutual_recursion_example.

预汇编语言方案思考 #

我考虑定义一个预汇编语言pre_asm，将标签引用作为指令的一部分，再通过预处理转换为现有asm类型，但需要证明该转换是语义保留的，希望能得到社区的经验反馈：

(* 候选预汇编语言定义 *)
Inductive pre_asm :=
  | pADD (rd rs1 rs2:N)
  | pBEQ (rs1 rs2:N) (si_or_label:sum Z string)
.

Fixpoint preprocess (base_address:N) (code:list (sum string pre_asm)) : list asm
  := (* 待实现预处理逻辑 *).

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