From a85a04b70e7f6731f818d1ff3748c80b5fbb3463 Mon Sep 17 00:00:00 2001
From: Isabelle Maluza <isamaluza30@gmail.com>
Date: Mon, 10 Nov 2025 18:54:19 -0300
Subject: [PATCH] Add links for loops_free functions

---
 .../examples/custom/links/loops_free.v        | 46 +++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 CoqOfRust/examples/default/examples/custom/links/loops_free.v

diff --git a/CoqOfRust/examples/default/examples/custom/links/loops_free.v b/CoqOfRust/examples/default/examples/custom/links/loops_free.v
new file mode 100644
index 000000000..428bdf823
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/custom/links/loops_free.v
@@ -0,0 +1,46 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import examples.default.examples.custom.loops_free.
+
+Instance run_max2 (a b : U32.t) : Run.Trait max2 [] [] [φ a; φ b] U32.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+Instance run_abs_i32 (x : I32.t) : Run.Trait abs_i32 [] [] [φ x] I32.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+Instance run_bool_and (a b : Bool.t) : Run.Trait bool_and [] [] [φ a; φ b] Bool.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+Instance run_get_or_zero (xs : Array.t U32.t 4) (i : Usize.t) :
+  Run.Trait get_or_zero [] [] [φ xs; φ i] U32.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+Instance run_eq2 (a b : Array.t U32.t 2) : Run.Trait eq2 [] [] [φ a; φ b] Bool.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+Instance run_eq_pair (x y : Prod.t U32.t U32.t) : Run.Trait eq_pair [] [] [φ x; φ y] Bool.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+Instance run_min3 (a b c : U32.t) : Run.Trait min3 [] [] [φ a; φ b; φ c] U32.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.