fact: Definition valid_block (m : mem) (b : block) (o : ptrofs) (n : Z) : Prop := 0 < n /\ Ptrofs.unsigned o + n <= Ptrofs.modulus /\ forall i : Z, 0 <= i < n -> common.Memory.Mem.valid_pointer m b (Ptrofs.unsigned o + i) = true.
imports: compcert.common.Events compcert.common.Memory compcert.common.Values compcert.common.AST compcert.lib.Integers Coq.ZArith.BinInt Coq.Lists.List Coq.micromega.Lia