just rule out retag in the unknown code for now

theories/sim/refl.v

@@ -27,14 +27,14 @@ Fixpoint expr_wf (e: expr) : Prop :=
   | Val v => value_wf v
   | Call f args => expr_wf f ∧ Forall id (fmap expr_wf args)
   | Case e branches => expr_wf e ∧ Forall id (fmap expr_wf branches)
-  | Deref e _ | Ref e  | Copy e | Retag e _ =>
+  | Deref e _ | Ref e | Copy e =>
     expr_wf e
   | Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
     expr_wf e1 ∧ expr_wf e2
   (* Forbidden cases. *)
   | InitCall e | EndCall e => False
   | Place _ _ _ => False
-  | Free _ => False (* TODO: We'd like to support deallocation! *)
+  | Free _ | Retag _ _ => False (* TODO: We'd like to support deallocation and retag! *)
   end.
 Definition prog_wf (prog: fn_env) :=
   has_main prog ∧
@@ -290,12 +290,7 @@ Proof using Type*.
     simpl. split; last done. constructor; last done.
     eapply arel_mono, arel_ptr; auto.
   - (* Free: can't happen *) done.
-  - (* Retag *)
-    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
-    eapply sim_simple_post_mono, IHe; [|by auto..].
-    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
-    eapply sim_simple_retag_public; [by auto..|].
-    do 3 (split; first done). constructor; done.
+  - (* Retag: can't happen *) done.
   - (* Let *)
     move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
     eapply sim_simple_frame_core.

theories/sim/simple.v

@@ -358,7 +358,7 @@ Lemma sim_simple_retag_public fs ft r n (rs rt: result) k css cst Φ :
   r ⊨ˢ{n,fs,ft} (Retag rs k, css) ≥ (Retag rt k, cst) : Φ.
 Proof.
   intros [Hrel ?]%rrel_with_eq. simplify_eq.
-Admitted.
+Abort.
 
 (** * Pure *)
 Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 css cst Φ :