proposition: Lemma make_header_range: forall g v, 0 <= make_header g v < two_p (WORD_SIZE * 8).
proof: Proof. intros. unfold make_header. destruct (raw_mark (vlabel g v)). - pose proof (two_p_gt_ZERO (WORD_SIZE * 8)). unfold WORD_SIZE in *; lia. - pose proof (raw_tag_range (vlabel g v)). pose proof (raw_color_range (vlabel g v)). pose proof (raw_fields_range (vlabel g v)). remember (raw_tag (vlabel g v)) as z1. clear Heqz1. remember (raw_color (vlabel g v)) as z2. clear Heqz2. remember (Zlength (raw_fields (vlabel g v))) as z3. clear Heqz3. assert (0 <= 8) by lia. apply (Zbits.Zshiftl_mul_two_p z2) in H2. rewrite H2. clear H2. assert (0 <= 10) by lia. apply (Zbits.Zshiftl_mul_two_p z3) in H2. rewrite H2. clear H2. assert (two_p 10 > 0) by (apply two_p_gt_ZERO; lia). assert (two_p 8 > 0) by (apply two_p_gt_ZERO; lia). split. + assert (0 <= z2 * two_p 8) by (apply Z.mul_nonneg_nonneg; lia). assert (0 <= z3 * two_p 10) by (apply Z.mul_nonneg_nonneg; lia). lia. + destruct H as [_ ?]. destruct H0 as [_ ?]. destruct H1 as [_ ?]. change 256 with (two_p 8) in H. change 4 with (two_p 2) in H0. assert (z1 <= two_p 8 - 1) by lia. clear H. assert (z2 <= two_p 2 - 1) by lia. clear H0. assert (z3 <= two_p (WORD_SIZE * 8 - 10) - 1) by lia. clear H1. apply Z.mul_le_mono_nonneg_r with (p := two_p 8) in H. 2: lia. apply Z.mul_le_mono_nonneg_r with (p := two_p 10) in H0. 2: lia. rewrite Z.mul_sub_distr_r in H, H0. rewrite Z.mul_1_l in H, H0. assert (0 <= WORD_SIZE * 8 - 10) by (unfold WORD_SIZE; lia). rewrite <- two_p_is_exp in H, H0 by lia. simpl Z.add in H, H0. clear H1. Opaque two_p. simpl. Transparent two_p. lia. 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