proposition: Lemma t_info_space_address: forall t_info i, 0 <= i -> isptr (ti_heap_p t_info) -> (if Archi.ptr64 then force_val (sem_add_ptr_long space_type (offset_val 0 (ti_heap_p t_info)) (Vlong (Int64.repr i))) else force_val (sem_add_ptr_int space_type Signed (offset_val 0 (ti_heap_p t_info)) (Vint (Int.repr i)))) = space_address (ti_heap_p t_info) (Z.to_nat i).
proof: Proof. intros. rewrite isptr_offset_val_zero by assumption. simpl. first [rewrite sem_add_pi_ptr_special' | rewrite sem_add_pl_ptr_special']; auto. unfold space_address. rewrite Z2Nat.id by lia. simpl. f_equal. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)