feat: retire RC from the emitter and the format — .wob v4 (7b Phase 3b)

The compiler no longer emits reference-counting ops anywhere, and the format
reserves them. With Phase 3a's collector this completes the runtime half of
iteration 7b: spec success criteria 3 (no RC ops in any image, opcodes
reserved) and 6 (corpus ASan-clean) are met — `just oop-accept` is fully green.

- owner.ml: the rc machinery is deleted outright — rc_site/rc_op types, the
  rcs table, fn_rcs/rc_groups/rc_escaped, record_rc, release_gc, gc_escape,
  resolve_rc, and the clobber rule (its only consumer was elision). The
  `push`-of-a-gc-value RC_INC special case is gone (the bug class cannot recur
  without RC). Drop tables (owned + LGc kinds) are untouched — the gc mask is
  what feeds the collector's root maps.
- emit.ml: emit_rc, the v_rc view, the escape-acquire anchor, and every
  caller deleted; assignment displacing a traced value emits nothing (the VM's
  store barrier owns it); scope-ended LGc handles clear their gc-mask bit so
  root maps stay precise.
- .wob v4: WOB_VERSION 3 -> 4 in wob.h + emit.ml + disasm.ml + the runner's
  loader battery; opcodes 27-28 removed from the enum/jump table/interpreter
  and REJECTED by the loader like any unknown opcode.
- dump.ml: the == RC == owner-dump section is gone; 6 goldens re-blessed
  (owner dumps lose the section, elision.wo's bc dump loses its RC ops).
- runner.ml: rc-table/ELIDED assertions deleted; the elision test now asserts
  the WHOLE image contains no RC op; the table-contract sweep asserts rc ops
  never appear.
- test_unwind.c: the rc-opcodes test becomes two — the loader rejects reserved
  opcode 27, and an abandoned traced instance is freed by rt_destroy
  (ASan-proven).

Verified: woc-test 540/0 + test_diag 14/0; runtime test + test-iso all suites
ASan/UBSan (test_unwind 12/0); cli_smoke; oop-e2e 79/0 (v4 images end to end);
employee 8/0; log-watcher 7/0; ring runs + reclaimed (freed=3) with zero RC
ops in its image; `just oop-accept` ALL CRITERIA MET.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

compiler/src/disasm.ml

@@ -140,8 +140,6 @@ let ins_str (i : int) (pc : int) : string =
   | 24 -> Printf.sprintf "BORROW_X  r%d" a
   | 25 -> Printf.sprintf "RELEASE_S r%d" a
   | 26 -> Printf.sprintf "RELEASE_X r%d" a
-  | 27 -> Printf.sprintf "RC_INC    r%d" a
-  | 28 -> Printf.sprintf "RC_DEC    r%d" a
   | 29 ->
     if c = 4 || c = 9 then Printf.sprintf "BUILTIN   r%d, kinds=0x%02x, %s" a b (builtin_name c)
     else Printf.sprintf "BUILTIN   r%d, r%d, %s" a b (builtin_name c)
@@ -164,7 +162,7 @@ let dump (img : string) : string =
   let line fmt = Buffer.add_string out (fmt ^ "\n") in
   if u32 img 0 <> magic then raise (Bad "bad magic");
   let ver = u32 img 4 in
-  if ver <> 3 then raise (Bad (Printf.sprintf "unsupported version %d" ver));
+  if ver <> 4 then raise (Bad (Printf.sprintf "unsupported version %d" ver));
   let coff = u32 img 8 and ccnt = u32 img 12 in
   let koff = u32 img 16 and kcnt = u32 img 20 in
   let ioff = u32 img 24 and icnt = u32 img 28 in

compiler/src/dump.ml

@@ -446,11 +446,6 @@ let dump_ast (prog : Ast.program) : string =
                       block; source order is only here to keep the
                       rendering deterministic.
 
-     == RC ==       "LINE:COL ACQUIRE|RELEASE <place> ELIDED|KEPT" for
-                      @gc reference counting. ELIDED marks a pair the
-                      emitter may skip because increment and decrement
-                      are provably balanced inside one scope.
-
      == RESIDUAL ==   "LINE:COL RESIDUAL <op> <place> vs <op> <place>" —
                       the sites static proof could not settle, so the
                       emitter wraps them in runtime borrow ops
@@ -523,12 +518,6 @@ let dump_owner (t : Owner.tables) : string =
     | Owner.DBreak -> Printf.sprintf "%s BREAK %s" pos (drop_items_str d.Owner.dr_items)
     | Owner.DContinue -> Printf.sprintf "%s CONTINUE %s" pos (drop_items_str d.Owner.dr_items)
   in
-  let rc_line (r : Owner.rc_site) =
-    Printf.sprintf "%s %s %s %s" (owner_pos_str r.Owner.rc_pos)
-      (match r.Owner.rc_op with Owner.RcAcquire -> "ACQUIRE" | Owner.RcRelease -> "RELEASE")
-      r.Owner.rc_place
-      (if r.Owner.rc_elided then "ELIDED" else "KEPT")
-  in
   let res_line (r : Owner.residual_site) =
     Printf.sprintf "%s RESIDUAL %s %s vs %s %s" (owner_pos_str r.Owner.rs_pos)
       (acc_kind_str r.Owner.rs_a_kind) r.Owner.rs_a (acc_kind_str r.Owner.rs_b_kind) r.Owner.rs_b
@@ -537,7 +526,6 @@ let dump_owner (t : Owner.tables) : string =
   let lines =
     section "== MOVES ==" (List.map move_line t.Owner.moves)
     @ section "== DROPS ==" (List.map drop_line t.Owner.drops)
-    @ section "== RC ==" (List.map rc_line t.Owner.rcs)
     @ section "== RESIDUAL ==" (List.map res_line t.Owner.residuals)
   in
   String.concat "\n" lines ^ "\n"

compiler/src/emit.ml

@@ -25,7 +25,6 @@
    Owner.tables            the four ownership tables, verbatim:
                              moves     -> which MOVEs are real transfers
                              drops     -> DROP placement + drop-table masks
-                             rcs       -> RC_INC / RC_DEC, minus ELIDED pairs
                              residuals -> the ONLY places borrow ops appear
 
    Where the drop map is synced is worth stating once: the owner table is
@@ -152,7 +151,7 @@ let stdlib_not_linked_code = Diag.emitter_prefix ^ "06"
    ============================================================ *)
 
 let wob_magic = 0x31424F57 (* "WOB1" read as an LE u32 *)
-let wob_version = 3 (* v3: v2 + per-class secondary-index metadata *)
+let wob_version = 4 (* v4 (iteration 7b): RC opcodes retired; gc mask = GC roots *)
 let wob_hdr_size = 44
 let wob_none = 0xFFFFFFFF
 let k_int = 0
@@ -187,8 +186,7 @@ let op_borrow_s = 23
 let op_borrow_x = 24
 let op_release_s = 25
 let op_release_x = 26
-let op_rc_inc = 27
+(* opcodes 27-28 (RC_INC/RC_DEC) retired in v4 — reserved, never emitted *)
-let op_rc_dec = 28
 let op_builtin = 29
 let op_db_stub = 30
 
@@ -567,7 +565,6 @@ type views = {
      This is how the emitter learns which locals the frame destroys
      without re-deriving owner.ml's own "holds" decision. *)
   v_holder : (int, Owner.local_kind) Hashtbl.t;
-  v_rc : (int, Owner.rc_site list) Hashtbl.t; (* by rc_node *)
   (* region node -> the region's position and its per-operand coalesced
      guards *)
   v_res : (int, Ast.pos * (int * Owner.acc_kind) list) Hashtbl.t;
@@ -585,7 +582,7 @@ let build_views (t : Owner.tables) : views =
     { v_move = Hashtbl.create 16; v_scope = Hashtbl.create 16; v_join = Hashtbl.create 16;
       v_return = Hashtbl.create 16; v_break = Hashtbl.create 16; v_continue = Hashtbl.create 16;
       v_overwrite = Hashtbl.create 16; v_mask = Hashtbl.create 16;
-      v_holder = Hashtbl.create 16; v_rc = Hashtbl.create 16; v_res = Hashtbl.create 16;
+      v_holder = Hashtbl.create 16; v_res = Hashtbl.create 16;
       v_res_used = Hashtbl.create 16 }
   in
   List.iter
@@ -606,11 +603,6 @@ let build_views (t : Owner.tables) : views =
       | Owner.DOverwrite -> Hashtbl.replace v.v_overwrite d.Owner.dr_node ()
       | Owner.DLiveMask -> Hashtbl.replace v.v_mask d.Owner.dr_node items)
     t.Owner.drops;
-  List.iter
-    (fun (r : Owner.rc_site) ->
-      let prev = try Hashtbl.find v.v_rc r.Owner.rc_node with Not_found -> [] in
-      Hashtbl.replace v.v_rc r.Owner.rc_node (prev @ [ r ]))
-    t.Owner.rcs;
   (* Guard coalescing, per dump.ml's normative note: one entry per
      (region, operand) with the strongest access kind, never one pair per
      table entry. AExcl outranks AShared; a move is never a residual
@@ -1235,9 +1227,10 @@ let emit_drops (p : pctx) (f : fstate) (items : Owner.drop_item list) : unit =
           put f (ins_abc op_drop r 0 0);
           mask_clear f r
         | Owner.LGc ->
-          (* a @gc handle's release is an rc site, never a DROP: the RC
+          (* a traced handle's death emits nothing — tracing owns the
-             table carries it (with its own ELIDED decision) *)
+             lifetime (7b). Clearing its gc-mask bit keeps the root maps
-          ()))
+             precise: a scope-ended handle must not pin garbage. *)
+          mask_clear f r))
     items
 
 let emit_scope_drops (p : pctx) (f : fstate) (v : views) ~(node : int) ~(label : string) : unit =
