proposition: Lemma make_header_tag: forall g v, raw_mark (vlabel g v) = false -> if Archi.ptr64 then Int64.and (Int64.repr (make_header g v)) (Int64.repr 255) = Int64.repr (raw_tag (vlabel g v)) else Int.and (Int.repr (make_header g v)) (Int.repr 255) = Int.repr (raw_tag (vlabel g v)).
proof: Proof. intros. cbv delta [Archi.ptr64]. simpl. first [rewrite make_header_tag_prep32 | rewrite make_header_tag_prep64]. 2: apply make_header_range. unfold make_header in *. remember (vlabel g v). clear Heqr. rewrite H, !Zbits.Zshiftl_mul_two_p in * by lia. rewrite <- Z.add_assoc. replace (raw_color r * two_p 8 + Zlength (raw_fields r) * two_p 10) with ((raw_color r + Zlength (raw_fields r) * two_p 2) * two_p 8) by (rewrite Z.mul_add_distr_r, <- Z.mul_assoc, <- two_p_is_exp by lia; reflexivity). rewrite Z.div_add by (vm_compute; intros S; inversion S). assert (raw_tag r / two_p 8 = 0) by (apply Z.div_small, raw_tag_range). rewrite H0, Z.add_0_l. first [rewrite mul_repr, sub_repr | rewrite mul64_repr, sub64_repr]. now rewrite <- Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen