proposition: Lemma make_header_Wosize: forall g v, raw_mark (vlabel g v) = false -> if Archi.ptr64 then Int64.shru (Int64.repr (make_header g v)) (Int64.repr 10) = Int64.repr (Zlength (raw_fields (vlabel g v))) else Int.shru (Int.repr (make_header g v)) (Int.repr 10) = Int.repr (Zlength (raw_fields (vlabel g v))).
proof: Proof. intros. cbv delta [Archi.ptr64]. simpl. match goal with | |- Int64.shru _ _ = Int64.repr _ => rewrite Int64.shru_div_two_p, !Int64.unsigned_repr | |- Int.shru _ _ = Int.repr _ => rewrite Int.shru_div_two_p, !Int.unsigned_repr end. - f_equal. unfold make_header. remember (vlabel g v). clear Heqr. rewrite H, !Zbits.Zshiftl_mul_two_p by lia. rewrite Z.div_add. 2: compute; lia. pose proof (raw_tag_range r). pose proof (raw_color_range r). cut ((raw_tag r + raw_color r * two_p 8) / two_p 10 = 0). 1: intros; lia. apply Z.div_small. change 256 with (two_p 8) in H0. change 4 with (two_p 2) in H1. assert (0 <= raw_tag r <= two_p 8 - 1) by lia. clear H0. destruct H2. assert (0 <= raw_color r <= two_p 2 - 1) by lia. clear H1. destruct H3. assert (two_p 8 > 0) by (apply two_p_gt_ZERO; lia). split. + assert (0 <= raw_color r * two_p 8) by (apply Z.mul_nonneg_nonneg; lia). lia. + apply Z.mul_le_mono_nonneg_r with (p := two_p 8) in H3. 2: lia. rewrite Z.mul_sub_distr_r, <- two_p_is_exp in H3 by lia. simpl Z.add in H3. lia. - rep_lia. - pose proof (make_header_range g v). unfold WORD_SIZE in *. match goal with | |- context [Int64.max_unsigned] => unfold Int64.max_unsigned, Int64.modulus, Int64.wordsize, Wordsize_64.wordsize | |- context [Int.max_unsigned] => unfold Int.max_unsigned, Int.modulus, Int.wordsize, Wordsize_32.wordsize end. simpl Z.mul in H0. rewrite two_power_nat_two_p. simpl Z.of_nat. 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