Как сделать код OCaml (или Coq) из кода llvmir с использованием фреймворка vellvm

Я изучаю vellvm framework.

Как я могу проверить простую функцию на C с помощью vellvm?

Я знаю, что могу использовать утверждения внутри кода .ll. ; ASSERT EQ: i32 0 = call i32 @foo(i32 0)

но я хочу большего

Это функция, которую мне нужно проверить:

int foo() {
  return 3;
}

Это .ll версия моего кода

; ModuleID = 'return3.c'
source_filename = "return3.c"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"

; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @foo() #0 {
  ret i32 3
}

attributes #0 = { noinline nounwind optnone uwtable "frame-pointer" = "all" "min-legal-vector-width" = "0" "no-trapping-math" = "true" "stack-protector-buffer-size" = "8" "target-cpu" = "x86-64" "target-features" = "+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu" = "generic" }

!llvm.module.flags = !{!0, !1, !2, !3, !4}
!llvm.ident = !{!5}

!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{i32 7, !"PIC Level", i32 2}
!2 = !{i32 7, !"PIE Level", i32 2}
!3 = !{i32 7, !"uwtable", i32 1}
!4 = !{i32 7, !"frame-pointer", i32 2}
!5 = !{!"Ubuntu clang version 14.0.0-1ubuntu1.1"}

а это внутреннее представление Coq AST (получено после интерпретации vellvm)

Internal Coq representation of the ast :

(TLE_Source_filename "return3.c")
(TLE_Datalayout "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128")
(TLE_Target "x86_64-pc-linux-gnu")
(TLE_Definition 
  (mk_definition _ 
    (mk_declaration (Name "foo") (TYPE_Function ((TYPE_I 32)) []false) 
      ([], []) 
      [(FNATTR_Attr_grp (0)%Z)] 
      [ANN_preemption_specifier PREEMPTION_Dso_local] 
      [] 
      ((mk_block (Anon (0)%Z) [] [] (TERM_Ret ((TYPE_I 32), (EXP_Integer (3)%Z))) None), [])
    )
  )

(TLE_Attribute_group (0)%Z [FNATTR_Noinline; FNATTR_Nounwind; FNATTR_Optnone; FNATTR_UwtableNone; 
  (FNATTR_Key_value ("frame-pointer", "all"));   
  (FNATTR_Key_value ("min-legal-vector-width", "0")); 
  (FNATTR_Key_value ("no-trapping-math", "true")); 
  (FNATTR_Key_value ("stack-protector-buffer-size", "8")); 
  (FNATTR_Key_value ("target-cpu", "x86-64")); 
  (FNATTR_Key_value ("target-features", "+cx8,+fxsr,+mmx,+sse,+sse2,+x87")); 
  (FNATTR_Key_value ("tune-cpu", "generic"))]
)

(TLE_Metadata 
  (Name "llvm.module.flags") 
  (METADATA_Node 
    [ (METADATA_Id (Anon (0)%Z)); 
      (METADATA_Id (Anon (1)%Z)); 
      (METADATA_Id (Anon (2)%Z));   
      (METADATA_Id (Anon (3)%Z)); 
      (METADATA_Id (Anon (4)%Z))
    ]
  )
)

(TLE_Metadata 
  (Name "llvm.ident") 
  (METADATA_Node [(METADATA_Id (Anon (5)%Z))])
)

(TLE_Metadata 
  (Anon (0)%Z) 
  (METADATA_Node 
    [(METADATA_Const ((TYPE_I 32), (EXP_Integer (1)%Z))); 
     (METADATA_String "wchar_size"); 
     (METADATA_Const ((TYPE_I 32), (EXP_Integer (4)%Z)))
    ]
  )
)

(TLE_Metadata (Anon (1)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "PIC Level"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (2)%Z)))]))

(TLE_Metadata (Anon (2)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "PIE Level"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (2)%Z)))]))

(TLE_Metadata (Anon (3)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "uwtable"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (1)%Z)))]))

(TLE_Metadata (Anon (4)%Z) (METADATA_Node [(METADATA_Const ((TYPE_I 32), (EXP_Integer (7)%Z))); (METADATA_String "frame-pointer"); (METADATA_Const ((TYPE_I 32), (EXP_Integer (2)%Z)))]))
        
(TLE_Metadata (Anon (5)%Z) (METADATA_Node [(METADATA_String "Ubuntu clang version 14.0.0-1ubuntu1.1")]))

Что я могу сделать с этим AST?

Мне нужно доказать (используя Coq) что-то о моей функции, например, что функция всегда возвращает 3.

Как этого можно достичь?

Какие варианты следует рассмотреть, если мне нужно проверить код C с помощью vellvm?

Спасибо.