From 8ef755da61392d67fa54aaf7c156414634316ea5 Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Wed, 22 May 2024 11:23:38 -0700 Subject: [PATCH] added one more lemma: `with_offset_no_wrap` --- theories/Morello/Capabilities.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index 34b5585..60a444a 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -463,6 +463,17 @@ Module AddressValue <: PTRADDR. destruct (Z.leb ADDR_MIN z) eqn:Hl, (Z.ltb z ADDR_LIMIT) eqn:Hu; split; try lia. Qed. + (** When using `[with_offset]`, it does not wrap as long as the resulting address is within the range. *) + Lemma with_offset_no_wrap: + forall (v:t) (o:Z), + (Z.le ADDR_MIN (to_Z v + o) /\ Z.lt (to_Z v + o) ADDR_LIMIT) -> + to_Z (with_offset v o) = Z.add (to_Z v) o. + Proof. + intros v o H. + apply of_Z_roundtrip. + assumption. + Qed. + End AddressValue. (** [OrderedType] for [AddressValue.t] is useful, for example, to use it