@@ -1258,37 +1251,6 @@ let emit_join_drops (p : pctx) (f : fstate) (v : views) ~(node : int) ~(label :
   | Some items -> emit_drops p f items
   | None -> ()
 
-(* RC sites, minus the ELIDED ones — the spec's zero-cost promise lives
-   here and in the residual-only borrow rule. `which` selects acquires or
-   releases; a return site carries both plus the returned value's own
-   escape increment, and acquires must precede releases or a balanced
-   pair could momentarily reach rc 0. *)
-let emit_rc (p : pctx) (f : fstate) (v : views) ~(node : int) ~(acquire : bool)
-    ?(groups : int list option) () : unit =
-  match Hashtbl.find_opt v.v_rc node with
-  | None -> ()
-  | Some sites ->
-    List.iter
-      (fun (r : Owner.rc_site) ->
-        let want = match r.Owner.rc_op with Owner.RcAcquire -> true | Owner.RcRelease -> false in
-        let in_scope =
-          match groups with None -> true | Some gs -> List.mem r.Owner.rc_group gs
-        in
-        if want = acquire && in_scope && not r.Owner.rc_elided then
-          let reg =
-            if r.Owner.rc_group >= 0 then Hashtbl.find_opt f.f_decl r.Owner.rc_group
-            else Hashtbl.find_opt f.f_node r.Owner.rc_node
-          in
-          match reg with
-          | Some g ->
-            put f (ins_abc (if acquire then op_rc_inc else op_rc_dec) g 0 0);
-            if not acquire then mask_clear f g
-          | None ->
-            err p ~code:unguardable_code ~file:f.f_file ~pos:r.Owner.rc_pos
-              ~message:
-                (Printf.sprintf "rc site for `%s` has no register in `%s`" r.Owner.rc_place f.f_fn))
-      sites
-
 (* The frame's drop map at a call / DB_STUB site. The owner table is
    authoritative here (it is taken after the call's own argument
    transfers, so a value moved in is the callee's responsibility); an
@@ -1827,16 +1789,6 @@ let rec emit_expr (p : pctx) (f : fstate) (v : views) ~(dst : int) ?expected (e
     put f (ins_abc op_db_stub 0 0 0)
   | Switch (subject, arms) -> emit_switch p f v e ~dst subject arms);
   Hashtbl.replace f.f_node e.id dst;
-  (* An escaping @gc value takes its increment right where the value
-     lands. owner.ml's gc_escape anchors that acquire on the *place
-     expression's* own node and gives it group -1 (never elidable), and
-     it fires for all four escapes alike: a constructor field, an
-     assignment into a field, a `take` argument, and a return. Emitting
-     it here — once, at the one place every expression passes through —
-     is what keeps all four in step; anchoring it per statement kind is
-     how the constructor-field case went missing. *)
-  emit_rc p f v ~node:e.id ~acquire:true ()
-
 (* An operand that only needs to *be* in some register: a place already
    living in one is used where it is, everything else lands in a fresh
    temporary. This is what keeps a proven method's disassembly free of
@@ -1861,7 +1813,6 @@ and emit_tail (p : pctx) (f : fstate) (v : views) (e : Ast.expr) : int =
   | Ident n when lookup_local f n <> None ->
     let r = match lookup_local f n with Some (r, _) -> r | None -> 0 in
     Hashtbl.replace f.f_node e.id r;
-    emit_rc p f v ~node:e.id ~acquire:true ();
     r
   | _ ->
     (* allocate (so the register counts towards the budget and the
@@ -2300,7 +2251,6 @@ and emit_switch ?(want_value = true) (p : pctx) (f : fstate) (v : views) (e : As
           | None -> ())
         | _ -> emit_stmt p f v last));
       emit_scope_drops p f v ~node:e.id ~label;
-      emit_rc p f v ~node:e.id ~acquire:false ~groups:(declared_since f saved_decls) ();
       f.f_nlocals <- saved_locals;
       f.f_env <- saved_env;
       f.f_declared <- saved_decls;
@@ -2400,7 +2350,6 @@ and emit_try (p : pctx) (f : fstate) (v : views) ~(dst : int) ?expected (e : Ast
       | None -> emit_expr p f v ~dst ve)
     | _ -> emit_stmt p f v last));
   emit_scope_drops p f v ~node:e.id ~label:"CATCH";
-  emit_rc p f v ~node:e.id ~acquire:false ~groups:(declared_since f saved_decls) ();
   f.f_nlocals <- saved_locals;
   f.f_env <- saved_env;
   f.f_declared <- saved_decls;
@@ -3560,8 +3509,7 @@ and emit_stmt_body (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) : unit =
     | None -> ());
     (match Hashtbl.find_opt v.v_holder s.s_id with
     | Some kind -> mask_set f kind r
-    | None -> ());
+    | None -> ())
-    emit_rc p f v ~node:s.s_id ~acquire:true ()
   | Assign { target; value } -> emit_assign p f v s target value
   | ExprStmt ({ kind = Ast.Switch (subj, arms); _ } as e) ->
     (* Task 4 fix round 1: the one place a switch's value is DISCARDED —
@@ -3577,7 +3525,6 @@ and emit_stmt_body (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) : unit =
     f.f_cur_line <- e.pos.line;
     emit_switch ~want_value:false p f v e ~dst:t subj arms;
     Hashtbl.replace f.f_node e.id t;
-    emit_rc p f v ~node:e.id ~acquire:true ();
     (match Hashtbl.find_opt v.v_move e.id with
     | Some place -> ( match lookup_local f place with Some (sr, _) -> mask_clear f sr | None -> ())
     | None -> ())
@@ -3616,17 +3563,9 @@ and emit_stmt_body (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) : unit =
 and emit_assign (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (target : Ast.expr)
     (value : Ast.expr) : unit =
   let overwrite = Hashtbl.mem v.v_overwrite s.s_id in
-  (* a @gc value the assignment displaces is released, not dropped: the
+  (* iteration 7b: a traced value an assignment displaces needs nothing —
-     RC table carries that RELEASE at the assignment's own node *)
+     tracing owns its lifetime (the VM's store barrier shades it while a
-  let releases =
+     mark is live). Only OVERWRITE (owned) entries lower to a drop. *)
-    match Hashtbl.find_opt v.v_rc s.s_id with
-    | None -> false
-    | Some sites ->
-      List.exists
-        (fun (r : Owner.rc_site) ->
-          r.Owner.rc_op = Owner.RcRelease && not r.Owner.rc_elided)
-        sites
-  in
   match target.kind with
   | Ident n -> (
     match lookup_local f n with
@@ -3635,7 +3574,7 @@ and emit_assign (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (target : Ast
         ~message:(Printf.sprintf "assignment to `%s`, which is not a local or parameter" n)
     | Some (r, ty) ->
       Hashtbl.replace f.f_node target.id r;
-      if overwrite || releases then begin
+      if overwrite then begin
         (* the replaced value dies here (the owner table's OVERWRITE or
            RELEASE entry); compute the new one into a temporary first so
            destroying the old one cannot destroy what is about to be
@@ -3649,14 +3588,8 @@ and emit_assign (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (target : Ast
            the source can live inside what is about to be dropped. *)
         copy_place_text p f t value;
         f.f_cur_line <- s.s_pos.line;
-        if overwrite then begin
+        put f (ins_abc op_drop r 0 0);
-          put f (ins_abc op_drop r 0 0);
+        mask_clear f r;
-          mask_clear f r
-        end;
-        if releases then begin
-          Hashtbl.replace f.f_node s.s_id r;
-          emit_rc p f v ~node:s.s_id ~acquire:false ()
-        end;
         put f (ins_abc op_move r t 0)
       end
       else begin
@@ -3715,18 +3648,15 @@ and emit_assign (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (target : Ast
             let b = emit_operand p f v base in
             Hashtbl.replace f.f_node target.id b;
             let idx = check_field_idx p f target.pos idx in
-            if overwrite || releases then begin
+            if overwrite then begin
-              (* SETF never auto-drops (format doc): the compiler emits
+              (* SETF never auto-drops (format doc): the compiler emits the
-                 the destruction of the field's previous value — a DROP
+                 destruction of the field's previous OWNED value. A traced
-                 for an owned field, an rc release for a @gc one *)
+                 old value needs nothing here — tracing owns its lifetime
+                 (the VM's SETF barrier shades it while a mark is live). *)
               let old = alloc_temp p f target.pos in
               f.f_cur_line <- s.s_pos.line;
               put f (ins_abc op_getf old b idx);
-              if overwrite then put f (ins_abc op_drop old 0 0);
+              put f (ins_abc op_drop old 0 0)
-              if releases then begin
-                Hashtbl.replace f.f_node s.s_id old;
-                emit_rc p f v ~node:s.s_id ~acquire:false ()
-              end
             end;
             let t = alloc_temp p f value.pos in
             emit_expr p f v ~dst:t ~expected:fty value;
@@ -3803,10 +3733,8 @@ and emit_assign (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (target : Ast
 and emit_return (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (opt : Ast.expr option) : unit =
   match opt with
   | None ->
-    emit_rc p f v ~node:s.s_id ~acquire:true ();
     (match Hashtbl.find_opt v.v_return s.s_id with Some items -> emit_drops p f items | None -> ());
     List.iter (fun r -> put f (ins_abc op_drop r 0 0)) f.f_esc_drops;
-    emit_rc p f v ~node:s.s_id ~acquire:false ();
     f.f_cur_line <- s.s_pos.line;
     put f (ins_abc op_ret0 0 0 0);
     f.f_div <- true
@@ -3833,13 +3761,8 @@ and emit_return (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (opt : Ast.ex
     (match Hashtbl.find_opt v.v_move e.id with
     | Some place -> ( match lookup_local f place with Some (sr, _) -> mask_clear f sr | None -> ())
     | None -> ());
-    (* the escaping value's own increment was emitted where the value
-       landed (emit_expr / emit_tail), which is before the frame's
-       releases below — a balanced pair must never reach rc 0 in between *)
-    emit_rc p f v ~node:s.s_id ~acquire:true ();
     (match Hashtbl.find_opt v.v_return s.s_id with Some items -> emit_drops p f items | None -> ());
     List.iter (fun r -> if r <> t then put f (ins_abc op_drop r 0 0)) f.f_esc_drops;
-    emit_rc p f v ~node:s.s_id ~acquire:false ();
     f.f_cur_line <- s.s_pos.line;
     put f (ins_abc op_ret t 0 0);
     f.f_div <- true
@@ -3861,9 +3784,7 @@ and emit_break (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) : unit =
   | [] ->
     err p ~code:cannot_lower_code ~file:f.f_file ~pos:s.s_pos ~message:"`break` outside of a loop"
   | lf :: _ ->
-    emit_rc p f v ~node:s.s_id ~acquire:true ();
     (match Hashtbl.find_opt v.v_break s.s_id with Some items -> emit_drops p f items | None -> ());
-    emit_rc p f v ~node:s.s_id ~acquire:false ();
     f.f_cur_line <- s.s_pos.line;
     let pc = here f in
     put f (ins_asbx op_jmp 0 0);
@@ -3876,9 +3797,7 @@ and emit_continue (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) : unit =
     err p ~code:cannot_lower_code ~file:f.f_file ~pos:s.s_pos
       ~message:"`continue` outside of a loop"
   | lf :: _ ->
-    emit_rc p f v ~node:s.s_id ~acquire:true ();
     (match Hashtbl.find_opt v.v_continue s.s_id with Some items -> emit_drops p f items | None -> ());
-    emit_rc p f v ~node:s.s_id ~acquire:false ();
     f.f_cur_line <- s.s_pos.line;
     let pc = here f in
     put f (ins_asbx op_jmp 0 0);
@@ -3891,10 +3810,8 @@ and emit_block (p : pctx) (f : fstate) (v : views) ~(node : int) ~(label : strin
   let saved_env = f.f_env in
   let saved_decls = f.f_declared in
   List.iter (emit_stmt p f v) body;
-  (* scope end: the owner table's DROPs first, then the @gc releases for
+  (* scope end: the owner table's DROPs, owner.ml's own pop_scope order *)
-     the handles this block declared — owner.ml's own pop_scope order *)
   emit_scope_drops p f v ~node ~label;
-  emit_rc p f v ~node ~acquire:false ~groups:(declared_since f saved_decls) ();
   f.f_nlocals <- saved_locals;
   f.f_env <- saved_env;
   f.f_declared <- saved_decls;
@@ -4049,7 +3966,6 @@ and emit_for (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (var : string)
     List.iter (emit_stmt p f v) body;
     f.f_loops <- List.tl f.f_loops;
     emit_scope_drops p f v ~node:s.s_id ~label:"FOR";
-    emit_rc p f v ~node:s.s_id ~acquire:false ~groups:(declared_since f saved_decls) ();
     let continue_target = here f in
     List.iter (fun pc -> patch_jump p f ~file:f.f_file ~pos:s.s_pos pc continue_target) lf.lf_continues;
     f.f_temp <- f.f_nlocals;
@@ -4112,7 +4028,6 @@ and emit_for (p : pctx) (f : fstate) (v : views) (s : Ast.stmt) (var : string)
     List.iter (emit_stmt p f v) body;
     f.f_loops <- List.tl f.f_loops;
     emit_scope_drops p f v ~node:s.s_id ~label:"FOR";
-    emit_rc p f v ~node:s.s_id ~acquire:false ~groups:(declared_since f saved_decls) ();
     (* haxe-parity Task 2: `continue` re-enters right here — after this
        iteration's own scope-end cleanup (a `continue` already ran the
        equivalent of it at its own site, from v_continue — see
@@ -4249,7 +4164,6 @@ let emit_method (p : pctx) (v : views) ~(file : string) ~(self_class : (int * st
   stmt_reset f;
   f.f_cur_line <- m.pos.line;
   emit_scope_drops p f v ~node:m.id ~label:"BODY";
-  emit_rc p f v ~node:m.id ~acquire:false ~groups:(declared_since f []) ();
   (* the terminator rule: the loader rejects a method whose last
      instruction is not one, and the implicit void return is what
      control falling off the end means *)

compiler/src/owner.ml

@@ -277,22 +277,9 @@ type drop_site = {
   dr_items : drop_item list;
 }
 
-type rc_op =
+(* iteration 7b: the rc-site machinery (acquire/release pairs, elision
-  | RcAcquire
+   groups, the clobber rule) is gone with reference counting itself — a
-  | RcRelease
+   traced value's aliases need no bookkeeping, tracing owns the lifetime. *)
-
-(* rc_group ties a binding's ACQUIRE to its RELEASE(s): both are elided
-   together when the pair is provably balanced inside one scope. Escape
-   sites (a @gc value returned, stored, or moved into a `take`) use group
-   -1 — an increment that outlives the scope can never be elided. *)
-type rc_site = {
-  rc_node : int;
-  rc_pos : Ast.pos;
-  rc_op : rc_op;
-  rc_place : string;
-  rc_group : int;
-  mutable rc_elided : bool;
-}
 
 type acc_kind =
   | AShared
@@ -319,7 +306,6 @@ type residual_site = {
 type tables = {
   moves : move_site list;
   drops : drop_site list;
-  rcs : rc_site list;
   residuals : residual_site list;
 }
 
@@ -368,7 +354,6 @@ type scope = {
 type sink = {
   mutable s_moves : move_site list;
   mutable s_drops : drop_site list;
-  mutable s_rcs : rc_site list;
   mutable s_res : residual_site list;
 }
 
@@ -393,14 +378,6 @@ type ctx = {
   (* set when the current path has returned; a diverged path contributes
      no scope-end drops and drops out of if/else joins *)
   mutable diverged : bool;
-  (* rc bookkeeping, resolved into rc_elided at the end of the function *)
-  mutable fn_rcs : rc_site list;
-  rc_groups : (int, string option) Hashtbl.t; (* group -> source root, None = fresh allocation *)
-  rc_escaped : (int, unit) Hashtbl.t;
-  (* roots that are assigned to, or exclusively borrowed, anywhere in
-     this function — an rc pair whose source root is clobbered cannot be
-     elided, because the original reference may die inside the scope *)
-  clobbered : (string, unit) Hashtbl.t;
   (* iteration 7b demand-promotion (Gcinfer): when Some, the pass runs in
      collect mode — a class value that would fail the escape rule records its
      class here instead of raising WO-E304, so inference can promote it to
@@ -860,13 +837,6 @@ let record_drop (ctx : ctx) ~node ~(pos : Ast.pos) ~kind ~items : unit =
     ctx.sink.s_drops <-
       { dr_node = node; dr_pos = pos; dr_kind = kind; dr_items = items } :: ctx.sink.s_drops
 
-let record_rc (ctx : ctx) ~node ~(pos : Ast.pos) ~op ~place ~group : unit =
-  if ctx.recording then
-    ctx.fn_rcs <-
-      { rc_node = node; rc_pos = pos; rc_op = op; rc_place = place; rc_group = group;
-        rc_elided = false }
-      :: ctx.fn_rcs
-
 let record_residual (ctx : ctx) ~node ~(pos : Ast.pos) ~(a : place) ~a_kind ~(b : place) ~b_kind :
     unit =
   if ctx.recording then
@@ -879,8 +849,6 @@ let record_residual (ctx : ctx) ~node ~(pos : Ast.pos) ~(a : place) ~a_kind ~(b
         rs_b_node = b.pnode }
       :: ctx.sink.s_res
 
-let clobber (ctx : ctx) (root : string) : unit = Hashtbl.replace ctx.clobbered root ()
-
 (* ============================================================
    Scopes, live sets, snapshots
    ============================================================ *)
@@ -929,14 +897,6 @@ let mask_items (ls : local list) : drop_item list =
       { di_name = l.l_name; di_kind = (if l.l_class = Gc then LGc else LOwned); di_node = l.l_node })
     ls
 
-(* Releases for the @gc handles a scope exit destroys. *)
-let release_gc (ctx : ctx) ~node ~pos (ls : local list) : unit =
-  List.iter
-    (fun l ->
-      if l.l_class = Gc then
-        record_rc ctx ~node ~pos ~op:RcRelease ~place:l.l_name ~group:l.l_node)
-    ls
-
 let pop_scope (ctx : ctx) : unit =
   match ctx.scopes with
   | [] -> ()
@@ -944,8 +904,7 @@ let pop_scope (ctx : ctx) : unit =
     if not ctx.diverged then begin
       let live = List.filter is_live_holder sc.sc_locals in
       record_drop ctx ~node:sc.sc_node ~pos:sc.sc_pos ~kind:(DScope sc.sc_label)
-        ~items:(owned_items live);
+        ~items:(owned_items live)
-      release_gc ctx ~node:sc.sc_node ~pos:sc.sc_pos live
     end;
     ctx.scopes <- rest
 
@@ -1087,16 +1046,6 @@ let escape (ctx : ctx) (l : local) ~(pos : Ast.pos) ~message
     report ctx ~code:borrow_escape_code ~pos ~message ~rel:l.l_pos
       ~label:(borrow_label l)
 
-(* A @gc value reaching a location that outlives this scope: one
-   increment at the escape site, never elidable. If the escaping value is
-   a whole local, its own binding pair can no longer be elided either. *)
-let gc_escape (ctx : ctx) (p : place) : unit =
-  record_rc ctx ~node:p.pnode ~pos:p.ppos ~op:RcAcquire ~place:(place_text p) ~group:(-1);
-  if p.projs = [] then
-    match root_local ctx p with
-    | Some l -> Hashtbl.replace ctx.rc_escaped l.l_node ()
-    | None -> ()
-
 (* Whether passing/assigning this place would be a *real* transfer — the
    positive half of `transfer`'s decision below, needed one step earlier by
    analyze_call: an argument that cannot transfer (a borrow, a projection,
@@ -1130,9 +1079,7 @@ let is_real_transfer (ctx : ctx) (p : place) : bool =
 let transfer (ctx : ctx) (p : place) ~(what : string) : bool =
   match place_class ctx p with
   | Copy -> false
-  | Gc ->
+  | Gc -> false (* traced values alias freely; tracing owns the lifetime *)
-    gc_escape ctx p;
-    false
   | Owned -> (
     match is_borrow_root ctx p with
     | Some l ->
@@ -1155,7 +1102,6 @@ let transfer (ctx : ctx) (p : place) ~(what : string) : bool =
           else begin
             check_against_borrows ctx ~node:p.pnode ~pos:p.ppos p AMove;
             l.l_state <- Moved p.ppos;
-            clobber ctx p.root;
             true
           end)))
 
@@ -1302,9 +1248,6 @@ and analyze_call (ctx : ctx) (call_e : Ast.expr) (callee : Ast.expr) (args : Ast
       let excl = match resolved with Some c -> c.ce_recv_excl | None -> false in
       (match place_of base with
       | Some p ->
-        (* same ordering as the argument case below: a receiver a method
-           writes to is clobbered whatever its class *)
-        if excl then clobber ctx p.root;
         if place_class ctx p = Owned then
           Some { ac_place = p; ac_kind = (if excl then AExcl else AShared) }
         else None
@@ -1329,13 +1272,6 @@ and analyze_call (ctx : ctx) (call_e : Ast.expr) (callee : Ast.expr) (args : Ast
            | None -> []
            | Some p -> (
              let _, conv = conv_of i in
-             (* Clobbering is decided *before* the ownership class, because
-                it is not an ownership question: a `mut` argument means the
-                callee may replace what the place holds, and for a @gc place
-                that is exactly what invalidates rc elision (the alias would
-                be the last reference and its increment was elided). Getting
-                this order wrong is a use-after-free, not an imprecision. *)
-             if conv = Mut then clobber ctx p.root;
              match (place_class ctx p, conv) with
              | Copy, _ | Gc, _ -> []
              | Owned, Take ->
@@ -1366,27 +1302,10 @@ and analyze_call (ctx : ctx) (call_e : Ast.expr) (callee : Ast.expr) (args : Ast
           a.ac_place AExcl)
     accesses;
   (* transfers last *)
-  (* `push`'s value argument (builtin `multi_push`) stores a @gc reference
+  (* iteration 7b deleted the `push`-of-a-gc-value special case (an RC_INC
-     inside the container permanently — an escape exactly like a ctor
+     escape site): a traced value stored into a container needs no
-     field or a `take` argument. `push` is never a resolved callee (it has
+     bookkeeping — tracing finds it through the container. The bug class the
-     no declared params), so `conv_of` defaults it to Borrow and the
+     old special case guarded against cannot recur without RC. *)
-     ordinary Take-gated transfer above never fires for it; without this
-     the container holds the reference with no matching RC_INC, and the
-     collector frees the value out from under the container it still sits
-     in. Narrow to `push`'s own value slot (index 1) and to Gc places only
-     — an Owned element's move-on-push is a separate, pre-existing gap
-     this task does not touch. *)
-  (* Keyed on "`push` is not a user-declared fn", NOT on "the callee did not
-     resolve": since 2026-08-14 resolve_callee answers for builtins too (their
-     return types are what give a `split`/`slice` binding its drop), and the
-     old `resolved = None` test silently stopped firing — the pushed @gc value
-     lost its RC_INC, the collector freed it while the container still held it,
-     and both `gc/` fixtures died with a use-after-free. *)
-  let is_push_gc_value i =
-    i = 1
-    && Types.StringMap.find_opt "push" ctx.syms.Types.free_fns = None
-    && match callee.kind with Ident "push" -> true | _ -> false
-  in
   List.iteri
     (fun i a ->
       match place_of a with
@@ -1396,7 +1315,7 @@ and analyze_call (ctx : ctx) (call_e : Ast.expr) (callee : Ast.expr) (args : Ast
         if conv = Take then
           (if transfer ctx p ~what:(Printf.sprintf "cannot be passed to `take %s`" pname) then
              record_move ctx p (MvArg pname))
-        else if is_push_gc_value i && place_class ctx p = Gc then gc_escape ctx p)
+        )
     args;
   record_drop ctx ~node:call_e.id ~pos:call_e.pos ~kind:DLiveMask
     ~items:(mask_items (live_holders ctx))
@@ -1860,15 +1779,8 @@ and analyze_let (ctx : ctx) (s : Ast.stmt) (name : string) (ty : Ast.field_ty op
             (true, None, Live)
           end
           else (false, Some p, Borrowed s.s_pos)))
-    | Gc, None ->
+    | Gc, None -> (true, None, Live) (* traced: no bookkeeping (7b) *)
-      (* fresh allocation: its release is the allocation's own, never
+    | Gc, Some p -> (true, Some p, Live)
-         elidable *)
-      Hashtbl.replace ctx.rc_groups s.s_id None;
-      (true, None, Live)
-    | Gc, Some p ->
-      Hashtbl.replace ctx.rc_groups s.s_id (Some p.root);
-      record_rc ctx ~node:s.s_id ~pos:s.s_pos ~op:RcAcquire ~place:(place_text p) ~group:s.s_id;
-      (true, Some p, Live)
   in
   declare ctx
     { l_name = name; l_ty = vty; l_class = cls; l_node = s.s_id; l_pos = s.s_pos; l_holds = holds;
@@ -1902,7 +1814,6 @@ and analyze_assign (ctx : ctx) (s : Ast.stmt) (target : Ast.expr) (value : Ast.e
   (match tplace with
   | None -> read_expr ctx target
   | Some p ->
-    clobber ctx p.root;
     check_against_borrows ctx ~node:s.s_id ~pos:p.ppos p AExcl;
     if p.projs = [] then begin
       match root_local ctx p with
@@ -1910,10 +1821,6 @@ and analyze_assign (ctx : ctx) (s : Ast.stmt) (target : Ast.expr) (value : Ast.e
         if l.l_class = Owned then
           record_drop ctx ~node:s.s_id ~pos:p.ppos ~kind:DOverwrite
             ~items:[ { di_name = place_text p; di_kind = LOwned; di_node = p.pnode } ]
-        else if l.l_class = Gc then begin
-          Hashtbl.replace ctx.rc_escaped l.l_node ();
-          record_rc ctx ~node:s.s_id ~pos:p.ppos ~op:RcRelease ~place:(place_text p) ~group:(-1)
-        end
       | _ -> ()
     end
     else begin
@@ -1924,7 +1831,7 @@ and analyze_assign (ctx : ctx) (s : Ast.stmt) (target : Ast.expr) (value : Ast.e
       | Owned ->
         record_drop ctx ~node:s.s_id ~pos:p.ppos ~kind:DOverwrite
             ~items:[ { di_name = place_text p; di_kind = LOwned; di_node = p.pnode } ]
-      | Gc -> record_rc ctx ~node:s.s_id ~pos:p.ppos ~op:RcRelease ~place:(place_text p) ~group:(-1)
+      | Gc -> () (* traced: tracing owns the old value's lifetime (7b) *)
       | Copy -> ()
     end);
   (* the incoming value *)
@@ -1966,7 +1873,6 @@ and analyze_return (ctx : ctx) (s : Ast.stmt) (opt : Ast.expr option) : unit =
         record_move ctx p MvReturn));
   let live = live_holders ctx in
   record_drop ctx ~node:s.s_id ~pos:s.s_pos ~kind:DReturn ~items:(owned_items live);
-  release_gc ctx ~node:s.s_id ~pos:s.s_pos live;
   ctx.diverged <- true
 
 (* haxe-parity Task 2: `break`/`continue` reuse analyze_return's own
@@ -1988,8 +1894,7 @@ and analyze_break (ctx : ctx) (s : Ast.stmt) : unit =
   | [] -> ()
   | loop_node :: _ ->
     let live = live_holders_upto ctx loop_node in
-    record_drop ctx ~node:s.s_id ~pos:s.s_pos ~kind:DBreak ~items:(owned_items live);
+    record_drop ctx ~node:s.s_id ~pos:s.s_pos ~kind:DBreak ~items:(owned_items live));
-    release_gc ctx ~node:s.s_id ~pos:s.s_pos live);
   ctx.diverged <- true
 
 and analyze_continue (ctx : ctx) (s : Ast.stmt) : unit =
@@ -1997,8 +1902,7 @@ and analyze_continue (ctx : ctx) (s : Ast.stmt) : unit =
   | [] -> ()
   | loop_node :: _ ->
     let live = live_holders_upto ctx loop_node in
-    record_drop ctx ~node:s.s_id ~pos:s.s_pos ~kind:DContinue ~items:(owned_items live);
+    record_drop ctx ~node:s.s_id ~pos:s.s_pos ~kind:DContinue ~items:(owned_items live));
-    release_gc ctx ~node:s.s_id ~pos:s.s_pos live);
   ctx.diverged <- true
 
 (* ============================================================
@@ -2022,25 +1926,12 @@ let param_local (ctx : ctx) (p : Ast.param) : local =
       { l_name = p.name; l_ty = p.ty; l_class = cls; l_node = p.id; l_pos = p.pos; l_holds = false;
         l_src = None; l_bkind = (if p.conv = Mut then AExcl else AShared); l_state = state })
 
-let resolve_rc (ctx : ctx) : unit =
-  List.iter
-    (fun r ->
-      if r.rc_group >= 0 then
-        r.rc_elided <-
-          (not (Hashtbl.mem ctx.rc_escaped r.rc_group))
-          && (match Hashtbl.find_opt ctx.rc_groups r.rc_group with
-             | Some (Some root) -> not (Hashtbl.mem ctx.clobbered root)
-             | _ -> false))
-    ctx.fn_rcs;
-  ctx.sink.s_rcs <- ctx.fn_rcs @ ctx.sink.s_rcs
-
 let analyze_fn ~(file : string) ?(promote : (string -> unit) option = None)
     (syms : Types.symbols) (coll : Diag.Collector.t) (sink : sink)
     ~(self_class : string option) (m : Ast.method_decl) : unit =
   let ctx =
     { file; syms; coll; sink; fn_name = m.name; scopes = []; loop_stack = []; recording = true;
-      diverged = false; fn_rcs = []; rc_groups = Hashtbl.create 8; rc_escaped = Hashtbl.create 8;
+      diverged = false; promote }
-      clobbered = Hashtbl.create 8; promote }
   in
   push_scope ctx ~node:m.id ~pos:m.pos ~label:"BODY";
   (* `self` is always a borrow (spec rule 6) *)
@@ -2055,8 +1946,7 @@ let analyze_fn ~(file : string) ?(promote : (string -> unit) option = None)
         l_state = (if cls = Gc then Live else Borrowed m.pos) });
   List.iter (fun p -> declare ctx (param_local ctx p)) m.params;
   List.iter (analyze_stmt ctx) m.body;
-  pop_scope ctx;
+  pop_scope ctx
-  resolve_rc ctx
 
 (* ============================================================
    Entry point
@@ -2066,7 +1956,7 @@ let pos_key (p : Ast.pos) = (p.line, p.col)
 
 let analyze ~(file : string) ?(promote : (string -> unit) option = None)
     (prog : Ast.program) (syms : Types.symbols) (coll : Diag.Collector.t) : tables =
-  let sink = { s_moves = []; s_drops = []; s_rcs = []; s_res = [] } in
+  let sink = { s_moves = []; s_drops = []; s_res = [] } in
   List.iter
     (function
       | Ast.Class c ->
@@ -2086,5 +1976,4 @@ let analyze ~(file : string) ?(promote : (string -> unit) option = None)
   let sort_by key l = List.stable_sort (fun a b -> compare (key a) (key b)) (List.rev l) in
   { moves = sort_by (fun m -> pos_key m.mv_pos) sink.s_moves;
     drops = sort_by (fun d -> pos_key d.dr_pos) sink.s_drops;
-    rcs = sort_by (fun r -> pos_key r.rc_pos) sink.s_rcs;
     residuals = sort_by (fun r -> pos_key r.rs_pos) sink.s_res }

compiler/test/golden/bc/elision.expected

@@ -28,26 +28,23 @@ m1   proven args=1 regs=3 [free fn]
   0002  CALL      r2, m0
   0003  RET       r2
 m2   main args=0 regs=6 [free fn] [ENTRY]
-  lines: 0->29 3->30 7->31 13->28
+  lines: 0->29 3->30 6->31 12->28
   drops: pc 3 owned={} gc={r0}
-  drops: pc 7 owned={r1} gc={r0}
+  drops: pc 6 owned={r1} gc={r0}
-  drops: pc 14 owned={} gc={r0}
+  drops: pc 13 owned={} gc={r0}
-  drops: pc 15 owned={} gc={}
   0000  NEW       r0, c0
   0001  LOADK     r1, k8
   0002  SETF      r0, f0, r1
   0003  NEW       r1, c1
   0004  MOVE      r2, r0
-  0005  RC_INC    r2
+  0005  SETF      r1, f0, r2
-  0006  SETF      r1, f0, r2
+  0006  MOVE      r4, r1
-  0007  MOVE      r4, r1
+  0007  CALL      r4, m1
-  0008  CALL      r4, m1
+  0008  MOVE      r3, r4
-  0009  MOVE      r3, r4
+  0009  LOADK     r5, k9
-  0010  LOADK     r5, k9
+  0010  ADD       r2, r3, r5
-  0011  ADD       r2, r3, r5
+  0011  BUILTIN   r2, r2, print_int
-  0012  BUILTIN   r2, r2, print_int
+  0012  DROP      r1
-  0013  DROP      r1
+  0013  RET0
-  0014  RC_DEC    r0
-  0015  RET0
 == ENTRY ==
 m2

compiler/test/golden/owner/drops.expected

@@ -19,5 +19,4 @@
 50:3 JOIN-DROP ELSE [a]
 58:3 RETURN [a]
 64:3 RETURN [a]
-== RC ==
 == RESIDUAL ==

compiler/test/golden/owner/moves.expected

@@ -7,5 +7,4 @@
 10:3 RETURN [it]
 16:16 LIVE-MASK [bag, held]
 17:3 RETURN [held]
-== RC ==
 == RESIDUAL ==

compiler/test/golden/owner/pricing-demo.expected

@@ -3,5 +3,4 @@
 == DROPS ==
 18:5 OVERWRITE self.name
 22:5 OVERWRITE self.prices
-== RC ==
 == RESIDUAL ==

compiler/test/golden/owner/rc.expected

@@ -4,13 +4,4 @@
 26:15 LIVE-MASK [c:gc]
 35:18 LIVE-MASK [c:gc]
 36:15 LIVE-MASK [c:gc]
-== RC ==
-15:3 ACQUIRE h.cache ELIDED
-16:3 RELEASE c ELIDED
-20:3 ACQUIRE h.cache KEPT
-21:3 RELEASE c KEPT
-21:10 ACQUIRE c KEPT
-26:3 RELEASE c KEPT
-34:3 ACQUIRE h.cache KEPT
-36:3 RELEASE c KEPT
 == RESIDUAL ==

compiler/test/golden/owner/residual.expected

@@ -1,6 +1,5 @@
 == MOVES ==
 == DROPS ==
-== RC ==
 == RESIDUAL ==
 22:22 RESIDUAL BORROW_X bag.items[i] vs BORROW_X bag.items[j]
 24:24 RESIDUAL BORROW_X bag.items[i] vs BORROW_S bag.items[j]

compiler/test/runner.ml

@@ -1965,13 +1965,6 @@ let () =
        (fun (d : Owner.drop_site) ->
          List.for_all (fun (i : Owner.drop_item) -> i.Owner.di_node > 0) d.Owner.dr_items)
        tables.Owner.drops);
-  let rc_path = "golden/owner/rc.wo" in
-  let rc_tables, _ = owner_str ~file:rc_path (read_file rc_path) in
-  check "rc table: every entry carries a real AST node id"
-    (List.for_all (fun (r : Owner.rc_site) -> r.Owner.rc_node > 0) rc_tables.Owner.rcs);
-  check "rc table: the balanced pair is elided, the escaping one kept"
-    (List.exists (fun (r : Owner.rc_site) -> r.Owner.rc_elided) rc_tables.Owner.rcs
-    && List.exists (fun (r : Owner.rc_site) -> not r.Owner.rc_elided) rc_tables.Owner.rcs);
   let res_path = "golden/owner/residual.wo" in
   let res_tables, _ = owner_str ~file:res_path (read_file res_path) in
   check_eq "residual table: only the runtime-index pairs are residual" ~expected:3
@@ -2235,23 +2228,6 @@ let () =
   check "switch let-class: `w` is dropped at the return (classified Owned, not silently Copy)"
     (List.exists (fun d -> names_of d = [ "w" ]) returns)
 
-let () =
-  (* IMPORTANT: a `mut` argument means the callee may replace what the place
-     holds. For a @gc place that invalidates rc elision — the elided
-     increment would leave the alias as the last reference to a freed
-     object. The clobber therefore has to happen before the ownership class
-     is consulted, since @gc arguments create no access entry at all. *)
-  let path = "golden/owner/rc.wo" in
-  let tables, _ = owner_str ~file:path (read_file path) in
-  let at line =
-    List.filter (fun (r : Owner.rc_site) -> r.Owner.rc_pos.Ast.line = line) tables.Owner.rcs
-  in
-  single_site "rc: `balanced` has one ACQUIRE" (at 15) (fun r ->
-      check "rc: an alias whose source is never clobbered is ELIDED" r.Owner.rc_elided);
-  single_site "rc: `clobbered` has one ACQUIRE" (at 34) (fun r ->
-      check "rc: an alias whose source root is passed `mut` is KEPT"
-        (not r.Owner.rc_elided))
-
 let () =
   let path = "golden/owner/moves.wo" in
   let exit_code, stdout, stderr = run_cli [ "--dump-owner"; path ] in
@@ -2295,7 +2271,7 @@ let validate_image (img : string) : string list =
   let u64 o = if ok 8 o then String.get_int64_le img o else 0L in
   let none = 0xFFFFFFFF in
   if u32 0 <> 0x31424F57 then fail "bad magic";
-  if u32 4 <> 3 then fail "unsupported version";
+  if u32 4 <> 4 then fail "unsupported version";
   let coff = u32 8 and ccnt = u32 12 in
   let koff = u32 16 and kcnt = u32 20 in
   let ioff = u32 24 and icnt = u32 28 in
@@ -2614,26 +2590,26 @@ let method_block (dump : string) (name : string) : string =
   String.concat "\n" (collect [] false lines)
 
 let () =
-  (* The spec's zero-cost promise, as an assertion and not only a pinned
+  (* The zero-cost promise, iteration 7b edition: a proven method emits no
-     dump: a method whose ownership is fully proven contains no borrow op
+     borrow op, and NO method anywhere emits an rc op — reference counting
-     and no rc op. golden/bc/elision.wo's `proven` aliases a @gc
+     is gone from the instruction stream entirely (opcodes 27/28 reserved). *)
-     reference and passes it to a reader; owner.ml marks the pair ELIDED
-     (golden/owner/rc.wo pins that), so nothing may be emitted for it. *)
   let path = "golden/bc/elision.wo" in
   let image, _ = emit_str ~file:path (read_file path) in
-  let block = method_block (Disasm.dump image) "proven" in
+  let dump = Disasm.dump image in
+  let block = method_block dump "proven" in
   check "elision: `proven` was found in the disassembly" (block <> "");
   List.iter
     (fun op ->
       check
         (Printf.sprintf "elision: `proven` emits no %s (zero-cost when provable)" op)
         (find_substring ~needle:op block = None))
-    [ "BORROW_S"; "BORROW_X"; "RELEASE_S"; "RELEASE_X"; "RC_INC"; "RC_DEC" ];
+    [ "BORROW_S"; "BORROW_X"; "RELEASE_S"; "RELEASE_X" ];
-  (* the contrast, so the fixture cannot pass by emitting nothing anywhere:
+  List.iter
-     main stores the @gc value into a field, which is a KEPT acquire *)
+    (fun op ->
-  let main_block = method_block (Disasm.dump image) "main" in
+      check
-  check "elision: the escaping acquire in `main` is still emitted (fixture is not vacuous)"
+        (Printf.sprintf "rc retired: the whole image contains no %s" op)
-    (find_substring ~needle:"RC_INC" main_block <> None)
+        (find_substring ~needle:op dump = None))
+    [ "RC_INC"; "RC_DEC" ]
 
 let () =
   (* haxe-parity Task 3: the compare-and-jump chain lowers onto the
@@ -2786,12 +2762,9 @@ let () =
     (List.fold_left max 0 masks <= List.fold_left max 0 popcounts)
 
 (* The ownership tables are a contract, not a hint: every DROP the DROPS
-   table asks for, and every rc op the RC table does not mark ELIDED, has
+   table asks for has to appear in the emitted code exactly once — and
-   to appear in the emitted code exactly once — and nothing else may. A
+   nothing else may (rc ops don't exist since iteration 7b). A count
-   count identity over a whole file is the cheapest way to state that, and
+   identity over a whole file is the cheapest way to state that. *)
-   it is what caught a missing constructor-field @gc acquire (the escape
-   increment is anchored on the value's expression node, so lowering it
-   per statement kind silently skipped one of the four escapes). *)
 let () =
   let count_op needle dump =
     String.split_on_char '\n' dump
@@ -2817,23 +2790,14 @@ let () =
                        d.Owner.dr_items))
             0 tables.Owner.drops
         in
-        let kept op =
-          List.length
-            (List.filter
-               (fun (r : Owner.rc_site) -> r.Owner.rc_op = op && not r.Owner.rc_elided)
-               tables.Owner.rcs)
-        in
         let image, _ = emit_str ~file:path src in
         let dump = Disasm.dump image in
         check_eq
           (Printf.sprintf "table contract %s: one DROP per owned drop-table item" path)
           ~expected:want_drops ~actual:(count_op "DROP " dump) string_of_int;
         check_eq
-          (Printf.sprintf "table contract %s: one RC_INC per KEPT acquire" path)
+          (Printf.sprintf "table contract %s: rc ops never appear (7b)" path)
-          ~expected:(kept Owner.RcAcquire) ~actual:(count_op "RC_INC" dump) string_of_int;
+          ~expected:0 ~actual:(count_op "RC_INC" dump + count_op "RC_DEC" dump) string_of_int;
-        check_eq
-          (Printf.sprintf "table contract %s: one RC_DEC per KEPT release" path)
-          ~expected:(kept Owner.RcRelease) ~actual:(count_op "RC_DEC" dump) string_of_int;
         (* The residual table is both the only licence to emit a borrow
            op and an obligation to emit one per *operand*: guards are
            coalesced per operand, never per entry (asking twice for an

runtime/src/loader.c

@@ -461,8 +461,6 @@ int wo_load_buf(wo_module *m, const uint8_t *buf, size_t len, char *err,
             case WOP_BORROW_X:
             case WOP_RELEASE_S:
             case WOP_RELEASE_X:
-            case WOP_RC_INC:
-            case WOP_RC_DEC:
                 RCHK(A);
                 break;
             case WOP_BUILTIN: {

runtime/src/vm.c

@@ -264,8 +264,7 @@ static int vm_run(wo_vm *vm, uint64_t *ret, wo_err *err) {
         [WOP_GETF] = &&L_GETF,         [WOP_SETF] = &&L_SETF,
         [WOP_DROP] = &&L_DROP,         [WOP_BORROW_S] = &&L_BORROW_S,
         [WOP_BORROW_X] = &&L_BORROW_X, [WOP_RELEASE_S] = &&L_RELEASE_S,
-        [WOP_RELEASE_X] = &&L_RELEASE_X, [WOP_RC_INC] = &&L_RC_INC,
+        [WOP_RELEASE_X] = &&L_RELEASE_X, [WOP_BUILTIN] = &&L_BUILTIN,
-        [WOP_RC_DEC] = &&L_RC_DEC,     [WOP_BUILTIN] = &&L_BUILTIN,
         [WOP_DB_STUB] = &&L_DB_STUB,   [WOP_TRAP] = &&L_TRAP,
         [WOP_TRY] = &&L_TRY,           [WOP_ENDTRY] = &&L_ENDTRY,
     };
@@ -488,14 +487,6 @@ dispatch:
         NEXT();
     }
 
-    /* iteration 7b: reference counting is retired — tracing owns traced
-     * lifetimes, so alias bookkeeping means nothing. The opcodes stay
-     * accepted as no-ops until the emitter stops producing them and the
-     * format reserves 27–28 (the .wob version bump); a no-op is also what
-     * deletes the old RC_DEC-on-nil trap that broke `?Node` field stores. */
-    CASE(RC_INC) : NEXT();
-    CASE(RC_DEC) : NEXT();
-
     CASE(CONCAT) : {
         const char *why;
         wo_str *x = str_check(R[wo_ins_b(ins)], &why);

runtime/src/wob.h

@@ -12,7 +12,8 @@
 
 /* ---- file header (44 bytes, absolute offsets) ---- */
 #define WOB_MAGIC 0x31424F57u /* "WOB1" read as LE u32 */
-#define WOB_VERSION 3u /* v3: v2's field metadata + per-class index metadata */
+#define WOB_VERSION 4u /* v4 (iteration 7b): opcodes 27-28 (RC_INC/RC_DEC) retired;
+ * the drop table's gc mask now means "GC roots at this pc" */
 #define WOB_HDR_SIZE 44u
 #define WOB_OFF_MAGIC 0u
 #define WOB_OFF_VERSION 4u
@@ -168,8 +169,8 @@ enum {
     WOP_BORROW_X = 24,
     WOP_RELEASE_S = 25,
     WOP_RELEASE_X = 26,
-    WOP_RC_INC = 27,
+    /* 27-28 were RC_INC/RC_DEC — retired with reference counting (v4,
-    WOP_RC_DEC = 28,
+       iteration 7b). Reserved: the loader rejects them. */
     WOP_BUILTIN = 29, /* A B C: r[A] = builtin C, args from r[B] */
     WOP_DB_STUB = 30, /* traps WO_T_DB "engine not linked" */
     WOP_TRAP = 31,    /* Bx: explicit trap */

runtime/test/test_unwind.c

@@ -104,30 +104,51 @@ static void test_two_frame_unwind_frees_both(void) {
 }
 
 /* rc inc/dec through opcodes frees exactly at zero (@gc malloc-path class) */
-static void test_rc_opcodes_free_at_zero(void) {
+/* iteration 7b: opcodes 27-28 (the old RC_INC/RC_DEC) are reserved in .wob
+ * v4 — the loader must reject an image that carries one, exactly like any
+ * other unknown opcode. A traced instance abandoned by a clean return is
+ * rt_destroy's to free (ASan proves it). */
+static void test_reserved_rc_opcode_rejected(void) {
     wb_t *b = wb_new();
     uint32_t kc = wb_const_text(b, "GBig");
     uint32_t kf = wb_const_text(b, "main");
     wb_class(b, kc, WO_CLASSF_GC, big_kinds, BIG);
     uint32_t code[] = {
-        wo_ins_abx(WOP_NEW, 0, 0),         /* rc 1 */
+        wo_ins_abx(WOP_NEW, 0, 0),
-        wo_ins_abc(WOP_RC_INC, 0, 0, 0),   /* rc 2 */
+        wo_ins_abc(27 /* retired RC_INC */, 0, 0, 0),
-        wo_ins_abc(WOP_RC_DEC, 0, 0, 0),   /* rc 1 */
-        wo_ins_abc(WOP_RC_DEC, 0, 0, 0),   /* rc 0: freed */
         wo_ins_abc(WOP_RET0, 0, 0, 0),
     };
-    wb_method(b, kf, WOB_NONE, 0, 1, code, 5, NULL, 0, NULL, 0);
+    wb_method(b, kf, WOB_NONE, 0, 1, code, 3, NULL, 0, NULL, 0);
     size_t len;
     uint8_t *img = wb_finish(b, &len);
     uint64_t ret = 0;
     wo_err err;
-    T_EQ(run_img(img, len, &ret, &err), 0); /* no trap; ASan proves the free */
+    T_EQ(run_img(img, len, &ret, &err), -2); /* loader rejection */
+    free(img);
+}
+
+static void test_abandoned_traced_freed_at_destroy(void) {
+    wb_t *b = wb_new();
+    uint32_t kc = wb_const_text(b, "GBig");
+    uint32_t kf = wb_const_text(b, "main");
+    wb_class(b, kc, WO_CLASSF_GC, big_kinds, BIG);
+    uint32_t code[] = {
+        wo_ins_abx(WOP_NEW, 0, 0), /* traced, linked; never dropped */
+        wo_ins_abc(WOP_RET0, 0, 0, 0),
+    };
+    wb_method(b, kf, WOB_NONE, 0, 1, code, 2, NULL, 0, NULL, 0);
+    size_t len;
+    uint8_t *img = wb_finish(b, &len);
+    uint64_t ret = 0;
+    wo_err err;
+    T_EQ(run_img(img, len, &ret, &err), 0); /* ASan: rt_destroy frees it */
     free(img);
 }
 
 int main(void) {
     test_borrow_violation_frees_owned();
     test_two_frame_unwind_frees_both();
-    test_rc_opcodes_free_at_zero();
+    test_reserved_rc_opcode_rejected();
+    test_abandoned_traced_freed_at_destroy();
     return t_report("test_unwind");
 }