proposition: Lemma MSS_max_wordsize_signed_range: forall n, 0 <= n <= MAX_SPACE_SIZE -> Ptrofs.min_signed <= WORD_SIZE * n < Ptrofs.max_signed.
proof: Proof. intros. destruct H. split. - unfold WORD_SIZE. transitivity 0. 2: lia. rewrite Z.le_lteq. left. apply Ptrofs.min_signed_neg. - apply Z.le_lt_trans with (WORD_SIZE * MAX_SPACE_SIZE). apply Z.mul_le_mono_nonneg_l. compute; congruence. auto. unfold WORD_SIZE. unfold MAX_SPACE_SIZE. unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. destruct Archi.ptr64 eqn:?; first [now inversion Heqb | simpl; 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