diff --git a/src/plugins/wp/.gitattributes b/src/plugins/wp/.gitattributes
index 6a84feb03c33c929346fe45eb86c1af7611987ae..0403cc5cb8c5f3a999adbfea876cb652d96c5851 100644
--- a/src/plugins/wp/.gitattributes
+++ b/src/plugins/wp/.gitattributes
@@ -64,5 +64,5 @@ MakeDoc header_spec=CEA_WP
/doc/manual/nullable.c header_spec=.ignore
/doc/manual/*.tex header_spec=.ignore
-
+/share/why3/frama_c_wp/Wp.header header_spec=.ignore
/tests/**/* header_spec=.ignore
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index 6f393270237475ee5eb2c886e0111e358fe797bd..a83f14990653d6de97debb2017cf8caa8f9863bd 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -64,6 +64,8 @@
(share/why3/frama_c_wp/vset.mlw as wp/why3/frama_c_wp/vset.mlw)
(share/why3/frama_c_wp/memaddr.mlw as wp/why3/frama_c_wp/memaddr.mlw)
(share/why3/frama_c_wp/memory.mlw as wp/why3/frama_c_wp/memory.mlw)
+ (share/why3/frama_c_wp/membytes.mlw as wp/why3/frama_c_wp/membytes.mlw)
(share/why3/frama_c_wp/cmath.mlw as wp/why3/frama_c_wp/cmath.mlw)
(share/why3/frama_c_wp/cfloat.mlw as wp/why3/frama_c_wp/cfloat.mlw)
+ (share/why3/frama_c_wp/sequence.mlw as wp/why3/frama_c_wp/sequence.mlw)
(share/wp.driver as wp/wp.driver)))
diff --git a/src/plugins/wp/share/why3/frama_c_wp/Wp.header b/src/plugins/wp/share/why3/frama_c_wp/Wp.header
new file mode 100644
index 0000000000000000000000000000000000000000..9d26ead4f953f335e05db0229554237d35eaeb86
--- /dev/null
+++ b/src/plugins/wp/share/why3/frama_c_wp/Wp.header
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/dune b/src/plugins/wp/share/why3/frama_c_wp/dune
new file mode 100644
index 0000000000000000000000000000000000000000..b1734cc1c28c791158e69f9eb1dcb3aa21252dbe
--- /dev/null
+++ b/src/plugins/wp/share/why3/frama_c_wp/dune
@@ -0,0 +1,29 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2024 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(executable (name membytesgen))
+
+(rule
+ (targets membytes.mlw)
+ (deps membytesgen.exe Wp.header)
+ (mode (promote))
+ (action (run ./membytesgen.exe)))
diff --git a/src/plugins/wp/share/why3/frama_c_wp/membytes.mlw b/src/plugins/wp/share/why3/frama_c_wp/membytes.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..04d1e5090ac0c9e3564b24e1811cad28c9dcb76b
--- /dev/null
+++ b/src/plugins/wp/share/why3/frama_c_wp/membytes.mlw
@@ -0,0 +1,1831 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* DO NOT EDIT: this file is generated at build time *)
+
+(* Tactics for failing proofs:
+ intros variables ; compute_in_goal ; cvc5 *)
+
+module ValueCodec
+ use int.Int
+ use int.ComputerDivision
+ use frama_c_wp.cint.Cint
+ use frama_c_wp.sequence.Seq
+
+ function decode_uint8 (s: seq int) : int =
+ match s with
+ | L.Cons b0 (L.Nil) ->
+ b0 * 0x1
+ | _ -> 0
+ end
+
+ function decode_sint8 (s: seq int) : int =
+ to_sint8 (decode_uint8 s)
+
+ function encode_uint8 (v: int) : seq int =
+ (L.Cons (mod v 0x100) L.Nil)
+
+ function encode_sint8 (v: int) : seq int =
+ encode_uint8 (to_uint8 v)
+
+ lemma decode_uint8_encode_uint8:
+ forall v: int [decode_uint8 (encode_uint8 v)].
+ is_uint8 v -> decode_uint8 (encode_uint8 v) = v
+
+ lemma decode_sint8_encode_uint8:
+ forall v: int [decode_sint8 (encode_uint8 v)].
+ is_uint8 v -> decode_sint8 (encode_uint8 v) = to_sint8 v
+
+ lemma decode_uint8_encode_sint8:
+ forall v: int [decode_uint8 (encode_sint8 v)].
+ is_sint8 v -> decode_uint8 (encode_sint8 v) = to_uint8 v
+
+ lemma decode_sint8_encode_sint8:
+ forall v: int [decode_sint8 (encode_sint8 v)].
+ is_sint8 v -> decode_sint8 (encode_sint8 v) = v
+
+ function decode_uint16 (s: seq int) : int =
+ match s with
+ | L.Cons b0 (L.Cons b1 (L.Nil)) ->
+ b0 * 0x1 + b1 * 0x100
+ | _ -> 0
+ end
+
+ function decode_sint16 (s: seq int) : int =
+ to_sint16 (decode_uint16 s)
+
+ function encode_uint16 (v: int) : seq int =
+ (L.Cons (mod v 0x100)
+ (L.Cons (mod (div v 0x100) 0x100) L.Nil))
+
+ function encode_sint16 (v: int) : seq int =
+ encode_uint16 (to_uint16 v)
+
+ lemma decode_uint16_encode_uint16:
+ forall v: int [decode_uint16 (encode_uint16 v)].
+ is_uint16 v -> decode_uint16 (encode_uint16 v) = v
+
+ lemma decode_sint16_encode_uint16:
+ forall v: int [decode_sint16 (encode_uint16 v)].
+ is_uint16 v -> decode_sint16 (encode_uint16 v) = to_sint16 v
+
+ lemma decode_uint16_encode_sint16:
+ forall v: int [decode_uint16 (encode_sint16 v)].
+ is_sint16 v -> decode_uint16 (encode_sint16 v) = to_uint16 v
+
+ lemma decode_sint16_encode_sint16:
+ forall v: int [decode_sint16 (encode_sint16 v)].
+ is_sint16 v -> decode_sint16 (encode_sint16 v) = v
+
+ function decode_uint32 (s: seq int) : int =
+ match s with
+ | L.Cons b0 (L.Cons b1 (L.Cons b2 (L.Cons b3 (L.Nil)))) ->
+ b0 * 0x1 + b1 * 0x100 + b2 * 0x10000 + b3 * 0x1000000
+ | _ -> 0
+ end
+
+ function decode_sint32 (s: seq int) : int =
+ to_sint32 (decode_uint32 s)
+
+ function encode_uint32 (v: int) : seq int =
+ (L.Cons (mod v 0x100)
+ (L.Cons (mod (div v 0x100) 0x100)
+ (L.Cons (mod (div v 0x10000) 0x100)
+ (L.Cons (mod (div v 0x1000000) 0x100) L.Nil))))
+
+ function encode_sint32 (v: int) : seq int =
+ encode_uint32 (to_uint32 v)
+
+ lemma decode_uint32_encode_uint32:
+ forall v: int [decode_uint32 (encode_uint32 v)].
+ is_uint32 v -> decode_uint32 (encode_uint32 v) = v
+
+ lemma decode_sint32_encode_uint32:
+ forall v: int [decode_sint32 (encode_uint32 v)].
+ is_uint32 v -> decode_sint32 (encode_uint32 v) = to_sint32 v
+
+ lemma decode_uint32_encode_sint32:
+ forall v: int [decode_uint32 (encode_sint32 v)].
+ is_sint32 v -> decode_uint32 (encode_sint32 v) = to_uint32 v
+
+ lemma decode_sint32_encode_sint32:
+ forall v: int [decode_sint32 (encode_sint32 v)].
+ is_sint32 v -> decode_sint32 (encode_sint32 v) = v
+
+ function decode_uint64 (s: seq int) : int =
+ match s with
+ | L.Cons b0 (L.Cons b1 (L.Cons b2 (L.Cons b3 (L.Cons b4 (L.Cons b5 (L.Cons b6 (L.Cons b7 (L.Nil)))))))) ->
+ b0 * 0x1 + b1 * 0x100 + b2 * 0x10000 + b3 * 0x1000000 + b4 * 0x100000000 + b5 * 0x10000000000 + b6 * 0x1000000000000 + b7 * 0x100000000000000
+ | _ -> 0
+ end
+
+ function decode_sint64 (s: seq int) : int =
+ to_sint64 (decode_uint64 s)
+
+ function encode_uint64 (v: int) : seq int =
+ (L.Cons (mod v 0x100)
+ (L.Cons (mod (div v 0x100) 0x100)
+ (L.Cons (mod (div v 0x10000) 0x100)
+ (L.Cons (mod (div v 0x1000000) 0x100)
+ (L.Cons (mod (div v 0x100000000) 0x100)
+ (L.Cons (mod (div v 0x10000000000) 0x100)
+ (L.Cons (mod (div v 0x1000000000000) 0x100)
+ (L.Cons (mod (div v 0x100000000000000) 0x100) L.Nil))))))))
+
+ function encode_sint64 (v: int) : seq int =
+ encode_uint64 (to_uint64 v)
+
+ lemma decode_uint64_encode_uint64:
+ forall v: int [decode_uint64 (encode_uint64 v)].
+ is_uint64 v -> decode_uint64 (encode_uint64 v) = v
+
+ lemma decode_sint64_encode_uint64:
+ forall v: int [decode_sint64 (encode_uint64 v)].
+ is_uint64 v -> decode_sint64 (encode_uint64 v) = to_sint64 v
+
+ lemma decode_uint64_encode_sint64:
+ forall v: int [decode_uint64 (encode_sint64 v)].
+ is_sint64 v -> decode_uint64 (encode_sint64 v) = to_uint64 v
+
+ lemma decode_sint64_encode_sint64:
+ forall v: int [decode_sint64 (encode_sint64 v)].
+ is_sint64 v -> decode_sint64 (encode_sint64 v) = v
+
+
+end
+
+module InitCodec
+ use bool.Bool
+ use frama_c_wp.sequence.Seq
+
+ function decode_init8 (s: seq bool) : bool =
+ match s with
+ | L.Cons b0 (L.Nil) ->
+ b0
+ | _ -> false
+ end
+
+ function encode_init8 (v: bool) : seq bool =
+ create v 1
+
+ lemma decode_init8_encode_init8:
+ forall v: bool [decode_init8 (encode_init8 v)].
+ decode_init8 (encode_init8 v) = v
+
+ function decode_init16 (s: seq bool) : bool =
+ match s with
+ | L.Cons b0 (L.Cons b1 (L.Nil)) ->
+ b0 && b1
+ | _ -> false
+ end
+
+ function encode_init16 (v: bool) : seq bool =
+ create v 2
+
+ lemma decode_init16_encode_init16:
+ forall v: bool [decode_init16 (encode_init16 v)].
+ decode_init16 (encode_init16 v) = v
+
+ function decode_init32 (s: seq bool) : bool =
+ match s with
+ | L.Cons b0 (L.Cons b1 (L.Cons b2 (L.Cons b3 (L.Nil)))) ->
+ b0 && b1 && b2 && b3
+ | _ -> false
+ end
+
+ function encode_init32 (v: bool) : seq bool =
+ create v 4
+
+ lemma decode_init32_encode_init32:
+ forall v: bool [decode_init32 (encode_init32 v)].
+ decode_init32 (encode_init32 v) = v
+
+ function decode_init64 (s: seq bool) : bool =
+ match s with
+ | L.Cons b0 (L.Cons b1 (L.Cons b2 (L.Cons b3 (L.Cons b4 (L.Cons b5 (L.Cons b6 (L.Cons b7 (L.Nil)))))))) ->
+ b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7
+ | _ -> false
+ end
+
+ function encode_init64 (v: bool) : seq bool =
+ create v 8
+
+ lemma decode_init64_encode_init64:
+ forall v: bool [decode_init64 (encode_init64 v)].
+ decode_init64 (encode_init64 v) = v
+
+
+end
+
+module Offset
+ use int.Int
+ type offset = int
+
+ predicate sepoffset (po: offset) (lp: int) (qo: offset) (lq: int) =
+ qo + lq <= po \/ po + lp <= qo
+
+end
+
+module RWBytes
+ use int.Int
+ use map.Map as M
+ use frama_c_wp.sequence.Seq as S
+ use Offset
+
+ type seq 'a = S.seq 'a
+ type block 'a = M.map int 'a
+
+ function bwrite_seq (b:block 'a) (o: int) (s: seq 'a) : block 'a =
+ match s with
+ | S.L.Nil -> b
+ | S.L.Cons h tl -> M.(set (bwrite_seq b (o+1) tl) o h)
+ end
+
+ predicate beq_blocks (b1 b2: block 'a) (o: int) (l: int) =
+ forall i: int. o <= i < o + l -> M.(get b1 i) = M.(get b2 i)
+
+ function bread_8bits (b: block 'a) (o: int) : seq 'a =
+ (S.L.Cons M.(b[o ]) S.L.Nil)
+
+ function bread_16bits (b: block 'a) (o: int) : seq 'a =
+ (S.L.Cons M.(b[o ])
+ (S.L.Cons M.(b[o+1]) S.L.Nil))
+
+ function bread_32bits (b: block 'a) (o: int) : seq 'a =
+ (S.L.Cons M.(b[o ])
+ (S.L.Cons M.(b[o+1])
+ (S.L.Cons M.(b[o+2])
+ (S.L.Cons M.(b[o+3]) S.L.Nil))))
+
+ function bread_64bits (b: block 'a) (o: int) : seq 'a =
+ (S.L.Cons M.(b[o ])
+ (S.L.Cons M.(b[o+1])
+ (S.L.Cons M.(b[o+2])
+ (S.L.Cons M.(b[o+3])
+ (S.L.Cons M.(b[o+4])
+ (S.L.Cons M.(b[o+5])
+ (S.L.Cons M.(b[o+6])
+ (S.L.Cons M.(b[o+7]) S.L.Nil))))))))
+
+ function bwrite_8bits (b: block 'a) (o: int) (s: seq 'a) : block 'a =
+ match s with
+ | S.L.Cons b0 (_) ->
+ M.(set b o b0)
+ | _ -> b
+ end
+
+ function bwrite_16bits (b: block 'a) (o: int) (s: seq 'a) : block 'a =
+ match s with
+ | S.L.Cons b0 (S.L.Cons b1 (_)) ->
+ M.(set (set b (o+1) b1) o b0)
+ | _ -> b
+ end
+
+ function bwrite_32bits (b: block 'a) (o: int) (s: seq 'a) : block 'a =
+ match s with
+ | S.L.Cons b0 (S.L.Cons b1 (S.L.Cons b2 (S.L.Cons b3 (_)))) ->
+ M.(set (set (set (set b (o+3) b3) (o+2) b2) (o+1) b1) o b0)
+ | _ -> b
+ end
+
+ function bwrite_64bits (b: block 'a) (o: int) (s: seq 'a) : block 'a =
+ match s with
+ | S.L.Cons b0 (S.L.Cons b1 (S.L.Cons b2 (S.L.Cons b3 (S.L.Cons b4 (S.L.Cons b5 (S.L.Cons b6 (S.L.Cons b7 (_)))))))) ->
+ M.(set (set (set (set (set (set (set (set b (o+7) b7) (o+6) b6) (o+5) b5) (o+4) b4) (o+3) b3) (o+2) b2) (o+1) b1) o b0)
+ | _ -> b
+ end
+
+ lemma bread_8bits_bwrite_8bits_eq:
+ forall b: block 'a, o: int, s: seq 'a [bread_8bits (bwrite_8bits b o s) o].
+ S.length s = 1 ->
+ bread_8bits (bwrite_8bits b o s) o = s
+
+ let rec lemma bread_8bits_bwrite_seq_sep (b: block 'a)(or ow: int)(s: seq 'a)
+ requires { sepoffset ow (S.length s) or 1 }
+ ensures { bread_8bits (bwrite_seq b ow s) or = bread_8bits b or }
+ = match s with
+ | S.L.Nil -> ()
+ | S.L.Cons _ tl -> bread_8bits_bwrite_seq_sep b or (ow + 1) tl
+ end
+
+ lemma bread_8bits_bwrite_8bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_8bits (bwrite_8bits b ow s) or].
+ sepoffset ow 1 or 1 ->
+ bread_8bits (bwrite_8bits b ow s) or = bread_8bits b or
+
+ lemma bread_8bits_bwrite_16bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_8bits (bwrite_16bits b ow s) or].
+ sepoffset ow 2 or 1 ->
+ bread_8bits (bwrite_16bits b ow s) or = bread_8bits b or
+
+ lemma bread_8bits_bwrite_32bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_8bits (bwrite_32bits b ow s) or].
+ sepoffset ow 4 or 1 ->
+ bread_8bits (bwrite_32bits b ow s) or = bread_8bits b or
+
+ lemma bread_8bits_bwrite_64bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_8bits (bwrite_64bits b ow s) or].
+ sepoffset ow 8 or 1 ->
+ bread_8bits (bwrite_64bits b ow s) or = bread_8bits b or
+
+ lemma bread_16bits_bwrite_16bits_eq:
+ forall b: block 'a, o: int, s: seq 'a [bread_16bits (bwrite_16bits b o s) o].
+ S.length s = 2 ->
+ bread_16bits (bwrite_16bits b o s) o = s
+
+ let rec lemma bread_16bits_bwrite_seq_sep (b: block 'a)(or ow: int)(s: seq 'a)
+ requires { sepoffset ow (S.length s) or 2 }
+ ensures { bread_16bits (bwrite_seq b ow s) or = bread_16bits b or }
+ = match s with
+ | S.L.Nil -> ()
+ | S.L.Cons _ tl -> bread_16bits_bwrite_seq_sep b or (ow + 1) tl
+ end
+
+ lemma bread_16bits_bwrite_8bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_16bits (bwrite_8bits b ow s) or].
+ sepoffset ow 1 or 2 ->
+ bread_16bits (bwrite_8bits b ow s) or = bread_16bits b or
+
+ lemma bread_16bits_bwrite_16bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_16bits (bwrite_16bits b ow s) or].
+ sepoffset ow 2 or 2 ->
+ bread_16bits (bwrite_16bits b ow s) or = bread_16bits b or
+
+ lemma bread_16bits_bwrite_32bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_16bits (bwrite_32bits b ow s) or].
+ sepoffset ow 4 or 2 ->
+ bread_16bits (bwrite_32bits b ow s) or = bread_16bits b or
+
+ lemma bread_16bits_bwrite_64bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_16bits (bwrite_64bits b ow s) or].
+ sepoffset ow 8 or 2 ->
+ bread_16bits (bwrite_64bits b ow s) or = bread_16bits b or
+
+ lemma bread_32bits_bwrite_32bits_eq:
+ forall b: block 'a, o: int, s: seq 'a [bread_32bits (bwrite_32bits b o s) o].
+ S.length s = 4 ->
+ bread_32bits (bwrite_32bits b o s) o = s
+
+ let rec lemma bread_32bits_bwrite_seq_sep (b: block 'a)(or ow: int)(s: seq 'a)
+ requires { sepoffset ow (S.length s) or 4 }
+ ensures { bread_32bits (bwrite_seq b ow s) or = bread_32bits b or }
+ = match s with
+ | S.L.Nil -> ()
+ | S.L.Cons _ tl -> bread_32bits_bwrite_seq_sep b or (ow + 1) tl
+ end
+
+ lemma bread_32bits_bwrite_8bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_32bits (bwrite_8bits b ow s) or].
+ sepoffset ow 1 or 4 ->
+ bread_32bits (bwrite_8bits b ow s) or = bread_32bits b or
+
+ lemma bread_32bits_bwrite_16bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_32bits (bwrite_16bits b ow s) or].
+ sepoffset ow 2 or 4 ->
+ bread_32bits (bwrite_16bits b ow s) or = bread_32bits b or
+
+ lemma bread_32bits_bwrite_32bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_32bits (bwrite_32bits b ow s) or].
+ sepoffset ow 4 or 4 ->
+ bread_32bits (bwrite_32bits b ow s) or = bread_32bits b or
+
+ lemma bread_32bits_bwrite_64bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_32bits (bwrite_64bits b ow s) or].
+ sepoffset ow 8 or 4 ->
+ bread_32bits (bwrite_64bits b ow s) or = bread_32bits b or
+
+ lemma bread_64bits_bwrite_64bits_eq:
+ forall b: block 'a, o: int, s: seq 'a [bread_64bits (bwrite_64bits b o s) o].
+ S.length s = 8 ->
+ bread_64bits (bwrite_64bits b o s) o = s
+
+ let rec lemma bread_64bits_bwrite_seq_sep (b: block 'a)(or ow: int)(s: seq 'a)
+ requires { sepoffset ow (S.length s) or 8 }
+ ensures { bread_64bits (bwrite_seq b ow s) or = bread_64bits b or }
+ = match s with
+ | S.L.Nil -> ()
+ | S.L.Cons _ tl -> bread_64bits_bwrite_seq_sep b or (ow + 1) tl
+ end
+
+ lemma bread_64bits_bwrite_8bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_64bits (bwrite_8bits b ow s) or].
+ sepoffset ow 1 or 8 ->
+ bread_64bits (bwrite_8bits b ow s) or = bread_64bits b or
+
+ lemma bread_64bits_bwrite_16bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_64bits (bwrite_16bits b ow s) or].
+ sepoffset ow 2 or 8 ->
+ bread_64bits (bwrite_16bits b ow s) or = bread_64bits b or
+
+ lemma bread_64bits_bwrite_32bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_64bits (bwrite_32bits b ow s) or].
+ sepoffset ow 4 or 8 ->
+ bread_64bits (bwrite_32bits b ow s) or = bread_64bits b or
+
+ lemma bread_64bits_bwrite_64bits_sep:
+ forall b: block 'a, or ow: int, s: seq 'a [bread_64bits (bwrite_64bits b ow s) or].
+ sepoffset ow 8 or 8 ->
+ bread_64bits (bwrite_64bits b ow s) or = bread_64bits b or
+
+
+end
+
+module ValueBlockRW
+ use int.Int
+ use frama_c_wp.cint.Cint
+ use ValueCodec
+ use Offset
+ use RWBytes
+
+ type vblock = block int
+
+ function bread_uint8 (b: vblock) (o: int) : int =
+ decode_uint8 (bread_8bits b o)
+
+ function bread_uint16 (b: vblock) (o: int) : int =
+ decode_uint16 (bread_16bits b o)
+
+ function bread_uint32 (b: vblock) (o: int) : int =
+ decode_uint32 (bread_32bits b o)
+
+ function bread_uint64 (b: vblock) (o: int) : int =
+ decode_uint64 (bread_64bits b o)
+
+ function bread_sint8 (b: vblock) (o: int) : int =
+ decode_sint8 (bread_8bits b o)
+
+ function bread_sint16 (b: vblock) (o: int) : int =
+ decode_sint16 (bread_16bits b o)
+
+ function bread_sint32 (b: vblock) (o: int) : int =
+ decode_sint32 (bread_32bits b o)
+
+ function bread_sint64 (b: vblock) (o: int) : int =
+ decode_sint64 (bread_64bits b o)
+
+ function bwrite_uint8 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_8bits b o (encode_uint8 v)
+
+ function bwrite_uint16 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_16bits b o (encode_uint16 v)
+
+ function bwrite_uint32 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_32bits b o (encode_uint32 v)
+
+ function bwrite_uint64 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_64bits b o (encode_uint64 v)
+
+ function bwrite_sint8 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_8bits b o (encode_sint8 v)
+
+ function bwrite_sint16 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_16bits b o (encode_sint16 v)
+
+ function bwrite_sint32 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_32bits b o (encode_sint32 v)
+
+ function bwrite_sint64 (b: vblock) (o: int) (v: int) : vblock =
+ bwrite_64bits b o (encode_sint64 v)
+
+ lemma bread_uint8_bwrite_uint8_eq:
+ forall b: vblock, o: int, v: int [bread_uint8 (bwrite_uint8 b o v) o].
+ is_uint8 v ->
+ bread_uint8 (bwrite_uint8 b o v) o = v
+
+ lemma bread_uint8_bwrite_sint8_eq:
+ forall b: vblock, o: int, v: int [bread_uint8 (bwrite_sint8 b o v) o].
+ is_sint8 v ->
+ bread_uint8 (bwrite_sint8 b o v) o = to_uint8 v
+
+ lemma bread_uint8_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_uint8 (bwrite_seq b ho u) or].
+ sepoffset or 1 ho (Seq.length u) ->
+ bread_uint8 (bwrite_seq b ho u) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 1 ->
+ bread_uint8 (bwrite_uint8 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 1 ->
+ bread_uint8 (bwrite_uint16 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 1 ->
+ bread_uint8 (bwrite_uint32 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 1 ->
+ bread_uint8 (bwrite_uint64 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 1 ->
+ bread_uint8 (bwrite_sint8 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 1 ->
+ bread_uint8 (bwrite_sint16 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 1 ->
+ bread_uint8 (bwrite_sint32 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint8_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint8 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 1 ->
+ bread_uint8 (bwrite_sint64 b ow v) or = bread_uint8 b or
+
+ lemma bread_uint16_bwrite_uint16_eq:
+ forall b: vblock, o: int, v: int [bread_uint16 (bwrite_uint16 b o v) o].
+ is_uint16 v ->
+ bread_uint16 (bwrite_uint16 b o v) o = v
+
+ lemma bread_uint16_bwrite_sint16_eq:
+ forall b: vblock, o: int, v: int [bread_uint16 (bwrite_sint16 b o v) o].
+ is_sint16 v ->
+ bread_uint16 (bwrite_sint16 b o v) o = to_uint16 v
+
+ lemma bread_uint16_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_uint16 (bwrite_seq b ho u) or].
+ sepoffset or 2 ho (Seq.length u) ->
+ bread_uint16 (bwrite_seq b ho u) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 2 ->
+ bread_uint16 (bwrite_uint8 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 2 ->
+ bread_uint16 (bwrite_uint16 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 2 ->
+ bread_uint16 (bwrite_uint32 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 2 ->
+ bread_uint16 (bwrite_uint64 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 2 ->
+ bread_uint16 (bwrite_sint8 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 2 ->
+ bread_uint16 (bwrite_sint16 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 2 ->
+ bread_uint16 (bwrite_sint32 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint16_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint16 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 2 ->
+ bread_uint16 (bwrite_sint64 b ow v) or = bread_uint16 b or
+
+ lemma bread_uint32_bwrite_uint32_eq:
+ forall b: vblock, o: int, v: int [bread_uint32 (bwrite_uint32 b o v) o].
+ is_uint32 v ->
+ bread_uint32 (bwrite_uint32 b o v) o = v
+
+ lemma bread_uint32_bwrite_sint32_eq:
+ forall b: vblock, o: int, v: int [bread_uint32 (bwrite_sint32 b o v) o].
+ is_sint32 v ->
+ bread_uint32 (bwrite_sint32 b o v) o = to_uint32 v
+
+ lemma bread_uint32_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_uint32 (bwrite_seq b ho u) or].
+ sepoffset or 4 ho (Seq.length u) ->
+ bread_uint32 (bwrite_seq b ho u) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 4 ->
+ bread_uint32 (bwrite_uint8 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 4 ->
+ bread_uint32 (bwrite_uint16 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 4 ->
+ bread_uint32 (bwrite_uint32 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 4 ->
+ bread_uint32 (bwrite_uint64 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 4 ->
+ bread_uint32 (bwrite_sint8 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 4 ->
+ bread_uint32 (bwrite_sint16 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 4 ->
+ bread_uint32 (bwrite_sint32 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint32_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint32 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 4 ->
+ bread_uint32 (bwrite_sint64 b ow v) or = bread_uint32 b or
+
+ lemma bread_uint64_bwrite_uint64_eq:
+ forall b: vblock, o: int, v: int [bread_uint64 (bwrite_uint64 b o v) o].
+ is_uint64 v ->
+ bread_uint64 (bwrite_uint64 b o v) o = v
+
+ lemma bread_uint64_bwrite_sint64_eq:
+ forall b: vblock, o: int, v: int [bread_uint64 (bwrite_sint64 b o v) o].
+ is_sint64 v ->
+ bread_uint64 (bwrite_sint64 b o v) o = to_uint64 v
+
+ lemma bread_uint64_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_uint64 (bwrite_seq b ho u) or].
+ sepoffset or 8 ho (Seq.length u) ->
+ bread_uint64 (bwrite_seq b ho u) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 8 ->
+ bread_uint64 (bwrite_uint8 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 8 ->
+ bread_uint64 (bwrite_uint16 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 8 ->
+ bread_uint64 (bwrite_uint32 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 8 ->
+ bread_uint64 (bwrite_uint64 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 8 ->
+ bread_uint64 (bwrite_sint8 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 8 ->
+ bread_uint64 (bwrite_sint16 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 8 ->
+ bread_uint64 (bwrite_sint32 b ow v) or = bread_uint64 b or
+
+ lemma bread_uint64_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_uint64 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 8 ->
+ bread_uint64 (bwrite_sint64 b ow v) or = bread_uint64 b or
+
+ lemma bread_sint8_bwrite_sint8_eq:
+ forall b: vblock, o: int, v: int [bread_sint8 (bwrite_sint8 b o v) o].
+ is_sint8 v ->
+ bread_sint8 (bwrite_sint8 b o v) o = v
+
+ lemma bread_sint8_bwrite_uint8_eq:
+ forall b: vblock, o: int, v: int [bread_sint8 (bwrite_uint8 b o v) o].
+ is_uint8 v ->
+ bread_sint8 (bwrite_uint8 b o v) o = to_sint8 v
+
+ lemma bread_sint8_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_sint8 (bwrite_seq b ho u) or].
+ sepoffset or 1 ho (Seq.length u) ->
+ bread_sint8 (bwrite_seq b ho u) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 1 ->
+ bread_sint8 (bwrite_uint8 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 1 ->
+ bread_sint8 (bwrite_uint16 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 1 ->
+ bread_sint8 (bwrite_uint32 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 1 ->
+ bread_sint8 (bwrite_uint64 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 1 ->
+ bread_sint8 (bwrite_sint8 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 1 ->
+ bread_sint8 (bwrite_sint16 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 1 ->
+ bread_sint8 (bwrite_sint32 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint8_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint8 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 1 ->
+ bread_sint8 (bwrite_sint64 b ow v) or = bread_sint8 b or
+
+ lemma bread_sint16_bwrite_sint16_eq:
+ forall b: vblock, o: int, v: int [bread_sint16 (bwrite_sint16 b o v) o].
+ is_sint16 v ->
+ bread_sint16 (bwrite_sint16 b o v) o = v
+
+ lemma bread_sint16_bwrite_uint16_eq:
+ forall b: vblock, o: int, v: int [bread_sint16 (bwrite_uint16 b o v) o].
+ is_uint16 v ->
+ bread_sint16 (bwrite_uint16 b o v) o = to_sint16 v
+
+ lemma bread_sint16_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_sint16 (bwrite_seq b ho u) or].
+ sepoffset or 2 ho (Seq.length u) ->
+ bread_sint16 (bwrite_seq b ho u) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 2 ->
+ bread_sint16 (bwrite_uint8 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 2 ->
+ bread_sint16 (bwrite_uint16 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 2 ->
+ bread_sint16 (bwrite_uint32 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 2 ->
+ bread_sint16 (bwrite_uint64 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 2 ->
+ bread_sint16 (bwrite_sint8 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 2 ->
+ bread_sint16 (bwrite_sint16 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 2 ->
+ bread_sint16 (bwrite_sint32 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint16_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint16 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 2 ->
+ bread_sint16 (bwrite_sint64 b ow v) or = bread_sint16 b or
+
+ lemma bread_sint32_bwrite_sint32_eq:
+ forall b: vblock, o: int, v: int [bread_sint32 (bwrite_sint32 b o v) o].
+ is_sint32 v ->
+ bread_sint32 (bwrite_sint32 b o v) o = v
+
+ lemma bread_sint32_bwrite_uint32_eq:
+ forall b: vblock, o: int, v: int [bread_sint32 (bwrite_uint32 b o v) o].
+ is_uint32 v ->
+ bread_sint32 (bwrite_uint32 b o v) o = to_sint32 v
+
+ lemma bread_sint32_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_sint32 (bwrite_seq b ho u) or].
+ sepoffset or 4 ho (Seq.length u) ->
+ bread_sint32 (bwrite_seq b ho u) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 4 ->
+ bread_sint32 (bwrite_uint8 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 4 ->
+ bread_sint32 (bwrite_uint16 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 4 ->
+ bread_sint32 (bwrite_uint32 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 4 ->
+ bread_sint32 (bwrite_uint64 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 4 ->
+ bread_sint32 (bwrite_sint8 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 4 ->
+ bread_sint32 (bwrite_sint16 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 4 ->
+ bread_sint32 (bwrite_sint32 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint32_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint32 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 4 ->
+ bread_sint32 (bwrite_sint64 b ow v) or = bread_sint32 b or
+
+ lemma bread_sint64_bwrite_sint64_eq:
+ forall b: vblock, o: int, v: int [bread_sint64 (bwrite_sint64 b o v) o].
+ is_sint64 v ->
+ bread_sint64 (bwrite_sint64 b o v) o = v
+
+ lemma bread_sint64_bwrite_uint64_eq:
+ forall b: vblock, o: int, v: int [bread_sint64 (bwrite_uint64 b o v) o].
+ is_uint64 v ->
+ bread_sint64 (bwrite_uint64 b o v) o = to_sint64 v
+
+ lemma bread_sint64_bhavoc_sep:
+ forall b: vblock, u: S.seq int, or ho: int [bread_sint64 (bwrite_seq b ho u) or].
+ sepoffset or 8 ho (Seq.length u) ->
+ bread_sint64 (bwrite_seq b ho u) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_uint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_uint8 b ow v) or].
+ sepoffset ow 1 or 8 ->
+ bread_sint64 (bwrite_uint8 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_uint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_uint16 b ow v) or].
+ sepoffset ow 2 or 8 ->
+ bread_sint64 (bwrite_uint16 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_uint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_uint32 b ow v) or].
+ sepoffset ow 4 or 8 ->
+ bread_sint64 (bwrite_uint32 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_uint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_uint64 b ow v) or].
+ sepoffset ow 8 or 8 ->
+ bread_sint64 (bwrite_uint64 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_sint8_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_sint8 b ow v) or].
+ sepoffset ow 1 or 8 ->
+ bread_sint64 (bwrite_sint8 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_sint16_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_sint16 b ow v) or].
+ sepoffset ow 2 or 8 ->
+ bread_sint64 (bwrite_sint16 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_sint32_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_sint32 b ow v) or].
+ sepoffset ow 4 or 8 ->
+ bread_sint64 (bwrite_sint32 b ow v) or = bread_sint64 b or
+
+ lemma bread_sint64_bwrite_sint64_sep:
+ forall b: vblock, or ow: int, v: int [bread_sint64 (bwrite_sint64 b ow v) or].
+ sepoffset ow 8 or 8 ->
+ bread_sint64 (bwrite_sint64 b ow v) or = bread_sint64 b or
+
+
+end
+
+module InitBlockRW
+ use bool.Bool
+ use int.Int
+ use InitCodec
+ use Offset
+ use RWBytes
+
+ type iblock = block bool
+
+ predicate is_init_range(b: iblock) (o: int) (size: int) =
+ forall i: int. o <= i < o + size -> M.get b i = True
+
+ function bread_init8 (b: iblock) (o: int) : bool =
+ decode_init8 (bread_8bits b o)
+
+ function bread_init16 (b: iblock) (o: int) : bool =
+ decode_init16 (bread_16bits b o)
+
+ function bread_init32 (b: iblock) (o: int) : bool =
+ decode_init32 (bread_32bits b o)
+
+ function bread_init64 (b: iblock) (o: int) : bool =
+ decode_init64 (bread_64bits b o)
+
+ function bwrite_init8 (b: iblock) (o: int) (init: bool) : iblock =
+ bwrite_8bits b o (encode_init8 init)
+
+ function bwrite_init16 (b: iblock) (o: int) (init: bool) : iblock =
+ bwrite_16bits b o (encode_init16 init)
+
+ function bwrite_init32 (b: iblock) (o: int) (init: bool) : iblock =
+ bwrite_32bits b o (encode_init32 init)
+
+ function bwrite_init64 (b: iblock) (o: int) (init: bool) : iblock =
+ bwrite_64bits b o (encode_init64 init)
+
+ lemma bread_init8_bwrite_init8_eq:
+ forall b: iblock, o: int, init: bool [bread_init8 (bwrite_init8 b o init) o].
+ bread_init8 (bwrite_init8 b o init) o = init
+
+ lemma bread_init8_bhavoc_sep:
+ forall b: iblock, u: S.seq bool, or ho: int [bread_init8 (bwrite_seq b ho u) or].
+ sepoffset or 1 ho (Seq.length u) ->
+ bread_init8 (bwrite_seq b ho u) or = bread_init8 b or
+
+ lemma bread_init8_bwrite_init8_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init8 (bwrite_init8 b ow init) or].
+ sepoffset ow 1 or 1 ->
+ bread_init8 (bwrite_init8 b ow init) or = bread_init8 b or
+
+ lemma bread_init8_bwrite_init16_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init8 (bwrite_init16 b ow init) or].
+ sepoffset ow 2 or 1 ->
+ bread_init8 (bwrite_init16 b ow init) or = bread_init8 b or
+
+ lemma bread_init8_bwrite_init32_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init8 (bwrite_init32 b ow init) or].
+ sepoffset ow 4 or 1 ->
+ bread_init8 (bwrite_init32 b ow init) or = bread_init8 b or
+
+ lemma bread_init8_bwrite_init64_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init8 (bwrite_init64 b ow init) or].
+ sepoffset ow 8 or 1 ->
+ bread_init8 (bwrite_init64 b ow init) or = bread_init8 b or
+
+ lemma bread_init16_bwrite_init16_eq:
+ forall b: iblock, o: int, init: bool [bread_init16 (bwrite_init16 b o init) o].
+ bread_init16 (bwrite_init16 b o init) o = init
+
+ lemma bread_init16_bhavoc_sep:
+ forall b: iblock, u: S.seq bool, or ho: int [bread_init16 (bwrite_seq b ho u) or].
+ sepoffset or 2 ho (Seq.length u) ->
+ bread_init16 (bwrite_seq b ho u) or = bread_init16 b or
+
+ lemma bread_init16_bwrite_init8_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init16 (bwrite_init8 b ow init) or].
+ sepoffset ow 1 or 2 ->
+ bread_init16 (bwrite_init8 b ow init) or = bread_init16 b or
+
+ lemma bread_init16_bwrite_init16_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init16 (bwrite_init16 b ow init) or].
+ sepoffset ow 2 or 2 ->
+ bread_init16 (bwrite_init16 b ow init) or = bread_init16 b or
+
+ lemma bread_init16_bwrite_init32_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init16 (bwrite_init32 b ow init) or].
+ sepoffset ow 4 or 2 ->
+ bread_init16 (bwrite_init32 b ow init) or = bread_init16 b or
+
+ lemma bread_init16_bwrite_init64_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init16 (bwrite_init64 b ow init) or].
+ sepoffset ow 8 or 2 ->
+ bread_init16 (bwrite_init64 b ow init) or = bread_init16 b or
+
+ lemma bread_init32_bwrite_init32_eq:
+ forall b: iblock, o: int, init: bool [bread_init32 (bwrite_init32 b o init) o].
+ bread_init32 (bwrite_init32 b o init) o = init
+
+ lemma bread_init32_bhavoc_sep:
+ forall b: iblock, u: S.seq bool, or ho: int [bread_init32 (bwrite_seq b ho u) or].
+ sepoffset or 4 ho (Seq.length u) ->
+ bread_init32 (bwrite_seq b ho u) or = bread_init32 b or
+
+ lemma bread_init32_bwrite_init8_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init32 (bwrite_init8 b ow init) or].
+ sepoffset ow 1 or 4 ->
+ bread_init32 (bwrite_init8 b ow init) or = bread_init32 b or
+
+ lemma bread_init32_bwrite_init16_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init32 (bwrite_init16 b ow init) or].
+ sepoffset ow 2 or 4 ->
+ bread_init32 (bwrite_init16 b ow init) or = bread_init32 b or
+
+ lemma bread_init32_bwrite_init32_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init32 (bwrite_init32 b ow init) or].
+ sepoffset ow 4 or 4 ->
+ bread_init32 (bwrite_init32 b ow init) or = bread_init32 b or
+
+ lemma bread_init32_bwrite_init64_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init32 (bwrite_init64 b ow init) or].
+ sepoffset ow 8 or 4 ->
+ bread_init32 (bwrite_init64 b ow init) or = bread_init32 b or
+
+ lemma bread_init64_bwrite_init64_eq:
+ forall b: iblock, o: int, init: bool [bread_init64 (bwrite_init64 b o init) o].
+ bread_init64 (bwrite_init64 b o init) o = init
+
+ lemma bread_init64_bhavoc_sep:
+ forall b: iblock, u: S.seq bool, or ho: int [bread_init64 (bwrite_seq b ho u) or].
+ sepoffset or 8 ho (Seq.length u) ->
+ bread_init64 (bwrite_seq b ho u) or = bread_init64 b or
+
+ lemma bread_init64_bwrite_init8_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init64 (bwrite_init8 b ow init) or].
+ sepoffset ow 1 or 8 ->
+ bread_init64 (bwrite_init8 b ow init) or = bread_init64 b or
+
+ lemma bread_init64_bwrite_init16_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init64 (bwrite_init16 b ow init) or].
+ sepoffset ow 2 or 8 ->
+ bread_init64 (bwrite_init16 b ow init) or = bread_init64 b or
+
+ lemma bread_init64_bwrite_init32_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init64 (bwrite_init32 b ow init) or].
+ sepoffset ow 4 or 8 ->
+ bread_init64 (bwrite_init32 b ow init) or = bread_init64 b or
+
+ lemma bread_init64_bwrite_init64_sep:
+ forall b: iblock, or ow: int, init: bool [bread_init64 (bwrite_init64 b ow init) or].
+ sepoffset ow 8 or 8 ->
+ bread_init64 (bwrite_init64 b ow init) or = bread_init64 b or
+
+
+end
+
+module MemBytes
+ use int.Int
+ use map.Map
+ use frama_c_wp.cint.Cint
+ use frama_c_wp.memaddr.MemAddr
+ use frama_c_wp.sequence.Seq as S
+ use RWBytes
+ use ValueBlockRW as VB
+ use InitBlockRW as IB
+
+ type memory = map int (VB.vblock)
+ type init = map int (IB.iblock)
+
+ (* override memory cinits for MemBytes memory *)
+ predicate cinits (init)
+
+ function raw_get (m: map int (map int 'a)) (a: addr) : 'a =
+ get (get m a.base) a.offset
+
+ function raw_set (m: map int (map int 'a)) (a: addr) (v: 'a) : map int (map int 'a) =
+ set m a.base (set (get m a.base) a.offset v)
+
+ let rec function to_seq (a: map int 'a) (b e: int) : S.seq 'a
+ ensures { e - b >= 0 -> S.length result = e - b }
+ ensures { forall i: int. b <= i < e -> S.(result[i - b]) = get a i }
+ variant { e - b }
+ = if e <= b then S.L.Nil else S.L.Cons (get a b) (to_seq a (b+1) e)
+
+ function init_seq (s: int) : S.seq bool =
+ S.create True s
+
+ function havoc (fresh cur: map int (block 'a)) (a: addr) (size: int): map int (block 'a) =
+ set cur a.base (bwrite_seq (get cur a.base) a.offset (to_seq fresh[a.base] 0 size))
+
+ predicate eqmem (m1 m2: map int (block 'a)) (a: addr) (size: int) =
+ beq_blocks (get m1 a.base) (get m2 a.base) (a.offset) size
+
+ predicate is_init_range (i: init) (a: addr) (size: int) =
+ IB.is_init_range (get i a.base) a.offset size
+
+ function set_init_range (cur: init) (a: addr) (size: int) : init =
+ set cur a.base (bwrite_seq (get cur a.base) a.offset (init_seq size))
+
+ function read_uint8 (m: memory) (a: addr) : int =
+ VB.bread_uint8 m[a.base] a.offset
+
+ function read_uint16 (m: memory) (a: addr) : int =
+ VB.bread_uint16 m[a.base] a.offset
+
+ function read_uint32 (m: memory) (a: addr) : int =
+ VB.bread_uint32 m[a.base] a.offset
+
+ function read_uint64 (m: memory) (a: addr) : int =
+ VB.bread_uint64 m[a.base] a.offset
+
+ function read_sint8 (m: memory) (a: addr) : int =
+ VB.bread_sint8 m[a.base] a.offset
+
+ function read_sint16 (m: memory) (a: addr) : int =
+ VB.bread_sint16 m[a.base] a.offset
+
+ function read_sint32 (m: memory) (a: addr) : int =
+ VB.bread_sint32 m[a.base] a.offset
+
+ function read_sint64 (m: memory) (a: addr) : int =
+ VB.bread_sint64 m[a.base] a.offset
+
+ function write_uint8 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_uint8 m [a.base] a.offset v)
+
+ function write_uint16 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_uint16 m [a.base] a.offset v)
+
+ function write_uint32 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_uint32 m [a.base] a.offset v)
+
+ function write_uint64 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_uint64 m [a.base] a.offset v)
+
+ function write_sint8 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_sint8 m [a.base] a.offset v)
+
+ function write_sint16 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_sint16 m [a.base] a.offset v)
+
+ function write_sint32 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_sint32 m [a.base] a.offset v)
+
+ function write_sint64 (m: memory) (a: addr) (v: int) : memory =
+ set m a.base (VB.bwrite_sint64 m [a.base] a.offset v)
+
+ lemma read_uint8_write_uint8_eq:
+ forall m: memory, a: addr, v: int [read_uint8 (write_uint8 m a v) a].
+ is_uint8 v ->
+ read_uint8 (write_uint8 m a v) a = v
+
+ lemma read_uint8_write_sint8_eq:
+ forall m: memory, a: addr, v: int [read_uint8 (write_sint8 m a v) a].
+ is_sint8 v ->
+ read_uint8 (write_sint8 m a v) a = to_uint8 v
+
+ lemma read_uint8_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_uint8 (havoc fresh cur aw size) ar].
+ separated ar 1 aw size ->
+ read_uint8 (havoc fresh cur aw size) ar = read_uint8 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint8 nb ar.offset = VB.bread_uint8 ob ar.offset
+
+ lemma read_uint8_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_uint8 m aw v) ar].
+ separated aw 1 ar 1 ->
+ read_uint8 (write_uint8 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_uint16 m aw v) ar].
+ separated aw 2 ar 1 ->
+ read_uint8 (write_uint16 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_uint32 m aw v) ar].
+ separated aw 4 ar 1 ->
+ read_uint8 (write_uint32 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_uint64 m aw v) ar].
+ separated aw 8 ar 1 ->
+ read_uint8 (write_uint64 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_sint8 m aw v) ar].
+ separated aw 1 ar 1 ->
+ read_uint8 (write_sint8 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_sint16 m aw v) ar].
+ separated aw 2 ar 1 ->
+ read_uint8 (write_sint16 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_sint32 m aw v) ar].
+ separated aw 4 ar 1 ->
+ read_uint8 (write_sint32 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint8_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint8 (write_sint64 m aw v) ar].
+ separated aw 8 ar 1 ->
+ read_uint8 (write_sint64 m aw v) ar = read_uint8 m ar
+
+ lemma read_uint16_write_uint16_eq:
+ forall m: memory, a: addr, v: int [read_uint16 (write_uint16 m a v) a].
+ is_uint16 v ->
+ read_uint16 (write_uint16 m a v) a = v
+
+ lemma read_uint16_write_sint16_eq:
+ forall m: memory, a: addr, v: int [read_uint16 (write_sint16 m a v) a].
+ is_sint16 v ->
+ read_uint16 (write_sint16 m a v) a = to_uint16 v
+
+ lemma read_uint16_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_uint16 (havoc fresh cur aw size) ar].
+ separated ar 2 aw size ->
+ read_uint16 (havoc fresh cur aw size) ar = read_uint16 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint16 nb ar.offset = VB.bread_uint16 ob ar.offset
+
+ lemma read_uint16_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_uint8 m aw v) ar].
+ separated aw 1 ar 2 ->
+ read_uint16 (write_uint8 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_uint16 m aw v) ar].
+ separated aw 2 ar 2 ->
+ read_uint16 (write_uint16 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_uint32 m aw v) ar].
+ separated aw 4 ar 2 ->
+ read_uint16 (write_uint32 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_uint64 m aw v) ar].
+ separated aw 8 ar 2 ->
+ read_uint16 (write_uint64 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_sint8 m aw v) ar].
+ separated aw 1 ar 2 ->
+ read_uint16 (write_sint8 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_sint16 m aw v) ar].
+ separated aw 2 ar 2 ->
+ read_uint16 (write_sint16 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_sint32 m aw v) ar].
+ separated aw 4 ar 2 ->
+ read_uint16 (write_sint32 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint16_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint16 (write_sint64 m aw v) ar].
+ separated aw 8 ar 2 ->
+ read_uint16 (write_sint64 m aw v) ar = read_uint16 m ar
+
+ lemma read_uint32_write_uint32_eq:
+ forall m: memory, a: addr, v: int [read_uint32 (write_uint32 m a v) a].
+ is_uint32 v ->
+ read_uint32 (write_uint32 m a v) a = v
+
+ lemma read_uint32_write_sint32_eq:
+ forall m: memory, a: addr, v: int [read_uint32 (write_sint32 m a v) a].
+ is_sint32 v ->
+ read_uint32 (write_sint32 m a v) a = to_uint32 v
+
+ lemma read_uint32_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_uint32 (havoc fresh cur aw size) ar].
+ separated ar 4 aw size ->
+ read_uint32 (havoc fresh cur aw size) ar = read_uint32 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint32 nb ar.offset = VB.bread_uint32 ob ar.offset
+
+ lemma read_uint32_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_uint8 m aw v) ar].
+ separated aw 1 ar 4 ->
+ read_uint32 (write_uint8 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_uint16 m aw v) ar].
+ separated aw 2 ar 4 ->
+ read_uint32 (write_uint16 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_uint32 m aw v) ar].
+ separated aw 4 ar 4 ->
+ read_uint32 (write_uint32 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_uint64 m aw v) ar].
+ separated aw 8 ar 4 ->
+ read_uint32 (write_uint64 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_sint8 m aw v) ar].
+ separated aw 1 ar 4 ->
+ read_uint32 (write_sint8 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_sint16 m aw v) ar].
+ separated aw 2 ar 4 ->
+ read_uint32 (write_sint16 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_sint32 m aw v) ar].
+ separated aw 4 ar 4 ->
+ read_uint32 (write_sint32 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint32_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint32 (write_sint64 m aw v) ar].
+ separated aw 8 ar 4 ->
+ read_uint32 (write_sint64 m aw v) ar = read_uint32 m ar
+
+ lemma read_uint64_write_uint64_eq:
+ forall m: memory, a: addr, v: int [read_uint64 (write_uint64 m a v) a].
+ is_uint64 v ->
+ read_uint64 (write_uint64 m a v) a = v
+
+ lemma read_uint64_write_sint64_eq:
+ forall m: memory, a: addr, v: int [read_uint64 (write_sint64 m a v) a].
+ is_sint64 v ->
+ read_uint64 (write_sint64 m a v) a = to_uint64 v
+
+ lemma read_uint64_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_uint64 (havoc fresh cur aw size) ar].
+ separated ar 8 aw size ->
+ read_uint64 (havoc fresh cur aw size) ar = read_uint64 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint64 nb ar.offset = VB.bread_uint64 ob ar.offset
+
+ lemma read_uint64_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_uint8 m aw v) ar].
+ separated aw 1 ar 8 ->
+ read_uint64 (write_uint8 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_uint16 m aw v) ar].
+ separated aw 2 ar 8 ->
+ read_uint64 (write_uint16 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_uint32 m aw v) ar].
+ separated aw 4 ar 8 ->
+ read_uint64 (write_uint32 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_uint64 m aw v) ar].
+ separated aw 8 ar 8 ->
+ read_uint64 (write_uint64 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_sint8 m aw v) ar].
+ separated aw 1 ar 8 ->
+ read_uint64 (write_sint8 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_sint16 m aw v) ar].
+ separated aw 2 ar 8 ->
+ read_uint64 (write_sint16 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_sint32 m aw v) ar].
+ separated aw 4 ar 8 ->
+ read_uint64 (write_sint32 m aw v) ar = read_uint64 m ar
+
+ lemma read_uint64_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_uint64 (write_sint64 m aw v) ar].
+ separated aw 8 ar 8 ->
+ read_uint64 (write_sint64 m aw v) ar = read_uint64 m ar
+
+ lemma read_sint8_write_sint8_eq:
+ forall m: memory, a: addr, v: int [read_sint8 (write_sint8 m a v) a].
+ is_sint8 v ->
+ read_sint8 (write_sint8 m a v) a = v
+
+ lemma read_sint8_write_uint8_eq:
+ forall m: memory, a: addr, v: int [read_sint8 (write_uint8 m a v) a].
+ is_uint8 v ->
+ read_sint8 (write_uint8 m a v) a = to_sint8 v
+
+ lemma read_sint8_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_sint8 (havoc fresh cur aw size) ar].
+ separated ar 1 aw size ->
+ read_sint8 (havoc fresh cur aw size) ar = read_sint8 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint8 nb ar.offset = VB.bread_uint8 ob ar.offset
+
+ lemma read_sint8_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_uint8 m aw v) ar].
+ separated aw 1 ar 1 ->
+ read_sint8 (write_uint8 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_uint16 m aw v) ar].
+ separated aw 2 ar 1 ->
+ read_sint8 (write_uint16 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_uint32 m aw v) ar].
+ separated aw 4 ar 1 ->
+ read_sint8 (write_uint32 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_uint64 m aw v) ar].
+ separated aw 8 ar 1 ->
+ read_sint8 (write_uint64 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_sint8 m aw v) ar].
+ separated aw 1 ar 1 ->
+ read_sint8 (write_sint8 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_sint16 m aw v) ar].
+ separated aw 2 ar 1 ->
+ read_sint8 (write_sint16 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_sint32 m aw v) ar].
+ separated aw 4 ar 1 ->
+ read_sint8 (write_sint32 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint8_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint8 (write_sint64 m aw v) ar].
+ separated aw 8 ar 1 ->
+ read_sint8 (write_sint64 m aw v) ar = read_sint8 m ar
+
+ lemma read_sint16_write_sint16_eq:
+ forall m: memory, a: addr, v: int [read_sint16 (write_sint16 m a v) a].
+ is_sint16 v ->
+ read_sint16 (write_sint16 m a v) a = v
+
+ lemma read_sint16_write_uint16_eq:
+ forall m: memory, a: addr, v: int [read_sint16 (write_uint16 m a v) a].
+ is_uint16 v ->
+ read_sint16 (write_uint16 m a v) a = to_sint16 v
+
+ lemma read_sint16_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_sint16 (havoc fresh cur aw size) ar].
+ separated ar 2 aw size ->
+ read_sint16 (havoc fresh cur aw size) ar = read_sint16 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint16 nb ar.offset = VB.bread_uint16 ob ar.offset
+
+ lemma read_sint16_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_uint8 m aw v) ar].
+ separated aw 1 ar 2 ->
+ read_sint16 (write_uint8 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_uint16 m aw v) ar].
+ separated aw 2 ar 2 ->
+ read_sint16 (write_uint16 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_uint32 m aw v) ar].
+ separated aw 4 ar 2 ->
+ read_sint16 (write_uint32 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_uint64 m aw v) ar].
+ separated aw 8 ar 2 ->
+ read_sint16 (write_uint64 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_sint8 m aw v) ar].
+ separated aw 1 ar 2 ->
+ read_sint16 (write_sint8 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_sint16 m aw v) ar].
+ separated aw 2 ar 2 ->
+ read_sint16 (write_sint16 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_sint32 m aw v) ar].
+ separated aw 4 ar 2 ->
+ read_sint16 (write_sint32 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint16_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint16 (write_sint64 m aw v) ar].
+ separated aw 8 ar 2 ->
+ read_sint16 (write_sint64 m aw v) ar = read_sint16 m ar
+
+ lemma read_sint32_write_sint32_eq:
+ forall m: memory, a: addr, v: int [read_sint32 (write_sint32 m a v) a].
+ is_sint32 v ->
+ read_sint32 (write_sint32 m a v) a = v
+
+ lemma read_sint32_write_uint32_eq:
+ forall m: memory, a: addr, v: int [read_sint32 (write_uint32 m a v) a].
+ is_uint32 v ->
+ read_sint32 (write_uint32 m a v) a = to_sint32 v
+
+ lemma read_sint32_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_sint32 (havoc fresh cur aw size) ar].
+ separated ar 4 aw size ->
+ read_sint32 (havoc fresh cur aw size) ar = read_sint32 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint32 nb ar.offset = VB.bread_uint32 ob ar.offset
+
+ lemma read_sint32_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_uint8 m aw v) ar].
+ separated aw 1 ar 4 ->
+ read_sint32 (write_uint8 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_uint16 m aw v) ar].
+ separated aw 2 ar 4 ->
+ read_sint32 (write_uint16 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_uint32 m aw v) ar].
+ separated aw 4 ar 4 ->
+ read_sint32 (write_uint32 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_uint64 m aw v) ar].
+ separated aw 8 ar 4 ->
+ read_sint32 (write_uint64 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_sint8 m aw v) ar].
+ separated aw 1 ar 4 ->
+ read_sint32 (write_sint8 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_sint16 m aw v) ar].
+ separated aw 2 ar 4 ->
+ read_sint32 (write_sint16 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_sint32 m aw v) ar].
+ separated aw 4 ar 4 ->
+ read_sint32 (write_sint32 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint32_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint32 (write_sint64 m aw v) ar].
+ separated aw 8 ar 4 ->
+ read_sint32 (write_sint64 m aw v) ar = read_sint32 m ar
+
+ lemma read_sint64_write_sint64_eq:
+ forall m: memory, a: addr, v: int [read_sint64 (write_sint64 m a v) a].
+ is_sint64 v ->
+ read_sint64 (write_sint64 m a v) a = v
+
+ lemma read_sint64_write_uint64_eq:
+ forall m: memory, a: addr, v: int [read_sint64 (write_uint64 m a v) a].
+ is_uint64 v ->
+ read_sint64 (write_uint64 m a v) a = to_sint64 v
+
+ lemma read_sint64_havoc_sep:
+ forall fresh cur: memory, size: int, ar aw: addr [read_sint64 (havoc fresh cur aw size) ar].
+ separated ar 8 aw size ->
+ read_sint64 (havoc fresh cur aw size) ar = read_sint64 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> VB.bread_uint64 nb ar.offset = VB.bread_uint64 ob ar.offset
+
+ lemma read_sint64_write_uint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_uint8 m aw v) ar].
+ separated aw 1 ar 8 ->
+ read_sint64 (write_uint8 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_uint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_uint16 m aw v) ar].
+ separated aw 2 ar 8 ->
+ read_sint64 (write_uint16 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_uint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_uint32 m aw v) ar].
+ separated aw 4 ar 8 ->
+ read_sint64 (write_uint32 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_uint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_uint64 m aw v) ar].
+ separated aw 8 ar 8 ->
+ read_sint64 (write_uint64 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_sint8_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_sint8 m aw v) ar].
+ separated aw 1 ar 8 ->
+ read_sint64 (write_sint8 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_sint16_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_sint16 m aw v) ar].
+ separated aw 2 ar 8 ->
+ read_sint64 (write_sint16 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_sint32_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_sint32 m aw v) ar].
+ separated aw 4 ar 8 ->
+ read_sint64 (write_sint32 m aw v) ar = read_sint64 m ar
+
+ lemma read_sint64_write_sint64_sep:
+ forall m: memory, ar aw: addr, v: int [read_sint64 (write_sint64 m aw v) ar].
+ separated aw 8 ar 8 ->
+ read_sint64 (write_sint64 m aw v) ar = read_sint64 m ar
+
+ function read_init8 (m: init) (a: addr) : bool =
+ IB.bread_init8 m[a.base] a.offset
+
+ function read_init16 (m: init) (a: addr) : bool =
+ IB.bread_init16 m[a.base] a.offset
+
+ function read_init32 (m: init) (a: addr) : bool =
+ IB.bread_init32 m[a.base] a.offset
+
+ function read_init64 (m: init) (a: addr) : bool =
+ IB.bread_init64 m[a.base] a.offset
+
+ function write_init8 (m: init) (a: addr) (i: bool) : init =
+ set m a.base (IB.bwrite_init8 m [a.base] a.offset i)
+
+ function write_init16 (m: init) (a: addr) (i: bool) : init =
+ set m a.base (IB.bwrite_init16 m [a.base] a.offset i)
+
+ function write_init32 (m: init) (a: addr) (i: bool) : init =
+ set m a.base (IB.bwrite_init32 m [a.base] a.offset i)
+
+ function write_init64 (m: init) (a: addr) (i: bool) : init =
+ set m a.base (IB.bwrite_init64 m [a.base] a.offset i)
+
+ lemma read_init8_write_init8_eq:
+ forall m: init, a: addr, i: bool [read_init8 (write_init8 m a i) a].
+ read_init8 (write_init8 m a i) a = i
+
+ lemma read_init8_havoc_sep:
+ forall fresh cur: init, size: int, ar aw: addr [read_init8 (havoc fresh cur aw size) ar].
+ separated ar 1 aw size ->
+ read_init8 (havoc fresh cur aw size) ar = read_init8 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> IB.bread_init8 nb ar.offset = IB.bread_init8 ob ar.offset
+
+ lemma read_init8_write_init8_sep:
+ forall m: init, ar aw: addr, i: bool [read_init8 (write_init8 m aw i) ar].
+ separated aw 1 ar 1 ->
+ read_init8 (write_init8 m aw i) ar = read_init8 m ar
+
+ lemma read_init8_write_init16_sep:
+ forall m: init, ar aw: addr, i: bool [read_init8 (write_init16 m aw i) ar].
+ separated aw 2 ar 1 ->
+ read_init8 (write_init16 m aw i) ar = read_init8 m ar
+
+ lemma read_init8_write_init32_sep:
+ forall m: init, ar aw: addr, i: bool [read_init8 (write_init32 m aw i) ar].
+ separated aw 4 ar 1 ->
+ read_init8 (write_init32 m aw i) ar = read_init8 m ar
+
+ lemma read_init8_write_init64_sep:
+ forall m: init, ar aw: addr, i: bool [read_init8 (write_init64 m aw i) ar].
+ separated aw 8 ar 1 ->
+ read_init8 (write_init64 m aw i) ar = read_init8 m ar
+
+ lemma read_init16_write_init16_eq:
+ forall m: init, a: addr, i: bool [read_init16 (write_init16 m a i) a].
+ read_init16 (write_init16 m a i) a = i
+
+ lemma read_init16_havoc_sep:
+ forall fresh cur: init, size: int, ar aw: addr [read_init16 (havoc fresh cur aw size) ar].
+ separated ar 2 aw size ->
+ read_init16 (havoc fresh cur aw size) ar = read_init16 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> IB.bread_init16 nb ar.offset = IB.bread_init16 ob ar.offset
+
+ lemma read_init16_write_init8_sep:
+ forall m: init, ar aw: addr, i: bool [read_init16 (write_init8 m aw i) ar].
+ separated aw 1 ar 2 ->
+ read_init16 (write_init8 m aw i) ar = read_init16 m ar
+
+ lemma read_init16_write_init16_sep:
+ forall m: init, ar aw: addr, i: bool [read_init16 (write_init16 m aw i) ar].
+ separated aw 2 ar 2 ->
+ read_init16 (write_init16 m aw i) ar = read_init16 m ar
+
+ lemma read_init16_write_init32_sep:
+ forall m: init, ar aw: addr, i: bool [read_init16 (write_init32 m aw i) ar].
+ separated aw 4 ar 2 ->
+ read_init16 (write_init32 m aw i) ar = read_init16 m ar
+
+ lemma read_init16_write_init64_sep:
+ forall m: init, ar aw: addr, i: bool [read_init16 (write_init64 m aw i) ar].
+ separated aw 8 ar 2 ->
+ read_init16 (write_init64 m aw i) ar = read_init16 m ar
+
+ lemma read_init32_write_init32_eq:
+ forall m: init, a: addr, i: bool [read_init32 (write_init32 m a i) a].
+ read_init32 (write_init32 m a i) a = i
+
+ lemma read_init32_havoc_sep:
+ forall fresh cur: init, size: int, ar aw: addr [read_init32 (havoc fresh cur aw size) ar].
+ separated ar 4 aw size ->
+ read_init32 (havoc fresh cur aw size) ar = read_init32 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> IB.bread_init32 nb ar.offset = IB.bread_init32 ob ar.offset
+
+ lemma read_init32_write_init8_sep:
+ forall m: init, ar aw: addr, i: bool [read_init32 (write_init8 m aw i) ar].
+ separated aw 1 ar 4 ->
+ read_init32 (write_init8 m aw i) ar = read_init32 m ar
+
+ lemma read_init32_write_init16_sep:
+ forall m: init, ar aw: addr, i: bool [read_init32 (write_init16 m aw i) ar].
+ separated aw 2 ar 4 ->
+ read_init32 (write_init16 m aw i) ar = read_init32 m ar
+
+ lemma read_init32_write_init32_sep:
+ forall m: init, ar aw: addr, i: bool [read_init32 (write_init32 m aw i) ar].
+ separated aw 4 ar 4 ->
+ read_init32 (write_init32 m aw i) ar = read_init32 m ar
+
+ lemma read_init32_write_init64_sep:
+ forall m: init, ar aw: addr, i: bool [read_init32 (write_init64 m aw i) ar].
+ separated aw 8 ar 4 ->
+ read_init32 (write_init64 m aw i) ar = read_init32 m ar
+
+ lemma read_init64_write_init64_eq:
+ forall m: init, a: addr, i: bool [read_init64 (write_init64 m a i) a].
+ read_init64 (write_init64 m a i) a = i
+
+ lemma read_init64_havoc_sep:
+ forall fresh cur: init, size: int, ar aw: addr [read_init64 (havoc fresh cur aw size) ar].
+ separated ar 8 aw size ->
+ read_init64 (havoc fresh cur aw size) ar = read_init64 cur ar
+ by
+ let ob = cur[aw.base] in
+ let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in
+ aw.base = ar.base -> IB.bread_init64 nb ar.offset = IB.bread_init64 ob ar.offset
+
+ lemma read_init64_write_init8_sep:
+ forall m: init, ar aw: addr, i: bool [read_init64 (write_init8 m aw i) ar].
+ separated aw 1 ar 8 ->
+ read_init64 (write_init8 m aw i) ar = read_init64 m ar
+
+ lemma read_init64_write_init16_sep:
+ forall m: init, ar aw: addr, i: bool [read_init64 (write_init16 m aw i) ar].
+ separated aw 2 ar 8 ->
+ read_init64 (write_init16 m aw i) ar = read_init64 m ar
+
+ lemma read_init64_write_init32_sep:
+ forall m: init, ar aw: addr, i: bool [read_init64 (write_init32 m aw i) ar].
+ separated aw 4 ar 8 ->
+ read_init64 (write_init32 m aw i) ar = read_init64 m ar
+
+ lemma read_init64_write_init64_sep:
+ forall m: init, ar aw: addr, i: bool [read_init64 (write_init64 m aw i) ar].
+ separated aw 8 ar 8 ->
+ read_init64 (write_init64 m aw i) ar = read_init64 m ar
+
+ predicate sconst (memory)
+
+ predicate bytes(m: memory) =
+ forall a: addr. 0 <= raw_get m a <= 255
+
+end
diff --git a/src/plugins/wp/share/why3/frama_c_wp/membytesgen.ml b/src/plugins/wp/share/why3/frama_c_wp/membytesgen.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8c93efb9bdb7604620afb4dd1202be3be6036830
--- /dev/null
+++ b/src/plugins/wp/share/why3/frama_c_wp/membytesgen.ml
@@ -0,0 +1,686 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Format
+
+let pp_type fmt (signed, size) =
+ let prefix = if signed then 's' else 'u' in
+ fprintf fmt "%cint%d" prefix size
+
+let pp_use fmt (m, alias) =
+ let pp_alias fmt = function
+ | Some alias -> fprintf fmt " as %s" alias
+ | None -> ()
+ in
+ fprintf fmt "use %s%a" m pp_alias alias
+
+let pp_use_list fmt l =
+ fprintf fmt "%a" (pp_print_list ~pp_sep:pp_print_cut pp_use) l
+
+let all_sizes = [ 8 ; 16 ; 32 ; 64 ]
+let all_types = [ (false, 8) ; (false, 16) ; (false, 32) ; (false, 64)
+ ; (true , 8) ; (true , 16) ; (true , 32) ; (true , 64) ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Value Encode/Decode --- *)
+(* -------------------------------------------------------------------------- *)
+
+let value_codec_preambule fmt () =
+ fprintf fmt "%a@," pp_use_list
+ [ "int.Int", None
+ ; "int.ComputerDivision", None
+ ; "frama_c_wp.cint.Cint", None
+ ; "frama_c_wp.sequence.Seq", None ]
+
+let value_codec_encode_unsigned fmt size =
+ let consbyte ~last fmt n =
+ if n = 1
+ then fprintf fmt "(L.Cons (mod v 0x100)"
+ else fprintf fmt "(L.Cons (mod (div v 0x%x) 0x100)" (1 lsl (8 * (n - 1))) ;
+
+ if last then fprintf fmt " L.Nil%s" (String.init n (fun _ -> ')')) ;
+ fprintf fmt "@,"
+ in
+ let rec all_consbytes n fmt m =
+ if n = m
+ then consbyte ~last:true fmt n
+ else begin consbyte ~last:false fmt n ; all_consbytes (n+1) fmt m end
+ in
+ fprintf fmt "@[<v 2>function encode_%a (v: int) : seq int =@," pp_type (false, size) ;
+ fprintf fmt "%a@]@," (all_consbytes 1) (size / 8)
+
+let value_codec_encode_signed fmt size =
+ fprintf fmt "@[<v 2>function encode_%a (v: int) : seq int =@," pp_type (true, size) ;
+ fprintf fmt "encode_%a (to_%a v)@,@]@," pp_type (false, size) pp_type (false, size)
+
+let value_codec_encode fmt size =
+ value_codec_encode_unsigned fmt size ;
+ value_codec_encode_signed fmt size
+
+let value_codec_decode_unsigned fmt size =
+ let rec mline n fmt stop =
+ if n = stop
+ then fprintf fmt "L.Nil"
+ else fprintf fmt "L.Cons b%d (%a)" n (mline (n + 1)) stop
+ in
+ let rec rline n fmt stop =
+ if n = stop - 1
+ then fprintf fmt "b%d * 0x%x" n (1 lsl (8 * n))
+ else fprintf fmt "b%d * 0x%x + %a" n (1 lsl (8 * n)) (rline (n + 1)) stop
+ in
+ let case fmt stop =
+ fprintf fmt "| %a ->@," (mline 0) stop ;
+ fprintf fmt " %a@," (rline 0) stop ;
+ in
+ fprintf fmt "@[<v 2>function decode_%a (s: seq int) : int =@," pp_type (false, size) ;
+ fprintf fmt "match s with@," ;
+ fprintf fmt "%a" case (size / 8) ;
+ fprintf fmt "| _ -> 0@," ;
+ fprintf fmt "end@,@]@,"
+
+let value_codec_decode_signed fmt size =
+ fprintf fmt "@[<v 2>function decode_%a (s: seq int) : int =@," pp_type (true, size) ;
+ fprintf fmt "to_%a (decode_%a s)@,@]@," pp_type (true, size) pp_type (false, size)
+
+let value_codec_decode fmt size =
+ value_codec_decode_unsigned fmt size ;
+ value_codec_decode_signed fmt size
+
+let value_codec_lemma_decode_encode fmt decoded encoded =
+ let guard fmt () =
+ fprintf fmt "is_%a v" pp_type encoded
+ in
+ let same = match decoded, encoded with (sd, _), (se, _) -> sd = se in
+ let decenc fmt () =
+ fprintf fmt "decode_%a (encode_%a v)"
+ pp_type decoded
+ pp_type encoded
+ in
+ let eq fmt () =
+ fprintf fmt "%a = %sv"
+ decenc ()
+ (if same then "" else asprintf "to_%a " pp_type decoded)
+ in
+ fprintf fmt "@[<v 2>lemma decode_%a_encode_%a:@,"
+ pp_type decoded pp_type encoded ;
+ fprintf fmt "forall v: int [%a].@,%a -> %a@,@]@," decenc () guard () eq ()
+
+let value_codec_lemma_decode_encode fmt size =
+ value_codec_lemma_decode_encode fmt (false, size) (false, size) ;
+ value_codec_lemma_decode_encode fmt (true, size) (false, size) ;
+ value_codec_lemma_decode_encode fmt (false, size) (true , size) ;
+ value_codec_lemma_decode_encode fmt (true, size) (true , size)
+
+let value_codec_all_symbols fmt size =
+ value_codec_decode fmt size ;
+ value_codec_encode fmt size ;
+ value_codec_lemma_decode_encode fmt size
+
+let value_codec fmt () =
+ fprintf fmt "%a@," value_codec_preambule () ;
+ List.iter (fprintf fmt "%a" value_codec_all_symbols) all_sizes
+
+(* -------------------------------------------------------------------------- *)
+(* --- Init Encode/Decode --- *)
+(* -------------------------------------------------------------------------- *)
+
+let init_codec_preambule fmt () =
+ fprintf fmt "%a@," pp_use_list
+ [ "bool.Bool", None
+ ; "frama_c_wp.sequence.Seq", None ]
+
+let init_codec_decode fmt size =
+ let rec mline n fmt stop =
+ if n = stop
+ then fprintf fmt "L.Nil"
+ else fprintf fmt "L.Cons b%d (%a)" n (mline (n + 1)) stop
+ in
+ let rec rline n fmt stop =
+ if n = stop - 1
+ then fprintf fmt "b%d" n
+ else fprintf fmt "b%d && %a" n (rline (n + 1)) stop
+ in
+ let case fmt stop =
+ fprintf fmt "| %a ->@," (mline 0) stop ;
+ fprintf fmt " %a@," (rline 0) stop
+ in
+ fprintf fmt "@[<v 2>function decode_init%d (s: seq bool) : bool =@," size ;
+ fprintf fmt "match s with@," ;
+ fprintf fmt "%a" case (size / 8) ;
+ fprintf fmt "| _ -> false@," ;
+ fprintf fmt "end@,@]@,"
+
+let init_codec_encode fmt size =
+ fprintf fmt "@[<v 2>function encode_init%d (v: bool) : seq bool =@," size ;
+ fprintf fmt "create v %d" (size / 8) ;
+ fprintf fmt "@,@]@,"
+
+let init_codec_lemma_decode_encode fmt size =
+ let decenc fmt () =
+ fprintf fmt "decode_init%d (encode_init%d v)" size size
+ in
+ let eq fmt () = fprintf fmt "%a = v" decenc () in
+ fprintf fmt "@[<v 2>lemma decode_init%d_encode_init%d:@," size size ;
+ fprintf fmt "forall v: bool [%a].@,%a@,@]@," decenc () eq ()
+
+
+let init_codec_all_symbols fmt size =
+ init_codec_decode fmt size ;
+ init_codec_encode fmt size ;
+ init_codec_lemma_decode_encode fmt size
+
+let init_codec fmt () =
+ fprintf fmt "%a@," init_codec_preambule () ;
+ List.iter (fprintf fmt "%a" init_codec_all_symbols) all_sizes
+
+(* -------------------------------------------------------------------------- *)
+(* --- Offset --- *)
+(* -------------------------------------------------------------------------- *)
+
+let offset fmt () =
+ fprintf fmt
+ {|use int.Int
+ type offset = int
+
+ predicate sepoffset (po: offset) (lp: int) (qo: offset) (lq: int) =
+ qo + lq <= po \/ po + lp <= qo
+|}
+
+(* -------------------------------------------------------------------------- *)
+(* --- RWBytes --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rwbytes_preambule fmt () =
+ fprintf fmt "%a@,@," pp_use_list
+ [ "int.Int", None ; "map.Map", Some "M" ;
+ "frama_c_wp.sequence.Seq", Some "S" ; "Offset", None] ;
+ fprintf fmt
+ {|type seq 'a = S.seq 'a
+ type block 'a = M.map int 'a
+
+ function bwrite_seq (b:block 'a) (o: int) (s: seq 'a) : block 'a =
+ match s with
+ | S.L.Nil -> b
+ | S.L.Cons h tl -> M.(set (bwrite_seq b (o+1) tl) o h)
+ end
+
+ predicate beq_blocks (b1 b2: block 'a) (o: int) (l: int) =
+ forall i: int. o <= i < o + l -> M.(get b1 i) = M.(get b2 i)
+|}
+
+let rwbytes_write fmt size =
+ let rec mline n max fmt stop =
+ if n = stop
+ then fprintf fmt "%s" (if max = stop then "_" else "S.L.Nil")
+ else fprintf fmt "S.L.Cons b%d (%a)" n (mline (n + 1) max) stop
+ in
+ let rec rline n fmt stop =
+ let pp_offset fmt = function
+ | 0 -> fprintf fmt "o"
+ | n -> fprintf fmt "(o+%d)" n
+ in
+ if n = stop
+ then fprintf fmt "b"
+ else fprintf fmt "(set %a %a b%d)" (rline (n + 1)) stop pp_offset n n
+ in
+ let case stop fmt max =
+ fprintf fmt "| %a ->@," (mline 0 max) stop ;
+ fprintf fmt " M.%a@," (rline 0) stop ;
+ in
+ fprintf fmt "@[<v 2>function bwrite_%dbits (b: block 'a) (o: int) (s: seq 'a) : block 'a =@," size ;
+ fprintf fmt "match s with@," ;
+ fprintf fmt "%a" (case (size / 8)) (size / 8) ;
+ fprintf fmt "| _ -> b@," ;
+ fprintf fmt "end@,@]@,"
+
+let rwbytes_read fmt size =
+ let consbyte ~last fmt n =
+ if n = 1
+ then fprintf fmt "(S.L.Cons M.(b[o ])"
+ else fprintf fmt "(S.L.Cons M.(b[o+%d])" (n - 1) ;
+
+ if last then fprintf fmt " S.L.Nil%s" (String.init n (fun _ -> ')')) ;
+ fprintf fmt "@,"
+ in
+ let rec all_consbytes n fmt m =
+ if n = m
+ then consbyte ~last:true fmt n
+ else begin consbyte ~last:false fmt n ; all_consbytes (n+1) fmt m end
+ in
+ fprintf fmt "@[<v 2>function bread_%dbits (b: block 'a) (o: int) : seq 'a =@," size ;
+ fprintf fmt "%a@]@," (all_consbytes 1) (size / 8)
+
+let rwbytes_read_write_eq fmt size =
+ let guard fmt () =
+ fprintf fmt "S.length s = %d" (size / 8)
+ in
+ let read_write fmt () =
+ fprintf fmt "bread_%dbits (bwrite_%dbits b o s) o" size size
+ in
+ let eq fmt () = fprintf fmt "%a = s" read_write () in
+ fprintf fmt "@[<v 2>lemma bread_%dbits_bwrite_%dbits_eq:@," size size ;
+ fprintf fmt "forall b: block 'a, o: int, s: seq 'a [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@]@,@," guard () eq ()
+
+let rwbytes_read_bwrite_seq_sep fmt rsize =
+ let brsize = rsize / 8 in
+ let guard fmt () =
+ fprintf fmt "sepoffset ow (S.length s) or %d" brsize in
+ let read_write fmt () =
+ fprintf fmt "bread_%dbits (bwrite_seq b ow s) or" rsize
+ in
+ let eq fmt () = fprintf fmt "%a = bread_%dbits b or" read_write () rsize in
+ fprintf fmt "@[<v 2>let rec lemma bread_%dbits_bwrite_seq_sep " rsize ;
+ fprintf fmt "(b: block 'a)(or ow: int)(s: seq 'a)@," ;
+ fprintf fmt "requires { %a }@," guard() ;
+ fprintf fmt "ensures { %a }@,@]" eq () ;
+ fprintf fmt "@[<v 2>= match s with@," ;
+ fprintf fmt "| S.L.Nil -> ()@," ;
+ fprintf fmt "| S.L.Cons _ tl -> bread_%dbits_bwrite_seq_sep b or (ow + 1) tl@," rsize ;
+ fprintf fmt "end@]@,@,"
+
+let rwbytes_read_write_sep fmt rsize wsize =
+ let brsize = rsize / 8 and bwsize = wsize / 8 in
+ let guard fmt () =
+ fprintf fmt "sepoffset ow %d or %d" bwsize brsize in
+ let read_write fmt () =
+ fprintf fmt "bread_%dbits (bwrite_%dbits b ow s) or" rsize wsize
+ in
+ let eq fmt () = fprintf fmt "%a = bread_%dbits b or" read_write () rsize in
+ fprintf fmt "@[<v 2>lemma bread_%dbits_bwrite_%dbits_sep:@," rsize wsize ;
+ fprintf fmt "forall b: block 'a, or ow: int, s: seq 'a [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@]@,@," guard () eq ()
+
+let rwbytes_all_lemmas fmt size =
+ rwbytes_read_write_eq fmt size ;
+ rwbytes_read_bwrite_seq_sep fmt size ;
+ List.iter (rwbytes_read_write_sep fmt size) all_sizes
+
+let rwbytes fmt () =
+ fprintf fmt "%a@," rwbytes_preambule () ;
+ List.iter (fprintf fmt "%a" rwbytes_read) all_sizes ;
+ List.iter (fprintf fmt "%a" rwbytes_write) all_sizes ;
+ List.iter (fprintf fmt "%a" rwbytes_all_lemmas) all_sizes
+
+(* -------------------------------------------------------------------------- *)
+(* --- ValueBlockRW --- *)
+(* -------------------------------------------------------------------------- *)
+
+let value_blockrw_preambule fmt () =
+ fprintf fmt "%a@,@," pp_use_list
+ [ "int.Int", None
+ ; "frama_c_wp.cint.Cint", None
+ ; "ValueCodec", None
+ ; "Offset", None
+ ; "RWBytes", None
+ ] ;
+ fprintf fmt "type vblock = block int@,"
+
+let value_blockrw_write fmt ((_, size) as t) =
+ fprintf fmt "@[<v 2>function bwrite_%a (b: vblock) (o: int) (v: int) : vblock =@," pp_type t;
+ fprintf fmt "bwrite_%dbits b o (encode_%a v)@,@]@," size pp_type t
+
+let value_blockrw_read fmt ((_, size) as t) =
+ fprintf fmt "@[<v 2>function bread_%a (b: vblock) (o: int) : int =@," pp_type t ;
+ fprintf fmt "decode_%a (bread_%dbits b o)@,@]@," pp_type t size
+
+let value_blockrw_read_write_eq_same fmt t =
+ let guard fmt () = fprintf fmt "is_%a v" pp_type t in
+ let read_write fmt () =
+ fprintf fmt "bread_%a (bwrite_%a b o v) o" pp_type t pp_type t
+ in
+ let eq fmt () = fprintf fmt "%a = v" read_write () in
+ fprintf fmt "@[<v 2>lemma bread_%a_bwrite_%a_eq:@," pp_type t pp_type t ;
+ fprintf fmt "forall b: vblock, o: int, v: int [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let value_blockrw_read_write_eq_opposite fmt rt =
+ let wt = not @@ fst rt, snd rt in
+ let guard fmt () = fprintf fmt "is_%a v" pp_type wt in
+ let read_write fmt () =
+ fprintf fmt "bread_%a (bwrite_%a b o v) o" pp_type rt pp_type wt
+ in
+ let eq fmt () = fprintf fmt "%a = to_%a v" read_write () pp_type rt in
+ fprintf fmt "@[<v 2>lemma bread_%a_bwrite_%a_eq:@," pp_type rt pp_type wt ;
+ fprintf fmt "forall b: vblock, o: int, v: int [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let value_blockrw_read_write_eq fmt t =
+ value_blockrw_read_write_eq_same fmt t ;
+ value_blockrw_read_write_eq_opposite fmt t
+
+let value_blockrw_read_write_sep fmt rt wt =
+ let guard fmt () =
+ fprintf fmt "sepoffset ow %d or %d" ((snd wt) / 8) ((snd rt) / 8) in
+ let read_write fmt () =
+ fprintf fmt "bread_%a (bwrite_%a b ow v) or" pp_type rt pp_type wt
+ in
+ let eq fmt () = fprintf fmt "%a = bread_%a b or" read_write () pp_type rt in
+ fprintf fmt "@[<v 2>lemma bread_%a_bwrite_%a_sep:@," pp_type rt pp_type wt ;
+ fprintf fmt "forall b: vblock, or ow: int, v: int [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let value_blockrw_read_havoc_sep fmt rt =
+ let guard fmt () =
+ fprintf fmt "sepoffset or %d ho (Seq.length u)" ((snd rt) / 8) in
+ let read_havoc fmt () =
+ fprintf fmt "bread_%a (bwrite_seq b ho u) or" pp_type rt
+ in
+ let eq fmt () = fprintf fmt "%a = bread_%a b or" read_havoc () pp_type rt in
+ fprintf fmt "@[<v 2>lemma bread_%a_bhavoc_sep:@," pp_type rt ;
+ fprintf fmt "forall b: vblock, u: S.seq int, or ho: int [%a].@," read_havoc () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let value_blockrw_all_lemmas fmt size =
+ value_blockrw_read_write_eq fmt size ;
+ value_blockrw_read_havoc_sep fmt size ;
+ List.iter (value_blockrw_read_write_sep fmt size) all_types
+
+let value_blockrw fmt () =
+ fprintf fmt "%a@," value_blockrw_preambule () ;
+ List.iter (fprintf fmt "%a" value_blockrw_read) all_types ;
+ List.iter (fprintf fmt "%a" value_blockrw_write) all_types ;
+ List.iter (fprintf fmt "%a" value_blockrw_all_lemmas) all_types
+
+(* -------------------------------------------------------------------------- *)
+(* --- InitBlockRW --- *)
+(* -------------------------------------------------------------------------- *)
+
+let init_blockrw_preambule fmt () =
+ fprintf fmt "%a@,@," pp_use_list
+ [ "bool.Bool", None
+ ; "int.Int", None
+ ; "InitCodec", None
+ ; "Offset", None
+ ; "RWBytes", None
+ ] ;
+ fprintf fmt "type iblock = block bool@,@," ;
+ fprintf fmt "predicate is_init_range(b: iblock) (o: int) (size: int) =@," ;
+ fprintf fmt " forall i: int. o <= i < o + size -> M.get b i = True@,"
+
+let init_blockrw_write fmt size =
+ fprintf fmt "@[<v 2>function bwrite_init%d (b: iblock) (o: int) (init: bool) : iblock =@," size;
+ fprintf fmt "bwrite_%dbits b o (encode_init%d init)@,@]@," size size
+
+let init_blockrw_read fmt size =
+ fprintf fmt "@[<v 2>function bread_init%d (b: iblock) (o: int) : bool =@," size ;
+ fprintf fmt "decode_init%d (bread_%dbits b o)@,@]@," size size
+
+let init_blockrw_read_write_eq fmt size =
+ let read_write fmt () =
+ fprintf fmt "bread_init%d (bwrite_init%d b o init) o" size size
+ in
+ let eq fmt () = fprintf fmt "%a = init" read_write () in
+ fprintf fmt "@[<v 2>lemma bread_init%d_bwrite_init%d_eq:@," size size ;
+ fprintf fmt "forall b: iblock, o: int, init: bool [%a].@," read_write () ;
+ fprintf fmt "%a@,@]@," eq ()
+
+let init_blockrw_read_write_sep fmt rsize wsize =
+ let guard fmt () =
+ fprintf fmt "sepoffset ow %d or %d" (wsize / 8) (rsize / 8) in
+ let read_write fmt () =
+ fprintf fmt "bread_init%d (bwrite_init%d b ow init) or" rsize wsize
+ in
+ let eq fmt () = fprintf fmt "%a = bread_init%d b or" read_write () rsize in
+ fprintf fmt "@[<v 2>lemma bread_init%d_bwrite_init%d_sep:@," rsize wsize ;
+ fprintf fmt "forall b: iblock, or ow: int, init: bool [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let init_blockrw_read_havoc_sep fmt rsize =
+ let guard fmt () =
+ fprintf fmt "sepoffset or %d ho (Seq.length u)" (rsize / 8) in
+ let read_havoc fmt () =
+ fprintf fmt "bread_init%d (bwrite_seq b ho u) or" rsize
+ in
+ let eq fmt () = fprintf fmt "%a = bread_init%d b or" read_havoc () rsize in
+ fprintf fmt "@[<v 2>lemma bread_init%d_bhavoc_sep:@," rsize ;
+ fprintf fmt "forall b: iblock, u: S.seq bool, or ho: int [%a].@," read_havoc () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let init_blockrw_all_lemmas fmt size =
+ init_blockrw_read_write_eq fmt size ;
+ init_blockrw_read_havoc_sep fmt size ;
+ List.iter (init_blockrw_read_write_sep fmt size) all_sizes
+
+let init_blockrw fmt () =
+ fprintf fmt "%a@," init_blockrw_preambule () ;
+ List.iter (fprintf fmt "%a" init_blockrw_read) all_sizes ;
+ List.iter (fprintf fmt "%a" init_blockrw_write) all_sizes ;
+ List.iter (fprintf fmt "%a" init_blockrw_all_lemmas) all_sizes
+
+(* -------------------------------------------------------------------------- *)
+(* --- MemBytes --- *)
+(* -------------------------------------------------------------------------- *)
+
+let membytes_preambule fmt () =
+ fprintf fmt "%a@,@," pp_use_list
+ [ "int.Int", None
+ ; "map.Map", None
+ ; "frama_c_wp.cint.Cint", None
+ ; "frama_c_wp.memaddr.MemAddr", None
+ ; "frama_c_wp.sequence.Seq", Some "S"
+ ; "RWBytes", None
+ ; "ValueBlockRW", Some "VB"
+ ; "InitBlockRW", Some "IB"
+ ] ;
+ fprintf fmt
+ {|type memory = map int (VB.vblock)
+ type init = map int (IB.iblock)
+
+ (* override memory cinits for MemBytes memory *)
+ predicate cinits (init)
+
+ function raw_get (m: map int (map int 'a)) (a: addr) : 'a =
+ get (get m a.base) a.offset
+
+ function raw_set (m: map int (map int 'a)) (a: addr) (v: 'a) : map int (map int 'a) =
+ set m a.base (set (get m a.base) a.offset v)
+
+ let rec function to_seq (a: map int 'a) (b e: int) : S.seq 'a
+ ensures { e - b >= 0 -> S.length result = e - b }
+ ensures { forall i: int. b <= i < e -> S.(result[i - b]) = get a i }
+ variant { e - b }
+ = if e <= b then S.L.Nil else S.L.Cons (get a b) (to_seq a (b+1) e)
+
+ function init_seq (s: int) : S.seq bool =
+ S.create True s
+
+ function havoc (fresh cur: map int (block 'a)) (a: addr) (size: int): map int (block 'a) =
+ set cur a.base (bwrite_seq (get cur a.base) a.offset (to_seq fresh[a.base] 0 size))
+
+ predicate eqmem (m1 m2: map int (block 'a)) (a: addr) (size: int) =
+ beq_blocks (get m1 a.base) (get m2 a.base) (a.offset) size
+
+ predicate is_init_range (i: init) (a: addr) (size: int) =
+ IB.is_init_range (get i a.base) a.offset size
+
+ function set_init_range (cur: init) (a: addr) (size: int) : init =
+ set cur a.base (bwrite_seq (get cur a.base) a.offset (init_seq size))
+|}
+
+let membytes_write fmt t =
+ fprintf fmt "@[<v 2>function write_%a (m: memory) (a: addr) (v: int) : memory =@," pp_type t;
+ fprintf fmt "set m a.base (VB.bwrite_%a m [a.base] a.offset v)@,@]@," pp_type t
+
+let membytes_read fmt t =
+ fprintf fmt "@[<v 2>function read_%a (m: memory) (a: addr) : int =@," pp_type t ;
+ fprintf fmt "VB.bread_%a m[a.base] a.offset@,@]@," pp_type t
+
+let membytes_read_write_eq_same fmt t =
+ let guard fmt () = fprintf fmt "is_%a v" pp_type t in
+ let read_write fmt () =
+ fprintf fmt "read_%a (write_%a m a v) a" pp_type t pp_type t
+ in
+ let eq fmt () = fprintf fmt "%a = v" read_write () in
+ fprintf fmt "@[<v 2>lemma read_%a_write_%a_eq:@," pp_type t pp_type t ;
+ fprintf fmt "forall m: memory, a: addr, v: int [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let membytes_read_write_eq_opposite fmt rt =
+ let wt = not @@ fst rt, snd rt in
+ let guard fmt () = fprintf fmt "is_%a v" pp_type wt in
+ let read_write fmt () =
+ fprintf fmt "read_%a (write_%a m a v) a" pp_type rt pp_type wt
+ in
+ let eq fmt () = fprintf fmt "%a = to_%a v" read_write () pp_type rt in
+ fprintf fmt "@[<v 2>lemma read_%a_write_%a_eq:@," pp_type rt pp_type wt ;
+ fprintf fmt "forall m: memory, a: addr, v: int [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let membytes_read_write_eq fmt t =
+ membytes_read_write_eq_same fmt t ;
+ membytes_read_write_eq_opposite fmt t
+
+let membytes_read_write_sep fmt rt wt =
+ let guard fmt () =
+ fprintf fmt "separated aw %d ar %d" ((snd wt)/8) ((snd rt)/8) in
+ let read_write fmt () =
+ fprintf fmt "read_%a (write_%a m aw v) ar" pp_type rt pp_type wt
+ in
+ let eq fmt () = fprintf fmt "%a = read_%a m ar" read_write () pp_type rt in
+ fprintf fmt "@[<v 2>lemma read_%a_write_%a_sep:@," pp_type rt pp_type wt ;
+ fprintf fmt "forall m: memory, ar aw: addr, v: int [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let membytes_read_havoc_sep fmt rt =
+ let guard fmt () =
+ fprintf fmt "separated ar %d aw size" ((snd rt) / 8) in
+ let read_havoc fmt () =
+ fprintf fmt "read_%a (havoc fresh cur aw size) ar" pp_type rt
+ in
+ let eq fmt () = fprintf fmt "%a = read_%a cur ar" read_havoc () pp_type rt in
+ fprintf fmt "@[<v 2>lemma read_%a_havoc_sep:@," pp_type rt ;
+ fprintf fmt "forall fresh cur: memory, size: int, ar aw: addr [%a].@," read_havoc () ;
+ fprintf fmt "%a ->@, %a@," guard () eq () ;
+ fprintf fmt "@[<v 2>by@," ;
+ fprintf fmt "let ob = cur[aw.base] in@," ;
+ fprintf fmt "let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in@," ;
+ fprintf fmt "aw.base = ar.base -> " ;
+ fprintf fmt "VB.bread_uint%d nb ar.offset = VB.bread_uint%d ob ar.offset@]@,"
+ (snd rt) (snd rt) ;
+ fprintf fmt "@]@,"
+
+let membytes_all_lemmas fmt size =
+ membytes_read_write_eq fmt size ;
+ membytes_read_havoc_sep fmt size ;
+ List.iter (membytes_read_write_sep fmt size) all_types
+
+let membytes_write_init fmt size =
+ fprintf fmt "@[<v 2>function write_init%d (m: init) (a: addr) (i: bool) : init =@," size;
+ fprintf fmt "set m a.base (IB.bwrite_init%d m [a.base] a.offset i)@,@]@," size
+
+let membytes_read_init fmt size =
+ fprintf fmt "@[<v 2>function read_init%d (m: init) (a: addr) : bool =@," size ;
+ fprintf fmt "IB.bread_init%d m[a.base] a.offset@,@]@," size
+
+let membytes_read_write_init_eq fmt size =
+ let read_write fmt () =
+ fprintf fmt "read_init%d (write_init%d m a i) a" size size
+ in
+ let eq fmt () = fprintf fmt "%a = i" read_write () in
+ fprintf fmt "@[<v 2>lemma read_init%d_write_init%d_eq:@," size size ;
+ fprintf fmt "forall m: init, a: addr, i: bool [%a].@," read_write () ;
+ fprintf fmt "%a@,@]@," eq ()
+
+let membytes_read_write_init_sep fmt rsize wsize =
+ let guard fmt () =
+ fprintf fmt "separated aw %d ar %d" (wsize/8) (rsize/8) in
+ let read_write fmt () =
+ fprintf fmt "read_init%d (write_init%d m aw i) ar" rsize wsize
+ in
+ let eq fmt () = fprintf fmt "%a = read_init%d m ar" read_write () rsize in
+ fprintf fmt "@[<v 2>lemma read_init%d_write_init%d_sep:@," rsize wsize ;
+ fprintf fmt "forall m: init, ar aw: addr, i: bool [%a].@," read_write () ;
+ fprintf fmt "%a ->@, %a@,@]@," guard () eq ()
+
+let membytes_read_havoc_init_sep fmt rsize =
+ let guard fmt () =
+ fprintf fmt "separated ar %d aw size" (rsize / 8) in
+ let read_havoc fmt () =
+ fprintf fmt "read_init%d (havoc fresh cur aw size) ar" rsize
+ in
+ let eq fmt () = fprintf fmt "%a = read_init%d cur ar" read_havoc () rsize in
+ fprintf fmt "@[<v 2>lemma read_init%d_havoc_sep:@," rsize ;
+ fprintf fmt "forall fresh cur: init, size: int, ar aw: addr [%a].@," read_havoc () ;
+ fprintf fmt "%a ->@, %a@," guard () eq () ;
+ fprintf fmt "@[<v 2>by@," ;
+ fprintf fmt "let ob = cur[aw.base] in@," ;
+ fprintf fmt "let nb = bwrite_seq ob aw.offset (to_seq fresh[aw.base] 0 size) in@," ;
+ fprintf fmt "aw.base = ar.base -> " ;
+ fprintf fmt "IB.bread_init%d nb ar.offset = IB.bread_init%d ob ar.offset@]@,"
+ rsize rsize ;
+ fprintf fmt "@]@,"
+
+let membytes_all_init_lemmas fmt size =
+ membytes_read_write_init_eq fmt size ;
+ membytes_read_havoc_init_sep fmt size ;
+ List.iter (membytes_read_write_init_sep fmt size) all_sizes
+
+let membytes_context fmt () =
+ fprintf fmt "predicate sconst (memory)@," ;
+ fprintf fmt
+ {|
+ predicate bytes(m: memory) =
+ forall a: addr. 0 <= raw_get m a <= 255
+|}
+
+let membytes fmt () =
+ fprintf fmt "%a@," membytes_preambule () ;
+ List.iter (fprintf fmt "%a" membytes_read) all_types ;
+ List.iter (fprintf fmt "%a" membytes_write) all_types ;
+ List.iter (fprintf fmt "%a" membytes_all_lemmas) all_types ;
+ List.iter (fprintf fmt "%a" membytes_read_init) all_sizes ;
+ List.iter (fprintf fmt "%a" membytes_write_init) all_sizes ;
+ List.iter (fprintf fmt "%a" membytes_all_init_lemmas) all_sizes ;
+ fprintf fmt "%a" membytes_context ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Main --- *)
+(* -------------------------------------------------------------------------- *)
+
+let wmodule name builder fmt () =
+ fprintf fmt "@[<v 2>module %s@," name ;
+ fprintf fmt "%a" builder () ;
+ fprintf fmt "@]@.end"
+
+let file_contents filename =
+ let input = open_in_bin filename in
+ let contents = really_input_string input (in_channel_length input) in
+ close_in input;
+ contents
+
+let () =
+ let out = open_out "membytes.mlw" in
+ let header = file_contents "Wp.header" in
+ let fmt = formatter_of_out_channel out in
+ fprintf fmt "%s@." header ;
+ fprintf fmt "(* DO NOT EDIT: this file is generated at build time *)@.@." ;
+ fprintf fmt "(* Tactics for failing proofs:@. \
+ intros variables ; compute_in_goal ; cvc5 *)@.@." ;
+ fprintf fmt "%a@.@;" (wmodule "ValueCodec" value_codec) () ;
+ fprintf fmt "%a@.@;" (wmodule "InitCodec" init_codec) () ;
+ fprintf fmt "%a@.@;" (wmodule "Offset" offset) () ;
+ fprintf fmt "%a@.@;" (wmodule "RWBytes" rwbytes) () ;
+ fprintf fmt "%a@.@;" (wmodule "ValueBlockRW" value_blockrw) () ;
+ fprintf fmt "%a@.@;" (wmodule "InitBlockRW" init_blockrw) () ;
+ fprintf fmt "%a@.@;" (wmodule "MemBytes" membytes) () ;
+ close_out out
diff --git a/src/plugins/wp/share/why3/frama_c_wp/sequence.mlw b/src/plugins/wp/share/why3/frama_c_wp/sequence.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..4d364de7ddd4f7207d7db9a0ca4110079ad774a2
--- /dev/null
+++ b/src/plugins/wp/share/why3/frama_c_wp/sequence.mlw
@@ -0,0 +1,289 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** {1 Finite Sequences}
+
+ This modules provides a persistent array interface to lists.
+ It is typically used to model byte arrays of COSMO implementation.
+*)
+
+module Seq
+
+ use int.Int
+ use int.MinMax
+ use option.Option
+ use list.ListRich as L
+
+ (** {2 Definition}
+
+ A sequence `s` is defined by its size `n = length s` and its elements
+ `s[i]` with `0 <= i < n`.
+
+ All other operations on sequences are defined
+ in terms of the length and elements of the returned sequences.
+ *)
+
+ type seq 'a = L.list 'a
+
+ (** Length of a sequence. *)
+ let function length (u : seq 'a) = L.length u
+ meta coercion function length
+
+ (** Elements of a sequence. *)
+ let rec function ([]) (u : seq 'a) (k : int) : 'a
+ requires { 0 <= k < u }
+ ensures { L.nth k u = Some result }
+ (*proof*)
+ variant { u }
+ = match u with L.Cons x w -> if k = 0 then x else w[k-1] end
+ (*qed*)
+
+ lemma head: forall x:'a, u. (L.Cons x u)[0] = x
+ lemma tail: forall x:'a, u k. 0 < k <= length u -> (L.Cons x u)[k] = u[k-1]
+
+ (** Definitionnal equality: `u == v` states that sequences `u` and `v` have
+ the same length and same elements. *)
+ predicate (==) (u v : seq 'a) =
+ length u = length v /\ forall k. 0 <= k < u -> u[k] = v[k]
+
+ (** Equal lists are definitionnaly equals. *)
+ lemma reflexivity : forall u : seq 'a. u == u
+
+ (** Definitionnaly equal lists _are_ equals. *)
+ let rec lemma extensivity (a b : seq 'a)
+ requires { a == b }
+ ensures { a = b }
+ (*proof*)
+ variant { a, b }
+ = match a, b with
+ | L.Cons _ a' , L.Cons _ b' -> extensivity a' b'
+ | _ -> ()
+ end
+ (*qed*)
+
+ (** Functional equality. *)
+ let rec equal (eq : 'a -> 'a -> bool) (u v : seq 'a) : bool
+ requires { forall x y. L.mem x u -> L.mem y v -> (eq x y <-> x = y) }
+ ensures { result <-> u = v }
+ (*proof*)
+ variant { u, v }
+ = match u, v with
+ | L.Cons x u', L.Cons y v' -> eq x y && equal eq u' v'
+ | L.Nil, L.Nil -> true
+ | _ -> false
+ end
+ (*qed*)
+
+ (** {2 Constructors}
+
+ Helper functions for constructing sequences.
+ *)
+
+ (** Empty sequence of length `0`. *)
+ let constant empty : seq 'a = L.Nil
+
+ (** Singleton sequence with a unique element. *)
+ let function elt (e : 'a) : seq 'a = L.Cons e L.Nil
+
+ (** Head element *)
+ let function hd (s : seq 'a) : 'a
+ requires { 0 < s.length }
+ ensures { result = s[0] }
+ (*proof*) = match s with L.Cons x _ -> x end (*qed*)
+
+ (** Tail element *)
+ let function tl (s : seq 'a) : 'a
+ requires { 0 < s.length }
+ ensures { result = s[ s.length - 1 ] }
+ (*proof*) = s[ s.length - 1 ] (*qed*)
+
+ (** `create e n` returns a sequence of length `n` filled with `e` elements. *)
+ let rec function create (e : 'a) (n : int) : seq 'a
+ requires { 0 <= n }
+ ensures { length result = n }
+ ensures { forall k. 0 <= k < result -> result[k] = e }
+ (*proof*)
+ variant { n }
+ = if n > 0 then L.Cons e (create e (n-1)) else L.Nil
+ (*qed*)
+
+ (** `reset e s` returns a sequence of same length `s` filled with `e` elements. *)
+ let function reset (e : 'a) (s : seq 'b) : seq 'a = create e s.length
+
+ (** `init f a b` returns the sequence of elements `f i` for `a <= i < b`. *)
+ let rec function init (f : int -> 'a) (a b : int) : seq 'a
+ requires { a <= b }
+ ensures { length result = b-a }
+ ensures { forall k. 0 <= k < result -> result[k] = f (a+k) }
+ (*proof*)
+ variant { b-a }
+ = if a < b then L.Cons (f a) (init f (a+1) b) else L.Nil
+ (*qed*)
+
+ (** `map f s` applies `f` to all elements f `s` *)
+ let rec function map (f : 'a -> 'b) (s : seq 'a) : seq 'b
+ ensures { length result = length s }
+ ensures { forall k. 0 <= k < result -> result[k] = f s[k] }
+ (*proof*)
+ variant { s }
+ = match s with L.Nil -> L.Nil | L.Cons x xs -> L.Cons (f x) (map f xs) end
+ (*qed*)
+
+ (** {2 Slices}
+
+ Sequences are commonly operated by a slice of their elements.
+ By convention, a slice `i..j` of elements denotes the range of elements
+ from `i` (_included_) to `j` (_excluded_), hence the range of indices `k`
+ such that `i <= k < j`.
+
+ The slice of all elements of a sequence of size `n` is then `0..n`, and
+ we also denote slice `0..i` by `..i` and slice `i..n` by `i..`.
+ Slice operations are properly defined only for a valid range of indices.
+
+ The dual operation of slice is the concatenation, here denoted by `(++)`.
+ *)
+
+ (** `u ++ v` is the concatenation of `u` and `v`,
+ where `u` elements comes first, and `v` elements follows. *)
+ let rec function (++) (u v : seq 'a) : seq 'a
+ ensures { length result = length u + length v }
+ ensures { forall k. 0 <= k < u -> result[k] = u[k] }
+ ensures { forall k. u <= k < result -> result[k] = v[k - u] }
+ (*proof*)
+ variant { u }
+ = match u with L.Nil -> v | L.Cons x w -> L.Cons x (w ++ v) end
+ (*qed*)
+
+ (** `u[i..j]` is the slice of `u` elements
+ from index `i` (_included_) to index `j` (_excluded_). *)
+ let rec function ([..]) (u : seq 'a) (i j : int) : seq 'a
+ requires { 0 <= i <= j <= u }
+ ensures { length result = j-i }
+ ensures { forall k. 0 <= k < result -> result[k] = u[i+k] }
+ (*proof*)
+ variant { u }
+ = match u with
+ | L.Nil -> L.Nil
+ | L.Cons x w ->
+ if 0 < i then w[i-1..j-1] else
+ if 0 < j then L.Cons x w[0..j-1]
+ else L.Nil
+ end
+ (*qed*)
+
+ (** `u[..i]` is the slice of `u` elements up to index `i` (_excluded_). *)
+ let function ([.._]) (u : seq 'a) (i : int) : seq 'a
+ requires { 0 <= i <= u }
+ ensures { length result = i }
+ ensures { forall k. 0 <= k < result -> result[k] = u[k] }
+ = u[0..i]
+
+ (** `u[i..]` is the slice of `u` elements from index `i` (_included_). *)
+ let function ([_..]) (u : seq 'a) (i : int) : seq 'a
+ requires { 0 <= i <= u }
+ ensures { result = u - i }
+ ensures { forall k. 0 <= k < result -> result[k] = u[i+k] }
+ = u[i..length u]
+
+ (** This property illustrates the duality of slice & concat. *)
+ goal split: forall u : seq 'a, i.
+ 0 <= i <= u ->
+ u[..i] ++ u[i..] = u
+ (*proof*)
+ by u[..i] ++ u[i..] == u
+ (*qed*)
+
+ (** This property illustrates the duality of slice & concat. *)
+ goal fullsplit: forall u : seq 'a, i j.
+ 0 <= i <= j <= u ->
+ u[..i] ++ u[i..j] ++ u[j..] = u
+ (*proof*)
+ by u[..i] ++ u[i..j] ++ u[j..] == u
+ (*qed*)
+
+ (** Tail insertion *)
+ let function (+.) (s : seq 'a) (e : 'a) : seq 'a
+ ensures { length result = length s + 1 }
+ ensures { forall k. 0 <= k < s -> result[k] = s[k] }
+ ensures { result[ s ] = e }
+ (*proof*) = s ++ elt e (*qed*)
+
+ (** Head insertion *)
+ let function (.+) (e : 'a) (s : seq 'a) : seq 'a
+ ensures { length result = length s + 1 }
+ ensures { forall k. 0 <= k < s -> result[1+k] = s[k] }
+ ensures { result[ 0 ] = e }
+ (*proof*) = elt e ++ s (*qed*)
+
+ (** {2 Updates & Copies} *)
+
+ (** `u[i<-x]` returns a copy of the sequence `u` where the element `u[i]`
+ has been replaced by `x`. *)
+ let rec function ([<-]) (u : seq 'a) (i : int) (x : 'a) : seq 'a
+ requires { 0 <= i < u }
+ ensures { length result = length u }
+ ensures { forall k. 0 <= k < result -> result[k] = if k=i then x else u[k] }
+ (*proof*)
+ variant { u }
+ = match u with L.Cons x0 w ->
+ if i = 0 then L.Cons x w else L.Cons x0 w[ i-1 <- x ]
+ end
+ (*qed*)
+
+ (** `memcpy u i v j n` returns a copy of `u` where the slice `u[i..i+n]` has been
+ replaced with the slice `v[j..j+n]` (last excluded). *)
+ let function memcpy (u : seq 'a) (i : int) (v : seq 'a) (j : int) (n : int)
+ requires { 0 <= i <= i+n <= u }
+ requires { 0 <= j <= j+n <= v }
+ ensures { length result = length u }
+ ensures { forall k. 0 <= k < i -> result[k] = u[k] }
+ ensures { forall k. i <= k < i+n -> result[k] = v[j+k-i] }
+ ensures { forall k. i+n <= k < u -> result[k] = u[k] }
+ = u[..i] ++ v[j..j+n] ++ u[i+n..]
+
+ (** `havoc u v p n` asserts that sequences `u` and `v` have identical elements
+ but elements in range `p..p+n` (last excluded). *)
+ predicate havoc (u v: seq 'a) (p n : int) =
+ u.length = v.length /\
+ (forall k. 0 <= k < p -> u[k] = v[k]) /\
+ (forall k. p+n <= k < u -> u[k] = v[k])
+
+end
+
+(** {2 Sequence Codomain} *)
+
+module Codomain
+
+ use int.Int
+ use set.Set
+ use Seq
+
+ let rec ghost function codomain (s : seq 'a) : set 'a
+ ensures { forall v. Set.mem v result <-> exists i. 0 <= i < s /\ s[i] = v }
+ (*proof*)
+ variant { s.length }
+ = if s.length = 0 then Set.empty else
+ let k = s.length-1 in
+ Set.add s[k] (codomain s[0..k])
+ (*qed*)
+
+end
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 2bbd925602a696a9392e6ad30bc658fe55cffb5d..05bbeb82931e3d9e35a63fa248c8b3268d120642 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -92,6 +92,18 @@ why3.import := "frama_c_wp.memaddr.MemAddr";
library memory: memaddr
why3.import := "frama_c_wp.memory.Memory";
+library membytes: memaddr
+why3.import += "frama_c_wp.membytes.ValueCodec";
+why3.import += "frama_c_wp.membytes.InitCodec";
+why3.import += "frama_c_wp.membytes.Offset";
+why3.import += "frama_c_wp.membytes.RWBytes";
+why3.import += "frama_c_wp.membytes.ValueBlockRW";
+why3.import += "frama_c_wp.membytes.InitBlockRW";
+why3.import += "frama_c_wp.membytes.MemBytes";
+
+library sequence: sequence
+why3.import := "frama_c_wp.sequence.Seq";
+
library sqrt: cmath
why3.import += "real.Square";
why3.import += "frama_c_wp.cmath.Square";