diff --git a/clang/hvm4.c b/clang/hvm4.c
index 65432a5..f1f12ee 100644
--- a/clang/hvm4.c
+++ b/clang/hvm4.c
@@ -92,6 +92,7 @@ typedef struct {
 #define MOV 47  // Mov(v, b): move binding
 #define GOT 48  // Got(n): linked mov variable
 
+
 // LAM Ext Flags
 // =============
 #define LAM_ERA_MASK 0x800000  // binder unused in lambda body
@@ -223,6 +224,7 @@ static u32 FRESH = 1;
 #include "wnf/tid.c"
 
 static int   DEBUG = 0;
+static int   SAFE_MOV  = 1;
 
 // Nick Alphabet
 // =============
@@ -321,6 +323,17 @@ static int    PARSE_FORK_SIDE = -1;      // -1 = off, 0 = left branch (DP0), 1 =
 #include "term/new/num.c"
 #include "term/clone.c"
 
+fn void safe_mov_init_from_env(void) {
+  const char *val = getenv("HVM4_SAFE_MOV");
+  if (val != NULL && val[0] != '\0') {
+    if (val[0] == '0' && val[1] == '\0') {
+      SAFE_MOV = 0;
+    } else {
+      SAFE_MOV = 1;
+    }
+  }
+}
+
 // Heap Substitution
 // =================
 
@@ -421,9 +434,11 @@ static int    PARSE_FORK_SIDE = -1;      // -1 = off, 0 = left branch (DP0), 1 =
 #include "wnf/app_mat_ctr.c"
 #include "wnf/mat_inc.c"
 #include "wnf/dup_nam.c"
+#include "wnf/dup_got.c"
 #include "wnf/dup_dry.c"
 #include "wnf/dup_red.c"
 #include "wnf/dup_lam.c"
+#include "wnf/dup_mov.c"
 #include "wnf/dup_sup.c"
 #include "wnf/dup_nod.c"
 #include "wnf/mov_nam.c"
diff --git a/clang/main.c b/clang/main.c
index b2a6b56..212ebb1 100644
--- a/clang/main.c
+++ b/clang/main.c
@@ -109,6 +109,7 @@ int main(int argc, char **argv) {
 
   // Set debug mode
   DEBUG = opts.debug;
+  safe_mov_init_from_env();
 
   // Parse prelude
   PState ps = {
diff --git a/clang/parse/term/mov.c b/clang/parse/term/mov.c
index afc705c..c0fd735 100644
--- a/clang/parse/term/mov.c
+++ b/clang/parse/term/mov.c
@@ -1,5 +1,93 @@
 fn Term parse_term(PState *s, u32 depth);
 
+fn u32 mov_region_count_go(u64 loc, u32 lvl, u8 tgt, u32 ext, int *viol);
+fn void mov_rebind_bjm_to_bjv_go(u64 loc, u32 lvl);
+fn Term mov_rebind_bjm_to_bjv_term(Term t, u32 lvl);
+
+fn u32 mov_region_count_term(Term t, u32 lvl, u8 tgt, u32 ext, int *viol) {
+  if (*viol) {
+    return 0;
+  }
+  u8  tg = term_tag(t);
+  u32 vl = term_val(t);
+
+  if (tg == tgt && vl == lvl && (tgt == BJV || term_ext(t) == ext)) {
+    return 1;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return 0;
+  }
+
+  if (tg == LAM) {
+    u32 cnt = mov_region_count_go(vl, lvl, tgt, ext, viol);
+    if (cnt > 1) {
+      *viol = 1;
+    }
+    return 0;
+  }
+
+  u32 sum = 0;
+  for (u32 i = 0; i < ari; i++) {
+    sum += mov_region_count_go(vl + i, lvl, tgt, ext, viol);
+  }
+  return sum;
+}
+
+fn u32 mov_region_count_go(u64 loc, u32 lvl, u8 tgt, u32 ext, int *viol) {
+  return mov_region_count_term(HEAP[loc], lvl, tgt, ext, viol);
+}
+
+fn int mov_region_violates(Term body, u32 lvl, u8 tgt, u32 ext) {
+  int viol = 0;
+  u32 cnt = mov_region_count_term(body, lvl, tgt, ext, &viol);
+  return viol || cnt > 1;
+}
+
+fn void mov_rebind_bjm_to_bjv_go(u64 loc, u32 lvl) {
+  Term t = HEAP[loc];
+  u8  tg = term_tag(t);
+  u32 vl = term_val(t);
+  u8  sub = term_sub_get(t);
+
+  if (tg == BJM && vl == lvl) {
+    Term v = term_new(0, BJV, 0, vl);
+    HEAP[loc] = sub ? term_sub_set(v, 1) : v;
+    return;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return;
+  }
+
+  for (u32 i = 0; i < ari; i++) {
+    mov_rebind_bjm_to_bjv_go(vl + i, lvl);
+  }
+}
+
+fn Term mov_rebind_bjm_to_bjv_term(Term t, u32 lvl) {
+  u8  tg = term_tag(t);
+  u32 vl = term_val(t);
+  u8  sub = term_sub_get(t);
+
+  if (tg == BJM && vl == lvl) {
+    Term v = term_new(0, BJV, 0, vl);
+    return sub ? term_sub_set(v, 1) : v;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return t;
+  }
+
+  for (u32 i = 0; i < ari; i++) {
+    mov_rebind_bjm_to_bjv_go(vl + i, lvl);
+  }
+  return t;
+}
+
 fn Term parse_term_mov(PState *s, u32 depth) {
   parse_skip(s);
   u32 nam = parse_name(s);
@@ -11,9 +99,24 @@ fn Term parse_term_mov(PState *s, u32 depth) {
   parse_skip(s);
   parse_bind_push(nam, depth, 0, PBIND_MOV, 0);
   Term body = parse_term(s, depth + 1);
+  u32 uses = parse_bind_get_uses();
   parse_bind_pop();
+  u32 lvl = depth + 1;
+  int viol = mov_region_violates(body, lvl, BJM, 0);
+  if (viol) {
+    body = mov_rebind_bjm_to_bjv_term(body, lvl);
+    body = parse_auto_dup(body, lvl, lvl, BJV, 0);
+    u64 lam_loc = heap_alloc(1);
+    HEAP[lam_loc] = body;
+    Term lam = term_new(0, LAM, lvl, lam_loc);
+    return term_new_app(lam, val);
+  }
   u64 loc = heap_alloc(2);
   HEAP[loc + 0] = val;
   HEAP[loc + 1] = body;
+  if (uses > 2) {
+    body = parse_auto_dup(body, lvl, lvl, BJM, 0);
+    HEAP[loc + 1] = body;
+  }
   return term_new(0, MOV, 0, loc);
 }
diff --git a/clang/wnf/_.c b/clang/wnf/_.c
index e3ae06f..5d5a5d0 100644
--- a/clang/wnf/_.c
+++ b/clang/wnf/_.c
@@ -639,6 +639,14 @@ __attribute__((hot)) fn Term wnf(Term term) {
               whnf = wnf_dup_lam(lab, loc, side, whnf);
               continue;
             }
+            case MOV: {
+              whnf = wnf_dup_mov(lab, loc, side, whnf);
+              continue;
+            }
+            case GOT: {
+              whnf = wnf_dup_got(lab, loc, side, whnf);
+              continue;
+            }
             case SUP: {
               next = wnf_dup_sup(lab, loc, side, whnf);
               goto enter;
@@ -708,6 +716,7 @@ __attribute__((hot)) fn Term wnf(Term term) {
               next = wnf_mov_sup(loc, whnf);
               goto enter;
             }
+            case VAR:
             case ERA:
             case ANY:
             case NUM: {
diff --git a/clang/wnf/app_lam.c b/clang/wnf/app_lam.c
index 27a0483..044b02f 100644
--- a/clang/wnf/app_lam.c
+++ b/clang/wnf/app_lam.c
@@ -1,7 +1,3 @@
-// (λx.f a)
-// -------- APP-LAM
-// x ← a
-// f
 fn Term wnf_app_lam(Term lam, Term arg) {
   ITRS++;
   u32  loc     = term_val(lam);
diff --git a/clang/wnf/dup_got.c b/clang/wnf/dup_got.c
new file mode 100644
index 0000000..fc144c2
--- /dev/null
+++ b/clang/wnf/dup_got.c
@@ -0,0 +1,21 @@
+// ! X &L = x
+// --------- DUP-GOT
+// ! A &L = v
+// X₀ ← A₀
+// X₁ ← A₁
+fn Term wnf_dup_got(u32 lab, u32 loc, u8 side, Term got) {
+  ITRS++;
+  u32  got_loc = term_val(got);
+  u32  got_ext = term_ext(got);
+  Term val     = heap_read(got_loc);
+  Copy V       = term_clone(lab, val);
+
+  u64  loc0 = heap_alloc(1);
+  u64  loc1 = heap_alloc(1);
+  heap_write(loc0, V.k0);
+  heap_write(loc1, V.k1);
+
+  Term g0 = term_new(0, GOT, got_ext, (u32)loc0);
+  Term g1 = term_new(0, GOT, got_ext, (u32)loc1);
+  return heap_subst_cop(side, loc, g0, g1);
+}
diff --git a/clang/wnf/dup_mov.c b/clang/wnf/dup_mov.c
new file mode 100644
index 0000000..fbc4da8
--- /dev/null
+++ b/clang/wnf/dup_mov.c
@@ -0,0 +1,55 @@
+// ! X &L = % Y = v; b
+// -------------------- DUP-MOV
+// ! A &L = v
+// X₀ ← % Y0 = A₀; b[Y:=Y0]
+// X₁ ← % Y1 = A₁; b[Y:=Y1]
+fn Term mov_clone_rebind_got(Term t, u32 old_loc, u32 new_loc) {
+  u8  tg  = term_tag(t);
+  u32 vl  = term_val(t);
+  u32 ext = term_ext(t);
+  u8  sub = term_sub_get(t);
+
+  if (tg == GOT && vl == old_loc) {
+    Term v = term_new_got(new_loc);
+    return sub ? term_sub_set(v, 1) : v;
+  }
+
+  u32 ari = term_arity(t);
+  if (ari == 0) {
+    return t;
+  }
+
+  u64 loc = heap_alloc(ari);
+  for (u32 i = 0; i < ari; i++) {
+    Term child = heap_read(vl + i);
+    Term repl  = mov_clone_rebind_got(child, old_loc, new_loc);
+    heap_write(loc + i, repl);
+  }
+
+  Term res = term_new(0, tg, ext, (u32)loc);
+  return sub ? term_sub_set(res, 1) : res;
+}
+
+fn Term wnf_dup_mov(u32 lab, u32 loc, u8 side, Term mov) {
+  ITRS++;
+  u32  mov_loc = term_val(mov);
+  u32  mov_ext = term_ext(mov);
+  Term val     = heap_read(mov_loc + 0);
+  Term bod     = heap_read(mov_loc + 1);
+
+  Copy V = term_clone(lab, val);
+
+  u64  loc0 = heap_alloc(2);
+  u64  loc1 = heap_alloc(2);
+  Term bod0 = mov_clone_rebind_got(bod, mov_loc, (u32)loc0);
+  Term bod1 = mov_clone_rebind_got(bod, mov_loc, (u32)loc1);
+
+  heap_write(loc0 + 0, V.k0);
+  heap_write(loc0 + 1, bod0);
+  heap_write(loc1 + 0, V.k1);
+  heap_write(loc1 + 1, bod1);
+
+  Term m0 = term_new(0, MOV, mov_ext, (u32)loc0);
+  Term m1 = term_new(0, MOV, mov_ext, (u32)loc1);
+  return heap_subst_cop(side, loc, m0, m1);
+}
diff --git a/clang/wnf/mov_lam.c b/clang/wnf/mov_lam.c
index a43144c..9d47db8 100644
--- a/clang/wnf/mov_lam.c
+++ b/clang/wnf/mov_lam.c
@@ -8,13 +8,15 @@ fn Term wnf_mov_lam(u32 loc, Term lam) {
   u32  lam_ext = term_ext(lam);
   Term bod     = heap_read(lam_loc);
 
-  u64  base    = heap_alloc(2);
-  u32  g_loc   = (u32)base;
-  u32  x_loc   = g_loc + 1;
+  u64 base  = heap_alloc(2);
+  u32 g_loc = (u32)base;
+  u32 x_loc = g_loc + 1;
   heap_write(g_loc, bod);
   heap_write(x_loc, term_new_got(g_loc));
   heap_subst_var(lam_loc, term_new(0, VAR, 0, x_loc));
-  Term res     = term_new(0, LAM, lam_ext, x_loc);
-  heap_subst_var(loc, res);
+  Term res = term_new(0, LAM, lam_ext, x_loc);
+  if (!SAFE_MOV || (lam_ext & LAM_ERA_MASK)) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }
diff --git a/clang/wnf/mov_nod.c b/clang/wnf/mov_nod.c
index 8da97a5..d22000c 100644
--- a/clang/wnf/mov_nod.c
+++ b/clang/wnf/mov_nod.c
@@ -8,7 +8,9 @@ fn Term wnf_mov_nod(u32 loc, Term term) {
   ITRS++;
   u32 ari = term_arity(term);
   if (ari == 0) {
-    heap_subst_var(loc, term);
+    if (!SAFE_MOV) {
+      heap_subst_var(loc, term);
+    }
     return term;
   }
   u32  t_loc = term_val(term);
@@ -22,6 +24,8 @@ fn Term wnf_mov_nod(u32 loc, Term term) {
     heap_write(nod_loc + i, term_new_got(got_loc + i));
   }
   Term res = term_new(0, t_tag, t_ext, nod_loc);
-  heap_subst_var(loc, res);
+  if (!SAFE_MOV) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }
diff --git a/clang/wnf/mov_red.c b/clang/wnf/mov_red.c
index 17d9574..3eea0af 100644
--- a/clang/wnf/mov_red.c
+++ b/clang/wnf/mov_red.c
@@ -13,6 +13,8 @@ fn Term wnf_mov_red(u32 loc, Term red) {
   Term f     = term_new_got(at + 0);
   Term g     = term_new_got(at + 1);
   Term res   = term_new_red_at(at + 2, f, g);
-  heap_subst_var(loc, res);
+  if (!SAFE_MOV) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }
diff --git a/clang/wnf/mov_sup.c b/clang/wnf/mov_sup.c
index 160b28a..a6c1eb4 100644
--- a/clang/wnf/mov_sup.c
+++ b/clang/wnf/mov_sup.c
@@ -14,6 +14,8 @@ fn Term wnf_mov_sup(u32 loc, Term sup) {
   Term a     = term_new_got(at + 0);
   Term b     = term_new_got(at + 1);
   Term res   = term_new_sup_at(at + 2, s_lab, a, b);
-  heap_subst_var(loc, res);
+  if (!SAFE_MOV) {
+    heap_subst_var(loc, res);
+  }
   return res;
 }
diff --git a/test/dup_basic.hvm4 b/test/dup_basic.hvm4
new file mode 100644
index 0000000..91b5149
--- /dev/null
+++ b/test/dup_basic.hvm4
@@ -0,0 +1,4 @@
+@main =
+  !x&A = 1;
+  x₀
+//1
diff --git a/test/mov_bounty.hvm4 b/test/mov_bounty.hvm4
new file mode 100644
index 0000000..4291a8f
--- /dev/null
+++ b/test/mov_bounty.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_B(@I(@I(@I(@I(@E)))))
+  @view(@rep(@bin(16n,512), ins, @O(@O(@O(@O(@O(@O(@E))))))))
+//#O{#O{#O{#O{#I{#O{#E{}}}}}}}
diff --git a/test/mov_bounty_dup.hvm4 b/test/mov_bounty_dup.hvm4
new file mode 100644
index 0000000..86a0487
--- /dev/null
+++ b/test/mov_bounty_dup.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_A(@I(@I(@I(@I(@E)))))
+  @view(@rep(@bin(16n,512), ins, @O(@O(@O(@O(@O(@O(@E))))))))
+//#O{#O{#O{#O{#I{#O{#E{}}}}}}}
diff --git a/test/mov_bounty_f3.hvm4 b/test/mov_bounty_f3.hvm4
new file mode 100644
index 0000000..44e3d64
--- /dev/null
+++ b/test/mov_bounty_f3.hvm4
@@ -0,0 +1,40 @@
+// Minimal repro: MOV insert used 3x via cloned lambda
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// MOV version
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+@main =
+  ! ins = @insert_B(@I(@E))
+  @view((λ&f. f(f(f(@O(@E)))))(ins))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_f3_dup.hvm4 b/test/mov_bounty_f3_dup.hvm4
new file mode 100644
index 0000000..6ff5ee2
--- /dev/null
+++ b/test/mov_bounty_f3_dup.hvm4
@@ -0,0 +1,38 @@
+// Minimal repro: DUP insert used 3x via cloned lambda
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// DUP version
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert_A(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+@main =
+  ! ins = @insert_A(@I(@E))
+  @view((λ&f. f(f(f(@O(@E)))))(ins))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_min.hvm4 b/test/mov_bounty_min.hvm4
new file mode 100644
index 0000000..baa7d68
--- /dev/null
+++ b/test/mov_bounty_min.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_B(@I(@E))
+  @view(@rep(@bin(2n,3), ins, @O(@E)))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_min_dup.hvm4 b/test/mov_bounty_min_dup.hvm4
new file mode 100644
index 0000000..4da60a6
--- /dev/null
+++ b/test/mov_bounty_min_dup.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_A(@I(@E))
+  @view(@rep(@bin(2n,3), ins, @O(@E)))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_small.hvm4 b/test/mov_bounty_small.hvm4
new file mode 100644
index 0000000..f6b5be9
--- /dev/null
+++ b/test/mov_bounty_small.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_B(@I(@E))
+  @view(@rep(@bin(4n,6), ins, @O(@O(@E))))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_small_dup.hvm4 b/test/mov_bounty_small_dup.hvm4
new file mode 100644
index 0000000..964673a
--- /dev/null
+++ b/test/mov_bounty_small_dup.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_A(@I(@E))
+  @view(@rep(@bin(4n,6), ins, @O(@O(@E))))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_tiny.hvm4 b/test/mov_bounty_tiny.hvm4
new file mode 100644
index 0000000..165947e
--- /dev/null
+++ b/test/mov_bounty_tiny.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_B(@I(@E))
+  @view(@rep(@bin(2n,2), ins, @O(@E)))
+//#O{#I{#E{}}}
diff --git a/test/mov_bounty_tiny_dup.hvm4 b/test/mov_bounty_tiny_dup.hvm4
new file mode 100644
index 0000000..0e3276e
--- /dev/null
+++ b/test/mov_bounty_tiny_dup.hvm4
@@ -0,0 +1,89 @@
+// PROBLEM: in the code below:
+// 1. both versions of @insert should output the same result with -C1
+// 2. the second version should take <50k interactions to halt
+// yet, on HVM4's current MOV node implementation, the outputs mismatch. why?
+// your goal is to find out, and fix HVM4 so that both points above hold.
+// $10k bounty: https://x.com/VictorTaelin/status/2006818916211834900
+
+@tail = λ{[]:[];<>:λa.λb.b}
+
+// List ::= Cons List | Succ List | Nil
+@C = λt. λc. λs. λn. c(t)
+@S = λp. λc. λs. λn. s(p)
+@N =     λc. λs. λn. n
+
+// Bits ::= O Bits | I Bits | E
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+
+// ℕ → U32 → Bin -- converts a U32 to a Bin with a given size
+@bin = λ{
+  0n: λn. λo.λi.λe.e;
+  1n+: λ&l. λ&n. (λ{
+    0: λo.λi.λe.o(@bin(l, n/2))
+    1: λo.λi.λe.i(@bin(l, n/2))
+  })(n % 2)
+}
+
+// Bin → (P → P) → P → P -- applies a function N times to an argument
+@rep = λxs.
+  ! O = λp.λ&f.λx.@rep(p,λk.f(f(k)),x)
+  ! I = λp.λ&f.λx.@rep(p,λk.f(f(k)),f(x))
+  ! E = λf.λx.x
+  xs(O, I, E)
+
+// [1,2,3] ::= Cons (Succ (Cons (Succ (Succ (Cons (Succ (Succ (Succ Nil))))))))
+@to_nats_go = λxs. λn.
+  ! C = λt. λn. n <> @to_nats_go(t, 0n)
+  ! S = λp. λn. @to_nats_go(p, 1n+n)
+  ! N = λn. [n]
+  xs(C, S, N, n)
+
+@to_nats = λxs.
+  @tail(@to_nats_go(xs,0n))
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+// control: using DUP nodes (this works)
+@insert_A = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_A(p, xs))
+    ! I = λxs. i(@insert_A(p, xs))
+    ! E = o(@insert(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// problem: using MOV nodes (this fails)
+@insert_B = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_B(p, xs))
+    ! I = λxs. i(@insert_B(p, xs))
+    ! E = f(@insert_B(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+// this should produce the same output with either @insert fns above when
+// running it with `HVM4 -C1`, but, currently, the outputs mismatch...
+@main =
+  ! ins = @insert_A(@I(@E))
+  @view(@rep(@bin(2n,2), ins, @O(@E)))
+//#O{#I{#E{}}}
diff --git a/test/mov_dup_func.hvm4 b/test/mov_dup_func.hvm4
new file mode 100644
index 0000000..0a587bd
--- /dev/null
+++ b/test/mov_dup_func.hvm4
@@ -0,0 +1,6 @@
+@f = λ&o. % g = o; λx. g(x)
+
+@main =
+  !x&A = @f(λz. z);
+  (x₀(1) + x₁(2))
+//3
diff --git a/test/mov_dup_nested.hvm4 b/test/mov_dup_nested.hvm4
new file mode 100644
index 0000000..6e51c87
--- /dev/null
+++ b/test/mov_dup_nested.hvm4
@@ -0,0 +1,6 @@
+@f = λ&o. % g = o; λx. g(x)
+
+@main =
+  !h&A = @f(λz. z);
+  h₀(h₁(1))
+//1
diff --git a/test/mov_dup_test.hvm4 b/test/mov_dup_test.hvm4
new file mode 100644
index 0000000..168f430
--- /dev/null
+++ b/test/mov_dup_test.hvm4
@@ -0,0 +1,4 @@
+@main =
+  !x&A = (%f = 1; f);
+  (x₀ + x₁)
+//2
diff --git a/test/mov_erase_test.hvm4 b/test/mov_erase_test.hvm4
new file mode 100644
index 0000000..521e9db
--- /dev/null
+++ b/test/mov_erase_test.hvm4
@@ -0,0 +1,5 @@
+@t = λx. λy. x
+
+@main =
+  (λo. %f = o; @t(f, f)) (#I{#E{}})
+//#I{#E{}}
diff --git a/test/mov_erase_test_dup.hvm4 b/test/mov_erase_test_dup.hvm4
new file mode 100644
index 0000000..394741a
--- /dev/null
+++ b/test/mov_erase_test_dup.hvm4
@@ -0,0 +1,5 @@
+@t = λx. λy. x
+
+@main =
+  (λo. !f&A = o; @t(f₀, f₁)) (#I{#E{}})
+//#I{#E{}}
diff --git a/test/mov_lam_bench.hvm4 b/test/mov_lam_bench.hvm4
new file mode 100644
index 0000000..1f783ff
--- /dev/null
+++ b/test/mov_lam_bench.hvm4
@@ -0,0 +1,8 @@
+@apply4 = λ&g. λx. g(g(g(g(x))))
+@apply16 = λ&g. λx. @apply4(g, @apply4(g, @apply4(g, @apply4(g, x))))
+@apply64 = λ&g. λx. @apply16(g, @apply16(g, @apply16(g, @apply16(g, x))))
+
+@main =
+  % f = λx.x;
+  @apply64(λy. f(f(y)), 0n)
+//0n
diff --git a/test/mov_lam_bench_dup.hvm4 b/test/mov_lam_bench_dup.hvm4
new file mode 100644
index 0000000..011a5ad
--- /dev/null
+++ b/test/mov_lam_bench_dup.hvm4
@@ -0,0 +1,8 @@
+@apply4 = λ&g. λx. g(g(g(g(x))))
+@apply16 = λ&g. λx. @apply4(g, @apply4(g, @apply4(g, @apply4(g, x))))
+@apply64 = λ&g. λx. @apply16(g, @apply16(g, @apply16(g, @apply16(g, x))))
+
+@main =
+  ! &f = λx.x;
+  @apply64(λy. f(f(y)), 0n)
+//0n
diff --git a/test/mov_lam_dupvar.hvm4 b/test/mov_lam_dupvar.hvm4
new file mode 100644
index 0000000..faa3fc6
--- /dev/null
+++ b/test/mov_lam_dupvar.hvm4
@@ -0,0 +1,4 @@
+@main =
+  % f = λ&x. (x + x)
+  f(1)
+//2
diff --git a/test/mov_lam_erase_bench.hvm4 b/test/mov_lam_erase_bench.hvm4
new file mode 100644
index 0000000..96e5aa9
--- /dev/null
+++ b/test/mov_lam_erase_bench.hvm4
@@ -0,0 +1,8 @@
+@apply4 = λ&g. λx. g(g(g(g(x))))
+@apply16 = λ&g. λx. @apply4(g, @apply4(g, @apply4(g, @apply4(g, x))))
+@apply64 = λ&g. λx. @apply16(g, @apply16(g, @apply16(g, @apply16(g, x))))
+
+@main =
+  % f = λx.0n;
+  @apply64(λy. f(f(y)), 0n)
+//0n
diff --git a/test/mov_lam_erase_bench_dup.hvm4 b/test/mov_lam_erase_bench_dup.hvm4
new file mode 100644
index 0000000..d7655af
--- /dev/null
+++ b/test/mov_lam_erase_bench_dup.hvm4
@@ -0,0 +1,8 @@
+@apply4 = λ&g. λx. g(g(g(g(x))))
+@apply16 = λ&g. λx. @apply4(g, @apply4(g, @apply4(g, @apply4(g, x))))
+@apply64 = λ&g. λx. @apply16(g, @apply16(g, @apply16(g, @apply16(g, x))))
+
+@main =
+  ! &f = λx.0n;
+  @apply64(λy. f(f(y)), 0n)
+//0n
diff --git a/test/mov_lam_test.hvm4 b/test/mov_lam_test.hvm4
new file mode 100644
index 0000000..bbc1e3f
--- /dev/null
+++ b/test/mov_lam_test.hvm4
@@ -0,0 +1,4 @@
+@main =
+  % f = λx. x
+  f(1)
+//1
diff --git a/test/new_issue.hvm4 b/test/new_issue.hvm4
new file mode 100644
index 0000000..b8e9578
--- /dev/null
+++ b/test/new_issue.hvm4
@@ -0,0 +1,54 @@
+@O = λp. λo. λi. λe. o(p)
+@I = λp. λo. λi. λe. i(p)
+@E =     λo. λi. λe. e
+@N =     λc. λs. λn. n
+
+@view = λxs.
+  ! O = λp. #O{@view(p)}
+  ! I = λp. #I{@view(p)}
+  ! E = #E
+  xs(O, I, E)
+
+@rep2 = λ&f. λx. f(f(x))
+@rep3 = λ&f. λx. f(f(f(x)))
+
+@insert_mov = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    % f = o
+    ! O = λxs. f(@insert_mov(p, xs))
+    ! I = λxs. i(@insert_mov(p, xs))
+    ! E = f(@insert_mov(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    % k = i
+    ! O = λxs. k(xs)
+    ! I = λxs. k(xs)
+    ! E = k(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+@insert_dup = λn.
+  ! O = &{}
+  ! I = (λ&p. λxs. λ&o. λi. λe.
+    ! O = λxs. o(@insert_dup(p, xs))
+    ! I = λxs. i(@insert_dup(p, xs))
+    ! E = o(@insert_dup(p, @N))
+    xs(O, I, E))
+  ! E = λxs. λo. λ&i. λe.
+    ! O = λxs. i(xs)
+    ! I = λxs. i(xs)
+    ! E = i(@N)
+    xs(O, I, E)
+  n(O, I, E)
+
+@ins_mov = @insert_mov(@I(@I(@E)))
+@ins_dup = @insert_dup(@I(@I(@E)))
+
+@main = #T{
+  @view(@rep2(@ins_mov, @O(@E))),  // OK:   #O{#O{#I{#E{}}}}
+  @view(@rep3(@ins_mov, @O(@E))),  // FAIL in unsafe mode
+  @view(@rep2(@ins_dup, @O(@E))),  // OK:   #O{#O{#I{#E{}}}}
+  @view(@rep3(@ins_dup, @O(@E)))   // OK:   #O{#O{#I{#E{}}}}
+}
+//#T{#O{#O{#I{#E{}}}},#O{#O{#I{#E{}}}},#O{#O{#I{#E{}}}},#O{#O{#I{#E{}}}}}
diff --git a/test/payor_new.hvm4 b/test/payor_new.hvm4
new file mode 100644
index 0000000..b19be17
--- /dev/null
+++ b/test/payor_new.hvm4
@@ -0,0 +1,16 @@
+@id = λa. a
+@fst = λa. λb. a
+@snd = λa. λb. b
+
+@make = λss. λf.
+  % s = ss
+  f(s, s)
+
+@movdup = λs. λf.
+  !& x = @make(s)
+  f(x(@fst), x(@snd))
+
+@twice = λf. λa. @movdup(f, λf0. λf1. f0(f1(a)))
+
+@main = @twice(@twice, @id)
+//λa.a
diff --git a/test/payor_new_dup.hvm4 b/test/payor_new_dup.hvm4
new file mode 100644
index 0000000..e483ce6
--- /dev/null
+++ b/test/payor_new_dup.hvm4
@@ -0,0 +1,16 @@
+@id = λa. a
+@fst = λa. λb. a
+@snd = λa. λb. b
+
+@make = λss. λf.
+  !& s = ss
+  f(s, s)
+
+@movdup = λs. λf.
+  !& x = @make(s)
+  f(x(@fst), x(@snd))
+
+@twice = λf. λa. @movdup(f, λf0. λf1. f0(f1(a)))
+
+@main = @twice(@twice, @id)
+//λa.a
diff --git a/test/payor_repro.hvm4 b/test/payor_repro.hvm4
new file mode 100644
index 0000000..a940c57
--- /dev/null
+++ b/test/payor_repro.hvm4
@@ -0,0 +1,6 @@
+// Payor repro (minimal). Uses MOV + DUP with label L.
+@main =
+  % G = λy.y;
+  ! F &L = λx. x(G, G);
+  F₀(λa.λb.a)(F₁(λc.λd.d))
+//λa.a
diff --git a/test/payor_repro_dup.hvm4 b/test/payor_repro_dup.hvm4
new file mode 100644
index 0000000..720e348
--- /dev/null
+++ b/test/payor_repro_dup.hvm4
@@ -0,0 +1,6 @@
+// Payor repro: explicit DUP for G
+@main =
+  ! G &L = λy.y;
+  ! F &L = λx. x(G₀, G₁);
+  F₀(λa.λb.a)(F₁(λc.λd.d))
+//λa.a